Skip to content

engine: phase_element_order builds the SCC element graph from per-variable mini-slots -- zero cross-member edges + unsound resolution of genuine multi-variable element cycles (masked by members.len()!=1; Phase 2 Subcomponent B must remove mask) #575

Description

@bpowers

Summary

phase_element_order (src/simlin-engine/src/db_dep_graph.rs:839) builds the SCC-induced element graph by keying a slot_to_node map on raw Expr::AssignCurr slot numbers, then matching each RHS read slot against that map. But the exprs it consumes come from var_phase_lowered_exprs_prod, which lowers each member in its own fresh per-variable mini-layout (every member's own variable sits at the same mini-slot, base = crate::vm::IMPLICIT_VAR_COUNT = 4 for the root model). Those slots are not model-global, cross-member-comparable absolute offsets.

For a single-member SCC this is correct (the one member reads its own earlier elements within ONE mini-layout). For any multi-member SCC it builds ZERO cross-member edges, producing (a) a wrong non-interleaved topological order and (b) -- fatally -- resolving a genuine multi-variable element cycle as acyclic. (b) is unsound: it violates the element-cycle-resolution AC4 loud-safe hard rule and the in-code invariant at db_dep_graph.rs that the resolver is "never an unsound one".

This is currently masked, not absent: refine_scc_to_element_verdict (db_dep_graph.rs:1023) short-circuits if members.len() != 1 { return SccVerdict::Unresolved; } before ever calling phase_element_order, and resolve_recurrence_sccs sets has_unresolved = true for multi-variable SCCs. So today only single-member SCCs reach phase_element_order. Phase 2 Subcomponent B (Task 6) of the element-cycle-resolution plan must remove that members.len() != 1 mask to resolve multi-variable element-acyclic SCCs -- at which point this defect becomes a live silent miscompilation unless fixed first.

Severity: HIGH -- latent unsoundness. With the mask removed and no fix, genuine circular-dependency models would silently miscompile (resolved instead of CircularDependency), and multi-member element-acyclic recurrences (e.g. C-LEARN's ce/ecc interleave) would get a wrong, non-reproducing per-element order.

Root cause (verified against the code)

var_phase_lowered_exprs_prod discards the per-member symbolic map and returns per-variable mini-slots

  • var_phase_lowered_exprs_prod (src/simlin-engine/src/db_dep_graph.rs:575-638) calls lower_var_fragment per member and returns only phase_var.ok().map(|v| v.ast) (db_dep_graph.rs:633) -- it discards the per-member rmap (ReverseOffsetMap).
  • lower_var_fragment (src/simlin-engine/src/db_var_fragment.rs:532-877) builds a fresh per-variable mini-layout:
    • mini_offset starts at crate::vm::IMPLICIT_VAR_COUNT (= 4 for the root model) -- db_var_fragment.rs:704-705.
    • the variable itself is placed FIRST: offset: mini_offset (db_var_fragment.rs:807), then mini_offset += var_size (db_var_fragment.rs:812). So every member's own variable sits at slot 4 in its own layout.
    • then its own deps (db_var_fragment.rs:838,843), then implicit module vars (db_var_fragment.rs:851,857).
    • rmap = ReverseOffsetMap::from_layout(&mini_layout) (db_var_fragment.rs:877) is the per-variable symbolic map -- and is not returned by var_phase_lowered_exprs_prod.

So Expr::AssignCurr slot operands are per-variable mini-slots (every member's own variable at slot 4; that member's private deps at 7,8,9,...), NOT model-global cross-member-comparable absolute slots.

phase_element_order keys edges on raw mini-slots

phase_element_order (src/simlin-engine/src/db_dep_graph.rs:839-912):

  • builds slot_to_node: HashMap<usize,(member,element)> keyed by the raw AssignCurr write slot (db_dep_graph.rs:858-871), then
  • builds edges by collect_read_slots(rhs, ...) and matching each read slot against slot_to_node (db_dep_graph.rs:876-903).

For a multi-member SCC:

  • (a) write-slot collision: every member's AssignCurr write slots are 4,5,6,... in its own mini-layout, so slot_to_node only retains the last-processed member (later inserts clobber earlier members' identical keys).
  • (b) cross-member reads miss: a member's RHS reference to another member resolves to the reading member's private dep mini-slots (7,8,9,... in that member's layout), which are absent from slot_to_node.

Net: zero cross-member edges are built.

Observed consequences (empirically probed by the Subcomponent B implementor; probe reverted, tree clean)

  • phase_element_order(ce <-> ecc, Dt) for test/sdeverywhere/models/ref/ref.mdl (ce[t1]=1; ce[tNext]=ecc[tPrev]+1; ecc[t1]=ce[t1]+1; ecc[tNext]=ce[tNext]+1) returns Some([(ce,0),(ce,1),(ce,2),(ecc,0),(ecc,1),(ecc,2)]) -- no cross-member edges, so a wrong non-interleaved order that does NOT reproduce ref.dat (ce = 1,3,5; ecc = 2,4,6). Element-cycle-resolution AC2.1 / AC2.2 would fail.
  • phase_element_order(a <-> b, Dt) for a genuine multi-variable element cycle a[i]=b[i]; b[i]=a[i] returns Some([(a,0),(a,1),(b,0),(b,1)]) instead of None -- it RESOLVES a genuine circular dependency. This is unsound: violates element-cycle-resolution AC4 loud-safe and the db_dep_graph.rs "never an unsound one" invariant.

Why it is currently safe (mask, not absence)

refine_scc_to_element_verdict (db_dep_graph.rs:1023) returns SccVerdict::Unresolved for members.len() != 1 before calling phase_element_order (commented "Subcomponent A scope: only single-variable self-recurrence resolves"), and resolve_recurrence_sccs sets has_unresolved = true for multi-variable SCCs before the builder. So only single-member SCCs reach phase_element_order (where the single member reads its own earlier elements within ONE mini-layout -- correct). Phase 1's passing tests (resolve_dt_scalar_two_cycle_is_unresolved, etc.) pass only because of this short-circuit, not because phase_element_order is correct for multi-member SCCs.

When it becomes live / required fix direction

Phase 2 Subcomponent B (Task 6) of docs/implementation-plans/2026-05-18-element-cycle-resolution/ must resolve multi-variable element-acyclic SCCs, which requires removing the members.len() != 1 mask at db_dep_graph.rs:1023. Before/while removing it:

  1. Rebuild the cross-member element graph from symbolic references (SymVarRef{name, element_offset} resolved via each member's rmap / ReverseOffsetMap), not raw mini-slots. var_phase_lowered_exprs_prod (or a new accessor) must surface each member's rmap / compiled symbolic fragment rather than discarding it (today it returns only v.ast).
  2. The combined-fragment interleave (plan Tasks 4/5) must likewise operate at the symbolic PerVarBytecodes / SymVarRef layer. The plan's Design deviation edit variable names #1 ("AssignCurr first operand = absolute slot offset") is verified FALSE -- the operands are per-variable mini-slots, base IMPLICIT_VAR_COUNT, every member's own var at slot 4. The plan revision must correct this.
  3. The single-member path should become the N=1 case of the corrected symbolic builder, preserving all Phase 1 regression guards (resolve_dt_scalar_two_cycle_is_unresolved, the dt cross-check dt_cycle_sccs_engine_consistent, etc.).

Components affected

  • src/simlin-engine/src/db_dep_graph.rs -- phase_element_order (:839-912; slot_to_node build :858-871, edge build :876-903), var_phase_lowered_exprs_prod (:575-638, the v.ast-only return at :633 that discards the per-member rmap), refine_scc_to_element_verdict (the members.len() != 1 mask at :1023), resolve_recurrence_sccs (sets has_unresolved for multi-var SCCs).
  • src/simlin-engine/src/db_var_fragment.rs -- lower_var_fragment (:532-877; per-variable mini_offset start :704-705, self placed first :807/:812, deps :838/:843, implicit module vars :851/:857, rmap = ReverseOffsetMap::from_layout(&mini_layout) :877).
  • docs/implementation-plans/2026-05-18-element-cycle-resolution/phase_02.md -- Design deviation edit variable names #1 (verified false; must be corrected), Tasks 4/5 (combined-fragment interleave must be symbolic, not slot-based), Task 6 (removing the members.len() != 1 mask is gated on this fix). Also phase_02_spike_findings.md.

Relationship to existing issues (DISTINCT, not duplicates)

Discovery context

Discovered during Phase 2 Subcomponent B of the element-level cycle-resolution work (branch clearn-hero-model, HEAD ~07b513b7). Verified directly against the code by the orchestrator and empirically probed by the Subcomponent B implementor (probe reverted; working tree clean). Flagged for explicit tracking per the project's "Tracking Discovered Issues" guidance (CLAUDE.md). Reference: docs/implementation-plans/2026-05-18-element-cycle-resolution/phase_02.md (Design deviation #1, Tasks 4/5/6), phase_02_spike_findings.md, and the in-code functions cited above.

Metadata

Metadata

Assignees

No one assigned

    Labels

    engineIssues with the rust-based simulation engine

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions