ProtoPB.lean🔗

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

SPQR V1: shared pq_ratchet.proto message structures

Trusted in part. The theorems of Computational/Theorems/ use every definition in this file except ChainParams.default, ChainParams.intoPbTest and the Inhabited ChainParams instance built from default, which are checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Defines the pq_ratchet.proto structures shared across Chain.lean, Auth.lean, and Proto.lean: symmetric-chain parameters (ChainParams, DEFAULT_CHAIN_PARAMS, ChainParamsPB, intoPb, maxJumpOrDefault, maxOooKeysOrDefault, trimSize), serialized chain epochs (EpochDirectionPB, ChainEpochPB, ChainPB), version negotiation (VersionNegotiationPB), and authenticator state (ProtoAuthenticator). Kept free of CryptoGames imports so Proto.lean stays within the symbolic statement dependency boundary.

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

ChainParams and pqrpb::ChainParams (src/chain.rs:17–89)

structure ChainParamsPBL35–39 ↗#

Protobuf symmetric-chain parameters (pqrpb::ChainParams, where 0 encodes the default).

structure ChainParamsPB where
  maxJump : BitVec 32 := 0#32
  maxOooKeys : BitVec 32 := 0#32
  deriving DecidableEq, Repr, Inhabited

structure ChainParamsL41–46 ↗#

Symmetric-chain limits (src/chain.rs:17–26): maximum forward counter jump maxJump and maximum retained out-of-order message keys maxOooKeys.

structure ChainParams where
  maxJump : BitVec 32 := 25000#32
  maxOooKeys : BitVec 32 := 2000#32
  deriving DecidableEq, Repr

def DEFAULT_CHAIN_PARAMSL48–50 ↗#

Default symmetric-chain parameters (maxJump = 25000, maxOooKeys = 2000).

def DEFAULT_CHAIN_PARAMS : ChainParams :=
  { maxJump := 25000#32, maxOooKeys := 2000#32 }

namespace ChainParams

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

CryptoVerification.LibsignalSpqrV1.ChainParams.default

def intoPbL56–61 ↗#

Converts ChainParams to ChainParamsPB, mapping default field values to 0.

def intoPb (self : ChainParams) : ChainParamsPB :=
  { maxJump :=
      if self.maxJump == DEFAULT_CHAIN_PARAMS.maxJump then 0#32 else self.maxJump
    maxOooKeys :=
      if self.maxOooKeys == DEFAULT_CHAIN_PARAMS.maxOooKeys then 0#32 else self.maxOooKeys }

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

CryptoVerification.LibsignalSpqrV1.ChainParams.intoPbTest

end ChainParams

namespace ChainParamsPB

def maxJumpOrDefaultL70–71 ↗#

def maxJumpOrDefault (self : ChainParamsPB) : BitVec 32 :=
  if self.maxJump > 0#32 then self.maxJump else DEFAULT_CHAIN_PARAMS.maxJump

def maxOooKeysOrDefaultL73–74 ↗#

def maxOooKeysOrDefault (self : ChainParamsPB) : BitVec 32 :=
  if self.maxOooKeys > 0#32 then self.maxOooKeys else DEFAULT_CHAIN_PARAMS.maxOooKeys

def trimSizeL76–79 ↗#

Out-of-order key history threshold maxOoo * 11 / 10 + 1 (src/chain.rs:84–88).

def trimSize (self : ChainParamsPB) : Nat :=
  let maxOoo := self.maxOooKeysOrDefault.toNat
  maxOoo * 11 / 10 + 1

end ChainParamsPB

structure EpochDirectionPBL83–88 ↗#

pqrpb::chain::epoch::EpochDirection (src/proto/pq_ratchet.proto:197–201).

structure EpochDirectionPB where
  ctr : BitVec 32 := 0#32
  next : Bytes := []
  prev : Bytes := []
  deriving DecidableEq, Repr, Inhabited

structure ChainEpochPBL90–94 ↗#

pqrpb::chain::Epoch (src/proto/pq_ratchet.proto:196–204).

structure ChainEpochPB where
  send : Option EpochDirectionPB := none
  recv : Option EpochDirectionPB := none
  deriving DecidableEq, Repr, Inhabited

structure ChainPBL96–104 ↗#

pqrpb::Chain (src/proto/pq_ratchet.proto:195–211).

structure ChainPB where
  direction : BitVec 32 := 0#32
  currentEpoch : Epoch := 0#64
  links : List ChainEpochPB := []
  nextRoot : Bytes := []
  sendEpoch : Epoch := 0#64
  params : Option ChainParamsPB := none
  deriving DecidableEq, Repr, Inhabited

structure VersionNegotiationPBL106–112 ↗#

pqrpb::pq_ratchet_state::VersionNegotiation (src/proto/pq_ratchet.proto:26–31).

structure VersionNegotiationPB where
  authKey : Bytes := []
  direction : BitVec 32 := 0#32
  minVersion : BitVec 32 := 0#32
  chainParams : Option ChainParamsPB := none
  deriving DecidableEq, Repr, Inhabited

structure ProtoAuthenticatorL115–119 ↗#

pqrpb::Authenticator (src/proto/pq_ratchet.proto:61–64).

structure ProtoAuthenticator where
  rootKey : Bytes
  macKey : Bytes
  deriving DecidableEq, Repr, Inhabited

end CryptoVerification.LibsignalSpqrV1