nx_webp_huff_gate.nx source
↩ module page · 127 lines · 5085 B
1// nx_webp_huff_gate.nx -- proves the VP8L Huffman code-group reader.
2//
3// The property that matters most is T2/T3: a single-symbol tree must decode
4// its symbol while consuming ZERO bits. Every other Huffman path in the tree
5// consumes at least one bit per symbol, so if this collapses to an ordinary
6// canonical table the bitstream desyncs one bit at a time and the image
7// decodes to noise -- silently, with no error anywhere. Constant-alpha and
8// constant-red images (most synthetic PNG-to-WebP conversions) hit this on
9// the very first tree.
10//
11// NON-VACUITY: T8/T9/T10 are negative controls. An all-zero length vector, a
12// null tree and an out-of-range simple symbol must each be REFUSED. If this
13// gate cannot fail it is not measuring anything -- flipping the T8
14// expectation to == 0 must turn it RED.
15//
16// license_tier: ORIGINAL
17import "nx_syscalls.nx"
18import "nx_bitstream.nx"
19import "nx_huffman.nx"
20import "nx_webp_huff.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 main() -> i64 {
30 var fails: i64 = 0
31
32 // ---- T1: a one-symbol length vector collapses to the trivial form ----
33 let l1: *i64 = sys_mmap(5 * 8 + 64) as *i64
34 var i: i64 = 0
35 while i < 5 { l1[i] = 0; i = i + 1 }
36 l1[2] = 1
37 let t1: *NxWlTree = wl_tree_from_lengths(l1, 5)
38 if t1 == (0 as *NxWlTree) { fails = fails + 1 } else {
39 if t1.trivial != 1 { fails = fails + 1 }
40 }
41
42 // ---- T2: the trivial tree returns the right symbol ----
43 let buf: *u8 = sys_mmap(64)
44 buf[0] = 0xff as u8; buf[1] = 0xff as u8; buf[2] = 0xff as u8
45 let bs2: *NxBitStream = nx_bitstream_alloc(buf, 3)
46 if wl_decode_symbol(t1, bs2) != 2 { fails = fails + 1 }
47
48 // ---- T3: ...and consumed ZERO bits doing it (the headline property) ----
49 if bs2.byte_pos != 0 { fails = fails + 1 }
50 if bs2.bit_pos != 0 { fails = fails + 1 }
51
52 // ---- T4: a two-symbol vector does NOT collapse ----
53 let l2: *i64 = sys_mmap(5 * 8 + 64) as *i64
54 i = 0
55 while i < 5 { l2[i] = 0; i = i + 1 }
56 l2[0] = 1
57 l2[1] = 1
58 let t2: *NxWlTree = wl_tree_from_lengths(l2, 5)
59 if t2 == (0 as *NxWlTree) { fails = fails + 1 } else {
60 if t2.trivial != 0 { fails = fails + 1 }
61 }
62
63 // ---- T5: canonical assignment -- bit 0 -> symbol 0, bit 1 -> symbol 1 ----
64 let z: *u8 = sys_mmap(64)
65 z[0] = 0x02 as u8
66 let bs5: *NxBitStream = nx_bitstream_alloc(z, 1)
67 if wl_decode_symbol(t2, bs5) != 0 { fails = fails + 1 }
68 if wl_decode_symbol(t2, bs5) != 1 { fails = fails + 1 }
69
70 // ---- T6: SIMPLE form off a real bitstream ----
71 // 0x09 = bits LSB-first 1,0,0,1 -> simple=1, num_symbols=1, len_code=0, sym=1
72 let sb: *u8 = sys_mmap(64)
73 sb[0] = 0x09 as u8
74 let bs6: *NxBitStream = nx_bitstream_alloc(sb, 1)
75 let t6: *NxWlTree = wl_read_huffman_code(bs6, 16)
76 if t6 == (0 as *NxWlTree) { fails = fails + 1 } else {
77 if t6.trivial != 1 { fails = fails + 1 }
78 if t6.symbol != 1 { fails = fails + 1 }
79 }
80
81 // ---- T7: SIMPLE two-symbol form, 8-bit symbols 3 and 7 ----
82 // bits: 1,1,1 | 3 as 8 LSB-first | 7 as 8 LSB-first -> 0x1F 0x38 0x00
83 let s2: *u8 = sys_mmap(64)
84 s2[0] = 0x1f as u8; s2[1] = 0x38 as u8; s2[2] = 0x00 as u8
85 let bs7: *NxBitStream = nx_bitstream_alloc(s2, 3)
86 let t7: *NxWlTree = wl_read_huffman_code(bs7, 256)
87 if t7 == (0 as *NxWlTree) { fails = fails + 1 } else {
88 if t7.trivial != 0 { fails = fails + 1 } else {
89 let q: *u8 = sys_mmap(64)
90 q[0] = 0x02 as u8
91 let bsq: *NxBitStream = nx_bitstream_alloc(q, 1)
92 if wl_decode_symbol(t7, bsq) != 3 { fails = fails + 1 }
93 if wl_decode_symbol(t7, bsq) != 7 { fails = fails + 1 }
94 }
95 }
96
97 // ---- T8 NEG: an all-zero length vector codes nothing -> REFUSE ----
98 let l0: *i64 = sys_mmap(5 * 8 + 64) as *i64
99 i = 0
100 while i < 5 { l0[i] = 0; i = i + 1 }
101 if wl_tree_from_lengths(l0, 5) != (0 as *NxWlTree) { fails = fails + 1 }
102
103 // ---- T9 NEG: a null tree must report -1, never a plausible symbol ----
104 if wl_decode_symbol(0 as *NxWlTree, bs2) != (0 - 1) { fails = fails + 1 }
105
106 // ---- T10 NEG: a SIMPLE symbol beyond the alphabet is malformed ----
107 let sb2: *u8 = sys_mmap(64)
108 sb2[0] = 0x09 as u8
109 let bs10: *NxBitStream = nx_bitstream_alloc(sb2, 1)
110 if wl_read_huffman_code(bs10, 1) != (0 as *NxWlTree) { fails = fails + 1 }
111
112 // ---- T11: the spec permuted code-length order ----
113 let ord: *i64 = sys_mmap(19 * 8 + 64) as *i64
114 wl_code_order(ord)
115 if ord[0] != 17 { fails = fails + 1 }
116 if ord[8] != 16 { fails = fails + 1 }
117 if ord[18] != 15 { fails = fails + 1 }
118
119 if fails == 0 {
120 g_puts("GATE nx_webp_huff verdict=GREEN pass=11/11 (trivial tree decodes zero-bit; canonical 2-symbol; SIMPLE 1+2 form; NEG all-zero/null/out-of-range refused; spec code order)\n" as *u8)
121 sys_exit(0)
122 return 0
123 }
124 g_puts("GATE nx_webp_huff verdict=RED\n" as *u8)
125 sys_exit(1)
126 return 1
127}