code wiki / _hdl_build / nx_builder_authors_cegis.nx
nx_builder_authors_cegis.nx source
↩ module page · 17 lines · 1016 B
1// nx_builder_authors_cegis.nx -- the BUILDER authors the S3.5 MECHANIZED CEGIS LOOP. The S3 round
2// PROVED the need (mod-impostors survived hand-picked examples twice); the loop closes it: search a
3// candidate -> probe vs the ORACLE over a deterministic grid -> first disagreement becomes a new
4// example -> re-search -> CONVERGED only at zero disagreements on the whole probe domain. The gate
5// re-runs the exact spec hand-CEGIS failed on (validator threshold) plus bitfield + clamp.
6// license_tier: ORIGINAL
7import "nx_module_author.nx"
8import "nx_syscalls.nx"
9func _b(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
10func main() -> i64 {
11 _b("BUILDER authors the S3.5 mechanized CEGIS loop (oracle-driven counterexamples)\n" as *u8)
12 let fd: i64 = sys_openat_wr("runtime/_hdl_build/_cegis_authored.nx" as *u8, 0x1a4)
13 ma_emit_cegis(fd)
14 sys_close(fd)
15 _b(" -> _cegis_authored.nx authored; Engineer verifies next\n" as *u8)
16 sys_exit(0); return 0
17}