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

↩ module page · 308 lines · 14349 B
1// nx_capres_gate.nx -- THE GATE FOR THE CAPTURE-RESOLUTION RULER (subject: nx_capres / nx_capres_lib).
2//
3// WHAT IT PROVES, AND WHY EACH TOOTH EXISTS:
4//   * the ruler READS a resolution out of a real capture header rather than assuming one (PNG + NXFH1)
5//   * a capture below its subject's declared full resolution is REFUSED, not rounded up
6//   * a judge whose ceiling sits below the capture is reported BLIND -- that is NO score, not a low one
7//   * every "I could not look" path abstains (UNPROVEN) instead of acquitting
8//   * the shipped conf actually declares the subject the world lane depends on, and declares it ONCE
9//   * the CLI's EXIT CODE carries the verdict, checked by forking the real binary
10//
11// THE REQUIRED NEGATIVE CONTROL is neg-control-downsampled-capture-must-not-verdict-FULL: the whole
12// policy is worthless if a reduced capture can pass, so a tooth asserts that it CANNOT. It is paired
13// with a bite cell (fires on the reduced input, silent on the full one), because a detector that has
14// only ever seen good input has not been shown to fire.
15//
16// FIXTURES ARE ASSEMBLED AT RUNTIME in /tmp/, never checked in and never under knowledge/store: a gate
17// that shares a fixture with a production beat measures the fixture, and a detector that scans source
18// will find its own fixture written as a literal.
19// license_tier: ORIGINAL   No hw writes (Rule 26).
20import "nx_syscalls.nx"
21import "nx_gate_verdict.nx"
22import "nx_capres_lib.nx"
23
24const CG_MODE_644: i64 = 420
25const CG_FIX_PNG: *u8 = "/tmp/nx_capres_gate_full.png" as *u8
26const CG_FIX_PNG_SMALL: *u8 = "/tmp/nx_capres_gate_small.png" as *u8
27const CG_FIX_NXFH: *u8 = "/tmp/nx_capres_gate_frame.nxfh" as *u8
28const CG_FIX_JUNK: *u8 = "/tmp/nx_capres_gate_junk.bin" as *u8
29const CG_ELF: *u8 = "./nx_capres.elf" as *u8
30const CG_SUBJECT: *u8 = "world" as *u8
31const CG_OUT_BYTES: i64 = 64
32const CG_FIXBUF: i64 = 256
33const CG_JUNK_LEN: i64 = 64
34const CG_JUNK_FILL: i64 = 90            // an ASCII letter: junk that is plainly neither PNG nor NXFH1
35const CG_IHDR_LEN: i64 = 13             // RFC 2083: IHDR carries exactly 13 bytes
36const CG_U32: i64 = 4
37const CG_BYTE_BASE: i64 = 256
38
39// THE FIXTURE EXTENTS. Written as the DECLARED world resolution read from the conf at setup, not as
40// literals: a fixture that hardcodes the number it is testing against cannot fail when that number
41// moves, and the estate has shipped exactly that vacuity before. The small fixture is derived from
42// the full one by the SAME divisor the engine's adaptive controller was measured using.
43const CG_SMALL_DIV: i64 = 8             // q=8 -- the value nx_world_snap was MEASURED landing on
44
45func cg_u32be(b: *u8, off: i64, v: i64) -> i64 {
  var x: i64 = v
  var i: i64 = 0
  while i < CG_U32 {
      b[off + CG_U32 - 1 - i] = (x % CG_BYTE_BASE) as u8
      x = x / CG_BYTE_BASE
      i = i + 1
  }
  return 0
54}
55
56// Build a minimal but REAL PNG header (signature + IHDR length/type/width/height) and write it.
57func cg_write_png(path: *u8, w: i64, h: i64) -> i64 {
  let b: *u8 = sys_mmap(CG_FIXBUF)
  b[0] = 137 as u8
  b[1] = 80 as u8
  b[2] = 78 as u8
  b[3] = 71 as u8
  b[4] = 13 as u8
  b[5] = 10 as u8
  b[6] = 26 as u8
  b[7] = 10 as u8
  cg_u32be(b, 8, CG_IHDR_LEN)
  b[12] = 73 as u8
  b[13] = 72 as u8
  b[14] = 68 as u8
  b[15] = 82 as u8
  cg_u32be(b, 16, w)
  cg_u32be(b, 20, h)
  let fd: i64 = sys_openat_wr(path, CG_MODE_644)
  if fd < 0 { sys_munmap(b, CG_FIXBUF); return 0 }
  sys_write(fd, b, 24)
  sys_close(fd)
  sys_munmap(b, CG_FIXBUF)
  return 1
80}
81
82func cg_num_into(b: *u8, o: i64, v: i64) -> i64 {
  var m: i64 = v
  var p: i64 = o
  let t: *u8 = sys_mmap(32)
  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 }
  while k > 0 { k = k - 1; b[p] = t[k]; p = p + 1 }
  sys_munmap(t, 32)
  return p
