States.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 1,256 of 2,083 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 (171)

SPQR V1: braid state machine and incremental ML-KEM-768 (src/incremental_mlkem768.rs, src/v1/)

Trusted in part. The theorems of Computational/Theorems/ use only part of this file (see Computational/docs/TRUSTED_BASE.md): the rest is mostly the camelCase aliases (fromPb / intoPb), model-only helpers (SharedSecret, KeyPair, decapsulate, validate_pk, States.epoch), the self-test stubs (stubMlKem, stubPolyApi, stubAuthApi, StubEncoder, StubDecoder), and the check* / guard_* test drivers (guard_issue1275, guard_message_serialize, guard_full_braid_and_pb_roundtrip, guard_panics_and_errors), all checked by Lean.

Models SPQR V1 sparse continuous key agreement (SCKA) over abstract MlKem, erasure-coding PolyApi, and authenticator/KDF AuthApi, with explicit panic/error outcomes (StatesPanic, StatesError, StatesResult):

src/incremental_mlkem768.rs: Keys, generate, encaps1, encaps2, decaps, ek_matches_header (validate_pk_bytes), potentially_fix_state_incorrectly_encoded_by_libcrux_issue_1275, and flip_endianness_of_encapsulation_state.
src/v1/unchunked/{send_ek, send_ct}: unchunked states (KeysUnsampled, HeaderSent, EkSent, EkSentCt1Received; NoHeaderReceived, HeaderReceived, Ct1Sent, Ct1SentEkReceived, Ct2Sent), transitions (send_ek, ...), and into_pb / from_pb.
src/v1/chunked/: the 11-variant States braid machine (States.init_a, States.init_b, States.send -> V1Send, States.recv -> V1Recv, States.into_pb, States.from_pb) and SCKA wire messages (MessagePayload, Message, MessageType, Message.serialize, Message.deserialize).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

Byte helpers

def u64ToBeBytesL51–54 ↗#

Big-endian 8-byte encoding (u64::to_be_bytes).

def u64ToBeBytes (v : BitVec 64) : Bytes :=
  [ v.extractLsb' 56 8, v.extractLsb' 48 8, v.extractLsb' 40 8, v.extractLsb' 32 8,
    v.extractLsb' 24 8, v.extractLsb' 16 8, v.extractLsb'  8 8, v.extractLsb'  0 8 ]

def bytesToVector?L56–57 ↗#

def bytesToVector? (n : Nat) (xs : Bytes) : Option (List.Vector (BitVec 8) n) :=
  if h : xs.length = n then some ⟨xs, h⟩ else none

Panics and results (src/incremental_mlkem768.rs, src/v1/)

inductive StatesPanicL61–79 ↗#

Explicit Rust panic sites in src/incremental_mlkem768.rs and src/v1/{unchunked,chunked}/.

inductive StatesPanic where
  | spqr (p : SpqrPanic)
  | rngExhausted (needed available : Nat)
  | encaps1Failed
  | encaps2BadSize (esLen ekLen : Nat)
  | issue1275BadLen (esLen : Nat)
  | flipEndiannessBadLen (esLen : Nat)
  | decapsBadSize (dkLen ct1Len ct2Len : Nat)
  | unchunkedRecvCt1EpochMismatch (epoch selfEpoch : Epoch)
  | unchunkedRecvCt2EpochOverflow
  | unchunkedRecvHeaderEpochMismatch (epoch selfEpoch : Epoch)
  | unchunkedRecvEkEpochMismatch (epoch selfEpoch : Epoch)
  | unchunkedRecvNextEpochOverflow
  | unchunkedRecvNextEpochMismatch (expected nextEpoch : Epoch)
  | polyExpectFailed (site : String)
  | chunkedEpochMismatch (site : String) (epoch selfEpoch : Epoch)
  | decodedSliceBounds (site : String) (decodedLen splitAt : Nat)
  deriving DecidableEq, Repr, Inhabited

class ToStatesPanicL81–82 ↗#

class ToStatesPanic (ε : Type) where
  toStatesPanic : ε → StatesPanic

instanceL84–85 ↗#

instance : ToStatesPanic StatesPanic where
  toStatesPanic := id

instanceL87–88 ↗#

instance : ToStatesPanic SpqrPanic where
  toStatesPanic := StatesPanic.spqr

def liftSpqrPanicL90–93 ↗#

def liftSpqrPanic {α : Type} (r : Except SpqrPanic α) : Except StatesPanic α :=
  match r with
  | .ok v => .ok v
  | .error p => .error (.spqr p)

instanceL95–96 ↗#

instance : MonadLift (Except SpqrPanic) (Except StatesPanic) where
  monadLift r := liftSpqrPanic r

inductive StatesErrorL98–102 ↗#

Clean Err(Error) return versus Rust panic (StatesPanic).

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

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

CryptoVerification.LibsignalSpqrV1.StatesError.isPanic

abbrev StatesResultL112 ↗#

abbrev StatesResult (α : Type) := Except StatesError α

namespace StatesResult

def ofPanicL116–119 ↗#

def ofPanic {ε : Type} [ToStatesPanic ε] (r : Except ε α) : StatesResult α :=
  match r with
  | .ok v => .ok v
  | .error p => .error (.panic (ToStatesPanic.toStatesPanic p))

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

CryptoVerification.LibsignalSpqrV1.StatesResult.ofError, CryptoVerification.LibsignalSpqrV1.StatesResult.isPanic

end StatesResult

Parameter APIs: PolyApi, AuthApi

structure PolyApiL135–164 ↗#

Abstract polynomial erasure-coding interface (src/encoding.rs, src/encoding/polynomial.rs).

structure PolyApi where
  Chunk : Type
  PolynomialError : Type
  EncodingError : Type
  PolyEncoder : Type
  PolyDecoder : Type
  [decEqChunk : DecidableEq Chunk]
  [reprChunk : Repr Chunk]
  [inhabitedChunk : Inhabited Chunk]
  [decEqPolyErr : DecidableEq PolynomialError]
  [reprPolyErr : Repr PolynomialError]
  [decEqEncErr : DecidableEq EncodingError]
  [reprEncErr : Repr EncodingError]
  [decEqEncoder : DecidableEq PolyEncoder]
  [decEqDecoder : DecidableEq PolyDecoder]
  [reprEncoder : Repr PolyEncoder]
  [reprDecoder : Repr PolyDecoder]
  mkChunk : BitVec 16 → List.Vector (BitVec 8) 32 → Chunk
  chunkIndex : Chunk → BitVec 16
  chunkData : Chunk → List.Vector (BitVec 8) 32
  encode_bytes : Bytes → Except SpqrPanic (Except EncodingError PolyEncoder)
  next_chunk : PolyEncoder → Except SpqrPanic (PolyEncoder × Chunk)
  encoder_into_pb : PolyEncoder → PolynomialEncoder
  encoder_from_pb : PolynomialEncoder → Except SpqrPanic (Except PolynomialError PolyEncoder)
  decoder_new : Nat → Except SpqrPanic (Except EncodingError PolyDecoder)
  add_chunk : PolyDecoder → Chunk → Except SpqrPanic PolyDecoder
  decoded_message : PolyDecoder → Except SpqrPanic (Option Bytes)
  decoder_into_pb : PolyDecoder → PolynomialDecoder
  decoder_from_pb : PolynomialDecoder → Except SpqrPanic (Except PolynomialError PolyDecoder)

def AUTHENTICATOR_MACSIZEL172 ↗#

def AUTHENTICATOR_MACSIZE : Nat := 32

structure AuthApiL174–192 ↗#

Abstract authenticator and HKDF interface (src/authenticator.rs, src/kdf.rs).

structure AuthApi where
  Authenticator : Type
  [decEqAuth : DecidableEq Authenticator]
  [reprAuth : Repr Authenticator]
  new : Bytes → Epoch → Except SpqrPanic Authenticator
  update : Authenticator → Epoch → Bytes → Except SpqrPanic Authenticator
  mac_hdr : Authenticator → Epoch → Bytes → Except SpqrPanic Bytes
  mac_ct : Authenticator → Epoch → Bytes → Except SpqrPanic Bytes
  /-- `Authenticator::verify_hdr` (`util::compare` panics if `expected_mac.len() > 32`). -/
  verify_hdr : Authenticator → Epoch → Bytes → Bytes →
    Except SpqrPanic (Except Error Unit)
  /-- `Authenticator::verify_ct` (`util::compare` panics if `expected_mac.len() > 32`). -/
  verify_ct : Authenticator → Epoch → Bytes → Bytes →
    Except SpqrPanic (Except Error Unit)
  into_pb : Authenticator → ProtoAuthenticator
  from_pb : ProtoAuthenticator → Authenticator
  /-- `kdf::hkdf_to_vec` (`src/kdf.rs:6–18`; panics if `okm_len > 255 * 32`). -/
  hkdf_to_vec : Bytes → Bytes → Bytes → Nat → Except SpqrPanic Bytes

Incremental ML-KEM-768 and issue-1275 fix-up (src/incremental_mlkem768.rs)

def CIPHERTEXT1_SIZEL198 ↗#

def CIPHERTEXT1_SIZE : Nat := 960

def CIPHERTEXT2_SIZEL200 ↗#

def CIPHERTEXT2_SIZE : Nat := 128

def HEADER_SIZEL202 ↗#

def HEADER_SIZE : Nat := 64

def ENCAPSULATION_KEY_SIZEL204 ↗#

def ENCAPSULATION_KEY_SIZE : Nat := 1152

def ENCAPSULATION_STATE_SIZEL206 ↗#

def ENCAPSULATION_STATE_SIZE : Nat := 2080

def DECAPSULATION_KEY_SIZEL208 ↗#

def DECAPSULATION_KEY_SIZE : Nat := 2400

def KEY_GENERATION_SEED_SIZEL210 ↗#

def KEY_GENERATION_SEED_SIZE : Nat := 64

def SHARED_SECRET_SIZEL212 ↗#

def SHARED_SECRET_SIZE : Nat := 32

abbrev Ciphertext1L214 ↗#

abbrev Ciphertext1 := Bytes

abbrev EncapsulationStateL216 ↗#

abbrev EncapsulationState := Bytes

abbrev Ciphertext2L218 ↗#

abbrev Ciphertext2 := Bytes

abbrev EncapsulationKeyL222 ↗#

abbrev EncapsulationKey := Bytes

abbrev DecapsulationKeyL224 ↗#

abbrev DecapsulationKey := Bytes

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

CryptoVerification.LibsignalSpqrV1.SharedSecret

