LibsignalSession.lean🔗

Tier 2 · definitions used by the symbolic proof 2 headline theorems depend on it 3 of 63 lines trusted trust banner B3, trusted in part source ↗

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.

Session Image Extern Hooks (LibsignalSession)

Trusted in part. Computational/Theorems/Main.lean unfolds blackBoxHook (installed in cliHookTablePlaced); sessionExterns and logFilterAddr belong to the non-ELF session-image harness. See Computational/docs/TRUSTED_BASE.md.

Extern hook table for the loaded session image:

blackBoxHook models subtle::black_box::<u8> as the identity on the low byte of x0.
sessionExterns maps sha2::sha256::compress256 to LibsignalHmac.compress256Hook F, memcpy / memmove / memset to ProofLib's libc hooks, __rust_no_alloc_shim_is_unstable_v2 to hookNoop, subtle::black_box::<u8> to blackBoxHook, <alloc::vec::Vec<_, _>>::remove::assert_failed to Rust.panicked, and the three Rust allocator entry points to alloc.
logFilterAddr is the extern-data address of log::MAX_LOG_LEVEL_FILTER (pinned by LibsignalSessionGuards.lean); holding 0 disables log::Log::log.

@[expose] public section

namespace CryptoVerification.LibsignalSession

open Arm64 ProofLib CryptoGames CryptoGames.HMAC CryptoGames.LibsignalSession

open CryptoVerification.RustHeap CryptoVerification.LibsignalSessionRepr

def blackBoxHookL41–43 ↗#

subtle::black_box::<u8>(input = w0) -> u8: x0 := the low byte of x0; pc := lr.

def blackBoxHook (s : State) : State :=
  retHook (fun s => s.writeReg64 .x0 (((s.readReg64 .x0).setWidth 8).zeroExtend 64)) s

2 declarations not shown (lines 45–61): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSession.sessionExterns, CryptoVerification.LibsignalSession.logFilterAddr

end CryptoVerification.LibsignalSession