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

↩ module page · 248 lines · 12823 B
1// nx_evidence_verdict_gate.nx -- proves the shared evidence law (nx_evidence_verdict.nx) REFUSES every
2// defect it was built to kill, and still passes an honestly-earned claim.
3//
4// This gate is written to its own rule 4 (NON-VACUITY): every clause below has a NEGATIVE CONTROL that
5// makes it fire. A gate that only ever demonstrates PASS has measured nothing -- that is precisely the
6// defect this library outlaws, so this gate must not commit it. T1 is the real, measured production
7// regression, replayed as a test: it is the exact medbilling evidence record from 2026-07-30.
8// license_tier: ORIGINAL  expect_exit: 0
9import "nx_syscalls.nx"
10import "nx_evidence_verdict.nx"
11import "nx_gate_verdict.nx"
12
13// D001 MIGRATION 2026-08-26: the verdict now comes from the shared base class, so this gate's outcome is
14// readable FROM OUTSIDE via its exit code (/api/gate_run) and it records a harness frame -- previously it
15// printed a perfect verdict line that nothing could consume. The hand-rolled fails[] counter survives only
16// to feed the legacy `fails=` line, which is this gate's public signature; gv_ctr is now the canonical
17// count, so a tooth that silently stops running can no longer read GREEN.
18// The counter is reached through file-scope state rather than a new ck() parameter on purpose: ck has 22
19// call sites, and a signature change is 22 chances to mistype a migration whose entire value is being
20// behaviour-neutral.
21static evg_ctr: i64
22
23func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
24func wn(v: i64) -> i64 { let t: *u8=sys_mmap(28); var m: i64=v; 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} let b: *u8=sys_mmap(28); var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
25func ck(pass: i64, label: *u8, fails: *i64) -> i64 {
  // gv_check emits the IDENTICAL `  <label>: PASS|FAIL` line, so ck no longer prints its own -- the first
  // cut of this migration emitted every tooth TWICE. fails[] is still tallied here because the legacy
  // `fails=` line is this gate's public signature and readers key on it.
  if pass==0 { fails[0]=fails[0]+1 }
  gv_check(label, pass, evg_ctr as *i64)
  return 0
32}
33
34// build a fully-honest record: 5 of 5 gates green, fresh, provenanced, non-vacuous, triangulated.
35// Each test below then breaks EXACTLY ONE field and asserts the verdict degrades to the named state.
36func ev_seed_good(r: *i64, now: i64) -> i64 {
  r[EV_R_GREEN] = 5
  r[EV_R_RAN] = 5
  r[EV_R_DECLARED] = 5
  r[EV_R_EPOCH] = now - 60
  r[EV_R_HOSTLEN] = 12
  r[EV_R_DIGLEN] = 64
  r[EV_R_REDSEEN] = 5
  r[EV_R_CLASSMASK] = EV_CLASS_MECH + EV_CLASS_HUMAN
  r[EV_R_DISSENT] = 0
  return 0
47}
48
49func main() -> i64 {
  let fails: *i64 = sys_mmap(16) as *i64
  fails[0]=0
  evg_ctr = gv_ctr() as i64
  let now: i64 = 1785433876
  let r: *i64 = sys_mmap(EV_R_SLOTS*8) as *i64
  let p: *i64 = sys_mmap(EV_P_SLOTS*8) as *i64
  p[EV_P_TTL] = 604800
  p[EV_P_MINCLASSES] = 2
  p[EV_P_REQHUMAN] = 0
59
  w("=== nx_evidence_verdict_gate -- the evidence law refuses what it was built to refuse ===\n" as *u8)
61
  // T0: the honest record PASSES. Without this the gate could refuse everything and look strict.
  ev_seed_good(r, now)
  var t0: i64=0
  if ev_verdict(r, p, now)==EV_PROVEN { t0=1 }
  ck(t0, "T0 fully-earned claim -> PROVEN (the law is accurate, not merely strict)" as *u8, fails)
67
  // T1: THE MEASURED PRODUCTION REGRESSION, replayed. medbilling 2026-07-30: 5 gates declared, the old
  // rule `liar_green = (green >= 1)` stamped ok=1 on a single green gate. Under the law: RED.
  ev_seed_good(r, now)
  r[EV_R_GREEN] = 1
  var t1: i64=0
  if ev_verdict(r, p, now)==EV_RED { t1=1 }
  ck(t1, "T1 REGRESSION 1-of-5 gates green (the live medbilling record) -> RED, was PROVEN" as *u8, fails)
75
  // T1b: the old rule, stated directly, to show this gate discriminates. `green>=1` accepts the very
  // record the law rejects -- so T1 is a real behaviour change, not a restatement.
  var t1b: i64=0
  if (r[EV_R_GREEN] >= 1) == 1 { if ev_verdict(r, p, now) != EV_PROVEN { t1b=1 } }
  ck(t1b, "T1b NEG-CONTROL: old rule green>=1 accepts this record; the law rejects it" as *u8, fails)
81
  // T2: a gate that did not RUN cannot be counted. declared 5, ran 4, all 4 green -> RED, not 4/4 PROVEN.
  ev_seed_good(r, now)
  r[EV_R_RAN] = 4
  r[EV_R_GREEN] = 4
  var t2: i64=0
  if ev_verdict(r, p, now)==EV_RED { t2=1 }
  ck(t2, "T2 a declared gate that never ran -> RED (cannot shrink its own denominator)" as *u8, fails)
89
  // T3: EXPIRY. The measured 13.7-day-old stamp (1183616s) against a 7-day TTL -> STALE, not PROVEN.
  ev_seed_good(r, now)
  r[EV_R_EPOCH] = now - 1183616
  var t3: i64=0
  if ev_verdict(r, p, now)==EV_STALE { t3=1 }
  ck(t3, "T3 the live 1183616s-old stamp vs 7d TTL -> STALE (a verdict has an expiry)" as *u8, fails)
96
  // T4: PROVENANCE. A v1 stamp carrying no host and no digest fails CLOSED -- no grandfathering.
  ev_seed_good(r, now)
  r[EV_R_HOSTLEN] = 0
  r[EV_R_DIGLEN] = 0
  var t4: i64=0
  if ev_verdict(r, p, now)==EV_UNPROVEN { t4=1 }
  ck(t4, "T4 legacy stamp with no host/digest -> UNPROVEN (fails closed, not grandfathered)" as *u8, fails)
104
  // T5: NON-VACUITY. Gates that have never been observed RED have not been shown to measure anything.
  ev_seed_good(r, now)
  r[EV_R_REDSEEN] = 0
  var t5: i64=0
  if ev_verdict(r, p, now)==EV_VACUOUS { t5=1 }
  ck(t5, "T5 gates never observed failing -> VACUOUS (coverage is not detection)" as *u8, fails)
111
  // T5b: PARTIAL non-vacuity is still vacuity -- 4 of 5 proven-able-to-fail leaves one permanently green.
  ev_seed_good(r, now)
  r[EV_R_REDSEEN] = 4
  var t5b: i64=0
  if ev_verdict(r, p, now)==EV_VACUOUS { t5b=1 }
  ck(t5b, "T5b 4-of-5 gates proven able to fail -> still VACUOUS" as *u8, fails)
118
  // T6: AN LLM MAY NOT CONVICT. Model judgment alone, however confident, cannot reach PROVEN.
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_LLM
  var t6: i64=0
  if ev_verdict(r, p, now)==EV_UNPROVEN { t6=1 }
  ck(t6, "T6 LLM-only evidence -> UNPROVEN (a model corroborates, it never convicts)" as *u8, fails)
125
  // T6b: LLM + HUMAN, two classes but NO mechanistic leg, is still not proof.
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_LLM + EV_CLASS_HUMAN
  var t6b: i64=0
  if ev_verdict(r, p, now)==EV_UNPROVEN { t6b=1 }
  ck(t6b, "T6b LLM+human with no mechanistic leg -> UNPROVEN (>=1 leg must be mechanistic)" as *u8, fails)
132
  // T7: A SINGLE mechanistic method is one measurement, not a triangulation.
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_MECH
  var t7: i64=0
  if ev_verdict(r, p, now)==EV_UNPROVEN { t7=1 }
  ck(t7, "T7 mechanistic alone -> UNPROVEN (one method is a measurement, not a triangulation)" as *u8, fails)
139
  // T8: DISAGREEMENT IS NOT AVERAGED. An independent method reporting FAIL is RED, outranking all else.
  ev_seed_good(r, now)
  r[EV_R_DISSENT] = EV_CLASS_HUMAN
  var t8: i64=0
  if ev_verdict(r, p, now)==EV_RED { t8=1 }
  ck(t8, "T8 a dissenting method on an otherwise-perfect record -> RED (never averaged)" as *u8, fails)
146
  // T9: the honesty ratio keeps an honest denominator -- 10 PROVEN of 40 domains is 250, not 1000.
  var t9: i64=0
  if ev_honesty_permil(10, 40)==250 { t9=1 }
  ck(t9, "T9 honesty ratio 10 of 40 domains = 250 permil (the live measured number)" as *u8, fails)
151
  // T10: clock skew (a stamp from the future) is refused, not treated as maximally fresh.
  ev_seed_good(r, now)
  r[EV_R_EPOCH] = now + 3600
  var t10: i64=0
  if ev_verdict(r, p, now)==EV_STALE { t10=1 }
  ck(t10, "T10 stamp dated in the future -> STALE (skew is refused, not trusted)" as *u8, fails)
158
  // T11: a domain declaring ZERO gates does not pass on an empty conjunction -- but it is UNPROVEN, not
  // RED. Nothing ran, so nothing failed. RED is reserved for a method that reported failure.
  ev_seed_good(r, now)
  r[EV_R_DECLARED] = 0
  r[EV_R_RAN] = 0
  r[EV_R_GREEN] = 0
  var t11: i64=0
  if ev_verdict(r, p, now)==EV_UNPROVEN { t11=1 }
  ck(t11, "T11 zero declared gates -> UNPROVEN (nothing ran, so nothing failed)" as *u8, fails)
168
  // T11b: RED and UNPROVEN must be DISTINGUISHABLE, not merely both non-PROVEN. A domain whose gate ran
  // and failed, and a domain with no gate at all, are different problems needing different work.
  let rb: *i64 = sys_mmap(EV_R_SLOTS*8) as *i64
  ev_seed_good(rb, now)
  rb[EV_R_GREEN] = 2
  var t11b: i64=0
  if ev_verdict(rb, p, now)==EV_RED { if ev_verdict(r, p, now)==EV_UNPROVEN { t11b=1 } }
  ck(t11b, "T11b a failed gate reads RED while a missing gate reads UNPROVEN (distinct diagnoses)" as *u8, fails)
177
  // T11c/d/e: AN ABSTENTION IS NOT A DISSENT (2026-08-26). A gate that exits SKIP because a PRECONDITION
  // was absent examined nothing, and this function's own doctrine says that is UNPROVEN territory, never
  // RED. Counting it in the quorum convicted a live domain of failures nobody measured and blocked a
  // deploy on gates whose own output says they must never do so.
  // T11c and T11d are the DISCRIMINATING PAIR: the two records are identical in every field except
  // skipped, so an implementation that ignores that field cannot pass both -- which is the only thing
  // that distinguishes this law from a blanket weakening of the quorum.
  let rsk: *i64 = sys_mmap(EV_R_SLOTS*8) as *i64
  ev_seed_good(rsk, now)
  rsk[EV_R_DECLARED] = 3
  rsk[EV_R_RAN] = 3
  rsk[EV_R_GREEN] = 1
  rsk[EV_R_SKIPPED] = 2
  var t11c: i64=0
  if ev_verdict(rsk, p, now)!=EV_RED { t11c=1 }
  ck(t11c, "T11c 1 green + 2 ABSTAINED of 3 -> not RED (an abstention is not a dissent)" as *u8, fails)
194
  let rns: *i64 = sys_mmap(EV_R_SLOTS*8) as *i64
  ev_seed_good(rns, now)
  rns[EV_R_DECLARED] = 3
  rns[EV_R_RAN] = 3
  rns[EV_R_GREEN] = 1
  rns[EV_R_SKIPPED] = 0
  var t11d: i64=0
  if ev_verdict(rns, p, now)==EV_RED { t11d=1 }
  ck(t11d, "T11d neg-control-identical-record-without-the-abstention: 1 green of 3 -> RED (real dissent still convicts)" as *u8, fails)
204
  let rall: *i64 = sys_mmap(EV_R_SLOTS*8) as *i64
  ev_seed_good(rall, now)
  rall[EV_R_DECLARED] = 3
  rall[EV_R_RAN] = 3
  rall[EV_R_GREEN] = 0
  rall[EV_R_SKIPPED] = 3
  var t11e: i64=0
  if ev_verdict(rall, p, now)==EV_UNPROVEN { t11e=1 }
  ck(t11e, "T11e neg-control-every-gate-abstained -> UNPROVEN: unobserved is never promotable to proven" as *u8, fails)
214
  // T12: THE HUMAN LEG CANNOT BE SELF-GRANTED. With require_human on, mechanistic + model agreement is
  // still not proof -- one agent can produce both in a single session, which is one opinion in two hats.
  let ph: *i64 = sys_mmap(EV_P_SLOTS*8) as *i64
  ph[EV_P_TTL] = 604800
  ph[EV_P_MINCLASSES] = 2
  ph[EV_P_REQHUMAN] = 1
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_MECH + EV_CLASS_LLM
  var t12: i64=0
  if ev_verdict(r, ph, now)==EV_UNPROVEN { t12=1 }
  ck(t12, "T12 mech+LLM under require_human -> UNPROVEN (an agent cannot certify its own work)" as *u8, fails)
226
  // T12b: add the human row and the same record earns PROVEN -- the clause gates on the missing leg, it
  // does not simply refuse everything.
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_MECH + EV_CLASS_LLM + EV_CLASS_HUMAN
  var t12b: i64=0
  if ev_verdict(r, ph, now)==EV_PROVEN { t12b=1 }
  ck(t12b, "T12b mech+LLM+human -> PROVEN (the third leg is what closes it)" as *u8, fails)
234
  // T12c: the human leg does NOT excuse a missing mechanistic leg. Human+LLM is still two opinions.
  ev_seed_good(r, now)
  r[EV_R_CLASSMASK] = EV_CLASS_HUMAN + EV_CLASS_LLM
  var t12c: i64=0
  if ev_verdict(r, ph, now)==EV_UNPROVEN { t12c=1 }
  ck(t12c, "T12c human+LLM without a mechanistic leg -> UNPROVEN (opinions are not measurements)" as *u8, fails)
241
  w("  fails=" as *u8); wn(fails[0]); w("\n" as *u8)
  // The rich domain line is KEPT and the canonical verdict is APPENDED after it, never instead of it:
  // the shared judge anchors on the LAST line by position, so both readers are served and neither has to
  // learn a second spelling of success.
  if fails[0]==0 { w("VERDICT: verdict=GREEN (evidence law: quorum, expiry, provenance, non-vacuity, triangulation -- each negative-controlled)\n" as *u8) } else { w("VERDICT: verdict=RED\n" as *u8) }
  return gv_verdict("evidence_law" as *u8, evg_ctr as *i64, "every clause of the shared evidence law negative-controlled, including that an ABSTENTION is not a dissent and that all-abstained is UNPROVEN rather than RED" as *u8)
248}
nx_evidence_verdict_gate.nx source

`nx_evidence_verdict_gate.nx` source
