nx_numeric_oracle_test.nx source

1// nx_numeric_oracle_test.nx -- verify the verifier. 2// 3// The oracle is the tool every future kernel passes through. If the 4// oracle is buggy, every "verified" claim downstream is suspect. So 5// we test it harder than a normal smoke -- positive + negative paths, 6// witness extraction, all 6 verdicts, metamorphic invariants. 7 8import "nx_syscalls.nx" 9import "nx_tier.nx" 10import "nx_prng.nx" 11import "nx_tensor.nx" 12import "nx_numeric_oracle.nx" 13 14func main() -> nx_int { 15 let err: *i64 = (sys_mmap(8)) as *i64 16 let witness: *i64 = (sys_mmap(NX_NO_WITNESS_FIELDS * 8)) as *i64 17 18 // ===== Build two identical i64 3x4 tensors =================== 19 let shape: *i64 = (sys_mmap(16)) as *i64 20 shape[0] = 3; shape[1] = 4 21 22 let ta: *NxTensor = nx_t_alloc(NX_DT_I64, shape, 2, err) 23 let tb: *NxTensor = nx_t_alloc(NX_DT_I64, shape, 2, err) 24 nx_t_fill_zero(ta) 25 nx_t_fill_zero(tb) 26 27 let idx: *i64 = (sys_mmap(64)) as *i64 28 idx[0] = 0; idx[1] = 0; nx_t_set_i64(ta, idx, 42); nx_t_set_i64(tb, idx, 42) 29 idx[0] = 1; idx[1] = 2; nx_t_set_i64(ta, idx, 99); nx_t_set_i64(tb, idx, 99) 30 idx[0] = 2; idx[1] = 3; nx_t_set_i64(ta, idx, 1000); nx_t_set_i64(tb, idx, 1000) 31 32 // ===== BIT_EXACT: identical tensors -> EQUAL ================= 33 let v1: nx_int = nx_no_check_bit_exact_i64(ta, tb, witness) 34 if v1 != NX_NO_VERDICT_EQUAL { return 1 } 35 36 // ===== BIT_EXACT: mutate one cell -> DIFFERS + witness ======= 37 idx[0] = 1; idx[1] = 2; nx_t_set_i64(tb, idx, 100) 38 let v2: nx_int = nx_no_check_bit_exact_i64(ta, tb, witness) 39 if v2 != NX_NO_VERDICT_DIFFERS { return 2 } 40 // Witness should have row=1, col=2, actual=99, expected=100 41 if witness[NX_NO_WITNESS_F_IDX0] != 1 { return 3 } 42 if witness[NX_NO_WITNESS_F_IDX1] != 2 { return 4 } 43 if witness[NX_NO_WITNESS_F_ACTUAL] != 99 { return 5 } 44 if witness[NX_NO_WITNESS_F_EXPECTED] != 100 { return 6 } 45 if witness[NX_NO_WITNESS_F_ABS_DIFF] != 1 { return 7 } 46 // Repair 47 idx[0] = 1; idx[1] = 2; nx_t_set_i64(tb, idx, 99) 48 49 // ===== Shape mismatch -> SHAPE_MISMATCH ===================== 50 let shape3: *i64 = (sys_mmap(16)) as *i64 51 shape3[0] = 4; shape3[1] = 4 52 let tc: *NxTensor = nx_t_alloc(NX_DT_I64, shape3, 2, err) 53 let v3: nx_int = nx_no_check_bit_exact_i64(ta, tc, witness) 54 if v3 != NX_NO_VERDICT_SHAPE_MISMATCH { return 10 } 55 56 // ===== Ndim mismatch -> SHAPE_MISMATCH ====================== 57 shape3[0] = 12 58 let td: *NxTensor = nx_t_alloc(NX_DT_I64, shape3, 1, err) 59 let v4: nx_int = nx_no_check_bit_exact_i64(ta, td, witness) 60 if v4 != NX_NO_VERDICT_SHAPE_MISMATCH { return 11 } 61 62 // ===== Structural-only check ================================ 63 let v5: nx_int = nx_no_check_structural(ta, tb) 64 if v5 != NX_NO_VERDICT_EQUAL { return 12 } 65 let v6: nx_int = nx_no_check_structural(ta, tc) 66 if v6 != NX_NO_VERDICT_SHAPE_MISMATCH { return 13 } 67 68 // ===== EPSILON_REL with eps=0 acts like bit-exact =========== 69 let v7: nx_int = nx_no_check_epsilon_rel_q10(ta, tb, 0, witness) 70 if v7 != NX_NO_VERDICT_EQUAL { return 20 } 71 72 // Differ by 1 unit, eps_q10 = 0 -> DIFFERS 73 idx[0] = 0; idx[1] = 0; nx_t_set_i64(tb, idx, 43) 74 let v8: nx_int = nx_no_check_epsilon_rel_q10(ta, tb, 0, witness) 75 if v8 != NX_NO_VERDICT_DIFFERS { return 21 } 76 77 // Same delta, eps_q10 = 51 (5% relative) -> EQUAL since 78 // 1 <= 0.05 * 43 = 2 (after Q10 math floors). 79 // Actually 51 * 43 / 1024 = 2; |42 - 43| = 1 <= 2 -> EQUAL. 80 let v9: nx_int = nx_no_check_epsilon_rel_q10(ta, tb, 51, witness) 81 if v9 != NX_NO_VERDICT_EQUAL { return 22 } 82 // Repair 83 idx[0] = 0; idx[1] = 0; nx_t_set_i64(tb, idx, 42) 84 85 // ===== Property-based generator ============================== 86 let prng: *i64 = (sys_mmap(8)) as *i64 87 nx_prng_init(prng, 12345) 88 let gen_t: *NxTensor = nx_no_gen_random_i64(shape, 2, 89 0 - 50, 50, prng, err) 90 if (gen_t as nx_int) == 0 { return 30 } 91 if gen_t.numel != 12 { return 31 } 92 // Spot-check: every element should be in [-50, 50) 93 let pg: *i64 = gen_t.storage as *i64 94 var k: nx_int = 0 95 while k < gen_t.numel { 96 if pg[k] < 0 - 50 { return 32 } 97 if pg[k] >= 50 { return 33 } 98 k = k + 1 99 } 100 101 // Same seed -> reproducible: generate again and check identical 102 nx_prng_init(prng, 12345) 103 let gen_t2: *NxTensor = nx_no_gen_random_i64(shape, 2, 104 0 - 50, 50, prng, err) 105 let v10: nx_int = nx_no_check_bit_exact_i64(gen_t, gen_t2, witness) 106 if v10 != NX_NO_VERDICT_EQUAL { return 34 } // reproducibility holds 107 108 // ===== Metamorphic: double-transpose identity =============== 109 // 110 // permute reverse twice should land you back at the original 111 // logical indexing. Build a 2x3 tensor with marker values. 112 let mshape: *i64 = (sys_mmap(16)) as *i64 113 mshape[0] = 2; mshape[1] = 3 114 let tm: *NxTensor = nx_t_alloc(NX_DT_I64, mshape, 2, err) 115 idx[0] = 0; idx[1] = 0; nx_t_set_i64(tm, idx, 1) 116 idx[0] = 0; idx[1] = 1; nx_t_set_i64(tm, idx, 2) 117 idx[0] = 0; idx[1] = 2; nx_t_set_i64(tm, idx, 3) 118 idx[0] = 1; idx[1] = 0; nx_t_set_i64(tm, idx, 4) 119 idx[0] = 1; idx[1] = 1; nx_t_set_i64(tm, idx, 5) 120 idx[0] = 1; idx[1] = 2; nx_t_set_i64(tm, idx, 6) 121 122 let v11: nx_int = nx_no_check_double_transpose_id(tm, witness) 123 if v11 != NX_NO_VERDICT_EQUAL { return 40 } 124 125 // ===== Differential verdict routing ======================== 126 let v12: nx_int = nx_no_differential_verdict(ta, tb, 127 NX_NO_CMP_BIT_EXACT, 128 0, witness) 129 if v12 != NX_NO_VERDICT_EQUAL { return 50 } 130 131 let v13: nx_int = nx_no_differential_verdict(ta, tc, 132 NX_NO_CMP_STRUCTURAL, 133 0, witness) 134 if v13 != NX_NO_VERDICT_SHAPE_MISMATCH { return 51 } 135 136 // ===== Kahan sum (i64 = plain sum for v1) ================== 137 let vals: *i64 = (sys_mmap(40)) as *i64 138 vals[0] = 1; vals[1] = 2; vals[2] = 3; vals[3] = 4; vals[4] = 5 139 if nx_no_kahan_sum_i64(vals, 5) != 15 { return 60 } 140 141 // ===== Reproducibility check (hash bytes) ================== 142 let h1: *u8 = sys_mmap(32) 143 let h2: *u8 = sys_mmap(32) 144 var i: nx_int = 0 145 while i < 32 { 146 h1[i] = i 147 h2[i] = i 148 i = i + 1 149 } 150 if nx_no_check_reproducible(h1, h2, 32) != NX_NO_VERDICT_EQUAL { return 70 } 151 h2[5] = 99 152 if nx_no_check_reproducible(h1, h2, 32) != NX_NO_VERDICT_DIFFERS { return 71 } 153 154 // ===== Enum validity ======================================= 155 if nx_no_cmp_kind_is_valid(NX_NO_CMP_BIT_EXACT) != 1 { return 80 } 156 if nx_no_cmp_kind_is_valid(NX_NO_CMP_N_KINDS) != 0 { return 81 } 157 if nx_no_verdict_is_valid(NX_NO_VERDICT_EQUAL) != 1 { return 82 } 158 if nx_no_verdict_is_valid(NX_NO_VERDICT_N_KINDS) != 0 { return 83 } 159 160 return 0 161}