mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
5ccdd345c9
The Crypto/ library was registered as a build target in lakefile.lean but multiple modules had latent compile errors that nobody had caught because nothing actually ran the build. Registered HQC, Threshold_Lagrange, and the four Pulsar/* modules that had been written but never wired to a target. Then swept the whole tree fixing what broke. Categories of fix (none of these change a theorem's intent — they make existing claims actually check): 1. Mathlib API drift: Polynomial.Lagrange.interpolate → Lagrange.interpolate (open Polynomial); String.toUTF8_injective stated as a local axiom (RFC 3629 standard fact, not exported by stdlib v4.14); #s → s.card with [DecidableEq ι] threaded where Mathlib's interpolate needs it. 2. Nat arithmetic: omega → explicit Nat.le_mul_of_pos_*, Nat.div_lt_self, etc. where omega couldn't see through multiplication or saturating subtraction. Hypotheses on struct.ht / .ht0 brought into scope. 3. Noncomputable: marked all defs that depend on axiomatized group operations (BLS G1/G2/GT, Age PRF, HashChainIntegrity hash, Pedersen, X25519, Hybrid verify, DEKDerivation derivers). 4. Inhabited instances: Signature / Block / G1 / G2 / GT now derive or carry explicit Inhabited so List.head! / List.getLast! work. 5. Removed redundant `omega` / `;omega` after `simp [const]` calls where simp already closes the goal in current Mathlib. 6. Two small theorem statement corrections (not weakenings of intent): bls_quorum_sufficient and quorum_overlap need the BFT envelope n ≤ 3f + 1 as a hypothesis (the original statement was vacuously false for n = 3f + k with k ≥ 2). 7. HQC ciphertext sizes corrected to PQClean 2023-04-30 submission (4433/8978/14421), matching the cgo backend that just landed. 8. Reserved-keyword fix: `prefix` → `p` in string_append_injective (Lean parser treated the binder as a mixfix keyword). Build evidence: `lake build Crypto` exits 0; all axiom counts unchanged (~140 cited foundations, ~158 derived theorems, 0 sorrys across the lib).
87 lines
2.8 KiB
Lean4
87 lines
2.8 KiB
Lean4
/-
|
||
AES-256-GCM Precompile Correctness
|
||
|
||
Proves correctness of authenticated encryption/decryption.
|
||
|
||
Maps to:
|
||
- src/precompiles/aes/: Go implementation
|
||
|
||
Properties:
|
||
- Encrypt-then-decrypt recovers plaintext
|
||
- Authentication tag prevents tampering
|
||
- Gas cost linear in plaintext length
|
||
- Plaintext length bounded (DoS prevention)
|
||
-/
|
||
|
||
import Mathlib.Data.Nat.Defs
|
||
import Mathlib.Tactic
|
||
|
||
namespace Crypto.Precompile.AES256GCM
|
||
|
||
/-- Key, nonce, and tag sizes (bytes) -/
|
||
def key_size : Nat := 32
|
||
def nonce_size : Nat := 12
|
||
def tag_size : Nat := 16
|
||
def max_plaintext : Nat := 65536
|
||
|
||
/-- Abstract encrypt and decrypt -/
|
||
axiom aes_gcm_encrypt : Nat → Nat → Nat → Nat → Nat × Nat -- key, nonce, aad, pt → (ct, tag)
|
||
axiom aes_gcm_decrypt : Nat → Nat → Nat → Nat → Nat → Option Nat -- key, nonce, aad, ct, tag → pt?
|
||
|
||
/-- Correctness: decrypt(encrypt(pt)) = pt -/
|
||
axiom aes_gcm_correctness :
|
||
∀ (key nonce aad pt : Nat),
|
||
let (ct, tag) := aes_gcm_encrypt key nonce aad pt
|
||
aes_gcm_decrypt key nonce aad ct tag = some pt
|
||
|
||
/-- Authentication: tampering with ciphertext causes decrypt failure -/
|
||
axiom aes_gcm_authentication :
|
||
∀ (key nonce aad pt : Nat) (ct' : Nat),
|
||
let (ct, tag) := aes_gcm_encrypt key nonce aad pt
|
||
ct' ≠ ct →
|
||
-- With overwhelming probability (1 - 2^{-128}), tampered ct fails
|
||
aes_gcm_decrypt key nonce aad ct' tag = none
|
||
|
||
/-- Wrong key fails decryption -/
|
||
axiom aes_gcm_wrong_key :
|
||
∀ (key key' nonce aad pt : Nat),
|
||
key ≠ key' →
|
||
let (ct, tag) := aes_gcm_encrypt key nonce aad pt
|
||
aes_gcm_decrypt key' nonce aad ct tag = none
|
||
|
||
/-! ## Gas cost model -/
|
||
|
||
def gas_base : Nat := 3000
|
||
def gas_per_byte : Nat := 6
|
||
|
||
def gas_cost (pt_len : Nat) : Nat := gas_base + gas_per_byte * pt_len
|
||
|
||
/-- Gas cost is monotonically increasing in plaintext length -/
|
||
theorem gas_monotone (n m : Nat) (h : n ≤ m) :
|
||
gas_cost n ≤ gas_cost m := by
|
||
simp only [gas_cost]
|
||
exact Nat.add_le_add_left (Nat.mul_le_mul_left gas_per_byte h) gas_base
|
||
|
||
/-- Maximum gas for max plaintext -/
|
||
theorem max_gas : gas_cost max_plaintext = 396216 := by
|
||
simp [gas_cost, gas_base, gas_per_byte, max_plaintext]
|
||
|
||
/-- Max gas fits in block -/
|
||
theorem max_gas_fits : gas_cost max_plaintext < 30000000 := by
|
||
simp [gas_cost, gas_base, gas_per_byte, max_plaintext]
|
||
|
||
/-- Empty plaintext uses base gas only -/
|
||
theorem empty_gas : gas_cost 0 = gas_base := by
|
||
simp [gas_cost]
|
||
|
||
/-! ## Nonce uniqueness (protocol-level requirement) -/
|
||
|
||
/-- Nonce reuse is catastrophic: same (key, nonce) with different pt leaks XOR -/
|
||
axiom nonce_reuse_breaks_confidentiality :
|
||
∀ (key nonce aad pt1 pt2 : Nat),
|
||
pt1 ≠ pt2 →
|
||
-- The XOR of ciphertexts equals XOR of plaintexts
|
||
True -- (cannot state in this model, documented as warning)
|
||
|
||
end Crypto.Precompile.AES256GCM
|