Chain.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 418 of 891 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 (46)

SPQR V1: symmetric key chain (Chain, src/chain.rs and 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 (the private self-test drivers run*, sendMany, recvAndCheckAll, testHkdf and testShaCompress, and the isPanic helpers of ChainError and ChainResult) is checked by Lean.

Panic-explicit specification of SPQR's symmetric per-epoch, per-direction hash chain (src/chain.rs and src/lib.rs): HkdfFn, spqrHkdfWith, ChainPanic, ChainError, ChainResult, bounded skipped-key store KeyHistory (get, add, gc), directional chain state ChainEpochDirection (nextKey, key), and multi-epoch ChainEpoch / Chain (new, addEpoch, sendKey, recvKey, intoPb, fromPb, chainFromVersionNegotiation, chainFrom).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.HMAC (ShaState hmacWith toBEBytes)

open CryptoGames.HKDF (hkdfExpand)

Helper functions and HKDF parameter signature

abbrev HkdfFnL40–41 ↗#

Signature of kdf::hkdf_to_vec / kdf::hkdf_to_slice: salt → ikm → info → okm_len → Bytes.

abbrev HkdfFn := Bytes → Bytes → Bytes → Nat → Bytes

def spqrHkdfWithL43–45 ↗#

HKDF-SHA256 instantiation of HkdfFn over compression function F (src/kdf.rs:14–18).

def spqrHkdfWith (F : ShaState → Bytes → ShaState) : HkdfFn :=
  fun salt ikm info okmLen => hkdfExpand F (hmacWith F salt ikm) info okmLen

def asciiBytesL47–48 ↗#

def asciiBytes (s : String) : Bytes :=
  s.toList.map fun c => BitVec.ofNat 8 c.toNat

def bytesLtL50–55 ↗#

Lexicographical < on byte slices.

def bytesLt : Bytes → Bytes → Bool
  | [], [] => false
  | [], _ :: _ => true
  | _ :: _, [] => false
  | x :: xs, y :: ys => if x < y then true else if y < x then false else bytesLt xs ys

inductive ChainPanicL57–77 ↗#

Rust panic sites in src/chain.rs.

inductive ChainPanic where
  /-- `src/chain.rs:149`: `current_key < params.max_ooo_keys_or_default()` in `KeyHistory::gc`. -/
  | gcKeyUnderflow
  /-- `src/chain.rs:157`: `&self.data[i..i + 4]` out of bounds in `KeyHistory::gc`. -/
  | gcSliceBounds
  /-- `src/chain.rs:191`: `self.data.len() % KEY_SIZE != 0` in `KeyHistory::get`. -/
  | keyHistoryUnaligned
  /-- `src/chain.rs:192`: `at + max_ooo_keys_or_default()` `u32` overflow in `KeyHistory::get`. -/
  | keyHistoryAddOverflow
  /-- `src/chain.rs:230`: `next.len() != 32` in `ChainEpochDirection::next_key_internal`. -/
  | nextKeyBadLen
  /-- `src/chain.rs:231, 266, 271, 280`: `u32` addition overflow on `ctr`. -/
  | ctrOverflow
  /-- `src/chain.rs:361`: `self.current_epoch + 1` `u64` overflow in `Chain::add_epoch`. -/
  | addEpochOverflow
  /-- `src/chain.rs:361`: `epoch_secret.epoch != self.current_epoch + 1` in `Chain::add_epoch`. -/
  | addEpochMismatch
  /-- `src/chain.rs:405, 413, 421`: `self.links[epoch_index]` out of bounds. -/
  | linksOutOfBounds
  deriving DecidableEq, Repr, Inhabited

inductive ChainErrorL79–83 ↗#

Error or panic outcome of a fallible chain operation.

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

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

CryptoVerification.LibsignalSpqrV1.ChainError.isPanic

abbrev ChainResultL93 ↗#

abbrev ChainResult (α : Type) := Except ChainError α

namespace ChainResult

def ofPanicL97–100 ↗#

def ofPanic (r : Except ChainPanic α) : ChainResult α :=
  match r with
  | .ok v => .ok v
  | .error p => .error (.panic p)

def ofErrorL102–105 ↗#

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

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

CryptoVerification.LibsignalSpqrV1.ChainResult.isPanic

end ChainResult

KeyHistory (src/chain.rs:91–208)

structure KeyHistoryL116–119 ↗#

Skipped-key table storing 36-byte entries [u8; 4][u8; 32] (4-byte BE index + 32-byte key).

structure KeyHistory where
  data : Bytes := []
  deriving DecidableEq, Repr, Inhabited

namespace KeyHistory

def KEY_SIZEL123 ↗#

def KEY_SIZE : Nat := 4 + 32

def newL125–126 ↗#

def new : KeyHistory :=
  { data := [] }

def addL128–129 ↗#

def add (self : KeyHistory) (k : BitVec 32 × Bytes) (_params : ChainParamsPB) : KeyHistory :=
  { data := self.data ++ toBEBytes 4 k.1 ++ k.2 }

def clearL131–132 ↗#

def clear (_self : KeyHistory) : KeyHistory :=
  { data := [] }

def removeL134–144 ↗#

Swap-remove the 36-byte entry at byte offset myArrayIndex (src/chain.rs:175–182).

def remove (self : KeyHistory) (myArrayIndex : Nat) (_params : ChainParamsPB) : KeyHistory :=
  { data :=
      if myArrayIndex + KEY_SIZE < self.data.length then
        let newEnd := self.data.length - KEY_SIZE
        let moved := self.data.drop newEnd
        let prefixBytes := self.data.take myArrayIndex
        let restBytes := (self.data.take newEnd).drop (myArrayIndex + KEY_SIZE)
        (prefixBytes ++ moved ++ restBytes).take newEnd
      else
        self.data.take myArrayIndex }

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

CryptoVerification.LibsignalSpqrV1.KeyHistory.remove_length_lt

def gcLoopL152–171 ↗#

Inner while i < self.data.len() loop of KeyHistory::gc (src/chain.rs:155–166).

def gcLoop (self : KeyHistory) (trimHorizon : Bytes) (params : ChainParamsPB) (i : Nat) :
    Except ChainPanic KeyHistory :=
  if h : i < self.data.length then
    if self.data.length < i + 4 then
      .error .gcSliceBounds
    else
      let entryKey := (self.data.drop i).take 4
      if bytesLt entryKey trimHorizon then
        have _hlt : (self.remove i params).data.length < self.data.length :=
          remove_length_lt self i params h
        gcLoop (self.remove i params) trimHorizon params i
      else
        gcLoop self trimHorizon params (i + KEY_SIZE)
  else
    .ok self
termination_by self.data.length - i
decreasing_by
  ·trimHorizon:Bytesparams:ChainParamsPBself:KeyHistoryi:ℕh:i < List.length self.datah✝¹:¬List.length self.data < i + 4entryKey:List (BitVec 8) := List.take 4 (List.drop i self.data)h✝:bytesLt entryKey trimHorizon = true_hlt:List.length (self.remove i params).data < List.length self.data⊢ List.length (self.remove i params).data - i < List.length self.data - i omegaAll goals completed! 🐙
  ·trimHorizon:Bytesself:KeyHistoryi:ℕh:i < List.length self.datah✝¹:¬List.length self.data < i + 4entryKey:List (BitVec 8) := List.take 4 (List.drop i self.data)h✝:¬bytesLt entryKey trimHorizon = true⊢ List.length self.data - (i + KEY_SIZE) < List.length self.data - i simp only [KEY_SIZE]trimHorizon:Bytesself:KeyHistoryi:ℕh:i < List.length self.datah✝¹:¬List.length self.data < i + 4entryKey:List (BitVec 8) := List.take 4 (List.drop i self.data)h✝:¬bytesLt entryKey trimHorizon = true⊢ List.length self.data - (i + (4 + 32)) < List.length self.data - i; omegaAll goals completed! 🐙

def gcL173–187 ↗#

KeyHistory::gc(&mut self, current_key: u32, params: &pqrpb::ChainParams) (src/chain.rs:145–168). Panics with .gcKeyUnderflow at src/chain.rs:149 if self.data.len() >= trim_size * 36 and current_key < max_ooo_keys_or_default().

def gc (self : KeyHistory) (currentKey : BitVec 32) (params : ChainParamsPB) :
    Except ChainPanic KeyHistory :=
  if self.data.length ≥ params.trimSize * KEY_SIZE then
    let maxOoo := params.maxOooKeysOrDefault
    if currentKey < maxOoo then
      .error .gcKeyUnderflow
    else
      let trimHorizon := toBEBytes 4 (currentKey - maxOoo)
      gcLoop self trimHorizon params 0
  else
    .ok self

def getLoopL189–204 ↗#

Inner for i in (0..self.data.len()).step_by(Self::KEY_SIZE) loop of KeyHistory::get (src/chain.rs:197–203).

def getLoop (self : KeyHistory) (atIdx : BitVec 32) (want : Bytes) (params : ChainParamsPB)
    (i : Nat) : ChainResult (KeyHistory × Bytes) :=
  if _h : i < self.data.length then
    if (self.data.drop i).take 4 == want then
      let out := (self.data.drop (i + 4)).take 32
      let self' := self.remove i params
      .ok (self', out)
    else
      getLoop self atIdx want params (i + KEY_SIZE)
  else
    .error (.err (.keyAlreadyRequested atIdx))
termination_by self.data.length - i
decreasing_by
  simp only [KEY_SIZE]self:KeyHistorywant:Bytesi:ℕ_h:i < List.length self.datah✝:¬(List.take 4 (List.drop i self.data) == want) = true⊢ List.length self.data - (i + (4 + 32)) < List.length self.data - i; omegaAll goals completed! 🐙

def getL206–220 ↗#

KeyHistory::get (src/chain.rs:185–207): retrieves and swap-removes the key for atIdx, checking 36-byte alignment, u32 overflow on atIdx + maxOoo, and the trim horizon currentCtr.

def get (self : KeyHistory) (atIdx currentCtr : BitVec 32) (params : ChainParamsPB) :
    ChainResult (KeyHistory × Bytes) :=
  if self.data.length % KEY_SIZE != 0 then
    .error (.panic .keyHistoryUnaligned)
  else
    let maxOoo := params.maxOooKeysOrDefault
    if atIdx.toNat + maxOoo.toNat ≥ 2 ^ 32 then
      .error (.panic .keyHistoryAddOverflow)
    else if atIdx + maxOoo < currentCtr then
      .error (.err (.keyTrimmed atIdx))
    else
      let want := toBEBytes 4 atIdx
      getLoop self atIdx want params 0

end KeyHistory

ChainEpochDirection (src/chain.rs:99–104, 210–321)

structure ChainEpochDirectionL226–231 ↗#

Directional chain state within one epoch (src/chain.rs:99–104).

structure ChainEpochDirection where
  ctr : BitVec 32
  next : Bytes
  prev : KeyHistory
  deriving DecidableEq, Repr, Inhabited

def chainNextInfoL233–234 ↗#

def chainNextInfo : Bytes :=
  asciiBytes "Signal PQ Ratchet V1 Chain Next"

namespace ChainEpochDirection

def newL238–241 ↗#

def new (k : Bytes) : ChainEpochDirection :=
  { ctr := 0#32
    prev := KeyHistory.new
    next := k }

def nextKeyInternalL243–259 ↗#

ChainEpochDirection::next_key_internal (src/chain.rs:229–246): advances (next, ctr) via 64-byte HKDF (next' = out[..32], key = out[32..64]), panicking if next.length != 32 or ctr == u32::MAX.

def nextKeyInternal (hkdf : HkdfFn) (next : Bytes) (ctr : BitVec 32) :
    Except ChainPanic (Bytes × BitVec 32 × (BitVec 32 × Bytes)) :=
  if next.length != 32 then
    .error .nextKeyBadLen
  else if ctr == 0xffffffff#32 then
    .error .ctrOverflow
  else
    let ctr' := ctr + 1#32
    let salt := List.replicate 32 0#8
    let info := toBEBytes 4 ctr' ++ chainNextInfo
    let genr8r := hkdf salt next info 64
    let next' := genr8r.take 32
    let key := (genr8r.drop 32).take 32
    .ok (next', ctr', (ctr', key))

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

CryptoVerification.LibsignalSpqrV1.ChainEpochDirection.nextKeyInternal_ctr

def nextKeyL278–282 ↗#

ChainEpochDirection::next_key(&mut self) -> (u32, Vec<u8>) (src/chain.rs:222–225).

def nextKey (hkdf : HkdfFn) (self : ChainEpochDirection) :
    Except ChainPanic (ChainEpochDirection × (BitVec 32 × Bytes)) := do
  let (next', ctr', out) ← nextKeyInternal hkdf self.next self.ctr
  return ({ self with next := next', ctr := ctr' }, out)

def keyAdvanceLoopL284–310 ↗#

Inner while at > self.ctr + 1 loop of ChainEpochDirection::key (src/chain.rs:271–287).

def keyAdvanceLoop (hkdf : HkdfFn) (self : ChainEpochDirection) (atIdx : BitVec 32)
    (params : ChainParamsPB) : ChainResult ChainEpochDirection :=
  if _h : self.ctr.toNat + 1 < atIdx.toNat then
    match hnk : nextKeyInternal hkdf self.next self.ctr with
    | .error p => .error (.panic p)
    | .ok (next', ctr', k) =>
      have _hctr' : ctr'.toNat = self.ctr.toNat + 1 :=
        nextKeyInternal_ctr hkdf self.next next' self.ctr ctr' k hnk
      let maxOoo := params.maxOooKeysOrDefault
      if ctr'.toNat + maxOoo.toNat ≥ 2 ^ 32 then
        .error (.panic .ctrOverflow)
      else
        let prev' :=
          if ctr' + maxOoo ≥ atIdx then
            self.prev.add k params
          else
            self.prev
        keyAdvanceLoop hkdf { ctr := ctr', next := next', prev := prev' } atIdx params
  else if self.ctr == 0xffffffff#32 then
    -- Unreachable when `self.ctr < atIdx`, included for completeness of `self.ctr + 1` check.
    .error (.panic .ctrOverflow)
  else
    .ok self
termination_by atIdx.toNat - self.ctr.toNat
decreasing_by
  omegaAll goals completed! 🐙

def keyL312–339 ↗#

ChainEpochDirection::key(&mut self, at: u32, params: &pqrpb::ChainParams) -> Result<Vec<u8>, Error> (src/chain.rs:248–297).

def key (hkdf : HkdfFn) (self : ChainEpochDirection) (atIdx : BitVec 32)
    (params : ChainParamsPB) : ChainResult (ChainEpochDirection × Bytes) :=
  if atIdx < self.ctr then do
    let (prev', out) ← self.prev.get atIdx self.ctr params
    return ({ self with prev := prev' }, out)
  else if atIdx == self.ctr then
    .error (.err (.keyAlreadyRequested atIdx))
  else
    if atIdx - self.ctr > params.maxJumpOrDefault then
      .error (.err (.keyJump self.ctr atIdx))
    else
      let maxOoo := params.maxOooKeysOrDefault
      if self.ctr.toNat + maxOoo.toNat ≥ 2 ^ 32 then
        .error (.panic .ctrOverflow)
      else do
        let self0 :=
          if atIdx > self.ctr + maxOoo then
            { self with prev := self.prev.clear }
          else
            self
        let self1 ← keyAdvanceLoop hkdf self0 atIdx params
        let prevGc ← ChainResult.ofPanic (self1.prev.gc self1.ctr params)
        let self2 := { self1 with prev := prevGc }
        let (next', ctr', (_, outKey)) ←
          ChainResult.ofPanic (nextKeyInternal hkdf self2.next self2.ctr)
        return ({ self2 with next := next', ctr := ctr' }, outKey)

def intoPbL341–344 ↗#

def intoPb (self : ChainEpochDirection) : EpochDirectionPB :=
  { ctr := self.ctr
    next := self.next
    prev := self.prev.data }

def fromPbL346–352 ↗#

ChainEpochDirection::from_pb (src/chain.rs:307–316), rejecting non-empty next of length ≠ 32.

def fromPb (pb : EpochDirectionPB) : Except Error ChainEpochDirection :=
  if !pb.next.isEmpty && pb.next.length != 32 then
    .error .stateDecode
  else
    .ok { ctr := pb.ctr, next := pb.next, prev := { data := pb.prev } }

def clearNextL354–355 ↗#

def clearNext (self : ChainEpochDirection) : ChainEpochDirection :=
  { self with next := [] }

end ChainEpochDirection

ChainEpoch and Chain (src/chain.rs:106–125, 323–463)

structure ChainEpochL361–365 ↗#

Send and receive chains of a single epoch (src/chain.rs:107–110).

structure ChainEpoch where
  send : ChainEpochDirection
  recv : ChainEpochDirection
  deriving DecidableEq, Repr, Inhabited

structure ChainL367–375 ↗#

Full symmetric chain state (src/chain.rs:113–121).

structure Chain where
  dir : Direction
  currentEpoch : Epoch
  sendEpoch : Epoch
  links : List ChainEpoch
  nextRoot : Bytes
  params : ChainParamsPB
  deriving DecidableEq, Repr, Inhabited

def EPOCHS_TO_KEEP_PRIOR_TO_SEND_EPOCHL377 ↗#

def EPOCHS_TO_KEEP_PRIOR_TO_SEND_EPOCH : Nat := 1

def chainStartInfoL379–381 ↗#

"Signal PQ Ratchet V1 Chain Start" (src/chain.rs:338; two spaces before Start).

def chainStartInfo : Bytes :=
  asciiBytes "Signal PQ Ratchet V1 Chain  Start"

def chainAddEpochInfoL383–384 ↗#

def chainAddEpochInfo : Bytes :=
  asciiBytes "Signal PQ Ratchet V1 Chain Add Epoch"

namespace Chain

def cedForDirectionL388–392 ↗#

def cedForDirection (genr8r : Bytes) (dir : Direction) : ChainEpochDirection :=
  ChainEpochDirection.new <|
    match dir with
    | .a2b => (genr8r.drop 32).take 32
    | .b2a => (genr8r.drop 64).take 32

def newL394–408 ↗#

Chain::new (src/chain.rs:333–354).

def new (hkdf : HkdfFn) (initialKey : Bytes) (dir : Direction) (params : ChainParamsPB) :
    Except Error Chain :=
  let salt := List.replicate 32 0#8
  let genr8r := hkdf salt initialKey chainStartInfo 96
  let epoch0 : ChainEpoch :=
    { send := cedForDirection genr8r dir
      recv := cedForDirection genr8r dir.switch }
  .ok
    { dir := dir
      currentEpoch := 0#64
      sendEpoch := 0#64
      links := [epoch0]
      nextRoot := genr8r.take 32
      params := params }

def addEpochL410–429 ↗#

Chain::add_epoch(&mut self, epoch_secret: EpochSecret) (src/chain.rs:356–375).

Panics with .addEpochOverflow if self.current_epoch == u64::MAX (src/chain.rs:361).
Panics with .addEpochMismatch if epoch_secret.epoch != self.current_epoch + 1 (src/chain.rs:361).

def addEpoch (hkdf : HkdfFn) (self : Chain) (epochSecret : EpochSecret) :
    Except ChainPanic Chain :=
  if self.currentEpoch == 0xffffffffffffffff#64 then
    .error .addEpochOverflow
  else if epochSecret.epoch != self.currentEpoch + 1#64 then
    .error .addEpochMismatch
  else
    let genr8r := hkdf self.nextRoot epochSecret.secret chainAddEpochInfo 96
    let newLink : ChainEpoch :=
      { send := cedForDirection genr8r self.dir
        recv := cedForDirection genr8r self.dir.switch }
    .ok
      { self with
        currentEpoch := epochSecret.epoch
        nextRoot := genr8r.take 32
        links := self.links ++ [newLink] }

def epochIdxL431–441 ↗#

Chain::epoch_idx(&mut self, epoch: Epoch) -> Result<usize, Error> (src/chain.rs:378–388).

def epochIdx (self : Chain) (epoch : Epoch) : Except Error Nat :=
  if epoch > self.currentEpoch then
    .error (.epochOutOfRange epoch)
  else
    let back := (self.currentEpoch - epoch).toNat
    let linksLen := self.links.length
    if back ≥ linksLen then
      .error (.epochOutOfRange epoch)
    else
      .ok (linksLen - 1 - back)

def clearSendNextPrefixL443–448 ↗#

Clear send.next on the first n elements of links (for i in 0..epoch_index in Chain::send_key, src/chain.rs:403–406).

def clearSendNextPrefix : Nat → List ChainEpoch → List ChainEpoch
  | 0, xs => xs
  | _ + 1, [] => []
  | n + 1, x :: xs => { x with send := x.send.clearNext } :: clearSendNextPrefix n xs

def sendKeyL450–473 ↗#

Derive the next sending key (index, key) in epoch, dropping older epochs when the send epoch advances. Chain::send_key(&mut self, epoch: Epoch) -> Result<(u32, Vec<u8>), Error> (src/chain.rs:390–414).

def sendKey (hkdf : HkdfFn) (self : Chain) (epoch : Epoch) :
    ChainResult (Chain × (BitVec 32 × Bytes)) :=
  if epoch < self.sendEpoch then
    .error (.err (.sendKeyEpochDecreased self.sendEpoch epoch))
  else do
    let epochIndex0 ← ChainResult.ofError (self.epochIdx epoch)
    let (self1, epochIndex) :=
      if self.sendEpoch != epoch then
        let dropCount := epochIndex0 - EPOCHS_TO_KEEP_PRIOR_TO_SEND_EPOCH
        let epochIndex' := epochIndex0 - dropCount
        let links1 := self.links.drop dropCount
        let links2 := clearSendNextPrefix epochIndex' links1
        ({ self with sendEpoch := epoch, links := links2 }, epochIndex')
      else
        (self, epochIndex0)
    match self1.links[epochIndex]? with
    | none => .error (.panic .linksOutOfBounds)
    | some link => do
      let (send', out) ← ChainResult.ofPanic (link.send.nextKey hkdf)
      let links' := self1.links.set epochIndex { link with send := send' }
      return ({ self1 with links := links' }, out)

def recvKeyL475–489 ↗#

Derive the receiving key for message index of epoch; epoch 0, index 0 yields the empty key. Chain::recv_key(&mut self, epoch: Epoch, index: u32) -> Result<Vec<u8>, Error> (src/chain.rs:416–422).

def recvKey (hkdf : HkdfFn) (self : Chain) (epoch : Epoch) (index : BitVec 32) :
    ChainResult (Chain × Bytes) :=
  if epoch == 0#64 && index == 0#32 then
    .ok (self, [])
  else do
    let epochIndex ← ChainResult.ofError (self.epochIdx epoch)
    match self.links[epochIndex]? with
    | none => .error (.panic .linksOutOfBounds)
    | some link => do
      let (recv', out) ← link.recv.key hkdf index self.params
      let links' := self.links.set epochIndex { link with recv := recv' }
      return ({ self with links := links' }, out)

def intoPbL491–499 ↗#

def intoPb (self : Chain) : ChainPB :=
  { direction := self.dir.toI32
    currentEpoch := self.currentEpoch
    sendEpoch := self.sendEpoch
    links := self.links.map fun link =>
      { send := some link.send.intoPb
        recv := some link.recv.intoPb }
    nextRoot := self.nextRoot
    params := some self.params }

def linksFromPbL501–515 ↗#

def linksFromPb : List ChainEpochPB → Except Error (List ChainEpoch)
  | [] => .ok []
  | link :: rest => do
    let sendPb ←
      match link.send with
      | some s => .ok s
      | none => .error .stateDecode
    let send ← ChainEpochDirection.fromPb sendPb
    let recvPb ←
      match link.recv with
      | some r => .ok r
      | none => .error .stateDecode
    let recv ← ChainEpochDirection.fromPb recvPb
    let tail ← linksFromPb rest
    return { send := send, recv := recv } :: tail

def fromPbL517–535 ↗#

Chain::from_pb (src/chain.rs:444–462).

def fromPb (pb : ChainPB) : Except Error Chain := do
  let dir ←
    match Direction.fromI32? pb.direction with
    | some d => .ok d
    | none => .error .stateDecode
  let links ← linksFromPb pb.links
  let params ←
    match pb.params with
    | some p => .ok p
    | none => .error .stateDecode
  return {
    dir := dir
    currentEpoch := pb.currentEpoch
    sendEpoch := pb.sendEpoch
    nextRoot := pb.nextRoot
    links := links
    params := params
  }

end Chain

chain_from_version_negotiation and chain_from (src/lib.rs:332–353)

def chainFromVersionNegotiationL541–552 ↗#

chain_from_version_negotiation (src/lib.rs:332–340).

def chainFromVersionNegotiation (hkdf : HkdfFn) (vn : VersionNegotiationPB) :
    Except Error Chain := do
  let dir ←
    match Direction.fromI32? vn.direction with
    | some d => .ok d
    | none => .error .stateDecode
  let params ←
    match vn.chainParams with
    | some p => .ok p
    | none => .error .chainNotAvailable
  Chain.new hkdf vn.authKey dir params

def chainFromL554–562 ↗#

chain_from (src/lib.rs:342–353).

def chainFrom (hkdf : HkdfFn) (pb : Option ChainPB) (vn : Option VersionNegotiationPB) :
    Except Error Chain :=
  match pb with
  | some pb => Chain.fromPb pb
  | none =>
    match vn with
    | none => .error .chainNotAvailable
    | some vn => chainFromVersionNegotiation hkdf vn

23 declarations not shown (lines 568–887): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.testShaCompress, CryptoVerification.LibsignalSpqrV1.testHkdf, CryptoVerification.LibsignalSpqrV1.sendMany, CryptoVerification.LibsignalSpqrV1.recvAndCheckAll, CryptoVerification.LibsignalSpqrV1.guard_chain_params, CryptoVerification.LibsignalSpqrV1.runDirectionsMatch, CryptoVerification.LibsignalSpqrV1.guard_directions_match, CryptoVerification.LibsignalSpqrV1.guard_rejects_malformed_next_key, CryptoVerification.LibsignalSpqrV1.runPreviouslyReturnedKey, CryptoVerification.LibsignalSpqrV1.guard_previously_returned_key, CryptoVerification.LibsignalSpqrV1.runVeryOldKeysAreTrimmed, CryptoVerification.LibsignalSpqrV1.guard_very_old_keys_are_trimmed, CryptoVerification.LibsignalSpqrV1.runOutOfOrderKeys, CryptoVerification.LibsignalSpqrV1.guard_out_of_order_keys, CryptoVerification.LibsignalSpqrV1.runClearOldSendKeys, CryptoVerification.LibsignalSpqrV1.guard_clear_old_send_keys, CryptoVerification.LibsignalSpqrV1.runKeyHistoryTrace, CryptoVerification.LibsignalSpqrV1.guard_key_history_trace, CryptoVerification.LibsignalSpqrV1.runCedTrace, CryptoVerification.LibsignalSpqrV1.guard_ced_trace, CryptoVerification.LibsignalSpqrV1.runChainPbAndVersionNegotiation, CryptoVerification.LibsignalSpqrV1.guard_chain_pb_and_version_negotiation, CryptoVerification.LibsignalSpqrV1.guard_chain_panics

end CryptoVerification.LibsignalSpqrV1