Witness-coverage gap surfaced by the #330 Phase 7 review (PR #338). This is the non-vacuity/witness axis, adjacent to #320 and #334 — not part of #330's InputsAgree decomposition.
The gap
root_soundness gained the premise rowsAligned : StepRowsAligned ziskTrace ziskStep …: at every step with a successor, the step's execution-bus producer entry is its own Main row's successor pc. For 62 of the 63 arms it is rfl. Only a two-row unaligned JALR lowering can violate it, because JalrLoweringRows permits finish = start + 1 and StepSound's JALR arm is indexed by finish.
No witness in the tree exercises it against a real two-row lowering. The only two-row JALR witness, RawProgramBindingJalrExpansionNonvacuity, is an all-empty execution (numInstructions = 0), so rowsAligned is vacuous there. jalrSpinRootSoundness does use the unaligned lowering, but the JALR is its last step, so rowsAligned is vacuous there too (it binds only where j + 1 < numInstructions).
So the premise is satisfiable in every checked-in instantiation without ever being tested against the configuration it exists to exclude.
Why this matters, stated precisely
This is not unsoundness. rowsAligned is a premise; a trace that violates it is simply outside the theorem. The issue is that we have no evidence about what the premise costs a real caller — whether an honest multi-instruction trace containing an unaligned JALR followed by another instruction can satisfy it at all.
If it cannot, that is worth knowing: it would mean root_soundness silently excludes a reachable program shape, and the right response is the discharge route rather than the premise.
What "done" looks like
A witness with an unaligned two-row JALR at a non-final step, instantiating root_soundness, with rowsAligned discharged non-vacuously — or a precise statement of why such a trace cannot be built, which would itself be the answer.
Note that #334 records the related problem that the remaining spin-trace witnesses carry hand-authored ind_width placeholders and are not usable for ProgramRowsBinding; a new witness here should not repeat that.
Relation to the discharge route
Separate from this. trust/defects.md's ZISK-MODEL-GAP-JALR-EXPANSION-STEP-ROW-INDEX records two retirement conditions:
- (a) prove an accepted trace cannot place an unaligned two-row expansion at a non-final step, discharging
rowsAligned from the trace instead of assuming it;
- (b) decouple the executed-step index from the physical Main-row index, so a multi-row lowering consumes one step.
Those are premise-discharge work and belong with the #330/#341 follow-on. This issue is only about coverage: does anything test the premise as it stands.
Witness-coverage gap surfaced by the #330 Phase 7 review (PR #338). This is the non-vacuity/witness axis, adjacent to #320 and #334 — not part of #330's
InputsAgreedecomposition.The gap
root_soundnessgained the premiserowsAligned : StepRowsAligned ziskTrace ziskStep …: at every step with a successor, the step's execution-bus producer entry is its own Main row's successorpc. For 62 of the 63 arms it isrfl. Only a two-row unaligned JALR lowering can violate it, becauseJalrLoweringRowspermitsfinish = start + 1andStepSound's JALR arm is indexed byfinish.No witness in the tree exercises it against a real two-row lowering. The only two-row JALR witness,
RawProgramBindingJalrExpansionNonvacuity, is an all-empty execution (numInstructions = 0), sorowsAlignedis vacuous there.jalrSpinRootSoundnessdoes use the unaligned lowering, but the JALR is its last step, sorowsAlignedis vacuous there too (it binds only wherej + 1 < numInstructions).So the premise is satisfiable in every checked-in instantiation without ever being tested against the configuration it exists to exclude.
Why this matters, stated precisely
This is not unsoundness.
rowsAlignedis a premise; a trace that violates it is simply outside the theorem. The issue is that we have no evidence about what the premise costs a real caller — whether an honest multi-instruction trace containing an unaligned JALR followed by another instruction can satisfy it at all.If it cannot, that is worth knowing: it would mean
root_soundnesssilently excludes a reachable program shape, and the right response is the discharge route rather than the premise.What "done" looks like
A witness with an unaligned two-row JALR at a non-final step, instantiating
root_soundness, withrowsAligneddischarged non-vacuously — or a precise statement of why such a trace cannot be built, which would itself be the answer.Note that
#334records the related problem that the remaining spin-trace witnesses carry hand-authoredind_widthplaceholders and are not usable forProgramRowsBinding; a new witness here should not repeat that.Relation to the discharge route
Separate from this.
trust/defects.md'sZISK-MODEL-GAP-JALR-EXPANSION-STEP-ROW-INDEXrecords two retirement conditions:rowsAlignedfrom the trace instead of assuming it;Those are premise-discharge work and belong with the #330/#341 follow-on. This issue is only about coverage: does anything test the premise as it stands.