code wiki / _hdl_build / nx_relchan_gate.nx

nx_relchan_gate.nx

buildroot/runtime/_hdl_build/nx_relchan_gate.nx

5160 B101 linesdepth 3pulls 5 transitivereach 0 importersview sourcekind gate/proof
docsdependenciesstructsconstsfunctions

about

nx_relchan_gate.nx -- proves + MEASURES the sovereign reliable/ordered/exactly-once event channel (nx_relchan) over a LOSSY link (drops both events AND acks). Critical game events survive packet loss without being lost or double-applied -- the correctness the position stream doesn't need but captures do. 1) all N events delivered EXACTLY ONCE, IN ORDER, despite event+ack loss (converges via retransmit) 2) idempotent (neg): replaying an already-delivered event delivers nothing more 3) honest no-fake (neg): under TOTAL loss nothing is delivered (no fabricated delivery) 4) ack advances the window: a cumulative ack stops retransmission of acked events Built nx_cc_sovereign -> nxasm_x86 (no gcc, no .sh). license_tier: ORIGINAL

dependencies 4 imports · 0 importers

nx_syscalls.nx nx_gate_emit_lib.nx nx_relchan.nx nx_gate_verdict.nx nx_relchan_gate.nx

imports: nx_syscalls.nxnx_gate_emit_lib.nxnx_relchan.nxnx_gate_verdict.nx

imported by: nobody (leaf or entry point)

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

main g_puts sys_write sys_mmap nxa_die sys_write ↻ sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ rc_rinit rc_sinit rc_unacked_lo rc_expected rc_recv rc_ack_value rc_ack rc_delivered g_pn sys_mmap ↻ sys_write ↻ g_check g_puts ↻ rc_all_acked gv_ctr sys_mmap ↻ gv_verdict gv_note_bare_rate gv_bare_rate gv_at gv_obj_has_n gv_at ↻

structs

none

consts

none

functions

14func main() -> i64