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

↩ module page · 194 lines · 10539 B
1// nx_suitebench_gate.nx -- the regression proof for the suite ruler. It imports nx_suitebench_lib, which is
2// the SAME code the shipped ruler runs, so these teeth verify the instrument rather than a copy of it.
3//
4// The teeth that matter are the negative ones. An instrument that only demonstrates its happy path proves
5// nothing: the whole value of this ruler is that it REFUSES bad input, so the gate has to show the refusals
6// actually fire -- a fabricated citation must not be findable, a stub-worded claim must fall, and a cell an
7// incumbent does not ship must not reach the denominator. T9 goes further and MUTATES a real row to prove
8// the cynical bar is load-bearing: if the mutation does not lower the score, the bar is decoration.
9// license_tier: ORIGINAL  expect_exit: 0
10import "nx_suitebench_lib.nx"
11import "nx_honesty_grade_lib.nx"
12
13const GT_AXBUF:  i64 = 65536
14const GT_CORPUS: i64 = 262144
15const GT_ROWBUF: i64 = 512
16
17func g_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
18func g_n(v: i64) -> i64 {
  let bb: *u8=sys_mmap(28); var m: i64=v
  if m<0 { m=0-m; sys_write(1,"-" as *u8,1) }
  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); return 0
27}
28func g_t(pass: i64, label: *u8, fails: *i64) -> i64 {
  g_w("  " as *u8); g_w(label); g_w(": " as *u8)
  if pass==1 { g_w("PASS\n" as *u8) } else { g_w("FAIL\n" as *u8); fails[0]=fails[0]+1 }
  return 0
32}
33// copy a NUL-terminated literal into a writable buffer (the splitter mutates in place, literals must not be)
34func g_cp(dst: *u8, src: *u8) -> i64 {
  var i: i64=0
  while src[i]!=(0 as u8) { dst[i]=src[i]; i=i+1 }
  dst[i]=0 as u8
  return i
39}
40
41func main() -> i64 {
  let fails: *i64 = sys_mmap(16) as *i64
  fails[0]=0
  // every read below goes through the portable resolver: this gate must run beside the SSOT on the NAS,
  // not only in the laptop tree where the corpus happened to be born (seq884).
  let scratch: *u8 = sys_mmap(GT_ROWBUF)
  g_w("=== nx_suitebench_gate -- the suite ruler must refuse what it cannot prove ===\n" as *u8)
48
  // ---- T1: the shipped data planes load and parse ----
  let axbuf: *u8 = sys_mmap(GT_AXBUF)
  let n_ax: i64 = sb_read_rooted("knowledge/registry/suitebench.axes" as *u8, axbuf, GT_AXBUF, scratch)
  let rvbuf: *u8 = sys_mmap(GT_AXBUF)
  let n_rv: i64 = sb_read_rooted("knowledge/registry/suitebench.rivals" as *u8, rvbuf, GT_AXBUF, scratch)
  var t1: i64=0
  if n_ax>0 { if n_rv>0 { t1=1 } }
  g_w("  axes bytes=" as *u8); g_n(n_ax); g_w("  rivals bytes=" as *u8); g_n(n_rv); g_w("\n" as *u8)
  g_t(t1, "T1 both data planes load from disk (rows are data, not code)" as *u8, fails)
58
  // ---- T2: a REAL claim whose evidence carries a stub-tell falls to STUB ----
  let honest_stub: i64 = hg_grade(3, "a live synthetic roster of 4 people" as *u8)
  g_t(honest_stub==1, "T2 REAL claim + stub-tell evidence is downgraded to STUB" as *u8, fails)
62
  // ---- T3: a REAL claim with no active reality token is capped at PARTIAL ----
  let honest_cap: i64 = hg_grade(3, "a complete calendar engine with recurrence and conflicts" as *u8)
  g_t(honest_cap==2, "T3 REAL claim without a reality token is capped at PARTIAL" as *u8, fails)
66
  // ---- T4: a phrase that IS in the banked corpus is found ----
  let corp: *u8 = sys_mmap(GT_CORPUS)
  let n_c: i64 = sb_read_rooted("knowledge/library/rival_telegram.txt" as *u8, corp, GT_CORPUS, scratch)
  let found_real: i64 = sb_find(corp, n_c, "instant messaging" as *u8)
  g_w("  corpus bytes read=" as *u8); g_n(n_c); g_w("\n" as *u8)
  var t4: i64=0
  if n_c>0 { if found_real==1 { t4=1 } }
  g_t(t4, "T4 a real incumbent phrase is found in the banked bytes" as *u8, fails)
75
  // ---- T5: NEG-CONTROL. A fabricated incumbent fact must NOT be findable. This is the whole liar-kill:
  // if this tooth ever passes by finding the phrase, any claim could be invented and cited. ----
  let found_fake: i64 = sb_find(corp, n_c, "Telegram ships a sovereign family calendar" as *u8)
  g_t(found_fake==0, "T5 NEG-CONTROL fabricated incumbent claim is NOT citable" as *u8, fails)
80
  // ---- T6: the EXT-only law, all four cases ----
  let ext_has_cited:   i64 = sb_is_ext(SB_HAS, 1)
  let ext_has_uncited: i64 = sb_is_ext(SB_HAS, 0)
  let ext_lacks:       i64 = sb_is_ext(SB_LACKS, 1)
  let ext_unknown:     i64 = sb_is_ext(SB_UNKNOWN, 1)
  var t6: i64=0
  if ext_has_cited==1 { if ext_has_uncited==0 { if ext_lacks==0 { if ext_unknown==0 { t6=1 } } } }
  g_t(t6, "T6 only a cited HAS cell counts; lacks, unmeasured and uncited never reach the denominator" as *u8, fails)
89
  // ---- T7: the in-place splitter ----
  let row: *u8 = sys_mmap(GT_ROWBUF)
  let rlen: i64 = g_cp(row, "C2|calendar|1|0|no shared or family calendar exists" as *u8)
  let fld: **u8 = sys_mmap(8*SB_NFIELD) as **u8
  let nf: i64 = sb_split(row, 0, rlen, fld)
  var t7: i64=0
  if nf==5 {
      if sb_eq(fld[0], "C2" as *u8)==1 {
          if sb_eq(fld[1], "calendar" as *u8)==1 {
              if sb_atoi(fld[2])==1 {
                  if sb_atoi(fld[3])==0 {
                      if sb_eq(fld[4], "no shared or family calendar exists" as *u8)==1 { t7=1 }
                  }
              }
          }
      }
  }
  g_w("  split fields=" as *u8); g_n(nf); g_w("\n" as *u8)
  g_t(t7, "T7 a five-field row splits in place into exactly the right five fields" as *u8, fails)
109
  // ---- T8: the ranking keys behave, and admission is not a popularity contest ----
  let r_far:  i64 = sb_rank(2, 0)
  let r_near: i64 = sb_rank(2, 2)
  let r_many: i64 = sb_rank(4, 1)
  let r_few:  i64 = sb_rank(1, 1)
  let adm_op_alone: i64 = sb_admit(0, 1, 0)
  let adm_nobody:   i64 = sb_admit(0, 0, 0)
  let adm_done:     i64 = sb_admit(4, 1, 3)
  var t8: i64=0
  if r_far>r_near { if r_many>r_few { if adm_op_alone==1 { if adm_nobody==0 { if adm_done==0 { t8=1 } } } } }
  g_t(t8, "T8 rank rises with shortfall and with incumbent count; an operator-named axis enters even at zero incumbents; a satisfied axis never does" as *u8, fails)
121
  // ---- T9: MUTATION PROOF. Take a row that currently grades PARTIAL, inject a stub-tell into its
  // evidence, and require the honest level to FALL. If it does not, the cynical bar is decoration and
  // every number this ruler prints is unearned. ----
  let ev_ok:  *u8 = "live OPAQUE aPAKE register login whoami over the public edge" as *u8
  let ev_bad: *u8 = "live OPAQUE aPAKE register login on a synthetic roster" as *u8
  let lvl_ok:  i64 = hg_grade(2, ev_ok)
  let lvl_bad: i64 = hg_grade(2, ev_bad)
  g_w("  mutation: level " as *u8); g_n(lvl_ok); g_w(" -> " as *u8); g_n(lvl_bad); g_w("\n" as *u8)
  var t9: i64=0
  if lvl_bad<lvl_ok { t9=1 }
  g_t(t9, "T9 MUTATION mutating real evidence into stub evidence LOWERS the score" as *u8, fails)
133
  // ---- T10: every HAS row in the SHIPPED rivals file is citable right now. This is the tooth that
  // breaks the build if the corpus is moved, truncated or drifts away from the claims made about it. ----
  let cbuf: *u8 = sys_mmap(GT_CORPUS*4)
  var scanned: i64=0
  var bad: i64=0
  var p: i64=0
  var last_file: *u8 = "" as *u8
  var last_len: i64 = 0
  while p<n_rv {
      var e: i64=p
      while e<n_rv { if rvbuf[e]==(SB_NL as u8) { break } e=e+1 }
      if rvbuf[p]!=(SB_HASH as u8) {
          if e>p {
              let nfr: i64 = sb_split(rvbuf, p, e, fld)
              if nfr>=5 {
                  if sb_atoi(fld[2])==SB_HAS {
                      if sb_eq(fld[3], last_file)==0 {
                          last_len = sb_read_rooted(fld[3], cbuf, GT_CORPUS*4, scratch)
                          last_file = fld[3]
                      }
                      scanned=scanned+1
                      if last_len<=0 { bad=bad+1 }
                      else { if sb_find(cbuf, last_len, fld[4])==0 { bad=bad+1 } }
                  }
              }
          }
      }
      p=e+1
  }
  g_w("  shipped HAS cells scanned=" as *u8); g_n(scanned); g_w("  uncitable=" as *u8); g_n(bad); g_w("\n" as *u8)
  var t10: i64=0
  if scanned>0 { if bad==0 { t10=1 } }
  g_t(t10, "T10 every incumbent claim in the shipped rivals file is citable against the banked corpus" as *u8, fails)
167
  // ---- T11: the PORTABLE EVIDENCE ROOT. seq884 was that the citation corpus lived only in the laptop
  // tree, so this gate could not run beside the SSOT on the NAS. The fix is only real if the resolver
  // actually answers AND can still say NO for a path that exists under no root -- a resolver that always
  // finds something would mask a missing corpus, which is the exact failure it was built to prevent.
  // Building this tooth is also what surfaced the compiler bug in the resolver: `"" as *u8` returns a
  // pointer to the NEXT literal in the pool, so the "here" root silently became "runtime/".
  let probe: *u8 = sys_mmap(GT_ROWBUF)
  let root_ok: i64 = sb_which_root("knowledge/registry/suitebench.axes" as *u8, scratch, probe, GT_ROWBUF)
  let root_no: i64 = sb_which_root("knowledge/registry/there_is_no_such_plane.axes" as *u8, scratch, probe, GT_ROWBUF)
  let via: *u8 = sys_mmap(GT_AXBUF)
  let n_via: i64 = sb_read_rooted("knowledge/registry/suitebench.axes" as *u8, via, GT_AXBUF, scratch)
  g_w("  evidence root index=" as *u8); g_n(root_ok)
  g_w("  bytes via resolver=" as *u8); g_n(n_via)
  g_w("  no-such-plane resolves to=" as *u8); g_n(root_no); g_w("\n" as *u8)
  var t11: i64=0
  if root_ok>=0 { if n_via==n_ax { if root_no==(0-1) { t11=1 } } }
  g_t(t11, "T11 the portable evidence root finds the same bytes AND still answers NO for a path under no root" as *u8, fails)
185
  g_w("  fails=" as *u8); g_n(fails[0]); g_w("\n" as *u8)
  if fails[0]==0 {
      g_w("VERDICT: verdict=GREEN (11/11 -- the refusals fire, the bar is load-bearing, the corpus backs every claim, and the instrument runs wherever the evidence landed)\n" as *u8)
      sys_exit(0)
  }
  g_w("VERDICT: RED\n" as *u8)
  sys_exit(1)
  return 1
194}
nx_suitebench_gate.nx source

`nx_suitebench_gate.nx` source
