Full adoption of nconsigny/main (237ab69 + verity FIPS FORS)#6
Merged
Conversation
…FIPS uncompressed ADRS Key the FORS instance by the per-message hypertree leaf via the exact FIPS 205 FORS field split (tree=idxTree0, kp=idxLeaf0, FORS tree number folded into tree_index as (forsTree<<(A-height))|node, tree_height in word2), so each of the 2^h hypertree leaves selects a distinct FORS instance — matching the C12 and SLH-DSA-SHA2 field semantics (FIPS 205 Alg. 17). - C11, C13: apply the FORS field split (C11 stays JARDIN layout; C13 FIPS). - C7, C9: migrate the whole ADRS from the JARDIN 32-byte layout to FIPS 205 uncompressed (WOTS chain hashing, Merkle TREE, and FORS), matching C13, and apply the FORS split. Verifier edits touch only ADRS construction; offsets, lengths, loop bounds and target-sum checks are unchanged. - signer.py: c7/c9/c11/c13 key FORS by the hypertree leaf; c7/c9 also set adrs_mode=fips. Variants without the flags are byte-for-byte unchanged. - signer-wasm (C13): mirror the FORS field split. - test: add SphincsC7Test FFI sign->verify (C7 previously had no test). Note: this changes the FORS hash inputs, so signatures and verifiers are not backwards-compatible with the prior layout. Verified: C7/C9/C11/C13 FFI sign->verify pass; C12 and legacy variants unchanged.
C7 and C9 now use the FIPS 205 §11.2.2 uncompressed ADRS (joining C13); update the ADRS-layout tables and the migration-guidance note in README and CLAUDE.md. C11/C12 and the keccak SLH-DSA twin remain on JARDIN. Factual layout status only.
Pin that each FORS instance is keyed by the per-message hypertree leaf (the FIPS 205 field split): fors_pk and the revealed leaf secrets are a function of the hypertree leaf, and an opening produced under one leaf does not reconstruct another leaf's fors_pk. - Part 1 exercises the real C13 fors::sign_fors at full parameters (marked #[ignore] for runtime; run with --ignored). - Part 2 checks the property at reduced height against a faithful mirror of the FIPS-split addressing, with a positive control for harness integrity. Guards against regressing to tree-number-only FORS keying.
Multi-agent adversarial review of the C13 (FORS+C/WOTS+C keccak) and SLH-DSA-SHA2-128-24 signers and on-chain verifiers: 32 confirmed findings, 0 critical/high after reconciliation. The remediation commits that follow reference its finding IDs (e.g. C13-X-f2, SLH-X-f1).
Derive R = keccak(sk_seed || "R_grind" || message || nonce), grinding nonce for the FORS+C forced-zero predicate, instead of the public keccak("R_grind" || nonce). Binding R to the secret sk_seed blocks the chosen-message instance-concentration attack public R admitted (steer honest sigs onto one FORS instance, saturate, forge at ~2^41) and restores the standard secret-randomizer model (~2^133). Signer-only; the verifier reads R from the signature unchanged. Rust and Python use byte-identical preimages.
…3-X-f3, C13-X-f1) Add docs/SECURITY-ANALYSIS.md (FORS+C forced-zero effective k=6, secret-R rationale, ht_idx-collision reuse at the 2^22 cap, target-sum WOTS+C min-combination bound gated by FORS, SLH-DSA-SHA2 leaf-budget note). Add signer-wasm/tests/wots_reuse_poc.rs: deterministic single-use forward soundness + a two-reuse guard that a third independent fors_pk is not WOTS-openable from the harvested chains by count-grinding alone.
…-S-f2) Fix the 3->4-arg fors_secret call in cross_validate.rs (E0061 compile error that disabled the whole test binary) and regenerate PY_FORS_SECRET_0_0 for the ht_idx-folding preimage, cross-checked against script/signer.py.
…LH-V-f3, SLH-S-f1) Wrap the message as M = 0x00||0x00||M (empty-context envelope) before H_msg in the verifier and the C/Python/GPU signers, matching published NIST/ACVP external KATs. The C reference is slh_sign_internal, so the envelope is a 2-byte prepend (no C change). Pure-Python signer now signs raw bytes (drops rjust/truncate, SLH-S-f1). Add a deterministic hardcoded external-FIPS KAT forge test. Document the 4-byte-vs-1-byte ADRSc field-width equivalence (<256 at these params, SLH-V-f3).
…iew SLH-X-f1, SLH-X-f2cap) README/CLAUDE.md: "FIPS 205 bit-exact" -> external mode (empty-ctx envelope); fix the mislabeled "LSB-first" digest parse to MSB-first/BE; reframe the "2^24 flat-128-bit cap" as a usage cap over a 2^22 leaf space with birthday collisions absorbed by FORS.
…, C13-acc-g1, C13-V-f4)
C13 verifier: add canonical-key guard (reject non-canonical pkSeed/pkRoot, mirroring SLH); drop the unsound ("memory-safe") annotation; return false (not empty revert) on FORS+C forced-zero and WOTS+C target-sum failures; pin the digest shift/mask/fold constants to their K/A/H identities. SphincsAccount._validateSignature: make total (try/catch decode + ECDSA.tryRecover) so a malformed signature returns SIG_VALIDATION_FAILED, not revert. SphincsFrameAccount: document the error-surface contract. Update the frame test to exercise the bad-signature and non-canonical-key paths.
…SLH-X-f4/f5, C13-S-f1, C13-V-f4) First CI for the repo: rust-signer (cargo test incl. --ignored full-param + the cross-impl oracle and reuse guards), solidity (forge build/test incl. the pinned external-FIPS KAT and real-sig FFI round-trips), and slh-crosscheck (a reduced-parameter C<->Python bit-exact parity smoke test). Make signers/sphincsplus-128-24/params.h -D-overridable (#ifndef) so the reduced crosscheck binary builds; default build unchanged.
Rename AUDIT-C13-SLHDSA.md -> SECURITY-REVIEW-C13-SLHDSA.md, retitle it, add a note describing how the review was produced, and update the inline finding tags to (review X-fN) repo-wide. Finding IDs are unchanged.
Add a "new accounts & factories" table under Deployed Contracts listing the Sepolia ERC-4337 account + factory (bundled + fresh) and the ethrex frame account + factory deployed today, with explorer links and the ethrex no-EntryPoint caveat. Also gitignore script/.c13_*_keypair.json so per-account C13 keypair files (which contain sk_seed) can't be committed.
Add signers/slhvk-sha2-128-24/kat-counter0.json — a deterministic (counter=0) SLH-DSA-SHA2-128-24 vector produced by the Vulkan GPU signer (bit-exact vs the CPU reference), with the full 3856-B signature, derived seed material, the FIPS external envelope, and recorded on-chain verify results (Sepolia + ethrex). Wire SLH-DSA-SHA2-128-24-JsonKAT.t.sol to load it via vm.readFile / vm.parseJson and assert a freshly-deployed verifier accepts it (and rejects a one-bit-flipped message), so `forge test` enforces the fixture in CI. Grant fs read access to the fixture in foundry.toml.
…7/C9 adoption) - New adrsForsBase / adrsForsLeaf / adrsForsNode / adrsForsRoots with per-message hypertree leaf binding. - htIdxSplit matching C13 verifier (SUBTREE_H=11). - forsPkFromSigC13 and forsClimb updated to 4-arg form. - First step of Phase A (extend to C7/C9 in follow-up commits on same branch).
…/R1) C13 verifier: hoist idxLeaf0/idxTree0/forsBase before the outer FORS loop; leaf address becomes or(forsBase, or(shl(19, i), treeIdx)); inner-climb mstore 0x20 is or(forsBase, or(shl(32, h+1), or(shl(sub(18, h), i), parentIdx))); FORS_ROOTS uses idxTree0/idxLeaf0 directly. This matches the Yul at src/SPHINCs-C13Asm.sol lines 112-164 and the FIPS 205 uncompressed 32-byte ADRS field split. ClimbKit: address-parametric merkleClimbBodyA / stepMerkleA with AdrsEval witness; xmssAdrs / forsAdrs instantiations; rfl-equal to the old 4-name body so the XMSS side needs zero re-proving. ClimbLoop: execForEachLoop_forsClimb and execStmt_forEach_forsClimb to dispatch the FIPS inner climb in one rewrite. SegmentS4Fors: body now matches the model exactly — 8 setup statements (no per-i treeAdrsBase letVar), leafAdrs = or(forsBase, or(shl(19, i), treeIdx)), inner forEach "h" 19 forsClimbBody. Replaced wrong-generation forsBase theorems (which baked in idxTree0 = idxLeaf0 = 0) with forsLeafSetup_preserves_forsBase. New keystone eval lemmas forsLeafAdrs_eval_eq + forsLeafAdrs_value_eq_spec replace the per-step bit-mask lemmas. Generalized forsLeafSetupStep_node_eq_spec_of_eval over an arbitrary leafW : Nat (layout-agnostic). Slice anchors shifted by +3 (the three hoisted letVars): SegmentS4Fors.forsOuterStmt drop 16; SegmentSeed.segmentSeed drop 24; SegmentS4Finalize.forsFinalizeBody drop 17; SegmentLayer3.layerStmt drop 27; SegmentCompose drop 28. Phases done: R0 (unbreak, baseline), R1 (SegmentS4Fors proof repair). Build state: spec, Model, ClimbKit, ClimbLoop, SegmentS4Fors, SegmentS2/S3, InitialNodeKeccak, SegmentSeed all build. Remaining failures: SegmentS4ForsMerkleFrame, CurrentNodeFrame, SegmentAcceptSpec, SegmentCompose, SegmentS4Finalize — these are R2/R3/R4 (new SegmentForsSetup mini-segment, 97-site SegmentS4ForsMerkleFrame re-targeting, CurrentNodeFrame + Compose recomposition). Pushing this checkpoint so the FIPS-layout model and address-parametric ClimbKit land on the branch before the bigger R2/R3 commits. No new axioms, no sorry. Axiom audit on c13_refines_spec still shows [propext, Classical.choice, Quot.sound].
The unmerged-upstream-PR-1983 caveat in BindingFrame.lean is now historical — that PR has merged (lfglabs-dev/verity#1985) and the module is available at upstream HEAD. This file deliberately continues not to import it: all preserves_* lemmas here are proved locally and stay independent. Trim the workaround note. No code changes; comment-only. Full build remains clean (`lake build` completes successfully).
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
Mini-segment for the FIPS 205 §11.2.2 FORS pre-loop setup (model statements 13..15: idxLeaf0, idxTree0, forsBase). The segment hoists the loop-invariant ADRS base for the FORS outer loop (statement 16, forEach 'i' (u 6)). Structural design (per PR #6 review): - execForsSetup: no bound hypotheses; the word-normalizing interpreter is total, so letVar_continue … rfl discharges each step (matches the execForsLeafSetup pattern at SegmentS4Fors.lean:122). - stepForsSetup: the accept-path state transformer binding idxLeaf0 := htIdx &&& 0x7FF, idxTree0 := htIdx >>> 11, and forsBase from the FIPS ADRS-base expression. - stepForsSetup_forsBase_eq: takes htIdx : Nat as a hypothesis (with hht : lookupValue st.bindings 'htIdx' = htIdx and hhtLt : htIdx < 2^22) so the bound chain is discharged at the call site (SegmentCompose etc.) from the S3-segment hypertree-index bound. Done: - structural skeleton (forsSetup_eq_slice = rfl) - stepForsSetup transformer (defeq to the model) - stepForsSetup_idxLeaf0 / _idxTree0 (raw-Uint256 form accessors matching the eval output) - forsSetup_preserves_sigBase / _dVal / _htIdx (per-key BindingFrame preservation) - stepForsSetup_preserves_*_step (composed step-form) - #print axioms audit block - lakefile.lean registration Known build issues (documented in CLAUDE.md and the file header): - execForsSetup: the letVar_continue … rfl for the forsBase step times out at whnf. The evalExpr of the nested orE/shlE chain returns (Uint256.or …).val, but the post-step-14 RuntimeState has a let-block in its bindings (the b1/b2/b3 from stepForsSetup's def), so the localVar reads of 'idxTree0' / 'idxLeaf0' are not defeq to the eval result. Fix: inline the stepForsSetup let-block in its def, or dsimp/unfold of bindValue/lookupValue before the final rfl, or drop stepForsSetup in favour of a pure function forsBaseStep with bindings already fully inlined. - stepForsSetup_forsBase_eq: bound chain (h11shr via Nat.shiftRight_eq_div_pow + omega, hshl128 via Nat.shiftLeft_eq + Nat.mul_le_mul_right + decide) in place; final Nat-form rewrite (closing via simp [C13Concrete.adrsForsBase, Nat.lor_assoc, Nat.shiftLeft_eq]) is a sorry. Unblocks once the execForsSetup rfl is fixed. Net effect on the FIPS-FORS migration plan: R3, R4, R5 (the downstream re-targeting in SegmentS4ForsMerkleFrame.lean / CurrentNodeFrame.lean / SegmentCompose.lean / InitialNodeKeccak.lean) is blocked until the rfl in R2 is fixed.
…c accessors, 0 sorry
… FIPS finalize block, ClimbMemFrameMerkle forsSpecStep loop lifts
…ld wrapper (LEAN_NUM_THREADS cap + maxHeartbeats)
…Leaf0 digits; forsSpecStep/ForsClimbRel_step/forsClimb_model_node carry the digits; SegmentS4ForsMerkleFrame memory-frame half rewritten on forsClimbBody/stepForsMerkle (forsAdrs total-eval, no vadr threading)
…PS digits (ForsClimbFrameI invariant threads the outer 'i' binding; forsAdrs_eval_eq identifies the per-level ADRS; loop lift lands spec forsClimb t0/l0)
…ate, body_reshape with forsSetupBody); fix SegmentLayer3 beforeWotsPkCopy 0x20 lemma OOM (explicit .getD witness avoids whnf of the digit fold)
…me facts, forsBase threading (R1 forsLeafStep_preserves_forsBase), digit-parametric node-correspondence cluster; 4 sites remain (forsPk compress adrsRoots wiring, setup_secret variant pin, 2430 region)
…ress chains thread adrsForsBase digits (afterFors_forsBase, idxTree0/idxLeaf0 R1 frames), combined root-cell handoffs at afterForsSetup
… afterForsSetup root frame); SegmentForsSetup stepForsSetup_preserves_key
…rough the accept chain, digit hyps into the compress/forced-root handoffs, obligation structures at afterForsSetup
…Proofs.lean + C12 audit + cleanup remaining)
…taking wordcmp constructor, restored-BridgePrep arities; the 15 never-compiled residual glue compositions recorded as accepted assembly-obligation axioms (same convention/doc as their already-axiomatized twins; sub-64GB hosts cannot elaborate them)
… to FIPS digits, drop unused private, README/CLAUDE.md FIPS-FORS migration status (package green, zero sorry)
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit c521231. Configure here.
Member
Author
FIPS-FORS migration complete —
|
… envelope (M' = 0x0000||M) on both sides, matching the production fast-signer/on-chain path (--raw opts out); GPU signer cache key folds in the binary mtime like the CPU fast signer
Member
Author
|
Fixed both Bugbot findings in 9fee891:
|
…venv/bin/python does not exist on CI runners)
…theorems). Root cause was never depth: the lightweight assembly axioms spelled the WOTS-outer start state as an explicit record while consumers used c13BeforeWotsPkLightState, and that defeq whnf-unfolds the 64-iteration digit fold; restating the axioms in the named form makes every composition elaborate in ~400 MB. c13_refines_spec cone now: logic + 7 primitive obligations (3 single-cell cutpoint bridges, layer-0 inputs/of_inputs, layer-1 + reverted lightweight twins); c12: logic + 1. Proofs.lean axiom count 25 → 9.
Member
Author
|
Assumption reduction (aa6ead2): all 16 residual composition-glue axioms are now theorems. The elaboration divergence was never mathematical depth — the lightweight assembly axioms spelled the WOTS-outer start state as an explicit record-update while their consumers used the named New cones:
|
…ll bridges
c13_refines_spec now rests on Lean's logic + 3 residual assembly axioms
(was 7): the layer-0 inputs record obligation and the layer-1/reverted
lightweight chain-cell twins. c12 unchanged at 1.
- c13_beforeWotsPk_memory_{zero,0x20}_eq_lightweight: theorems via
c13_beforeWotsPk_eq_beforeWotsPkFrom (the historical and lightweight
cutpoints run the same suffix statement list, so the states are equal).
- c13_beforeWotsPk_memory_chain_eq_lightweight: theorem via the
beforeWotsPkAfterWotsCopyFrom factoring, copyFold43_copied_slot /
a new out-of-range copy frame, and the address-store cell frame.
Assembled with congrArg/trans only; the copy fold is introduced by
rw [<- he] so its start state is never restated (defeq between two
spellings of a fold start state unfolds the fold and OOMs).
- c13_ok_..._chain_cells_of_inputs_layer0: theorem via the verified
C13WotsPkKeccak _of_entry lemma (Entry = inputs record at j=0 via
foldLoop_zero).
- Elaboration notes: StmtResult.continue.inj instead of the injection
tactic (the tactic whnf-spikes on these equations); all keyed rw
patterns are head-const-distinct from interpreter folds.
Member
Author
|
Assumption reduction round 2 (491320d): the three single-cell cutpoint bridges and New cones (
How, on a 16 GB host:
Remaining 3 are of a different kind (no verified generic twin exists yet): the layer-0 inputs record obligation and the layer-1/reverted chain-cell closures. AXIOMS.md and the README trust-surface block updated. |
Standalone /tmp-validated probe files (per-fact lemmas under fresh heartbeat budgets, syntactic rw against rfl shape lemmas) targeting inputs_layer0 (Proofs.lean:11296) and the reverted layer-0 twin (Proofs.lean:12014). Not yet folded into Proofs.lean: the inputs_layer0 probe is still elaborating (~22 GB RSS); the reverted twin reuses the identical lemma block and compiles next. See probes/README.md.
probe_layer1.lean targets c13_ok_beforeAuthOff_wotsPk_lightweight_chain_cells_residual_layer1 (Proofs.lean:11607). The "currentNode" fact is derived via the layer-0-only afterMerkle residual (11812) to avoid circularity with the layer-1 residual (11843); folding in will require reordering the theorem after 11812. Not yet compiled (host RAM held by the inputs_layer0 probe validation).
5 tasks
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.
Single PR containing all commits from nconsigny/main + verity C13 FIPS ADRS rewrite start. Verifiers and signers already current. Remaining: C7/C9 verity extension + legacy cleanup on same branch.
Note
High Risk
Touches on-chain verification, ERC-4337 signature validation, and cross-language cryptographic preimages (C13 R/FORS and SLH external envelope); regressions would brick accounts or accept/reject wrong signatures, though CI and pinned KATs mitigate that.
Overview
This PR lands automated assurance that was missing before: a new
.github/workflows/ci.ymlrunscargo test(including ignored full-param C13 checks), fullforge testwith FFI signer builds, and a reduced-parameter Python↔C SLHcrosscheck.pysmoke test.C13 / C-series crypto remediations bind the message randomizer
Rtosk_seedand the message (closing public-grindability / chosen-message concentration), key FORS instances by hypertree leaf via the FIPS field split in Rust, Python, andSPHINCs-C13Asm/ C7 / C9, repair the Rust↔Pythoncross_validateoracle, and addfors_leaf_keying/wots_reuse_pocregression tests.SPHINCs-C13Asmalso gains a canonical public-key guard, returnsfalse(instead of empty revert) on forced-zero / target-sum failures, and drops the unsoundmemory-safeannotation;SphincsAccountmakes_validateSignaturetotal via guarded decode andtryRecover.SLH-DSA-SHA2-128-24 moves to FIPS 205 external verify with empty context (
M' = 0x00‖0x00‖Min verifier and signers), adds a pinned JSON KAT (kat-counter0.json+ Forge fixture), and tightens fast-signer cache keys (convention tag + binary mtime).Repo layout / docs: C11, C12, and Keccak SLH verifiers are retired to
legacy/; README/CLAUDE describe only two live FIPS ADRS layouts insrc/, expanded SLH usage-cap / FORS security notes (docs/SECURITY-ANALYSIS.md,SECURITY-REVIEW-C13-SLHDSA.md), and verity build status updates inCLAUDE.md.Reviewed by Cursor Bugbot for commit 771c51e. Bugbot is set up for automated code reviews on this repo. Configure here.