code wiki / _hdl_build / nx_gaterigor_gate.nx
nx_gaterigor_gate.nx source
↩ module page · 112 lines · 5467 B
1// nx_gaterigor_gate.nx -- GATE for the junk auditor (5 teeth). ITS OWN neg-control makes it rigorous
2// by its own standard (self-consistency = a NASA/DARPA property). PREREQ: stage _offc/nx_gaterigor.elf.
3// Fixture dir /tmp/grdir with a_gate.nx (has "neg-control" = RIGOROUS), b_gate.nx (no marker = VACUOUS),
4// notagate.nx (ignored). T1 vacuous named | T2 rigorous NOT flagged | T3 summary gates=2 vacuous=1 |
5// T4 determinism | T5 MUTATION: add "mutation" marker to b_gate -> now RIGOROUS -> vacuous=0.
6// license_tier: ORIGINAL No hw writes (Rule 26).
7import "nx_seat_drive_lib.nx"
8import "nx_seg_store.nx"
9import "nx_deploy_lib.nx"
10import "nx_syscalls.nx"
11
12func rg_atoi(s: *u8) -> i64 { var v: i64 = 0; var i: i64 = 0; while s[i] != (0 as u8) { let c: i64 = s[i] as i64; if c >= 48 { if c <= 57 { v = v * 10 + (c - 48) } } i = i + 1 } return v }
13func rg_itoa(dst: *u8, v: i64) -> i64 { var m: i64 = v; let t: *u8 = sys_mmap(24); var k: i64 = 0; if m == 0 { t[0] = 48 as u8; k = 1 } while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } var i: i64 = 0; while i < k { dst[i] = t[k - 1 - i]; i = i + 1 } dst[k] = 0 as u8; return k }
14func rg_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
15
16func rg_run(dir: *u8, outp: *u8) -> i64 {
17 let av: *i64 = sys_mmap(16) as *i64
18 av[0] = dir as i64
19 return dep_run_capture("_offc/nx_gaterigor.elf" as *u8, av, 1, outp)
20}
21
22func rg_seed(mutate: i64) -> i64 {
23 sys_mkdir("/tmp/grdir" as *u8, 0x1ed)
24 let ag: *u8 = "// a rigorous gate with a neg-control tooth\nfunc main() -> i64 { return 0 }\n" as *u8
25 ss_writefile("/tmp/grdir/a_gate.nx" as *u8, ag, rg_len(ag))
26 var bg: *u8 = "// a gate with only positive assertions, no way to fail\nfunc main() -> i64 { return 0 }\n" as *u8
27 if mutate == 1 { bg = "// now with a mutation tooth\nfunc main() -> i64 { return 0 }\n" as *u8 }
28 ss_writefile("/tmp/grdir/b_gate.nx" as *u8, bg, rg_len(bg))
29 let ng: *u8 = "// not a gate file\nfunc main() -> i64 { return 0 }\n" as *u8
30 ss_writefile("/tmp/grdir/notagate.nx" as *u8, ng, rg_len(ng))
31 return 0
32}
33
34func main(argc: i64, argv: *i64) -> i64 {
35 var stage: i64 = 1
36 var pass: i64 = 0
37 if argc >= 2 { let ss1: *u8 = argv[1] as *u8; stage = rg_atoi(ss1) }
38 if argc >= 3 { let ps: *u8 = argv[2] as *u8; pass = rg_atoi(ps) }
39 if stage < 1 { stage = 1 }
40
41 if stage == 1 {
42 rg_seed(0)
43 let rc: i64 = rg_run("/tmp/grdir" as *u8, "/tmp/gr_t1.out" as *u8)
44 let out: *u8 = sys_mmap(16384)
45 let n: i64 = dp_read("/tmp/gr_t1.out" as *u8, out, 16384)
46 var ok: i64 = 0
47 if rc == 0 { if sd_count(out, n, "VACUOUS /tmp/grdir/b_gate.nx" as *u8) == 1 { ok = 1 } }
48 if ok == 1 { sd_w("T1 vacuous-named PASS\n" as *u8); pass = pass + 1 } else { sd_w("T1 vacuous-named FAIL\n" as *u8) }
49 }
50 if stage == 2 {
51 let out: *u8 = sys_mmap(16384)
52 let n: i64 = dp_read("/tmp/gr_t1.out" as *u8, out, 16384)
53 var ok: i64 = 0
54 if sd_count(out, n, "VACUOUS /tmp/grdir/a_gate.nx" as *u8) == 0 { ok = 1 }
55 if ok == 1 { sd_w("T2 rigorous-not-flagged PASS\n" as *u8); pass = pass + 1 } else { sd_w("T2 rigorous-not-flagged FAIL\n" as *u8) }
56 }
57 if stage == 3 {
58 let out: *u8 = sys_mmap(16384)
59 let n: i64 = dp_read("/tmp/gr_t1.out" as *u8, out, 16384)
60 var ok: i64 = 0
61 if sd_count(out, n, "gates=2 rigorous=1 vacuous=1" as *u8) == 1 { ok = 1 }
62 if ok == 1 { sd_w("T3 summary-exact PASS\n" as *u8); pass = pass + 1 } else { sd_w("T3 summary-exact FAIL\n" as *u8) }
63 }
64 if stage == 4 {
65 let rc: i64 = rg_run("/tmp/grdir" as *u8, "/tmp/gr_t4.out" as *u8)
66 let a: *u8 = sys_mmap(16384)
67 let an: i64 = dp_read("/tmp/gr_t1.out" as *u8, a, 16384)
68 let b: *u8 = sys_mmap(16384)
69 let bn: i64 = dp_read("/tmp/gr_t4.out" as *u8, b, 16384)
70 var same: i64 = 0
71 if rc == 0 { if an == bn { if an > 0 { same = 1; var i: i64 = 0; while i < an { if a[i] != b[i] { same = 0; i = an } else { i = i + 1 } } } } }
72 if same == 1 { sd_w("T4 deterministic PASS\n" as *u8); pass = pass + 1 } else { sd_w("T4 deterministic FAIL\n" as *u8) }
73 }
74 if stage == 5 {
75 rg_seed(1)
76 let rc: i64 = rg_run("/tmp/grdir" as *u8, "/tmp/gr_t5.out" as *u8)
77 let out: *u8 = sys_mmap(16384)
78 let n: i64 = dp_read("/tmp/gr_t5.out" as *u8, out, 16384)
79 var ok: i64 = 0
80 if rc == 0 { if sd_count(out, n, "vacuous=0 " as *u8) == 1 { ok = 1 } }
81 if ok == 1 { sd_w("T5 mutation-flips-rigorous PASS\n" as *u8); pass = pass + 1 } else { sd_w("T5 mutation-flips-rigorous FAIL\n" as *u8) }
82 }
83
84 if stage >= 5 {
85 sd_w("NX-GATERIGOR-GATE pass=" as *u8)
86 let pb: *u8 = sys_mmap(8)
87 pb[0] = (48 + pass) as u8
88 pb[1] = 0 as u8
89 sd_w(pb)
90 if pass == 5 { sd_w("/5 verdict=GREEN\n" as *u8); sys_exit(0); return 0 }
91 sd_w("/5 verdict=RED\n" as *u8)
92 sys_exit(1)
93 return 1
94 }
95
96 let self: *u8 = argv[0] as *u8
97 let sb: *u8 = sys_mmap(24)
98 rg_itoa(sb, stage + 1)
99 let pb2: *u8 = sys_mmap(24)
100 rg_itoa(pb2, pass)
101 let nav: *i64 = sys_mmap(40) as *i64
102 nav[0] = self as i64
103 nav[1] = sb as i64
104 nav[2] = pb2 as i64
105 nav[3] = 0
106 let envp: *i64 = sys_mmap(16) as *i64
107 envp[0] = 0
108 sys_execve(self, nav, envp)
109 sd_w("GRG-EXEC-FAIL\n" as *u8)
110 sys_exit(1)
111 return 1
112}