nx_h264_cabac_residual_gate.nx source
↩ module page · 136 lines · 6287 B
1// nx_h264_cabac_residual_gate.nx -- teeth for STEP 2 residual decoding.
2//
3// WHAT THESE TEETH DO AND DO NOT PROVE. There is no CABAC ENCODER and no reference decoder in this
4// ecosystem, so I cannot assert "these bins decode to these coefficients" -- that would need a
5// vector I have no way to produce. What IS provable without one: bounds refusal, array
6// initialisation, loop TERMINATION on adversarial input, and sign/zero handling. Those are real
7// defects if broken, and every one below is a matched pair (the property fires AND its control).
8// END-TO-END SPEC CONFORMANCE IS NOT CLAIMED HERE -- it needs a real CABAC stream decoded to an
9// image. Do not read GREEN here as "CABAC posters work".
10import "nx_syscalls.nx"
11import "nx_h264_cabac.nx"
12import "nx_h264_cabac_residual.nx"
13import "nx_gate_verdict.nx"
14
15func gw(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
16func gn(v: i64) -> i64 {
17 let b: *u8 = sys_mmap(28)
18 var m: i64 = v
19 if m < 0 { sys_write(1, "-\x00" as *u8, 1); m = 0 - m }
20 let t: *u8 = sys_mmap(28)
21 var k: i64 = 0
22 if m == 0 { t[0] = 48 as u8; k = 1 }
23 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
24 var i: i64 = 0
25 while i < k { b[i] = t[k-1-i]; i = i + 1 }
26 sys_write(1, b, k)
27 return 0
28}
29
30func main(argc: i64, argv: *i64) -> i64 {
31 var pass: i64 = 0
32 var tot: i64 = 0
33 let cab: *i64 = sys_mmap(8*16) as *i64
34 let ctx: *i64 = sys_mmap(8*2048) as *i64
35 let rlps: *i64 = sys_mmap(8*256) as *i64
36 let tlps: *i64 = sys_mmap(8*128) as *i64
37 let tmps: *i64 = sys_mmap(8*128) as *i64
38 let sig: *i64 = sys_mmap(8*128) as *i64
39 let out: *i64 = sys_mmap(8*128) as *i64
40 let data: *u8 = sys_mmap(4096)
41 cab_load_tables(rlps, tlps, tmps)
42
43 // T1 + T2: bounds are REFUSED, and a legal size is NOT refused (matched pair)
44 tot = tot + 1
45 var r1: i64 = cbr_sigmap(cab, ctx, rlps, tlps, tmps, 0, 100, 0, sig)
46 var r2: i64 = cbr_sigmap(cab, ctx, rlps, tlps, tmps, 0, 100, CBR_MAXCOEFF + 1, sig)
47 if r1 < 0 { if r2 < 0 { pass = pass + 1; gw("T1 sigmap refuses maxc<=0 and maxc>cap OK\n\x00" as *u8) } }
48 if r1 >= 0 { gw("T1 FAIL maxc=0 not refused\n\x00" as *u8) }
49
50 tot = tot + 1
51 var i: i64 = 0
52 while i < 4096 { data[i] = 170 as u8; i = i + 1 }
53 cab_init(cab, data, 0, 4096)
54 let r3: i64 = cbr_sigmap(cab, ctx, rlps, tlps, tmps, 0, 100, 16, sig)
55 if r3 >= 0 { pass = pass + 1; gw("T2 legal maxc=16 accepted (control) n=\x00" as *u8); gn(r3); gw("\n\x00" as *u8) }
56 if r3 < 0 { gw("T2 FAIL legal size refused\n\x00" as *u8) }
57
58 // T3: every position the map reports is inside the block
59 tot = tot + 1
60 var bad: i64 = 0
61 i = 0
62 while i < 16 { if sig[i] != 0 { if sig[i] != 1 { bad = bad + 1 } } i = i + 1 }
63 if bad == 0 { pass = pass + 1; gw("T3 sigmap writes only 0/1 within bounds OK\n\x00" as *u8) } else { gw("T3 FAIL dirty flags=\x00" as *u8); gn(bad); gw("\n\x00" as *u8) }
64
65 // T4 + T5: levels are ZERO where the map says nothing, NONZERO where it says something
66 tot = tot + 1
67 i = 0
68 while i < 16 { sig[i] = 0; i = i + 1 }
69 sig[3] = 1
70 sig[9] = 1
71 cab_init(cab, data, 0, 4096)
72 let nl: i64 = cbr_levels(cab, ctx, rlps, tlps, tmps, 200, 16, sig, out)
73 var zeros_ok: i64 = 1
74 i = 0
75 while i < 16 {
76 if sig[i] == 0 { if out[i] != 0 { zeros_ok = 0 } }
77 i = i + 1
78 }
79 if nl == 2 { if zeros_ok == 1 { pass = pass + 1; gw("T4 levels: 2 decoded, all non-significant positions ZERO OK\n\x00" as *u8) } }
80 if nl != 2 { gw("T4 FAIL decoded=\x00" as *u8); gn(nl); gw(" expected 2\n\x00" as *u8) }
81
82 tot = tot + 1
83 var nz: i64 = 0
84 if out[3] != 0 { nz = nz + 1 }
85 if out[9] != 0 { nz = nz + 1 }
86 if nz == 2 { pass = pass + 1; gw("T5 both significant positions carry a NONZERO level OK\n\x00" as *u8) } else { gw("T5 FAIL nonzero=\x00" as *u8); gn(nz); gw("\n\x00" as *u8) }
87
88 // T6: the Exp-Golomb suffix TERMINATES on an all-ones bypass stream (adversarial input must
89 // not spin forever -- CBR_EG0_MAXK is the guard). If this hangs, the gate never returns.
90 tot = tot + 1
91 i = 0
92 while i < 4096 { data[i] = 255 as u8; i = i + 1 }
93 cab_init(cab, data, 0, 4096)
94 let e: i64 = cbr_eg0_bypass(cab)
95 if e < 0 { pass = pass + 1; gw("T6 eg0 REFUSES a corrupt all-ones bypass stream OK\n\x00" as *u8) } else { gw("T6 FAIL emitted an absurd level instead of refusing: \x00" as *u8); gn(e); gw("\n\x00" as *u8) }
96
97 // T8: the refusal PROPAGATES -- cbr_levels must not write a corrupt level
98 tot = tot + 1
99 i = 0
100 while i < 16 { sig[i] = 0; i = i + 1 }
101 sig[5] = 1
102 cab_init(cab, data, 0, 4096)
103 let nbad: i64 = cbr_levels(cab, ctx, rlps, tlps, tmps, 200, 16, sig, out)
104 var inb: i64 = 1
105 if nbad < 0 { inb = 1 } else {
106 var q: i64 = 0
107 while q < 16 {
108 var a: i64 = out[q]
109 if a < 0 { a = 0 - a }
110 if a > CBR_MAX_LEVEL { inb = 0 }
111 if sig[q] == 1 { if out[q] == 0 { inb = 0 } }
112 if sig[q] == 0 { if out[q] != 0 { inb = 0 } }
113 q = q + 1
114 }
115 }
116 if inb == 1 { pass = pass + 1; gw("T8 every emitted level is within the legal bound and matches the map OK\n\x00" as *u8) } else { gw("T8 FAIL an out-of-bound or map-inconsistent level escaped\n\x00" as *u8) }
117
118 // T7: a map with NOTHING significant yields zero levels and an all-zero output (control for T4)
119 tot = tot + 1
120 i = 0
121 while i < 16 { sig[i] = 0; out[i] = 7; i = i + 1 }
122 cab_init(cab, data, 0, 4096)
123 let n0: i64 = cbr_levels(cab, ctx, rlps, tlps, tmps, 200, 16, sig, out)
124 var allz: i64 = 1
125 i = 0
126 while i < 16 { if out[i] != 0 { allz = 0 } i = i + 1 }
127 if n0 == 0 { if allz == 1 { pass = pass + 1; gw("T7 empty map -> 0 levels, output cleared OK\n\x00" as *u8) } }
128 if n0 != 0 { gw("T7 FAIL decoded=\x00" as *u8); gn(n0); gw(" expected 0\n\x00" as *u8) }
129
130 let ctr: *i64 = gv_ctr()
131 ctr[0] = pass
132 ctr[1] = tot
133 let rc: i64 = gv_verdict("H264-CABAC-RESIDUAL" as *u8, ctr, "residual decoding is bounded, terminates on adversarial input, and honours the significance map (spec conformance NOT claimed: needs a real stream)" as *u8)
134 sys_exit(rc)
135 return rc
136}