clazel-p384: group law, scalar product and verify, proven against the contract (3.5h, PR3), tier 0

crates/clazel-p384/Cargo.toml

@@ -11,9 +11,10 @@ vstd = "=0.0.0-2026-10-04-0306"
 fiat-crypto = { version = "=0.3.0", default-features = false }
 
 # Verification tier (docs/VERIFICATION.md). `tier` is what is proven about
-# the shipped code today; `target-tier` is what the policy requires. The spec
-# and the field arithmetic exist, but there is no `verify` and none of the
-# tier 1 or tier 2 evidence yet, so tier 0.
+# the shipped code today; `target-tier` is what the policy requires. The spec,
+# the field, the group law and `verify` exist and are proven, but none of the
+# tier 1 or tier 2 evidence (Kani harnesses, mutations of the code, an
+# independent transcription, conformance suites) does yet, so tier 0.
 [package.metadata.clazel]
 tier = 0
 target-tier = 2

crates/clazel-p384/README.md

@@ -4,10 +4,12 @@ ECDSA signature verification over NIST P-384 (FIPS 186-5 §6.4.2), specified
 in Verus. Part of [Clazel](../../README.md), a web browser whose parsers of
 untrusted input carry machine-checked proofs.
 
-## Status: specification and field arithmetic
+## Status: specification, field, point arithmetic and `verify`
 
-**Tier 0, target tier 2.** The specification and the field arithmetic are
-written; the point arithmetic and `verify` are not. What exists:
+**Tier 0, target tier 2.** The specification, the field arithmetic, the
+point arithmetic and `verify` are written, and `verify` is proven against
+the contract below the six axioms. The tier 1 and tier 2 evidence is not
+(see Verification). What exists:
 
 - `src/spec.rs`: what "a valid ECDSA P-384 signature" means, transcribed
   step by step from FIPS 186-5 §6.4.2, with the routines it defers to taken
@@ -16,17 +18,24 @@ written; the point arithmetic and `verify` are not. What exists:
   sources are pinned by SHA-256 in the file's header, which also lists every
   modelling choice (13 of them) and how the lossy text extraction of the
   PDFs was read.
-- `src/contract.rs`: what the executable `verify(digest, r, s, point)` will
-  be proven to satisfy, as predicates over the spec.
+- `src/contract.rs`: what the executable `verify(digest, r, s, point)` is
+  proven to satisfy, as predicates over the spec. `src/point_contract.rs`:
+  the same for the group law, the scalar product, the key decoding and the
+  digest's reduction.
 - `src/examples.rs`: known answers, proven by evaluating the spec
   (`by (compute_only)`), on a toy curve and on P-384.
 - `src/axioms.rs`, `src/field/`: the field arithmetic, described below.
+- `src/point.rs`, `src/scalar.rs`, `src/verify.rs`, `src/convert.rs`,
+  `src/lemmas.rs`: the executable group law, key decoding, scalar product,
+  `verify`, and their lemmas, described below.
 - `tests/field.rs`: known answers for the field, computed with Python.
+- `tests/verify.rs`: smoke tests of `verify` (Wycheproof vectors and
+  hand-damaged inputs), described below.
 
-Nothing here claims verification of `verify`, which does not exist yet. What
-is evaluated is the spec itself, which shows the transcription computes what
-was worked out independently, not that it matches the standards (a person
-reads it against them; [docs/SPEC-STYLE.md](../../docs/SPEC-STYLE.md)).
+What is evaluated in `examples.rs` is the spec itself, which shows the
+transcription computes what was worked out independently, not that it matches
+the standards (a person reads it against them;
+[docs/SPEC-STYLE.md](../../docs/SPEC-STYLE.md)).
 
 ## The field (modulo p and modulo n)
 
@@ -66,6 +75,48 @@ they stand for.
   That is the check on the axioms' fit to the real fiat, and on the constants
   of `field/spec.rs` and `fe.rs` (the moduli, `R^2 mod m`, the exponents).
 
