code wiki / _hdl_build / _atomic_rewrite_gate.nx
_atomic_rewrite_gate.nx source
↩ module page · 176 lines · 8738 B
1// _atomic_rewrite_gate.nx -- WMS-R3 gate. PROVES the generic atomic_rewrite
2// primitive (nx_atomic_rewrite.nx) is crash-safe, with a WORKING NEGATIVE
3// CONTROL (the old in-place rewrite) that demonstrably tears under the SAME
4// crash point -- so the gate can actually detect failure (no false green).
5//
6// All four sub-tests run on real /tmp victim files (NO mocks):
7//
8// (1) commit_ok -- atomic_rewrite(v1) then atomic_rewrite(v2): reader sees
9// exactly v2, NOT v1 (clean whole-file replace works).
10// (2) crash_safe -- establish v1 on disk; a FORKED CHILD calls ar_crashwrite
11// (stage temp + fsync, NO rename) then exits; a FRESH
12// reader of the live path still sees EXACTLY v1, intact
13// (the headline crash-before-commit claim). Then a real
14// atomic_rewrite(v2) -> reader now sees v2 (after_commit).
15// (3) neg_torn -- NEGATIVE CONTROL: a FORKED CHILD runs the OLD unguarded
16// ar_unsafe_inplace, which TRUNCATES the live file then
17// writes only HALF the new bytes, then exits (crash
18// mid-write). A fresh reader sees a TORN file: neither
19// the intact previous content NOR the full new content.
20// If this does NOT tear, the gate is INVALID -> RED.
21// (4) tamper_bites -- atomic_rewrite to an UNWRITABLE path (bad dir) MUST
22// return negative AND leave the real victim unchanged
23// (the primitive reports failure, never half-commits).
24//
25// pass = commit_ok AND crash_safe AND after_commit AND neg_torn AND tamper_bites
26//
27// Evidence -> knowledge/status/atomic_rewrite.log (ATOMICRWGATE row).
28// SOVEREIGN: nx_atomic_rewrite (-> nx_syscalls) only. license_tier: ORIGINAL
29import "nx_atomic_rewrite.nx"
30
31const VICTIM: *u8 = "/tmp/_arw_victim"
32const LOGP: *u8 = "knowledge/status/atomic_rewrite.log"
33
34// V1 is LONGER than V2 so a truncating tear is byte-detectable.
35const V1: *u8 = "QUEUE-V1-INTACT-row1-row2-row3-row4-row5-row6-PADDED-TO-BE-MULTI-WRITE-SIZED-XXXXXXXX"
36const V2: *u8 = "QUEUE-V2-COMMITTED"
37
38func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
39func g_fp(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 }
40func g_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;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{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 }
41
42// read whole file into buf (cap-bounded); returns byte count (0 if absent).
43func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
44 let fd: i64 = sys_openat_rd(path)
45 if fd < 0 { return 0 }
46 var n: i64 = 0
47 var go: i64 = 1
48 while go == 1 {
49 let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - n)
50 if r <= 0 { go = 0 } else { n = n + r }
51 if n >= cap { go = 0 }
52 }
53 sys_close(fd)
54 return n
55}
56
57// exact byte equality of a buffer[0,n) vs a null-terminated string.
58func g_eq(buf: *u8, n: i64, s: *u8) -> i64 {
59 let sl: i64 = ar_len(s)
60 if n != sl { return 0 }
61 var i: i64 = 0
62 while i < n { if buf[i] != s[i] { return 0 } i = i + 1 }
63 return 1
64}
65
66// substring search (buf[0,n) contains pat[0,pl)).
67func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 {
68 if pl <= 0 { return 0 }
69 var i: i64 = 0
70 while i + pl <= n {
71 var k: i64 = 0; var hit: i64 = 1
72 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } }
73 if hit == 1 { return 1 }
74 i = i + 1
75 }
76 return 0
77}
78
79func main() -> i64 {
80 g_p("=== WMS-R3 atomic_rewrite gate (generic tmp+fsync+rename+dir-sync; crash-before-commit safety + WORKING neg-control) ===\n" as *u8)
81 let lfd: i64 = sys_openat_append(LOGP, 0x1a4)
82
83 let v1l: i64 = ar_len(V1)
84 let v2l: i64 = ar_len(V2)
85 let rb: *u8 = sys_mmap(4096)
86 let st: *i64 = sys_mmap(16) as *i64
87
88 // ---- (1) commit_ok: clean whole-file replace v1 -> v2 ----
89 atomic_rewrite(VICTIM, V1, v1l)
90 var rn: i64 = g_read(VICTIM, rb, 4096)
91 let saw_v1: i64 = g_eq(rb, rn, V1)
92 atomic_rewrite(VICTIM, V2, v2l)
93 rn = g_read(VICTIM, rb, 4096)
94 var commit_ok: i64 = 0
95 if g_eq(rb, rn, V2) == 1 { if g_has(rb, rn, "QUEUE-V1" as *u8, 8) == 0 { commit_ok = 1 } }
96
97 // ---- (2) crash_safe: stage temp + fsync in a child, NO rename, child dies ----
98 // Re-establish intact v1 on disk first.
99 atomic_rewrite(VICTIM, V1, v1l)
100 let pid1: i64 = sys_fork()
101 if pid1 == 0 {
102 // child: stage v2 to the temp, fsync, then DIE before the rename.
103 ar_crashwrite(VICTIM, V2, v2l)
104 sys_exit(0)
105 }
106 sys_wait4(pid1, st, 0)
107 // FRESH reader of the live path: must STILL see exactly v1 (untouched).
108 rn = g_read(VICTIM, rb, 4096)
109 var crash_safe: i64 = 0
110 if g_eq(rb, rn, V1) == 1 { crash_safe = 1 }
111 // after the simulated crash, a real commit to v2 must now take effect.
112 atomic_rewrite(VICTIM, V2, v2l)
113 rn = g_read(VICTIM, rb, 4096)
114 var after_commit: i64 = 0
115 if g_eq(rb, rn, V2) == 1 { after_commit = 1 }
116
117 // ---- (3) NEGATIVE CONTROL: old in-place rewrite, crash mid-write -> TORN ----
118 // Establish full v1 via the SAFE primitive, then a child runs the UNSAFE
119 // in-place path with only HALF of v2's bytes and dies = crash mid-write.
120 atomic_rewrite(VICTIM, V1, v1l)
121 let half: i64 = v2l / 2
122 let pid2: i64 = sys_fork()
123 if pid2 == 0 {
124 ar_unsafe_inplace(VICTIM, V2, half) // O_TRUNC live file, write half, die
125 sys_exit(0)
126 }
127 sys_wait4(pid2, st, 0)
128 rn = g_read(VICTIM, rb, 4096)
129 // TORN iff the live file is NEITHER intact-v1 NOR full-v2: a corrupt prefix.
130 var neg_torn: i64 = 0
131 if g_eq(rb, rn, V1) == 0 { if g_eq(rb, rn, V2) == 0 { neg_torn = 1 } }
132 let neg_len: i64 = rn
133
134 // ---- (4) tamper: rewrite to an unwritable path -> negative rc, victim intact ----
135 // Restore a known-good v2 first so we can prove the victim stays unchanged.
136 atomic_rewrite(VICTIM, V2, v2l)
137 let badrc: i64 = atomic_rewrite("/proc/nonexist_dir_xyz/cannot" as *u8, V1, v1l)
138 rn = g_read(VICTIM, rb, 4096)
139 var tamper_bites: i64 = 0
140 if badrc < 0 { if g_eq(rb, rn, V2) == 1 { tamper_bites = 1 } }
141
142 g_p(" saw_v1_first=" as *u8); g_fn(1, saw_v1)
143 g_p(" commit_ok=" as *u8); g_fn(1, commit_ok)
144 g_p(" crash_safe=" as *u8); g_fn(1, crash_safe)
145 g_p(" after_commit=" as *u8); g_fn(1, after_commit)
146 g_p(" neg_torn=" as *u8); g_fn(1, neg_torn); g_p("(torn_len=" as *u8); g_fn(1, neg_len); g_p("/v1_len=" as *u8); g_fn(1, v1l); g_p(")" as *u8)
147 g_p(" tamper_bites=" as *u8); g_fn(1, tamper_bites); g_p("(badrc=" as *u8); if badrc < 0 { g_p("-" as *u8) } g_fn(1, badrc); g_p(")\n" as *u8)
148
149 var pass: i64 = 0
150 if commit_ok == 1 { if crash_safe == 1 { if after_commit == 1 { if neg_torn == 1 { if tamper_bites == 1 { pass = 1 } } } } }
151
152 if pass == 1 {
153 g_p("ATOMICRWGATE verdict=GREEN (generic atomic_rewrite: crash BEFORE rename leaves intact v1; after rename reader sees v2; the OLD in-place rewrite under the SAME crash point TORE the file [torn_len=" as *u8); g_fn(1, neg_len); g_p("!=v1_len=" as *u8); g_fn(1, v1l); g_p("] -> atomicity proven necessary; tamper rejected)\n" as *u8)
154 if lfd >= 0 {
155 g_fp(lfd, "ATOMICRWGATE verdict=GREEN commit_ok=1 crash_safe=1(reader-sees-intact-v1-after-stage-crash) after_commit=1 neg_torn=1(unsafe-inplace-crash-leaves-TORN-file torn_len=" as *u8); g_fn(lfd, neg_len)
156 g_fp(lfd, " v1_len=" as *u8); g_fn(lfd, v1l)
157 g_fp(lfd, ") tamper_bites=1(badrc=" as *u8); if badrc < 0 { g_fp(lfd, "-" as *u8) } g_fn(lfd, badrc)
158 g_fp(lfd, ") keystone=atomic-rewrite probe=wms-r3 epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8)
159 sys_close(lfd)
160 }
161 sys_exit(0); return 0
162 }
163
164 g_p("ATOMICRWGATE verdict=RED (not all sub-flags green)\n" as *u8)
165 if lfd >= 0 {
166 g_fp(lfd, "ATOMICRWGATE verdict=RED commit_ok=" as *u8); g_fn(lfd, commit_ok)
167 g_fp(lfd, " crash_safe=" as *u8); g_fn(lfd, crash_safe)
168 g_fp(lfd, " after_commit=" as *u8); g_fn(lfd, after_commit)
169 g_fp(lfd, " neg_torn=" as *u8); g_fn(lfd, neg_torn)
170 g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites)
171 g_fp(lfd, " badrc=" as *u8); g_fn(lfd, badrc); g_fp(lfd, " epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8)
172 sys_close(lfd)
173 }
174 sys_exit(1)
175 return 1
176}