code wiki / _hdl_build / nx_vcodec_golomb_gate.nx
nx_vcodec_golomb_gate.nx source
↩ module page · 47 lines · 2278 B
1// nx_vcodec_golomb_gate.nx -- KAT for the vcv-10 exp-Golomb MV-delta verbs (F608 MVD bundle).
2// Proves: (1) vc_gput -> vc_gget round-trips exact over the signed sweep (qpel MV deltas live inside);
3// (2) emitted bit-length == the probe's gbits() cost mirror (2*blen(zze+1)-1) for EVERY value -- the RD
4// costing and the wire can never drift; (3) packed-stream decode in order with exact end position.
5// Rides nx_gate_verdict (migrate-on-touch law D001). license_tier: ORIGINAL expect_exit: 0
6import "nx_vcodec.nx"
7import "nx_gate_verdict.nx"
8
9func zzg(v: i64) -> i64 { if v < 0 { return ((0 - v) << 1) - 1 } return v << 1 }
10func blg(z: i64) -> i64 { var n: i64 = 0; var x: i64 = z; while x > 0 { n = n + 1; x = x >> 1 } return n }
11
12func main() -> i64 {
13 gv_head("=== nx_vcodec_golomb_gate: exp-Golomb MV-delta verbs (vcv-10 MVD bundle KAT) ===" as *u8)
14 let ctr: *i64 = gv_ctr()
15 let buf: *u8 = sys_mmap(65536)
16 let bpb: *i64 = sys_mmap(16) as *i64
17 // T1+T2: round-trip sweep + cost-mirror over -256..256
18 var ok: i64 = 1
19 var lenok: i64 = 1
20 var v: i64 = 0 - 256
21 while v <= 256 {
22 let bp1: i64 = vc_gput(buf, 0, v)
23 let want: i64 = 2*blg(zzg(v)+1) - 1
24 if bp1 != want { lenok = 0 }
25 bpb[0] = 0
26 if vc_gget(buf, bpb) != v { ok = 0 }
27 if bpb[0] != bp1 { ok = 0 }
28 v = v + 1
29 }
30 gv_check("round-trip -256..256 exact + end positions" as *u8, ok, ctr)
31 gv_check("emitted length == gbits cost mirror" as *u8, lenok, ctr)
32 // T3: packed stream of mixed values decodes in order at a non-zero start offset
33 let vals: *i64 = sys_mmap(64) as *i64
34 vals[0]=0; vals[1]=1; vals[2]=0-1; vals[3]=17; vals[4]=0-33; vals[5]=128; vals[6]=0-255
35 var bp: i64 = 5 // deliberately unaligned start
36 var i: i64 = 0
37 while i < 7 { bp = vc_gput(buf, bp, vals[i]); i = i + 1 }
38 bpb[0] = 5
39 var ok2: i64 = 1
40 i = 0
41 while i < 7 { if vc_gget(buf, bpb) != vals[i] { ok2 = 0 } i = i + 1 }
42 if bpb[0] != bp { ok2 = 0 }
43 gv_check("7-value packed stream (offset start) in order" as *u8, ok2, ctr)
44 let rc: i64 = gv_verdict("VCODEC-GOLOMB-GATE" as *u8, ctr, "vc_gput/vc_gget bit-exact + cost-mirror-true" as *u8)
45 sys_exit(rc)
46 return rc
47}