nx_bit_provenance_pipeline_test.nx source

1// nx_bit_provenance_pipeline_test.nx -- BP-2 proof: bit-provenance 2// composes through a multi-layer pipeline silicon-to-death. 3// 4// Pipeline simulated: 5// L-1 silicon: 4 input bits born (b_a / b_b / b_c / b_d) 6// L0 ISA: each input bit consumed by a load instruction 7// L3 primitive: XOR composes b_a^b_b -> b_x, b_c^b_d -> b_y 8// L3.5 ML: weighted sum composes b_x * w + b_y * (1-w) -> b_z 9// L7 browser: b_z displayed (death) 10// 11// Audit at end: zombies = 0 (every produced bit consumed somewhere). 12// 13// expect_exit: 0 14 15import "nx_bit_provenance.nx" 16 17// FNV-1a-style primitive tags (small constants standing in for 18// content-addressed primitive identifiers). 19const TAG_SILICON: i64 = 0xCAFE0000 20const TAG_LOAD: i64 = 0xC0DE0001 21const TAG_XOR: i64 = 0xC0DE0002 22const TAG_WSUM: i64 = 0xC0DE0003 23const TAG_DISPLAY: i64 = 0xC0DE0004 24 25func main() -> i64 { 26 if nx_bprov_init() != 0 { return 1 } 27 28 // ===== L-1 silicon: 4 input bits born ===== 29 let b_a: i64 = nx_bprov_alloc() 30 let b_b: i64 = nx_bprov_alloc() 31 let b_c: i64 = nx_bprov_alloc() 32 let b_d: i64 = nx_bprov_alloc() 33 34 // Silicon-side emit (no upstream, layer = L-1). 35 if nx_bprov_emit(b_a, 0, 0, NX_BPROV_L_NEG_1, TAG_SILICON) != 0 { return 10 } 36 if nx_bprov_emit(b_b, 0, 0, NX_BPROV_L_NEG_1, TAG_SILICON) != 0 { return 11 } 37 if nx_bprov_emit(b_c, 0, 0, NX_BPROV_L_NEG_1, TAG_SILICON) != 0 { return 12 } 38 if nx_bprov_emit(b_d, 0, 0, NX_BPROV_L_NEG_1, TAG_SILICON) != 0 { return 13 } 39 40 // ===== L0 ISA: each input loaded by a load instr ===== 41 if nx_bprov_join(b_a, NX_BPROV_L_0, TAG_LOAD) != 0 { return 20 } 42 if nx_bprov_join(b_b, NX_BPROV_L_0, TAG_LOAD) != 0 { return 21 } 43 if nx_bprov_join(b_c, NX_BPROV_L_0, TAG_LOAD) != 0 { return 22 } 44 if nx_bprov_join(b_d, NX_BPROV_L_0, TAG_LOAD) != 0 { return 23 } 45 46 // ===== L3 primitive: XOR composes ===== 47 let b_x: i64 = nx_bprov_alloc() 48 if nx_bprov_emit(b_x, b_a, b_b, NX_BPROV_L_3, TAG_XOR) != 0 { return 30 } 49 let b_y: i64 = nx_bprov_alloc() 50 if nx_bprov_emit(b_y, b_c, b_d, NX_BPROV_L_3, TAG_XOR) != 0 { return 31 } 51 52 // ===== L3.5 ML: weighted sum (3-source emit) ===== 53 let b_z: i64 = nx_bprov_alloc() 54 // For provenance purposes b_z derives from (b_x, b_y, and a weight constant). 55 // The weight constant is represented as bit ID 0 (silicon-immutable). 56 if nx_bprov_emit3(b_z, b_x, b_y, 0, NX_BPROV_L_35, TAG_WSUM) != 0 { return 40 } 57 58 // Mid-pipeline audit: all intermediate bits are still zombies 59 // until L7 joins b_z. Zombies: b_x, b_y, b_z = 3. 60 if nx_bprov_audit_zombies() != 3 { return 50 } 61 62 // ===== L7 browser: b_z displayed (death) ===== 63 if nx_bprov_join(b_z, NX_BPROV_L_7, TAG_DISPLAY) != 0 { return 60 } 64 65 // ===== Audit: every bit alive in the chain has been observed ===== 66 // Final state: 67 // b_a/b/c/d: produced L-1, joined L0 -> alive 68 // b_x/b_y: produced L3 from a/b and c/d -> zombies (no one consumed) 69 // b_z: produced L3.5 from x/y, joined L7 -> alive 70 // 71 // Zombies count = 2 (b_x, b_y) -- they were intermediate, never 72 // observed by a downstream consumer. In a fully-traced 73 // substrate, we'd expect either (a) L3 primitive INTERNALLY 74 // calls join on intermediates before returning, OR (b) audit 75 // rules consider an intermediate's join implied by the 76 // emit-chain pointing through it. V0 uses rule (a): we 77 // explicitly join b_x and b_y at the L3.5 layer where they 78 // were consumed. 79 if nx_bprov_join(b_x, NX_BPROV_L_35, TAG_WSUM) != 0 { return 70 } 80 if nx_bprov_join(b_y, NX_BPROV_L_35, TAG_WSUM) != 0 { return 71 } 81 82 if nx_bprov_audit_zombies() != 0 { return 80 } 83 84 // Verify lookup_join returns the consumer layer for each bit. 85 if nx_bprov_lookup_join(b_a) != NX_BPROV_L_0 { return 90 } 86 if nx_bprov_lookup_join(b_b) != NX_BPROV_L_0 { return 91 } 87 if nx_bprov_lookup_join(b_c) != NX_BPROV_L_0 { return 92 } 88 if nx_bprov_lookup_join(b_d) != NX_BPROV_L_0 { return 93 } 89 if nx_bprov_lookup_join(b_x) != NX_BPROV_L_35 { return 94 } 90 if nx_bprov_lookup_join(b_y) != NX_BPROV_L_35 { return 95 } 91 if nx_bprov_lookup_join(b_z) != NX_BPROV_L_7 { return 96 } 92 93 // Total records: 4 silicon + 2 L3 XOR + 1 L3.5 WSUM = 7. 94 if nx_bprov_n_records() != 7 { return 100 } 95 96 return 0 97}