Skip to content

Document reusable assemblies and local contracts #174

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MarcIlunga merged 1 commit into from
Nov 2, 2026
Merged

Document reusable assemblies and local contracts #174

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down
188 changes: 103 additions & 85 deletions REUSE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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] |
Expand All @@ -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
Expand All @@ -54,20 +70,16 @@ 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
[Group]: src/Probability/Group.lean
[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
Expand All @@ -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

Expand Down Expand Up @@ -185,12 +204,11 @@ scripts/review-reuse.sh
scripts/review-reuse.sh <base-commit>
```

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
Expand Down
Loading