nx_av1_txfm_gate.nx source
↩ module page · 189 lines · 8122 B
1// nx_av1_txfm_gate.nx -- proves the AV1/AV2 transform primitives.
2//
3// T1 pins the DIFFERENCE between Round2 and Round2Signed on negatives. They
4// agree on non-negative input and diverge below zero: Round2(-3,1) is -1,
5// Round2Signed(-3,1) is -2. Substituting one for the other yields a transform
6// that is correct on a test pattern of positives and half-wrong on real
7// signal. The gate asserts the divergence explicitly rather than testing each
8// in isolation, because testing them separately is exactly what lets the
9// substitution survive.
10//
11// T4 pins the cosine table's QUADRANT SIGNS. Only angles 0..64 are stored;
12// the rest are reflections. A wrong sign in one quadrant inverts half the
13// basis functions and decodes to a recognisable-but-wrong image -- it does
14// not look like noise, so it ships easily. The test walks all four quadrants
15// and asserts the Pythagorean identity holds at 12-bit precision throughout.
16//
17// T5 round-trips the Walsh-Hadamard pair over pseudo-random vectors --
18// the lossless path must be EXACTLY invertible, not approximately.
19//
20// license_tier: ORIGINAL
21import "nx_syscalls.nx"
22import "nx_av1_txfm.nx"
23
24func g_puts(s: *u8) -> i64 {
25 var i: i64 = 0
26 while s[i] != (0 as u8) { i = i + 1 }
27 sys_write(1, s, i)
28 return i
29}
30
31func g_putn(v: i64) -> i64 {
32 let buf: *u8 = sys_mmap(32)
33 var x: i64 = v
34 if x < 0 { g_puts("-" as *u8); x = 0 - x }
35 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
36 let tmp: *u8 = sys_mmap(32)
37 var d: i64 = 0
38 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
39 var i: i64 = 0
40 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
41 sys_write(1, buf, d)
42 return d
43}
44
45func main() -> i64 {
46 var fails: i64 = 0
47 var mark: i64 = 0
48
49 // ---- T1: Round2 vs Round2Signed -- they DIVERGE on negatives ----
50 if nx_av1_round2(0, 1) != 0 { fails = fails + 1 }
51 if nx_av1_round2(1, 1) != 1 { fails = fails + 1 }
52 if nx_av1_round2(3, 1) != 2 { fails = fails + 1 }
53 if nx_av1_round2(4, 2) != 1 { fails = fails + 1 }
54 if nx_av1_round2(5, 0) != 5 { fails = fails + 1 }
55 // arithmetic shift rounds negatives toward +infinity
56 if nx_av1_round2(0 - 1, 1) != 0 { fails = fails + 1 }
57 if nx_av1_round2(0 - 3, 1) != (0 - 1) { fails = fails + 1 }
58 // ...whereas Round2Signed rounds AWAY from zero
59 if nx_av1_round2_signed(0 - 3, 1) != (0 - 2) { fails = fails + 1 }
60 if nx_av1_round2_signed(0 - 1, 1) != (0 - 1) { fails = fails + 1 }
61 // they must AGREE on non-negatives
62 if nx_av1_round2_signed(3, 1) != nx_av1_round2(3, 1) { fails = fails + 1 }
63 // and DISAGREE on these negatives -- the property that catches a swap
64 if nx_av1_round2_signed(0 - 3, 1) == nx_av1_round2(0 - 3, 1) { fails = fails + 1 }
65 if fails > 0 { if mark == 0 { mark = 1 } }
66
67 // ---- T2: bit reversal ----
68 if nx_av1_brev(4, 1) != 8 { fails = fails + 1 }
69 if nx_av1_brev(4, 8) != 1 { fails = fails + 1 }
70 if nx_av1_brev(4, 0) != 0 { fails = fails + 1 }
71 if nx_av1_brev(4, 15) != 15 { fails = fails + 1 }
72 if nx_av1_brev(3, 3) != 6 { fails = fails + 1 }
73 if nx_av1_brev(5, 1) != 16 { fails = fails + 1 }
74 if fails > 0 { if mark == 0 { mark = 2 } }
75
76 // ---- T3: clamping ----
77 if nx_av1_clamp(5, 0, 10) != 5 { fails = fails + 1 }
78 if nx_av1_clamp(0 - 5, 0, 10) != 0 { fails = fails + 1 }
79 if nx_av1_clamp(50, 0, 10) != 10 { fails = fails + 1 }
80 if fails > 0 { if mark == 0 { mark = 3 } }
81
82 // ---- T4: the cosine table and its QUADRANT SIGNS ----
83 let t: *i64 = sys_mmap(128 * 8) as *i64
84 if nx_av1_cos_table(t) != 65 { fails = fails + 1 }
85 if t[0] != 4096 { fails = fails + 1 }
86 if t[64] != 0 { fails = fails + 1 }
87 if t[32] != 2896 { fails = fails + 1 }
88 // the four quadrants
89 if nx_av1_cos128(t, 0) != 4096 { fails = fails + 1 }
90 if nx_av1_cos128(t, 64) != 0 { fails = fails + 1 }
91 if nx_av1_cos128(t, 128) != (0 - 4096) { fails = fails + 1 }
92 if nx_av1_cos128(t, 192) != 0 { fails = fails + 1 }
93 if nx_av1_cos128(t, 256) != 4096 { fails = fails + 1 }
94 // quadrant 2 is NEGATIVE, quadrant 4 is POSITIVE -- the sign trap
95 if nx_av1_cos128(t, 96) >= 0 { fails = fails + 1 }
96 if nx_av1_cos128(t, 160) >= 0 { fails = fails + 1 }
97 if nx_av1_cos128(t, 224) <= 0 { fails = fails + 1 }
98 if nx_av1_cos128(t, 32) <= 0 { fails = fails + 1 }
99 // sine is cosine shifted a quarter period
100 if nx_av1_sin128(t, 0) != 0 { fails = fails + 1 }
101 if nx_av1_sin128(t, 64) != 4096 { fails = fails + 1 }
102 if nx_av1_sin128(t, 128) != 0 { fails = fails + 1 }
103 if nx_av1_sin128(t, 192) != (0 - 4096) { fails = fails + 1 }
104 // cos^2 + sin^2 must be one at 12-bit precision, across the circle
105 var ang: i64 = 0
106 var ident_bad: i64 = 0
107 while ang < 256 {
108 let c: i64 = nx_av1_cos128(t, ang)
109 let s: i64 = nx_av1_sin128(t, ang)
110 let sum: i64 = c * c + s * s
111 // allow the table's own quantisation slack
112 if sum < 16700000 { ident_bad = ident_bad + 1 }
113 if sum > 16880000 { ident_bad = ident_bad + 1 }
114 ang = ang + 1
115 }
116 if ident_bad != 0 { fails = fails + 1 }
117 if fails > 0 { if mark == 0 { mark = 4 } }
118
119 // ---- T5: the Walsh-Hadamard pair is EXACTLY invertible ----
120 let a: *i64 = sys_mmap(64) as *i64
121 let f: *i64 = sys_mmap(64) as *i64
122 let r: *i64 = sys_mmap(64) as *i64
123 var seed: i64 = 12345
124 var trial: i64 = 0
125 var wht_bad: i64 = 0
126 while trial < 200 {
127 var i: i64 = 0
128 while i < 4 {
129 seed = (seed * 1103515245 + 12345) & 0x7fffffff
130 a[i] = (seed % 2001) - 1000
131 i = i + 1
132 }
133 nx_av1_fwht4(a, f)
134 // the forward scales by 4; the inverse shifts it back
135 f[0] = f[0] * 4; f[1] = f[1] * 4; f[2] = f[2] * 4; f[3] = f[3] * 4
136 nx_av1_iwht4(f, r, 2)
137 i = 0
138 while i < 4 {
139 if r[i] != a[i] { wht_bad = wht_bad + 1 }
140 i = i + 1
141 }
142 trial = trial + 1
143 }
144 if wht_bad != 0 { fails = fails + 1 }
145 if fails > 0 { if mark == 0 { mark = 5 } }
146
147 // ---- T6: identity transform scale factors ----
148 // size 8 and 32 are plain doublings
149 if nx_av1_identity8(100) != 200 { fails = fails + 1 }
150 if nx_av1_identity32(100) != 400 { fails = fails + 1 }
151 // 4 and 16 use the root-two 5793/4096 scaling
152 if nx_av1_identity4(4096) != 5793 { fails = fails + 1 }
153 if nx_av1_identity16(4096) != 11586 { fails = fails + 1 }
154 if nx_av1_identity4(0) != 0 { fails = fails + 1 }
155 // identity16 must be exactly twice identity4 on the same input
156 if nx_av1_identity16(1000) != (2 * 1000 * 5793 + 2048) >> 12 { fails = fails + 1 }
157 if fails > 0 { if mark == 0 { mark = 6 } }
158
159 // ---- T7: the Hadamard butterfly ----
160 let h: *i64 = sys_mmap(64) as *i64
161 h[0] = 10; h[1] = 3
162 nx_av1_butterfly_h(h, 0, 1, 0)
163 if h[0] != 13 { fails = fails + 1 }
164 if h[1] != 7 { fails = fails + 1 }
165 // flipped, the roles swap
166 h[0] = 10; h[1] = 3
167 nx_av1_butterfly_h(h, 0, 1, 1)
168 if h[1] != 13 { fails = fails + 1 }
169 if h[0] != (0 - 7) { fails = fails + 1 }
170 // a rotation by angle 0 is the identity pair (cos=1, sin=0)
171 h[0] = 100; h[1] = 200
172 nx_av1_butterfly_b(t, h, 0, 1, 0, 0)
173 if h[0] != 100 { fails = fails + 1 }
174 if h[1] != 200 { fails = fails + 1 }
175 if fails > 0 { if mark == 0 { mark = 7 } }
176
177 if fails == 0 {
178 g_puts("GATE nx_av1_txfm verdict=GREEN pass=7/7 (Round2 vs Round2Signed DIVERGE on negatives and AGREE on positives -- the swap-catching property asserted directly; bit reversal; clamp; 12-bit cosine table with all four QUADRANT SIGNS and cos^2+sin^2 identity across all 256 angles; Walsh-Hadamard EXACTLY invertible over 200 pseudo-random vectors; identity scale factors 4/8/16/32 incl the 5793 root-two; Hadamard and rotation butterflies)\n" as *u8)
179 sys_exit(0)
180 return 0
181 }
182 g_puts("GATE nx_av1_txfm verdict=RED fails=" as *u8)
183 g_putn(fails)
184 g_puts(" first_stage=" as *u8)
185 g_putn(mark)
186 g_puts("\n" as *u8)
187 sys_exit(1)
188 return 1
189}