92}
93
94// "NXFH1 <w> <h>" then a newline, then one pixel of hex so the file is not a bare header.
95func cg_write_nxfh(path: *u8, w: i64, h: i64) -> i64 {
  let b: *u8 = sys_mmap(CG_FIXBUF)
  let mg: *u8 = "NXFH1 " as *u8
  var p: i64 = 0
  var i: i64 = 0
  while mg[i] != (0 as u8) { b[p] = mg[i]; p = p + 1; i = i + 1 }
  p = cg_num_into(b, p, w)
  b[p] = 32 as u8
  p = p + 1
  p = cg_num_into(b, p, h)
  b[p] = 10 as u8
  p = p + 1
  let px: *u8 = "0011ff" as *u8
  i = 0
  while px[i] != (0 as u8) { b[p] = px[i]; p = p + 1; i = i + 1 }
  let fd: i64 = sys_openat_wr(path, CG_MODE_644)
  if fd < 0 { sys_munmap(b, CG_FIXBUF); return 0 }
  sys_write(fd, b, p)
  sys_close(fd)
  sys_munmap(b, CG_FIXBUF)
  return 1
116}
117
118func cg_write_junk(path: *u8) -> i64 {
  let b: *u8 = sys_mmap(CG_FIXBUF)
  var i: i64 = 0
  while i < CG_JUNK_LEN { b[i] = CG_JUNK_FILL as u8; i = i + 1 }
  let fd: i64 = sys_openat_wr(path, CG_MODE_644)
  if fd < 0 { sys_munmap(b, CG_FIXBUF); return 0 }
  sys_write(fd, b, CG_JUNK_LEN)
  sys_close(fd)
  sys_munmap(b, CG_FIXBUF)
  return 1
128}
129
130// 127 is execve-failed, negative is fork-failed. Either way the SUBJECT was never run, and that is a
131// precondition failure of this gate's environment -- never evidence about the subject.
132func cg_present(rc: i64) -> i64 {
  if rc < 0 { return 0 }
  if rc == 127 { return 0 }
  return 1
136}
137
138// fork the REAL binary and return its exit code; 127 = absent (a NAMED absence, not a pass)
139func cg_run3(elf: *u8, a1: *u8, a2: *u8, a3: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      let av: *i64 = sys_mmap(64) as *i64
      av[0] = elf as i64
      av[1] = a1 as i64
      av[2] = a2 as i64
      av[3] = a3 as i64
      av[4] = 0
      let ev: *i64 = sys_mmap(16) as *i64
      ev[0] = 0
      sys_execve(elf, av, ev)
      sys_exit(127)
  }
  if pid < 0 { return 0 - 1 }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  return (st[0] >> 8) & 0xff
157}
158
159func main(argc: i64, argv: *i64) -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_capres gate -- a capture below the product's own resolution is REFUSABLE, and a judge that cannot see it says so" as *u8)
162
  // ---- the conf IS the denominator. Bind every assertion below to it. --------------------------
  let f: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  let havew: i64 = cr_conf_res(CR_CONF, CG_SUBJECT, f)
  gv_check("conf-declares-the-world-subject-so-the-teeth-below-have-a-denominator" as *u8, havew, ctr)
  // A CONF THAT PERMITS TWO ANSWERS FOR ONE KEY IS A COIN FLIP WEARING A SCHEMA: first-match versus
  // last-match would silently decide the verdict.
  let dup: i64 = cr_conf_count(CR_CONF, CG_SUBJECT)
  var dup1: i64 = 0
  if dup == 1 { dup1 = 1 }
  gv_check("conf-declares-that-subject-exactly-once-no-duplicate-key" as *u8, dup1, ctr)
173
  let FW: i64 = f[0]
  let FH: i64 = f[1]
  // ASSERT THE FIXTURE REACHED THE CONDITION BEFORE ASSERTING ANY OUTCOME. A zero-extent conf row
  // would make every comparison below vacuously true.
  var extok: i64 = 0
  if FW > 0 { if FH > 0 { extok = 1 } }
  gv_check("fixture-precondition-declared-extent-is-nonzero" as *u8, extok, ctr)
  let SW: i64 = FW/CG_SMALL_DIV
  let SH: i64 = FH/CG_SMALL_DIV
  var smallok: i64 = 0
  if SW > 0 { if SW < FW { smallok = 1 } }
  gv_check("fixture-precondition-the-reduced-fixture-is-genuinely-smaller" as *u8, smallok, ctr)
