nx_av1_obu_gate.nx source

1// nx_av1_obu_gate.nx -- proves the AV1/AV2 OBU layer by ROUND-TRIP. 2// 3// T2 pins LEB128 to its canonical encodings absolutely (128 -> 0x80 0x01), 4// because a writer that emits a longer-than-necessary form still round-trips 5// against its own reader while producing streams other decoders reject. 6// 7// T6/T7 are the security-shaped ones: obu_forbidden_bit and obu_reserved_1bit 8// must both be REFUSED. A parser that ignores them consumes arbitrary bytes 9// as headers and resynchronises onto garbage -- the standard way a malformed 10// file becomes a long walk through memory. T8 also bounds LEB128 at 8 bytes, 11// so a continuation run cannot march off the buffer. 12// 13// T4 separates UVLC from LEB128. They are both 'variable length' and they are 14// not the same code; confusing them misreads every frame-header field after 15// the first, silently. 16// 17// license_tier: ORIGINAL 18import "nx_syscalls.nx" 19import "nx_bitstream.nx" 20import "nx_av1_obu.nx" 21 22func g_puts(s: *u8) -> i64 { 23 var i: i64 = 0 24 while s[i] != (0 as u8) { i = i + 1 } 25 sys_write(1, s, i) 26 return i 27} 28 29func g_putn(v: i64) -> i64 { 30 let buf: *u8 = sys_mmap(32) 31 var x: i64 = v 32 if x < 0 { g_puts("-" as *u8); x = 0 - x } 33 if x == 0 { buf[0] = 0x30 as u8; sys_write(1, buf, 1); return 1 } 34 let tmp: *u8 = sys_mmap(32) 35 var d: i64 = 0 36 while x > 0 { tmp[d] = ((x % 10) + 0x30) as u8; x = x / 10; d = d + 1 } 37 var i: i64 = 0 38 while i < d { buf[i] = tmp[d - 1 - i]; i = i + 1 } 39 sys_write(1, buf, d) 40 return d 41} 42 43func main() -> i64 { 44 var fails: i64 = 0 45 var mark: i64 = 0 46 47 // ---- T1: LEB128 round-trip across the group boundaries ---- 48 let lb: *u8 = sys_mmap(256) 49 let ll: *i64 = sys_mmap(64) as *i64 50 let vals: *i64 = sys_mmap(128) as *i64 51 vals[0] = 0; vals[1] = 1; vals[2] = 127; vals[3] = 128 52 vals[4] = 16383; vals[5] = 16384; vals[6] = 2097151; vals[7] = 268435455 53 var k: i64 = 0 54 while k < 8 { 55 let w: i64 = nx_obu_leb128_write(lb, 256, 0, vals[k]) 56 if w <= 0 { fails = fails + 1 } else { 57 if nx_obu_leb128_read(lb, 256, 0, ll) != vals[k] { fails = fails + 1 } 58 if ll[0] != w { fails = fails + 1 } 59 } 60 k = k + 1 61 } 62 if fails > 0 { if mark == 0 { mark = 1 } } 63 64 // ---- T2: the CANONICAL encodings, pinned absolutely ---- 65 nx_obu_leb128_write(lb, 256, 0, 0) 66 if (lb[0] as i64 & 255) != 0x00 { fails = fails + 1 } 67 nx_obu_leb128_write(lb, 256, 0, 127) 68 if (lb[0] as i64 & 255) != 0x7f { fails = fails + 1 } 69 // 128 must be exactly two bytes: 0x80 0x01 70 if nx_obu_leb128_write(lb, 256, 0, 128) != 2 { fails = fails + 1 } 71 if (lb[0] as i64 & 255) != 0x80 { fails = fails + 1 } 72 if (lb[1] as i64 & 255) != 0x01 { fails = fails + 1 } 73 // 16384 must be exactly three: 0x80 0x80 0x01 74 if nx_obu_leb128_write(lb, 256, 0, 16384) != 3 { fails = fails + 1 } 75 if (lb[0] as i64 & 255) != 0x80 { fails = fails + 1 } 76 if (lb[2] as i64 & 255) != 0x01 { fails = fails + 1 } 77 if fails > 0 { if mark == 0 { mark = 2 } } 78 79 // ---- T4: UVLC is NOT LEB128 -- Exp-Golomb style, MSB-first ---- 80 let ub: *u8 = sys_mmap(64) 81 ub[0] = 0x80 as u8 // '1' -> 0 82 let b1: *NxBitStream = nx_bitstream_alloc(ub, 1) 83 if nx_obu_uvlc(b1) != 0 { fails = fails + 1 } 84 ub[0] = 0x40 as u8 // '0','1','0' -> 1 85 let b2: *NxBitStream = nx_bitstream_alloc(ub, 1) 86 if nx_obu_uvlc(b2) != 1 { fails = fails + 1 } 87 ub[0] = 0x60 as u8 // '0','1','1' -> 2 88 let b3: *NxBitStream = nx_bitstream_alloc(ub, 1) 89 if nx_obu_uvlc(b3) != 2 { fails = fails + 1 } 90 ub[0] = 0x20 as u8 // '0','0','1','0','0' -> 3 91 let b4: *NxBitStream = nx_bitstream_alloc(ub, 1) 92 if nx_obu_uvlc(b4) != 3 { fails = fails + 1 } 93 if fails > 0 { if mark == 0 { mark = 4 } } 94 95 // ---- T5: write three OBUs and walk the temporal unit back ---- 96 let tu: *u8 = sys_mmap(4096) 97 let pay1: *u8 = sys_mmap(256) 98 var i: i64 = 0 99 while i < 40 { pay1[i] = ((i * 3) & 255) as u8; i = i + 1 } 100 let pay2: *u8 = sys_mmap(512) 101 i = 0 102 while i < 200 { pay2[i] = ((i * 7 + 1) & 255) as u8; i = i + 1 } 103 104 var off: i64 = 0 105 // a temporal delimiter carries no payload 106 off = nx_obu_write(tu, 4096, off, NX_OBU_TEMPORAL_DELIM, 0, 0, 0, pay1, 0) 107 if off <= 0 { fails = fails + 1 } 108 off = nx_obu_write(tu, 4096, off, NX_OBU_SEQ_HEADER, 0, 0, 0, pay1, 40) 109 if off <= 0 { fails = fails + 1 } 110 // a frame OBU carrying the extension header, temporal 5 spatial 2 111 off = nx_obu_write(tu, 4096, off, NX_OBU_FRAME, 5, 2, 1, pay2, 200) 112 if off <= 0 { fails = fails + 1 } 113 114 if nx_obu_count(tu, off) != 3 { fails = fails + 1 } 115 116 let fld: *i64 = sys_mmap(128) as *i64 117 var p: i64 = 0 118 var seen: i64 = 0 119 var bad: i64 = 0 120 while seen < 3 { 121 if nx_obu_parse(tu, off, p, fld) != 1 { fails = fails + 1; seen = 3 } else { 122 if seen == 0 { 123 if fld[NX_OBU_FLD_TYPE] != NX_OBU_TEMPORAL_DELIM { bad = bad + 1 } 124 if fld[NX_OBU_FLD_PAYLEN] != 0 { bad = bad + 1 } 125 } 126 if seen == 1 { 127 if fld[NX_OBU_FLD_TYPE] != NX_OBU_SEQ_HEADER { bad = bad + 1 } 128 if fld[NX_OBU_FLD_PAYLEN] != 40 { bad = bad + 1 } 129 let po: i64 = fld[NX_OBU_FLD_PAYOFF] 130 var j: i64 = 0 131 while j < 40 { 132 if (tu[po+j] as i64 & 255) != (pay1[j] as i64 & 255) { bad = bad + 1 } 133 j = j + 1 134 } 135 } 136 if seen == 2 { 137 if fld[NX_OBU_FLD_TYPE] != NX_OBU_FRAME { bad = bad + 1 } 138 if fld[NX_OBU_FLD_EXTFLAG] != 1 { bad = bad + 1 } 139 if fld[NX_OBU_FLD_TEMPORAL] != 5 { bad = bad + 1 } 140 if fld[NX_OBU_FLD_SPATIAL] != 2 { bad = bad + 1 } 141 if fld[NX_OBU_FLD_PAYLEN] != 200 { bad = bad + 1 } 142 let po2: i64 = fld[NX_OBU_FLD_PAYOFF] 143 var j2: i64 = 0 144 while j2 < 200 { 145 if (tu[po2+j2] as i64 & 255) != (pay2[j2] as i64 & 255) { bad = bad + 1 } 146 j2 = j2 + 1 147 } 148 } 149 p = fld[NX_OBU_FLD_NEXT] 150 seen = seen + 1 151 } 152 } 153 if bad != 0 { fails = fails + 1 } 154 if p != off { fails = fails + 1 } 155 if fails > 0 { if mark == 0 { mark = 5 } } 156 157 // ---- T6 NEG: obu_forbidden_bit must be REFUSED ---- 158 tu[0] = ((tu[0] as i64) | 0x80) as u8 159 if nx_obu_parse(tu, off, 0, fld) != 0 { fails = fails + 1 } 160 if nx_obu_count(tu, off) != (0 - 1) { fails = fails + 1 } 161 tu[0] = ((tu[0] as i64) & 0x7f) as u8 162 if nx_obu_parse(tu, off, 0, fld) != 1 { fails = fails + 1 } 163 if fails > 0 { if mark == 0 { mark = 6 } } 164 165 // ---- T7 NEG: obu_reserved_1bit must be REFUSED ---- 166 tu[0] = ((tu[0] as i64) | 0x01) as u8 167 if nx_obu_parse(tu, off, 0, fld) != 0 { fails = fails + 1 } 168 tu[0] = ((tu[0] as i64) & 0xfe) as u8 169 if nx_obu_parse(tu, off, 0, fld) != 1 { fails = fails + 1 } 170 if fails > 0 { if mark == 0 { mark = 7 } } 171 172 // ---- T8 NEG: LEB128 is BOUNDED -- a runaway continuation is refused ---- 173 let run: *u8 = sys_mmap(64) 174 i = 0 175 while i < 16 { run[i] = 0xff as u8; i = i + 1 } 176 if nx_obu_leb128_read(run, 16, 0, ll) != (0 - 1) { fails = fails + 1 } 177 // and a continuation that runs past the buffer end 178 run[0] = 0x80 as u8 179 if nx_obu_leb128_read(run, 1, 0, ll) != (0 - 1) { fails = fails + 1 } 180 // out-of-range write arguments 181 if nx_obu_write(tu, 4096, 0, 16, 0, 0, 0, pay1, 0) != 0 { fails = fails + 1 } 182 if nx_obu_write(tu, 4096, 0, 1, 8, 0, 1, pay1, 0) != 0 { fails = fails + 1 } 183 if nx_obu_write(tu, 4, 0, 1, 0, 0, 0, pay1, 40) != 0 { fails = fails + 1 } 184 if fails > 0 { if mark == 0 { mark = 8 } } 185 186 if fails == 0 { 187 g_puts("GATE nx_av1_obu verdict=GREEN pass=8/8 (LEB128 round-trip across group boundaries; CANONICAL encodings pinned 128=0x80,0x01 and 16384=3 bytes; UVLC Exp-Golomb 0/1/2/3 distinct from LEB128; 3-OBU temporal unit written and walked back with extension ids temporal=5 spatial=2 and 240 payload bytes EXACT; NEG forbidden-bit and reserved-bit both refused then restored-and-accepted; LEB128 bounded at 8 bytes and at the buffer end; bad type/temporal-id/capacity refused)\n" as *u8) 188 sys_exit(0) 189 return 0 190 } 191 g_puts("GATE nx_av1_obu verdict=RED fails=" as *u8) 192 g_putn(fails) 193 g_puts(" first_stage=" as *u8) 194 g_putn(mark) 195 g_puts("\n" as *u8) 196 sys_exit(1) 197 return 1 198}