code wiki / _hdl_build / nx_conductor_notes_migration_gate.nx

nx_conductor_notes_migration_gate.nx

buildroot/runtime/_hdl_build/nx_conductor_notes_migration_gate.nx

10911 B266 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic conductor
docsdependenciesstructsconstsfunctions

about

nx_conductor_notes_migration_gate.nx -- WMS-R0b DELIVERABLE B referee. Proves the MIGRATED conductor-notes record write (multi-_fp/_fn sequence -> single atomic locked fa_appendz) produces ZERO torn lines under concurrency, AND proves the detector can actually SEE tearing via the mandatory in-gate NEGATIVE CONTROL: the OLD _fp/_fn multi-write path, which MUST tear (bad_torn > 0) -- if it doesn't, the test is worthless => RED (no false green). GOOD lane (the migration): N workers fork concurrently, each emits NRECS NOTES records the NEW way -- assemble the whole "NOTES epoch=<e> weakest_arc=<arc> call=...:triage ... verdict=DRILL-CALLED" line into one buffer + ONE fa_appendz (the exact cn_emit_red shape). Expect ZERO torn lines and ALL N*NRECS lines present. BAD lane (NEGATIVE CONTROL): same concurrency, but each record emitted the ORIGINAL way -- a SEQUENCE of separate _fp/_fn sys_write() calls to one O_APPEND fd ("NOTES epoch=" then the number then " weakest_arc=" ...). Concurrent workers interleave between those writes -> torn lines MUST appear. TAMPER: an oversized record (rec_len+1 > cap) must be REJECTED with -2. A line is WELL-FORMED iff it starts "NOTES epoch=" AND its last 12 bytes before the '\n' are "DRILL-CALLED" AND it contains exactly one "NOTES epoch=" head and exactly one "DRILL-CALLED" tail. Any interleaving breaks one of those -> torn. Output: rows -> stdout + knowledge/status/conductor_notes_migration_gate.log, then a verdict line. Exit 0 on GREEN, 1 on RED. Sovereign: only nx_syscalls + nx_framed_append. license_tier: ORIGINAL

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_framed_append.nx nx_conductor_notes_migration_g

imports: nx_syscalls.nxnx_framed_append.nx

imported by: nobody (leaf or entry point)

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

main sys_openat_append gp sys_write gn sys_mmap sys_write ↻ sys_now_realtime_sec sys_mmap ↻ sys_clock_gettime_real sys_openat_wr sys_close spawn_all sys_mmap ↻ sys_fork good_worker sys_mmap ↻ fa_cat fa_catn sys_mmap ↻ fa_appendz fa_append sys_mmap ↻ sys_openat_append ↻ sys_flock fa_write_all sys_write ↻ sys_close ↻ fa_len bad_worker sys_openat_append ↻ sys_write ↻ bad_num sys_mmap ↻ sys_write ↻ sys_close ↻ sys_exit sys_wait4 sys_mmap ↻ count_torn

structs

none

consts

29const NWORKERS: i64 = 16 // concurrency (matches framed_append_gate)
30const NRECS: i64 = 300 // records per worker
31const RECCAP: i64 = 256 // bounded record size (matches CN_REC_CAP)
33const GOODP: *u8 = "/tmp/cn_good.log\x00" as *u8
34const BADP: *u8 = "/tmp/cn_bad.log\x00" as *u8

functions

37func gp(logfd: i64, s: *u8) -> i64
called by 1: main calls 1: sys_write
44func gn(logfd: i64, v: i64) -> i64
called by 1: main calls 2: sys_mmapsys_write
61func good_worker(wid: i64) -> i64
79func bad_num(fd: i64, v: i64) -> i64
called by 1: bad_worker calls 2: sys_mmapsys_write
95func bad_worker(wid: i64) -> i64
113func spawn_all(which: i64) -> i64
136func slice_count(hay: *u8, a: i64, b: i64, pat: *u8, pl: i64) -> i64
called by 1: count_torn
152func count_torn(path: *u8, outs: *i64) -> i64
193func main() -> i64