nx_vsbest_gate.nx source

1// nx_vsbest_gate.nx -- proves the comparative axis REFUSES every unearned claim. 2// 3// This gate is mostly NEG-CONTROLS on purpose. The whole value of the comparative axis is what it 4// REFUSES: if it admits a claim with no competitor, no method, or unreadable evidence, it becomes 5// the same laundering path permil_to_level was. T1 is the only positive tooth; T2-T8 are the ways a 6// claim can be hollow, and each must be refused with its OWN code so the caller learns WHICH leg 7// failed rather than getting a bare no. 8// 9// T9 is the anti-Goodhart tooth: a `behind` verdict must earn NOTHING above PRODUCTION. Losing to 10// the best in class is not a comparative achievement, and a scale that rewarded merely HAVING run a 11// comparison would be gameable by running easy ones. 12// license_tier: ORIGINAL No hw writes (Rule 26). 13import "nx_vsbest_lib.nx" 14import "nx_gate_verdict.nx" 15 16func vg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 17 18func main(argc: i64, argv: *i64) -> i64 { 19 let ctr: *i64 = gv_ctr() 20 gv_head("nx_vsbest -- a comparative claim is ADMITTED only with a named competitor, a re-runnable method, and evidence that says so" as *u8) 21 22 let out: *i64 = sys_mmap(64) as *i64 23 24 // A real, readable witness: this gate's own source tree always contains the maturity auditor, 25 // and MAT_SCLASS appears in it. Using a file that genuinely exists keeps the positive tooth 26 // honest -- a fixture log written by the gate itself would be testing its own side effect. 27 let evlog: *u8 = "buildroot/runtime/_hdl_build/nx_maturity_auditor.nx" as *u8 28 let rc1: i64 = vb_admit("gcc" as *u8, "ran both compilers over the same corpus, compared emitted bytes" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, out) 29 var t1: i64 = 0 30 if rc1 == VB_OK { if vg_eq(out[0], VB_PARITY) == 1 { if vg_eq(out[1], MAT_SCLASS) == 1 { t1 = 1 } } } 31 gv_check("T1 a complete claim with READABLE evidence is ADMITTED and earns S-CLASS" as *u8, t1, ctr) 32 33 gv_check("T2 NEG empty competitor is REFUSED" as *u8, vg_eq(vb_admit("" as *u8, "ran both over the same corpus" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, out), VB_NO_COMPETITOR), ctr) 34 gv_check("T3 NEG self-referential competitor 'baseline' is REFUSED (the vs-0-SOTA-src defect)" as *u8, vg_eq(vb_admit("baseline" as *u8, "ran both over the same corpus" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, out), VB_NO_COMPETITOR), ctr) 35 gv_check("T4 NEG competitor 'none' is REFUSED" as *u8, vg_eq(vb_admit("none" as *u8, "ran both over the same corpus" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, out), VB_NO_COMPETITOR), ctr) 36 gv_check("T5 NEG a method too short to re-run is REFUSED" as *u8, vg_eq(vb_admit("gcc" as *u8, "faster" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, out), VB_NO_METHOD), ctr) 37 gv_check("T6 NEG a MISSING evidence log is REFUSED (an unreadable witness is NO witness)" as *u8, vg_eq(vb_admit("gcc" as *u8, "ran both over the same corpus" as *u8, "knowledge/status/definitely_not_here_xyz.log" as *u8, "MAT_SCLASS" as *u8, "parity" as *u8, out), VB_NO_EVIDENCE), ctr) 38 gv_check("T7 NEG evidence that does NOT contain the declared pattern is REFUSED (dangling witness)" as *u8, vg_eq(vb_admit("gcc" as *u8, "ran both over the same corpus" as *u8, evlog, "THIS_STRING_IS_NOT_IN_THAT_FILE_9z" as *u8, "parity" as *u8, out), VB_PATTERN_ABSENT), ctr) 39 gv_check("T8 NEG an invalid verdict is REFUSED" as *u8, vg_eq(vb_admit("gcc" as *u8, "ran both over the same corpus" as *u8, evlog, "MAT_SCLASS" as *u8, "probably-better" as *u8, out), VB_BAD_VERDICT), ctr) 40 41 // ANTI-GOODHART: running a comparison and LOSING must earn nothing. Otherwise the axis rewards 42 // merely having compared, which is gameable by choosing easy competitors. 43 let rc9: i64 = vb_admit("llvm" as *u8, "ran both over the same corpus, compared emitted bytes" as *u8, evlog, "MAT_SCLASS" as *u8, "behind" as *u8, out) 44 var t9: i64 = 0 45 if rc9 == VB_OK { if vg_eq(out[1], MAT_PRODUCTION) == 1 { t9 = 1 } } 46 gv_check("T9 ANTI-GOODHART a 'behind' verdict is admitted but earns NOTHING above PRODUCTION" as *u8, t9, ctr) 47 48 let rc10: i64 = vb_admit("seL4" as *u8, "ran the same conformance suite against both kernels" as *u8, evlog, "MAT_SCLASS" as *u8, "ahead" as *u8, out) 49 var t10: i64 = 0 50 if rc10 == VB_OK { if vg_eq(out[1], MAT_EXCEED) == 1 { t10 = 1 } } 51 gv_check("T10 an 'ahead' verdict earns EXCEED, and only with all four legs present" as *u8, t10, ctr) 52 53 gv_check("T11 refusal codes are DISTINCT so the caller learns which leg failed" as *u8, vg_eq(VB_NO_COMPETITOR == VB_NO_METHOD, 0), ctr) 54 55 // ---- SCOPE TEETH, added the moment the FIRST real comparison was attempted ---- 56 // Our SPIR-V emitter IS validated by the Khronos reference (spirv-val, SPIRV-Tools v2025.1, 57 // verdict=VALID, full battery). That is genuine triangulated parity -- on SPIR-V VALIDITY, not 58 // on the gpu domain, which also spans a 3D pipeline, tensor cores and real-silicon submit. 59 // Granting the DOMAIN S-CLASS from a conformance-axis parity would be the same overclaim as 60 // minting it from a coverage percentage. T12/T13 pin that a narrow win is NOT a domain win. 61 let m: *u8 = "emitted a full-battery SPIR-V module and validated it with the Khronos reference validator" as *u8 62 let rc12: i64 = vb_admit_scoped("SPIRV-Tools v2025.1 spirv-val" as *u8, m, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, "spirv-validity" as *u8, "gpu" as *u8, out) 63 var t12: i64 = 0 64 if rc12 == VB_SCOPE_NARROWER { if vg_eq(out[1], MAT_PRODUCTION) == 1 { if vg_eq(out[3], 0) == 1 { t12 = 1 } } } 65 gv_check("T12 SCOPE a narrow-axis parity is ADMITTED but does NOT lift the domain (earns PRODUCTION)" as *u8, t12, ctr) 66 67 let rc13: i64 = vb_admit_scoped("gcc" as *u8, "ran both compilers over the same corpus, compared emitted bytes" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, "compiler" as *u8, "compiler" as *u8, out) 68 var t13: i64 = 0 69 if rc13 == VB_OK { if vg_eq(out[1], MAT_SCLASS) == 1 { if vg_eq(out[3], 1) == 1 { t13 = 1 } } } 70 gv_check("T13 SCOPE a claim whose scope IS the domain DOES lift it to S-CLASS" as *u8, t13, ctr) 71 72 gv_check("T14 SCOPE an empty scope is REFUSED" as *u8, vg_eq(vb_admit_scoped("gcc" as *u8, "ran both over the same corpus" as *u8, evlog, "MAT_SCLASS" as *u8, "parity" as *u8, "" as *u8, "compiler" as *u8, out), VB_NO_SCOPE), ctr) 73 74 let rc: i64 = gv_verdict("VSBEST" as *u8, ctr, "comparative claims require a named competitor, a re-runnable method and evidence that actually says so" as *u8) 75 sys_exit(rc) 76 return rc 77}