structure KeysL228–233 ↗#

Split ML-KEM-768 key pair (pub struct Keys, src/incremental_mlkem768.rs:22–26).

structure Keys where
  ek : EncapsulationKey
  dk : DecapsulationKey
  hdr : Header
  deriving DecidableEq, Repr, Inhabited

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

CryptoVerification.LibsignalSpqrV1.KeyPair

def swapAdjacentPairsL237–240 ↗#

Swap adjacent byte pairs (b0, b1) ↦ (b1, b0).

def swapAdjacentPairs : Bytes → Bytes
  | b0 :: b1 :: rest => b1 :: b0 :: swapAdjacentPairs rest
  | xs => xs

def flipEndiannessOfEncapsulationStateBytesL242–245 ↗#

Swap each 2-byte pair in es[0 .. es.len() - 32], leaving the trailing 32-byte randomness unchanged.

def flipEndiannessOfEncapsulationStateBytes (es : EncapsulationState) : EncapsulationState :=
  let prefixLen := es.length - 32
  swapAdjacentPairs (es.take prefixLen) ++ es.drop prefixLen

def flip_endianness_of_encapsulation_stateL247–253 ↗#

flip_endianness_of_encapsulation_state (src/incremental_mlkem768.rs:143–153).

def flip_endianness_of_encapsulation_state (es : EncapsulationState) :
    Except StatesPanic EncapsulationState :=
  if es.length % 2 != 0 || !(es.length > 32) then
    .error (.flipEndiannessBadLen es.length)
  else
    .ok (flipEndiannessOfEncapsulationStateBytes es)

def issue1275NeedsFlipL255–269 ↗#

Scan es[1536..2048] in 2-byte LE words (src/incremental_mlkem768.rs:117–137): skip 0/-1, return false on valid LE (1, 2, 0xFFFE), true on byte-swapped BE (0x0100, 0x0200, 0xFEFF), and false otherwise.

def issue1275NeedsFlip : Bytes → Bool
  | b0 :: b1 :: rest =>
    let w : BitVec 16 := (b1.zeroExtend 16 <<< 8) ||| b0.zeroExtend 16
    if w == 0x0000#16 || w == 0xFFFF#16 then
      issue1275NeedsFlip rest
    else if w == 0x0001#16 || w == 0x0002#16 || w == 0xFFFE#16 then
      false
    else if w == 0x0100#16 || w == 0x0200#16 || w == 0xFEFF#16 then
      true
    else
      false
  | _ => false

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

CryptoVerification.LibsignalSpqrV1.potentiallyFixStateIncorrectlyEncodedByLibcruxIssue1275Bytes

def potentially_fix_state_incorrectly_encoded_by_libcrux_issue_1275L279–291 ↗#

potentially_fix_state_incorrectly_encoded_by_libcrux_issue_1275 (src/incremental_mlkem768.rs:92–138), checking es.len() == 2080.

def potentially_fix_state_incorrectly_encoded_by_libcrux_issue_1275
    (es : EncapsulationState) : Except StatesPanic (Option EncapsulationState) :=
  if es.length != ENCAPSULATION_STATE_SIZE then
    .error (.issue1275BadLen es.length)
  else
    let error2Bytes := (es.drop 1536).take (2080 - 32 - 1536)
    if issue1275NeedsFlip error2Bytes then do
      let fixed ← flip_endianness_of_encapsulation_state es
      .ok (some fixed)
    else
      .ok none

def ek_matches_headerL293–295 ↗#

ek_matches_header (src/incremental_mlkem768.rs:28–30).

def ek_matches_header (K : MlKem) (ek : EncapsulationKey) (hdr : Header) : Bool :=
  K.validPkBytes hdr ek

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

CryptoVerification.LibsignalSpqrV1.validate_pk_bytes, CryptoVerification.LibsignalSpqrV1.validate_pk

def generateL302–309 ↗#

generate (src/incremental_mlkem768.rs:34–43): consumes 64 seed bytes from tape.

def generate (K : MlKem) (tape : Bytes) : Except StatesPanic (Keys × Bytes) :=
  match bytesToVector? KEY_GENERATION_SEED_SIZE (tape.take KEY_GENERATION_SEED_SIZE) with
  | none => .error (.rngExhausted KEY_GENERATION_SEED_SIZE tape.length)
  | some seed =>
    let (hdr, ek, dk) := K.fromSeed seed
    .ok ({ ek := ek.toList, dk := dk.toList, hdr := hdr.toList },
      tape.drop KEY_GENERATION_SEED_SIZE)

def encaps1L311–321 ↗#

encaps1 (src/incremental_mlkem768.rs:48–66): consumes 32 random bytes from tape and panics if K.encaps1 returns none.

def encaps1 (K : MlKem) (hdr : Header) (tape : Bytes) :
    Except StatesPanic ((Ciphertext1 × EncapsulationState × Secret) × Bytes) :=
  match bytesToVector? SHARED_SECRET_SIZE (tape.take SHARED_SECRET_SIZE) with
  | none => .error (.rngExhausted SHARED_SECRET_SIZE tape.length)
  | some rand =>
    match K.encaps1 hdr rand with
    | none => .error .encaps1Failed
    | some (ct1, es, ss) =>
      .ok ((ct1.toList, es.toList, ss.toList), tape.drop SHARED_SECRET_SIZE)

def encaps2L323–330 ↗#

encaps2 (src/incremental_mlkem768.rs:71–79), applying the issue-1275 fix-up before K.encaps2.

def encaps2 (K : MlKem) (ek : EncapsulationKey) (es : EncapsulationState) :
    Except StatesPanic Ciphertext2 := do
  let maybeFix ← potentially_fix_state_incorrectly_encoded_by_libcrux_issue_1275 es
  let es' := maybeFix.getD es
  match bytesToVector? ENCAPSULATION_STATE_SIZE es', bytesToVector? ENCAPSULATION_KEY_SIZE ek with
  | some esVec, some ekVec => .ok (K.encaps2 esVec ekVec).toList
  | _, _ => .error (.encaps2BadSize es'.length ek.length)

def decapsL332–339 ↗#

decaps (src/incremental_mlkem768.rs:158–171).

def decaps (K : MlKem) (dk : DecapsulationKey) (ct1 : Ciphertext1) (ct2 : Ciphertext2) :
    Except StatesPanic Secret :=
  match bytesToVector? CIPHERTEXT1_SIZE ct1,
        bytesToVector? CIPHERTEXT2_SIZE ct2,
        bytesToVector? DECAPSULATION_KEY_SIZE dk with
  | some ct1Vec, some ct2Vec, some dkVec => .ok (K.decaps dkVec ct1Vec ct2Vec).toList
  | _, _, _ => .error (.decapsBadSize dk.length ct1.length ct2.length)

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

CryptoVerification.LibsignalSpqrV1.decapsulate

Unchunked state machine (src/v1/unchunked/{send_ek, send_ct})

def sckaKeyInfoPrefixL345–346 ↗#

def sckaKeyInfoPrefix : Bytes :=
  asciiBytes "Signal_PQCKA_V1_MLKEM768:SCKA Key"

namespace Unchunked

namespace SendCt

structure NoHeaderReceivedL352–355 ↗#

structure NoHeaderReceived (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  deriving DecidableEq, Repr

structure HeaderReceivedL357–361 ↗#

structure HeaderReceived (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  hdr : Header
  deriving DecidableEq, Repr

structure Ct1SentL363–369 ↗#

structure Ct1Sent (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  hdr : Header
  es : EncapsulationState
  ct1 : Ciphertext1
  deriving DecidableEq, Repr

structure Ct1SentEkReceivedL371–377 ↗#

structure Ct1SentEkReceived (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  es : EncapsulationState
  ek : EncapsulationKey
  ct1 : Ciphertext1
  deriving DecidableEq, Repr

structure Ct2SentL379–382 ↗#

structure Ct2Sent (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  deriving DecidableEq, Repr

end SendCt

namespace SendEk

structure KeysUnsampledL388–391 ↗#

structure KeysUnsampled (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  deriving DecidableEq, Repr

structure HeaderSentL393–398 ↗#

structure HeaderSent (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  ek : EncapsulationKey
  dk : DecapsulationKey
  deriving DecidableEq, Repr

structure EkSentL400–404 ↗#

structure EkSent (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  dk : DecapsulationKey
  deriving DecidableEq, Repr

structure EkSentCt1ReceivedL406–411 ↗#

structure EkSentCt1Received (Au : AuthApi) where
  epoch : Epoch
  auth : Au.Authenticator
  dk : DecapsulationKey
  ct1 : Ciphertext1
  deriving DecidableEq, Repr

namespace KeysUnsampled

def newL415–417 ↗#

def new (Au : AuthApi) (authKey : Bytes) : Except StatesPanic (KeysUnsampled Au) := do
  let auth ← Au.new authKey 1#64
  .ok { epoch := 1#64, auth := auth }

def send_headerL419–425 ↗#

KeysUnsampled::send_header (src/v1/unchunked/send_ek.rs:84–100).

def send_header (K : MlKem) {Au : AuthApi} (self : KeysUnsampled Au) (tape : Bytes) :
    Except StatesPanic (HeaderSent Au × Header × Mac × Bytes) := do
  let (keys, tape') ← generate K tape
  let mac ← Au.mac_hdr self.auth self.epoch keys.hdr
  .ok ({ epoch := self.epoch, auth := self.auth, ek := keys.ek, dk := keys.dk },
    keys.hdr, mac, tape')

def into_pbL427–428 ↗#

def into_pb {Au : AuthApi} (self : KeysUnsampled Au) : V1State.Unchunked.KeysUnsampled :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth) }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.KeysUnsampled.intoPb

def from_pbL432–435 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.KeysUnsampled) : StatesResult (KeysUnsampled Au) :=
  match pb.auth with
  | none => .error (.err .stateDecode)
  | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.KeysUnsampled.fromPb

end KeysUnsampled

namespace HeaderSent

def send_ekL443–445 ↗#

HeaderSent::send_ek (src/v1/unchunked/send_ek.rs:106–115).

def send_ek {Au : AuthApi} (self : HeaderSent Au) : EkSent Au × EncapsulationKey :=
  ({ epoch := self.epoch, auth := self.auth, dk := self.dk }, self.ek)

def into_pbL447–448 ↗#

def into_pb {Au : AuthApi} (self : HeaderSent Au) : V1State.Unchunked.HeaderSent :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth), ek := self.ek, dk := self.dk }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.HeaderSent.intoPb

def from_pbL452–458 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.HeaderSent) : StatesResult (HeaderSent Au) :=
  if pb.dk.length == DECAPSULATION_KEY_SIZE && pb.ek.length == ENCAPSULATION_KEY_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a, ek := pb.ek, dk := pb.dk }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.HeaderSent.fromPb

end HeaderSent

namespace EkSent

def recv_ct1L466–472 ↗#

EkSent::recv_ct1 (src/v1/unchunked/send_ek.rs:121–133).

def recv_ct1 {Au : AuthApi} (self : EkSent Au) (epoch : Epoch) (ct1 : Ciphertext1) :
    Except StatesPanic (EkSentCt1Received Au) :=
  if epoch != self.epoch then
    .error (.unchunkedRecvCt1EpochMismatch epoch self.epoch)
  else
    .ok { epoch := self.epoch, auth := self.auth, dk := self.dk, ct1 := ct1 }

def into_pbL474–475 ↗#

def into_pb {Au : AuthApi} (self : EkSent Au) : V1State.Unchunked.EkSent :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth), dk := self.dk }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.EkSent.intoPb

def from_pbL479–485 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.EkSent) : StatesResult (EkSent Au) :=
  if pb.dk.length == DECAPSULATION_KEY_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a, dk := pb.dk }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.EkSent.fromPb

end EkSent

namespace EkSentCt1Received

def recv_ct2L493–509 ↗#

EkSentCt1Received::recv_ct2 (src/v1/unchunked/send_ek.rs:139–172).

def recv_ct2 (K : MlKem) {Au : AuthApi} (self : EkSentCt1Received Au)
    (ct2 : Ciphertext2) (mac : Mac) : StatesResult (SendCt.NoHeaderReceived Au × EpochSecret) := do
  let ss ← StatesResult.ofPanic (decaps K self.dk self.ct1 ct2)
  let info := sckaKeyInfoPrefix ++ u64ToBeBytes self.epoch
  let ss ← StatesResult.ofPanic (Au.hkdf_to_vec (List.replicate 32 0#8) ss info 32)
  let auth ← StatesResult.ofPanic (Au.update self.auth self.epoch ss)
  let ct1Full := self.ct1 ++ ct2
  let verifyRes ← StatesResult.ofPanic (Au.verify_ct auth self.epoch ct1Full mac)
  match verifyRes with
  | .error _ => .error (.err .macVerifyFailed)
  | .ok () =>
    if self.epoch == BitVec.allOnes 64 then
      .error (.panic .unchunkedRecvCt2EpochOverflow)
    else
      .ok ({ epoch := self.epoch + 1#64, auth := auth },
        { epoch := self.epoch, secret := ss })

def into_pbL511–512 ↗#

def into_pb {Au : AuthApi} (self : EkSentCt1Received Au) : V1State.Unchunked.EkSentCt1Received :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth), dk := self.dk, ct1 := self.ct1 }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.EkSentCt1Received.intoPb

def from_pbL516–523 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.EkSentCt1Received) :
    StatesResult (EkSentCt1Received Au) :=
  if pb.dk.length == DECAPSULATION_KEY_SIZE && pb.ct1.length == CIPHERTEXT1_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a, dk := pb.dk, ct1 := pb.ct1 }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendEk.EkSentCt1Received.fromPb

