nx_property_test.nx
buildroot/runtime/nx_property_test.nx
about
nx_property_test.nx -- PROPERTY-BASED + METAMORPHIC testing of the capability core (census gap). Instead of fixed
cases, GENERATE random capabilities (reproducible LCG) and assert INVARIANTS hold over hundreds of them:
P1 (property): verify(issue(allow,exp), tool) == OK <=> (tool in allow) AND (not expired)
M1 (metamorphic): attenuate(all-cap, narrow) grants tool <=> tool in narrow (attenuation never widens)
A single violation prints the (minimal-ish) counterexample and reds. This is what would have caught a subtler
MAC/allow-logic bug that a hand-written fixed case might miss. license_tier: ORIGINAL
dependencies 2 imports · 0 importers
imports: nx_cap_token.nxnx_gate.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| none |
functions
| 11 | func pt_rand(state: *i64) -> i64 { state[0] = state[0] * 1103515245 + 12345; return (state[0] >> 16) & 0x7fffffff } called by 1: main |
| 14 | func pt_tool(i: i64, buf: *u8) -> i64 { buf[0] = 116 as u8; buf[1] = (48 + i) as u8; return 2 } called by 1: main |
| 17 | func pt_allow(mask: i64, buf: *u8) -> i64 called by 1: main |
| 30 | func main() -> i64 |