Proto.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 578 of 1,112 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 (140)

SPQR V1: Protobuf types and prost 0.14.4 codec for pq_ratchet.proto

Trusted in part. The theorems of Computational/Theorems/ use only part of this file (see Computational/docs/TRUSTED_BASE.md): the message types (PolynomialEncoder, PolynomialDecoder, ProtoChunk, V1State, InnerState, PqRatchetState) and the encodeRaw / mergeField codec functions (WireType, DecodeErr, decodeVarint, encodeVarint, decodeKey, encodeKey, skipField, mergeFieldsLoop, mergeMessage, mergeTopLevelMessage, decodeTopLevelMessage, encodeMessage, decodeState, encodeState) that the SPQR V1 state goes through. The remaining definitions (encode, decode, encodedLen, merge, V1Msg, decodeV1Msg, encodeV1Msg, and spqrDecodeState) are checked by Lean.

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

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

CryptoVerification.LibsignalSpqrV1.ProtoChainParams, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch, CryptoVerification.LibsignalSpqrV1.ProtoChain, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation, CryptoVerification.LibsignalSpqrV1.AuthenticatorPB

structure PolynomialEncoderL47–52 ↗#

message PolynomialEncoder (src/proto/pq_ratchet.proto:8–16).

structure PolynomialEncoder where
  idx : BitVec 32 := 0#32
  pts : List Bytes := []
  polys : List Bytes := []
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.PolynomialEncoderPB

structure PolynomialDecoderL56–62 ↗#

message PolynomialDecoder (src/proto/pq_ratchet.proto:18–23).

structure PolynomialDecoder where
  ptsNeeded : BitVec 32 := 0#32
  polys : BitVec 32 := 0#32
  pts : List Bytes := []
  isComplete : Bool := false
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.PolynomialDecoderPB, CryptoVerification.LibsignalSpqrV1.ProtoChunk.index, CryptoVerification.LibsignalSpqrV1.ProtoChunk.data, CryptoVerification.LibsignalSpqrV1.ProtoChunk, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.hdr, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.ekCt1Ack, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.ct2, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.ek, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.ct1Ack, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.ct1, CryptoVerification.LibsignalSpqrV1.V1Msg.innerMsg, CryptoVerification.LibsignalSpqrV1.V1Msg, CryptoVerification.LibsignalSpqrV1.V1Msg.epoch, CryptoVerification.LibsignalSpqrV1.V1Msg.index, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked

namespace V1State.Unchunked

structure KeysUnsampledL94–97 ↗#

structure KeysUnsampled where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  deriving DecidableEq, Repr, Inhabited

structure HeaderSentL98–103 ↗#

structure HeaderSent where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  ek : Bytes := []
  dk : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure EkSentL104–108 ↗#

structure EkSent where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  dk : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure EkSentCt1ReceivedL109–114 ↗#

structure EkSentCt1Received where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  dk : Bytes := []
  ct1 : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure NoHeaderReceivedL115–118 ↗#

structure NoHeaderReceived where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  deriving DecidableEq, Repr, Inhabited

structure HeaderReceivedL119–123 ↗#

structure HeaderReceived where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  hdr : Bytes := []
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.auth, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.hdr, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.ek, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.epoch

structure Ct1SentL130–136 ↗#

structure Ct1Sent where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  hdr : Bytes := []
  es : Bytes := []
  ct1 : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure Ct1SentEkReceivedL137–143 ↗#

structure Ct1SentEkReceived where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  es : Bytes := []
  ek : Bytes := []
  ct1 : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure Ct2SentL144–147 ↗#

structure Ct2Sent where
  epoch : Epoch := 0#64
  auth : Option ProtoAuthenticator := none
  deriving DecidableEq, Repr, Inhabited

end V1State.Unchunked

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked

namespace V1State.Chunked

structure KeysUnsampledL155–157 ↗#

structure KeysUnsampled where
  uc : Option V1State.Unchunked.KeysUnsampled := none
  deriving DecidableEq, Repr, Inhabited

structure KeysSampledL158–161 ↗#

structure KeysSampled where
  uc : Option V1State.Unchunked.HeaderSent := none
  sendingHdr : Option PolynomialEncoder := none
  deriving DecidableEq, Repr, Inhabited

structure HeaderSentL162–166 ↗#

structure HeaderSent where
  uc : Option V1State.Unchunked.EkSent := none
  sendingEk : Option PolynomialEncoder := none
  receivingCt1 : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure Ct1ReceivedL167–170 ↗#

structure Ct1Received where
  uc : Option V1State.Unchunked.EkSentCt1Received := none
  sendingEk : Option PolynomialEncoder := none
  deriving DecidableEq, Repr, Inhabited

structure EkSentCt1ReceivedL171–175 ↗#

V1State.Chunked.EkSentCt1Received (pq_ratchet.proto:144–147): tags uc = 1, receiving_ct2 = 3.

structure EkSentCt1Received where
  uc : Option V1State.Unchunked.EkSentCt1Received := none
  receivingCt2 : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure NoHeaderReceivedL176–179 ↗#

structure NoHeaderReceived where
  uc : Option V1State.Unchunked.NoHeaderReceived := none
  receivingHdr : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure HeaderReceivedL180–183 ↗#

structure HeaderReceived where
  uc : Option V1State.Unchunked.HeaderReceived := none
  receivingEk : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure Ct1SampledL184–188 ↗#

structure Ct1Sampled where
  uc : Option V1State.Unchunked.Ct1Sent := none
  sendingCt1 : Option PolynomialEncoder := none
  receivingEk : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure EkReceivedCt1SampledL189–192 ↗#

structure EkReceivedCt1Sampled where
  uc : Option V1State.Unchunked.Ct1SentEkReceived := none
  sendingCt1 : Option PolynomialEncoder := none
  deriving DecidableEq, Repr, Inhabited

structure Ct1AcknowledgedL193–196 ↗#

structure Ct1Acknowledged where
  uc : Option V1State.Unchunked.Ct1Sent := none
  receivingEk : Option PolynomialDecoder := none
  deriving DecidableEq, Repr, Inhabited

structure Ct2SampledL197–200 ↗#

structure Ct2Sampled where
  uc : Option V1State.Unchunked.Ct2Sent := none
  sendingCt2 : Option PolynomialEncoder := none
  deriving DecidableEq, Repr, Inhabited

end V1State.Chunked

namespace V1State

inductive InnerStateL204–217 ↗#

oneof V1State.inner_state (src/proto/pq_ratchet.proto:177–192).

