code wiki / _hdl_build / nx_media_budget_gate.nx
nx_media_budget_gate.nx source
↩ module page · 135 lines · 7235 B
1import "nx_gate_base.nx"
2// nx_media_budget_gate.nx -- proves the shared resource-intelligence controller's two hard doctrines.
3// MONOTONE: sweeping ANY budget input up never lowers quality on ANY plan axis (fps/height/audio/lossless
4// non-decreasing; qp/gpu_detail non-increasing = better) -> no thrash, no inversion.
5// ENVELOPE-SAFE: over a grid of (peers, uplink), the plan's per-stream kbps x fan-out <= the MEASURED edge
6// ceiling AND <= the sender uplink -> scales DOWN under pressure BY CONSTRUCTION (never floods the family).
7// FLOOR/CEILING: a starved budget lands tier 0; a rich 2-peer budget lands tier 9 (60fps/1080/192k).
8// NEG-CONTROL: the monotone checker is run on a DELIBERATELY inverted sequence and MUST flag it (teeth).
9// expect_exit: 0 license_tier: ORIGINAL
10import "nx_syscalls.nx"
11import "nx_media_budget.nx"
12
13func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw("
14" as *u8); return ok }
15func gn(v: i64) -> i64 {
16 let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m}
17 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}
18 var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
19
20// check plan B is quality-GE plan A on every axis (B from a budget >= A's budget). returns 1 ok / 0 violated.
21func plan_ge(a: *i64, b: *i64) -> i64 {
22 if b[0] < a[0] { return 0 } // fps up
23 if b[1] < a[1] { return 0 } // height up
24 if b[2] > a[2] { return 0 } // qp down (better)
25 if b[3] < a[3] { return 0 } // audio rate up
26 if b[4] < a[4] { return 0 } // lossless up
27 if b[5] > a[5] { return 0 } // gpu_detail down (better)
28 if b[6] < a[6] { return 0 } // kbps up
29 if b[7] < a[7] { return 0 } // tier up
30 return 1
31}
32
33func main() -> i64 {
34 gw("=== nx_media_budget_gate: resource-intelligence MONOTONE + ENVELOPE-SAFE ===\n" as *u8)
35 var bad: i64 = 0
36 let pa: *i64 = sys_mmap(128) as *i64
37 let pb: *i64 = sys_mmap(128) as *i64
38
39 // 1. MONOTONE in cpu_class (generous other inputs so cpu binds)
40 var c: i64 = 1
41 mb_plan(0, 20000, 101, 2, pa)
42 while c <= 9 {
43 mb_plan(c, 20000, 101, 2, pb)
44 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-CPU violation at class " as *u8); gn(c); gw("\n" as *u8) }
45 var i: i64 = 0
46 while i < 8 { pa[i] = pb[i]; i = i + 1 }
47 c = c + 1
48 }
49 // 2. MONOTONE in uplink (cpu/battery generous, peers=4 so bandwidth binds meaningfully)
50 var u: i64 = 100
51 mb_plan(9, 100, 101, 4, pa)
52 while u <= 20000 {
53 mb_plan(9, u, 101, 4, pb)
54 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-UPLINK violation at " as *u8); gn(u); gw("kbps\n" as *u8) }
55 var i: i64 = 0
56 while i < 8 { pa[i] = pb[i]; i = i + 1 }
57 u = u + 300
58 }
59 // 3. MONOTONE in battery
60 let batts: *i64 = sys_mmap(64) as *i64
61 batts[0]=5; batts[1]=15; batts[2]=30; batts[3]=50; batts[4]=80; batts[5]=101
62 mb_plan(9, 20000, 5, 2, pa)
63 var bi: i64 = 1
64 while bi < 6 {
65 mb_plan(9, 20000, batts[bi], 2, pb)
66 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-BATTERY violation at " as *u8); gn(batts[bi]); gw("%\n" as *u8) }
67 var i: i64 = 0
68 while i < 8 { pa[i] = pb[i]; i = i + 1 }
69 bi = bi + 1
70 }
71 if bad == 0 { gw(" MONOTONE: PASS across cpu/uplink/battery sweeps (no quality inversion)\n" as *u8) }
72
73 // 4. ENVELOPE-SAFE grid: plan kbps x fanout never exceeds ceiling or uplink
74 var env_bad: i64 = 0
75 let ceil: i64 = mb_edge_ceil_kbps()
76 var peers: i64 = 1
77 while peers <= 8 {
78 var up: i64 = 100
79 while up <= 20000 {
80 mb_plan(9, up, 101, peers, pb)
81 var fanout: i64 = peers - 1
82 if fanout < 1 { fanout = 1 }
83 // the safety property applies ONLY when video is on; video_on=0 = audio-only (nothing to breach).
84 if pb[8] == 1 {
85 if pb[6] * fanout > ceil { env_bad = env_bad + 1; gw(" ENVELOPE breach: peers=" as *u8); gn(peers); gw(" up=" as *u8); gn(up); gw(" kbps=" as *u8); gn(pb[6]); gw(" x" as *u8); gn(fanout); gw(">ceil\n" as *u8) }
86 if pb[6] > up { env_bad = env_bad + 1; gw(" UPLINK breach: peers=" as *u8); gn(peers); gw(" up=" as *u8); gn(up); gw(" kbps=" as *u8); gn(pb[6]); gw("\n" as *u8) }
87 }
88 up = up + 250
89 }
90 peers = peers + 1
91 }
92 if env_bad == 0 { gw(" ENVELOPE-SAFE: PASS -- plan x fan-out within the measured " as *u8); gn(ceil); gw("kbps ceiling AND uplink for all peers/up\n" as *u8) }
93
94 // 5. FLOOR/CEILING
95 mb_plan(0, 50, 5, 6, pa) // starved everything
96 mb_plan(9, 20000, 101, 2, pb) // rich, small room
97 gw(" FLOOR (starved): tier=" as *u8); gn(pa[7]); gw(" fps=" as *u8); gn(pa[0]); gw(" h=" as *u8); gn(pa[1]); gw(" arate=" as *u8); gn(pa[3]); gw("\n" as *u8)
98 gw(" CEILING (rich, 2-peer): tier=" as *u8); gn(pb[7]); gw(" fps=" as *u8); gn(pb[0]); gw(" h=" as *u8); gn(pb[1]); gw(" arate=" as *u8); gn(pb[3]); gw(" lossless=" as *u8); gn(pb[4]); gw("\n" as *u8)
99 var fc_bad: i64 = 0
100 if pa[7] != 0 { fc_bad = fc_bad + 1 }
101 if pb[7] != 9 { fc_bad = fc_bad + 1 }
102 if pb[0] != 60 { fc_bad = fc_bad + 1 }
103 if pb[3] != 192000 { fc_bad = fc_bad + 1 }
104 if fc_bad == 0 { gw(" FLOOR/CEILING: PASS (floor=tier0, ceiling=tier9 60fps/1080/192k)\n" as *u8) }
105
106 // 5b. AUDIO-ONLY scale-down: a pipe too small even for the floor tier drops video, keeps audio.
107 mb_plan(9, 50, 101, 2, pa) // 50kbps < 110kbps floor -> video must drop
108 mb_plan(9, 20000, 101, 2, pb) // rich -> video on
109 gw(" AUDIO-ONLY (50kbps pipe): video_on=" as *u8); gn(pa[8]); gw(" audio_rate=" as *u8); gn(pa[3]); gw(" (audio survives)\n" as *u8)
110 var ao_bad: i64 = 0
111 if pa[8] != 0 { ao_bad = ao_bad + 1 } // must be audio-only
112 if pa[3] <= 0 { ao_bad = ao_bad + 1 } // audio still present
113 if pb[8] != 1 { ao_bad = ao_bad + 1 } // rich pipe keeps video
114 if ao_bad == 0 { gw(" AUDIO-ONLY scale-down: PASS (video sheds before audio under extreme scarcity)\n" as *u8) }
115
116 // 6. NEG-CONTROL: the monotone checker must FLAG an inverted sequence (proves teeth)
117 let inv_a: *i64 = sys_mmap(128) as *i64
118 let inv_b: *i64 = sys_mmap(128) as *i64
119 var z: i64 = 0
120 while z < 8 { inv_a[z] = 30; inv_b[z] = 30; z = z + 1 }
121 inv_b[0] = 20 // fps DROPPED while "budget rose" -> a real inversion
122 var neg_ok: i64 = 0
123 if plan_ge(inv_a, inv_b) == 0 { neg_ok = 1 }
124 if neg_ok == 1 { gw(" NEG-CONTROL: PASS (checker catches a planted fps inversion)\n" as *u8) } else { bad = bad + 1; gw(" NEG-CONTROL: FAIL -- checker is blind, monotone results are meaningless\n" as *u8) }
125
126 var green: i64 = 1
127 if bad != 0 { green = 0 }
128 if env_bad != 0 { green = 0 }
129 if fc_bad != 0 { green = 0 }
130 if ao_bad != 0 { green = 0 }
131 if neg_ok != 1 { green = 0 }
132 if green == 1 { gw("MEDIA-BUDGET-GATE verdict=GREEN -- the resource-intelligence policy is monotone + envelope-safe (proven)\n" as *u8); return 0 }
133 gw("MEDIA-BUDGET-GATE verdict=RED\n" as *u8)
134 return 1
135}