code wiki / _hdl_build / nx_doc_vault_gate.nx

nx_doc_vault_gate.nx

buildroot/runtime/_hdl_build/nx_doc_vault_gate.nx

6475 B138 linesdepth 3pulls 4 transitivereach 0 importersview sourcekind gate/prooftopic doc
docsdependenciesstructsconstsfunctions

about

nx_doc_vault_gate.nx -- GATE for LEGAL D1 (nx_doc_vault). Drives the REAL vault and asserts the retention invariants: ADDITIVE+VERSIONED : 3 versions of doc A -> version_count(A)=3, current is version 3 (older versions retained, not overwritten). SINGLE-AUTHORITATIVE: exactly one is_current per doc (UETA 16). CHAIN TAMPER-EVIDENT: verify_chain(A)=OK; corrupt a non-final version's hash -> CHAIN_BROKEN; restore -> OK (UETA 12). SOFT-DELETE KEEPS HISTORY: soft_delete(A) -> no current, but version_count(A) still 3 (Rule 13 additive-only). SEAL ATTACH : a D5 seal attaches to the CURRENT version only. TENANT ISOLATION : valid tid accepted; '.'/'/'/empty rejected (no cross-tenant traversal -- MRPC 1.6 confidentiality). MULTI-DOC : adding doc B leaves doc A's history untouched. Evidence -> knowledge/status/doc_vault.log license_tier: ORIGINAL

dependencies 3 imports · 0 importers

nx_doc_vault.nx nx_syscalls.nx nx_gate_verdict.nx nx_doc_vault_gate.nx

imports: nx_doc_vault.nxnx_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

main 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 ↻ nx_vault_add nx_vault_version_count nx_vault_current_idx nx_vault_current_count nx_vault_verify_chain nx_vault_attach_seal nx_vault_current_idx ↻ nx_vault_soft_delete nx_vault_current_idx ↻ nx_vault_valid_tid ew sys_write ↻ ewn sys_mmap ↻ sys_write ↻ sys_openat_append sys_close gv_ctr sys_mmap ↻ gv_verdict gv_note_bare_rate gv_bare_rate gv_at gv_obj_has_n

structs

none

consts

22const DV_LOG: *u8 = "knowledge/status/doc_vault.log"

functions

24func ew(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 }
called by 1: main calls 1: sys_write
25func ewn(fd: i64, v: i64) -> i64
called by 1: main calls 2: sys_mmapsys_write
35func main() -> i64