///|
/// A concrete original-row serial certificate, not a relabelled SI certificate.
fn model_relation_serial_completion_v4(
  history : HistoryV4,
  source : ModelSourceV4,
  orders : ModelOrdersV4,
  context : ScopedOrderContextV4,
  options : ModelOptionsV4,
  d_rule : ModelRuleV4,
) -> ModelRuleV4 {
  let id = "completion/original-row-serial/" + scoped_context_name_v4(context)
  if source.profile != "captured-relation-row-slots/v1" ||
    options.completion_policy != ModelObservationOnlyCompletion ||
    !model_observation_premises_v4(source, true) ||
    d_rule.status != "checked-compatible" {
    return model_rule_v4(
      id, "pending", "requires a closed atomic-row program, checked snapshot/own overlay premises and an acyclic complete D in the selected original-order context",
    )
  }
  let graph = match
    scoped_dependency_graph_v4(
      source.nodes,
      source.edges,
      order_edges=orders.edges,
      data_complete=true,
      process_complete=orders.process_complete,
      realtime_complete=orders.realtime_complete,
    ) {
    Ok(g) => g
    Err(reason) => return model_rule_v4(id, "unknown", reason)
  }
  if !scoped_context_complete_v4(graph, context) {
    return model_rule_v4(
      id, "unknown", "necessary original order context is incomplete",
    )
  }
  let budget : ScopedSearchBudgetV4 = {
    max_states: options.max_states,
    max_edges: options.max_edge_checks,
    states: 0,
    edge_checks: 0,
    limited: false,
    reason: "complete",
  }
  let indegree = FixedArray::make(graph.nodes.length(), 0)
  let adjacency : Array[Array[Int32]] = Array::makei(graph.nodes.length(), _ => {
    []
  })
  for position, edge in graph.edges {
    if !scoped_charge_edge_v4(budget) {
      break
    }
    if edge.data_kind is Some(_) || scoped_order_allowed_v4(edge, context) {
      adjacency[edge.from].push(position)
      indegree[edge.to] += 1
    }
  }
  let queue : Array[Int32] = []
  for node in 0..