inductive InnerState where
  | keysUnsampled (v : Chunked.KeysUnsampled)
  | keysSampled (v : Chunked.KeysSampled)
  | headerSent (v : Chunked.HeaderSent)
  | ct1Received (v : Chunked.Ct1Received)
  | ekSentCt1Received (v : Chunked.EkSentCt1Received)
  | noHeaderReceived (v : Chunked.NoHeaderReceived)
  | headerReceived (v : Chunked.HeaderReceived)
  | ct1Sampled (v : Chunked.Ct1Sampled)
  | ekReceivedCt1Sampled (v : Chunked.EkReceivedCt1Sampled)
  | ct1Acknowledged (v : Chunked.Ct1Acknowledged)
  | ct2Sampled (v : Chunked.Ct2Sampled)
  deriving DecidableEq, Repr

end V1State

structure V1StateL220–223 ↗#

message V1State (src/proto/pq_ratchet.proto:66–193).

structure V1State where
  innerState : Option V1State.InnerState := none
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.V1StatePB

inductive PqRatchetState.InnerL227–230 ↗#

oneof PqRatchetState.inner (src/proto/pq_ratchet.proto:35–37).

inductive PqRatchetState.Inner where
  | v1 (v : V1State)
  deriving DecidableEq, Repr

structure PqRatchetStateL232–237 ↗#

message PqRatchetState (src/proto/pq_ratchet.proto:25–38).

structure PqRatchetState where
  versionNegotiation : Option VersionNegotiationPB := none
  chain : Option ChainPB := none
  inner : Option PqRatchetState.Inner := none
  deriving DecidableEq, Repr, Inhabited

namespace Proto

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

CryptoVerification.LibsignalSpqrV1.Proto.ChainParams, CryptoVerification.LibsignalSpqrV1.Proto.EpochDirection, CryptoVerification.LibsignalSpqrV1.Proto.Chain, CryptoVerification.LibsignalSpqrV1.Proto.VersionNegotiation, CryptoVerification.LibsignalSpqrV1.Proto.Chunk, CryptoVerification.LibsignalSpqrV1.Proto.Authenticator

inductive WireTypeL250–253 ↗#

prost::encoding::WireType.

inductive WireType where
  | varint | SixtyFourBit | lengthDelimited | startGroup | endGroup | ThirtyTwoBit
  deriving DecidableEq, Repr, Inhabited

namespace WireType

def ofU64?L256–259 ↗#

def ofU64? (v : BitVec 64) : Option WireType :=
  if v == 0#64 then some .varint else if v == 1#64 then some .SixtyFourBit
  else if v == 2#64 then some .lengthDelimited else if v == 3#64 then some .startGroup
  else if v == 4#64 then some .endGroup else if v == 5#64 then some .ThirtyTwoBit else none

def toU32L260–262 ↗#

def toU32 : WireType → BitVec 32
  | .varint => 0#32 | .SixtyFourBit => 1#32 | .lengthDelimited => 2#32
  | .startGroup => 3#32 | .endGroup => 4#32 | .ThirtyTwoBit => 5#32

end WireType

inductive DecodeErrL265–270 ↗#

prost::DecodeError kinds.

inductive DecodeErr where
  | invalidVarint | bufferUnderflow | invalidWireType (v : BitVec 64)
  | invalidKey (key : BitVec 64) | invalidTag (tag : BitVec 32)
  | unexpectedWireType (expected actual : WireType) | unexpectedEndGroupTag | recursionLimitExceeded
  deriving DecidableEq, Repr, Inhabited

def RECURSION_LIMITL272 ↗#

def RECURSION_LIMIT : Nat := 100

def MIN_TAGL273 ↗#

def MIN_TAG : BitVec 32 := 1#32

def decodeVarintAuxL275–289 ↗#

LEB128 varint decoder (prost::encoding::varint::decode_varint_slow): 1 to 10 bytes, with the 10th byte required to be < 0x02.