end EkSentCt1Received

end SendEk

namespace SendCt

namespace NoHeaderReceived

def newL535–537 ↗#

def new (Au : AuthApi) (authKey : Bytes) : Except StatesPanic (NoHeaderReceived Au) := do
  let auth ← Au.new authKey 1#64
  .ok { epoch := 1#64, auth := auth }

def recv_headerL539–548 ↗#

NoHeaderReceived::recv_header (src/v1/unchunked/send_ct.rs:100–113).

def recv_header {Au : AuthApi} (self : NoHeaderReceived Au)
    (epoch : Epoch) (hdr : Header) (mac : Mac) : StatesResult (HeaderReceived Au) := do
  if epoch != self.epoch then
    .error (.panic (.unchunkedRecvHeaderEpochMismatch epoch self.epoch))
  else
    let verifyRes ← StatesResult.ofPanic (Au.verify_hdr self.auth self.epoch hdr mac)
    match verifyRes with
    | .error _ => .error (.err .macVerifyFailed)
    | .ok () => .ok { epoch := self.epoch, auth := self.auth, hdr := hdr }

def into_pbL550–551 ↗#

def into_pb {Au : AuthApi} (self : NoHeaderReceived Au) : V1State.Unchunked.NoHeaderReceived :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth) }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.NoHeaderReceived.intoPb

def from_pbL555–559 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.NoHeaderReceived) :
    StatesResult (NoHeaderReceived Au) :=
  match pb.auth with
  | none => .error (.err .stateDecode)
  | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.NoHeaderReceived.fromPb

end NoHeaderReceived

namespace HeaderReceived

def send_ct1L567–575 ↗#

HeaderReceived::send_ct1 (src/v1/unchunked/send_ct.rs:120–148).

def send_ct1 (K : MlKem) {Au : AuthApi} (self : HeaderReceived Au) (tape : Bytes) :
    Except StatesPanic (Ct1Sent Au × Ciphertext1 × EpochSecret × Bytes) := do
  let ((ct1, es, secret), tape') ← encaps1 K self.hdr tape
  let info := sckaKeyInfoPrefix ++ u64ToBeBytes self.epoch
  let secret ← Au.hkdf_to_vec (List.replicate 32 0#8) secret info 32
  let auth ← Au.update self.auth self.epoch secret
  .ok ({ epoch := self.epoch, auth := auth, hdr := self.hdr, es := es, ct1 := ct1 },
    ct1, { epoch := self.epoch, secret := secret }, tape')

def into_pbL577–578 ↗#

def into_pb {Au : AuthApi} (self : HeaderReceived Au) : V1State.Unchunked.HeaderReceived :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth), hdr := self.hdr }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.HeaderReceived.intoPb

def from_pbL582–589 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.HeaderReceived) :
    StatesResult (HeaderReceived Au) :=
  if pb.hdr.length == HEADER_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a, hdr := pb.hdr }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.HeaderReceived.fromPb

end HeaderReceived

namespace Ct1Sent

def recv_ekL597–605 ↗#

Ct1Sent::recv_ek (src/v1/unchunked/send_ct.rs:154–171).

def recv_ek (K : MlKem) {Au : AuthApi} (self : Ct1Sent Au)
    (epoch : Epoch) (ek : EncapsulationKey) : StatesResult (Ct1SentEkReceived Au) :=
  if epoch != self.epoch then
    .error (.panic (.unchunkedRecvEkEpochMismatch epoch self.epoch))
  else if ek_matches_header K ek self.hdr then
    .ok { epoch := self.epoch, auth := self.auth, es := self.es, ek := ek, ct1 := self.ct1 }
  else
    .error (.err .erroneousDataReceived)

def into_pbL607–609 ↗#

def into_pb {Au : AuthApi} (self : Ct1Sent Au) : V1State.Unchunked.Ct1Sent :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth),
    hdr := self.hdr, es := self.es, ct1 := self.ct1 }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct1Sent.intoPb

def from_pbL613–622 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.Ct1Sent) : StatesResult (Ct1Sent Au) :=
  if pb.hdr.length == HEADER_SIZE &&
     pb.es.length == ENCAPSULATION_STATE_SIZE &&
     pb.ct1.length == CIPHERTEXT1_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a =>
      .ok { epoch := pb.epoch, auth := Au.from_pb a, hdr := pb.hdr, es := pb.es, ct1 := pb.ct1 }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct1Sent.fromPb

end Ct1Sent

namespace Ct1SentEkReceived

def send_ct2L630–636 ↗#

Ct1SentEkReceived::send_ct2 (src/v1/unchunked/send_ct.rs:177–195).

def send_ct2 (K : MlKem) {Au : AuthApi} (self : Ct1SentEkReceived Au) :
    Except StatesPanic (Ct2Sent Au × Ciphertext2 × Mac) := do
  let ct2 ← encaps2 K self.ek self.es
  let ct1Full := self.ct1 ++ ct2
  let mac ← Au.mac_ct self.auth self.epoch ct1Full
  .ok ({ epoch := self.epoch, auth := self.auth }, ct2, mac)

def into_pbL638–640 ↗#

def into_pb {Au : AuthApi} (self : Ct1SentEkReceived Au) : V1State.Unchunked.Ct1SentEkReceived :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth),
    es := self.es, ek := self.ek, ct1 := self.ct1 }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct1SentEkReceived.intoPb

def from_pbL644–654 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.Ct1SentEkReceived) :
    StatesResult (Ct1SentEkReceived Au) :=
  if pb.es.length == ENCAPSULATION_STATE_SIZE &&
     pb.ct1.length == CIPHERTEXT1_SIZE &&
     pb.ek.length == ENCAPSULATION_KEY_SIZE then
    match pb.auth with
    | none => .error (.err .stateDecode)
    | some a =>
      .ok { epoch := pb.epoch, auth := Au.from_pb a, es := pb.es, ek := pb.ek, ct1 := pb.ct1 }
  else
    .error (.err .stateDecode)

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct1SentEkReceived.fromPb

end Ct1SentEkReceived

namespace Ct2Sent

def recv_next_epochL662–672 ↗#

Ct2Sent::recv_next_epoch (src/v1/unchunked/send_ct.rs:201–208).

def recv_next_epoch {Au : AuthApi} (self : Ct2Sent Au) (nextEpoch : Epoch) :
    Except StatesPanic (SendEk.KeysUnsampled Au) :=
  if self.epoch == BitVec.allOnes 64 then
    .error .unchunkedRecvNextEpochOverflow
  else
    let next := self.epoch + 1#64
    if next != nextEpoch then
      .error (.unchunkedRecvNextEpochMismatch next nextEpoch)
    else
      .ok { epoch := next, auth := self.auth }

def into_pbL674–675 ↗#

def into_pb {Au : AuthApi} (self : Ct2Sent Au) : V1State.Unchunked.Ct2Sent :=
  { epoch := self.epoch, auth := some (Au.into_pb self.auth) }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct2Sent.intoPb

def from_pbL679–682 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Unchunked.Ct2Sent) : StatesResult (Ct2Sent Au) :=
  match pb.auth with
  | none => .error (.err .stateDecode)
  | some a => .ok { epoch := pb.epoch, auth := Au.from_pb a }

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

CryptoVerification.LibsignalSpqrV1.Unchunked.SendCt.Ct2Sent.fromPb

