code wiki / _hdl_build / nx_media_budget_gate.nx
nx_media_budget_gate.nx source
↩ module page · 142 lines · 7603 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"
12import "nx_gate_verdict.nx"
13
14func grow(name: *u8, ok: i64) -> i64 { if ok==1 { gw(" PASS " as *u8) } else { gw(" FAIL " as *u8) } gw(name); gw("
15" as *u8); return ok }
16func gn(v: i64) -> i64 {
17 let b: *u8=sys_mmap(28); var m: i64=v; if m<0{sys_write(1,"-" as *u8,1);m=0-m}
18 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}
19 var i: i64=0; while i<k{b[i]=t[k-1-i];i=i+1} sys_write(1,b,k); return 0 }
20
21// check plan B is quality-GE plan A on every axis (B from a budget >= A's budget). returns 1 ok / 0 violated.
22func plan_ge(a: *i64, b: *i64) -> i64 {
23 if b[0] < a[0] { return 0 } // fps up
24 if b[1] < a[1] { return 0 } // height up
25 if b[2] > a[2] { return 0 } // qp down (better)
26 if b[3] < a[3] { return 0 } // audio rate up
27 if b[4] < a[4] { return 0 } // lossless up
28 if b[5] > a[5] { return 0 } // gpu_detail down (better)
29 if b[6] < a[6] { return 0 } // kbps up
30 if b[7] < a[7] { return 0 } // tier up
31 return 1
32}
33
34func main() -> i64 {
35 gw("=== nx_media_budget_gate: resource-intelligence MONOTONE + ENVELOPE-SAFE ===\n" as *u8)
36 var bad: i64 = 0
37 let pa: *i64 = sys_mmap(128) as *i64
38 let pb: *i64 = sys_mmap(128) as *i64
39
40 // 1. MONOTONE in cpu_class (generous other inputs so cpu binds)
41 var c: i64 = 1
42 mb_plan(0, 20000, 101, 2, pa)
43 while c <= 9 {
44 mb_plan(c, 20000, 101, 2, pb)
45 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-CPU violation at class " as *u8); gn(c); gw("\n" as *u8) }
46 var i: i64 = 0
47 while i < 8 { pa[i] = pb[i]; i = i + 1 }
48 c = c + 1
49 }
50 // 2. MONOTONE in uplink (cpu/battery generous, peers=4 so bandwidth binds meaningfully)
51 var u: i64 = 100
52 mb_plan(9, 100, 101, 4, pa)
53 while u <= 20000 {
54 mb_plan(9, u, 101, 4, pb)
55 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-UPLINK violation at " as *u8); gn(u); gw("kbps\n" as *u8) }
56 var i: i64 = 0
57 while i < 8 { pa[i] = pb[i]; i = i + 1 }
58 u = u + 300
59 }
60 // 3. MONOTONE in battery
61 let batts: *i64 = sys_mmap(64) as *i64
62 batts[0]=5; batts[1]=15; batts[2]=30; batts[3]=50; batts[4]=80; batts[5]=101
63 mb_plan(9, 20000, 5, 2, pa)
64 var bi: i64 = 1
65 while bi < 6 {
66 mb_plan(9, 20000, batts[bi], 2, pb)
67 if plan_ge(pa, pb) == 0 { bad = bad + 1; gw(" MONO-BATTERY violation at " as *u8); gn(batts[bi]); gw("%\n" as *u8) }
68 var i: i64 = 0
69 while i < 8 { pa[i] = pb[i]; i = i + 1 }
70 bi = bi + 1
71 }
72 if bad == 0 { gw(" MONOTONE: PASS across cpu/uplink/battery sweeps (no quality inversion)\n" as *u8) }
73
74 // 4. ENVELOPE-SAFE grid: plan kbps x fanout never exceeds ceiling or uplink
75 var env_bad: i64 = 0
76 let ceil: i64 = mb_edge_ceil_kbps()
77 var peers: i64 = 1
78 while peers <= 8 {
79 var up: i64 = 100
80 while up <= 20000 {
81 mb_plan(9, up, 101, peers, pb)
82 var fanout: i64 = peers - 1
83 if fanout < 1 { fanout = 1 }
84 // the safety property applies ONLY when video is on; video_on=0 = audio-only (nothing to breach).
85 if pb[8] == 1 {
86 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) }
87 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) }
88 }
89 up = up + 250
90 }
91 peers = peers + 1
92 }
93 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) }
94
95 // 5. FLOOR/CEILING
96 mb_plan(0, 50, 5, 6, pa) // starved everything
97 mb_plan(9, 20000, 101, 2, pb) // rich, small room
98 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)
99 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)
100 var fc_bad: i64 = 0
101 if pa[7] != 0 { fc_bad = fc_bad + 1 }
102 if pb[7] != 9 { fc_bad = fc_bad + 1 }
103 if pb[0] != 60 { fc_bad = fc_bad + 1 }
104 if pb[3] != 192000 { fc_bad = fc_bad + 1 }
105 if fc_bad == 0 { gw(" FLOOR/CEILING: PASS (floor=tier0, ceiling=tier9 60fps/1080/192k)\n" as *u8) }
106
107 // 5b. AUDIO-ONLY scale-down: a pipe too small even for the floor tier drops video, keeps audio.
108 mb_plan(9, 50, 101, 2, pa) // 50kbps < 110kbps floor -> video must drop
109 mb_plan(9, 20000, 101, 2, pb) // rich -> video on
110 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)
111 var ao_bad: i64 = 0
112 if pa[8] != 0 { ao_bad = ao_bad + 1 } // must be audio-only
113 if pa[3] <= 0 { ao_bad = ao_bad + 1 } // audio still present
114 if pb[8] != 1 { ao_bad = ao_bad + 1 } // rich pipe keeps video
115 if ao_bad == 0 { gw(" AUDIO-ONLY scale-down: PASS (video sheds before audio under extreme scarcity)\n" as *u8) }
116
117 // 6. NEG-CONTROL: the monotone checker must FLAG an inverted sequence (proves teeth)
118 let inv_a: *i64 = sys_mmap(128) as *i64
119 let inv_b: *i64 = sys_mmap(128) as *i64
120 var z: i64 = 0
121 while z < 8 { inv_a[z] = 30; inv_b[z] = 30; z = z + 1 }
122 inv_b[0] = 20 // fps DROPPED while "budget rose" -> a real inversion
123 var neg_ok: i64 = 0
124 if plan_ge(inv_a, inv_b) == 0 { neg_ok = 1 }
125 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) }
126
127 var green: i64 = 1
128 if bad != 0 { green = 0 }
129 if env_bad != 0 { green = 0 }
130 if fc_bad != 0 { green = 0 }
131 if ao_bad != 0 { green = 0 }
132 if neg_ok != 1 { green = 0 }
133 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
134 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
135 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
136 let ctr__dry: *i64 = gv_ctr()
137 ctr__dry[0] = green
138 ctr__dry[1] = 1
139 let rc__dry: i64 = gv_verdict("MEDIA-BUDGET-GATE" as *u8, ctr__dry, "the resource-intelligence policy is monotone + envelope-safe (proven)" as *u8)
140 sys_exit(rc__dry)
141 return rc__dry
142}