Sphincs FV - #275
Merged
Merged
Conversation
Sign layers from bottom to top, stop at the first failed encoding search, and compute the discarded top root on success. Update the reference cost models and execution proofs, with regression coverage for failure positions and serialization order. Validation: full lake build without warnings, independent public-theorem and axiom checks, and kernel replay of all eight changed modules.
Bound hash calls on supported executions of the consistent cached random oracle, counting cache hits and all honest computation. Adapt both security proofs without strengthening their public hypotheses, and add regression proofs separating consistent execution budgets from arbitrary reply paths. Validate both full Lake builds, explicit public theorem types, standard-axiom audits, regression kernel checks, fresh leanchecker replays, and the SPHINCS LaTeX build. Independent adversarial reviews found no remaining issues.
Tighten definitions and explanations, remove implementation-specific references, and clarify parameter meanings. Add vector diagrams for the branching hypertree, vertical WOTS chains, the FORS forest, and complete verification. Build with latexmk and visually check all four figures. The final build has no LaTeX warnings or layout issues.
Derive each FORS and hypertree parent index from the previous index by clearing its low bit and dividing by GEN. Preserve the existing tweak bytes. For aggregate --sphincs 245 --log-inv-rate 1 --repeat 3, VM cycles fall from 2,351,886 to 2,123,791 (9.7%). Validation: benchmark proof verification, aggregate_mixed_two_to_one, aggregate_hints_bind, and git diff --check passed.
Use a 16-byte layout with protocol_domain_sep 0 for XMSS and 1 for SPHINCS. Align type codes and field positions across the native encoders, aggregation guest, specifications, and Lean statements. Adapt the byte-injectivity proofs and preserve the incremental SPHINCS parent-index calculation. Keep both specifications self-contained. Remove the exact-layout test and the complete-verification diagram. Validation: release workspace tests, adversarial witness checks, affected-crate Clippy, both LaTeX builds, and both Lean security proofs with unchanged axiom footprints pass. Aggregation benchmarks verify at 2,132,425 cycles for 245 SPHINCS signatures and 1,573,750 cycles for 900 XMSS signatures.
Use the full 32-byte SPHINCS seed for WOTS and FORS derivation. Derive both schemes public parameters under tweak type 10 with a zero public-parameter field. Use dedicated types 0 and 5 for signing secrets and type 11 for XMSS filler nodes, retaining separate protocol prefixes. Update SPHINCS secret-key serialization to 48 bytes, expose MasterSecret, refresh benchmark caches, and document the seeded constructions. The seeded Lean proof extensions remain separate work. Validation: release workspace tests, full-master and domain-separation regressions, adversarial aggregation hints, affected-crate Clippy, and both LaTeX builds pass.
Derive the public parameter and signing secrets from one 256-bit master seed in both complete Statement.lean specifications. Preserve scheme and key-derivation domain separation. Reduce the shared consistent random-oracle games to independent secrets, account for adaptive seed guessing and every actual hash call, and retain the 127-bit bound. Keep proof machinery separate from the statements and align the standalone documents. Validation: both full Lean builds and standard-axiom guards passed; final edited modules checked; both LaTeX projects built. Independent adversarial reviews found no proof blockers, and their documentation findings were corrected. Existing XMSS implementation coverage limits are recorded in its README.
Use a separate type-12 hash domain for deterministic signing trials, bound XMSS search, and remove RNG arguments from both signing APIs and their callers. Update both specifications and keep the complete deterministic schemes in Statement.lean. Prove both public 127-bit security claims by coupling seed-derived trials to independent tables, replaying repeated requests, and transferring the consistent random-oracle query budget. Keep randomized reference schemes inside the proof modules. Validation: both full Lean builds and standard-axiom guards; release signature tests and aggregate_two_to_one; release workspace check; focused clippy; rustdoc; formatting; both LaTeX builds; adversarial reviews.
Expose only hash and signing queries in the public adversary interface and sample the master seed outside the hash-only game. Preserve the complete counted experiment through an embedding into the internal randomized game, and prove the independent-strategy averaging bound. Update both specifications and proof guides. Validated both full Lean builds, query-budget regression checks, standard axiom footprints, both LaTeX builds, and adversarial reviews.
Reuse each scheme’s key-generation definition, factor duplicated game code, and shorten the oracle logging and counting arguments. Make hash byte lengths explicit in each self-contained statement while keeping the projects independent. Validation: both full Lean builds and query-budget tests pass. Public security claims and randomized-adversary results use only the three standard Lean axioms. Independent adversarial reviews found no issues.
Keep main's README structure and naming while preserving the updated SPHINCS benchmark results.
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.
127 bits of classical SUF for our sphincs, in the ROM
Lean4 checked, based on VCVio