nx_pabi_native_core_gate.nx source
↩ module page · 216 lines · 8914 B
1// nx_pabi_native_core_gate.nx -- F103b "pabi-native core byte-exact" (os lane, M3; dep F103a=D 2026-07-21).
2// THE CLAIM: the NishiOS-NATIVE pabi core (block-VFS files/dirs + verified-NXE exec + the portable
3// forge judge) is BYTE-EXACT with the linux-host lane at WORKLOAD SCALE. nx_pabi_gate proves
4// single-op identity; THIS gate proves the core: a 24-file binary workload (block-boundary sizes
5// 255/256/257/512, embedded 0x00/0xFF bytes, >15KB total) + a 5-arg exec sweep (fork lane vs
6// verified-NXE lane) + the judge loop, folded into ORDER-SENSITIVE rolling checksums that must be
7// IDENTICAL across substrates, plus per-file byte-diff (mism==0). D001: emits the nx_gate_verdict
8// contract. REFUTATION: argv[1]=negctl corrupts ONE byte of ONE nishios payload -> the byte-exact
9// teeth (C02/C03) MUST go RED; registered sibling tool nx_pabi_native_negtest pins that arg.
10// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26).
11import "nx_pabi.nx"
12import "nx_gate_verdict.nx"
13
14const PN_NF: i64 = 24
15const PN_BUF: i64 = 8192
16const PN_EXECN: i64 = 5
17
18// deterministic size table: boundary sizes first, then arithmetic tail (all well under vfs data budget)
19func pn_sz(i: i64) -> i64 {
20 if i == 0 { return 1 }
21 if i == 1 { return 255 }
22 if i == 2 { return 256 }
23 if i == 3 { return 257 }
24 if i == 4 { return 512 }
25 if i == 5 { return 2000 }
26 if i == 6 { return 4000 }
27 if i == 7 { return 64 }
28 return 50 + ((i * 37) % 900)
29}
30
31// deterministic binary payload: LCG bytes + planted 0x00 and 0xFF (embedded-NUL correctness rides dlen)
32func pn_fill(buf: *u8, seed: i64, sz: i64) -> i64 {
33 var s: i64 = seed * 48271 + 12345
34 var k: i64 = 0
35 while k < sz {
36 s = s * 1103515245 + 12345
37 let b: i64 = (s >> 16) & 255
38 buf[k] = b as u8
39 k = k + 1
40 }
41 if sz >= 4 { buf[1] = 0 as u8; buf[2] = 255 as u8 }
42 return 0
43}
44
45func pn_copy(dst: *u8, off: i64, src: *u8) -> i64 {
46 var i: i64 = 0
47 while src[i] != (0 as u8) { dst[off + i] = src[i]; i = i + 1 }
48 dst[off + i] = 0 as u8
49 return off + i
50}
51
52func pn_d2(buf: *u8, off: i64, v: i64) -> i64 {
53 let d1: i64 = (v / 10) % 10
54 buf[off] = (48 + d1) as u8
55 let d0: i64 = v % 10
56 buf[off + 1] = (48 + d0) as u8
57 buf[off + 2] = 0 as u8
58 return 0
59}
60
61// order-sensitive rolling fold (vb_sum family): a swapped pair changes it; length folded too
62func pn_fold(ck: i64, buf: *u8, n: i64) -> i64 {
63 var s: i64 = ck
64 var k: i64 = 0
65 while k < n { s = s * 131 + (buf[k] as i64); k = k + 1 }
66 s = s * 1000003 + n
67 return s
68}
69
70func main(argc: i64, argv: *i64) -> i64 {
71 var neg: i64 = 0
72 if argc >= 2 {
73 let a1v: i64 = argv[1]
74 let a1: *u8 = a1v as *u8
75 if a1[0] == (110 as u8) { if a1[1] == (101 as u8) { if a1[2] == (103 as u8) { neg = 1 } } }
76 }
77 let ctr: *i64 = gv_ctr()
78 gv_head("PABI-NATIVE-CORE (F103b) -- NishiOS-native pabi core (block-VFS + verified-NXE exec + portable judge) BYTE-EXACT vs the linux-host lane at workload scale" as *u8)
79 if neg == 1 { gv_puts(" [negctl] ONE byte of ONE nishios payload corrupted -- byte-exact teeth MUST go RED\n" as *u8) }
80 let pbuf: *u8 = sys_mmap(PN_BUF) as *u8
81 let qbuf: *u8 = sys_mmap(PN_BUF) as *u8
82 let lxb: *u8 = sys_mmap(PN_BUF) as *u8
83 let nsb: *u8 = sys_mmap(PN_BUF) as *u8
84 let img: *u8 = pabi_nishios_new()
85 var ck_lx: i64 = 7
86 var ck_ns: i64 = 7
87 var errs: i64 = 0
88 var mism: i64 = 0
89 var tbytes: i64 = 0
90 var i: i64 = 0
91 while i < PN_NF {
92 let sz: i64 = pn_sz(i)
93 pn_fill(pbuf, i, sz)
94 var k: i64 = 0
95 while k < sz { qbuf[k] = pbuf[k]; k = k + 1 }
96 if neg == 1 { if i == 5 { let ob: i64 = qbuf[3] as i64; qbuf[3] = (ob ^ 1) as u8 } }
97 let lp: *u8 = sys_mmap(64) as *u8
98 let e1: i64 = pn_copy(lp, 0, "/tmp/f103b_" as *u8)
99 pn_d2(lp, e1, i)
100 let w1: i64 = pabi_write(PABI_LINUX, 0 as *u8, lp, pbuf, sz)
101 let n1: i64 = pabi_read(PABI_LINUX, 0 as *u8, lp, lxb, PN_BUF)
102 if w1 != 0 { errs = errs + 1 }
103 if n1 != sz { errs = errs + 1 }
104 let np: *u8 = sys_mmap(64) as *u8
105 let e2: i64 = pn_copy(np, 0, "/core_" as *u8)
106 pn_d2(np, e2, i)
107 let w2: i64 = pabi_write(PABI_NISHIOS, img, np, qbuf, sz)
108 let n2: i64 = pabi_read(PABI_NISHIOS, img, np, nsb, PN_BUF)
109 if w2 != 0 { errs = errs + 1 }
110 if n2 != sz { errs = errs + 1 }
111 var d: i64 = 0
112 if n1 != n2 { d = 1 }
113 if d == 0 { var m: i64 = 0; while m < n1 { if lxb[m] != nsb[m] { d = 1; m = n1 } else { m = m + 1 } } }
114 if d == 1 { mism = mism + 1 }
115 ck_lx = pn_fold(ck_lx, lxb, n1)
116 ck_ns = pn_fold(ck_ns, nsb, n2)
117 tbytes = tbytes + sz
118 i = i + 1
119 }
120 let mkl: i64 = pabi_mkdir(PABI_LINUX, 0 as *u8, "/tmp/f103b_dir" as *u8)
121 let exl: i64 = pabi_exists(PABI_LINUX, 0 as *u8, "/tmp/f103b_dir" as *u8)
122 let mkn: i64 = pabi_mkdir(PABI_NISHIOS, img, "/coredir" as *u8)
123 let exn: i64 = pabi_exists(PABI_NISHIOS, img, "/coredir" as *u8)
124 let ax: i64 = pabi_exists(PABI_LINUX, 0 as *u8, "/tmp/f103b_absent_zz" as *u8)
125 let an: i64 = pabi_exists(PABI_NISHIOS, img, "/absent_zz" as *u8)
126 let rn: i64 = pabi_read(PABI_NISHIOS, img, "/absent_zz" as *u8, nsb, PN_BUF)
127 var exok: i64 = 0
128 var ckx_lx: i64 = 3
129 var ckx_ns: i64 = 3
130 var a: i64 = 0
131 while a < PN_EXECN {
132 let arg: i64 = a * 53
133 let want: i64 = (arg + 100) & 255
134 let r1: i64 = pabi_exec(PABI_LINUX, arg)
135 let r2: i64 = pabi_exec(PABI_NISHIOS, arg)
136 ckx_lx = ckx_lx * 131 + r1
137 ckx_ns = ckx_ns * 131 + r2
138 if r1 == want { if r2 == want { exok = exok + 1 } }
139 a = a + 1
140 }
141 let jimg1: *u8 = pabi_nishios_new()
142 let jl1: i64 = pabi_judge(PABI_LINUX, 0 as *u8, 7, "107" as *u8, 3)
143 let jn1: i64 = pabi_judge(PABI_NISHIOS, jimg1, 7, "107" as *u8, 3)
144 let jimg2: *u8 = pabi_nishios_new()
145 let jl2: i64 = pabi_judge(PABI_LINUX, 0 as *u8, 42, "142" as *u8, 3)
146 let jn2: i64 = pabi_judge(PABI_NISHIOS, jimg2, 42, "142" as *u8, 3)
147 let jimg3: *u8 = pabi_nishios_new()
148 let jlr: i64 = pabi_judge(PABI_LINUX, 0 as *u8, 7, "999" as *u8, 3)
149 let jnr: i64 = pabi_judge(PABI_NISHIOS, jimg3, 7, "999" as *u8, 3)
150 gv_puts(" evidence: files=" as *u8)
151 gv_num(PN_NF)
152 gv_puts(" bytes=" as *u8)
153 gv_num(tbytes)
154 gv_puts(" ck_lx=" as *u8)
155 gv_num(ck_lx)
156 gv_puts(" ck_ns=" as *u8)
157 gv_num(ck_ns)
158 gv_puts(" ckx_lx=" as *u8)
159 gv_num(ckx_lx)
160 gv_puts(" ckx_ns=" as *u8)
161 gv_num(ckx_ns)
162 gv_puts(" errs=" as *u8)
163 gv_num(errs)
164 gv_puts(" mism=" as *u8)
165 gv_num(mism)
166 gv_puts(" mkl=" as *u8)
167 gv_num(mkl)
168 gv_puts("\n" as *u8)
169 var t: i64 = 0
170 if errs == 0 { t = 1 }
171 gv_check("C01 all writes+reads completed on BOTH substrates (errs==0)" as *u8, t, ctr)
172 t = 0
173 if ck_lx == ck_ns { t = 1 }
174 gv_check("C02 BYTE-EXACT rolling checksum identical across substrates" as *u8, t, ctr)
175 t = 0
176 if mism == 0 { t = 1 }
177 gv_check("C03 per-file byte-diff: zero mismatching files" as *u8, t, ctr)
178 t = 0
179 if tbytes > 15000 { t = 1 }
180 gv_check("C04 non-vacuous scale: workload above 15000 bytes" as *u8, t, ctr)
181 t = 0
182 if ck_lx != 7 { t = 1 }
183 gv_check("C05 checksum moved off its seed (bytes really folded)" as *u8, t, ctr)
184 let b1: i64 = pn_sz(1)
185 let b2: i64 = pn_sz(2)
186 let b3: i64 = pn_sz(3)
187 let b4: i64 = pn_sz(4)
188 let bsum: i64 = b1 + b2 + b3 + b4
189 t = 0
190 if bsum == 1280 { t = 1 }
191 gv_check("C06 block-boundary sizes exercised (255+256+257+512)" as *u8, t, ctr)
192 t = 0
193 if pbuf[1] == (0 as u8) { if pbuf[2] == (255 as u8) { t = 1 } }
194 gv_check("C07 binary alphabet: embedded 0x00 and 0xFF bytes in payloads" as *u8, t, ctr)
195 t = 0
196 if exl == 1 { if mkn == 0 { if exn == 1 { t = 1 } } }
197 gv_check("C08 dir identity: mkdir+exists on host-fs AND block-vfs" as *u8, t, ctr)
198 t = 0
199 if ax == 0 { if an == 0 { if rn < 0 { t = 1 } } }
200 gv_check("C09 NEG absent: exists=0 both lanes and vfs read -1 (nothing fabricated)" as *u8, t, ctr)
201 t = 0
202 if exok == PN_EXECN { t = 1 }
203 gv_check("C10 exec sweep: 5 args verdict-correct on BOTH lanes (fork == verified-NXE)" as *u8, t, ctr)
204 t = 0
205 if ckx_lx == ckx_ns { t = 1 }
206 gv_check("C11 exec verdict stream byte-exact across substrates" as *u8, t, ctr)
207 t = 0
208 if jl1 == 1 { if jn1 == 1 { if jl2 == 1 { if jn2 == 1 { t = 1 } } } }
209 gv_check("C12 portable judge GREEN on both lanes (2 candidates)" as *u8, t, ctr)
210 t = 0
211 if jlr == 0 { if jnr == 0 { t = 1 } }
212 gv_check("C13 judge REJECTS wrong-expected on both lanes (cheat-proof)" as *u8, t, ctr)
213 let rc: i64 = gv_verdict("PABI-NATIVE-CORE" as *u8, ctr, "F103b native core byte-exact vs linux lane at workload scale" as *u8)
214 sys_exit(rc)
215 return rc
216}