nx_av1_txfm2d_gate.nx source

1// nx_av1_txfm2d_gate.nx -- proves the 16 2-D transform types are a BIJECTION 2// onto the 4x4 grid of 1-D kinds, and that FLIPADST really flips. 3// 4// T1 IS THE HEADLINE. AOMedia's own AV2 overview says AV2 reuses "four primary 5// 1-D transform types producing 16 2-D combinations" from AV1 unchanged. That 6// sentence is a testable claim, so it is tested: build a 4x4 occupancy grid 7// from (col_kind, row_kind) over all sixteen types and assert every cell is hit 8// EXACTLY once. Any single mis-assignment double-books one cell and empties 9// another, so the check catches a one-type error, not just gross breakage. 10// 11// T3 pins the AV1 naming convention -- first token is the COLUMN. Swapping it 12// yields a transposed error that decodes cleanly on symmetric content and only 13// shows on directional detail, which is the worst kind of bug to ship. 14// 15// T5/T6 are non-vacuity: an unknown type must return -1 rather than defaulting 16// to DCT, and the 1-D dispatcher must REPORT that it did nothing rather than 17// quietly leaving a plausible block behind. 18// 19// license_tier: ORIGINAL 20import "nx_syscalls.nx" 21import "nx_av1_txfm.nx" 22import "nx_av1_dct.nx" 23import "nx_av1_adst.nx" 24import "nx_av1_txfm2d.nx" 25 26func g_puts(s: *u8) -> i64 { 27 var i: i64 = 0 28 while s[i] != (0 as u8) { i = i + 1 } 29 sys_write(1, s, i) 30 return i 31} 32 33func g_putn(v: i64) -> i64 { 34 let buf: *u8 = sys_mmap(32) 35 let tmp: *u8 = sys_mmap(32) 36 var x: i64 = v 37 var d: i64 = 0 38 var i: i64 = 0 39 if x < 0 { g_puts("-" as *u8); x = 0 - x } 40 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 } 41 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 } 42 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 } 43 sys_write(1, buf, d) 44 return d 45} 46 47func main() -> i64 { 48 var fails: i64 = 0 49 var mark: i64 = 0 50 var i: i64 = 0 51 var ck: i64 = 0 52 var rk: i64 = 0 53 54 let grid: *i64 = sys_mmap(64 * 8) as *i64 55 let a: *i64 = sys_mmap(64 * 8) as *i64 56 let b: *i64 = sys_mmap(64 * 8) as *i64 57 let t: *i64 = sys_mmap(128 * 8) as *i64 58 nx_av1_cos_table(t) 59 60 // ---- T1: the 16 types are a BIJECTION onto the 4x4 kind grid ---- 61 i = 0 62 while i < NX_TX1D_N * NX_TX1D_N { grid[i] = 0; i = i + 1 } 63 i = 0 64 while i < NX_TX2D_N { 65 ck = nx_av1_tx2d_col_kind(i) 66 rk = nx_av1_tx2d_row_kind(i) 67 if ck < 0 { fails = fails + 1 } else { 68 if rk < 0 { fails = fails + 1 } else { 69 if ck >= NX_TX1D_N { fails = fails + 1 } else { 70 if rk >= NX_TX1D_N { fails = fails + 1 } else { 71 grid[ck * NX_TX1D_N + rk] = grid[ck * NX_TX1D_N + rk] + 1 72 } 73 } 74 } 75 } 76 i = i + 1 77 } 78 // every cell hit EXACTLY once -- not at least once, exactly 79 i = 0 80 while i < NX_TX1D_N * NX_TX1D_N { 81 if grid[i] != 1 { fails = fails + 1 } 82 i = i + 1 83 } 84 // and there are exactly as many types as cells 85 if NX_TX2D_N != NX_TX1D_N * NX_TX1D_N { fails = fails + 1 } 86 if fails > 0 { if mark == 0 { mark = 1 } } 87 88 // ---- T2: FLIPADST is the ADST, reversed ---- 89 a[0] = 4096; a[1] = 0; a[2] = 0; a[3] = 0 90 nx_av1_iadst4(a) 91 b[0] = 4096; b[1] = 0; b[2] = 0; b[3] = 0 92 nx_av1_iflipadst4(b) 93 i = 0 94 while i < 4 { 95 if b[i] != a[3 - i] { fails = fails + 1 } 96 i = i + 1 97 } 98 // the basis-0 ADST is the rising SINPI ramp, so its flip must DESCEND -- 99 // a flip that returned the same vector would satisfy nothing above if 100 // the input were symmetric, so assert the asymmetry directly 101 if b[0] != NX_SINPI_4_9 { fails = fails + 1 } 102 if b[3] != NX_SINPI_1_9 { fails = fails + 1 } 103 if b[0] <= b[3] { fails = fails + 1 } 104 if a[0] >= a[3] { fails = fails + 1 } 105 if fails > 0 { if mark == 0 { mark = 2 } } 106 107 // ---- T3: the AV1 naming convention -- FIRST token is the COLUMN ---- 108 if nx_av1_tx2d_col_kind(NX_TX2D_ADST_DCT) != NX_TX1D_ADST { fails = fails + 1 } 109 if nx_av1_tx2d_row_kind(NX_TX2D_ADST_DCT) != NX_TX1D_DCT { fails = fails + 1 } 110 if nx_av1_tx2d_col_kind(NX_TX2D_DCT_ADST) != NX_TX1D_DCT { fails = fails + 1 } 111 if nx_av1_tx2d_row_kind(NX_TX2D_DCT_ADST) != NX_TX1D_ADST { fails = fails + 1 } 112 // V_ means vertical-only: the COLUMN carries the transform, the row is identity 113 if nx_av1_tx2d_col_kind(NX_TX2D_V_DCT) != NX_TX1D_DCT { fails = fails + 1 } 114 if nx_av1_tx2d_row_kind(NX_TX2D_V_DCT) != NX_TX1D_IDTX { fails = fails + 1 } 115 if nx_av1_tx2d_col_kind(NX_TX2D_H_DCT) != NX_TX1D_IDTX { fails = fails + 1 } 116 if nx_av1_tx2d_row_kind(NX_TX2D_H_DCT) != NX_TX1D_DCT { fails = fails + 1 } 117 // IDTX is identity on BOTH axes 118 if nx_av1_tx2d_col_kind(NX_TX2D_IDTX) != NX_TX1D_IDTX { fails = fails + 1 } 119 if nx_av1_tx2d_row_kind(NX_TX2D_IDTX) != NX_TX1D_IDTX { fails = fails + 1 } 120 if fails > 0 { if mark == 0 { mark = 3 } } 121 122 // ---- T4: IDTX SCALES, it is not a copy ---- 123 a[0] = 4096; a[1] = 1024; a[2] = 0; a[3] = 0 - 2048 124 nx_av1_itx_identity4(a) 125 // sqrt(2) * 4096 = 5793 in Q12, so 4096 -> ~5793, not 4096 126 if a[0] == 4096 { fails = fails + 1 } 127 if a[0] != NX_TX_SQRT2_Q12 { fails = fails + 1 } 128 // it is LINEAR and sign-preserving 129 if a[1] <= 0 { fails = fails + 1 } 130 if a[2] != 0 { fails = fails + 1 } 131 if a[3] >= 0 { fails = fails + 1 } 132 // and it GROWS the magnitude -- a scale below 1 would wash the block out 133 if a[0] <= 4096 { fails = fails + 1 } 134 if fails > 0 { if mark == 0 { mark = 4 } } 135 136 // ---- T5: the 1-D dispatcher routes each kind to a DISTINCT result ---- 137 // feeding one impulse through all four kinds must give four different 138 // vectors, or two kinds are silently aliased to the same transform 139 let d0: *i64 = sys_mmap(64 * 8) as *i64 140 let d1: *i64 = sys_mmap(64 * 8) as *i64 141 var kind: i64 = 0 142 var same: i64 = 0 143 kind = 0 144 while kind < NX_TX1D_N { 145 d0[0] = 4096; d0[1] = 0; d0[2] = 0; d0[3] = 0 146 if nx_av1_itx1d_4(kind, t, d0) != 1 { fails = fails + 1 } 147 var other: i64 = kind + 1 148 while other < NX_TX1D_N { 149 d1[0] = 4096; d1[1] = 0; d1[2] = 0; d1[3] = 0 150 nx_av1_itx1d_4(other, t, d1) 151 same = 0 152 i = 0 153 while i < 4 { 154 if d0[i] == d1[i] { same = same + 1 } 155 i = i + 1 156 } 157 if same == 4 { fails = fails + 1 } 158 other = other + 1 159 } 160 kind = kind + 1 161 } 162 if fails > 0 { if mark == 0 { mark = 5 } } 163 164 // ---- T6 NEG: unknown types and kinds are REFUSED, not defaulted ---- 165 if nx_av1_tx2d_col_kind(NX_TX2D_N) != (0 - 1) { fails = fails + 1 } 166 if nx_av1_tx2d_row_kind(NX_TX2D_N) != (0 - 1) { fails = fails + 1 } 167 if nx_av1_tx2d_col_kind(0 - 1) != (0 - 1) { fails = fails + 1 } 168 if nx_av1_tx2d_row_kind(999) != (0 - 1) { fails = fails + 1 } 169 // the dispatcher must REPORT doing nothing, and must leave the data alone 170 d0[0] = 1234; d0[1] = 5678; d0[2] = 0; d0[3] = 0 171 if nx_av1_itx1d_4(NX_TX1D_N, t, d0) != 0 { fails = fails + 1 } 172 if d0[0] != 1234 { fails = fails + 1 } 173 if d0[1] != 5678 { fails = fails + 1 } 174 if nx_av1_itx1d_4(0 - 1, t, d0) != 0 { fails = fails + 1 } 175 if fails > 0 { if mark == 0 { mark = 6 } } 176 177 if fails == 0 { 178 g_puts("GATE nx_av1_txfm2d verdict=GREEN pass=6/6 (the sixteen 2-D transform types are proven a BIJECTION onto the 4x4 grid of {DCT,ADST,FLIPADST,IDTX} -- every cell hit EXACTLY once, so a single mis-assigned type double-books one cell and empties another; this is the component AOMedia's own AV2 overview lists as reused from AV1 UNCHANGED, so it is AV2 work already. FLIPADST is the ADST reversed, checked elementwise and by its endpoints 3803/1321 descending where ADST rises; the AV1 convention that the FIRST token is the COLUMN is pinned so an axis swap cannot ship; IDTX is proven to SCALE by sqrt2 Q12 rather than copy, which would wash every identity block out; all four 1-D kinds give pairwise DISTINCT results so none is aliased; unknown types return -1 and the dispatcher reports doing nothing while leaving the data untouched)\n" as *u8) 179 sys_exit(0) 180 return 0 181 } 182 g_puts("GATE nx_av1_txfm2d 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}