code wiki / (root) / nx_boundscheck_constidx.nx

nx_boundscheck_constidx.nx source

↩ module page · 20 lines · 879 B

1// nx_boundscheck_constidx.nx -- STANDING WITNESS for the COMPILE-TIME leg of LN3 raw-pointer 2// provenance (sibling of nx_boundscheck.nx; same family as nx_litprobe / nx_constidx_probe). 3// 4// buf[64] on a 64-byte allocation is a provable out-of-range access. Under the DEFAULT build 5// this compiles clean and runs (reading one byte of neighboring memory -- the silent C-class 6// behavior, kept as the hazard record). Under `--ptrprov` the compiler REFUSES it at parse 7// time with the 5W+H provenance diagnostic -- nx_boundscheck_gate asserts both directions and 8// that the refusal names the provenance rule, not some other error. 9// 10// license_tier: ORIGINAL No hw writes (Rule 26). 11import "nx_syscalls.nx" 12 13const BCC_ALLOC: i64 = 64 14 15func main() -> i64 { 16 let buf: *u8 = sys_mmap(BCC_ALLOC) 17 buf[0] = 1 as u8 18 let x: i64 = buf[BCC_ALLOC] as i64 19 return x 20}