Goal
The legibility deliverable for root_soundness, distinct from the derivation
work (#141 / #115 / #119 / #151). Make the theorem's premise list readable as a
clean trust boundary: every binder is visibly one of
Scope
- Audit every field of
InputsAgree / SailTrace / RowOutsideDefectRegion
consumed by root_soundness; tag each (a)/(b)/(c).
- Document the irreducible core (the (a) set) in the
root_soundness
docstring as the trust boundary a reader must accept, with a one-line
justification each (why it cannot come from the circuit alone).
- For each (c) field still carried as a premise, link the issue deriving it so a
reader sees it is dischargeable, not load-bearing trust.
- Cross-check against the trust gate: the documented (a) set should match what
actually appears in the audited axiom/binder closure.
This produces the reader-facing artifact that makes "a human reads the statement
and is convinced" true, even where #141/#115/#119 derivations are still in flight.
Acceptance
root_soundness docstring enumerates the irreducible-trust premise core with
justifications, and labels every other premise as derived-or-tracked.- A short
trust/ note (or section) cross-referencing binders ↔ trust classes.
- No code/proof change required (documentation + optional binder reordering for
readability).
Blocks #61. Relates to #141, #115, #119, #151.
Goal
The legibility deliverable for
root_soundness, distinct from the derivationwork (#141 / #115 / #119 / #151). Make the theorem's premise list readable as a
clean trust boundary: every binder is visibly one of
InputsAgreeregister / PC /memory agreement) and extraction fidelity;
hAvoidKnownBugs), knowndecode gap;
rowDecodes(already derived viaWire the committed-program decode into root_soundness in place (#61; #159 raw-program grounding deferred) #170/RomImageBinding: bind the in-build Aeneas decode pins to the committed program (make #111 load-bearing in root_soundness) #159) and, after root_soundness link assumes each op's effect *placement* (dest reg / store address / nextPC) instead of deriving it from the Main AIR #141/Eliminate the RowTraceCoherence memory trace-coherence floor — follow-on to #76 #115/Reduce the store RMW memory residual (h_m1..h_m7): extend the #76 Fold-B to stores #119/Make RowOutsideDefectRegion row-local: signed-defect Arith witness not trace-projectable (blocked on Arith range-table fidelity) #151, placement + memory + defect-locality.
Scope
InputsAgree/SailTrace/RowOutsideDefectRegionconsumed by
root_soundness; tag each (a)/(b)/(c).root_soundnessdocstring as the trust boundary a reader must accept, with a one-line
justification each (why it cannot come from the circuit alone).
reader sees it is dischargeable, not load-bearing trust.
actually appears in the audited axiom/binder closure.
This produces the reader-facing artifact that makes "a human reads the statement
and is convinced" true, even where #141/#115/#119 derivations are still in flight.
Acceptance
root_soundnessdocstring enumerates the irreducible-trust premise core withjustifications, and labels every other premise as derived-or-tracked.
trust/note (or section) cross-referencing binders ↔ trust classes.readability).
Blocks #61. Relates to #141, #115, #119, #151.