Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 59 additions & 0 deletions .github/ISSUE_SPECS/220-route-fold-corpus-differential.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
# 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).
## 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.

## 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.

## 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.
280 changes: 280 additions & 0 deletions crates/graph/src/program/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<Vec<GraphNodeId>> = (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");
Expand All @@ -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,
Expand All @@ -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<u32, (usize, usize)>,
runs: &[Vec<Vec<usize>>],
routes: &std::collections::BTreeMap<GraphNodeId, crate::RouteTransform>,
) -> Option<crate::runtime::RouteFoldObservation> {
let writer = |index: usize, buffer: BufferRef| {
(0..index)
.rev()
.find(|prior| program.ops[*prior].output == buffer)
};
let incoming: Vec<Vec<Option<usize>>> = 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::<Vec<_>>()
|| 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<GraphNodeId, crate::RouteTransform> {
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}"
);
}
}
Loading
Loading