code wiki / _hdl_build / nx_coedit_gate.nx
nx_coedit_gate.nx source
↩ module page · 193 lines · 11382 B
1// nx_coedit_gate.nx -- gate for the CO-EDITING KERNEL (RGA text CRDT). The rows ARE the CRDT laws:
2// 1 type+apply a session of position-based edits materializes exactly
3// 2 CONVERGENCE merge(A,B) and merge(B,A) apply to the SAME bytes (pinned): concurrent append after
4// the same char ordered by the (counter,replica) tie-break; a concurrent delete lands
5// 3 tombstone-anchor inserting AFTER a concurrently-DELETED char still places correctly (RGA property)
6// 4 idempotent-remerge merge(AB, A) == AB (byte-equal log; re-applying ops is a no-op)
7// 5 edit-del position-based delete produces the pinned text
8// 6 conflict-loud same op id with DIFFERENT content = LOUD protocol violation (never silent)
9// 7 badref-loud insert after an unknown id = LOUD
10// license_tier: ORIGINAL
11import "nx_syscalls.nx"
12
13func eg_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8) { n=n+1 } return n }
14func eg_p(s: *u8) -> i64 { sys_write(1, s, eg_slen(s)); return 0 }
15func eg_cat(dst: *u8, off: i64, s: *u8) -> i64 { var i: i64=0; while s[i]!=(0 as u8) { dst[off+i]=s[i]; i=i+1 } return off+i }
16func eg_catn(dst: *u8, off: i64, v: i64) -> i64 {
17 var o: i64=off; var m: i64=v; if m<0 { dst[o]=45 as u8; o=o+1; m=0-m }
18 let t: *u8=sys_mmap(28); var k: i64=0; if m==0 { t[0]=48 as u8; k=1 }
19 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 }
20 var i: i64=0; while i<k { dst[o+i]=t[k-1-i]; i=i+1 } return o+k
21}
22func eg_write(path: *u8, content: *u8) -> i64 {
23 let fd: i64=sys_openat_wr(path, 0x1a4); if fd<0 { return 0-1 }
24 sys_write(fd, content, eg_slen(content)); sys_close(fd); return 0
25}
26func eg_readall(path: *u8, szout: *i64) -> *u8 {
27 let fd: i64=sys_openat_rd(path); if fd<0 { szout[0]=0-1; return 0 as *u8 }
28 let buf: *u8=sys_mmap(1048576); var got: i64=0; var n: i64=1
29 while n>0 { n=sys_read(fd,(buf as i64+got) as *u8,65536); if n>0 { got=got+n } }
30 sys_close(fd); szout[0]=got; return buf
31}
32func eg_runv(elf: *u8, args: *i64, outpath: *u8) -> i64 {
33 let pid: i64=sys_fork()
34 if pid==0 {
35 if (outpath as i64)!=0 { let ofd: i64=sys_openat_wr(outpath,0x1a4); if ofd>=0 { sys_dup3(ofd,1,0); sys_dup3(ofd,2,0) } }
36 let argv: *i64=sys_mmap(128) as *i64
37 argv[0]=elf as i64; var i: i64=0; var go: i64=1
38 while go==1 { if args[i]==0 { go=0 } else { argv[i+1]=args[i]; i=i+1 } }
39 argv[i+1]=0
40 let envp: *i64=sys_mmap(16) as *i64; envp[0]=0
41 sys_execve(elf, argv, envp); sys_exit(127)
42 }
43 let st: *i64=sys_mmap(16) as *i64; sys_wait4(pid, st, 0)
44 let sig: i64=st[0]&0x7f; if sig!=0 { return 128+sig }
45 return (st[0]>>8)&0xff
46}
47func eg_has(path: *u8, needle: *u8) -> i64 {
48 let szp: *i64=sys_mmap(16) as *i64; let b: *u8=eg_readall(path, szp); let sz: i64=szp[0]
49 let n: i64=eg_slen(needle); if sz<n { return 0 }
50 var i: i64=0
51 while i+n<=sz { var ok: i64=1; var j: i64=0; while j<n { if b[i+j]!=needle[j] { ok=0; j=n } else { j=j+1 } } if ok==1 { return 1 } i=i+1 }
52 return 0
53}
54func eg_fileis(path: *u8, exact: *u8) -> i64 {
55 let szp: *i64=sys_mmap(16) as *i64; let b: *u8=eg_readall(path, szp)
56 let n: i64=eg_slen(exact)
57 if szp[0] != n { return 0 }
58 var i: i64=0
59 while i<n { if b[i]!=exact[i] { return 0 } i=i+1 }
60 return 1
61}
62func eg_fileeq(p1: *u8, p2: *u8) -> i64 {
63 let s1: *i64=sys_mmap(16) as *i64
64 let s2: *i64=sys_mmap(16) as *i64
65 let b1: *u8=eg_readall(p1, s1)
66 let b2: *u8=eg_readall(p2, s2)
67 if s1[0] != s2[0] { return 0 }
68 if s1[0]<0 { return 0 }
69 var i: i64=0
70 while i<s1[0] { if b1[i] != b2[i] { return 0 } i=i+1 }
71 return 1
72}
73func eg_args6(a1: *u8, a2: *u8, a3: *u8, a4: *u8, a5: *u8, a6: *u8) -> *i64 {
74 let a: *i64=sys_mmap(64) as *i64
75 a[0]=a1 as i64; a[1]=a2 as i64; a[2]=a3 as i64; a[3]=a4 as i64; a[4]=a5 as i64; a[5]=a6 as i64; a[6]=0
76 return a
77}
78func eg_row(name: *u8, pass: i64) -> i64 {
79 eg_p("ROW " as *u8); eg_p(name); if pass==1 { eg_p(" PASS\n" as *u8) } else { eg_p(" FAIL\n" as *u8) } return pass
80}
81// create/truncate to an EMPTY file. NEVER pass a "" literal (constant-pool ALIASING would write garbage).
82func eg_mkempty(path: *u8) -> i64 {
83 let fd: i64=sys_openat_wr(path, 0x1a4); if fd<0 { return 0-1 }
84 sys_close(fd)
85 return 0
86}
87func eg_cp(src: *u8, dst: *u8) -> i64 {
88 let szp: *i64=sys_mmap(16) as *i64
89 let b: *u8=eg_readall(src, szp)
90 if szp[0]<0 { return 0-1 }
91 let fd: i64=sys_openat_wr(dst, 0x1a4); if fd<0 { return 0-1 }
92 sys_write(fd, b, szp[0]); sys_close(fd); return 0
93}
94
95func main(argc: i64, argv: *i64) -> i64 {
96 eg_p("=== COEDIT GATE: RGA text CRDT -- convergence, tie-break, tombstone anchors, idempotent re-merge, LOUD conflicts ===\n" as *u8)
97 let ce: *u8="/tmp/nx_coedit.sov.elf" as *u8
98 let pr: i64=sys_openat_rd(ce)
99 if pr>=0 { sys_close(pr) } else {
100 eg_p(" instrument missing -> rebuilding\n" as *u8)
101 eg_runv("_offc/nx_sov_build_run.elf" as *u8, eg_args6("nx_coedit" as *u8, "--build-only" as *u8, 0 as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_rebuild.out" as *u8)
102 }
103
104 var pass: i64=0
105 var r: i64=0
106
107 // row 1: replica 1 types "Hi!" into a fresh log; apply materializes it exactly
108 eg_mkempty("/tmp/eg_l1" as *u8)
109 eg_runv(ce, eg_args6("edit" as *u8, "/tmp/eg_l1" as *u8, "1" as *u8, "0" as *u8, "ins" as *u8, "Hi!" as *u8), "/tmp/eg_r1a.txt" as *u8)
110 let rc1: i64=eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_l1" as *u8, "/tmp/eg_t1.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r1b.txt" as *u8)
111 r=0
112 if rc1==0 { if eg_fileis("/tmp/eg_t1.txt" as *u8, "Hi!" as *u8)==1 { r=1 } }
113 pass=pass+eg_row("type-apply" as *u8, r)
114
115 // shared base for rows 2-4: replica 1 types "abc" (ids 1:1 a, 1:2 b, 1:3 c)
116 eg_write("/tmp/eg_base" as *u8, "I 1 1 R a\nI 1 2 1:1 b\nI 1 3 1:2 c\n" as *u8)
117
118 // row 2: CONVERGENCE + tie-break. A(rep1) appends d after c (1:4); B(rep2) appends e after c (2:4) and
119 // deletes b (2:5 -> 1:2). RGA: children of c desc by (ctr,rep) -> 2:4 before 1:4 => "a c e d" minus b = "aced".
120 eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_A" as *u8)
121 eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_B" as *u8)
122 eg_runv(ce, eg_args6("ins" as *u8, "/tmp/eg_A" as *u8, "1" as *u8, "4" as *u8, "1:3" as *u8, "d" as *u8), "/tmp/eg_x.txt" as *u8)
123 eg_runv(ce, eg_args6("ins" as *u8, "/tmp/eg_B" as *u8, "2" as *u8, "4" as *u8, "1:3" as *u8, "e" as *u8), "/tmp/eg_x.txt" as *u8)
124 eg_runv(ce, eg_args6("del" as *u8, "/tmp/eg_B" as *u8, "2" as *u8, "5" as *u8, "1:2" as *u8, 0 as *u8), "/tmp/eg_x.txt" as *u8)
125 eg_runv(ce, eg_args6("merge" as *u8, "/tmp/eg_A" as *u8, "/tmp/eg_B" as *u8, "/tmp/eg_AB" as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r2a.txt" as *u8)
126 eg_runv(ce, eg_args6("merge" as *u8, "/tmp/eg_B" as *u8, "/tmp/eg_A" as *u8, "/tmp/eg_BA" as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r2b.txt" as *u8)
127 eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_AB" as *u8, "/tmp/eg_tAB.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r2c.txt" as *u8)
128 eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_BA" as *u8, "/tmp/eg_tBA.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r2d.txt" as *u8)
129 r=0
130 if eg_fileis("/tmp/eg_tAB.txt" as *u8, "aced" as *u8)==1 { if eg_fileeq("/tmp/eg_tAB.txt" as *u8, "/tmp/eg_tBA.txt" as *u8)==1 { r=1 } }
131 pass=pass+eg_row("convergence-tiebreak" as *u8, r)
132
133 // row 3: tombstone anchor -- A deletes c (1:4 -> 1:3); B inserts f AFTER c (2:4 -> after 1:3).
134 // Both orders: c is gone but still anchors f => "abf".
135 eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_C" as *u8)
136 eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_D" as *u8)
137 eg_runv(ce, eg_args6("del" as *u8, "/tmp/eg_C" as *u8, "1" as *u8, "4" as *u8, "1:3" as *u8, 0 as *u8), "/tmp/eg_x.txt" as *u8)
138 eg_runv(ce, eg_args6("ins" as *u8, "/tmp/eg_D" as *u8, "2" as *u8, "4" as *u8, "1:3" as *u8, "f" as *u8), "/tmp/eg_x.txt" as *u8)
139 eg_runv(ce, eg_args6("merge" as *u8, "/tmp/eg_C" as *u8, "/tmp/eg_D" as *u8, "/tmp/eg_CD" as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r3a.txt" as *u8)
140 eg_runv(ce, eg_args6("merge" as *u8, "/tmp/eg_D" as *u8, "/tmp/eg_C" as *u8, "/tmp/eg_DC" as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r3b.txt" as *u8)
141 eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_CD" as *u8, "/tmp/eg_tCD.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r3c.txt" as *u8)
142 eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_DC" as *u8, "/tmp/eg_tDC.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r3d.txt" as *u8)
143 r=0
144 if eg_fileis("/tmp/eg_tCD.txt" as *u8, "abf" as *u8)==1 { if eg_fileeq("/tmp/eg_tCD.txt" as *u8, "/tmp/eg_tDC.txt" as *u8)==1 { r=1 } }
145 pass=pass+eg_row("tombstone-anchor" as *u8, r)
146
147 // row 4: idempotent re-merge -- merge(AB, A) == AB byte-equal
148 eg_runv(ce, eg_args6("merge" as *u8, "/tmp/eg_AB" as *u8, "/tmp/eg_A" as *u8, "/tmp/eg_ABA" as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r4.txt" as *u8)
149 r=eg_fileeq("/tmp/eg_AB" as *u8, "/tmp/eg_ABA" as *u8)
150 pass=pass+eg_row("idempotent-remerge" as *u8, r)
151
152 // row 5: position-based delete -- type "abcd" fresh, delete pos1 count2 -> "ad"
153 eg_mkempty("/tmp/eg_l5" as *u8)
154 eg_runv(ce, eg_args6("edit" as *u8, "/tmp/eg_l5" as *u8, "1" as *u8, "0" as *u8, "ins" as *u8, "abcd" as *u8), "/tmp/eg_r5a.txt" as *u8)
155 eg_runv(ce, eg_args6("edit" as *u8, "/tmp/eg_l5" as *u8, "1" as *u8, "1" as *u8, "del" as *u8, "2" as *u8), "/tmp/eg_r5b.txt" as *u8)
156 let rc5: i64=eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_l5" as *u8, "/tmp/eg_t5.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r5c.txt" as *u8)
157 r=0
158 if rc5==0 { if eg_fileis("/tmp/eg_t5.txt" as *u8, "ad" as *u8)==1 { r=1 } }
159 pass=pass+eg_row("edit-del" as *u8, r)
160
161 // row 6 (neg): SAME id, DIFFERENT content = LOUD conflict
162 eg_write("/tmp/eg_l6" as *u8, "I 1 1 R x\nI 1 1 R y\n" as *u8)
163 let rc6: i64=eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_l6" as *u8, "/tmp/eg_t6.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r6.txt" as *u8)
164 r=0
165 if rc6==1 { if eg_has("/tmp/eg_r6.txt" as *u8, "err=3" as *u8)==1 { r=1 } }
166 pass=pass+eg_row("conflict-loud" as *u8, r)
167
168 // row 7 (neg): insert after an unknown id = LOUD bad-ref
169 eg_write("/tmp/eg_l7" as *u8, "I 1 1 R x\nI 1 2 9:9 y\n" as *u8)
170 let rc7: i64=eg_runv(ce, eg_args6("apply" as *u8, "/tmp/eg_l7" as *u8, "/tmp/eg_t7.txt" as *u8, 0 as *u8, 0 as *u8, 0 as *u8), "/tmp/eg_r7.txt" as *u8)
171 r=0
172 if rc7==1 { if eg_has("/tmp/eg_r7.txt" as *u8, "err=2" as *u8)==1 { r=1 } }
173 pass=pass+eg_row("badref-loud" as *u8, r)
174
175 let permil: i64=(pass*1000)/7
176 let logfd: i64=sys_openat_append("knowledge/status/vizsla_gate.log" as *u8, 0x1a4)
177 var fdi: i64=0
178 while fdi<2 {
179 var fd: i64=1; if fdi==1 { fd=logfd }
180 if fd>0 {
181 let line: *u8=sys_mmap(256); var o: i64=0
182 o=eg_cat(line,o,"COEDIT-GATE epoch=" as *u8); o=eg_catn(line,o,sys_now_realtime_sec())
183 o=eg_cat(line,o," rows=7 pass=" as *u8); o=eg_catn(line,o,pass)
184 o=eg_cat(line,o," permil=" as *u8); o=eg_catn(line,o,permil)
185 if pass==7 { o=eg_cat(line,o," verdict=GREEN\n" as *u8) } else { o=eg_cat(line,o," verdict=RED\n" as *u8) }
186 sys_write(fd, line, o)
187 }
188 fdi=fdi+1
189 }
190 if logfd>0 { sys_close(logfd) }
191 if pass==7 { return 0 }
192 return 1
193}