def decodeVarintAux : Nat → Nat → BitVec 64 → Bytes → Except DecodeErr (BitVec 64 × Bytes)
  | 0, _, _, _ => .error .invalidVarint
  | fuel + 1, idx, acc, bs =>
    match bs with
    | [] => .error .bufferUnderflow
    | b :: rest =>
      if idx == 9 then
        if b ≥ 0x02#8 then .error .invalidVarint
        else .ok (acc ||| ((b &&& 0x7f#8).zeroExtend 64 <<< 63), rest)
      else
        let acc' := acc ||| ((b &&& 0x7f#8).zeroExtend 64 <<< (idx * 7))
        if b < 0x80#8 then .ok (acc', rest)
        else decodeVarintAux fuel (idx + 1) acc' rest

def decodeVarintL291 ↗#

def decodeVarint (bs : Bytes) : Except DecodeErr (BitVec 64 × Bytes) := decodeVarintAux 10 0 0#64 bs

def encodeVarintAuxL293–297 ↗#

def encodeVarintAux : Nat → BitVec 64 → Bytes
  | 0, v => [v.truncate 8]
  | fuel + 1, v =>
    if v < 0x80#64 then [v.truncate 8]
    else ((v.truncate 8 ||| 0x80#8)) :: encodeVarintAux fuel (v >>> 7)

def encodeVarintL299–300 ↗#

prost::encoding::varint::encode_varint.

def encodeVarint (v : BitVec 64) : Bytes := encodeVarintAux 10 v

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

CryptoVerification.LibsignalSpqrV1.Proto.encodedLenVarint

def decodeKeyL303–312 ↗#

prost::encoding::decode_key: validates key ≤ u32::MAX, 3-bit WireType, and tag ≥ 1.

def decodeKey (bs : Bytes) : Except DecodeErr ((BitVec 32 × WireType) × Bytes) := do
  let (key, rest) ← decodeVarint bs
  if key > 0xffffffff#64 then .error (.invalidKey key)
  else
    let wt ← match WireType.ofU64? (key &&& 0x7#64) with
      | some w => .ok w
      | none => .error (.invalidWireType (key &&& 0x7#64))
    let tag : BitVec 32 := (key >>> 3).truncate 32
    if tag < MIN_TAG then .error (.invalidTag tag) else .ok ((tag, wt), rest)

def encodeKeyL314–315 ↗#

def encodeKey (tag : BitVec 32) (wt : WireType) : Bytes :=
  encodeVarint (((tag <<< 3) ||| wt.toU32).zeroExtend 64)

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

CryptoVerification.LibsignalSpqrV1.Proto.keyLen

def checkWireTypeL318–319 ↗#

def checkWireType (expected actual : WireType) : Except DecodeErr Unit :=
  if expected != actual then .error (.unexpectedWireType expected actual) else .ok ()

def takeExactL321–324 ↗#

def takeExact : Nat → Bytes → Except DecodeErr (Bytes × Bytes)
  | 0, bs => .ok ([], bs)
  | _ + 1, [] => .error .bufferUnderflow
  | n + 1, b :: rest => do let (hd, tl) ← takeExact n rest; .ok (b :: hd, tl)

def dropExactL326–329 ↗#

def dropExact : Nat → Bytes → Except DecodeErr Bytes
  | 0, bs => .ok bs
  | _ + 1, [] => .error .bufferUnderflow
  | n + 1, _ :: rest => dropExact n rest

def skipGroupLoopL331–340 ↗#

def skipGroupLoop (skipInner : WireType → BitVec 32 → Bytes → Except DecodeErr Bytes) :
    Nat → BitVec 32 → Bytes → Except DecodeErr Bytes
  | 0, _, _ => .error .bufferUnderflow
  | fuel + 1, groupTag, bs => do
    let ((innerTag, innerWt), rest) ← decodeKey bs
    if innerWt == .endGroup then
      if innerTag != groupTag then .error .unexpectedEndGroupTag else .ok rest
    else do
      let rest' ← skipInner innerWt innerTag rest
      skipGroupLoop skipInner fuel groupTag rest'

def skipFieldNonGroupL342–348 ↗#

def skipFieldNonGroup (wt : WireType) (bs : Bytes) : Except DecodeErr Bytes :=
  match wt with
  | .varint => do let (_, rest) ← decodeVarint bs; .ok rest
  | .ThirtyTwoBit => dropExact 4 bs
  | .SixtyFourBit => dropExact 8 bs
  | .lengthDelimited => do let (len, rest) ← decodeVarint bs; dropExact len.toNat rest
  | _ => .error .unexpectedEndGroupTag

def skipFieldAuxL350–355 ↗#

prost::encoding::skip_field, checking depth > 0 before dispatching on wt.

def skipFieldAux : Nat → WireType → BitVec 32 → Bytes → Except DecodeErr Bytes
  | 0, _, _, _ => .error .recursionLimitExceeded
  | depth' + 1, wt, tag, bs =>
    if wt == .startGroup then skipGroupLoop (skipFieldAux depth') bs.length tag bs
    else skipFieldNonGroup wt bs

def skipFieldL357–358 ↗#

def skipField (wt : WireType) (tag : BitVec 32) (bs : Bytes) (depth : Nat) : Except DecodeErr Bytes :=
  skipFieldAux depth wt tag bs

def mergeUint32L360–361 ↗#

def mergeUint32 (wt : WireType) (bs : Bytes) : Except DecodeErr (BitVec 32 × Bytes) := do
  checkWireType .varint wt; let (v, rest) ← decodeVarint bs; .ok (v.truncate 32, rest)

def mergeUint64L362–363 ↗#

def mergeUint64 (wt : WireType) (bs : Bytes) : Except DecodeErr (BitVec 64 × Bytes) := do
  checkWireType .varint wt; decodeVarint bs

def mergeInt32L364–365 ↗#

def mergeInt32 (wt : WireType) (bs : Bytes) : Except DecodeErr (BitVec 32 × Bytes) := do
  checkWireType .varint wt; let (v, rest) ← decodeVarint bs; .ok (v.truncate 32, rest)

def mergeBoolL366–367 ↗#

def mergeBool (wt : WireType) (bs : Bytes) : Except DecodeErr (Bool × Bytes) := do
  checkWireType .varint wt; let (v, rest) ← decodeVarint bs; .ok (v != 0#64, rest)

def mergeBytesL368–369 ↗#

def mergeBytes (wt : WireType) (bs : Bytes) : Except DecodeErr (Bytes × Bytes) := do
  checkWireType .lengthDelimited wt; let (len, rest) ← decodeVarint bs; takeExact len.toNat rest

def mergeRepeatedBytesL370–372 ↗#

def mergeRepeatedBytes (wt : WireType) (vals : List Bytes) (bs : Bytes) :
    Except DecodeErr (List Bytes × Bytes) := do
  let (b, rest) ← mergeBytes wt bs; .ok (vals ++ [b], rest)

def encodeUint32FieldL374–375 ↗#

def encodeUint32Field (tag : BitVec 32) (v : BitVec 32) : Bytes :=
  if v == 0#32 then [] else encodeKey tag .varint ++ encodeVarint (v.zeroExtend 64)

def encodeUint64FieldL376–377 ↗#

def encodeUint64Field (tag : BitVec 32) (v : BitVec 64) : Bytes :=
  if v == 0#64 then [] else encodeKey tag .varint ++ encodeVarint v

def encodeInt32FieldL378–379 ↗#

def encodeInt32Field (tag : BitVec 32) (v : BitVec 32) : Bytes :=
  if v == 0#32 then [] else encodeKey tag .varint ++ encodeVarint (v.signExtend 64)

def encodeBoolFieldL380–381 ↗#

def encodeBoolField (tag : BitVec 32) (v : Bool) : Bytes :=
  if v then encodeKey tag .varint ++ [1#8] else []

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

CryptoVerification.LibsignalSpqrV1.Proto.encodeBoolOneof

def encodeBytesUncondL385–386 ↗#

def encodeBytesUncond (tag : BitVec 32) (v : Bytes) : Bytes :=
  encodeKey tag .lengthDelimited ++ encodeVarint (BitVec.ofNat 64 v.length) ++ v

def encodeBytesFieldL387–388 ↗#

def encodeBytesField (tag : BitVec 32) (v : Bytes) : Bytes :=
  if v.isEmpty then [] else encodeBytesUncond tag v

def encodeRepeatedBytesL389–390 ↗#

def encodeRepeatedBytes (tag : BitVec 32) (vs : List Bytes) : Bytes :=
  vs.foldr (fun v acc => encodeBytesUncond tag v ++ acc) []

def mergeFieldsLoopL392–400 ↗#

def mergeFieldsLoop {M : Type}
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes)) :
    Nat → M → Bytes → Nat → Except DecodeErr M
  | _, m, [], _ => .ok m
  | 0, _, _ :: _, _ => .error .bufferUnderflow
  | fuel + 1, m, bs, depth => do
    let ((tag, wt), rest) ← decodeKey bs
    let (m', rest') ← mergeField m tag wt rest depth
    mergeFieldsLoop mergeField fuel m' rest' depth

def mergeMessageL402–414 ↗#

prost::encoding::message::merge: decodes a length-prefixed nested message with recursion budget depth.

def mergeMessage {M : Type}
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes))
    (wt : WireType) (m : M) (bs : Bytes) (depth : Nat) : Except DecodeErr (M × Bytes) := do
  checkWireType .lengthDelimited wt
  match depth with
  | 0 => .error .recursionLimitExceeded
  | depth' + 1 => do
    let (len, rest) ← decodeVarint bs
    let (sub, after) ← takeExact len.toNat rest
    let m' ← mergeFieldsLoop mergeField sub.length m sub depth'
    .ok (m', after)

def mergeOptMessageL416–420 ↗#

def mergeOptMessage {M : Type} [Inhabited M]
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes))
    (wt : WireType) (opt : Option M) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (Option M × Bytes) := do
  let (m', rest) ← mergeMessage mergeField wt (opt.getD default) bs depth; .ok (some m', rest)

def mergeRepeatedMessageL422–426 ↗#

def mergeRepeatedMessage {M : Type} [Inhabited M]
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes))
    (wt : WireType) (ms : List M) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (List M × Bytes) := do
  let (m', rest) ← mergeMessage mergeField wt default bs depth; .ok (ms ++ [m'], rest)

def encodeMessageL428–430 ↗#

def encodeMessage {M : Type} (encodeRaw : M → Bytes) (tag : BitVec 32) (m : M) : Bytes :=
  let raw := encodeRaw m
  encodeKey tag .lengthDelimited ++ encodeVarint (BitVec.ofNat 64 raw.length) ++ raw

def encodeOptMessageL431–432 ↗#

def encodeOptMessage {M : Type} (encodeRaw : M → Bytes) (tag : BitVec 32) : Option M → Bytes
  | none => [] | some m => encodeMessage encodeRaw tag m

def encodeRepeatedMessageL433–434 ↗#

def encodeRepeatedMessage {M : Type} (encodeRaw : M → Bytes) (tag : BitVec 32) (ms : List M) : Bytes :=
  ms.foldr (fun m acc => encodeMessage encodeRaw tag m ++ acc) []

def mergeTopLevelMessageL436–439 ↗#

def mergeTopLevelMessage {M : Type}
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes))
    (m : M) (bs : Bytes) : Except DecodeErr M :=
  mergeFieldsLoop mergeField bs.length m bs RECURSION_LIMIT

def decodeTopLevelMessageL440–443 ↗#

def decodeTopLevelMessage {M : Type} [Inhabited M]
    (mergeField : M → BitVec 32 → WireType → Bytes → Nat → Except DecodeErr (M × Bytes))
    (bs : Bytes) : Except DecodeErr M :=
  mergeTopLevelMessage mergeField default bs

end Proto

abbrev WireTypeL447 ↗#

abbrev WireType := Proto.WireType

abbrev DecodeErrL448 ↗#

abbrev DecodeErr := Proto.DecodeErr

namespace PolynomialEncoder

def mergeFieldL453–459 ↗#

open Proto in
def mergeField (m : PolynomialEncoder) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (PolynomialEncoder × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with idx := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeRepeatedBytes wt m.pts bs; .ok ({ m with pts := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeRepeatedBytes wt m.polys bs; .ok ({ m with polys := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.PolynomialEncoder.merge, CryptoVerification.LibsignalSpqrV1.PolynomialEncoder.decode

def encodeRawL462–463 ↗#

def encodeRaw (m : PolynomialEncoder) : Bytes :=
  Proto.encodeUint32Field 1#32 m.idx ++ Proto.encodeRepeatedBytes 2#32 m.pts ++ Proto.encodeRepeatedBytes 3#32 m.polys

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

CryptoVerification.LibsignalSpqrV1.PolynomialEncoder.encodedLen, CryptoVerification.LibsignalSpqrV1.PolynomialEncoder.encode

end PolynomialEncoder

namespace PolynomialDecoder

def mergeFieldL469–476 ↗#

open Proto in
def mergeField (m : PolynomialDecoder) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (PolynomialDecoder × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with ptsNeeded := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with polys := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeRepeatedBytes wt m.pts bs; .ok ({ m with pts := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBool wt bs; .ok ({ m with isComplete := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.PolynomialDecoder.merge, CryptoVerification.LibsignalSpqrV1.PolynomialDecoder.decode

def encodeRawL479–481 ↗#

def encodeRaw (m : PolynomialDecoder) : Bytes :=
  Proto.encodeUint32Field 1#32 m.ptsNeeded ++ Proto.encodeUint32Field 2#32 m.polys ++
  Proto.encodeRepeatedBytes 3#32 m.pts ++ Proto.encodeBoolField 4#32 m.isComplete

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

CryptoVerification.LibsignalSpqrV1.PolynomialDecoder.encodedLen, CryptoVerification.LibsignalSpqrV1.PolynomialDecoder.encode

end PolynomialDecoder

namespace ChainParamsPB

def mergeFieldL487–492 ↗#

open Proto in
def mergeField (m : ChainParamsPB) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (ChainParamsPB × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with maxJump := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with maxOooKeys := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.ChainParamsPB.merge, CryptoVerification.LibsignalSpqrV1.ChainParamsPB.decode

def encodeRawL495 ↗#

def encodeRaw (m : ChainParamsPB) : Bytes := Proto.encodeUint32Field 1#32 m.maxJump ++ Proto.encodeUint32Field 2#32 m.maxOooKeys

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

CryptoVerification.LibsignalSpqrV1.ChainParamsPB.encodedLen, CryptoVerification.LibsignalSpqrV1.ChainParamsPB.encode

end ChainParamsPB

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

CryptoVerification.LibsignalSpqrV1.ProtoChainParams.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoChainParams.merge, CryptoVerification.LibsignalSpqrV1.ProtoChainParams.decode, CryptoVerification.LibsignalSpqrV1.ProtoChainParams.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoChainParams.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoChainParams.encode

namespace EpochDirectionPB

def mergeFieldL510–516 ↗#

open Proto in
def mergeField (m : EpochDirectionPB) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (EpochDirectionPB × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint32 wt bs; .ok ({ m with ctr := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with next := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with prev := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.EpochDirectionPB.merge, CryptoVerification.LibsignalSpqrV1.EpochDirectionPB.decode

def encodeRawL519–520 ↗#

def encodeRaw (m : EpochDirectionPB) : Bytes :=
  Proto.encodeUint32Field 1#32 m.ctr ++ Proto.encodeBytesField 2#32 m.next ++ Proto.encodeBytesField 3#32 m.prev

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

CryptoVerification.LibsignalSpqrV1.EpochDirectionPB.encodedLen, CryptoVerification.LibsignalSpqrV1.EpochDirectionPB.encode

end EpochDirectionPB

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

CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.merge, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.decode, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoEpochDirection.encode

namespace ChainEpochPB

def mergeFieldL535–540 ↗#

open Proto in
def mergeField (m : ChainEpochPB) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (ChainEpochPB × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage EpochDirectionPB.mergeField wt m.send bs depth; .ok ({ m with send := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage EpochDirectionPB.mergeField wt m.recv bs depth; .ok ({ m with recv := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.ChainEpochPB.merge, CryptoVerification.LibsignalSpqrV1.ChainEpochPB.decode

def encodeRawL543–544 ↗#

def encodeRaw (m : ChainEpochPB) : Bytes :=
  Proto.encodeOptMessage EpochDirectionPB.encodeRaw 1#32 m.send ++ Proto.encodeOptMessage EpochDirectionPB.encodeRaw 2#32 m.recv

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

CryptoVerification.LibsignalSpqrV1.ChainEpochPB.encodedLen, CryptoVerification.LibsignalSpqrV1.ChainEpochPB.encode

end ChainEpochPB

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

CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.merge, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.decode, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoChainEpoch.encode

namespace ChainPB

def mergeFieldL559–568 ↗#

open Proto in
def mergeField (m : ChainPB) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (ChainPB × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeInt32 wt bs; .ok ({ m with direction := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with currentEpoch := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeRepeatedMessage ChainEpochPB.mergeField wt m.links bs depth; .ok ({ m with links := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with nextRoot := v }, bs')
  else if tag == 5#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with sendEpoch := v }, bs')
  else if tag == 6#32 then let (v, bs') ← mergeOptMessage ChainParamsPB.mergeField wt m.params bs depth; .ok ({ m with params := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.ChainPB.merge, CryptoVerification.LibsignalSpqrV1.ChainPB.decode

def encodeRawL571–575 ↗#

def encodeRaw (m : ChainPB) : Bytes :=
  Proto.encodeInt32Field 1#32 m.direction ++ Proto.encodeUint64Field 2#32 m.currentEpoch ++
  Proto.encodeRepeatedMessage ChainEpochPB.encodeRaw 3#32 m.links ++
  Proto.encodeBytesField 4#32 m.nextRoot ++ Proto.encodeUint64Field 5#32 m.sendEpoch ++
  Proto.encodeOptMessage ChainParamsPB.encodeRaw 6#32 m.params

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

CryptoVerification.LibsignalSpqrV1.ChainPB.encodedLen, CryptoVerification.LibsignalSpqrV1.ChainPB.encode

end ChainPB

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

CryptoVerification.LibsignalSpqrV1.ProtoChain.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoChain.merge, CryptoVerification.LibsignalSpqrV1.ProtoChain.decode, CryptoVerification.LibsignalSpqrV1.ProtoChain.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoChain.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoChain.encode

namespace VersionNegotiationPB

def mergeFieldL590–597 ↗#

open Proto in
def mergeField (m : VersionNegotiationPB) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (VersionNegotiationPB × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with authKey := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeInt32 wt bs; .ok ({ m with direction := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeInt32 wt bs; .ok ({ m with minVersion := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeOptMessage ChainParamsPB.mergeField wt m.chainParams bs depth; .ok ({ m with chainParams := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.VersionNegotiationPB.merge, CryptoVerification.LibsignalSpqrV1.VersionNegotiationPB.decode

def encodeRawL600–602 ↗#

def encodeRaw (m : VersionNegotiationPB) : Bytes :=
  Proto.encodeBytesField 1#32 m.authKey ++ Proto.encodeInt32Field 2#32 m.direction ++
  Proto.encodeInt32Field 3#32 m.minVersion ++ Proto.encodeOptMessage ChainParamsPB.encodeRaw 4#32 m.chainParams

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

CryptoVerification.LibsignalSpqrV1.VersionNegotiationPB.encodedLen, CryptoVerification.LibsignalSpqrV1.VersionNegotiationPB.encode

end VersionNegotiationPB

12 declarations not shown (lines 608–627): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.merge, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.decode, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoVersionNegotiation.encode, CryptoVerification.LibsignalSpqrV1.ProtoChunk.mergeField, CryptoVerification.LibsignalSpqrV1.ProtoChunk.merge, CryptoVerification.LibsignalSpqrV1.ProtoChunk.decode, CryptoVerification.LibsignalSpqrV1.ProtoChunk.encodeRaw, CryptoVerification.LibsignalSpqrV1.ProtoChunk.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoChunk.encode

namespace V1Msg.InnerMsg

def mergeL631–650 ↗#

open Proto in
def merge (cur : Option V1Msg.InnerMsg) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (Option V1Msg.InnerMsg × Bytes) := do
  if tag == 3#32 then
    let prev := match cur with | some (.hdr v) => v | _ => default
    let (v, rest) ← mergeMessage ProtoChunk.mergeField wt prev bs depth; .ok (some (.hdr v), rest)
  else if tag == 4#32 then
    let prev := match cur with | some (.ek v) => v | _ => default
    let (v, rest) ← mergeMessage ProtoChunk.mergeField wt prev bs depth; .ok (some (.ek v), rest)
  else if tag == 5#32 then
    let prev := match cur with | some (.ekCt1Ack v) => v | _ => default
    let (v, rest) ← mergeMessage ProtoChunk.mergeField wt prev bs depth; .ok (some (.ekCt1Ack v), rest)
  else if tag == 6#32 then let (v, rest) ← mergeBool wt bs; .ok (some (.ct1Ack v), rest)
  else if tag == 7#32 then
    let prev := match cur with | some (.ct1 v) => v | _ => default
    let (v, rest) ← mergeMessage ProtoChunk.mergeField wt prev bs depth; .ok (some (.ct1 v), rest)
  else if tag == 8#32 then
    let prev := match cur with | some (.ct2 v) => v | _ => default
    let (v, rest) ← mergeMessage ProtoChunk.mergeField wt prev bs depth; .ok (some (.ct2 v), rest)
  else let rest ← skipField wt tag bs depth; .ok (cur, rest)

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

CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.encode, CryptoVerification.LibsignalSpqrV1.V1Msg.InnerMsg.encodedLen

end V1Msg.InnerMsg

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

CryptoVerification.LibsignalSpqrV1.V1Msg.mergeField, CryptoVerification.LibsignalSpqrV1.V1Msg.merge, CryptoVerification.LibsignalSpqrV1.V1Msg.decode, CryptoVerification.LibsignalSpqrV1.V1Msg.encodeRaw, CryptoVerification.LibsignalSpqrV1.V1Msg.encodedLen, CryptoVerification.LibsignalSpqrV1.V1Msg.encode

namespace ProtoAuthenticator

def mergeFieldL677–682 ↗#

open Proto in
def mergeField (m : ProtoAuthenticator) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (ProtoAuthenticator × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with rootKey := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with macKey := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.ProtoAuthenticator.merge, CryptoVerification.LibsignalSpqrV1.ProtoAuthenticator.decode

def encodeRawL685 ↗#

def encodeRaw (m : ProtoAuthenticator) : Bytes := Proto.encodeBytesField 1#32 m.rootKey ++ Proto.encodeBytesField 2#32 m.macKey

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

CryptoVerification.LibsignalSpqrV1.ProtoAuthenticator.encodedLen, CryptoVerification.LibsignalSpqrV1.ProtoAuthenticator.encode

end ProtoAuthenticator

namespace V1State.Unchunked

open Proto

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.mergeField, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.decode, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.encodeRaw, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.encode

namespace KeysUnsampled

def mergeFieldL700–703 ↗#

def mergeField (m : KeysUnsampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (KeysUnsampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.KeysUnsampled.decode

def encodeRawL705 ↗#

def encodeRaw (m : KeysUnsampled) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.KeysUnsampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.KeysUnsampled.encode

end KeysUnsampled

namespace HeaderSent

def mergeFieldL711–716 ↗#

def mergeField (m : HeaderSent) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (HeaderSent × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with ek := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with dk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderSent.decode

def encodeRawL718 ↗#

def encodeRaw (m : HeaderSent) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.ek ++ encodeBytesField 4#32 m.dk

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderSent.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderSent.encode

end HeaderSent

namespace EkSent

def mergeFieldL724–728 ↗#

def mergeField (m : EkSent) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (EkSent × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with dk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSent.decode

def encodeRawL730 ↗#

def encodeRaw (m : EkSent) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.dk

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSent.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSent.encode

end EkSent

namespace EkSentCt1Received

def mergeFieldL736–741 ↗#

def mergeField (m : EkSentCt1Received) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (EkSentCt1Received × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with dk := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with ct1 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSentCt1Received.decode

def encodeRawL743 ↗#

def encodeRaw (m : EkSentCt1Received) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.dk ++ encodeBytesField 4#32 m.ct1

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSentCt1Received.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkSentCt1Received.encode

end EkSentCt1Received

namespace NoHeaderReceived

def mergeFieldL749–752 ↗#

def mergeField (m : NoHeaderReceived) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (NoHeaderReceived × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.NoHeaderReceived.decode

def encodeRawL754 ↗#

def encodeRaw (m : NoHeaderReceived) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.NoHeaderReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.NoHeaderReceived.encode

end NoHeaderReceived

namespace HeaderReceived

def mergeFieldL760–764 ↗#

def mergeField (m : HeaderReceived) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (HeaderReceived × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with hdr := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderReceived.decode

def encodeRawL766 ↗#

def encodeRaw (m : HeaderReceived) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.hdr

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.HeaderReceived.encode

end HeaderReceived

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.mergeField, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.decode, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.encodeRaw, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.EkReceived.encode

namespace Ct1Sent

def mergeFieldL785–791 ↗#

def mergeField (m : Ct1Sent) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct1Sent × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with hdr := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with es := v }, bs')
  else if tag == 5#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with ct1 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1Sent.decode

def encodeRawL793 ↗#

def encodeRaw (m : Ct1Sent) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.hdr ++ encodeBytesField 4#32 m.es ++ encodeBytesField 5#32 m.ct1

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1Sent.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1Sent.encode

end Ct1Sent

namespace Ct1SentEkReceived

def mergeFieldL799–805 ↗#

def mergeField (m : Ct1SentEkReceived) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct1SentEkReceived × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with es := v }, bs')
  else if tag == 4#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with ek := v }, bs')
  else if tag == 5#32 then let (v, bs') ← mergeBytes wt bs; .ok ({ m with ct1 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1SentEkReceived.decode

def encodeRawL807 ↗#

def encodeRaw (m : Ct1SentEkReceived) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth ++ encodeBytesField 3#32 m.es ++ encodeBytesField 4#32 m.ek ++ encodeBytesField 5#32 m.ct1

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1SentEkReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct1SentEkReceived.encode

end Ct1SentEkReceived

namespace Ct2Sent

def mergeFieldL813–816 ↗#

def mergeField (m : Ct2Sent) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct2Sent × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeUint64 wt bs; .ok ({ m with epoch := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage ProtoAuthenticator.mergeField wt m.auth bs depth; .ok ({ m with auth := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct2Sent.decode

def encodeRawL818 ↗#

def encodeRaw (m : Ct2Sent) : Bytes := encodeUint64Field 1#32 m.epoch ++ encodeOptMessage ProtoAuthenticator.encodeRaw 2#32 m.auth

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

CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct2Sent.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Unchunked.Ct2Sent.encode

end Ct2Sent

end V1State.Unchunked

namespace V1State.Chunked

open Proto

namespace KeysUnsampled

def mergeFieldL827–828 ↗#

def mergeField (m : KeysUnsampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (KeysUnsampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.KeysUnsampled.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs') else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysUnsampled.decode

def encodeRawL830 ↗#

def encodeRaw (m : KeysUnsampled) : Bytes := encodeOptMessage Unchunked.KeysUnsampled.encodeRaw 1#32 m.uc

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysUnsampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysUnsampled.encode

end KeysUnsampled

namespace KeysSampled

def mergeFieldL836–839 ↗#

def mergeField (m : KeysSampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (KeysSampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.HeaderSent.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingHdr bs depth; .ok ({ m with sendingHdr := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysSampled.decode

def encodeRawL841 ↗#

def encodeRaw (m : KeysSampled) : Bytes := encodeOptMessage Unchunked.HeaderSent.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingHdr

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysSampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.KeysSampled.encode

end KeysSampled

namespace HeaderSent

def mergeFieldL847–851 ↗#

def mergeField (m : HeaderSent) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (HeaderSent × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.EkSent.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingEk bs depth; .ok ({ m with sendingEk := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingCt1 bs depth; .ok ({ m with receivingCt1 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderSent.decode

def encodeRawL853 ↗#

def encodeRaw (m : HeaderSent) : Bytes := encodeOptMessage Unchunked.EkSent.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingEk ++ encodeOptMessage PolynomialDecoder.encodeRaw 3#32 m.receivingCt1

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderSent.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderSent.encode

end HeaderSent

namespace Ct1Received

def mergeFieldL859–862 ↗#

def mergeField (m : Ct1Received) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct1Received × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.EkSentCt1Received.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingEk bs depth; .ok ({ m with sendingEk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Received.decode

def encodeRawL864 ↗#

def encodeRaw (m : Ct1Received) : Bytes := encodeOptMessage Unchunked.EkSentCt1Received.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingEk

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Received.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Received.encode

end Ct1Received

namespace EkSentCt1Received

def mergeFieldL870–873 ↗#

def mergeField (m : EkSentCt1Received) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (EkSentCt1Received × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.EkSentCt1Received.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingCt2 bs depth; .ok ({ m with receivingCt2 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkSentCt1Received.decode

def encodeRawL875 ↗#

def encodeRaw (m : EkSentCt1Received) : Bytes := encodeOptMessage Unchunked.EkSentCt1Received.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialDecoder.encodeRaw 3#32 m.receivingCt2

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkSentCt1Received.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkSentCt1Received.encode

end EkSentCt1Received

namespace NoHeaderReceived

def mergeFieldL881–884 ↗#

def mergeField (m : NoHeaderReceived) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (NoHeaderReceived × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.NoHeaderReceived.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingHdr bs depth; .ok ({ m with receivingHdr := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.NoHeaderReceived.decode

def encodeRawL886 ↗#

def encodeRaw (m : NoHeaderReceived) : Bytes := encodeOptMessage Unchunked.NoHeaderReceived.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialDecoder.encodeRaw 2#32 m.receivingHdr

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.NoHeaderReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.NoHeaderReceived.encode

end NoHeaderReceived

namespace HeaderReceived

def mergeFieldL892–895 ↗#

def mergeField (m : HeaderReceived) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (HeaderReceived × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.HeaderReceived.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingEk bs depth; .ok ({ m with receivingEk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderReceived.decode

def encodeRawL897 ↗#

def encodeRaw (m : HeaderReceived) : Bytes := encodeOptMessage Unchunked.HeaderReceived.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialDecoder.encodeRaw 2#32 m.receivingEk

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderReceived.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.HeaderReceived.encode

end HeaderReceived

namespace Ct1Sampled

def mergeFieldL903–907 ↗#

def mergeField (m : Ct1Sampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct1Sampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.Ct1Sent.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingCt1 bs depth; .ok ({ m with sendingCt1 := v }, bs')
  else if tag == 3#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingEk bs depth; .ok ({ m with receivingEk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Sampled.decode

def encodeRawL909 ↗#

def encodeRaw (m : Ct1Sampled) : Bytes := encodeOptMessage Unchunked.Ct1Sent.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingCt1 ++ encodeOptMessage PolynomialDecoder.encodeRaw 3#32 m.receivingEk

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Sampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Sampled.encode

end Ct1Sampled

namespace EkReceivedCt1Sampled

def mergeFieldL915–918 ↗#

def mergeField (m : EkReceivedCt1Sampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (EkReceivedCt1Sampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.Ct1SentEkReceived.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingCt1 bs depth; .ok ({ m with sendingCt1 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkReceivedCt1Sampled.decode

def encodeRawL920 ↗#

def encodeRaw (m : EkReceivedCt1Sampled) : Bytes := encodeOptMessage Unchunked.Ct1SentEkReceived.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingCt1

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkReceivedCt1Sampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.EkReceivedCt1Sampled.encode

end EkReceivedCt1Sampled

namespace Ct1Acknowledged

def mergeFieldL926–929 ↗#

def mergeField (m : Ct1Acknowledged) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct1Acknowledged × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.Ct1Sent.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialDecoder.mergeField wt m.receivingEk bs depth; .ok ({ m with receivingEk := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Acknowledged.decode

def encodeRawL931 ↗#

def encodeRaw (m : Ct1Acknowledged) : Bytes := encodeOptMessage Unchunked.Ct1Sent.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialDecoder.encodeRaw 2#32 m.receivingEk

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Acknowledged.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct1Acknowledged.encode

end Ct1Acknowledged

namespace Ct2Sampled

def mergeFieldL937–940 ↗#

def mergeField (m : Ct2Sampled) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) : Except DecodeErr (Ct2Sampled × Bytes) := do
  if tag == 1#32 then let (v, bs') ← mergeOptMessage Unchunked.Ct2Sent.mergeField wt m.uc bs depth; .ok ({ m with uc := v }, bs')
  else if tag == 2#32 then let (v, bs') ← mergeOptMessage PolynomialEncoder.mergeField wt m.sendingCt2 bs depth; .ok ({ m with sendingCt2 := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct2Sampled.decode

def encodeRawL942 ↗#

def encodeRaw (m : Ct2Sampled) : Bytes := encodeOptMessage Unchunked.Ct2Sent.encodeRaw 1#32 m.uc ++ encodeOptMessage PolynomialEncoder.encodeRaw 2#32 m.sendingCt2

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

CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct2Sampled.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.Chunked.Ct2Sampled.encode

end Ct2Sampled

end V1State.Chunked

namespace V1State.InnerState

def mergeL949–974 ↗#

open Proto in
def merge (cur : Option V1State.InnerState) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (Option V1State.InnerState × Bytes) := do
  if tag == 1#32 then
    let (v, bs') ← mergeMessage Chunked.KeysUnsampled.mergeField wt (match cur with | some (.keysUnsampled v) => v | _ => default) bs depth; .ok (some (.keysUnsampled v), bs')
  else if tag == 2#32 then
    let (v, bs') ← mergeMessage Chunked.KeysSampled.mergeField wt (match cur with | some (.keysSampled v) => v | _ => default) bs depth; .ok (some (.keysSampled v), bs')
  else if tag == 3#32 then
    let (v, bs') ← mergeMessage Chunked.HeaderSent.mergeField wt (match cur with | some (.headerSent v) => v | _ => default) bs depth; .ok (some (.headerSent v), bs')
  else if tag == 4#32 then
    let (v, bs') ← mergeMessage Chunked.Ct1Received.mergeField wt (match cur with | some (.ct1Received v) => v | _ => default) bs depth; .ok (some (.ct1Received v), bs')
  else if tag == 5#32 then
    let (v, bs') ← mergeMessage Chunked.EkSentCt1Received.mergeField wt (match cur with | some (.ekSentCt1Received v) => v | _ => default) bs depth; .ok (some (.ekSentCt1Received v), bs')
  else if tag == 6#32 then
    let (v, bs') ← mergeMessage Chunked.NoHeaderReceived.mergeField wt (match cur with | some (.noHeaderReceived v) => v | _ => default) bs depth; .ok (some (.noHeaderReceived v), bs')
  else if tag == 7#32 then
    let (v, bs') ← mergeMessage Chunked.HeaderReceived.mergeField wt (match cur with | some (.headerReceived v) => v | _ => default) bs depth; .ok (some (.headerReceived v), bs')
  else if tag == 8#32 then
    let (v, bs') ← mergeMessage Chunked.Ct1Sampled.mergeField wt (match cur with | some (.ct1Sampled v) => v | _ => default) bs depth; .ok (some (.ct1Sampled v), bs')
  else if tag == 9#32 then
    let (v, bs') ← mergeMessage Chunked.EkReceivedCt1Sampled.mergeField wt (match cur with | some (.ekReceivedCt1Sampled v) => v | _ => default) bs depth; .ok (some (.ekReceivedCt1Sampled v), bs')
  else if tag == 10#32 then
    let (v, bs') ← mergeMessage Chunked.Ct1Acknowledged.mergeField wt (match cur with | some (.ct1Acknowledged v) => v | _ => default) bs depth; .ok (some (.ct1Acknowledged v), bs')
  else if tag == 11#32 then
    let (v, bs') ← mergeMessage Chunked.Ct2Sampled.mergeField wt (match cur with | some (.ct2Sampled v) => v | _ => default) bs depth; .ok (some (.ct2Sampled v), bs')
  else let bs' ← skipField wt tag bs depth; .ok (cur, bs')

def encodeL975–986 ↗#

def encode : V1State.InnerState → Bytes
  | .keysUnsampled v        => Proto.encodeMessage Chunked.KeysUnsampled.encodeRaw 1#32 v
  | .keysSampled v          => Proto.encodeMessage Chunked.KeysSampled.encodeRaw 2#32 v
  | .headerSent v           => Proto.encodeMessage Chunked.HeaderSent.encodeRaw 3#32 v
  | .ct1Received v          => Proto.encodeMessage Chunked.Ct1Received.encodeRaw 4#32 v
  | .ekSentCt1Received v    => Proto.encodeMessage Chunked.EkSentCt1Received.encodeRaw 5#32 v
  | .noHeaderReceived v     => Proto.encodeMessage Chunked.NoHeaderReceived.encodeRaw 6#32 v
  | .headerReceived v       => Proto.encodeMessage Chunked.HeaderReceived.encodeRaw 7#32 v
  | .ct1Sampled v           => Proto.encodeMessage Chunked.Ct1Sampled.encodeRaw 8#32 v
  | .ekReceivedCt1Sampled v => Proto.encodeMessage Chunked.EkReceivedCt1Sampled.encodeRaw 9#32 v
  | .ct1Acknowledged v      => Proto.encodeMessage Chunked.Ct1Acknowledged.encodeRaw 10#32 v
  | .ct2Sampled v           => Proto.encodeMessage Chunked.Ct2Sampled.encodeRaw 11#32 v

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

CryptoVerification.LibsignalSpqrV1.V1State.InnerState.encodedLen

end V1State.InnerState

namespace V1State

def mergeFieldL991–996 ↗#

open Proto in
def mergeField (m : V1State) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (V1State × Bytes) := do
  if tag ≥ 1#32 && tag ≤ 11#32 then
    let (is', bs') ← V1State.InnerState.merge m.innerState tag wt bs depth; .ok ({ m with innerState := is' }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.V1State.merge

def decodeL998 ↗#

def decode (bs : Bytes) : Except DecodeErr V1State := Proto.decodeTopLevelMessage mergeField bs

def encodeRawL999 ↗#

def encodeRaw (m : V1State) : Bytes := match m.innerState with | none => [] | some is => V1State.InnerState.encode is

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

CryptoVerification.LibsignalSpqrV1.V1State.encodedLen, CryptoVerification.LibsignalSpqrV1.V1State.encode

end V1State

namespace PqRatchetState.Inner

def mergeL1005–1011 ↗#

open Proto in
def merge (cur : Option PqRatchetState.Inner) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (Option PqRatchetState.Inner × Bytes) := do
  if tag == 3#32 then
    let prev := match cur with | some (.v1 v) => v | none => default
    let (v, bs') ← mergeMessage V1State.mergeField wt prev bs depth; .ok (some (.v1 v), bs')
  else let bs' ← skipField wt tag bs depth; .ok (cur, bs')

def encodeL1012 ↗#

def encode : PqRatchetState.Inner → Bytes | .v1 v => Proto.encodeMessage V1State.encodeRaw 3#32 v

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

CryptoVerification.LibsignalSpqrV1.PqRatchetState.Inner.encodedLen

end PqRatchetState.Inner

namespace PqRatchetState

def mergeFieldL1017–1029 ↗#

open Proto in
def mergeField (m : PqRatchetState) (tag : BitVec 32) (wt : WireType) (bs : Bytes) (depth : Nat) :
    Except DecodeErr (PqRatchetState × Bytes) := do
  if tag == 1#32 then
    let (v, bs') ← mergeOptMessage VersionNegotiationPB.mergeField wt m.versionNegotiation bs depth
    .ok ({ m with versionNegotiation := v }, bs')
  else if tag == 2#32 then
    let (v, bs') ← mergeOptMessage ChainPB.mergeField wt m.chain bs depth
    .ok ({ m with chain := v }, bs')
  else if tag == 3#32 then
    let (v, bs') ← PqRatchetState.Inner.merge m.inner tag wt bs depth
    .ok ({ m with inner := v }, bs')
  else let bs' ← skipField wt tag bs depth; .ok (m, bs')

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

CryptoVerification.LibsignalSpqrV1.PqRatchetState.merge

def decodeL1031 ↗#

def decode (bs : Bytes) : Except DecodeErr PqRatchetState := Proto.decodeTopLevelMessage mergeField bs

def encodeRawL1032–1035 ↗#

def encodeRaw (m : PqRatchetState) : Bytes :=
  Proto.encodeOptMessage VersionNegotiationPB.encodeRaw 1#32 m.versionNegotiation ++
  Proto.encodeOptMessage ChainPB.encodeRaw 2#32 m.chain ++
  match m.inner with | none => [] | some i => PqRatchetState.Inner.encode i

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

CryptoVerification.LibsignalSpqrV1.PqRatchetState.encodedLen

def encodeL1037 ↗#

def encode (m : PqRatchetState) : Bytes := encodeRaw m

end PqRatchetState

namespace Proto

def decodeStateL1044–1045 ↗#

PqRatchetState::decode (src/lib.rs:503).

def decodeState (bs : Bytes) : Except DecodeErr PqRatchetState := PqRatchetState.decode bs

def spqrDecodeStateL1047–1051 ↗#

spqr::decode_state (src/lib.rs:495–505): returns default PqRatchetState on [], and maps any decode error to Error::StateDecode.

def spqrDecodeState (bs : Bytes) : Except Error PqRatchetState :=
  if bs.isEmpty then .ok { versionNegotiation := none, chain := none, inner := none }
  else match PqRatchetState.decode bs with | .ok st => .ok st | .error _ => .error .stateDecode

def encodeStateL1053–1054 ↗#

PqRatchetState::encode_to_vec.

def encodeState (s : PqRatchetState) : Bytes := PqRatchetState.encode s

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

CryptoVerification.LibsignalSpqrV1.Proto.decodeV1Msg, CryptoVerification.LibsignalSpqrV1.Proto.encodeV1Msg

end Proto

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

CryptoVerification.LibsignalSpqrV1.spqrDecodeState, CryptoVerification.LibsignalSpqrV1.guard_varint_roundtrip, CryptoVerification.LibsignalSpqrV1.guard_varint_10th_byte, CryptoVerification.LibsignalSpqrV1.guard_direction_enums, CryptoVerification.LibsignalSpqrV1.guard_state_roundtrip_all_v1_variants, CryptoVerification.LibsignalSpqrV1.guard_v1msg_roundtrip_all_variants

end CryptoVerification.LibsignalSpqrV1