code wiki / _hdl_build / nx_ventropy_pack_gate.nx
nx_ventropy_pack_gate.nx source
↩ module page · 65 lines · 3939 B
1// nx_ventropy_pack_gate.nx -- proves position-aware entropy coding (ve_encode_at/ve_decode_at): several coefficient
2// blocks pack into ONE contiguous bitstream (threading the bit position) and decode back byte/coeff-faithful, resuming
3// at exactly the bit offset each block ended. This is what lets a whole frame's blocks become one transmittable stream.
4import "nx_syscalls.nx"
5import "nx_gate_emit_lib.nx"
6import "nx_ventropy.nx"
7import "nx_gate_verdict.nx"
8
9func blocks_equal(a: *i64, b: *i64) -> i64 { var i: i64=0; while i<16 { if a[i]!=b[i] { return 0 } i=i+1 } return 1 }
10
11func main() -> i64 {
12 g_puts("nx_ventropy pack gate (contiguous multi-block bitstream, round-trip)\n" as *u8)
13 var pass: i64 = 0; var total: i64 = 0
14
15 // three distinct quantized 4x4 coefficient blocks (DC + a few AC, the realistic post-quant shape)
16 let A: *i64 = sys_mmap(16*8) as *i64
17 let B: *i64 = sys_mmap(16*8) as *i64
18 let C: *i64 = sys_mmap(16*8) as *i64
19 var i: i64=0; while i<16 { A[i]=0; B[i]=0; C[i]=0; i=i+1 }
20 A[0]=12; A[1]=-3; A[5]=1 // block A
21 B[0]=-7; B[2]=4; B[3]=-2; B[8]=1 // block B
22 C[0]=1 // block C (near-static, ~DC only)
23
24 // PACK: encode all three into ONE buffer, threading the bit position
25 let buf: *u8 = sys_mmap(256) as *u8
26 var bp: i64 = 0
27 let p1: i64 = ve_encode_at(A, buf, bp); bp = p1
28 let p2: i64 = ve_encode_at(B, buf, bp); bp = p2
29 let p3: i64 = ve_encode_at(C, buf, bp); bp = p3
30 let total_bits: i64 = bp
31 let total_bytes: i64 = (total_bits + 7) / 8
32 g_puts(" [measure] 3 blocks packed into " as *u8); g_pn(total_bits); g_puts(" bits = " as *u8); g_pn(total_bytes); g_puts(" bytes (one contiguous stream)\n" as *u8)
33
34 // UNPACK: decode them back out of the SAME buffer, resuming at each block's end position
35 let A2: *i64 = sys_mmap(16*8) as *i64
36 let B2: *i64 = sys_mmap(16*8) as *i64
37 let C2: *i64 = sys_mmap(16*8) as *i64
38 var q: i64 = 0
39 let q1: i64 = ve_decode_at(buf, A2, q); q = q1
40 let q2: i64 = ve_decode_at(buf, B2, q); q = q2
41 let q3: i64 = ve_decode_at(buf, C2, q); q = q3
42
43 pass = pass + g_check("decode positions match encode positions (no drift across blocks)" as *u8, (q1==p1) & (q2==p2) & (q3==p3)); total=total+1
44 pass = pass + g_check("block A round-trips exactly" as *u8, blocks_equal(A, A2)); total=total+1
45 pass = pass + g_check("block B round-trips exactly" as *u8, blocks_equal(B, B2)); total=total+1
46 pass = pass + g_check("block C round-trips exactly" as *u8, blocks_equal(C, C2)); total=total+1
47 // contiguous pack vs each block padded to its own byte boundary: contiguous wastes no per-block padding
48 let bufA: *u8 = sys_mmap(64) as *u8
49 let bufB: *u8 = sys_mmap(64) as *u8
50 let bufC: *u8 = sys_mmap(64) as *u8
51 let sep_bytes: i64 = (ve_encode(A, bufA)+7)/8 + (ve_encode(B, bufB)+7)/8 + (ve_encode(C, bufC)+7)/8
52 g_puts(" [measure] contiguous=" as *u8); g_pn(total_bytes); g_puts("B vs byte-aligned-per-block=" as *u8); g_pn(sep_bytes); g_puts("B\n" as *u8)
53 pass = pass + g_check("contiguous pack <= byte-aligned-per-block (no padding waste)" as *u8, total_bytes <= sep_bytes); total=total+1
54
55 g_puts("---- ventropy pack gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8)
56 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
57 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
58 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
59 let ctr__dry: *i64 = gv_ctr()
60 ctr__dry[0] = pass
61 ctr__dry[1] = total
62 let rc__dry: i64 = gv_verdict("VENTROPY-PACK-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
63 sys_exit(rc__dry)
64 return rc__dry
65}