Top.lean🔗

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

Declarations on this page (28)

SPQR V1: top-level protocol model (src/lib.rs)

Trusted in part. The theorems of Computational/Theorems/ use only part of this file (see Computational/docs/TRUSTED_BASE.md): the rest (toSpqrRecvModel, SecretOutput and its accessors, CurrentVersion / currentVersion, decodeVarintChecked, decodeVarintCheckedLoop, sendPanicsB, recvPanicsSaltB, and the error-conversion helpers fromEncodingError, fromSerializeError, fromAuthenticatorError of Error, SpqrApiError and SpqrApiResult) is checked by Lean.

Models spqr/src/lib.rs over PqRatchetStatePB and SpqrApiDeps: API records (Params, Send, Recv), version and initialization (stateVersion, decodeState, initInner, initialState, currentVersion), top-level send (sendAfterStates) and recv, explicit panic type SpqrApiPanic and predicates (sendPanicsPureB, recvPanicsB), adapters toSpqrModel and toSpqrRecvModel (DEV-SPQR2, DEV-LS25), empty-state agreement (recv_empty_state, toSpqrModel_recv_empty, not_toSpqrModel_recvPanics_empty), and kernel-checked guards (guard_version_and_types, guard_varint_and_preamble).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.HKDF (Salt)

open CryptoVerification.LibsignalTripleRatchet (SpqrModel)

Core types and conversions (src/lib.rs)

structure ParamsL45–52 ↗#

