verity: C13 accept-path climb-correspondence workbench#3
Draft
Th0rgal wants to merge 81 commits into
Draft
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.
Member
Author
|
Checkpoint pushed at Status: this is still WIP, not the final MODEL-EXEC-BRIDGE discharge. Local verification before push:
Current progress in this checkpoint:
Remaining before ready-for-review:
|
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
High Risk
Touches formal verification of a cryptographic signature verifier and changes byte-spec final-root comparison and hypertree semantics; bridge axioms remain, but mistakes in spec or proof glue would undermine correctness claims.
Overview
Adds concrete byte-spec primitive packages for SPHINCS-C13 and C12:
c13PrimitivesConcrete/c12PrimitivesConcreteroute hashing through the same interpreter-alignedkeccakWordskernel asSourceSemantics, with variant-specific parse layouts,H_msg, FORS/WOTS/XMSS reconstruction, and many parser/shape/canonical lemmas for later bridge proofs.Spec layer updates extend
Primitiveswith layer-indexed WOTS/XMSS hooks, switch the hypertree fold towotsGrindingFailsAtLayer/*AtLayerreconstruction, and replace rawroot == pk.pkRootwithrootMatchesPk(includinglowBytesProjectionwhenfullPkRoot).Mirror and glue:
C13Mirrornames S2–S4 / layer-climb intermediates and provesverifyBytes_c13_eq_mirror;C13BridgePreppackages observedexecC13outcomes againstverifyByteson accept/reject subdomains;BindingFrameandClimbKeccakStepadd keccak-free binding frames andevalExpridentities for masked keccak and ADRS words.Docs:
AUDIT.md/AXIOMS.mdrecord partial MODEL-EXEC-BRIDGE progress (c13_refines_byte_specand opaqueexecC13still open).Reviewed by Cursor Bugbot for commit af8f42e. Bugbot is set up for automated code reviews on this repo. Configure here.