nx_boolsynth_test.nx source

1// nx_boolsynth_test.nx -- prove the new BOOLEAN search space finds the PROVABLY-MINIMAL 2// circuit for 3-input functions, verified EXACTLY (the truth-table byte covers all 8 inputs). 3// Targets: majority 0xE8, parity 0x96, mux a?b:c 0xD8, and an arbitrary 0x69. For each it 4// finds the shortest circuit over {and,or,xor,not} and RE-EVALUATES it to confirm the output 5// truth table equals the target. Known answer: every one solved + re-verified -> exit 0. 6 7import "nx_boolsynth.nx" 8 9func bt_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 10func bt_num(v: i64) -> i64 { 11 let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 12 let t: *u8 = sys_mmap(28); var k: i64 = 0 13 if m == 0 { t[0] = 48; k = 1 } 14 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 15 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 16 sys_write(1, bb, k); return 0 17} 18func tally(r: *i64, n: i64) -> i64 { var ec: i64 = 0; var i: i64 = 0; while i < n { if r[i] != 1 { if ec == 0 { ec = i + 1 } } i = i + 1 } return ec } 19 20// re-evaluate a found circuit on the magic columns -> its truth-table byte (exhaustive check). 21func bt_reeval(op: *i64, a: *i64, b: *i64, L: i64) -> i64 { 22 let sv: *i64 = sys_mmap(8 * (L + 6)) as *i64 23 sv[0] = BL_A; sv[1] = BL_B; sv[2] = BL_C 24 var t: i64 = 0 25 while t < L { sv[t + 3] = bl_eval(op[t], sv[a[t]], sv[b[t]]); t = t + 1 } 26 return sv[L + 2] & 255 27} 28 29// slot name for printing: a/b/c or t<n> 30func bt_slot(s: i64) -> i64 { 31 if s == 0 { bt_puts("a" as *u8) } else { if s == 1 { bt_puts("b" as *u8) } else { if s == 2 { bt_puts("c" as *u8) } else { bt_puts("t" as *u8); bt_num(s - 3) } } } 32 return 0 33} 34 35func bt_one(target: i64, label: *u8, r: *i64, slot: i64) -> i64 { 36 let op: *i64 = sys_mmap(8 * 12) as *i64 37 let a: *i64 = sys_mmap(8 * 12) as *i64 38 let b: *i64 = sys_mmap(8 * 12) as *i64 39 let L: i64 = bl_find(target, op, a, b, 6) 40 let chk: i64 = bt_reeval(op, a, b, L) 41 bt_puts(" " as *u8); bt_puts(label); bt_puts(" (tt=" as *u8); bt_num(target); bt_puts("): " as *u8); bt_num(L); bt_puts(" ops [ " as *u8) 42 var t: i64 = 0 43 while t < L { 44 bt_puts("t" as *u8); bt_num(t); bt_puts("=" as *u8); bt_puts(bl_opname(op[t])); bt_puts("(" as *u8); bt_slot(a[t]) 45 if bl_is_unary(op[t]) == 0 { bt_puts("," as *u8); bt_slot(b[t]) } 46 bt_puts(") " as *u8) 47 t = t + 1 48 } 49 bt_puts("] reverify=" as *u8); if chk == target { bt_puts("OK\n" as *u8) } else { bt_puts("MISMATCH\n" as *u8) } 50 r[slot] = 0; if L > 0 { if chk == target { r[slot] = 1 } } 51 return 0 52} 53 54func bt_main(r: *i64) -> i64 { 55 bt_puts("=== BOOLEAN SEARCH SPACE: provably-minimal 3-input circuits, exact verification (truth-table) ===\n" as *u8) 56 bt_one(232, "majority " as *u8, r, 0) // 0xE8 57 bt_one(150, "parity " as *u8, r, 1) // 0x96 58 bt_one(216, "mux a?b:c" as *u8, r, 2) // 0xD8 59 bt_one(105, "arbitrary" as *u8, r, 3) // 0x69 60 bt_puts("----------------------------------------------------------------\n" as *u8) 61 bt_puts(" the team found the FLOOR for each function -- the class where exhaustive search can beat a heuristic compiler.\n" as *u8) 62 return 4 63} 64 65func main() -> i64 { 66 let r: *i64 = sys_mmap(8 * 8) as *i64 67 let n: i64 = bt_main(r) 68 let ec: i64 = tally(r, n) 69 sys_exit(ec) 70 return ec 71}