code wiki / (root) / nx_p256_solinas_difftest.nx
`nx_p256_solinas_difftest.nx` source

↩ module page · 456 lines · 14053 B
1// nx_p256_solinas_difftest.nx -- DIFFERENTIAL correctness gate for the
2// NIST P-256 Solinas fast reduction used by TLS ECDSA certificate verify.
3//
4// It proves the FAST Solinas reduction (_p256_solinas_reduce, reached via
5// the public p256_field_reduce_solinas) is BIT-IDENTICAL, in every one of
6// the 8 output limbs, to a trivially-correct bit-serial long-division
7// reduction mod p -- over the FULL 512-bit product domain:
8//   * >= 2000 deterministic LCG-random 512-bit products (seeded from the
9//     loop index; NO Date.now/random -- the .nx runtime forbids them), and
10//   * the exact reduction boundary values: 0, p-1, p, p+1, 2p-1, 2p, 2p+1,
11//     3p, 2^256-1, 2^256, (p-1)^2, p^2, p<<256, 2^512-1, 2^512-2, 2^512-1-p.
12// Plus an end-to-end cross-check: p256_field_mul (fast) == p256_field_mul_slow
13// (the retained bit-serial oracle) over random a,b.
14//
15// WHY THIS MATTERS: this reduction is on the cert-verify hot path
16// (p256_field_mul -> point add/double -> scalar mul -> ECDSA verify).  A
17// single wrong reduction could let a FORGED signature verify.  The test
18// exits 0 ONLY if EVERY input is bit-identical; any mismatch exits 1.
19//
20// ORACLE INDEPENDENCE: the bit-serial oracle here (_dt_oracle_reduce) shares
21// ZERO code with _p256_solinas_reduce except the prime-constant loader
22// p256_field_load_p (both must reduce mod the same p).  It is the SAME
23// algorithm p256_field_mul_slow uses for its reduction step; the end-to-end
24// section cross-checks it against p256_field_mul_slow so a faithful
25// transcription is proven, not assumed.
26//
27// NOTE ON PREMISE: the Solinas reduction ALREADY existed and was ALREADY
28// wired into p256_field_mul before this test (commit "ECDSA-P256 §1c").
29// This organ ADDS a far stronger correctness proof (>= 2000 random + full
30// boundary set) than the pre-existing 606-case oracle test; it modifies no
31// production logic.
32//
33// expect_exit: 0
34// license_tier: ORIGINAL
35
36import "nx_syscalls.nx"
37import "nx_u256.nx"
38import "nx_u256_mul.nx"
39import "nx_p256_field.nx"
40import "nx_p256_field_mul.nx"
41const K_MAGIC_2500: i64 = 2500
42const K_MAGIC_2654435761: i64 = 2654435761
43const K_MAGIC_1013904223: i64 = 1013904223
44const K_MAGIC_1103515245: i64 = 1103515245
45const K_MAGIC_12345: i64 = 12345
46const K_MAGIC_40503: i64 = 40503
47
48// ---- bounded decimal printer (self-contained; no runtime import) ----
49func _dt_print_dec(n: i64) -> i64 {
  let out: *u8 = sys_mmap(32)
  if n == 0 {
      out[0] = 48 as u8
      sys_write(1, out, 1)
      return 0
  }
  let tmp: *u8 = sys_mmap(32)
  var v: i64 = n
  var i: i64 = 0
  while v > 0 {
      let d: i64 = v - (v / 10) * 10
      tmp[i] = (48 + d) as u8
      v = v / 10
      i = i + 1
  }
  var j: i64 = 0
  while i > 0 {
      i = i - 1
      out[j] = tmp[i]
      j = j + 1
  }
  sys_write(1, out, j)
  return 0
73}
74
75// ---- independent bit-serial oracle: out8 = c16 mod p ----
76// Repeated conditional subtract of (p << k) for k = 256 down to 0 -- plain
77// schoolbook long division.  Uses ONLY compare/subtract/shift on 16 limbs
78// (u256_wide_cmp / u256_wide_sub / u256_wide_shr_1), none of which is part
79// of the Solinas path under test.
80func _dt_oracle_reduce(out8: *i64, c16: *i64) -> i64 {
  let _m: i64 = nx_scratch_save()
  let work: *i64 = u256_wide_alloc()
  let shp: *i64 = u256_wide_alloc()
  let p: *i64 = u256_alloc()
  p256_field_load_p(p)
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      work[i] = c16[i] & NX_U256_LIMB_MASK
      i = i + 1
  }
  i = 0
  while i < NX_U256_WIDE_LIMBS {
      shp[i] = 0
      i = i + 1
  }
  i = 0
  while i < NX_U256_LIMBS {
      shp[i + 8] = p[i] & NX_U256_LIMB_MASK
      i = i + 1
  }
  var k: i64 = 0
  while k < 257 {
      if u256_wide_cmp(work, shp) >= 0 {
          u256_wide_sub(work, work, shp)
      }
      u256_wide_shr_1(shp)
      k = k + 1
  }
  i = 0
  while i < NX_U256_LIMBS {
      out8[i] = work[i] & NX_U256_LIMB_MASK
      i = i + 1
  }
  nx_scratch_restore(_m)
  return 0
