SessionRecord.lean🔗

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

Declarations on this page (10)

Persisted Session Record Mirrors and Protobuf Codecs

Plain-data mirrors and proto3 serializers for libsignal persisted session records (SessionRecord, SessionStructure, Chain), together with stored-secret membership (KeyInRecord) and single-session promotion eligibility (EligibleForSessionPromotion).

@[expose] public section

namespace DY.Libsignal.Rust

open DY.Libsignal (HwBytes)

open DY.Libsignal.Refinement (encodeField)

open DY.Libsignal.PQXDH.Refinement (parsePreKeyWire)

structure ChainRecL30–35 ↗#

Mirror of session_structure::Chain, with messageKeys in (index, seed) form.

structure ChainRec where
  senderRatchetKey : List (BitVec 8)
  senderRatchetKeyPrivate : List (BitVec 8)
  chainKey : Option (BitVec 32 × List (BitVec 8))
  messageKeys : List (BitVec 32 × List (BitVec 8))

structure SessionRecL37–53 ↗#

Mirror of proto::storage::SessionStructure. Pending pre-key submessages (pendingPreKey field 9 and pendingKyberPreKey field 14) split into their leading byte vector and remaining raw bytes.

structure SessionRec where
  sessionVersion : BitVec 32
  localIdentityPublic : List (BitVec 8)
  remoteIdentityPublic : List (BitVec 8)
  rootKey : List (BitVec 8)
  previousCounter : BitVec 32
  senderChain : Option ChainRec
  receiverChains : List ChainRec
  pendingPreKey : Option (List (BitVec 8) × List (BitVec 8))
  pendingKyberPreKey : Option (List (BitVec 8) × List (BitVec 8))
  remoteRegistrationId : BitVec 32
  localRegistrationId : BitVec 32
  aliceBaseKey : List (BitVec 8)
  pqRatchetState : List (BitVec 8)

structure RecordRecL55–58 ↗#

Mirror of SessionRecord: current session and serialized previous sessions (newest first).

structure RecordRec where
  current : SessionRec
  previous : List (List (BitVec 8))

def bytesFieldL60–62 ↗#

Encodes a proto3 bytes field (omitted when empty).

def bytesField (tag : Nat) (b : HwBytes) : HwBytes :=
  if b = [] then [] else encodeField tag 0 0 (.bytes b)

def u32FieldL64–66 ↗#

Encodes a proto3 uint32 field (omitted when zero).

def u32Field (tag : Nat) (v : BitVec 32) : HwBytes :=
  if v = 0 then [] else encodeField tag 0 0 (.varint v.toNat)

def msgFieldL68–69 ↗#

Encodes a length-delimited submessage or repeated bytes element.

def msgField (tag : Nat) (body : HwBytes) : HwBytes := encodeField tag 0 0 (.bytes body)

def chainBytesL71–74 ↗#

def chainBytes (c : ChainRec) : HwBytes :=
  bytesField 1 c.senderRatchetKey ++ bytesField 2 c.senderRatchetKeyPrivate ++
    ((c.chainKey.map fun k => msgField 3 (u32Field 1 k.1 ++ bytesField 2 k.2)).getD []) ++
    c.messageKeys.flatMap fun k => msgField 4 (u32Field 1 k.1 ++ bytesField 5 k.2)

def recordBytesL76–89 ↗#

Proto3 encoding of rec, writing pending pre-key submessages (fields 9 and 14) as raw payloads p.1 ++ p.2.

def recordBytes (rec : RecordRec) : HwBytes :=
  let s := rec.current
  msgField 1 (u32Field 1 s.sessionVersion ++ bytesField 2 s.localIdentityPublic ++
    bytesField 3 s.remoteIdentityPublic ++ bytesField 4 s.rootKey ++
    u32Field 5 s.previousCounter ++ ((s.senderChain.map (msgField 6 ∘ chainBytes)).getD []) ++
    s.receiverChains.flatMap (msgField 7 ∘ chainBytes) ++
    ((s.pendingPreKey.map fun p => msgField 9 (p.1 ++ p.2)).getD []) ++
    u32Field 10 s.remoteRegistrationId ++ u32Field 11 s.localRegistrationId ++
    bytesField 13 s.aliceBaseKey ++
    ((s.pendingKyberPreKey.map fun p => msgField 14 (p.1 ++ p.2)).getD []) ++
    bytesField 15 s.pqRatchetState) ++
  rec.previous.flatMap (msgField 2)

def KeyInRecordL91–100 ↗#

Whether k is a secret stored in rec.current (root key, chain key, ratchet private key, cached skipped seed, or SPQR state).

def KeyInRecord (rec : RecordRec) (k : HwBytes) : Prop :=
  k = rec.current.rootKey ∨
  (∃ sc, rec.current.senderChain = some sc ∧
    (k = sc.senderRatchetKeyPrivate ∨ ∃ ck, sc.chainKey = some ck ∧ k = ck.2)) ∨
  (∃ rc ∈ rec.current.receiverChains,
    (rc.senderRatchetKeyPrivate ≠ [] ∧ k = rc.senderRatchetKeyPrivate) ∨
    (∃ ck, rc.chainKey = some ck ∧ k = ck.2) ∨ (∃ mk ∈ rc.messageKeys, k = mk.2)) ∨
  k = rec.current.pqRatchetState

def EligibleForSessionPromotionL102–106 ↗#

Whether rec encodes a single session (no archived previous sessions) whose aliceBaseKey matches the outer base key of pre-key message b.

def EligibleForSessionPromotion (rec b : HwBytes) : Prop :=
  ∃ rr p, rec = recordBytes rr ∧ rr.previous = [] ∧ parsePreKeyWire b = some p ∧
    rr.current.aliceBaseKey = p.baseKey.take 33

end DY.Libsignal.Rust