nx_av1_adst_gate.nx source
↩ module page · 202 lines · 8503 B
1// nx_av1_adst_gate.nx -- proves the inverse ADST and its distinctness from DCT.
2//
3// T1 is exact and needs no reference vectors: a basis-0 impulse of 4096 must
4// return the four SINPI constants themselves, in order --
5// [1321, 2482, 3344, 3803]. Any wrong constant, any mis-wired term, any wrong
6// rounding shift moves at least one of them.
7//
8// T2 is the property that says WHY the ADST exists: its basis-0 output is a
9// RISING RAMP, where the DCT's is FLAT. The gate runs the same impulse through
10// both transforms and asserts the DCT gives four equal values while the ADST
11// gives four strictly increasing ones. Substituting one for the other decodes
12// without error and produces wrong gradients at block edges -- banding, not
13// corruption -- so proving they DISAGREE is the point.
14//
15// T4 pins the per-axis transform-type selector. AV1 picks independently for
16// rows and columns; swapping the axes yields a transposed-looking error that
17// survives on square symmetric content and breaks everything else.
18//
19// license_tier: ORIGINAL
20import "nx_syscalls.nx"
21import "nx_av1_txfm.nx"
22import "nx_av1_dct.nx"
23import "nx_av1_adst.nx"
24
25func g_puts(s: *u8) -> i64 {
26 var i: i64 = 0
27 while s[i] != (0 as u8) { i = i + 1 }
28 sys_write(1, s, i)
29 return i
30}
31
32func g_putn(v: i64) -> i64 {
33 let buf: *u8 = sys_mmap(32)
34 var x: i64 = v
35 if x < 0 { g_puts("-" as *u8); x = 0 - x }
36 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 }
37 let tmp: *u8 = sys_mmap(32)
38 var d: i64 = 0
39 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 }
40 var i: i64 = 0
41 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 }
42 sys_write(1, buf, d)
43 return d
44}
45
46func absv(x: i64) -> i64 { if x < 0 { return 0 - x } return x }
47
48func main() -> i64 {
49 var fails: i64 = 0
50 var mark: i64 = 0
51 var i: i64 = 0
52
53 let a: *i64 = sys_mmap(64 * 8) as *i64
54 let b: *i64 = sys_mmap(64 * 8) as *i64
55 let c: *i64 = sys_mmap(64 * 8) as *i64
56
57 // ---- T1: a basis-0 impulse returns the SINPI constants EXACTLY ----
58 a[0] = 4096; a[1] = 0; a[2] = 0; a[3] = 0
59 nx_av1_iadst4(a)
60 if a[0] != NX_SINPI_1_9 { fails = fails + 1 }
61 if a[1] != NX_SINPI_2_9 { fails = fails + 1 }
62 if a[2] != NX_SINPI_3_9 { fails = fails + 1 }
63 if a[3] != NX_SINPI_4_9 { fails = fails + 1 }
64 // and those constants are the ones the spec names
65 if NX_SINPI_1_9 != 1321 { fails = fails + 1 }
66 if NX_SINPI_2_9 != 2482 { fails = fails + 1 }
67 if NX_SINPI_3_9 != 3344 { fails = fails + 1 }
68 if NX_SINPI_4_9 != 3803 { fails = fails + 1 }
69 if fails > 0 { if mark == 0 { mark = 1 } }
70
71 // ---- T2: ADST RAMPS where DCT is FLAT -- they must DISAGREE ----
72 let t: *i64 = sys_mmap(128 * 8) as *i64
73 nx_av1_cos_table(t)
74
75 // the same impulse through the DCT: four EQUAL values
76 b[0] = 4096; b[1] = 0; b[2] = 0; b[3] = 0
77 nx_av1_idct4(t, b)
78 if b[0] != b[1] { fails = fails + 1 }
79 if b[1] != b[2] { fails = fails + 1 }
80 if b[2] != b[3] { fails = fails + 1 }
81
82 // through the ADST: four STRICTLY INCREASING values
83 c[0] = 4096; c[1] = 0; c[2] = 0; c[3] = 0
84 nx_av1_iadst4(c)
85 if c[0] >= c[1] { fails = fails + 1 }
86 if c[1] >= c[2] { fails = fails + 1 }
87 if c[2] >= c[3] { fails = fails + 1 }
88
89 // and the two transforms must genuinely DIFFER on this input -- if they
90 // agreed, one could silently stand in for the other
91 var same: i64 = 0
92 i = 0
93 while i < 4 {
94 if b[i] == c[i] { same = same + 1 }
95 i = i + 1
96 }
97 if same == 4 { fails = fails + 1 }
98 if fails > 0 { if mark == 0 { mark = 2 } }
99
100 // ---- T3: the ADST is LINEAR within rounding ----
101 let x: *i64 = sys_mmap(64 * 8) as *i64
102 let y: *i64 = sys_mmap(64 * 8) as *i64
103 let z: *i64 = sys_mmap(64 * 8) as *i64
104 var seed: i64 = 55555
105 var trial: i64 = 0
106 var lin_bad: i64 = 0
107 while trial < 100 {
108 i = 0
109 while i < 4 {
110 seed = (seed * 1103515245 + 12345) & 0x7fffffff
111 x[i] = (seed % 801) - 400
112 seed = (seed * 1103515245 + 12345) & 0x7fffffff
113 y[i] = (seed % 801) - 400
114 z[i] = x[i] + y[i]
115 i = i + 1
116 }
117 nx_av1_iadst4(x)
118 nx_av1_iadst4(y)
119 nx_av1_iadst4(z)
120 i = 0
121 while i < 4 {
122 if absv(z[i] - (x[i] + y[i])) > 4 { lin_bad = lin_bad + 1 }
123 i = i + 1
124 }
125 trial = trial + 1
126 }
127 if lin_bad != 0 { fails = fails + 1 }
128 // a zero input gives a zero output
129 z[0] = 0; z[1] = 0; z[2] = 0; z[3] = 0
130 nx_av1_iadst4(z)
131 i = 0
132 while i < 4 {
133 if z[i] != 0 { fails = fails + 1 }
134 i = i + 1
135 }
136 if fails > 0 { if mark == 0 { mark = 3 } }
137
138 // ---- T4: the PER-AXIS transform-type selector ----
139 if nx_av1_txt_row_is_adst(NX_TXT_DCT_DCT) != 0 { fails = fails + 1 }
140 if nx_av1_txt_col_is_adst(NX_TXT_DCT_DCT) != 0 { fails = fails + 1 }
141 if nx_av1_txt_row_is_adst(NX_TXT_ADST_ADST) != 1 { fails = fails + 1 }
142 if nx_av1_txt_col_is_adst(NX_TXT_ADST_ADST) != 1 { fails = fails + 1 }
143 // the mixed types are where an axis swap shows: ADST_DCT is ADST on the
144 // COLUMN pass only, DCT_ADST is ADST on the ROW pass only
145 if nx_av1_txt_col_is_adst(NX_TXT_ADST_DCT) != 1 { fails = fails + 1 }
146 if nx_av1_txt_row_is_adst(NX_TXT_ADST_DCT) != 0 { fails = fails + 1 }
147 if nx_av1_txt_row_is_adst(NX_TXT_DCT_ADST) != 1 { fails = fails + 1 }
148 if nx_av1_txt_col_is_adst(NX_TXT_DCT_ADST) != 0 { fails = fails + 1 }
149 // the two mixed types must NOT agree on either axis -- if they did, the
150 // swap would be undetectable
151 if nx_av1_txt_row_is_adst(NX_TXT_ADST_DCT) == nx_av1_txt_row_is_adst(NX_TXT_DCT_ADST) { fails = fails + 1 }
152 if nx_av1_txt_col_is_adst(NX_TXT_ADST_DCT) == nx_av1_txt_col_is_adst(NX_TXT_DCT_ADST) { fails = fails + 1 }
153 if fails > 0 { if mark == 0 { mark = 4 } }
154
155 // ---- T5: basis 1 is EXACTLY [s3, s3, 0, -s3], and CHANGES SIGN ----
156 //
157 // Derived by hand, not measured: with input [0,4096,0,0] every term
158 // vanishes except s3 = SINPI_3_9 * 4096, leaving x = [s3, s3, 0, -s3]
159 // and Round2(s3*4096, 12) = SINPI_3_9. So slots 0 and 1 must come back
160 // as the constant 3344 itself and slot 2 as an exact zero.
161 //
162 // A first draft of this test asserted the shape "changes direction",
163 // which is what a DCT basis 1 does. This one does not -- it is flat,
164 // then descends through zero. The module was right and the expectation
165 // was wrong; the fix is to pin the derived values rather than a shape
166 // guess, which is also a strictly stronger check.
167 c[0] = 0; c[1] = 4096; c[2] = 0; c[3] = 0
168 nx_av1_iadst4(c)
169 if c[0] != NX_SINPI_3_9 { fails = fails + 1 }
170 if c[1] != NX_SINPI_3_9 { fails = fails + 1 }
171 if c[2] != 0 { fails = fails + 1 }
172 // slot 3 is the negation before rounding; the only free bit is which
173 // way Round2 breaks a .5 tie on a negative, so allow exactly one ULP
174 if c[3] >= 0 { fails = fails + 1 }
175 if absv(c[3] + NX_SINPI_3_9) > 1 { fails = fails + 1 }
176 // SIGN CHANGE is what separates a higher basis from the DC-like basis 0:
177 // basis 0 is strictly positive and rising, basis 1 crosses zero
178 if c[0] <= 0 { fails = fails + 1 }
179 if c[3] >= 0 { fails = fails + 1 }
180 // ...and basis 1 must not BE basis 0 -- `a` still holds the T1 result
181 var differ: i64 = 0
182 i = 0
183 while i < 4 {
184 if c[i] != a[i] { differ = differ + 1 }
185 i = i + 1
186 }
187 if differ < 3 { fails = fails + 1 }
188 if fails > 0 { if mark == 0 { mark = 5 } }
189
190 if fails == 0 {
191 g_puts("GATE nx_av1_adst verdict=GREEN pass=5/5 (a basis-0 impulse of 4096 returns the SINPI constants EXACTLY -- 1321/2482/3344/3803 in order, no reference vectors needed; ADST RAMPS where DCT is FLAT on the same input and the two are proven to DISAGREE so neither can silently stand in for the other; linear over 100 random pairs and zero-in zero-out; the PER-AXIS type selector with the two mixed types proven to differ on both axes so an axis swap is detectable; basis 1 comes back as EXACTLY [3344,3344,0,-3344] -- the SINPI_3_9 constant, its repeat, an exact zero and its negation -- crossing zero where basis 0 only rises)\n" as *u8)
192 sys_exit(0)
193 return 0
194 }
195 g_puts("GATE nx_av1_adst verdict=RED fails=" as *u8)
196 g_putn(fails)
197 g_puts(" first_stage=" as *u8)
198 g_putn(mark)
199 g_puts("\n" as *u8)
200 sys_exit(1)
201 return 1
202}