nx_triangulate.nx source

1// nx_triangulate.nx -- REUSABLE triangulation harness: a generic ">=K of N 2// independent legs must agree with the oracle" checker the Engineer can point at 3// ANY capability (divider, codec, crypto, search ranking, ...). 4// 5// WHY this organ exists: every proof in this codebase is some variant of "run M 6// independent methods + an oracle over the same battery and assert they all 7// agree" (nx_alu_divider_newton.nx hand-rolls exactly this: leg A Newton, leg B 8// restoring, leg C `/` oracle). That pattern is the invention loop's VERIFIER 9// step (memory: triangulation = math + independent-method + oracle, three legs 10// that must agree). It was being copy-pasted per capability. This extracts it 11// (Cardinal 15 DRY: a pattern in 3+ places -> shared/) so a new capability gets 12// triangulated by FILLING IN its legs, not by re-deriving the agreement logic. 13// 14// CONTRACT (the generic checker): 15// - You supply N independent method results for one input vector (an i64[]), 16// plus the oracle value for that vector. 17// - A leg AGREES iff its result == the oracle. (The oracle is ground truth; 18// legs are independent estimators that must all land on it.) 19// - The verdict reports: how many legs agreed, which leg index FIRST diverged 20// (-1 if none), and PASS iff agree_count >= K AND agree_count == n_legs 21// (i.e. the configurable consensus floor K is met AND no leg disagreed -- 22// a divider proof wants ALL legs to agree; a fault-tolerant consensus wants 23// >=K). Both knobs are exposed so the caller picks the regime. 24// 25// DESIGN: data-driven (legs + oracle + K are parameters, no hardcoded count -- 26// Cardinal 11 no magic numbers / Cardinal 2 data-driven), single-responsibility 27// (Cardinal 9: this ONLY judges agreement; it does not produce legs or oracles), 28// and FAIL-LOUD by construction (the verdict is a value the caller asserts on a 29// known answer; nothing is silently swallowed). Pure i64, no allocation inside 30// the hot path -- the caller owns the leg buffer (Cardinal 12: trust internal 31// callers, validate at the boundary = nx_tri_check's n_legs/K range guard). 32// 33// license_tier: ORIGINAL 34 35import "nx_syscalls.nx" 36 37// A reusable verdict record for one triangulated vector. The Engineer reads 38// these fields to assert on a known answer (FAIL LOUD) and to get the actionable 39// 5W1H diagnostic (WHICH leg diverged, WHAT it said vs the oracle). 40struct NxTriVerdict { 41 n_legs: i64 // how many legs were offered 42 agree_count: i64 // how many legs == oracle 43 pass: i64 // 1 iff agree_count >= k_min AND agree_count == n_legs 44 first_bad: i64 // index of the FIRST leg that != oracle, or -1 if all agree 45 bad_value: i64 // that leg's wrong value (oracle when first_bad == -1) 46 oracle: i64 // the ground-truth value echoed back for the diagnostic 47} 48 49const NX_TRI_OK: i64 = 0 50const NX_TRI_BAD_ARGS: i64 = 1 // returned-in-pass=-1 sentinel on a boundary violation 51 52// Judge ONE input vector. legs[] holds n_legs independent method results; 53// oracle is ground truth; k_min is the consensus floor. Writes the verdict to 54// v and returns NX_TRI_OK, or 0-NX_TRI_BAD_ARGS (LOUD) on a malformed request 55// (n_legs <= 0, or k_min outside [1, n_legs]) -- a boundary check, since legs 56// and oracle come from caller code we cannot assume are well-formed. 57func nx_tri_check(legs: *i64, n_legs: i64, oracle: i64, k_min: i64, v: *NxTriVerdict) -> i64 { 58 if n_legs <= 0 { v.pass = 0 - 1; return 0 - NX_TRI_BAD_ARGS } 59 if k_min < 1 { v.pass = 0 - 1; return 0 - NX_TRI_BAD_ARGS } 60 if k_min > n_legs { v.pass = 0 - 1; return 0 - NX_TRI_BAD_ARGS } 61 62 var agree: i64 = 0 63 var first_bad: i64 = 0 - 1 64 var bad_val: i64 = oracle 65 var i: i64 = 0 66 while i < n_legs { 67 if legs[i] == oracle { 68 agree = agree + 1 69 } 70 if legs[i] != oracle { 71 if first_bad < 0 { 72 first_bad = i 73 bad_val = legs[i] 74 } 75 } 76 i = i + 1 77 } 78 79 v.n_legs = n_legs 80 v.agree_count = agree 81 v.first_bad = first_bad 82 v.bad_value = bad_val 83 v.oracle = oracle 84 // PASS = consensus floor met AND every leg landed on the oracle. The "== 85 // n_legs" arm is what makes this a divider-grade proof (one wrong leg = FAIL 86 // LOUD); the ">= k_min" arm lets a future caller relax to >=K fault tolerance 87 // by passing k_min < n_legs and reading agree_count directly. 88 var pass: i64 = 0 89 if agree >= k_min { 90 if agree == n_legs { pass = 1 } 91 } 92 v.pass = pass 93 return NX_TRI_OK 94} 95 96// Convenience: does this vector pass a STRICT all-legs-agree triangulation with 97// at least min_legs independent legs offered? This is the common case (the 98// divider proof, the codec proof): "at least 3 independent legs, ALL agree with 99// the oracle". Returns 1 (pass) / 0 (fail) / 0-NX_TRI_BAD_ARGS (LOUD bad args). 100func nx_tri_pass_strict(legs: *i64, n_legs: i64, oracle: i64, min_legs: i64, v: *NxTriVerdict) -> i64 { 101 if n_legs < min_legs { v.pass = 0 - 1; return 0 - NX_TRI_BAD_ARGS } 102 // k_min = n_legs forces unanimity; min_legs is enforced above so we know we 103 // have >= min_legs independent witnesses (the ">=3 legs agree" requirement). 104 let rc: i64 = nx_tri_check(legs, n_legs, oracle, n_legs, v) 105 if rc != NX_TRI_OK { return rc } 106 return v.pass 107} 108 109// Running tally across a whole battery of vectors -- the Engineer accumulates 110// this while sweeping inputs, then asserts total == passed (FAIL LOUD) at the 111// end, mirroring the ok/total counters in every existing proof. 112struct NxTriTally { 113 total: i64 // vectors judged 114 passed: i64 // vectors that passed 115 first_fail_v: i64 // index of the FIRST failing vector, or -1 116 first_fail_leg: i64 // which leg diverged on that vector, or -1 117 first_fail_got: i64 // what that leg said 118 first_fail_exp: i64 // what the oracle said 119} 120 121func nx_tri_tally_init(t: *NxTriTally) -> i64 { 122 t.total = 0 123 t.passed = 0 124 t.first_fail_v = 0 - 1 125 t.first_fail_leg = 0 - 1 126 t.first_fail_got = 0 127 t.first_fail_exp = 0 128 return 0 129} 130 131// Fold one verdict into the tally. vec_idx is the caller's vector counter (used 132// only to record WHERE the first failure was, for the 5W1H diagnostic). 133func nx_tri_tally_add(t: *NxTriTally, v: *NxTriVerdict, vec_idx: i64) -> i64 { 134 t.total = t.total + 1 135 if v.pass == 1 { 136 t.passed = t.passed + 1 137 } 138 if v.pass != 1 { 139 if t.first_fail_v < 0 { 140 t.first_fail_v = vec_idx 141 t.first_fail_leg = v.first_bad 142 t.first_fail_got = v.bad_value 143 t.first_fail_exp = v.oracle 144 } 145 } 146 return 0 147}