diff --git a/verification/Proofs/AddSpec.lean b/verification/Proofs/AddSpec.lean new file mode 100644 index 0000000..bcd70e4 --- /dev/null +++ b/verification/Proofs/AddSpec.lean @@ -0,0 +1,90 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/AddSpec.lean — addition of the transpiled Fp. + + RUST ANALOG (src/fields/fp.rs:392-403): 4-limb adc chain computing the raw + sum d = a + b (the final carry is PROVABLY zero: a, b < p < 2²⁵⁵ so + a + b < 2²⁵⁶), followed by `(&Fp(d)).sub(&MODULUS)` — the same conditional + reduction proven general in Proofs/SubNegSpec.lean (d < 2P shape). + + SPEC (exact ℕ, additive): + Canon a → Canon b → + add a b = ok r with Canon r ∧ (r = a + b ∨ r + P = a + b). + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.SubNegSpec +open Aeneas Aeneas.Std Result +open pasta_curves + +set_option maxHeartbeats 8000000 +set_option linter.unusedTactic false +set_option linter.unreachableTactic false + +namespace PastaProofs + +open Aeneas.Std.WP + +macro "dis" : tactic => + `(tactic| (subst_vars; try simp [Array.set_val_eq, *]; try scalar_tac)) + +/-- `Fp::add`: total, canonical, exact value (see file header). -/ +theorem add_spec (a b : Fe) (ha : Canon a) (hb : Canon b) : + fields.fp.Fp.add a b + ⦃ r => Canon r ∧ + (feVal r = feVal a + feVal b ∨ + feVal r + P = feVal a + feVal b) ⦄ := by + obtain ⟨a0, a1, a2, a3, hla⟩ := Fe.exists_limbs a + obtain ⟨b0, b1, b2, b3, hlb⟩ := Fe.exists_limbs b + unfold Canon at ha hb + rw [feVal_eq a a0 a1 a2 a3 hla] at ha + rw [feVal_eq b b0 b1 b2 b3 hlb] at hb + unfold fields.fp.Fp.add + let* ⟨ i, hi ⟩ ← Array.index_usize_spec by dis + let* ⟨ i1, hi1 ⟩ ← Array.index_usize_spec by dis + let* ⟨ d0, carry0, hadc0 ⟩ ← adc_spec by dis + let* ⟨ i2, hi2 ⟩ ← Array.index_usize_spec by dis + let* ⟨ i3, hi3 ⟩ ← Array.index_usize_spec by dis + let* ⟨ d1, carry1, hadc1 ⟩ ← adc_spec by dis + let* ⟨ i4, hi4 ⟩ ← Array.index_usize_spec by dis + let* ⟨ i5, hi5 ⟩ ← Array.index_usize_spec by dis + let* ⟨ d2, carry2, hadc2 ⟩ ← adc_spec by dis + let* ⟨ i6, hi6 ⟩ ← Array.index_usize_spec by dis + let* ⟨ i7, hi7 ⟩ ← Array.index_usize_spec by dis + let* ⟨ d3, carry3, hadc3 ⟩ ← adc_spec by dis + -- identify reads + have hv_i : i.val = a0.val := by simp [hi, hla] + have hv_i1 : i1.val = b0.val := by simp [hi1, hlb] + have hv_i2 : i2.val = a1.val := by simp [hi2, hla] + have hv_i3 : i3.val = b1.val := by simp [hi3, hlb] + have hv_i4 : i4.val = a2.val := by simp [hi4, hla] + have hv_i5 : i5.val = b2.val := by simp [hi5, hlb] + have hv_i6 : i6.val = a3.val := by simp [hi6, hla] + have hv_i7 : i7.val = b3.val := by simp [hi7, hlb] + have hb_d0 : d0.val < 2^64 := by scalar_tac + have hb_d1 : d1.val < 2^64 := by scalar_tac + have hb_d2 : d2.val < 2^64 := by scalar_tac + have hb_d3 : d3.val < 2^64 := by scalar_tac + -- the raw sum: Σd + 2²⁵⁶·carry3 = a + b < 2P < 2²⁵⁶, hence carry3 = 0 + have hsum : limbsVal d0 d1 d2 d3 + 2^256 * carry3.val = + limbsVal a0 a1 a2 a3 + limbsVal b0 b1 b2 b3 := by + unfold limbsVal at * + omega + -- the conditional reduction: sub (Σd) MODULUS with Σd < 2P + have hMle : feVal fields.fp.MODULUS ≤ P := le_of_eq feVal_MODULUS + have hdlt : feVal (Array.make 4#usize [d0, d1, d2, d3] (by simp)) < + feVal fields.fp.MODULUS + P := by + rw [feVal_MODULUS, feVal_make] + unfold limbsVal P at * + omega + -- MEMORY DISCIPLINE (post 2026-07-02 OOM): sub_spec's two arithmetic + -- preconditions are discharged by EXACT matches against the facts proven + -- above — never by the blanket `dis` (simp [*] + scalar_tac saturates in + -- this ~60-hypothesis context and allocates without bound). + let* ⟨ r, hr_canon, hr_val ⟩ ← sub_spec by + (first | exact hMle | exact hdlt) + -- conclude + rw [feVal_eq a a0 a1 a2 a3 hla, feVal_eq b b0 b1 b2 b3 hlb] + refine ⟨hr_canon, ?_⟩ + rw [feVal_MODULUS, feVal_make] at hr_val + unfold Canon limbsVal P at * + omega + +end PastaProofs diff --git a/verification/Proofs/ConstSpecs.lean b/verification/Proofs/ConstSpecs.lean new file mode 100644 index 0000000..e1f8387 --- /dev/null +++ b/verification/Proofs/ConstSpecs.lean @@ -0,0 +1,103 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ConstSpecs.lean — the transpiled constants are the right numbers. + + RUST ANALOG (src/fields/fp.rs): `MODULUS` (feVal_MODULUS lives in + SubNegSpec.lean), `R = 2²⁵⁶ mod p` (Montgomery one), `R2 = 2⁵¹² mod p`, + `INV = −p⁻¹ mod 2⁶⁴` (the Montgomery reduction multiplier), `zero`, `one`. + + Every proof here is kernel-checked literal arithmetic (norm_num on + 256/512-bit numerals — GMP-backed, milliseconds; NO native_decide). + + WHY THESE MATTER + * `INV_spec` is THE hinge of montgomery_reduce: k = r·INV makes + r + k·p ≡ 0 (mod 2⁶⁴) — each reduction round clears one limb exactly. + * `R_val`/`one` give ⟪one⟫ = 1 (the denotation absorbs the R factor). + * `R2_val` makes from_raw(x) = mont_mul(x, R2) denote x (used later for + GENERATOR and the encode/surjectivity argument in FieldMain). + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.SubNegSpec +open Aeneas Aeneas.Std Result +open pasta_curves + +set_option maxHeartbeats 4000000 + +namespace PastaProofs + +/-- R constant, as a limb list. -/ +theorem R_limbs : + (↑fields.fp.R : List U64) = + [3780891978758094845#u64, 11037255111966004397#u64, + 18446744073709551615#u64, 4611686018427387903#u64] := by + unfold fields.fp.R + rfl + +/-- feVal R = 2²⁵⁶ mod p (the Montgomery factor, reduced). -/ +theorem feVal_R : feVal fields.fp.R = 2^256 % P := by + rw [feVal_eq _ _ _ _ _ R_limbs] + unfold limbsVal P + norm_num + +theorem R_canon : Canon fields.fp.R := by + unfold Canon + rw [feVal_R] + unfold P + norm_num + +/-- R2 constant, as a limb list. -/ +theorem R2_limbs : + (↑fields.fp.R2 : List U64) = + [10122100416058490895#u64, 15551789045973377255#u64, + 8617542898466512152#u64, 679271340751763220#u64] := by + unfold fields.fp.R2 + rfl + +/-- feVal R2 = 2⁵¹² mod p. -/ +theorem feVal_R2 : feVal fields.fp.R2 = 2^512 % P := by + rw [feVal_eq _ _ _ _ _ R2_limbs] + unfold limbsVal P + norm_num + +theorem R2_canon : Canon fields.fp.R2 := by + unfold Canon + rw [feVal_R2] + unfold P + norm_num + +/-- INV is the Montgomery multiplier: INV · p ≡ −1 (mod 2⁶⁴). -/ +theorem INV_spec : (fields.fp.INV.val * P + 1) % 2^64 = 0 := by + unfold fields.fp.INV P + norm_num + +/-- `Fp::zero` runs and denotes 0 (canonically). -/ +theorem zero_spec : + fields.fp.Fp.zero ⦃ r => Canon r ∧ feVal r = 0 ⦄ := by + unfold fields.fp.Fp.zero + simp only [Aeneas.Std.WP.spec_ok] -- ok (Array.repeat …) + constructor + · unfold Canon feVal + simp [Array.repeat, List.replicate] + unfold P + norm_num + · unfold feVal + simp [Array.repeat, List.replicate] + rfl + +/-- `Fp::one` runs, is canonical, and its value is R mod p — so ⟪one⟫ = 1. -/ +theorem one_spec : + fields.fp.Fp.one ⦃ r => Canon r ∧ feVal r = 2^256 % P ⦄ := by + unfold fields.fp.Fp.one + simp only [Aeneas.Std.WP.spec_ok] + exact ⟨R_canon, feVal_R⟩ + +/-- ⟪one⟫ = 1: the denotation cancels the Montgomery factor. -/ +theorem one_denotes_one (r : Fe) (h : feVal r = 2^256 % P) : ⟪r⟫ = 1 := by + unfold denote + rw [h] + have : ((2^256 % P : ℕ) : Fp) = (R : Fp) := by + unfold R + rw [ZMod.natCast_eq_natCast_iff'] + simp [Nat.mod_mod_self, Nat.mod_mod_of_dvd] + rw [this] + exact R_mul_Rinv + +end PastaProofs diff --git a/verification/Proofs/MulSpec.lean b/verification/Proofs/MulSpec.lean new file mode 100644 index 0000000..cd65261 --- /dev/null +++ b/verification/Proofs/MulSpec.lean @@ -0,0 +1,160 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/MulSpec.lean — multiplication of the transpiled Fp. + + RUST ANALOG (src/fields/fp.rs:367-370 / 423-447): + `mul = montgomery_reduce ∘ mul_unreduced`, where mul_unreduced is the + schoolbook 4×4 product: row i (multiplier aᵢ) runs a 4-step mac chain over + b's limbs, accumulating into the running 8-limb result. + + PROOF ARCHITECTURE + 1. `mul_unreduced_spec` — the EXACT 512-bit identity + Σ uₖ·2^(64k) = feVal a · feVal b + The 16 mac equations are summed with weights 2^(64(i+j)) — the + cross-products aᵢ·bⱼ are NONLINEAR atoms, so this is `linear_combination` + over ℤ (after zify), NOT omega. Intermediate accumulators and carries + telescope away by construction. + 2. `mul_spec` — compose with montgomery_reduce_spec (t = a·b < P² < 2²⁵⁶·P) + to get Canon r ∧ (feVal r · 2²⁵⁶) % P = (feVal a · feVal b) % P, + i.e. ⟪r⟫ = ⟪a⟫·⟪b⟫ after the denotation absorbs both R factors + (packaged in FieldMain). + + MEMORY DISCIPLINE: cheap-first `dix` discharge; the linear_combination is + one closed-form certificate (no search). + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ReduceSpec +import Mathlib.Tactic.LinearCombination +open Aeneas Aeneas.Std Result +open pasta_curves + +set_option maxHeartbeats 8000000 +set_option linter.unusedTactic false +set_option linter.unreachableTactic false + +namespace PastaProofs + +open Aeneas.Std.WP + +macro "dix" : tactic => + `(tactic| (first | scalar_tac | (subst_vars; simp [Array.set_val_eq, *]; scalar_tac))) + +/-- 8-limb value (the unreduced product). -/ +def limbsVal8 (u0 u1 u2 u3 u4 u5 u6 u7 : U64) : ℕ := + u0.val + 2^64 * u1.val + 2^128 * u2.val + 2^192 * u3.val + + 2^256 * u4.val + 2^320 * u5.val + 2^384 * u6.val + 2^448 * u7.val + +/-- `mul_unreduced` computes the exact 512-bit product. -/ +theorem mul_unreduced_spec (a b : Fe) (a0 a1 a2 a3 b0 b1 b2 b3 : U64) + (hla : (↑a : List U64) = [a0, a1, a2, a3]) + (hlb : (↑b : List U64) = [b0, b1, b2, b3]) : + fields.fp.Fp.mul_unreduced a b + ⦃ u => ∃ u0 u1 u2 u3 u4 u5 u6 u7 : U64, + (↑u : List U64) = [u0, u1, u2, u3, u4, u5, u6, u7] ∧ + limbsVal8 u0 u1 u2 u3 u4 u5 u6 u7 = + limbsVal a0 a1 a2 a3 * limbsVal b0 b1 b2 b3 ⦄ := by + unfold fields.fp.Fp.mul_unreduced + let* ⟨ i, hi ⟩ ← Array.index_usize_spec by dix + let* ⟨ i1, hi1 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r0, carry, hm00 ⟩ ← mac_spec by dix + let* ⟨ i2, hi2 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r1, carry1, hm01 ⟩ ← mac_spec by dix + let* ⟨ i3, hi3 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r2, carry2, hm02 ⟩ ← mac_spec by dix + let* ⟨ i4, hi4 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r3, r4, hm03 ⟩ ← mac_spec by dix + let* ⟨ i5, hi5 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r11, carry3, hm10 ⟩ ← mac_spec by dix + let* ⟨ r21, carry4, hm11 ⟩ ← mac_spec by dix + let* ⟨ r31, carry5, hm12 ⟩ ← mac_spec by dix + let* ⟨ r41, r5, hm13 ⟩ ← mac_spec by dix + let* ⟨ i6, hi6 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r22, carry6, hm20 ⟩ ← mac_spec by dix + let* ⟨ r32, carry7, hm21 ⟩ ← mac_spec by dix + let* ⟨ r42, carry8, hm22 ⟩ ← mac_spec by dix + let* ⟨ r51, r6, hm23 ⟩ ← mac_spec by dix + let* ⟨ i7, hi7 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r33, carry9, hm30 ⟩ ← mac_spec by dix + let* ⟨ r43, carry10, hm31 ⟩ ← mac_spec by dix + let* ⟨ r52, carry11, hm32 ⟩ ← mac_spec by dix + let* ⟨ r61, r7, hm33 ⟩ ← mac_spec by dix + -- identify the limb reads + have hv_i : i.val = a0.val := by simp [hi, hla] + have hv_i1 : i1.val = b0.val := by simp [hi1, hlb] + have hv_i2 : i2.val = b1.val := by simp [hi2, hlb] + have hv_i3 : i3.val = b2.val := by simp [hi3, hlb] + have hv_i4 : i4.val = b3.val := by simp [hi4, hlb] + have hv_i5 : i5.val = a1.val := by simp [hi5, hla] + have hv_i6 : i6.val = a2.val := by simp [hi6, hla] + have hv_i7 : i7.val = a3.val := by simp [hi7, hla] + rw [hv_i, hv_i1, hv_i2, hv_i3, hv_i4] at * + rw [hv_i5] at hm10 hm11 hm12 hm13 + rw [hv_i6] at hm20 hm21 hm22 hm23 + rw [hv_i7] at hm30 hm31 hm32 hm33 + refine ⟨r0, r11, r22, r33, r43, r52, r61, r7, rfl, ?_⟩ + -- the exact 512-bit identity: weighted sum of the 16 mac equations. + unfold limbsVal8 limbsVal + zify at hm00 hm01 hm02 hm03 hm10 hm11 hm12 hm13 + hm20 hm21 hm22 hm23 hm30 hm31 hm32 hm33 ⊢ + linear_combination + hm00 + 2^64 * hm01 + 2^128 * hm02 + 2^192 * hm03 + + 2^64 * hm10 + 2^128 * hm11 + 2^192 * hm12 + 2^256 * hm13 + + 2^128 * hm20 + 2^192 * hm21 + 2^256 * hm22 + 2^320 * hm23 + + 2^192 * hm30 + 2^256 * hm31 + 2^320 * hm32 + 2^384 * hm33 + +/-- `Fp::mul`: total, canonical, r·R ≡ a·b (mod p). -/ +theorem mul_spec (a b : Fe) (ha : Canon a) (hb : Canon b) : + fields.fp.Fp.mul a b + ⦃ r => Canon r ∧ + (feVal r * 2^256) % P = (feVal a * feVal b) % P ⦄ := by + obtain ⟨a0, a1, a2, a3, hla⟩ := Fe.exists_limbs a + obtain ⟨b0, b1, b2, b3, hlb⟩ := Fe.exists_limbs b + unfold fields.fp.Fp.mul + let* ⟨ u, hu ⟩ ← mul_unreduced_spec by + (first | exact hla | exact hlb) + obtain ⟨u0, u1, u2, u3, u4, u5, u6, u7, hlu, huval⟩ := hu + let* ⟨ j0, hj0 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j1, hj1 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j2, hj2 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j3, hj3 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j4, hj4 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j5, hj5 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j6, hj6 ⟩ ← Array.index_usize_spec by dix + let* ⟨ j7, hj7 ⟩ ← Array.index_usize_spec by dix + have he0 : j0 = u0 := by simp [hj0, hlu] + have he1 : j1 = u1 := by simp [hj1, hlu] + have he2 : j2 = u2 := by simp [hj2, hlu] + have he3 : j3 = u3 := by simp [hj3, hlu] + have he4 : j4 = u4 := by simp [hj4, hlu] + have he5 : j5 = u5 := by simp [hj5, hlu] + have he6 : j6 = u6 := by simp [hj6, hlu] + have he7 : j7 = u7 := by simp [hj7, hlu] + subst he0 he1 he2 he3 he4 he5 he6 he7 + -- t = a·b < P·P ≤ 2²⁵⁶·P: montgomery_reduce's precondition + unfold Canon at ha hb + rw [feVal_eq a a0 a1 a2 a3 hla] at ha + rw [feVal_eq b b0 b1 b2 b3 hlb] at hb + have hbound : limbsVal u0 u1 u2 u3 + 2^256 * limbsVal u4 u5 u6 u7 < + 2^256 * P := by + have h1 : limbsVal a0 a1 a2 a3 * limbsVal b0 b1 b2 b3 < P * P := + Nat.mul_lt_mul'' ha hb + have h2 : P * P ≤ 2^256 * P := by + apply Nat.mul_le_mul_right + unfold P + norm_num + have h3 : limbsVal u0 u1 u2 u3 + 2^256 * limbsVal u4 u5 u6 u7 = + limbsVal8 u0 u1 u2 u3 u4 u5 u6 u7 := by + unfold limbsVal limbsVal8 + ring + rw [h3, huval] + omega + let* ⟨ r, hr_canon, hr_val ⟩ ← montgomery_reduce_spec by + exact hbound + refine ⟨hr_canon, ?_⟩ + rw [feVal_eq a a0 a1 a2 a3 hla, feVal_eq b b0 b1 b2 b3 hlb] + have h3 : limbsVal u0 u1 u2 u3 + 2^256 * limbsVal u4 u5 u6 u7 = + limbsVal8 u0 u1 u2 u3 u4 u5 u6 u7 := by + unfold limbsVal limbsVal8 + ring + rw [h3, huval] at hr_val + exact hr_val + +end PastaProofs diff --git a/verification/Proofs/ReduceSpec.lean b/verification/Proofs/ReduceSpec.lean new file mode 100644 index 0000000..6a8c688 --- /dev/null +++ b/verification/Proofs/ReduceSpec.lean @@ -0,0 +1,194 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ReduceSpec.lean — Montgomery reduction of the transpiled Fp. + + RUST ANALOG (src/fields/fp.rs:319-363, HAC Algorithm 14.32): + 4 rounds; round i computes k = rᵢ·INV mod 2⁶⁴ and adds k·p aligned at limb + i (mac chain + carry into an adc), which makes limb i vanish — the mac's + low output is DISCARDED because it is provably 0: + rᵢ + k·p ≡ rᵢ·(1 + INV·p) ≡ 0 (mod 2⁶⁴) [INV = −p⁻¹ mod 2⁶⁴] + After 4 rounds the value is (t + m·p)/2²⁵⁶ for m = Σ kᵢ·2^(64i) < 2²⁵⁶, + hence < 2P whenever t < 2²⁵⁶·P; the final `sub · MODULUS` (the general + conditional reduction proven in SubNegSpec) lands it in [0, P). + + SPEC (multiplicative phrasing, no inverses over ℕ): + t := limbsVal r0..r3 + 2²⁵⁶·limbsVal r4..r7 < 2²⁵⁶·P → + montgomery_reduce … = ok r with Canon r ∧ (feVal r·2²⁵⁶) % P = t % P + — i.e. ⟪r⟫ = t·R⁻² in 𝔽_p wording is left to the callers (mul divides by + one R via the denotation, the other via this congruence). + + MEMORY DISCIPLINE (post 2026-07-02 OOM): step side conditions are + discharged by `scalar_tac` first (cheap), falling back to the simp-based + discharge only if needed; per-round facts are established as small `have`s + so no single tactic call sees an unbounded rewrite space. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ConstSpecs +open Aeneas Aeneas.Std Result +open pasta_curves + +set_option maxHeartbeats 8000000 +set_option linter.unusedTactic false +set_option linter.unreachableTactic false + +namespace PastaProofs + +open Aeneas.Std.WP + +macro "dix" : tactic => + `(tactic| (first | scalar_tac | (subst_vars; simp [Array.set_val_eq, *]; scalar_tac))) + +/-- The four MODULUS limbs as named literals (readability of the rounds). -/ +private def p0 : ℕ := 11037532056220336129 +private def p1 : ℕ := 2469829653914515739 +private def p2 : ℕ := 0 +private def p3 : ℕ := 4611686018427387904 +private def invLit : ℕ := 11037532056220336127 + +private theorem INV_val : fields.fp.INV.val = invLit := by + unfold fields.fp.INV invLit + rfl + +/-- `montgomery_reduce`: total, canonical, and r·R ≡ t (mod p) — see header. -/ +theorem montgomery_reduce_spec (r0 r1 r2 r3 r4 r5 r6 r7 : U64) + (hbound : limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7 < 2^256 * P) : + fields.fp.Fp.montgomery_reduce r0 r1 r2 r3 r4 r5 r6 r7 + ⦃ r => Canon r ∧ + (feVal r * 2^256) % P = + (limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7) % P ⦄ := by + unfold fields.fp.Fp.montgomery_reduce + -- ── round 1 (clears limb 0) ─────────────────────────────────────────────── + let* ⟨ k, hk ⟩ ← lift_spec by dix + let* ⟨ i, hi ⟩ ← Array.index_usize_spec by dix + let* ⟨ lo0, c00, hm00 ⟩ ← mac_spec by dix + let* ⟨ i1, hi1 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r11, c01, hm01 ⟩ ← mac_spec by dix + let* ⟨ i2, hi2 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r21, c02, hm02 ⟩ ← mac_spec by dix + let* ⟨ i3, hi3 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r31, c03, hm03 ⟩ ← mac_spec by dix + let* ⟨ r41, c0e, ha0 ⟩ ← adc_spec by dix + -- ── round 2 (clears limb 1) ─────────────────────────────────────────────── + let* ⟨ k1, hk1 ⟩ ← lift_spec by dix + let* ⟨ i4, hi4 ⟩ ← Array.index_usize_spec by dix + let* ⟨ lo1, c10, hm10 ⟩ ← mac_spec by dix + let* ⟨ i5, hi5 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r22, c11, hm11 ⟩ ← mac_spec by dix + let* ⟨ i6, hi6 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r32, c12, hm12 ⟩ ← mac_spec by dix + let* ⟨ i7, hi7 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r42, c13, hm13 ⟩ ← mac_spec by dix + let* ⟨ r51, c1e, ha1 ⟩ ← adc_spec by dix + -- ── round 3 (clears limb 2) ─────────────────────────────────────────────── + let* ⟨ k2, hk2 ⟩ ← lift_spec by dix + let* ⟨ i8, hi8 ⟩ ← Array.index_usize_spec by dix + let* ⟨ lo2, c20, hm20 ⟩ ← mac_spec by dix + let* ⟨ i9, hi9 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r33, c21, hm21 ⟩ ← mac_spec by dix + let* ⟨ i10, hi10 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r43, c22, hm22 ⟩ ← mac_spec by dix + let* ⟨ i11, hi11 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r52, c23, hm23 ⟩ ← mac_spec by dix + let* ⟨ r61, c2e, ha2 ⟩ ← adc_spec by dix + -- ── round 4 (clears limb 3) ─────────────────────────────────────────────── + let* ⟨ k3, hk3 ⟩ ← lift_spec by dix + let* ⟨ i12, hi12 ⟩ ← Array.index_usize_spec by dix + let* ⟨ lo3, c30, hm30 ⟩ ← mac_spec by dix + let* ⟨ i13, hi13 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r44, c31, hm31 ⟩ ← mac_spec by dix + let* ⟨ i14, hi14 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r53, c32, hm32 ⟩ ← mac_spec by dix + let* ⟨ i15, hi15 ⟩ ← Array.index_usize_spec by dix + let* ⟨ r62, c33, hm33 ⟩ ← mac_spec by dix + let* ⟨ r71, c3e, ha3 ⟩ ← adc_spec by dix + -- ── identifications: MODULUS reads and k values ─────────────────────────── + have hp_i : i.val = p0 := by simp [hi, MODULUS_limbs, p0] + have hp_i1 : i1.val = p1 := by simp [hi1, MODULUS_limbs, p1] + have hp_i2 : i2.val = p2 := by simp [hi2, MODULUS_limbs, p2] + have hp_i3 : i3.val = p3 := by simp [hi3, MODULUS_limbs, p3] + have hp_i4 : i4.val = p0 := by simp [hi4, MODULUS_limbs, p0] + have hp_i5 : i5.val = p1 := by simp [hi5, MODULUS_limbs, p1] + have hp_i6 : i6.val = p2 := by simp [hi6, MODULUS_limbs, p2] + have hp_i7 : i7.val = p3 := by simp [hi7, MODULUS_limbs, p3] + have hp_i8 : i8.val = p0 := by simp [hi8, MODULUS_limbs, p0] + have hp_i9 : i9.val = p1 := by simp [hi9, MODULUS_limbs, p1] + have hp_i10 : i10.val = p2 := by simp [hi10, MODULUS_limbs, p2] + have hp_i11 : i11.val = p3 := by simp [hi11, MODULUS_limbs, p3] + have hp_i12 : i12.val = p0 := by simp [hi12, MODULUS_limbs, p0] + have hp_i13 : i13.val = p1 := by simp [hi13, MODULUS_limbs, p1] + have hp_i14 : i14.val = p2 := by simp [hi14, MODULUS_limbs, p2] + have hp_i15 : i15.val = p3 := by simp [hi15, MODULUS_limbs, p3] + have hkv : k.val = (r0.val * invLit) % 2^64 := by + subst hk; simp [INV_val, U64.size, U64.numBits_def] + have hkv1 : k1.val = (r11.val * invLit) % 2^64 := by + subst hk1; simp [INV_val, U64.size, U64.numBits_def] + have hkv2 : k2.val = (r22.val * invLit) % 2^64 := by + subst hk2; simp [INV_val, U64.size, U64.numBits_def] + have hkv3 : k3.val = (r33.val * invLit) % 2^64 := by + subst hk3; simp [INV_val, U64.size, U64.numBits_def] + -- ── the dropped low limbs are 0 (the whole point of k = r·INV) ──────────── + have hb_lo0 : lo0.val < 2^64 := by scalar_tac + have hb_lo1 : lo1.val < 2^64 := by scalar_tac + have hb_lo2 : lo2.val < 2^64 := by scalar_tac + have hb_lo3 : lo3.val < 2^64 := by scalar_tac + have hlo0 : lo0.val = 0 := by + rw [hp_i] at hm00; unfold p0 invLit at *; omega + have hlo1 : lo1.val = 0 := by + rw [hp_i4] at hm10; unfold p0 invLit at *; omega + have hlo2 : lo2.val = 0 := by + rw [hp_i8] at hm20; unfold p0 invLit at *; omega + have hlo3 : lo3.val = 0 := by + rw [hp_i12] at hm30; unfold p0 invLit at *; omega + -- ── the pre-reduction value t' = (t + m·p)/2²⁵⁶ < 2P ───────────────────── + have hb_r44 : r44.val < 2^64 := by scalar_tac + have hb_r53 : r53.val < 2^64 := by scalar_tac + have hb_r62 : r62.val < 2^64 := by scalar_tac + have hb_r71 : r71.val < 2^64 := by scalar_tac + have hb_k : k.val < 2^64 := by scalar_tac + have hb_k1 : k1.val < 2^64 := by scalar_tac + have hb_k2 : k2.val < 2^64 := by scalar_tac + have hb_k3 : k3.val < 2^64 := by scalar_tac + -- exact division identity: t'·2²⁵⁶ = t + m·p (all mac/adc rows summed) + have hkey : limbsVal r44 r53 r62 r71 * 2^256 = + (limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7) + + (k.val + 2^64 * k1.val + 2^128 * k2.val + 2^192 * k3.val) * P := by + rw [hp_i1, hp_i2, hp_i3] at hm01 hm02 hm03 + rw [hp_i5, hp_i6, hp_i7] at hm11 hm12 hm13 + rw [hp_i9, hp_i10, hp_i11] at hm21 hm22 hm23 + rw [hp_i13, hp_i14, hp_i15] at hm31 hm32 hm33 + rw [hp_i] at hm00; rw [hp_i4] at hm10; rw [hp_i8] at hm20; rw [hp_i12] at hm30 + unfold limbsVal P p0 p1 p2 p3 at * + omega + have ht' : limbsVal r44 r53 r62 r71 < 2 * P := by + unfold limbsVal P at * + omega + -- ── final conditional reduction ─────────────────────────────────────────── + have hMle : feVal fields.fp.MODULUS ≤ P := le_of_eq feVal_MODULUS + have hdlt : feVal (Array.make 4#usize [r44, r53, r62, r71] (by simp)) < + feVal fields.fp.MODULUS + P := by + rw [feVal_MODULUS, feVal_make] + omega + let* ⟨ r, hr_canon, hr_val ⟩ ← sub_spec by + (first | exact hMle | exact hdlt) + refine ⟨hr_canon, ?_⟩ + rw [feVal_MODULUS, feVal_make] at hr_val + -- feVal r ∈ {t', t' − P}; both give feVal r·2²⁵⁶ ≡ t (mod P) via hkey + unfold Canon at hr_canon + rcases hr_val with hv | hv + · -- feVal r + P = t' … wait: hv : feVal r + P = t' ∨ feVal r = t' — see below + -- (sub_spec: r + b = a): here b = P, a = t' → feVal r + P = t' + have : (feVal r + P) * 2^256 = + (limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7) + + (k.val + 2^64 * k1.val + 2^128 * k2.val + 2^192 * k3.val) * P := by + rw [hv]; exact hkey + unfold limbsVal P at * + omega + · -- feVal r + P = t' + P → feVal r = t' + have : (feVal r + P) * 2^256 = + ((limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7) + + (k.val + 2^64 * k1.val + 2^128 * k2.val + 2^192 * k3.val) * P) + P * 2^256 := by + rw [hv] + rw [← hkey] + ring + unfold limbsVal P at * + omega + +end PastaProofs diff --git a/verification/lean-guard b/verification/lean-guard new file mode 100755 index 0000000..256ef42 --- /dev/null +++ b/verification/lean-guard @@ -0,0 +1,130 @@ +#!/usr/bin/env bash +# ──────────────────────────────────────────────────────────────────────────── +# lean-guard — HARD-CAPPED Lean compiler wrapper. +# +# Successor to lean-safe after the 2026-07-02 OOM incident: a single `lean` +# elaboration (tactic-search blowup: simp[*]/scalar_tac over a ~60-hypothesis +# context with 2^256-scale literals) grew to 12.2GB RSS and was killed by the +# GLOBAL kernel OOM killer, taking the driving session down with it. +# lean-safe's guards (timeout + affinity + PREFLIGHT headroom) cannot stop +# that: the process passes preflight, then balloons inside its timeout. +# +# NEW GUARDS (in addition to all lean-safe guards): +# A. lean -M — Lean's internal cap: elaboration aborts +# with a clean "maximum memory exceeded" +# error. First line of defense; graceful. +# B. systemd-run --user --scope +# -p MemoryMax / MemorySwapMax — kernel cgroup cap around the process: +# if Lean's own accounting misses (C-level +# allocations), the cgroup kills ONLY this +# lean, never the session, never the box. +# C. flock on /tmp/lean-guard.lock — machine-wide single-flight: at most ONE +# lean compile at a time, regardless of +# how many agents/scripts are active. +# +# Env knobs (defaults for this 14GB / 8-core ThinkPad): +# LEAN_TIMEOUT per-file wall clock seconds (default 400) +# LEAN_MEM_MB lean -M internal cap, MB (default 4096) +# LEAN_CGROUP_MB cgroup MemoryMax, MB (default LEAN_MEM_MB+1024) +# LEAN_MAX_CORES taskset core range (default 0-3) +# LEAN_MIN_FREE_MB preflight available-RAM floor (default 3072) +# LEAN_LOCK_WAIT max seconds to wait for the lock (default 7200) +# +# Usage: lean-guard [extra lean args...] +# The .olean output path is always computed as ${file%.lean}.olean. +# Requires: lean on PATH (caller sources the toolchain env; typically run +# inside `lake env` so LEAN_PATH is set — this wrapper does NOT clobber env). +# ──────────────────────────────────────────────────────────────────────────── +set -uo pipefail + +# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort; +# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport +# popups and fill /var/crash. ulimit applies to this shell and every child. +ulimit -c 0 2>/dev/null || true + +TIMEOUT_SEC=${LEAN_TIMEOUT:-400} +MEM_MB=${LEAN_MEM_MB:-4096} +CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))} +CORES=${LEAN_MAX_CORES:-0-3} +MIN_FREE_MB=${LEAN_MIN_FREE_MB:-3072} +LOCK_WAIT=${LEAN_LOCK_WAIT:-7200} +LOCK_FILE=/tmp/lean-guard.lock +LOG_FILE="${HOME}/.lean-guard.log" + +if ! command -v lean &>/dev/null; then + echo "FATAL: lean not on PATH — source ~/aeneas-toolchain/env.sh (and run inside lake env)" + exit 1 +fi +if [ $# -eq 0 ]; then + echo "Usage: lean-guard [lean args...]" + exit 1 +fi + +LEAN_FILE="$1"; shift || true + +# ── Guard 1: source integrity (anti olean-clobber) ────────────────────────── +if [ ! -f "$LEAN_FILE" ]; then + echo "MISSING: $LEAN_FILE"; exit 1 +fi +if ! grep -qE '^[[:space:]]*(/-|import |namespace |theorem |def |open |set_option |--)' "$LEAN_FILE" 2>/dev/null; then + echo "FATAL: $LEAN_FILE is not Lean source (binary/olean data?)." + echo " Restore: git checkout HEAD -- $LEAN_FILE" + exit 1 +fi + +# ── Guard 2: output path ───────────────────────────────────────────────────── +case "$LEAN_FILE" in + *.lean) ;; + *) echo "FATAL: input lacks .lean extension"; exit 1 ;; +esac +OLEAN_FILE="${LEAN_FILE%.lean}.olean" +[ "$OLEAN_FILE" = "$LEAN_FILE" ] && { echo "FATAL: output would clobber source"; exit 1; } + +# ── Guard C: machine-wide single-flight ───────────────────────────────────── +exec 9>"$LOCK_FILE" +if ! flock -w "$LOCK_WAIT" 9; then + echo "FATAL: could not acquire lean-guard lock within ${LOCK_WAIT}s (another compile stuck?)" + exit 1 +fi + +# ── Guard 3: preflight headroom (after lock: serialized measurement) ──────── +AVAIL_MB=$(free -m | awk '/Mem:/{print $7}') +if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then + echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile" + exit 1 +fi + +echo "[$(date -u +%F' '%T)] $LEAN_FILE (t=${TIMEOUT_SEC}s M=${MEM_MB}MB cg=${CGROUP_MB}MB cores=$CORES avail=${AVAIL_MB}MB)" >> "$LOG_FILE" + +# ── Compile under both caps ────────────────────────────────────────────────── +run_leancmd() { + taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" +} +if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then + # --scope runs the command as a child of THIS shell (env inherited), + # merely placing it in a fresh cgroup with the hard caps below. + systemd-run --user --scope --quiet \ + -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \ + -- taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" + EXIT_CODE=$? +else + echo " (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE" + run_leancmd "$@" + EXIT_CODE=$? +fi + +case $EXIT_CODE in + 0) echo " OK" >> "$LOG_FILE" ;; + 124) echo " TIMEOUT ${TIMEOUT_SEC}s" >> "$LOG_FILE" + echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" ;; + 137) echo " KILLED (cgroup MemoryMax ${CGROUP_MB}MB hit)" >> "$LOG_FILE" + echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" ;; + *) echo " FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE" ;; +esac +# stale partial olean from a failed compile must not poison later imports +[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE" +exit $EXIT_CODE