code wiki / (root) / nx_meshcheck_gate.nx

nx_meshcheck_gate.nx

buildroot/runtime/nx_meshcheck_gate.nx

11846 B202 linesdepth 3pulls 4 transitivereach 0 importersview sourcekind gate/proof
docsdependenciesstructsconstsfunctions

about

nx_meshcheck_gate.nx -- proves the mesh integrity sweep, in BOTH directions, per defect class. THE POSITIVE CONTROL IS A TETRAHEDRON, and it is chosen because it is the smallest object for which every property under test is simultaneously non-trivial: 4 vertices, 4 faces, 6 edges each shared by exactly two faces traversing it in OPPOSITE directions, no loose vertices, no degeneracies, and an Euler characteristic of exactly 2. A cube would work too and would hide a winding bug behind more symmetry; a single triangle would pass most teeth vacuously because it has no shared edge at all. EVERY DEFECT CLASS GETS ITS OWN PLANTED MUTANT, because the classes have DIFFERENT REMEDIES and a detector that fires on all of them identically is one counter wearing six names. Each mutant is built at runtime from the same clean tetrahedron, so a tooth that fires is firing on exactly one injected difference.

dependencies 3 imports · 0 importers

nx_syscalls.nx nx_gate_verdict.nx nx_meshcheck.nx nx_meshcheck_gate.nx

imports: nx_syscalls.nxnx_gate_verdict.nxnx_meshcheck.nx

imported by: nobody (leaf or entry point)

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

main gv_ctr sys_mmap nxa_die sys_write sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ gv_head gv_puts sys_write ↻ mg_out sys_mmap ↻ mg_list sys_mmap ↻ mc_list_slots mg_tet_verts sys_mmap ↻ mg_tet_tris sys_mmap ↻ mc_check mc_list_slots ↻ mc_list_put sys_mmap ↻ sys_munmap mc_min mc_max mc_msort gv_subjects gv_puts ↻ gv_num

structs

none

consts

17const MG_U: i64 = 1000 // one millimetre in the micrometre units this fixture uses
18const MG_SCRATCH: i64 = 64

functions

20func mg_out() -> *i64 { return sys_mmap(MC_O_SLOTS * MC_I64) as *i64 }
called by 1: main calls 1: sys_mmap
21func mg_list() -> *i64 { return sys_mmap(mc_list_slots() * MC_I64) as *i64 }
called by 1: main calls 2: sys_mmapmc_list_slots
24func mg_tet_verts(extra: i64) -> *i64
called by 1: main calls 1: sys_mmap
35func mg_tet_tris(extra: i64) -> *i64
called by 1: main calls 1: sys_mmap
44func mg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 }
called by 1: main
45func mg_pos(a: i64) -> i64 { if a > 0 { return 1 } return 0 }
called by 1: main
46func mg_zero(a: i64) -> i64 { if a == 0 { return 1 } return 0 }
called by 1: main
47func mg_eq2(a: i64, b: i64, c: i64, d: i64) -> i64 { if a == b { if c == d { return 1 } } return 0 }
called by 1: main
48func mg_eq3(a: i64, b: i64, c: i64, d: i64, e: i64, f: i64) -> i64
called by 1: main
52func main() -> i64