nx_uxf_remux_gate.nx source

1// nx_uxf_remux_gate.nx -- FM4: drives the EXTRACTED uxf_remux_frame and proves the rewrap is lossless. 2// 3// This is both the D001 migration of nx_uxf_remux_test and the proof that the extraction is faithful: the 4// five original teeth are preserved in order and predicate, now asserted against the CALLABLE entry point 5// rather than against logic inlined in a test. Three refusal teeth are added because the extraction 6// introduced boundary checks, and a deny path that has never been shown to fire is not a guard. 7// The positive control is T1 to T5 themselves: a well-formed element MUST be accepted, so a function that 8// refused everything would fail them. 9// license_tier: ORIGINAL No hw writes (Rule 26). 10import "nx_gate_verdict.nx" 11import "nx_syscalls.nx" 12import "nx_uxf_remux.nx" 13 14const URG_INBUF: i64 = 64 15const URG_OUTBUF: i64 = 65536 16const URG_TINYCAP: i64 = 16 // deliberately too small to hold the rewrap 17const URG_WANT_FRAMESIZE: i64 = 8 18const URG_WANT_ID: i64 = 0xA3 19const URG_SAMPLECOUNT: i64 = 1 20 21func main(argc: i64, argv: *i64) -> i64 { 22 let ctr: *i64 = gv_ctr() 23 gv_head("nx_uxf_remux -- a frame is REWRAPPED into MP4, never re-encoded" as *u8) 24 25 // a synthetic MKV SimpleBlock element: [id 0xA3][size 0x88 = 8][8 frame bytes] 26 let inb: *u8 = sys_mmap(URG_INBUF) 27 inb[0] = 0xA3 as u8; inb[1] = 0x88 as u8 28 inb[2] = 0x11 as u8; inb[3] = 0x22 as u8; inb[4] = 0x33 as u8; inb[5] = 0x44 as u8 29 inb[6] = 0x55 as u8; inb[7] = 0x66 as u8; inb[8] = 0x77 as u8; inb[9] = 0x88 as u8 30 let inlen: i64 = 10 31 32 let out: *u8 = sys_mmap(URG_OUTBUF) 33 let meta: *i64 = sys_mmap(URG_INBUF) as *i64 34 let total: i64 = uxf_remux_frame(inb, inlen, out, URG_OUTBUF, meta) 35 let src_off: i64 = uxf_remux_src_off(inb) 36 37 let id: i64 = meta[UXR_META_ID] 38 let fsize: i64 = meta[UXR_META_FRAMESIZE] 39 let mdat_off: i64 = meta[UXR_META_MDAT_OFF] 40 let stsz_off: i64 = meta[UXR_META_STSZ_OFF] 41 42 // FIXTURE REACHED THE CONDITION: the call must have SUCCEEDED before any carry is judged. 43 var accepted: i64 = 0 44 if total > 0 { accepted = 1 } 45 gv_check("T0 fixture reached the condition: a well-formed element was ACCEPTED and rewrapped" as *u8, accepted, ctr) 46 47 gv_check_eq("T1 the frame was parsed and its declared size is 8" as *u8, fsize, URG_WANT_FRAMESIZE, ctr) 48 gv_check("T2 mdat carries the frame BYTE-IDENTICAL, which is rewrap and not re-encode" as *u8, uxr_bytes_eq(out, mdat_off, inb, src_off, fsize), ctr) 49 gv_check_eq("T3 the stsz sample_size equals the frame size" as *u8, uxr_r32(out, stsz_off + UXR_STSZ_SAMPLESIZE_OFF), fsize, ctr) 50 gv_check("T4 the emitted MP4 box structure walks aligned to exactly the total length" as *u8, uxr_walk_ok(out, total), ctr) 51 gv_check_eq("T5 the parsed SimpleBlock id is 0xA3" as *u8, id, URG_WANT_ID, ctr) 52 53 // --- refusal controls: the boundary checks the extraction introduced must actually FIRE --- 54 let bad_vint: *u8 = sys_mmap(URG_INBUF) 55 bad_vint[0] = 0x00 as u8 // 0x00 is not a legal EBML vint leading byte 56 let r_vint: i64 = uxf_remux_frame(bad_vint, URG_INBUF, out, URG_OUTBUF, meta) 57 gv_check_eq("neg-control-a-malformed-vint-is-REFUSED-by-name-not-truncated" as *u8, r_vint, UXR_ERR_VINT, ctr) 58 59 let overrun: *u8 = sys_mmap(URG_INBUF) 60 overrun[0] = 0xA3 as u8; overrun[1] = 0x88 as u8 // declares 8 frame bytes 61 let r_over: i64 = uxf_remux_frame(overrun, 3, out, URG_OUTBUF, meta) // but only 1 byte follows 62 gv_check_eq("neg-control-a-frame-running-past-the-input-is-REFUSED-as-OVERRUN" as *u8, r_over, UXR_ERR_OVERRUN, ctr) 63 64 let r_cap: i64 = uxf_remux_frame(inb, inlen, out, URG_TINYCAP, meta) 65 gv_check_eq("neg-control-an-output-that-would-not-fit-is-REFUSED-as-CAPACITY-not-overflowed" as *u8, r_cap, UXR_ERR_CAPACITY, ctr) 66 67 gv_values_head() 68 gv_kv("total_mp4_bytes" as *u8, total) 69 gv_kv("parsed_id" as *u8, id) 70 gv_kv("parsed_frame_size" as *u8, fsize) 71 gv_kv("frame_src_offset_in_input" as *u8, src_off) 72 gv_kv("mdat_payload_offset" as *u8, mdat_off) 73 gv_kv("stsz_box_offset" as *u8, stsz_off) 74 gv_kv("stsz_sample_size" as *u8, uxr_r32(out, stsz_off + UXR_STSZ_SAMPLESIZE_OFF)) 75 gv_kv("box_walk_ok" as *u8, uxr_walk_ok(out, total)) 76 gv_kv("mdat_bytes_identical" as *u8, uxr_bytes_eq(out, mdat_off, inb, src_off, fsize)) 77 gv_kv("refusal_bad_vint" as *u8, r_vint) 78 gv_kv("refusal_overrun" as *u8, r_over) 79 gv_kv("refusal_capacity" as *u8, r_cap) 80 81 let rc: i64 = gv_verdict("UXF-REMUX-GATE" as *u8, ctr, "the frame bytes reach the mdat unchanged and every malformed or oversized input is refused by name; a spec-complete playable muxer is FM5 and is not claimed here" as *u8) 82 sys_exit(rc) 83 return rc 84}