From 3719156140bf8c974491277353728677e8de7419 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 2 Jul 2026 20:16:07 +0200 Subject: [PATCH] pasta field FOUNDATION proven + honest status; check.sh green MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proven & compiling (check.sh): PPallas primality cert, Denote (Montgomery denotation + Canon), HelperSpecs (adc/sbb/mac exact specs), SubNegSpec (sub/neg), ConstSpecs (R/R2/INV/zero/one) — all against the real extraction, no bridge axioms. Diagnosed and documented: add/mul/montgomery_reduce/square/invert/FieldMain overflow the Lean kernel's proof-checking memory because omega certificates with 2^256/2^512-scale coefficients (intrinsic to 4x64 Montgomery arithmetic) exceed the kernel budget. Drafts + the standalone-proven montgomery accounting lemma retained under Proofs/drafts/. Fix (linear_combination + context-free big-coefficient lemmas) is mechanical, not yet complete. Documented honestly, not shipped behind an axiom. Co-Authored-By: Claude Fable 5 --- README.md | 27 +- verification/Proofs/ConstSpecs.lean | 29 +- verification/Proofs/ReduceSpec.lean | 194 ---------- verification/Proofs/SubNegSpec.lean | 1 - verification/Proofs/{ => drafts}/AddSpec.lean | 31 +- verification/Proofs/{ => drafts}/MulSpec.lean | 0 verification/Proofs/drafts/ReduceSpec.lean | 349 ++++++++++++++++++ verification/check.sh | 37 ++ 8 files changed, 454 insertions(+), 214 deletions(-) delete mode 100644 verification/Proofs/ReduceSpec.lean rename verification/Proofs/{ => drafts}/AddSpec.lean (76%) rename verification/Proofs/{ => drafts}/MulSpec.lean (100%) create mode 100644 verification/Proofs/drafts/ReduceSpec.lean create mode 100755 verification/check.sh diff --git a/README.md b/README.md index e2d43ca..f73a0d6 100644 --- a/README.md +++ b/README.md @@ -23,12 +23,27 @@ statements; this repository exists to do it properly.) ## Layer status -> **Construction note (2026-07-02):** the field layer is mid-build. PROVEN and -> compiled: PPallas (primality), Denote (Montgomery denotation), HelperSpecs -> (adc/sbb/mac), SubNegSpec (sub/neg). DRAFTED, awaiting compilation: -> AddSpec, ConstSpecs, ReduceSpec (Montgomery reduction), MulSpec. Not yet -> written: SquareSpec, InvertSpec, FieldMain (the certificate), check.sh. -> This note is removed when `verification/check.sh` goes green end-to-end. +> **Construction status (2026-07-02).** The field FOUNDATION is proven and +> compiles (`verification/check.sh` is green): **PPallas** (Lucas/Pratt +> primality certificate for the 255-bit Pallas modulus), **Denote** (the +> Montgomery denotation ⟪a⟫ = feVal a·R⁻¹ and the `Canon` invariant), +> **HelperSpecs** (exact ℕ specs for the `adc`/`sbb`/`mac` u64 primitives, +> proven against the transpiled code), **SubNegSpec** (`sub`/`neg`), and +> **ConstSpecs** (R, R², INV, zero, one). Every one is stated about the REAL +> Aeneas-extracted code with **no bridge axioms**. +> +> **In progress:** `add`, `mul`, `montgomery_reduce`, `square`, `invert`, and +> the aggregate `fieldImplementation` certificate. These are drafted in +> `verification/Proofs/drafts/` and the Montgomery accounting is proven +> standalone, but the full theorems currently overflow the Lean **kernel's +> proof-checking memory**: omega certificates with 2²⁵⁶/2⁵¹²-scale +> coefficients (unavoidable in 4×64 Montgomery arithmetic) are too large for +> the kernel, whereas the ed25519 5×51 field (2⁵¹-scale, ×19 folding) stays +> small. The fix — reformulating every arithmetic step via `linear_combination` +> and isolating each big-coefficient step into a context-free lemma (the +> `montgomery_rows_conclusion` accounting lemma already does this and compiles) +> — is mechanical but not yet complete. Tracked honestly here rather than +> shipped behind an axiom. | Layer | Certificate | Status | Axioms of certificate | |-------|-------------|--------|-----------------------| diff --git a/verification/Proofs/ConstSpecs.lean b/verification/Proofs/ConstSpecs.lean index e1f8387..389ca9d 100644 --- a/verification/Proofs/ConstSpecs.lean +++ b/verification/Proofs/ConstSpecs.lean @@ -55,13 +55,26 @@ theorem R2_limbs : theorem feVal_R2 : feVal fields.fp.R2 = 2^512 % P := by rw [feVal_eq _ _ _ _ _ R2_limbs] unfold limbsVal P - norm_num + -- explicit division witness: 2⁵¹² = P·Q + R with R < P (norm_num checks the + -- one big multiplication; omega concludes the mod identity) + have hq : 28948022309329048855892746252171976963363056481941560715954676764349967630337 * + 463168356949264781694283940034751631412350973614059540860385843833705555034097 + + 4263855311831330276397237192126260515652039413828781833859739249380679483407 = + 13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096 := by + norm_num + have hpow : (2:ℕ)^512 = + 13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096 := by + have hsplit : (2:ℕ)^512 = ((2:ℕ)^64)^8 := by + rw [← pow_mul] + rw [hsplit] + norm_num + rw [hpow] + norm_num [hq] theorem R2_canon : Canon fields.fp.R2 := by unfold Canon rw [feVal_R2] - unfold P - norm_num + exact Nat.mod_lt _ (by 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 @@ -76,11 +89,12 @@ theorem zero_spec : constructor · unfold Canon feVal simp [Array.repeat, List.replicate] - unfold P - norm_num + unfold limbsVal P + simp · unfold feVal simp [Array.repeat, List.replicate] - rfl + unfold limbsVal + simp /-- `Fp::one` runs, is canonical, and its value is R mod p — so ⟪one⟫ = 1. -/ theorem one_spec : @@ -96,7 +110,8 @@ theorem one_denotes_one (r : Fe) (h : feVal r = 2^256 % P) : ⟪r⟫ = 1 := by 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] + unfold P + omega rw [this] exact R_mul_Rinv diff --git a/verification/Proofs/ReduceSpec.lean b/verification/Proofs/ReduceSpec.lean deleted file mode 100644 index 6a8c688..0000000 --- a/verification/Proofs/ReduceSpec.lean +++ /dev/null @@ -1,194 +0,0 @@ -/- ────────────────────────────────────────────────────────────────────────────── - 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/Proofs/SubNegSpec.lean b/verification/Proofs/SubNegSpec.lean index 4ab8407..79db6c0 100644 --- a/verification/Proofs/SubNegSpec.lean +++ b/verification/Proofs/SubNegSpec.lean @@ -133,7 +133,6 @@ theorem sub_spec (a b : Fe) (hbP : feVal b ≤ P) (hab : feVal a < feVal b + P) unfold Canon simp only [feVal_make] unfold limbsVal P at * - trace_state omega · -- the two-case value identity simp only [feVal_make] diff --git a/verification/Proofs/AddSpec.lean b/verification/Proofs/drafts/AddSpec.lean similarity index 76% rename from verification/Proofs/AddSpec.lean rename to verification/Proofs/drafts/AddSpec.lean index bcd70e4..24c4131 100644 --- a/verification/Proofs/AddSpec.lean +++ b/verification/Proofs/drafts/AddSpec.lean @@ -11,6 +11,7 @@ add a b = ok r with Canon r ∧ (r = a + b ∨ r + P = a + b). ────────────────────────────────────────────────────────────────────────────── -/ import Proofs.SubNegSpec +import Mathlib.Tactic.LinearCombination open Aeneas Aeneas.Std Result open pasta_curves @@ -25,6 +26,18 @@ open Aeneas.Std.WP macro "dis" : tactic => `(tactic| (subst_vars; try simp [Array.set_val_eq, *]; try scalar_tac)) + +/-- Context-free (isolated big-coefficient omega, like ReduceSpec's accounting): + a full-width add produces no final carry when both inputs are < P, and the + low limbs then hold the exact sum. Kept standalone so the 2²⁵⁶-scale omega + certificate never lands inside the WP-threaded proof term of `add_spec` + (that is what overflows the Lean kernel — see POSTMORTEM-2026-07-02). -/ +private theorem add_carry_zero (Ld La Lb c3 : ℕ) + (h : Ld + 2^256 * c3 = La + Lb) (hA : La < P) (hB : Lb < P) : + c3 = 0 ∧ Ld = La + Lb := by + unfold P at hA hB + omega + /-- `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 @@ -65,14 +78,19 @@ theorem add_spec (a b : Fe) (ha : Canon a) (hb : Canon b) : -- 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 + unfold limbsVal + -- weighted sum of the 4 adc rows; carries telescope (compact `ring`, not + -- a big-coefficient omega certificate) + have e0 := hadc0; have e1 := hadc1; have e2 := hadc2; have e3 := hadc3 + zify at e0 e1 e2 e3 ⊢ + linear_combination e0 + 2^64 * e1 + 2^128 * e2 + 2^192 * e3 -- the conditional reduction: sub (Σd) MODULUS with Σd < 2P have hMle : feVal fields.fp.MODULUS ≤ P := le_of_eq feVal_MODULUS + obtain ⟨hc3, hexact⟩ := add_carry_zero _ _ _ _ hsum ha hb 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 * + rw [feVal_MODULUS, feVal_make, hexact] + -- limbsVal a + limbsVal b < 2P, atoms; small omega omega -- MEMORY DISCIPLINE (post 2026-07-02 OOM): sub_spec's two arithmetic -- preconditions are discharged by EXACT matches against the facts proven @@ -83,8 +101,9 @@ theorem add_spec (a b : Fe) (ha : Canon a) (hb : Canon b) : -- 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 * + rw [feVal_MODULUS, feVal_make, hexact] at hr_val + unfold Canon at hr_canon + -- feVal r vs (limbsVal a + limbsVal b); all atoms, small coefficients omega end PastaProofs diff --git a/verification/Proofs/MulSpec.lean b/verification/Proofs/drafts/MulSpec.lean similarity index 100% rename from verification/Proofs/MulSpec.lean rename to verification/Proofs/drafts/MulSpec.lean diff --git a/verification/Proofs/drafts/ReduceSpec.lean b/verification/Proofs/drafts/ReduceSpec.lean new file mode 100644 index 0000000..ee054a4 --- /dev/null +++ b/verification/Proofs/drafts/ReduceSpec.lean @@ -0,0 +1,349 @@ +/- ────────────────────────────────────────────────────────────────────────────── + 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 +import Mathlib.Tactic.LinearCombination +open Aeneas Aeneas.Std Result +open pasta_curves + +set_option maxHeartbeats 8000000 +set_option maxRecDepth 4096 +set_option linter.unusedTactic false +set_option linter.unreachableTactic false + +namespace PastaProofs + +open Aeneas.Std.WP + +macro "dix" : tactic => + `(tactic| 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 + +/-- One Montgomery round drops a PROVABLY ZERO low limb: + k = r·INV mod 2⁶⁴ makes r + k·p₀ ≡ r·(1 + INV·p₀) ≡ 0 (mod 2⁶⁴). + Standalone so each instantiation carries a tiny proof term. -/ +private theorem round_lo_zero (r k lo c z : ℕ) + (hk : k = (r * invLit) % 2^64) + (hm : lo + 2^64 * c = r + k * p0 + z) (hz : z = 0) + (hb : lo < 2^64) : lo = 0 := by + unfold invLit p0 at * + omega + +/-- THE ACCOUNTING LEMMA, context-free over plain ℕ (48 variables, the 20 + row equations of the 4 Montgomery rounds). Keeping it standalone keeps + the kernel term of the main theorem small (the 2026-07-02 postmortem + discipline: no giant certificates inside a 100-hypothesis context). -/ +private theorem montgomery_rows_conclusion + (r0 r1 r2 r3 r4 r5 r6 r7 k k1 k2 k3 : ℕ) + (r11 r21 r31 r41 r22 r32 r42 r51 r33 r43 r52 r61 r44 r53 r62 r71 : ℕ) + (c00 c01 c02 c03 c0e c10 c11 c12 c13 c1e : ℕ) + (c20 c21 c22 c23 c2e c30 c31 c32 c33 c3e : ℕ) + (hbound : r0 + 2^64 * r1 + 2^128 * r2 + 2^192 * r3 + + 2^256 * (r4 + 2^64 * r5 + 2^128 * r6 + 2^192 * r7) < 2^256 * P) + (hm00 : 0 + 2^64 * c00 = r0 + k * p0 + 0) + (hm01 : r11 + 2^64 * c01 = r1 + k * p1 + c00) + (hm02 : r21 + 2^64 * c02 = r2 + k * p2 + c01) + (hm03 : r31 + 2^64 * c03 = r3 + k * p3 + c02) + (ha0 : r41 + 2^64 * c0e = r4 + 0 + c03) + (hm10 : 0 + 2^64 * c10 = r11 + k1 * p0 + 0) + (hm11 : r22 + 2^64 * c11 = r21 + k1 * p1 + c10) + (hm12 : r32 + 2^64 * c12 = r31 + k1 * p2 + c11) + (hm13 : r42 + 2^64 * c13 = r41 + k1 * p3 + c12) + (ha1 : r51 + 2^64 * c1e = r5 + c0e + c13) + (hm20 : 0 + 2^64 * c20 = r22 + k2 * p0 + 0) + (hm21 : r33 + 2^64 * c21 = r32 + k2 * p1 + c20) + (hm22 : r43 + 2^64 * c22 = r42 + k2 * p2 + c21) + (hm23 : r52 + 2^64 * c23 = r51 + k2 * p3 + c22) + (ha2 : r61 + 2^64 * c2e = r6 + c1e + c23) + (hm30 : 0 + 2^64 * c30 = r33 + k3 * p0 + 0) + (hm31 : r44 + 2^64 * c31 = r43 + k3 * p1 + c30) + (hm32 : r53 + 2^64 * c32 = r52 + k3 * p2 + c31) + (hm33 : r62 + 2^64 * c33 = r61 + k3 * p3 + c32) + (ha3 : r71 + 2^64 * c3e = r7 + c2e + c33) + (hbk : k < 2^64) (hbk1 : k1 < 2^64) (hbk2 : k2 < 2^64) (hbk3 : k3 < 2^64) + (hb44 : r44 < 2^64) (hb53 : r53 < 2^64) (hb62 : r62 < 2^64) (hb71 : r71 < 2^64) : + (r44 + 2^64 * r53 + 2^128 * r62 + 2^192 * r71) < 2 * P ∧ + ((r44 + 2^64 * r53 + 2^128 * r62 + 2^192 * r71) * 2^256) % P = + (r0 + 2^64 * r1 + 2^128 * r2 + 2^192 * r3 + + 2^256 * (r4 + 2^64 * r5 + 2^128 * r6 + 2^192 * r7)) % P := by + -- exact division identity with the final carry explicit + -- (weights machine-derived offline: mac(i,j) ↦ 2^(64(i+j)), adc(i) ↦ 2^(64(i+4))) + have hkey : (r44 + 2^64 * r53 + 2^128 * r62 + 2^192 * r71) * 2^256 + + 2^512 * c3e = + (r0 + 2^64 * r1 + 2^128 * r2 + 2^192 * r3 + + 2^256 * (r4 + 2^64 * r5 + 2^128 * r6 + 2^192 * r7)) + + (k + 2^64 * k1 + 2^128 * k2 + 2^192 * k3) * P := by + unfold P p0 p1 p2 p3 at * + omega + have hc3e : c3e = 0 := by + unfold P at hkey hbound + omega + rw [hc3e, Nat.mul_zero, Nat.add_zero] at hkey + constructor + · unfold P at hkey hbound ⊢ + omega + · rw [hkey] + exact Nat.add_mul_mod_self_right _ _ _ + +/-- Case-closing steps for the final congruence, standalone (context-free + omega: the in-proof context confuses omega's preprocessing). -/ +private theorem close_lo (x t' T M F : ℕ) + (hv : x + M = t') (h2 : t' * F % M = T % M) : + x * F % M = T % M := by + have hx : x ≡ t' [MOD M] := by + unfold Nat.ModEq + rw [← hv] + exact (Nat.add_mod_right x M).symm + exact (hx.mul_right F).trans h2 + +private theorem close_hi (x t' T M F : ℕ) + (hv : x + M = t' + M) (h2 : t' * F % M = T % M) : + x * F % M = T % M := by + have hx : x = t' := by omega + rw [hx] + exact h2 + +/-- The reduce postcondition, NAMED: the WP machinery carries this through + all 41 steps of the body — as one small symbol instead of a term with + 78-digit literals (kernel-size discipline). -/ +def MRPost (r0 r1 r2 r3 r4 r5 r6 r7 : U64) (r : Fe) : Prop := + Canon r ∧ + (feVal r * 2^256) % P = + (limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7) % P + + +/-- The round-3-4 tail of `montgomery_reduce` (verbatim from the generated + body), as its own definition so the proof can be split at the round + boundary — a 41-`let*` monadic proof term overflows the Lean kernel's + memory budget, but two ~20-op halves do not (SubNegSpec's 24-op chain is + the empirical ceiling; see POSTMORTEM-2026-07-02). -/ +def mont_tail (r22 r32 r42 r51 r6 r7 c1e : U64) : Result Fe := do + let k2 ← lift (core.num.U64.wrapping_mul r22 fields.fp.INV) + let i8 ← Array.index_usize fields.fp.MODULUS 0#usize + let (_, carry8) ← arithmetic.fields.mac r22 k2 i8 0#u64 + let i9 ← Array.index_usize fields.fp.MODULUS 1#usize + let (r33, carry9) ← arithmetic.fields.mac r32 k2 i9 carry8 + let i10 ← Array.index_usize fields.fp.MODULUS 2#usize + let (r43, carry10) ← arithmetic.fields.mac r42 k2 i10 carry9 + let i11 ← Array.index_usize fields.fp.MODULUS 3#usize + let (r52, carry11) ← arithmetic.fields.mac r51 k2 i11 carry10 + let (r61, carry23) ← arithmetic.fields.adc r6 c1e carry11 + let k3 ← lift (core.num.U64.wrapping_mul r33 fields.fp.INV) + let i12 ← Array.index_usize fields.fp.MODULUS 0#usize + let (_, carry12) ← arithmetic.fields.mac r33 k3 i12 0#u64 + let i13 ← Array.index_usize fields.fp.MODULUS 1#usize + let (r44, carry13) ← arithmetic.fields.mac r43 k3 i13 carry12 + let i14 ← Array.index_usize fields.fp.MODULUS 2#usize + let (r53, carry14) ← arithmetic.fields.mac r52 k3 i14 carry13 + let i15 ← Array.index_usize fields.fp.MODULUS 3#usize + let (r62, carry15) ← arithmetic.fields.mac r61 k3 i15 carry14 + let (r71, _) ← arithmetic.fields.adc r7 carry23 carry15 + fields.fp.Fp.sub (Array.make 4#usize [ r44, r53, r62, r71 ]) fields.fp.MODULUS + +/-- Rounds 3-4 + final reduction: given the round-1-2 accounting (as the input + value `T`, the pre-round-3 limbs r22/r32/r42/r51 and their column + identities), the tail lands the Montgomery result. -/ +theorem mont_tail_spec (r0 r1 r2 r3 r4 r5 r6 r7 k k1 : U64) + (r11 r21 r31 r41 r22 r32 r42 r51 : U64) + (c00 c01 c02 c03 c0e c10 c11 c12 c13 c1e : U64) + (hbound : limbsVal r0 r1 r2 r3 + 2^256 * limbsVal r4 r5 r6 r7 < 2^256 * P) + (hm00 : (0:ℕ) + 2^64 * c00.val = r0.val + k.val * p0 + 0) + (hm01 : r11.val + 2^64 * c01.val = r1.val + k.val * p1 + c00.val) + (hm02 : r21.val + 2^64 * c02.val = r2.val + k.val * p2 + c01.val) + (hm03 : r31.val + 2^64 * c03.val = r3.val + k.val * p3 + c02.val) + (ha0 : r41.val + 2^64 * c0e.val = r4.val + 0 + c03.val) + (hm10 : (0:ℕ) + 2^64 * c10.val = r11.val + k1.val * p0 + 0) + (hm11 : r22.val + 2^64 * c11.val = r21.val + k1.val * p1 + c10.val) + (hm12 : r32.val + 2^64 * c12.val = r31.val + k1.val * p2 + c11.val) + (hm13 : r42.val + 2^64 * c13.val = r41.val + k1.val * p3 + c12.val) + (ha1 : r51.val + 2^64 * c1e.val = r5.val + c0e.val + c13.val) + (hbk : k.val < 2^64) (hbk1 : k1.val < 2^64) : + mont_tail r22 r32 r42 r51 r6 r7 c1e + ⦃ r => MRPost r0 r1 r2 r3 r4 r5 r6 r7 r ⦄ := by + unfold mont_tail + -- round 3 + 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 + 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 + -- MODULUS reads + 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 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] + have hb_lo2 : lo2.val < 2^64 := by scalar_tac + have hb_lo3 : lo3.val < 2^64 := by scalar_tac + rw [hp_i8] at hm20 + have hlo2 : lo2.val = 0 := round_lo_zero _ _ _ _ _ hkv2 hm20 rfl hb_lo2 + rw [hp_i12] at hm30 + have hlo3 : lo3.val = 0 := round_lo_zero _ _ _ _ _ hkv3 hm30 rfl hb_lo3 + rw [hlo2] at hm20 + rw [hlo3] at hm30 + 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_k2 : k2.val < 2^64 := by scalar_tac + have hb_k3 : k3.val < 2^64 := by scalar_tac + rw [hp_i9] at hm21; rw [hp_i10] at hm22; rw [hp_i11] at hm23 + rw [hp_i13] at hm31; rw [hp_i14] at hm32; rw [hp_i15] at hm33 + try clear hi8 + try clear hi9 + try clear hi10 + try clear hi11 + try clear hi12 + try clear hi13 + try clear hi14 + try clear hi15 + try clear hp_i8 + try clear hp_i9 + try clear hp_i10 + try clear hp_i11 + try clear hp_i12 + try clear hp_i13 + try clear hp_i14 + try clear hp_i15 + try clear hk2 + try clear hk3 + try clear hkv2 + try clear hkv3 + try clear hlo2 + try clear hlo3 + try clear hb_lo2 + try clear hb_lo3 + have hbound' : r0.val + 2^64 * r1.val + 2^128 * r2.val + 2^192 * r3.val + + 2^256 * (r4.val + 2^64 * r5.val + 2^128 * r6.val + 2^192 * r7.val) < + 2^256 * P := by + unfold limbsVal at hbound + exact hbound + have hfin := montgomery_rows_conclusion + r0.val r1.val r2.val r3.val r4.val r5.val r6.val r7.val + k.val k1.val k2.val k3.val + r11.val r21.val r31.val r41.val r22.val r32.val r42.val r51.val + r33.val r43.val r52.val r61.val r44.val r53.val r62.val r71.val + c00.val c01.val c02.val c03.val c0e.val c10.val c11.val c12.val c13.val c1e.val + c20.val c21.val c22.val c23.val c2e.val c30.val c31.val c32.val c33.val c3e.val + hbound' hm00 hm01 hm02 hm03 ha0 hm10 hm11 hm12 hm13 ha1 + hm20 hm21 hm22 hm23 ha2 hm30 hm31 hm32 hm33 ha3 + hbk hbk1 hb_k2 hb_k3 hb_r44 hb_r53 hb_r62 hb_r71 + clear hm00 hm01 hm02 hm03 hm10 hm11 hm12 hm13 + hm20 hm21 hm22 hm23 hm30 hm31 hm32 hm33 ha0 ha1 ha2 ha3 + 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] + unfold limbsVal + exact lt_of_lt_of_le hfin.1 (by omega) + let* ⟨ r, hr_canon, hr_val ⟩ ← sub_spec by + (first | exact hMle | exact hdlt) + unfold MRPost + refine ⟨hr_canon, ?_⟩ + rw [feVal_MODULUS, feVal_make] at hr_val + have h2 := hfin.2 + unfold limbsVal at hr_val ⊢ + rcases hr_val with hv | hv + · exact close_lo _ _ _ _ _ hv h2 + · exact close_hi _ _ _ _ _ hv h2 + +/-- `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 => MRPost r0 r1 r2 r3 r4 r5 r6 r7 r ⦄ := by + unfold fields.fp.Fp.montgomery_reduce + -- ── rounds 1-2 only (rounds 3-4 + reduction are mont_tail_spec) ─────────── + 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 + 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 + -- identify the modulus reads / k for the tail's hypotheses + 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 hbk : k.val < 2^64 := by scalar_tac + have hbk1 : k1.val < 2^64 := by scalar_tac + rw [hp_i] at hm00; rw [hp_i1] at hm01; rw [hp_i2] at hm02; rw [hp_i3] at hm03 + rw [hp_i4] at hm10; rw [hp_i5] at hm11; rw [hp_i6] at hm12; rw [hp_i7] at hm13 + -- the tail carries the full result + exact mont_tail_spec r0 r1 r2 r3 r4 r5 r6 r7 k k1 + r11 r21 r31 r41 r22 r32 r42 r51 + c00 c01 c02 c03 c0e c10 c11 c12 c13 c1e + hbound hm00 hm01 hm02 hm03 ha0 hm10 hm11 hm12 hm13 ha1 hbk hbk1 + +end PastaProofs diff --git a/verification/check.sh b/verification/check.sh new file mode 100755 index 0000000..b5a1b4f --- /dev/null +++ b/verification/check.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash +# THE button for the pasta field FOUNDATION (what is proven & compiles today). +# Layers add/mul/reduce/square/invert/FieldMain are drafted but withheld from +# this manifest pending a kernel-certificate reformulation (see README + the +# standalone-proven accounting lemma in Proofs/_Accounting.lean). Nothing in +# this manifest depends on them; every file here compiles axiom-clean. +set -uo pipefail +source ~/aeneas-toolchain/env.sh +HERE="$(cd "$(dirname "$0")" && pwd)" +AENEAS_LEAN="$AENEAS_HOME/backends/lean" +GEN=(PallasFp/TypesExternal PallasFp/Types PallasFp/FunsExternal PallasFp/Funs) +PROOFS=(PPallas Denote HelperSpecs SubNegSpec ConstSpecs) + +echo "=== Phase 1: stub/axiom-smuggling audit ===" +if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then echo STUB; exit 1; fi +if grep -rn ' : True :=' "$HERE"/Proofs/*.lean 2>/dev/null; then echo STUB; exit 1; fi +if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean 2>/dev/null; then + echo "AXIOM under Proofs/ — forbidden"; exit 1; fi +echo " clean" + +echo "=== Phase 2: compile (guarded) ===" +cd "$AENEAS_LEAN" +lake env bash -c " + set -uo pipefail + cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" + for m in ${GEN[*]}; do + echo \" · gen \$m\" + LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1 + done + cd '$HERE' + for m in ${PROOFS[*]}; do + echo \" · proof \$m\" + LEAN_TIMEOUT=400 LEAN_MEM_MB=8192 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1 + done +" || { echo FAIL; exit 1; } +echo "" +echo "PASTA FOUNDATION: ALL PROOFS PASS (primality, denotation, adc/sbb/mac, sub/neg, constants)."