mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
mrwulf
59ab518093
Ported from the locally verified Hermes working copy; FeQ and Square2Spec (dead files in the published replica) now compile and are in the check manifest. Basic.lean (never compiled under v4 Aeneas) removed rather than shipped dead. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
169 lines
9.5 KiB
Text
169 lines
9.5 KiB
Text
/- ──────────────────────────────────────────────────────────────────────────────
|
||
Proofs/ReduceSpec.lean — total-correctness spec of the "weak reduction"
|
||
|
||
WHAT THIS FILE CONTAINS
|
||
Spec for the transpiled `FieldElement51::reduce`:
|
||
it never panics, its output limbs are < 2⁵¹ + 19·2¹³ (⊂ 2⁵²), and it
|
||
preserves the value modulo p (exact Nat relation: it subtracts (l4 ≫ 51)·p).
|
||
It also proves two tiny ℕ-level rewrite lemmas (`nat_and_mask`, `nat_shift_div`)
|
||
that turn the hardware bit operations `&&&`/`>>>` into `%`/`/`, the form the
|
||
`omega` decision procedure understands.
|
||
|
||
RUST ANALOG
|
||
`FieldElement51::reduce`, curve25519/solana-ed25519/src/backend/serial/u64/field.rs:290-323
|
||
(its local constant `LOW_51_BIT_MASK`, field.rs:291). The transpiled bodies live in
|
||
gen/CurveField/Funs.lean as `backend.serial.u64.field.FieldElement51.reduce` and
|
||
`...reduce.LOW_51_BIT_MASK`.
|
||
|
||
THE ALGORITHM (what the Rust does)
|
||
A field element is 5 limbs l0..l4 in radix 2⁵¹:
|
||
feVal l = l0 + l1·2⁵¹ + l2·2¹⁰² + l3·2¹⁵³ + l4·2²⁰⁴.
|
||
`reduce` performs one parallel carry pass ("weak reduction" — it shrinks limbs back
|
||
under ~2⁵¹ but does NOT canonicalize below p):
|
||
c_i := l_i >> 51 (the carry-out of limb i; c_i < 2¹³ since l_i < 2⁶⁴)
|
||
m_i := l_i & (2⁵¹ − 1) (the low 51 bits, i.e. l_i mod 2⁵¹)
|
||
r0 := m0 + 19·c4, r_{i+1} := m_{i+1} + c_i (i = 0..3).
|
||
Each carry c_i moves from weight 2^(51·i)·2⁵¹ = 2^(51·(i+1)) to limb i+1 — except c4,
|
||
whose weight 2²⁵⁵ does not exist in the representation; since 2²⁵⁵ ≡ 19 (mod p) it is
|
||
folded back into limb 0 as 19·c4. The value therefore drops by exactly
|
||
c4·(2²⁵⁵ − 19) = p·(l4 div 2⁵¹), giving the EXACT ℕ accounting proved below:
|
||
feVal r + p·(l4 div 2⁵¹) = feVal l.
|
||
No u64 addition can overflow: m_i < 2⁵¹ and 19·c4 < 19·2¹³, so every output limb is
|
||
< 2⁵¹ + 19·2¹³ < 2⁵² ≪ 2⁶⁴ — this is simultaneously the panic-freedom argument and
|
||
the restored limb-bound invariant `Bnd r (2⁵¹ + 19·2¹³)`.
|
||
|
||
ROLE IN THE MAIN THEOREM (Proofs/FieldMain.lean: fieldImplementation)
|
||
`sub` and `negate` (Proofs/SubNegSpec.lean) end with a call to `reduce`; their specs
|
||
compose `reduce_spec` (via the packaged `reduce_make_spec`) with their own limb
|
||
arithmetic. The exact (not merely mod-p) value equation is what lets those callers
|
||
finish their accounting purely over ℕ with `omega` and cast to 𝔽_p only once.
|
||
The `nat_and_mask`/`nat_shift_div` simp lemmas are reused by every carry-chain proof
|
||
(MulSpec, SquareSpec) since `mul`/`pow2k` inline the same mask/shift idiom.
|
||
|
||
FILE RELATIONS
|
||
Imports Proofs/Denote.lean (Fe, feVal, limbsVal, Bnd, P). Imported by
|
||
Proofs/SubNegSpec.lean and Proofs/AddSpec.lean, hence (transitively) by everything
|
||
up to Proofs/FieldMain.lean.
|
||
────────────────────────────────────────────────────────────────────────────── -/
|
||
import Proofs.Denote
|
||
open Aeneas Aeneas.Std Result
|
||
open curve25519_dalek
|
||
|
||
set_option maxHeartbeats 4000000
|
||
|
||
namespace CurveFieldProofs
|
||
|
||
/-- The mask constant evaluates to 2⁵¹ − 1.
|
||
|
||
Rust: `const LOW_51_BIT_MASK: u64 = (1u64 << 51) - 1;` inside `FieldElement51::reduce`,
|
||
curve25519/solana-ed25519/src/backend/serial/u64/field.rs:291.
|
||
|
||
MATH: reduce.LOW_51_BIT_MASK = ok m with m = 2^51 - 1 (= 2251799813685247).
|
||
|
||
WHY NEEDED: in the Aeneas model even this constant is a *fallible* computation
|
||
(`1#u64 <<< 51` then `- 1#u64` — each could in principle overflow), so proving the
|
||
field theorem requires proving it succeeds and pinning its value. The `@[step]`
|
||
attribute registers it with the `step` tactic, so the symbolic execution of
|
||
`reduce`'s body picks it up automatically when it reaches the mask read. -/
|
||
@[step]
|
||
theorem reduce_mask_spec :
|
||
backend.serial.u64.field.FieldElement51.reduce.LOW_51_BIT_MASK
|
||
⦃ m => m.val = 2^51 - 1 ⦄ := by
|
||
unfold backend.serial.u64.field.FieldElement51.reduce.LOW_51_BIT_MASK
|
||
-- symbolically execute the two machine ops (shift, subtract); no side conditions remain
|
||
step*
|
||
|
||
/-- Convert `&&& (2^51-1)` and `>>> 51` on `ℕ` to `%`/`/` so `omega` can reason.
|
||
Stated with the *literal* (2251799813685247 = 2⁵¹−1) since simp normalizes
|
||
`2^51 - 1` to it before these lemmas get a chance to fire.
|
||
|
||
Rust analog: the expression `x & LOW_51_BIT_MASK` (field.rs:310-314 and the same
|
||
idiom in `mul`/`square`); at the `.val : ℕ` level the U64 bitwise-and becomes ℕ's
|
||
`&&&` (`Nat.land`).
|
||
|
||
MATH: n AND (2^51 - 1) = n mod 2^51 — masking the low 51 bits IS reduction
|
||
mod 2^51 (standard two-power identity `Nat.and_two_pow_sub_one_eq_mod`).
|
||
|
||
WHY NEEDED: `omega` (the linear-arithmetic closer of every carry proof) knows
|
||
`/` and `%` but not bitwise ops. Tagging with `@[simp, scalar_tac_simps]` makes
|
||
both `simp_all` and `scalar_tac` eliminate `&&&` on sight, here and in
|
||
MulSpec/SquareSpec. -/
|
||
@[simp, scalar_tac_simps]
|
||
theorem nat_and_mask (n : ℕ) : n &&& 2251799813685247 = n % 2251799813685248 := by
|
||
have := Nat.and_two_pow_sub_one_eq_mod n 51
|
||
norm_num at this
|
||
simpa using this
|
||
|
||
/-- Companion to `nat_and_mask` for the right shift.
|
||
|
||
Rust analog: the carry extraction `limbs[i] >> 51` (field.rs:304-308 and the same
|
||
idiom in `mul`/`square`).
|
||
|
||
MATH: n >> 51 = n div 2^51 (2251799813685248 = 2⁵¹; `Nat.shiftRight_eq_div_pow`).
|
||
|
||
WHY NEEDED: same as `nat_and_mask` — rewrites the hardware shift into the division
|
||
that `omega` can reason about linearly. -/
|
||
@[simp, scalar_tac_simps]
|
||
theorem nat_shift_div (n : ℕ) : n >>> 51 = n / 2251799813685248 := by
|
||
simp [Nat.shiftRight_eq_div_pow]
|
||
|
||
/-- `reduce` spec: total (no panic), output bounded, value preserved mod p.
|
||
|
||
Rust: `FieldElement51::reduce`,
|
||
curve25519/solana-ed25519/src/backend/serial/u64/field.rs:290-323.
|
||
|
||
MATH (note: NO precondition — `reduce` is total on arbitrary u64 limbs):
|
||
ASCII: forall l : Fe with limbs [l0..l4],
|
||
reduce l = ok r with Bnd(r, 2^51 + 19*2^13)
|
||
and feVal r + p * (l4 div 2^51) = feVal l.
|
||
LaTeX: $\forall l,\ \exists r,\ \mathrm{reduce}(l) = \mathrm{ok}\ r \wedge
|
||
\mathrm{Bnd}(r, 2^{51} + 19\cdot 2^{13}) \wedge
|
||
\llbracket r\rrbracket_{\mathbb N} + p\lfloor l_4/2^{51}\rfloor
|
||
= \llbracket l\rrbracket_{\mathbb N}$.
|
||
|
||
The value clause is EXACT ℕ arithmetic, not a congruence mod p: the only multiple
|
||
of p that `reduce` removes is c4·p where c4 = l4 div 2⁵¹ (the carry out of the top
|
||
limb, folded back as 19·c4 because 2²⁵⁵ ≡ 19 mod p — see the file header). Crucially
|
||
it is stated WITHOUT subtraction (`feVal r + P·c4 = feVal l`, not
|
||
`feVal r = feVal l − P·c4`): ℕ-subtraction truncates at 0 and breaks linear
|
||
reasoning, whereas this purely additive form is a linear Diophantine equation in
|
||
the `%`/`/` terms of the input limbs — exactly the fragment `omega` decides.
|
||
|
||
The bound 2⁵¹ + 19·2¹³ is sharp for limb 0 (mask < 2⁵¹ plus 19·c4 with c4 < 2¹³);
|
||
limbs 1–4 satisfy the stronger < 2⁵¹ + 2¹³. Callers weaken it to `Bnd r (2^52)`
|
||
via `Bnd.mono`.
|
||
|
||
WHY NEEDED: `sub_spec`/`neg_spec` (SubNegSpec.lean) run `reduce` on their raw
|
||
"a + 16p − b" limbs; this spec provides both their panic-freedom (one conjunct of
|
||
the main theorem's totality claim) and the value bookkeeping that turns into
|
||
⟪r⟫ = ⟪a⟫ − ⟪b⟫ after the single cast to 𝔽_p. -/
|
||
theorem reduce_spec (l : Fe) (l0 l1 l2 l3 l4 : U64)
|
||
(hl : (↑l : List U64) = [l0, l1, l2, l3, l4]) :
|
||
fe_reduce l ⦃ r =>
|
||
Bnd r (2^51 + 19 * 2^13) ∧
|
||
feVal r + P * (l4.val / 2^51) = feVal l ⦄ := by
|
||
-- expose the transpiled monadic body (gen/CurveField/Funs.lean)
|
||
unfold fe_reduce backend.serial.u64.field.FieldElement51.reduce
|
||
-- step*: symbolically execute the whole program, one machine op per step (5 shifts,
|
||
-- 5 masks, the ×19, 5 carry adds, plus the interleaved array reads/writes — ~45 ops).
|
||
-- For each op it applies the registered @[step] spec (U64.add_spec, reduce_mask_spec,
|
||
-- Array.index_usize_spec, ...), names the result, and discharges every overflow /
|
||
-- index-in-bounds side condition with the supplied `by` block:
|
||
-- subst_vars — substitute the equations of earlier steps,
|
||
-- simp [...] — evaluate array get-after-set chains,
|
||
-- scalar_tac — close the remaining linear bound (e.g. mask + 19·carry < 2⁶⁴).
|
||
step* by (subst_vars
|
||
try simp [Array.set_val_eq, *]
|
||
try scalar_tac)
|
||
-- Final postcondition: normalize the set-chain + all value equations to
|
||
-- %/÷ arithmetic over the input limbs (simp_all also uses the inaccessible
|
||
-- step*-generated hypotheses), then close with omega.
|
||
-- After simp_all (which fires nat_and_mask/nat_shift_div) the goal is the pure
|
||
-- linear identity over ℕ:
|
||
-- Σᵢ (lᵢ % 2⁵¹)·2^(51i) + 19·(l4/2⁵¹) + Σᵢ₌₀..₃ (lᵢ/2⁵¹)·2^(51(i+1))
|
||
-- + (2²⁵⁵−19)·(l4/2⁵¹) = Σᵢ lᵢ·2^(51i)
|
||
-- which follows from lᵢ = (lᵢ % 2⁵¹) + 2⁵¹·(lᵢ/2⁵¹); scalar_tac ends in omega.
|
||
simp_all [Array.set_val_eq, P, limbsVal, Bnd, feVal]
|
||
scalar_tac
|
||
|
||
end CurveFieldProofs
|