code wiki / _hdl_build / nx_nack_gate.nx

nx_nack_gate.nx source

↩ module page · 98 lines · 6072 B

1import "nx_gate_base.nx" 2// nx_nack_gate.nx -- proves the sovereign NACK does what WebRTC's does, MEASURED on a deterministic lossy 3// trace: recoverable losses ARE requested and recovered before deadline; hopeless losses (deadline too 4// near) are NOT requested (no wasted bandwidth); requests are rate-limited to one per RTT and capped at 5// NACK_MAX_RETRIES (no storm); the sender history honors requests. NEG-CONTROL: a too-shallow playout 6// budget makes retransmit impossible -> ZERO requests + ZERO recovery (it correctly gives up). 7// expect_exit: 0 license_tier: ORIGINAL 8import "nx_syscalls.nx" 9import "nx_nack.nx" 10 11const K: i64 = 200 12const FRAME_US: i64 = 33333 13const NET_US: i64 = 30000 // one-way; RTT = 2*NET 14const RTT_US: i64 = 60000 15 16func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw(" 17" as *u8); return ok } 18func gn(v: i64) -> i64 { 19 let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m} 20 let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48 as u8;k=1} while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1} 21 var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 } 22 23func is_lost(s: i64) -> i64 { if (s % 7) == 3 { if s > 0 { return 1 } } return 0 } 24 25// run the trace at playout budget target_delay_us; res[0]=losses res[1]=nacks res[2]=recovered 26func run(target_delay_us: i64, res: *i64) -> i64 { 27 let anchor_play: i64 = NET_US + target_delay_us // seq0 arrives at NET, playout starts +delay 28 var losses: i64 = 0 29 var nacks: i64 = 0 30 var recovered: i64 = 0 31 var s: i64 = 1 32 while s < K { 33 if is_lost(s) == 1 { 34 losses = losses + 1 35 // gap detected when the next (received) frame arrives; losses are %7-spaced so s+1 is present 36 let detect_now: i64 = (s + 1) * FRAME_US + NET_US 37 if nack_should_request(s, detect_now, anchor_play, 0, FRAME_US, RTT_US, 0, 0) == 1 { 38 nacks = nacks + 1 39 let retransmit_arrival: i64 = detect_now + RTT_US // request out + resend back 40 let deadline: i64 = anchor_play + s * FRAME_US 41 if retransmit_arrival <= deadline { recovered = recovered + 1 } 42 } 43 } 44 s = s + 1 45 } 46 res[0] = losses; res[1] = nacks; res[2] = recovered 47 return 0 48} 49 50func main() -> i64 { 51 gw("=== nx_nack_gate: sovereign selective-retransmit (WebRTC-class NACK, from scratch) ===\n" as *u8) 52 let main_r: *i64 = sys_mmap(8 * 4) as *i64 53 let neg_r: *i64 = sys_mmap(8 * 4) as *i64 54 run(250000, main_r) // generous 7.5-frame budget -> retransmit fits 55 run(50000, neg_r) // shallow 1.5-frame budget -> retransmit CANNOT arrive in time 56 57 gw(" MAIN (budget 250ms): losses=" as *u8); gn(main_r[0]); gw(" nacks=" as *u8); gn(main_r[1]); gw(" recovered=" as *u8); gn(main_r[2]); gw("\n" as *u8) 58 gw(" NEG (budget 50ms) : losses=" as *u8); gn(neg_r[0]); gw(" nacks=" as *u8); gn(neg_r[1]); gw(" recovered=" as *u8); gn(neg_r[2]); gw(" (retransmit impossible -> must be 0/0)\n" as *u8) 59 60 // ---- unit asserts on the decision function (rate-limit, retry-cap, deadline) ---- 61 let AP: i64 = NET_US + 250000 62 let far_seq: i64 = 100 63 let far_now: i64 = 101 * FRAME_US + NET_US 64 let u_recoverable: i64 = nack_should_request(far_seq, far_now, AP, 0, FRAME_US, RTT_US, 0, 0) // 1 65 let u_ratelimited: i64 = nack_should_request(far_seq, far_now, AP, 0, FRAME_US, RTT_US, 1, far_now - 100) // 0 (too soon) 66 let u_after_rtt: i64 = nack_should_request(far_seq, far_now, AP, 0, FRAME_US, RTT_US, 1, far_now - RTT_US - 1) // 1 (RTT elapsed) 67 let u_capped: i64 = nack_should_request(far_seq, far_now, AP, 0, FRAME_US, RTT_US, NACK_MAX_RETRIES, 0) // 0 (gave up) 68 let u_hopeless: i64 = nack_should_request(far_seq, far_now, NET_US + 50000, 0, FRAME_US, RTT_US, 0, 0) // 0 (deadline near) 69 gw(" decision: recoverable=" as *u8); gn(u_recoverable); gw(" ratelimited=" as *u8); gn(u_ratelimited); gw(" after_rtt=" as *u8); gn(u_after_rtt); gw(" capped=" as *u8); gn(u_capped); gw(" hopeless=" as *u8); gn(u_hopeless); gw("\n" as *u8) 70 71 // ---- sender history ring ---- 72 let H: i64 = 128 73 let hist: *i64 = sys_mmap(8 * H) as *i64 74 var i: i64 = 0 75 while i < H { hist[i] = 0 - 1; i = i + 1 } 76 i = 0 77 while i < K { nack_hist_put(hist, H, i); i = i + 1 } 78 let recent_has: i64 = nack_hist_has(hist, H, K - 10) // 1 (recent, still in ring) 79 let old_has: i64 = nack_hist_has(hist, H, 5) // 0 (evicted: 5 + 128 < 200) 80 81 var bad: i64 = 0 82 if main_r[2] != main_r[0] { bad = bad + 1; gw(" FAIL: not all recoverable losses recovered\n" as *u8) } 83 if main_r[1] != main_r[0] { bad = bad + 1; gw(" FAIL: nack count != losses (should request each once)\n" as *u8) } 84 if main_r[0] <= 0 { bad = bad + 1; gw(" FAIL: trace produced no losses\n" as *u8) } 85 if neg_r[1] != 0 { bad = bad + 1; gw(" FAIL neg: requested a hopeless retransmit\n" as *u8) } 86 if neg_r[2] != 0 { bad = bad + 1; gw(" FAIL neg: 'recovered' something un-retransmittable\n" as *u8) } 87 if u_recoverable != 1 { bad = bad + 1; gw(" FAIL: recoverable not requested\n" as *u8) } 88 if u_ratelimited != 0 { bad = bad + 1; gw(" FAIL: rate-limit not enforced\n" as *u8) } 89 if u_after_rtt != 1 { bad = bad + 1; gw(" FAIL: retry after RTT not allowed\n" as *u8) } 90 if u_capped != 0 { bad = bad + 1; gw(" FAIL: retry cap not enforced\n" as *u8) } 91 if u_hopeless != 0 { bad = bad + 1; gw(" FAIL: hopeless request not suppressed\n" as *u8) } 92 if recent_has != 1 { bad = bad + 1; gw(" FAIL: sender lost a recent frame from history\n" as *u8) } 93 if old_has != 0 { bad = bad + 1; gw(" FAIL: history ring did not evict old frame\n" as *u8) } 94 95 if bad == 0 { gw("NACK-GATE verdict=GREEN -- recoverable losses recovered, hopeless suppressed, rate-limited + capped (no storm)\n" as *u8); return 0 } 96 gw("NACK-GATE verdict=RED fails=" as *u8); gn(bad); gw("\n" as *u8) 97 return 1 98}