nx_av1_dct_gate.nx source
↩ module page · 210 lines · 7757 B
1// nx_av1_dct_gate.nx -- proves the inverse DCT networks by STRUCTURAL property.
2//
3// Reference bit-exactness needs libaom's test vectors, which are not present
4// here. What IS provable without them is the set of properties a correct DCT
5// basis must have and a mis-wired one cannot fake:
6//
7// T1 DC-only in -> FLAT out. Any butterfly wired to the wrong index or any
8// sign error in the even path breaks this immediately.
9// T2 odd basis index -> ANTISYMMETRIC out (out[i] == -out[n-1-i]). This is
10// what catches a wrong rotation angle in the odd path.
11// T3 even basis index -> the specific symmetric pattern.
12// T4 LINEARITY within rounding slack. A network that is structurally right
13// but uses a halved angle still passes T1; it does not survive T2 plus
14// the basis-frequency check in T5.
15// T5 the constants land where the angle mapping says: cospi_16_64 is
16// cos128(32) = 2896, not cos128(16). Halving the factor yields a
17// transform that still LOOKS like a DCT and decodes blurred.
18//
19// This gate does NOT claim bit-exactness against libaom. It claims the
20// network is structurally a DCT with the right frequencies.
21//
22// license_tier: ORIGINAL
23import "nx_syscalls.nx"
24import "nx_av1_txfm.nx"
25import "nx_av1_dct.nx"
26
27func g_puts(s: *u8) -> i64 {
28 var i: i64 = 0
29 while s[i] != (0 as u8) { i = i + 1 }
30 sys_write(1, s, i)
31 return i
32}
33
34func g_putn(v: i64) -> i64 {
35 let buf: *u8 = sys_mmap(32)
36 var x: i64 = v
37 if x < 0 { g_puts("-" as *u8); x = 0 - x }
38 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
39 let tmp: *u8 = sys_mmap(32)
40 var d: i64 = 0
41 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
42 var i: i64 = 0
43 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
44 sys_write(1, buf, d)
45 return d
46}
47
48func absv(x: i64) -> i64 { if x < 0 { return 0 - x } return x }
49
50func main() -> i64 {
51 var fails: i64 = 0
52 var mark: i64 = 0
53
54 let t: *i64 = sys_mmap(128 * 8) as *i64
55 nx_av1_cos_table(t)
56
57 // ---- T5 first: the constants must be at the RIGHT frequencies ----
58 if nx_av1_cos128(t, 32) != 2896 { fails = fails + 1 } // cospi_16_64
59 if nx_av1_cos128(t, 16) != 3784 { fails = fails + 1 } // cospi_8_64
60 if nx_av1_cos128(t, 48) != 1567 { fails = fails + 1 } // cospi_24_64
61 if nx_av1_cos128(t, 8) != 4017 { fails = fails + 1 } // cospi_4_64
62 if nx_av1_cos128(t, 56) != 799 { fails = fails + 1 } // cospi_28_64
63 // the halved-angle mistake must be VISIBLY different, not coincidentally equal
64 if nx_av1_cos128(t, 32) == nx_av1_cos128(t, 16) { fails = fails + 1 }
65 if fails > 0 { if mark == 0 { mark = 5 } }
66
67 let io: *i64 = sys_mmap(64 * 8) as *i64
68
69 // ---- T1: idct4, DC-only gives a FLAT output ----
70 io[0] = 1000; io[1] = 0; io[2] = 0; io[3] = 0
71 nx_av1_idct4(t, io)
72 if io[0] != io[1] { fails = fails + 1 }
73 if io[1] != io[2] { fails = fails + 1 }
74 if io[2] != io[3] { fails = fails + 1 }
75 if io[0] == 0 { fails = fails + 1 }
76 if fails > 0 { if mark == 0 { mark = 1 } }
77
78 // ---- T2: idct4, basis 1 gives an ANTISYMMETRIC output ----
79 io[0] = 0; io[1] = 1000; io[2] = 0; io[3] = 0
80 nx_av1_idct4(t, io)
81 if io[0] != (0 - io[3]) { fails = fails + 1 }
82 if io[1] != (0 - io[2]) { fails = fails + 1 }
83 // and it must be DECREASING across the block -- a real basis-1 shape
84 if io[0] <= io[1] { fails = fails + 1 }
85 if fails > 0 { if mark == 0 { mark = 2 } }
86
87 // ---- T3: idct4, basis 2 gives the [+,-,-,+] pattern ----
88 io[0] = 0; io[1] = 0; io[2] = 1000; io[3] = 0
89 nx_av1_idct4(t, io)
90 if io[0] != (0 - io[1]) { fails = fails + 1 }
91 if io[1] != io[2] { fails = fails + 1 }
92 if io[3] != io[0] { fails = fails + 1 }
93 if fails > 0 { if mark == 0 { mark = 3 } }
94
95 // ---- T4: idct4 is LINEAR within rounding slack ----
96 let x: *i64 = sys_mmap(64 * 8) as *i64
97 let y: *i64 = sys_mmap(64 * 8) as *i64
98 let z: *i64 = sys_mmap(64 * 8) as *i64
99 var seed: i64 = 987654
100 var trial: i64 = 0
101 var lin_bad: i64 = 0
102 while trial < 100 {
103 var i: i64 = 0
104 while i < 4 {
105 seed = (seed * 1103515245 + 12345) & 0x7fffffff
106 x[i] = (seed % 801) - 400
107 seed = (seed * 1103515245 + 12345) & 0x7fffffff
108 y[i] = (seed % 801) - 400
109 z[i] = x[i] + y[i]
110 i = i + 1
111 }
112 nx_av1_idct4(t, x)
113 nx_av1_idct4(t, y)
114 nx_av1_idct4(t, z)
115 i = 0
116 while i < 4 {
117 if absv(z[i] - (x[i] + y[i])) > 4 { lin_bad = lin_bad + 1 }
118 i = i + 1
119 }
120 trial = trial + 1
121 }
122 if lin_bad != 0 { fails = fails + 1 }
123 if fails > 0 { if mark == 0 { mark = 4 } }
124
125 // ---- T6: idct8, DC-only gives a FLAT output across all eight ----
126 var i: i64 = 0
127 while i < 8 { io[i] = 0; i = i + 1 }
128 io[0] = 800
129 nx_av1_idct8(t, io)
130 var flat_bad: i64 = 0
131 i = 1
132 while i < 8 {
133 if io[i] != io[0] { flat_bad = flat_bad + 1 }
134 i = i + 1
135 }
136 if flat_bad != 0 { fails = fails + 1 }
137 if io[0] == 0 { fails = fails + 1 }
138 if fails > 0 { if mark == 0 { mark = 6 } }
139
140 // ---- T7: idct8, basis 1 gives an ANTISYMMETRIC output ----
141 i = 0
142 while i < 8 { io[i] = 0; i = i + 1 }
143 io[1] = 800
144 nx_av1_idct8(t, io)
145 var anti_bad: i64 = 0
146 i = 0
147 while i < 8 {
148 if io[i] != (0 - io[7 - i]) { anti_bad = anti_bad + 1 }
149 i = i + 1
150 }
151 if anti_bad != 0 { fails = fails + 1 }
152 // a genuine basis-1 shape is monotonically decreasing
153 if io[0] <= io[1] { fails = fails + 1 }
154 if io[1] <= io[2] { fails = fails + 1 }
155 if io[2] <= io[3] { fails = fails + 1 }
156 if fails > 0 { if mark == 0 { mark = 7 } }
157
158 // ---- T8: idct8 is LINEAR within rounding slack ----
159 seed = 24680
160 trial = 0
161 lin_bad = 0
162 while trial < 100 {
163 i = 0
164 while i < 8 {
165 seed = (seed * 1103515245 + 12345) & 0x7fffffff
166 x[i] = (seed % 801) - 400
167 seed = (seed * 1103515245 + 12345) & 0x7fffffff
168 y[i] = (seed % 801) - 400
169 z[i] = x[i] + y[i]
170 i = i + 1
171 }
172 nx_av1_idct8(t, x)
173 nx_av1_idct8(t, y)
174 nx_av1_idct8(t, z)
175 i = 0
176 while i < 8 {
177 if absv(z[i] - (x[i] + y[i])) > 8 { lin_bad = lin_bad + 1 }
178 i = i + 1
179 }
180 trial = trial + 1
181 }
182 if lin_bad != 0 { fails = fails + 1 }
183 if fails > 0 { if mark == 0 { mark = 8 } }
184
185 // ---- T9: the bit-reversal permutation the spec feeds the network ----
186 i = 0
187 while i < 8 { io[i] = i; i = i + 1 }
188 nx_av1_dct_permute(io, 3)
189 // brev(3, i): 0,4,2,6,1,5,3,7
190 if io[0] != 0 { fails = fails + 1 }
191 if io[1] != 4 { fails = fails + 1 }
192 if io[2] != 2 { fails = fails + 1 }
193 if io[3] != 6 { fails = fails + 1 }
194 if io[4] != 1 { fails = fails + 1 }
195 if io[7] != 7 { fails = fails + 1 }
196 if fails > 0 { if mark == 0 { mark = 9 } }
197
198 if fails == 0 {
199 g_puts("GATE nx_av1_dct verdict=GREEN pass=9/9 (constants at the RIGHT frequencies -- cospi_16_64=cos128(32)=2896 not cos128(16), halved-angle visibly distinct; idct4 DC->flat, basis-1 antisymmetric and decreasing, basis-2 [+,-,-,+]; idct4 linear over 100 random pairs; idct8 DC->flat across all 8, basis-1 antisymmetric and monotonic, linear over 100 pairs; bit-reversal permutation. STRUCTURAL proof -- bit-exactness vs libaom reference vectors NOT claimed)\n" as *u8)
200 sys_exit(0)
201 return 0
202 }
203 g_puts("GATE nx_av1_dct verdict=RED fails=" as *u8)
204 g_putn(fails)
205 g_puts(" first_stage=" as *u8)
206 g_putn(mark)
207 g_puts("\n" as *u8)
208 sys_exit(1)
209 return 1
210}