nx_mmbench_gate.nx source

1// nx_mmbench_gate.nx -- proves the media+companion ruler is a RULER, not a rubber stamp. 2// 3// It imports nx_mmbench_lib -- THE SAME lib nx_mmbench ships -- so these teeth bite the code that 4// actually produces the published number, not a re-implementation of it. 5// 6// The ruler's entire honesty claim is aud(). If aud() does not really downgrade an unbacked claim, 7// then coverage_permil is decoration and every gap-queue ranking derived from it is fiction. The 8// first live run reported liar_killed=0, which is exactly the reading a BROKEN audit would also 9// produce -- indistinguishable from a healthy one without these tests. Hence: 10// 11// T1 CLEAN : HAVE + an artifact that exists -> stays HAVE. (the ruler can say YES) 12// T2 NEGATIVE CTRL : HAVE + an artifact that does NOT exist -> GAP, flagged liar-killed. 13// THE anti-vacuity tooth. Without this, liar_killed=0 proves nothing. 14// T3 UNGROUNDED : HAVE + no artifact named at all -> capped to PARTIAL, flagged ungrounded. 15// T4 KILL-BEATS-RANK: PARTIAL + absent artifact -> GAP too. A false SPECIFIC claim is killed 16// regardless of how modest the declared level was. 17// T5 SILENCE-OK : PARTIAL + no artifact -> stays PARTIAL, unflagged. Declining to claim is 18// not a lie; only asserting an unbacked WIN is. 19// T6 ONE-WAY : GAP + a present artifact -> stays GAP. Evidence may only ever DEMOTE. 20// A gate that let evidence PROMOTE could launder any gap into a win. 21// T7/T8 PROBE : have() is truthful in both directions (present->1, absent->0). 22// T9 STREQ : verb matching is exact -- a prefix must NOT match, or 'json' would fire on 23// 'jsonx' and silently change which report is published. 24// T10 MONOTONIC : a liar-kill must LOWER the computed headline. Proves the demotion actually 25// reaches the arithmetic instead of just printing a warning next to it. 26// expect_exit: 0 license_tier: ORIGINAL No hw writes (Rule 26). 27import "nx_mmbench_lib.nx" 28import "nx_gate_verdict.nx" 29 30const T_CLEAN: i64 = 20 31const T_KILLED: i64 = 1 32const T_UNGROUND: i64 = 12 33const T_PART_OK: i64 = 10 34const T_GAP_OK: i64 = 0 35 36func main() -> i64 { 37 let ctr: *i64 = gv_ctr() 38 gv_head("nx_mmbench_gate -- the media+companion ruler must be able to say NO" as *u8) 39 40 let PRESENT: *u8 = "buildroot/runtime/_hdl_build/nx_mmbench_lib.nx" as *u8 41 let ABSENT: *u8 = "buildroot/runtime/_hdl_build/nx_mmbench_no_such_artifact_probe.nx" as *u8 42 let pev: i64 = PRESENT as i64 43 let aev: i64 = ABSENT as i64 44 45 var ok: i64 = 0 46 47 if aud(V_HAVE, pev)==T_CLEAN { ok=1 } else { ok=0 } 48 gv_check("T1 CLEAN: HAVE + existing artifact stays HAVE" as *u8, ok, ctr) 49 50 if aud(V_HAVE, aev)==T_KILLED { ok=1 } else { ok=0 } 51 gv_check("T2 NEGATIVE CONTROL: HAVE + ABSENT artifact -> GAP (liar-killed)" as *u8, ok, ctr) 52 53 if aud(V_HAVE, 0)==T_UNGROUND { ok=1 } else { ok=0 } 54 gv_check("T3 UNGROUNDED: HAVE with no artifact -> capped PARTIAL" as *u8, ok, ctr) 55 56 if aud(V_PART, aev)==T_KILLED { ok=1 } else { ok=0 } 57 gv_check("T4 KILL-BEATS-RANK: PARTIAL + ABSENT artifact -> GAP" as *u8, ok, ctr) 58 59 if aud(V_PART, 0)==T_PART_OK { ok=1 } else { ok=0 } 60 gv_check("T5 SILENCE-OK: PARTIAL with no artifact stays PARTIAL, unflagged" as *u8, ok, ctr) 61 62 if aud(V_GAP, pev)==T_GAP_OK { ok=1 } else { ok=0 } 63 gv_check("T6 ONE-WAY: GAP + present artifact stays GAP (evidence never promotes)" as *u8, ok, ctr) 64 65 if have(PRESENT)==1 { ok=1 } else { ok=0 } 66 gv_check("T7 PROBE-POSITIVE: have() sees a file that exists" as *u8, ok, ctr) 67 68 if have(ABSENT)==0 { ok=1 } else { ok=0 } 69 gv_check("T8 PROBE-NEGATIVE: have() reports 0 for a file that does not" as *u8, ok, ctr) 70 71 var s1: i64 = streq("json" as *u8, "json" as *u8) 72 var s2: i64 = streq("json" as *u8, "gapq" as *u8) 73 var s3: i64 = streq("json" as *u8, "jsonx" as *u8) 74 if s1==1 { if s2==0 { if s3==0 { ok=1 } else { ok=0 } } else { ok=0 } } else { ok=0 } 75 gv_check("T9 STREQ: exact match only -- a prefix must not match" as *u8, ok, ctr) 76 77 // T10: three demanded cells, all declared HAVE. One names an absent artifact. The audited 78 // headline MUST fall below the unaudited one, proving the kill reaches the arithmetic. 79 var clean_sum: i64 = (aud(V_HAVE,pev)/10) + (aud(V_HAVE,pev)/10) + (aud(V_HAVE,pev)/10) 80 var dirty_sum: i64 = (aud(V_HAVE,pev)/10) + (aud(V_HAVE,pev)/10) + (aud(V_HAVE,aev)/10) 81 var clean_permil: i64 = clean_sum*1000/6 82 var dirty_permil: i64 = dirty_sum*1000/6 83 if dirty_permil < clean_permil { ok=1 } else { ok=0 } 84 gv_check("T10 MONOTONIC: a liar-kill LOWERS the computed headline" as *u8, ok, ctr) 85 gv_puts(" (clean=" as *u8); gv_num(clean_permil); gv_puts(" permil, one-killed=" as *u8); gv_num(dirty_permil); gv_puts(" permil)\n" as *u8) 86 87 // ---- WIRED DIMENSION (added with it, not after it) ---- 88 if wired(pev)==1 { ok=1 } else { ok=0 } 89 gv_check("T11 WIRED: a deployed artifact reports wired" as *u8, ok, ctr) 90 91 if wired(aev)==0 { ok=1 } else { ok=0 } 92 gv_check("T12 DARK-ABSENT: a named-but-missing deployment reports dark" as *u8, ok, ctr) 93 94 if wired(0)==0 { ok=1 } else { ok=0 } 95 gv_check("T13 DARK-UNNAMED: no deployment artifact named reports dark" as *u8, ok, ctr) 96 97 // THE TOOTH THAT MATTERS: nx_media_extract is gate-proven 6/6 and deployed NOWHERE. A ruler that 98 // scored it on code quality would call it HAVE and overstate what the product can do. usable() 99 // must collapse a perfect build to GAP when it is unreachable. 100 if usable(V_HAVE, 0)==V_GAP { ok=1 } else { ok=0 } 101 gv_check("T14 DARK-COLLAPSE: a fully-built HAVE with no deployment scores GAP" as *u8, ok, ctr) 102 103 if usable(V_HAVE, aev)==V_GAP { ok=1 } else { ok=0 } 104 gv_check("T15 DARK-COLLAPSE-ABSENT: built HAVE + missing deployment scores GAP" as *u8, ok, ctr) 105 106 if usable(V_HAVE, pev)==V_HAVE { ok=1 } else { ok=0 } 107 gv_check("T16 WIRED-PASSTHROUGH: built HAVE + real deployment stays HAVE" as *u8, ok, ctr) 108 109 // usable() must never INVENT capability: deploying something we never built cannot create a win. 110 if usable(V_GAP, pev)==V_GAP { ok=1 } else { ok=0 } 111 gv_check("T17 NO-INVENTION: a deployment cannot promote an unbuilt GAP" as *u8, ok, ctr) 112 113 // T18: the second dimension must be able to LOWER the headline, or it is decoration. 114 var built_sum: i64 = (usable(V_HAVE,pev)/1) + V_HAVE + V_HAVE 115 var usable_sum: i64 = usable(V_HAVE,pev) + usable(V_HAVE,0) + V_HAVE 116 var built_p: i64 = built_sum*1000/6 117 var usable_p: i64 = usable_sum*1000/6 118 if usable_p < built_p { ok=1 } else { ok=0 } 119 gv_check("T18 WIRED-MONOTONIC: darkness LOWERS coverage below built" as *u8, ok, ctr) 120 gv_puts(" (built=" as *u8); gv_num(built_p); gv_puts(" permil, one-dark=" as *u8); gv_num(usable_p); gv_puts(" permil)\n" as *u8) 121 122 // ---- STRONG WIRING TEST (adopted from nx_reader_liveness) ---- 123 // Ground truth verified by hand on the live host before these teeth were written: 124 // nx_gallery_serve.elf contains "nx_ts_index.elf"; it does not contain a nonsense token. 125 let SERVE: *u8 = "/volume1/ai/galx/nx_gallery_serve.elf" as *u8 126 let NEED_OK: *u8 = "nx_ts_index.elf" as *u8 127 let NEED_BAD: *u8 = "nx_no_such_organ_zzq" as *u8 128 let BADBIN: *u8 = "/no/such/binary/at/all" as *u8 129 let sv_i: i64 = SERVE as i64 130 let nok_i: i64 = NEED_OK as i64 131 let nbad_i: i64 = NEED_BAD as i64 132 let bad_i: i64 = BADBIN as i64 133 let dep: i64 = PRESENT as i64 134 135 if bin_ref(SERVE, NEED_OK)==1 { ok=1 } else { ok=0 } 136 gv_check("T19 REF-POSITIVE: serving binary is seen to reference a real organ" as *u8, ok, ctr) 137 138 if bin_ref(SERVE, NEED_BAD)==0 { ok=1 } else { ok=0 } 139 gv_check("T20 REF-NEGATIVE: an absent token is reported absent, not found" as *u8, ok, ctr) 140 141 if bin_ref(BADBIN, NEED_OK)==(0-1) { ok=1 } else { ok=0 } 142 gv_check("T21 REF-UNKNOWN: an unreadable binary returns UNKNOWN, never a false ABSENT" as *u8, ok, ctr) 143 144 // THE POINT OF THE UPGRADE: a capability whose artifact is deployed but which the serving binary 145 // never references must still be DARK. Deployment alone stops being sufficient. 146 if wired_ref(dep, sv_i, nbad_i)==0 { ok=1 } else { ok=0 } 147 gv_check("T22 DEPLOYED-BUT-UNREFERENCED is DARK (deployment is no longer enough)" as *u8, ok, ctr) 148 149 if wired_ref(dep, sv_i, nok_i)==1 { ok=1 } else { ok=0 } 150 gv_check("T23 DEPLOYED-AND-REFERENCED is WIRED" as *u8, ok, ctr) 151 152 // UNKNOWN must fall back to the weaker artifact test, not silently condemn a real capability. 153 if wired_ref(dep, bad_i, nok_i)==1 { ok=1 } else { ok=0 } 154 gv_check("T24 UNKNOWN falls back to artifact existence, never to a false DARK" as *u8, ok, ctr) 155 156 let rc: i64 = gv_verdict("MMBENCH" as *u8, ctr, "evidence audit demotes, never promotes; headline moves with it" as *u8) 157 sys_exit(rc) 158 return rc 159}