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" 10 11const PG_PREFIX: *u8 = "knowledge/store/plgate-" 12const PG_LOG: *u8 = "knowledge/status/pipeline_gate.log" 13 14func pg(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 15func pgn(v: i64) -> i64 { 16 let bb: *u8 = sys_mmap(28); var m: i64 = v 17 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m } 18 let t: *u8 = sys_mmap(28); var k: i64 = 0 19 if m == 0 { t[0] = 48 as u8; k = 1 } 20 while m > 0 { t[k] = ((48 + (m % 10)) as u8); m = m / 10; k = k + 1 } 21 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 22 sys_write(1, bb, k); return 0 23} 24 25func main(argc: i64, argv: *i64) -> i64 { 26 // T1 POS: in-order advance to EXCEEDED. 27 let s0: i64 = pl_seed_p(PG_PREFIX, "PL-A" as *u8, "demo gap: no-float training" as *u8) 28 let a2: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_DISCOVERED, "knowledge/fetched/x.raw" as *u8) 29 let a3: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_RESEARCHED, "knowledge/specs/x.spec" as *u8) 30 let a4: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_SPECED, "_offc/x.elf" as *u8) 31 let a5: i64 = pl_advance_p(PG_PREFIX, "PL-A" as *u8, PL_BUILT, "knowledge/status/x_exceed.log" as *u8) 32 var pass1: i64 = 0 33 if s0 == PL_DISCOVERED { if a2 == 2 { if a3 == 3 { if a4 == 4 { if a5 == 5 { pass1 = 1 } } } } } 34 35 // T2 NEG (invariant): a fresh item at DISCOVERED; try to SKIP to SPECED -> must be refused (-1) 36 // and the stage must stay DISCOVERED. 37 pl_seed_p(PG_PREFIX, "PL-B" as *u8, "skip attempt" as *u8) 38 let skip: i64 = pl_advance_p(PG_PREFIX, "PL-B" as *u8, PL_SPECED, "fabricated.elf" as *u8) 39 let stillB: i64 = pl_stage_p(PG_PREFIX, "PL-B" as *u8) 40 var pass2: i64 = 0 41 if skip == 0 - 1 { if stillB == PL_DISCOVERED { pass2 = 1 } } 42 43 // T3 HONEST: a never-seeded id is UNKNOWN (0), not a fake hit. 44 let unseen: i64 = pl_stage_p(PG_PREFIX, "PL-NEVER-SEEDED" as *u8) 45 var pass3: i64 = 0 46 if unseen == 0 { pass3 = 1 } 47 48 var green: i64 = 0 49 if pass1 == 1 { if pass2 == 1 { if pass3 == 1 { green = 1 } } } 50 51 pg("PIPELINE-GATE seedA=" as *u8); pgn(s0) 52 pg(" advA=" as *u8); pgn(a2); pg("," as *u8); pgn(a3); pg("," as *u8); pgn(a4); pg("," as *u8); pgn(a5) 53 pg(" skip_refused=" as *u8); pgn(skip); pg(" B_stage=" as *u8); pgn(stillB) 54 pg(" unseen=" as *u8); pgn(unseen) 55 pg(" T1=" as *u8); pgn(pass1); pg(" T2=" as *u8); pgn(pass2); pg(" T3=" as *u8); pgn(pass3) 56 57 let buf: *u8 = sys_mmap(512) 58 var o: i64 = 0 59 o = fa_cat(buf, o, "PIPELINE-GATE ts=\x00" as *u8); o = fa_catn(buf, o, sys_now_realtime_sec()) 60 o = fa_cat(buf, o, " T1=\x00" as *u8); o = fa_catn(buf, o, pass1) 61 o = fa_cat(buf, o, " T2=\x00" as *u8); o = fa_catn(buf, o, pass2) 62 o = fa_cat(buf, o, " T3=\x00" as *u8); o = fa_catn(buf, o, pass3) 63 if green == 1 { o = fa_cat(buf, o, " verdict=GREEN\x00" as *u8) } else { o = fa_cat(buf, o, " verdict=RED\x00" as *u8) } 64 fa_appendz(PG_LOG, buf, 512) 65 66 if green == 1 { pg(" verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 67 pg(" verdict=RED\n" as *u8); sys_exit(1); return 1 68}