nx_av1_seq_gate.nx source
↩ module page · 174 lines · 7787 B
1// nx_av1_seq_gate.nx -- proves the AV1/AV2 sequence header by ROUND-TRIP.
2//
3// T3 is the one worth having: the frame dimension is written in a field whose
4// WIDTH is itself coded immediately before it. A parser using a fixed width
5// happens to work near 16-bit sizes and mis-parses everything after the field
6// on any other size, because the bit cursor is then wrong for the whole rest
7// of the header. T3 round-trips dimensions spanning 1 to 65536 -- 1x1, 64x64,
8// 1920x1080, 3840x2160, 65536x65536 -- so a fixed-width reader cannot pass.
9//
10// T5 covers the AVIF shapes specifically: 8/10/12-bit, monochrome, and 4:2:0
11// vs 4:4:4, since those are what a still image actually carries.
12//
13// NON-VACUITY: T6 covers refusals -- a non-reduced header (unsupported here,
14// and refused rather than half-parsed), a bad profile, 12-bit outside
15// profile 2, and zero dimensions.
16//
17// license_tier: ORIGINAL
18import "nx_syscalls.nx"
19import "nx_bitstream.nx"
20import "nx_av1_seq.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: bit-width helper ----
48 if nx_av1_bits_for(0) != 1 { fails = fails + 1 }
49 if nx_av1_bits_for(1) != 1 { fails = fails + 1 }
50 if nx_av1_bits_for(2) != 2 { fails = fails + 1 }
51 if nx_av1_bits_for(255) != 8 { fails = fails + 1 }
52 if nx_av1_bits_for(256) != 9 { fails = fails + 1 }
53 if fails > 0 { if mark == 0 { mark = 1 } }
54
55 // ---- T2: the bit writer packs MSB-first ----
56 let wb: *u8 = sys_mmap(64)
57 let w: *NxAv1Bw = nx_av1_bw_new(wb, 64)
58 nx_av1_bw_put(w, 5, 3) // 101
59 nx_av1_bw_put(w, 1, 1) // 1
60 nx_av1_bw_put(w, 0, 4) // 0000
61 // bits so far: 101 | 1 | 0000 -> 1011 0000 = 0xB0
62 if (wb[0] as i64 & 255) != 0xb0 { fails = fails + 1 }
63 if nx_av1_bw_bytes(w) != 1 { fails = fails + 1 }
64 if fails > 0 { if mark == 0 { mark = 2 } }
65
66 // ---- T3: dimensions across the whole field-width range ----
67 let dims: *i64 = sys_mmap(128) as *i64
68 dims[0] = 1; dims[1] = 1
69 dims[2] = 64; dims[3] = 64
70 dims[4] = 1920; dims[5] = 1080
71 dims[6] = 3840; dims[7] = 2160
72 dims[8] = 65536; dims[9] = 65536
73 let sb: *u8 = sys_mmap(256)
74 let fld: *i64 = sys_mmap(128) as *i64
75 var k: i64 = 0
76 while k < 5 {
77 let ww: i64 = dims[k*2]
78 let hh: i64 = dims[k*2+1]
79 let nb: i64 = nx_av1_seq_write_still(sb, 256, 0, 8, ww, hh, 8, 0, 1, 1)
80 if nb <= 0 { fails = fails + 1 } else {
81 if nx_av1_seq_parse(sb, nb, fld) != 1 { fails = fails + 1 } else {
82 if fld[NX_SEQ_MAXW] != ww { fails = fails + 1 }
83 if fld[NX_SEQ_MAXH] != hh { fails = fails + 1 }
84 if fld[NX_SEQ_REDUCED] != 1 { fails = fails + 1 }
85 if fld[NX_SEQ_STILL] != 1 { fails = fails + 1 }
86 }
87 }
88 k = k + 1
89 }
90 if fails > 0 { if mark == 0 { mark = 3 } }
91
92 // ---- T4: tool flags and level survive ----
93 let nb2: i64 = nx_av1_seq_write_still(sb, 256, 0, 13, 1280, 720, 8, 0, 1, 1)
94 if nb2 <= 0 { fails = fails + 1 } else {
95 if nx_av1_seq_parse(sb, nb2, fld) != 1 { fails = fails + 1 } else {
96 if fld[NX_SEQ_LEVEL] != 13 { fails = fails + 1 }
97 if fld[NX_SEQ_CDEF] != 1 { fails = fails + 1 }
98 if fld[NX_SEQ_RESTORATION] != 1 { fails = fails + 1 }
99 if fld[NX_SEQ_SB128] != 0 { fails = fails + 1 }
100 if fld[NX_SEQ_SUPERRES] != 0 { fails = fails + 1 }
101 if fld[NX_SEQ_FILMGRAIN] != 0 { fails = fails + 1 }
102 }
103 }
104 if fails > 0 { if mark == 0 { mark = 4 } }
105
106 // ---- T5: the AVIF colour shapes ----
107 // 8-bit 4:2:0 profile 0
108 let a1: i64 = nx_av1_seq_write_still(sb, 256, 0, 8, 512, 512, 8, 0, 1, 1)
109 if nx_av1_seq_parse(sb, a1, fld) != 1 { fails = fails + 1 } else {
110 if fld[NX_SEQ_BITDEPTH] != 8 { fails = fails + 1 }
111 if fld[NX_SEQ_SUBX] != 1 { fails = fails + 1 }
112 if fld[NX_SEQ_SUBY] != 1 { fails = fails + 1 }
113 if fld[NX_SEQ_MONO] != 0 { fails = fails + 1 }
114 }
115 // 10-bit 4:2:0 profile 0
116 let a2: i64 = nx_av1_seq_write_still(sb, 256, 0, 8, 512, 512, 10, 0, 1, 1)
117 if nx_av1_seq_parse(sb, a2, fld) != 1 { fails = fails + 1 } else {
118 if fld[NX_SEQ_BITDEPTH] != 10 { fails = fails + 1 }
119 }
120 // monochrome 8-bit
121 let a3: i64 = nx_av1_seq_write_still(sb, 256, 0, 8, 320, 200, 8, 1, 1, 1)
122 if nx_av1_seq_parse(sb, a3, fld) != 1 { fails = fails + 1 } else {
123 if fld[NX_SEQ_MONO] != 1 { fails = fails + 1 }
124 if fld[NX_SEQ_BITDEPTH] != 8 { fails = fails + 1 }
125 }
126 // 4:4:4 profile 1
127 let a4: i64 = nx_av1_seq_write_still(sb, 256, 1, 8, 640, 480, 8, 0, 0, 0)
128 if nx_av1_seq_parse(sb, a4, fld) != 1 { fails = fails + 1 } else {
129 if fld[NX_SEQ_PROFILE] != 1 { fails = fails + 1 }
130 if fld[NX_SEQ_SUBX] != 0 { fails = fails + 1 }
131 if fld[NX_SEQ_SUBY] != 0 { fails = fails + 1 }
132 }
133 // 12-bit profile 2
134 let a5: i64 = nx_av1_seq_write_still(sb, 256, 2, 8, 800, 600, 12, 0, 1, 1)
135 if nx_av1_seq_parse(sb, a5, fld) != 1 { fails = fails + 1 } else {
136 if fld[NX_SEQ_BITDEPTH] != 12 { fails = fails + 1 }
137 if fld[NX_SEQ_PROFILE] != 2 { fails = fails + 1 }
138 }
139 if fails > 0 { if mark == 0 { mark = 5 } }
140
141 // ---- T6 NEG: refusals ----
142 // zero and negative dimensions
143 if nx_av1_seq_write_still(sb, 256, 0, 8, 0, 100, 8, 0, 1, 1) != 0 { fails = fails + 1 }
144 if nx_av1_seq_write_still(sb, 256, 0, 8, 100, 0, 8, 0, 1, 1) != 0 { fails = fails + 1 }
145 // an out-of-range profile
146 if nx_av1_seq_write_still(sb, 256, 3, 8, 100, 100, 8, 0, 1, 1) != 0 { fails = fails + 1 }
147 // 12-bit is only legal in profile 2
148 if nx_av1_seq_write_still(sb, 256, 0, 8, 100, 100, 12, 0, 1, 1) != 0 { fails = fails + 1 }
149 // a nonsense bit depth
150 if nx_av1_seq_write_still(sb, 256, 0, 8, 100, 100, 9, 0, 1, 1) != 0 { fails = fails + 1 }
151 // an out-of-range level
152 if nx_av1_seq_write_still(sb, 256, 0, 32, 100, 100, 8, 0, 1, 1) != 0 { fails = fails + 1 }
153 // a NON-reduced header is unsupported here and must be REFUSED, not
154 // half-parsed: clear the reduced bit (bit 4 of byte 0, MSB-first)
155 let a6: i64 = nx_av1_seq_write_still(sb, 256, 0, 8, 100, 100, 8, 0, 1, 1)
156 sb[0] = ((sb[0] as i64) & 0xf7) as u8
157 if nx_av1_seq_parse(sb, a6, fld) != 0 { fails = fails + 1 }
158 sb[0] = ((sb[0] as i64) | 0x08) as u8
159 if nx_av1_seq_parse(sb, a6, fld) != 1 { fails = fails + 1 }
160 if fails > 0 { if mark == 0 { mark = 6 } }
161
162 if fails == 0 {
163 g_puts("GATE nx_av1_seq verdict=GREEN pass=6/6 (bit-width helper; MSB-first writer packs 0xB0; SELF-DESCRIBING dimension field round-trips 1x1 / 64x64 / 1920x1080 / 3840x2160 / 65536x65536 so a fixed-width reader cannot pass; level and tool flags survive; AVIF colour shapes 8/10/12-bit, monochrome, 4:2:0 and 4:4:4; NEG zero-dims/profile-3/12-bit-outside-profile-2/9-bit/level-32 refused, non-reduced header refused then restored-and-accepted)\n" as *u8)
164 sys_exit(0)
165 return 0
166 }
167 g_puts("GATE nx_av1_seq verdict=RED fails=" as *u8)
168 g_putn(fails)
169 g_puts(" first_stage=" as *u8)
170 g_putn(mark)
171 g_puts("\n" as *u8)
172 sys_exit(1)
173 return 1
174}