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

↩ module page · 253 lines · 11337 B
1// nx_models_page_emit_gate.nx -- the models gallery is EMITTED FROM DATA and cannot drift from the
2// assets: this gate proves the emitter END-TO-END by forking the deployed _offc elf over the real
3// rows, the real corpus and the banked hand-page baseline. Teeth (per-tooth gv_check, verdict via
4// gv_verdict so the exit code IS the verdict):
5//   - emit over production rows exits 0 and writes
6//   - card count equals row count and is nonzero (denominator IN the condition, both printed)
7//   - every row's measurement is announced on stdout
8//   - neg-control: removing a row makes its card VANISH (positional row, no content coupling)
9//   - baseline parity: every h2 title and every measured triple in knowledge/models_page.baseline
10//     appears in the emitted page (transcription proof: content moved, none lost)
11//   - honesty tokens carried (TEXM FACE MORF + the provenance caption)
12//   - generated-artefact stamp present
13//   - neg-control: empty rows REFUSE and write nothing
14//   - determinism: same inputs emit byte-identical output
15// Fixtures live in /tmp/nx_models_page_emit_gate/ and are REBUILT AND REMOVED AT SETUP (a stale
16// outC from a crashed run would fail the absence tooth -- idempotency is part of the gate).
17// license_tier: ORIGINAL   expect_exit: 0
18import "nx_syscalls.nx"
19import "nx_gatekit_lib.nx"
20import "nx_gate_verdict.nx"
21
22const MPG_A_NL:   i64 = 10
23const MPG_A_CR:   i64 = 13
24const MPG_A_HASH: i64 = 35
25const MPG_A_PIPE: i64 = 124
26const MPG_A_D0:   i64 = 48
27const MPG_A_D9:   i64 = 57
28const MPG_EXIT_UNOBS: i64 = 3
29const MPG_CAP_STDOUT: i64 = 262144
30const MPG_CAP_PAGE:   i64 = 1048576
31const MPG_CAP_PATH:   i64 = 4096
32const MPG_WORD:       i64 = 8
33const MPG_ROW2:       i64 = 2
34
35const MPG_SUBJECT: *u8 = "_offc/nx_models_page_emit.elf"
36const MPG_ROWS:    *u8 = "knowledge/models_page.rows"
37const MPG_BASE:    *u8 = "knowledge/models_page.baseline"
38const MPG_DIR:     *u8 = "/tmp/nx_models_page_emit_gate"
39const MPG_OUTA:    *u8 = "/tmp/nx_models_page_emit_gate/outA.html"
40const MPG_OUTB:    *u8 = "/tmp/nx_models_page_emit_gate/outB.html"
41const MPG_OUTC:    *u8 = "/tmp/nx_models_page_emit_gate/outC.html"
42const MPG_OUTD:    *u8 = "/tmp/nx_models_page_emit_gate/outD.html"
43const MPG_RMINUS:  *u8 = "/tmp/nx_models_page_emit_gate/rows_minus"
44const MPG_REMPTY:  *u8 = "/tmp/nx_models_page_emit_gate/rows_empty"
45
46func mpg_find(hay: *u8, hn: i64, from: i64, ned: *u8, nl: i64) -> i64 {
  if nl <= 0 { return 0 - 1 }
  var i: i64 = from
  while i + nl <= hn {
      var k: i64 = 0
      var hit: i64 = 1
      while k < nl {
          if hay[i + k] != ned[k] { hit = 0; k = nl } else { k = k + 1 }
      }
      if hit == 1 { return i }
      i = i + 1
  }
  return 0 - 1
59}
60
61func mpg_finds(hay: *u8, hn: i64, from: i64, ned: *u8) -> i64 { return mpg_find(hay, hn, from, ned, gk_len(ned)) }
62
63func mpg_num_after(b: *u8, n: i64, ned: *u8) -> i64 {
  let p: i64 = mpg_finds(b, n, 0, ned)
  if p < 0 { return 0 - 1 }
  var i: i64 = p + gk_len(ned)
  var v: i64 = 0
  var any: i64 = 0
  while i < n {
      let c: i64 = b[i] as i64
      if c >= MPG_A_D0 { if c <= MPG_A_D9 { v = v * (MPG_A_D9 - MPG_A_D0 + 1) + (c - MPG_A_D0); any = 1; i = i + 1 } else { i = n } } else { i = n }
  }
  if any == 0 { return 0 - 1 }
  return v
75}
76
77func mpg_count_occurs(b: *u8, n: i64, ned: *u8) -> i64 {
  var c: i64 = 0
  var p: i64 = 0
  let nl: i64 = gk_len(ned)
  while p >= 0 {
      p = mpg_find(b, n, p, ned, nl)
      if p >= 0 { c = c + 1; p = p + nl }
  }
  return c
86}
87
88func main(argc: i64, argv: *i64) -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_models_page_emit gate -- the gallery is emitted from data and measurement, proven end-to-end" as *u8)
91
  // ---- setup: idempotent fixtures ----
  gk_mkdir(MPG_DIR)
  gk_rm(MPG_OUTA)
  gk_rm(MPG_OUTB)
  gk_rm(MPG_OUTC)
  gk_rm(MPG_OUTD)
  let rp: *i64 = sys_mmap(MPG_WORD * 2) as *i64
  let rb: *u8 = sys_read_file(MPG_ROWS, rp)
  gv_need("production-rows-readable" as *u8, (rb as i64) != 0, ctr)
  if (rb as i64) == 0 { return gv_verdict("nx_models_page_emit" as *u8, ctr, "rows unreadable" as *u8) }
  let rn: i64 = rp[0]
