nx_boundscheck.nx source

1// nx_boundscheck.nx -- LN3 RAW-POINTER PROVENANCE fixture organ (lang.plan rung LN3, watch 2// symbol bck_ptr_provenance on /compare/lang row "Raw-pointer access prevented"). 3// 4// WHAT THIS IS. The runnable witness for the compiler's --ptrprov declared mode: a `let`-bound 5// sys_mmap(<const>) pointer's indexing is bounds-checked like a typed array (nx_parse.nx, the 6// LN3 block). Each phase is selected by argv so a single trap ends exactly one phase and the 7// gate (nx_boundscheck_gate) can assert every outcome independently: 8// 9// nx_boundscheck ok in-range read+write+alias walk -> exit 0 under BOTH modes 10// (the positive control: a deny mode that refuses everything fails here) 11// nx_boundscheck read the 2026-07-08 READ-TO-NUL class (CWE-125): a scan with no length 12// bound walks off a 64-byte allocation. Default build: the over-read 13// SURVIVES on arena/page slack (exit 0 -- reading bytes that belong to 14// a NEIGHBORING allocation, the silent-wrong-answer this rung exists to 15// kill). --ptrprov build: traps exit 71 (NX_TRAP_BOUNDS) at index 64. 16// nx_boundscheck write CWE-787, the corruption primitive: s[10] on a 10-element allocation. 17// Default: lands in slack, exit 0. --ptrprov: traps exit 71. 18// 19// The sibling witness nx_boundscheck_constidx.nx carries the COMPILE-TIME leg (a constant 20// out-of-range index refused before any binary exists). 21// 22// license_tier: ORIGINAL No hw writes (Rule 26). 23import "nx_syscalls.nx" 24 25const BCK_ALLOC: i64 = 64 26const BCK_FILL: i64 = 7 27const BCK_W_ELEMS: i64 = 10 28// The mmap argument must be a SINGLE const/literal: provenance capture keys on VK_CONST_INT, 29// and a `N * 8` argument is a parse-time BINOP value, not a folded constant -- passing it would 30// make this fixture silently unbound (a vacuous fixture, the exact class gv_bite exists to catch). 31const BCK_W_BYTES: i64 = 80 32 33// THE WATCH SYMBOL and the READ-leg fixture in one: the allocation, the terminator-free fill, 34// and the unbounded scan all live in ONE function because provenance is bound where the compiler 35// can SEE the allocation -- a parameter would honestly carry no extent (declared floor). 36func bck_ptr_provenance() -> i64 { 37 let buf: *u8 = sys_mmap(BCK_ALLOC) 38 var i: i64 = 0 39 while i < BCK_ALLOC { buf[i] = BCK_FILL as u8; i = i + 1 } 40 // No terminator was ever written: the producer half of the 2026-07-08 bug. 41 var n: i64 = 0 42 while buf[n] != (0 as u8) { n = n + 1 } 43 return n 44} 45 46// CWE-787 leg: the store lands one element past the allocation's extent. 47func bck_write_overrun() -> i64 { 48 let s: *i64 = sys_mmap(BCK_W_BYTES) as *i64 49 var i: i64 = 0 50 while i <= BCK_W_ELEMS { s[i] = i; i = i + 1 } 51 return 0 52} 53 54// Positive control: in-range reads and writes, plus the alias inherit (`let q = w`) -- must 55// complete under BOTH modes or the checker is refusing valid programs. 56func bck_inrange_control() -> i64 { 57 let buf: *u8 = sys_mmap(BCK_ALLOC) 58 var i: i64 = 0 59 while i < BCK_ALLOC { buf[i] = 1 as u8; i = i + 1 } 60 var s: i64 = 0 61 var j: i64 = 0 62 while j < BCK_ALLOC { s = s + (buf[j] as i64); j = j + 1 } 63 let w: *i64 = sys_mmap(BCK_W_BYTES) as *i64 64 w[BCK_W_ELEMS - 1] = s 65 let q: *i64 = w 66 if q[BCK_W_ELEMS - 1] == BCK_ALLOC { return 0 } 67 return 1 68} 69 70// ===================== LN7: SOUND BOUNDS-CHECK ELISION (bck_elide_dominated) ================= 71// The RUNNABLE WITNESSES for the elision rung. The capability itself is the optimizer pass in 72// runtime/nx_bck_elide.nx; these are the programs whose BEHAVIOUR must be identical with and 73// without --bckelide, and whose ASSEMBLY must differ only where an elision is provably sound. 74// 75// Two of the three legs are OUT-OF-BOUNDS ON PURPOSE and MUST STILL TRAP. They are the point: 76// an unsound elision does not crash, it silently reads or writes memory it had no right to, so 77// the only tooth that can catch it is one where a check the pass must NOT remove is the sole 78// thing standing between the program and a real overrun. 79// 80// BCK_E_ELEMS must equal the literal in the array types below. Nothing in the language lets 81// this file assert that, so the GATE pins it from both sides instead: the in-range leg exits 0 82// (which fails if the const is too LARGE) and the two trap legs exit NX_TRAP_BOUNDS (which 83// fails if it is too SMALL). 84const BCK_E_ELEMS: i64 = 64 85const BCK_E_SMALL: i64 = 8 86const BCK_E_PERF_ITERS: i64 = 10000000 87 88// WITNESS A -- a genuinely DOMINATED re-check, the case the rung exists to speed up. 89// `let i` is SSA, so all three accesses name ONE index value id, and the second and third 90// checks sit in blocks dominated by the first check's ok block. Under --bckelide the two 91// re-checks become unconditional; the FIRST is always kept. The returned value must be 92// identical either way -- that is the entire correctness claim, and main() checks it against a 93// closed form rather than against a remembered number. 94func bck_elide_dominated_witness(iters: i64) -> i64 { 95 var a: [64]i64 96 var f: i64 = 0 97 while f < BCK_E_ELEMS { a[f] = f; f = f + 1 } 98 var acc: i64 = 0 99 var k: i64 = 0 100 while k < iters { 101 let i: i64 = k % BCK_E_ELEMS 102 a[i] = a[i] + 1 // read-check, then write-check, on ONE index value id 103 acc = acc + a[i] // a third use, also dominated by the first check 104 k = k + 1 105 } 106 return acc 107} 108 109// WITNESS A2 -- the SAME access pattern as A with the DIVISION taken out of the loop. 110// A's index is `k % BCK_E_ELEMS`, and an integer remainder costs tens of cycles while a bounds 111// check costs a compare and a predictable branch -- so A's loop is dominated by an operation 112// this rung does not touch, and its wall-clock ratio understates the check's share by a lot. 113// Nesting the loops reaches exactly the same elements in the same order with the same number of 114// accesses and no divide. Kept BESIDE A rather than replacing it: both numbers are reported, 115// because removing a confound is only honest if the confounded figure stays on the record. 116func bck_elide_perf_witness(reps: i64) -> i64 { 117 var a: [64]i64 118 var f: i64 = 0 119 while f < BCK_E_ELEMS { a[f] = f; f = f + 1 } 120 var acc: i64 = 0 121 var r: i64 = 0 122 while r < reps { 123 var k: i64 = 0 124 while k < BCK_E_ELEMS { 125 let i: i64 = k 126 a[i] = a[i] + 1 127 acc = acc + a[i] 128 k = k + 1 129 } 130 r = r + 1 131 } 132 return acc 133} 134 135// WITNESS B -- a re-check that is NOT dominated, and the sharpest tooth in the rung. 136// The first access sits inside `if i < BCK_E_SMALL`, so the path where that test FAILS reaches 137// the second access having proven nothing. A pass that treats "there is an earlier check with 138// the same key" as sufficient -- without asking whether it DOMINATES -- elides the second check 139// and this function then reads a[128] out of a 64-element array with no diagnostic at all. 140// Called with an out-of-range index it MUST exit NX_TRAP_BOUNDS under every mode. 141func bck_elide_notdominated_witness(n: i64) -> i64 { 142 var a: [64]i64 143 var f: i64 = 0 144 while f < BCK_E_ELEMS { a[f] = f; f = f + 1 } 145 let i: i64 = n 146 var acc: i64 = 0 147 if i < BCK_E_SMALL { acc = acc + a[i] } 148 acc = acc + a[i] 149 return acc 150} 151 152// WITNESS C -- the LENGTH half of the key, which is the other way to build the same hole. 153// Both accesses use ONE index value id and the second IS dominated by the first, so a pass that 154// keyed only on the index would elide it. The arrays have different extents, so an index that 155// is in range for the first is out of range for the second. Called with an index between the 156// two extents it MUST exit NX_TRAP_BOUNDS. 157func bck_elide_keylen_witness(n: i64) -> i64 { 158 var big: [64]i64 159 var small: [8]i64 160 var f: i64 = 0 161 while f < BCK_E_ELEMS { big[f] = f; f = f + 1 } 162 var g: i64 = 0 163 while g < BCK_E_SMALL { small[g] = g; g = g + 1 } 164 let i: i64 = n 165 var acc: i64 = 0 166 acc = acc + big[i] 167 acc = acc + small[i] 168 return acc 169} 170 171func main(argc: i64, argv: *i64) -> i64 { 172 var ph: i64 = 111 // 'o' -- default phase is the safe control 173 if argc >= 2 { 174 let a: *u8 = argv[1] as *u8 175 ph = a[0] as i64 176 } 177 if ph == 114 { // 'r' read 178 let r: i64 = bck_ptr_provenance() 179 // Any n >= the extent proves the scan left the allocation without a trap. The exact 180 // value depends on whatever neighboring memory holds -- which is the point. 181 if r >= BCK_ALLOC { return 0 } 182 return 1 183 } 184 if ph == 119 { // 'w' write 185 return bck_write_overrun() 186 } 187 if ph == 100 { // 'd' LN7 dominated re-check, MUST stay correct 188 // The expected total is a CLOSED FORM, not a remembered number: every element is 189 // visited exactly once (iters == BCK_E_ELEMS, index k % BCK_E_ELEMS), each is 190 // incremented from f to f+1 and then accumulated, so the sum is 1+2+...+BCK_E_ELEMS. 191 // Deriving it here rather than pasting a literal means the tooth still holds if the 192 // extent above ever changes. 193 let got: i64 = bck_elide_dominated_witness(BCK_E_ELEMS) 194 let want: i64 = (BCK_E_ELEMS * (BCK_E_ELEMS + 1)) / 2 195 if got == want { return 0 } 196 return 1 197 } 198 if ph == 110 { // 'n' LN7 NOT-dominated re-check, MUST TRAP 199 // Index deliberately past the extent AND past the guard, so the guarded access is 200 // skipped entirely and the unguarded one is the only thing left to catch it. 201 bck_elide_notdominated_witness(BCK_E_ELEMS * 2) 202 return 2 // reaching here at all means the check was lost 203 } 204 if ph == 112 { // 'p' LN7 h2h COST leg -- timed by the gate 205 // Sized so the loop dominates process startup by ~3 orders of magnitude: the ratio the 206 // gate reports is then a property of the loop body, not of exec+mmap. The ratio is 207 // insensitive to this value once that holds, so it is a scale choice, not a threshold -- 208 // nothing branches on it. 209 let acc: i64 = bck_elide_dominated_witness(BCK_E_PERF_ITERS) 210 // Observing acc is what keeps the loop from being dead-code eliminated; a benchmark whose 211 // result nobody reads measures an empty loop. 212 if acc > 0 { return 0 } 213 return 3 214 } 215 if ph == 113 { // 'q' LN7 h2h COST leg, division-free (witness A2) 216 // Same element count and same access order as 'p', reps chosen so the TOTAL number of 217 // checked accesses is identical -- only the remainder is gone. 218 let acc2: i64 = bck_elide_perf_witness(BCK_E_PERF_ITERS / BCK_E_ELEMS) 219 if acc2 > 0 { return 0 } 220 return 3 221 } 222 if ph == 120 { // 'x' LN7 same index, DIFFERENT extent, MUST TRAP 223 // In range for the 64-element array, out of range for the 8-element one. 224 bck_elide_keylen_witness(BCK_E_ELEMS / 4) 225 return 2 // reaching here at all means the check was lost 226 } 227 return bck_inrange_control() // 'o' / anything else 228}