code wiki / _hdl_build / _ale_format_gate.nx

_ale_format_gate.nx

buildroot/runtime/_hdl_build/_ale_format_gate.nx

7664 B162 linesdepth 2pulls 2 transitivereach 0 importersview sourcekind gate/prooftopic ale

docs dependencies structs consts functions

about

_ale_format_gate.nx -- the ALE-FORMAT gate (rungs ALE-R0a/R0b, sovereign schema). Diff-lane / no-mocks: runs the REAL sovereign validator nx_ale_format_validate.elf (built by nx_cc_sovereign->nxasm_x86_main, NO gcc) over REAL fixtures and asserts: ACCEPT-1 -- validator EXIT 0 on the golden valid triple (good_triple.txt) ACCEPT-2 -- validator EXIT 0 on the FIRST EXTERNAL fixture ale_real_task01.txt (demo/hello from rdi-berkeley/agents-last-exam@6b7f1b98, real provenance) REJECT-1 -- validator NONZERO on bad_missing.txt (missing required field) REJECT-2 -- validator NONZERO on bad_range.txt (score out of [0,1]) REJECT-3 -- validator NONZERO on bad_nondet.txt (grader non-deterministic) REJECT-4 -- validator NONZERO on bad_leak.txt (staged_reference_after=no LEAKAGE) REJECT-5 -- validator NONZERO on bad_humanjudge.txt (code_graded=no HUMAN JUDGE) SPEC -- ale_format.spec carries the three contract names + PROVENANCE + RECONCILED The "diff" here = the sovereign ACCEPT lane vs the REFUSAL lane disagreeing on valid-vs-tampered input (the validator's own exit code is the gating signal). The REAL Berkeley repo is the external oracle: ale_real_task01 is extracted from the actual cloned code, so the spec is no longer self-authored-only. Evidence -> knowledge/status/ale_format.log (ALEFMTGATE row; the queue row's ||MARK= reads it). license_tier: ORIGINAL

dependencies 1 imports · 0 importers

imports: nx_syscalls.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

structs

none

consts

none

functions

21	func g_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } called by 1: main calls 1: sys_write
22	func g_fp(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 } called by 1: main calls 1: sys_write
23	func g_fn(fd: i64, 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)) as u8; m = m / 10; k = k + 1 }; var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }; sys_write(fd, bb, k); return 0 } called by 1: main calls 2: sys_mmap sys_write
26	func g_run_val(triple: *u8) -> i64 called by 1: main calls 7: sys_fork sys_openat_wr sys_dup3 sys_mmap sys_execve sys_exit+1
46	func g_file_has(path: u8, pat: u8) -> i64 called by 1: main calls 4: sys_mmap sys_openat_rd sys_read sys_close
71	func main() -> i64 calls 9: g_p g_run_val g_file_has g_fn sys_openat_append g_fp+3