116}
117
118// 8-limb equality (1 == equal, 0 == differ).
119func _dt_eq8(a: *i64, b: *i64) -> i64 {
  var i: i64 = 0
  while i < NX_U256_LIMBS {
      if (a[i] & NX_U256_LIMB_MASK) != (b[i] & NX_U256_LIMB_MASK) {
          return 0
      }
      i = i + 1
  }
  return 1
128}
129
130// Reduce c16 with BOTH paths; return 0 if bit-identical, 1 if any limb differs.
131func _dt_check_c(c16: *i64, fast: *i64, oracle: *i64) -> i64 {
  p256_field_reduce_solinas(fast, c16)
  _dt_oracle_reduce(oracle, c16)
  if _dt_eq8(fast, oracle) == 1 {
      return 0
  }
  return 1
138}
139
140// ---- 16-limb helpers for building boundary inputs ----
141func _dt_zero16(c: *i64) -> i64 {
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      c[i] = 0
      i = i + 1
  }
  return 0
148}
149
150func _dt_copy16(dst: *i64, src: *i64) -> i64 {
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      dst[i] = src[i] & NX_U256_LIMB_MASK
      i = i + 1
  }
  return 0
157}
158
159// dst (16-limb) += src (16-limb), in place.  High-order carry-out dropped
160// (all callers keep the sum < 2^512).
161func _dt_add16(dst: *i64, src: *i64) -> i64 {
  var carry: i64 = 0
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      let s: i64 = (dst[i] & NX_U256_LIMB_MASK) + (src[i] & NX_U256_LIMB_MASK) + carry
      dst[i] = s & NX_U256_LIMB_MASK
      carry = (s >> NX_U256_LIMB_BITS) & 1
      i = i + 1
  }
  return 0
171}
172
173// c (16-limb) += small scalar in [0, 2^32), in place.
174func _dt_add_small(c: *i64, val: i64) -> i64 {
  var carry: i64 = val & NX_U256_LIMB_MASK
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      if carry == 0 {
          i = NX_U256_WIDE_LIMBS
      } else {
          let s: i64 = (c[i] & NX_U256_LIMB_MASK) + carry
          c[i] = s & NX_U256_LIMB_MASK
          carry = s >> NX_U256_LIMB_BITS
          i = i + 1
      }
  }
  return 0