Session initialization parameters (pub struct Params<'a>, src/lib.rs:55–61).

structure Params where
  direction : Direction
  version : Version
  minVersion : Version
  authKey : Bytes
  chainParams : ChainParams := ChainParams.default
  deriving DecidableEq, Repr, Inhabited

6 declarations not shown (lines 54–89): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.SecretOutput.send, CryptoVerification.LibsignalSpqrV1.SecretOutput, CryptoVerification.LibsignalSpqrV1.SecretOutput.none, CryptoVerification.LibsignalSpqrV1.SecretOutput.recv, CryptoVerification.LibsignalSpqrV1.SecretOutput.sendSecret, CryptoVerification.LibsignalSpqrV1.SecretOutput.recvSecret, CryptoVerification.LibsignalSpqrV1.SecretOutput.secret, CryptoVerification.LibsignalSpqrV1.SecretOutput.hasSecret, CryptoVerification.LibsignalSpqrV1.CurrentVersion.stillNegotiating, CryptoVerification.LibsignalSpqrV1.CurrentVersion.negotiationComplete, CryptoVerification.LibsignalSpqrV1.CurrentVersion

structure SendL91–96 ↗#

Output of send (pub struct Send, src/lib.rs:242–246).

structure Send where
  state : SerializedState
  msg : SerializedMessage
  key : MessageKey
  deriving DecidableEq, Repr, Inhabited

structure RecvL98–102 ↗#

Output of recv (pub struct Recv, src/lib.rs:327–330).

structure Recv where
  state : SerializedState
  key : MessageKey
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.Error.fromEncodingError, CryptoVerification.LibsignalSpqrV1.Error.fromSerializeError, CryptoVerification.LibsignalSpqrV1.Error.fromAuthenticatorError

Explicit panic sites and result types (src/lib.rs)

inductive SpqrApiPanicL116–141 ↗#

Rust panic sites in src/lib.rs and its callees (overflow-checks = true).

inductive SpqrApiPanic where
  | chain (p : ChainPanic)
  | spqr (p : SpqrPanic)
  | v1
  /-- `src/lib.rs:292`: `assert!(key.is_none())` in `send` when `chain` is `None`. -/
  | sendKeySomeWithoutChain
  /-- `src/lib.rs:299`: `msg.epoch - 1` underflow in `send`. -/
  | sendEpochUnderflow
  /-- `src/lib.rs:305`: `assert!(!msg.is_empty())` in `send`. -/
  | sendMsgEmpty
  /-- `src/lib.rs:306`: `assert_eq!(msg[0], Version::V1.into())` in `send`. -/
  | sendMsgBadVersion
  /-- `src/lib.rs:425`: `assert!(current_version > 0 && version_still_negotiating)` in `recv`. -/
  | recvNegotiateAssert
  /-- `src/lib.rs:429`: `version_negotiation.as_ref().expect("still negotiating")` in `recv`. -/
  | recvExpectStillNegotiating
  /-- `src/lib.rs:433`: `msg.version.try_into().expect("should support all lower versions")` in `recv`. -/
  | recvExpectLowerVersion
  /-- `src/lib.rs:462`: `msg.epoch - 1` underflow in `recv`. -/
  | recvEpochUnderflow
  /-- `src/lib.rs:541`: `from[start_at + i]` bounds check in `decode_varint`. -/
  | decodeVarintBounds
  /-- `src/lib.rs:542`: `<< (7 * i as i32)` shift overflow when `7 * i >= 64` in `decode_varint`. -/
  | decodeVarintShiftOverflow
  deriving DecidableEq, Repr, Inhabited

inductive SpqrApiErrorL143–147 ↗#

Outcome of a fallible top-level SPQR operation: clean Err(Error) or SpqrApiPanic.

inductive SpqrApiError where
  | err (e : Error)
  | panic (p : SpqrApiPanic)
  deriving DecidableEq, Repr, Inhabited

namespace SpqrApiError

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

CryptoVerification.LibsignalSpqrV1.SpqrApiError.isPanic

def ofChainErrorL155–157 ↗#

def ofChainError : ChainError → SpqrApiError
  | .err e => .err e
  | .panic p => .panic (.chain p)

end SpqrApiError

abbrev SpqrApiResultL161 ↗#

abbrev SpqrApiResult (α : Type) := Except SpqrApiError α

namespace SpqrApiResult

def ofErrorL165–168 ↗#

def ofError {α : Type} (r : Except Error α) : SpqrApiResult α :=
  match r with
  | .ok v => .ok v
  | .error e => .error (.err e)

def ofPanicL170–173 ↗#

def ofPanic {α : Type} (r : Except SpqrApiPanic α) : SpqrApiResult α :=
  match r with
  | .ok v => .ok v
  | .error p => .error (.panic p)

def ofChainPanicL175–178 ↗#

def ofChainPanic {α : Type} (r : Except ChainPanic α) : SpqrApiResult α :=
  match r with
  | .ok v => .ok v
  | .error p => .error (.panic (.chain p))

def ofChainResultL180–183 ↗#

def ofChainResult {α : Type} (r : ChainResult α) : SpqrApiResult α :=
  match r with
  | .ok v => .ok v
  | .error ce => .error (SpqrApiError.ofChainError ce)

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

CryptoVerification.LibsignalSpqrV1.SpqrApiResult.isPanic

end SpqrApiResult

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

CryptoVerification.LibsignalSpqrV1.decodeVarintCheckedLoop, CryptoVerification.LibsignalSpqrV1.decodeVarintChecked

PqRatchetStatePB and SpqrApiDeps dependency bundle

structure PqRatchetStatePBL233–238 ↗#

pqrpb::PqRatchetState (src/proto/pq_ratchet.proto:25–38), parameterized by V1StatePB.

structure PqRatchetStatePB (V1StatePB : Type) where
  inner : Option V1StatePB := none
  versionNegotiation : Option VersionNegotiationPB := none
  chain : Option ChainPB := none
  deriving DecidableEq, Repr, Inhabited

structure SpqrApiDepsL240–257 ↗#

Abstract dependency bundle for src/lib.rs over PqRatchetState codecs (Proto.lean) and V1 States / Message operations (States.lean).

structure SpqrApiDeps where
  V1StatePB : Type
  decodeState : Bytes → Except Unit (PqRatchetStatePB V1StatePB)
  encodeState : PqRatchetStatePB V1StatePB → Bytes
  States : Type
  statesFromPb : V1StatePB → SpqrApiResult States
  statesIntoPb : States → V1StatePB
  MessageV1 : Type
  /-- `States::send(self, rng)` (`src/v1/chunked/states.rs:115–289`), returning
  `((msg, key, state), remainingTape)`. -/
  statesSend : States → Bytes → SpqrApiResult (MessageV1 × Option EpochSecret × States) × Bytes
  statesRecv : States → MessageV1 → SpqrApiResult (Option EpochSecret × States)
  msgSerialize : MessageV1 → BitVec 32 → Bytes
  msgDeserialize : Epoch → Bytes → SpqrApiResult MessageV1
  msgEpoch : MessageV1 → Epoch
  initV1Inner : Direction → Bytes → Except SpqrApiPanic V1StatePB

state_version, decode_state, init_inner, initial_state, current_version

def stateVersionL261–264 ↗#

def stateVersion {V1StatePB : Type} (state : PqRatchetStatePB V1StatePB) : Version :=
  match state.inner with
  | none => .v0
  | some _ => .v1

def decodeStateL266–274 ↗#

spqr::decode_state (src/lib.rs:495–505).

def decodeState (D : SpqrApiDeps) (s : SerializedState) :
    Except Error (PqRatchetStatePB D.V1StatePB) :=
  if s.isEmpty then
    .ok { inner := none, versionNegotiation := none, chain := none }
  else
    match D.decodeState s with
    | .ok st => .ok st
    | .error () => .error .stateDecode

def initInnerL276–280 ↗#

def initInner (D : SpqrApiDeps) (v : Version) (d : Direction) (authKey : Bytes) :
    Except SpqrApiPanic (Option D.V1StatePB) :=
  match v with
  | .v0 => .ok none
  | .v1 => some <$> D.initV1Inner d authKey

def initialStateL282–299 ↗#

spqr::initial_state (src/lib.rs:211–235).

def initialState (D : SpqrApiDeps) (params : Params) : SpqrApiResult SerializedState :=
  match params.version with
  | .v0 => .ok emptyState
  | .v1 => do
    let inner ← SpqrApiResult.ofPanic (initInner D params.version params.direction params.authKey)
    let versionNegotiation : Option VersionNegotiationPB :=
      some {
        authKey := params.authKey
        direction := params.direction.toI32
        minVersion := params.minVersion.toI32
        chainParams := some params.chainParams.intoPb
      }
    .ok <| D.encodeState {
      inner := inner
      chain := none
      versionNegotiation := versionNegotiation
    }

def currentVersionL301–310 ↗#

spqr::current_version (src/lib.rs:248–261).

def currentVersion (D : SpqrApiDeps) (state : SerializedState) : Except Error CurrentVersion := do
  let statePb ← decodeState D state
  let version := stateVersion statePb
  match statePb.versionNegotiation with
  | none => .ok (.negotiationComplete version)
  | some vn =>
    match Version.fromI32? vn.minVersion with
    | some minVer => .ok (.stillNegotiating version minVer)
    | none => .error .stateDecode

send and recv (src/lib.rs:264–486)

def sendAfterStatesL314–369 ↗#

Continuation of send after States::send (src/lib.rs:274–323): updates the symmetric chain, derives the message key, serializes the message, and re-encodes the state.

def sendAfterStates (D : SpqrApiDeps) (hkdf : HkdfFn)
    (statePb : PqRatchetStatePB D.V1StatePB)
    (msg : D.MessageV1) (key : Option EpochSecret) (state : D.States) : SpqrApiResult Send := do
  let chain : Option Chain ←
    match statePb.chain with
    | none =>
      match statePb.versionNegotiation with
      | some vn =>
        -- Signed `i32` comparison (`vn.min_version > Version::V0 as i32`).
        if BitVec.slt Version.v0.toI32 vn.minVersion then do
          let c ← SpqrApiResult.ofError (chainFromVersionNegotiation hkdf vn)
          pure (some c)
        else
          pure none
      | none => .error (.err .chainNotAvailable)
    | some pb => do
      let c ← SpqrApiResult.ofError (Chain.fromPb pb)
      pure (some c)
  let (index, msgKey, chainPb) ←
    match chain with
    | none =>
      if key.isNone then
        pure (0#32, ([] : Bytes), (none : Option ChainPB))
      else
        .error (.panic .sendKeySomeWithoutChain)
    | some chain0 => do
      let chain1 ←
        match key with
        | some epochSecret => SpqrApiResult.ofChainPanic (chain0.addEpoch hkdf epochSecret)
        | none => pure chain0
      let epoch := D.msgEpoch msg
      if epoch == 0#64 then
        .error (.panic .sendEpochUnderflow)
      else do
        let (chain2, (idx, mk)) ← SpqrApiResult.ofChainResult (chain1.sendKey hkdf (epoch - 1#64))
        pure (idx, mk, some chain2.intoPb)
  let msgBytes := D.msgSerialize msg index
  match msgBytes with
  | [] => .error (.panic .sendMsgEmpty)
  | b0 :: _ =>
    if b0 != Version.v1.toU8 then
      .error (.panic .sendMsgBadVersion)
    else
      let newStateBytes := D.encodeState {
        inner := some (D.statesIntoPb state)
        versionNegotiation := statePb.versionNegotiation
        chain := chainPb
      }
      let outKey : MessageKey := if msgKey.isEmpty then none else some msgKey
      .ok {
        state := newStateBytes
        msg := msgBytes
        key := outKey
      }

def sendL371–388 ↗#

spqr::send (src/lib.rs:264–325), returning (result, remainingTape).

def send (D : SpqrApiDeps) (hkdf : HkdfFn) (state : SerializedState) (tape : Bytes) :
    SpqrApiResult Send × Bytes :=
  match decodeState D state with
  | .error e => (.error (.err e), tape)
  | .ok statePb =>
    match statePb.inner with
    | none =>
      (.ok { state := [], msg := [], key := none }, tape)
    | some pb =>
      match D.statesFromPb pb with
      | .error e => (.error e, tape)
      | .ok st0 =>
        let (sendRes, tape') := D.statesSend st0 tape
        match sendRes with
        | .error e => (.error e, tape')
        | .ok (msg, key, st1) =>
          (sendAfterStates D hkdf statePb msg key st1, tape')

def recvL390–476 ↗#

spqr::recv (src/lib.rs:355–486). In the Ordering::Greater branch (src/lib.rs:383–420), key is wrapped in some unconditionally without filtering empty keys (some [] when msg.index == 0, DEV-SPQR2).

def recv (D : SpqrApiDeps) (hkdf : HkdfFn) (state : SerializedState) (msg : SerializedMessage) :
    SpqrApiResult Recv := do
  let msg ← SpqrApiResult.ofError (msgPreamble msg)
  let prenegotiatedStatePb ← SpqrApiResult.ofError (decodeState D state)
  let currentVersion : BitVec 8 := (stateVersion prenegotiatedStatePb).toU8
  let (minVersion, versionStillNegotiating) : BitVec 8 × Bool :=
    match prenegotiatedStatePb.versionNegotiation with
    | some vn => (vn.minVersion.truncate 8, true)
    | none => (currentVersion, currentVersion == 0#8)
  if msg.version < minVersion then
    .error (.err .minimumVersion)
  else if msg.version != currentVersion && !versionStillNegotiating then
    .error (.err .versionMismatch)
  else if currentVersion == 0#8 then
    .ok { state := [], key := none }
  else if msg.version > currentVersion then do
    let zeroEpoch : Epoch := 0#64
    let chain0 ←
      SpqrApiResult.ofError
        (chainFrom hkdf prenegotiatedStatePb.chain prenegotiatedStatePb.versionNegotiation)
    let (chain1, rawKey) ← SpqrApiResult.ofChainResult (chain0.recvKey hkdf zeroEpoch msg.index)
    let newStateBytes := D.encodeState {
      chain := some chain1.intoPb
      versionNegotiation := prenegotiatedStatePb.versionNegotiation
      inner := prenegotiatedStatePb.inner
    }
    .ok {
      key := some rawKey
      state := newStateBytes
    }
  else do
    let statePb : PqRatchetStatePB D.V1StatePB ←
      if msg.version == currentVersion then
        pure prenegotiatedStatePb
      else do
        if !(currentVersion > 0#8 && versionStillNegotiating) then
          .error (.panic .recvNegotiateAssert)
        else
          let vn ←
            match prenegotiatedStatePb.versionNegotiation with
            | some vn => pure vn
            | none => .error (.panic .recvExpectStillNegotiating)
          let v ←
            match Version.fromU8? msg.version with
            | some v => pure v
            | none => .error (.panic .recvExpectLowerVersion)
          let dir ←
            match Direction.fromI32? vn.direction with
            | some d => pure d
            | none => .error (.err .stateDecode)
          let inner' ← SpqrApiResult.ofPanic (initInner D v dir vn.authKey)
          let chain' ← SpqrApiResult.ofError (chainFrom hkdf prenegotiatedStatePb.chain (some vn))
          pure {
            inner := inner'
            versionNegotiation := none
            chain := some chain'.intoPb
          }
    match statePb.inner with
    | none =>
      .ok { state := [], key := none }
    | some pb => do
      let sckaMsg ← D.msgDeserialize msg.epoch msg.remaining
      let st0 ← D.statesFromPb pb
      let (key, st1) ← D.statesRecv st0 sckaMsg
      if msg.epoch == 0#64 then
        .error (.panic .recvEpochUnderflow)
      else do
        let msgKeyEpoch : Epoch := msg.epoch - 1#64
        let chain0 ← SpqrApiResult.ofError (chainFrom hkdf statePb.chain statePb.versionNegotiation)
        let chain1 ←
          match key with
          | some epochSecret => SpqrApiResult.ofChainPanic (chain0.addEpoch hkdf epochSecret)
          | none => pure chain0
        let (chain2, msgKey) ← SpqrApiResult.ofChainResult (chain1.recvKey hkdf msgKeyEpoch msg.index)
        let newStateBytes := D.encodeState {
          inner := some (D.statesIntoPb st1)
          versionNegotiation := none
          chain := some chain2.intoPb
        }
        let outKey : MessageKey := if msgKey.isEmpty then none else some msgKey
        .ok {
          state := newStateBytes
          key := outKey
        }

Bridging Send / Recv to SpqrModel and SpqrRecvModel (DEV-SPQR2)

def messageKeyToSalt?L480–488 ↗#

Converts a MessageKey (Option Bytes) to Option Salt: none ↦ some none, 32-byte some k ↦ some (some ⟨k, h⟩), and any other length ↦ none.

def messageKeyToSalt? : MessageKey → Option Salt
  | none => some none
  | some k =>
    if h : k.length = 32 then
      some (some ⟨k, h⟩)
    else
      none

def recvKeyToSalt?L490–493 ↗#

Converts a recv message key to Option Salt, mapping some [] to some none (DEV-SPQR2, DEV-LS25).

def recvKeyToSalt? (k : MessageKey) : Option Salt :=
  if k = some [] then some none else messageKeyToSalt? k

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

CryptoVerification.LibsignalSpqrV1.recvKeyToSalt?_some_nil, CryptoVerification.LibsignalSpqrV1.recvKeyToSalt?_of_ne, CryptoVerification.LibsignalSpqrV1.recvKeyToSalt?_of_isSome

def sendPanicsBL507–512 ↗#

true iff send panics or produces a non-32-byte Some key.

def sendPanicsB (D : SpqrApiDeps) (hkdf : HkdfFn) (stateBytes tape : Bytes) : Bool :=
  match (send D hkdf stateBytes tape).1 with
  | .ok s => (messageKeyToSalt? s.key).isNone
  | .error (.err _) => false
  | .error (.panic _) => true

def recvPanicsSaltBL514–519 ↗#

true iff recv panics or produces a Some key rejected by recvKeyToSalt? (DEV-SPQR2).

def recvPanicsSaltB (D : SpqrApiDeps) (hkdf : HkdfFn) (stateBytes msgBytes : Bytes) : Bool :=
  match recv D hkdf stateBytes msgBytes with
  | .ok r => (recvKeyToSalt? r.key).isNone
  | .error (.err _) => false
  | .error (.panic _) => true

def recvPanicsBL521–526 ↗#

true iff recv returns .error (.panic _).

def recvPanicsB (D : SpqrApiDeps) (hkdf : HkdfFn) (stateBytes msgBytes : Bytes) : Bool :=
  match recv D hkdf stateBytes msgBytes with
  | .ok _ => false
  | .error (.err _) => false
  | .error (.panic _) => true

def sendPanicsPureBL528–533 ↗#

true iff send returns .error (.panic _).

def sendPanicsPureB (D : SpqrApiDeps) (hkdf : HkdfFn) (stateBytes tape : Bytes) : Bool :=
  match (send D hkdf stateBytes tape).1 with
  | .ok _ => false
  | .error (.err _) => false
  | .error (.panic _) => true

def toSpqrModelL535–558 ↗#

Packages send and recv as a SpqrModel (LibsignalTripleRatchet.lean), mapping some [] on recv to none via recvKeyToSalt? (DEV-SPQR2).

def toSpqrModel (D : SpqrApiDeps) (hkdf : HkdfFn) : SpqrModel where
  send := fun stateBytes tape =>
    match (send D hkdf stateBytes tape).1 with
    | .ok s =>
      match messageKeyToSalt? s.key with
      | some salt => some (s.state, salt, s.msg)
      | none => none
    | .error _ => none
  draws := fun stateBytes tape =>
    tape.length - (send D hkdf stateBytes tape).2.length
  recv := fun stateBytes msgBytes =>
    match recv D hkdf stateBytes msgBytes with
    | .ok r =>
      match recvKeyToSalt? r.key with
      | some salt => .ok (r.state, salt)
      | none => .error false
    | .error (.err e) => .error e.isStateDecode
    | .error (.panic _) => .error false
  recvPanics := fun stateBytes msgBytes =>
    recvPanicsB D hkdf stateBytes msgBytes
  sendPanics := fun stateBytes tape =>
    sendPanicsPureB D hkdf stateBytes tape

6 declarations not shown (lines 560–653): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.toSpqrRecvModel, CryptoVerification.LibsignalSpqrV1.recv_empty_state, CryptoVerification.LibsignalSpqrV1.toSpqrModel_recv_empty, CryptoVerification.LibsignalSpqrV1.not_toSpqrModel_recvPanics_empty, CryptoVerification.LibsignalSpqrV1.guard_version_and_types, CryptoVerification.LibsignalSpqrV1.guard_varint_and_preamble

end CryptoVerification.LibsignalSpqrV1