+## The group law, the scalar product and `verify`
+
+Proven in Verus against `spec.rs`, over the six axioms and nothing else (no
+new axiom, no `assume`, no `external_body` outside `axioms.rs`).
+
+- **`point::Point`** is the point at infinity or an affine pair of `Fe`s
+  modulo p, with a view to `spec::Point`. `point::ec_add` runs SEC 1 §2.2.1's
+  rules in the spec's order (rules 1 and 2, then the negation test `x1 == x2
+  && (y1 + y2) % p == 0`, then different x, then doubling), each field
+  operation an `Fe` operation, so its contract is `r == spec::ec_add(p384(),
+  a, b)`, `None` exactly when the spec's is (a failed `inv`).
+- **`point::decode_public_key`** is `spec::decode_public_key`: length 97, first
+  octet `04`, each coordinate below p by `Fe::from_octets`, and the curve
+  equation. Compressed, hybrid and infinity encodings are refused.
+- **`scalar::scalar_mul`** is MSB-first double-and-add over the 48 octets of
+  the scalar, one bit at a time; the loop invariant is that after the top `i`
+  bits the accumulator is `spec::scalar_mul` of the integer they make, from
+  the spec's own recursion. No associativity is used.
+- **`scalar::derive_e`** reads the leftmost `min(|H|, 48)` octets of the digest
+  and reduces them modulo n by Horner's rule in the field, so `e >= n` is
+  handled; the proof relates the spec's bit-string `derive_e` to `os2ip`.
+- **`verify::verify`** follows the spec's order: the key first, step 1 (`r`
+  and `s` in `[1, n - 1]` as integers, before any reduction), step 3, step 4
+  (`Fe::inv` mod n), step 5, step 6 as the sum of two separately computed
+  products (infinity and any failed operation reject), and step 9 with
+  `x_R mod n` reduced properly (`x_R < p` can exceed n). Its contract is
+  `ok == ecdsa_verify(p384(), digest, os2ip(r), os2ip(s), point)` for a
+  digest of 0 to 64 octets.
+- **Not constant time, by design**, and slow by design: this is the affine
+  stage, one field inversion (about 768 multiplications) per group
+  operation. Measured by `tests/verify.rs`'s `timing` test on the development
+  machine (Apple silicon): about 0.94 s per verification in a debug build and
+  about 45 ms in a release build.
+- **Smoke tests, not conformance.** `tests/verify.rs` accepts eight valid
+  and rejects six invalid vectors of Wycheproof's
+  `ecdsa_secp384r1_sha384_test.json` (commit `d17cc89f`; tcIds in the file),
+  and rejects damaged `r`, `s`, digests and keys. Wycheproof in full, ACVP and
+  a differential against another engine are later work.
+- **One addition to `field::Fe`:** `Fe::dup`, a copy with the same
+  `which` and `val`. `Fe` is not `Clone` and `Fe`'s contracts and the axioms
+  are unchanged.
+
 ## What it is, and what it is not
 
 **Public-key verification only.** The key, the signature and the digest are
@@ -114,16 +165,19 @@ times out on it.
 
 Run `cargo verus focus -- -A missing_docs` in this directory. What it
 proves today is that every spec function terminates (each recursive one has a
-`decreases`), that the evaluated examples hold, and that each field function
-meets its contract in `field/contract.rs` over the six axioms.
+`decreases`), that the evaluated examples hold, that each field function
+meets its contract in `field/contract.rs`, and that `ec_add`,
+`scalar_mul`, `decode_public_key`, `derive_e` and `verify` meet theirs
+(`point_contract.rs`, `contract.rs`), over the six axioms.
 `mutations.json` holds 26 mutations of `spec.rs`, each killed with a
-certificate that contradicts one of those examples; the field code has no
-mutations yet. There is no lemma about the spec of the signature itself, no
-independent transcription, no conformance test against an official suite and
-no Kani harness yet, so the crate stays at tier 0; see
+certificate that contradicts one of those examples; the executable code has
+no mutations yet. There is no lemma about the spec of the signature itself,
+no independent transcription, no conformance test against an official suite
+and no Kani harness yet, so the crate stays at tier 0; see
 [docs/VERIFICATION.md](../../docs/VERIFICATION.md) for what each tier
-requires. `verify` is not written, so nothing here proves anything about
-ECDSA verification yet.
+requires. The proofs cover memory and arithmetic safety of the Verus-checked
+code, but the claim is only as good as `spec.rs` (read against the standards
+by a person) and the six axioms (fiat-crypto's printed postconditions).
 
 ## Licence
 

crates/clazel-p384/src/contract.rs

@@ -1,8 +1,9 @@
-//! The contract the executable `verify` must be proven to meet. There is no
-//! executable code yet; these predicates are what its `requires` and
-//! `ensures` clauses will be, so reviewing them and [`super::spec`] is
-//! enough to know what the implementation will guarantee (the same shape as
-//! `clazel-pkcs1`'s `contract.rs`).
+//! The contract the executable `verify` is proven to meet. These predicates
+//! are its `requires` and `ensures` clauses (`src/verify.rs`), so reviewing
+//! them and [`super::spec`] is enough to know what the implementation
+//! guarantees (the same shape as `clazel-pkcs1`'s `contract.rs`). The
+//! contracts of the functions it is built from are in
+//! [`super::point_contract`] and [`super::field::contract`].
 //!
 //! ```text
 //! pub fn verify(digest: &[u8], r: &[u8; 48], s: &[u8; 48], point: &[u8]) -> (ok: bool)