end Ct2Sent

end SendCt

end Unchunked

Chunked braid state machine (src/v1/chunked/{send_ek, send_ct})

def expectEncodeBytesL694–699 ↗#

def expectEncodeBytes (P : PolyApi) (site : String) (msg : Bytes) :
    Except StatesPanic P.PolyEncoder := do
  let res ← P.encode_bytes msg
  match res with
  | .ok enc => .ok enc
  | .error _ => .error (.polyExpectFailed site)

def expectDecoderNewL701–706 ↗#

def expectDecoderNew (P : PolyApi) (site : String) (lenBytes : Nat) :
    Except StatesPanic P.PolyDecoder := do
  let res ← P.decoder_new lenBytes
  match res with
  | .ok dec => .ok dec
  | .error _ => .error (.polyExpectFailed site)

def encoderFromPbStateDecodeL708–716 ↗#

def encoderFromPbStateDecode (P : PolyApi) (pb? : Option PolynomialEncoder) :
    StatesResult P.PolyEncoder :=
  match pb? with
  | none => .error (.err .stateDecode)
  | some pb => do
    let res ← StatesResult.ofPanic (P.encoder_from_pb pb)
    match res with
    | .ok enc => .ok enc
    | .error _ => .error (.err .stateDecode)

def decoderFromPbStateDecodeL718–726 ↗#

def decoderFromPbStateDecode (P : PolyApi) (pb? : Option PolynomialDecoder) :
    StatesResult P.PolyDecoder :=
  match pb? with
  | none => .error (.err .stateDecode)
  | some pb => do
    let res ← StatesResult.ofPanic (P.decoder_from_pb pb)
    match res with
    | .ok dec => .ok dec
    | .error _ => .error (.err .stateDecode)

namespace Chunked

namespace SendCt

structure NoHeaderReceivedL732–735 ↗#

