code wiki / _hdl_build / nx_transport_gate.nx

nx_transport_gate.nx

buildroot/runtime/_hdl_build/nx_transport_gate.nx

4003 B66 linesdepth 2pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic transport
docsdependenciesstructsconstsfunctions

about

nx_transport_gate.nx -- proves the SOVEREIGN transport CONTRACT (nx_transport). A frame handed to a transport must come out the other side byte-identical + in FIFO order, and the open/send/recv/close lifecycle + honest drops (oversized/full/closed -> -1, empty -> 0) must hold. Any transport adapter (browser WebSocket, NishiOS datagram) MUST satisfy this -> it is the seam where WebSocket is just a swappable pipe. Reference impl = the loopback ring. NEG-controls give the checker teeth. 0=GREEN/1=RED.

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_transport.nx nx_transport_gate.nx

imports: nx_syscalls.nxnx_transport.nx

imported by: nobody (leaf or entry point)

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

main g_p sys_write sys_mmap tp_open tp_hset chk g_p ↻ tp_send tp_h tp_slot_len tp_slot_bytes tp_hset ↻ tp_pending tp_h ↻ tp_recv tp_h ↻ tp_slot_len ↻ tp_slot_bytes ↻ tp_hset ↻ bytes_eq tp_close tp_hset ↻ g_n g_p ↻ sys_mmap ↻ sys_write ↻

structs

none

consts

none

functions

9func 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 3: g_nchkmain calls 1: sys_write
10func g_n(v: i64) -> i64
called by 1: main calls 3: g_psys_mmapsys_write
14func chk(cond: i64, name: *u8, pp: *i64, tp: *i64) -> i64
called by 1: main calls 1: g_p
18func bytes_eq(a: *u8, al: i64, b: *u8, bl: i64) -> i64
called by 1: main
23func main() -> i64
calls 10: g_psys_mmaptp_openchktp_sendtp_pending+4