nx_x25519_extvec_gate.nx source

1// nx_x25519_extvec_gate.nx -- THE FIRST PROVABLY THIRD-PARTY-VALIDATED CLAIM. 2// Proven GREEN on the laptop 2026-07-31 (pass=2 fail=0). Shipped here so it runs where claims are served. 3// 4// Every other KAT in this corpus embeds its expected values as constants a developer copied out of a 5// specification. Honest work, but NOT provably external: nothing in the artifact distinguishes a value 6// transcribed from the IETF from one an author -- or an AGENT -- merely believed. This gate closes that: 7// 1 it reads the vectors FROM knowledge/extvec/rfc7748.txt AT RUN TIME. NO expected value appears in 8// this source at all, so there is nothing here for anyone to have mistyped or invented. 9// 2 it PINS the acquisition digest: the file must sha256 to the value nx_vecfetch computed IN-PROCESS, 10// at the socket, before the bytes ever touched disk. Edited, truncated or substituted -> pin fails. 11// 3 only then does it run x25519() and compare. 12// 13// THE PIN IS THE SECURITY PROPERTY, NOT THE RUN-TIME PARSE. Parsing from a file is necessary but NOT 14// sufficient: an agent could edit the fetched file to contain whatever answers make its implementation 15// pass, and the parse would faithfully read the forgery. Pinning to an ACQUISITION-TIME digest is what 16// turns "we read it from a file" into evidence. 17// AND THE PIN MAKES TRANSPORT UNTRUSTED-BUT-VERIFIED: whoever carries rfc7748.txt to this host -- scp, an 18// agent, a USB stick -- cannot corrupt it undetected, because sha256 preimage resistance means bytes that 19// hash to ab200228.. ARE the fetched bytes. The carrier never has to be trusted. That is the whole point 20// of content-addressing, and it is why this gate is safe to ship even though its data file is not. 21// 22// TO MAKE IT GREEN HERE: place knowledge/extvec/rfc7748.txt (any byte-exact copy; the pin checks it), or 23// build+run nx_vecfetch on this host. Until then it reports RED-and-honest: absent file, never a fallback 24// to constants. license_tier: ORIGINAL expect_exit: 0 25import "nx_syscalls.nx" 26import "nx_sha256_wasm.nx" 27import "nx_x25519.nx" 28 29func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 30func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 } 31 32func nn(v: i64) -> i64 { 33 var m: i64 = v 34 if m < 0 { w("-" as *u8); m = 0 - m } 35 let t: *u8 = sys_mmap(32) 36 var k: i64 = 0 37 if m == 0 { t[0] = 48 as u8; k = 1 } 38 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 39 let b: *u8 = sys_mmap(32) 40 var j: i64 = 0 41 while j < k { b[j] = t[k - 1 - j]; j = j + 1 } 42 sys_write(1, b, k) 43 return 0 44} 45 46func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v } 47 48func hexval(c: i64) -> i64 { 49 if c >= 48 { if c <= 57 { return c - 48 } } 50 if c >= 97 { if c <= 102 { return c - 87 } } 51 if c >= 65 { if c <= 70 { return c - 55 } } 52 return 0 - 1 53} 54 55func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64 { 56 var i: i64 = 0 57 while s[i] != (0 as u8) { 58 if at + i >= n { return 0 } 59 if b[at + i] != s[i] { return 0 } 60 i = i + 1 61 } 62 return 1 63} 64 65func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64 { 66 var p: i64 = from 67 while p < n { 68 if starts(b, n, p, s) == 1 { return p } 69 p = p + 1 70 } 71 return 0 - 1 72} 73 74// Strict: refuses a short hex run, so a reflowed or truncated document fails loudly rather than yielding 75// a half-vector that would then be compared as if complete. 76func parse32(b: *u8, n: i64, from: i64, out: *u8) -> i64 { 77 var p: i64 = from 78 var got: i64 = 0 79 while p < n { 80 if got >= 32 { return p } 81 let c: i64 = b[p] as i64 82 let hv: i64 = hexval(c) 83 if hv < 0 { 84 if got > 0 { if got < 32 { got = 0 } } 85 p = p + 1 86 } else { 87 if p + 1 >= n { return 0 - 1 } 88 let hv2: i64 = hexval(b[p + 1] as i64) 89 if hv2 < 0 { p = p + 1 } 90 else { 91 out[got] = ((hv * 16) + hv2) as u8 92 got = got + 1 93 p = p + 2 94 } 95 } 96 } 97 if got >= 32 { return p } 98 return 0 - 1 99} 100 101func eq32(a: *u8, b: *u8) -> i64 { 102 var i: i64 = 0 103 while i < 32 { if a[i] != b[i] { return 0 } i = i + 1 } 104 return 1 105} 106 107func main() -> i64 { 108 w("nx_x25519_extvec_gate -- x25519 vs RFC 7748 5.2, vectors READ FROM THE FETCHED DOCUMENT\n" as *u8) 109 110 let lp: *i64 = sys_mmap(16) as *i64 111 lp[0] = 0 112 let b: *u8 = sys_read_file("knowledge/extvec/rfc7748.txt\x00" as *u8, lp) 113 if lp[0] <= 0 { 114 w("RED: fetched vector file absent -- run nx_vecfetch first. NOT falling back to constants.\n" as *u8) 115 return 1 116 } 117 118 let ctx: *u8 = sys_mmap(1024) 119 let dig: *u8 = sys_mmap(64) 120 nx_sha256_one_shot(b, lp[0], ctx, dig) 121 let hx: *u8 = sys_mmap(80) 122 var i: i64 = 0 123 while i < 32 { 124 hx[i * 2] = hexnib(((dig[i] as i64) / 16) & 15) as u8 125 hx[i * 2 + 1] = hexnib((dig[i] as i64) & 15) as u8 126 i = i + 1 127 } 128 // A MODULE-LEVEL `const NAME: *u8 = "..." as *u8` DOES NOT COMPARE CORRECTLY IN nx_cc. First run printed 129 // this digest byte-for-byte identical to the constant and STILL reported PIN FAILED -- a check 130 // disagreeing with its own displayed evidence means the INSTRUMENT is broken, not the subject. Bound as 131 // a LOCAL literal. Had I trusted that RED and loosened the pin, I would have disabled the one clause 132 // that makes this gate evidence. 133 let want: *u8 = "ab200228b7369398bc112917a0e3dcf6dbb943105b5e170be565e309c104b8dd\x00" as *u8 134 var pin: i64 = 1 135 i = 0 136 while i < 64 { if hx[i] != want[i] { pin = 0 } i = i + 1 } 137 w(" acquisition digest: " as *u8); wb(hx, 64); w("\n" as *u8) 138 if pin == 0 { 139 w("RED: PIN FAILED -- this file is not the one nx_vecfetch acquired.\n" as *u8) 140 w(" Refusing to read vectors from an unpinned document: an edited file would let us\n" as *u8) 141 w(" grade ourselves against answers of our own choosing.\n" as *u8) 142 return 1 143 } 144 w(" PIN OK -- bytes match the digest computed in-process at the socket\n" as *u8) 145 146 var pass: i64 = 0 147 var fail: i64 = 0 148 let sc: *u8 = sys_mmap(64) 149 let uu: *u8 = sys_mmap(64) 150 let ex: *u8 = sys_mmap(64) 151 let got: *u8 = sys_mmap(64) 152 153 var cur: i64 = 0 154 var vec: i64 = 0 155 while vec < 2 { 156 let ls: i64 = findfrom(b, lp[0], "Input scalar:" as *u8, cur) 157 if ls < 0 { w(" RED: could not locate 'Input scalar:' in the document\n" as *u8); fail = fail + 1; vec = 2 } 158 else { 159 let p1: i64 = parse32(b, lp[0], ls + 13, sc) 160 let lu: i64 = findfrom(b, lp[0], "Input u-coordinate:" as *u8, p1) 161 let p2: i64 = parse32(b, lp[0], lu + 19, uu) 162 let lo: i64 = findfrom(b, lp[0], "Output u-coordinate:" as *u8, p2) 163 let p3: i64 = parse32(b, lp[0], lo + 20, ex) 164 if p1 < 0 { fail = fail + 1 } else { if p2 < 0 { fail = fail + 1 } else { if p3 < 0 { fail = fail + 1 } else { 165 x25519(sc, uu, got) 166 if eq32(got, ex) == 1 { 167 pass = pass + 1 168 w(" PASS vector " as *u8); nn(vec + 1) 169 w(": x25519(scalar,u) == the document's Output u-coordinate\n" as *u8) 170 } else { 171 fail = fail + 1 172 w(" FAIL vector " as *u8); nn(vec + 1); w(": output mismatch\n" as *u8) 173 } 174 cur = p3 175 } } } 176 vec = vec + 1 177 } 178 } 179 180 w("\n refsrc=https://www.rfc-editor.org/rfc/rfc7748.txt\n" as *u8) 181 w(" refsrcdig=" as *u8); wb(hx, 64); w("\n" as *u8) 182 w(" ref=RFC7748-5.2 gate=nx_x25519_extvec_gate\n" as *u8) 183 w("nx_x25519_extvec_gate: pass=" as *u8); nn(pass); w(" fail=" as *u8); nn(fail) 184 if fail == 0 { if pass == 2 { w(" verdict=GREEN\n" as *u8); return 0 } } 185 w(" verdict=RED\n" as *u8) 186 return 1 187}