103
  // count data rows; build rows_minus (drop the SECOND data row, positionally -- no content
  // coupling) and remember the dropped row's TITLE (field 4) for the vanish assertion
  let minus: *u8 = sys_mmap(rn + MPG_WORD)
  let title: *u8 = sys_mmap(MPG_CAP_PATH)
  var nrows: i64 = 0
  var mpos: i64 = 0
  var i: i64 = 0
  var tlen: i64 = 0
  while i < rn {
      let e: i64 = gk_eol(rb, i, rn)
      var len: i64 = e - i
      if len > 0 { if rb[i + len - 1] == (MPG_A_CR as u8) { len = len - 1 } }
      var isdata: i64 = 1
      if len <= 0 { isdata = 0 }
      if isdata == 1 { if rb[i] == (MPG_A_HASH as u8) { isdata = 0 } }
      var drop: i64 = 0
      if isdata == 1 {
          nrows = nrows + 1
          if nrows == MPG_ROW2 {
              drop = 1
              var f: i64 = 0
              var c: i64 = i
              while c < i + len {
                  if rb[c] == (MPG_A_PIPE as u8) {
                      f = f + 1
                      if f == 4 {
                          var t: i64 = c + 1
                          while t < i + len {
                              if rb[t] == (MPG_A_PIPE as u8) { c = i + len; t = i + len } else { title[tlen] = rb[t]; tlen = tlen + 1; t = t + 1 }
                          }
                      }
                  }
                  c = c + 1
              }
          }
      }
      if drop == 0 {
          var k: i64 = 0
          while k < e - i { minus[mpos] = rb[i + k]; mpos = mpos + 1; k = k + 1 }
          minus[mpos] = MPG_A_NL as u8
          mpos = mpos + 1
      }
      i = e + 1
  }
  title[tlen] = 0 as u8
  minus[mpos] = 0 as u8
  gk_write(MPG_RMINUS, minus)
  gk_write(MPG_REMPTY, "# no data rows -- the empty-refusal fixture\n" as *u8)
  gv_need("fixture-reached-the-condition (a second data row exists to drop, its title captured)" as *u8, tlen > 0, ctr)
153
  // ---- T1: emit over production rows ----
  let so: *u8 = sys_mmap(MPG_CAP_STDOUT)
  let sl: *i64 = sys_mmap(MPG_WORD) as *i64
  let rc1: i64 = gk_run_capture(MPG_SUBJECT, MPG_ROWS, MPG_OUTA, 0 as *u8, 0 as *u8, so, MPG_CAP_STDOUT, sl)
  gv_check("emit-over-production-rows-exits-OK-and-writes" as *u8, (rc1 == 0) * gk_exists(MPG_OUTA), ctr)
159
  // ---- T2: cards == rows, nonzero, from the organ's own announcement ----
  let cards: i64 = mpg_num_after(so, sl[0], "NX-MODELS-PAGE cards=" as *u8)
  gv_puts("  values: rows=" as *u8); gv_num(nrows); gv_puts(" cards=" as *u8); gv_num(cards); gv_puts("\n" as *u8)
  var t2: i64 = 0
  if cards == nrows { if nrows > 0 { t2 = 1 } }
  gv_check("cards-count-equals-rows-count-and-nonzero" as *u8, t2, ctr)
166
  // ---- T3: every row's measurement announced ----
  let ann: i64 = mpg_count_occurs(so, sl[0], "card id=" as *u8)
  var t3: i64 = 0
  if ann == nrows { if nrows > 0 { t3 = 1 } }
  gv_check("per-card-measurement-announced-for-every-row" as *u8, t3, ctr)
172
  // ---- T4: neg-control -- removed row vanishes ----
  let rc2: i64 = gk_run_capture(MPG_SUBJECT, MPG_RMINUS, MPG_OUTB, 0 as *u8, 0 as *u8, so, MPG_CAP_STDOUT, sl)
  gv_need("minus-fixture-emits" as *u8, rc2 == 0, ctr)
  let pa: *i64 = sys_mmap(MPG_WORD * 2) as *i64
  let pageA: *u8 = sys_read_file(MPG_OUTA, pa)
  let pb: *i64 = sys_mmap(MPG_WORD * 2) as *i64
  let pageB: *u8 = sys_read_file(MPG_OUTB, pb)
  var inA: i64 = 0
  var inB: i64 = 0
  if (pageA as i64) != 0 { if mpg_finds(pageA, pa[0], 0, title) >= 0 { inA = 1 } }
  if (pageB as i64) != 0 { if mpg_finds(pageB, pb[0], 0, title) >= 0 { inB = 1 } }
  gv_bite("neg-control-removed-row-vanishes-from-emit" as *u8, 1 - inB, 1 - inA, ctr)
