nx_webp_alpha_gate.nx source
↩ module page · 201 lines · 8842 B
1// nx_webp_alpha_gate.nx -- proves VP8X + ALPH by exact filter ROUND-TRIP.
2//
3// T3 runs all four filters over pseudo-random alpha planes at several shapes
4// and requires the filtered-then-unfiltered plane to be byte-identical. A
5// filter pair that disagrees anywhere -- including only at the edges -- fails.
6//
7// T4 pins the EDGE PREDICTION explicitly. Horizontal predicts the first
8// column from ABOVE and vertical predicts the first row from the LEFT. Using
9// the nominal direction at an edge reads outside the plane; substituting zero
10// leaves the interior correct and both edges wrong, which reads as a subtle
11// halo rather than a decode failure. The test uses a 1-pixel-wide and a
12// 1-pixel-tall plane, where the whole image IS the edge case.
13//
14// T5 pins the gradient clamp ORDER: clamp(left + top - topleft) to 0..255,
15// THEN add the residual modulo 256. It uses values that deliberately
16// overshoot both ends, since that is the only place the orders differ.
17//
18// license_tier: ORIGINAL
19import "nx_syscalls.nx"
20import "nx_webp_alpha.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 VP8X chunk round-trips, incl. the minus-one dimensions ----
48 let vb: *u8 = sys_mmap(256)
49 let vf: *i64 = sys_mmap(128) as *i64
50 let dims: *i64 = sys_mmap(128) as *i64
51 dims[0]=1; dims[1]=1; dims[2]=16; dims[3]=16
52 dims[4]=1920; dims[5]=1080; dims[6]=16777216; dims[7]=16777216
53 var k: i64 = 0
54 while k < 4 {
55 let ww: i64 = dims[k*2]
56 let hh: i64 = dims[k*2+1]
57 if nx_vp8x_write(vb, 256, NX_VP8X_FLAG_ALPHA, ww, hh) != 18 { fails = fails + 1 } else {
58 if nx_vp8x_parse(vb, 256, 0, vf) != 1 { fails = fails + 1 } else {
59 if vf[NX_VP8X_FLD_WIDTH] != ww { fails = fails + 1 }
60 if vf[NX_VP8X_FLD_HEIGHT] != hh { fails = fails + 1 }
61 if nx_vp8x_has_alpha(vf[NX_VP8X_FLD_FLAGS]) != 1 { fails = fails + 1 }
62 }
63 }
64 k = k + 1
65 }
66 // without the alpha flag, has_alpha must be false
67 nx_vp8x_write(vb, 256, NX_VP8X_FLAG_ANIM, 100, 100)
68 nx_vp8x_parse(vb, 256, 0, vf)
69 if nx_vp8x_has_alpha(vf[NX_VP8X_FLD_FLAGS]) != 0 { fails = fails + 1 }
70 if fails > 0 { if mark == 0 { mark = 1 } }
71
72 // ---- T2: the ALPH header byte ----
73 let af: *i64 = sys_mmap(128) as *i64
74 let hb: i64 = nx_alph_build_header(0, NX_ALPH_FILTER_GRAD, 1)
75 if hb < 0 { fails = fails + 1 } else {
76 if nx_alph_parse_header(hb, af) != 1 { fails = fails + 1 } else {
77 if af[NX_ALPH_FLD_FILTER] != NX_ALPH_FILTER_GRAD { fails = fails + 1 }
78 if af[NX_ALPH_FLD_COMPRESS] != 1 { fails = fails + 1 }
79 if af[NX_ALPH_FLD_PREPROC] != 0 { fails = fails + 1 }
80 }
81 }
82 // the two top bits are reserved and must be zero
83 if nx_alph_parse_header(0x80, af) != 0 { fails = fails + 1 }
84 if nx_alph_parse_header(0x40, af) != 0 { fails = fails + 1 }
85 // an out-of-range compression method is refused
86 if nx_alph_build_header(0, 0, 2) != (0 - 1) { fails = fails + 1 }
87 if nx_alph_build_header(0, 4, 0) != (0 - 1) { fails = fails + 1 }
88 if fails > 0 { if mark == 0 { mark = 2 } }
89
90 // ---- T3: ALL FOUR filters round-trip exactly, at several shapes ----
91 let shapes: *i64 = sys_mmap(128) as *i64
92 shapes[0]=1; shapes[1]=1
93 shapes[2]=1; shapes[3]=8 // one pixel wide -- all edge
94 shapes[4]=8; shapes[5]=1 // one pixel tall -- all edge
95 shapes[6]=7; shapes[7]=5 // odd dimensions
96 shapes[8]=16; shapes[9]=16
97 shapes[10]=32; shapes[11]=17
98
99 let src: *u8 = sys_mmap(4096)
100 let enc: *u8 = sys_mmap(4096)
101 let dec: *u8 = sys_mmap(4096)
102 var seed: i64 = 777
103 var si: i64 = 0
104 var rt_bad: i64 = 0
105 while si < 6 {
106 let w: i64 = shapes[si*2]
107 let h: i64 = shapes[si*2+1]
108 var fi: i64 = 0
109 while fi < 4 {
110 var i: i64 = 0
111 while i < w * h {
112 seed = (seed * 1103515245 + 12345) & 0x7fffffff
113 src[i] = ((seed >> 7) & 255) as u8
114 i = i + 1
115 }
116 if nx_alph_filter(src, enc, w, h, fi) != 1 { fails = fails + 1 } else {
117 if nx_alph_unfilter(enc, dec, w, h, fi) != 1 { fails = fails + 1 } else {
118 i = 0
119 while i < w * h {
120 if (dec[i] as i64 & 255) != (src[i] as i64 & 255) { rt_bad = rt_bad + 1 }
121 i = i + 1
122 }
123 }
124 }
125 fi = fi + 1
126 }
127 si = si + 1
128 }
129 if rt_bad != 0 { fails = fails + 1 }
130 if fails > 0 { if mark == 0 { mark = 3 } }
131
132 // ---- T4: the EDGE prediction directions, asserted explicitly ----
133 // a 2x2 plane, horizontal filter: the first column comes from ABOVE
134 let s4: *u8 = sys_mmap(64)
135 let e4: *u8 = sys_mmap(64)
136 s4[0] = 10 as u8; s4[1] = 30 as u8
137 s4[2] = 50 as u8; s4[3] = 90 as u8
138 nx_alph_filter(s4, e4, 2, 2, NX_ALPH_FILTER_HORIZ)
139 // residual[0] is the raw value
140 if (e4[0] as i64 & 255) != 10 { fails = fails + 1 }
141 // first row predicts from the LEFT: 30 - 10
142 if (e4[1] as i64 & 255) != 20 { fails = fails + 1 }
143 // first COLUMN of row 1 predicts from ABOVE: 50 - 10
144 if (e4[2] as i64 & 255) != 40 { fails = fails + 1 }
145 // interior predicts from the left: 90 - 50
146 if (e4[3] as i64 & 255) != 40 { fails = fails + 1 }
147
148 // the same plane, vertical filter: interior predicts from ABOVE
149 nx_alph_filter(s4, e4, 2, 2, NX_ALPH_FILTER_VERT)
150 if (e4[1] as i64 & 255) != 20 { fails = fails + 1 } // first row still LEFT
151 if (e4[3] as i64 & 255) != 60 { fails = fails + 1 } // 90 - 30, from above
152 if fails > 0 { if mark == 0 { mark = 4 } }
153
154 // ---- T5: the gradient predictor CLAMPS BEFORE ADDING ----
155 // left=250 top=250 topleft=10 -> raw 490, clamped to 255
156 let s5: *u8 = sys_mmap(64)
157 let e5: *u8 = sys_mmap(64)
158 let d5: *u8 = sys_mmap(64)
159 s5[0] = 10 as u8; s5[1] = 250 as u8
160 s5[2] = 250 as u8; s5[3] = 200 as u8
161 nx_alph_filter(s5, e5, 2, 2, NX_ALPH_FILTER_GRAD)
162 // residual = 200 - clamp(250 + 250 - 10) = 200 - 255 = -55 -> 201 mod 256
163 if (e5[3] as i64 & 255) != 201 { fails = fails + 1 }
164 nx_alph_unfilter(e5, d5, 2, 2, NX_ALPH_FILTER_GRAD)
165 if (d5[3] as i64 & 255) != 200 { fails = fails + 1 }
166 // and the negative overshoot: left=5 top=5 topleft=250 -> raw -240 -> 0
167 s5[0] = 250 as u8; s5[1] = 5 as u8
168 s5[2] = 5 as u8; s5[3] = 77 as u8
169 nx_alph_filter(s5, e5, 2, 2, NX_ALPH_FILTER_GRAD)
170 if (e5[3] as i64 & 255) != 77 { fails = fails + 1 }
171 nx_alph_unfilter(e5, d5, 2, 2, NX_ALPH_FILTER_GRAD)
172 if (d5[3] as i64 & 255) != 77 { fails = fails + 1 }
173 if fails > 0 { if mark == 0 { mark = 5 } }
174
175 // ---- T6 NEG: refusals ----
176 if nx_vp8x_write(vb, 256, 0, 0, 100) != 0 { fails = fails + 1 }
177 if nx_vp8x_write(vb, 256, 0, 100, 0) != 0 { fails = fails + 1 }
178 if nx_vp8x_write(vb, 10, 0, 100, 100) != 0 { fails = fails + 1 }
179 if nx_alph_unfilter(src, dec, 0, 8, 0) != 0 { fails = fails + 1 }
180 if nx_alph_unfilter(src, dec, 8, 8, 4) != 0 { fails = fails + 1 }
181 // a VP8X chunk whose declared payload size is not ten
182 nx_vp8x_write(vb, 256, NX_VP8X_FLAG_ALPHA, 64, 64)
183 vb[4] = 9 as u8
184 if nx_vp8x_parse(vb, 256, 0, vf) != 0 { fails = fails + 1 }
185 vb[4] = 10 as u8
186 if nx_vp8x_parse(vb, 256, 0, vf) != 1 { fails = fails + 1 }
187 if fails > 0 { if mark == 0 { mark = 6 } }
188
189 if fails == 0 {
190 g_puts("GATE nx_webp_alpha verdict=GREEN pass=6/6 (VP8X round-trip incl minus-one dims at 1x1 and 16777216, alpha flag; ALPH header with reserved bits enforced; ALL FOUR filters round-trip byte-exact over 6 shapes incl 1-wide and 1-tall where the whole plane is edge; EDGE directions asserted -- horizontal takes the first column from ABOVE, vertical takes the first row from LEFT; gradient CLAMPS BEFORE ADDING proven at both overshoot ends; NEG zero-dims/small-buffer/bad-filter/bad-chunk-size refused)\n" as *u8)
191 sys_exit(0)
192 return 0
193 }
194 g_puts("GATE nx_webp_alpha verdict=RED fails=" as *u8)
195 g_putn(fails)
196 g_puts(" first_stage=" as *u8)
197 g_putn(mark)
198 g_puts("\n" as *u8)
199 sys_exit(1)
200 return 1
201}