186
  // ---- 1. the ruler READS the resolution, it does not assume one ------------------------------
  cg_write_png(CG_FIX_PNG, FW, FH)
  let d: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  cr_dims_of_file(CG_FIX_PNG, d)
  var t1: i64 = 0
  if d[0] == CR_KIND_PNG { if d[1] == FW { if d[2] == FH { t1 = 1 } } }
  gv_check("png-IHDR-width-and-height-are-READ-from-the-file" as *u8, t1, ctr)
  gv_puts("    read kind=" as *u8); gv_num(d[0])
  gv_puts(" w=" as *u8); gv_num(d[1])
  gv_puts(" h=" as *u8); gv_num(d[2])
  gv_puts(" expected w=" as *u8); gv_num(FW)
  gv_puts(" h=" as *u8); gv_num(FH); gv_puts("\n" as *u8)
199
  cg_write_nxfh(CG_FIX_NXFH, FW, FH)
  let d2: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  cr_dims_of_file(CG_FIX_NXFH, d2)
  var t2: i64 = 0
  if d2[0] == CR_KIND_NXFH1 { if d2[1] == FW { if d2[2] == FH { t2 = 1 } } }
  gv_check("nxfh1-header-width-and-height-are-READ-from-the-file" as *u8, t2, ctr)
206
  // ---- 2. THE NEGATIVE CONTROL: a downsampled capture must NOT read as full -------------------
  cg_write_png(CG_FIX_PNG_SMALL, SW, SH)
  let ds: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  cr_dims_of_file(CG_FIX_PNG_SMALL, ds)
  let pm_small: i64 = cr_permil(ds[1], ds[2], FW, FH)
  let v_small: i64 = cr_verdict(pm_small)
  var t3: i64 = 0
  if v_small == CR_V_REDUCED { t3 = 1 }
  gv_check("neg-control-downsampled-capture-must-not-verdict-FULL" as *u8, t3, ctr)
  gv_puts("    reduced fixture " as *u8); gv_num(ds[1]); gv_puts("x" as *u8); gv_num(ds[2])
  gv_puts(" of " as *u8); gv_num(FW); gv_puts("x" as *u8); gv_num(FH)
  gv_puts(" -> res_permil=" as *u8); gv_num(pm_small)
  gv_puts(" verdict_code=" as *u8); gv_num(v_small); gv_puts("\n" as *u8)
220
  let pm_full: i64 = cr_permil(d[1], d[2], FW, FH)
  let v_full: i64 = cr_verdict(pm_full)
  var t4: i64 = 0
  if v_full == CR_V_FULL { t4 = 1 }
  gv_check("a-native-capture-verdicts-FULL" as *u8, t4, ctr)
226
  // BITE: the detector must FIRE on the reduced capture and stay SILENT on the full one. A rule that
  // has only ever seen good input is unverified.
  var fired: i64 = 0
  if v_small == CR_V_REDUCED { fired = 1 }
  var falsepos: i64 = 0
  if v_full != CR_V_FULL { falsepos = 1 }
  gv_bite("bite-reduction-detector-fires-on-reduced-and-is-silent-on-native" as *u8, fired, falsepos, ctr)
234
  // ---- 3. abstain, never acquit ---------------------------------------------------------------
  cg_write_junk(CG_FIX_JUNK)
  let dj: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  let kj: i64 = cr_dims_of_file(CG_FIX_JUNK, dj)
  var t5: i64 = 0
  if kj == CR_KIND_UNKNOWN { t5 = 1 }
  gv_check("neg-control-an-unreadable-artifact-is-UNKNOWN-not-a-resolution" as *u8, t5, ctr)
242
  var t6: i64 = 0
  if cr_permil(0, 0, FW, FH) < 0 { if cr_verdict(cr_permil(0, 0, FW, FH)) == CR_V_UNPROVEN { t6 = 1 } }
  gv_check("neg-control-an-unusable-numerator-abstains-UNPROVEN-never-passes" as *u8, t6, ctr)
  var t7: i64 = 0
  if cr_verdict(cr_permil(FW, FH, 0, FH)) == CR_V_UNPROVEN { t7 = 1 }
  gv_check("neg-control-a-zero-denominator-abstains-UNPROVEN-never-passes" as *u8, t7, ctr)
249
  // a capture LARGER than declared is not a reduction: more evidence is never less
  var t8: i64 = 0
  if cr_verdict(cr_permil(FW*2, FH*2, FW, FH)) == CR_V_FULL { t8 = 1 }
  gv_check("a-superset-capture-is-still-FULL-not-a-false-REDUCED" as *u8, t8, ctr)