188}
189
190// c (16-limb) -= small scalar in [0, 2^32), in place.  Caller guarantees
191// no underflow below zero.
192func _dt_sub_small(c: *i64, val: i64) -> i64 {
  var borrow: i64 = val & NX_U256_LIMB_MASK
  var i: i64 = 0
  while i < NX_U256_WIDE_LIMBS {
      if borrow == 0 {
          i = NX_U256_WIDE_LIMBS
      } else {
          let d: i64 = (c[i] & NX_U256_LIMB_MASK) - borrow
          if d < 0 {
              c[i] = (d + (1 << NX_U256_LIMB_BITS)) & NX_U256_LIMB_MASK
              borrow = 1
          } else {
              c[i] = d & NX_U256_LIMB_MASK
              borrow = 0
          }
          i = i + 1
      }
  }
  return 0
211}
212
213// Run one boundary case: check c16, bump counters. Returns updated fails.
214// (Helper kept out; counters live in main for clarity.)
215
216func main() -> i64 {
  let _s0: i64 = nx_scratch_save()
218
  let p: *i64 = u256_alloc()
  p256_field_load_p(p)
221
  // Persistent working buffers (allocated ONCE; both reducers frame and
  // reclaim their own temporaries internally, so the arena never grows
  // across the loops below).
  let c16: *i64 = u256_wide_alloc()
  let fast: *i64 = u256_alloc()
  let oracle: *i64 = u256_alloc()
228
  var total: i64 = 0
  var fails: i64 = 0
231
  // ================================================================
  // 1) >= 2000 LCG-random 512-bit products, deterministically seeded
  //    from the loop index.  Each of 16 limbs gets a fresh 32-bit LCG
  //    output, covering the full 512-bit domain.
  // ================================================================
  let NRAND: i64 = K_MAGIC_2500
  var idx: i64 = 0
  while idx < NRAND {
      var st: i64 = (idx * K_MAGIC_2654435761 + K_MAGIC_1013904223) & NX_U256_LIMB_MASK
      var k: i64 = 0
      while k < NX_U256_WIDE_LIMBS {
          st = (st * K_MAGIC_1103515245 + K_MAGIC_12345) & NX_U256_LIMB_MASK
          c16[k] = st
          k = k + 1
      }
      fails = fails + _dt_check_c(c16, fast, oracle)
      total = total + 1
      idx = idx + 1
  }
251
  // ================================================================
  // 2) Explicit boundary inputs.
  // ================================================================
  // p as a 16-limb value (low 8 limbs = p, high 8 = 0).
  let pw: *i64 = u256_wide_alloc()
  _dt_zero16(pw)
  var bi: i64 = 0
  while bi < NX_U256_LIMBS {
      pw[bi] = p[bi] & NX_U256_LIMB_MASK
      bi = bi + 1
  }
263
  // 0
  _dt_zero16(c16)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
268
  // p
  _dt_copy16(c16, pw)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
273
  // p - 1
  _dt_copy16(c16, pw)
  _dt_sub_small(c16, 1)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
279
  // p + 1
  _dt_copy16(c16, pw)
  _dt_add_small(c16, 1)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
285
  // 2p
  _dt_copy16(c16, pw)
  _dt_add16(c16, pw)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
291
  // 2p - 1
  _dt_copy16(c16, pw)
  _dt_add16(c16, pw)
  _dt_sub_small(c16, 1)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
298
  // 2p + 1
  _dt_copy16(c16, pw)
  _dt_add16(c16, pw)
  _dt_add_small(c16, 1)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
305
  // 3p  (stresses the reduce9 multi-subtract loop)
  _dt_copy16(c16, pw)
  _dt_add16(c16, pw)
  _dt_add16(c16, pw)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
312
  // 2^256 - 1  (low 8 limbs all ones)
  _dt_zero16(c16)
  var i2: i64 = 0
  while i2 < NX_U256_LIMBS {
      c16[i2] = NX_U256_LIMB_MASK
      i2 = i2 + 1
  }
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
322
  // 2^256  (limb 8 = 1)
  _dt_zero16(c16)
  c16[8] = 1
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
328
  // 2^512 - 1  (all 16 limbs all ones)
  var i3: i64 = 0
  while i3 < NX_U256_WIDE_LIMBS {
      c16[i3] = NX_U256_LIMB_MASK
      i3 = i3 + 1
  }
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
337
  // 2^512 - 2
  var i4: i64 = 0
  while i4 < NX_U256_WIDE_LIMBS {
      c16[i4] = NX_U256_LIMB_MASK
      i4 = i4 + 1
  }
  c16[0] = 0xFFFFFFFE
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
347
  // 2^512 - 1 - p  (all ones minus p)
  var i5: i64 = 0
  while i5 < NX_U256_WIDE_LIMBS {
      c16[i5] = NX_U256_LIMB_MASK
      i5 = i5 + 1
  }
  u256_wide_sub(c16, c16, pw)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
357
  // (p - 1)^2  -- the maximum real field product (via the production wide mul)
  let pm1: *i64 = u256_alloc()
  u256_copy(pm1, p)
  var bpm: i64 = 1
  var jpm: i64 = 0
  while jpm < NX_U256_LIMBS {
      let d: i64 = (pm1[jpm] & NX_U256_LIMB_MASK) - bpm
      if d < 0 {
          pm1[jpm] = (d + (1 << NX_U256_LIMB_BITS)) & NX_U256_LIMB_MASK
          bpm = 1
      } else {
          pm1[jpm] = d & NX_U256_LIMB_MASK
          bpm = 0
      }
      jpm = jpm + 1
  }
  u256_mul_wide(c16, pm1, pm1)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
377
  // p^2  (reduces to 0)
  u256_mul_wide(c16, p, p)
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
382
  // p << 256  (high 8 limbs = p, low 8 = 0; reduces to 0)
  _dt_zero16(c16)
  var i6: i64 = 0
  while i6 < NX_U256_LIMBS {
      c16[i6 + 8] = p[i6] & NX_U256_LIMB_MASK
      i6 = i6 + 1
  }
  fails = fails + _dt_check_c(c16, fast, oracle)
  total = total + 1
392
  // ================================================================
  // 3) End-to-end cross-check on the ACTUAL production functions:
  //    p256_field_mul (fast) == p256_field_mul_slow (bit-serial oracle)
  //    over random a,b.  Also confirms the standalone _dt_oracle_reduce
  //    matches the retained slow path (faithful-transcription check).
  // ================================================================
  let a: *i64 = u256_alloc()
  let b: *i64 = u256_alloc()
  let e_fast: *i64 = u256_alloc()
  let e_slow: *i64 = u256_alloc()
  let e_orac: *i64 = u256_alloc()
  let cab: *i64 = u256_wide_alloc()
  var e: i64 = 0
  while e < 600 {
      var sa: i64 = (e * K_MAGIC_40503 + K_MAGIC_12345) & NX_U256_LIMB_MASK
      var ka: i64 = 0
      while ka < NX_U256_LIMBS {
          sa = (sa * K_MAGIC_1103515245 + K_MAGIC_12345) & NX_U256_LIMB_MASK
          a[ka] = sa
          ka = ka + 1
      }
      var sb: i64 = (e * K_MAGIC_2654435761 + 7) & NX_U256_LIMB_MASK
      var kb: i64 = 0
      while kb < NX_U256_LIMBS {
          sb = (sb * K_MAGIC_1103515245 + K_MAGIC_12345) & NX_U256_LIMB_MASK
          b[kb] = sb
          kb = kb + 1
      }
      p256_field_mul(e_fast, a, b)
      p256_field_mul_slow(e_slow, a, b)
      if _dt_eq8(e_fast, e_slow) == 0 {
          fails = fails + 1
      }
      total = total + 1
      // faithful-transcription check: my oracle on the same product
      u256_mul_wide(cab, a, b)
      _dt_oracle_reduce(e_orac, cab)
      if _dt_eq8(e_orac, e_slow) == 0 {
          fails = fails + 1
      }
      total = total + 1
      e = e + 1
  }
436
  // ================================================================
  // Verdict.
  // ================================================================
  if fails == 0 {
      sys_write(1, "=== difftest PASS " as *u8, 18)
      _dt_print_dec(total)
      sys_write(1, "/" as *u8, 1)
      _dt_print_dec(total)
      sys_write(1, "\n" as *u8, 1)
      nx_scratch_restore(_s0)
      return 0
  }
  sys_write(1, "=== difftest FAIL " as *u8, 18)
  _dt_print_dec(fails)
  sys_write(1, " of " as *u8, 4)
  _dt_print_dec(total)
  sys_write(1, " mismatched\n" as *u8, 12)
  nx_scratch_restore(_s0)
  return 1
456}
nx_p256_solinas_difftest.nx source

`nx_p256_solinas_difftest.nx` source
