AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › Symbolic/Proofs/SpecLemmas › ElfBindingProofDefs.leanTier 2 · definitions

ElfBindingProofDefs.lean🔗

Tier 2 · definitions used by the symbolic proof 1 headline theorem depend on it 4 of 37 lines trusted source ↗

trust banner in the header: none; the closure computes B4 for the symbolic proof

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

No theorem of the theorem folders uses this file: only headline theorems stated in proof files do. The tier tables do not count it, and its trust banner refers to the theorems of the theorem folders.

CLI extern-contract satisfiability predicate

Defines CompExternsSatisfiableCli, asserting the joint satisfiability of ExternInterpretationTotalOnUsedSymbols, ExternContractsHoldCli, and HooksMatchInterpretation.

@[expose] public section
set_option autoImplicit false
namespace DY.Libsignal.Composed.Refinement.Cli
open CryptoProofLib.Refinement (ExternInterpretation)
open CryptoVerification.SignalSession (CliHooks)

def CompExternsSatisfiableCli used only by headline theorems stated in proof filesL32–38 ↗#

Joint satisfiability of extern totality, CLI extern contracts, and hook agreement.

def CompExternsSatisfiableCli : Prop := ∃ (interp : ExternInterpretation) (W : CliHooks), ExternInterpretationTotalOnUsedSymbols interp ∧ ExternContractsHoldCli interp ∧ HooksMatchInterpretation interp W
end DY.Libsignal.Composed.Refinement.Cli