code wiki / _hdl_build / nx_coedit_gate.nx
`nx_coedit_gate.nx` source

↩ module page · 201 lines · 11928 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"
12import "nx_gate_verdict.nx"
13
14func eg_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8) { n=n+1 } return n }
15func eg_p(s: *u8) -> i64 { sys_write(1, s, eg_slen(s)); return 0 }
16func 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 }
17func eg_catn(dst: *u8, off: i64, v: i64) -> i64 {
  var o: i64=off; var m: i64=v; if m<0 { dst[o]=45 as u8; o=o+1; m=0-m }
  let t: *u8=sys_mmap(28); 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[o+i]=t[k-1-i]; i=i+1 } return o+k
22}
23func eg_write(path: *u8, content: *u8) -> i64 {
  let fd: i64=sys_openat_wr(path, 0x1a4); if fd<0 { return 0-1 }
  sys_write(fd, content, eg_slen(content)); sys_close(fd); return 0
26}
27func eg_readall(path: *u8, szout: *i64) -> *u8 {
  let fd: i64=sys_openat_rd(path); if fd<0 { szout[0]=0-1; return 0 as *u8 }
  let buf: *u8=sys_mmap(1048576); var got: i64=0; var n: i64=1
  while n>0 { n=sys_read(fd,(buf as i64+got) as *u8,65536); if n>0 { got=got+n } }
  sys_close(fd); szout[0]=got; return buf
32}
33func eg_runv(elf: *u8, args: *i64, outpath: *u8) -> i64 {
  let pid: i64=sys_fork()
  if pid==0 {
      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) } }
      let argv: *i64=sys_mmap(128) as *i64
      argv[0]=elf as i64; var i: i64=0; var go: i64=1
      while go==1 { if args[i]==0 { go=0 } else { argv[i+1]=args[i]; i=i+1 } }
      argv[i+1]=0
      let envp: *i64=sys_mmap(16) as *i64; envp[0]=0
      sys_execve(elf, argv, envp); sys_exit(127)
  }
  let st: *i64=sys_mmap(16) as *i64; sys_wait4(pid, st, 0)
  let sig: i64=st[0]&0x7f; if sig!=0 { return 128+sig }
  return (st[0]>>8)&0xff
47}
48func eg_has(path: *u8, needle: *u8) -> i64 {
  let szp: *i64=sys_mmap(16) as *i64; let b: *u8=eg_readall(path, szp); let sz: i64=szp[0]
  let n: i64=eg_slen(needle); if sz<n { return 0 }
  var i: i64=0
  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 }
  return 0
54}
55func eg_fileis(path: *u8, exact: *u8) -> i64 {
  let szp: *i64=sys_mmap(16) as *i64; let b: *u8=eg_readall(path, szp)
  let n: i64=eg_slen(exact)
  if szp[0] != n { return 0 }
  var i: i64=0
  while i<n { if b[i]!=exact[i] { return 0 } i=i+1 }
  return 1
62}
63func eg_fileeq(p1: *u8, p2: *u8) -> i64 {
  let s1: *i64=sys_mmap(16) as *i64
  let s2: *i64=sys_mmap(16) as *i64
  let b1: *u8=eg_readall(p1, s1)
  let b2: *u8=eg_readall(p2, s2)
  if s1[0] != s2[0] { return 0 }
  if s1[0]<0 { return 0 }
  var i: i64=0
  while i<s1[0] { if b1[i] != b2[i] { return 0 } i=i+1 }
  return 1
73}
74func eg_args6(a1: *u8, a2: *u8, a3: *u8, a4: *u8, a5: *u8, a6: *u8) -> *i64 {
  let a: *i64=sys_mmap(64) as *i64
  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
  return a
78}
79func eg_row(name: *u8, pass: i64) -> i64 {
  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
81}
82// create/truncate to an EMPTY file. NEVER pass a "" literal (constant-pool ALIASING would write garbage).
83func eg_mkempty(path: *u8) -> i64 {
  let fd: i64=sys_openat_wr(path, 0x1a4); if fd<0 { return 0-1 }
  sys_close(fd)
  return 0
87}
88func eg_cp(src: *u8, dst: *u8) -> i64 {
  let szp: *i64=sys_mmap(16) as *i64
  let b: *u8=eg_readall(src, szp)
  if szp[0]<0 { return 0-1 }
  let fd: i64=sys_openat_wr(dst, 0x1a4); if fd<0 { return 0-1 }
  sys_write(fd, b, szp[0]); sys_close(fd); return 0
94}
95
96func main(argc: i64, argv: *i64) -> i64 {
  eg_p("=== COEDIT GATE: RGA text CRDT -- convergence, tie-break, tombstone anchors, idempotent re-merge, LOUD conflicts ===\n" as *u8)
  let ce: *u8="buildroot/_build/nx_coedit.sov.elf" as *u8
  let pr: i64=sys_openat_rd(ce)
  if pr>=0 { sys_close(pr) } else {
      eg_p(" instrument missing -> rebuilding\n" as *u8)
      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)
  }
