nx_vsroll_gate.nx source

1// nx_vsroll_gate.nx -- proves a domain lifts on its WEAKEST leg and refuses on any unmeasured one. 2// 3// The teeth that matter are T4 and T7. T4 is the anti-Goodhart tooth: the roll must take the MIN, 4// so a domain with one EXCEED axis and one PRODUCTION axis earns PRODUCTION. T7 is the tooth that 5// makes the roster worth having at all: ADDING a scope must be able to LOWER a domain and never 6// raise it. If declaring more of what a domain means could improve its grade, the roster would be 7// a lever instead of a ruler, and every domain would be described in whatever terms flattered it. 8// 9// T5 is the cross-domain leak: a claim on scope `latency` under `search` must not satisfy scope 10// `latency` under `network`. Sharing an axis NAME is not sharing the WORK. 11// license_tier: ORIGINAL No hw writes (Rule 26). 12import "nx_vsroll_lib.nx" 13import "nx_gate_verdict.nx" 14 15func rg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 16 17func main(argc: i64, argv: *i64) -> i64 { 18 let ctr: *i64 = gv_ctr() 19 gv_head("nx_vsroll -- a domain earns a comparative rung only when EVERY declared scope has a claim, and it lifts on the MIN" as *u8) 20 21 let out: *i64 = sys_mmap(64) as *i64 22 23 // Roster: two scopes for `gpu`, one for `search`, plus a comment line and a blank. 24 let R: *u8 = "# comment must be skipped\ngpu|spirv-validity|khronos\ngpu|3d-pipeline|reference renderer\nsearch|latency|p99 vs lucene\n" as *u8 25 let rn: i64 = el_len(R) 26 27 // Claims: gpu/spirv-validity=EXCEED, gpu/3d-pipeline=PRODUCTION, search/latency absent. 28 let C: *u8 = "VSBEST epoch=1 domain=gpu scope=spirv-validity verdict=ahead earns=EXCEED domain_lifting=0\nVSBEST epoch=2 domain=gpu scope=3d-pipeline verdict=parity earns=PRODUCTION domain_lifting=0\n" as *u8 29 let cn: i64 = el_len(C) 30 31 gv_check("T1 ROSTER a domain with no declared axes is NO-ROSTER, not an empty pass" as *u8, rg_eq(vr_roll_buf("kernel" as *u8, R, rn, C, cn, out), VR_NO_ROSTER), ctr) 32 33 gv_check("T2 ROSTER comment lines (#) are not scopes" as *u8, rg_eq(vr_scope_at(R, rn, "#" as *u8, 0, sys_mmap(VR_SCOPE_CAP), VR_SCOPE_CAP), 0), ctr) 34 35 let rc3: i64 = vr_roll_buf("search" as *u8, R, rn, C, cn, out) 36 var t3: i64 = 0 37 if rc3 == VR_INCOMPLETE { if rg_eq(out[VRO_NREQ], 1) == 1 { if rg_eq(out[VRO_NHAVE], 0) == 1 { t3 = 1 } } } 38 gv_check("T3 UNMEASURED one declared scope with no claim REFUSES the whole roll" as *u8, t3, ctr) 39 40 let rc4: i64 = vr_roll_buf("gpu" as *u8, R, rn, C, cn, out) 41 var t4: i64 = 0 42 if rc4 == VR_OK { if rg_eq(out[VRO_MINLV], MAT_PRODUCTION) == 1 { t4 = 1 } } 43 gv_check("T4 MIN a complete domain with EXCEED+PRODUCTION earns PRODUCTION, never EXCEED" as *u8, t4, ctr) 44 45 // Cross-domain leak: `latency` is claimed under `network`, but `search` also declares `latency`. 46 let C5: *u8 = "VSBEST epoch=3 domain=network scope=latency verdict=ahead earns=EXCEED domain_lifting=0\n" as *u8 47 gv_check("T5 LEAK a claim on the same scope under ANOTHER domain does not satisfy this one" as *u8, rg_eq(vr_claim_level(C5, el_len(C5), "search" as *u8, "latency" as *u8), 0 - 1), ctr) 48 49 gv_check("T6 LABEL an unknown earns= label reads UNMEASURED, not level 0" as *u8, rg_eq(vr_level_of("VSBEST domain=gpu scope=x earns=WORLD_BEATING z" as *u8, 0, 46), 0 - 1), ctr) 50 51 // T7: same claims, but the roster now declares a THIRD gpu scope nobody has measured. 52 let R7: *u8 = "gpu|spirv-validity|k\ngpu|3d-pipeline|r\ngpu|tensor-compute|gemm\n" as *u8 53 gv_check("T7 MONOTONE adding a scope to the roster LOWERS the domain (OK -> REFUSED), never raises it" as *u8, rg_eq(vr_roll_buf("gpu" as *u8, R7, el_len(R7), C, cn, out), VR_INCOMPLETE), ctr) 54 55 gv_check("T8 EMPTY an empty claims buffer refuses a rostered domain rather than passing it" as *u8, rg_eq(vr_roll_buf("gpu" as *u8, R, rn, "" as *u8, 0, out), VR_INCOMPLETE), ctr) 56 57 let F: *u8 = "gpu|spirv-validity|khronos\n" as *u8 58 let sc: *u8 = sys_mmap(VR_SCOPE_CAP) 59 vr_scope_at(F, el_len(F), "gpu" as *u8, 0, sc, VR_SCOPE_CAP) 60 gv_check("T9 FIELD the scope is field 1, not the trailing note" as *u8, el_streq(sc, "spirv-validity" as *u8), ctr) 61 62 gv_check("T10 RANGE asking past the last scope returns 0, terminating the walk" as *u8, rg_eq(vr_scope_at(F, el_len(F), "gpu" as *u8, 9, sc, VR_SCOPE_CAP), 0), ctr) 63 64 // Positive control: a genuinely complete roster must actually roll GREEN, or every tooth above 65 // could be passing because the roll refuses unconditionally. 66 let R11: *u8 = "gpu|spirv-validity|k\n" as *u8 67 let rc11: i64 = vr_roll_buf("gpu" as *u8, R11, el_len(R11), C, cn, out) 68 var t11: i64 = 0 69 if rc11 == VR_OK { if rg_eq(out[VRO_MINLV], MAT_EXCEED) == 1 { t11 = 1 } } 70 gv_check("T11 POSCTL a fully-claimed roster DOES roll GREEN at the claimed level" as *u8, t11, ctr) 71 72 let rc: i64 = gv_verdict("VSROLL" as *u8, ctr, "a domain earns a comparative rung only when every declared scope has an admitted claim, and it lifts on the MIN" as *u8) 73 sys_exit(rc) 74 return rc 75}