risc0-ed25519-verified/verification/Proofs/Field.lean

/- ───────────────────────────────────────────────────────────────────────────
   Proofs/Field.lean — Field packaging, part 1 of 2 (part 2 = multiplicative
   inverses, which land in InvertSpec.lean and FieldMain.lean).

   CONTEXT. The Rust crate curve25519/solana-ed25519 implements arithmetic in
   F_p, p = 2^255 - 19, on 5 radix-2^51 u64 limbs (`FieldElement51`, in
   curve25519/solana-ed25519/src/backend/serial/u64/field.rs, driven by
   src/field.rs). That code was transpiled mechanically (Charon + Aeneas) to
   gen/CurveField/{Types,Funs}.lean. The denotation ⟪a⟫ ∈ F_p of a limb
   vector a and the limb-bound invariant `Bnd` live in Proofs/Denote.lean.

   THIS FILE supplies the purely mathematical scaffolding that the main
   theorem (Proofs/FieldMain.lean: `fieldImplementation`) needs around the
   per-operation specs:

   * 𝔽_p IS a field: p = 2²⁵⁵ − 19 is prime (Proofs/P25519.lean, axiom-free),
     so mathlib's `ZMod.instField` applies.  Registering `Fact (Nat.Prime P)`
     is what unlocks that instance (`P_prime`, the two instances below).
   * The denotation ⟪·⟫ : Fe → 𝔽_p is SURJECTIVE on bounded elements (via the
     canonical `encode`, which writes y < p in base 2⁵¹), so the transpiled
     type covers all of 𝔽_p — without this, "implements the field" would be
     vacuous on unreachable elements (`encode` … `denote_surjective`).
   * The transpiled ops realize the field ops of 𝔽_p through ⟪·⟫ (proved in
     the *Spec.lean files this file imports; re-packaged in FieldMain.lean).
   * `spec_exists` converts total-correctness triples `x ⦃ post ⦄` into plain
     existentials `∃ r, x = ok r ∧ post r`, the form used by FieldMain.lean.

   There is NO Rust analog for this file: it is meta-level mathematics about
   the transpiled code, not transpiled code itself.

   Imports: ConstSpecs/AddSpec/SubNegSpec/MulSpec (the operation specs) and
   P25519 (primality).  Imported by: InvertSpec.lean (needs the `Field Fp`
   instance for `⁻¹` and Fermat) and, through it, FieldMain.lean.
   ─────────────────────────────────────────────────────────────────────── -/
import Proofs.ConstSpecs
import Proofs.AddSpec
import Proofs.SubNegSpec
import Proofs.MulSpec
import Proofs.P25519
open Aeneas Aeneas.Std Result
open curve25519_dalek

set_option maxHeartbeats 4000000
set_option maxRecDepth 8000

namespace CurveFieldProofs

/-! ## 𝔽_p is a field -/

/- MATH:  Nat.Prime P  where  P = 2^255 - 19  (the numeral defined in
   Proofs/Denote.lean).  This is `p25519_prime` from Proofs/P25519.lean — a
   fully kernel-checked Pratt/Lucas primality certificate, no `native_decide`,
   no axioms — restated with the literal `2^255 - 19` rewritten to `P` so it
   matches the form mathlib's instance machinery will look for.
   WHY NEEDED: primality of the modulus is THE reason `ZMod P` is a field
   (inverses exist); everything in InvertSpec/FieldMain rests on it. -/
theorem P_prime : Nat.Prime P := by
  have h := p25519_prime                       -- the certificate, for 2^255 - 19
  have : (2:ℕ)^255 - 19 = P := by norm_num [P] -- the numeral really is P
  rwa [this] at h                              -- transport the certificate to P

/- Register the primality as a typeclass `Fact`, the hook mathlib uses to
   activate `Field (ZMod P)` (instance `ZMod.instField`).  Without this
   instance, `Fp` would only be a commutative ring and `⟪a⟫⁻¹` would not be
   available.  WHY NEEDED: unlocks `Field Fp` for every later proof. -/
instance : Fact (Nat.Prime P) := ⟨P_prime⟩

/- MATH: P ≠ 0.  A small side instance some mathlib lemmas about `ZMod.val`
   require (e.g. `ZMod.val_lt` used in `val_lt_P` below). -/
