From edb4e48a6de3705e138fd417acbfc89465f544e4 Mon Sep 17 00:00:00 2001 From: Marc Ilunga Date: Mon, 2 Nov 2026 21:52:29 +0100 Subject: [PATCH] Document assembly clients and their explicit contracts --- AGENTS.md | 2 + REUSE.md | 188 ++++++++++++++++++++++++++++++------------------------ 2 files changed, 105 insertions(+), 85 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 295eef4..ac8aa21 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -400,6 +400,8 @@ globally; use `letI` or a wrapper carrier. mechanisms. Random-systems vocabulary is DDS, DDC, DDE and PDS; avoid operational names such as `exec`, `step`, `fuel`, `scheduler` and `reset` for mathematical objects. +- Name reusable objects neutrally, such as `PKE.system`; real and ideal name + their roles in a particular comparison. - Preserve an existing declaration name as one atom inside theorem names, and state the operation and conclusion: `_iff`, `_eq`, `_le`, `_subset`, `_mono`, `_of_`, `_comp`. diff --git a/REUSE.md b/REUSE.md index 27d3799..23a40ba 100644 --- a/REUSE.md +++ b/REUSE.md @@ -5,29 +5,30 @@ law in a construction, identify its declaration, owner, parameters, domain and s Use the live declaration to check the fit. The map below supplies starting points, not a list of interchangeable objects. -Ideal systems are in the `Commons` namespace; typed systems and converters are in -`SystemAlgebra`. The probability operations below are in `Probability.Distribution`. +Ideal systems, schemes and constructions are in `Commons`; typed systems, converters and games +are in `SystemAlgebra`. The probability operations below are in `Probability.Distribution`. | Needed object | Declaration and module | | --- | --- | -| Random function | `URF` in [Ideal] | -| Random permutation | `URP` in [Ideal] | +| Random function | `URF`, `URF.lazy_eq` in [Ideal] | +| Random permutation | `URP` in [Ideal]; `URP.lazy_eq` in [LazyPermutation] | | Forward and inverse queries to one permutation | `StrongURP` in [Ideal] | | Independent permutation per tweak | `TweakableURP`, `TweakableStrongURP` in [Ideal] | | Fresh samples | `TypedSystem.source` in [Source]; `MemorylessSource` in [Ideal] | | Fresh query-dependent replies | `TypedSystem.ofMemoryless` in [Memoryless] | -| Ordered tuple collection | `TypedConverter.collect` and its functional/source laws in [Collector] | -| Finite-family hybrid | `parallelAllImplication`, `distance_smul_parallelAll_le_sum` in [FamilyHybrid] | +| Ordered tuple collection | `TypedConverter.collect` in [Collector] | +| Family hybrid | `parallelAllImplication`, `distance_smul_parallelAll_le_sum` in [FamilyHybrid] | | Fixed finite-family context | `TypedConverter.parallelAllContext` in [FamilyContext] | | Fresh reply families | `TypedSystem.parallelAll_ofMemoryless` in [FamilyMemoryless] | | Retained key, fresh replies | `TypedSystem.keyed` in [Keyed] | +| Signature oracle | `SignatureScheme.system.eq_keyed` in [Signature] | | Retained state | `TypedSystem.sample` in [Functional]; `ofAutomaton` in [Automaton] | -| Hidden monotone event on retained state | `TypedGame.ofAutomaton` in [AutomatonGame] | +| Hidden condition on initial draw and inputs | `TypedGame.ofAutomaton` in [AutomatonGame] | | URF distinct-input collision game | `URF.collisionGame` in [CollisionGame] | | Adaptive URF collision bound | `URF.collisionGame_win_le` in [CollisionBound] | | Retained state with fresh transitions | `TypedSystem.ofProbAutomaton` in [ProbAutomaton] | | Retained key as an automaton | `TypedSystem.ofProbAutomaton_eq_keyed` in [KeyedAutomaton] | -| Program with fresh inside transitions | `TypedConverter.ofProgram_smul_ofProbAutomaton` in [ProbProgramAttachment] | +| Program attachment | `TypedConverter.ofProgram_smul_ofProbAutomaton` in [ProgramAttachment] | | Independent joint law | `prodProbDist` in [Distribution] | | Independent finite family of draws | `ProbDist.pi` in [Distribution] | | Independent draws with different outcome types | `ProbDist.piDep` in [DependentProduct] | @@ -36,14 +37,29 @@ Ideal systems are in the `Commons` namespace; typed systems and converters are i | Root blinding | `ProbDist.blindRootSolver`, `ProbDist.rootSuccessLaw` in [Group] | | RSA unit-root blinding | `Commons.RSA.blinding_success_eq` in [RSA] | | Nonce-unique encryption inputs | `nonceRestricted` in [Nonce] | -| KEM–DEM composition | `KEMDEM.scheme` and `KEMDEM.correct` in [KEM–DEM](src/Commons/Constructions/KEMDEM.lean) | +| KEM–DEM composition | `KEMDEM.scheme` in [KEMDEM]; `KEMDEM.correct` in [KEMDEMCorrectness] | +| Encrypt-then-MAC | `encryptThenMAC.system` in [EncryptThenMAC]; [roundtrip][EtMCorrectness] | +| Hash-and-sign | `hashAndSign.system` and its correctness contract in [HashAndSign] | +| Recorded-reply rejection | `TypedConverter.recordingGuard` in [RecordingGuard] | +| Hidden-bit guessing | `TypedDistinguisher.guessingProbability` in [Guessing] | | Nonce/AD encrypt-then-MAC | `nonceEncryptThenMAC` in [NonceEncryptThenMAC] | -| Hash-and-sign | `hashAndSign` in [HashAndSign] | | Restricted interface | `TypedConverter.filter` in [Filter] | | Relabeled interface | `TypedConverter.rename` in [Relabel] | | One-query input and reply translation | `TypedConverter.routing` in [QueryRouting] | | Shared access by tagged callers | `routing` in [QueryRouting], `smul_sample` in [Functional] | +[LazyPermutation]: src/Commons/Definitions/LazyPermutation.lean +[Signature]: src/Commons/Definitions/Signature/Keyed.lean +[EncryptThenMAC]: src/Commons/Constructions/EncryptThenMAC.lean +[EtMCorrectness]: src/Commons/Constructions/EncryptThenMAC/Correctness.lean +[HashAndSign]: src/Commons/Constructions/HashAndSign.lean +[RecordingGuard]: src/RandomSystems/Typed/RecordingGuard.lean +[AutomatonGame]: src/RandomSystems/Typed/AutomatonGame.lean +[CollisionGame]: src/Commons/Definitions/CollisionGame.lean +[CollisionBound]: src/Commons/Definitions/CollisionBound.lean +[Guessing]: src/RandomSystems/Typed/Guessing.lean +[KEMDEM]: src/Commons/Constructions/KEMDEM.lean +[KEMDEMCorrectness]: src/Commons/Constructions/KEMDEM/Correctness.lean [Ideal]: src/Commons/Definitions/Ideal.lean [Source]: src/RandomSystems/Typed/Source.lean [Keyed]: src/RandomSystems/Typed/Keyed.lean @@ -54,12 +70,9 @@ Ideal systems are in the `Commons` namespace; typed systems and converters are i [FamilyMemoryless]: src/RandomSystems/Typed/ParallelAllMemoryless.lean [Functional]: src/RandomSystems/Typed/Functional.lean [Automaton]: src/RandomSystems/Typed/Automaton.lean -[AutomatonGame]: src/RandomSystems/Typed/AutomatonGame.lean -[CollisionGame]: src/Commons/Definitions/CollisionGame.lean -[CollisionBound]: src/Commons/Definitions/CollisionBound.lean [ProbAutomaton]: src/RandomSystems/Typed/ProbAutomaton.lean [KeyedAutomaton]: src/RandomSystems/Typed/KeyedAutomaton.lean -[ProbProgramAttachment]: src/RandomSystems/Typed/ProbProgramAttachment.lean +[ProgramAttachment]: src/RandomSystems/Typed/ProbProgramAttachment.lean [Distribution]: src/Probability/Distribution.lean [DependentProduct]: src/Probability/DependentProduct.lean [Kernel]: src/Probability/Kernel.lean @@ -67,7 +80,6 @@ Ideal systems are in the `Commons` namespace; typed systems and converters are i [RSA]: src/Commons/Definitions/RSA.lean [Nonce]: src/Commons/Definitions/Nonce.lean [NonceEncryptThenMAC]: src/Commons/Constructions/NonceEncryptThenMAC.lean -[HashAndSign]: src/Commons/Constructions/HashAndSign.lean [Filter]: src/RandomSystems/Typed/Filter.lean [Relabel]: src/RandomSystems/Typed/Relabel.lean [QueryRouting]: src/RandomSystems/Typed/QueryRouting.lean @@ -83,70 +95,77 @@ Read the declaration and its documentation, then use `#check` or `#print` in the to inspect its complete signature. An interface mismatch calls for explicit routing, renaming or restriction, or an extension in the owning module. Keep the domain guarantee in that bridge. -## Before implementation - -The client supplies the mathematical inputs to existing objects: - -| Input | Existing boundary | Local obligation | -| --- | --- | --- | -| A retained draw | `TypedSystem.sample` | Which operations share it. | -| Fresh reply laws | `TypedSystem.ofMemoryless` | Interface and admitted queries. | -| Random transitions | `RandomSystem.ofProbAutomaton` | Domain, invariant or simulation. | -| Uniform functions or permutations | [Ideal] | Interface and sharing. | -| Independent families | `∥ k, R k`, `⨂ₘ k, α k` | Component contracts and call allowances. | -| Relabeling or restriction | [Relabel], [Filter] | Wiring or admission. | -| A standard scheme | e.g. `PKE.system` | Algorithms and their contracts. | -| A common context | `≫`, `•`, `∥`, `cc_normalize`, `cc_substitute` | Local equality or bound. | - -Keep types and domains in shared declarations, and explain parameters beside their binders. -Use construction names for objects; real/ideal labels identify their roles in an experiment. -Choose the standard object before writing its implementation or introducing another wrapper. -The [PKE correspondence](src/Commons/Definitions/PublicKeyEncryption/Keyed.lean) exposes -`TypedSystem.keyed` under the existing CCA converter, with one pair and fresh encryption replies. - -1. Map the intended objects and laws to existing declarations. For each gap, state the missing - capability. Put this short mapping in the task update or ignored `Scratch/` working notes. -2. Write the system assembly using these declarations. Identify the owner of every retained - draw, its callers, and the domain and budget at each interface. -3. Compare constructions under their common context. Compile the assembly with component - contracts as hypotheses, then instantiate it with the chosen existing objects. -4. Implement the missing components and their contracts. Keep reusable laws in the model's - owning module, available to every world and proof that uses them. - -Check a changed boundary with the smallest relevant integration probe: - -- A retained parameter shared by several operations, with fresh replies on each call. -- A finite parallel family and a shared component, preserving their different sampling scopes. -- A standard construction assembled from named components and supplied contracts. - -Inspect the definition and elaborated goals. Routine normalization, wiring and transport should -leave the stated local mathematics. A difficult local claim can remain an explicit hypothesis -while the surrounding conditional theorem is checked; discharge it for an unconditional result. -Add another example only when it exercises a different capability. - -Consumer projects must adopt this workflow in their own contributor instructions and link to -this guide at their dependency version. Importing the library does not apply its `AGENTS.md` -to that checkout. - -The [compiled examples](src/Examples/Usability.lean) include a canonical permutation inside -different surrounding assemblies. The -[general comparison test](src/Tests/ProofErgonomics.lean) normalizes two different wirings and -then uses only the supplied component equation. - -For a retained-state component, use `ProbDist.map init P`; name `P` when it is a nontrivial -law shared by several statements. The -[AE assembly contracts](src/Examples/AuthenticatedEncryption/Hybrid.lean) compose named sources -and programs before opening their transition rules. `inline` supplies the combined automaton; -`prodProbDist_map` and `ProbDist.map_map` normalize its initial law, preserving independent draws. - -For each draw, `automatonSystem_eq_of_bisim` turns the local bisimulation into equality of -deterministic systems. `TypedSystem.ofAutomaton_map_congr` lifts this equality when both -representations use the same law `P`. Compose these component equations to obtain `hybrid_system` -or `ideal_system`, then read transcript masses. - -The [PRG example](src/Examples/PRGLengthExtension.lean) defines its real world with -`MemorylessSource` and the mapped seed law. Its converter contracts use explicit equalities -`R = TypedSystem.ofMemoryless A ν`; `inline using` leaves only the reply-law calculation. +## Client workflow + +1. Import the owning modules. At the CC layer, use `ConstructiveCryptography.Notation` and + `open scoped SystemAlgebra NNReal`. Find the stock system, interface or converter and check its + domain, query costs and sampling scope. +2. Define a short named assembly with `•`, `≫`, `∥` and `⨂ₘ`. Keep retained draws in their + owning components and make interface rewirings explicit. +3. State the component contracts. Apply a named correctness law or normalize the common + context, then carry the supplied local equality or bound through it. +4. Prove the remaining local claim in its owning layer. A difficult claim can stay an explicit + hypothesis while the surrounding conditional theorem is checked. + +The [three compiled clients](src/Tests/AuthoringWorkflows.lean) import these owning modules +together: + +```lean +import Commons.Definitions.PublicKeyEncryption.Keyed +import Commons.Constructions.EncryptThenMAC +import RandomSystems.Typed.FiniteFamilyCollect +``` + +- **Retained oracle:** [retainedOracle_snoc](src/Tests/AuthoringWorkflows.lean). Use + `PKE.system.perPort (budget := q) scheme`, where `q : PKE.Port → ℕ` bounds each port. + Write `h` for the prior history, `m` for the next plaintext, and `c` for its candidate reply; + `ν keys` is the supplied reply law at key pair `keys`. Publication, encryption and decryption + share the pair; each encryption reply is fresh conditional on it. After supplying admission + of the next query after `h`, rewriting with `PKE.system.perPort_eq_keyed` and + `TypedSystem.keyed_snoc` leaves `scheme.enc keys.1 m = ν keys` at generated pairs. + The extended-history mass sums `scheme.gen keys` times that pair's likelihood of `h` and + `ν keys c`. +- **Shared value and independent sources:** + [collectedSharedSources_eq](src/Tests/AuthoringWorkflows.lean). `retainedDrawClient` defines + `collector • TypedSystem.sample P (fun s => ∥ k, R s k)`, with one retained `s ∼ P`; + here `collector` abbreviates the client's `TypedConverter.collect` expression. + Supply `R s k = TypedSystem.source (μ s k) q` for every `s` and `k`. + `TypedConverter.smul_sample` and `collect_smul_parallelAll_source` give + `TypedSystem.sample P (fun s => TypedSystem.source (ProbDist.piDep (μ s)) q)`. + Replies are independent conditional on `s`; the shared draw stays outside the family. + The collector's explicit order visits each component once, so `q` outside triggers fit + each component's allowance of `q`. +- **Construction bound:** + [encryptThenMAC_component_bound](src/Tests/AuthoringWorkflows.lean). + `encryptThenMACClient` defines + `context • encryptThenMAC.system scheme mac q`. `rw [encryptThenMACClient]` followed by + `cc_normalize` exposes the assembly. + `cc_nonexpand` transports a bound through the fixed MAC and both attachments, leaving exactly + `Δ (AE.system scheme) cipher' ≤ ε`, supplied as `hlocal`. The replacement `cipher'` has + interface `AE M C (2 * q)`, the declared inside allowance. Here `ε : ℝ≥0` bounds this + cipher hybrid; the MAC keeps its own independent key. + +Keep a difficult obligation as a named theorem parameter, such as the last client's `hlocal`, +and finish the conditional proof using it. Prove the obligation separately to apply that +theorem. [Contract checks](src/Tests/ContractApplication.lean) pin the elaborated local goals. +Key support, domain admission and supplied component contracts remain explicit premises. + +Use neutral names such as `PKE.system`; real/ideal names describe roles in a comparison. +Share ambient types and instances in a short section. Explain unfamiliar symbols beside their +binders, and use named contracts instead of nested representation projections. Before implementing +an internal program, compile its intended assembly and endpoint using explicit component contracts. + +For representation changes, use the existing boundary once: `TypedSystem.ofProbAutomaton_eq_keyed` +for retained-key transitions, `TypedSystem.ofProbAutomaton_eq_of_simulation` for conditional state +laws, or `TypedSystem.ofAutomaton_map_congr` for representations initialized from one draw law +`P` whose deterministic systems agree at every draw. Clients then rewrite that component equation. +Stock constructions also supply property contracts: +`encryptThenMAC.system.enc_dec_eq_of_correct` uses encryption and MAC correctness; +`hashAndSign.system.sign_verify_eq_of_correct` uses signing correctness for any hash `H : M → D`. +Their budget hypotheses admit both queries of the roundtrip. + +Consumer projects adopt this workflow in their own contributor instructions and link to this +guide at their dependency version. The library's `AGENTS.md` applies to this checkout. ## Reuse preserves sampling scope @@ -185,12 +204,11 @@ scripts/review-reuse.sh scripts/review-reuse.sh ``` -It reports added definition heads and common probability-construction sites in tracked changes -and untracked Lean files. It scans the current Git checkout, including Lean modules outside -`src/`. Inspect each site against the object map: reuse an existing object, extend its owner, -or explain the distinct mathematical object. The scan is lexical: it can flag -comments and proof rewrites and misses other spellings, so it neither finds every semantic -duplicate nor certifies their absence. CI does not run it. +It reports added definitions and common sampling sites in tracked changes and untracked Lean +files, including modules outside `src/`. Inspect each site against the object map: reuse an +existing object, extend its owner, or explain the distinct mathematical object. This lexical +index includes comments and can miss other spellings; semantic reuse requires reading the +definitions. CI does not run it. `cc_normalize` and the [proof commands](src/ConstructiveCryptography/DSL/GRAMMAR.md#proof-commands) assemble supplied equations and bounds. They preserve the chosen sampling scope and leave