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}