code wiki / _hdl_build / nx_stackaudit_targets_gate.nx

nx_stackaudit_targets_gate.nx

buildroot/runtime/_hdl_build/nx_stackaudit_targets_gate.nx

3056 B73 linesdepth 5pulls 6 transitivereach 0 importersview sourcekind gate/prooftopic stackaudit
docsdependenciesstructsconstsfunctions

about

nx_stackaudit_targets_gate.nx -- gate for the loop-closer. Proves the EXACT production code path (sax_should_emit + sax_emit_targets_core) against a /tmp queue it writes itself. NEGATIVE CONTROLS are load-bearing: idempotency (an id already in the queue is NOT re-emitted -- the invariant that makes per-beat emission safe), a healthy rung is NEVER targeted, and a re-run against the just- written queue emits ZERO. verdict GREEN iff 6/6. license_tier: ORIGINAL

dependencies 1 imports · 0 importers

nx_stackaudit_lib.nx nx_stackaudit_targets_gate.nx

imports: nx_stackaudit_lib.nx

imported by: nobody (leaf or entry point)

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

main sax_mkid stg_row sax_should_emit sax_mkid ↻ el_contains el_len el_match ss_writefile sys_openat_wr sys_write sys_close sys_fsync ss_readall sys_openat_rd sys_lseek sys_mmap sys_read sys_close ↻ sys_openat_append sax_emit_targets_core sax_kind sax_eval ss_readall ↻ el_last_after el_len ↻ el_match ↻ el_contains ↻ el_last_green el_len ↻ el_match ↻ sax_log sax_pat sax_name sax_healthy _fp el_len ↻ sys_write ↻ _fn sys_mmap ↻

structs

none

consts

none

functions

8func stg_row(name: *u8, ok: i64) -> i64
called by 1: main
15func main(argc: i64, argv: *i64) -> i64