185
  // ---- T5: baseline parity -- every h2 title and measured triple survives transcription ----
  let bp: *i64 = sys_mmap(MPG_WORD * 2) as *i64
  let base: *u8 = sys_read_file(MPG_BASE, bp)
  gv_need("baseline-readable" as *u8, (base as i64) != 0, ctr)
  var total: i64 = 0
  var found: i64 = 0
  if (base as i64) != 0 { if (pageA as i64) != 0 {
      var scan: i64 = 0
      while scan >= 0 {
          let h: i64 = mpg_finds(base, bp[0], scan, "<h2>" as *u8)
          if h < 0 { scan = 0 - 1 } else {
              let hend: i64 = mpg_finds(base, bp[0], h, "</h2>" as *u8)
              if hend < 0 { scan = 0 - 1 } else {
                  total = total + 1
                  if mpg_find(pageA, pa[0], 0, (base as i64 + h + 4) as *u8, hend - h - 4) >= 0 { found = found + 1 }
                  scan = hend
              }
          }
      }
      scan = 0
      while scan >= 0 {
          let v: i64 = mpg_finds(base, bp[0], scan, "<b>verts" as *u8)
          if v < 0 { scan = 0 - 1 } else {
              let vend: i64 = mpg_finds(base, bp[0], v, "</b>" as *u8)
              if vend < 0 { scan = 0 - 1 } else {
                  total = total + 1
                  if mpg_find(pageA, pa[0], 0, (base as i64 + v) as *u8, vend - v) >= 0 { found = found + 1 }
                  scan = vend
              }
          }
      }
  } }
  gv_puts("  values: parity_total=" as *u8); gv_num(total); gv_puts(" parity_found=" as *u8); gv_num(found); gv_puts("\n" as *u8)
  var t5: i64 = 0
  if total > 0 { if found == total { t5 = 1 } }
  gv_check("baseline-content-parity-titles-and-triples-lost-zero" as *u8, t5, ctr)
  var tok: i64 = 1
  if gk_contains(MPG_OUTA, "TEXM" as *u8) == 0 { tok = 0 }
  if gk_contains(MPG_OUTA, "FACE" as *u8) == 0 { tok = 0 }
  if gk_contains(MPG_OUTA, "MORF" as *u8) == 0 { tok = 0 }
  if gk_contains(MPG_OUTA, "not a hardware policy" as *u8) == 0 { tok = 0 }
  if gk_contains(MPG_OUTA, "provenance" as *u8) == 0 { tok = 0 }
  gv_check("honesty-tokens-carried-TEXM-FACE-MORF-provenance" as *u8, tok, ctr)
229
  // ---- T6: the page declares itself generated ----
  gv_check("generated-artefact-stamp-present" as *u8, gk_contains(MPG_OUTA, "NX-DERIVED: regenerated artefact" as *u8), ctr)
232
  // ---- T7: neg-control -- empty rows refuse and write nothing ----
  let rc3: i64 = gk_run_capture(MPG_SUBJECT, MPG_REMPTY, MPG_OUTC, 0 as *u8, 0 as *u8, so, MPG_CAP_STDOUT, sl)
  var t7: i64 = 0
  if rc3 == MPG_EXIT_UNOBS { if gk_exists(MPG_OUTC) == 0 { t7 = 1 } }
  gv_check("neg-control-empty-rows-refuses-and-writes-nothing" as *u8, t7, ctr)
238
  // ---- T8: determinism ----
  let rc4: i64 = gk_run_capture(MPG_SUBJECT, MPG_ROWS, MPG_OUTD, 0 as *u8, 0 as *u8, so, MPG_CAP_STDOUT, sl)
  gv_need("second-emit-exits-OK" as *u8, rc4 == 0, ctr)
  let pd: *i64 = sys_mmap(MPG_WORD * 2) as *i64
  let pageD: *u8 = sys_read_file(MPG_OUTD, pd)
  var same: i64 = 0
  if (pageA as i64) != 0 { if (pageD as i64) != 0 { if pa[0] == pd[0] {
      same = 1
      var k: i64 = 0
      while k < pa[0] { if pageA[k] != pageD[k] { same = 0; k = pa[0] } else { k = k + 1 } }
  } } }
  gv_check("same-inputs-byte-identical-emit" as *u8, same, ctr)
251
  return gv_verdict("nx_models_page_emit" as *u8, ctr, "the gallery is emitted from data and per-emit measurement; content proven moved, never lost" as *u8)
253}
nx_models_page_emit_gate.nx source

`nx_models_page_emit_gate.nx` source
