nx_pipeline_gate.nx source

1// nx_pipeline_gate.nx -- proves the R1 pipeline spine. T1 a work-item advances IN ORDER to 2// EXCEEDED; T2 (load-bearing neg-control) a skip is REFUSED and the stage is unchanged (fabricated 3// completion is mechanically impossible); T3 a never-seeded id is honestly UNKNOWN (0). GREEN iff 4// all three. Uses a scratch prefix (cleaned by the harness before each run). license_tier: ORIGINAL 5import "nx_pipeline_spine.nx" 6import "nx_workstream_store.nx" 7import "nx_seg_store.nx" 8import "nx_framed_append.nx" 9import "nx_syscalls.nx" 10import "nx_gate_verdict.nx" 11 12const PG_PREFIX: *u8 = "knowledge/store/plgate-" 13const PG_LOG: *u8 = "knowledge/status/pipeline_gate.log" 14 15func pg(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 16func pgn(v: i64) -> i64 { 17 let bb: *u8 = sys_mmap(28); var m: i64 = v 18 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 19 let t: *u8 = sys_mmap(28); var k: i64 = 0 20 if m == 0 { t[0] = 48 as u8; k = 1 } 21 while m > 0 { t[k] = ((48 + (m % 10)) as u8); m = m / 10; k = k + 1 } 22 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 23 sys_write(1, bb, k); return 0 24} 25 26func main(argc: i64, argv: *i64) -> i64 { 27 // T1 POS: in-order advance to EXCEEDED. 28 let s0: i64 = pl_seed_p(PG_PREFIX, "PL-A" as *u8, "demo gap: no-float training" as *u8) 29 let a2: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_DISCOVERED, "knowledge/fetched/x.raw" as *u8) 30 let a3: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_RESEARCHED, "knowledge/specs/x.spec" as *u8) 31 let a4: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_SPECED, "_offc/x.elf" as *u8) 32 let a5: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_BUILT, "knowledge/status/x_exceed.log" as *u8) 33 var pass1: i64 = 0 34 if s0 == PL_DISCOVERED { if a2 == 2 { if a3 == 3 { if a4 == 4 { if a5 == 5 { pass1 = 1 } } } } } 35 36 // T2 NEG (invariant): a fresh item at DISCOVERED; try to SKIP to SPECED -> must be refused (-1) 37 // and the stage must stay DISCOVERED. 38 pl_seed_p(PG_PREFIX, "PL-B" as *u8, "skip attempt" as *u8) 39 let skip: i64 = pl_advance_p(PG_PREFIX, "PL-B" as *u8, PL_SPECED, "fabricated.elf" as *u8) 40 let stillB: i64 = pl_stage_p(PG_PREFIX, "PL-B" as *u8) 41 var pass2: i64 = 0 42 if skip == 0 - 1 { if stillB == PL_DISCOVERED { pass2 = 1 } } 43 44 // T3 HONEST: a never-seeded id is UNKNOWN (0), not a fake hit. 45 let unseen: i64 = pl_stage_p(PG_PREFIX, "PL-NEVER-SEEDED" as *u8) 46 var pass3: i64 = 0 47 if unseen == 0 { pass3 = 1 } 48 49 var green: i64 = 0 50 if pass1 == 1 { if pass2 == 1 { if pass3 == 1 { green = 1 } } } 51 52 pg("PIPELINE-GATE seedA=" as *u8); pgn(s0) 53 pg(" advA=" as *u8); pgn(a2); pg("," as *u8); pgn(a3); pg("," as *u8); pgn(a4); pg("," as *u8); pgn(a5) 54 pg(" skip_refused=" as *u8); pgn(skip); pg(" B_stage=" as *u8); pgn(stillB) 55 pg(" unseen=" as *u8); pgn(unseen) 56 pg(" T1=" as *u8); pgn(pass1); pg(" T2=" as *u8); pgn(pass2); pg(" T3=" as *u8); pgn(pass3) 57 58 let buf: *u8 = sys_mmap(512) 59 var o: i64 = 0 60 o = fa_cat(buf, o, "PIPELINE-GATE ts=\x00" as *u8); o = fa_catn(buf, o, sys_now_realtime_sec()) 61 o = fa_cat(buf, o, " T1=\x00" as *u8); o = fa_catn(buf, o, pass1) 62 o = fa_cat(buf, o, " T2=\x00" as *u8); o = fa_catn(buf, o, pass2) 63 o = fa_cat(buf, o, " T3=\x00" as *u8); o = fa_catn(buf, o, pass3) 64 if green == 1 { o = fa_cat(buf, o, " verdict=GREEN\x00" as *u8) } else { o = fa_cat(buf, o, " verdict=RED\x00" as *u8) } 65 fa_appendz(PG_LOG, buf, 512) 66 67 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 68 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 69 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 70 let ctr__dry: *i64 = gv_ctr() 71 ctr__dry[0] = green 72 ctr__dry[1] = 1 73 let rc__dry: i64 = gv_verdict("PIPELINE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 74 sys_exit(rc__dry) 75 return rc__dry 76}