code wiki / (root) / nx_framed_append_gate.nx
`nx_framed_append_gate.nx` source

↩ module page · 293 lines · 12238 B
1// nx_framed_append_gate.nx -- the REFEREE for WMS-R0 (atomic framed-append).
2//
3// Proves the nx_framed_append primitive defeats concurrent-appender tearing, AND
4// proves the test can actually DETECT tearing (the mandatory negative control).
5//
6//   GOOD lane: N workers fork concurrently, each emits NRECS records via the NEW
7//              single-write primitive fa_append(GOODPATH, ...).  Expect ZERO torn
8//              lines and ALL N*NRECS lines present (nothing lost, nothing torn).
9//   BAD  lane (NEGATIVE CONTROL): the SAME concurrency, but each record is emitted
10//              the OLD way -- a SEQUENCE of separate sys_write() calls per record.
11//              O_APPEND only makes ONE write atomic, not the sequence, so workers
12//              interleave -> torn lines MUST appear.  bad_torn == 0 => the detector
13//              is worthless => RED (no false green).
14//   TAMPER:    an oversized record (rec_len+1 > cap) must be REJECTED with -2,
15//              never silently written/torn.
16//
17// A line is WELL-FORMED iff it starts "FA w=" AND the bytes just before its '\n'
18// are "END" AND it contains exactly one " END" token.  Any interleaving violates
19// one of those -> counted as torn.  Output: rows -> stdout + the evidence log
20// knowledge/status/framed_append_gate.log, then a final verdict line.  Exit 0 on
21// GREEN, 1 on RED.  Sovereign: only nx_syscalls + nx_framed_append.
22// license_tier: ORIGINAL
23import "nx_syscalls.nx"
24import "nx_framed_append.nx"
25
26const NWORKERS: i64 = 16          // concurrency (raised so the neg-control tears robustly)
27const NRECS:    i64 = 300         // records per worker
28const RECCAP:   i64 = 256         // bounded record size for the primitive
29
30// dual-sink writer: stdout (fd 1) AND the evidence log fd
31func gp(logfd: i64, s: *u8) -> i64 {
  var n: i64 = 0
  while s[n] != (0 as u8) { n = n + 1 }
  sys_write(1, s, n)
  if logfd > 0 { sys_write(logfd, s, n) }
  return 0
37}
38func gn(logfd: i64, v: i64) -> i64 {
  let bb: *u8 = sys_mmap(28)
  var m: i64 = v
  if m < 0 { sys_write(1, "-\x00" as *u8, 1); if logfd > 0 { sys_write(logfd, "-\x00" as *u8, 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 { bb[i] = t[k - 1 - i]; i = i + 1 }
  sys_write(1, bb, k)
  if logfd > 0 { sys_write(logfd, bb, k) }
  return 0
51}
52
53// assemble one record into buf (NO trailing newline): "FA w=<wid> i=<seq> pid=<pid> END"
54// returns rec_len.  The trailing " END" sentinel is what the parser checks for.
55func build_rec(buf: *u8, wid: i64, seq: i64, pid: i64) -> i64 {
  var o: i64 = 0
  o = fa_cat(buf, o, "FA w=\x00" as *u8)
  o = fa_catn(buf, o, wid)
  o = fa_cat(buf, o, " i=\x00" as *u8)
  o = fa_catn(buf, o, seq)
  o = fa_cat(buf, o, " pid=\x00" as *u8)
  o = fa_catn(buf, o, pid)
  o = fa_cat(buf, o, " END\x00" as *u8)
  return o
65}
66
67// GOOD worker: NRECS framed single-write appends, then exit.
68func good_worker(wid: i64) -> i64 {
  let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0)   // getpid
  let buf: *u8 = sys_mmap(RECCAP + 16)
  var i: i64 = 0
  while i < NRECS {
      let rl: i64 = build_rec(buf, wid, i, pid)
      fa_append("/tmp/fa_good.log\x00" as *u8, buf, rl, RECCAP)
      i = i + 1
  }
  return 0
78}
79
80// BAD worker (NEGATIVE CONTROL): same records, but emitted as a SEQUENCE of
81// separate sys_write() calls per record -- exactly the torn-line bug.  Opens the
82// file ONCE in O_APPEND, then per record: many little writes + a final newline.
83// Concurrent workers interleave between these writes -> torn lines.
84func bad_worker(wid: i64) -> i64 {
  let pid: i64 = __syscall(39, 0, 0, 0, 0, 0, 0)   // getpid
  let fd: i64 = sys_openat_append("/tmp/fa_bad.log\x00" as *u8, 0x1a4)
  if fd < 0 { return 0 - 1 }
  let nb: *u8 = sys_mmap(28)
  var i: i64 = 0
  while i < NRECS {
      sys_write(fd, "FA w=\x00" as *u8, 5)
      var l: i64 = 0; var m: i64 = wid
      if m == 0 { nb[0] = 48 as u8; l = 1 }
      while m > 0 { nb[l] = (48 + (m % 10)) as u8; m = m / 10; l = l + 1 }
      var x: i64 = 0
      let d1: *u8 = sys_mmap(28)
      while x < l { d1[x] = nb[l - 1 - x]; x = x + 1 }
      sys_write(fd, d1, l)
      sys_write(fd, " i=\x00" as *u8, 3)
      l = 0; m = i
      if m == 0 { nb[0] = 48 as u8; l = 1 }
      while m > 0 { nb[l] = (48 + (m % 10)) as u8; m = m / 10; l = l + 1 }
      let d2: *u8 = sys_mmap(28); x = 0
      while x < l { d2[x] = nb[l - 1 - x]; x = x + 1 }
      sys_write(fd, d2, l)
      sys_write(fd, " pid=\x00" as *u8, 6)
      l = 0; m = pid
      if m == 0 { nb[0] = 48 as u8; l = 1 }
      while m > 0 { nb[l] = (48 + (m % 10)) as u8; m = m / 10; l = l + 1 }
      let d3: *u8 = sys_mmap(28); x = 0
      while x < l { d3[x] = nb[l - 1 - x]; x = x + 1 }
      sys_write(fd, d3, l)
      sys_write(fd, " END\x00" as *u8, 4)
      sys_write(fd, "\n\x00" as *u8, 1)
      i = i + 1
  }
  sys_close(fd)
  return 0
119}
120
121// spawn NWORKERS children running f(wid), wait all.  which: 0=good, 1=bad.
122func spawn_all(which: i64) -> i64 {
  let pids: *i64 = sys_mmap(8 * (NWORKERS + 4)) as *i64
  var w: i64 = 0
  while w < NWORKERS {
      let pid: i64 = sys_fork()
      if pid == 0 {
          if which == 0 { good_worker(w) }
          if which == 1 { bad_worker(w) }
          sys_exit(0)
      }
      pids[w] = pid
      w = w + 1
  }
  let st: *i64 = sys_mmap(16) as *i64
  w = 0
  while w < NWORKERS {
      sys_wait4(pids[w], st, 0)
      w = w + 1
  }
  return 0
142}
143
144// parse a file: total_lines into outs[0], torn_count returned.
145// A '\n'-terminated line is WELL-FORMED iff:
146//   - it begins with "FA w="
147//   - the 4 bytes immediately before the '\n' are " END" (space,E,N,D)
148//   - it contains exactly one " END" occurrence (no embedded second record head)
149// Anything else (interleaved fragments, a record head mid-line, missing sentinel)
150// is TORN.  An empty trailing segment (file ends with '\n') is not a line.
151func count_torn(path: *u8, outs: *i64) -> i64 {
  let szp: *i64 = sys_mmap(16) as *i64
  let b: *u8 = sys_read_file(path, szp)
  let sz: i64 = szp[0]
  var torn: i64 = 0
  var lines: i64 = 0
  var ls: i64 = 0
  var i: i64 = 0
  while i < sz {
      if b[i] == (10 as u8) {
          let llen: i64 = i - ls
          lines = lines + 1
          var ok: i64 = 1
          // prefix "FA w=" (5 bytes)
          if llen < 9 { ok = 0 }
          if ok == 1 {
              if b[ls] != (70 as u8) { ok = 0 }       // F
              if b[ls + 1] != (65 as u8) { ok = 0 }   // A
              if b[ls + 2] != (32 as u8) { ok = 0 }   // space
              if b[ls + 3] != (119 as u8) { ok = 0 }  // w
              if b[ls + 4] != (61 as u8) { ok = 0 }   // =
          }
          // suffix " END" immediately before '\n'
          if ok == 1 {
              let e: i64 = i - 1
              if b[e - 3] != (32 as u8) { ok = 0 }    // space
              if b[e - 2] != (69 as u8) { ok = 0 }    // E
              if b[e - 1] != (78 as u8) { ok = 0 }    // N
              if b[e]     != (68 as u8) { ok = 0 }    // D
          }
          // exactly one " END" token inside the line (no interleaved 2nd record)
          if ok == 1 {
              var ends: i64 = 0
              var j: i64 = ls
              while j + 3 < i + 1 {
                  if b[j] == (32 as u8) {
                      if b[j + 1] == (69 as u8) {
                          if b[j + 2] == (78 as u8) {
                              if b[j + 3] == (68 as u8) { ends = ends + 1 }
                          }
                      }
                  }
                  j = j + 1
              }
              if ends != 1 { ok = 0 }
              // also: no second "FA w=" record-head embedded (head appears only at ls)
              var k: i64 = ls + 1
              while k + 4 < i + 1 {
                  if b[k] == (70 as u8) {
                      if b[k + 1] == (65 as u8) {
                          if b[k + 2] == (32 as u8) {
                              if b[k + 3] == (119 as u8) {
                                  if b[k + 4] == (61 as u8) { ok = 0 }
                              }
                          }
                      }
                  }
                  k = k + 1
              }
          }
          if ok == 0 { torn = torn + 1 }
          ls = i + 1
      }
      i = i + 1
  }
  outs[0] = lines
  return torn
218}
219
220func main() -> i64 {
  let logfd: i64 = sys_openat_append("knowledge/status/framed_append_gate.log\x00" as *u8, 0x1a4)
  gp(logfd, "FRAMED-APPEND epoch=\x00" as *u8)
  gn(logfd, sys_now_realtime_sec())
  gp(logfd, " workers=\x00" as *u8); gn(logfd, NWORKERS)
  gp(logfd, " recs=\x00" as *u8); gn(logfd, NRECS)
  gp(logfd, " cap=\x00" as *u8); gn(logfd, RECCAP)
  gp(logfd, "\n\x00" as *u8)
228
  // fresh files each run (truncate)
  let gtr: i64 = sys_openat_wr("/tmp/fa_good.log\x00" as *u8, 0x1a4)
  if gtr > 0 { sys_close(gtr) }
  let btr: i64 = sys_openat_wr("/tmp/fa_bad.log\x00" as *u8, 0x1a4)
  if btr > 0 { sys_close(btr) }
234
  // GOOD lane: concurrent framed single-write appends
  spawn_all(0)
  // BAD lane (NEGATIVE CONTROL): same concurrency, OLD multi-write pattern
  spawn_all(1)
239
  let outs: *i64 = sys_mmap(16) as *i64
  let good_torn: i64 = count_torn("/tmp/fa_good.log\x00" as *u8, outs)
  let good_lines: i64 = outs[0]
  let bad_torn: i64 = count_torn("/tmp/fa_bad.log\x00" as *u8, outs)
  let bad_lines: i64 = outs[0]
  let want_lines: i64 = NWORKERS * NRECS
246
  // TAMPER: oversized record (rec_len+1 > cap=8) must be REJECTED with -2
  let trec: *u8 = sys_mmap(64)
  var ti: i64 = 0
  while ti < 32 { trec[ti] = 65 as u8; ti = ti + 1 }   // 32 'A's, way over cap=8
  let tamper_rc: i64 = fa_append("/tmp/fa_tamper.log\x00" as *u8, trec, 32, 8)
252
  gp(logfd, "FA row=good_lines got=\x00" as *u8); gn(logfd, good_lines)
  gp(logfd, " want=\x00" as *u8); gn(logfd, want_lines)
  if good_lines == want_lines { gp(logfd, " verdict=PASS\n\x00" as *u8) } else { gp(logfd, " verdict=FAIL\n\x00" as *u8) }
256
  gp(logfd, "FA row=good_torn got=\x00" as *u8); gn(logfd, good_torn)
  gp(logfd, " want=0\x00" as *u8)
  if good_torn == 0 { gp(logfd, " verdict=PASS\n\x00" as *u8) } else { gp(logfd, " verdict=FAIL\n\x00" as *u8) }
260
  gp(logfd, "FA row=neg_control bad_lines=\x00" as *u8); gn(logfd, bad_lines)
  gp(logfd, " bad_torn=\x00" as *u8); gn(logfd, bad_torn)
  gp(logfd, " want=POSITIVE\x00" as *u8)
  if bad_torn > 0 { gp(logfd, " verdict=PASS(detector-sees-tearing)\n\x00" as *u8) } else { gp(logfd, " verdict=FAIL(no-tearing-detected)\n\x00" as *u8) }
265
  gp(logfd, "FA row=tamper_oversize got=\x00" as *u8); gn(logfd, tamper_rc)
  gp(logfd, " want=-2\x00" as *u8)
  if tamper_rc == (0 - 2) { gp(logfd, " verdict=PASS\n\x00" as *u8) } else { gp(logfd, " verdict=FAIL\n\x00" as *u8) }
269
  var green: i64 = 1
  if good_lines != want_lines { green = 0 }
  if good_torn != 0 { green = 0 }
  if bad_torn <= 0 { green = 0 }
  if tamper_rc != (0 - 2) { green = 0 }
275
  gp(logfd, "FRAMED-APPEND verdict=\x00" as *u8)
  if green == 1 { gp(logfd, "GREEN\x00" as *u8) } else { gp(logfd, "RED\x00" as *u8) }
  gp(logfd, " good_lines=\x00" as *u8); gn(logfd, good_lines)
  gp(logfd, " good_torn=\x00" as *u8); gn(logfd, good_torn)
  gp(logfd, " bad_torn=\x00" as *u8); gn(logfd, bad_torn)
  gp(logfd, " tamper=\x00" as *u8); gn(logfd, tamper_rc)
  if green == 0 {
      gp(logfd, " reason=\x00" as *u8)
      if good_lines != want_lines { gp(logfd, "good-lines-lost \x00" as *u8) }
      if good_torn != 0 { gp(logfd, "GOOD-TORE \x00" as *u8) }
      if bad_torn <= 0 { gp(logfd, "neg-control-saw-no-tearing \x00" as *u8) }
      if tamper_rc != (0 - 2) { gp(logfd, "oversize-not-rejected \x00" as *u8) }
  }
  gp(logfd, "\n\x00" as *u8)
  if logfd > 0 { sys_close(logfd) }
  if green == 1 { return 0 }
  return 1
293}
nx_framed_append_gate.nx source

`nx_framed_append_gate.nx` source
