code wiki / _hdl_build / nx_coedit_gate.nx

nx_coedit_gate.nx

buildroot/runtime/_hdl_build/nx_coedit_gate.nx

11928 B201 linesdepth 3pulls 3 transitivereach 0 importersview sourcekind gate/proof

docs dependencies structs consts functions

about

nx_coedit_gate.nx -- gate for the CO-EDITING KERNEL (RGA text CRDT). The rows ARE the CRDT laws: 1 type+apply a session of position-based edits materializes exactly 2 CONVERGENCE merge(A,B) and merge(B,A) apply to the SAME bytes (pinned): concurrent append after the same char ordered by the (counter,replica) tie-break; a concurrent delete lands 3 tombstone-anchor inserting AFTER a concurrently-DELETED char still places correctly (RGA property) 4 idempotent-remerge merge(AB, A) == AB (byte-equal log; re-applying ops is a no-op) 5 edit-del position-based delete produces the pinned text 6 conflict-loud same op id with DIFFERENT content = LOUD protocol violation (never silent) 7 badref-loud insert after an unknown id = LOUD license_tier: ORIGINAL

dependencies 2 imports · 0 importers

imports: nx_syscalls.nxnx_gate_verdict.nx

imported by: nobody (leaf or entry point)

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

structs

none

consts

none

functions

14	func eg_slen(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8) { n=n+1 } return n } called by 4: eg_p eg_write eg_has eg_fileis
15	func eg_p(s: *u8) -> i64 { sys_write(1, s, eg_slen(s)); return 0 } called by 2: eg_row main calls 2: sys_write eg_slen
16	func eg_cat(dst: u8, off: i64, s: u8) -> i64 { var i: i64=0; while s[i]!=(0 as u8) { dst[off+i]=s[i]; i=i+1 } return off+i } called by 1: main
17	func eg_catn(dst: *u8, off: i64, v: i64) -> i64 called by 1: main calls 1: sys_mmap
23	func eg_write(path: u8, content: u8) -> i64 called by 1: main calls 4: sys_openat_wr sys_write eg_slen sys_close
27	func eg_readall(path: u8, szout: i64) -> *u8 called by 4: eg_has eg_fileis eg_fileeq eg_cp calls 4: sys_openat_rd sys_mmap sys_read sys_close
33	func eg_runv(elf: u8, args: i64, outpath: *u8) -> i64 called by 1: main calls 7: sys_fork sys_openat_wr sys_dup3 sys_mmap sys_execve sys_exit+1
48	func eg_has(path: u8, needle: u8) -> i64 called by 1: main calls 3: sys_mmap eg_readall eg_slen
55	func eg_fileis(path: u8, exact: u8) -> i64 called by 1: main calls 3: sys_mmap eg_readall eg_slen
63	func eg_fileeq(p1: u8, p2: u8) -> i64 called by 1: main calls 2: sys_mmap eg_readall
74	func eg_args6(a1: u8, a2: u8, a3: u8, a4: u8, a5: u8, a6: u8) -> *i64 called by 1: main calls 1: sys_mmap
79	func eg_row(name: *u8, pass: i64) -> i64 called by 1: main calls 1: eg_p
83	func eg_mkempty(path: *u8) -> i64 called by 1: main calls 2: sys_openat_wr sys_close
88	func eg_cp(src: u8, dst: u8) -> i64 called by 1: main calls 5: sys_mmap eg_readall sys_openat_wr sys_write sys_close
96	func main(argc: i64, argv: *i64) -> i64 calls 21: eg_p sys_openat_rd sys_close eg_runv eg_args6 eg_mkempty+15