instance : NeZero P := ⟨by norm_num [P]⟩

/-- 𝔽_p = ZMod p with p prime is a field (mathlib instance).
    This `example` is a compile-time sanity check that the two instances
    above really do trigger mathlib's `ZMod.instField`; it generates no
    code and is never referenced (FieldMain.lean re-exposes the instance
    as the abbrev `Fp_field`). -/
noncomputable example : Field Fp := inferInstance

/-! ## Surjectivity of the denotation

The representation is REDUNDANT: many limb vectors denote the same field
element, and arbitrary `Fe`s (limbs up to 2⁶⁴) may not even satisfy the
operations' preconditions. To state "the code implements all of 𝔽_p" we must
therefore exhibit, for every y ∈ 𝔽_p, at least one WELL-BOUNDED limb vector
denoting y. `encode` constructs the canonical one: the base-2⁵¹ digits of
the unique representative y.val ∈ [0, p). -/

/-- Build a `U64` from a natural number (mod 2⁶⁴).
    Aeneas's `U64` wraps a 64-bit `BitVec`; `.val : Nat` is its mathematical
    value. Rust analog: a `u64` literal / `as u64` cast.
    WHY NEEDED: `encode` must manufacture concrete machine limbs. -/
def mkU64 (n : ℕ) : U64 := ⟨BitVec.ofNat 64 n⟩

/- MATH:  forall n < 2^64,  (mkU64 n).val = n  — the round-trip is exact as
   long as the input fits in 64 bits (BitVec.ofNat reduces mod 2^64, and the
   hypothesis makes the reduction a no-op).
   WHY NEEDED: lets `encode_bnd`/`denote_encode` compute with the limb values
   of `encode y` as plain naturals. -/
theorem mkU64_val (n : ℕ) (h : n < 2^64) : (mkU64 n).val = n := by
  show (BitVec.ofNat 64 n).toNat = n
  simp only [BitVec.toNat_ofNat]  -- .val of ofNat is n % 2^64
  omega                            -- n < 2^64 kills the mod

/-- Canonical (reduced, base-2⁵¹) representative of a field element:
    limb i = the i-th base-2⁵¹ digit of y.val (the canonical natural < p).

    MATH:  encode y = [ y mod 2^51, (y / 2^51) mod 2^51, (y / 2^102) mod 2^51,
                        (y / 2^153) mod 2^51,  y / 2^204 ]
    so   limbsVal (encode y) = y.val   exactly (no mod p reduction needed,
    since y.val < p < 2^255).  The top limb needs no mask: y.val / 2^204 <
    2^51 because y.val < p < 2^255.

    Rust analog (conceptually): `FieldElement51::from_bytes` of the little-
    endian encoding of y — here built directly as digits, which is simpler
    to reason about.  `Array.make 5#usize [...]` mirrors the transpiled
    representation `FieldElement51 = Array U64 5` (a Rust `[u64; 5]`).
    WHY NEEDED: the witness for `denote_surjective`. -/
def encode (y : Fp) : Fe :=
  Array.make 5#usize
    [ mkU64 (y.val % 2^51),
      mkU64 (y.val / 2^51 % 2^51),
      mkU64 (y.val / 2^102 % 2^51),
      mkU64 (y.val / 2^153 % 2^51),
      mkU64 (y.val / 2^204) ]

/- MATH: the underlying limb list of `encode y` is literally the 5-digit
   list above (`rfl`: true by unfolding the definitions).
   WHY NEEDED: `Bnd`/`feVal` are stated via the limb LIST (`Bnd_eq`,
   `feVal_eq` in Proofs/Denote.lean), so the next two proofs need the list
   in explicit form. -/
theorem encode_list (y : Fp) :
    (↑(encode y) : List U64)
      = [ mkU64 (y.val % 2^51), mkU64 (y.val / 2^51 % 2^51),
          mkU64 (y.val / 2^102 % 2^51), mkU64 (y.val / 2^153 % 2^51),
          mkU64 (y.val / 2^204) ] := rfl

/- MATH:  forall y in F_p,  y.val < P  — the canonical representative is
   reduced.  Pure mathlib (`ZMod.val_lt`, needs `NeZero P` above); restated
   here for convenient repeated use.
   WHY NEEDED: gives the size bound that makes all of `encode`'s digits and
   their recombination fit (P < 2^255 = (2^51)^5). -/
