Init.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 32 of 100 lines trusted 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.

SPQR V1: initial state (spqrV1Init) and session instances

Trusted: definitions used by the statement. SpqrModel.spqr (LibsignalTripleRatchet.lean) sets Spqr.init to the empty state of spqr::Version::V0, whereas libsignal initializes SPQR with version = V1 and min_version = V1 (rust/protocol/src/ratchet.rs:83–89, 146–152). This file defines libsignal's V1 initial state (spqrV1Init) and the resulting Spqr instances (spqrV1Session and spqrV1SessionUniformCoins).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.LibsignalSession (Spqr SpqrDirection ShaCompress)

open CryptoVerification.LibsignalTripleRatchet (SpqrModel)

def Direction.ofSpqrDirectionL31–34 ↗#

Converts the session model's SpqrDirection to spqr::Direction.

def Direction.ofSpqrDirection : SpqrDirection → Direction
  | .a2b => .a2b
  | .b2a => .b2a

def libsignalChainParamsL36–38 ↗#

spqr_chain_params(self_connection) (rust/protocol/src/ratchet.rs:27–38).

def libsignalChainParams (selfSession : Bool) : ChainParams :=
  { maxJump := if selfSession then BitVec.allOnes 32 else 25000#32, maxOooKeys := 2000#32 }

1 declaration not shown (lines 40–40): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.libsignalChainParams_false

def libsignalSpqrParamsL42–48 ↗#

spqr::Params passed by libsignal's session constructors (ratchet.rs:83–89, 146–152).

def libsignalSpqrParams (selfSession : Bool) (dir : SpqrDirection) (k : BitVec 256) : Params where
  direction := Direction.ofSpqrDirection dir
  version := .v1
  minVersion := .v1
  authKey := CryptoGames.HMAC.keyToBytes32 k
  chainParams := libsignalChainParams selfSession

def spqrV1InitialStateForL50–55 ↗#

V1 initial SPQR state for a non-self libsignal session (spqr::initial_state, spqr/src/lib.rs:211–235), falling back to [] only on unreachable init_inner errors.

def spqrV1InitialStateFor (D : SpqrApiDeps) (dir : SpqrDirection) (k : BitVec 256) : List (BitVec 8) :=
  match initialState D (libsignalSpqrParams false dir k) with
  | .ok st => st
  | .error _ => []

def spqrV1InitL57–60 ↗#

spqrV1InitialStateFor instantiated at spqrDeps F K.

def spqrV1Init (F : ShaCompress) (K : MlKem) (dir : SpqrDirection) (k : BitVec 256) :
    List (BitVec 8) :=
  spqrV1InitialStateFor (spqrDeps F K) dir k

3 declarations not shown (lines 62–73): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalTripleRatchet.SpqrModel.spqrWith, CryptoVerification.LibsignalSpqrV1.spqrV1Session, CryptoVerification.LibsignalSpqrV1.spqrV1Session_init

Uniform coins: spqrV1SessionUniformCoins

abbrev coinBytesL77–79 ↗#

Little-endian 64-byte view of r : BitVec 512 (toLEBytes 64 r).

abbrev coinBytes (r : BitVec 512) : List (BitVec 8) :=
  CryptoVerification.LibsignalAesCbc.toLEBytes 64 r

def spqrV1SessionUniformCoinsL81–85 ↗#

SPQR V1 Spqr session instance parameterized by uniform 512-bit coins (coinBytes r), which suffice for every States.send branch (generate reads 64 bytes, encaps1 reads 32).

def spqrV1SessionUniformCoins (F : ShaCompress) (K : MlKem) : Spqr (List (BitVec 8)) (BitVec 512) :=
  ⟨spqrV1Init F K, fun st r => (spqrV1 F K).send st (coinBytes r), (spqrV1 F K).recv,
    fun st r => (spqrV1 F K).sendPanics st (coinBytes r), (spqrV1 F K).recvPanics⟩

4 declarations not shown (lines 87–98): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.spqrV1SessionB_init, CryptoVerification.LibsignalSpqrV1.spqrV1SessionB_send, CryptoVerification.LibsignalSpqrV1.spqrV1SessionB_recv, CryptoVerification.LibsignalSpqrV1.coinBytes_length

end CryptoVerification.LibsignalSpqrV1