254
  // ---- 4. THE HIDDEN HALF: can the judge SEE it? ----------------------------------------------
  // A judge whose ceiling is below the capture returns a number about a downsample, a crop or a
  // prefix. That is not a low score, it is NO score, and reading it as quality is how a resolution
  // ceiling gets mistaken for a quality ceiling.
  let j: *i64 = sys_mmap(CG_OUT_BYTES) as *i64
  let havej: i64 = cr_conf_res(CR_CONF, "judge.nx_percept" as *u8, j)
  gv_check("conf-declares-a-judge-ceiling-so-the-blindness-teeth-have-a-denominator" as *u8, havej, ctr)
  var t9: i64 = 0
  if cr_judge(FW, FH, j[0], j[1]) == CR_J_BLIND { t9 = 1 }
  gv_check("neg-control-a-judge-whose-ceiling-is-below-the-capture-is-reported-BLIND" as *u8, t9, ctr)
  gv_puts("    judge ceiling " as *u8); gv_num(j[0]); gv_puts("x" as *u8); gv_num(j[1])
  gv_puts(" vs capture " as *u8); gv_num(FW); gv_puts("x" as *u8); gv_num(FH); gv_puts("\n" as *u8)
  var t10: i64 = 0
  if cr_judge(j[0], j[1], j[0], j[1]) == CR_J_SEES { t10 = 1 }
  gv_check("a-judge-handed-exactly-its-ceiling-SEES-the-whole-image" as *u8, t10, ctr)
  var t11: i64 = 0
  if cr_judge(j[0]+1, j[1], j[0], j[1]) == CR_J_BLIND { t11 = 1 }
  gv_check("neg-control-one-axis-over-the-ceiling-is-still-BLIND-extent-not-area" as *u8, t11, ctr)
273
  // ---- 5. THE EXIT CODE CARRIES THE VERDICT, proven by forking the real binary ----------------
  // A ruler whose exit code does not carry its verdict silently blesses every failure it finds, so
  // this is checked end-to-end rather than in-process. An absent binary is a NAMED absence (SKIP),
  // never a pass: the gate must not report on its own environment in the same word it reports on
  // the subject.
  let rc_full: i64 = cg_run3(CG_ELF, "check" as *u8, CG_FIX_PNG, CG_SUBJECT)
  let present: i64 = gv_need("nx_capres.elf built and forkable from the serving root" as *u8, cg_present(rc_full), ctr)
  if present == 1 {
      var t12: i64 = 0
      if rc_full == CR_V_FULL { t12 = 1 }
      gv_check("e2e-CLI-exits-0-FULL-on-a-native-capture" as *u8, t12, ctr)
      let rc_small: i64 = cg_run3(CG_ELF, "check" as *u8, CG_FIX_PNG_SMALL, CG_SUBJECT)
      var t13: i64 = 0
      if rc_small == CR_V_REDUCED { t13 = 1 }
      gv_check("neg-control-e2e-CLI-exits-1-REDUCED-on-a-downsampled-capture" as *u8, t13, ctr)
      let rc_junk: i64 = cg_run3(CG_ELF, "check" as *u8, CG_FIX_JUNK, CG_SUBJECT)
      var t14: i64 = 0
      if rc_junk == CR_V_UNPROVEN { t14 = 1 }
      gv_check("e2e-CLI-exits-3-UNPROVEN-on-an-unreadable-artifact" as *u8, t14, ctr)
      let rc_unk: i64 = cg_run3(CG_ELF, "check" as *u8, CG_FIX_PNG, "no_such_subject_declared" as *u8)
      var t15: i64 = 0
      if rc_unk == CR_V_UNPROVEN { t15 = 1 }
      gv_check("neg-control-e2e-an-UNDECLARED-subject-abstains-rather-than-acquitting" as *u8, t15, ctr)
      gv_puts("    e2e exits: full=" as *u8); gv_num(rc_full)
      gv_puts(" reduced=" as *u8); gv_num(rc_small)
      gv_puts(" junk=" as *u8); gv_num(rc_junk)
      gv_puts(" unknown_subject=" as *u8); gv_num(rc_unk); gv_puts("\n" as *u8)
  }
302
  sys_unlinkat(CG_FIX_PNG)
  sys_unlinkat(CG_FIX_PNG_SMALL)
  sys_unlinkat(CG_FIX_NXFH)
  sys_unlinkat(CG_FIX_JUNK)
  return gv_verdict("CAPRES-GATE" as *u8, ctr, "a capture below the product's declared resolution is refusable, and a judge that cannot see it says UNJUDGED-AT-RESOLUTION instead of scoring" as *u8)
308}
nx_capres_gate.nx source

`nx_capres_gate.nx` source
