mirror of
https://github.com/saymrwulf/pasta-pallas-verified.git
synced 2026-09-08 20:40:31 +00:00
pasta field FOUNDATION proven + honest status; check.sh green
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 <noreply@anthropic.com>
This commit is contained in:
parent
9da0902640
commit
3719156140
8 changed files with 454 additions and 214 deletions
27
README.md
27
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 |
|
||||
|-------|-------------|--------|-----------------------|
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
349
verification/Proofs/drafts/ReduceSpec.lean
Normal file
349
verification/Proofs/drafts/ReduceSpec.lean
Normal file
|
|
@ -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
|
||||
37
verification/check.sh
Executable file
37
verification/check.sh
Executable file
|
|
@ -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)."
|
||||
Loading…
Reference in a new issue