104
  var pass: i64=0
  var r: i64=0
107
  // row 1: replica 1 types "Hi!" into a fresh log; apply materializes it exactly
  eg_mkempty("/tmp/eg_l1" as *u8)
  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)
  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)
  r=0
  if rc1==0 { if eg_fileis("/tmp/eg_t1.txt" as *u8, "Hi!" as *u8)==1 { r=1 } }
  pass=pass+eg_row("type-apply" as *u8, r)
115
  // shared base for rows 2-4: replica 1 types "abc" (ids 1:1 a, 1:2 b, 1:3 c)
  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)
118
  // row 2: CONVERGENCE + tie-break. A(rep1) appends d after c (1:4); B(rep2) appends e after c (2:4) and
  // 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".
  eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_A" as *u8)
  eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_B" as *u8)
  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)
  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)
  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)
  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)
  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)
  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)
  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)
  r=0
  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 } }
  pass=pass+eg_row("convergence-tiebreak" as *u8, r)
133
  // row 3: tombstone anchor -- A deletes c (1:4 -> 1:3); B inserts f AFTER c (2:4 -> after 1:3).
  // Both orders: c is gone but still anchors f => "abf".
  eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_C" as *u8)
  eg_cp("/tmp/eg_base" as *u8, "/tmp/eg_D" as *u8)
  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)
  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)
  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)
  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)
  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)
  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)
  r=0
  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 } }
  pass=pass+eg_row("tombstone-anchor" as *u8, r)
147
  // row 4: idempotent re-merge -- merge(AB, A) == AB byte-equal
  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)
  r=eg_fileeq("/tmp/eg_AB" as *u8, "/tmp/eg_ABA" as *u8)
  pass=pass+eg_row("idempotent-remerge" as *u8, r)
152
  // row 5: position-based delete -- type "abcd" fresh, delete pos1 count2 -> "ad"
  eg_mkempty("/tmp/eg_l5" as *u8)
  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)
  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)
  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)
  r=0
  if rc5==0 { if eg_fileis("/tmp/eg_t5.txt" as *u8, "ad" as *u8)==1 { r=1 } }
  pass=pass+eg_row("edit-del" as *u8, r)
161
  // row 6 (neg): SAME id, DIFFERENT content = LOUD conflict
  eg_write("/tmp/eg_l6" as *u8, "I 1 1 R x\nI 1 1 R y\n" as *u8)
  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)
  r=0
  if rc6==1 { if eg_has("/tmp/eg_r6.txt" as *u8, "err=3" as *u8)==1 { r=1 } }
  pass=pass+eg_row("conflict-loud" as *u8, r)
168
  // row 7 (neg): insert after an unknown id = LOUD bad-ref
  eg_write("/tmp/eg_l7" as *u8, "I 1 1 R x\nI 1 2 9:9 y\n" as *u8)
  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)
  r=0
  if rc7==1 { if eg_has("/tmp/eg_r7.txt" as *u8, "err=2" as *u8)==1 { r=1 } }
  pass=pass+eg_row("badref-loud" as *u8, r)
175
  let permil: i64=(pass*1000)/7
  let logfd: i64=sys_openat_append("knowledge/status/vizsla_gate.log" as *u8, 0x1a4)
  var fdi: i64=0
  while fdi<2 {
      var fd: i64=1; if fdi==1 { fd=logfd }
      if fd>0 {
          let line: *u8=sys_mmap(256); var o: i64=0
          o=eg_cat(line,o,"COEDIT-GATE epoch=" as *u8); o=eg_catn(line,o,sys_now_realtime_sec())
          o=eg_cat(line,o," rows=7 pass=" as *u8); o=eg_catn(line,o,pass)
          o=eg_cat(line,o," permil=" as *u8); o=eg_catn(line,o,permil)
          if pass==7 { o=eg_cat(line,o," verdict=GREEN\n" as *u8) } else { o=eg_cat(line,o," verdict=RED\n" as *u8) }
          sys_write(fd, line, o)
      }
      fdi=fdi+1
  }
  if logfd>0 { sys_close(logfd) }
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = pass
  ctr__dry[1] = 7
  let rc__dry: i64 = gv_verdict("COEDIT-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
201}
nx_coedit_gate.nx source

`nx_coedit_gate.nx` source
