code wiki / _hdl_build / nx_dgram_media_gate.nx

nx_dgram_media_gate.nx source

↩ module page · 212 lines · 10648 B

1// nx_dgram_media_gate.nx -- proves the SOVEREIGN datagram media wire (nx_dgram_media, task #15 R1) under 2// the conditions UDP actually delivers: LOSS, REORDER, DUPLICATION -- the in-process netem-class proof, 3// fully sovereign. Frames must reassemble BIT-EXACT; gaps must surface as NACKs; the NACK wire must round- 4// trip; retransmits must complete the set with NO double-delivery; hostile packets must be refused without 5// corrupting state. Deterministic PRNG (seeded LCG -- reproducible, no Math.random). 0=GREEN / 1=RED. 6import "nx_syscalls.nx" 7import "nx_dgram_media.nx" 8 9func g_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 10func g_n(v: i64) -> i64 { 11 var m: i64=v; if m<0{g_w("-\x00" as *u8);m=0-m} 12 let t: *u8=sys_mmap(24); var k: i64=0; if m==0{t[0]=48 as u8;k=1} else {while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1}} 13 let o: *u8=sys_mmap(24); var j: i64=0; while j<k{o[j]=t[k-1-j];j=j+1} sys_write(1,o,k); return 0 } 14func chk(cond: i64, name: *u8, pp: *i64, tp: *i64) -> i64 { 15 tp[0]=tp[0]+1; g_w(name) 16 if cond==1 { pp[0]=pp[0]+1; g_w(" ok\n\x00" as *u8) } else { g_w(" FAIL\n\x00" as *u8) } 17 return 0 } 18func beq(a: *u8, b: *u8, n: i64) -> i64 { var i: i64=0; while i<n { if a[i]!=b[i] { return 0 } i=i+1 } return 1 } 19func fill(dst: *u8, n: i64, key: i64) -> i64 { var i: i64=0; while i<n { dst[i]=(((i*31)+(key*77)+((i>>5)*13))&255) as u8; i=i+1 } return 0 } 20 21// deterministic channel PRNG 22func rnd(state: *i64) -> i64 { state[0] = (state[0] * 1103515245 + 12345) & 0x7fffffff; return (state[0] >> 16) & 0x7fff } 23 24// send every packet in a packed stream through the channel into rx; loss_pct drops, dup3 duplicates every 25// 3rd surviving packet, swap2 swaps each adjacent surviving pair. Returns delivered-complete count. 26func channel(stream: *u8, npkts: i64, loss_pct: i64, dup3: i64, swap2: i64, st: *i64, 27 rxm: *u8, fout: *u8, fcap: i64, rinfo: *i64, got: *i64, orig: *u8, fsz: i64, okp: *i64) -> i64 { 28 // collect surviving packet offsets first (so reorder/dup operate on the survivor list) 29 let offs: *i64 = sys_mmap(8 * 512) as *i64 30 let lens: *i64 = sys_mmap(8 * 512) as *i64 31 var nsur: i64 = 0 32 var o: i64 = 0 33 var i: i64 = 0 34 while i < npkts { 35 let pl: i64 = (stream[o] & 0xff) + ((stream[o+1] & 0xff) << 8) 36 if (rnd(st) % 100) >= loss_pct { 37 offs[nsur] = o + 2; lens[nsur] = pl; nsur = nsur + 1 38 } 39 o = o + 2 + pl 40 i = i + 1 41 } 42 if swap2 == 1 { 43 var s2: i64 = 0 44 while s2 + 1 < nsur { 45 let to: i64 = offs[s2]; let tl: i64 = lens[s2] 46 offs[s2] = offs[s2+1]; lens[s2] = lens[s2+1] 47 offs[s2+1] = to; lens[s2+1] = tl 48 s2 = s2 + 2 49 } 50 } 51 var done: i64 = 0 52 var k: i64 = 0 53 while k < nsur { 54 var times: i64 = 1 55 if dup3 == 1 { if (k % 3) == 2 { times = 2 } } 56 var t2: i64 = 0 57 while t2 < times { 58 let r: i64 = dgm_rx_add(rxm, ((stream as i64) + offs[k]) as *u8, lens[k], fout, fcap, rinfo) 59 if r > 0 { 60 let sq: i64 = rinfo[1] 61 if got[sq] == 0 { 62 got[sq] = 1 63 if r == fsz { if beq(fout, ((orig as i64) + sq * fsz) as *u8, fsz) == 1 { okp[0] = okp[0] + 1 } } 64 done = done + 1 65 } else { got[sq] = got[sq] + 1 } // double-delivery detector (>1 = bug) 66 } 67 t2 = t2 + 1 68 } 69 k = k + 1 70 } 71 return done } 72 73func main() -> i64 { 74 g_w("=== nx_dgram_media_gate: sovereign UDP-class wire -- loss/reorder/dup, NACK round-trip, bit-exact ===\n\x00" as *u8) 75 let pp: *i64 = sys_mmap(8) as *i64; pp[0]=0 76 let tp: *i64 = sys_mmap(8) as *i64; tp[0]=0 77 let sender: *u8 = sys_mmap(8) 78 var si: i64 = 0 79 while si < 8 { sender[si] = (65 + si) as u8; si = si + 1 } 80 let rxm: *u8 = sys_mmap(DGM_RX_REGION) 81 dgm_rx_init(rxm) 82 let rinfo: *i64 = sys_mmap(8 * 12) as *i64 83 let fout: *u8 = sys_mmap(65536) 84 let pkts: *u8 = sys_mmap(65536) 85 86 // T1: small single-packet frame round-trips bit-exact 87 let f1: *u8 = sys_mmap(400) 88 fill(f1, 400, 1) 89 let n1: i64 = dgm_pack_frame(0x57, sender, 0, f1, 400, pkts, 65536) 90 chk((n1 == 1) as i64, "T1a 400B frame -> 1 packet\x00" as *u8, pp, tp) 91 let pl1: i64 = (pkts[0] & 0xff) + ((pkts[1] & 0xff) << 8) 92 let r1: i64 = dgm_rx_add(rxm, ((pkts as i64) + 2) as *u8, pl1, fout, 65536, rinfo) 93 chk((r1 == 400) as i64, "T1b delivers 400B\x00" as *u8, pp, tp) 94 chk(beq(fout, f1, 400), "T1c bit-exact\x00" as *u8, pp, tp) 95 96 // T2: 7KB keyframe-sized frame fragments + reassembles bit-exact 97 let f2: *u8 = sys_mmap(7110) 98 fill(f2, 7110, 2) 99 let n2: i64 = dgm_pack_frame(0x57, sender, 1, f2, 7110, pkts, 65536) 100 chk((n2 == 7) as i64, "T2a 7110B -> 7 fragments\x00" as *u8, pp, tp) 101 var o2: i64 = 0 102 var d2: i64 = 0 103 var i2: i64 = 0 104 while i2 < n2 { 105 let pl: i64 = (pkts[o2] & 0xff) + ((pkts[o2+1] & 0xff) << 8) 106 let rr: i64 = dgm_rx_add(rxm, ((pkts as i64) + o2 + 2) as *u8, pl, fout, 65536, rinfo) 107 if rr > 0 { d2 = rr } 108 o2 = o2 + 2 + pl 109 i2 = i2 + 1 110 } 111 chk((d2 == 7110) as i64, "T2b reassembles 7110B\x00" as *u8, pp, tp) 112 chk(beq(fout, f2, 7110), "T2c bit-exact across fragments\x00" as *u8, pp, tp) 113 114 // T3: 100 x 1500B frames through 20% LOSS -> gaps -> NACK wire round-trip -> retransmit -> ALL delivered 115 let NFR: i64 = 100 116 let FSZ: i64 = 1500 117 let orig: *u8 = sys_mmap(NFR * FSZ) 118 var fi3: i64 = 0 119 while fi3 < NFR { fill(((orig as i64) + fi3 * FSZ) as *u8, FSZ, 100 + fi3); fi3 = fi3 + 1 } 120 let rxm3: *u8 = sys_mmap(DGM_RX_REGION) 121 dgm_rx_init(rxm3) 122 let got: *i64 = sys_mmap(8 * NFR) as *i64 123 let okp: *i64 = sys_mmap(8) as *i64; okp[0] = 0 124 let st: *i64 = sys_mmap(8) as *i64; st[0] = 20260705 125 var delivered: i64 = 0 126 var fi4: i64 = 0 127 while fi4 < NFR { 128 let np: i64 = dgm_pack_frame(0x57, sender, fi4, ((orig as i64) + fi4 * FSZ) as *u8, FSZ, pkts, 65536) 129 delivered = delivered + channel(pkts, np, 20, 0, 0, st, rxm3, fout, 65536, rinfo, got, orig, FSZ, okp) 130 fi4 = fi4 + 1 131 } 132 g_w(" after 20% loss: delivered=\x00" as *u8); g_n(delivered); g_w("/100\n\x00" as *u8) 133 chk((delivered < NFR) as i64, "T3a loss actually lost frames (channel has teeth)\x00" as *u8, pp, tp) 134 // NACK wire: receiver lists gaps -> packs NACK -> sender parses -> retransmits those; then sweep the tail 135 let gaps: *i64 = sys_mmap(8 * 64) as *i64 136 let ng: i64 = dgm_rx_gaps(rxm3, 0, gaps, 32) 137 let nkb: *u8 = sys_mmap(2048) 138 let nkn: i64 = dgm_pack_nack(sender, gaps, ng, nkb, 2048) 139 chk((nkn == 1) as i64, "T3b NACK packs (1 packet)\x00" as *u8, pp, tp) 140 let plk: i64 = (nkb[0] & 0xff) + ((nkb[1] & 0xff) << 8) 141 let rxn: *u8 = sys_mmap(DGM_RX_REGION) 142 dgm_rx_init(rxn) 143 let rk: i64 = dgm_rx_add(rxn, ((nkb as i64) + 2) as *u8, plk, fout, 65536, rinfo) 144 var nasked: i64 = 0 - 1 145 if rk > 0 { if rinfo[0] == DGM_KIND_NACK { 146 let asked: *i64 = sys_mmap(8 * 64) as *i64 147 nasked = dgm_parse_nack(fout, rk, asked, 64) 148 var ri: i64 = 0 149 while ri < nasked { 150 let sq: i64 = asked[ri] 151 let np2: i64 = dgm_pack_frame(0x57, sender, sq, ((orig as i64) + sq * FSZ) as *u8, FSZ, pkts, 65536) 152 delivered = delivered + channel(pkts, np2, 0, 0, 0, st, rxm3, fout, 65536, rinfo, got, orig, FSZ, okp) 153 ri = ri + 1 154 } 155 } } 156 chk((nasked == ng) as i64, "T3c NACK wire round-trips the gap list\x00" as *u8, pp, tp) 157 var fi5: i64 = 0 158 while fi5 < NFR { 159 if got[fi5] == 0 { 160 let np3: i64 = dgm_pack_frame(0x57, sender, fi5, ((orig as i64) + fi5 * FSZ) as *u8, FSZ, pkts, 65536) 161 delivered = delivered + channel(pkts, np3, 0, 0, 0, st, rxm3, fout, 65536, rinfo, got, orig, FSZ, okp) 162 } 163 fi5 = fi5 + 1 164 } 165 chk((delivered == NFR) as i64, "T3d retransmit completes ALL 100\x00" as *u8, pp, tp) 166 chk((okp[0] == NFR) as i64, "T3e every frame bit-exact\x00" as *u8, pp, tp) 167 168 // T4: REORDER + DUP on fragmented frames -> all deliver once, bit-exact, no double-delivery 169 let rxm4: *u8 = sys_mmap(DGM_RX_REGION) 170 dgm_rx_init(rxm4) 171 let got4: *i64 = sys_mmap(8 * 20) as *i64 172 let ok4: *i64 = sys_mmap(8) as *i64; ok4[0] = 0 173 let orig4: *u8 = sys_mmap(20 * 3000) 174 var f6: i64 = 0 175 while f6 < 20 { fill(((orig4 as i64) + f6 * 3000) as *u8, 3000, 500 + f6); f6 = f6 + 1 } 176 var d4: i64 = 0 177 var f7: i64 = 0 178 while f7 < 20 { 179 let np4: i64 = dgm_pack_frame(0x57, sender, f7, ((orig4 as i64) + f7 * 3000) as *u8, 3000, pkts, 65536) 180 d4 = d4 + channel(pkts, np4, 0, 1, 1, st, rxm4, fout, 65536, rinfo, got4, orig4, 3000, ok4) 181 f7 = f7 + 1 182 } 183 chk((d4 == 20) as i64, "T4a reorder+dup: all 20 deliver\x00" as *u8, pp, tp) 184 chk((ok4[0] == 20) as i64, "T4b all bit-exact\x00" as *u8, pp, tp) 185 var dd: i64 = 0 186 var f8: i64 = 0 187 while f8 < 20 { if got4[f8] > 1 { dd = 1 } f8 = f8 + 1 } 188 chk((dd == 0) as i64, "T4c NO double-delivery (dedupe holds)\x00" as *u8, pp, tp) 189 190 // T5 NEG: hostile packets refused; state uncorrupted (a good frame still delivers after) 191 let bad: *u8 = sys_mmap(64) 192 var bi: i64 = 0 193 while bi < 40 { bad[bi] = 65 as u8; bi = bi + 1 } 194 chk((dgm_rx_add(rxm4, bad, 40, fout, 65536, rinfo) == 0 - 1) as i64, "T5a bad magic -> -1\x00" as *u8, pp, tp) 195 chk((dgm_rx_add(rxm4, bad, 6, fout, 65536, rinfo) == 0 - 1) as i64, "T5b truncated -> -1\x00" as *u8, pp, tp) 196 bad[0] = 78 as u8; bad[1] = 68 as u8 197 bad[15] = 5 as u8; bad[16] = 3 as u8 // frag_i >= frag_n 198 chk((dgm_rx_add(rxm4, bad, 40, fout, 65536, rinfo) == 0 - 1) as i64, "T5c frag_i>=frag_n -> -1\x00" as *u8, pp, tp) 199 let f9: *u8 = sys_mmap(800) 200 fill(f9, 800, 999) 201 let np9: i64 = dgm_pack_frame(0x57, sender, 21, f9, 800, pkts, 65536) 202 let pl9: i64 = (pkts[0] & 0xff) + ((pkts[1] & 0xff) << 8) 203 let r9: i64 = dgm_rx_add(rxm4, ((pkts as i64) + 2) as *u8, pl9, fout, 65536, rinfo) 204 var ok9: i64 = 0 205 if r9 == 800 { ok9 = beq(fout, f9, 800) } 206 chk(ok9, "T5d good frame still delivers after hostiles (state intact)\x00" as *u8, pp, tp) 207 208 g_w(" SCORE: \x00" as *u8); g_n(pp[0]); g_w("/\x00" as *u8); g_n(tp[0]); g_w("\n\x00" as *u8) 209 if pp[0] == tp[0] { g_w("DGRAM-MEDIA-GATE verdict=GREEN -- the sovereign UDP-class wire survives loss/reorder/dup, NACKs round-trip, frames bit-exact\n\x00" as *u8); return 0 } 210 g_w("DGRAM-MEDIA-GATE verdict=RED\n\x00" as *u8) 211 return 1 212}