Model.lean🔗

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

SPQR V1: assembled models (spqrV1, spqrV1Recv)

Trusted in part. The theorems of Computational/Theorems/ use spqrV1; spqrV1Recv is checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Packages the concrete SPQR V1 models over F : ShaCompress and K : MlKem (Assemble.lean): spqrV1 F K : SpqrModel for the session model and spqrV1Recv F K : SpqrRecvModel returning the exact Option Bytes message key (DEV-SPQR2).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.LibsignalSession CryptoVerification.LibsignalTripleRatchet

def spqrV1L31–33 ↗#

Concrete SPQR V1 SpqrModel (Top.toSpqrModel instantiated with spqrDeps F K).

def spqrV1 (F : CryptoGames.LibsignalSession.ShaCompress) (K : MlKem) : SpqrModel :=
  spqrV1Assembled F K

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

CryptoVerification.LibsignalSpqrV1.spqrV1Recv, CryptoVerification.LibsignalSpqrV1.spqrV1_eq, CryptoVerification.LibsignalSpqrV1.spqrV1Recv_eq

end CryptoVerification.LibsignalSpqrV1