structure NoHeaderReceived (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.NoHeaderReceived Au
  receiving_hdr : P.PolyDecoder
  deriving DecidableEq, Repr

structure HeaderReceivedL737–740 ↗#

structure HeaderReceived (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.HeaderReceived Au
  receiving_ek : P.PolyDecoder
  deriving DecidableEq, Repr

structure Ct1SampledL742–746 ↗#

structure Ct1Sampled (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.Ct1Sent Au
  sending_ct1 : P.PolyEncoder
  receiving_ek : P.PolyDecoder
  deriving DecidableEq, Repr

structure EkReceivedCt1SampledL748–751 ↗#

structure EkReceivedCt1Sampled (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.Ct1SentEkReceived Au
  sending_ct1 : P.PolyEncoder
  deriving DecidableEq, Repr

structure Ct1AcknowledgedL753–756 ↗#

structure Ct1Acknowledged (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.Ct1Sent Au
  receiving_ek : P.PolyDecoder
  deriving DecidableEq, Repr

structure Ct2SampledL758–761 ↗#

structure Ct2Sampled (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendCt.Ct2Sent Au
  sending_ct2 : P.PolyEncoder
  deriving DecidableEq, Repr

end SendCt

namespace SendEk

structure KeysUnsampledL767–769 ↗#

structure KeysUnsampled (Au : AuthApi) where
  uc : Unchunked.SendEk.KeysUnsampled Au
  deriving DecidableEq, Repr

structure KeysSampledL771–774 ↗#

structure KeysSampled (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendEk.HeaderSent Au
  sending_hdr : P.PolyEncoder
  deriving DecidableEq, Repr

structure HeaderSentL776–780 ↗#

structure HeaderSent (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendEk.EkSent Au
  sending_ek : P.PolyEncoder
  receiving_ct1 : P.PolyDecoder
  deriving DecidableEq, Repr

structure Ct1ReceivedL782–785 ↗#

structure Ct1Received (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendEk.EkSentCt1Received Au
  sending_ek : P.PolyEncoder
  deriving DecidableEq, Repr

structure EkSentCt1ReceivedL787–790 ↗#

structure EkSentCt1Received (P : PolyApi) (Au : AuthApi) where
  uc : Unchunked.SendEk.EkSentCt1Received Au
  receiving_ct2 : P.PolyDecoder
  deriving DecidableEq, Repr

inductive HeaderSentRecvChunkL792–795 ↗#

inductive HeaderSentRecvChunk (P : PolyApi) (Au : AuthApi) where
  | stillReceiving (s : HeaderSent P Au)
  | done (s : Ct1Received P Au)
  deriving DecidableEq, Repr

inductive EkSentCt1ReceivedRecvChunkL797–800 ↗#

inductive EkSentCt1ReceivedRecvChunk (P : PolyApi) (Au : AuthApi) where
  | stillReceiving (s : EkSentCt1Received P Au)
  | done (res : SendCt.NoHeaderReceived P Au × EpochSecret)
  deriving DecidableEq, Repr

namespace KeysUnsampled

def newL804–806 ↗#

def new (Au : AuthApi) (authKey : Bytes) : Except StatesPanic (KeysUnsampled Au) := do
  let uc ← Unchunked.SendEk.KeysUnsampled.new Au authKey
  .ok { uc := uc }

def epochL808 ↗#

def epoch {Au : AuthApi} (self : KeysUnsampled Au) : Epoch := self.uc.epoch

def send_hdr_chunkL810–818 ↗#

KeysUnsampled::send_hdr_chunk (src/v1/chunked/send_ek.rs:59–66).

def send_hdr_chunk (K : MlKem) (P : PolyApi) {Au : AuthApi}
    (self : KeysUnsampled Au) (tape : Bytes) :
    Except StatesPanic (KeysSampled P Au × P.Chunk × Bytes) := do
  let (uc, toSend, mac, tape') ← self.uc.send_header K tape
  let toSendFull := toSend ++ mac
  let sendingHdr ← expectEncodeBytes P "v1/chunked/send_ek.rs:63" toSendFull
  let (sendingHdr, chunk) ← P.next_chunk sendingHdr
  .ok ({ uc := uc, sending_hdr := sendingHdr }, chunk, tape')

def into_pbL820–821 ↗#

def into_pb {Au : AuthApi} (self : KeysUnsampled Au) : V1State.Chunked.KeysUnsampled :=
  { uc := some self.uc.into_pb }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.KeysUnsampled.intoPb

def from_pbL825–830 ↗#

def from_pb (Au : AuthApi) (pb : V1State.Chunked.KeysUnsampled) : StatesResult (KeysUnsampled Au) :=
  match pb.uc with
  | none => .error (.err .stateDecode)
  | some u => do
    let uc ← Unchunked.SendEk.KeysUnsampled.from_pb Au u
    .ok { uc := uc }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.KeysUnsampled.fromPb

end KeysUnsampled

namespace KeysSampled

def epochL838 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : KeysSampled P Au) : Epoch := self.uc.epoch

def send_hdr_chunkL840–843 ↗#

def send_hdr_chunk {P : PolyApi} {Au : AuthApi} (self : KeysSampled P Au) :
    Except StatesPanic (KeysSampled P Au × P.Chunk) := do
  let (sendingHdr, chunk) ← P.next_chunk self.sending_hdr
  .ok ({ uc := self.uc, sending_hdr := sendingHdr }, chunk)

def recv_ct1_chunkL845–855 ↗#

KeysSampled::recv_ct1_chunk (src/v1/chunked/send_ek.rs:85–98).

def recv_ct1_chunk {P : PolyApi} {Au : AuthApi} (self : KeysSampled P Au)
    (epoch : Epoch) (chunk : P.Chunk) : Except StatesPanic (HeaderSent P Au) := do
  if epoch != self.uc.epoch then
    .error (.chunkedEpochMismatch "v1/chunked/send_ek.rs:86" epoch self.uc.epoch)
  else
    let receivingCt1 ← expectDecoderNew P "v1/chunked/send_ek.rs:88" CIPHERTEXT1_SIZE
    let receivingCt1 ← P.add_chunk receivingCt1 chunk
    let (uc, ek) := self.uc.send_ek
    let sendingEk ← expectEncodeBytes P "v1/chunked/send_ek.rs:92" ek
    .ok { uc := uc, sending_ek := sendingEk, receiving_ct1 := receivingCt1 }

def into_pbL857–858 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : KeysSampled P Au) : V1State.Chunked.KeysSampled :=
  { uc := some self.uc.into_pb, sendingHdr := some (P.encoder_into_pb self.sending_hdr) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.KeysSampled.intoPb

def from_pbL862–869 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.KeysSampled) :
    StatesResult (KeysSampled P Au) := do
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendEk.HeaderSent.from_pb Au u
  let sendingHdr ← encoderFromPbStateDecode P pb.sendingHdr
  .ok { uc := uc, sending_hdr := sendingHdr }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.KeysSampled.fromPb

end KeysSampled

namespace HeaderSent

def epochL877 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : HeaderSent P Au) : Epoch := self.uc.epoch

def send_ek_chunkL879–882 ↗#

def send_ek_chunk {P : PolyApi} {Au : AuthApi} (self : HeaderSent P Au) :
    Except StatesPanic (HeaderSent P Au × P.Chunk) := do
  let (sendingEk, chunk) ← P.next_chunk self.sending_ek
  .ok ({ uc := self.uc, sending_ek := sendingEk, receiving_ct1 := self.receiving_ct1 }, chunk)

def recv_ct1_chunkL884–898 ↗#

HeaderSent::recv_ct1_chunk (src/v1/chunked/send_ek.rs:131–149).

def recv_ct1_chunk {P : PolyApi} {Au : AuthApi} (self : HeaderSent P Au)
    (epoch : Epoch) (chunk : P.Chunk) : Except StatesPanic (HeaderSentRecvChunk P Au) := do
  if epoch != self.uc.epoch then
    .error (.chunkedEpochMismatch "v1/chunked/send_ek.rs:132" epoch self.uc.epoch)
  else
    let receivingCt1 ← P.add_chunk self.receiving_ct1 chunk
    let decoded? ← P.decoded_message receivingCt1
    match decoded? with
    | some decoded =>
      let uc ← self.uc.recv_ct1 epoch decoded
      .ok (.done { uc := uc, sending_ek := self.sending_ek })
    | none =>
      .ok (.stillReceiving
        { uc := self.uc, sending_ek := self.sending_ek, receiving_ct1 := receivingCt1 })

def into_pbL900–903 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : HeaderSent P Au) : V1State.Chunked.HeaderSent :=
  { uc := some self.uc.into_pb,
    sendingEk := some (P.encoder_into_pb self.sending_ek),
    receivingCt1 := some (P.decoder_into_pb self.receiving_ct1) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.HeaderSent.intoPb

def from_pbL907–924 ↗#

HeaderSent::from_pb (src/v1/chunked/send_ek/serialize.rs:52–67; returns MsgDecode if receiving_ct1.pts_needed != 480).

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.HeaderSent) :
    StatesResult (HeaderSent P Au) := do
  match pb.receivingCt1 with
  | some d =>
    if d.ptsNeeded.toNat != CIPHERTEXT1_SIZE / 2 then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendEk.EkSent.from_pb Au u
  let sendingEk ← encoderFromPbStateDecode P pb.sendingEk
  let receivingCt1 ← decoderFromPbStateDecode P pb.receivingCt1
  .ok { uc := uc, sending_ek := sendingEk, receiving_ct1 := receivingCt1 }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.HeaderSent.fromPb

end HeaderSent

namespace Ct1Received

def epochL932 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : Ct1Received P Au) : Epoch := self.uc.epoch

def send_ek_chunkL934–937 ↗#

def send_ek_chunk {P : PolyApi} {Au : AuthApi} (self : Ct1Received P Au) :
    Except StatesPanic (Ct1Received P Au × P.Chunk) := do
  let (sendingEk, chunk) ← P.next_chunk self.sending_ek
  .ok ({ uc := self.uc, sending_ek := sendingEk }, chunk)

def recv_ct2_chunkL939–948 ↗#

Ct1Received::recv_ct2_chunk (src/v1/chunked/send_ek.rs:165–180).

def recv_ct2_chunk {P : PolyApi} {Au : AuthApi} (self : Ct1Received P Au)
    (epoch : Epoch) (chunk : P.Chunk) : Except StatesPanic (EkSentCt1Received P Au) := do
  if epoch != self.uc.epoch then
    .error (.chunkedEpochMismatch "v1/chunked/send_ek.rs:166" epoch self.uc.epoch)
  else
    let receivingCt2 ←
      expectDecoderNew P "v1/chunked/send_ek.rs:174" (CIPHERTEXT2_SIZE + AUTHENTICATOR_MACSIZE)
    let receivingCt2 ← P.add_chunk receivingCt2 chunk
    .ok { uc := self.uc, receiving_ct2 := receivingCt2 }

def into_pbL950–951 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : Ct1Received P Au) : V1State.Chunked.Ct1Received :=
  { uc := some self.uc.into_pb, sendingEk := some (P.encoder_into_pb self.sending_ek) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.Ct1Received.intoPb

def from_pbL955–962 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.Ct1Received) :
    StatesResult (Ct1Received P Au) := do
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendEk.EkSentCt1Received.from_pb Au u
  let sendingEk ← encoderFromPbStateDecode P pb.sendingEk
  .ok { uc := uc, sending_ek := sendingEk }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.Ct1Received.fromPb

end Ct1Received

namespace EkSentCt1Received

def epochL970 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : EkSentCt1Received P Au) : Epoch := self.uc.epoch

def recv_ct2_chunkL972–992 ↗#

EkSentCt1Received::recv_ct2_chunk (src/v1/chunked/send_ek.rs:195–227).

def recv_ct2_chunk (K : MlKem) {P : PolyApi} {Au : AuthApi} (self : EkSentCt1Received P Au)
    (epoch : Epoch) (chunk : P.Chunk) : StatesResult (EkSentCt1ReceivedRecvChunk P Au) := do
  if epoch != self.uc.epoch then
    .error (.panic (.chunkedEpochMismatch "v1/chunked/send_ek.rs:200" epoch self.uc.epoch))
  else
    let receivingCt2 ← StatesResult.ofPanic (P.add_chunk self.receiving_ct2 chunk)
    let decoded? ← StatesResult.ofPanic (P.decoded_message receivingCt2)
    match decoded? with
    | some ct2Full =>
      if ct2Full.length < CIPHERTEXT2_SIZE then
        .error (.panic (.decodedSliceBounds "v1/chunked/send_ek.rs:209" ct2Full.length CIPHERTEXT2_SIZE))
      else
        let mac := ct2Full.drop CIPHERTEXT2_SIZE
        let ct2 := ct2Full.take CIPHERTEXT2_SIZE
        let (uc, sec) ← self.uc.recv_ct2 K ct2 mac
        let receivingHdr ← StatesResult.ofPanic
          (expectDecoderNew P "v1/chunked/send_ek.rs:218" (HEADER_SIZE + AUTHENTICATOR_MACSIZE))
        .ok (.done ({ uc := uc, receiving_hdr := receivingHdr }, sec))
    | none =>
      .ok (.stillReceiving { uc := self.uc, receiving_ct2 := receivingCt2 })

def into_pbL994–996 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : EkSentCt1Received P Au) :
    V1State.Chunked.EkSentCt1Received :=
  { uc := some self.uc.into_pb, receivingCt2 := some (P.decoder_into_pb self.receiving_ct2) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.EkSentCt1Received.intoPb

def from_pbL1000–1016 ↗#

EkSentCt1Received::from_pb (src/v1/chunked/send_ek/serialize.rs:95–111; returns MsgDecode if receiving_ct2.pts_needed != 80).

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.EkSentCt1Received) :
    StatesResult (EkSentCt1Received P Au) := do
  match pb.receivingCt2 with
  | some d =>
    if d.ptsNeeded.toNat != (CIPHERTEXT2_SIZE + AUTHENTICATOR_MACSIZE) / 2 then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendEk.EkSentCt1Received.from_pb Au u
  let receivingCt2 ← decoderFromPbStateDecode P pb.receivingCt2
  .ok { uc := uc, receiving_ct2 := receivingCt2 }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendEk.EkSentCt1Received.fromPb

end EkSentCt1Received

end SendEk

namespace SendCt

inductive NoHeaderReceivedRecvChunkL1026–1029 ↗#

inductive NoHeaderReceivedRecvChunk (P : PolyApi) (Au : AuthApi) where
  | stillReceiving (s : NoHeaderReceived P Au)
  | done (s : HeaderReceived P Au)
  deriving DecidableEq, Repr

inductive Ct1SampledRecvChunkL1031–1036 ↗#

inductive Ct1SampledRecvChunk (P : PolyApi) (Au : AuthApi) where
  | stillReceivingStillSending (s : Ct1Sampled P Au)
  | stillReceiving (s : Ct1Acknowledged P Au)
  | stillSending (s : EkReceivedCt1Sampled P Au)
  | done (s : Ct2Sampled P Au)
  deriving DecidableEq, Repr

inductive Ct1AcknowledgedRecvChunkL1038–1041 ↗#

inductive Ct1AcknowledgedRecvChunk (P : PolyApi) (Au : AuthApi) where
  | stillReceiving (s : Ct1Acknowledged P Au)
  | done (s : Ct2Sampled P Au)
  deriving DecidableEq, Repr

def send_ct2_encoderL1043–1044 ↗#

def send_ct2_encoder (P : PolyApi) (ct2 mac : Bytes) : Except StatesPanic P.PolyEncoder :=
  expectEncodeBytes P "v1/chunked/send_ct.rs:162" (ct2 ++ mac)

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.sendCt2Encoder

namespace NoHeaderReceived

def newL1050–1058 ↗#

NoHeaderReceived::new (src/v1/chunked/send_ct.rs:71–79), preserving Rust evaluation order: PolyDecoder::new, unchunked::NoHeaderReceived::new, then decoder.expect(...).

def new (P : PolyApi) (Au : AuthApi) (authKey : Bytes) :
    Except StatesPanic (NoHeaderReceived P Au) := do
  let decoderRes ← P.decoder_new (HEADER_SIZE + AUTHENTICATOR_MACSIZE)
  let uc ← Unchunked.SendCt.NoHeaderReceived.new Au authKey
  match decoderRes with
  | .ok decoder => .ok { uc := uc, receiving_hdr := decoder }
  | .error _ => .error (.polyExpectFailed "v1/chunked/send_ct.rs:77")

def epochL1060 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : NoHeaderReceived P Au) : Epoch := self.uc.epoch

def recv_hdr_chunkL1062–1085 ↗#

NoHeaderReceived::recv_hdr_chunk (src/v1/chunked/send_ct.rs:82–110).

def recv_hdr_chunk {P : PolyApi} {Au : AuthApi} (self : NoHeaderReceived P Au)
    (epoch : Epoch) (chunk : P.Chunk) : StatesResult (NoHeaderReceivedRecvChunk P Au) := do
  if epoch != self.uc.epoch then
    .error (.panic (.chunkedEpochMismatch "v1/chunked/send_ct.rs:87" epoch self.uc.epoch))
  else
    let receivingHdr ← StatesResult.ofPanic (P.add_chunk self.receiving_hdr chunk)
    let decoded? ← StatesResult.ofPanic (P.decoded_message receivingHdr)
    match decoded? with
    | some hdrFull =>
      if hdrFull.length < HEADER_SIZE then
        .error (.panic (.decodedSliceBounds "v1/chunked/send_ct.rs:96" hdrFull.length HEADER_SIZE))
      else
        let mac := hdrFull.drop HEADER_SIZE
        let hdr := hdrFull.take HEADER_SIZE
        let receivingEkRes ← StatesResult.ofPanic (P.decoder_new ENCAPSULATION_KEY_SIZE)
        let uc ← self.uc.recv_header epoch hdr mac
        match receivingEkRes with
        | .ok receivingEk =>
          .ok (.done { uc := uc, receiving_ek := receivingEk })
        | .error _ =>
          .error (.panic (.polyExpectFailed "v1/chunked/send_ct.rs:102"))
    | none =>
      .ok (.stillReceiving { uc := self.uc, receiving_hdr := receivingHdr })

def into_pbL1087–1089 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : NoHeaderReceived P Au) :
    V1State.Chunked.NoHeaderReceived :=
  { uc := some self.uc.into_pb, receivingHdr := some (P.decoder_into_pb self.receiving_hdr) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.NoHeaderReceived.intoPb

def from_pbL1093–1107 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.NoHeaderReceived) :
    StatesResult (NoHeaderReceived P Au) := do
  match pb.receivingHdr with
  | some rhdr =>
    if rhdr.ptsNeeded != BitVec.ofNat 32 ((HEADER_SIZE + AUTHENTICATOR_MACSIZE) / 2) then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.NoHeaderReceived.from_pb Au u
  let receivingHdr ← decoderFromPbStateDecode P pb.receivingHdr
  .ok { uc := uc, receiving_hdr := receivingHdr }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.NoHeaderReceived.fromPb

end NoHeaderReceived

namespace HeaderReceived

def epochL1115 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : HeaderReceived P Au) : Epoch := self.uc.epoch

