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}