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" 12import "nx_gate_verdict.nx" 13 14func main() -> i64 { 15 g_puts("nx_relchan gate (sovereign reliable/ordered/exactly-once events over a lossy link)\n" as *u8) 16 var pass: i64 = 0; var total: i64 = 0 17 18 let N: i64 = 8 19 let CAP: i64 = 8 20 let r: *i64 = sys_mmap((2 + CAP) * 8) as *i64 21 let s: *i64 = sys_mmap(2 * 8) as *i64 22 rc_rinit(r, CAP) 23 rc_sinit(s, N) 24 let dord: *i64 = sys_mmap(N * 8) as *i64 25 var dc: i64 = 0 26 var txs: i64 = 0 // measured wire transmissions (incl. retransmits) 27 28 // 1) lossy convergence: drop events on ((tick*7+seq*3)%5==0); drop acks on (tick%4==0) 29 var tick: i64 = 0 30 var converged: i64 = 0 31 while tick < 80 { 32 if converged == 0 { 33 var seq: i64 = rc_unacked_lo(s) // resend the whole unacked window (go-back-N) 34 while seq < N { 35 txs = txs + 1 36 let drop: i64 = ((tick*7 + seq*3) % 5) 37 if drop != 0 { // survived the lossy link 38 let before: i64 = rc_expected(r) 39 let nd: i64 = rc_recv(r, CAP, seq) 40 var k: i64 = 0 41 while k < nd { dord[dc] = before + k; dc = dc + 1; k = k + 1 } 42 } 43 seq = seq + 1 44 } 45 let ackv: i64 = rc_ack_value(r) 46 if ackv >= 0 { if (tick % 4) != 0 { rc_ack(s, ackv) } } // some acks dropped 47 if rc_delivered(r) == N { converged = 1 } 48 } 49 tick = tick + 1 50 } 51 var r1: i64 = 1 52 if rc_delivered(r) != N { r1 = 0 } 53 if dc != N { r1 = 0 } 54 var i: i64 = 0 55 while i < N { if dord[i] != i { r1 = 0 } i = i + 1 } // strictly in order 0..N-1, each once 56 g_puts(" [measure] delivered " as *u8); g_pn(rc_delivered(r)); g_puts("/" as *u8); g_pn(N) 57 g_puts(" events exactly-once in-order over a lossy link; wire transmissions=" as *u8); g_pn(txs); g_puts("\n" as *u8) 58 pass = pass + g_check("all events delivered exactly-once, in order, despite loss" as *u8, r1); total=total+1 59 60 // 2) idempotent: replay an already-delivered event -> nothing more delivered 61 let dbefore: i64 = rc_delivered(r) 62 let nd_dup: i64 = rc_recv(r, CAP, 3) 63 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 64 65 // 3) honest no-fake: total loss -> nothing delivered 66 let r2: *i64 = sys_mmap((2 + CAP) * 8) as *i64 67 let s2: *i64 = sys_mmap(2 * 8) as *i64 68 rc_rinit(r2, CAP); rc_sinit(s2, N) 69 var t2: i64 = 0 70 while t2 < 40 { 71 var seq: i64 = rc_unacked_lo(s2) 72 while seq < N { seq = seq + 1 } // ALL sends dropped (total-loss neg-control) 73 t2 = t2 + 1 74 } 75 pass = pass + g_check("honest: total loss -> 0 delivered (no fabricated delivery, neg)" as *u8, rc_delivered(r2) == 0); total=total+1 76 77 // 4) ack advances the window: after a cumulative ack, the unacked window starts past the acked events 78 let s3: *i64 = sys_mmap(2 * 8) as *i64 79 rc_sinit(s3, N) 80 let lo0: i64 = rc_unacked_lo(s3) // = 0 81 rc_ack(s3, 4) // peer confirms 0..4 82 let lo1: i64 = rc_unacked_lo(s3) // = 5 83 var r4: i64 = 1 84 if lo0 != 0 { r4 = 0 } 85 if lo1 != 5 { r4 = 0 } 86 if rc_all_acked(s3) == 1 { r4 = 0 } // not all yet (5,6,7 remain) 87 rc_ack(s3, 7) 88 if rc_all_acked(s3) != 1 { r4 = 0 } // now all acked 89 pass = pass + g_check("cumulative ack advances window + retires retransmits" as *u8, r4); total=total+1 90 91 g_puts("---- relchan gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 92 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 93 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 94 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 95 let ctr__dry: *i64 = gv_ctr() 96 ctr__dry[0] = pass 97 ctr__dry[1] = total 98 let rc__dry: i64 = gv_verdict("RELCHAN-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 99 sys_exit(rc__dry) 100 return rc__dry 101}