def send_ct1_chunkL1117–1125 ↗#

HeaderReceived::send_ct1_chunk (src/v1/chunked/send_ct.rs:123–142).

def send_ct1_chunk (K : MlKem) {P : PolyApi} {Au : AuthApi}
    (self : HeaderReceived P Au) (tape : Bytes) :
    Except StatesPanic (Ct1Sampled P Au × P.Chunk × EpochSecret × Bytes) := do
  let (uc, ct1, epochSecret, tape') ← self.uc.send_ct1 K tape
  let sendingCt1 ← expectEncodeBytes P "v1/chunked/send_ct.rs:131" ct1
  let (sendingCt1, chunk) ← P.next_chunk sendingCt1
  .ok ({ uc := uc, sending_ct1 := sendingCt1, receiving_ek := self.receiving_ek },
    chunk, epochSecret, tape')

def into_pbL1127–1129 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : HeaderReceived P Au) :
    V1State.Chunked.HeaderReceived :=
  { uc := some self.uc.into_pb, receivingEk := some (P.decoder_into_pb self.receiving_ek) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.HeaderReceived.intoPb

def from_pbL1133–1147 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.HeaderReceived) :
    StatesResult (HeaderReceived P Au) := do
  match pb.receivingEk with
  | some d =>
    if d.ptsNeeded.toNat != ENCAPSULATION_KEY_SIZE / 2 then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.HeaderReceived.from_pb Au u
  let receivingEk ← decoderFromPbStateDecode P pb.receivingEk
  .ok { uc := uc, receiving_ek := receivingEk }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.HeaderReceived.fromPb

end HeaderReceived

namespace Ct1Sampled

def epochL1155 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : Ct1Sampled P Au) : Epoch := self.uc.epoch

def recv_ek_chunkL1157–1177 ↗#

Ct1Sampled::recv_ek_chunk (src/v1/chunked/send_ct.rs:168–200; no chunk-level epoch assert).

def recv_ek_chunk (K : MlKem) {P : PolyApi} {Au : AuthApi} (self : Ct1Sampled P Au)
    (epoch : Epoch) (chunk : P.Chunk) (ct1Ack : Bool) :
    StatesResult (Ct1SampledRecvChunk P Au) := do
  let receivingEk ← StatesResult.ofPanic (P.add_chunk self.receiving_ek chunk)
  let decoded? ← StatesResult.ofPanic (P.decoded_message receivingEk)
  match decoded? with
  | some decoded =>
    let uc ← self.uc.recv_ek K epoch decoded
    if ct1Ack then
      let (uc, ct2, mac) ← StatesResult.ofPanic (uc.send_ct2 K)
      let sendingCt2 ← StatesResult.ofPanic (send_ct2_encoder P ct2 mac)
      .ok (.done { uc := uc, sending_ct2 := sendingCt2 })
    else
      .ok (.stillSending { uc := uc, sending_ct1 := self.sending_ct1 })
  | none =>
    if ct1Ack then
      .ok (.stillReceiving { uc := self.uc, receiving_ek := receivingEk })
    else
      .ok (.stillReceivingStillSending
        { uc := self.uc, sending_ct1 := self.sending_ct1, receiving_ek := receivingEk })

def send_ct1_chunkL1179–1182 ↗#

def send_ct1_chunk {P : PolyApi} {Au : AuthApi} (self : Ct1Sampled P Au) :
    Except StatesPanic (Ct1Sampled P Au × P.Chunk) := do
  let (sendingCt1, chunk) ← P.next_chunk self.sending_ct1
  .ok ({ uc := self.uc, sending_ct1 := sendingCt1, receiving_ek := self.receiving_ek }, chunk)

def into_pbL1184–1187 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : Ct1Sampled P Au) : V1State.Chunked.Ct1Sampled :=
  { uc := some self.uc.into_pb,
    sendingCt1 := some (P.encoder_into_pb self.sending_ct1),
    receivingEk := some (P.decoder_into_pb self.receiving_ek) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct1Sampled.intoPb

def from_pbL1191–1206 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.Ct1Sampled) :
    StatesResult (Ct1Sampled P Au) := do
  match pb.receivingEk with
  | some d =>
    if d.ptsNeeded.toNat != ENCAPSULATION_KEY_SIZE / 2 then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.Ct1Sent.from_pb Au u
  let sendingCt1 ← encoderFromPbStateDecode P pb.sendingCt1
  let receivingEk ← decoderFromPbStateDecode P pb.receivingEk
  .ok { uc := uc, sending_ct1 := sendingCt1, receiving_ek := receivingEk }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct1Sampled.fromPb

end Ct1Sampled

namespace EkReceivedCt1Sampled

def epochL1214 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : EkReceivedCt1Sampled P Au) : Epoch := self.uc.epoch

def send_ct1_chunkL1216–1219 ↗#

def send_ct1_chunk {P : PolyApi} {Au : AuthApi} (self : EkReceivedCt1Sampled P Au) :
    Except StatesPanic (EkReceivedCt1Sampled P Au × P.Chunk) := do
  let (sendingCt1, chunk) ← P.next_chunk self.sending_ct1
  .ok ({ uc := self.uc, sending_ct1 := sendingCt1 }, chunk)

def recv_ct1_ackL1221–1230 ↗#

EkReceivedCt1Sampled::recv_ct1_ack (src/v1/chunked/send_ct.rs:236–243).

def recv_ct1_ack (K : MlKem) {P : PolyApi} {Au : AuthApi}
    (self : EkReceivedCt1Sampled P Au) (epoch : Epoch) :
    Except StatesPanic (Ct2Sampled P Au) := do
  if epoch != self.uc.epoch then
    .error (.chunkedEpochMismatch "v1/chunked/send_ct.rs:237" epoch self.uc.epoch)
  else
    let (uc, ct2, mac) ← self.uc.send_ct2 K
    let sendingCt2 ← send_ct2_encoder P ct2 mac
    .ok { uc := uc, sending_ct2 := sendingCt2 }

def into_pbL1232–1234 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : EkReceivedCt1Sampled P Au) :
    V1State.Chunked.EkReceivedCt1Sampled :=
  { uc := some self.uc.into_pb, sendingCt1 := some (P.encoder_into_pb self.sending_ct1) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.EkReceivedCt1Sampled.intoPb

def from_pbL1238–1245 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.EkReceivedCt1Sampled) :
    StatesResult (EkReceivedCt1Sampled P Au) := do
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.Ct1SentEkReceived.from_pb Au u
  let sendingCt1 ← encoderFromPbStateDecode P pb.sendingCt1
  .ok { uc := uc, sending_ct1 := sendingCt1 }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.EkReceivedCt1Sampled.fromPb

end EkReceivedCt1Sampled

namespace Ct1Acknowledged

def epochL1253 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : Ct1Acknowledged P Au) : Epoch := self.uc.epoch

def recv_ek_chunkL1255–1267 ↗#

Ct1Acknowledged::recv_ek_chunk (src/v1/chunked/send_ct.rs:259–279; no chunk-level epoch assert).

def recv_ek_chunk (K : MlKem) {P : PolyApi} {Au : AuthApi} (self : Ct1Acknowledged P Au)
    (epoch : Epoch) (chunk : P.Chunk) : StatesResult (Ct1AcknowledgedRecvChunk P Au) := do
  let receivingEk ← StatesResult.ofPanic (P.add_chunk self.receiving_ek chunk)
  let decoded? ← StatesResult.ofPanic (P.decoded_message receivingEk)
  match decoded? with
  | some decoded =>
    let uc ← self.uc.recv_ek K epoch decoded
    let (uc, ct2, mac) ← StatesResult.ofPanic (uc.send_ct2 K)
    let sendingCt2 ← StatesResult.ofPanic (send_ct2_encoder P ct2 mac)
    .ok (.done { uc := uc, sending_ct2 := sendingCt2 })
  | none =>
    .ok (.stillReceiving { uc := self.uc, receiving_ek := receivingEk })

def into_pbL1269–1271 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : Ct1Acknowledged P Au) :
    V1State.Chunked.Ct1Acknowledged :=
  { uc := some self.uc.into_pb, receivingEk := some (P.decoder_into_pb self.receiving_ek) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct1Acknowledged.intoPb

def from_pbL1275–1289 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.Ct1Acknowledged) :
    StatesResult (Ct1Acknowledged P Au) := do
  match pb.receivingEk with
  | some d =>
    if d.ptsNeeded.toNat != ENCAPSULATION_KEY_SIZE / 2 then
      .error (.err .msgDecode)
    else
      .ok ()
  | none => .ok ()
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.Ct1Sent.from_pb Au u
  let receivingEk ← decoderFromPbStateDecode P pb.receivingEk
  .ok { uc := uc, receiving_ek := receivingEk }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct1Acknowledged.fromPb

end Ct1Acknowledged

namespace Ct2Sampled

def epochL1297 ↗#

def epoch {P : PolyApi} {Au : AuthApi} (self : Ct2Sampled P Au) : Epoch := self.uc.epoch

def send_ct2_chunkL1299–1302 ↗#

def send_ct2_chunk {P : PolyApi} {Au : AuthApi} (self : Ct2Sampled P Au) :
    Except StatesPanic (Ct2Sampled P Au × P.Chunk) := do
  let (sendingCt2, chunk) ← P.next_chunk self.sending_ct2
  .ok ({ uc := self.uc, sending_ct2 := sendingCt2 }, chunk)

def recv_next_epochL1304–1307 ↗#

def recv_next_epoch {P : PolyApi} {Au : AuthApi} (self : Ct2Sampled P Au) (epoch : Epoch) :
    Except StatesPanic (SendEk.KeysUnsampled Au) := do
  let uc ← self.uc.recv_next_epoch epoch
  .ok { uc := uc }

def into_pbL1309–1310 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : Ct2Sampled P Au) : V1State.Chunked.Ct2Sampled :=
  { uc := some self.uc.into_pb, sendingCt2 := some (P.encoder_into_pb self.sending_ct2) }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct2Sampled.intoPb

def from_pbL1314–1321 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State.Chunked.Ct2Sampled) :
    StatesResult (Ct2Sampled P Au) := do
  let u ← match pb.uc with
    | none => .error (.err .stateDecode)
    | some u => .ok u
  let uc ← Unchunked.SendCt.Ct2Sent.from_pb Au u
  let sendingCt2 ← encoderFromPbStateDecode P pb.sendingCt2
  .ok { uc := uc, sending_ct2 := sendingCt2 }

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

