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

↩ module page · 195 lines · 9532 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"
11
12func w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
13func 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 }
14func ck(pass: i64, label: *u8, fails: *i64) -> i64 {
  w("  " as *u8); w(label); w(": " as *u8)
  if pass==1 { w("PASS\n" as *u8) } else { w("FAIL\n" as *u8); fails[0]=fails[0]+1 }
  return 0
18}
19
20// build a fully-honest record: 5 of 5 gates green, fresh, provenanced, non-vacuous, triangulated.
21// Each test below then breaks EXACTLY ONE field and asserts the verdict degrades to the named state.
22func 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
33}
34
35func main() -> i64 {
  let fails: *i64 = sys_mmap(16) as *i64
  fails[0]=0
  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
44
  w("=== nx_evidence_verdict_gate -- the evidence law refuses what it was built to refuse ===\n" as *u8)
46
  // 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)
52
  // 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)
60
  // 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)
66
  // 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)
74
  // 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)
81
  // 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)
89
  // 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)
96
  // 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)
103
  // 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)
110
  // 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)
117
  // 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)
124
  // 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)
131
  // 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)
136
  // 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)
143
  // 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)
153
  // 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)
162
  // 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)
174
  // 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)
182
  // 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)
189
  w("  fails=" as *u8); wn(fails[0]); w("\n" as *u8)
  if fails[0]==0 { w("VERDICT: verdict=GREEN (evidence law: quorum, expiry, provenance, non-vacuity, triangulation -- each negative-controlled)\n" as *u8); sys_exit(0) }
  w("VERDICT: verdict=RED\n" as *u8)
  sys_exit(1)
  return 1
195}
nx_evidence_verdict_gate.nx source

`nx_evidence_verdict_gate.nx` source
