code wiki / _hdl_build / nx_builder_synth_test.nx
`nx_builder_synth_test.nx` source

1// nx_builder_synth_test.nx -- prove the TEAM authored the answer, not Claude. The Builder is handed
2// ONLY the objective (importances + budget) and SEARCHES for the allocation; the Engineer verifies.
3// Two different specs (so it's a general capability, not a one-off): the team must (1) discover an
4// allocation that matches the rate-distortion optimum and beats uniform, and (2) author a DIFFERENT
5// allocation for a DIFFERENT importance profile -- proving it builds solutions, not memorizes one.
6// Exit 0 if the team's searched answers are valid + better on both. license_tier: ORIGINAL
7
8import "nx_builder_synth.nx"
9import "nx_syscalls.nx"
10
11func 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 }
12func bt_num(v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;k=1}; while m>0 {t[k]=48+(m%10); m=m/10; k=k+1}; var i: i64=0; while i<k {bb[i]=t[k-1-i]; i=i+1}; sys_write(1, bb, k); return 0 }
13func bt_alloc(n: i64, b: *i64) -> i64 { bt_puts("[" as *u8); var i: i64=0; while i<n { bt_num(b[i]); if i<n-1 {bt_puts("," as *u8)} i=i+1 } bt_puts("]" as *u8); return 0 }
14
15func main() -> i64 {
16    bt_puts("=== BUILDER SYNTHESIS: the TEAM searches + authors the allocation (who wrote the answer?) ===\n" as *u8)
17    let N: i64 = 4; let budget: i64 = 16
18
19    // SPEC 1: importance heavy on group 0
20    let imp1: *i64 = sys_mmap(8*8) as *i64; imp1[0]=100; imp1[1]=10; imp1[2]=10; imp1[3]=1
21    let a1: *i64 = sys_mmap(8*8) as *i64
22    let s1: i64 = bsy_author_alloc(N, imp1, budget, a1)
23    bt_puts(" spec1 imp[100,10,10,1] -> team SEARCHED " as *u8); bt_num(s1); bt_puts(" steps -> authored " as *u8); bt_alloc(N, a1); bt_puts(" err=" as *u8); bt_num(imat_weighted_error(N,imp1,a1)); bt_puts(" verify=" as *u8); bt_num(bsy_verify(N,imp1,budget,a1)); bt_puts("\n" as *u8)
24
25    // SPEC 2: a DIFFERENT profile (heavy on group 3) -> the team must author a DIFFERENT allocation
26    let imp2: *i64 = sys_mmap(8*8) as *i64; imp2[0]=1; imp2[1]=5; imp2[2]=20; imp2[3]=200
27    let a2: *i64 = sys_mmap(8*8) as *i64
28    let s2: i64 = bsy_author_alloc(N, imp2, budget, a2)
29    bt_puts(" spec2 imp[1,5,20,200] -> team SEARCHED " as *u8); bt_num(s2); bt_puts(" steps -> authored " as *u8); bt_alloc(N, a2); bt_puts(" err=" as *u8); bt_num(imat_weighted_error(N,imp2,a2)); bt_puts(" verify=" as *u8); bt_num(bsy_verify(N,imp2,budget,a2)); bt_puts("\n" as *u8)
30
31    let r: *i64 = sys_mmap(8*8) as *i64
32    r[0] = 0; if bsy_verify(N, imp1, budget, a1) == 1 { r[0] = 1 }              // team's spec1 answer valid+better
33    r[1] = 0; if bsy_verify(N, imp2, budget, a2) == 1 { r[1] = 1 }              // team's spec2 answer valid+better
34    r[2] = 0; if a1[0] > a1[3] { if a2[3] > a2[0] { r[2] = 1 } }                // DIFFERENT answers per spec (not memorized)
35    r[3] = 0; if imat_weighted_error(N, imp1, a1) <= 173056 { r[3] = 1 }        // matched/beat the RD optimum
36    var pass: i64 = 0; var j: i64 = 0
37    while j < 4 { pass = pass + r[j]; j = j + 1 }
38    bt_puts("----\n passed " as *u8); bt_num(pass); bt_puts("/4\n" as *u8)
39    if pass == 4 { bt_puts(" THE TEAM AUTHORED IT: handed only the objective, the Builder SEARCHED + found the optimal allocation per spec; Engineer verified. Not hand-coded.\n" as *u8); sys_exit(0); return 0 }
40    bt_puts(" FAIL\n" as *u8); sys_exit(1); return 1
41}
nx_builder_synth_test.nx source

`nx_builder_synth_test.nx` source
