code wiki / _hdl_build / nx_profile_backup_gate.nx

nx_profile_backup_gate.nx

buildroot/runtime/_hdl_build/nx_profile_backup_gate.nx

4792 B99 linesdepth 8pulls 14 transitivereach 0 importersview sourcekind gate/prooftopic profile
docsdependenciesstructsconstsfunctions

about

nx_profile_backup_gate.nx -- gate for the ENCRYPTED PROFILE BACKUP (R5, "two is one one is none"). Proves on /tmp fixtures with a FIXED test ikm (mechanism proof; the runner uses /etc/machine-id): T1 backup-with-built-in-roundtrip returns 0 (a backup that doesn't restore is not a backup) T2 restore to a new file is BYTE-IDENTICAL to the source (binary-safe incl NUL bytes) T3 NEG: one flipped ciphertext byte -> restore MUST fail (Poly1305 auth = tamper-evident) T4 NEG: wrong ikm (another machine) -> restore MUST fail (machine-bound) T5 encrypted-at-rest: the blob must NOT contain the known plaintext marker (it is really encrypted) expect_exit: 0 license_tier: ORIGINAL

dependencies 1 imports · 0 importers

nx_profile_backup.nx nx_profile_backup_gate.nx

imports: nx_profile_backup.nx

imported by: nobody (leaf or entry point)

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

main t_pw pb_slen sys_openat_wr pb_backup_file sys_mmap sys_read_file sys_openat_rd sys_lseek sys_mmap ↻ sys_read sys_close pb_rand sys_openat_rd ↻ sys_read ↻ sys_close ↻ pb_derive_key sys_mmap ↻ hkdf_extract sys_mmap ↻ hmac_sha256 sys_mmap ↻ sha256_digest sys_mmap ↻ sha256_init sha256_update sha256_final sha256_init ↻ sha256_update ↻ sha256_final ↻ hkdf_expand sys_mmap ↻ hmac_sha256 ↻ nx_chacha20_poly1305_encry sys_mmap ↻ aead_derive_otk sys_mmap ↻ chacha20_block sys_mmap ↻ _chacha20_set_consts_key

structs

none

consts

none

functions

11func t_pw(s: *u8) -> i64 { sys_write(1, s, pb_slen(s)); return 0 }
called by 2: chkmain calls 1: pb_slen
12func t_pn(v: i64) -> i64
called by 1: main
16func chk(name: *u8, ok: i64, pass: *i64) -> i64
called by 1: main calls 1: t_pw
21func t_contains(hay: *u8, n: i64, needle: *u8) -> i64
called by 1: main calls 1: pb_slen
27func main() -> i64