diff --git a/dag/extdeps/crypto/nist_p256.dag b/dag/extdeps/crypto/nist_p256.dag new file mode 100644 index 00000000000..f8433f5ff5c --- /dev/null +++ b/dag/extdeps/crypto/nist_p256.dag @@ -0,0 +1,242 @@ +module extdeps.crypto.nist_p256 + +import std.types { Int, List, Bool } +import std.integer { UInt8 } +import std.bignat { + BigNat, MontgomeryModulus, bignat_from_octets, bignat_compare, bignat_is_zero, bignat_bits, bignat_zero_limbs, bignat_one, + montgomery_modulus, montgomery_mul, montgomery_add, montgomery_sub, montgomery_to, montgomery_from, + montgomery_inverse_prime, montgomery_reduce_once, +} +import extdeps.crypto.sha2 { sha256 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// The NIST P-256 curve (SP 800-186 §3.2.1.3) and ECDSA verification over it with SHA-256 +// (FIPS 186-5 §6.4.2), computed in the substrate on std.bignat's Montgomery arithmetic. +// +// WHO CONSUMES THIS TODAY, STATED AS THE FRONTIER IT IS (DESIGN 3c; review 69091 of gunbc#11645). +// NOTHING IN PRODUCTION DOES. The only importers of this module are the witness files under +// dag/test/claim. An earlier version of this header said it was "the producer behind +// extdeps.crypto.signature p256_ecdsa_verify" in the PRESENT TENSE -- and that module declares no +// such name. extdeps.crypto.signature is real and owns the suite, the encodings and the refusal +// vocabulary (SignatureSuite, SignatureVerification, signature_verification_from_implementation), +// but p256_ecdsa_verify does not exist in it or anywhere else outside this module and its tests. +// +// THAT IS THE CLASS THIS REPOSITORY ALREADY ROSTERS AS +// gunbc.recurring_failure_mode unlanded_citation_indistinguishable_at_the_citing_end, and this +// PR's own failure-mode receipts flag their unlanded names scrupulously ("UNLANDED NAMES, read as +// such") while this header -- the one sentence a reader consults to learn who consumes the module +// -- did not. A citation is not made true by being the plan. +// +// DECLARED FRONTIER WITH ITS TRIGGER: extdeps.crypto.signature gains p256_ecdsa_verify, binding +// p256_ecdsa_verify_octets below through signature_verification_from_implementation with the +// decoded octet lengths. Until that declaration exists, this module's consumers are its witnesses +// and nothing else, and no reader should infer otherwise from this comment. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "csrc.nist.gov/pubs/sp/800/186/final" + } +} + +// ── Domain parameters (SP 800-186 §3.2.1.3), as published octets ──────────────────────────── +// THE DOMAIN PARAMETERS ARE OCTETS, NOT A DECODE, BECAUSE A DECODE HAS A FAILURE ARM AND THESE MAY +// NOT HAVE ONE (review 69034 of gunbc#11645). They were previously written as hex strings run +// through base16_decode_lower, whose Absent arm answered bignat_small(n: 0) -- so a mistyped literal +// would have substituted ZERO FOR THE FIELD PRIME and every verification below would have computed +// confidently on a degenerate curve. That is the fabricated default DESIGN 5 names a hard reject, +// and it sat on the five values the whole curve is defined by. +// +// GUARDING THE ARM WAS NOT THE FIX. A refusing p256_hex_nat would make every consumer of the field +// arithmetic answer an Optional for a condition that cannot occur at runtime at all, since the input +// is a source literal. Removing the DECODE removes the arm: each parameter is now its big-endian +// octet encoding, read directly by bignat_from_octets, which is total. There is no longer a state in +// which a parameter is wrong-but-accepted, rather than a check that such a state is reported. +// +// Values: SP 800-186 section 3.2.1.3 (P-256), big-endian, 32 octets each, as SEC1 renders them. +data p256_p_octets: List = [255, 255, 255, 255, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255, 255] +data p256_n_octets: List = [255, 255, 255, 255, 0, 0, 0, 0, 255, 255, 255, 255, 255, 255, 255, 255, 188, 230, 250, 173, 167, 23, 158, 132, 243, 185, 202, 194, 252, 99, 37, 81] +data p256_b_octets: List = [90, 198, 53, 216, 170, 58, 147, 231, 179, 235, 189, 85, 118, 152, 134, 188, 101, 29, 6, 176, 204, 83, 176, 246, 59, 206, 60, 62, 39, 210, 96, 75] +data p256_gx_octets: List = [107, 23, 209, 242, 225, 44, 66, 71, 248, 188, 230, 229, 99, 164, 64, 242, 119, 3, 125, 129, 45, 235, 51, 160, 244, 161, 57, 69, 216, 152, 194, 150] +data p256_gy_octets: List = [79, 227, 66, 226, 254, 26, 127, 155, 142, 231, 235, 74, 124, 15, 158, 22, 43, 206, 51, 87, 107, 49, 94, 206, 203, 182, 64, 104, 55, 191, 81, 245] + +data p256_p: BigNat = bignat_from_octets(octets: p256_p_octets) +data p256_n: BigNat = bignat_from_octets(octets: p256_n_octets) +data p256_b: BigNat = bignat_from_octets(octets: p256_b_octets) +data p256_gx: BigNat = bignat_from_octets(octets: p256_gx_octets) +data p256_gy: BigNat = bignat_from_octets(octets: p256_gy_octets) + +// 256-bit moduli in 24-bit limbs: 11 limbs. +data p256_field: MontgomeryModulus = montgomery_modulus(m: p256_p, width: 11) +data p256_order: MontgomeryModulus = montgomery_modulus(m: p256_n, width: 11) + +// ── Jacobian points over the field, coordinates in Montgomery form ────────────────────────── +// (X, Y, Z) represents (X/Z², Y/Z³); Z = 0 is the point at infinity. +type P256Jacobian { + x: BigNat + y: BigNat + z: BigNat +} + +fn fmul(a: BigNat, b: BigNat) -> BigNat { montgomery_mul(ctx: p256_field, a: a, b: b) } +fn fadd(a: BigNat, b: BigNat) -> BigNat { montgomery_add(ctx: p256_field, a: a, b: b) } +fn fsub(a: BigNat, b: BigNat) -> BigNat { montgomery_sub(ctx: p256_field, a: a, b: b) } +fn fsqr(a: BigNat) -> BigNat { montgomery_mul(ctx: p256_field, a: a, b: a) } + +data p256_infinity: P256Jacobian = P256Jacobian { x: bignat_zero_limbs(), y: bignat_zero_limbs(), z: bignat_zero_limbs() } + +fn p256_is_infinity(p: P256Jacobian) -> Bool { + bignat_is_zero(a: p.z) +} + +fn p256_affine(x: BigNat, y: BigNat) -> P256Jacobian { + P256Jacobian { x: montgomery_to(ctx: p256_field, a: x), y: montgomery_to(ctx: p256_field, a: y), z: montgomery_to(ctx: p256_field, a: bignat_one()) } +} + +// Doubling for a = −3 (Bernstein and Lange, Explicit-Formulas Database, dbl-2001-b). +fn p256_double(p: P256Jacobian) -> P256Jacobian { + if p256_is_infinity(p: p) { p } else { + let delta = fsqr(a: p.z) + let gamma = fsqr(a: p.y) + let beta = fmul(a: p.x, b: gamma) + let t = fmul(a: fsub(a: p.x, b: delta), b: fadd(a: p.x, b: delta)) + let alpha = fadd(a: fadd(a: t, b: t), b: t) + let beta4 = fadd(a: fadd(a: beta, b: beta), b: fadd(a: beta, b: beta)) + let x3 = fsub(a: fsqr(a: alpha), b: fadd(a: beta4, b: beta4)) + let yz = fadd(a: p.y, b: p.z) + let z3 = fsub(a: fsub(a: fsqr(a: yz), b: gamma), b: delta) + let g2 = fsqr(a: gamma) + let g8 = fadd(a: fadd(a: fadd(a: g2, b: g2), b: fadd(a: g2, b: g2)), b: fadd(a: fadd(a: g2, b: g2), b: fadd(a: g2, b: g2))) + let y3 = fsub(a: fmul(a: alpha, b: fsub(a: beta4, b: x3)), b: g8) + P256Jacobian { x: x3, y: y3, z: z3 } + } +} + +// Addition (Explicit-Formulas Database, add-2007-bl), with its two exceptional inputs decided rather +// than fed through: equal points double, opposite points give infinity. +fn p256_add(p: P256Jacobian, q: P256Jacobian) -> P256Jacobian { + if p256_is_infinity(p: p) { q } else if p256_is_infinity(p: q) { p } else { + let z1z1 = fsqr(a: p.z) + let z2z2 = fsqr(a: q.z) + let u1 = fmul(a: p.x, b: z2z2) + let u2 = fmul(a: q.x, b: z1z1) + let s1 = fmul(a: fmul(a: p.y, b: q.z), b: z2z2) + let s2 = fmul(a: fmul(a: q.y, b: p.z), b: z1z1) + let h = fsub(a: u2, b: u1) + let rr = fsub(a: s2, b: s1) + if bignat_is_zero(a: h) { + if bignat_is_zero(a: rr) { p256_double(p: p) } else { p256_infinity } + } else { + let h2 = fadd(a: h, b: h) + let i = fsqr(a: h2) + let j = fmul(a: h, b: i) + let r = fadd(a: rr, b: rr) + let v = fmul(a: u1, b: i) + let x3 = fsub(a: fsub(a: fsqr(a: r), b: j), b: fadd(a: v, b: v)) + let s1j = fmul(a: s1, b: j) + let y3 = fsub(a: fmul(a: r, b: fsub(a: v, b: x3)), b: fadd(a: s1j, b: s1j)) + let zz = fadd(a: p.z, b: q.z) + let z3 = fmul(a: fsub(a: fsub(a: fsqr(a: zz), b: z1z1), b: z2z2), b: h) + P256Jacobian { x: x3, y: y3, z: z3 } + } + } +} + +// ── u1·G + u2·Q by Shamir's simultaneous method ───────────────────────────────────────────── +type P256ShamirBit { + u1: Int + u2: Int +} + +fn p256_zip_bits(a: List, b: List, acc: List) -> List { + match a { + Empty => acc + Cons { head: x, tail: at } => + match b { + Empty => p256_zip_bits(a: at, b: [], acc: acc |> list_push(P256ShamirBit { u1: x, u2: 0 })) + Cons { head: y, tail: bt } => p256_zip_bits(a: at, b: bt, acc: acc |> list_push(P256ShamirBit { u1: x, u2: y })) + } + } +} + +fn p256_double_scalar(u1: BigNat, g: P256Jacobian, u2: BigNat, q: P256Jacobian) -> P256Jacobian { + let gq = p256_add(p: g, q: q) + fold(reverse(p256_zip_bits(a: bignat_bits(a: u1), b: bignat_bits(a: u2), acc: [])), init: p256_infinity, f: (acc, bit) => { + let d = p256_double(p: acc) + if bit.u1 == 1 && bit.u2 == 1 { p256_add(p: d, q: gq) } + else if bit.u1 == 1 { p256_add(p: d, q: g) } + else if bit.u2 == 1 { p256_add(p: d, q: q) } + else { d } + }) +} + +// ── Public key validation (SP 800-186 §D.1.1 partial validation: on the curve, in range) ───── +fn p256_on_curve(x: BigNat, y: BigNat) -> Bool { + let xm = montgomery_to(ctx: p256_field, a: x) + let ym = montgomery_to(ctx: p256_field, a: y) + let bm = montgomery_to(ctx: p256_field, a: p256_b) + let x3 = fmul(a: fsqr(a: xm), b: xm) + let three_x = fadd(a: fadd(a: xm, b: xm), b: xm) + bignat_compare(a: fsqr(a: ym), b: fadd(a: fsub(a: x3, b: three_x), b: bm)) == 0 +} + +fn p256_below(a: BigNat, m: BigNat) -> Bool { + bignat_compare(a: a, b: m) < 0 +} + +fn p256_nonzero_below(a: BigNat, m: BigNat) -> Bool { + !bignat_is_zero(a: a) && p256_below(a: a, m: m) +} + +// Split a list after `n` elements. +type P256Split { + front: List + back: List +} + +fn p256_split(xs: List, n: Int) -> P256Split { + fold(xs, init: P256Split { front: [], back: [] }, f: (acc, x) => + if count(acc.front) < n { P256Split { front: acc.front |> list_push(x), back: acc.back } } + else { P256Split { front: acc.front, back: acc.back |> list_push(x) } }) +} + +// ── ECDSA verification (FIPS 186-5 §6.4.2) ─────────────────────────────────────────────────── +// key: the 65-octet SEC 1 uncompressed point 0x04 || X || Y. signature: the 64-octet r || s. The +// message is hashed here with SHA-256. Answers: +// Present true -- the signature verifies; +// Present false -- well-formed inputs, and it does not; +// Absent -- an input is not an admitted encoding: wrong length, a prefix other than 0x04, +// a coordinate ≥ p, a point off the curve, r or s outside [1, n−1]. +fn p256_ecdsa_verify_octets(key: List, signature: List, message: List) -> Bool? { + if count(key) != 65 || count(signature) != 64 { none } else { + let prefixed = p256_split(xs: key, n: 1) + if prefixed.front != [4] { none } else { + let coords = p256_split(xs: prefixed.back, n: 32) + let qx = bignat_from_octets(octets: coords.front) + let qy = bignat_from_octets(octets: coords.back) + let rs = p256_split(xs: signature, n: 32) + let r = bignat_from_octets(octets: rs.front) + let s = bignat_from_octets(octets: rs.back) + if !p256_below(a: qx, m: p256_p) || !p256_below(a: qy, m: p256_p) || !p256_on_curve(x: qx, y: qy) { none } + else if !p256_nonzero_below(a: r, m: p256_n) || !p256_nonzero_below(a: s, m: p256_n) { none } + else { Present { value: p256_verify_checked(qx: qx, qy: qy, r: r, s: s, message: message) } } + } + } +} + +// e = SHA-256(message) as an integer; 256 bits is the bit length of n, so there is no truncation +// (§6.4.2 step 3). e may exceed n; one reduction suffices because e < 2^256 < 2n. Likewise the final +// v = x mod n needs one reduction, because x < p < 2n. +fn p256_verify_checked(qx: BigNat, qy: BigNat, r: BigNat, s: BigNat, message: List) -> Bool { + let e = montgomery_reduce_once(ctx: p256_order, a: bignat_from_octets(octets: sha256(message: message))) + let sm = montgomery_to(ctx: p256_order, a: s) + let w = montgomery_inverse_prime(ctx: p256_order, a: sm) + let u1 = montgomery_from(ctx: p256_order, a: montgomery_mul(ctx: p256_order, a: montgomery_to(ctx: p256_order, a: e), b: w)) + let u2 = montgomery_from(ctx: p256_order, a: montgomery_mul(ctx: p256_order, a: montgomery_to(ctx: p256_order, a: r), b: w)) + let point = p256_double_scalar(u1: u1, g: p256_affine(x: p256_gx, y: p256_gy), u2: u2, q: p256_affine(x: qx, y: qy)) + if p256_is_infinity(p: point) { false } else { + let zinv = montgomery_inverse_prime(ctx: p256_field, a: point.z) + let x = montgomery_from(ctx: p256_field, a: fmul(a: point.x, b: fsqr(a: zinv))) + bignat_compare(a: montgomery_reduce_once(ctx: p256_order, a: x), b: r) == 0 + } +} diff --git a/dag/extdeps/crypto/sha2.dag b/dag/extdeps/crypto/sha2.dag new file mode 100644 index 00000000000..a8282a81a9d --- /dev/null +++ b/dag/extdeps/crypto/sha2.dag @@ -0,0 +1,207 @@ +module extdeps.crypto.sha2 + +import std.types { Int, List, String } +import std.integer { UInt8, UInt32 } +import std.bitwise { word32_and, word32_xor, word32_not, word32_add, word32_shr, word32_rotr, bitwise_pow2 } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.numeric.base16 { base16_encode_lower } + +// SHA-256 per FIPS 180-4 (Secure Hash Standard), computed in the substrate. extdeps.crypto.hash owns +// the Digest carrier and cites the same standard; this module is the computation that produces the +// bytes such a digest names. Every operation it needs is in std.bitwise. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "csrc.nist.gov/pubs/fips/180-4/upd1/final" + } +} + +// §4.2.2: the first 32 bits of the fractional parts of the cube roots of the first 64 primes. +data sha256_round_constants: List = [ + 1116352408, 1899447441, 3049323471, 3921009573, 961987163, 1508970993, 2453635748, 2870763221, + 3624381080, 310598401, 607225278, 1426881987, 1925078388, 2162078206, 2614888103, 3248222580, + 3835390401, 4022224774, 264347078, 604807628, 770255983, 1249150122, 1555081692, 1996064986, + 2554220882, 2821834349, 2952996808, 3210313671, 3336571891, 3584528711, 113926993, 338241895, + 666307205, 773529912, 1294757372, 1396182291, 1695183700, 1986661051, 2177026350, 2456956037, + 2730485921, 2820302411, 3259730800, 3345764771, 3516065817, 3600352804, 4094571909, 275423344, + 430227734, 506948616, 659060556, 883997877, 958139571, 1322822218, 1537002063, 1747873779, + 1955562222, 2024104815, 2227730452, 2361852424, 2428436474, 2756734187, 3204031479, 3329325298, +] + +// §5.3.3: the first 32 bits of the fractional parts of the square roots of the first 8 primes. +type Sha256State { + a: UInt32 + b: UInt32 + c: UInt32 + d: UInt32 + e: UInt32 + f: UInt32 + g: UInt32 + h: UInt32 +} + +data sha256_initial_state: Sha256State = Sha256State { + a: 1779033703, b: 3144134277, c: 1013904242, d: 2773480762, + e: 1359893119, f: 2600822924, g: 528734635, h: 1541459225, +} + +// §4.1.2 functions. +fn sha256_ch(x: UInt32, y: UInt32, z: UInt32) -> UInt32 { + word32_xor(a: word32_and(a: x, b: y), b: word32_and(a: word32_not(a: x), b: z)) +} + +fn sha256_maj(x: UInt32, y: UInt32, z: UInt32) -> UInt32 { + word32_xor(a: word32_xor(a: word32_and(a: x, b: y), b: word32_and(a: x, b: z)), b: word32_and(a: y, b: z)) +} + +fn sha256_big_sigma0(x: UInt32) -> UInt32 { + word32_xor(a: word32_xor(a: word32_rotr(a: x, n: 2), b: word32_rotr(a: x, n: 13)), b: word32_rotr(a: x, n: 22)) +} + +fn sha256_big_sigma1(x: UInt32) -> UInt32 { + word32_xor(a: word32_xor(a: word32_rotr(a: x, n: 6), b: word32_rotr(a: x, n: 11)), b: word32_rotr(a: x, n: 25)) +} + +fn sha256_small_sigma0(x: UInt32) -> UInt32 { + word32_xor(a: word32_xor(a: word32_rotr(a: x, n: 7), b: word32_rotr(a: x, n: 18)), b: word32_shr(a: x, n: 3)) +} + +fn sha256_small_sigma1(x: UInt32) -> UInt32 { + word32_xor(a: word32_xor(a: word32_rotr(a: x, n: 17), b: word32_rotr(a: x, n: 19)), b: word32_shr(a: x, n: 10)) +} + +// ── The message schedule, as a sliding window ──────────────────────────────────────────────── +// At round t the window holds W[t] .. W[t+15]. Round t reads w0 = W[t], and the window advances by +// shifting in W[t+16] = σ1(W[t+14]) + W[t+9] + σ0(W[t+1]) + W[t] (§6.2.2 step 1). Every read is a +// named field, so no index can fall outside it. +type Sha256Window { + w0: UInt32 + w1: UInt32 + w2: UInt32 + w3: UInt32 + w4: UInt32 + w5: UInt32 + w6: UInt32 + w7: UInt32 + w8: UInt32 + w9: UInt32 + w10: UInt32 + w11: UInt32 + w12: UInt32 + w13: UInt32 + w14: UInt32 + w15: UInt32 +} + +fn sha256_window_push(w: Sha256Window, next: UInt32) -> Sha256Window { + Sha256Window { + w0: w.w1, w1: w.w2, w2: w.w3, w3: w.w4, w4: w.w5, w5: w.w6, w6: w.w7, w7: w.w8, + w8: w.w9, w9: w.w10, w10: w.w11, w11: w.w12, w12: w.w13, w13: w.w14, w14: w.w15, w15: next, + } +} + +fn sha256_window_next(w: Sha256Window) -> UInt32 { + word32_add(a: word32_add(a: sha256_small_sigma1(x: w.w14), b: w.w9), b: word32_add(a: sha256_small_sigma0(x: w.w1), b: w.w0)) +} + +// The block's sixteen big-endian words shifted in one by one: after sixteen pushes every field holds +// a block word, so the empty window's zeros are never read. +data sha256_empty_window: Sha256Window = Sha256Window { + w0: 0, w1: 0, w2: 0, w3: 0, w4: 0, w5: 0, w6: 0, w7: 0, w8: 0, w9: 0, w10: 0, w11: 0, w12: 0, w13: 0, w14: 0, w15: 0, +} + +type Sha256WordFold { + window: Sha256Window + word: Int + filled: Int +} + +fn sha256_block_window(block: List) -> Sha256Window { + fold(block, init: Sha256WordFold { window: sha256_empty_window, word: 0, filled: 0 }, f: (acc, octet) => + if acc.filled == 3 { + Sha256WordFold { window: sha256_window_push(w: acc.window, next: acc.word * 256 + octet), word: 0, filled: 0 } + } else { + Sha256WordFold { window: acc.window, word: acc.word * 256 + octet, filled: acc.filled + 1 } + } + ).window +} + +// ── Compression (§6.2.2) ───────────────────────────────────────────────────────────────────── +type Sha256Rounds { + state: Sha256State + window: Sha256Window +} + +fn sha256_round(r: Sha256Rounds, k: UInt32) -> Sha256Rounds { + let s = r.state + let t1 = word32_add(a: word32_add(a: word32_add(a: s.h, b: sha256_big_sigma1(x: s.e)), b: word32_add(a: sha256_ch(x: s.e, y: s.f, z: s.g), b: k)), b: r.window.w0) + let t2 = word32_add(a: sha256_big_sigma0(x: s.a), b: sha256_maj(x: s.a, y: s.b, z: s.c)) + Sha256Rounds { + state: Sha256State { a: word32_add(a: t1, b: t2), b: s.a, c: s.b, d: s.c, e: word32_add(a: s.d, b: t1), f: s.e, g: s.f, h: s.g }, + window: sha256_window_push(w: r.window, next: sha256_window_next(w: r.window)), + } +} + +fn sha256_compress(h: Sha256State, block: List) -> Sha256State { + let done = fold(sha256_round_constants, init: Sha256Rounds { state: h, window: sha256_block_window(block: block) }, f: (r, k) => sha256_round(r: r, k: k)) + let s = done.state + Sha256State { + a: word32_add(a: h.a, b: s.a), b: word32_add(a: h.b, b: s.b), c: word32_add(a: h.c, b: s.c), d: word32_add(a: h.d, b: s.d), + e: word32_add(a: h.e, b: s.e), f: word32_add(a: h.f, b: s.f), g: word32_add(a: h.g, b: s.g), h: word32_add(a: h.h, b: s.h), + } +} + +// ── Padding (§5.1.1) and block parsing (§5.2.1) ───────────────────────────────────────────── +// The message, 0x80, the fewest zero octets that leave the length ≡ 56 (mod 64), then the bit length +// as a 64-bit big-endian integer. Messages are bounded well below 2^53 bits here, so the length's +// high octets are computed from an Int without overflow. +fn sha256_zero_octets(n: Int, acc: List) -> List { + if n <= 0 { acc } else { sha256_zero_octets(n: n - 1, acc: acc |> list_push(0)) } +} + +fn sha256_length_octets(bits: Int) -> List { + [0, 7, 6, 5, 4, 3, 2, 1] |> map(i => if i == 0 { 0 } else { (bits / bitwise_pow2(n: 8 * (i - 1))) % 256 }) +} + +fn sha256_padded(message: List) -> List { + let len = count(message) + let zeros = (119 - len % 64) % 64 + list_append_octets(left: list_append_octets(left: message |> list_push(128), right: sha256_zero_octets(n: zeros, acc: [])), right: sha256_length_octets(bits: len * 8)) +} + +fn list_append_octets(left: List, right: List) -> List { + fold(right, init: left, f: (acc, o) => acc |> list_push(o)) +} + +type Sha256BlockFold { + state: Sha256State + block: List +} + +// Compress each full 64-octet block as it completes. +fn sha256_state_of(message: List) -> Sha256State { + fold(sha256_padded(message: message), init: Sha256BlockFold { state: sha256_initial_state, block: [] }, f: (acc, octet) => { + let block = acc.block |> list_push(octet) + if count(block) == 64 { + Sha256BlockFold { state: sha256_compress(h: acc.state, block: block), block: [] } + } else { + Sha256BlockFold { state: acc.state, block: block } + } + }).state +} + +fn sha256_word_octets(w: UInt32) -> List { + [(w / 16777216) % 256, (w / 65536) % 256, (w / 256) % 256, w % 256] +} + +// The 32-octet digest, big-endian words a..h. +fn sha256(message: List) -> List { + let s = sha256_state_of(message: message) + fold([s.a, s.b, s.c, s.d, s.e, s.f, s.g, s.h], init: [], f: (acc, w) => list_append_octets(left: acc, right: sha256_word_octets(w: w))) +} + +// The lowercase hex rendering extdeps.crypto.hash Digest.hex carries. +fn sha256_hex(message: List) -> String { + base16_encode_lower(octets: sha256(message: message)) +} diff --git a/dag/gunbc/recurring_failure_mode/check_subject_shape_cannot_represent_the_state_the_check_detects.dag b/dag/gunbc/recurring_failure_mode/check_subject_shape_cannot_represent_the_state_the_check_detects.dag index 50c013d2d3b..13b583ba2aa 100644 --- a/dag/gunbc/recurring_failure_mode/check_subject_shape_cannot_represent_the_state_the_check_detects.dag +++ b/dag/gunbc/recurring_failure_mode/check_subject_shape_cannot_represent_the_state_the_check_detects.dag @@ -16,6 +16,7 @@ data check_subject_shape_cannot_represent_the_state_the_check_detects: Recurring "**THE REPORTING RULE THAT FOLLOWS: a class's rung is the minimum across its in-scope paths (4b(1)), so a fixture path where the RED is authorable does NOT stand in for a live path where it is not.** Citing the fixture rung while the live path is dark is rung inflation. **AND IT IS NOT A 4b(3) DECLARED DROP -- filing one is its own error**, which is where the specimen nearly went: 4b(3) governs a REGRESSION, with a previous rung and a population that LOST a guarantee. When the shape mismatch predates the check, the wall was never lit through that path, and a capability that was never real cannot be dropped. The honest instruments are 4b(1) rung honesty and 4b(2) an untracked stall made tracked.", "**RUNG: 1 (mitigatable) -- the gap is nameable and, once found, held open by the two-arm control. CEILING: 4, since whether a subject's representation can inhabit the state a check matches on is decidable from two declarations the tree already carries. NEXT-RUNG TRIGGER, a CAPABILITY and not an artifact: a check declares the subject representation it matches over, and a check whose match is unsatisfiable by that representation fails to compile -- so the decoration cannot be authored at all, rather than being found later by someone constructing the value by hand.**)", + "**A GUARD AGAINST AN UNREPRESENTABLE STATE CAN BE WORSE THAN A DECORATION: IT CAN BE THE FAILURE ITSELF** (gunbc#11645, lane A of the approval app, 2026-09-20, review 69054 and the author's correction to it). Review 69034 found std.bignat bignat_small minting a BigNat from an unchecked caller Int and named two invalid inputs: a NEGATIVE n, which writes negative limbs, and n >= 2^72, which overflows the 24-bit top limb. The first is real. THE SECOND IS UNREPRESENTABLE IN THE SUBJECT: Int is 64-bit, so the largest expressible n is 2^63 - 1, whose top limb is 2^63 / 2^48 = 32767, comfortably inside 2^24. No Int reaches the boundary, so a check for it is permanently green over its own subject -- this class exactly, arrived at from a REVIEW FINDING rather than from a lens. **THE NEW PART, AND IT IS WHY THIS ROW SHOULD NOT READ AS ONLY INERTNESS:** the guard first authored was `n >= bignat_base * bignat_base * bignat_base`, and that expression IS 2^72, which the substrate cannot evaluate -- it RAISES IntegerOverflow. So the check against an input that cannot occur would itself have been the only way to make the function fail. A decoration costs a reader's trust; this would have converted a total function into a raising one, on every call, in service of a state no caller could ever supply. **HOW IT WAS CAUGHT is the receipt worth keeping for this row's recognition rule:** not by reasoning, but by trying to WRITE THE RED -- the witness asserting the refusal could not be authored, because 4722366482869645213696 is not a writable Int literal. The row's own rule (construct a value in the subject's representation that exhibits the state) was satisfied by the compiler refusing the construction. The reachable half shipped as a real refusal with a passing negative control; the unreachable half is described on the carrier instead of authored.", "**THE REPAIR LANDED AND ITS DIRECTION IS NOT SYMMETRIC: RESHAPE THE PRODUCER, NEVER WIDEN THE CHECK** (gunbc#10282, cool-fox-470, the reshape arm of the same specimen this row was filed from). `v1.stage0.coproduct_reflection` `marshal_generic` now returns a `ComputationNode { behavior: Transform }` record for an `ExprCall` with a non-empty authored name -- the case where the callee identity leaf is already the first positional edge -- so the subject representation gained the constructor the check matches on and the RED became authorable over the live substrate. The arm NOT taken is the one that looks equally available and is not: widening `node_is_call` to also accept the Conj spelling would have made the check green again by ratifying the fork, leaving the substrate with two definitions of a call and the compiler's own lowered-body carrier advisory. A check may not be taught the producer's spelling; the producer must emit the substrate's carrier.", "**THE FIELD TELL IS VISIBLE BY READING, BEFORE ANYTHING RUNS: A PRIVATE COPY OF THE SHARED PREDICATE.** `v2.lens.no_dual_representation_test.scan` carried `skeleton_is_call`, `skeleton_is_callee_atom` and `skeleton_call_argument_targets` -- `v2.std.node_query`'s `node_is_call` / `call_callee_target` / `call_argument_targets` respelled against `TypeNode { connective: Conj }` -- because the shared authority could not read its own substrate. A SECOND PREDICATE ANSWERING ONE QUESTION IS EVIDENCE THAT THE FIRST DOES NOT APPLY TO SOMEBODY'S INPUT, and it is a static, greppable symptom of this class that needs no execution to find. The fork and the defect shipped together: the workaround is what let the unrepresentable subject go unnoticed. It is deleted rather than parameterised in #10282, and `replace_param_in_output` in that same module -- which descended `Conj` alone -- would have returned every body containing a call UNSUBSTITUTED the moment the carrier appeared, a fail-open the repair itself would have created.", diff --git a/dag/std/bignat.dag b/dag/std/bignat.dag new file mode 100644 index 00000000000..33dbb67078c --- /dev/null +++ b/dag/std/bignat.dag @@ -0,0 +1,364 @@ +module std.bignat + +import std.types { Int, List, String, Bool } +import std.integer { UInt8 } + +// A MULTI-LIMB UNSIGNED NATURAL over the substrate's 64-bit Int, which refuses on overflow. +// +// LIMB WIDTH IS 24 BITS, and the reason is the product bound, not taste: a limb is below 2^24, so a +// limb product is below 2^48, and a step that adds a product, a limb and a carry stays below 2^49 -- +// fourteen bits of headroom under 2^63, so no step can reach the overflow refusal. 32-bit limbs +// would overflow on a single product; 31 would leave one bit. 24 is also exactly three octets, so +// octet and hex conversion is slicing rather than bit shuffling. A 256-bit value is 11 limbs. +// +// Limbs are least significant first. A BigNat may carry high zero limbs; every operation below is +// correct for any lengths, and fixed-width users (the Montgomery context) pad to their width. +// SOLE-CONSTRUCTED, BECAUSE EVERY OVERFLOW ARGUMENT IN THIS MODULE RESTS ON THE LIMB INVARIANT +// (review of gunbc#11645). The limb width of 24 bits is what keeps a limb product below 2^48 and the +// CIOS accumulator inside the host integer -- but that reasoning holds only if every limb really is +// in [0, 2^24). As an ordinary record, any caller could write BigNat { limbs: [-5, 99999999] } and +// the arithmetic below would compute confidently on it. A proof resting on an invariant the +// constructor does not enforce is validation standing where construction was available (DESIGN 5), +// and its tell is exactly the one DESIGN names: the guarantee can be satisfied by reading the +// declaration while the realization lies. +// +// WHAT THIS CLOSES AND WHAT IT DOES NOT. sole_constructor restricts WHO may construct: outside +// std.bignat there is no expression that mints one, so the FABRICATION route is gone by +// construction. It does not restrict WHAT this module may construct. +// +// AN EARLIER VERSION OF THIS NOTE CLAIMED THE INTERNAL CONSTRUCTIONS NEVER DERIVE FROM UNCHECKED +// CALLER INPUT. THAT WAS FALSE WHEN WRITTEN (review 69034 of gunbc#11645): bignat_small took a raw +// caller Int and wrote n / base^2 as its top limb with no reduction, so any n >= 2^72 produced a +// limb above 2^24 and any negative n produced a negative limb -- through a PUBLIC function, which +// is the very route the wall above was claimed to close. An annotation is never evidence (DESIGN +// 4c); this one asserted the invariant it was standing next to a breach of. +type BigNat sole_constructor { + limbs: List +} + +data bignat_base: Int = 16777216 + +fn bignat_zero() -> BigNat { + BigNat { limbs: [] } +} + +// THE ONLY ENTRY THAT TOOK AN UNCHECKED CALLER Int, NOW REFUSING -- ON THE ONE CONDITION THAT CAN +// ACTUALLY OCCUR. A NEGATIVE n has no unsigned representation, and before this it produced a +// NEGATIVE LIMB through a public function, breaking the invariant every overflow argument in this +// module rests on (review 69034 of gunbc#11645). +// +// THE OVER-LARGE CASE THE REVIEW ALSO NAMED IS UNREACHABLE HERE, AND GUARDING IT WOULD HAVE BEEN +// WORSE THAN USELESS. Three limbs carry values below base^3 = 2^72, so the review is right that a +// larger n would overflow the top limb -- but Int is 64-bit, so the largest n expressible is +// 2^63 - 1, whose top limb is 32767, comfortably inside 2^24. No Int reaches the boundary. Writing +// `n >= bignat_base * bignat_base * bignat_base` would not merely be dead: evaluating 2^72 RAISES +// IntegerOverflow, so the guard against an impossible input would itself be the failure. The +// unreachable arm is therefore described here rather than authored (DESIGN 4b: ask whether the +// check's RED is authorable before writing the check). +fn bignat_small(n: Int) -> BigNat? { + if n < 0 { + none + } else { + Present { value: BigNat { limbs: [n % bignat_base, (n / bignat_base) % bignat_base, n / (bignat_base * bignat_base)] } } + } +} + +// Total, because their limbs are written here rather than derived from an argument. Byte-identical +// to what bignat_small produced for 0 and 1, so substituting them changes no value anywhere. +fn bignat_zero_limbs() -> BigNat { + BigNat { limbs: [0, 0, 0] } +} + +fn bignat_one() -> BigNat { + BigNat { limbs: [1, 0, 0] } +} + +// ── Octets and hex (big-endian on the wire) ────────────────────────────────────────────────── +type BignatOctetFold { + limbs: List + limb: Int + place: Int +} + +// Big-endian octets to limbs: walk the octets from the least significant end. +fn bignat_from_octets(octets: List) -> BigNat { + let r = fold(reverse(octets), init: BignatOctetFold { limbs: [], limb: 0, place: 1 }, f: (acc, o) => + if acc.place == 65536 { + BignatOctetFold { limbs: acc.limbs |> list_push(acc.limb + o * 65536), limb: 0, place: 1 } + } else { + BignatOctetFold { limbs: acc.limbs, limb: acc.limb + o * acc.place, place: acc.place * 256 } + }) + if r.place == 1 { BigNat { limbs: r.limbs } } else { BigNat { limbs: r.limbs |> list_push(r.limb) } } +} + +fn bignat_limb_octets(limb: Int) -> List { + [limb / 65536, (limb / 256) % 256, limb % 256] +} + +// Exactly `width` big-endian octets. A value that does not fit answers Absent rather than truncating. +fn bignat_to_octets(a: BigNat, width: Int) -> List? { + let all = fold(reverse(a.limbs), init: [], f: (acc, limb) => fold(bignat_limb_octets(limb: limb), init: acc, f: (acc2, o) => acc2 |> list_push(o))) + bignat_fit_octets(octets: all, width: width) +} + +fn bignat_fit_octets(octets: List, width: Int) -> List? { + let n = count(octets) + if n == width { + Present { value: octets } + } else if n < width { + Present { value: bignat_pad_front(octets: octets, zeros: width - n) } + } else { + match octets { + Empty => none + Cons { head: h, tail: t } => if h == 0 { bignat_fit_octets(octets: t, width: width) } else { none } + } + } +} + +fn bignat_pad_front(octets: List, zeros: Int) -> List { + if zeros <= 0 { octets } else { bignat_pad_front(octets: fold(octets, init: [0], f: (acc, o) => acc |> list_push(o)), zeros: zeros - 1) } +} + +// ── Comparison ─────────────────────────────────────────────────────────────────────────────── +// -1, 0 or 1. Walks both limb lists from the least significant end; the most significant +// difference decides, and missing limbs are zero. +fn bignat_compare(a: BigNat, b: BigNat) -> Int { + bignat_compare_limbs(a: a.limbs, b: b.limbs, decided: 0) +} + +fn bignat_compare_limbs(a: List, b: List, decided: Int) -> Int { + match a { + Empty => + match b { + Empty => decided + Cons { head: y, tail: bt } => bignat_compare_limbs(a: [], b: bt, decided: if y > 0 { -1 } else { decided }) + } + Cons { head: x, tail: at } => + match b { + Empty => bignat_compare_limbs(a: at, b: [], decided: if x > 0 { 1 } else { decided }) + Cons { head: y, tail: bt } => + bignat_compare_limbs(a: at, b: bt, decided: if x > y { 1 } else if x < y { -1 } else { decided }) + } + } +} + +fn bignat_is_zero(a: BigNat) -> Bool { + fold(a.limbs, init: true, f: (acc, x) => acc && x == 0) +} + +// ── Addition and subtraction ───────────────────────────────────────────────────────────────── +fn bignat_add(a: BigNat, b: BigNat) -> BigNat { + BigNat { limbs: bignat_add_limbs(a: a.limbs, b: b.limbs, carry: 0, acc: []) } +} + +fn bignat_add_limbs(a: List, b: List, carry: Int, acc: List) -> List { + match a { + Empty => + match b { + Empty => if carry > 0 { acc |> list_push(carry) } else { acc } + Cons { head: y, tail: bt } => bignat_add_limbs(a: [], b: bt, carry: (y + carry) / bignat_base, acc: acc |> list_push((y + carry) % bignat_base)) + } + Cons { head: x, tail: at } => + match b { + Empty => bignat_add_limbs(a: at, b: [], carry: (x + carry) / bignat_base, acc: acc |> list_push((x + carry) % bignat_base)) + Cons { head: y, tail: bt } => bignat_add_limbs(a: at, b: bt, carry: (x + y + carry) / bignat_base, acc: acc |> list_push((x + y + carry) % bignat_base)) + } + } +} + +// a - b, or Absent when b > a: a natural has no negative to answer with. +fn bignat_sub(a: BigNat, b: BigNat) -> BigNat? { + if bignat_compare(a: a, b: b) < 0 { none } else { Present { value: BigNat { limbs: bignat_sub_limbs(a: a.limbs, b: b.limbs, borrow: 0, acc: []) } } } +} + +// Called only with a >= b, so the final borrow is zero. +fn bignat_sub_limbs(a: List, b: List, borrow: Int, acc: List) -> List { + match a { + Empty => acc + Cons { head: x, tail: at } => + match b { + Empty => { + let d = x - borrow + if d < 0 { bignat_sub_limbs(a: at, b: [], borrow: 1, acc: acc |> list_push(d + bignat_base)) } else { bignat_sub_limbs(a: at, b: [], borrow: 0, acc: acc |> list_push(d)) } + } + Cons { head: y, tail: bt } => { + let d = x - y - borrow + if d < 0 { bignat_sub_limbs(a: at, b: bt, borrow: 1, acc: acc |> list_push(d + bignat_base)) } else { bignat_sub_limbs(a: at, b: bt, borrow: 0, acc: acc |> list_push(d)) } + } + } + } +} + +// ── Bits ───────────────────────────────────────────────────────────────────────────────────── +// Bit i of a (0 = least significant), as 0 or 1. +fn bignat_limb_bits(limb: Int, remaining: Int, acc: List) -> List { + if remaining <= 0 { acc } else { bignat_limb_bits(limb: limb / 2, remaining: remaining - 1, acc: acc |> list_push(limb % 2)) } +} + +// All bits, least significant first: 24 per limb. +fn bignat_bits(a: BigNat) -> List { + fold(a.limbs, init: [], f: (acc, limb) => bignat_limb_bits(limb: limb, remaining: 24, acc: acc)) +} + +// ── Montgomery arithmetic modulo an odd m ──────────────────────────────────────────────────── +// Values are held as a·R mod m with R = 2^(24·width). mont_mul(a, b) = a·b·R⁻¹ mod m by the +// coarsely integrated operand scanning method (Koç, Acar and Kaliski, "Analyzing and Comparing +// Montgomery Multiplication Algorithms", 1996): for each limb a_i, t ← (t + a_i·b + q·m) / 2^24 with +// q = (t_0 + a_i·b_0)·(−m⁻¹) mod 2^24, which makes the division exact. Every step is one product plus +// a limb plus a carry, inside the 2^49 bound stated at the top. +// SOLE-CONSTRUCTED FOR THE SAME REASON, AND WITH A LARGER REMAINING GAP THAT IS STATED RATHER THAN +// IMPLIED. The Montgomery routines additionally assume a positive width, an odd nonzero modulus, a +// modulus fitting the declared width, a neg_inverse and r_squared consistent with that modulus, and +// operands that are reduced residues. sole_constructor stops an outside caller from ASSEMBLING an +// inconsistent one, which is the fabrication hole; it does NOT check the fields montgomery_modulus +// itself computes from its arguments. +// +// SO THIS IS A PARTIAL CLOSE AND MUST NOT BE READ AS A FULL ONE. NEXT-RUNG TRIGGER, a capability: a +// refusing admission on montgomery_modulus that establishes each invariant above and returns a typed +// refusal naming the one that failed, SUFFICIENT FOR an inconsistent modulus to have no constructor +// rather than merely no outside constructor. It is deferred to its own change because making this +// admission refusing turns p256_field and p256_order into refusable data rows, cascading through +// every consumer of the field arithmetic -- and the P-256 witness suite has never executed, so that +// restructuring cannot yet be read for breakage. +type MontgomeryModulus sole_constructor { + modulus: BigNat + width: Int + neg_inverse: Int + r_squared: BigNat +} + +// −m⁻¹ mod 2^24 from the lowest limb, by Newton's iteration x ← x(2 − m₀x), which doubles the +// number of correct low bits each step: 1 → 2 → 4 → 8 → 16 → 32 ≥ 24 after five steps. Each product +// is reduced mod 2^24 before the next multiplication, so nothing exceeds 2^48. +fn montgomery_neg_inverse(m0: Int) -> Int { + let x1 = montgomery_newton(m0: m0, x: 1) + let x2 = montgomery_newton(m0: m0, x: x1) + let x3 = montgomery_newton(m0: m0, x: x2) + let x4 = montgomery_newton(m0: m0, x: x3) + let x5 = montgomery_newton(m0: m0, x: x4) + (bignat_base - x5) % bignat_base +} + +fn montgomery_newton(m0: Int, x: Int) -> Int { + let mx = (m0 * x) % bignat_base + (x * ((2 + bignat_base - mx) % bignat_base)) % bignat_base +} + +fn bignat_pad(limbs: List, width: Int) -> List { + let n = count(limbs) + if n >= width { limbs } else { bignat_pad(limbs: limbs |> list_push(0), width: width) } +} + +fn bignat_lowest(limbs: List) -> Int { + match limbs { + Empty => 0 + Cons { head: h, tail: _ } => h + } +} + +fn bignat_drop_lowest(limbs: List) -> List { + match limbs { + Empty => [] + Cons { head: _, tail: t } => t + } +} + +// t + k·x, as limbs, where t has at least as many limbs as x. +fn bignat_add_scaled(t: List, x: List, k: Int, carry: Int, acc: List) -> List { + match t { + Empty => if carry > 0 { acc |> list_push(carry) } else { acc } + Cons { head: tj, tail: tt } => + match x { + Empty => bignat_add_scaled(t: tt, x: [], k: k, carry: (tj + carry) / bignat_base, acc: acc |> list_push((tj + carry) % bignat_base)) + Cons { head: xj, tail: xt } => { + let v = tj + k * xj + carry + bignat_add_scaled(t: tt, x: xt, k: k, carry: v / bignat_base, acc: acc |> list_push(v % bignat_base)) + } + } + } +} + +fn montgomery_step(ctx: MontgomeryModulus, t: List, ai: Int, b: List) -> List { + let u = bignat_add_scaled(t: t, x: b, k: ai, carry: 0, acc: []) + let q = (bignat_lowest(limbs: u) * ctx.neg_inverse) % bignat_base + bignat_pad(limbs: bignat_drop_lowest(limbs: bignat_add_scaled(t: u, x: ctx.modulus.limbs, k: q, carry: 0, acc: [])), width: ctx.width + 1) +} + +// a·b·R⁻¹ mod m, for a, b < m. The loop result is below 2m, so one conditional subtraction finishes. +fn montgomery_mul(ctx: MontgomeryModulus, a: BigNat, b: BigNat) -> BigNat { + let t = fold(bignat_pad(limbs: a.limbs, width: ctx.width), init: bignat_pad(limbs: [], width: ctx.width + 1), f: (acc, ai) => montgomery_step(ctx: ctx, t: acc, ai: ai, b: b.limbs)) + montgomery_reduce_once(ctx: ctx, a: BigNat { limbs: t }) +} + +fn montgomery_reduce_once(ctx: MontgomeryModulus, a: BigNat) -> BigNat { + match bignat_sub(a: a, b: ctx.modulus) { + Present { value: d } => BigNat { limbs: bignat_truncate(limbs: d.limbs, width: ctx.width) } + Absent => BigNat { limbs: bignat_truncate(limbs: a.limbs, width: ctx.width) } + } +} + +// Keep the low `width` limbs. Used only where the dropped limbs are known to be zero. +fn bignat_truncate(limbs: List, width: Int) -> List { + fold(limbs, init: [], f: (acc, x) => if count(acc) < width { acc |> list_push(x) } else { acc }) +} + +// R² mod m by doubling 1 modulo m, 2·24·width times, each doubling followed by a conditional +// subtraction. Derived from the modulus; never a transcribed constant. +fn montgomery_r_squared(m: BigNat, width: Int) -> BigNat { + montgomery_double_times(m: m, a: bignat_one(), times: 48 * width) +} + +fn montgomery_double_times(m: BigNat, a: BigNat, times: Int) -> BigNat { + if times <= 0 { a } else { + let d = bignat_add(a: a, b: a) + montgomery_double_times(m: m, a: match bignat_sub(a: d, b: m) { Present { value: r } => r Absent => d }, times: times - 1) + } +} + +// The context for an odd modulus of `width` limbs. +fn montgomery_modulus(m: BigNat, width: Int) -> MontgomeryModulus { + MontgomeryModulus { + modulus: BigNat { limbs: bignat_pad(limbs: m.limbs, width: width) }, + width: width, + neg_inverse: montgomery_neg_inverse(m0: bignat_lowest(limbs: m.limbs)), + r_squared: montgomery_r_squared(m: m, width: width), + } +} + +fn montgomery_to(ctx: MontgomeryModulus, a: BigNat) -> BigNat { + montgomery_mul(ctx: ctx, a: a, b: ctx.r_squared) +} + +fn montgomery_from(ctx: MontgomeryModulus, a: BigNat) -> BigNat { + montgomery_mul(ctx: ctx, a: a, b: bignat_one()) +} + +// Modular addition and subtraction of RESIDUES: both operands below m, which every montgomery_* +// producer guarantees. Under that invariant m - b is a natural, so it is computed directly and no +// arm exists for an impossible negative to be answered with a made-up value. +fn montgomery_add(ctx: MontgomeryModulus, a: BigNat, b: BigNat) -> BigNat { + montgomery_reduce_once(ctx: ctx, a: bignat_add(a: a, b: b)) +} + +fn montgomery_negate(ctx: MontgomeryModulus, b: BigNat) -> BigNat { + BigNat { limbs: bignat_sub_limbs(a: ctx.modulus.limbs, b: b.limbs, borrow: 0, acc: []) } +} + +fn montgomery_sub(ctx: MontgomeryModulus, a: BigNat, b: BigNat) -> BigNat { + montgomery_reduce_once(ctx: ctx, a: bignat_add(a: a, b: montgomery_negate(ctx: ctx, b: b))) +} + +// a^e in Montgomery form, left to right over e's bits. `one` is R mod m (1 in Montgomery form). +fn montgomery_pow(ctx: MontgomeryModulus, a: BigNat, e: BigNat) -> BigNat { + let one = montgomery_to(ctx: ctx, a: bignat_one()) + fold(reverse(bignat_bits(a: e)), init: one, f: (acc, bit) => { + let sq = montgomery_mul(ctx: ctx, a: acc, b: acc) + if bit == 1 { montgomery_mul(ctx: ctx, a: sq, b: a) } else { sq } + }) +} + +// The inverse of a nonzero a modulo a prime m, by Fermat: a^(m−2). Montgomery form in and out. +// m is an odd prime, so m ≥ 3 and m − 2 is a natural. +fn montgomery_inverse_prime(ctx: MontgomeryModulus, a: BigNat) -> BigNat { + montgomery_pow(ctx: ctx, a: a, e: BigNat { limbs: bignat_sub_limbs(a: ctx.modulus.limbs, b: [2], borrow: 0, acc: []) }) +} diff --git a/dag/std/bitwise.dag b/dag/std/bitwise.dag new file mode 100644 index 00000000000..28322700ba5 --- /dev/null +++ b/dag/std/bitwise.dag @@ -0,0 +1,216 @@ +module std.bitwise + +import std.types { Int, List } +import std.integer { UInt32 } + +// BITWISE OPERATIONS OVER BOUNDED NATURALS, emulated with the only integer operations the substrate +// has (+ - * / %, over a 64-bit Int that refuses on overflow). The operands are std.integer's +// bounded naturals -- UInt32 here, and Word64 below as its two halves, because a 64-bit unsigned +// value does not fit a signed 64-bit Int. std.bit's Word32 is the same width read as a list of +// bits; this module is the arithmetic reading of it, not a second word type. +// +// WHICH OPERATIONS ARE ARITHMETIC AND WHICH ARE NOT. Shifts, rotations, complement and addition +// modulo 2^w are exact integer identities (x / 2^n, x % 2^n, (2^w - 1) - x, (a + b) % 2^w). Only +// conjunction has no closed arithmetic form, so it is computed four bits at a time from a 16 x 16 +// table DERIVED below from the one-bit definition, and exclusive-or and disjunction follow from it: +// a xor b = a + b - 2 (a and b), a or b = a + b - (a and b). + +data word32_modulus: Int = 4294967296 + +fn bitwise_pow2_defined(n: Int) -> Int { + if n <= 0 { 1 } else { 2 * bitwise_pow2_defined(n: n - 1) } +} + +// 2^0 .. 2^62, derived from the definition above so the hot paths index rather than recurse. +data bitwise_pow2_table: List = fold( + [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, + 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62], + init: [], f: (acc, n) => acc |> list_push(bitwise_pow2_defined(n: n))) + +// The Absent arm is the definition itself, reached only for n outside [0, 62]; it answers the same +// value the table would, so it is not a fallback to something else. +fn bitwise_pow2(n: Int) -> Int { + match get(bitwise_pow2_table, n) { + Present { value: v } => v + Absent => bitwise_pow2_defined(n: n) + } +} + +// One bit of a nibble. +fn nibble_bit(x: Int, i: Int) -> Int { + (x / bitwise_pow2_defined(n: i)) % 2 +} + +fn nibble_and(a: Int, b: Int) -> Int { + nibble_bit(x: a, i: 0) * nibble_bit(x: b, i: 0) + + 2 * nibble_bit(x: a, i: 1) * nibble_bit(x: b, i: 1) + + 4 * nibble_bit(x: a, i: 2) * nibble_bit(x: b, i: 2) + + 8 * nibble_bit(x: a, i: 3) * nibble_bit(x: b, i: 3) +} + +// Per-bit exclusive or: a + b - 2ab is 0,1,1,0 over the four bit pairs, and every term here is a +// single BIT, so nothing in this function approaches a word boundary. +fn nibble_xor(a: Int, b: Int) -> Int { + let x0 = nibble_bit(x: a, i: 0) + nibble_bit(x: b, i: 0) - 2 * nibble_bit(x: a, i: 0) * nibble_bit(x: b, i: 0) + let x1 = nibble_bit(x: a, i: 1) + nibble_bit(x: b, i: 1) - 2 * nibble_bit(x: a, i: 1) * nibble_bit(x: b, i: 1) + let x2 = nibble_bit(x: a, i: 2) + nibble_bit(x: b, i: 2) - 2 * nibble_bit(x: a, i: 2) * nibble_bit(x: b, i: 2) + let x3 = nibble_bit(x: a, i: 3) + nibble_bit(x: b, i: 3) - 2 * nibble_bit(x: a, i: 3) * nibble_bit(x: b, i: 3) + x0 + 2 * x1 + 4 * x2 + 8 * x3 +} + +fn nibble_values() -> List { + [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15] +} + +// Row-major: entry 16a + b is (a and b). Derived, never transcribed. +data nibble_and_table: List = fold(nibble_values(), init: [], f: (acc, a) => + fold(nibble_values(), init: acc, f: (row, b) => row |> list_push(nibble_and(a: a, b: b)))) + +// Row-major: entry 16a + b is (a xor b). Derived, never transcribed. +data nibble_xor_table: List = fold(nibble_values(), init: [], f: (acc, a) => + fold(nibble_values(), init: acc, f: (row, b) => row |> list_push(nibble_xor(a: a, b: b)))) + +// As with bitwise_pow2, the Absent arm is the definition itself and is unreachable for a, b < 16. +fn nibble_and_lookup(a: Int, b: Int) -> Int { + match get(nibble_and_table, a * 16 + b) { + Present { value: v } => v + Absent => nibble_and(a: a, b: b) + } +} + +fn nibble_xor_lookup(a: Int, b: Int) -> Int { + match get(nibble_xor_table, a * 16 + b) { + Present { value: v } => v + Absent => nibble_xor(a: a, b: b) + } +} + +// Conjunction over `digits` nibbles, least significant first. +fn nibbles_and(a: Int, b: Int, digits: Int) -> Int { + if digits <= 0 { 0 } else { nibble_and_lookup(a: a % 16, b: b % 16) + 16 * nibbles_and(a: a / 16, b: b / 16, digits: digits - 1) } +} + +// Exclusive or over `digits` nibbles, least significant first. The accumulated value is bounded by +// the digits consumed so far, so it never exceeds the word it is building. +fn nibbles_xor(a: Int, b: Int, digits: Int) -> Int { + if digits <= 0 { 0 } else { nibble_xor_lookup(a: a % 16, b: b % 16) + 16 * nibbles_xor(a: a / 16, b: b / 16, digits: digits - 1) } +} + +fn word32_and(a: UInt32, b: UInt32) -> UInt32 { + nibbles_and(a: a, b: b, digits: 8) +} + +// NO INTERMEDIATE HERE LEAVES [0, 2^32), AND THAT IS THE POINT RATHER THAN AN OPTIMISATION +// (review 69054 of gunbc#11645). These were written as `a + b - 2 * and` and `a + b - and`, whose +// answers are correct but whose SUM reaches 2^33 - 2 while typed UInt32 -- the population of +// gunbc.recurring_failure_mode bounded_natural_arithmetic_evaluated_as_unbounded_int, which that +// row cites at this very line, and which DESIGN 4b places BELOW THE LADDER rather than on it. +// +// Nibble-wise exclusive or removes the oversized intermediate instead of declaring it: each lookup +// is over values below 16 and the accumulator is bounded by the digits consumed, exactly as +// word32_and already worked. Disjunction is then xor plus and, which are disjoint bit sets, so +// their sum IS the disjunction and is bounded by it -- no wider than the result. +fn word32_xor(a: UInt32, b: UInt32) -> UInt32 { + nibbles_xor(a: a, b: b, digits: 8) +} + +fn word32_or(a: UInt32, b: UInt32) -> UInt32 { + word32_xor(a: a, b: b) + word32_and(a: a, b: b) +} + +fn word32_not(a: UInt32) -> UInt32 { + word32_modulus - 1 - a +} + +// Addition modulo 2^32 decided BEFORE the sum is formed, so the wrap is computed rather than +// recovered from an oversized value: when a would carry past the modulus, the answer is the +// distance it travelled past it. `word32_modulus - b` is at least 1 for every b in range, and both +// branches stay strictly below the modulus. +fn word32_add(a: UInt32, b: UInt32) -> UInt32 { + if a >= word32_modulus - b { + a - (word32_modulus - b) + } else { + a + b + } +} + +fn word32_shr(a: UInt32, n: Int) -> UInt32 { + a / bitwise_pow2(n: n) +} + +fn word32_shl(a: UInt32, n: Int) -> UInt32 { + (a % bitwise_pow2(n: 32 - n)) * bitwise_pow2(n: n) +} + +// Rotate right by n in [0, 32): the low n bits move to the top. +fn word32_rotr(a: UInt32, n: Int) -> UInt32 { + a / bitwise_pow2(n: n) + (a % bitwise_pow2(n: n)) * bitwise_pow2(n: 32 - n) +} + +// ── 64-bit words ───────────────────────────────────────────────────────────────────────────── +// Two 32-bit halves, because 2^64 - 1 exceeds the signed 64-bit Int. Every operation is the 32-bit +// operation on each half, except where bits cross the boundary (addition's carry, shifts and +// rotations), which are stated explicitly. +type Word64 { + hi: UInt32 + lo: UInt32 +} + +fn word64_and(a: Word64, b: Word64) -> Word64 { + Word64 { hi: word32_and(a: a.hi, b: b.hi), lo: word32_and(a: a.lo, b: b.lo) } +} + +fn word64_xor(a: Word64, b: Word64) -> Word64 { + Word64 { hi: word32_xor(a: a.hi, b: b.hi), lo: word32_xor(a: a.lo, b: b.lo) } +} + +fn word64_or(a: Word64, b: Word64) -> Word64 { + Word64 { hi: word32_or(a: a.hi, b: b.hi), lo: word32_or(a: a.lo, b: b.lo) } +} + +fn word64_not(a: Word64) -> Word64 { + Word64 { hi: word32_not(a: a.hi), lo: word32_not(a: a.lo) } +} + +// THE SAME REPAIR AS word32_add, WHICH THIS SKIPPED IN THE DIFF THAT MADE IT (review 69076 of +// gunbc#11645). It was `let lo = a.lo + b.lo` over two UInt32 halves, reaching 2^33 - 2 while +// typed UInt32, and `a.hi + b.hi + carry` doing it again -- the same population the note above +// says word32_xor, word32_or and word32_add were rewritten to leave. Applying a repair to the +// 32-bit family and not the 64-bit one in one change is the defect surviving inside its own fix, +// and it was LIVE rather than latent: sha256_fips_witness_test drives lo to exactly 2^32. +// +// The carry is decided BEFORE either sum is formed, by the same comparison word32_add uses, and +// both halves are then produced by word32_add itself rather than by a raw `%` -- so the wrap is +// computed once, in one place, and no intermediate here leaves [0, 2^32). +fn word64_add(a: Word64, b: Word64) -> Word64 { + let carry = if a.lo >= word32_modulus - b.lo { 1 } else { 0 } + Word64 { + hi: word32_add(a: word32_add(a: a.hi, b: b.hi), b: carry), + lo: word32_add(a: a.lo, b: b.lo), + } +} + +// Shift right by n in [0, 64). +fn word64_shr(a: Word64, n: Int) -> Word64 { + if n >= 32 { + Word64 { hi: 0, lo: word32_shr(a: a.hi, n: n - 32) } + } else if n == 0 { + a + } else { + Word64 { hi: word32_shr(a: a.hi, n: n), lo: word32_shr(a: a.lo, n: n) + (a.hi % bitwise_pow2(n: n)) * bitwise_pow2(n: 32 - n) } + } +} + +// Rotate right by n in [0, 64): a rotation by 32 or more swaps the halves first. +fn word64_rotr(a: Word64, n: Int) -> Word64 { + if n >= 32 { + word64_rotr(a: Word64 { hi: a.lo, lo: a.hi }, n: n - 32) + } else if n == 0 { + a + } else { + Word64 { + hi: word32_shr(a: a.hi, n: n) + (a.lo % bitwise_pow2(n: n)) * bitwise_pow2(n: 32 - n), + lo: word32_shr(a: a.lo, n: n) + (a.hi % bitwise_pow2(n: n)) * bitwise_pow2(n: 32 - n), + } + } +} diff --git a/dag/std/bounded_nat.dag b/dag/std/bounded_nat.dag new file mode 100644 index 00000000000..be3e8bb8876 --- /dev/null +++ b/dag/std/bounded_nat.dag @@ -0,0 +1,311 @@ +module std.bounded_nat + +import std.types { Int, Bool, List } +import std.measure { BitWidth, bit_width, bit_width_count } +import std.bitwise { bitwise_pow2 } + +// ARITHMETIC ON BOUNDED NATURALS, AS DECLARED OPERATIONS RATHER THAN INFIX. +// +// std.operator_realization refuses infix + - * / % on a structural operand and says why: structural +// arithmetic is a call to a DECLARED OPERATION whose typed outcome an infix form would hide. The +// bounded naturals of std.integer (Compose>) are structural, so this module is +// the operation family that refusal points at. It is ONE family over a width, never one row per +// operator per type. +// +// WHY THIS IS NOT A SECOND AUTHORITY FOR THE TYPES. std.integer declares WHICH bounded naturals +// exist; this module declares WHAT ARITHMETIC ON ONE MEANS. Reification of the N in MachineWidth +// (operator ruling, 2026-09-20) would let a CALLER stop naming a width; until it lands the width +// arrives as a value and nothing here names one. +// +// REIFICATION IS NOT WHAT STANDS BETWEEN THIS FAMILY AND ITS FIRST CONSUMER, AND SAYING SO WAS A +// TRIGGER STATED AT THE WRONG GRAIN (review 69054 of gunbc#11645; DESIGN 4b(3): a trigger naming +// less than the capability it gates is satisfied while the capability stays dead). The operations +// take a width as a VALUE and the witnesses pass bit_width(count: 32) today, so nothing stops +// std.bitwise passing one too. +// +// THE ACTUAL BLOCKER IS AN IMPORT CYCLE. std.bounded_nat imports std.bitwise for bitwise_pow2, so +// std.bitwise cannot import std.bounded_nat back, and DESIGN 3 makes acyclicity the import graph's +// ONLY structural law -- a wall rather than a preference. It is breakable: relocate bitwise_pow2 +// below both and the cycle is gone. +// +// THE SECOND COST, STATED BESIDE IT so the next reader sees the real shape rather than a one-line +// blocker: after the cycle is broken, every word32_* operation answers a BoundedNatArith, a six-arm +// coproduct, and threading that through SHA-256's 64-round compression fold is the crypto +// restructuring this family's first consumer actually costs. It is deferred to its own change with +// the P-256 suite as its gate (operator-lane ruling, 2026-09-20), in that order -- because the only +// suite covering that fold has never returned a result. +// +// THE DEFECT THIS EXISTS TO REMOVE is gunbc.recurring_failure_mode +// bounded_natural_arithmetic_evaluated_as_unbounded_int: the v1 interpreter evaluates infix +// arithmetic on these types as unbounded Int, so a value outside [0, 2^N) is silently admitted and +// the interpreted and emitted realizations of one program disagree. + +// ── Width admission, decided before any arithmetic ─────────────────────────────────────────── +// THREE ARMS, BECAUSE THE TWO REFUSALS ARE DIFFERENT FACTS. A width with no source constant +// (MachineWidth, whose inhabitants std.integer IntPlatform and UIntPlatform are real +// declarations) is not the same deficit as a constant that does not fit the host integer. Collapsing +// them into one refusal would put two deficits under one name, so neither could rank for repair. +// +// THE HOST BOUND IS 62 BITS: a value must be representable in the substrate's 64-bit signed Int, and +// the sum of two N-bit values needs N + 1 bits, so 2^62 - 1 is the largest admitted magnitude. +// +// WidthNotStatic HAS NO PRODUCER IN THIS MODULE, and that is a declared frontier rather than dead +// code: only reification can report that a MachineWidth's index is PointerWidth rather than a +// literal, so the arm is minted by the binding layer that reads a declaration's width, which cannot +// be written until reification lands. bounded_nat_admit below therefore never returns it, and no +// witness here can exercise it. Stated so a reader does not mistake an unreachable arm for a +// reachable one, and so the binding layer's obligation is visible before it is written. +type BoundedNatAdmission + = WidthAdmitted { bits: BitWidth } + | WidthNotStatic + | WidthExceedsHostInt { bits: BitWidth } + +// The CARRIER bound, stated once: the widest bounded natural this family admits. +fn bounded_nat_host_bit_ceiling() -> Int { + 62 +} + +// THE HOST'S POSITIVE CAPACITY, WHICH IS A DIFFERENT LIMIT AND MUST NOT SHARE A CONSTANT WITH THE +// ONE ABOVE. The carrier ceiling is 62 because a SUM of two N-bit values needs N + 1 bits; the host +// integer itself represents positives up to 2^63 - 1, so an intermediate is representable while its +// bit demand is at most 63. Those two facts are unrelated, and collapsing them cost exactly one +// width: the wrapping split was refusing width 42, whose largest intermediate is 9223367638808264705 +// against a host maximum of 9223372036854775807 -- representable, with room to spare. +// +// THIS IS THE SAME DEFECT THIS FILE REMOVED ONE LEVEL UP, RECURRING (review of gunbc#11645). The +// checked and wrapping products were forced through one admission predicate; splitting them left two +// unrelated LIMITS still sharing one CONSTANT. A predicate that serves two facts is the shape to +// distrust, not the particular pair. +fn bounded_nat_host_positive_bit_capacity() -> Int { + 63 +} + +// WIDTH-EXCEEDS-HOST IS A CEILING WITH A TRIGGER, NOT A TERMINAL DESIGN (DESIGN 4b(2): no untracked +// stall). It is a fact about the HOST integer this family computes in, not about bounded naturals: +// UInt64 and UInt128 are perfectly ordinary bounded naturals whose magnitudes exceed one i64. +// NEXT-RUNG TRIGGER, a capability: arbitrary-precision arithmetic for this family through +// std.bignat's multi-limb naturals, SUFFICIENT FOR UInt64 and UInt128 to be ADMITTED widths whose +// operations carry the same typed outcomes, at which point this arm's population is empty rather +// than refused. std.bignat already carries the limbs and the Montgomery arithmetic that would serve. +// A reified width admitted, or refused with the reason. `bits` is what reification returns for a +// MachineWidth whose index is a literal; a MachineWidth has no constant to reify +// and reaches this as WidthNotStatic, which is a caller's arm to answer rather than a default. +fn bounded_nat_admit(bits: BitWidth) -> BoundedNatAdmission { + if bit_width_count(b: bits) > bounded_nat_host_bit_ceiling() { + WidthExceedsHostInt { bits: bits } + } else { + WidthAdmitted { bits: bits } + } +} + +// The exclusive upper bound of a width: 2^N. +fn bounded_nat_modulus(bits: BitWidth) -> Int { + bitwise_pow2(n: bit_width_count(b: bits)) +} + +// ── The carrier: sole-constructed, its admission the only mint ─────────────────────────────── +// An out-of-width value has NO CONSTRUCTOR. That is the ceiling the failure-mode row names, and it +// is why this is a carrier rather than a bare Int with a check beside it: a check can be bypassed by +// constructing the value another way, and a constructor cannot. +type BoundedNat sole_constructor { + bits: BitWidth + value: Int +} + +type BoundedNatMint + = Minted { n: BoundedNat } + | OutOfWidth { bits: BitWidth, value: Int } + | WidthRefused { cause: BoundedNatAdmission } + +fn bounded_nat(bits: BitWidth, value: Int) -> BoundedNatMint { + match bounded_nat_admit(bits: bits) { + WidthNotStatic => WidthRefused { cause: WidthNotStatic } + WidthExceedsHostInt { bits: b } => WidthRefused { cause: WidthExceedsHostInt { bits: b } } + WidthAdmitted { bits: b } => + if value < 0 || value >= bounded_nat_modulus(bits: b) { + OutOfWidth { bits: b, value: value } + } else { + Minted { n: BoundedNat { bits: b, value: value } } + } + } +} + +// ── The operations ─────────────────────────────────────────────────────────────────────────── +// EVERY ARM IS A FACT THE CALLER MUST ANSWER, and there is no silent wrap anywhere: wrapping exists +// only under its own name below. This is std.integer IntegerOverflowSemantics read at the operation +// grain -- OverflowRaises for the checked operations, OverflowReturns{ReturnWrapping} for the _mod +// pair -- so no third overflow vocabulary is minted here. +// +// WIDTH MISMATCH IS ITS OWN ARM because two bounded naturals of different widths are not the +// operands of one operation. Widening the narrower one silently is exactly the fail-open this family +// exists to remove, so the disagreement is reported rather than resolved. +// +// THE TWO MULTIPLICATIONS ANSWER DIFFERENT QUESTIONS AND NEITHER IS ADMITTED BY WIDTH. A sum of two +// N-bit values needs N + 1 bits. A product would need 2N -- but NEITHER ARM EVER FORMS ONE IT CANNOT +// HOLD, so neither needs 2N of host headroom, and a width-keyed refusal on either was rejecting +// operands whose actual product was small. The checked arm decides overflow by comparison BEFORE +// multiplying; the wrapping arm computes the low N bits by splitting. Each is described where it is +// defined below. +// +// THE WRAPPING PRODUCT NEEDS NO FULL PRODUCT EITHER, AND GIVING IT THE CHECKED CEILING WAS AN OVER-PROHIBITION +// (DESIGN 4d: a mechanism that forbids more than the evidence supports costs the thing you never did). +// Reduction modulo 2^N depends only on the LOW N bits, which a host int can carry for widths the full +// product would overflow. Splitting one operand at h = N / 2 gives the identity +// (a * b) mod 2^N = ((a1 * b) mod 2^(N - h)) * 2^h + a0 * b (mod 2^N), a = a1 * 2^h + a0 +// whose largest intermediates are a0 * b and a1 * b, of h + N and (N - h) + N bits. So UInt32 +// wrapping multiplication is computable here for EVERY pair of operands, including those whose full +// product does not exist on this host -- which is what the checked arm's comparison cannot do, since +// it answers whether a product fits rather than what its low bits are. The two arms are separate +// because they answer different questions, not because one has more headroom than the other. +// +// THE WRAPPING CEILING IS REAL BUT HIGHER, AND IS STATED RATHER THAN ROUNDED. The split admits a +// width only while max(h + N, (N - h) + N) stays inside the HOST'S POSITIVE CAPACITY -- 63, not the +// carrier ceiling of 62 -- which is N <= 42. Width 43 is the first whose worst intermediate genuinely +// does not fit, so 43..62 refuse. +// +// THAT RESIDUAL IS A PROPERTY OF THIS ONE-LEVEL SPLIT, NOT OF BOUNDED NATURALS, AND THE ARM IS NAMED +// FOR THAT. A refusal at width 43 says nothing about the operands: 3 * 5 is 15 there, and calling +// that "product exceeds host int" would state a falsehood about values in order to describe a +// realization's limit, which is anemic modeling in the diagnostic layer. +// +// NEXT-RUNG TRIGGER, a capability, and it names BOTH routes because either suffices: RECURSIVE +// SPLITTING (applying the same identity to the sub-products until every intermediate fits) or +// routing the wrapping product through std.bignat's multi-limb arithmetic -- SUFFICIENT FOR every +// width this carrier admits to have a computable wrapping product, at which point +// bounded_nat_wrapping_product_admitted is constantly true and dissolves along with its arm. +type BoundedNatArith + = Within { n: BoundedNat } + | Overflows { bits: BitWidth } + | NegativeResult { bits: BitWidth } + | DividesByZero + | WidthMismatch { left: BitWidth, right: BitWidth } + | WrappingProductUnavailableAtWidth { bits: BitWidth } + +fn bounded_nat_widths_agree(a: BoundedNat, b: BoundedNat) -> Bool { + bit_width_count(b: a.bits) == bit_width_count(b: b.bits) +} + +fn bounded_nat_in_width(bits: BitWidth, value: Int) -> BoundedNatArith { + if value < 0 { + NegativeResult { bits: bits } + } else if value >= bounded_nat_modulus(bits: bits) { + Overflows { bits: bits } + } else { + Within { n: BoundedNat { bits: bits, value: value } } + } +} + +fn bounded_nat_add(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else { + bounded_nat_in_width(bits: a.bits, value: a.value + b.value) + } +} + +fn bounded_nat_sub(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else { + bounded_nat_in_width(bits: a.bits, value: a.value - b.value) + } +} + +// THE PRE-CHECK DISCIPLINE AND THE DIVISION-BASED BOUND TEST ARE NOT DERIVED HERE. std.checked_arithmetic +// already owns both -- "PRE-CHECK, NEVER POST-CHECK: each function decides whether the operation WOULD +// cross the bound before performing it", realized in checked_int_multiply as a division-based bound +// test per sign quadrant. This is that pattern CONSUMED, not restated: re-deriving it in a second +// module would be the DESIGN 3 fork, and the earlier width-wide rule here was exactly that fork +// wearing a stricter rule (review of gunbc#11645). +// +// WHAT IS GENUINELY LOCAL is only the BOUND. std.checked_arithmetic tests against the HOST's +// representable range; this family tests against the CARRIER's width, 2^N - 1, which is a different +// and smaller bound. The shape of the test is borrowed; the limit it is applied to is this module's +// own fact. `a * b > 2^N - 1` iff `a > (2^N - 1) / b` under integer division, which forms no product, +// and when it admits, the product is bounded by 2^N - 1 -- inside the carrier's admitted width and so +// inside the host's. +// +// THIS REPLACED A WIDTH-KEYED REFUSAL THAT REJECTED VALID PRODUCTS (review of gunbc#11645). The old +// rule asked `2N <= 62` and so refused 40-bit 3 * 3, whose product is 9: it keyed on the TYPE's width +// rather than the OPERANDS' values, which is the over-prohibition arm of DESIGN 4d in its purest +// form -- the refused population was every small product of a wide type. The earlier claim that the +// checked arm "needs the full product in order to detect overflow" was simply false, and the witness +// that asserted the old refusal encoded the defect rather than catching it. +fn bounded_nat_product_overflows(bits: BitWidth, a: Int, b: Int) -> Bool { + b != 0 && a > (bounded_nat_modulus(bits: bits) - 1) / b +} + +fn bounded_nat_mul(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else if bounded_nat_product_overflows(bits: a.bits, a: a.value, b: b.value) { + Overflows { bits: a.bits } + } else { + bounded_nat_in_width(bits: a.bits, value: a.value * b.value) + } +} + +// Division and remainder are total only away from a zero divisor, which is the typed arm an infix +// `/` would have hidden -- the reason std.operator_realization refuses the infix form at all. +fn bounded_nat_div(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else if b.value == 0 { + DividesByZero + } else { + bounded_nat_in_width(bits: a.bits, value: a.value / b.value) + } +} + +fn bounded_nat_rem(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else if b.value == 0 { + DividesByZero + } else { + bounded_nat_in_width(bits: a.bits, value: a.value % b.value) + } +} + +// ── Wrapping, under its own name ───────────────────────────────────────────────────────────── +// THE DECLARED OverflowReturns{ReturnWrapping} ARM. Reduction modulo 2^N is what a hash's word +// arithmetic means -- SHA-256's additions are defined mod 2^32 -- so it is an operation with a name, +// not a silent outcome of the checked one. A caller that wants the checked arm calls the checked +// arm; nothing here decides that for it. +// +// These still refuse on a width disagreement and on a product the host cannot hold, because those +// are not overflow of the DECLARED width: they are the operation being inapplicable. +fn bounded_nat_add_mod(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else { + Within { n: BoundedNat { bits: a.bits, value: (a.value + b.value) % bounded_nat_modulus(bits: a.bits) } } + } +} + +// Admitted while the SPLIT's intermediates fit the host, which is a weaker demand than the checked +// product's 2N; see the note above the carrier for the identity and the residual 42..62 ceiling. +fn bounded_nat_wrapping_product_admitted(bits: BitWidth) -> Bool { + bit_width_count(b: bits) + (bit_width_count(b: bits) - bit_width_count(b: bits) / 2) + <= bounded_nat_host_positive_bit_capacity() +} + +// The low N bits of a product, without ever forming the whole product. +fn bounded_nat_wrapping_product(bits: BitWidth, a: Int, b: Int) -> Int { + let n = bit_width_count(b: bits) + let h = n / 2 + let low_modulus = bitwise_pow2(n: h) + let high_modulus = bitwise_pow2(n: n - h) + let high = ((a / low_modulus) * b) % high_modulus + (high * low_modulus + (a % low_modulus) * b) % bounded_nat_modulus(bits: bits) +} + +fn bounded_nat_mul_mod(a: BoundedNat, b: BoundedNat) -> BoundedNatArith { + if !bounded_nat_widths_agree(a: a, b: b) { + WidthMismatch { left: a.bits, right: b.bits } + } else if !bounded_nat_wrapping_product_admitted(bits: a.bits) { + WrappingProductUnavailableAtWidth { bits: a.bits } + } else { + Within { n: BoundedNat { bits: a.bits, value: bounded_nat_wrapping_product(bits: a.bits, a: a.value, b: b.value) } } + } +} diff --git a/dag/test/claim/bignat_montgomery_witness_test.dag b/dag/test/claim/bignat_montgomery_witness_test.dag new file mode 100644 index 00000000000..cf2b7c03989 --- /dev/null +++ b/dag/test/claim/bignat_montgomery_witness_test.dag @@ -0,0 +1,124 @@ +module test.claim.bignat_montgomery_witness_test + +import std.logic { Bool } +import std.types { Int } +import std.bignat { + BigNat, MontgomeryModulus, + bignat_small, bignat_compare, bignat_is_zero, + montgomery_modulus, montgomery_to, montgomery_from, montgomery_mul, montgomery_add, +} + +// THE PAIRED HALF OF THE sole_constructor WALL ON BigNat AND MontgomeryModulus (review of +// gunbc#11645). The wall establishes that no caller OUTSIDE std.bignat can mint a carrier with +// negative or oversized limbs. It establishes nothing about whether the module's OWN constructions +// preserve the limb invariant they all reason from, and a wall whose protected interior is never +// exercised is specification-without-execution (DESIGN 5). +// +// SO THESE CLAIMS RUN THE REAL PRODUCERS AND READ THEIR ANSWERS. They are deliberately small-modulus +// rather than P-256 sized: the subject is whether Montgomery arithmetic over this carrier returns +// the right residues, which is a property of the limb handling and not of the modulus's size, and a +// P-256 vector costs minutes per verify while these cost seconds. The P-256 suite remains the +// separate, heavier obligation over the curve itself. +// +// WHY A ROUND TRIP IS A DISCRIMINATING CLAIM AND NOT A TAUTOLOGY: montgomery_to multiplies by +// r_squared and montgomery_from multiplies by one, and BOTH run the CIOS reduction. A limb that left +// [0, 2^24) would propagate a wrong carry through that reduction, so the value would not come back. +// +// EVERY INPUT IS THREADED THROUGH ITS REFUSAL RATHER THAN UNWRAPPED. bignat_small now answers +// Optional, and a claim that cannot BUILD its input must FAIL rather than pass -- substituting a +// default here would be the same fabricated-default defect the review found in the curve parameters, +// reproduced in the evidence layer, where it would additionally defeat the claim's own red. + +fn with_modulus(f: fn(MontgomeryModulus) -> Bool) -> Bool { + match bignat_small(n: 97) { + Absent => false + Present { value: m } => f(montgomery_modulus(m: m, width: 3)) + } +} + +fn with2(a: Int, b: Int, f: fn(BigNat, BigNat) -> Bool) -> Bool { + match bignat_small(n: a) { + Absent => false + Present { value: x } => + match bignat_small(n: b) { + Absent => false + Present { value: y } => f(x, y) + } + } +} + +fn with3(a: Int, b: Int, c: Int, f: fn(BigNat, BigNat, BigNat) -> Bool) -> Bool { + with2(a: a, b: b, f: fn(x, y) { + match bignat_small(n: c) { + Absent => false + Present { value: z } => f(x, y, z) + } + }) +} + +fn residues_equal(a: BigNat, b: BigNat) -> Bool { + bignat_compare(a: a, b: b) == 0 +} + +// A value carried into Montgomery form and back is the value it started as. +test fn montgomery_form_round_trips_a_residue() -> Bool { + with_modulus(f: fn(ctx) { + with2(a: 5, b: 5, f: fn(five, same) { + residues_equal(a: montgomery_from(ctx: ctx, a: montgomery_to(ctx: ctx, a: five)), b: same) + }) + }) +} + +// 5 * 7 = 35, and 35 is already reduced modulo 97, so the product survives the round trip unchanged. +test fn montgomery_multiplication_answers_the_residue() -> Bool { + with_modulus(f: fn(ctx) { + with3(a: 5, b: 7, c: 35, f: fn(five, seven, expected) { + let product = montgomery_mul(ctx: ctx, a: montgomery_to(ctx: ctx, a: five), b: montgomery_to(ctx: ctx, a: seven)) + residues_equal(a: montgomery_from(ctx: ctx, a: product), b: expected) + }) + }) +} + +// 20 * 30 = 600 = 6 * 97 + 18, so the reduction must actually reduce rather than return the product. +// This is the case a wrong carry reaches: 600 does not fit in the modulus and 18 is not a prefix of +// it, so an unreduced or mis-carried answer cannot coincide with the right one. +test fn montgomery_multiplication_reduces_past_the_modulus() -> Bool { + with_modulus(f: fn(ctx) { + with3(a: 20, b: 30, c: 18, f: fn(twenty, thirty, expected) { + let product = montgomery_mul(ctx: ctx, a: montgomery_to(ctx: ctx, a: twenty), b: montgomery_to(ctx: ctx, a: thirty)) + residues_equal(a: montgomery_from(ctx: ctx, a: product), b: expected) + }) + }) +} + +// Addition of residues wraps at the modulus: 90 + 20 = 110 = 97 + 13. +test fn montgomery_addition_wraps_at_the_modulus() -> Bool { + with_modulus(f: fn(ctx) { + with3(a: 90, b: 20, c: 13, f: fn(ninety, twenty, expected) { + residues_equal(a: montgomery_add(ctx: ctx, a: ninety, b: twenty), b: expected) + }) + }) +} + +// Zero is carried and recognised rather than confused with an empty limb list. +test fn zero_survives_montgomery_form_and_is_recognised() -> Bool { + with_modulus(f: fn(ctx) { + with2(a: 0, b: 0, f: fn(zero, _unused) { + bignat_is_zero(a: montgomery_from(ctx: ctx, a: montgomery_to(ctx: ctx, a: zero))) + }) + }) +} + +// THE REFUSAL IS REACHABLE AND IS ASSERTED, so bignat_small's new arm is not vocabulary nothing +// produces: a negative has no unsigned representation, and before this change it minted a BigNat +// with a NEGATIVE limb through a public function. +// +// THE UPPER EDGE IS ASSERTED AS AN ADMISSION RATHER THAN A REFUSAL, because no Int can exceed three +// limbs: the largest expressible n is 2^63 - 1, whose top limb is 32767 and so is inside 2^24. That +// is the positive control for the note on bignat_small -- if the top limb ever did escape, this is +// the input that would show it. +test fn bignat_small_refuses_a_negative_and_admits_the_largest_int() -> Bool { + let negative = match bignat_small(n: 0 - 1) { Absent => true Present { value: _ } => false } + let largest = match bignat_small(n: 9223372036854775807) { Absent => false Present { value: _ } => true } + negative && largest +} diff --git a/dag/test/claim/bounded_nat_witness_test.dag b/dag/test/claim/bounded_nat_witness_test.dag new file mode 100644 index 00000000000..f7edc836bf0 --- /dev/null +++ b/dag/test/claim/bounded_nat_witness_test.dag @@ -0,0 +1,160 @@ +module test.claim.bounded_nat_witness_test + +import std.logic { Bool } +import std.types { Int } +import std.measure { BitWidth, bit_width } +import std.bounded_nat { + BoundedNat, BoundedNatMint, Minted, OutOfWidth, WidthRefused, + BoundedNatAdmission, WidthAdmitted, WidthExceedsHostInt, + BoundedNatArith, Within, Overflows, NegativeResult, DividesByZero, WidthMismatch, WrappingProductUnavailableAtWidth, + bounded_nat, bounded_nat_admit, bounded_nat_add, bounded_nat_sub, bounded_nat_mul, + bounded_nat_div, bounded_nat_rem, bounded_nat_add_mod, bounded_nat_mul_mod, +} + +// The widths are SUPPLIED here, as every caller must supply one until reification can read a +// declaration's own width (DESIGN 3's witness rule: the inputs belong at the boundary as values). +fn w32() -> BitWidth { bit_width(count: 32) } +fn w8() -> BitWidth { bit_width(count: 8) } + +// A mint or nothing. The witness never constructs a BoundedNat itself: the carrier is +// sole-constructed, and fabricating one on a failed mint would be the fail-open this family removes. +fn m(bits: BitWidth, value: Int) -> BoundedNat? { + match bounded_nat(bits: bits, value: value) { + Minted { n } => Present { value: n } + OutOfWidth { bits: _, value: _ } => none + WidthRefused { cause: _ } => none + } +} + +// Applies an operation to two mints, or answers Absent if either did not mint. Absent is never a +// pass in the tests below: each asserts the arm it expects. +fn on2(a: BoundedNat?, b: BoundedNat?, f: fn(BoundedNat, BoundedNat) -> BoundedNatArith) -> BoundedNatArith? { + match a { + Absent => none + Present { value: x } => + match b { + Absent => none + Present { value: y } => Present { value: f(x, y) } + } + } +} + +fn arm_is_overflow(r: BoundedNatArith?) -> Bool { + match r { Present { value: Overflows { bits: _ } } => true _ => false } +} + +fn arm_value(r: BoundedNatArith?) -> Int? { + match r { + Present { value: Within { n } } => Present { value: n.value } + _ => none + } +} + +// ── The carrier admits only values inside its width ───────────────────────────────────────── +test fn a_value_inside_the_width_mints_and_one_outside_it_does_not() -> Bool { + let inside = match bounded_nat(bits: w8(), value: 255) { Minted { n } => n.value == 255 _ => false } + let above = match bounded_nat(bits: w8(), value: 256) { OutOfWidth { bits: _, value: v } => v == 256 _ => false } + let below = match bounded_nat(bits: w8(), value: -1) { OutOfWidth { bits: _, value: v } => v == -1 _ => false } + inside && above && below +} + +// A width the host integer cannot hold refuses at admission, and says which of the two refusals it is. +test fn a_width_beyond_the_host_bound_is_refused_as_such() -> Bool { + let admitted = match bounded_nat_admit(bits: w32()) { WidthAdmitted { bits: _ } => true _ => false } + let refused = match bounded_nat_admit(bits: bit_width(count: 64)) { WidthExceedsHostInt { bits: _ } => true _ => false } + let mint_refused = match bounded_nat(bits: bit_width(count: 64), value: 1) { WidthRefused { cause: WidthExceedsHostInt { bits: _ } } => true _ => false } + admitted && refused && mint_refused +} + +// ── Checked arithmetic refuses at the edge rather than wrapping ────────────────────────────── +test fn addition_at_the_top_of_the_width_overflows_rather_than_wrapping() -> Bool { + let ok = arm_value(r: on2(a: m(bits: w32(), value: 4294967294), b: m(bits: w32(), value: 1), f: bounded_nat_add)) == Present { value: 4294967295 } + let over = arm_is_overflow(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 1), f: bounded_nat_add)) + ok && over +} + +test fn subtraction_below_zero_is_a_negative_result_not_a_wrap() -> Bool { + match on2(a: m(bits: w8(), value: 3), b: m(bits: w8(), value: 4), f: bounded_nat_sub) { + Present { value: NegativeResult { bits: _ } } => true + _ => false + } +} + +test fn multiplication_overflowing_the_width_refuses_and_division_by_zero_refuses() -> Bool { + let over = arm_is_overflow(r: on2(a: m(bits: w8(), value: 16), b: m(bits: w8(), value: 16), f: bounded_nat_mul)) + let ok = arm_value(r: on2(a: m(bits: w8(), value: 15), b: m(bits: w8(), value: 17), f: bounded_nat_mul)) == Present { value: 255 } + let div0 = match on2(a: m(bits: w8(), value: 5), b: m(bits: w8(), value: 0), f: bounded_nat_div) { Present { value: DividesByZero } => true _ => false } + let rem0 = match on2(a: m(bits: w8(), value: 5), b: m(bits: w8(), value: 0), f: bounded_nat_rem) { Present { value: DividesByZero } => true _ => false } + let div = arm_value(r: on2(a: m(bits: w8(), value: 7), b: m(bits: w8(), value: 2), f: bounded_nat_div)) == Present { value: 3 } + over && ok && div0 && rem0 && div +} + +// ── Two widths are not the operands of one operation ───────────────────────────────────────── +test fn operands_of_different_widths_refuse_rather_than_widening() -> Bool { + match on2(a: m(bits: w8(), value: 1), b: m(bits: w32(), value: 1), f: bounded_nat_add) { + Present { value: WidthMismatch { left: _, right: _ } } => true + _ => false + } +} + +// ── Wrapping exists only under its own name ───────────────────────────────────────────────── +// The same pair that OVERFLOWS under the checked operation WRAPS here: the discriminating pair for +// the claim that no silent wrap exists. +test fn the_mod_operations_wrap_where_the_checked_ones_refuse() -> Bool { + let wrapped = arm_value(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 1), f: bounded_nat_add_mod)) == Present { value: 0 } + let checked = arm_is_overflow(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 1), f: bounded_nat_add)) + let mul_wrapped = arm_value(r: on2(a: m(bits: w8(), value: 16), b: m(bits: w8(), value: 16), f: bounded_nat_mul_mod)) == Present { value: 0 } + wrapped && checked && mul_wrapped +} + +// A product needs twice the width, so a width the host can hold may still have no admissible product. +test fn a_small_product_of_a_wide_type_is_not_refused_for_its_width() -> Bool { + let w40 = bit_width(count: 40) + let tiny = arm_value(r: on2(a: m(bits: w40, value: 3), b: m(bits: w40, value: 3), f: bounded_nat_mul)) == Present { value: 9 } + let genuinely_over = arm_is_overflow(r: on2(a: m(bits: w40, value: 1048576), b: m(bits: w40, value: 1048576), f: bounded_nat_mul)) + let at_the_edge = arm_value(r: on2(a: m(bits: w40, value: 1099511627775), b: m(bits: w40, value: 1), f: bounded_nat_mul)) == Present { value: 1099511627775 } + tiny && genuinely_over && at_the_edge +} + + +// THE REVIEWER'S SECOND DISCRIMINATING CASE (review of gunbc#11645): 40-bit 3 * 3 is 9, and the +// checked multiplication used to REFUSE it because the old admission keyed on the TYPE's width +// (2N <= 62) rather than the OPERANDS' values. This witness previously asserted that refusal, so it +// encoded the defect instead of catching it; it now asserts the corrected behaviour at three points +// -- a tiny product of a wide type, a genuinely overflowing one, and the exact top of the width. +// +// THE REVIEWER'S FIRST DISCRIMINATING CASE (review of gunbc#11645): does the host-width rule refuse an +// operand that is valid and computable? It did, for the WRAPPING product, and this is the red that +// would have caught it. Both vectors have a 64-bit full product, so neither answer is reachable by +// forming the product on this host -- the split is doing the work, not luck. The paired half is that +// the CHECKED product on the same operands reports Overflows -- not WrappingProductUnavailableAtWidth. The two +// arms give different ANSWERS about the same operands because they are asked different questions: +// the wrapping arm returns the low 32 bits, the checked arm reports that the product left the width. +// Neither refuses for want of host headroom. +test fn the_wrapping_product_is_computed_where_the_checked_one_cannot_be() -> Bool { + let all_ones = arm_value(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 4294967295), f: bounded_nat_mul_mod)) == Present { value: 1 } + let mixed = arm_value(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 3735928559), f: bounded_nat_mul_mod)) == Present { value: 559038737 } + let checked_reports_overflow = arm_is_overflow(r: on2(a: m(bits: w32(), value: 4294967295), b: m(bits: w32(), value: 4294967295), f: bounded_nat_mul)) + all_ones && mixed && checked_reports_overflow +} + +// THE RESIDUAL CEILING IS ASSERTED WITH OPERANDS THAT ACTUALLY REACH IT. An earlier version of this +// witness asserted a REFUSAL at width 42 for 3 * 5, whose product is 15 -- so it certified an +// off-by-one instead of catching it, and it exercised only the admission predicate rather than the +// intermediate bound that predicate is about (review of gunbc#11645). +// +// The admitted edge is therefore near-MAXIMAL width-42 operands: (2^42 - 1)^2 mod 2^42 = 1, whose +// largest split intermediate is 9223367638806167553 against a host maximum of 9223372036854775807. +// That answer is unobtainable by forming the product -- the true product has 84 bits -- so this +// discriminates the split at the exact width where the bound nearly binds. 43 is the first width +// whose worst intermediate genuinely does not fit, and it refuses. +test fn the_wrapping_product_ceiling_sits_between_42_and_43() -> Bool { + let w42 = bit_width(count: 42) + let at_the_edge = arm_value(r: on2(a: m(bits: w42, value: 4398046511103), b: m(bits: w42, value: 4398046511103), f: bounded_nat_mul_mod)) == Present { value: 1 } + let refused = match on2(a: m(bits: bit_width(count: 43), value: 8796093022207), b: m(bits: bit_width(count: 43), value: 8796093022207), f: bounded_nat_mul_mod) { + Present { value: WrappingProductUnavailableAtWidth { bits: _ } } => true + _ => false + } + at_the_edge && refused +} + diff --git a/dag/test/claim/p256_dag_ecdsa_witness_test.dag b/dag/test/claim/p256_dag_ecdsa_witness_test.dag new file mode 100644 index 00000000000..678775f02ee --- /dev/null +++ b/dag/test/claim/p256_dag_ecdsa_witness_test.dag @@ -0,0 +1,110 @@ +module test.claim.p256_dag_ecdsa_witness_test + +import std.logic { Bool } +import std.types { Int, List } +import std.integer { UInt8 } +import std.bytes { bytes_octets, utf8_encode_bytes } +import std.bignat { BigNat, bignat_zero_limbs } +import extdeps.crypto.nist_p256 { p256_ecdsa_verify_octets, p256_on_curve, p256_gx, p256_gy, p256_n, p256_double_scalar, p256_affine, p256_is_infinity } + +fn ascii(s: String) -> List { + bytes_octets(b: utf8_encode_bytes(s: s)) +} + +fn is_true(v: Bool?) -> Bool { + match v { + Present { value: b } => b + Absent => false + } +} + +fn is_false(v: Bool?) -> Bool { + match v { + Present { value: b } => !b + Absent => false + } +} + +fn is_absent(v: Bool?) -> Bool { + match v { + Present { value: _ } => false + Absent => true + } +} + +// ── The parameters themselves ──────────────────────────────────────────────────────────────── +// G is on the curve, and n·G is the point at infinity: the published constants are the curve's. +test fn the_base_point_is_on_the_curve_and_has_order_n() -> Bool { + let zero = p256_hex_zero() + p256_on_curve(x: p256_gx, y: p256_gy) + && p256_is_infinity(p: p256_double_scalar(u1: p256_n, g: p256_affine(x: p256_gx, y: p256_gy), u2: zero, q: p256_affine(x: p256_gx, y: p256_gy))) +} + +// The scalar zero, from the total constructor rather than the refusing mint: bignat_small now +// answers Optional, and a witness that unwrapped it with a default would reintroduce here exactly +// the fabricated default this file was corrected for (review 69034 of gunbc#11645). +fn p256_hex_zero() -> BigNat { + bignat_zero_limbs() +} + +// ── RFC 6979 §A.2.5: a published P-256 / SHA-256 key and two signatures ───────────────────── +data rfc6979_key: List = [4, 96, 254, 212, 186, 37, 90, 157, 49, 201, 97, 235, 116, 198, 53, 109, 104, 192, 73, 184, 146, 59, 97, 250, 108, 230, 105, 98, 46, 96, 242, 159, 182, 121, 3, 254, 16, 8, 184, 188, 153, 164, 26, 233, 233, 86, 40, 188, 100, 242, 241, 178, 12, 45, 126, 159, 81, 119, 163, 194, 148, 212, 70, 34, 153] +data rfc6979_sample_sig: List = [239, 212, 139, 42, 172, 182, 168, 253, 17, 64, 221, 156, 212, 94, 129, 214, 157, 44, 135, 123, 86, 170, 249, 145, 195, 77, 14, 168, 78, 175, 55, 22, 247, 203, 28, 148, 45, 101, 124, 65, 212, 54, 199, 161, 182, 226, 159, 101, 243, 233, 0, 219, 185, 175, 244, 6, 77, 196, 171, 47, 132, 58, 205, 168] +data rfc6979_test_sig: List = [241, 171, 176, 35, 81, 131, 81, 205, 113, 216, 129, 86, 123, 30, 166, 99, 237, 62, 252, 246, 197, 19, 43, 53, 79, 40, 211, 176, 183, 211, 131, 103, 1, 159, 65, 19, 116, 42, 43, 20, 189, 37, 146, 107, 73, 198, 73, 21, 95, 38, 126, 96, 211, 129, 75, 76, 12, 200, 66, 80, 228, 111, 0, 131] + +test fn the_rfc6979_sample_signature_verifies() -> Bool { + is_true(v: p256_ecdsa_verify_octets(key: rfc6979_key, signature: rfc6979_sample_sig, message: ascii(s: "sample"))) +} + +test fn the_rfc6979_test_signature_verifies() -> Bool { + is_true(v: p256_ecdsa_verify_octets(key: rfc6979_key, signature: rfc6979_test_sig, message: ascii(s: "test"))) +} + +// The "sample" signature presented for "test": well-formed, and false. +test fn a_signature_for_a_different_message_is_false() -> Bool { + is_false(v: p256_ecdsa_verify_octets(key: rfc6979_key, signature: rfc6979_sample_sig, message: ascii(s: "test"))) +} + +// The RFC 7515 A.3 key under the RFC 6979 signature: the wrong key, false. +test fn the_wrong_key_is_false() -> Bool { + is_false(v: p256_ecdsa_verify_octets(key: [4, 127, 205, 206, 39, 112, 246, 196, 93, 65, 131, 203, 238, 111, 219, 75, 123, 88, 7, 51, 53, 123, 233, 239, 19, 186, 207, 110, 60, 123, 209, 84, 69, 199, 241, 68, 205, 27, 189, 155, 126, 135, 44, 223, 237, 185, 238, 185, 244, 179, 105, 93, 110, 169, 11, 36, 173, 138, 70, 35, 40, 133, 136, 229, 173], signature: rfc6979_sample_sig, message: ascii(s: "sample"))) +} + +// The RFC key with the last bit of y flipped: 65 octets, 0x04, and not a point on the curve. +test fn a_point_off_the_curve_is_absent() -> Bool { + is_absent(v: p256_ecdsa_verify_octets(key: [4, 96, 254, 212, 186, 37, 90, 157, 49, 201, 97, 235, 116, 198, 53, 109, 104, 192, 73, 184, 146, 59, 97, 250, 108, 230, 105, 98, 46, 96, 242, 159, 182, 121, 3, 254, 16, 8, 184, 188, 153, 164, 26, 233, 233, 86, 40, 188, 100, 242, 241, 178, 12, 45, 126, 159, 81, 119, 163, 194, 148, 212, 70, 34, 152], signature: rfc6979_sample_sig, message: ascii(s: "sample"))) +} + +// ── Wycheproof ecdsa_secp256r1_sha256_p1363_test.json ─────────────────────────────────────── +data wycheproof_key: List = [4, 41, 39, 177, 5, 18, 186, 227, 237, 220, 254, 70, 120, 40, 18, 139, 173, 41, 3, 38, 153, 25, 247, 8, 96, 105, 200, 196, 223, 108, 115, 40, 56, 199, 120, 121, 100, 234, 172, 0, 229, 146, 31, 177, 73, 138, 96, 244, 96, 103, 102, 179, 217, 104, 80, 1, 85, 141, 26, 151, 78, 115, 65, 81, 62] +data wycheproof_msg: List = [49, 50, 51, 52, 48, 48] + +// tcId 1, valid: the high-s form. ECDSA verification has no low-s rule, so it verifies. +test fn wycheproof_1_the_malleable_signature_verifies() -> Bool { + is_true(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [43, 163, 168, 190, 107, 148, 213, 236, 128, 166, 217, 209, 25, 10, 67, 110, 255, 229, 13, 133, 161, 238, 232, 89, 184, 204, 106, 249, 189, 92, 46, 24, 76, 214, 11, 133, 93, 68, 47, 91, 60, 123, 17, 235, 108, 78, 10, 231, 82, 95, 231, 16, 250, 185, 170, 124, 119, 166, 127, 121, 230, 250, 221, 118], message: wycheproof_msg)) +} + +// tcId 60, valid: an edge case for Shamir multiplication. +test fn wycheproof_60_the_shamir_edge_case_verifies() -> Bool { + is_true(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [100, 161, 170, 181, 0, 13, 14, 128, 79, 62, 47, 192, 43, 222, 233, 190, 143, 243, 18, 51, 78, 43, 161, 109, 17, 84, 124, 151, 113, 28, 137, 142, 106, 240, 21, 151, 28, 195, 11, 230, 209, 162, 6, 212, 224, 19, 224, 153, 119, 114, 162, 249, 29, 115, 40, 111, 253, 104, 59, 155, 178, 207, 79, 27], message: [54, 57, 56, 49, 57])) +} + +// tcId 4, invalid: r replaced by n - r. Well-formed, so the answer is false. +test fn wycheproof_4_n_minus_r_is_false() -> Bool { + is_false(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [212, 92, 87, 64, 148, 107, 42, 20, 127, 89, 38, 46, 230, 245, 188, 144, 189, 1, 237, 40, 5, 40, 182, 43, 58, 237, 95, 201, 63, 6, 247, 57, 179, 41, 244, 121, 162, 187, 208, 165, 195, 132, 238, 20, 147, 177, 245, 24, 106, 135, 19, 156, 172, 93, 244, 8, 124, 19, 75, 73, 21, 104, 71, 219], message: wycheproof_msg)) +} + +// tcId 11, invalid: r = 0 and s = 0, outside [1, n-1]. +test fn wycheproof_11_r_and_s_zero_are_absent() -> Bool { + is_absent(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], message: wycheproof_msg)) +} + +// tcId 26, invalid: r = n, outside [1, n-1]. +test fn wycheproof_26_r_equal_to_n_is_absent() -> Bool { + is_absent(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [255, 255, 255, 255, 0, 0, 0, 0, 255, 255, 255, 255, 255, 255, 255, 255, 188, 230, 250, 173, 167, 23, 158, 132, 243, 185, 202, 194, 252, 99, 37, 81, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], message: wycheproof_msg)) +} + +// tcId 2, invalid: r replaced by r + n, which needs 33 octets -- not the 64-octet encoding. +test fn wycheproof_2_r_plus_n_is_absent() -> Bool { + is_absent(v: p256_ecdsa_verify_octets(key: wycheproof_key, signature: [1, 43, 163, 168, 189, 107, 148, 213, 237, 128, 166, 217, 209, 25, 10, 67, 110, 188, 204, 8, 51, 73, 6, 134, 222, 172, 134, 53, 188, 185, 191, 83, 105, 0, 179, 41, 244, 121, 162, 187, 208, 165, 195, 132, 238, 20, 147, 177, 245, 24, 106, 135, 19, 156, 172, 93, 244, 8, 124, 19, 75, 73, 21, 104, 71, 219], message: wycheproof_msg)) +} diff --git a/dag/test/claim/sha256_fips_witness_test.dag b/dag/test/claim/sha256_fips_witness_test.dag new file mode 100644 index 00000000000..bcc815310a7 --- /dev/null +++ b/dag/test/claim/sha256_fips_witness_test.dag @@ -0,0 +1,54 @@ +module test.claim.sha256_fips_witness_test + +import std.logic { Bool } +import std.types { Int, List } +import std.integer { UInt8 } +import std.bytes { bytes_octets, utf8_encode_bytes } +import std.bitwise { word32_and, word32_xor, word32_or, word32_not, word32_add, word32_rotr, word32_shr, Word64, word64_add, word64_rotr, word64_xor } +import extdeps.crypto.sha2 { sha256_hex } + +fn ascii(s: String) -> List { + bytes_octets(b: utf8_encode_bytes(s: s)) +} + +// ── std.bitwise against values computed by an independent implementation (Python int ops) ───── +test fn word32_xor_and_or_not_match_the_bit_definitions() -> Bool { + word32_xor(a: 305419896, b: 2596069104) == 2290649224 + && word32_and(a: 305419896, b: 2596069104) == 305419888 + && word32_or(a: 0, b: 4294967295) == 4294967295 + && word32_not(a: 0) == 4294967295 + && word32_add(a: 4294967295, b: 2) == 1 +} + +test fn word32_rotr_moves_the_low_bits_to_the_top() -> Bool { + word32_rotr(a: 305419896, n: 7) == 4028917932 && word32_shr(a: 305419896, n: 7) == 2386092 +} + +// 64-bit: the carry crosses the halves, and a rotation by 32 or more swaps them. +test fn word64_add_carries_across_the_halves_and_rotr_swaps_them() -> Bool { + let all_ones = Word64 { hi: 4294967295, lo: 4294967295 } + let one = Word64 { hi: 0, lo: 1 } + let sum = word64_add(a: all_ones, b: one) + let r = word64_rotr(a: Word64 { hi: 1, lo: 0 }, n: 33) + let x = word64_xor(a: all_ones, b: one) + sum.hi == 0 && sum.lo == 0 && r.hi == 2147483648 && r.lo == 0 && x.hi == 4294967295 && x.lo == 4294967294 +} + +// ── SHA-256: FIPS 180-2 Appendix B, the published examples ──────────────────────────────────── +test fn sha256_of_the_empty_message_is_the_published_value() -> Bool { + sha256_hex(message: []) == "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" +} + +test fn sha256_of_abc_is_the_published_one_block_value() -> Bool { + sha256_hex(message: ascii(s: "abc")) == "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +} + +// 448 bits: the padding no longer fits the first block, so this is the two-block path. +test fn sha256_of_the_448_bit_message_is_the_published_two_block_value() -> Bool { + sha256_hex(message: ascii(s: "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == "248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1" +} + +// One changed octet changes the digest: the discriminating red for the vectors above. +test fn sha256_of_a_one_octet_change_is_a_different_digest() -> Bool { + sha256_hex(message: ascii(s: "abd")) != "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +}