nx_uxf_mp4box_gate.nx source
↩ module page · 128 lines · 7631 B
1// nx_uxf_mp4box_gate.nx -- the D001 MIGRATION of nx_uxf_mp4box_test onto nx_gate_verdict (2026-09-06).
2//
3// IT DRIVES THE EXTRACTED LIB, NOT A THIRD COPY. nx_uxf_mp4box_test carried its own mp4_w32, mp4_r32,
4// mp4_4cc, mp4_box_begin and mp4_box_end, which are the same primitives now shipping in nx_uxf_remux.nx as
5// uxr_w32, uxr_r32, uxr_4cc, uxr_box_begin and uxr_box_end. Pointing the teeth at the lib keeps ONE MP4 box
6// writer in the estate. The 4cc comparison is done here with the lib's own uxr_bytes_eq rather than by adding
7// a helper to a lib that is already bite-proven, because editing a proven lib to satisfy a test invalidates
8// the proof for no capability gain.
9//
10// ALL FOUR ORIGINAL TEETH PRESERVED IN PREDICATE, split where the original bundled several claims into one
11// boolean: the walk's ALIGNMENT and its BOX COUNT are separate teeth, and each of the three expected box types
12// is its own tooth, so a failure names which box is wrong rather than reporting that the tree is wrong.
13// license_tier: ORIGINAL No hw writes (Rule 26).
14import "nx_gate_verdict.nx"
15import "nx_syscalls.nx"
16import "nx_uxf_remux.nx"
17
18const UM_OUT: i64 = 65536
19const UM_TAG: i64 = 8
20const UM_WANT_FTYP_SIZE: i64 = 24 // 8 header + isom + minor + isom + mp41
21const UM_WANT_TOPLEVEL: i64 = 2 // ftyp and moov
22const UM_MVHD_PAYLOAD: i64 = 100
23const UM_HDR: i64 = 8
24const UM_TYPE_OFF: i64 = 4 // the 4cc type sits at box_start+4, not box_start
25const UM_HIGHBYTE_KAT: i64 = 16909060 // 0x01020304 -- FOUR DISTINCT NON-ZERO BYTES. Every box size this
26 // gate builds (24, 116, 108, 140) fits in ONE byte, so every
27 // high-order byte of every uxr_r32 read here is ZERO and the
28 // 16777216 / 65536 / 256 multipliers are untested BY CONSTRUCTION.
29 // nx_gate_bite proved it on 2026-09-06: mutating 16777216 and the
30 // buf[off+1] index produced two VALID mutants and BOTH survived all
31 // nine GREEN teeth, because 0 times anything is still 0.
32
33// count top-level boxes and report whether their sizes tile the buffer exactly
34func um_walk_count(buf: *u8, n: i64, out_count: *i64) -> i64 {
35 var off: i64 = 0
36 var c: i64 = 0
37 while (off + UM_HDR) <= n {
38 let sz: i64 = uxr_r32(buf, off)
39 if sz < UM_HDR { out_count[0] = c; return 0 }
40 off = off + sz
41 c = c + 1
42 }
43 out_count[0] = c
44 if off == n { return 1 }
45 return 0
46}
47
48func main(argc: i64, argv: *i64) -> i64 {
49 let ctr: *i64 = gv_ctr()
50 gv_head("nx_uxf_remux MP4 box primitives -- the OUTPUT side of an MKV to MP4 rewrap" as *u8)
51
52 let out: *u8 = sys_mmap(UM_OUT)
53 var off: i64 = 0
54
55 // ftyp: major isom, minor 0x200, compatible isom and mp41
56 let ftyp: i64 = off
57 off = uxr_box_begin(out, off, 102, 116, 121, 112)
58 off = uxr_4cc(out, off, 105, 115, 111, 109)
59 off = uxr_w32(out, off, 512)
60 off = uxr_4cc(out, off, 105, 115, 111, 109)
61 off = uxr_4cc(out, off, 109, 112, 52, 49)
62 off = uxr_box_end(out, ftyp, off)
63 let ftyp_size: i64 = off - ftyp
64
65 // moov containing an mvhd with a 100-byte payload
66 let moov: i64 = off
67 off = uxr_box_begin(out, off, 109, 111, 111, 118)
68 let mvhd: i64 = off
69 off = uxr_box_begin(out, off, 109, 118, 104, 100)
70 var z: i64 = 0
71 while z < UM_MVHD_PAYLOAD { out[off] = 0 as u8; off = off + 1; z = z + 1 }
72 off = uxr_box_end(out, mvhd, off)
73 off = uxr_box_end(out, moov, off)
74 let total: i64 = off
75
76 // expected 4cc tags, compared with the lib's own byte comparator
77 let t_ftyp: *u8 = sys_mmap(UM_TAG); uxr_4cc(t_ftyp, 0, 102, 116, 121, 112)
78 let t_moov: *u8 = sys_mmap(UM_TAG); uxr_4cc(t_moov, 0, 109, 111, 111, 118)
79 let t_mvhd: *u8 = sys_mmap(UM_TAG); uxr_4cc(t_mvhd, 0, 109, 118, 104, 100)
80
81 let cnt: *i64 = sys_mmap(UM_TAG) as *i64
82 let aligned: i64 = um_walk_count(out, total, cnt)
83
84 // BIND THE GOOD WALK'S COUNT BEFORE THE NEG-CONTROL RE-WALKS INTO THE SAME OUT-PARAMETER. Restoring the
85 // BUFFER below cannot undo a value already written into cnt, so emitting cnt[0] after that re-walk
86 // published the CORRUPT walk's 0 under the good walk's name while T2b passed on 2 (measured 2026-09-06).
87 let toplevel_good: i64 = cnt[0]
88
89 gv_check_eq("T1 the ftyp box size back-patched to 24, header plus four payload words" as *u8, ftyp_size, UM_WANT_FTYP_SIZE, ctr)
90 gv_check_eq("T2a the top-level walk lands exactly on the buffer end, so every size back-patch is consistent" as *u8, aligned, 1, ctr)
91 gv_check_eq("T2b the walk finds exactly two top-level boxes" as *u8, cnt[0], UM_WANT_TOPLEVEL, ctr)
92 gv_check("T3a the first top-level box types as ftyp, read at box start plus four" as *u8, uxr_bytes_eq(out, ftyp + UM_TYPE_OFF, t_ftyp, 0, 4), ctr)
93 gv_check("T3b the second top-level box types as moov" as *u8, uxr_bytes_eq(out, moov + UM_TYPE_OFF, t_moov, 0, 4), ctr)
94 gv_check("T3c the NESTED box inside moov types as mvhd, so nesting is real and not adjacency" as *u8, uxr_bytes_eq(out, mvhd + UM_TYPE_OFF, t_mvhd, 0, 4), ctr)
95 gv_check_eq("T3d the moov box encloses the mvhd box, its size covering header plus child" as *u8, uxr_r32(out, moov), (UM_HDR + UM_HDR + UM_MVHD_PAYLOAD), ctr)
96
97 // T4 HIGH-BYTE COVERAGE, added 2026-09-06 because a bite proved the teeth above cannot see it. Uses its
98 // OWN buffer so it cannot perturb the tree the walk teeth just measured. A value with four distinct
99 // non-zero bytes round-trips only if EVERY multiplier and EVERY byte index in uxr_w32 and uxr_r32 is
100 // right; with the single-byte sizes above, all three multipliers could be wrong and nothing would fail.
101 let hbuf: *u8 = sys_mmap(UM_TAG)
102 uxr_w32(hbuf, 0, UM_HIGHBYTE_KAT)
103 gv_check_eq("T4 HIGH BYTES: a 32-bit value with four distinct non-zero bytes round-trips through uxr_w32 and uxr_r32, so every multiplier and byte index is load-bearing rather than multiplied by a zero byte" as *u8, uxr_r32(hbuf, 0), UM_HIGHBYTE_KAT, ctr)
104
105 // neg-control: corrupt the first box size to something smaller than a header and the walk MUST refuse
106 uxr_w32(out, 0, 3)
107 let corrupt_aligned: i64 = um_walk_count(out, total, cnt)
108 gv_check_eq("neg-control-a-box-size-below-the-header-length-is-DETECTED-and-the-walk-refuses" as *u8, corrupt_aligned, 0, ctr)
109 gv_check_eq("neg-control-the-corrupt-walk-CLOBBERS-the-shared-counter-which-is-why-the-published-count-is-bound-before-it" as *u8, cnt[0], 0, ctr)
110 uxr_w32(out, 0, ftyp_size) // restores the BUFFER only -- it cannot undo cnt[0], which is why toplevel_good is bound above
111
112 gv_values_head()
113 gv_kv("ftyp_size" as *u8, ftyp_size)
114 gv_kv("moov_size" as *u8, uxr_r32(out, moov))
115 gv_kv("mvhd_size" as *u8, uxr_r32(out, mvhd))
116 gv_kv("total_bytes" as *u8, total)
117 gv_kv("toplevel_box_count" as *u8, toplevel_good)
118 gv_kv("toplevel_box_count_after_corrupt_walk" as *u8, cnt[0])
119 gv_kv("walk_aligned_on_good_tree" as *u8, aligned)
120 gv_kv("walk_aligned_on_corrupt_size" as *u8, corrupt_aligned)
121 gv_kv("mvhd_payload_bytes" as *u8, UM_MVHD_PAYLOAD)
122 gv_kv("high_byte_roundtrip" as *u8, uxr_r32(hbuf, 0))
123 gv_kv("high_byte_kat" as *u8, UM_HIGHBYTE_KAT)
124
125 let rc: i64 = gv_verdict("UXF-MP4BOX-GATE" as *u8, ctr, "box sizes back-patch correctly, the tree walks aligned to its exact length, nesting is real, and a size below the header length is detected rather than walked past" as *u8)
126 sys_exit(rc)
127 return rc
128}