///|
priv struct ScopedExtensionArcV4 {
  from : Int32
  to : Int32
  path : Array[Int32]
}

///|
priv struct ScopedExtensionWorkV4 {
  arcs : Array[ScopedExtensionArcV4]
  adjacency : Array[Array[Int32]]
  budget : ScopedSearchBudgetV4
  color : FixedArray[Int32]
  stack_nodes : Array[Int32]
  stack_arcs : Array[Int32]
  mut found : Array[Int32]
}

///|
fn scoped_extension_add_v4(
  arcs : Array[ScopedExtensionArcV4],
  adjacency : Array[Array[Int32]],
  pairs : Map[(Int32, Int32), Int32],
  from : Int32,
  to : Int32,
  path : Array[Int32],
) -> Int32 {
  match pairs.get((from, to)) {
    Some(position) => {
      if path.length() < arcs[position].path.length() {
        arcs[position] = { from, to, path, }
      }
      position
    }
    None => {
      let position = arcs.length()
      arcs.push({ from, to, path, })
      adjacency[from].push(position)
      pairs[(from, to)] = position
      position
    }
  }
}

///|
fn scoped_extension_visit_v4(
  work : ScopedExtensionWorkV4,
  node : Int32,
) -> Unit {
  if !scoped_charge_state_v4(work.budget) {
    return
  }
  work.color[node] = 1
  work.stack_nodes.push(node)
  for position in work.adjacency[node] {
    if !scoped_charge_edge_v4(work.budget) {
      return
    }
    let arc = work.arcs[position]
    if work.color[arc.to] == 0 {
      work.stack_arcs.push(position)
      scoped_extension_visit_v4(work, arc.to)
      let _ = work.stack_arcs.pop()
      if work.budget.limited || !work.found.is_empty() {
        return
      }
    } else if work.color[arc.to] == 1 {
      let mut start = 0
      while work.stack_nodes[start] != arc.to {
        start += 1
      }
      for index in start.. Json {
  if cycle.is_empty() {
    return Json::null()
  }
  let original : Array[Int32] = []
  for position in cycle {
    for edge in arcs[position].path {
      original.push(edge)
    }
  }
  let result = scoped_cycle_witness_v4(graph, original, rules)
  let fields = object_fields_unchecked_v3(result)
  fields["kind"] = Json("source-bound-scoped-extension-cycle")
  fields["minimality"] = Json(
    "simple virtual cycle in Ext; the expanded original closed walk may repeat vertices",
  )
  fields["virtualSteps"] = Json(
    cycle.map(position => {
      let arc = arcs[position]
      (
        {
          "from": Json(graph.nodes[arc.from]),
          "to": Json(graph.nodes[arc.to]),
          "originalSteps": Json(
            arc.path.map(index => graph.edges[index].original),
          ),
          "composition": Json(if arc.path.length() == 1 { "I" } else { "I;A" }),
        } : Json)
    }),
  )
  fields["formula"] = Json(
    "Ext(I,A)=I union (I;A); each I may be an explicit process/realtime edge in the chosen context",
  )
  result
}

///|
/// Fixed Elle sequential-extension is one I step, optionally one A step, not
/// I union A and not a transitive closure. Derived self-loops are retained.
pub fn search_si_extension_v4(
  graph : ScopedDependencyGraphV4,
  rule_set~ : ScopedRuleSetV4,
  order_context~ : ScopedOrderContextV4 = ScopedDataOnly,
  max_states~ : Int32 = 100000,
  max_edge_checks~ : Int32 = 1000000,
) -> ScopedSearchResultV4 {
  let budget : ScopedSearchBudgetV4 = {
    max_states,
    max_edges: max_edge_checks,
    states: 0,
    edge_checks: 0,
    limited: false,
    reason: "complete",
  }
  let valid = scoped_budget_valid_v4(max_states, max_edge_checks)
  let arcs : Array[ScopedExtensionArcV4] = []
  let adjacency : Array[Array[Int32]] = []
  for _ in graph.nodes {
    adjacency.push([])
  }
  let pairs : Map[(Int32, Int32), Int32] = Map([])
  let mut composed = 0
  let work : ScopedExtensionWorkV4 = {
    arcs,
    adjacency,
    budget,
    color: FixedArray::make(graph.nodes.length(), 0),
    stack_nodes: [],
    stack_arcs: [],
    found: [],
  }
  if valid {
    for position, edge in graph.edges {
      if !scoped_charge_edge_v4(budget) {
        break
      }
      if !(scoped_is_ww_v4(edge) ||
        scoped_is_wr_v4(edge) ||
        scoped_order_allowed_v4(edge, order_context)) {
        continue
      }
      let _ = scoped_extension_add_v4(
        arcs,
        adjacency,
        pairs,
        edge.from,
        edge.to,
        [position],
      )
      for next in graph.adjacency[edge.to] {
        if !scoped_charge_edge_v4(budget) {
          break
        }
        let target = graph.edges[next]
        if !scoped_is_rw_v4(target) {
          continue
        }
        composed += 1
        let index = scoped_extension_add_v4(
          arcs,
          adjacency,
          pairs,
          edge.from,
          target.to,
          [position, next],
        )
        if edge.from == target.to {
          work.found = [index]
          break
        }
      }
      if budget.limited || !work.found.is_empty() {
        break
      }
    }
    if !budget.limited && work.found.is_empty() {
      for node in 0.. Bool {
  supplied ==
  search_si_extension_v4(
    graph,
    rule_set~,
    order_context~,
    max_states~,
    max_edge_checks~,
  ).record
}