code wiki / (root) / nx_uxf_mp4box_test.nx

nx_uxf_mp4box_test.nx

buildroot/runtime/nx_uxf_mp4box_test.nx

6468 B123 linesdepth 2pulls 2 transitivereach 0 importersview sourcekind gate/prooftopic uxf
docsdependenciesstructsconstsfunctions

about

nx_uxf_mp4box_test.nx -- UXF arc #2 (real remux), rung 1: the ISO-BMFF (MP4) container BOX primitive -- the OUTPUT side of an MKV->MP4 remux. An MP4 is a tree of boxes: [u32be size (incl. 8-byte header)][4cc type][payload | child boxes]. This builds a real box WRITER (begin/end with size back-patching) + a box PARSER (walk), then KAT-proves: a built ftyp + moov{mvhd} tree has correct sizes, parses back to the right types, nests correctly, and a corrupted size is DETECTED (neg-control). HONEST SCOPE: this is the container-construction primitive (the foundation for "rewrap into MP4"). It does NOT yet emit a *playable* MP4 (needs populated sample tables stsd/stts/stsc/stsz/stco) nor parse MKV/EBML (the input side) -- those are the named downstream rungs of #2. No hardware writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL

dependencies 1 imports · 0 importers

nx_syscalls.nx nx_uxf_mp4box_test.nx

imports: nx_syscalls.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main m_puts sys_write sys_mmap mp4_box_begin mp4_w32 mp4_4cc mp4_4cc ↻ mp4_w32 ↻ mp4_box_end mp4_w32 ↻ m_putn sys_mmap ↻ sys_write ↻ mp4_walk mp4_r32 mp4_type_is sys_exit

structs

none

consts

none

functions

14func m_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
called by 1: main calls 1: sys_write
15func m_putn(v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) } let t: *u8 = sys_mmap(28); var k: i64 = 0; if m == 0 { t[0] = 48 as u8; k = 1 } while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 } sys_write(1, bb, k); return 0 }
called by 1: main calls 2: sys_mmapsys_write
17func mp4_w32(out: *u8, off: i64, v: i64) -> i64
24func mp4_r32(buf: *u8, off: i64) -> i64
called by 1: mp4_walk
27func mp4_4cc(out: *u8, off: i64, a: i64, b: i64, c: i64, d: i64) -> i64
called by 2: mp4_box_beginmain
31func mp4_type_is(buf: *u8, off: i64, a: i64, b: i64, c: i64, d: i64) -> i64
called by 1: main
39func mp4_box_begin(out: *u8, off: i64, a: i64, b: i64, c: i64, d: i64) -> i64
called by 1: main calls 2: mp4_w32mp4_4cc
45func mp4_box_end(out: *u8, start: i64, curoff: i64) -> i64
called by 1: main calls 1: mp4_w32
51func mp4_walk(buf: *u8, n: i64, out_first_off: *i64, out_count: *i64) -> i64
called by 1: main calls 1: mp4_r32
67func main() -> i64