Main.lean
Cited in the paper
/-
Copyright 2026 Google LLC
All code is licensed under the Apache License, Version 2.0 (the "Apache 2.0"); you may not use this file except in compliance with the Apache 2.0 license. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import Computational.Specifications.LibsignalCli.StatementPqElf
public import LibsignalBinary.Specifications.SignalSession.CliBinaryPq
public import LibsignalBinary.Specifications.SignalSession.CliLabels
public import Computational.Proofs.LibsignalCli.ElfHeadlinePq
Lemma 4 and Main Theorem: Computational Correctness and Security of the libsignal-cli Binary
Trusted: the statement. Built by lake build CliElfLib. Each theorem below states a proposition from Computational/ or LibsignalBinary/ on the SHA-256-pinned AArch64 binary cliElfBytes (LibsignalBinary/) and is proved by a corresponding *_proof theorem in Computational/. See Computational/ for the trusted definitions and kernel axioms of each theorem, and Computational/ for the specification deviations referenced below.
Lemmas 1–3 (Computational/), relocatable Lemma 4, and freedom from .OutOfMemory in PQXDH mode imply the relocatable Main Theorem (main_of_lemmas_placed, Computational/); for cliElfBytes, .OutOfMemory freedom is discharged unconditionally under the 1 GiB dynamic-mapping budget (DEV-CLI12, retired).
Trusted computing base. Lean's kernel checks code bytes, relocations, addresses, and segment layout directly against cliElfBytes (Placed. / InElf, cliElf_linkedAt_unique). Symbol-name labels rest on the trusted .o extractor (libsignal_, assumption A-LINK in Computational/).
@[expose] public sectionset_option autoImplicit falsenamespace CryptoVerification.SignalSession
theorem libsignal_
Lemma 4 (binary refinement, relocatable) (CliPqxdhBinaryCorrectPlaced cliElfBytes, LibsignalBinary/). For every multi-block placement mpl linked in cliElfBytes (libsignalSessionLib.cliElfBytes mpl), cliElfBytes parses as an AArch64 ELF satisfying Placed. mpl, and for all hook implementations W and model extras X, the relocatable process Placed. mpl satisfies CliSpecPqxdh and CliSpecPqxdhNoMatch (DEV-CLI11) at primitives ⟨W.C, W. (SPQR V1) or terminates with .OutOfMemory (CliReachesOOMPlaced, DEV-CLI15).
theorem libsignal_cli_pq_binary_correct_placed :
CliPqxdhBinaryCorrectPlaced cliElfBytes := ⋯theorem libsignal_cli_elf_linked_in
Session placement witness. cliElfBytes links libsignalSessionLib at a concrete multi-block placement (libsignalSessionLib.cliElfBytes).
theorem libsignal_cli_elf_linked_in : libsignalSessionLib.LinkedIn cliElfBytes := ⋯
theorem libsignal_
Allocator placement witness. cliElfBytes links the musl mallocng allocator library VerifiedLibraries. at a concrete multi-block placement (VerifiedLibraries.cliElfBytes), discharging both LinkedAt hypotheses (mpl and mmpl) together with libsignal_cli_elf_linked_in.
theorem libsignal_cli_elf_mallocng_linked_in :
VerifiedLibraries.mallocngLib.LinkedIn cliElfBytes := ⋯
theorem libsignal_
Label gate A (CliLabelsFromObjects, LibsignalBinary/). The symbol names interpreted by the placed theorems (hooked externs, SIGABRT panic externs, and SPQR CPU-probe statics) match the symbol names extracted from the pre-link .o objects.
theorem libsignal_cli_labels_from_objects : CliLabelsFromObjects := ⋯end CryptoVerification.SignalSessionnamespace CryptoVerification.LibsignalCliopen CryptoVerification.SignalSession (cliElfBytes)
theorem libsignal_
Main Theorem (binary correctness and security, relocatable) (Cli cliElfBytes, Computational/). Across every pair of multi-block placements (mpl, mmpl) linked in cliElfBytes (libsignalSessionLib.cliElfBytes mpl, VerifiedLibraries.cliElfBytes mmpl), cliElfBytes parses as an AArch64 ELF, satisfies CliPqxdhElfCorrectPlaced mpl mmpl (allowing .OutOfMemory per DEV-CLI15), and for every point type Pt, setup S, and plaintext length ℓ satisfies CliPqxdhElfSecurePlaced mpl mmpl for all hooks W and model extras X meeting the primitive hypotheses (with no .OutOfMemory hypothesis; DEV-CLI12, retired).
theorem libsignal_cli_pq_secure_elf_binary_placed :
CliPqxdhBinaryCorrectAndSecurePlaced cliElfBytes := ⋯end CryptoVerification.LibsignalCli