crates/clazel-p384/src/convert.rs

@@ -0,0 +1,103 @@
+//! Small conversions the point and scalar code needs: an octet as a
+//! residue, and an octet string reduced modulo p or n (Horner's rule over
+//! the field operations). Both are proven against [`crate::spec::os2ip`].
+
+#[allow(unused_imports)]
+use super::spec::*;
+#[allow(unused_imports)]
+use vstd::prelude::*;
+
+verus! {
+
+use crate::field::Fe;
+
+/// The residue `b`, for an octet `b` (both moduli exceed 255).
+pub fn fe_of_byte(w: crate::field::spec::Which, b: u8) -> (r: Fe)
+    ensures
+        r.which() == w,
+        r.val() == b as nat,
+{
+    let mut o = [0u8;48];
+    o[47] = b;
+    proof {
+        crate::lemmas::lemma_os2ip_last(o@);
+        crate::lemmas::lemma_modulus_gt_256(w);
+    }
+    match Fe::from_octets(w, &o) {
+        Some(f) => f,
+        // Unreachable: os2ip(o) = b < 256 < modulus.
+        None => {
+            proof {
+                assert(false);
+            }
+            Fe::one(w)
+        },
+    }
+}
+
+/// The residue 256.
+fn fe_256(w: crate::field::spec::Which) -> (r: Fe)
+    ensures
+        r.which() == w,
+        r.val() == 256,
+{
+    let a = fe_of_byte(w, 255);
+    let one = Fe::one(w);
+    proof {
+        crate::lemmas::lemma_modulus_gt_256(w);
+        vstd::arithmetic::div_mod::lemma_small_mod(256nat, crate::field::spec::modulus(w));
+    }
+    a.add(&one)
+}
+
+/// The octets `o[0..k]`, big-endian, as an integer reduced modulo the
+/// modulus of `w`: `os2ip(o[0..k]) mod m`. Horner's rule in the field, so
+/// that no integer ever exceeds the modulus; this is how a value that may be
+/// at least the modulus (the digest `e` against n, `x_R` against n) is
+/// reduced.
+pub fn reduce_prefix(w: crate::field::spec::Which, o: &[u8], k: usize) -> (r: Fe)
+    requires
+        k <= o.len(),
+    ensures
+        r.which() == w,
+        r.val() == os2ip(o@.subrange(0, k as int)) % crate::field::spec::modulus(w),
+{
+    let c256 = fe_256(w);
+    let mut acc = fe_of_byte(w, 0);
+    let mut i: usize = 0;
+    proof {
+        assert(o@.subrange(0, 0) =~= Seq::<u8>::empty());
+        crate::lemmas::lemma_modulus_gt_256(w);
+        vstd::arithmetic::div_mod::lemma_small_mod(0nat, crate::field::spec::modulus(w));
+    }
+    while i < k
+        invariant
+            i <= k,
+            k <= o.len(),
+            acc.which() == w,
+            c256.which() == w,
+            c256.val() == 256,
+            acc.val() == os2ip(o@.subrange(0, i as int)) % crate::field::spec::modulus(w),
+        decreases k - i,
+    {
+        let byte: u8 = match o.get(i) {
+            Some(b) => *b,
+            None => 0,
+        };
+        let b = fe_of_byte(w, byte);
+        let shifted = acc.mul(&c256);
+        let next = shifted.add(&b);
+        proof {
+            let pre = o@.subrange(0, i as int);
+            crate::field::lemmas::lemma_os2ip_push(pre, byte);
+            assert(o@.subrange(0, i as int + 1) =~= pre.push(byte));
+            crate::lemmas::lemma_modulus_gt_256(w);
+            crate::lemmas::lemma_horner_mod(os2ip(pre), byte as nat, crate::field::spec::modulus(w));
+        }
+        acc = next;
+        i = i.saturating_add(1);
+    }
+    acc
+}
+
+} // verus!

crates/clazel-p384/src/field/fe.rs

@@ -50,6 +50,19 @@ impl Fe {
         from_montgomery(self.which, self.limbs@)
     }
 
+    /// A copy: the same limbs, so the same modulus and residue. (`Fe` is not
+    /// `Clone`: the derive would give no contract.)
+    pub fn dup(&self) -> (r: Fe)
+        ensures
+            r.which() == self.which(),
+            r.val() == self.val(),
+    {
+        proof {
+            use_type_invariant(self);
+        }
+        Fe { which: self.which, limbs: self.limbs }
+    }
+
     /// The residue is below the modulus. A no-op at run time: it hands the
     /// type invariant to the caller's proof.
     pub fn val_lt_modulus(&self)