Wire.lean🔗

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

SPQR V1: wire format, Version, varint, and msg_preamble (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 (encodeVarint, decodeVarint, decodeVarintAt, decode_varint_at, MsgPreamble.ofLibsignalSpqr / toLibsignalSpqr, the Version constants V0, V1, MAX and DISABLED, Version.fromI32? and Version.tryFromU8) is checked by Lean.

Defines the shared wire-format aliases (MessageKey, SerializedState, SerializedMessage, empty_state / emptyState), Version (toU8, toI32), 10-byte LEB128 varint codecs (MAX_VARINT_BYTES_LEN, encode_varint, decode_varint), and message header parser (MsgPreamble, msg_preamble / msgPreamble), together with equivalence theorems against LibsignalSpqr.lean (decodeVarintLoop_eq_spqrVarintAux, decode_varint_eq_spqrDecodeVarint).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

Wire type aliases and Version (src/lib.rs:42–48, 177–195, 237–240)

abbrev MessageKeyL36 ↗#

abbrev MessageKey := Option Bytes

abbrev SerializedStateL38 ↗#

abbrev SerializedState := Bytes

abbrev SerializedMessageL40 ↗#

abbrev SerializedMessage := Bytes

def empty_stateL42 ↗#

def empty_state : SerializedState := []

abbrev emptyStateL44 ↗#

abbrev emptyState : SerializedState := empty_state

inductive VersionL46–50 ↗#

SPQR protocol version (pub enum Version, src/proto/pq_ratchet.proto:213–216).

inductive Version where
  | v0
  | v1
  deriving DecidableEq, Repr, Inhabited

namespace Version

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

CryptoVerification.LibsignalSpqrV1.Version.V0, CryptoVerification.LibsignalSpqrV1.Version.V1, CryptoVerification.LibsignalSpqrV1.Version.DISABLED, CryptoVerification.LibsignalSpqrV1.Version.MAX

def toU8L62–64 ↗#

def toU8 : Version → BitVec 8
  | .v0 => 0#8
  | .v1 => 1#8

def fromU8?L66–69 ↗#

def fromU8? (value : BitVec 8) : Option Version :=
  if value == 0#8 then some .v0
  else if value == 1#8 then some .v1
  else none

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

CryptoVerification.LibsignalSpqrV1.Version.tryFromU8

def toI32L76–78 ↗#

def toI32 : Version → BitVec 32
  | .v0 => 0#32
  | .v1 => 1#32

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

CryptoVerification.LibsignalSpqrV1.Version.fromI32?

end Version

Varint encoding/decoding and msg_preamble (src/lib.rs:507–590)

def MAX_VARINT_BYTES_LENL89 ↗#

def MAX_VARINT_BYTES_LEN : Nat := 10

def encodeVarintLoopL91–98 ↗#

def encodeVarintLoop : Nat → BitVec 64 → Bytes
  | 0, _ => []
  | fuel + 1, a =>
    let byte : BitVec 8 := (a &&& 0x7f#64).truncate 8
    if a < 0x80#64 then
      [byte]
    else
      (0x80#8 ||| byte) :: encodeVarintLoop fuel (a >>> 7)

def encode_varintL100–102 ↗#

encode_varint (src/lib.rs:509–521).

def encode_varint (a : BitVec 64) (into : SerializedMessage := []) : SerializedMessage :=
  into ++ encodeVarintLoop MAX_VARINT_BYTES_LEN a

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

CryptoVerification.LibsignalSpqrV1.encodeVarint

def decodeVarintLoopL107–118 ↗#

Inner loop of decode_varint (src/lib.rs:537–553); at i = 9, << 63 drops bits 1..6 of b & 0x7f.

def decodeVarintLoop : Nat → BitVec 64 → Bytes → Option (BitVec 64 × Bytes)
  | _, _, [] => 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 = MAX_VARINT_BYTES_LEN then
      none
    else
      decodeVarintLoop (i + 1) out rest

def decode_varintL120–125 ↗#

LEB128 u64 decoder (decode_varint, src/lib.rs:524–554); returns .error .msgDecode on truncation or a continuation bit on the 10th byte.

def decode_varint (fromSlice : Bytes) : Except Error (BitVec 64 × Bytes) :=
  match decodeVarintLoop 0 0#64 fromSlice with
  | some res => .ok res
  | none => .error .msgDecode

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

CryptoVerification.LibsignalSpqrV1.decodeVarint, CryptoVerification.LibsignalSpqrV1.decode_varint_at, CryptoVerification.LibsignalSpqrV1.decodeVarintAt

structure MsgPreambleL141–147 ↗#

Parsed SPQR message header (struct MsgPreamble<'a>, src/lib.rs:556–561).

structure MsgPreamble where
  version : BitVec 8
  epoch : Epoch
  index : BitVec 32
  remaining : Bytes
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.MsgPreamble.toLibsignalSpqr, CryptoVerification.LibsignalSpqrV1.MsgPreamble.ofLibsignalSpqr, CryptoVerification.LibsignalSpqrV1.MsgPreamble.toEmptyOk_ofEmptyOk, CryptoVerification.LibsignalSpqrV1.MsgPreamble.ofEmptyOk_toEmptyOk

def msg_preambleL169–183 ↗#

msg_preamble (src/lib.rs:563–590): returns all-zero preamble on [], otherwise parses the version byte, nonzero u64 varint epoch, and u32 varint index.

def msg_preamble (msg : SerializedMessage) : Except Error MsgPreamble :=
  match msg with
  | [] => .ok { version := 0#8, epoch := 0#64, index := 0#32, remaining := [] }
  | version :: rest => do
    let (epoch, rest) ← decode_varint rest
    if epoch = 0#64 then
      .error .msgDecode
    else
      let (index64, rest) ← decode_varint rest
      if index64.toNat < 2 ^ 32 then
        .ok { version := version, epoch := epoch, index := index64.setWidth 32, remaining := rest }
      else
        .error .msgDecode

abbrev msgPreambleL185 ↗#

abbrev msgPreamble := msg_preamble

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

CryptoVerification.LibsignalSpqrV1.decodeVarintLoop_eq_spqrVarintAux, CryptoVerification.LibsignalSpqrV1.decode_varint_eq_spqrDecodeVarint, CryptoVerification.LibsignalSpqrV1.msg_preamble_eq_msgPreamble?

end CryptoVerification.LibsignalSpqrV1