clazel-p384: field arithmetic over fiat-crypto behind six axioms (3.5h, PR2), tier 0

crates/clazel-p384/Cargo.toml

@@ -8,10 +8,12 @@ description = "ECDSA signature verification over NIST P-384 (FIPS 186-5 §6.4.2)
 
 [dependencies]
 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. This
-# crate is specification only so far: nothing is implemented, so tier 0.
+# 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.
 [package.metadata.clazel]
 tier = 0
 target-tier = 2

crates/clazel-p384/README.md

@@ -4,11 +4,10 @@ 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 only
+## Status: specification and field arithmetic
 
-**Tier 0, target tier 2.** Nothing is implemented. This crate has no
-executable code: no field arithmetic, no point arithmetic and no `verify`
-function. What exists is the part a person reviews:
+**Tier 0, target tier 2.** The specification and the field arithmetic are
+written; the point arithmetic and `verify` are not. 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
@@ -21,11 +20,51 @@ function. What exists is the part a person reviews:
   be proven to satisfy, as predicates over the spec.
 - `src/examples.rs`: known answers, proven by evaluating the spec
   (`by (compute_only)`), on a toy curve and on P-384.
-
-Nothing here claims verification of any code. 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)).
+- `src/axioms.rs`, `src/field/`: the field arithmetic, described below.
+- `tests/field.rs`: known answers for the field, computed with Python.
+
+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)).
+
+## The field (modulo p and modulo n)
+
+A field element, `field::Fe`, is a residue modulo p (coordinates) or modulo n
+(scalars): six little-endian `u64` limbs in the Montgomery domain, with the
+invariant that their value is below the modulus. `Fe::val` is the residue
+they stand for.
+
+- **fiat-crypto =0.3.0 is a shipped dependency** (default features off, no
+  dependencies of its own, no `unsafe`). Its `p384_64` and `p384_scalar_64`
+  modules are Coq-synthesized Montgomery arithmetic. It cannot be vendored
+  under our lints (it indexes arrays and uses plain arithmetic), so it is
+  called, and trusted as a verified library: see the TCB in
+  [docs/VERIFICATION.md](../../docs/VERIFICATION.md).
+- **Six axioms**, in `src/axioms.rs`: `mul`, `add` and `sub` for each of the
+  two modules. Each is a thin `external_body` wrapper around one fiat
+  function whose `ensures` copies the postcondition fiat prints above it and
+  whose `requires` copies the printed precondition (an input below `m`). The
+  `Fe` invariant discharges that precondition at every call. Nothing else
+  about fiat is assumed, and a different session reviews the six.
+- **Proven over those axioms** (`src/field/fe.rs`, `lemmas.rs`, against
+  `field/contract.rs`): conversion into the Montgomery domain (`mul` by
+  `R^2 mod m`) and out of it (`mul` by 1); our own big-endian octet-string
+  conversions, with the range check as a limb comparison (`from_octets`
+  returns none unless the integer is below the modulus); equality; `pow` by
+  square-and-multiply over a 48-octet exponent against the spec's `pow_mod`;
+  and `inv`, `pow` with exponent `m - 2` and the check `a w ≡ 1`, against
+  the spec's `inv` (so `Some(w)` exactly when the spec's `inv` is, and
+  Fermat's little theorem is not used).
+- **Not used from fiat:** its `to_bytes`, `from_bytes`, `to_montgomery`,
+  `from_montgomery`, `nonzero`, `opp`, `square` and `divstep` (no axiom for
+  any of them).
+- **Not constant time, by design:** `pow` branches on the exponent's bits
+  (every input is public).
+- **Checked against Python:** `tests/field.rs` compares `add`, `sub`, `mul`,
+  `inv`, `pow` and the octet conversions with known answers for both moduli.
+  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).
 
 ## What it is, and what it is not
 
@@ -34,9 +73,10 @@ public, so nothing here has a constant-time requirement, and none is claimed.
 No signing, no private key.
 
 **The input is the digest**, 0 to 64 octets, not the message. Hashing is done
-by `clazel-crypto`, so this crate has **no axiom**. The key is the full
-97-octet ECPoint `04 || X || Y`; decoding and validation are inside the
-verified code (uncompressed form only; the compressed form is refused).
+by `clazel-crypto`, so the only axioms are the six field ones above. The key
+is the full 97-octet ECPoint `04 || X || Y`; decoding and validation are
+inside the verified code (uncompressed form only; the compressed form is
+refused).
 
 ## The spec's shape
 
@@ -74,13 +114,16 @@ 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`) and that the evaluated examples hold. `mutations.json` holds 26
-mutations of `spec.rs`, each killed with a certificate that contradicts one
-of those examples. There is no lemma about the spec, no independent
-transcription, no conformance test and no Kani harness yet, so the crate
-stays at tier 0; see
+`decreases`), that the evaluated examples hold, and that each field function
+meets its contract in `field/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
 [docs/VERIFICATION.md](../../docs/VERIFICATION.md) for what each tier
-requires.
+requires. `verify` is not written, so nothing here proves anything about
+ECDSA verification yet.
 
 ## Licence