Skip to content

Commit 8bd9846

Browse files
quangvdaoquangvdao
authored
feat(crypto): perfect secrecy framework, forking lemma progress, and seeded oracle proofs (#112)
* feat(QueryCache, PreservesInv, CachingOracle): add connective tissue for random oracle proofs - QueryCache: partial order, simp lemmas (empty, cacheQuery), sum spec projections (fst/snd/inl/inr), membership, extensionality - PreservesInv: composition lemma for oracle transformers, bind lemma for StateT invariant preservation - CachingOracle: cache monotonicity (withCaching_cache_le) and PreservesInv instance showing the cache only grows Made-with: Cursor * chore(SimSemantics): silence unused section var warning in apply_compose Use a local `omit [LawfulMonad m]` on `QueryImpl.apply_compose` so the build stays warning-clean except for existing `sorry` declarations. Made-with: Cursor * feat(SeededOracle): prove generateSeed-simulateQ distribution preservation Prove that running an oracle computation with a seeded oracle (backed by a randomly generated seed) preserves the output distribution, i.e. sampling a seed and simulating queries is equivalent to real oracle calls. Key additions: - QuerySeed.pop, prependValues helpers and injectivity lemma (Structures) - probOutput_generateSeed_prependValues factorization lemma (GenerateSeed) - evalDist_generateSeed_eq_of_countEq seed normalization (GenerateSeed) - probOutput_generateSeed_bind_simulateQ_bind main theorem (SeededOracle) - Union bound lemma probEvent_exists_finset_le_sum (EvalDist/Fintype) Made-with: Cursor * fork progress * fix(EvalDist): remove incorrect OracleComp imports from EvalDist/List and EvalDist/BitVec Both files contained lemmas generic over any `m` with `[HasEvalSPMF m]` but incorrectly imported from OracleComp, violating the EvalDist → OracleComp layering. List.lean needed no split — just import and namespace fixes. BitVec.lean's SampleableType instance moved to SampleableType.lean. README updated to fix outdated notation (++ₒ→+, [=x|]→Pr[=x|], etc.). Made-with: Cursor * fork progress: add collision-penalty helper theory and scaffold final bound Extend Fork.lean with seed-slot collision probability bounds and the global collision penalty lemma, then wire these into le_probOutput_fork while leaving the final seed-factor/square step explicitly marked for continuation. Made-with: Cursor * docs(agents): preserve partial proof attempts Add agent guidance to keep unfinished Lean proof structure with local `stop` checkpoints instead of deleting blocks, so later iterations can continue from prior search context. Made-with: Cursor * feat(crypto): standardize perfect secrecy and prove OTP privacy Adopt independence as the canonical perfect-secrecy definition with equivalent formulations, so privacy statements align with textbook semantics and are easier to reuse. Prove one-time-pad privacy against the new notion and document the updated proof status. * feat(crypto): finish Shannon backward proof and remove remaining sorrys Add reusable perfect-secrecy experiment decomposition lemmas and complete the backward Shannon direction constructively. Make the forward direction explicit via a passed hypothesis so the theorem family is fully sorry-free while keeping proof obligations transparent. * refactor(crypto): clarify Shannon statements and add all-priors theorem Replace the misleading Shannon iff path with an explicit constructive theorem over `perfectSecrecyAt`, and add the stronger PMF-prior theorem that proves uniform+unique implies all-priors secrecy. This keeps theorem semantics honest while preserving reusable proof helpers. * refactor: extract helpers, deduplicate proofs, relocate misplaced code - Extract ENNReal Cauchy-Schwarz inequalities to ToMathlib/Data/ENNReal/SumSquares.lean - Factor out cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey in SymmEncAlg.lean, derive both Shannon theorems and ciphertextRowsEqualAt from it - Remove unused perfectSecrecyAt_iff_allDefs / perfectSecrecy_iff_allDefs lemmas - Move XOR probability lemmas to OracleComp/Constructions/BitVec.lean - Add generic probEvent_liftComp_uniformSample_eq_of_eq helper in SeededOracle.lean, simplify seed-slot collision lemmas in Fork.lean - Extract length_eq_of_mem_support_generateSeed to deduplicate repeated blocks Net -150 lines. Made-with: Cursor * chore(Fork): remove superseded commented-out code Delete ~390 lines of old forking lemma code that used obsolete API (guard, getM, [= x | ...] notation, s+1 index bug). All theorem statements are now covered by the active uncommented code. Made-with: Cursor * fix(ci): add missing imports for BitVec and SumSquares to library files Made-with: Cursor
1 parent cab88b5 commit 8bd9846

File tree

20 files changed

+2033
-492
lines changed

20 files changed

+2033
-492
lines changed

‎AGENTS.md‎

Lines changed: 240 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,240 @@
1+
# VCV-io — AI Agent Guide
2+
3+
Formally verified cryptography proofs in Lean 4, built on Mathlib.
4+
5+
## Fast Start For Agents
6+
7+
If you are new to this repo, do this first:
8+
9+
1. Run `lake exe cache get && lake build`.
10+
2. Read `Examples/OneTimePad.lean` for a compact modern proof (correctness and privacy).
11+
3. Keep `VCVio/` as your default work area.
12+
4. If probability lemmas fail unexpectedly, first check for `[spec.Fintype]` and `[spec.Inhabited]`.
13+
14+
`AGENTS.md` is the canonical guide. `CLAUDE.md` is a symlink to this file.
15+
16+
## What This Project Is
17+
18+
VCV-io is a foundational framework for reasoning about cryptographic protocols in the computational model. It provides:
19+
20+
- **`OracleComp spec α`**: A monadic type for computations with oracle access, defined as a free monad (`PFunctor.FreeM`) over a polynomial functor derived from `OracleSpec`.
21+
- **`simulateQ`**: Operational semantics — substitutes oracle queries with concrete implementations via `QueryImpl`.
22+
- **`evalDist`**: Denotational semantics — embeds computations into the `PMF` monad for probability reasoning. This is literally `simulateQ` with uniform distributions as the oracle implementation.
23+
- **`ProbComp α`**: Abbreviation for `OracleComp unifSpec α` (pure probabilistic computation with no custom oracles).
24+
25+
## Repository Structure
26+
27+
```
28+
VCVio/ # Main library (the only part that matters for most work)
29+
OracleComp/ # Core computation type and oracle machinery
30+
OracleSpec.lean # OracleSpec ι := ι → Type v (just a function!)
31+
OracleComp.lean # OracleComp spec α := PFunctor.FreeM spec.toPFunctor
32+
OracleQuery.lean # Single oracle query type
33+
ProbComp.lean # ProbComp = OracleComp unifSpec, sampling notations
34+
SimSemantics/ # Oracle simulation: QueryImpl, simulateQ, state/reader/writer transformers
35+
QueryTracking/ # Counting, logging, caching, seeded oracles
36+
Constructions/ # GenerateSeed, Replicate, SampleableType
37+
Coercions/ # SubSpec (⊂ₒ), automatic lifting between oracle specs
38+
EvalDist.lean # Bridge: evalDist, support, finSupport, probOutput/Event/Failure
39+
EvalDist/ # Denotational semantics machinery
40+
Defs/ # Core: HasEvalSPMF, HasEvalPMF, support, probOutput, Pr[...] notation
41+
Monad/ # Simp lemmas: probOutput_bind, support_pure, etc.
42+
Instances/ # EvalDist for OptionT, ErrorT, ReaderT
43+
CryptoFoundations/ # Crypto primitives and security definitions
44+
SecExp.lean # Security experiments (SecExp, SecAdv)
45+
SymmEncAlg.lean # Symmetric encryption
46+
AsymmEncAlg.lean # Asymmetric encryption
47+
SignatureAlg.lean # Signature schemes
48+
SigmaAlg.lean # Σ-protocols
49+
FiatShamir.lean # Fiat-Shamir transform
50+
Fork.lean # Forking lemma (active research — has sorry)
51+
HardnessAssumptions/ # DDH, DLP, LWE, hard homogeneous spaces
52+
Asymptotics/ # Negligible functions, polynomial-time
53+
ProgramLogic/ # WIP: Hoare-style program logic (mostly stubs)
54+
Prelude.lean # Declares aesop rule set [UnfoldEvalDist]
55+
Examples/ # Concrete crypto constructions (OneTimePad is the canonical complete example)
56+
ToMathlib/ # Upstream candidates for Mathlib (control theory, PFunctor, probability)
57+
LibSodium/ # FFI to C crypto libraries (experimental)
58+
```
59+
60+
### Module Layering (dependency order)
61+
62+
```
63+
ToMathlib → Prelude → EvalDist/Defs → OracleComp core → OracleComp/EvalDist bridge
64+
→ {SimSemantics, QueryTracking, Constructions, Coercions, ProbComp}
65+
→ CryptoFoundations → Examples
66+
```
67+
68+
New files must respect this DAG. In particular, `EvalDist/` files must never import from `OracleComp/`.
69+
70+
`ProgramLogic/` is a WIP side branch. `Relational/Basic.lean` is an empty namespace, and `Unary/Examples.lean` is generic monad theory. Only `HoareTriple.lean` connects to the main library.
71+
72+
## Core Type Signatures
73+
74+
```lean
75+
-- Oracle specification: just a function from index type to response type
76+
def OracleSpec (ι : Type u) : Type _ := ι → Type v
77+
78+
-- Computation with oracle access: free monad over polynomial functor
79+
def OracleComp {ι : Type u} (spec : OracleSpec ι) : Type w → Type _ :=
80+
PFunctor.FreeM spec.toPFunctor
81+
82+
-- Oracle implementation: just a function
83+
@[reducible] def QueryImpl (spec : OracleSpec ι) (m : Type u → Type v) :=
84+
(x : spec.Domain) → m (spec.Range x)
85+
86+
-- Simulation: substitute oracle queries with implementations
87+
def simulateQ [Monad m] (impl : QueryImpl spec m) : OracleComp spec α → m α
88+
89+
-- Pure probabilistic computation (no custom oracles)
90+
abbrev ProbComp := OracleComp unifSpec
91+
```
92+
93+
## Notation Reference
94+
95+
| Notation | Meaning | Defined in |
96+
|----------|---------|------------|
97+
| `Pr[= x \| mx]` | Probability of output `x` (`probOutput`) | `EvalDist/Defs/Basic.lean` |
98+
| `Pr[p \| mx]` | Probability of event `p` (`probEvent`) | `EvalDist/Defs/Basic.lean` |
99+
| `Pr[⊥ \| mx]` | Probability of failure (`probFailure`) | `EvalDist/Defs/Basic.lean` |
100+
| `$ᵗ T` | Uniform type-level sampling (`uniformSample`, requires `SampleableType`) | `Constructions/SampleableType.lean` |
101+
| `$ xs` | Uniform container selection (can fail) | `OracleComp/ProbComp.lean` |
102+
| `$! xs` | Uniform container selection (never fails) | `OracleComp/ProbComp.lean` |
103+
| `$[0..n]` | Uniform selection from `Fin n` | `OracleComp/ProbComp.lean` |
104+
| `spec₁ + spec₂` | Combine oracle specs (was `++ₒ`, now uses standard `+`) | `OracleComp/OracleSpec.lean` |
105+
| `⊂ₒ` | SubSpec relation (auto-lifts via `MonadLift`) | `Coercions/SubSpec.lean` |
106+
| `→ₒ` | Singleton oracle spec `(T →ₒ U)` | `OracleComp/OracleSpec.lean` |
107+
| `[]ₒ` | Empty oracle spec | `OracleComp/OracleSpec.lean` |
108+
| `∘ₛ` | QueryImpl composition | `SimSemantics/Constructions.lean` |
109+
| `⦃P⦄ comp ⦃Q⦄` | Hoare triple (scoped to `OracleComp.StateM`) | `ProgramLogic/Unary/HoareTriple.lean` |
110+
111+
**WARNING**: The README uses `[= x | comp]` notation (without `Pr` prefix) — this is outdated. Always use `Pr[...]`.
112+
113+
### Legacy API Migration (Do / Don't)
114+
115+
| Don't use | Do use |
116+
|-----------|--------|
117+
| `[= x \| comp]` | `Pr[= x \| comp]` |
118+
| `++ₒ` | `+` |
119+
| Commented legacy blocks as templates | Un-commented modern code paths and `Examples/OneTimePad.lean` |
120+
121+
## Critical Gotchas
122+
123+
### 1. `[spec.Fintype]` and `[spec.Inhabited]` are required for probability reasoning
124+
125+
Any file using `evalDist`, `probOutput`, `probEvent`, or `Pr[...]` on `OracleComp spec` needs these instances on the spec. Without them, typeclass resolution silently fails with confusing errors.
126+
127+
### 2. `autoImplicit` is `false` project-wide
128+
129+
Every variable must be explicitly declared. Do not rely on Lean's auto-implicit mechanism.
130+
131+
### 3. Core types are `@[reducible]` thin wrappers
132+
133+
`OracleSpec`, `QueryImpl`, and `OracleComp` are all defined as simple `def`/`abbrev`/`@[reducible]` over `PFunctor` machinery. Lean may unfold them aggressively. Use `OracleComp.inductionOn` / `OracleComp.construct` as canonical eliminators rather than pattern matching on `PFunctor.FreeM.pure`/`roll` directly.
134+
135+
### 4. `evalDist` IS `simulateQ`
136+
137+
They share the exact same code path: `evalDist` is `simulateQ` with `m = PMF` and uniform distributions. This identity is definitional (`rfl`).
138+
139+
### 5. `++ₒ` is dead — use `+`
140+
141+
The README and large amounts of commented-out code use `++ₒ` for combining oracle specs. The current API uses standard `+` (`HAdd`).
142+
143+
### 6. Commented-out code uses OLD API patterns
144+
145+
Files like `Fork.lean`, `HHS_Elgamal.lean`, `HHS_Sigma.lean`, and `RF_RP_Switching_alt.lean` contain large commented-out blocks that use obsolete patterns (`[= x | ...]`, `++ₒ`, `simulate'`, `getM`, `guard` via `Alternative`). **Only follow patterns in uncommented code.** Use `Examples/OneTimePad.lean` as the canonical reference for a completed proof.
146+
147+
### 6b. Preserve partial proof attempts (prefer `stop` over deletion)
148+
149+
When a proof attempt is not finished or is currently broken, prefer leaving the attempted structure in place and insert a local `stop`/checkpoint marker instead of deleting large proof blocks. This preserves search context and failed approaches for later agents to continue from.
150+
151+
### 7. Structure inheritance pattern for crypto primitives
152+
153+
Crypto structures (`SymmEncAlg`, `AsymmEncAlg`, `SignatureAlg`, `SecExp`) extend `OracleContext` or `ExecutionMethod`. Fill parent fields with anonymous field syntax:
154+
155+
```lean
156+
@[simps!] def myAlg : SymmEncAlg ℕ (M := ...) (K := ...) (C := ...) where
157+
keygen n := ...
158+
encrypt k m := ...
159+
decrypt k σ := ...
160+
__ := unifSpec.defaultContext
161+
```
162+
163+
### 8. Universe polymorphism
164+
165+
`OracleComp` has 3 universe parameters, `SubSpec` has 6. Universe unification errors are common when composing specs or building reductions. When stuck, check universe levels explicitly.
166+
167+
## Proof Patterns
168+
169+
### Tactics
170+
171+
- **`simp`** with project-specific simp lemmas is the starting point (most lemmas in `EvalDist/Monad/` are `@[simp]`)
172+
- **`grind`** is the workhorse tactic. Many lemmas are tagged `@[grind =]` or `@[grind =>]`. The `=`/`=>` annotations matter.
173+
- **`aesop`** with custom rule sets (e.g., `aesop (rule_sets := [UnfoldEvalDist])`) for evaluation/unfolding
174+
- Standard Mathlib tactics (`rw`, `exact`, `apply`, `ext`, `congr`, `calc`) are used throughout
175+
176+
### Lemma Naming
177+
178+
Follow Mathlib convention: `{head_symbol}_{operation}_{rhs_form}`.
179+
180+
Examples: `probOutput_bind_eq_tsum`, `support_pure`, `simulateQ_map`, `evalDist_bind`.
181+
182+
Use `_iff` for biconditionals, `_congr`/`_mono` for relational lemmas, primed variants (`'`) for versions with weaker hypotheses.
183+
184+
### Structure/Class Names
185+
186+
Use UpperCamelCase: `ForkInput`, `QueryImpl`, `SecExp`, `SymmEncAlg`.
187+
188+
## Canonical Examples By Task
189+
190+
- Need a compact modern crypto proof flow (correctness + privacy): start with `Examples/OneTimePad.lean`.
191+
- Working on oracle computation core behavior: read `VCVio/OracleComp/OracleComp.lean`.
192+
- Working on probability/evaluation lemmas: read `VCVio/EvalDist/Monad/Basic.lean`.
193+
- Working on subspec coercions/lifting issues: read `VCVio/OracleComp/Coercions/SubSpec.lean`.
194+
- Touching forking-lemma research code: read uncommented parts of `VCVio/CryptoFoundations/Fork.lean`.
195+
196+
## Building
197+
198+
```bash
199+
lake exe cache get && lake build
200+
```
201+
202+
The `lake exe cache get` step downloads Mathlib's pre-compiled cache and is essential (building Mathlib from source takes hours).
203+
204+
### Adding New Files
205+
206+
After adding a new `.lean` file, run:
207+
208+
```bash
209+
./scripts/update-lib.sh
210+
```
211+
212+
This regenerates the root import files (`VCVio.lean`, `Examples.lean`, `ToMathlib.lean`). CI checks that these are up to date.
213+
214+
Then run `lake build` to verify imports and dependencies are still valid.
215+
216+
### Version Pinning
217+
218+
Lean toolchain and Mathlib version must stay in sync (both currently `v4.28.0`). When upgrading, update both `lean-toolchain` and `lakefile.lean`'s `require mathlib` line simultaneously, then run `lake update`.
219+
220+
### Linters
221+
222+
Several Mathlib-style linters are enabled as weak linters (warn, don't error). `longFile` caps at 1500 lines. The lint CI job is currently commented out in `build.yml`.
223+
224+
## Troubleshooting Quick Hits
225+
226+
### Probability lemmas fail with confusing typeclass errors
227+
228+
Check that your active `spec` has `[spec.Fintype]` and `[spec.Inhabited]` in scope before using `evalDist`, `probOutput`, `probEvent`, or `Pr[...]`.
229+
230+
### Universe mismatch errors around `SubSpec` or composed specs
231+
232+
`OracleComp` and `SubSpec` are highly universe-polymorphic. Introduce explicit universe parameters and explicit type annotations at composition boundaries.
233+
234+
### Unexpected import-cycle or layering failures
235+
236+
Re-check the layering DAG: `EvalDist/` must not import from `OracleComp/`, and new files must respect the stated module order.
237+
238+
## File Size Guideline
239+
240+
Files should stay under 1500 lines (enforced by `linter.style.longFile`). Line length soft limit is 100 characters.

‎CLAUDE.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
AGENTS.md

‎Examples/OneTimePad.lean‎

Lines changed: 33 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,15 @@ Copyright (c) 2024 Devon Tuma. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Devon Tuma
55
-/
6-
import VCVio
6+
import VCVio.CryptoFoundations.SymmEncAlg
7+
import VCVio.OracleComp.Constructions.BitVec
78
import Mathlib.Data.Vector.Zip
89

910
/-!
1011
# One Time Pad
1112
12-
This file defines and proves the perfect secrecy of the one-time pad encryption algorithm.
13+
This file defines the one-time pad scheme, proves correctness, and proves perfect secrecy
14+
in the canonical independence form used by `SymmEncAlg.perfectSecrecy`.
1315
-/
1416

1517
open Mathlib OracleSpec OracleComp ENNReal BigOperators
@@ -30,4 +32,33 @@ namespace oneTimePad
3032
lemma complete : (oneTimePad).Complete := by
3133
simp [oneTimePad, SymmEncAlg.Complete, SymmEncAlg.CompleteExp]
3234

35+
lemma probOutput_cipher_uniform (sp : ℕ)
36+
(mgen : OracleComp oneTimePad.spec (BitVec sp)) (σ : BitVec sp) :
37+
Pr[= σ | oneTimePad.PerfectSecrecyCipherExp sp mgen] =
38+
(Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
39+
simpa [SymmEncAlg.PerfectSecrecyCipherExp, SymmEncAlg.PerfectSecrecyExp, oneTimePad] using
40+
probOutput_cipher_from_pair_uniform sp (mx := simulateQ oneTimePad.impl mgen) σ
41+
42+
/-- The one-time pad is perfectly secret in the canonical independence form. -/
43+
lemma perfectSecrecyAt (sp : ℕ) : oneTimePad.perfectSecrecyAt sp := by
44+
intro mgen msg σ
45+
have hpair :
46+
Pr[= (msg, σ) | oneTimePad.PerfectSecrecyExp sp mgen] =
47+
Pr[= msg | oneTimePad.PerfectSecrecyPriorExp sp mgen] *
48+
(Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := by
49+
simpa [SymmEncAlg.PerfectSecrecyExp, SymmEncAlg.PerfectSecrecyPriorExp, oneTimePad] using
50+
probOutput_pair_xor_uniform sp (mx := simulateQ oneTimePad.impl mgen) msg σ
51+
calc
52+
Pr[= (msg, σ) | oneTimePad.PerfectSecrecyExp sp mgen] =
53+
Pr[= msg | oneTimePad.PerfectSecrecyPriorExp sp mgen] *
54+
(Fintype.card (BitVec sp) : ℝ≥0∞)⁻¹ := hpair
55+
_ = Pr[= msg | oneTimePad.PerfectSecrecyPriorExp sp mgen] *
56+
Pr[= σ | oneTimePad.PerfectSecrecyCipherExp sp mgen] := by
57+
rw [probOutput_cipher_uniform]
58+
59+
/-- The one-time pad is perfectly secret for all security parameters. -/
60+
lemma perfectSecrecy : oneTimePad.perfectSecrecy := by
61+
intro sp
62+
exact perfectSecrecyAt sp
63+
3364
end oneTimePad

0 commit comments

Comments
 (0)