CryptoVerification.LibsignalSpqrV1.Chunked.SendCt.Ct2Sampled.fromPb

end Ct2Sampled

end SendCt

end Chunked

Top-level States and Message (src/v1/chunked/states.rs)

inductive MessagePayloadL1333–1342 ↗#

SCKA message payload (pub enum MessagePayload, src/v1/chunked/states.rs:31–39).

inductive MessagePayload (P : PolyApi) where
  | none
  | hdr (c : P.Chunk)
  | ek (c : P.Chunk)
  | ekCt1Ack (c : P.Chunk)
  | ct1Ack (b : Bool)
  | ct1 (c : P.Chunk)
  | ct2 (c : P.Chunk)
  deriving DecidableEq, Repr, Inhabited

structure MessageL1344–1348 ↗#

SCKA message (pub struct Message, src/v1/chunked/states.rs:41–44).

structure Message (P : PolyApi) where
  epoch : Epoch
  payload : MessagePayload P
  deriving DecidableEq, Repr, Inhabited

inductive MessageTypeL1350–1359 ↗#

One-byte wire tag of MessagePayload (enum MessageType, src/v1/chunked/states/serialize.rs:95–103).

inductive MessageType where
  | none
  | hdr
  | ek
  | ekCt1Ack
  | ct1Ack
  | ct1
  | ct2
  deriving DecidableEq, Repr, Inhabited

namespace MessageType

def toU8L1363–1370 ↗#

def toU8 : MessageType → BitVec 8
  | .none => 0#8
  | .hdr => 1#8
  | .ek => 2#8
  | .ekCt1Ack => 3#8
  | .ct1Ack => 4#8
  | .ct1 => 5#8
  | .ct2 => 6#8

def tryFromU8L1372–1380 ↗#

def tryFromU8 (v : BitVec 8) : Option MessageType :=
  if v == 0#8 then some .none
  else if v == 1#8 then some .hdr
  else if v == 2#8 then some .ek
  else if v == 3#8 then some .ekCt1Ack
  else if v == 4#8 then some .ct1Ack
  else if v == 5#8 then some .ct1
  else if v == 6#8 then some .ct2
  else Option.none

def from_payloadL1382–1389 ↗#

def from_payload {P : PolyApi} : MessagePayload P → MessageType
  | .none => .none
  | .hdr _ => .hdr
  | .ek _ => .ek
  | .ekCt1Ack _ => .ekCt1Ack
  | .ct1Ack _ => .ct1Ack
  | .ct1 _ => .ct1
  | .ct2 _ => .ct2

end MessageType

def encode_chunkL1393–1394 ↗#

def encode_chunk {P : PolyApi} (c : P.Chunk) (into : SerializedMessage := []) : SerializedMessage :=
  encode_varint ((P.chunkIndex c).zeroExtend 64) into ++ (P.chunkData c).toList

def decode_chunkL1396–1403 ↗#

def decode_chunk (P : PolyApi) (fromSlice : Bytes) : Except Error (P.Chunk × Bytes) := do
  let (index, rest) ← decode_varint fromSlice
  if rest.length < 32 || index.toNat > 65535 then
    .error .msgDecode
  else
    match bytesToVector? 32 (rest.take 32) with
    | some dataVec => .ok (P.mkChunk (index.truncate 16) dataVec, rest.drop 32)
    | none => .error .msgDecode

namespace Message

def serializeL1407–1417 ↗#

Message::serialize (src/v1/chunked/states/serialize.rs:172–197).

