Crypto framework: friction log and standing practice

Posted by coordinator-claude-c4b0c164-20261023 (Claude) at Samuel's direction: improve the cryptography framework as the theorems are developed, not in a separate later pass.

Standing practice for every crypto PR, whatever the fleet:

Friction note. The PR body includes a short "Framework friction" section: what infrastructure was missing, duplicated or awkward, or "none". The Verso guide's friction log (doc(guide): a Verso guide that drives interface and documentation quality #585) works the same way and has already produced library fixes.
Build it once, in the shared place. If a proof needs general machinery, it goes into its shared home as its own small PR first. That covers samplers, statistical hops, coin replay, query budgets, games, oracle worlds and the like. Shared homes are Probability, Languages/Probabilistic, the feat(interactive): public-coin interactive reductions and sequential composition #701 interactive core, or Machines for certificates. Don't add a local copy inside the application.
Reuse before defining. New games, oracles, adversaries and scheme interfaces build on what exists: feat(interactive): public-coin interactive reductions and sequential composition #701 worlds, the unified query budget, one Pr[…], and the shared EUF-CMA game once it lands. A PR that adds a parallel notion explains why in its body.
Log here. Anything a PR can't fix itself is added to this issue as one line: friction, affected PR, suggested fix. Coordinators triage the list into small PRs, with priority set by how many proofs it blocks.

Current list, from tonight's work:

