nx_horizontal_test.nx source

1// nx_horizontal_test.nx -- the team's find-minimal-verify loop runs HORIZONTAL, across many 2// DISTINCT functionalities, not just one vertical codegen path. The same engine handles a 3// spread of functional domains, each synthesized + verified by the team: 4// ARITHMETIC mul -- multiply-by-constant (machine code, exec-verified) 5// ARITHMETIC add -- an N-bit adder composed from synthesized gates (verified to add) 6// LOGIC -- majority (exact-verified) 7// CHECKSUM -- parity / odd-ones (exact-verified) 8// SELECT/CONTROL -- mux a?b:c (exact-verified) 9// Combined with the vertical level-8->0 stack, this is the team improving across the whole 10// 2D grid: up the sovereign stack AND across functionalities. 11 12import "nx_mulchain.nx" 13import "nx_superopt_emit.nx" 14import "nx_engineer_crash.nx" 15import "nx_boolsynth.nx" 16 17func hz_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 18func hz_num(v: i64) -> i64 { 19 let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m } 20 let t: *u8 = sys_mmap(28); var k: i64 = 0 21 if m == 0 { t[0] = 48; k = 1 } 22 while m > 0 { t[k] = 48 + (m % 10); m = m / 10; k = k + 1 } 23 var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } 24 sys_write(1, bb, k); return 0 25} 26func 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 } 27func hz_bwrite(path: *u8, buf: *u8, len: i64) -> i64 { let fd: i64 = sys_openat_wr(path, 0x1a4); if fd < 0 { return 0 - 1 } sys_write(fd, buf, len); sys_close(fd); return 0 } 28func hz_booleval(op: *i64, a: *i64, b: *i64, L: i64) -> i64 { 29 let sv: *i64 = sys_mmap(8 * (L + 6)) as *i64 30 sv[0]=BL_A; sv[1]=BL_B; sv[2]=BL_C 31 var t: i64 = 0; while t < L { sv[t+3] = bl_eval(op[t], sv[a[t]], sv[b[t]]); t = t+1 } return sv[L+2] & 255 32} 33func hz_eval1(op: *i64, a: *i64, b: *i64, L: i64, x0: i64, x1: i64, x2: i64) -> i64 { 34 let sv: *i64 = sys_mmap(8 * (L + 6)) as *i64 35 sv[0]=x0; sv[1]=x1; sv[2]=x2 36 var t: i64 = 0; while t < L { sv[t+3] = bl_eval(op[t], sv[a[t]], sv[b[t]]); t = t+1 } return sv[L+2] & 1 37} 38 39// FUNCTIONALITY 1: multiply-by-constant codegen, verified by execution. 40func hz_mul(label: *u8) -> i64 { 41 let op: *i64 = sys_mmap(8*12) as *i64; let a: *i64 = sys_mmap(8*12) as *i64; let b: *i64 = sys_mmap(8*12) as *i64 42 let dd: *i64 = sys_mmap(8*16) as *i64; let buf: *u8 = sys_mmap(8192); let icnt: *i64 = sys_mmap(8) as *i64 43 dd[0]=5; dd[1]=0-8; dd[2]=123; dd[3]=0-456; dd[4]=77; dd[5]=0-1; dd[6]=1000; dd[7]=0-1000 44 var ref: i64 = 0; var kk: i64 = 0; while kk < 8 { ref = ref + dd[kk]*45; kk = kk+1 }; ref = ref & 255 45 let L: i64 = mulchain_find(45, 8, op, a, b) 46 let blen: i64 = se_emit_full(op, a, b, L, dd, 8, buf, icnt) 47 hz_bwrite("/tmp/hz.s" as *u8, buf, blen) 48 var ok: i64 = 0 49 if eng_link("/tmp/hz.s" as *u8, "/tmp/hz.elf" as *u8) == 0 { if eng_run("/tmp/hz.elf" as *u8, 0 as *u8) == ref { ok = 1 } } 50 hz_puts(label); hz_puts(": x*45 in " as *u8); hz_num(icnt[0]); hz_puts(" insns, exec-verified " as *u8); if ok==1 {hz_puts("OK\n" as *u8)} else {hz_puts("FAIL\n" as *u8)} 51 return ok 52} 53 54// FUNCTIONALITY 2: an N-bit adder composed from synthesized sum/carry gates, verified. 55func hz_add(label: *u8) -> i64 { 56 let so: *i64 = sys_mmap(8*12) as *i64; let sa: *i64 = sys_mmap(8*12) as *i64; let sb: *i64 = sys_mmap(8*12) as *i64 57 let co: *i64 = sys_mmap(8*12) as *i64; let ca: *i64 = sys_mmap(8*12) as *i64; let cb: *i64 = sys_mmap(8*12) as *i64 58 let sL: i64 = bl_find(150, so, sa, sb, 6) 59 let cL: i64 = bl_find(232, co, ca, cb, 6) 60 let mask: i64 = 255 61 var bad: i64 = 0 62 var t: i64 = 0 63 while t < 300 { 64 let x: i64 = (t*37+11) & mask; let y: i64 = (t*53+7) & mask 65 var res: i64 = 0; var cin: i64 = 0; var i: i64 = 0 66 while i < 8 { 67 let ai: i64 = (x>>i)&1; let bi: i64 = (y>>i)&1 68 res = res | (hz_eval1(so, sa, sb, sL, ai, bi, cin) << i) 69 cin = hz_eval1(co, ca, cb, cL, ai, bi, cin) 70 i = i + 1 71 } 72 if res != ((x+y) & mask) { bad = bad + 1 } 73 t = t + 1 74 } 75 hz_puts(label); hz_puts(": 8-bit adder from gates, verified 300 pairs, mismatches=" as *u8); hz_num(bad); hz_puts("\n" as *u8) 76 var ok: i64 = 0; if bad == 0 { ok = 1 } 77 return ok 78} 79 80// FUNCTIONALITY 3-5: a boolean functionality, exact-verified. 81func hz_bool(target: i64, label: *u8) -> i64 { 82 let op: *i64 = sys_mmap(8*12) as *i64; let a: *i64 = sys_mmap(8*12) as *i64; let b: *i64 = sys_mmap(8*12) as *i64 83 let L: i64 = bl_find(target, op, a, b, 6) 84 var ok: i64 = 0; if L > 0 { if hz_booleval(op, a, b, L) == target { ok = 1 } } 85 hz_puts(label); hz_puts(": " as *u8); hz_num(L); hz_puts(" gates, exact-verified " as *u8); if ok==1 {hz_puts("OK\n" as *u8)} else {hz_puts("FAIL\n" as *u8)} 86 return ok 87} 88 89func hz_run(r: *i64) -> i64 { 90 hz_puts("=== HORIZONTAL: one loop across DISTINCT functionalities (not just one vertical path) ===\n" as *u8) 91 r[0] = hz_mul(" ARITHMETIC-mul" as *u8) 92 r[1] = hz_add(" ARITHMETIC-add" as *u8) 93 r[2] = hz_bool(232, " LOGIC-majority" as *u8) 94 r[3] = hz_bool(150, " CHECKSUM-parity" as *u8) 95 r[4] = hz_bool(216, " SELECT-mux a?b:c" as *u8) 96 hz_puts("----------------------------------------------------------------\n" as *u8) 97 hz_puts(" the same synthesize+verify loop covers the functional breadth -- horizontal. with level-8-up = the full 2D grid.\n" as *u8) 98 return 5 99} 100 101func main() -> i64 { 102 let r: *i64 = sys_mmap(8 * 8) as *i64 103 let n: i64 = hz_run(r) 104 let ec: i64 = tally(r, n) 105 sys_exit(ec) 106 return ec 107}