code wiki / _hdl_build / nx_rankmap_gate.nx

nx_rankmap_gate.nx source

↩ module page · 63 lines · 3625 B

1// nx_rankmap_gate.nx -- proves the ranking vocabulary is TOTAL, AXIS-SPLIT, and UNGAMEABLE. 2// 3// The anti-gaming property is only worth stating if something asserts it. T7/T8 are the load-bearing 4// teeth: NO coverage percentage may reach a COMPARATIVE rung. T9 is the live check against the 5// actual deriving function -- permil_to_level must never return a comparative level for ANY input 6// 0..1000, which is swept exhaustively rather than sampled. That is the tooth that would have caught 7// the original defect (p>=700 -> S-CLASS) on the day it shipped. 8// license_tier: ORIGINAL No hw writes (Rule 26). 9import "nx_rankmap.nx" 10import "nx_ecomat_lib.nx" 11import "nx_gate_verdict.nx" 12 13func rg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 14 15func main(argc: i64, argv: *i64) -> i64 { 16 let ctr: *i64 = gv_ctr() 17 gv_head("nx_rankmap -- one vocabulary, axes split, comparative rungs unreachable by a number" as *u8) 18 19 // TOTALITY: every level 0..5 must map to a label, a TRL band, an axis and an evidence clause. 20 var total: i64 = 1 21 var l: i64 = 0 22 while l < MAT_NLEVELS { 23 if (mat_label(l) as i64) == 0 { total = 0 } 24 if (rm_trl(l) as i64) == 0 { total = 0 } 25 if (rm_evidence(l) as i64) == 0 { total = 0 } 26 if (rm_capgraph(l) as i64) == 0 { total = 0 } 27 l = l + 1 28 } 29 gv_check("T1 mapping is TOTAL over all 6 levels (label/TRL/axis/evidence/sibling)" as *u8, total, ctr) 30 31 gv_check("T2 level 0-2 are CAPABILITY axis" as *u8, rg_eq(rm_axis(MAT_FUNCTIONAL), RM_AXIS_CAPABILITY), ctr) 32 gv_check("T3 PRODUCTION is CAPABILITY axis" as *u8, rg_eq(rm_axis(MAT_PRODUCTION), RM_AXIS_CAPABILITY), ctr) 33 gv_check("T4 S-CLASS is COMPARATIVE axis" as *u8, rg_eq(rm_axis(MAT_SCLASS), RM_AXIS_COMPARATIVE), ctr) 34 gv_check("T5 EXCEED is COMPARATIVE axis" as *u8, rg_eq(rm_axis(MAT_EXCEED), RM_AXIS_COMPARATIVE), ctr) 35 36 // THE STRUCTURAL PROOF: the two comparative rungs share one readiness band. If they ever stop 37 // sharing it, the split-axis argument itself needs revisiting -- so pin it. 38 gv_check("T6 S-CLASS and EXCEED share the SAME TRL band (readiness saturates; only the comparison differs)" as *u8, rg_eq(el_streq(rm_trl(MAT_SCLASS), rm_trl(MAT_EXCEED)), 1), ctr) 39 40 gv_check("T7 ANTI-GAMING S-CLASS is NOT permil-reachable" as *u8, rg_eq(rm_permil_reachable(MAT_SCLASS), 0), ctr) 41 gv_check("T8 ANTI-GAMING EXCEED is NOT permil-reachable" as *u8, rg_eq(rm_permil_reachable(MAT_EXCEED), 0), ctr) 42 43 // T9 -- THE LIVE SWEEP. Not a sample: every permil 0..1000 is fed to the ACTUAL deriving 44 // function, and none may yield a comparative level. This is the tooth that fails loudly if 45 // anyone re-introduces p>=700 -> S-CLASS. 46 var worst: i64 = 0 47 var p: i64 = 0 48 while p <= 1000 { 49 let lv: i64 = permil_to_level(p) 50 if lv > worst { worst = lv } 51 p = p + 1 52 } 53 gv_check("T9 LIVE SWEEP permil_to_level(0..1000) never returns a COMPARATIVE level" as *u8, rg_eq(rm_axis(worst), RM_AXIS_CAPABILITY), ctr) 54 gv_check("T10 LIVE SWEEP its ceiling is exactly PRODUCTION" as *u8, rg_eq(worst, MAT_PRODUCTION), ctr) 55 56 // NEG-CONTROL: the sweep must be able to SEE a comparative level, otherwise T9 passes vacuously 57 // on a function that returns nothing at all. 58 gv_check("T11 NEG-CONTROL rm_axis DOES classify a comparative level when given one" as *u8, rg_eq(rm_axis(MAT_EXCEED), RM_AXIS_COMPARATIVE), ctr) 59 60 let rc: i64 = gv_verdict("RANKMAP" as *u8, ctr, "axes split, TRL-anchored, comparative rungs unreachable by any coverage number" as *u8) 61 sys_exit(rc) 62 return rc 63}