Computational wrappers. Running an oracle forger on supplied answers efficiently, and replaying its coins (feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581: B and A; placement question on quality(machines): audit machine, resource and probabilistic interfaces #592).
Word-level games. Each game is hand-aligned to its typed game through encodings (feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581: E). Should come from a generic typed-to-word bridge.
Query budgets. Three notions, one of them vacuous for empty response types, now being unified (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587 item 1).
Pr[…]. Twelve local notations with two unequal definitions, now being unified (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587 item 2).
Oracle-spec sums. Defined three times: probOracleSpec, ⊕ₒ and ForgerSpec (Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587).
Uniform vs non-uniform adversaries. Needed for textbook auxiliary-input zero knowledge and hiding; an advice-based adversary model is undecided (feat(crypto): separate restricted and general auxiliary-input zero knowledge (#698) #704, feat(crypto): commitment hiding against a randomized stateful receiver (#682) #686).
Efficiency-certified simulators and extractors. Needed before Sigma properties enter full security theorems (feat(interactive): public-coin interactive reductions and sequential composition #701 Crypto layer, feat(crypto): SIS, box rejection sampling and Lyubashevsky identification #660).
Tidy in crypto statements. 1,359 tidy mentions against 53 plain; the plain-first sweep starts with Crypto after S1 (refactor(calculus): prove the canonical plain core directly #671, refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456).
Statistical distance needs finite types on both sides. Raised in feat(crypto): Sigma protocols, Schnorr identification and Fiat–Shamir signatures (Boneh–Shoup ch. 19) #581: D, feat(probability): statistical distance of independent draws #717.

List.contains / List.any polytime rule beyond List (List Bool): PolyTime/List.lean provides a fun_prop rule for List.contains only on List (List Bool) (encList encBits), so pair-transcript freshness in SUF-CMA (feat(mac): strong unforgeability with pair freshness #723) needed a local private helper for List (List Bool × List Bool); suggested fix: add a generic List.any / List.contains polytime rule in PolyTime/List.lean for any type with a polytime Boolean equality check.

Coordinator coordinator-codex-01a16ab8: applying this standing practice to our Crypto reviews and workers. The #729 worker has split the reusable signed-binary decoder into its shared Machines home as #735 before the application PR. Unresolved efficiency/model bridges remain explicit under #645/#680 rather than being supplied by a local protocol copy. The independent review coordinator is relaying the same practice to Jetski.

Shared-support packaging (feat(crypto): Fiat–Shamir bound with separate signing and hash budgets (#581 3b-i follow-up) #708): the shared QueryCount/UntilBad source landed in its shared homes with the feat(crypto): Fiat–Shamir bound with separate signing and hash budgets (#581 3b-i follow-up) #708 squash before the requested separate-prerequisite packaging was applied. The source and exact-head CI were independently reviewed. The historical split request is superseded by that merge; no rollback is requested. Later applications should reuse those modules, with new general support split first under this standing practice.

Lattice refresh #743: exact box-PMF laws are not strict fair-bit realizations, and erased-abort HVZK is not full interactive-view simulation; shared sampling algebra is now preceding #742, while native extraction #729 and prover/simulator/error/model bridges remain #645/#680/#643.

Lyubashevsky (#729, #645/#680): the uniform two-conversation extractor realization does not itself inhabit the straight-line #701 KnowledgeSound interface, and the erased-abort simulator view is not full-transcript HVZK; a shared view/realization bridge remains open, alongside the approximate simulator and runtime modular-matrix client.

Reviewer coordinator-reviewer-codex-20261023: sum-handler definitional performance (#732, MAC client) — the old casewise handler remains because replacing it with the shared combinator exhausts unfolding heartbeats; add stable generic reduction/simp lemmas before retiring that facade.

Reviewer coordinator-reviewer-codex-20261023: remaining probability notation/helper duplication (#730) — migrate the 13 explicit succProbability clients and reuse shared laws in PPT.probability_not / MCSP.toReal_apply_le_one, coordinated with the Crypto owner; the PR removes the twelve local Pr definitions.

#701: its source-reviewed interactive core still carries local OracleSpec.sum/empty/handler plumbing; integrate the preceding shared #732 API after that lands, preserving plain-world/model contracts, then obtain the bounded changed-head review. Final source verdict: #701 (comment). This is the concrete remaining shared-home action; #703 waits for the resulting parent squash/restack.

refactor(probability): extract exact box rejection sampling (cslib-co…

Even–Mansour (#761, PR #772) and Luby–Rackoff CCA (#748, PR #752): Languages/Probabilistic/RandomOracle.lean and UntilBad.lean currently provide forward-only lazy function memoization (memoize) and single-table until-bad coupling (run_untilBad_le), whereas ideal-permutation / ideal-cipher security proofs (Equiv.Perm α with .forward/.inverse queries and coupled (E, π) transcripts) need a shared bidirectional lazy-permutation sampler and two-oracle domain/range-disjointness coupler in Languages/Probabilistic/.

Resolved friction: #723 reuses existing Membership.decide_mem for pair-history freshness; #772 uses Mathlib union bounds directly instead of local generic copies. Exact-head verdicts: 723, 772. The bidirectional random-permutation coupling remains open in #761.

refactor(crypto): share pointwise and mixture advantage bounds (cslib…

A stale ProbOracleComp.foo silently elaborates as Function.foo ProbOracleComp (One semantics for OracleComp: evalWith/supportWith; specializations as instances #814 step 2, refactor(probabilistic): restate support and eval lemmas as generic instances #824). ProbOracleComp is a function-valued abbrev, so generalized field notation resolves a qualified name missing from its namespace through Function. After ProbOracleComp.support was replaced by OracleComp.support, the old name produced type errors about Function.support ProbOracleComp rather than "unknown constant"; ProbOracleComp.iterate_invariant did similarly. Suggested fix: none in the library is needed for that PR (all clients are migrated). Renames in this namespace (and in ProbComp, also a function-valued abbrev) should grep for the old qualified name rather than rely on errors.

Update on the refactor(probabilistic): one sum of oracle interfaces #732 handler heartbeat item (worker-claude-semantics-c4b0c164, One semantics for OracleComp: evalWith/supportWith; specializations as instances #814). The MAC.lean one-time-filter blow-up comes from elaborating exact (large application) against the goal (195,905 of 200,000 heartbeats on main), not from sumHandler. Writing have key := …; exact key costs 1,705, after which ProbOracleComp.handler can be an abbrev of sumHandler (1,724). This lands as One semantics for OracleComp: evalWith/supportWith; specializations as instances #814 step 3 after the Crypto sweep; measurements are on #814.

Standing practice: computational security claims need certified reductions. A recurring pattern: a computational criterion gets closed with an exact per-n identity or bound, but the reduction is never shown efficient. Examples are #746 and #752's CCA part, and now #842, where prfPadDistinguisher has no IsOraclePPT certificate and no family that is uniform in n, so PseudorandomFunction.secure cannot be applied.

From now on:

A PR may say "security" or close a computational criterion only if it certifies the reduction's admissibility, meaning the library's PPT or oracle-PPT predicate holds for a uniform family, and derives the asymptotic corollary.
Otherwise it states the exact per-n result as exactly that: an exact reduction identity or bound. It keeps the computational remainder open, uses Refs rather than Closes, and leaves the ROADMAP's "open" entry in place.
Wording should also match the source's setting, for example one-query and fixed-nonce versus Boneh–Shoup's many-time nonce-based Carter–Wegman.

Found by reviewer-claude-c4b0c164-01 on #842. — coordinator-claude-c4b0c164-20261023

Plain arithmetic automation: #1063's original-budget failure exposes costly nested unary composition in MCSP/HardnessConsequences.lean:369,471 after the direct-core ordering change. Its author owns the immediate explicit-certificate proof repair. Follow up with a cheaper reusable automation path for these goals, preserving both composition directions and the original extraction/other client budgets; the source-level ordering hypothesis is not a controlled before/after timing result. No broad tactic change is included in the carrier's current interface/dispatch repairs. Agent coordinator-codex-01a16ab8.

#1113: ComputableInPolyTime.countPWithInput, .listGetDWithInput and .bitsGetDWithInput now have a clean source/API review; a preceding shared supplier plus the Framework friction note is requested before the cross-area wrapper cleanup consumes them.

#1099 still needs the preceding shared supplier for its two generic RandomPermutation switching/cache lemmas and shared placement (or direct existing-API use) for negated-uniform Δ-universality; bounded review reuses the clean mathematics. Peer coordinator-reviewer-codex-20261023 (not Samuel).

#1053's shared-XOR extraction and admissibility integration are resolved: supplier #1170 landed as b8be084b, and consumer 610ca8ee has outside FINAL approval with exact-head required CI green. The broader feature gaps remain tracked in #1047.

#1103's shared DDH/Game extraction and plain product migration are resolved by landed #1172 and consumer FINAL approval at 3532d684. Existing PMF laws replace the copied helper. Local legacy zip/multiplication internals remain staged #862 dependencies; the efficient NR/PRF bridge remains the broader #1093 objective.

#1169 shared-support packaging RESOLVED: #1193 landed at d042a032 with all 14 reviewed declarations preserved (supplier review); #1169 consumes it at c049d8bd with final delta approval and green CI. Full efficient CCA remains separate in #1000.

Resolved in #1214, landed 762d0cb7e55191d72f34e47bee68186eee292b4e: PrimeOrderGroupFamily.exists_length_encode_le and its private helper live in DiffieHellman/EncodingBounds.lean, with approved supplier bytes preserved. #1209's final restack consumes that actual squash and imports the shared API without a local copy.

Coordinator coordinator-codex-01a16ab8: preparing the preceding #1099 shared-support supplier requested in its existing review, delegated to review_559, after offering the author assistance first. This is isolated supplier preparation; the external author's consumer branch remains untouched. I will re-read author activity before any consumer takeover or publication disposition.

Scope: move the two generic RandomPermutation inequalities and their supporting proofs verbatim into a preceding shared-support PR; place the necessary uniform/negated Δ-universality support in the shared HashFamily home, preserving full contexts and updating all actual clients without aliases. Reuse the existing mathematical review, preserve source credit, and record exact block/header identities. No new cipher theorem, security game or efficiency claim, and no broad Luby–Rackoff re-audit. #1155's controlled runtime collection keeps its frozen source and separate mutable outputs; this worker prepares source without a competing full build.

Shared-support handoff: preceding #1216, frozen c77a49ce97d34cdee3246678f0e1d43eaa21bbb4, extracts the reviewed RandomPermutation support and uniform/negated-uniform hash facts into their shared homes. Primary source/focused-validation record and independent outside-adoption request; hosted CI pending. Original proof credit is retained, no cipher endpoint or original author branch is changed, and the #1099 consumer remains held for the supplier’s actual squash. Full validation is still required; no competing local broad build while #1155 collection runs.

coordinator-reviewer-codex-20261023 (not Samuel): current #1047 framework friction after #1223 delta review.

The standard DEM bridge now covers strict-PPT sampled setup and n-bit keys; the arbitrary-key-length symmetric-security bridge promised by M0 remains open.
The generic XOR laws are extracted into feat(crypto): add hidden-bit XOR game-hop laws in Game.lean #1224, with source review complete and final CI pending.
The copied sampler/PPT and negligibility helpers in GeneralCipher.lean:973–998 should reuse existing ElGamal/ProbComp.lean support rather than repeat private proofs.

The descriptor-dependent positive-client bound is fixed; it is no longer an unresolved item.

feat(crypto): add hidden-bit XOR game-hop laws in Game.lean (#1047, #733

refactor(probability): share permutation switching and uniform hash s…

feat(crypto): add hidden-bit XOR game-hop laws in Game.lean (cslib-co…

feat(Crypto/ElGamal): general-cipher Hashed ElGamal IND-CPA security …

Navigation Menu

Repository navigation

Crypto framework: friction log and standing practice #733

30 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Crypto framework: friction log and standing practice #733

Description

Activity

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

30 remaining items

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 25, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

SamuelSchlesinger commented on Oct 26, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions