nx_relchan_gate.nx source

1// nx_relchan_gate.nx -- proves + MEASURES the sovereign reliable/ordered/exactly-once event channel 2// (nx_relchan) over a LOSSY link (drops both events AND acks). Critical game events survive packet loss 3// without being lost or double-applied -- the correctness the position stream doesn't need but captures do. 4// 1) all N events delivered EXACTLY ONCE, IN ORDER, despite event+ack loss (converges via retransmit) 5// 2) idempotent (neg): replaying an already-delivered event delivers nothing more 6// 3) honest no-fake (neg): under TOTAL loss nothing is delivered (no fabricated delivery) 7// 4) ack advances the window: a cumulative ack stops retransmission of acked events 8// Built nx_cc_sovereign -> nxasm_x86 (no gcc, no .sh). license_tier: ORIGINAL 9import "nx_syscalls.nx" 10import "nx_gate_emit_lib.nx" 11import "nx_relchan.nx" 12 13func main() -> i64 { 14 g_puts("nx_relchan gate (sovereign reliable/ordered/exactly-once events over a lossy link)\n" as *u8) 15 var pass: i64 = 0; var total: i64 = 0 16 17 let N: i64 = 8 18 let CAP: i64 = 8 19 let r: *i64 = sys_mmap((2 + CAP) * 8) as *i64 20 let s: *i64 = sys_mmap(2 * 8) as *i64 21 rc_rinit(r, CAP) 22 rc_sinit(s, N) 23 let dord: *i64 = sys_mmap(N * 8) as *i64 24 var dc: i64 = 0 25 var txs: i64 = 0 // measured wire transmissions (incl. retransmits) 26 27 // 1) lossy convergence: drop events on ((tick*7+seq*3)%5==0); drop acks on (tick%4==0) 28 var tick: i64 = 0 29 var converged: i64 = 0 30 while tick < 80 { 31 if converged == 0 { 32 var seq: i64 = rc_unacked_lo(s) // resend the whole unacked window (go-back-N) 33 while seq < N { 34 txs = txs + 1 35 let drop: i64 = ((tick*7 + seq*3) % 5) 36 if drop != 0 { // survived the lossy link 37 let before: i64 = rc_expected(r) 38 let nd: i64 = rc_recv(r, CAP, seq) 39 var k: i64 = 0 40 while k < nd { dord[dc] = before + k; dc = dc + 1; k = k + 1 } 41 } 42 seq = seq + 1 43 } 44 let ackv: i64 = rc_ack_value(r) 45 if ackv >= 0 { if (tick % 4) != 0 { rc_ack(s, ackv) } } // some acks dropped 46 if rc_delivered(r) == N { converged = 1 } 47 } 48 tick = tick + 1 49 } 50 var r1: i64 = 1 51 if rc_delivered(r) != N { r1 = 0 } 52 if dc != N { r1 = 0 } 53 var i: i64 = 0 54 while i < N { if dord[i] != i { r1 = 0 } i = i + 1 } // strictly in order 0..N-1, each once 55 g_puts(" [measure] delivered " as *u8); g_pn(rc_delivered(r)); g_puts("/" as *u8); g_pn(N) 56 g_puts(" events exactly-once in-order over a lossy link; wire transmissions=" as *u8); g_pn(txs); g_puts("\n" as *u8) 57 pass = pass + g_check("all events delivered exactly-once, in order, despite loss" as *u8, r1); total=total+1 58 59 // 2) idempotent: replay an already-delivered event -> nothing more delivered 60 let dbefore: i64 = rc_delivered(r) 61 let nd_dup: i64 = rc_recv(r, CAP, 3) 62 pass = pass + g_check("idempotent: replay of a delivered event delivers nothing (neg)" as *u8, (nd_dup == 0) & (rc_delivered(r) == dbefore)); total=total+1 63 64 // 3) honest no-fake: total loss -> nothing delivered 65 let r2: *i64 = sys_mmap((2 + CAP) * 8) as *i64 66 let s2: *i64 = sys_mmap(2 * 8) as *i64 67 rc_rinit(r2, CAP); rc_sinit(s2, N) 68 var t2: i64 = 0 69 while t2 < 40 { 70 var seq: i64 = rc_unacked_lo(s2) 71 while seq < N { seq = seq + 1 } // ALL sends dropped (total-loss neg-control) 72 t2 = t2 + 1 73 } 74 pass = pass + g_check("honest: total loss -> 0 delivered (no fabricated delivery, neg)" as *u8, rc_delivered(r2) == 0); total=total+1 75 76 // 4) ack advances the window: after a cumulative ack, the unacked window starts past the acked events 77 let s3: *i64 = sys_mmap(2 * 8) as *i64 78 rc_sinit(s3, N) 79 let lo0: i64 = rc_unacked_lo(s3) // = 0 80 rc_ack(s3, 4) // peer confirms 0..4 81 let lo1: i64 = rc_unacked_lo(s3) // = 5 82 var r4: i64 = 1 83 if lo0 != 0 { r4 = 0 } 84 if lo1 != 5 { r4 = 0 } 85 if rc_all_acked(s3) == 1 { r4 = 0 } // not all yet (5,6,7 remain) 86 rc_ack(s3, 7) 87 if rc_all_acked(s3) != 1 { r4 = 0 } // now all acked 88 pass = pass + g_check("cumulative ack advances window + retires retransmits" as *u8, r4); total=total+1 89 90 g_puts("---- relchan gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 91 if pass == total { g_puts("verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 92 g_puts("verdict=RED\n" as *u8); sys_exit(1); return 1 93}