diff --git a/Cargo.lock b/Cargo.lock index 9a3aea1..525825e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -281,6 +281,7 @@ dependencies = [ name = "clazel-p384" version = "0.0.0" dependencies = [ + "fiat-crypto", "vstd", ] @@ -498,6 +499,12 @@ version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "00d174d5400e5e8fd687ad1049e2f578285fa914201b1af7e8b112a4546bd826" +[[package]] +name = "fiat-crypto" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64cd1e32ddd350061ae6edb1b082d7c54915b5c672c389143b9a63403a109f24" + [[package]] name = "find-msvc-tools" version = "0.1.15" diff --git a/crates/clazel-p384/Cargo.toml b/crates/clazel-p384/Cargo.toml index 50a5059..740eaa3 100644 --- a/crates/clazel-p384/Cargo.toml +++ b/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 diff --git a/crates/clazel-p384/README.md b/crates/clazel-p384/README.md index 8f2f9b7..1a15f6b 100644 --- a/crates/clazel-p384/README.md +++ b/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 diff --git a/crates/clazel-p384/src/axioms.rs b/crates/clazel-p384/src/axioms.rs new file mode 100644 index 0000000..67ef558 --- /dev/null +++ b/crates/clazel-p384/src/axioms.rs @@ -0,0 +1,271 @@ +//! The trust boundary of the field: every call into fiat-crypto, each one +//! axiom. Six in all, `mul`, `add` and `sub` for each of `p384_64` (mod p) +//! and `p384_scalar_64` (mod n). +//! +//! Each wrapper is `external_body`. Verus takes its `ensures` on trust, and +//! the body is one call to one fiat function and nothing else: it wraps the +//! limb arrays in fiat's tuple structs, calls, and unwraps. The `ensures` +//! copies the postcondition that fiat prints above that function, in the +//! terms of `crate::field::spec`, and the `requires` copies the printed +//! precondition (inputs below `m`; the "unique saturated representation" is +//! the `[u64; 6]` type). That fiat-crypto's code meets its printed +//! postcondition is the Coq proof of `word_by_word_montgomery`, recorded in +//! the TCB (docs/VERIFICATION.md), and nothing else about fiat is assumed. +//! +//! **No wrapper checks its inputs at run time.** The precondition is a +//! `requires`, so Verus proves it at every call site; `field/fe.rs`'s +//! `Fe` type invariant (`value(limbs) < modulus`) is what discharges it. No +//! wrapper can be called with an argument whose precondition is not proven. +//! +//! There is no axiom for conversion into or out of the Montgomery domain, +//! for byte conversion, for `nonzero` or for `to_bytes`/`from_bytes`: the +//! first two are `mul` by R^2 and by 1 (`field/fe.rs`), and the octet +//! conversions are our own proven code. Inversion is `pow` over `mul`. +//! +//! These axioms are counted in the README table. A session other than the +//! one that wrote them reviews every change to this file +//! (docs/phases/phase-3.md 3.5f). + +#[allow(unused_imports)] +use vstd::prelude::*; + +use fiat_crypto::p384_64 as fiat_p; +use fiat_crypto::p384_scalar_64 as fiat_n; + +verus! { + +/// Multiplication modulo p on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_64.rs`, above `fiat_p384_mul`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::P)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::P, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_64::fiat_p384_mul` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn p_mul(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::P), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::P), + ensures + crate::field::spec::from_montgomery(crate::field::spec::Which::P, out@) + % crate::field::spec::modulus(crate::field::spec::Which::P) + == (crate::field::spec::from_montgomery(crate::field::spec::Which::P, a@) + * crate::field::spec::from_montgomery(crate::field::spec::Which::P, b@)) + % crate::field::spec::modulus(crate::field::spec::Which::P), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::P), +{ + let mut out = fiat_p::fiat_p384_montgomery_domain_field_element([0; 6]); + let a = fiat_p::fiat_p384_montgomery_domain_field_element(*a); + let b = fiat_p::fiat_p384_montgomery_domain_field_element(*b); + fiat_p::fiat_p384_mul(&mut out, &a, &b); + out.0 +} + +/// Addition modulo p on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_64.rs`, above `fiat_p384_add`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::P)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::P, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_64::fiat_p384_add` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn p_add(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::P), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::P), + ensures + crate::field::spec::from_montgomery(crate::field::spec::Which::P, out@) + % crate::field::spec::modulus(crate::field::spec::Which::P) + == (crate::field::spec::from_montgomery(crate::field::spec::Which::P, a@) + + crate::field::spec::from_montgomery(crate::field::spec::Which::P, b@)) + % crate::field::spec::modulus(crate::field::spec::Which::P), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::P), +{ + let mut out = fiat_p::fiat_p384_montgomery_domain_field_element([0; 6]); + let a = fiat_p::fiat_p384_montgomery_domain_field_element(*a); + let b = fiat_p::fiat_p384_montgomery_domain_field_element(*b); + fiat_p::fiat_p384_add(&mut out, &a, &b); + out.0 +} + +/// Subtraction modulo p on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_64.rs`, above `fiat_p384_sub`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::P)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::P, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_64::fiat_p384_sub` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn p_sub(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::P), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::P), + ensures + (crate::field::spec::from_montgomery(crate::field::spec::Which::P, out@) as int) + % (crate::field::spec::modulus(crate::field::spec::Which::P) as int) + == ((crate::field::spec::from_montgomery(crate::field::spec::Which::P, a@) as int) + - (crate::field::spec::from_montgomery(crate::field::spec::Which::P, b@) as int)) + % (crate::field::spec::modulus(crate::field::spec::Which::P) as int), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::P), +{ + let mut out = fiat_p::fiat_p384_montgomery_domain_field_element([0; 6]); + let a = fiat_p::fiat_p384_montgomery_domain_field_element(*a); + let b = fiat_p::fiat_p384_montgomery_domain_field_element(*b); + fiat_p::fiat_p384_sub(&mut out, &a, &b); + out.0 +} + +/// Multiplication modulo n on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_scalar_64.rs`, above `fiat_p384_scalar_mul`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::N)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::N, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_scalar_64::fiat_p384_scalar_mul` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn n_mul(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::N), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::N), + ensures + crate::field::spec::from_montgomery(crate::field::spec::Which::N, out@) + % crate::field::spec::modulus(crate::field::spec::Which::N) + == (crate::field::spec::from_montgomery(crate::field::spec::Which::N, a@) + * crate::field::spec::from_montgomery(crate::field::spec::Which::N, b@)) + % crate::field::spec::modulus(crate::field::spec::Which::N), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::N), +{ + let mut out = fiat_n::fiat_p384_scalar_montgomery_domain_field_element([0; 6]); + let a = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*a); + let b = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*b); + fiat_n::fiat_p384_scalar_mul(&mut out, &a, &b); + out.0 +} + +/// Addition modulo n on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_scalar_64.rs`, above `fiat_p384_scalar_add`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::N)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::N, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_scalar_64::fiat_p384_scalar_add` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn n_add(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::N), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::N), + ensures + crate::field::spec::from_montgomery(crate::field::spec::Which::N, out@) + % crate::field::spec::modulus(crate::field::spec::Which::N) + == (crate::field::spec::from_montgomery(crate::field::spec::Which::N, a@) + + crate::field::spec::from_montgomery(crate::field::spec::Which::N, b@)) + % crate::field::spec::modulus(crate::field::spec::Which::N), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::N), +{ + let mut out = fiat_n::fiat_p384_scalar_montgomery_domain_field_element([0; 6]); + let a = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*a); + let b = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*b); + fiat_n::fiat_p384_scalar_add(&mut out, &a, &b); + out.0 +} + +/// Subtraction modulo n on Montgomery-domain limbs. +/// +/// Fiat's printed conditions (`p384_scalar_64.rs`, above `fiat_p384_scalar_sub`): +/// +/// ```text +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// ``` +/// +/// Here `m` is `modulus(Which::N)`, `eval` is `value` and `eval +/// (from_montgomery z)` is `from_montgomery(Which::N, z)` (docs of +/// `crate::field::spec`, choices 1 to 3). Every limb is below 2^64 by its +/// type, which is fiat's "unique saturated representation". +// AXIOM: fiat-crypto =0.3.0 `p384_scalar_64::fiat_p384_scalar_sub` satisfies the Postconditions printed above it, +// given its Preconditions (Coq-proven word-by-word Montgomery code; see docs/VERIFICATION.md). +#[verifier::external_body] +pub fn n_sub(a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + crate::field::spec::value(a@) < crate::field::spec::modulus(crate::field::spec::Which::N), + crate::field::spec::value(b@) < crate::field::spec::modulus(crate::field::spec::Which::N), + ensures + (crate::field::spec::from_montgomery(crate::field::spec::Which::N, out@) as int) + % (crate::field::spec::modulus(crate::field::spec::Which::N) as int) + == ((crate::field::spec::from_montgomery(crate::field::spec::Which::N, a@) as int) + - (crate::field::spec::from_montgomery(crate::field::spec::Which::N, b@) as int)) + % (crate::field::spec::modulus(crate::field::spec::Which::N) as int), + crate::field::spec::value(out@) < crate::field::spec::modulus(crate::field::spec::Which::N), +{ + let mut out = fiat_n::fiat_p384_scalar_montgomery_domain_field_element([0; 6]); + let a = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*a); + let b = fiat_n::fiat_p384_scalar_montgomery_domain_field_element(*b); + fiat_n::fiat_p384_scalar_sub(&mut out, &a, &b); + out.0 +} + +} // verus! diff --git a/crates/clazel-p384/src/field/contract.rs b/crates/clazel-p384/src/field/contract.rs new file mode 100644 index 0000000..9c71afe --- /dev/null +++ b/crates/clazel-p384/src/field/contract.rs @@ -0,0 +1,94 @@ +//! What each executable field function is proven to satisfy. The arguments +//! are the residues the field elements stand for (`Fe::val`, in `[0, +//! modulus(w))`, by `Fe`'s type invariant) and octet strings, so these +//! predicates mention neither limbs nor Montgomery form: reviewing them and +//! [`crate::spec`] is enough to know what the field code guarantees. The +//! shapes (a predicate per function, named `_ensures`) are those of +//! `clazel-pkcs1`'s `contract.rs`. +//! +//! ```text +//! Fe::add(&self, &Fe) -> (r: Fe) ensures add_ensures(w, a.val(), b.val(), r.val()) +//! Fe::sub(&self, &Fe) -> (r: Fe) ensures sub_ensures(w, a.val(), b.val(), r.val()) +//! Fe::mul(&self, &Fe) -> (r: Fe) ensures mul_ensures(w, a.val(), b.val(), r.val()) +//! Fe::one(w) -> (r: Fe) ensures one_ensures(r.val()) +//! Fe::equals(&self, &Fe) -> (r: bool) ensures eq_ensures(a.val(), b.val(), r) +//! Fe::from_octets(w, &[u8; 48]) -> Option +//! ensures from_octets_ensures(w, o@, r.map(val)) +//! Fe::to_octets(&self) -> [u8; 48] ensures to_octets_ensures(a.val(), r@) +//! Fe::pow(&self, &[u8; 48]) -> Fe ensures pow_ensures(w, a.val(), e@, r.val()) +//! Fe::inv(&self) -> Option ensures inv_ensures(w, a.val(), r.map(val)) +//! ``` +//! +//! `w` is the modulus selector of both operands (`requires a.which() == +//! b.which()` where there are two). + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// `a + b` in GF(m): the residue of the sum. Fiat's `add`, "(eval a + eval b) +/// mod m", seen through the abstraction of [`super::spec`]. +pub open spec fn add_ensures(w: Which, a: nat, b: nat, r: nat) -> bool { + r == (a + b) % modulus(w) +} + +/// `a - b` in GF(m): [`crate::spec::fe_sub`], the spec's subtraction. +pub open spec fn sub_ensures(w: Which, a: nat, b: nat, r: nat) -> bool { + r == crate::spec::fe_sub(modulus(w), a, b) +} + +/// `a b` in GF(m): the residue of the product. +pub open spec fn mul_ensures(w: Which, a: nat, b: nat, r: nat) -> bool { + r == a * b % modulus(w) +} + +/// The element 1. +pub open spec fn one_ensures(r: nat) -> bool { + r == 1 +} + +/// Equality of residues. Two field elements are equal exactly when the +/// residues they stand for are. +pub open spec fn eq_ensures(a: nat, b: nat, r: bool) -> bool { + r == (a == b) +} + +/// SEC 1 §2.3.6 for a 48-octet string, and for either modulus: the octets +/// are read big-endian ([`crate::spec::os2ip`]) and the result is the +/// integer if it lies in `[0, m)`, and none otherwise. For `Which::P` this +/// is [`crate::spec::os2fe`] of `p384()` (`lemmas.rs`, `lemma_from_octets_os2fe`). +pub open spec fn from_octets_ensures(w: Which, o: Seq, r: Option) -> bool { + match r { + Some(x) => crate::spec::os2ip(o) < modulus(w) && x == crate::spec::os2ip(o), + None => crate::spec::os2ip(o) >= modulus(w), + } +} + +/// The 48 octets of the residue, big-endian: SEC 1 §2.3.5 (a field element +/// to an octet string, through the integer of §2.3.9 and the octet string of +/// §2.3.7), whose inverse is [`crate::spec::os2ip`], SEC 1 §2.3.8. +pub open spec fn to_octets_ensures(a: nat, out: Seq) -> bool { + out.len() == 48 && crate::spec::os2ip(out) == a +} + +/// `a^e mod m`, `e` the big-endian octets of the exponent: the spec's +/// [`crate::spec::pow_mod`]. +pub open spec fn pow_ensures(w: Which, a: nat, e: Seq, r: nat) -> bool { + r == crate::spec::pow_mod(a, crate::spec::os2ip(e), modulus(w)) +} + +/// `a⁻¹` in GF(m) is the spec's [`crate::spec::inv`]: `Some(w)` exactly when +/// `inv(m, a)` is, with the same `w`, and none exactly when it is none. In +/// particular `Some(w)` implies `a w ≡ 1`, and (FIPS 186-5 step 4, choice 3 +/// of `spec.rs`) none is returned for `a ≡ 0`. +pub open spec fn inv_ensures(w: Which, a: nat, r: Option) -> bool { + match r { + Some(x) => crate::spec::inv(modulus(w), a) == Some(x), + None => crate::spec::inv(modulus(w), a) is None, + } +} + +} // verus! diff --git a/crates/clazel-p384/src/field/fe.rs b/crates/clazel-p384/src/field/fe.rs new file mode 100644 index 0000000..fe373d9 --- /dev/null +++ b/crates/clazel-p384/src/field/fe.rs @@ -0,0 +1,812 @@ +//! The executable field: a residue modulo p or n as six Montgomery-domain +//! limbs, with arithmetic that calls fiat-crypto through the six axioms of +//! `crate::axioms` and is proven against [`super::contract`]. +//! +//! What is proven here, over those axioms and nothing else: +//! +//! - the conversion into the Montgomery domain (`mul` by `R^2 mod m`) and +//! out of it (`mul` by 1); +//! - our own octet-string conversions, big-endian, with the range check +//! (SEC 1 §2.3.6 step 1) as a limb comparison; +//! - `pow`, square-and-multiply from the most significant bit of a 48-octet +//! exponent, against [`crate::spec::pow_mod`]; +//! - `inv`: `pow` with exponent `m - 2` and the check `a w ≡ 1`, against +//! [`crate::spec::inv`]. +//! +//! No fiat byte function, no fiat conversion function and no fiat `nonzero` +//! is called: the axioms are `mul`, `add` and `sub`, and nothing else. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// A residue modulo p ([`Which::P`]) or n ([`Which::N`]). +/// +/// The limbs are the Montgomery form, little-endian, of a number below the +/// modulus (the type invariant, which is fiat's precondition `0 <= eval z < +/// m`). [`Fe::val`] is the residue they stand for. +pub struct Fe { + which: Which, + limbs: [u64; 6], +} + +impl Fe { + #[verifier::type_invariant] + spec fn well_formed(&self) -> bool { + value(self.limbs@) < modulus(self.which) + } + + /// Which modulus this element is a residue of. + pub closed spec fn which(&self) -> Which { + self.which + } + + /// The residue this element stands for: fiat's `eval (from_montgomery + /// limbs)`, a number in `[0, modulus(which))`. + pub closed spec fn val(&self) -> nat { + from_montgomery(self.which, 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) + ensures + self.val() < modulus(self.which()), + { + proof { + use_type_invariant(self); + super::lemmas::lemma_from_montgomery(self.which, self.limbs@); + } + } +} + +// --------------------------------------------------------------------- +// The six fiat operations, dispatched on the modulus. +// --------------------------------------------------------------------- + +/// Montgomery multiplication: fiat's `mul`, with the equation read off its +/// postcondition (`from_montgomery out` is already reduced). +fn raw_mul(w: Which, a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + value(a@) < modulus(w), + value(b@) < modulus(w), + ensures + value(out@) < modulus(w), + from_montgomery(w, out@) == from_montgomery(w, a@) * from_montgomery(w, b@) % modulus(w), +{ + let out = match w { + Which::P => crate::axioms::p_mul(a, b), + Which::N => crate::axioms::n_mul(a, b), + }; + proof { + super::lemmas::lemma_from_montgomery(w, out@); + vstd::arithmetic::div_mod::lemma_small_mod(from_montgomery(w, out@), modulus(w)); + } + out +} + +/// Addition: fiat's `add`. +fn raw_add(w: Which, a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + value(a@) < modulus(w), + value(b@) < modulus(w), + ensures + value(out@) < modulus(w), + from_montgomery(w, out@) == (from_montgomery(w, a@) + from_montgomery(w, b@)) % modulus( + w, + ), +{ + let out = match w { + Which::P => crate::axioms::p_add(a, b), + Which::N => crate::axioms::n_add(a, b), + }; + proof { + super::lemmas::lemma_from_montgomery(w, out@); + vstd::arithmetic::div_mod::lemma_small_mod(from_montgomery(w, out@), modulus(w)); + } + out +} + +/// Subtraction: fiat's `sub`, with its `(x - y) mod m` read as +/// [`crate::spec::fe_sub`]. +fn raw_sub(w: Which, a: &[u64; 6], b: &[u64; 6]) -> (out: [u64; 6]) + requires + value(a@) < modulus(w), + value(b@) < modulus(w), + ensures + value(out@) < modulus(w), + from_montgomery(w, out@) == crate::spec::fe_sub( + modulus(w), + from_montgomery(w, a@), + from_montgomery(w, b@), + ), +{ + let out = match w { + Which::P => crate::axioms::p_sub(a, b), + Which::N => crate::axioms::n_sub(a, b), + }; + proof { + super::lemmas::lemma_from_montgomery(w, out@); + super::lemmas::lemma_from_montgomery(w, a@); + super::lemmas::lemma_from_montgomery(w, b@); + super::lemmas::lemma_modulus(w); + super::lemmas::lemma_fe_sub(modulus(w), from_montgomery(w, a@), from_montgomery(w, b@)); + vstd::arithmetic::div_mod::lemma_small_mod(from_montgomery(w, out@), modulus(w)); + } + out +} + +// --------------------------------------------------------------------- +// Constants. +// --------------------------------------------------------------------- + +/// The limbs of the modulus. +fn modulus_limbs(w: Which) -> (r: [u64; 6]) + ensures + value(r@) == modulus(w), +{ + let r = match w { + Which::P => [ + 0xffff_ffffu64, + 0xffff_ffff_0000_0000, + 0xffff_ffff_ffff_fffe, + 0xffff_ffff_ffff_ffff, + 0xffff_ffff_ffff_ffff, + 0xffff_ffff_ffff_ffff, + ], + Which::N => [ + 0xecec_196a_ccc5_2973u64, + 0x581a_0db2_48b0_a77a, + 0xc763_4d81_f437_2ddf, + 0xffff_ffff_ffff_ffff, + 0xffff_ffff_ffff_ffff, + 0xffff_ffff_ffff_ffff, + ], + }; + proof { + super::lemmas::lemma_value6(r@); + match w { + Which::P => { + assert(modulus(Which::P) == 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_fffffffe_ffffffff_00000000_00000000_ffffffffnat) + by (compute_only); + }, + Which::N => { + assert(modulus(Which::N) == 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_c7634d81_f4372ddf_581a0db2_48b0a77a_ecec196a_ccc52973nat) + by (compute_only); + }, + } + } + r +} + +/// The limbs of `R^2 mod m`, which the conversion into the Montgomery domain +/// multiplies by. +fn r2_limbs(w: Which) -> (r: [u64; 6]) + ensures + value(r@) == radix() * radix() % modulus(w), + value(r@) < modulus(w), +{ + let r = match w { + Which::P => [ + 0xffff_fffe_0000_0001u64, + 0x2_0000_0000, + 0xffff_fffe_0000_0000, + 0x2_0000_0000, + 0x1, + 0x0, + ], + Which::N => [ + 0x2d31_9b24_19b4_09a9u64, + 0xff3d_81e5_df1a_a419, + 0xbc3e_483a_fcb8_2947, + 0xd40d_4917_4aab_1cc5, + 0x3fb0_5b7a_2826_6895, + 0x0c84_ee01_2b39_bf21, + ], + }; + proof { + super::lemmas::lemma_value6(r@); + super::lemmas::lemma_limb_pow_consts(); + match w { + Which::P => { + assert(radix() * radix() % modulus(Which::P) == 0x1_00000002_00000000_fffffffe_00000000_00000002_00000000_fffffffe_00000001nat) + by (compute_only); + assert(modulus(Which::P) == 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_fffffffe_ffffffff_00000000_00000000_ffffffffnat) + by (compute_only); + }, + Which::N => { + assert(radix() * radix() % modulus(Which::N) == 0x0c84ee01_2b39bf21_3fb05b7a_28266895_d40d4917_4aab1cc5_bc3e483a_fcb82947_ff3d81e5_df1aa419_2d319b24_19b409a9nat) + by (compute_only); + assert(modulus(Which::N) == 0xffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_c7634d81_f4372ddf_581a0db2_48b0a77a_ecec196a_ccc52973nat) + by (compute_only); + }, + } + } + r +} + +/// The exponent `m - 2` of Fermat's inverse, as 48 big-endian octets. +fn exponent_m_minus_2(w: Which) -> (e: [u8; 48]) + ensures + crate::spec::os2ip(e@) == modulus(w) - 2, +{ + let e = match w { + Which::P => [ + 0xffu8, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xfe, 0xff, 0xff, 0xff, 0xff, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, + 0x00, 0x00, 0xff, 0xff, 0xff, 0xfd, + ], + Which::N => [ + 0xffu8, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, + 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xc7, 0x63, 0x4d, 0x81, + 0xf4, 0x37, 0x2d, 0xdf, 0x58, 0x1a, 0x0d, 0xb2, 0x48, 0xb0, 0xa7, 0x7a, 0xec, 0xec, + 0x19, 0x6a, 0xcc, 0xc5, 0x29, 0x71, + ], + }; + proof { + super::lemmas::lemma_exponent(w); + match w { + Which::P => { + assert(e@ =~= super::lemmas::exponent_octets(Which::P)); + }, + Which::N => { + assert(e@ =~= super::lemmas::exponent_octets(Which::N)); + }, + } + } + e +} + +// --------------------------------------------------------------------- +// Montgomery-domain conversion, by `mul`. +// --------------------------------------------------------------------- + +impl Fe { + /// The residue `x`, for `x` the limbs of a number below the modulus (not + /// in Montgomery form): `mul(x, R^2 mod m)`, whose `from_montgomery` is + /// `x R^(-1) R^2 R^(-1) = x`. + fn from_raw(w: Which, x: &[u64; 6]) -> (r: Fe) + requires + value(x@) < modulus(w), + ensures + r.which() == w, + r.val() == value(x@), + { + let r2 = r2_limbs(w); + let out = raw_mul(w, x, &r2); + proof { + super::lemmas::lemma_modulus(w); + super::lemmas::lemma_rinv(w); + super::lemmas::lemma_from_montgomery(w, x@); + super::lemmas::lemma_from_montgomery(w, r2@); + // r2 = R^2 mod m is below m, so it is its own residue. + vstd::arithmetic::div_mod::lemma_small_mod(value(r2@), modulus(w)); + super::lemmas::lemma_to_mont( + modulus(w), + radix(), + super::lemmas::rinv(w), + value(r2@), + value(x@), + ); + vstd::arithmetic::div_mod::lemma_small_mod(value(x@), modulus(w)); + } + Fe { which: w, limbs: out } + } + + /// The limbs of the residue itself, not in Montgomery form: `mul(self, + /// 1)`. Fiat's `mul` leaves `value(out) R^(-1) = a R^(-1) R^(-1)`, so + /// `value(out) = a R^(-1)`, which is below the modulus. + fn to_raw(&self) -> (raw: [u64; 6]) + ensures + value(raw@) == self.val(), + { + proof { + use_type_invariant(self); + } + let one = [1u64, 0, 0, 0, 0, 0]; + proof { + super::lemmas::lemma_value6(one@); + super::lemmas::lemma_modulus(self.which); + } + let out = raw_mul(self.which, &self.limbs, &one); + proof { + let w = self.which; + let m = modulus(w); + let r = super::lemmas::rinv(w); + let x = from_montgomery(w, self.limbs@); + super::lemmas::lemma_modulus(w); + super::lemmas::lemma_rinv(w); + super::lemmas::lemma_from_montgomery(w, self.limbs@); + super::lemmas::lemma_from_montgomery(w, one@); + super::lemmas::lemma_from_montgomery(w, out@); + assert(value(one@) == 1); + // value(out) r = x (1 r) = x r (mod m) + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(x as int, (1 * r) as int, m as int); + super::lemmas::lemma_cancel(m, radix(), r, value(out@), x); + vstd::arithmetic::div_mod::lemma_small_mod(value(out@), m); + vstd::arithmetic::div_mod::lemma_small_mod(x, m); + } + out + } + + /// The element 1. + pub fn one(w: Which) -> (r: Fe) + ensures + r.which() == w, + super::contract::one_ensures(r.val()), + { + let one = [1u64, 0, 0, 0, 0, 0]; + proof { + super::lemmas::lemma_value6(one@); + super::lemmas::lemma_modulus(w); + } + Fe::from_raw(w, &one) + } +} + +// --------------------------------------------------------------------- +// Field operations. +// --------------------------------------------------------------------- + +impl Fe { + /// `self + other`. + pub fn add(&self, other: &Fe) -> (r: Fe) + requires + self.which() == other.which(), + ensures + r.which() == self.which(), + super::contract::add_ensures(self.which(), self.val(), other.val(), r.val()), + { + proof { + use_type_invariant(self); + use_type_invariant(other); + } + let out = raw_add(self.which, &self.limbs, &other.limbs); + Fe { which: self.which, limbs: out } + } + + /// `self - other`. + pub fn sub(&self, other: &Fe) -> (r: Fe) + requires + self.which() == other.which(), + ensures + r.which() == self.which(), + super::contract::sub_ensures(self.which(), self.val(), other.val(), r.val()), + { + proof { + use_type_invariant(self); + use_type_invariant(other); + } + let out = raw_sub(self.which, &self.limbs, &other.limbs); + Fe { which: self.which, limbs: out } + } + + /// `self * other`. + pub fn mul(&self, other: &Fe) -> (r: Fe) + requires + self.which() == other.which(), + ensures + r.which() == self.which(), + super::contract::mul_ensures(self.which(), self.val(), other.val(), r.val()), + { + proof { + use_type_invariant(self); + use_type_invariant(other); + } + let out = raw_mul(self.which, &self.limbs, &other.limbs); + Fe { which: self.which, limbs: out } + } + + /// Whether `self` and `other` are the same residue. The Montgomery form + /// of a residue below the modulus is unique (`from_montgomery` is + /// injective on numbers below the modulus), so this compares limbs. + pub fn equals(&self, other: &Fe) -> (r: bool) + requires + self.which() == other.which(), + ensures + super::contract::eq_ensures(self.val(), other.val(), r), + { + proof { + use_type_invariant(self); + use_type_invariant(other); + } + let r = self.limbs[0] == other.limbs[0] && self.limbs[1] == other.limbs[1] + && self.limbs[2] == other.limbs[2] && self.limbs[3] == other.limbs[3] + && self.limbs[4] == other.limbs[4] && self.limbs[5] == other.limbs[5]; + proof { + let w = self.which; + let m = modulus(w); + super::lemmas::lemma_modulus(w); + super::lemmas::lemma_rinv(w); + super::lemmas::lemma_from_montgomery(w, self.limbs@); + super::lemmas::lemma_from_montgomery(w, other.limbs@); + if r { + assert(self.limbs@ =~= other.limbs@); + } + if self.val() == other.val() { + // value(a) r = value(b) r (mod m), so value(a) = value(b) + // (both are below m), so the limbs are equal. + super::lemmas::lemma_cancel( + m, + radix(), + super::lemmas::rinv(w), + value(self.limbs@), + value(other.limbs@), + ); + vstd::arithmetic::div_mod::lemma_small_mod(value(self.limbs@), m); + vstd::arithmetic::div_mod::lemma_small_mod(value(other.limbs@), m); + super::lemmas::lemma_value_inj(self.limbs@, other.limbs@); + assert(r); + } + } + r + } +} + +// --------------------------------------------------------------------- +// Octet strings. +// --------------------------------------------------------------------- + +/// `a < b` as numbers, comparing from the most significant limb. +fn lt6(a: &[u64; 6], b: &[u64; 6]) -> (r: bool) + ensures + r == (value(a@) < value(b@)), +{ + proof { + super::lemmas::lemma_value6(a@); + super::lemmas::lemma_value6(b@); + } + if a[5] != b[5] { + return a[5] < b[5]; + } + if a[4] != b[4] { + return a[4] < b[4]; + } + if a[3] != b[3] { + return a[3] < b[3]; + } + if a[2] != b[2] { + return a[2] < b[2]; + } + if a[1] != b[1] { + return a[1] < b[1]; + } + a[0] < b[0] +} + +/// The eight octets `o[start..start + 8]` as a big-endian integer. +fn load_be64(o: &[u8; 48], start: usize) -> (v: u64) + requires + start <= 40, + ensures + v as nat == crate::spec::os2ip(o@.subrange(start as int, start as int + 8)), +{ + let mut v: u64 = 0; + let mut j: usize = 0; + proof { + assert(o@.subrange(start as int, start as int) =~= Seq::::empty()); + } + while j < 8 + invariant + j <= 8, + start <= 40, + v as nat == crate::spec::os2ip(o@.subrange(start as int, start as int + j as int)), + decreases 8 - j, + { + let idx = start.saturating_add(j); + let x: u8 = match o.get(idx) { + Some(b) => *b, + None => 0, + }; + proof { + let pre = o@.subrange(start as int, start as int + j as int); + super::lemmas::lemma_os2ip_push(pre, x); + super::lemmas::lemma_os2ip_below_2_56(pre); + assert(o@.subrange(start as int, start as int + j as int + 1) =~= pre.push(x)); + } + // Never saturates: the octets so far are below 2^56. + v = v.saturating_mul(256).saturating_add(x as u64); + j = j.saturating_add(1); + } + v +} + +/// The 48 octets as six limbs, least significant first: SEC 1 §2.3.8 +/// () step 1, `x = Σ 2^(8 (mlen - 1 - i)) +/// M_i`, the first octet the most significant. +fn load_limbs(o: &[u8; 48]) -> (l: [u64; 6]) + ensures + value(l@) == crate::spec::os2ip(o@), +{ + let l0 = load_be64(o, 40); + let l1 = load_be64(o, 32); + let l2 = load_be64(o, 24); + let l3 = load_be64(o, 16); + let l4 = load_be64(o, 8); + let l5 = load_be64(o, 0); + let l = [l0, l1, l2, l3, l4, l5]; + proof { + super::lemmas::lemma_os2ip_chunks(o@); + super::lemmas::lemma_value6(l@); + } + l +} + +/// The eight octets of a limb, big-endian. +fn store_be64(x: u64) -> (r: [u8; 8]) + ensures + crate::spec::os2ip(r@) == x as nat, +{ + let d1 = x / 256; + let d2 = d1 / 256; + let d3 = d2 / 256; + let d4 = d3 / 256; + let d5 = d4 / 256; + let d6 = d5 / 256; + let d7 = d6 / 256; + let r = [ + d7 as u8, + (d6 % 256) as u8, + (d5 % 256) as u8, + (d4 % 256) as u8, + (d3 % 256) as u8, + (d2 % 256) as u8, + (d1 % 256) as u8, + (x % 256) as u8, + ]; + proof { + super::lemmas::lemma_os2ip8(r@); + } + r +} + +/// The six limbs as 48 octets, most significant first: the inverse of SEC 1 +/// §2.3.8 step 1, that is SEC 1 §2.3.7 (Integer-to-Octet-String) with `mlen = +/// 48`. +fn store_limbs(l: &[u64; 6]) -> (o: [u8; 48]) + ensures + o@.len() == 48, + crate::spec::os2ip(o@) == value(l@), +{ + let c5 = store_be64(l[5]); + let c4 = store_be64(l[4]); + let c3 = store_be64(l[3]); + let c2 = store_be64(l[2]); + let c1 = store_be64(l[1]); + let c0 = store_be64(l[0]); + let o = [ + c5[0], c5[1], c5[2], c5[3], c5[4], c5[5], c5[6], c5[7], c4[0], c4[1], c4[2], c4[3], c4[4], + c4[5], c4[6], c4[7], c3[0], c3[1], c3[2], c3[3], c3[4], c3[5], c3[6], c3[7], c2[0], c2[1], + c2[2], c2[3], c2[4], c2[5], c2[6], c2[7], c1[0], c1[1], c1[2], c1[3], c1[4], c1[5], c1[6], + c1[7], c0[0], c0[1], c0[2], c0[3], c0[4], c0[5], c0[6], c0[7], + ]; + proof { + super::lemmas::lemma_os2ip_chunks(o@); + super::lemmas::lemma_value6(l@); + assert(o@.subrange(0, 8) =~= c5@); + assert(o@.subrange(8, 16) =~= c4@); + assert(o@.subrange(16, 24) =~= c3@); + assert(o@.subrange(24, 32) =~= c2@); + assert(o@.subrange(32, 40) =~= c1@); + assert(o@.subrange(40, 48) =~= c0@); + } + o +} + +impl Fe { + /// SEC 1 §2.3.6: the residue whose big-endian octets are `o`, if that + /// integer is below the modulus (step 1: "Output 'invalid' and stop if a + /// does not lie in the interval [0, m - 1]"), and none otherwise. + pub fn from_octets(w: Which, o: &[u8; 48]) -> (r: Option) + ensures + match r { + Some(f) => f.which() == w && super::contract::from_octets_ensures( + w, + o@, + Some(f.val()), + ), + None => super::contract::from_octets_ensures(w, o@, None), + }, + { + let limbs = load_limbs(o); + let m = modulus_limbs(w); + if lt6(&limbs, &m) { + Some(Fe::from_raw(w, &limbs)) + } else { + None + } + } + + /// The 48 octets of the residue, big-endian: SEC 1 §2.3.5 + /// (Field-Element-to-Octet-String), whose step 1 (§2.3.9) is the identity + /// for an odd prime (SP 800-186 F.1) and whose step 2 is §2.3.7. + pub fn to_octets(&self) -> (r: [u8; 48]) + ensures + super::contract::to_octets_ensures(self.val(), r@), + { + let raw = self.to_raw(); + store_limbs(&raw) + } +} + +// --------------------------------------------------------------------- +// Exponentiation and inversion. +// --------------------------------------------------------------------- + +/// A bit as a number. +spec fn bit_nat(b: bool) -> nat { + if b { + 1 + } else { + 0 + } +} + +/// Take the bit worth `t` off `rem`: whether `rem >= t`, and `rem` without it. +fn split_bit(rem: u8, t: u8) -> (r: (bool, u8)) + ensures + r.0 == (rem >= t), + rem as nat == r.1 as nat + (if r.0 { + t as nat + } else { + 0nat + }), + r.1 <= rem, +{ + if rem >= t { + (true, rem.wrapping_sub(t)) + } else { + (false, rem) + } +} + +/// One step of square-and-multiply: `acc^2`, times `a` if `bit`. +fn pow_step(a: &Fe, acc: &Fe, bit: bool, Ghost(q): Ghost) -> (r: Fe) + requires + a.which() == acc.which(), + acc.val() == crate::spec::pow_mod(a.val(), q, modulus(a.which())), + ensures + r.which() == a.which(), + r.val() == crate::spec::pow_mod(a.val(), 2 * q + bit_nat(bit), modulus(a.which())), +{ + a.val_lt_modulus(); + proof { + super::lemmas::lemma_modulus(a.which()); + super::lemmas::lemma_pow_mod_step(a.val(), q, bit, modulus(a.which())); + vstd::arithmetic::div_mod::lemma_small_mod(a.val(), modulus(a.which())); + } + let sq = acc.mul(acc); + if bit { + sq.mul(a) + } else { + sq + } +} + +/// Eight steps of square-and-multiply, one per bit of `byte`, most +/// significant first: `acc^256 a^byte`. +fn pow_byte(a: &Fe, acc: &Fe, byte: u8, Ghost(q): Ghost) -> (r: Fe) + requires + a.which() == acc.which(), + acc.val() == crate::spec::pow_mod(a.val(), q, modulus(a.which())), + ensures + r.which() == a.which(), + r.val() == crate::spec::pow_mod(a.val(), q * 256 + byte as nat, modulus(a.which())), +{ + let (b7, rem) = split_bit(byte, 128); + let acc = pow_step(a, acc, b7, Ghost(q)); + let ghost q1: nat = 2 * q + bit_nat(b7); + let (b6, rem) = split_bit(rem, 64); + let acc = pow_step(a, &acc, b6, Ghost(q1)); + let ghost q2: nat = 2 * q1 + bit_nat(b6); + let (b5, rem) = split_bit(rem, 32); + let acc = pow_step(a, &acc, b5, Ghost(q2)); + let ghost q3: nat = 2 * q2 + bit_nat(b5); + let (b4, rem) = split_bit(rem, 16); + let acc = pow_step(a, &acc, b4, Ghost(q3)); + let ghost q4: nat = 2 * q3 + bit_nat(b4); + let (b3, rem) = split_bit(rem, 8); + let acc = pow_step(a, &acc, b3, Ghost(q4)); + let ghost q5: nat = 2 * q4 + bit_nat(b3); + let (b2, rem) = split_bit(rem, 4); + let acc = pow_step(a, &acc, b2, Ghost(q5)); + let ghost q6: nat = 2 * q5 + bit_nat(b2); + let (b1, rem) = split_bit(rem, 2); + let acc = pow_step(a, &acc, b1, Ghost(q6)); + let ghost q7: nat = 2 * q6 + bit_nat(b1); + let last = split_bit(rem, 1); + let b0 = last.0; + let acc = pow_step(a, &acc, b0, Ghost(q7)); + proof { + // rem is now 0, and byte = 128 b7 + 64 b6 + ... + b0. + assert(last.1 == 0); + assert(2 * q7 + bit_nat(b0) == q * 256 + byte as nat); + } + acc +} + +impl Fe { + /// `self^e` for the exponent `e` given as 48 big-endian octets. + pub fn pow(&self, e: &[u8; 48]) -> (r: Fe) + ensures + r.which() == self.which(), + super::contract::pow_ensures(self.which(), self.val(), e@, r.val()), + { + let mut acc = Fe::one(self.which); + let mut i: usize = 0; + let ghost mut q: nat = 0; + proof { + super::lemmas::lemma_modulus(self.which); + assert(e@.subrange(0, 0) =~= Seq::::empty()); + assert(crate::spec::pow_mod(self.val(), 0, modulus(self.which)) == 1nat % modulus( + self.which, + )); + vstd::arithmetic::div_mod::lemma_small_mod(1nat, modulus(self.which)); + } + while i < 48 + invariant + i <= 48, + acc.which() == self.which(), + q == crate::spec::os2ip(e@.subrange(0, i as int)), + acc.val() == crate::spec::pow_mod(self.val(), q, modulus(self.which())), + decreases 48 - i, + { + let byte: u8 = match e.get(i) { + Some(b) => *b, + None => 0, + }; + let next = pow_byte(self, &acc, byte, Ghost(q)); + proof { + let pre = e@.subrange(0, i as int); + super::lemmas::lemma_os2ip_push(pre, byte); + assert(e@.subrange(0, i as int + 1) =~= pre.push(byte)); + q = q * 256 + byte as nat; + } + acc = next; + i = i.saturating_add(1); + } + proof { + assert(e@.subrange(0, 48) =~= e@); + } + acc + } + + /// `self^(-1)`: `self^(m - 2)`, accepted only if `self * self^(m - 2)` + /// is 1. This is the spec's `inv`; FIPS 186-5 §6.4.2 step 4 says "using + /// the routine in Appendix B.1", and B.1 allows any algorithm with an + /// equivalent result (choice 3 of `crate::spec`). + pub fn inv(&self) -> (r: Option) + ensures + match r { + Some(f) => f.which() == self.which() && super::contract::inv_ensures( + self.which(), + self.val(), + Some(f.val()), + ), + None => super::contract::inv_ensures(self.which(), self.val(), None), + }, + { + let w = self.which; + let e = exponent_m_minus_2(w); + let x = self.pow(&e); + let chk = self.mul(&x); + let one = Fe::one(w); + let ok = chk.equals(&one); + self.val_lt_modulus(); + proof { + super::lemmas::lemma_modulus(w); + vstd::arithmetic::div_mod::lemma_small_mod(self.val(), modulus(w)); + } + if ok { + Some(x) + } else { + None + } + } +} + +} // verus! diff --git a/crates/clazel-p384/src/field/lemmas.rs b/crates/clazel-p384/src/field/lemmas.rs new file mode 100644 index 0000000..14cd5e7 --- /dev/null +++ b/crates/clazel-p384/src/field/lemmas.rs @@ -0,0 +1,592 @@ +//! Facts the executable field code is proven from: about the spec's +//! constants, about `value`, and the modular arithmetic of Montgomery form. +//! Everything here is proven, none is assumed. + +#[allow(unused_imports)] +use super::spec::*; +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +// --------------------------------------------------------------------- +// The constants. +// --------------------------------------------------------------------- + +/// `R^(-1) mod m` as a number: `((2^64)⁻¹ mod m)^6 mod m`, the factor that +/// fiat's `from_montgomery` multiplies by. +pub open spec fn rinv(w: Which) -> nat { + match w { + Which::P => 0x00000014_00000014_0000000c_00000002_fffffffc_fffffffa_fffffffb_fffffffd_ffffffeb_ffffffd8_ffffffe1_00000006nat, + Which::N => 0x355ca87d_e39dbb1f_a150206c_e4f194ac_78d4ba58_66d61787_e29f9fb7_0a9da219_d26d4aeb_a664edb0_610ae855_f2c0d911nat, + } +} + +/// `limb_pow` at the arguments the code uses, as numerals. +pub proof fn lemma_limb_pow_consts() + ensures + limb_pow(0) == 1, + limb_pow(1) == 0x1_0000_0000_0000_0000nat, + limb_pow(2) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000nat, + limb_pow(3) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat, + limb_pow(4) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat, + limb_pow(5) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat, + limb_pow(6) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat, +{ + assert(limb_pow(1) == 0x1_0000_0000_0000_0000nat) by (compute_only); + assert(limb_pow(2) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000nat) by (compute_only); + assert(limb_pow(3) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat) by (compute_only); + assert(limb_pow(4) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat) by (compute_only); + assert(limb_pow(5) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat) by (compute_only); + assert(limb_pow(6) == 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat) by (compute_only); +} + +/// The moduli are odd numbers between 2 and `R = 2^384`. +pub proof fn lemma_modulus(w: Which) + ensures + 2 < modulus(w) < radix(), + modulus(w) % 2 == 1, +{ + lemma_limb_pow_consts(); + match w { + Which::P => { + assert(modulus(Which::P) == crate::spec::p384().p); + assert(2 < crate::spec::p384().p < limb_pow(6) && crate::spec::p384().p % 2 == 1) by (compute_only); + }, + Which::N => { + assert(2 < crate::spec::p384().n < limb_pow(6) && crate::spec::p384().n % 2 == 1) by (compute_only); + }, + } +} + +/// `(2^64)⁻¹ mod m` is an inverse of `2^64`, below `m`, and `rinv` is its +/// sixth power, which inverts `R`. +pub proof fn lemma_rinv(w: Which) + ensures + base_inv(w) < modulus(w), + base() * base_inv(w) % modulus(w) == 1, + rinv(w) < modulus(w), + (base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w)) % modulus(w) == rinv(w), + radix() * rinv(w) % modulus(w) == 1, +{ + match w { + Which::P => { + assert(base_inv(Which::P) < modulus(Which::P) + && base() * base_inv(Which::P) % modulus(Which::P) == 1 + && rinv(Which::P) < modulus(Which::P) + && (base_inv(Which::P) * base_inv(Which::P) * base_inv(Which::P) * base_inv(Which::P) * base_inv(Which::P) * base_inv(Which::P)) % modulus(Which::P) == rinv(Which::P) + && radix() * rinv(Which::P) % modulus(Which::P) == 1) by (compute_only); + }, + Which::N => { + assert(base_inv(Which::N) < modulus(Which::N) + && base() * base_inv(Which::N) % modulus(Which::N) == 1 + && rinv(Which::N) < modulus(Which::N) + && (base_inv(Which::N) * base_inv(Which::N) * base_inv(Which::N) * base_inv(Which::N) * base_inv(Which::N) * base_inv(Which::N)) % modulus(Which::N) == rinv(Which::N) + && radix() * rinv(Which::N) % modulus(Which::N) == 1) by (compute_only); + }, + } +} + +/// `from_montgomery` multiplies by `rinv` (fiat's `((2^64)⁻¹ mod m)^6`, reduced). +pub proof fn lemma_from_montgomery(w: Which, z: Seq) + ensures + from_montgomery(w, z) == value(z) * rinv(w) % modulus(w), + from_montgomery(w, z) < modulus(w), +{ + lemma_modulus(w); + lemma_rinv(w); + let q = base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w); + let m = modulus(w); + // value * q % m == value * (q % m) % m + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(value(z) as int, q as int, m as int); + vstd::arithmetic::div_mod::lemma_mod_bound(value(z) as int * q as int, m as int); +} + +// --------------------------------------------------------------------- +// Modular arithmetic of Montgomery form, on abstract numbers: `m` the +// modulus, `rr` the radix `R` and `r` its inverse, `rr * r ≡ 1 (mod m)`. +// --------------------------------------------------------------------- + +/// `x r R ≡ x`. +proof fn lemma_unit(m: nat, rr: nat, r: nat, x: nat) + requires + m > 0, + rr * r % m == 1, + ensures + (x * r) * rr % m == x % m, +{ + assert((x * r) * rr == x * (rr * r)) by (nonlinear_arith); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(x as int, (rr * r) as int, m as int); + assert(x * ((rr * r) % m) == x * 1); +} + +/// Multiplying by `r` can be undone: `x r ≡ y r` gives `x ≡ y`. +pub proof fn lemma_cancel(m: nat, rr: nat, r: nat, x: nat, y: nat) + requires + m > 0, + rr * r % m == 1, + x * r % m == y * r % m, + ensures + x % m == y % m, +{ + lemma_unit(m, rr, r, x); + lemma_unit(m, rr, r, y); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left((x * r) as int, rr as int, m as int); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left((y * r) as int, rr as int, m as int); +} + +/// Into the Montgomery domain: multiplying `x` (as a Montgomery-domain +/// number) by `R^2 mod m` stands for `x`: `(x r)(r2 r) ≡ x` when `r2 ≡ R R`. +pub proof fn lemma_to_mont(m: nat, rr: nat, r: nat, r2: nat, x: nat) + requires + m > 0, + rr * r % m == 1, + r2 % m == (rr * rr) % m, + ensures + ((x * r % m) * (r2 * r % m)) % m == x % m, +{ + let t = rr * r; + vstd::arithmetic::div_mod::lemma_mul_mod_noop((x * r) as int, (r2 * r) as int, m as int); + // (x r)(r2 r) = (x r r) r2 + assert((x * r) * (r2 * r) == (x * r * r) * r2) by (nonlinear_arith); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right((x * r * r) as int, r2 as int, m as int); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right((x * r * r) as int, (rr * rr) as int, m as int); + // (x r r)(R R) = x (R r)(R r) + assert((x * r * r) * (rr * rr) == x * ((rr * r) * (rr * r))) by (nonlinear_arith); + vstd::arithmetic::div_mod::lemma_mul_mod_noop(t as int, t as int, m as int); + assert(t * t % m == 1) by { + assert((t % m) * (t % m) == 1); + vstd::arithmetic::div_mod::lemma_small_mod(1nat, m); + } + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(x as int, (t * t) as int, m as int); + assert(x * ((t * t) % m) == x * 1); +} + +/// The Montgomery form of `x` stands for `x`: `(x R mod m) r ≡ x`. +pub proof fn lemma_mont_inv(m: nat, rr: nat, r: nat, x: nat) + requires + m > 0, + rr * r % m == 1, + ensures + (x * rr % m) * r % m == x % m, +{ + vstd::arithmetic::div_mod::lemma_mul_mod_noop_left((x * rr) as int, r as int, m as int); + assert((x * rr) * r == x * (rr * r)) by (nonlinear_arith); + vstd::arithmetic::div_mod::lemma_mul_mod_noop_right(x as int, (rr * r) as int, m as int); + assert(x * ((rr * r) % m) == x * 1); +} + +/// `mont(x)` stands for `x`: for `x < m`, `from_montgomery` of any limbs of +/// value `mont(x)` is `x`. +pub proof fn lemma_mont_roundtrip(w: Which, z: Seq, x: nat) + requires + x < modulus(w), + value(z) == mont(w, x), + ensures + from_montgomery(w, z) == x, +{ + lemma_modulus(w); + lemma_rinv(w); + lemma_from_montgomery(w, z); + lemma_mont_inv(modulus(w), radix(), rinv(w), x); + vstd::arithmetic::div_mod::lemma_small_mod(x, modulus(w)); +} + +// --------------------------------------------------------------------- +// Limb sequences. +// --------------------------------------------------------------------- + +/// A sequence of `n` limbs is below `base^n`. +pub proof fn lemma_value_bound(s: Seq) + ensures + value(s) < limb_pow(s.len()), + decreases s.len(), +{ + if s.len() > 0 { + let d = s.drop_last(); + lemma_value_bound(d); + let p = limb_pow(d.len()); + let l = s.last() as nat; + assert(limb_pow(s.len()) == p * base()); + assert(value(s) == value(d) + l * p); + assert(value(s) < p * base()) by (nonlinear_arith) + requires + value(d) < p, + l < base(), + value(s) == value(d) + l * p, + ; + } +} + +/// `limb_pow` is positive. +pub proof fn lemma_limb_pow_pos(i: nat) + ensures + limb_pow(i) > 0, + decreases i, +{ + if i > 0 { + lemma_limb_pow_pos((i - 1) as nat); + assert(limb_pow((i - 1) as nat) * base() > 0) by (nonlinear_arith) + requires + limb_pow((i - 1) as nat) > 0, + base() > 0, + ; + } +} + +/// Six limbs, written out: the sum fiat's header calls `eval`. +pub proof fn lemma_value6(s: Seq) + requires + s.len() == 6, + ensures + value(s) == s[0] + s[1] * 0x1_0000_0000_0000_0000nat + s[2] * 0x1_0000_0000_0000_0000_0000_0000_0000_0000nat + s[3] * 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat + s[4] * 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat + s[5] * 0x1_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000_0000nat, + value(s) < radix(), +{ + lemma_limb_pow_consts(); + lemma_value_bound(s); + let s5 = s.drop_last(); + let s4 = s5.drop_last(); + let s3 = s4.drop_last(); + let s2 = s3.drop_last(); + let s1 = s2.drop_last(); + let s0 = s1.drop_last(); + assert(s5.len() == 5 && s4.len() == 4 && s3.len() == 3 && s2.len() == 2 && s1.len() == 1 + && s0.len() == 0); + assert(s.last() == s[5] && s5.last() == s[4] && s4.last() == s[3] && s3.last() == s[2] + && s2.last() == s[1] && s1.last() == s[0]); + assert(value(s) == value(s5) + s[5] * limb_pow(5)); + assert(value(s5) == value(s4) + s[4] * limb_pow(4)); + assert(value(s4) == value(s3) + s[3] * limb_pow(3)); + assert(value(s3) == value(s2) + s[2] * limb_pow(2)); + assert(value(s2) == value(s1) + s[1] * limb_pow(1)); + assert(value(s1) == value(s0) + s[0] * limb_pow(0)); + assert(value(s0) == 0); +} + +/// One limb and the rest: `v1 + l1 p = v2 + l2 p` with `v1, v2 < p` gives +/// `l1 = l2` and `v1 = v2`. +proof fn lemma_digit_split(p: nat, v1: nat, l1: nat, v2: nat, l2: nat) + requires + p > 0, + v1 < p, + v2 < p, + v1 + l1 * p == v2 + l2 * p, + ensures + l1 == l2, + v1 == v2, +{ + vstd::arithmetic::div_mod::lemma_fundamental_div_mod_converse( + (v1 + l1 * p) as int, + p as int, + l1 as int, + v1 as int, + ); + vstd::arithmetic::div_mod::lemma_fundamental_div_mod_converse( + (v2 + l2 * p) as int, + p as int, + l2 as int, + v2 as int, + ); +} + +/// Limb sequences of one length with one value are one sequence. +pub proof fn lemma_value_inj(a: Seq, b: Seq) + requires + a.len() == b.len(), + value(a) == value(b), + ensures + a =~= b, + decreases a.len(), +{ + if a.len() > 0 { + let da = a.drop_last(); + let db = b.drop_last(); + lemma_value_bound(da); + lemma_value_bound(db); + lemma_limb_pow_pos(da.len()); + lemma_digit_split( + limb_pow(da.len()), + value(da), + a.last() as nat, + value(db), + b.last() as nat, + ); + lemma_value_inj(da, db); + assert(a =~= da.push(a.last())); + assert(b =~= db.push(b.last())); + } +} + +// --------------------------------------------------------------------- +// Octet strings. +// --------------------------------------------------------------------- + +/// `256^n`. +pub open spec fn pow256(n: nat) -> nat + decreases n, +{ + if n == 0 { + 1 + } else { + pow256((n - 1) as nat) * 256 + } +} + +/// Appending an octet is Horner's step. +pub proof fn lemma_os2ip_push(s: Seq, b: u8) + ensures + crate::spec::os2ip(s.push(b)) == crate::spec::os2ip(s) * 256 + b as nat, +{ + assert(s.push(b).drop_last() =~= s); +} + +/// An octet string of `n` octets is below `256^n`. +pub proof fn lemma_os2ip_bound(s: Seq) + ensures + crate::spec::os2ip(s) < pow256(s.len()), + decreases s.len(), +{ + if s.len() > 0 { + let d = s.drop_last(); + lemma_os2ip_bound(d); + let p = pow256(d.len()); + let x = crate::spec::os2ip(d); + let l = s.last() as nat; + assert(crate::spec::os2ip(s) == x * 256 + l); + assert(pow256(s.len()) == p * 256); + assert(x * 256 + l < p * 256) by (nonlinear_arith) + requires + x < p, + l < 256, + ; + } +} + +/// `256^8` is the limb radix. +pub proof fn lemma_pow256_8() + ensures + pow256(8) == base(), +{ + reveal_with_fuel(pow256, 9); +} + +/// `256^i <= 256^j` for `i <= j`. +pub proof fn lemma_pow256_mono(i: nat, j: nat) + requires + i <= j, + ensures + pow256(i) <= pow256(j), + decreases j, +{ + if i < j { + lemma_pow256_mono(i, (j - 1) as nat); + } +} + +/// Concatenation: `os2ip(a || b) = os2ip(a) 256^|b| + os2ip(b)`. +pub proof fn lemma_os2ip_concat(a: Seq, b: Seq) + ensures + crate::spec::os2ip(a + b) == crate::spec::os2ip(a) * pow256(b.len()) + crate::spec::os2ip( + b, + ), + decreases b.len(), +{ + if b.len() == 0 { + assert(a + b =~= a); + assert(pow256(0) == 1); + assert(crate::spec::os2ip(b) == 0); + assert(crate::spec::os2ip(a) * 1 == crate::spec::os2ip(a)); + } else { + let bd = b.drop_last(); + lemma_os2ip_concat(a, bd); + assert((a + b).drop_last() =~= a + bd); + assert((a + b).last() == b.last()); + let x = crate::spec::os2ip(a); + let y = crate::spec::os2ip(bd); + let p = pow256(bd.len()); + let l = b.last() as nat; + assert(pow256(b.len()) == p * 256); + assert(crate::spec::os2ip(a + b) == crate::spec::os2ip(a + bd) * 256 + l); + assert(crate::spec::os2ip(b) == y * 256 + l); + assert(crate::spec::os2ip(a + bd) == x * p + y); + assert(crate::spec::os2ip(a + b) == (x * p + y) * 256 + l); + assert((x * p + y) * 256 + l == x * (p * 256) + (y * 256 + l)) by (nonlinear_arith); + assert(crate::spec::os2ip(a) * pow256(b.len()) == x * (p * 256)); + } +} + +/// Forty-eight octets as six chunks of eight, each chunk a limb's worth +/// (Horner's rule with radix `2^64`). +pub proof fn lemma_os2ip_chunks(s: Seq) + requires + s.len() == 48, + ensures + crate::spec::os2ip(s) == (((((crate::spec::os2ip(s.subrange(0, 8)) * 0x1_0000_0000_0000_0000nat + + crate::spec::os2ip(s.subrange(8, 16))) * 0x1_0000_0000_0000_0000nat + crate::spec::os2ip( + s.subrange(16, 24), + )) * 0x1_0000_0000_0000_0000nat + crate::spec::os2ip(s.subrange(24, 32))) * 0x1_0000_0000_0000_0000nat + crate::spec::os2ip( + s.subrange(32, 40), + )) * 0x1_0000_0000_0000_0000nat + crate::spec::os2ip(s.subrange(40, 48))), +{ + lemma_pow256_8(); + let c0 = s.subrange(0, 8); + let c1 = s.subrange(8, 16); + let c2 = s.subrange(16, 24); + let c3 = s.subrange(24, 32); + let c4 = s.subrange(32, 40); + let c5 = s.subrange(40, 48); + let s2 = c0 + c1; + let s3 = s2 + c2; + let s4 = s3 + c3; + let s5 = s4 + c4; + assert(s5 + c5 =~= s); + lemma_os2ip_concat(s5, c5); + lemma_os2ip_concat(s4, c4); + lemma_os2ip_concat(s3, c3); + lemma_os2ip_concat(s2, c2); + lemma_os2ip_concat(c0, c1); +} + +/// The first `k + 1` octets are the first `k` and octet `k`. +pub proof fn lemma_os2ip_take(s: Seq, k: int) + requires + 0 <= k < s.len(), + ensures + crate::spec::os2ip(s.take(k + 1)) == crate::spec::os2ip(s.take(k)) * 256 + s[k] as nat, +{ + lemma_os2ip_push(s.take(k), s[k]); + assert(s.take(k + 1) =~= s.take(k).push(s[k])); +} + +/// Eight octets, written out (Horner's rule with radix 256). +pub proof fn lemma_os2ip8(s: Seq) + requires + s.len() == 8, + ensures + crate::spec::os2ip(s) == ((((((s[0] as nat * 256 + s[1] as nat) * 256 + s[2] as nat) * 256 + + s[3] as nat) * 256 + s[4] as nat) * 256 + s[5] as nat) * 256 + s[6] as nat) * 256 + + s[7] as nat, +{ + lemma_os2ip_take(s, 0); + lemma_os2ip_take(s, 1); + lemma_os2ip_take(s, 2); + lemma_os2ip_take(s, 3); + lemma_os2ip_take(s, 4); + lemma_os2ip_take(s, 5); + lemma_os2ip_take(s, 6); + lemma_os2ip_take(s, 7); + assert(s.take(0) =~= Seq::::empty()); + assert(s.take(8) =~= s); +} + +/// Seven octets are below `2^56`, so a limb built from them can take +/// another octet. +pub proof fn lemma_os2ip_below_2_56(s: Seq) + requires + s.len() <= 7, + ensures + crate::spec::os2ip(s) * 256 + 255 < 0x1_0000_0000_0000_0000nat, +{ + lemma_os2ip_bound(s); + lemma_pow256_mono(s.len(), 7); + reveal_with_fuel(pow256, 8); + assert(pow256(7) == 0x100_0000_0000_0000nat); +} + +/// For `Which::P`, `from_octets_ensures` is SEC 1 §2.3.6 (`os2fe`). +pub proof fn lemma_from_octets_os2fe(o: Seq, r: Option) + requires + super::contract::from_octets_ensures(Which::P, o, r), + ensures + r == crate::spec::os2fe(crate::spec::p384(), o), +{ +} + +// --------------------------------------------------------------------- +// The spec's residue arithmetic. +// --------------------------------------------------------------------- + +/// Fiat's `(x - y) mod m` (mathematical modulus) is the spec's `fe_sub`. +pub proof fn lemma_fe_sub(m: nat, x: nat, y: nat) + requires + m > 0, + x < m, + y < m, + ensures + (x as int - y as int) % (m as int) == crate::spec::fe_sub(m, x, y) as int, +{ + vstd::arithmetic::div_mod::lemma_small_mod(x, m); + vstd::arithmetic::div_mod::lemma_small_mod(y, m); + vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(x as int - y as int, m as int); + assert((m as int + (x as int - y as int)) == (x % m + m - y % m) as int); +} + +/// One bit of square-and-multiply: `pow_mod(a, 2q + bit) = pow_mod(a, q)^2` +/// times `a` if the bit is set. +pub proof fn lemma_pow_mod_step(a: nat, q: nat, bit: bool, m: nat) + requires + m > 1, + ensures + crate::spec::pow_mod(a, 2 * q + (if bit { 1nat } else { 0nat }), m) == (if bit { + (crate::spec::pow_mod(a, q, m) * crate::spec::pow_mod(a, q, m) % m) * (a % m) % m + } else { + crate::spec::pow_mod(a, q, m) * crate::spec::pow_mod(a, q, m) % m + }), +{ + let e = 2 * q + (if bit { 1nat } else { 0nat }); + let h = crate::spec::pow_mod(a, q, m); + if e == 0 { + // q = 0 and the bit is clear: pow_mod(a, 0) = 1 % m, and 1 % m + // squared is 1 % m. + assert(q == 0 && !bit); + assert(crate::spec::pow_mod(a, 0, m) == 1nat % m); + vstd::arithmetic::div_mod::lemma_small_mod(1nat, m); + assert(h == 1); + assert(crate::spec::pow_mod(a, e, m) == 1nat % m); + assert(h * h == 1) by (nonlinear_arith) + requires + h == 1, + ; + assert(h * h % m == 1); + } else { + assert(e / 2 == q); + assert(e % 2 == (if bit { 1nat } else { 0nat })); + assert(crate::spec::pow_mod(a, e, m) == (if e % 2 == 0 { + h * h % m + } else { + (h * h % m) * (a % m) % m + })); + } +} + +// --------------------------------------------------------------------- +// The exponent of Fermat's inverse. +// --------------------------------------------------------------------- + +/// The octets of `m - 2`, big-endian, for the exponent of the inverse. +pub open spec fn exponent_octets(w: Which) -> Seq { + match w { + Which::P => seq![0xffu8, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xfe, 0xff, 0xff, 0xff, 0xff, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xff, 0xff, 0xff, 0xfd], + Which::N => seq![0xffu8, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xc7, 0x63, 0x4d, 0x81, 0xf4, 0x37, 0x2d, 0xdf, 0x58, 0x1a, 0x0d, 0xb2, 0x48, 0xb0, 0xa7, 0x7a, 0xec, 0xec, 0x19, 0x6a, 0xcc, 0xc5, 0x29, 0x71], + } +} + +/// `exponent_octets` is 48 octets and is `m - 2`. +pub proof fn lemma_exponent(w: Which) + ensures + exponent_octets(w).len() == 48, + crate::spec::os2ip(exponent_octets(w)) == modulus(w) - 2, +{ + match w { + Which::P => { + assert(exponent_octets(Which::P).len() == 48 && crate::spec::os2ip(exponent_octets(Which::P)) + == modulus(Which::P) - 2) by (compute_only); + }, + Which::N => { + assert(exponent_octets(Which::N).len() == 48 && crate::spec::os2ip(exponent_octets(Which::N)) + == modulus(Which::N) - 2) by (compute_only); + }, + } +} + +} // verus! diff --git a/crates/clazel-p384/src/field/mod.rs b/crates/clazel-p384/src/field/mod.rs new file mode 100644 index 0000000..bdbde7a --- /dev/null +++ b/crates/clazel-p384/src/field/mod.rs @@ -0,0 +1,21 @@ +//! Field arithmetic modulo p (coordinates) and modulo n (scalars) for NIST +//! P-384, over fiat-crypto's generated Montgomery code. +//! +//! - [`spec`]: what a field element is: six little-endian `u64` limbs in the +//! Montgomery domain, and the number they stand for. This is the part to +//! review against fiat-crypto's printed pre- and postconditions. +//! - [`contract`]: what each executable field function is proven to satisfy, +//! as predicates over residues and octet strings (the vocabulary of +//! [`crate::spec`]). +//! - [`fe`]: the executable field element [`Fe`] and its operations, proven +//! against the contracts over the six axioms of [`crate::axioms`]. +//! - [`lemmas`]: the facts those proofs use (about the spec's constants, +//! limb sequences, octet strings and modular arithmetic). + +pub mod contract; +pub mod fe; +pub mod lemmas; +pub mod spec; + +pub use fe::Fe; +pub use spec::Which; diff --git a/crates/clazel-p384/src/field/spec.rs b/crates/clazel-p384/src/field/spec.rs new file mode 100644 index 0000000..454769b --- /dev/null +++ b/crates/clazel-p384/src/field/spec.rs @@ -0,0 +1,130 @@ +//! What a field element is: a Montgomery-domain limb array, and the residue +//! it stands for. The vocabulary of fiat-crypto's printed conditions. +//! +//! # Source (pinned) +//! +//! **fiat-crypto 0.3.0** (crates.io, `Cargo.lock` checksum +//! `64cd1e32ddd350061ae6edb1b082d7c54915b5c672c389143b9a63403a109f24`), +//! generated by `word_by_word_montgomery`: +//! +//! - `src/p384_64.rs`, SHA-256 +//! `2dab86b68de2533016b4226f029f82951393819bad0956cff97e33e754a74765`: the +//! field GF(p), `m = 0xfff...fffeffffffff0000000000000000ffffffff` +//! (printed in its header, equal to `2^384 - 2^128 - 2^96 + 2^32 - 1`); +//! - `src/p384_scalar_64.rs`, SHA-256 +//! `df99d668d71d98640aad16bea65354f6a511ee0a24891f439ae4be0165164a06`: the +//! integers mod n, `m = 0xfff...fffc7634d81f4372ddf581a0db248b0a77aecec196accc52973` +//! (printed in its header, equal to n). +//! +//! The two files have the same shape. Each function documents, above its +//! signature, a `Preconditions` and a `Postconditions` block; those blocks +//! are what `axioms.rs` copies. This file gives their words a meaning. +//! +//! # Modelling choices +//! +//! 1. **`eval` is [`value`].** Fiat's header defines `eval z = z[0] + (z[1] +//! << 64) + ... + (z[5] << 0x140)`. [`value`] is the same sum for a +//! sequence of any length (as `clazel-pkcs1`'s bignum `value`), and a +//! field element is a sequence of exactly 6 limbs, each below 2^64 by its +//! type. That is fiat's "unique saturated representation" ("the input is +//! in the unique saturated representation"); the only other requirement +//! its blocks print is `eval z < m`. +//! 2. **`m` is [`modulus`]**: the `p` or the `n` of [`crate::spec::p384`], +//! not a second copy of the constant. That it is the number fiat's header +//! prints as `m` was compared digit by digit with a script when this file +//! was written; fiat's `m` is a comment, so no proof can check it, and +//! `tests/field.rs` checks it indirectly (arithmetic modulo it agrees with +//! Python's). +//! 3. **`from_montgomery` is [`from_montgomery`].** Fiat's `mul`, `add` and +//! `sub` are stated through `eval (from_montgomery z)`, where +//! `from_montgomery` is fiat's own function, whose printed postcondition +//! is `eval out mod m = (eval z * ((2^64)⁻¹ mod m)^6) mod m` and `0 <= eval +//! out < m`. So `eval (from_montgomery z)` is that residue, in `[0, m)`. +//! The spec writes it as fiat does, with `(2^64)⁻¹ mod m` a number +//! ([`base_inv`], one literal per modulus). Writing the inverse as a +//! literal needs no primality; that it is an inverse is a ground fact +//! (`lemmas.rs`, `lemma_rinv`). +//! 4. **The residue a limb array stands for** is its `from_montgomery`. With +//! `R = 2^384`, [`mont`]`(x) = x R mod m` is the Montgomery form of `x`, +//! and `from_montgomery(mont(x)) = x` (`lemmas.rs`, `lemma_mont_roundtrip`). +//! The code never needs `mont` itself: it converts by fiat's `mul` (by +//! `R^2 mod m` and by 1). +//! 5. **Subtraction** is `(x - y) mod m` for the residues `x` and `y`, the +//! mathematical modulus, which is [`crate::spec::fe_sub`]. + +#[allow(unused_imports)] +use vstd::prelude::*; + +verus! { + +/// Which of fiat's two generated modules: `p384_64` (the field GF(p), for +/// coordinates) or `p384_scalar_64` (the integers mod n, for scalars). +#[derive(Clone, Copy, PartialEq, Eq)] +pub enum Which { + /// Arithmetic mod p, fiat's `p384_64`. + P, + /// Arithmetic mod n, fiat's `p384_scalar_64`. + N, +} + +/// Fiat's `m`: p for [`Which::P`], n for [`Which::N`] (choice 2). +pub open spec fn modulus(w: Which) -> nat { + match w { + Which::P => crate::spec::p384().p, + Which::N => crate::spec::p384().n, + } +} + +/// The radix of a limb, 2^64. +pub open spec fn base() -> nat { + 0x1_0000_0000_0000_0000nat +} + +/// `base()^i`, the weight of limb `i`. +pub open spec fn limb_pow(i: nat) -> nat + decreases i, +{ + if i == 0 { + 1 + } else { + limb_pow((i - 1) as nat) * base() + } +} + +/// Fiat's `eval` (choice 1): `z[0] + z[1] 2^64 + z[2] 2^128 + ...`. +pub open spec fn value(z: Seq) -> nat + decreases z.len(), +{ + if z.len() == 0 { + 0 + } else { + value(z.drop_last()) + (z.last() as nat) * limb_pow((z.len() - 1) as nat) + } +} + +/// `R = 2^384`, the Montgomery radix of six 64-bit limbs. +pub open spec fn radix() -> nat { + limb_pow(6) +} + +/// `(2^64)⁻¹ mod m` as a number in `[0, m)` (choice 3). +pub open spec fn base_inv(w: Which) -> nat { + match w { + Which::P => 0x00000001_00000000_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_ffffffff_fffffffe_fffffffd_ffffffff_00000001nat, + Which::N => 0x6ed46089_e88fdc44_ffffffff_ffffffff_ffffffff_ffffffff_e77db430_c4555788_7cd47351_23d969cd_0432fa0c_a03b08afnat, + } +} + +/// Fiat's `eval (from_montgomery z)` (choice 3): `(eval z * ((2^64)⁻¹ mod +/// m)^6) mod m`, which is in `[0, m)`. +pub open spec fn from_montgomery(w: Which, z: Seq) -> nat { + value(z) * (base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w) * base_inv(w)) + % modulus(w) +} + +/// The Montgomery form of the residue `x` (choice 4): `x R mod m`. +pub open spec fn mont(w: Which, x: nat) -> nat { + x * radix() % modulus(w) +} + +} // verus! diff --git a/crates/clazel-p384/src/lib.rs b/crates/clazel-p384/src/lib.rs index 42e4007..e64f716 100644 --- a/crates/clazel-p384/src/lib.rs +++ b/crates/clazel-p384/src/lib.rs @@ -1,10 +1,11 @@ //! ECDSA signature verification over NIST P-384, FIPS 186-5 §6.4.2. //! -//! **Specification only so far.** This crate has no executable code: no -//! field arithmetic, no point code and no `verify` function exist yet. What -//! is here is the part a person reviews, the meaning of "a valid ECDSA -//! P-384 signature", written in Verus, and the contract the later -//! implementation must meet. +//! **Specification and field arithmetic so far.** There is no point code +//! and no `verify` function yet. What is here is the part a person reviews, +//! the meaning of "a valid ECDSA P-384 signature", written in Verus, the +//! contract the later implementation must meet, and the field arithmetic +//! modulo p and n: fiat-crypto's Montgomery code behind six axioms, with the +//! rest (conversions, octet strings, `pow`, `inv`) proven over them. //! //! This is public-key *verification* only: the key, the signature and the //! digest are all public, so there is no constant-time requirement and no @@ -17,10 +18,14 @@ //! toy curve for evaluated examples. //! - [`contract`]: what the executable `verify` will be proven to satisfy. //! - [`examples`]: known answers, proven by evaluating the spec. +//! - [`field`]: the field arithmetic, over fiat-crypto, with its contracts. +//! - [`axioms`]: the six calls into fiat-crypto, each an axiom. //! - [`certificates`]: the host module for mutation kill certificates //! (empty until `mutations.json` exists). +pub mod axioms; pub mod certificates; pub mod contract; pub mod examples; +pub mod field; pub mod spec; diff --git a/crates/clazel-p384/tests/field.rs b/crates/clazel-p384/tests/field.rs new file mode 100644 index 0000000..f15817e --- /dev/null +++ b/crates/clazel-p384/tests/field.rs @@ -0,0 +1,622 @@ +//! Field arithmetic (`clazel_p384::field`) against known answers. +//! +//! Every expected value below was computed with Python 3 integers +//! (`(a + b) % m`, `a * b % m`, `pow(a, -1, m)`, `pow(a, e, m)`), not with +//! this crate or fiat-crypto. The inputs are P-384's base point +//! coordinates (SP 800-186 §3.2.1.4) and small or boundary values, for both +//! moduli. All values are 48 octets, big-endian, as 96 hexadecimal digits. +//! +//! The proofs show the field functions meet `field/contract.rs` over six +//! axioms that state fiat-crypto's printed postconditions; these tests are +//! the independent check on those axioms and on the constants in `spec.rs` +//! (that fiat's `m` is p and n, and that its Montgomery domain is the one +//! the code assumes). + +use clazel_p384::field::{Fe, Which}; + +type TestResult = Result<(), String>; + +fn octets(hex: &str) -> Result<[u8; 48], String> { + let digits = hex.as_bytes(); + if digits.len() != 96 { + return Err(format!("{} hex digits, want 96", digits.len())); + } + let mut out = [0u8; 48]; + for (slot, pair) in out.iter_mut().zip(digits.chunks(2)) { + let pair = std::str::from_utf8(pair).map_err(|e| e.to_string())?; + *slot = u8::from_str_radix(pair, 16).map_err(|e| format!("{pair}: {e}"))?; + } + Ok(out) +} + +fn hex(o: &[u8; 48]) -> String { + o.iter().map(|b| format!("{b:02x}")).collect() +} + +fn elem(w: Which, hex: &str) -> Result { + Fe::from_octets(w, &octets(hex)?).ok_or_else(|| format!("{hex} was refused")) +} + +fn same(f: &Fe, expect: &str) -> TestResult { + let got = hex(&f.to_octets()); + if got == expect { + Ok(()) + } else { + Err(format!("got {got}, want {expect}")) + } +} + +fn named(w: Which) -> &'static str { + match w { + Which::P => "p", + Which::N => "n", + } +} + +/// Binary operations: `(a, b, a + b, a - b, a * b)` modulo p. +const BINARY_P: &[(&str, &str, &str, &str, &str)] = &[ + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "e09fa86d54b131a6ec505fde85b3899e6711591fb441b01543d172f43844e2f85f63a42bdcd3ab09b4977bb503601916", + "746febd82864d8c831132e5f608dd14a75291da5630d871b701d10cccc6371784aa2408fa1d6a7cec01140bbe18bfc58", + "332e559389c970313cb29c4b55af5783821971a99c250daf84dc5d3cc441cb0a482e90de9d3ccd96b3c8c48b2ad3f025", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "e09fa86d54b131a6ec505fde85b3899e6711591fb441b01543d172f43844e2f85f63a42bdcd3ab09b4977bb503601916", + "8b901427d79b2737ceecd1a09f722eb58ad6e25a9cf278e48fe2ef33339c8e86b55dbf6f5e2958313feebf451e7403a7", + "332e559389c970313cb29c4b55af5783821971a99c250daf84dc5d3cc441cb0a482e90de9d3ccd96b3c8c48b2ad3f025", + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "abab0f8a4836d3268fd50c867ccc7b636f4080ca155369875b1a87480bfff827562637c54900f75b3b77a39ffc21d8a6", + "569b7b44cb20c8b772717e48968b207a93060a04fe043256a72c03870757a3b5ac205308ca56a482c6cee7301735c337", + "5f493ac6c23d5d581f526ddd722c90d72931e9fc1f3518e8695a688e14dc6b6424c2fa7740139e4eb626418d6d335eed", + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffb", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000004", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), +]; + +/// Inverses: `(a, a^-1 or none)` modulo p. +const INVERSE_P: &[(&str, Option<&str>)] = &[ + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + None, + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + Some( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + Some( + "7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7fffffff800000000000000080000000", + ), + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + Some( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + ), + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + Some( + "7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7fffffff80000000000000007fffffff", + ), + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + Some( + "1ce18121749aa29a393faddf4e55522af8c67dabdfa413aac45da5c5f0781147133e1c96ca2a8234440fbf89e7e96410", + ), + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + Some( + "9eee8231a5913c8aac5a8f03b92fee93f6d05a5777cb0bf87063909e7e5682f7a26736b36031e4006ecf009e5f9c8231", + ), + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + Some( + "083ba7221f8540bce4baa0d81a28cd3a9cd5fda67bd6eacf37bcee804c2e7a83953328d6fdb7499c7a3679d32aec85a7", + ), + ), +]; + +/// Powers: `(a, e, a^e)` modulo p, `e` also 48 octets. +const POWER_P: &[(&str, &str, &str)] = &[ + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "046af925fa51ac496728217df5bc7c1fc3353aca34a380e1ffd8419fe7b13f6a92e8614fee38a288e2222412aca8b019", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010001", + "8be4f5f04eb6f8dd47bacdb4bdbaa5d645906f972413e32f27854253e3b3dd7104f0a7748db0d2fca2dd2297545ac094", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "9eee8231a5913c8aac5a8f03b92fee93f6d05a5777cb0bf87063909e7e5682f7a26736b36031e4006ecf009e5f9c8231", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "6d2588c497808712d6ddb0bccfa7c5bbdea4947e8b014335a6fc80d42c46cf26d22a7fd8366812b09d0027a62c8848e5", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "0f7ab66865508d65dd41b1dbcc104f7cfb6b19188236ea7315ba8a86ef07bcc8a216fd6963428a0365bd81b0a0fc4022", + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "1951c767fbd507d75dfcdd0ab00c04ce5e9f8c840b62a913637f975804279291b82f84bf0735488baa9f6d05cc6cef4b", + ), +]; + +/// Octet strings of p that are residues, and ones that are not. +const IN_RANGE_P: &[&str] = &[ + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffd", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", +]; +const OUT_OF_RANGE_P: &[&str] = &[ + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff000000000000000100000000", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000100000000ffffffff", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", +]; + +/// Binary operations: `(a, b, a + b, a - b, a * b)` modulo n. +const BINARY_N: &[(&str, &str, &str, &str, &str)] = &[ + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "e09fa86d54b131a6ec505fde85b3899e6711591fb441b01543d172f43844e2f85f63a42bdcd3ab09b4977bb503601916", + "746febd82864d8c831132e5f608dd14a75291da5630d871b701d10cccc6371784aa2408fa1d6a7cec01140bbe18bfc58", + "2a8e172f52ea8a3f1864714efafb6588d0ed2fc509e9b4502bdd369bdbeeb9019f58804fbe958008223ba8752ead1f2c", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "e09fa86d54b131a6ec505fde85b3899e6711591fb441b01543d172f43844e2f85f63a42bdcd3ab09b4977bb503601916", + "8b901427d79b2737ceecd1a09f722eb58ad6e25a9cf278e457463cb527d3bc670d77cd22a6d9ffac2cdad8aeeb392d1b", + "2a8e172f52ea8a3f1864714efafb6588d0ed2fc509e9b4502bdd369bdbeeb9019f58804fbe958008223ba8752ead1f2c", + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "abab0f8a4836d3268fd50c867ccc7b636f4080ca155369875b1a87480bfff827562637c54900f75b3b77a39ffc21d8a6", + "569b7b44cb20c8b772717e48968b207a93060a04fe0432566e8f5108fb8ed196043a60bc13074bfdb3bb0099e3faecab", + "f08ef28044c2bdaf8ddc2192b5cc753040ed1aa5298de782dde9d083376e1963df48de687b5dd8e9f9535ded3d5f646a", + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc5296f", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000004", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), +]; + +/// Inverses: `(a, a^-1 or none)` modulo n. +const INVERSE_N: &[(&str, Option<&str>)] = &[ + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + None, + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + Some( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + Some( + "7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efac0d06d9245853bd76760cb5666294ba", + ), + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + Some( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + ), + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + Some( + "7fffffffffffffffffffffffffffffffffffffffffffffffe3b1a6c0fa1b96efac0d06d9245853bd76760cb5666294b9", + ), + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + Some( + "c0345088d98aa2f119e693230bbfb7a15f02792e7267cb55b3b0da1cb38a1c5d5f05c8d102d5128f524604074c4c8846", + ), + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + Some( + "195089baf8f5f0aff5c30a6cbde5b89a548ed7f739d253a675186a655eb60fe5e7973625ab399512e7a68c6b1bc8c167", + ), + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + Some( + "46ae825365df7a1d62825d81fa487fc38308db2cd6f56ceb22e631917f150eb006e8baeef59facc741d22ac15aad230b", + ), + ), +]; + +/// Powers: `(a, e, a^e)` modulo n, `e` also 48 octets. +const POWER_N: &[(&str, &str, &str)] = &[ + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "a067a4d6fd10d2108a2d4649446529d5501f3734e9d5075a68178b74a7fb933b79d068c4f3d6e8585115c859fd9c0bc3", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010001", + "86970749f08da887bd258aa6157760202526bd6275c5c393748c139aedc22ff58ee3fd0e4711f8ede5fd57ed73fc8829", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "195089baf8f5f0aff5c30a6cbde5b89a548ed7f739d253a675186a655eb60fe5e7973625ab399512e7a68c6b1bc8c167", + ), + ( + "3617de4a96262c6f5d9e98bf9292dc29f8f41dbd289a147ce9da3113b5f0b8c00a60b1ce1d7e819d7a431d7c90ea0e5f", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "89cb315840a564fc1a7bdefc1d2c84f6afada827883d396e812a65c2c2a8b87239d53ba024b3f5a98bcf81839f72e558", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + ), + ( + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + ), + ( + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "51851b3973f5614cee410b803872239260684ee82effe90e9cea8f1b9d52761671bc824bec54e198a0b9dc974b59cb84", + ), + ( + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", + "5cc922b0883daf1711b0da1e33bb3154cb48799d3c77ccd77a957c5a7ddc436db68e3ce6fab6ac4d37e74c8a8b43b4e7", + ), +]; + +/// Octet strings of n that are residues, and ones that are not. +const IN_RANGE_N: &[&str] = &[ + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52972", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52971", + "aa87ca22be8b05378eb1c71ef320ad746e1d3b628ba79b9859f741e082542a385502f25dbf55296c3a545e3872760ab7", + "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef", +]; +const OUT_OF_RANGE_N: &[&str] = &[ + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52974", + "ffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77becec196accc52973", + "ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe", + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe", +]; + +/// One modulus and its known answers. +struct Table { + which: Which, + binary: &'static [( + &'static str, + &'static str, + &'static str, + &'static str, + &'static str, + )], + inverse: &'static [(&'static str, Option<&'static str>)], + power: &'static [(&'static str, &'static str, &'static str)], + in_range: &'static [&'static str], + out_of_range: &'static [&'static str], +} + +const TABLES: [Table; 2] = [ + Table { + which: Which::P, + binary: BINARY_P, + inverse: INVERSE_P, + power: POWER_P, + in_range: IN_RANGE_P, + out_of_range: OUT_OF_RANGE_P, + }, + Table { + which: Which::N, + binary: BINARY_N, + inverse: INVERSE_N, + power: POWER_N, + in_range: IN_RANGE_N, + out_of_range: OUT_OF_RANGE_N, + }, +]; + +#[test] +fn add_sub_mul_known_answers() -> TestResult { + for t in &TABLES { + let w = t.which; + for &(a, b, sum, diff, prod) in t.binary { + let (x, y) = (elem(w, a)?, elem(w, b)?); + same(&x.add(&y), sum).map_err(|e| format!("mod {}: {a} + {b}: {e}", named(w)))?; + same(&x.sub(&y), diff).map_err(|e| format!("mod {}: {a} - {b}: {e}", named(w)))?; + same(&x.mul(&y), prod).map_err(|e| format!("mod {}: {a} * {b}: {e}", named(w)))?; + } + } + Ok(()) +} + +#[test] +#[cfg_attr(miri, ignore = "each inverse is 768 field multiplications")] +fn inverse_known_answers() -> TestResult { + for t in &TABLES { + let w = t.which; + for &(a, expect) in t.inverse { + let x = elem(w, a)?; + match (x.inv(), expect) { + (Some(got), Some(want)) => { + same(&got, want).map_err(|e| format!("mod {}: inv {a}: {e}", named(w)))?; + if !x.mul(&got).equals(&Fe::one(w)) { + return Err(format!("mod {}: {a} * inv {a} is not 1", named(w))); + } + } + (None, None) => {} + (Some(_), None) => return Err(format!("mod {}: inv {a} should be none", named(w))), + (None, Some(_)) => return Err(format!("mod {}: inv {a} should exist", named(w))), + } + } + } + Ok(()) +} + +/// The three inverses the task names: of 1, of 2 and of m - 1, spelled out. +#[test] +#[cfg_attr(miri, ignore = "each inverse is 768 field multiplications")] +fn inverse_of_one_two_and_minus_one() -> TestResult { + let tail = |last: &str| format!("{}{last}", "0".repeat(94)); + for t in &TABLES { + let w = t.which; + let one = elem(w, &tail("01"))?; + let two = elem(w, &tail("02"))?; + same(&one.inv().ok_or("inv 1")?, &tail("01"))?; + // inv 2 = (m + 1) / 2, so 2 * inv 2 = 1. + let half = two.inv().ok_or("inv 2")?; + if !two.mul(&half).equals(&one) { + return Err(format!("mod {}: 2 * inv 2 is not 1", named(w))); + } + // m - 1 = 1 - 2 is its own inverse: (-1)(-1) = 1. + let minus_one = one.sub(&two); + same( + &minus_one.inv().ok_or("inv -1")?, + &hex(&minus_one.to_octets()), + )?; + } + Ok(()) +} + +#[test] +#[cfg_attr(miri, ignore = "each power is up to 768 field multiplications")] +fn pow_known_answers() -> TestResult { + for t in &TABLES { + let w = t.which; + for &(a, e, expect) in t.power { + let got = elem(w, a)?.pow(&octets(e)?); + same(&got, expect).map_err(|err| format!("mod {}: {a} ^ {e}: {err}", named(w)))?; + } + } + Ok(()) +} + +#[test] +fn octets_round_trip_and_the_range_check() -> TestResult { + for t in &TABLES { + let w = t.which; + for &h in t.in_range { + same(&elem(w, h)?, h).map_err(|e| format!("mod {}: round trip {h}: {e}", named(w)))?; + } + for &h in t.out_of_range { + if Fe::from_octets(w, &octets(h)?).is_some() { + return Err(format!("mod {}: {h} is not below the modulus", named(w))); + } + } + } + Ok(()) +} + +#[test] +fn p_minus_one_is_a_residue_mod_p_but_not_mod_n() -> TestResult { + let p_minus_1 = "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000fffffffe"; + if Fe::from_octets(Which::P, &octets(p_minus_1)?).is_none() { + return Err("p - 1 should be a residue mod p".into()); + } + if Fe::from_octets(Which::N, &octets(p_minus_1)?).is_some() { + return Err("p - 1 is above n".into()); + } + Ok(()) +} + +#[test] +fn one_and_equality() -> TestResult { + for t in &TABLES { + let w = t.which; + same(&Fe::one(w), &format!("{}01", "0".repeat(94)))?; + for &(a, b, ..) in t.binary { + let (x, y) = (elem(w, a)?, elem(w, b)?); + if x.equals(&y) != (a == b) { + return Err(format!("mod {}: {a} equals {b} is wrong", named(w))); + } + if !x.equals(&x) { + return Err(format!("mod {}: {a} does not equal itself", named(w))); + } + } + } + Ok(()) +} diff --git a/docs/DEPENDENCIES.md b/docs/DEPENDENCIES.md index fed5623..b811034 100644 --- a/docs/DEPENDENCIES.md +++ b/docs/DEPENDENCIES.md @@ -128,6 +128,7 @@ Changing a row is a reviewable act. Adding one means saying why below. | windows_x86_64_msvc | 0.52.6 | test | Locked but never compiled: Windows import library, dependency of `windows-targets`. | | der | 0.8.2 | test | RustCrypto's DER implementation (used by `rsa`, `x509-cert` and `pkcs8`): the reference engine in `clazel-der`'s differential test (`tests/conformance_der.rs`). Used with default features off and only `alloc` and `oid`, so its only dependencies are `const-oid` and `zeroize` (the smallest DER crate that parses and writes every type item 3.5a covers; no other candidate was needed). Pinned to 0.8.2, the latest stable release. | | const-oid | 0.10.2 | test | `der`'s OBJECT IDENTIFIER type (the `oid` feature). No dependencies with default features off. | +| fiat-crypto | 0.3.0 | shipped | fiat-crypto's Coq-synthesized word-by-word Montgomery arithmetic (`MIT OR Apache-2.0 OR BSD-1-Clause`), mul, add and sub carry Coq proofs of the postconditions printed above them; no `unsafe` anywhere in the crate; no dependencies. Default features off (`std` only lifts `no_std`). P-384's field and scalar arithmetic for `clazel-p384` (`src/axioms.rs`): exactly six calls, `fiat_p384_{mul,add,sub}` of `p384_64` (mod p) and `fiat_p384_scalar_{mul,add,sub}` of `p384_scalar_64` (mod n), each one axiom. The crate's other generated modules are compiled but never called. Its generated code indexes arrays and uses plain arithmetic, which our lints would reject, so it cannot be vendored (CLAUDE.md rule 2); it is taken as a verified library (rule 8) instead. | | libcrux-chacha20poly1305 | 0.0.10 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. ChaCha20-Poly1305 (RFC 8439): the record AEAD (`traffic::provider::Factory`). Used by `clazel-crypto` (src/axioms.rs). | | libcrux-curve25519 | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. X25519 (RFC 7748): `hello::key_exchange::KeyExchange`. Used by `clazel-crypto` (src/axioms.rs). | | libcrux-ecdsa | 0.0.9 | shipped | libcrux, badge `verified-hacl` (safe Rust from proven HACL* code), no `unsafe`. ECDSA P-256 with SHA-256 (FIPS 186-5): `ecdsa_secp256r1_sha256` CertificateVerify signatures. Only `p256::verify` with raw r, s and the point coordinates X and Y is called; its DER signature helpers are not (we parse Ecdsa-Sig-Value with `clazel-der`, CLAUDE.md rule 8). Default features off, so `rand` is not reached. Used by `clazel-crypto` (src/axioms.rs). | diff --git a/docs/VERIFICATION.md b/docs/VERIFICATION.md index 59a588d..045db07 100644 --- a/docs/VERIFICATION.md +++ b/docs/VERIFICATION.md @@ -162,7 +162,8 @@ We list this openly. Proofs are only as good as their assumptions. - `clazel-sys`, the one crate with `unsafe` (see "The `unsafe` exception" below): a handful of foreign calls that enter the OS sandbox, and `libc`, its only shipped dependency, for struct layouts and constants -- Cryptography, which comes from formally verified libraries (libcrux / HACL\*), not our own code. +- Cryptographic primitives, which come from formally verified libraries (libcrux / HACL\*, and + fiat-crypto for P-384's field arithmetic), not our own code. What that trusts, precisely: HACL\*'s F\* proofs; the toolchain that translates the verified code to the Rust libcrux ships (in the TCB, not itself proven); libcrux's hand-written, unverified glue around that code @@ -171,6 +172,23 @@ We list this openly. Proofs are only as good as their assumptions. (`libcrux-hacl-rs`, `-secrets`, `-traits`, `-macros`). Every call into libcrux is one axiom in `crates/clazel-crypto/src/axioms.rs`, stating only libcrux's documented types, output lengths and failure cases +- fiat-crypto 0.3.0, for the field arithmetic of `clazel-p384` (`mul`, `add` + and `sub` modulo P-384's p and n). What that trusts, precisely: the Coq + kernel; Coq's extraction to OCaml and the OCaml compiler that runs the + synthesizer; fiat's unverified printer from its intermediate representation + to Rust text (the Rust it ships is not itself proven), including the + pre- and postcondition comments it prints above each function, which are + taken to state the Coq theorem; rustc's fixed-width integer arithmetic + (`u128`, `i128`, `u64`, `i8`) and `as` casts, which the generated code + relies on and whose freedom from overflow comes from fiat's bounds + analysis; and that the published 0.3.0 crate is the synthesizer's output + (`Cargo.lock` pins the tarball's checksum, not a regeneration). Every call + into fiat is one of six axioms in `crates/clazel-p384/src/axioms.rs`, each + stating only the postcondition fiat prints above that function. The + conversions into and out of the Montgomery domain, the octet-string + conversions, exponentiation and inversion are our own code, proven over + those axioms; the ECDSA group law and verification steps will be too, but + are not written yet - That each spec matches the standard it transcribes. No proof can check this, because the standard is English. It is backed by machine-checked evidence instead of a reviewer (next section), and that evidence is only as