nx_gensota_gate.nx source
↩ module page · 46 lines · 2236 B
1// nx_gensota_gate.nx -- executable proof for the per-generation rollup instrument.
2// Imports gs_run DIRECTLY (main stripped by expand_imports) -- no fork, no PATH.
3// Teeth prove the instrument BITES BOTH WAYS on the REAL store:
4// T1 runs GREEN at bar=0 (partition sums, BFS completes, every gen printed)
5// T2 neg-control: bar=1001 permil is unsatisfiable -> MUST return RED(1);
6// a rollup that cannot fail is not an instrument
7// T3 blind is not green: an absent store MUST return INSTRUMENT-BLIND(3), not 0
8// T4 absent bars conf reads as -1 (the caller REFUSES rather than defaults)
9// T5 the deployed bars conf parses to a sane permil (0..1000)
10// license_tier: ORIGINAL expect_exit:0 No hw writes (Rule 26).
11import "nx_syscalls.nx"
12import "nx_gate_verdict.nx"
13import "nx_gensota.nx"
14
15const GG_RC_GREEN: i64 = 0
16const GG_RC_RED: i64 = 1
17const GG_RC_BLIND: i64 = 3
18
19func main() -> i64 {
20 let ctr: *i64 = gv_ctr()
21 gv_head("NX-GENSOTA-GATE -- the generation rollup bites both ways" as *u8)
22 let store: *u8 = "knowledge/store/ecograph_full\x00" as *u8
23 let rc1: i64 = gs_run(store, 0, 2)
24 var t1: i64 = 0
25 if rc1 == GG_RC_GREEN { t1 = 1 }
26 gv_check("T1 live store at bar=0 runs GREEN (partition sums)" as *u8, t1, ctr)
27 let rc2: i64 = gs_run(store, 1001, 2)
28 var t2: i64 = 0
29 if rc2 == GG_RC_RED { t2 = 1 }
30 gv_check("T2 neg-control bar=1001 goes RED (instrument can fail)" as *u8, t2, ctr)
31 let rc3: i64 = gs_run("knowledge/store/gensota_absent_fixture_zz\x00" as *u8, 500, 2)
32 var t3: i64 = 0
33 if rc3 == GG_RC_BLIND { t3 = 1 }
34 gv_check("T3 absent store reads INSTRUMENT-BLIND, never GREEN" as *u8, t3, ctr)
35 let rb1: i64 = gs_read_bar("knowledge/gensota_bars_absent_zz.conf\x00" as *u8)
36 var t4: i64 = 0
37 if rb1 < 0 { t4 = 1 }
38 gv_check("T4 absent bars conf parses to refuse-value" as *u8, t4, ctr)
39 let rb2: i64 = gs_read_bar("knowledge/gensota_bars.conf\x00" as *u8)
40 var t5: i64 = 0
41 if rb2 >= 0 { if rb2 <= 1000 { t5 = 1 } }
42 gv_check("T5 deployed bars conf parses to a sane permil" as *u8, t5, ctr)
43 let rc: i64 = gv_verdict("GENSOTA-GATE" as *u8, ctr, "rollup measured, refusals fail-closed" as *u8)
44 sys_exit(rc)
45 return 0
46}