verity: C13 accept-path climb-correspondence workbench#3
Open
Th0rgal wants to merge 21 commits into
Open
Conversation
Adds the layered C13 MODEL-EXEC-BRIDGE discharge workbench: the spec mirror/concrete kernels (C13Concrete/C13Mirror), the per-segment interpreter characterisations (SegmentSeed/S2/S2R/S3/S4Fors/S4Finalize/ Layer3/Compose/AcceptSpec), and the reusable climb engines (ClimbKit, ClimbLoop, ClimbKeccakStep, ClimbMemFrame[Merkle], KeccakBridge, MemoryKit, MkC13State, RootFrame, BindingFrame, PreflightC13). Segment S2 (H_msg) is proved unconditional; the Merkle-climb per-step correspondence (stepMerkle_eq_merkleSpecStep, xmssClimb_eq_specFold) and ADRS-word assembly (address_assembly_eq) are axiom-clean. The residual open obligation is the per-iteration auth-path calldata correspondence (blocker #20) and the Layer-3 hypertree compose that flips execC13 from opaque to a concrete interpreter run. The 3 bridge axioms still stand. Full `lake build SphincsMinusVerifiers` green, no sorry.
Member
Author
|
@codex review |
|
To use Codex here, create a Codex account and connect to github. |
Add SiblingCalldata.lean with masked_sig_read_eq_wordOfHash16: for any 16-byte-aligned signature offset, the masked calldata word equals the spec's wordOfHash16(read16 sig sOff). Covers R, FORS sk, and FORS auth reads. Split into aligned/straddle case lemmas; zeta-reduce the calldataloadWord let-bindings via an explicit defeq `show` to avoid a kernel deep-recursion from the reduceIte/reduceMul simprocs. Axiom-clean.
Add `read32BE_calldata` (frozen calldata word = 32-byte big-endian read for ANY offset, via low/high stitching across the 32-byte word boundary in the straddle case) and `masked_sig_read_eq_wordOfHash16_gen`, dropping the `sOff % 16 = 0` hypothesis. Covers the XMSS auth offsets (≡4/≡8 mod 16). Built on new readBE split bricks (readBE_split_at/_div, word_eq_readBE, readBE_eq_read16). Axiom-clean (propext, Classical.choice, Quot.sound).
Add `merkleClimbData_of_frozenCalldata`: discharges the per-height `MerkleClimbData auth cdAt h` (fully-reduced blocker #20, definitionally `maskN (cdAt h) = wordOfHash16 auth[h]`) against the frozen mkC13State calldata, given that `cdAt h` is the frozen word at `sigDataOffset + sOff` and the spec parse fact `auth[h] = read16 sig sOff`. Closes via `SiblingCalldata.masked_sig_read_eq_wordOfHash16_gen` (maskN is defeq `Nat.land · N_MASK`). Works for ANY offset, incl. XMSS auth ≡4/≡8 mod 16. Imports SiblingCalldata (no cycle). Axiom-clean; full build green.
Pure-spec list-indexing lemmas pinning every climb auth-path sibling to its sig byte-offset: * XMSS: layer.authPath[h]? = read16 sig (1952+868*layer+692+16*h), h<11 * FORS: fors.authPath[t][h]? = read16 sig (128+304*t+16*h), t<6,h<19 plus getElem?_map_range helper and parseSignatureC13_size. Axiom-clean (propext only).
climb_calldata_read_eq_frozen (P2): the per-step `calldataload(authPtr + h<<4)` in the model resolves to the frozen-image word at `sigDataOffset + sOff`, via evalExpr_siblingOffset + offset arithmetic (no execC13). xmss_climb_data_range (P3): composes parseSignatureC13_layer_authPath_getElem? (hauth) with merkleClimbData_of_frozenCalldata to supply the whole-loop `∀ i<11, MerkleClimbData lsig.authPath cdAt i` range hypothesis consumed by foldLoop_invariant_cond. Both axiom-clean (propext, Classical.choice, Quot.sound).
FORS analog of xmss_climb_data_range: the FORS outer loop's inner Merkle climb (forsLeafBody, forEach h<19 over the same merkleClimbBody) gets its whole-inner-loop range hypothesis ∀ h<19, MerkleClimbData tAuth cdAt h from parseSignatureC13_fors_authPath_getElem? (hauth) composed with merkleClimbData_of_frozenCalldata, with authPtr = sigDataOffset + (128+304·t). Axiom-clean (propext, Classical.choice, Quot.sound).
merkleClimb_foldLoop_correspondence: foldLoop_invariant_cond specialised to the Merkle climb (R=MerkleClimbRel, specStep=merkleSpecStep, D=MerkleClimbData, step=stepMerkle). The whole climb loop advances MerkleClimbRel together with specFold, gated on the per-step advance hstep and the range hypothesis supplied by xmss/fors_climb_data_range. xmssClimb_model_node: combines the above (node projection) with xmssClimb_eq_specFold to give the "model node = spec xmssClimb root piece" equality, conditional on hstep (frame bookkeeping at the segment-trace climb-entry state) and hR (initial node = WOTS-PK/FORS-leaf keccak). Both axiom-clean (propext, Classical.choice, Quot.sound).
…ec inputs to bytes)
…l projection MerkleClimbRel (idx+node bindings only) cannot self-preserve under one stepMerkle step. MerkleClimbFrame bundles it with the static frame the step lemma needs (adrsBaseVar/authPtrVar bindings, mem[0x00]=seed, selector=0, frozen calldata image, name-distinctness). MerkleClimbFrame.toRel projects back to MerkleClimbRel. Axiom-clean ([propext, Quot.sound]).
Add three frame-preservation lemmas proving one merkleClimb step leaves the non-rebound frame components fixed: - stepMerkle_selector_calldata: selector and world.calldata unchanged - stepMerkle_binding_frozen: any binding w distinct from the five rebinds (sibling/parentIdx/s/nodeVar/idxVar) is preserved - stepMerkle_mem_zero: seed cell mem[0x00] preserved (writes land at 0x20/o5/o6) All axiom-clean [propext, Classical.choice, Quot.sound].
Resolves the climb body's parity-xored child slots (merkleClimbBody stmts 5/6, 0x40 ^^^ s and 0x60 ^^^ s) to bare Nat.xor on bounded operands, mirroring evalExpr_bitOr_bounded. Axiom-clean.
Add three generic combinators resolving the h2/h4/h5off/h6off evalExpr hypotheses of MerkleClimbRel_step from variable bindings alone: - eval_parentIdx_shr: shr(1, idxVar) = mIdx >>> 1 - eval_selector_shl: shl(5, and(idxVar,1)) = (mIdx &&& 1) <<< 5 - eval_childOffset_xor: xor(off, s) = Nat.xor off sval h5val/h6val are bare .localVar reads (definitional at the assembly site); h1 is merkle_sibling_read_frozen, h3 is address_assembly_eq. All axiom-clean.
Assemble MerkleClimbFrame_step: one climb step carries the whole frame (relation + adrsBaseVar/authPtrVar bindings + seed cell + selector + calldata image + name-distinctness) forward, given the same per-step bundle MerkleClimbRel_step consumes. Relation advance via MerkleClimbRel_step; static conjuncts via the three frame-frozen projections; distinctness tail carried verbatim. Does not discharge h1..h6val/StepDataObligations (offset/address/ sibling content, isolated in the per-fact combinators + MerkleClimbData). Axiom-clean.
MerkleClimbFrame_h_inject (frame survives the loop's "h" rebind), merkleClimbFrame_foldLoop_correspondence and xmssClimbFrame_model_node (foldLoop_invariant_cond specialised to the frame invariant), so the static frame rides the loop invariant and each per-step hstep instance receives it for free. Axiom-clean.
Composes MerkleClimbFrame_h_inject + MerkleClimbFrame_step to produce the exact hstep body the frame-carrying loop lift demands, folding the static frame in so a concrete climb-entry instantiation supplies only the per-step data facts (h1 bottoming at the site-specific offset identity). Axiom-clean.
Add SegmentS4ForsDataObligations with two axiom-clean reductions for the remaining FORS data obligations of C13SeedNamedAcceptGuardedPkRootSizeLeafObligations: * hLeaf_of_stepMerkle_seed_frame reduces the hLeaf field (one FORS leaf-step preserves the public-seed cell mem[0x00] for idx < 6) to a single unconditional per-step stepMerkle seed-cell frame for the inner FORS Merkle climb. * hmRlo_of_afterFors_root_slots reduces the hmRlo field (the six ordinary FORS root cells 0x80 + 32*j, j < 6, after forsFinalizePreCopyStep) to the afterFors root-slot correspondence; the pre-copy finalize prefix is a frame over those six source slots. Both depend only on [propext, Classical.choice, Quot.sound]. Standalone: they touch neither execC13 nor c13_refines_byte_spec, and introduce no axiom, sorry, or native_decide.
…rame Removes the residual hstep hypothesis of hLeaf_of_stepMerkle_seed_frame: stepMerkle_seed_frame_unconditional proves one branchless Merkle swap step preserves mem[0x00] for every state (no pathIdx < 2^256 bound, via the parity witness n := pathIdx % 2^256 and the new bound-free evalExpr_bitAnd_literal_modself). hLeaf_discharged then closes hLeaf outright. #print axioms: foundational only.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit dd1e753. Configure here.
| as written by `mstore(0x80, 0xFF…FB...)` — the contract literal has a leading | ||
| zero nibble (63 `F`'s). -/ | ||
| def hMsgPad : Word := | ||
| 0x00FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF |
There was a problem hiding this comment.
hMsgPad has 64 F-nibbles instead of 63
High Severity
hMsgPad is defined as 0x00FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF (leading 00 + 64 F's). Since Word := Nat, the leading 00 is a no-op, making this 2^256 - 1. However, the contract model in Model.lean and SegmentS2.lean uses a literal with 63 F's (2^252 - 1), and the comment on hMsgPad itself says "the contract literal has a leading zero nibble (63 F's)." The spec constant doesn't match the contract model, so hMsgC13 computes the wrong H_msg digest.
Reviewed by Cursor Bugbot for commit dd1e753. Configure here.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Builds out the C13
MODEL-EXEC-BRIDGEdischarge — the segment-by-segmentproof that the compiled Verity model's keccak accept path refines the byte
spec. (Follows up the merged #1; depends on the keccak256/calldata
interpreter support in lfglabs-dev/verity#1943.)
C13Concrete,C13Mirror+ axiom files).SegmentSeed,SegmentS2,SegmentS2R(H_msg, proved unconditional),SegmentS3,SegmentS4Fors,SegmentS4Finalize,SegmentLayer3,SegmentCompose,SegmentAcceptSpec.ClimbKit,ClimbLoop,ClimbLoopGuarded,ClimbKeccakStep,ClimbMemFrame,ClimbMemFrameMerkle,ClimbStepSpec,KeccakBridge,MemoryKit,MkC13State,RootFrame,BindingFrame,PreflightC13.The Merkle-climb per-step correspondence (
stepMerkle_eq_merkleSpecStep,xmssClimb_eq_specFold) and ADRS-word assembly (address_assembly_eq) areaxiom-clean (
[propext, Classical.choice, Quot.sound]).Still open (the 3 named bridge axioms remain): the per-iteration
auth-path calldata correspondence (blocker #20), the Layer-3 hypertree
compose, and the atomic
execC13flip. Nosorryanywhere.Test plan
lake build SphincsMinusVerifiersgreen (against verity#1943 branch)#print axiomson per-verifier theorems shows only[propext, <prims>, <bridge axiom>]Note
Medium Risk
Large formal-verification surface on the SPHINCS C13 accept path; mistakes could block or mislead the eventual bridge proof, but the change is additive and leaves the live bridge axiom and opaque executor untouched.
Overview
Adds a large additive Lean layer for discharging the C13
MODEL-EXEC-BRIDGE: concrete byte-spec primitives, a segment-aligned spec mirror, reusable climb/keccak/frame engines, and synced audit/axiom docs.execC13andc13_refines_byte_specare unchanged (still opaque/axiom).C13Concreteintroducesc13PrimitivesConcretewith hashing via the sameKeccakEngine/ big-endian word preimages as the Verity interpreter (keccakWords,maskN, tweakable hash). It implements C13 parsing,H_msg, FORS/WOTS/XMSS reconstruction, and many spec-side lemmas (16-byte canonical outputs, auth-path offsets, hypertree root shape) without new axioms orsorry.C13MirrorfactorsverifyBytesinto named intermediates (S2 digest, S3 forced-zero, S4 FORS, Layer-3 climb) and provesverifyBytes_c13_eq_mirrorso later segment proofs can compose against one RHS.Climb stack (
ClimbKit,ClimbLoop,ClimbLoopGuarded,ClimbKeccakStep,ClimbMemFrame,BindingFrame) proves interpreter step/loop shape for branchless Merkle and WOTS bodies, guarded hypertree loops, boundedevalExprfor masked keccak and ADRS assembly, and memory/binding frame preservation for keccak correspondences.AUDIT.md/AXIOMS.mdrecord partial progress: concretec13Primitives, build green, standalone lemma footprints; bridge theorem, auth calldata (#20), and full compose still open.Reviewed by Cursor Bugbot for commit dd1e753. Bugbot is set up for automated code reviews on this repo. Configure here.