SPQR.Chunked.Payload.none {Sym : Type} :
  SPQR.Chunked.Payload Sym

`None`: no payload (paper `type = None`, `data = none`). 

SPQR.Chunked.Payload.hdr {Sym : Type} (chunk : ℕ × Sym) :
  SPQR.Chunked.Payload Sym

`Hdr(chunk)`: indexed symbol of the header and tag stream. 

SPQR.Chunked.Payload.ek {Sym : Type} (chunk : ℕ × Sym) :
  SPQR.Chunked.Payload Sym

`Ek(chunk)`: indexed symbol of the encapsulation-key vector. 

SPQR.Chunked.Payload.ekCt1Ack {Sym : Type}
  (chunk : ℕ × Sym) : SPQR.Chunked.Payload Sym

`EkCt1Ack(chunk)`: vector symbol, and the sender holds all of `ct₁`. 

SPQR.Chunked.Payload.ct1Ack {Sym : Type} :
  SPQR.Chunked.Payload Sym

`Ct1Ack(true)`: the sender holds all of `ct₁`; the false flag is unreachable
(`states.rs:182`, `serialize.rs:268`). 

SPQR.Chunked.Payload.ct1 {Sym : Type} (chunk : ℕ × Sym) :
  SPQR.Chunked.Payload Sym

`Ct1(chunk)`: indexed symbol of the first ciphertext component. 

SPQR.Chunked.Payload.ct2 {Sym : Type} (chunk : ℕ × Sym) :
  SPQR.Chunked.Payload Sym

`Ct2(chunk)`: indexed symbol of the second ciphertext component and its tag. 

SPQR.Chunked.PartyState.keysUnsampled.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.EkSender.KeysUnsampled AuthState) :
  SPQR.Chunked.PartyState P AuthState

Before sampling an encapsulation key (`states.rs:17`). 

SPQR.Chunked.PartyState.keysSampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.EkSender.HeaderSent P.inc AuthState)
  (sendingHdr :
    ErasureCodePayload.Streaming.EncoderState
      (P.inc.PKheader × P.Mac) P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending the authenticated header stream (`states.rs:18`). 

SPQR.Chunked.PartyState.headerSent.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.EkSender.EkSent P.inc AuthState)
  (sendingEk :
    ErasureCodePayload.Streaming.EncoderState P.inc.PKvector
      P.Sym)
  (receivingCt1 :
    ErasureCodePayload.Streaming.DecoderState P.inc.C₁
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending the vector and receiving the first ciphertext component (`states.rs:19-20`). 

SPQR.Chunked.PartyState.ct1Received.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.EkSender.EkSentCt1Received P.inc AuthState)
  (sendingEk :
    ErasureCodePayload.Streaming.EncoderState P.inc.PKvector
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending vector chunks that acknowledge complete first-ciphertext receipt
(`states.rs:21`). 

SPQR.Chunked.PartyState.ekSentCt1Received.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.EkSender.EkSentCt1Received P.inc AuthState)
  (receivingCt2 :
    ErasureCodePayload.Streaming.DecoderState
      (P.inc.C₂ × P.Mac) P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Receiving the second ciphertext component (`states.rs:22`). 

SPQR.Chunked.PartyState.noHeaderReceived.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.NoHeaderReceived AuthState)
  (receivingHdr :
    ErasureCodePayload.Streaming.DecoderState
      (P.inc.PKheader × P.Mac) P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Receiving the authenticated header stream (`states.rs:23`). 

SPQR.Chunked.PartyState.headerReceived.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.HeaderReceived P.inc AuthState)
  (receivingEk :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Receiving the encapsulation-key vector after authenticating the header
(`states.rs:24`). 

SPQR.Chunked.PartyState.ct1Sampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.Ct1Sent P.inc AuthState)
  (sendingCt1 :
    ErasureCodePayload.Streaming.EncoderState P.inc.C₁
      P.Sym)
  (receivingEk :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending the first ciphertext component while receiving the vector
(`states.rs:25`). 

SPQR.Chunked.PartyState.ekReceivedCt1Sampled.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.Ct1SentEkReceived P.inc AuthState)
  (sendingCt1 :
    ErasureCodePayload.Streaming.EncoderState P.inc.C₁
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending the first ciphertext after validating the vector (`states.rs:26`). 

SPQR.Chunked.PartyState.ct1Acknowledged.{u}
  {m : Type → Type u} [Monad m]
  {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.Ct1Sent P.inc AuthState)
  (receivingEk :
    ErasureCodePayload.Streaming.DecoderState P.inc.PKvector
      P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Receiving the vector after the first ciphertext is acknowledged (`states.rs:27`). 

SPQR.Chunked.PartyState.ct2Sampled.{u} {m : Type → Type u}
  [Monad m] {P : MLKEMBraid.Parameters m} {AuthState : Type}
  (core : SPQR.CtSender.Ct2Sent AuthState)
  (sendingCt2 :
    ErasureCodePayload.Streaming.EncoderState
      (P.inc.C₂ × P.Mac) P.Sym) :
  SPQR.Chunked.PartyState P AuthState

Sending the second ciphertext component (`states.rs:28`). 

SPQR.Chunked.Error.epochOutOfRange (epoch : ℕ) :
  SPQR.Chunked.Error

The message epoch is ahead of the state. 

SPQR.Chunked.Error.macVerifyFailed : SPQR.Chunked.Error

A header or ciphertext tag was rejected, or deterministic decapsulation refused the
ciphertext; ML-KEM never refuses. 

SPQR.Chunked.Error.erroneousDataReceived :
  SPQR.Chunked.Error

The received vector failed validation.