Sphincs FV in ROM - #19
Open
TomWambsgans wants to merge 932 commits into
Open
Conversation
Prove that each layer message provides a stopped query reserve sufficient for the actual OTS encoding search. Transfer the fresh-query bound through finite search failure, all signing layers, and message grinding. Derive signing cache caps from the original monitored execution and its whole-experiment query bound. Bound sampled signing encoding-pair charges by the existing nonencoding signing reserve, preserve the unused reserve, and cancel the pair term from the security inequality. The full 127-bit SUF theorem remains open. Validation: full lake build passed (4318 jobs). Axiom audit passed for 3818 declarations, including private and generated declarations, with only propext, Classical.choice, and Quot.sound. Existing public 120/125/126-bit theorem audits passed. No proof holes, new axioms, kernel bypasses, resource-limit increases, or changes to the scheme or adversary model.
Prove a joint stopped bound for signing encoding-pair charges and the FTS opening work retained by selected signing executions without a parent exception. Carry the credit through the actual monitored adversary game and sampling under the original whole-experiment query bound. Keep the remaining signing reserve separately and expose the survival credit in the security inequality. Prove that newly revealed admissible signing views can use this credit. The full 127-bit SUF theorem remains open. Validation: full lake build passed (4322 jobs). Axiom audit passed for 3854 declarations, including private and generated declarations, using only propext, Classical.choice, and Quot.sound. Public 120/125/126-bit theorem audits passed. No proof holes, added axioms, resource-limit increases, or changes to the scheme or adversary model.
Split surviving new target coverage at the FTS opening allowance. Pay the bounded part with the preserved signing survival credit and retain the full excess as an unconditional fresh-view expectation. Combine this with the encoding-pair payment so both charges share one reserve without double counting. Prove that the excess is zero with an empty signing log and no cached message inputs, including every supported original root initialization and its expectation. Arbitrary adaptive histories retain the explicit excess, and the full 127-bit SUF theorem remains open. Validation: lake build passed 4326 jobs. The axiom audit passed 3881 declarations, including private and generated declarations, with only propext, Classical.choice, and Quot.sound. The public 120, 125, and 126-bit theorem audits passed. No new proof holes, axioms, adversary restrictions, kernel bypasses, or resource-limit increases.
Pay the surviving new-target coverage and the signing encoding-pair charge from one actual non-encoding signing reserve. Keep the positive excess as an operational expectation over the real signer, so the adaptive recurrence needs no fresh-reference choice or conditional-uniformity assumption. Recover the full decrease of the remaining coverage potential when the original syntactic signing budget is debited. Lift the checked step inequality through the adaptive adversary, retained trace, root initialization and key sampling. Add an alternative whole-game bound that cancels the signing reserve and encoding pairs using proved finite cancellation terms. The residual remains explicit. Prove its initial value is zero even at the reduced continuation budget and signing count. Validation: full lake build passes 4336 jobs. Axiom audit passes 3976 declarations, including the new private and generated declarations and the public 120, 125 and 126-bit theorems. No proof holes, new axioms, kernel bypasses or resource-limit increases. Full 127-bit SUF remains open: adaptive residual allocation and parent accounting still need to close.
Bound the operational signing excess by its unconditional new-target coverage and compare the resulting raw-index term to the full signing execution refund. Guard the excess at the existing valid-signing boundary, proving the inactive case has zero surviving coverage without restricting the adversary. The bound propagates through actual adaptive execution and key sampling: excess is at most 2^-22 of the refund. Compare the new refund to the previous unused-coverage reserve to prove both the refund and excess finite under the original query bound. Cancel the excess using that finiteness and retain a net refund of at least 1-2^-22 of the original refund. Connect the resulting whole-game bound to parent funding, reusing the existing parent conservation lemma. Validation: full lake build passes 4340 jobs. Axiom audit passes 4007 declarations, including new private and generated declarations and the public 120, 125 and 126-bit theorems. No new axioms, proof holes, kernel bypasses or resource-limit increases. Full 127-bit SUF remains open because the final global budget allocation, including parent releases, is not yet proved.
Track pending parent candidates together with unused cache capacity. A direct release spends pairs from this potential, giving a full adaptive cross-release bound of choose(q, 2) / 2^128 under the original whole-experiment query bound. Multiple cached candidates at one parent position remain allowed. Prove direct releases and fresh parent funding finite, then cancel direct releases and terminal discards against their existing funding. Carry the remaining parent credit and the net coverage refund into the concrete security inequality. The full 127-bit allocation is still open. Validation: full lake build passed (4345 jobs). Axiom audit passed for 4062 selected declarations, including private and generated declarations, with only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit security proofs and the new endpoint passed the audit.
Generalize the refund argument over step refunds that satisfy the existing coverage payment law, preserving the original theorems as specializations. Add the unused one-step slack to the refund and prove an exact balance over the full adaptive computation, including signing failure and probe stopping. Lift the larger refund through actual key sampling under the original hash-query bound, prove it finite, and pay the coverage residual from it. The security endpoint retains the resulting larger net refund together with the proved parent funding and cross-release bounds. No new game restrictions or cryptographic assumptions are introduced. The full 127-bit allocation remains open. Validation: full lake build passed (4349 jobs). The axiom audit passed for 4103 selected declarations, including private and generated declarations, with only propext, Classical.choice, and Quot.sound. Public 120-, 125-, and 126-bit proofs, the exact adaptive balance, and the new security endpoint passed the audit.
Identify the clamped current signing-log coverage potential with the exact valid coverage indicator. Retain the difference from the terminal envelope, including its hypothetical future signatures and excess assignment counts, as an additional refund through the actual stopped execution, root initialization and independent key sampling. Prove an exact adaptive balance and a finite sampled refund under the original whole-experiment hash-query bound. Carry the larger net refund through the parent-funding security endpoints. The full 127-bit allocation remains open; the public security theorem remains 126 bits. Validation: lake build passed 4354 jobs. The axiom audit passed 4152 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. No new warnings in changed modules.
Compare the exact adaptive coverage balance with the earlier unused-query bound. Prove that the complete net refund retains the unused-query credit plus the signing reserve left after encoding-pair costs, with no loss from the residual. Cancel only quantities proved finite under the original whole-experiment query bound. Identify the terminal indicator with the older bounded completion potential and prove that terminal retirement covers its joint completion credit through the retained trace and actual key sampling. Preserve these compatible credits together in the double-parent and net-parent security endpoints. Full 127-bit SUF remains open; the public theorem remains 126 bits. Validation: lake build passed 4356 jobs. The axiom audit passed 4176 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. No new warnings in changed modules.
Prove the local, adaptive, initialized and independently sampled comparison under the original whole-experiment hash-query bound. The joint credit is bounded by the unused coverage reserve plus the encoding-exhaustion allowance, so it cannot be counted as an independent additional saving. Combine the comparison with the compatible signing and completion reserves in the retired-refund SUF inequality. Full 127-bit SUF remains open; the public 120-, 125- and 126-bit theorems are unchanged. Validation: full lake build and axiom dependency audit, including private and generated declarations, with only propext, Classical.choice and Quot.sound permitted.
Generalize the retired coverage estimate to every live terminal cache with a valid covered signing log. Prove that the residual forgery event excludes structural failures, so the probability of a covered structural failure can be retained alongside the existing coverage refund and collision credit. Carry the correction through the actual retained execution and independent secret sampling into the SUF inequality, with the original hash-query bound and no additional error allowance. Prove that the collision terminal reserve plus this correction bounds the terminal collision/coverage product. Keep the earlier coverage theorem interfaces as corollaries. Full 127-bit SUF remains open. Validation: full lake build passed, 4358 jobs. Axiom dependency audit passed for 4212 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound permitted. No new module warnings or proof holes.
Prove an exact uniform hash-output coverage probability from the product of distinct revealed leaf counts at each index, including the message-digest grinding condition. Carry this sharper count to fresh observed-cover queries with the existing target-input exclusion, and retain the occupancy bounds as corollaries. Add a kernel-checked twelve-view example whose conditional coverage probability exceeds 2^-127. This rules out a uniform per-log rate shortcut, not the full adaptive SUF claim. The adaptive numerical allocation needed for 127 bits remains open. Validation: full lake build and axiom dependency audit, including private and generated declarations, with only propext, Classical.choice and Quot.sound permitted.
Derive the exact fresh digest-selection distribution from the existing optional completion theorem. Factor the completed signer support argument at digest selection, retain the probability of taking that fresh branch in conditional coverage and target-completion bounds, and preserve the earlier interfaces as corollaries. The signer, Option failures, SUF game and whole-experiment query budget are unchanged. The full 127-bit theorem remains open. Validation: full lake build (4360 jobs) and an axiom audit including private and generated declarations, allowing only propext, Classical.choice and Quot.sound.
The expected-growth bounds charged a full uniform view even when the signer selected a cached digest or exhausted its digest search. Keep the actual fresh-selection probability in admissible-cache growth, raw-index moments, new-target envelopes, transformed target costs and successful-signature input weights. Factor the common expectation argument once and retain the previous interfaces as corollaries. These proofs retain cache entries produced before a later Option signing failure. The final 127-bit allocation remains open. Validation: full lake build (4360 jobs) and an axiom audit including private and generated declarations, allowing only propext, Classical.choice and Quot.sound.
Propagate the actual probability of selecting a fresh digest through signer weights, index moments and the logged signing transition. Preserve the existing unweighted bounds as corollaries. Prove an exact nonfresh signing gap for future envelopes and retain it alongside the query commutation gap for the actual changing signer cache. This is an intermediate improvement; the full 127-bit SUF inequality remains open. Validation: lake build passed all 4361 jobs. The extended axiom audit checked 4336 declarations, including private and generated declarations, and found only propext, Classical.choice and Quot.sound. The public 120-, 125- and 126-bit theorem axiom checks also passed.
Retain the nonfresh selection and query commutation gaps in the capped remaining-budget signing envelope. Preserve the reduction when accounting for new targets, encoding pairs and signing execution refunds, and transport it through arbitrary adaptive computations with the existing query bound. Prove that the sampled signing gap fits inside the additional complete coverage refund. The cancellation uses a proved finite bound on the shared terminal potential and encoding charges. Derive an explicit global forgery bound retaining the gap alongside the net coverage refund, terminal retirement, double-parent credit and structural overlap. The final numerical inequality for 127-bit SUF remains open. Validation: lake build passed all 4364 jobs. The extended axiom audit checked 4374 declarations, including private and generated declarations, and found only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorem axiom checks passed. No proof holes, custom axioms, native_decide, unsafe declarations or option overrides were added.
Prove exact cached-selection probabilities from the expected number of reached digest attempts, and retain digest-search exhaustion in the normalization. Carry the exact coefficient into successful signer input weights and prove it is bounded by the existing query-budget coefficient. Preserve the old signer interfaces. Full lake build passed (4369 jobs). The extended axiom audit passed, including the new lemmas and public 120-, 125- and 126-bit theorems, with only propext, Classical.choice and Quot.sound. The full 127-bit SUF bound remains open.
Generalize the signer moment bounds to accept a proved reuse coefficient and specialize them to the actual digest-selection coefficient. Retain both the missing fresh-selection contribution and the excess of the old reuse coefficient in the remaining-budget signing gap, including its adaptive and sampled global refund bounds. Prove a quantitative lower bound using the actual admissible-cache count and retain exhaustion explicitly. Full lake build passed (4371 jobs). The extended axiom audit checked 4444 declarations with only propext, Classical.choice and Quot.sound, including the public 120-, 125- and 126-bit theorems. The full 127-bit SUF allocation remains open.
Relate reached digest attempts to actual fresh-selection probability, retaining cached stopping and exhaustion. Bound the nonfresh probability below by A/(A+2^118), where A counts admissible cached inputs for the current message. Carry the resulting whole-increment signing refund through adaptive execution and sampling into the combined forgery inequality. Full lake build passed (4374 jobs). The extended axiom audit checked 4480 declarations with only propext, Classical.choice and Quot.sound, including the public 120-, 125- and 126-bit theorems. The full 127-bit numerical allocation remains open.
Split cached signer weight into inputs matching the requested key, root and message, and their complement. Retain exact digest reuse weight times that complement through weighted moments and the raw-index signing envelope. Include the additional nonnegative gap in the existing remaining-signing refund, so the adaptive and sampled global bounds preserve it alongside the nonfresh, reuse and commutation gaps. Adjust the cached-selection lower bound for the enlarged refund. The concrete algorithms, SUF game and whole-experiment query bound are unchanged. The final 127-bit numerical allocation remains open. Validation: full lake build passed (4377 jobs). Extended axiom audit passed for 4495 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No proof holes, custom axioms or resource-option increases were added.
Bound the combined signing gaps below by A/(A+C) times the full signing increment envelope plus R_other/(A+C), where A counts admissible cached inputs for the requested key, root and message, C=2^118, and R_other is the envelope of unmatched cached weight. Carry this stronger credit through the existing adaptive and sampled cached-selection bounds into the global SUF inequality. Prove that A=0 forces all cached signer weight to be unmatched and that the exact reuse and unmatched gaps then recover the full coarse reuse contribution. The scalar mixture argument retains finite-loop selection probabilities and actual failures; it does not restrict the security game. The final 127-bit numerical allocation remains open. Validation: full lake build passed (4378 jobs). Extended axiom audit passed for 4508 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No new axioms, proof holes or resource/transparency options.
Prove the exact randomizer cache-hit probability from all cached inputs matching the requested key, root and message. Bound fresh digest selection by exact reuse weight times S=(1-C_all/2^128)*2^118, retaining the actual finite retry loop and failures. Replace the coarse 2^118 denominator in the cached selection and unmatched reuse refunds by S. Prove its positivity in the existing cache-budget range, inverse domination by the coarse reuse weight, and comparison with the previous refund. The stronger credit propagates through the existing adaptive and sampled bounds to the global SUF inequality. The scheme and query accounting are unchanged; the final 127-bit numerical allocation remains open. Validation: full lake build passed (4380 jobs). Extended axiom audit passed for 4535 declarations including private and generated declarations, with only propext, Classical.choice and Quot.sound. Public 120-, 125- and 126-bit theorems remain checked. No new proof holes, axioms or resource/transparency options.
Bound the exact digest reuse coefficient by D / (1 + A * D) using the finite signing-loop selection mass. Combine it with the unmatched-cache credit and carry the stronger refund through the SUF bound. Prove that it dominates the previous refund and recovers the full coarse reuse contribution when the message has no admissible cached digest. Validation: lake build completed successfully (4381 jobs). Audited 4554 declarations, including generated and private declarations, with only propext, Classical.choice and Quot.sound dependencies. The public 120-bit, 125-bit and 126-bit theorems pass explicit axiom checks. The full 127-bit bound remains open.
Use the shared probability mass of fresh selection and cached reuse to lower-bound their combined envelope gap. Take the stronger of this joint credit and the existing normalized credit, and carry it through the adaptive SUF bound without adding it independently to the underlying refund. Preserve the exact full-reuse refund when the requested message has no admissible cached digest. Validation: lake build succeeded (4382 jobs). Audited 4563 declarations, including private and generated declarations, with only propext, Classical.choice and Quot.sound dependencies. Explicit axiom checks passed for the public 120-bit, 125-bit and 126-bit theorems. The full 127-bit numerical allocation remains open.
Bound the fresh digest hazard by the cache entries for the requested root and message plus the remaining attempts. Normalize with the admissible count and carry the stronger reuse credit through the existing adaptive SUF bound. Prove exact cache-count updates, a closed reciprocal formula, and a near-uniform reuse bound conditional on a bounded admissible-count deficit. Validation: lake build completed successfully (4386 jobs). Audited 4609 declarations, including generated and private declarations, with only propext, Classical.choice and Quot.sound dependencies. Public 120-bit, 125-bit and 126-bit theorem axiom checks passed. The deficit probability and full 127-bit numerical allocation remain open.
Prove a budget-dependent potential bound for the existing exception monitor, then derive a q/2^223 bound from second- and fourth-moment growth conditions. The monitor retains the first exceptional query even if later cache entries remove the deficit. Prove the positive-part moment inequalities for increments +1 and -1023 with admissibility probability 1/1024. These are auxiliary results. The cache-moment hypotheses and integration into the 127-bit SUF bound remain open. The concrete scheme, game, and public security statements are unchanged. Validation: full lake build and an axiom audit covering the new modules plus the existing audited reduction; only propext, Classical.choice, and Quot.sound.
Prove second- and fourth-moment growth for the actual message cache counts. Each fresh query changes at most one message bucket, with the concrete admissibility probability. Bound the probability of ever exceeding the admissible-count deficit threshold by q/2^223 under the original whole-experiment hash query bound. Carry the bound through key generation and secret sampling. Prove that the monitored experiment projects to the original SUF game, and derive the tighter digest-reuse bound on monitored prefixes without an exception. The full 127-bit inequality remains open; the scheme and public security statements are unchanged. Validation: full lake build (4396 jobs); audit of 4697 declarations, including private/generated declarations and explicit public120/125/126 checks, with only propext, Classical.choice, and Quot.sound. No proof holes or resource-option changes in the new modules.
Bound raw index moments on executions that have not triggered a message-deficit exception. Parameterize the envelope by the reuse weight and debit the original syntactic hash-query budget across adaptive hash and signing requests. Instantiate the reuse weight with the proved clean-cache estimate, retain the signing cap and failure flags, and reduce the initial envelope to the existing index-moment calculation. Generalize the cache exception invariant to any monitor that detects the exceptional cache condition, preserving its existing interfaces. The public algorithms, SUF game and security statements are unchanged. The full 127-bit SUF theorem remains open; the new coverage calculation still needs to be combined with the forgery reduction and its query credits. Validation: full lake build; expanded axiom-dependency audit including private and generated declarations and the public 120-, 125- and 126-bit endpoints; source and whitespace checks. Only propext, Classical.choice and Quot.sound are permitted by the audit.
The clean-cache digest reuse estimate now bounds the actual cached-target coverage event across adaptive signing and hash requests. Parameterize the target moments and envelopes by reuse, retain exclusion of the target's own input, and carry the tighter estimate through the original remaining-query budget. Preserve unused-query credits, budget and signing execution gaps, terminal reserves, and potential discarded on exceptions or failures. Specialize the adaptive bound to the union of an existing exception and the message-deficit exception. Express the initial charge through initialNearUniformRawIndexRate for the next numerical bound and reduction step. Factor out a fixed-budget raw signing lemma while preserving its previous interface. Public algorithms, the SUF game, and the 120-, 125- and 126-bit statements are unchanged. Full 127-bit SUF remains open: the new numerical rate and its integration with the final forgery inequality still need proof. Validation: full lake build passed 4411 jobs; expanded axiom audit passed 4817 declarations, including private and generated declarations, plus explicit public and new endpoints. Dependencies were limited to propext, Classical.choice and Quot.sound. Source and whitespace checks passed with no new proof options or warnings.
Bound initialNearUniformRawIndexRate by 3/(16*2^128) using the proved near-uniform digest reuse weight. Carry the mixed-moment domination through a finite factorial envelope and discharge the common-denominator integer certificate with kernel decide. Apply the numerical bound to adaptive cached-target coverage while retaining the unused-budget and discard credits. Prove an adaptive union bound for exception monitors and project the exception flag of runWithFailure back to the original expanded oracle execution. Adding the message-deficit exception increases its probability by at most q/2^223, without assuming that the internal couplings for the two exceptions coincide. The public scheme, SUF game, and 120-, 125- and 126-bit statements are unchanged. Full 127-bit SUF remains open: parent-record lemmas that require every exception to be a parent settlement need an appropriate extension, and the final query-credit inequality still needs proof. Validation: full lake build passed 4418 jobs; expanded audit passed 4863 declarations including private and generated declarations, plus explicit public and new endpoints. Axiom dependencies were limited to propext, Classical.choice and Quot.sound. Source and whitespace checks passed with no added proof options or new warnings.
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.
126 bits security proven, now working for 127