code wiki / _hdl_build / nx_relchan_gate.nx

nx_relchan_gate.nx

buildroot/runtime/_hdl_build/nx_relchan_gate.nx

4719 B93 linesdepth 3pulls 4 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 3 imports · 0 importers

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

imports: nx_syscalls.nxnx_gate_emit_lib.nxnx_relchan.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 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 sys_exit

structs

none

consts

none

functions

13func main() -> i64