code wiki / _hdl_build / nx_ed25519_extvec_gate.nx
`nx_ed25519_extvec_gate.nx` source

↩ module page · 201 lines · 8927 B
1// nx_ed25519_extvec_gate.nx -- SECOND provably third-party-validated claim: Ed25519 vs RFC 8032 7.1.
2//
3// Same construction as nx_x25519_extvec_gate, applied to a different authority to prove the pattern
4// GENERALISES rather than being a one-off:
5//   1 no expected value appears in this source -- the public key, message and signature are read at run
6//     time out of knowledge/extvec/rfc8032.txt;
7//   2 that file is PINNED to the sha256 nx_vecfetch computed IN-PROCESS at the socket, before the bytes
8//     touched disk (e3705131.., independently confirmed by GNU coreutils sha256sum);
9//   3 only then does ed25519_verify_full() run against the document's own signature.
10// ★The pin is the security property. Parsing from a file is necessary but not sufficient -- an edited file
11// would let us grade ourselves against answers of our own choosing. Pinning to an ACQUISITION-time digest
12// is what makes it evidence.
13//
14// SCOPE STATED HONESTLY: this proves our Ed25519 VERIFIER accepts the IETF's own signature over the IETF's
15// own message under the IETF's own public key. It does NOT prove our SIGNER produces those bytes -- that is
16// a separate claim needing the secret-key vector, and it is deliberately not asserted here.
17// license_tier: ORIGINAL  expect_exit: 0
18import "nx_syscalls.nx"
19import "nx_sha256_wasm.nx"
20import "nx_ed25519_signature.nx"
21import "nx_gate_verdict.nx"
22
23func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
24func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 }
25
26func nn(v: i64) -> i64 {
  var m: i64 = v
  if m < 0 { w("-" as *u8); m = 0 - m }
  let t: *u8 = sys_mmap(32)
  var k: i64 = 0
  if m == 0 { t[0] = 48 as u8; k = 1 }
  while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  let b: *u8 = sys_mmap(32)
  var j: i64 = 0
  while j < k { b[j] = t[k - 1 - j]; j = j + 1 }
  sys_write(1, b, k)
  return 0
38}
39
40func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v }
41
42func hexval(c: i64) -> i64 {
  if c >= 48 { if c <= 57 { return c - 48 } }
  if c >= 97 { if c <= 102 { return c - 87 } }
  if c >= 65 { if c <= 70 { return c - 55 } }
  return 0 - 1
47}
48
49func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 {
  var i: i64 = 0
  while s[i] != (0 as u8) {
      if at + i >= n { return 0 }
      if b[at + i] != s[i] { return 0 }
      i = i + 1
  }
  return 1
57}
58
59func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 {
  var p: i64 = from
  while p < n {
      if starts(b, n, p, s) == 1 { return p }
      p = p + 1
  }
  return 0 - 1
66}
67
68// Decode exactly `want` bytes of hex starting at the first hex run at/after `from`.
69// STRICT: a short run returns -1 rather than a partial value -- a truncated key or signature must fail
70// loudly, never be compared as if complete.
71func parsehex(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64 {
  // ⚠RFC 8032 WRAPS EACH VALUE ACROSS TWO 32-CHAR LINES. My first cut reset the accumulator on ANY
  // non-hex byte -- which the newline between those lines is -- so a 64-hex key parsed as "short/absent"
  // and the gate went RED against a perfectly good document. ★The RED was honest and the parser was wrong:
  // a strict rule that cannot read the authority's own layout reports its own blindness as the source's
  // defect. Fix: WHITESPACE CONTINUES a run; any other non-hex byte still resets it, so the strictness
  // that rejects genuinely short values is preserved.
  var p: i64 = from
  var got: i64 = 0
  while p < n {
      if got >= want { return p }
      let c0: i64 = b[p] as i64
      var ws: i64 = 0
      if c0 == 32 { ws = 1 }
      if c0 == 10 { ws = 1 }
      if c0 == 13 { ws = 1 }
      if c0 == 9 { ws = 1 }
      let hv: i64 = hexval(c0)
      if ws == 1 { p = p + 1 }
      else { if hv < 0 {
          if got > 0 { if got < want { got = 0 } }
          p = p + 1
      } else {
          if p + 1 >= n { return 0 - 1 }
          let hv2: i64 = hexval(b[p + 1] as i64)
          if hv2 < 0 { p = p + 1 }
          else {
              out[got] = ((hv * 16) + hv2) as u8
              got = got + 1
              p = p + 2
          }
      } }
  }
  if got >= want { return p }
  return 0 - 1
106}
107
108func main() -> i64 {
  w("nx_ed25519_extvec_gate -- Ed25519 vs RFC 8032 7.1, vectors READ FROM THE FETCHED DOCUMENT\n" as *u8)
110
  let lp: *i64 = sys_mmap(16) as *i64
  lp[0] = 0
  let b: *u8 = sys_read_file("knowledge/extvec/rfc8032.txt\x00" as *u8, lp)
  if lp[0] <= 0 {
      w("RED: fetched vector file absent -- run nx_vecfetch. NOT falling back to constants.\n" as *u8)
      return 1
  }
118
  // ---- CLAUSE 1: PIN THE ACQUISITION ----
  let ctx: *u8 = sys_mmap(1024)
  let dig: *u8 = sys_mmap(64)
  nx_sha256_one_shot(b, lp[0], ctx, dig)
  let hx: *u8 = sys_mmap(80)
  var i: i64 = 0
  while i < 32 {
      hx[i * 2] = hexnib(((dig[i] as i64) / 16) & 15) as u8
      hx[i * 2 + 1] = hexnib((dig[i] as i64) & 15) as u8
      i = i + 1
  }
  // LOCAL literal, never a module-level `const *u8` -- those mis-compare in nx_cc (proven 2026-07-31:
  // the digest printed byte-identical and the comparison still said FAILED).
  let want: *u8 = "ed63657ff389301282b169b0abde9b5dd2c7e4d524fdfa5da6ff3094fc93c4c3\x00" as *u8
  var pin: i64 = 1
  i = 0
  while i < 64 { if hx[i] != want[i] { pin = 0 } i = i + 1 }
  w("  acquisition digest: " as *u8); wb(hx, 64); w("\n" as *u8)
  if pin == 0 {
      w("RED: PIN FAILED -- this file is not the one nx_vecfetch acquired. Refusing to read vectors\n" as *u8)
      w("     from an unpinned document.\n" as *u8)
      return 1
  }
  w("  PIN OK -- bytes match the digest computed in-process at the socket\n" as *u8)
143
  // ---- CLAUSE 2: TEST 1 of 7.1 -- the empty-message vector, parsed out of the document ----
  // Chosen deliberately: MESSAGE is zero bytes, so there is no message-hex parsing step that could
  // silently mis-slice and turn a real failure into a pass.
  let t1: i64 = findfrom(b, lp[0], "-----TEST 1" as *u8, 0)
  if t1 < 0 { w("RED: could not locate '-----TEST 1' in the document\n" as *u8); return 1 }
149
  let lpub: i64 = findfrom(b, lp[0], "PUBLIC KEY:" as *u8, t1)
  let pub: *u8 = sys_mmap(64)
  let p1: i64 = parsehex(b, lp[0], lpub + 11, pub, 32)
  let lsig: i64 = findfrom(b, lp[0], "SIGNATURE:" as *u8, t1)
  let sig: *u8 = sys_mmap(96)
  let p2: i64 = parsehex(b, lp[0], lsig + 10, sig, 64)
156
  if lpub < 0 { w("RED: no PUBLIC KEY label\n" as *u8); return 1 }
  if lsig < 0 { w("RED: no SIGNATURE label\n" as *u8); return 1 }
  if p1 < 0 { w("RED: public key hex short/absent\n" as *u8); return 1 }
  if p2 < 0 { w("RED: signature hex short/absent\n" as *u8); return 1 }
161
  let msg: *u8 = sys_mmap(16)
  var pass: i64 = 0
  var fail: i64 = 0
165
  if ed25519_verify_full(pub, msg, 0, sig) == 1 {
      pass = pass + 1
      w("  PASS T1 verify: the IETF's own signature over the empty message verifies under\n" as *u8)
      w("       the IETF's own public key, using our ed25519 verifier\n" as *u8)
  } else {
      fail = fail + 1
      w("  FAIL T1 verify: published signature REJECTED by our verifier\n" as *u8)
  }
174
  // ---- NEGATIVE CONTROL: the clause must be able to fail. Flip one byte of the published signature. ----
  // Without this the gate has not been shown to measure anything -- a verifier stuck at "accept" would
  // pass T1 forever.
  sig[0] = (((sig[0] as i64) ^ 1) & 255) as u8
  if ed25519_verify_full(pub, msg, 0, sig) == 1 {
      fail = fail + 1
      w("  FAIL NEG: a TAMPERED signature was ACCEPTED -- the verifier is not discriminating\n" as *u8)
  } else {
      pass = pass + 1
      w("  PASS NEG: one-bit-tampered signature REJECTED (the check can fail, so T1 means something)\n" as *u8)
  }
186
  w("\n  refsrc=https://www.rfc-editor.org/rfc/rfc8032.txt\n" as *u8)
  w("  refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8)
  w("  ref=RFC8032-7.1   gate=nx_ed25519_extvec_gate\n" as *u8)
  w("  SCOPE: proves our VERIFIER accepts the published signature; does NOT assert our signer.\n" as *u8)
  w("nx_ed25519_extvec_gate: pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail)
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = pass
  ctr__dry[1] = pass + fail
  let rc__dry: i64 = gv_verdict("ED25519-EXTVEC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
201}
nx_ed25519_extvec_gate.nx source

`nx_ed25519_extvec_gate.nx` source
