nx_flatstore_flip_gate.nx source
↩ module page · 67 lines · 3615 B
1// nx_flatstore_flip_gate.nx -- proves the GENERIC store-law flip primitive (nx_flatstore_flip) works on a planted
2// fixture: writes a temp .conf (3 data rows + comments + a blank line), flips it to a temp seg_store, and checks
3// migrate byte-exactness (ver==tot==3), round-trip (fsf_count==3), reader reconstruction (fsf_read_all = 3 lines,
4// row 0 == the first data line), + neg-controls (no phantom row past the end; the byte compare has teeth). Run
5// standalone (CWD=nxc2; fixture + store live under /tmp). license_tier: ORIGINAL
6import "nx_flatstore_flip.nx"
7import "nx_syscalls.nx"
8
9func gp(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10func gn(v: i64) -> i64 {
11 let t: *u8=sys_mmap(24); var m: i64=v; var k: i64=0
12 if m==0 { t[0]=48 as u8; k=1 }
13 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 }
14 let o: *u8=sys_mmap(24); var i: i64=0; while i<k { o[i]=t[k-1-i]; i=i+1 } sys_write(1,o,k); return 0
15}
16func gred(msg: *u8) -> i64 { gp(" RED: " as *u8); gp(msg); gp("\n" as *u8); sys_exit(1); return 1 }
17func gstreq(a: *u8, b: *u8) -> i64 { var i: i64=0; while a[i]!=(0 as u8){ if a[i]!=b[i]{return 0} i=i+1 } if b[i]!=(0 as u8){return 0} return 1 }
18
19const FX_CONF: *u8 = "/tmp/fsf_fixture.conf"
20const FX_STORE: *u8 = "/tmp/fsf_store"
21const FX_KEY: *u8 = "fsftest:row:"
22
23func main() -> i64 {
24 gp("=== nx_flatstore_flip_gate: prove the GENERIC flip primitive on a planted fixture ===\n" as *u8)
25
26 // plant the fixture .conf: 3 DATA rows (alpha/beta/gamma) among comments + a blank line
27 let fd: i64 = sys_openat_wr(FX_CONF, 0x1a4)
28 if fd < 0 { gred("cannot write fixture conf") }
29 let fx: *u8 = "# fixture comment\nalpha|1|x\nbeta|2|y\n\n# c2\ngamma|3|z\n" as *u8
30 var fl: i64 = 0; while fx[fl]!=(0 as u8){ fl=fl+1 }
31 sys_write(fd, fx, fl); sys_close(fd)
32
33 // T1 -- migrate byte-exact (3 data rows; comments + blank skipped)
34 let totp: *i64 = sys_mmap(16) as *i64
35 let verp: *i64 = sys_mmap(16) as *i64
36 fsf_migrate(FX_CONF, FX_STORE, FX_KEY, totp, verp)
37 let tot: i64 = totp[0]
38 let ver: i64 = verp[0]
39 gp(" T1 migrate: tot=" as *u8); gn(tot); gp(" verified=" as *u8); gn(ver); gp("\n" as *u8)
40 if tot != 3 { gred("expected 3 data rows (comments + blank must be skipped)") }
41 if ver != tot { gred("byte-verify mismatch (store row != conf row)") }
42
43 // T2 -- round-trip
44 let cnt: i64 = fsf_count(FX_STORE, FX_KEY)
45 gp(" T2 fsf_count=" as *u8); gn(cnt); gp("\n" as *u8)
46 if cnt != tot { gred("fsf_count != tot") }
47
48 // T3 -- reader reconstructs 3 lines; row 0 is the first data line byte-exact
49 let buf: *u8 = sys_mmap(4096)
50 let rlen: i64 = fsf_read_all(FX_STORE, FX_KEY, buf, 4096)
51 var lines: i64 = 0; var i: i64 = 0
52 while i < rlen { if buf[i]==(10 as u8) { lines=lines+1 } i=i+1 }
53 gp(" T3 fsf_read_all bytes=" as *u8); gn(rlen); gp(" lines=" as *u8); gn(lines); gp("\n" as *u8)
54 if lines != tot { gred("read_all line count != tot") }
55 let r0: *u8 = sys_mmap(256)
56 fsf_row(FX_STORE, FX_KEY, 0, r0, 256)
57 if gstreq(r0, "alpha|1|x" as *u8) != 1 { gred("row 0 != 'alpha|1|x' (order/content drift)") }
58
59 // T4 -- neg-controls
60 let past: *u8 = sys_mmap(256)
61 if fsf_row(FX_STORE, FX_KEY, tot, past, 256) != (0 - 1) { gred("neg-control FAIL: phantom row past the end") }
62 if gstreq(r0, "not_a_real_row" as *u8) == 1 { gred("neg-control FAIL: comparison matched a wrong string (no teeth)") }
63
64 gp("\nFLATSTORE-FLIP GATE GREEN -- generic primitive: 3/3 byte-exact, count + reader + neg-controls hold.\n" as *u8)
65 sys_exit(0)
66 return 0
67}