From 27bae4c659359256e82a525028994446555bf086 Mon Sep 17 00:00:00 2001 From: BL Date: Fri, 11 Sep 2026 01:25:22 +0000 Subject: [PATCH 1/4] Scope bounded current implementation of #220 --- .../220-route-fold-corpus-differential.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 .github/ISSUE_SPECS/220-route-fold-corpus-differential.md diff --git a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md new file mode 100644 index 00000000..0970f29e --- /dev/null +++ b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md @@ -0,0 +1,19 @@ +# route_fold needs a corpus differential (the three shadowed clauses are schedule-order-dependent) + +## Approved current scope — 2026-09-11 + +Add a narrow test-support observation of the runtime's actual route-fold decisions and compare it with an independent model using the existing seeded graph corpus. Cover sole-readership, intervening master reads, and one-master retention, including bounded constructed valid program shapes where compiler schedule ordering otherwise shadows the clauses. Preserve production routing decisions and PCM. Add the requested comment guard for plain_route_gains/node_kind coupling. Reuse existing corpus infrastructure; no new benchmark framework or exhaustive fixture campaign. + +Own crates/graph/src/runtime.rs narrow test-support seam/comments and crates/graph/src/program/tests.rs (or existing directly relevant graph tests). No production route-fold algorithm, bind-error correction, policy, artifact pin or compiler edits. #221 must follow this issue's delivered coverage. + +Gates: focused graph corpus and existing route-fold tests; each named safety clause must have a discriminating physical negative control or an explicit evidence-based scope ruling before PASS. Avoid self-comparison: oracle cannot call the same predicate it verifies. Maintain accepted/refused coverage and stable ordering. Separate negative and positive build targets. Strict focused Clippy, relevant graph tests and required PR/main CI; no timing claim. If existing corpus cannot exercise the frozen contract with one bounded extension, report before building a new harness. + +Astra XHIGH scoping approved; user authorized execution. Astra LOW implements, Astra XHIGH independently verifies. Five attempts maximum; each coherent pass gets one adversarial verdict. Root checkpoints exact paths and pushes promptly when focused checks pass, before more implementation. At most two active issues: #220 and #162; #221 queued behind delivered #220. Isolated worktrees; no overlapping edits. Root/lane B owns artifact qualification and pinning. Preserve histories and failed evidence; never weaken gates or commit compiler-IR captures. + +Record actual argv/environment/source/exits/logs externally; pause green for root checkpoint. Stop on first unexpected failure and report for bounded correction. Required exact-head PR and main qualification plus upstream GitHub synchronization precede closure. Remove clean delivered worktrees after preserving evidence/history. Historical model names below are superseded by user routing. + +## Historical issue body + +Required follow-up F1 from strip Job 3's adversarial verification. The fold's three GREEN clauses (sole-readership of the last slot, the in-between master scan, one-master retain) are genuinely shadowed in every compilable session today — proven by five adversarially constructed shapes — but the shadowing rests on incidental deterministic-schedule facts (submix-destination edges sorting before output-destination routes; sidechain consumers scheduling before routes) that nothing pins. A scheduler-order change would make the sole-readership clause the only defense, with zero red tests. + +Fix: an M1-style `route_folds_over_program` corpus differential driving the runtime's own `route_fold` clause code over the seeded random-graph corpus (house precedent: #208's scatter_redirects_over_program, which this same round demanded and landed). Must land BEFORE the next change in the route-fold/mixdown class. Also fold in a comment-level guard for the `plain_route_gains`/`node_kind` cascade coupling (F7 residual). \ No newline at end of file From 9b00b42f09724ad238ce3c60d142cb2383e4c3be Mon Sep 17 00:00:00 2001 From: BL Date: Fri, 11 Sep 2026 01:30:46 +0000 Subject: [PATCH 2/4] Compare actual route-fold admission with independent program oracle (#220) --- .../220-route-fold-corpus-differential.md | 13 +- crates/graph/src/program/tests.rs | 280 ++++++++++++++++++ crates/graph/src/runtime.rs | 80 ++++- 3 files changed, 370 insertions(+), 3 deletions(-) diff --git a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md index 0970f29e..c12b4cd6 100644 --- a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md +++ b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md @@ -16,4 +16,15 @@ Record actual argv/environment/source/exits/logs externally; pause green for roo Required follow-up F1 from strip Job 3's adversarial verification. The fold's three GREEN clauses (sole-readership of the last slot, the in-between master scan, one-master retain) are genuinely shadowed in every compilable session today — proven by five adversarially constructed shapes — but the shadowing rests on incidental deterministic-schedule facts (submix-destination edges sorting before output-destination routes; sidechain consumers scheduling before routes) that nothing pins. A scheduler-order change would make the sole-readership clause the only defense, with zero red tests. -Fix: an M1-style `route_folds_over_program` corpus differential driving the runtime's own `route_fold` clause code over the seeded random-graph corpus (house precedent: #208's scatter_redirects_over_program, which this same round demanded and landed). Must land BEFORE the next change in the route-fold/mixdown class. Also fold in a comment-level guard for the `plain_route_gains`/`node_kind` cascade coupling (F7 residual). \ No newline at end of file +Fix: an M1-style `route_folds_over_program` corpus differential driving the runtime's own `route_fold` clause code over the seeded random-graph corpus (house precedent: #208's scatter_redirects_over_program, which this same round demanded and landed). Must land BEFORE the next change in the route-fold/mixdown class. Also fold in a comment-level guard for the `plain_route_gains`/`node_kind` cascade coupling (F7 residual). +## Astra LOW attempt 1 focused checkpoint + +Added an appended cfg(test) observation seam calling actual route_fold, an +independent backward-writer oracle in the existing seeded cohort corpus, and +one accepted plus three bounded valid-program guard controls. Production +predicates are unchanged; coupling comment replacement preserves line count. +Focused route-fold fixture, seeded cohort corpus and formatting passed. +Evidence: `/tmp/issue220-attempt1` actual argv/env/source/log/exit records. +Incidental lock ordering preserved externally and restored. Root checkpoints; +independent XHIGH validity/oracle review, three physical guard removals, focused +strict Clippy/broader graph tests and required PR/main qualification remain. diff --git a/crates/graph/src/program/tests.rs b/crates/graph/src/program/tests.rs index 3dd5c1e8..b3612582 100644 --- a/crates/graph/src/program/tests.rs +++ b/crates/graph/src/program/tests.rs @@ -1610,6 +1610,8 @@ fn bank_window_hoisting_preserves_dataflow_on_random_graphs() { #[test] fn cohort_chain_merging_preserves_dataflow_on_random_graphs() { let mut state = 0x0fed_cba9_8765_4321_u64; + let mut route_accepted = 0usize; + let mut route_refused = 0usize; let mut chained_graphs = 0usize; let mut merged_runs = 0usize; let mut redirected_lanes = 0usize; @@ -1748,6 +1750,40 @@ fn cohort_chain_merging_preserves_dataflow_on_random_graphs() { "graph {graph}: the runtime and the model disagree about which lanes redirect" ); + // Reuse the same seeded semantic graph, with output-stage banks whose last slots + // feed routes directly. Re-lower with these banks so their hoisting windows are valid. + let matrix_banks: Vec> = (0..4) + .map(|cohort| { + (0..track_count) + .filter(|track| cohort_of_track[*track] == cohort) + .map(|track| stage_node(&format!("t{track:02}"), TrackStage::PostMatrix)) + .collect() + }) + .filter(|members: &Vec<_>| members.len() > 1) + .collect(); + let route_program = + lower(&spec, &schedule, &levels, &delays, &matrix_banks).expect("route lowering"); + let route_lanes = member_lanes(&spec, &matrix_banks); + let route_runs = runs_in_runtime_order(&route_program, &route_lanes); + let routes = route_constants(&spec); + let expected = route_fold_model(&route_program, &spec, &route_lanes, &route_runs, &routes); + if expected.is_some() { + route_accepted += 1; + } else { + route_refused += 1; + } + assert_eq!( + crate::runtime::route_folds_over_program( + &route_program, + &spec, + &route_lanes, + &route_runs, + &routes + ), + expected, + "graph {graph}: route-fold decisions differ" + ); + // The narrow-window arm: every bank's own span, and no union across banks. let narrow = lower_with_per_bank_windows(&spec, &schedule, &levels, &delays, &banks) .expect("lowers"); @@ -1760,6 +1796,8 @@ fn cohort_chain_merging_preserves_dataflow_on_random_graphs() { unaware_divergences += 1; } } + assert!(route_accepted > 0, "route corpus must admit folds"); + assert!(route_refused > 0, "route corpus must refuse folds"); assert_eq!(chained_graphs, 3563, "the chained corpus moved"); assert_eq!( merged_runs, 3752, @@ -1782,3 +1820,245 @@ fn cohort_chain_merging_preserves_dataflow_on_random_graphs() { "the number of graphs reaching the pre-#169 defect moved" ); } + +/// Independent route-fold oracle: resolve every input backwards to its last writer, then +/// group complete bank lanes by their unique destination. No runtime predicate is used. +/// These fixtures have route constants and bank memberships but no host bindings or observers. +fn route_fold_model( + program: &ExecutionProgram, + spec: &GraphSpec, + lanes: &std::collections::BTreeMap, + runs: &[Vec>], + routes: &std::collections::BTreeMap, +) -> Option { + let writer = |index: usize, buffer: BufferRef| { + (0..index) + .rev() + .find(|prior| program.ops[*prior].output == buffer) + }; + let incoming: Vec>> = program + .ops + .iter() + .enumerate() + .map(|(index, op)| { + program + .inputs_of(op) + .iter() + .map(|input| writer(index, input.buffer)) + .collect() + }) + .collect(); + let mut uses = vec![Vec::new(); program.ops.len()]; + for (index, op) in program.ops.iter().enumerate() { + for producer in incoming[index] + .iter() + .copied() + .flatten() + .chain(op.sidechain.and_then(|input| writer(index, input.buffer))) + { + uses[producer].push(index); + } + } + let mut groups = Vec::new(); + for (run, slots) in runs.iter().enumerate() { + if !lanes.contains_key(&program.ops[slots[0][0]].node) { + continue; + } + let mut group = Vec::new(); + for producer in slots.last().expect("last slot") { + let [route] = uses[*producer].as_slice() else { + break; + }; + let op = &program.ops[*route]; + let Some(transform) = routes.get(&spec.nodes[op.node as usize].id) else { + break; + }; + if lanes.contains_key(&op.node) + || op.sidechain.is_some() + || incoming[*route] != [Some(*producer)] + || program + .inputs_of(op) + .iter() + .any(|input| input.delay.is_some()) + || program.ops[*producer].output == program.output + || op.output == program.output + { + break; + } + group.push(( + run, + *route, + [ + transform.gain * transform.ll, + transform.gain * transform.lr, + transform.gain * transform.rl, + transform.gain * transform.rr, + ] + .map(f32::to_bits), + false, + )); + } + if group.len() == slots.last().expect("last slot").len() { + groups.push(group); + } + } + let first = groups.first()?.first()?.1; + let [master] = uses[first].as_slice() else { + return None; + }; + groups.retain(|group| group.iter().all(|lane| uses[lane.1] == [*master])); + let mut admitted: Vec<_> = groups.into_iter().flatten().collect(); + let opening = admitted.first()?.0; + let op = &program.ops[*master]; + if op.sidechain.is_some() + || lanes.contains_key(&op.node) + || program + .inputs_of(op) + .iter() + .any(|input| input.delay.is_some()) + || incoming[*master] != admitted.iter().map(|lane| Some(lane.1)).collect::>() + || admitted + .iter() + .any(|lane| program.ops[lane.1].output == op.output) + { + return None; + } + let closing = runs + .iter() + .position(|run| run.iter().flatten().any(|index| index == master))?; + if closing <= opening { + return None; + } + for slots in &runs[opening + 1..closing] { + for index in slots.iter().flatten() { + if admitted.iter().any(|lane| lane.1 == *index) { + continue; + } + let other = &program.ops[*index]; + if other.output == op.output + || program + .inputs_of(other) + .iter() + .copied() + .chain(other.sidechain) + .any(|input| { + input.buffer == op.output + || input.delay.is_some_and(|delay| delay.staging == op.output) + }) + { + return None; + } + } + } + admitted[0].3 = true; + Some((*master, admitted)) +} + +fn route_constants( + spec: &GraphSpec, +) -> std::collections::BTreeMap { + spec.nodes + .iter() + .enumerate() + .filter_map(|(index, node)| { + matches!(node.id, GraphNodeId::Route { .. }).then_some(( + node.id.clone(), + crate::RouteTransform { + gain: 0.75, + ll: 1.0 + index as f32 / 32.0, + lr: -0.125, + rl: 0.25, + rr: -0.5, + }, + )) + }) + .collect() +} + +/// Future topological orders can expose hazards currently hidden by canonical node ordering. +/// This tiny valid program owns distinct route buffers and reuses a dead source slot for the +/// master, just as arena colouring can. Additional readers execute after routes, so the plain +/// route and association guards cannot accidentally stand in for the reader guards. +#[test] +fn route_fold_shadowed_clauses_over_valid_programs() { + for hazard in 0..4 { + let ids = [ + stage_node("source", TrackStage::Input), + stage_node("a", TrackStage::PostMatrix), + stage_node("b", TrackStage::PostMatrix), + GraphNodeId::Route { route_id: gid("a") }, + GraphNodeId::Route { route_id: gid("b") }, + stage_node("observer", TrackStage::PostFader), + GraphNodeId::Output { + output_id: gid("out"), + }, + ]; + let (spec, _, _) = build(ids.iter().cloned().map(node).collect(), Vec::new()); + // source -> two bank lanes -> two routes -> master. The observer normally reads the + // source before its slot is reused. Hazard 1 reads a last-slot buffer; hazard 2 reads a + // route in addition to the master; hazard 3 reads the soon-to-be master's old contents. + let observer_input = match hazard { + 1 => 1, + 2 => 4, + _ => 0, + }; + let buffers = [0, 1, 2, 3, 4, 5, if hazard == 3 { 0 } else { 6 }]; + let input_buffers: [&[u32]; 7] = [&[], &[0], &[0], &[1], &[2], &[observer_input], &[3, 4]]; + let mut inputs = Vec::new(); + let mut ops = Vec::new(); + for index in 0..ids.len() { + let start = inputs.len() as u32; + inputs.extend(input_buffers[index].iter().map(|buffer| InputRef { + buffer: BufferRef(*buffer), + delay: None, + })); + ops.push(Op { + node: node_index(&spec, &ids[index]).expect("node"), + level: index as u64, + inputs: (start, inputs.len() as u32), + sidechain: None, + output: BufferRef(buffers[index]), + in_place: false, + }); + } + let mut node_buffer = vec![BufferRef(0); ids.len()]; + let mut node_op = vec![None; ids.len()]; + for (index, op) in ops.iter().enumerate() { + node_buffer[op.node as usize] = op.output; + node_op[op.node as usize] = Some(index as u32); + } + let program = ExecutionProgram { + ops: ops.into_boxed_slice(), + inputs: inputs.into_boxed_slice(), + delays: Box::new([]), + node_buffer: node_buffer.into_boxed_slice(), + node_op: node_op.into_boxed_slice(), + taps: Box::new([]), + buffers: 7, + output: BufferRef(buffers[6]), + }; + let lanes = [(program.ops[1].node, (0, 0)), (program.ops[2].node, (0, 1))] + .into_iter() + .collect(); + let runs = vec![ + vec![vec![0]], + vec![vec![1, 2]], + vec![vec![3]], + vec![vec![4]], + vec![vec![5]], + vec![vec![6]], + ]; + let routes = route_constants(&spec); + let expected = route_fold_model(&program, &spec, &lanes, &runs, &routes); + assert_eq!( + expected.is_some(), + hazard == 0, + "hazard {hazard}: independent oracle" + ); + assert_eq!( + crate::runtime::route_folds_over_program(&program, &spec, &lanes, &runs, &routes), + expected, + "hazard {hazard}" + ); + } +} diff --git a/crates/graph/src/runtime.rs b/crates/graph/src/runtime.rs index 21d23137..34976d67 100644 --- a/crates/graph/src/runtime.rs +++ b/crates/graph/src/runtime.rs @@ -3380,8 +3380,8 @@ const fn folded_route(transform: &RouteTransform) -> [f32; 4] { /// `parts` as it answers, so it can be asked exactly once and only while its op is being built. /// The fold has to know before any op is built -- it decides which ops are built at all -- so this /// restates the same cascade as a query, in the same precedence order, and returns `None` for -/// every arm that is not a plain route. A node that a host bound, that a bank owns, that a source -/// set fills or that carries a prepared effect is not a route however the session named it. +/// every arm that is not a plain route. Keep its exclusions coupled to new `node_kind` arms. +/// Bindings, banks, sources and effects take precedence regardless of the node's session name. fn plain_route_gains(parts: &RuntimeParts, node: &GraphNodeId, index: u32) -> Option<[f32; 4]> { if parts.source_inputs.contains(node) || parts.membership.contains_key(&index) @@ -6170,3 +6170,79 @@ mod tests { ); } } + +#[cfg(test)] +pub(crate) type RouteFoldObservation = (usize, Vec<(usize, usize, [u32; 4], bool)>); + +/// Observe the actual route-fold proof for unbound program fixtures. Constants are supplied by +/// the fixture; no admission predicate is replicated here. Like the scatter seam, run layout +/// comes from the independent program interpreter. Observers and prepared effects are absent. +#[cfg(test)] +pub(crate) fn route_folds_over_program( + program: &ExecutionProgram, + spec: &GraphSpec, + lanes: &BTreeMap, + runs: &[Vec>], + routes: &BTreeMap, +) -> Option { + let mut parts = RuntimeParts::new( + spec, + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Default::default(), + Vec::new(), + 1, + ); + parts.routes.clone_from(routes); + parts.membership = lanes + .iter() + .map(|(node, (bank, lane))| (*node, (Membership::Effect(*bank), *lane))) + .collect(); + let units: Vec<_> = runs + .iter() + .map(|run| { + let banked = lanes.contains_key(&program.ops[run[0][0]].node); + ( + if banked { + vec![Membership::Effect(0); run.len()] + } else { + Vec::new() + }, + run.iter().flatten().copied().collect(), + ) + }) + .collect(); + route_fold(program, spec, &parts, &units).map(|fold| { + let mut routes = fold.retired.into_iter().collect::>(); + // Retirement is a set, but lane order is render order, not op-index order. + let (readers, _) = op_dataflow(program); + let lanes = fold + .runs + .into_iter() + .flat_map(|(run, folded)| { + runs[run] + .last() + .expect("last slot") + .iter() + .zip(folded) + .map(|(producer, lane)| { + let route = readers[*producer][0]; + routes.retain(|retired| *retired != route); + (run, route, lane.coefficients.map(f32::to_bits), lane.store) + }) + .collect::>() + }) + .collect(); + assert!( + routes.is_empty(), + "every retired route belongs to a folded lane" + ); + (fold.master_op, lanes) + }) +} From 032dc98d6b4d45761a8b0ccacea9eea5c6cfc70a Mon Sep 17 00:00:00 2001 From: BL Date: Fri, 11 Sep 2026 01:38:25 +0000 Subject: [PATCH 3/4] Place test seam correctly and record precise route-fold evidence (#220) --- .../220-route-fold-corpus-differential.md | 18 ++ crates/graph/src/runtime.rs | 190 +++++++++--------- 2 files changed, 113 insertions(+), 95 deletions(-) diff --git a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md index c12b4cd6..43be4175 100644 --- a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md +++ b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md @@ -28,3 +28,21 @@ Evidence: `/tmp/issue220-attempt1` actual argv/env/source/log/exit records. Incidental lock ordering preserved externally and restored. Root checkpoints; independent XHIGH validity/oracle review, three physical guard removals, focused strict Clippy/broader graph tests and required PR/main qualification remain. + +## Attempt 1 review and bounded attempt 2 + +Astra XHIGH verified independent oracle, valid program controls and exact source +restoration. All three physical guard removals failed their intended assertion; +debug and release-unwind graph suites each passed71 tests. Strict Clippy then +failed items_after_test_module on the appended seam. Review also required the +stale no-red ledger to describe new evidence precisely. Root authorized moving +the seam before the existing test module and replacing the same25 comment lines. + +Astra LOW applied only those changes, preserving production line numbers and all +predicates/oracles. Formatting, locked strict all-target/all-feature Clippy and +both focused route/corpus tests passed. Existing non-fatal Clippy configuration +warnings remain unchanged. Evidence: `/tmp/issue220-attempt2`. Candidate retention +has evidence for exclusive route readership; its master-equality conjunct remains +subsumed by whole-list association, without independent mutation credit. Earlier +full-suite/control receipts: `/tmp/issue220-xhigh-review-9b00b42f/review.md`. +Independent exact-correction review and required PR/main qualification remain. diff --git a/crates/graph/src/runtime.rs b/crates/graph/src/runtime.rs index 34976d67..72ed7ce2 100644 --- a/crates/graph/src/runtime.rs +++ b/crates/graph/src/runtime.rs @@ -3545,26 +3545,26 @@ fn foldable_lane( /// * **the whole fold** -> `every_standing_workload_folds_one_route_per_track`, on a count. There /// is no output difference to see: that is the point of the counter. /// -/// Four clauses have **no** red test, and each is kept for a stated reason rather than a measured -/// one. Saying so is the point of writing the ledger down: +/// Historically four clauses had no red test in compiled-session fixtures. Issue #220 now +/// drives the actual proof over the seeded corpus and bounded valid lowered-program shapes. /// -/// * **sole readership of a chain's last slot.** Genuinely load-bearing -- a folded lane stops -/// writing that buffer, so a second reader would carry the previous block -- but *shadowed* in -/// every session a compiler can build. A second route from the same tap adds a summand the -/// master's input list has, so the association proof declines on length first; a sidechain from -/// that tap is read by an op scheduled *before* the route, so `readers[producer][0]` is not a -/// route and the plain-route clause declines instead. Dropping the clause reddens nothing, and -/// that is reported rather than dressed up. -/// * **nothing in between names the master.** No compiled session reaches the hazard, and the -/// reason is structural: the master's colour is the first colour the lowering frees, which is -/// track zero's input buffer, and track zero is always in the *opening* cohort -- whose ops the -/// scan excludes because they all precede the first master write. A later cohort naming the -/// master's slot is expressible in a lowered program and not in a session, exactly as -/// `scatter_target`'s compensation-delay clause is. -/// * **one master op for the whole plan.** A session whose tracks reduce into several submixes -/// could fold each submix separately; this folds one reduction or none. The proof would have to -/// be run per master and the chains partitioned between them, and no fixture in the tree needs -/// it. Dropping it is shadowed by the association proof's length check. +/// * **sole readership of a chain's last slot** -> +/// `route_fold_shadowed_clauses_over_valid_programs`, hazard 1. Removing the guard admits a +/// fold whose last-slot buffer still has another reader after its route. Compiled-session +/// ordering used to hide this: another route changed the association list, while a sidechain +/// reader scheduled before the route made the first reader fail the plain-route check. +/// The constructed order isolates the last-slot readership guard from those other refusals. +/// * **nothing in between names the master** -> +/// `route_fold_shadowed_clauses_over_valid_programs`, hazard 3. Removing the access check admits +/// a fold that overwrites a reused buffer before an intervening reader consumes its old value. +/// Existing compiled-session colouring hid this hazard in the opening cohort, which the scan +/// correctly excludes. The constructed program puts that reader in a later unit instead. +/// These are measured physical guard removals, not mutations of the independent oracle. +/// * **candidate retention requires exclusive route readership** -> +/// `route_fold_shadowed_clauses_over_valid_programs`, hazard 2. Removing the retain block admits +/// a route with an additional reader while the master's ordered contributors still match. +/// This does not independently prove the same-master equality conjunct: that conjunct remains +/// logically shadowed by the association proof. This implementation folds one reduction only. /// * **the master buffer is distinct from every folded buffer.** The colouring cannot hand the /// master a slot a folded lane still writes -- a chain's last slot is `program::is_dedicated` /// storage and is never returned to the free list -- so this is a construction check, in the @@ -4004,6 +4004,82 @@ fn cohort_runs( runs } +#[cfg(test)] +pub(crate) type RouteFoldObservation = (usize, Vec<(usize, usize, [u32; 4], bool)>); + +/// Observe the actual route-fold proof for unbound program fixtures. Constants are supplied by +/// the fixture; no admission predicate is replicated here. Like the scatter seam, run layout +/// comes from the independent program interpreter. Observers and prepared effects are absent. +#[cfg(test)] +pub(crate) fn route_folds_over_program( + program: &ExecutionProgram, + spec: &GraphSpec, + lanes: &BTreeMap, + runs: &[Vec>], + routes: &BTreeMap, +) -> Option { + let mut parts = RuntimeParts::new( + spec, + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Vec::new(), + Default::default(), + Vec::new(), + 1, + ); + parts.routes.clone_from(routes); + parts.membership = lanes + .iter() + .map(|(node, (bank, lane))| (*node, (Membership::Effect(*bank), *lane))) + .collect(); + let units: Vec<_> = runs + .iter() + .map(|run| { + let banked = lanes.contains_key(&program.ops[run[0][0]].node); + ( + if banked { + vec![Membership::Effect(0); run.len()] + } else { + Vec::new() + }, + run.iter().flatten().copied().collect(), + ) + }) + .collect(); + route_fold(program, spec, &parts, &units).map(|fold| { + let mut routes = fold.retired.into_iter().collect::>(); + // Retirement is a set, but lane order is render order, not op-index order. + let (readers, _) = op_dataflow(program); + let lanes = fold + .runs + .into_iter() + .flat_map(|(run, folded)| { + runs[run] + .last() + .expect("last slot") + .iter() + .zip(folded) + .map(|(producer, lane)| { + let route = readers[*producer][0]; + routes.retain(|retired| *retired != route); + (run, route, lane.coefficients.map(f32::to_bits), lane.store) + }) + .collect::>() + }) + .collect(); + assert!( + routes.is_empty(), + "every retired route belongs to a folded lane" + ); + (fold.master_op, lanes) + }) +} + #[cfg(test)] mod tests { use super::*; @@ -6170,79 +6246,3 @@ mod tests { ); } } - -#[cfg(test)] -pub(crate) type RouteFoldObservation = (usize, Vec<(usize, usize, [u32; 4], bool)>); - -/// Observe the actual route-fold proof for unbound program fixtures. Constants are supplied by -/// the fixture; no admission predicate is replicated here. Like the scatter seam, run layout -/// comes from the independent program interpreter. Observers and prepared effects are absent. -#[cfg(test)] -pub(crate) fn route_folds_over_program( - program: &ExecutionProgram, - spec: &GraphSpec, - lanes: &BTreeMap, - runs: &[Vec>], - routes: &BTreeMap, -) -> Option { - let mut parts = RuntimeParts::new( - spec, - Vec::new(), - Vec::new(), - Vec::new(), - Vec::new(), - Vec::new(), - Vec::new(), - Vec::new(), - Vec::new(), - Default::default(), - Vec::new(), - 1, - ); - parts.routes.clone_from(routes); - parts.membership = lanes - .iter() - .map(|(node, (bank, lane))| (*node, (Membership::Effect(*bank), *lane))) - .collect(); - let units: Vec<_> = runs - .iter() - .map(|run| { - let banked = lanes.contains_key(&program.ops[run[0][0]].node); - ( - if banked { - vec![Membership::Effect(0); run.len()] - } else { - Vec::new() - }, - run.iter().flatten().copied().collect(), - ) - }) - .collect(); - route_fold(program, spec, &parts, &units).map(|fold| { - let mut routes = fold.retired.into_iter().collect::>(); - // Retirement is a set, but lane order is render order, not op-index order. - let (readers, _) = op_dataflow(program); - let lanes = fold - .runs - .into_iter() - .flat_map(|(run, folded)| { - runs[run] - .last() - .expect("last slot") - .iter() - .zip(folded) - .map(|(producer, lane)| { - let route = readers[*producer][0]; - routes.retain(|retired| *retired != route); - (run, route, lane.coefficients.map(f32::to_bits), lane.store) - }) - .collect::>() - }) - .collect(); - assert!( - routes.is_empty(), - "every retired route belongs to a folded lane" - ); - (fold.master_op, lanes) - }) -} From ddd99eeb3bddfe641a88e2c0408ae5845b40dfe2 Mon Sep 17 00:00:00 2001 From: BL Date: Fri, 11 Sep 2026 01:41:32 +0000 Subject: [PATCH 4/4] Record independent route-fold coverage PASS (#220) --- .../ISSUE_SPECS/220-route-fold-corpus-differential.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md index 43be4175..ab6f3121 100644 --- a/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md +++ b/.github/ISSUE_SPECS/220-route-fold-corpus-differential.md @@ -46,3 +46,14 @@ has evidence for exclusive route readership; its master-equality conjunct remain subsumed by whole-list association, without independent mutation credit. Earlier full-suite/control receipts: `/tmp/issue220-xhigh-review-9b00b42f/review.md`. Independent exact-correction review and required PR/main qualification remain. + +## Independent Astra XHIGH attempt 2 PASS + +Reviewed032dc98d6b4d45761a8b0ccacea9eea5c6cfc70a. Seam relocation is byte-identical, +production locations/predicates and oracle unchanged;25-line ledger now states +exactly the evidence earned. Fresh formatting, strict Clippy and both focused +receipts passed; previous three physical controls and both71-test suites remain +applicable without repetition. Remote issue/spec/head parity and clean status +verified. Existing artifact product evidence remains applicable; required CI +must reproduce its pin. Review: `/tmp/issue220-xhigh-review-032dc98d/review.md`. +Only this evidence record follows; required PR/main qualification remains.