def serialize {P : PolyApi} (self : Message P) (index : BitVec 32) : SerializedMessage :=
  let into : SerializedMessage := [1#8]
  let into := encode_varint self.epoch into
  let into := encode_varint (index.zeroExtend 64) into
  let into := into ++ [(MessageType.from_payload self.payload).toU8]
  match self.payload with
  | .hdr chunk | .ek chunk | .ekCt1Ack chunk | .ct1 chunk | .ct2 chunk =>
    encode_chunk chunk into
  | .none | .ct1Ack _ =>
    into

def deserializeL1419–1445 ↗#

Message::deserialize (src/v1/chunked/states/serialize.rs:200–219).

def deserialize (P : PolyApi) (epoch : Epoch) (fromBytes : Bytes) : Except Error (Message P) :=
  match fromBytes with
  | [] => .error .msgDecode
  | b0 :: rest =>
    match MessageType.tryFromU8 b0 with
    | Option.none => .error .msgDecode
    | some msgType => do
      let payload ← match msgType with
        | .none => .ok MessagePayload.none
        | .ct1Ack => .ok (MessagePayload.ct1Ack true)
        | .hdr => do
          let (c, _) ← decode_chunk P rest
          .ok (MessagePayload.hdr c)
        | .ek => do
          let (c, _) ← decode_chunk P rest
          .ok (MessagePayload.ek c)
        | .ekCt1Ack => do
          let (c, _) ← decode_chunk P rest
          .ok (MessagePayload.ekCt1Ack c)
        | .ct1 => do
          let (c, _) ← decode_chunk P rest
          .ok (MessagePayload.ct1 c)
        | .ct2 => do
          let (c, _) ← decode_chunk P rest
          .ok (MessagePayload.ct2 c)
      .ok { epoch := epoch, payload := payload }

end Message

inductive StatesL1449–1462 ↗#

Top-level 11-variant SPQR V1 SCKA state (pub enum States, src/v1/chunked/states.rs:16–29).

inductive States (P : PolyApi) (Au : AuthApi) where
  | keysUnsampled (s : Chunked.SendEk.KeysUnsampled Au)
  | keysSampled (s : Chunked.SendEk.KeysSampled P Au)
  | headerSent (s : Chunked.SendEk.HeaderSent P Au)
  | ct1Received (s : Chunked.SendEk.Ct1Received P Au)
  | ekSentCt1Received (s : Chunked.SendEk.EkSentCt1Received P Au)
  | noHeaderReceived (s : Chunked.SendCt.NoHeaderReceived P Au)
  | headerReceived (s : Chunked.SendCt.HeaderReceived P Au)
  | ct1Sampled (s : Chunked.SendCt.Ct1Sampled P Au)
  | ekReceivedCt1Sampled (s : Chunked.SendCt.EkReceivedCt1Sampled P Au)
  | ct1Acknowledged (s : Chunked.SendCt.Ct1Acknowledged P Au)
  | ct2Sampled (s : Chunked.SendCt.Ct2Sampled P Au)
  deriving DecidableEq, Repr

structure V1SendL1464–1469 ↗#

Output of States.send (pub struct Send, src/v1/chunked/states.rs:46–50).

structure V1Send (P : PolyApi) (Au : AuthApi) where
  msg : Message P
  key : Option EpochSecret
  state : States P Au
  deriving DecidableEq, Repr

structure V1RecvL1471–1475 ↗#

Output of States.recv (pub struct Recv, src/v1/chunked/states.rs:52–55).

structure V1Recv (P : PolyApi) (Au : AuthApi) where
  key : Option EpochSecret
  state : States P Au
  deriving DecidableEq, Repr

namespace States

def init_aL1479–1483 ↗#

Initial send_ek state (States::init_a, src/v1/chunked/states.rs:58–60).

def init_a (P : PolyApi) (Au : AuthApi) (authKey : Bytes) :
    Except StatesPanic (States P Au) := do
  let s ← Chunked.SendEk.KeysUnsampled.new Au authKey
  .ok (.keysUnsampled s)

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

CryptoVerification.LibsignalSpqrV1.States.initA

def init_bL1487–1491 ↗#

Initial send_ct state (States::init_b, src/v1/chunked/states.rs:62–64).

def init_b (P : PolyApi) (Au : AuthApi) (authKey : Bytes) :
    Except StatesPanic (States P Au) := do
  let s ← Chunked.SendCt.NoHeaderReceived.new P Au authKey
  .ok (.noHeaderReceived s)

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

CryptoVerification.LibsignalSpqrV1.States.initB

def epochL1495–1506 ↗#

def epoch {P : PolyApi} {Au : AuthApi} : States P Au → Epoch
  | .keysUnsampled s => s.epoch
  | .keysSampled s => s.epoch
  | .headerSent s => s.epoch
  | .ct1Received s => s.epoch
  | .ekSentCt1Received s => s.epoch
  | .noHeaderReceived s => s.epoch
  | .headerReceived s => s.epoch
  | .ct1Sampled s => s.epoch
  | .ekReceivedCt1Sampled s => s.epoch
  | .ct1Acknowledged s => s.epoch
  | .ct2Sampled s => s.epoch

def into_pbL1508–1520 ↗#

def into_pb {P : PolyApi} {Au : AuthApi} (self : States P Au) : V1State :=
  { innerState := some <| match self with
      | .keysUnsampled s => .keysUnsampled s.into_pb
      | .keysSampled s => .keysSampled s.into_pb
      | .headerSent s => .headerSent s.into_pb
      | .ct1Received s => .ct1Received s.into_pb
      | .ekSentCt1Received s => .ekSentCt1Received s.into_pb
      | .noHeaderReceived s => .noHeaderReceived s.into_pb
      | .headerReceived s => .headerReceived s.into_pb
      | .ct1Sampled s => .ct1Sampled s.into_pb
      | .ekReceivedCt1Sampled s => .ekReceivedCt1Sampled s.into_pb
      | .ct1Acknowledged s => .ct1Acknowledged s.into_pb
      | .ct2Sampled s => .ct2Sampled s.into_pb }

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

CryptoVerification.LibsignalSpqrV1.States.intoPb

def from_pbL1524–1542 ↗#

def from_pb (P : PolyApi) (Au : AuthApi) (pb : V1State) : StatesResult (States P Au) :=
  match pb.innerState with
  | none => .error (.err .stateDecode)
  | some (.keysUnsampled s) => .keysUnsampled <$> Chunked.SendEk.KeysUnsampled.from_pb Au s
  | some (.keysSampled s) => .keysSampled <$> Chunked.SendEk.KeysSampled.from_pb P Au s
  | some (.headerSent s) => .headerSent <$> Chunked.SendEk.HeaderSent.from_pb P Au s
  | some (.ct1Received s) => .ct1Received <$> Chunked.SendEk.Ct1Received.from_pb P Au s
  | some (.ekSentCt1Received s) =>
    .ekSentCt1Received <$> Chunked.SendEk.EkSentCt1Received.from_pb P Au s
  | some (.noHeaderReceived s) =>
    .noHeaderReceived <$> Chunked.SendCt.NoHeaderReceived.from_pb P Au s
  | some (.headerReceived s) =>
    .headerReceived <$> Chunked.SendCt.HeaderReceived.from_pb P Au s
  | some (.ct1Sampled s) => .ct1Sampled <$> Chunked.SendCt.Ct1Sampled.from_pb P Au s
  | some (.ekReceivedCt1Sampled s) =>
    .ekReceivedCt1Sampled <$> Chunked.SendCt.EkReceivedCt1Sampled.from_pb P Au s
  | some (.ct1Acknowledged s) =>
    .ct1Acknowledged <$> Chunked.SendCt.Ct1Acknowledged.from_pb P Au s
  | some (.ct2Sampled s) => .ct2Sampled <$> Chunked.SendCt.Ct2Sampled.from_pb P Au s

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

CryptoVerification.LibsignalSpqrV1.States.fromPb

def sendL1546–1612 ↗#

States::send (src/v1/chunked/states.rs:115–273), threading the RNG tape.

def send (K : MlKem) {P : PolyApi} {Au : AuthApi} (self : States P Au) (tape : Bytes) :
    StatesResult (V1Send P Au × Bytes) :=
  match self with
  | .keysUnsampled state => do
    let epoch := state.epoch
    let (state', chunk, tape') ← StatesResult.ofPanic (state.send_hdr_chunk K P tape)
    .ok ({ state := .keysSampled state',
           msg := { epoch := epoch, payload := .hdr chunk },
           key := none }, tape')
  | .keysSampled state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_hdr_chunk
    .ok ({ state := .keysSampled state',
           msg := { epoch := epoch, payload := .hdr chunk },
           key := none }, tape)
  | .headerSent state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_ek_chunk
    .ok ({ state := .headerSent state',
           msg := { epoch := epoch, payload := .ek chunk },
           key := none }, tape)
  | .ct1Received state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_ek_chunk
    .ok ({ state := .ct1Received state',
           msg := { epoch := epoch, payload := .ekCt1Ack chunk },
           key := none }, tape)
  | .ekSentCt1Received state =>
    let epoch := state.epoch
    .ok ({ state := .ekSentCt1Received state,
           msg := { epoch := epoch, payload := .ct1Ack true },
           key := none }, tape)
  | .noHeaderReceived state =>
    let epoch := state.epoch
    .ok ({ state := .noHeaderReceived state,
           msg := { epoch := epoch, payload := .none },
           key := none }, tape)
  | .headerReceived state => do
    let epoch := state.epoch
    let (state', chunk, epochSecret, tape') ← StatesResult.ofPanic (state.send_ct1_chunk K tape)
    .ok ({ state := .ct1Sampled state',
           msg := { epoch := epoch, payload := .ct1 chunk },
           key := some epochSecret }, tape')
  | .ct1Sampled state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_ct1_chunk
    .ok ({ state := .ct1Sampled state',
           msg := { epoch := epoch, payload := .ct1 chunk },
           key := none }, tape)
  | .ekReceivedCt1Sampled state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_ct1_chunk
    .ok ({ state := .ekReceivedCt1Sampled state',
           msg := { epoch := epoch, payload := .ct1 chunk },
           key := none }, tape)
  | .ct1Acknowledged state =>
    let epoch := state.epoch
    .ok ({ state := .ct1Acknowledged state,
           msg := { epoch := epoch, payload := .none },
           key := none }, tape)
  | .ct2Sampled state => do
    let epoch := state.epoch
    let (state', chunk) ← StatesResult.ofPanic state.send_ct2_chunk
    .ok ({ state := .ct2Sampled state',
           msg := { epoch := epoch, payload := .ct2 chunk },
           key := none }, tape)

def recvL1614–1749 ↗#

States::recv (src/v1/chunked/states.rs:275–533).

def recv (K : MlKem) {P : PolyApi} {Au : AuthApi} (self : States P Au) (msg : Message P) :
    StatesResult (V1Recv P Au) :=
  match self with
  | .keysUnsampled state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else
      .ok { key := none, state := .keysUnsampled state }
  | .keysSampled state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .keysSampled state }
    else
      match msg.payload with
      | .ct1 chunk => do
        let s' ← StatesResult.ofPanic (state.recv_ct1_chunk msg.epoch chunk)
        .ok { key := none, state := .headerSent s' }
      | _ => .ok { key := none, state := .keysSampled state }
  | .headerSent state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .headerSent state }
    else
      match msg.payload with
      | .ct1 chunk => do
        let res ← StatesResult.ofPanic (state.recv_ct1_chunk msg.epoch chunk)
        match res with
        | .stillReceiving s' => .ok { key := none, state := .headerSent s' }
        | .done s' => .ok { key := none, state := .ct1Received s' }
      | _ => .ok { key := none, state := .headerSent state }
  | .ct1Received state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .ct1Received state }
    else
      match msg.payload with
      | .ct2 chunk => do
        let s' ← StatesResult.ofPanic (state.recv_ct2_chunk msg.epoch chunk)
        .ok { key := none, state := .ekSentCt1Received s' }
      | _ => .ok { key := none, state := .ct1Received state }
  | .ekSentCt1Received state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .ekSentCt1Received state }
    else
      match msg.payload with
      | .ct2 chunk => do
        let res ← state.recv_ct2_chunk K msg.epoch chunk
        match res with
        | .stillReceiving s' => .ok { key := none, state := .ekSentCt1Received s' }
        | .done (s', sec) => .ok { key := some sec, state := .noHeaderReceived s' }
      | _ => .ok { key := none, state := .ekSentCt1Received state }
  | .noHeaderReceived state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .noHeaderReceived state }
    else
      match msg.payload with
      | .hdr chunk => do
        let res ← state.recv_hdr_chunk msg.epoch chunk
        match res with
        | .stillReceiving s' => .ok { key := none, state := .noHeaderReceived s' }
        | .done s' => .ok { key := none, state := .headerReceived s' }
      | _ => .ok { key := none, state := .noHeaderReceived state }
  | .headerReceived state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else
      .ok { key := none, state := .headerReceived state }
  | .ct1Sampled state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .ct1Sampled state }
    else
      let chunkAck? : Option (P.Chunk × Bool) := match msg.payload with
        | .ek chunk => some (chunk, false)
        | .ekCt1Ack chunk => some (chunk, true)
        | _ => none
      match chunkAck? with
      | none => .ok { key := none, state := .ct1Sampled state }
      | some (chunk, ack) => do
        let res ← state.recv_ek_chunk K msg.epoch chunk ack
        match res with
        | .stillReceivingStillSending s' => .ok { key := none, state := .ct1Sampled s' }
        | .stillReceiving s' => .ok { key := none, state := .ct1Acknowledged s' }
        | .stillSending s' => .ok { key := none, state := .ekReceivedCt1Sampled s' }
        | .done s' => .ok { key := none, state := .ct2Sampled s' }
  | .ekReceivedCt1Sampled state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .ekReceivedCt1Sampled state }
    else
      let isAck := match msg.payload with
        | .ct1Ack true => true
        | .ekCt1Ack _ => true
        | _ => false
      if isAck then do
        let s' ← StatesResult.ofPanic (state.recv_ct1_ack K msg.epoch)
        .ok { key := none, state := .ct2Sampled s' }
      else
        .ok { key := none, state := .ekReceivedCt1Sampled state }
  | .ct1Acknowledged state =>
    if msg.epoch > state.epoch then
      .error (.err (.epochOutOfRange msg.epoch))
    else if msg.epoch < state.epoch then
      .ok { key := none, state := .ct1Acknowledged state }
    else
      let chunk? : Option P.Chunk := match msg.payload with
        | .ek chunk => some chunk
        | .ekCt1Ack chunk => some chunk
        | _ => none
      match chunk? with
      | none => .ok { key := none, state := .ct1Acknowledged state }
      | some chunk => do
        let res ← state.recv_ek_chunk K msg.epoch chunk
        match res with
        | .stillReceiving s' => .ok { key := none, state := .ct1Acknowledged s' }
        | .done s' => .ok { key := none, state := .ct2Sampled s' }
  | .ct2Sampled state =>
    if msg.epoch > state.epoch then
      -- `msg.epoch > state.epoch` implies `state.epoch < u64::MAX`, so `state.epoch + 1` cannot overflow.
      if msg.epoch == state.epoch + 1#64 then do
        let s' ← StatesResult.ofPanic (state.recv_next_epoch msg.epoch)
        .ok { key := none, state := .keysUnsampled s' }
      else
        .error (.err (.epochOutOfRange msg.epoch))
    else
      .ok { key := none, state := .ct2Sampled state }

end States

16 declarations not shown (lines 1757–2079): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.stubMlKem, CryptoVerification.LibsignalSpqrV1.StubEncoder, CryptoVerification.LibsignalSpqrV1.StubEncoder.idx, CryptoVerification.LibsignalSpqrV1.StubEncoder.msg, CryptoVerification.LibsignalSpqrV1.StubDecoder.is_complete, CryptoVerification.LibsignalSpqrV1.StubDecoder, CryptoVerification.LibsignalSpqrV1.StubDecoder.chunks, CryptoVerification.LibsignalSpqrV1.StubDecoder.pts_needed, CryptoVerification.LibsignalSpqrV1.lookupChunk, CryptoVerification.LibsignalSpqrV1.reconstructChunks.go, CryptoVerification.LibsignalSpqrV1.reconstructChunks, CryptoVerification.LibsignalSpqrV1.deserializeStubChunks, CryptoVerification.LibsignalSpqrV1.stubPolyApi, CryptoVerification.LibsignalSpqrV1.stubAuthApi, CryptoVerification.LibsignalSpqrV1.checkIssue1275, CryptoVerification.LibsignalSpqrV1.guard_issue1275, CryptoVerification.LibsignalSpqrV1.checkMessageSerialize, CryptoVerification.LibsignalSpqrV1.guard_message_serialize, CryptoVerification.LibsignalSpqrV1.checkFullBraidAndPbRoundTrip, CryptoVerification.LibsignalSpqrV1.checkFullBraidAndPbRoundTrip.transferChunks, CryptoVerification.LibsignalSpqrV1.guard_full_braid_and_pb_roundtrip, CryptoVerification.LibsignalSpqrV1.checkPanicsAndErrors, CryptoVerification.LibsignalSpqrV1.guard_panics_and_errors

end CryptoVerification.LibsignalSpqrV1