nx_av1_frame_gate.nx source

1// nx_av1_frame_gate.nx -- proves the AV1/AV2 frame-header parameter blocks. 2// 3// T1 pins su() at its ACTUAL widths. A delta-Q is su(1+6) -- seven bits, not 4// eight. Sign-extending from the wrong bit turns -1 into +63 and every 5// negative delta into a large positive one; the frame then decodes at the 6// wrong quantiser with no error anywhere. The test walks every value of a 7// 7-bit signed field, so an off-by-one in the sign mask cannot survive. 8// 9// T4 pins the CDEF secondary-strength gap: coded 0,1,2,3 means strength 10// 0,1,2,FOUR. Strength 3 does not exist. A writer storing 4 verbatim 11// overflows a 2-bit field; one storing 3 silently means 4. The gate asserts 12// the mapping in both directions AND that strength 3 is REFUSED as 13// unrepresentable rather than quietly coerced. 14// 15// license_tier: ORIGINAL 16import "nx_syscalls.nx" 17import "nx_bitstream.nx" 18import "nx_av1_seq.nx" 19import "nx_av1_frame.nx" 20 21func g_puts(s: *u8) -> i64 { 22 var i: i64 = 0 23 while s[i] != (0 as u8) { i = i + 1 } 24 sys_write(1, s, i) 25 return i 26} 27 28func g_putn(v: i64) -> i64 { 29 let buf: *u8 = sys_mmap(32) 30 var x: i64 = v 31 if x < 0 { g_puts("-" as *u8); x = 0 - x } 32 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 } 33 let tmp: *u8 = sys_mmap(32) 34 var d: i64 = 0 35 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 } 36 var i: i64 = 0 37 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 } 38 sys_write(1, buf, d) 39 return d 40} 41 42func main() -> i64 { 43 var fails: i64 = 0 44 var mark: i64 = 0 45 let b: *u8 = sys_mmap(512) 46 47 // ---- T1: su(7) over its ENTIRE range, -64..63 ---- 48 var v: i64 = 0 - 64 49 while v < 64 { 50 let w: *NxAv1Bw = nx_av1_bw_new(b, 512) 51 if nx_av1_su_write(w, v, 7) != 1 { fails = fails + 1 } else { 52 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 53 if nx_av1_su_read(bs, 7) != v { fails = fails + 1 } 54 } 55 v = v + 1 56 } 57 let w8: *NxAv1Bw = nx_av1_bw_new(b, 512) 58 nx_av1_su_write(w8, 0 - 128, 8) 59 let bs8: *NxBitStream = nx_bitstream_alloc(b, 512) 60 if nx_av1_su_read(bs8, 8) != (0 - 128) { fails = fails + 1 } 61 let wx: *NxAv1Bw = nx_av1_bw_new(b, 512) 62 if nx_av1_su_write(wx, 64, 7) != 0 { fails = fails + 1 } 63 if nx_av1_su_write(wx, 0 - 65, 7) != 0 { fails = fails + 1 } 64 if fails > 0 { if mark == 0 { mark = 1 } } 65 66 // ---- T2: read_delta_q round-trip, including the zero shortcut ---- 67 let dq: *i64 = sys_mmap(64) as *i64 68 dq[0] = 0; dq[1] = 1; dq[2] = 0 - 1; dq[3] = 63; dq[4] = 0 - 64 69 var k: i64 = 0 70 while k < 5 { 71 let w: *NxAv1Bw = nx_av1_bw_new(b, 512) 72 if nx_av1_delta_q_write(w, dq[k]) != 1 { fails = fails + 1 } else { 73 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 74 if nx_av1_delta_q_read(bs) != dq[k] { fails = fails + 1 } 75 } 76 k = k + 1 77 } 78 // a zero delta costs exactly ONE bit, not eight 79 let wz: *NxAv1Bw = nx_av1_bw_new(b, 512) 80 nx_av1_delta_q_write(wz, 0) 81 if wz.bitpos != 1 { fails = fails + 1 } 82 if fails > 0 { if mark == 0 { mark = 2 } } 83 84 // ---- T3: quantization_params round-trip ---- 85 let q: *i64 = sys_mmap(128) as *i64 86 let r: *i64 = sys_mmap(128) as *i64 87 q[NX_QP_BASE] = 128 88 q[NX_QP_YDC] = 0 - 5 89 q[NX_QP_UDC] = 3 90 q[NX_QP_UAC] = 0 - 2 91 q[NX_QP_VDC] = 7 92 q[NX_QP_VAC] = 0 - 9 93 q[NX_QP_USEQM] = 1 94 q[NX_QP_QMY] = 5; q[NX_QP_QMU] = 6; q[NX_QP_QMV] = 7 95 let wq: *NxAv1Bw = nx_av1_bw_new(b, 512) 96 if nx_av1_quant_write(wq, 0, 1, q) != 1 { fails = fails + 1 } else { 97 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 98 if nx_av1_quant_read(bs, 0, 1, r) != 1 { fails = fails + 1 } else { 99 if r[NX_QP_BASE] != 128 { fails = fails + 1 } 100 if r[NX_QP_YDC] != (0 - 5) { fails = fails + 1 } 101 if r[NX_QP_UDC] != 3 { fails = fails + 1 } 102 if r[NX_QP_UAC] != (0 - 2) { fails = fails + 1 } 103 if r[NX_QP_VDC] != 7 { fails = fails + 1 } 104 if r[NX_QP_VAC] != (0 - 9) { fails = fails + 1 } 105 if r[NX_QP_QMY] != 5 { fails = fails + 1 } 106 if r[NX_QP_QMV] != 7 { fails = fails + 1 } 107 } 108 } 109 // monochrome: the chroma deltas are absent from the bitstream entirely 110 q[NX_QP_USEQM] = 0 111 let wm: *NxAv1Bw = nx_av1_bw_new(b, 512) 112 if nx_av1_quant_write(wm, 1, 0, q) != 1 { fails = fails + 1 } else { 113 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 114 if nx_av1_quant_read(bs, 1, 0, r) != 1 { fails = fails + 1 } else { 115 if r[NX_QP_BASE] != 128 { fails = fails + 1 } 116 if r[NX_QP_YDC] != (0 - 5) { fails = fails + 1 } 117 if r[NX_QP_UDC] != 0 { fails = fails + 1 } 118 if r[NX_QP_VAC] != 0 { fails = fails + 1 } 119 } 120 } 121 // when V is NOT coded separately it must MIRROR U, not stay zero 122 q[NX_QP_UDC] = 4; q[NX_QP_UAC] = 4; q[NX_QP_VDC] = 4; q[NX_QP_VAC] = 4 123 let wn: *NxAv1Bw = nx_av1_bw_new(b, 512) 124 if nx_av1_quant_write(wn, 0, 0, q) != 1 { fails = fails + 1 } else { 125 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 126 if nx_av1_quant_read(bs, 0, 0, r) != 1 { fails = fails + 1 } else { 127 if r[NX_QP_VDC] != 4 { fails = fails + 1 } 128 if r[NX_QP_VAC] != 4 { fails = fails + 1 } 129 } 130 } 131 if fails > 0 { if mark == 0 { mark = 3 } } 132 133 // ---- T4: the CDEF secondary-strength gap ---- 134 if nx_av1_cdef_sec_decode(0) != 0 { fails = fails + 1 } 135 if nx_av1_cdef_sec_decode(1) != 1 { fails = fails + 1 } 136 if nx_av1_cdef_sec_decode(2) != 2 { fails = fails + 1 } 137 if nx_av1_cdef_sec_decode(3) != 4 { fails = fails + 1 } 138 if nx_av1_cdef_sec_encode(4) != 3 { fails = fails + 1 } 139 if nx_av1_cdef_sec_encode(0) != 0 { fails = fails + 1 } 140 if nx_av1_cdef_sec_encode(3) != (0 - 1) { fails = fails + 1 } 141 if nx_av1_cdef_sec_encode(5) != (0 - 1) { fails = fails + 1 } 142 if fails > 0 { if mark == 0 { mark = 4 } } 143 144 // ---- T5: cdef_params round-trip with four strength sets ---- 145 let c: *i64 = sys_mmap(256) as *i64 146 let cr: *i64 = sys_mmap(256) as *i64 147 c[NX_CDEF_DAMPING] = 5 148 c[NX_CDEF_BITS] = 2 149 c[NX_CDEF_YPRI + 0] = 0; c[NX_CDEF_YSEC + 0] = 0 150 c[NX_CDEF_YPRI + 1] = 7; c[NX_CDEF_YSEC + 1] = 2 151 c[NX_CDEF_YPRI + 2] = 15; c[NX_CDEF_YSEC + 2] = 4 152 c[NX_CDEF_YPRI + 3] = 3; c[NX_CDEF_YSEC + 3] = 1 153 c[NX_CDEF_UVPRI + 0] = 1; c[NX_CDEF_UVSEC + 0] = 4 154 c[NX_CDEF_UVPRI + 1] = 2; c[NX_CDEF_UVSEC + 1] = 0 155 c[NX_CDEF_UVPRI + 2] = 4; c[NX_CDEF_UVSEC + 2] = 2 156 c[NX_CDEF_UVPRI + 3] = 8; c[NX_CDEF_UVSEC + 3] = 1 157 let wc: *NxAv1Bw = nx_av1_bw_new(b, 512) 158 if nx_av1_cdef_write(wc, 3, c) != 1 { fails = fails + 1 } else { 159 let bs: *NxBitStream = nx_bitstream_alloc(b, 512) 160 if nx_av1_cdef_read(bs, 3, cr) != 1 { fails = fails + 1 } else { 161 if cr[NX_CDEF_DAMPING] != 5 { fails = fails + 1 } 162 if cr[NX_CDEF_BITS] != 2 { fails = fails + 1 } 163 var i: i64 = 0 164 while i < 4 { 165 if cr[NX_CDEF_YPRI + i] != c[NX_CDEF_YPRI + i] { fails = fails + 1 } 166 if cr[NX_CDEF_YSEC + i] != c[NX_CDEF_YSEC + i] { fails = fails + 1 } 167 if cr[NX_CDEF_UVPRI + i] != c[NX_CDEF_UVPRI + i] { fails = fails + 1 } 168 if cr[NX_CDEF_UVSEC + i] != c[NX_CDEF_UVSEC + i] { fails = fails + 1 } 169 i = i + 1 170 } 171 } 172 } 173 if fails > 0 { if mark == 0 { mark = 5 } } 174 175 // ---- T6 NEG: refusals ---- 176 let wr: *NxAv1Bw = nx_av1_bw_new(b, 512) 177 c[NX_CDEF_YSEC + 2] = 3 178 if nx_av1_cdef_write(wr, 3, c) != 0 { fails = fails + 1 } 179 c[NX_CDEF_YSEC + 2] = 4 180 c[NX_CDEF_DAMPING] = 2 181 if nx_av1_cdef_write(wr, 3, c) != 0 { fails = fails + 1 } 182 c[NX_CDEF_DAMPING] = 7 183 if nx_av1_cdef_write(wr, 3, c) != 0 { fails = fails + 1 } 184 c[NX_CDEF_DAMPING] = 5 185 c[NX_CDEF_YPRI + 1] = 16 186 if nx_av1_cdef_write(wr, 3, c) != 0 { fails = fails + 1 } 187 c[NX_CDEF_YPRI + 1] = 7 188 q[NX_QP_BASE] = 256 189 if nx_av1_quant_write(wr, 1, 0, q) != 0 { fails = fails + 1 } 190 q[NX_QP_BASE] = 128 191 if nx_av1_delta_q_write(wr, 64) != 0 { fails = fails + 1 } 192 if nx_av1_delta_q_write(wr, 0 - 65) != 0 { fails = fails + 1 } 193 if fails > 0 { if mark == 0 { mark = 6 } } 194 195 if fails == 0 { 196 g_puts("GATE nx_av1_frame verdict=GREEN pass=6/6 (su(7) round-trips ALL 128 values so a sign-mask off-by-one cannot survive, su(8) boundary, out-of-range refused; delta_q round-trip with zero costing exactly 1 bit; quantization_params colour/separate-UV/monochrome, V MIRRORS U when not coded separately; CDEF secondary strength 3-means-FOUR mapped both ways and strength 3 REFUSED as unrepresentable; cdef_params round-trip over 4 strength sets; NEG bad strength/damping/primary/base_q/delta_q refused)\n" as *u8) 197 sys_exit(0) 198 return 0 199 } 200 g_puts("GATE nx_av1_frame verdict=RED fails=" as *u8) 201 g_putn(fails) 202 g_puts(" first_stage=" as *u8) 203 g_putn(mark) 204 g_puts("\n" as *u8) 205 sys_exit(1) 206 return 1 207}