WireFormat.lean🔗

Tier 2 · definitions used by the symbolic proof 3 headline theorems depend on it 257 of 406 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 (48)

Wire and Pre-Key Bundle Codecs

Concrete protobuf and binary wire encoders, decoders, and field accessors for SignalMessage / trWireMsg (DY.Libsignal.Refinement), PreKeySignalMessage, the SPQR message preamble, and the 1813-byte PublicBundle blob (DY.Libsignal.PQXDH.Refinement).

@[expose] public section

namespace DY.Libsignal.Refinement

open DY.TrWire

export DY.TrWire (PbValue FieldItem EncodingVariation canonicalVariation)

export CryptoVerification.SignalSession (le32)

def sliceL34–35 ↗#

len bytes of b starting at off.

def slice (b : HwBytes) (off len : Nat) : HwBytes := (b.drop off).take len

def paddedVarintL37–43 ↗#

Protobuf LEB128 varint of n padded with pad redundant continuation bytes (pad = 0 is minimal).

def paddedVarint (n pad : Nat) : HwBytes :=
  if n < 128 ∧ pad = 0 then [BitVec.ofNat 8 n]
  else BitVec.ofNat 8 (n % 128 + 128) :: paddedVarint (n / 128) (if n < 128 then pad - 1 else pad)
termination_by n + pad
decreasing_by all_goals (splitisTruen:ℕpad:ℕh✝¹:¬(n < 128 ∧ pad = 0)h✝:n < 128⊢ n / 128 + (pad - 1) < n + padisFalsen:ℕpad:ℕh✝¹:¬(n < 128 ∧ pad = 0)h✝:¬n < 128⊢ n / 128 + pad < n + pad <;>isTruen:ℕpad:ℕh✝¹:¬(n < 128 ∧ pad = 0)h✝:n < 128⊢ n / 128 + (pad - 1) < n + padisFalsen:ℕpad:ℕh✝¹:¬(n < 128 ∧ pad = 0)h✝:¬n < 128⊢ n / 128 + pad < n + pad omegaAll goals completed! 🐙)

def encodeFieldL45–49 ↗#

Encode one protobuf field with keyPad and valuePad varint padding.

def encodeField (tag keyPad valuePad : Nat) : PbValue → HwBytes
  | .varint n => paddedVarint (tag * 8) keyPad ++ paddedVarint n valuePad
  | .bytes b => paddedVarint (tag * 8 + 2) keyPad ++ paddedVarint b.length valuePad ++ b
  | .unknown wt p => paddedVarint (tag * 8 + wt) keyPad ++ p

structure WireFieldsL51–58 ↗#

Fields decoded by SignalMessage::try_from.

structure WireFields where
  version : Nat
  /-- 32-byte sender ratchet key (excluding the `0x05` type byte). -/
  ratchetKey : HwBytes
  counter : Nat
  previousCounter : Nat
  ciphertext : HwBytes

def knownValue?L60–65 ↗#

