You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
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
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.
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() != 1before 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:
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).
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.
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).
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)
engine: element-cycle dt-recurrence SCC resolution uses no-input build_var_info wiring; Phase 2 must plumb real module_input_names before consuming ResolvedScc.element_order #573 (element-cycle dt-recurrence SCC resolution uses no-input build_var_info wiring; Phase 2 must plumb real module_input_names before consuming ResolvedScc.element_order): a wiring-correctness hazard -- whichbuild_var_info wiring (no-input &[] vs with-inputs &module_input_names) feeds SCC identification and per-element ordering. This issue is orthogonal: even with perfectly correct wiring, the cross-member element-graph construction in phase_element_order is structurally wrong for multi-member SCCs because it compares per-variable mini-slots as if they were model-global. Different mechanism, different failure (zero cross-member edges / unsound resolution vs. wrong SCC universe under input-cut edges).
No docs/tech-debt.md entry covers this (the cycle/SCC entries there -- LTM dedup / loop-partition keying / per-reference element graph -- are unrelated subsystems, not the element-cycle dt/init phase_element_order cross-member-edge construction).
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.
Summary
phase_element_order(src/simlin-engine/src/db_dep_graph.rs:839) builds the SCC-induced element graph by keying aslot_to_nodemap on rawExpr::AssignCurrslot numbers, then matching each RHS read slot against that map. But the exprs it consumes come fromvar_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.rsthat the resolver is "never an unsound one".This is currently masked, not absent:
refine_scc_to_element_verdict(db_dep_graph.rs:1023) short-circuitsif members.len() != 1 { return SccVerdict::Unresolved; }before ever callingphase_element_order, andresolve_recurrence_sccssetshas_unresolved = truefor multi-variable SCCs. So today only single-member SCCs reachphase_element_order. Phase 2 Subcomponent B (Task 6) of the element-cycle-resolution plan must remove thatmembers.len() != 1mask 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'sce/eccinterleave) would get a wrong, non-reproducing per-element order.Root cause (verified against the code)
var_phase_lowered_exprs_proddiscards the per-member symbolic map and returns per-variable mini-slotsvar_phase_lowered_exprs_prod(src/simlin-engine/src/db_dep_graph.rs:575-638) callslower_var_fragmentper member and returns onlyphase_var.ok().map(|v| v.ast)(db_dep_graph.rs:633) -- it discards the per-memberrmap(ReverseOffsetMap).lower_var_fragment(src/simlin-engine/src/db_var_fragment.rs:532-877) builds a fresh per-variable mini-layout:mini_offsetstarts atcrate::vm::IMPLICIT_VAR_COUNT(= 4 for the root model) --db_var_fragment.rs:704-705.offset: mini_offset(db_var_fragment.rs:807), thenmini_offset += var_size(db_var_fragment.rs:812). So every member's own variable sits at slot 4 in its own layout.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 byvar_phase_lowered_exprs_prod.So
Expr::AssignCurrslot 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_orderkeys edges on raw mini-slotsphase_element_order(src/simlin-engine/src/db_dep_graph.rs:839-912):slot_to_node: HashMap<usize,(member,element)>keyed by the rawAssignCurrwrite slot (db_dep_graph.rs:858-871), thencollect_read_slots(rhs, ...)and matching each read slot againstslot_to_node(db_dep_graph.rs:876-903).For a multi-member SCC:
AssignCurrwrite slots are 4,5,6,... in its own mini-layout, soslot_to_nodeonly retains the last-processed member (later inserts clobber earlier members' identical keys).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)fortest/sdeverywhere/models/ref/ref.mdl(ce[t1]=1; ce[tNext]=ecc[tPrev]+1; ecc[t1]=ce[t1]+1; ecc[tNext]=ce[tNext]+1) returnsSome([(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 reproduceref.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 cyclea[i]=b[i]; b[i]=a[i]returnsSome([(a,0),(a,1),(b,0),(b,1)])instead ofNone-- it RESOLVES a genuine circular dependency. This is unsound: violates element-cycle-resolution AC4 loud-safe and thedb_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) returnsSccVerdict::Unresolvedformembers.len() != 1before callingphase_element_order(commented "Subcomponent A scope: only single-variable self-recurrence resolves"), andresolve_recurrence_sccssetshas_unresolved = truefor multi-variable SCCs before the builder. So only single-member SCCs reachphase_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 becausephase_element_orderis 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 themembers.len() != 1mask atdb_dep_graph.rs:1023. Before/while removing it:SymVarRef{name, element_offset}resolved via each member'srmap/ReverseOffsetMap), not raw mini-slots.var_phase_lowered_exprs_prod(or a new accessor) must surface each member'srmap/ compiled symbolic fragment rather than discarding it (today it returns onlyv.ast).PerVarBytecodes/SymVarReflayer. 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, baseIMPLICIT_VAR_COUNT, every member's own var at slot 4. The plan revision must correct this.resolve_dt_scalar_two_cycle_is_unresolved, the dt cross-checkdt_cycle_sccs_engine_consistent, etc.).Components affected
src/simlin-engine/src/db_dep_graph.rs--phase_element_order(:839-912;slot_to_nodebuild :858-871, edge build :876-903),var_phase_lowered_exprs_prod(:575-638, thev.ast-only return at :633 that discards the per-memberrmap),refine_scc_to_element_verdict(themembers.len() != 1mask at :1023),resolve_recurrence_sccs(setshas_unresolvedfor multi-var SCCs).src/simlin-engine/src/db_var_fragment.rs--lower_var_fragment(:532-877; per-variablemini_offsetstart :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 themembers.len() != 1mask is gated on this fix). Alsophase_02_spike_findings.md.Relationship to existing issues (DISTINCT, not duplicates)
build_var_infowiring; Phase 2 must plumb realmodule_input_namesbefore consumingResolvedScc.element_order): a wiring-correctness hazard -- whichbuild_var_infowiring (no-input&[]vs with-inputs&module_input_names) feeds SCC identification and per-element ordering. This issue is orthogonal: even with perfectly correct wiring, the cross-member element-graph construction inphase_element_orderis structurally wrong for multi-member SCCs because it compares per-variable mini-slots as if they were model-global. Different mechanism, different failure (zero cross-member edges / unsound resolution vs. wrong SCC universe under input-cut edges).dt_cycle_sccs/dt_cycle_sccs_consistency_violationinstrumentation). This issue is a concrete production-code correctness defect in the element-graph builder itself (both dt and init paths route throughphase_element_orderviarefine_scc_to_element_verdict), not a gap in test instrumentation. An init cross-check (engine: no init-phase cycle instrumentation + engine-consistency cross-check (init analogue of dt_cycle_sccs / dt_cycle_sccs_consistency_violation) #574) would in fact help detect this defect once the mask is removed, but they are distinct work items: engine: no init-phase cycle instrumentation + engine-consistency cross-check (init analogue of dt_cycle_sccs / dt_cycle_sccs_consistency_violation) #574 is "build the harness", this is "the builder is unsound for N>=2 and must be rewritten symbolically before the mask comes off".docs/tech-debt.mdentry covers this (the cycle/SCC entries there -- LTM dedup / loop-partition keying / per-reference element graph -- are unrelated subsystems, not the element-cycle dt/initphase_element_ordercross-member-edge construction).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.