mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
mrwulf
d08a6e1890
Canonicity pass (the layer is now closed under its own preconditions): - sub_val_spec post carries the exact value equation (exists beta <= 1, scVal r + scVal b = scVal a + ell*beta, with the underflow guard beta = 1 -> scVal a < scVal b) - add/montgomery_reduce/mul/aggregate posts all carry scVal r < ell: canonical inputs give canonical outputs everywhere. Needed because from_bytes_wide (hash-to-scalar) feeds Montgomery outputs into add. Hash-to-scalar foundation (toward Scalar::from_hash / EdDSA verify): - extraction scope + from_bytes_wide (brings constants::R); regenerated gen - source repos carry a documented Aeneas-compat patch: the bare `hi[4] = words[7] >> 20` extracts ill-typed at pin bf13c42e; masked (semantic no-op, words[7] >> 20 < 2^44) - Proofs/ScalarWideSpec.lean: R constant lemmas (R = 2^260 mod ell, witness 2^260 = R + 255*ell) and montgomery_mul_spec, the single Montgomery round: [r]*2^260 = [a]*[b], canonical bounded output check-scalar.sh: 10 proof files, 11 kernel audits, all exactly [propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
99 lines
5.4 KiB
Text
99 lines
5.4 KiB
Text
/- ──────────────────────────────────────────────────────────────────────────────
|
||
Proofs/ScalarMain.lean — the scalar-layer aggregate certificate.
|
||
|
||
Clean-interface corollaries of the assembly proofs, stated through
|
||
`ScBnd` (52-bit limb representation) and `scDenote` (⟦·⟧ : Scalar52 →
|
||
ZMod ℓ), plus the single bundled certificate `scalarImplementation`:
|
||
|
||
· add: canonical inputs → ⟦add a b⟧ = ⟦a⟧ + ⟦b⟧
|
||
· sub: canonical inputs → ⟦sub a b⟧ = ⟦a⟧ − ⟦b⟧
|
||
· mul: Montgomery input bound → ⟦mul a b⟧ = ⟦a⟧ · ⟦b⟧
|
||
(canonical inputs satisfy it: ℓ·ℓ < 2^260·ℓ)
|
||
Every output is both ScBnd (52-bit limbs) and canonical (scVal < ℓ):
|
||
the layer is closed under its own preconditions.
|
||
|
||
Audit: `#print axioms ScalarProofs.scalarImplementation` must report
|
||
exactly [propext, Classical.choice, Quot.sound].
|
||
────────────────────────────────────────────────────────────────────────────── -/
|
||
import Proofs.ScalarFullMulSpec
|
||
import Proofs.ScalarAddSpec
|
||
open Aeneas Aeneas.Std Result
|
||
open curve25519_dalek
|
||
|
||
set_option linter.unusedSimpArgs false
|
||
set_option exponentiation.threshold 600
|
||
|
||
namespace ScalarProofs
|
||
|
||
open Aeneas.Std.WP
|
||
|
||
/-- Addition, clean interface. -/
|
||
theorem scalar_add_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b)
|
||
(hca : scVal a < Ell) (hcb : scVal b < Ell) :
|
||
backend.serial.u64.scalar.Scalar52.add a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a + scDenote b ⦄ := by
|
||
obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha
|
||
obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb
|
||
apply spec_mono (add_val_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl
|
||
⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hca hcb)
|
||
intro r hr
|
||
exact ⟨hr.1, hr.2.1, hr.2.2⟩
|
||
|
||
/-- Subtraction, clean interface: canonical inputs give a canonical output
|
||
(β = 0: r = a − b < ℓ; β = 1: the guard says a < b, so r = a − b + ℓ < ℓ). -/
|
||
theorem scalar_sub_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b)
|
||
(hca : scVal a < Ell) (hcb : scVal b ≤ Ell) :
|
||
backend.serial.u64.scalar.Scalar52.sub a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a - scDenote b ⦄ := by
|
||
obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha
|
||
obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb
|
||
apply spec_mono (sub_val_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl
|
||
⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hcb)
|
||
intro r hr
|
||
obtain ⟨hbnds, ⟨β, hβle, heq, hguard⟩, hden⟩ := hr
|
||
refine ⟨hbnds, ?_, hden⟩
|
||
rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hβle with h0 | h1
|
||
· subst h0; omega
|
||
· subst h1; have := hguard rfl; omega
|
||
|
||
/-- Multiplication, clean interface. The Montgomery hypothesis
|
||
scVal a · scVal b < 2^260·ℓ holds in particular for canonical inputs. -/
|
||
theorem scalar_mul_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b)
|
||
(hm : scVal a * scVal b < 2^260 * Ell) :
|
||
backend.serial.u64.scalar.Scalar52.mul a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a * scDenote b ⦄ := by
|
||
obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha
|
||
obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb
|
||
apply spec_mono (mul_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl
|
||
⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hm)
|
||
intro r hr
|
||
exact ⟨hr.1, hr.2.1, hr.2.2⟩
|
||
|
||
/-- Canonical inputs always satisfy the Montgomery multiplication bound. -/
|
||
theorem canonical_mul_bound {a b : Sc} (hca : scVal a < Ell) (hcb : scVal b < Ell) :
|
||
scVal a * scVal b < 2^260 * Ell := by
|
||
have h1 : scVal a * scVal b < Ell * Ell := Nat.mul_lt_mul'' hca hcb
|
||
have h2 : Ell * Ell ≤ 2^260 * Ell :=
|
||
Nat.mul_le_mul_right Ell (by unfold Ell; norm_num)
|
||
exact lt_of_lt_of_le h1 h2
|
||
|
||
/-- **The scalar-layer certificate**: the transpiled `Scalar52` add, sub
|
||
and mul all denote the ring operations of ZMod ℓ on canonical inputs,
|
||
and every output is again 52-bit-bounded AND canonical — the layer is
|
||
closed under its own preconditions. One theorem, one axiom audit. -/
|
||
theorem scalarImplementation :
|
||
(∀ a b : Sc, ScBnd a → ScBnd b → scVal a < Ell → scVal b < Ell →
|
||
backend.serial.u64.scalar.Scalar52.add a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a + scDenote b ⦄) ∧
|
||
(∀ a b : Sc, ScBnd a → ScBnd b → scVal a < Ell → scVal b ≤ Ell →
|
||
backend.serial.u64.scalar.Scalar52.sub a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a - scDenote b ⦄) ∧
|
||
(∀ a b : Sc, ScBnd a → ScBnd b → scVal a < Ell → scVal b < Ell →
|
||
backend.serial.u64.scalar.Scalar52.mul a b
|
||
⦃ r => ScBnd r ∧ scVal r < Ell ∧ scDenote r = scDenote a * scDenote b ⦄) :=
|
||
⟨fun a b ha hb hca hcb => scalar_add_correct a b ha hb hca hcb,
|
||
fun a b ha hb hca hcb => scalar_sub_correct a b ha hb hca hcb,
|
||
fun a b ha hb hca hcb =>
|
||
scalar_mul_correct a b ha hb (canonical_mul_bound hca hcb)⟩
|
||
|
||
end ScalarProofs
|