theorem val_lt_P (y : Fp) : y.val < P := ZMod.val_lt y

/- MATH:  forall y in F_p,  Bnd (encode y) (2^51)  — every limb of the
   canonical representative is < 2^51 (it is a base-2^51 digit; the top limb
   because y.val < P < 2^255).  This is even stronger than the 2^52 "valid
   output" bound used downstream.
   WHY NEEDED: surjectivity must produce BOUNDED witnesses, otherwise the
   operations' preconditions could never be met on them. -/
theorem encode_bnd (y : Fp) : Bnd (encode y) (2^51) := by
  have h := val_lt_P y
  have hP : P < 2^255 := by norm_num [P]
  -- switch from the opaque `Fe` to the explicit 5-element limb list
  rw [Bnd_eq _ _ _ _ _ _ _ (encode_list y)]
  -- 5 goals, one per limb: each digit is < 2^51 by omega
  -- (mod-2^51 digits trivially; the top limb via y.val < P < 2^255)
  refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;>
    (rw [mkU64_val _ (by omega)]; omega)

/- MATH:  forall y in F_p,  ⟪encode y⟫ = y  — decode ∘ encode = id.
   LaTeX:  $\forall y,\ \llbracket \mathrm{encode}\,y \rrbracket = y$.
   Proof: the base-2^51 digits recombine to exactly y.val (omega), and
   casting y.val back into ZMod P is the identity.
   WHY NEEDED: the second half of the surjectivity witness. -/
theorem denote_encode (y : Fp) : ⟪encode y⟫ = y := by
  have h := val_lt_P y
  have hP : P < 2^255 := by norm_num [P]
  -- step 1: the natural-number value of the limbs is exactly y.val
  have hval : feVal (encode y) = y.val := by
    rw [feVal_eq _ _ _ _ _ _ (encode_list y)]
    simp only [limbsVal]
    -- each digit fits in u64, so mkU64 is value-preserving on it
    rw [mkU64_val _ (by omega), mkU64_val _ (by omega), mkU64_val _ (by omega),
        mkU64_val _ (by omega), mkU64_val _ (by omega)]
    -- digit recombination: d0 + d1·2^51 + d2·2^102 + d3·2^153 + d4·2^204 = y.val
    omega
  -- step 2: (y.val : ZMod P) = y  (cast of the canonical representative)
  simp [denote, hval, ZMod.natCast_val, ZMod.cast_id]

/-- Every element of 𝔽_p is the denotation of a (well-bounded) `Fe`.

    MATH:  forall y : F_p,  exists a : Fe,  Bnd(a, 2^52)  and  ⟪a⟫ = y.
    LaTeX: $\forall y \in \mathbb{F}_p\ \exists a,\
            \mathrm{Bnd}(a,2^{52}) \wedge \llbracket a\rrbracket = y$.
    The witness is `encode y` (bounded by 2⁵¹, weakened to the standard
    "valid element" bound 2⁵² via `Bnd.mono`).
    WHY NEEDED: this is the `surj` field of `IsFieldImplementation`
    (FieldMain.lean) — it makes "implements 𝔽_p" mean ALL of 𝔽_p. -/
theorem denote_surjective : ∀ y : Fp, ∃ a : Fe, Bnd a (2^52) ∧ ⟪a⟫ = y :=
  fun y => ⟨encode y, (encode_bnd y).mono (by norm_num), denote_encode y⟩

/-! ## The triple → existential bridge (library: `Std.WP.spec_imp_exists`) -/

/- MATH:  if  x ⦃ post ⦄  (total correctness: x does not panic AND its result
   satisfies post), then  exists r, x = ok r and post r.
   This merely re-exports the Aeneas library lemma `Std.WP.spec_imp_exists`
   with the triple written in this project's notation.
   WHY NEEDED: the `run_*` theorems and `IsFieldImplementation` fields in
   FieldMain.lean are phrased as plain existentials over `= ok r` (readable
   without knowing the WP calculus); this is the converter. -/
theorem spec_exists {α} {x : Result α} {p : α → Prop}
    (h : x ⦃ r => p r ⦄) : ∃ r, x = ok r ∧ p r :=
  Std.WP.spec_imp_exists h

end CurveFieldProofs