def knownValue? (v : EncodingVariation) (f : WireFields) : Nat → Option PbValue
  | 1 => some (.bytes (0x05#8 :: f.ratchetKey ++ v.ratchetKeyTrailingBytes))
  | 2 => some (.varint (f.counter + 2 ^ 32 * v.counterHigh))
  | 3 => some (.varint (f.previousCounter + 2 ^ 32 * v.previousCounterHigh))
  | 4 => some (.bytes f.ciphertext)
  | _ => none

def _root_.DY.TrWire.FieldItem.encodeL67–69 ↗#

def _root_.DY.TrWire.FieldItem.encode (v : EncodingVariation) (f : WireFields) : FieldItem → HwBytes
  | .known tag kp vp => ((knownValue? v f tag).map (encodeField tag kp vp)).getD []
  | .extra tag x kp vp => encodeField tag kp vp x

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

DY.Libsignal.Refinement.encodeWith

def trItemEncodeL76–82 ↗#

def trItemEncode (addr : HwBytes) (v : EncodingVariation) (f : WireFields) (pq : HwBytes) :
    FieldItem → HwBytes
  | .known t kp vp =>
    if t = 5 then encodeField 5 kp vp (.bytes pq)
    else if t = 6 then encodeField 6 kp vp (.bytes addr)
    else FieldItem.encode v f (.known t kp vp)
  | .extra t x kp vp => FieldItem.encode v f (.extra t x kp vp)

def honestTrItemsL84–86 ↗#

def honestTrItems (addr pq : HwBytes) : List FieldItem :=
  (if pq = [] then [] else [FieldItem.known 5 0 0]) ++
    (if addr = [] then [] else [FieldItem.known 6 0 0])

def trFieldsL88–89 ↗#

def trFields (addr : HwBytes) (v : EncodingVariation) (pq : HwBytes) : List FieldItem :=
  if v = canonicalVariation then v.fields ++ honestTrItems addr pq else v.fields

def trWireBytesL91–95 ↗#

Serialize a Triple Ratchet trWireMsg body from addr, v, f, and pq.

def trWireBytes (addr : HwBytes) (v : EncodingVariation) (f : WireFields) (pq : HwBytes) :
    HwBytes :=
  BitVec.ofNat 8 (f.version * 16 + v.versionLowNibble % 16) ::
    (trFields addr v pq).flatMap (trItemEncode addr v f pq)

5 declarations not shown (lines 97–115): theorems, which Lean checks, or definitions that no headline statement uses

DY.Libsignal.Refinement.decodeLittleEndianNat, DY.Libsignal.Refinement.WireFields.ofBytes, DY.TrWire.FieldItem.toWireNats, DY.TrWire.EncodingVariation.toNats, DY.TrWire.EncodingVariation.toBytes

def readVarintL117–121 ↗#

def readVarint : HwBytes → Option (Nat × HwBytes)
  | [] => none
  | b :: rest =>
    if b.toNat < 128 then some (b.toNat, rest)
    else (readVarint rest).map fun (n, r) => (b.toNat - 128 + 128 * n, r)

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

DY.Libsignal.Refinement.readNats, DY.Libsignal.Refinement.takeBytes

def itemsOfNatsL134–149 ↗#

def itemsOfNats : Nat → List Nat → Option (List FieldItem)
  | _, [] => some []
  | 0, _ :: _ => none
  | k + 1, 0 :: t :: kp :: vp :: rest => (itemsOfNats k rest).map (.known t kp vp :: ·)
  | k + 1, 1 :: t :: n :: kp :: vp :: rest =>
    (itemsOfNats k rest).map (.extra t (.varint n) kp vp :: ·)
  | k + 1, 2 :: t :: len :: rest =>
    match takeBytes len rest with
    | some (b, kp :: vp :: rest') => (itemsOfNats k rest').map (.extra t (.bytes b) kp vp :: ·)
    | _ => none
  | k + 1, 3 :: t :: wt :: len :: rest =>
    match takeBytes len rest with
    | some (p, kp :: vp :: rest') =>
      (itemsOfNats k rest').map (.extra t (.unknown wt p) kp vp :: ·)
    | _ => none
  | _ + 1, _ :: _ => none

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

DY.TrWire.EncodingVariation.ofNats?, DY.TrWire.EncodingVariation.ofBytes

end DY.Libsignal.Refinement

namespace DY.Libsignal.PQXDH.Refinement

open DY.Libsignal (HwBytes)

open DY.Libsignal.Refinement (le32 slice)

open CryptoVerification.LibsignalProtoCodec (WireType decodeKey encodeBytesField encodeUint32Field
  mergeBytes mergeUint32 skipField recursionLimit protoSignalCodec)

open CryptoVerification.SignalSession (PublicBundle bundleDir)

structure PreKeyProtoL175–184 ↗#

Protobuf fields of proto::wire::PreKeySignalMessage.

structure PreKeyProto where
  registrationId : Option (BitVec 32)
  preKeyId : Option (BitVec 32)
  signedPreKeyId : Option (BitVec 32)
  kyberPreKeyId : Option (BitVec 32)
  kyberCiphertext : Option (List (BitVec 8))
  baseKey : Option (List (BitVec 8))
  identityKey : Option (List (BitVec 8))
  message : Option (List (BitVec 8))

def PreKeyProto.encodeL186–195 ↗#

Canonical prost encoder for PreKeySignalMessage (fields 1..8 in ascending tag order).

def PreKeyProto.encode (m : PreKeyProto) : List (BitVec 8) :=
  encodeUint32Field 1 m.preKeyId ++
  encodeBytesField 2 m.baseKey ++
  encodeBytesField 3 m.identityKey ++
  encodeBytesField 4 m.message ++
  encodeUint32Field 5 m.registrationId ++
  encodeUint32Field 6 m.signedPreKeyId ++
  encodeUint32Field 7 m.kyberPreKeyId ++
  encodeBytesField 8 m.kyberCiphertext

def versionByteL197–199 ↗#

Header version byte ((v & 0x0F) << 4) | currentVersion.

def versionByte (v : BitVec 8) : BitVec 8 :=
  ((v &&& 0x0F) <<< 4) ||| CryptoGames.LibsignalSession.currentVersion

def spqrMaxVarintBytesL201 ↗#

def spqrMaxVarintBytes : Nat := 10

def spqrVarintAuxL203–209 ↗#

def spqrVarintAux : Nat → BitVec 64 → List (BitVec 8) → Option (BitVec 64 × List (BitVec 8))
  | _, _, [] => none
  | i, out, b :: rest =>
    let out := out ||| ((b &&& 0x7F#8).zeroExtend 64 <<< (7 * i))
    if b &&& 0x80#8 = 0#8 then some (out, rest)
    else if i + 1 = spqrMaxVarintBytes then none
    else spqrVarintAux (i + 1) out rest

def spqrDecodeVarintL211–213 ↗#

SPQR decode_varint (at most 10 bytes).

def spqrDecodeVarint (bs : List (BitVec 8)) : Option (BitVec 64 × List (BitVec 8)) :=
  spqrVarintAux 0 0#64 bs

structure MsgPreambleL215–220 ↗#

Decoded SPQR message preamble (version, epoch, 32-bit index, and remaining payload).

structure MsgPreamble where
  version : BitVec 8
  epoch : BitVec 64
  index : BitVec 32
  remaining : List (BitVec 8)

def msgPreamble?L222–235 ↗#

SPQR msg_preamble: returns ⟨0, 0, 0, []⟩ on [], and otherwise decodes version, nonzero epoch, and 32-bit index.

def msgPreamble? : List (BitVec 8) → Option MsgPreamble
  | [] => some ⟨0#8, 0#64, 0#32, []⟩
  | version :: rest =>
    match spqrDecodeVarint rest with
    | none => none
    | some (epoch, rest) =>
      if epoch = 0#64 then none
      else match spqrDecodeVarint rest with
        | none => none
        | some (index, rest) =>
          if index.toNat < 2 ^ 32 then some ⟨version, epoch, index.setWidth 32, rest⟩
          else none

def emptyPreKeyMsgL237–239 ↗#

def emptyPreKeyMsg : PreKeyProto :=
  { registrationId := none, preKeyId := none, signedPreKeyId := none, kyberPreKeyId := none,
    kyberCiphertext := none, baseKey := none, identityKey := none, message := none }

def mergePreKeyFieldL241–252 ↗#

def mergePreKeyField (m : PreKeyProto) (tag : Nat) (wt : WireType) (bs : HwBytes) :
    Option (PreKeyProto × HwBytes) :=
  match tag with
  | 1 => (mergeUint32 wt bs).map fun (v, r) => ({ m with preKeyId := some v }, r)
  | 2 => (mergeBytes wt bs).map fun (v, r) => ({ m with baseKey := some v }, r)
  | 3 => (mergeBytes wt bs).map fun (v, r) => ({ m with identityKey := some v }, r)
  | 4 => (mergeBytes wt bs).map fun (v, r) => ({ m with message := some v }, r)
  | 5 => (mergeUint32 wt bs).map fun (v, r) => ({ m with registrationId := some v }, r)
  | 6 => (mergeUint32 wt bs).map fun (v, r) => ({ m with signedPreKeyId := some v }, r)
  | 7 => (mergeUint32 wt bs).map fun (v, r) => ({ m with kyberPreKeyId := some v }, r)
  | 8 => (mergeBytes wt bs).map fun (v, r) => ({ m with kyberCiphertext := some v }, r)
  | _ => (skipField (2 * bs.length + 2) recursionLimit tag wt bs).map fun r => (m, r)

def decodePreKeyLoopL254–263 ↗#

def decodePreKeyLoop : Nat → PreKeyProto → HwBytes → Option PreKeyProto
  | _, m, [] => some m
  | 0, _, _ :: _ => none
  | fuel + 1, m, bs@(_ :: _) =>
    match decodeKey bs with
    | none => none
    | some ((tag, wt), rest) =>
      match mergePreKeyField m tag wt rest with
      | none => none
      | some (m', rest') => decodePreKeyLoop fuel m' rest'

def decodePreKeyL265–266 ↗#

def decodePreKey (bs : HwBytes) : Option PreKeyProto :=
  decodePreKeyLoop bs.length emptyPreKeyMsg bs

def ecKeyParsesL268–269 ↗#

Whether PublicKey::deserialize accepts b (0x05 prefix and length ≥ 33).

def ecKeyParses (b : HwBytes) : Bool := b.head? == some 0x05#8 && 33 ≤ b.length

structure PreKeyFieldsL271–281 ↗#

Validated PreKeySignalMessage fields accepted by PreKeySignalMessage::try_from.

structure PreKeyFields where
  version : Nat
  preKeyId : Option (BitVec 32)
  signedPreKeyId : BitVec 32
  kyberPreKeyId : Option (BitVec 32)
  kyberCiphertext : Option HwBytes
  baseKey : HwBytes
  identityKey : HwBytes
  message : HwBytes
  inner : CryptoGames.LibsignalSession.SignalMessage

def parsePreKeyL283–305 ↗#

PreKeySignalMessage::try_from (versions 3..4, valid EC keys, and valid inner SignalMessage).

def parsePreKey (v : HwBytes) : Option PreKeyFields :=
  match v with
  | [] => none
  | vb :: body =>
    let ver := (vb >>> 4).toNat
    if ver < 3 ∨ 4 < ver then none else
    match decodePreKey body with
    | none => none
    | some m =>
      match m.baseKey, m.identityKey, m.message, m.signedPreKeyId with
      | some bk, some ik, some msg, some sid =>
        let kyberOk := (m.kyberPreKeyId.isSome && m.kyberCiphertext.isSome) ||
          (m.kyberPreKeyId.isNone && m.kyberCiphertext.isNone && ver ≤ 3)
        if kyberOk && ecKeyParses bk && ecKeyParses ik then
          match CryptoGames.LibsignalSession.SignalMessage.tryFrom protoSignalCodec msg with
          | .ok inner =>
            some { version := ver, preKeyId := m.preKeyId, signedPreKeyId := sid,
                   kyberPreKeyId := m.kyberPreKeyId, kyberCiphertext := m.kyberCiphertext,
                   baseKey := bk, identityKey := ik, message := msg, inner }
          | .error _ => none
        else none
      | _, _, _, _ => none

def parsePreKeyWireL307–311 ↗#

Decode a wirePrekeyTag-prefixed PreKeySignalMessage frame.

def parsePreKeyWire (b : HwBytes) : Option PreKeyFields :=
  match b with
  | t :: body => if t = wirePrekeyTag then parsePreKey body else none
  | [] => none

def preKeyWireL313–320 ↗#

Canonical wirePrekeyTag-prefixed version-4 PreKeySignalMessage wire frame.

def preKeyWire (preKeyId : Option (BitVec 32)) (spkId kpkId regId : BitVec 32)
    (ik ek ct msg : HwBytes) : HwBytes :=
  wirePrekeyTag :: versionByte 4#8 ::
    PreKeyProto.encode
      { registrationId := some regId, preKeyId, signedPreKeyId := some spkId,
        kyberPreKeyId := some kpkId, kyberCiphertext := some (0x08#8 :: ct),
        baseKey := some (0x05#8 :: ek), identityKey := some ik, message := some msg }

def preKeySpqrIndexL322–324 ↗#

SPQR message index extracted from the inner pq_ratchet preamble (0 on decode failure).

def preKeySpqrIndex (p : PreKeyFields) : UInt32 :=
  ((msgPreamble? p.inner.pqRatchet).map fun x => UInt32.ofNat x.index.toNat).getD 0

def bundleBlobL326–333 ↗#

Serialize PublicBundle b to the 1813-byte session_initiate bundle blob.

def bundleBlob (b : PublicBundle) : HwBytes :=
  le32 b.registrationId ++
    (match b.oneTime with
     | some (id, key) => 1#8 :: (le32 id ++ key)
     | none => List.replicate 38 0#8) ++
    le32 b.signedId ++ b.signedKey ++ b.signedSig ++
    le32 b.kyberId ++ b.kyberKey ++ b.kyberSig ++ b.identityKey

def bundleU32L335–337 ↗#

def bundleU32 : HwBytes → Option (BitVec 32)
  | [b0, b1, b2, b3] => some (b3 ++ b2 ++ b1 ++ b0)
  | _ => none

def decodeLe32L339–340 ↗#

def decodeLe32 (bs : HwBytes) : BitVec 32 :=
  (bundleU32 bs).getD 0#32

def bundleSplitIdL342–344 ↗#

def bundleSplitId : HwBytes → Option (BitVec 32 × HwBytes)
  | b0 :: b1 :: b2 :: b3 :: rest => (bundleU32 [b0, b1, b2, b3]).map (·, rest)
  | _ => none

def bundleSplitSignedL346–351 ↗#

def bundleSplitSigned (file : HwBytes) : Option (BitVec 32 × HwBytes × HwBytes) :=
  match bundleSplitId file with
  | some (id, rest) =>
    if 64 ≤ rest.length then some (id, rest.take (rest.length - 64), rest.drop (rest.length - 64))
    else none
  | none => none

def parseEcKeyL353–354 ↗#

def parseEcKey (b : HwBytes) : Option HwBytes :=
  if ecKeyParses b then some (b.take 33) else none

def parseKyberKeyL356–358 ↗#

def parseKyberKey : HwBytes → Option HwBytes
  | t :: rest => if t = 0x08#8 ∧ rest.length = 1568 then some (t :: rest) else none
  | [] => none

def parseBundleFilesL360–376 ↗#

Parse a PublicBundle from the bundle/ directory of d following public.rs::read_bundle.

def parseBundleFiles (d : String → Option HwBytes) : Option PublicBundle := do
  let file := fun name => (d (bundleDir ++ "/" ++ name)).getD []
  let identityKey ← parseEcKey (file "identity-key")
  let registrationId ← bundleU32 (file "registration-id")
  let (signedId, spk, signedSig) ← bundleSplitSigned (file "signed-pre-key")
  let (kyberId, kpk, kyberSig) ← bundleSplitSigned (file "kyber-pre-key")
  let oneTime ← (match file "one-time-pre-key" with
    | [] => some none
    | opk => do
      let (id, key) ← bundleSplitId opk
      let key ← parseEcKey key
      some (some (id, key)) : Option (Option (BitVec 32 × HwBytes)))
  let signedKey ← parseEcKey spk
  let kyberKey ← parseKyberKey kpk
  some { identityKey, registrationId, signedId, signedKey, signedSig, kyberId, kyberKey, kyberSig,
         oneTime }

namespace BundleBlob

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

DY.Libsignal.PQXDH.Refinement.BundleBlob.regId

abbrev hasOpkByteL383 ↗#

abbrev hasOpkByte (b : HwBytes) : Option (BitVec 8) := b[4]?

abbrev opkIdL385–407 ↗#

abbrev opkId (b : HwBytes) : Option (BitVec 32) :=
  if hasOpkByte b == some 1#8 then some (decodeLe32 (slice b 5 4)) else none

abbrev opkPubL388 ↗#

abbrev opkPub (b : HwBytes) : HwBytes := slice b 9 33

abbrev spkIdL390 ↗#

abbrev spkId (b : HwBytes) : BitVec 32 := decodeLe32 (slice b 42 4)

abbrev spkPubL392 ↗#

abbrev spkPub (b : HwBytes) : HwBytes := slice b 46 33

abbrev spkSigL394 ↗#

abbrev spkSig (b : HwBytes) : HwBytes := slice b 79 64

abbrev kpkIdL396 ↗#

abbrev kpkId (b : HwBytes) : BitVec 32 := decodeLe32 (slice b 143 4)

abbrev kpkPubL398 ↗#

abbrev kpkPub (b : HwBytes) : HwBytes := slice b 147 1569

abbrev kpkSigL400 ↗#

abbrev kpkSig (b : HwBytes) : HwBytes := slice b 1716 64

abbrev ikPubL402 ↗#

abbrev ikPub (b : HwBytes) : HwBytes := slice b 1780 33

end BundleBlob

end DY.Libsignal.PQXDH.Refinement