nx_vp8_gate.nx source
↩ module page · 187 lines · 8202 B
1// nx_vp8_gate.nx -- proves the VP8 boolean decoder and keyframe header.
2//
3// T2 is the one that validates the whole entropy engine without needing an
4// encoder: at probability 128 the split lands exactly at the midpoint, so the
5// coder degenerates to reading the stream MSB-first. Decoding 128 prob-128
6// bits must therefore reproduce the raw bits of the input bytes EXACTLY. Any
7// error in the shift, the carry or the 8-bit byte refill breaks it on the
8// first refill boundary.
9//
10// T3 asserts the RANGE INVARIANT after every single decode: 128 <= range <=
11// 255. A renormalisation loop that under- or over-shifts returns plausible
12// bits for a while and then diverges, so checking the invariant per call
13// catches it at the first bit rather than the thousandth.
14//
15// T6 pins the mandatory start code. Without it a corrupt or non-VP8 payload
16// decodes as a frame with dimensions read out of arbitrary bytes.
17//
18// license_tier: ORIGINAL
19import "nx_syscalls.nx"
20import "nx_vp8.nx"
21
22func g_puts(s: *u8) -> i64 {
23 var i: i64 = 0
24 while s[i] != (0 as u8) { i = i + 1 }
25 sys_write(1, s, i)
26 return i
27}
28
29func g_putn(v: i64) -> i64 {
30 let buf: *u8 = sys_mmap(32)
31 var x: i64 = v
32 if x < 0 { g_puts("-" as *u8); x = 0 - x }
33 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
34 let tmp: *u8 = sys_mmap(32)
35 var d: i64 = 0
36 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
37 var i: i64 = 0
38 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
39 sys_write(1, buf, d)
40 return d
41}
42
43func main() -> i64 {
44 var fails: i64 = 0
45 var mark: i64 = 0
46
47 // ---- T1: the decoder initialises with range 255 ----
48 let d: *u8 = sys_mmap(256)
49 var i: i64 = 0
50 while i < 64 { d[i] = ((i * 37 + 11) & 255) as u8; i = i + 1 }
51 let b0: *NxVp8Bool = nx_vp8_bool_init(d, 64, 0)
52 if b0 == (0 as *NxVp8Bool) { fails = fails + 1 } else {
53 if b0.range != 255 { fails = fails + 1 }
54 if b0.overflow != 0 { fails = fails + 1 }
55 }
56 // a buffer too short to prime the value register is refused
57 if nx_vp8_bool_init(d, 1, 0) != (0 as *NxVp8Bool) { fails = fails + 1 }
58 if fails > 0 { if mark == 0 { mark = 1 } }
59
60 // ---- T2: prob-128 bits ARE the raw stream bits, MSB-first ----
61 let b1: *NxVp8Bool = nx_vp8_bool_init(d, 64, 0)
62 var bad: i64 = 0
63 var n: i64 = 0
64 while n < 128 {
65 let expect: i64 = (nx_vp8_at(d, n >> 3) >> (7 - (n & 7))) & 1
66 let got: i64 = nx_vp8_bool_bit(b1)
67 if got != expect { bad = bad + 1 }
68 n = n + 1
69 }
70 if bad != 0 { fails = fails + 1 }
71 if fails > 0 { if mark == 0 { mark = 2 } }
72
73 // ---- T3: the RANGE INVARIANT holds after EVERY decode ----
74 let b2: *NxVp8Bool = nx_vp8_bool_init(d, 64, 0)
75 var inv_bad: i64 = 0
76 var probs: *i64 = sys_mmap(64) as *i64
77 probs[0] = 1; probs[1] = 2; probs[2] = 64; probs[3] = 128
78 probs[4] = 200; probs[5] = 254; probs[6] = 255; probs[7] = 100
79 n = 0
80 while n < 300 {
81 nx_vp8_bool_get(b2, probs[n % 8])
82 if b2.range < 128 { inv_bad = inv_bad + 1 }
83 if b2.range > 255 { inv_bad = inv_bad + 1 }
84 if b2.value < 0 { inv_bad = inv_bad + 1 }
85 if b2.value > 65535 { inv_bad = inv_bad + 1 }
86 n = n + 1
87 }
88 if inv_bad != 0 { fails = fails + 1 }
89 if fails > 0 { if mark == 0 { mark = 3 } }
90
91 // ---- T4: multi-bit literals compose from single bits ----
92 let b3: *NxVp8Bool = nx_vp8_bool_init(d, 64, 0)
93 let lit: i64 = nx_vp8_bool_literal(b3, 8)
94 // the first eight prob-128 bits are the first byte, MSB-first
95 if lit != nx_vp8_at(d, 0) { fails = fails + 1 }
96 let lit2: i64 = nx_vp8_bool_literal(b3, 16)
97 if lit2 != ((nx_vp8_at(d, 1) << 8) | nx_vp8_at(d, 2)) { fails = fails + 1 }
98 // out-of-range widths are refused
99 if nx_vp8_bool_literal(b3, 0) != 0 { fails = fails + 1 }
100 if nx_vp8_bool_literal(b3, 33) != 0 { fails = fails + 1 }
101 if fails > 0 { if mark == 0 { mark = 4 } }
102
103 // ---- T5: signed values are magnitude then sign ----
104 // craft a stream whose bits are 0000_0011 -> literal(3)=0, sign=0 ... use
105 // an explicit pattern so the expected value is unambiguous
106 let s: *u8 = sys_mmap(64)
107 s[0] = 0xb0 as u8 // 1011 0000
108 s[1] = 0x00 as u8
109 s[2] = 0x00 as u8
110 let b4: *NxVp8Bool = nx_vp8_bool_init(s, 3, 0)
111 // literal(3) reads 101 = 5, then the sign bit reads 1 -> negative
112 if nx_vp8_bool_signed(b4, 3) != (0 - 5) { fails = fails + 1 }
113 // next: flag bit reads 0 -> the optional value is absent, returns 0
114 if nx_vp8_bool_maybe_signed(b4, 4) != 0 { fails = fails + 1 }
115 if fails > 0 { if mark == 0 { mark = 5 } }
116
117 // ---- T6: the keyframe header round-trips ----
118 let f: *u8 = sys_mmap(64)
119 let fl: *i64 = sys_mmap(128) as *i64
120 let dims: *i64 = sys_mmap(64) as *i64
121 dims[0]=1; dims[1]=1; dims[2]=640; dims[3]=480
122 dims[4]=1920; dims[5]=1080; dims[6]=16383; dims[7]=16383
123 var k: i64 = 0
124 while k < 4 {
125 let ww: i64 = dims[k*2]
126 let hh: i64 = dims[k*2+1]
127 if nx_vp8_frame_write(f, 64, ww, hh, 1, 2, 12345) != 10 { fails = fails + 1 } else {
128 if nx_vp8_frame_parse(f, 10, fl) != 1 { fails = fails + 1 } else {
129 if fl[NX_VP8_FLD_KEYFRAME] != 1 { fails = fails + 1 }
130 if fl[NX_VP8_FLD_SHOW] != 1 { fails = fails + 1 }
131 if fl[NX_VP8_FLD_WIDTH] != ww { fails = fails + 1 }
132 if fl[NX_VP8_FLD_HEIGHT] != hh { fails = fails + 1 }
133 if fl[NX_VP8_FLD_HSCALE] != 1 { fails = fails + 1 }
134 if fl[NX_VP8_FLD_VSCALE] != 2 { fails = fails + 1 }
135 if fl[NX_VP8_FLD_PART1LEN] != 12345 { fails = fails + 1 }
136 if fl[NX_VP8_FLD_HDRLEN] != 10 { fails = fails + 1 }
137 }
138 }
139 k = k + 1
140 }
141 if fails > 0 { if mark == 0 { mark = 6 } }
142
143 // ---- T7 NEG: the start code is MANDATORY ----
144 nx_vp8_frame_write(f, 64, 640, 480, 0, 0, 100)
145 f[3] = 0x9e as u8
146 if nx_vp8_frame_parse(f, 10, fl) != 0 { fails = fails + 1 }
147 f[3] = 0x9d as u8
148 f[5] = 0x2b as u8
149 if nx_vp8_frame_parse(f, 10, fl) != 0 { fails = fails + 1 }
150 f[5] = 0x2a as u8
151 if nx_vp8_frame_parse(f, 10, fl) != 1 { fails = fails + 1 }
152 // a truncated keyframe header
153 if nx_vp8_frame_parse(f, 6, fl) != 0 { fails = fails + 1 }
154 // zero dimensions in the stream are refused
155 f[6] = 0x00 as u8; f[7] = 0x00 as u8
156 if nx_vp8_frame_parse(f, 10, fl) != 0 { fails = fails + 1 }
157 // out-of-range writer arguments
158 if nx_vp8_frame_write(f, 64, 16384, 100, 0, 0, 0) != 0 { fails = fails + 1 }
159 if nx_vp8_frame_write(f, 64, 100, 100, 4, 0, 0) != 0 { fails = fails + 1 }
160 if nx_vp8_frame_write(f, 5, 100, 100, 0, 0, 0) != 0 { fails = fails + 1 }
161 if fails > 0 { if mark == 0 { mark = 7 } }
162
163 // ---- T8: an interframe tag carries no dimensions and a 3-byte header ----
164 let inter: *u8 = sys_mmap(64)
165 inter[0] = 0x01 as u8 // frame_type bit set = interframe
166 inter[1] = 0x00 as u8
167 inter[2] = 0x00 as u8
168 if nx_vp8_frame_parse(inter, 3, fl) != 1 { fails = fails + 1 } else {
169 if fl[NX_VP8_FLD_KEYFRAME] != 0 { fails = fails + 1 }
170 if fl[NX_VP8_FLD_HDRLEN] != 3 { fails = fails + 1 }
171 if fl[NX_VP8_FLD_WIDTH] != 0 { fails = fails + 1 }
172 }
173 if fails > 0 { if mark == 0 { mark = 8 } }
174
175 if fails == 0 {
176 g_puts("GATE nx_vp8 verdict=GREEN pass=8/8 (bool decoder inits at range 255, short buffer refused; PROB-128 LITERALS REPRODUCE 128 RAW STREAM BITS EXACTLY across 16 byte-refill boundaries; RANGE INVARIANT 128..255 and value 0..65535 held after all 300 decodes at 8 probabilities incl 1 and 255; 8- and 16-bit literals compose; signed magnitude-then-sign and the optional-flag form; keyframe header round-trip at 1x1 and 16383x16383 with scales; NEG start-code both bytes/truncated/zero-dims/oversize-args refused; interframe gives a 3-byte header and no dimensions)\n" as *u8)
177 sys_exit(0)
178 return 0
179 }
180 g_puts("GATE nx_vp8 verdict=RED fails=" as *u8)
181 g_putn(fails)
182 g_puts(" first_stage=" as *u8)
183 g_putn(mark)
184 g_puts("\n" as *u8)
185 sys_exit(1)
186 return 1
187}