LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory (ICFP'26)

Mechanized proofs accompanying the ICFP 2026 paper "LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory" (paper #60). Two complementary developments are included: Soundness (Rocq 9.0.1). Mechanized soundness theorems for the paper's two memory models — location-addressable memory (LAM) and content-addressable memory (CAM) — together with their typed-data foundation. Includes round-trip correctness of serialization/deserialization, equivalence of the deep-equality relation, correctness of shallow treeification and value duplication, preservation of deep equality under garbage-collection evacuation, encode/decode determinism and canonicity, and wrapper-freeness of decoded and committed heaps. Locality (Lean 4.27.0 + Mathlib4 v4.27.0). Mechanized locality theorem for content-defined chunking — the rolling-hash spillover distribution, and expected and worst-case bounds on the number of chunks affected by a small (depth-d) edit, together with the supporting metafunctions. The artifact has no admitted goals. The trusted base is enumerated in the README. Two files are archived in this record: locallmem-artifact-source.tgz — source archive (97 KB) for reviewers building on a stock environment with Rocq 9.0.1 and Lean 4.27.0 installed. locallmem-artifact-vm.tar.xz — self-contained QEMU VM image (2.56 GB) with both toolchains pre-installed and Mathlib4 pre-cached. Re-checks the proofs entirely offline (~22 min from a clean state on 8 vCPUs). SHA256 checksums. locallmem-artifact-source.tgz: 3744c9883e8ab8978675c35a3f537f6a0b9cd8f4e56308239db930601ea298d2. locallmem-artifact-vm.tar.xz: e19710a007747a0dbfe72700821ca33fe36f2a052e7bb74b46c9031422731fd5.