StateXModel.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 58 of 105 lines trusted trust banner B2, trusted: definitions used by the statement 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 (9)

Session-Record Encoding with PQXDH Extras (encodeRecordUnderExtras)

Trusted: definitions used by the statement. Generalizes encodeRecord (State.lean, DEV-M9) from constant placeholder fields to the per-session public transcript fields RecordExtras produced by a PQXDH handshake (pending_pre_key, pending_kyber_pre_key with Kyber1024 round-3 ciphertext per DEV-PQ2, registration IDs, and alice_base_key). Both pending sub-messages are emitted iff st.pendingPreKey holds. See Computational/docs/TRUSTED_BASE.md.

@[expose] public section

namespace CryptoVerification.E2E

open CryptoGames CryptoGames.LibsignalSession CryptoVerification.LibsignalProtoCodec

The record extras

structure RecordExtrasL34–48 ↗#

The SessionStructure fields of one party's record that the session model does not track, constant over one session: the pending pre-key and pending Kyber pre-key (written only while the session model's pendingPreKey flag is set), the registration ids and alice_base_key. Field numbers: libsignal v0.105.4 rust/protocol/src/proto/storage.proto.

structure RecordExtras where
  /-- `pending_pre_key` (tag 9) while unacknowledged. -/
  pending : LibsignalSessionApi.PendingPreKey
  /-- `pending_kyber_pre_key` (tag 14) while unacknowledged (`none`: no Kyber payload). -/
  kyber : Option LibsignalSessionApi.PendingKyberPreKey
  /-- `remote_registration_id` (tag 10). -/
  remoteRegistrationId : BitVec 32
  /-- `local_registration_id` (tag 11). -/
  localRegistrationId : BitVec 32
  /-- `alice_base_key` (tag 13). -/
  aliceBaseKey : Bytes

Field writers not needed by State.lean

def uint64FieldXL52–54 ↗#

proto3 uint64: omitted when 0.

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

def int32FieldXL56–58 ↗#

proto3 int32: omitted when 0; a negative value is sign-extended to 64 bits (prost).

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

def optUint32FieldXL60–63 ↗#

optional uint32 (explicit presence): written whenever some.

def optUint32FieldX (tag : ℕ) : Option (BitVec 32) → Bytes
  | none => []
  | some v => encodeKey tag .varint ++ encodeVarint (v.setWidth 64)

Messages

def encPendingPreKeyXL67–71 ↗#

PendingPreKey { optional uint32 pre_key_id = 1; bytes base_key = 2; int32 signed_pre_key_id = 3; uint64 timestamp = 4; }.

def encPendingPreKeyX (p : LibsignalSessionApi.PendingPreKey) : Bytes :=
  optUint32FieldX 1 p.preKeyId ++ bytesField 2 p.baseKey.serialize ++
    int32FieldX 3 p.signedPreKeyId ++ uint64FieldX 4 p.timestamp

def encPendingKyberXL73–75 ↗#

PendingKyberPreKey { uint32 pre_key_id = 1; bytes ciphertext = 2; }.

def encPendingKyberX (p : LibsignalSessionApi.PendingKyberPreKey) : Bytes :=
  uint32Field 1 p.preKeyId ++ bytesField 2 p.ciphertext

def encStateUnderExtrasL77–93 ↗#

SessionStructure of a session-model state with extras x, fields in tag order 1–7, 9, 10, 11, 13, 14, 15. The pending items (9, 14) are written exactly while the session model's pendingPreKey flag is set.

def encStateUnderExtras (x : RecordExtras) (st : SessionState Bytes) : Bytes :=
  uint32Field 1 st.sessionVersion ++
  bytesField 2 st.localIdentity.serialize ++
  bytesField 3 ((st.remoteIdentity.map IdentityKey.serialize).getD []) ++
  bytesField 4 (HMAC.keyToBytes32 st.rootKey) ++
  uint32Field 5 st.previousCounter ++
  msgField 6 (st.senderChain.map encSenderChain) ++
  (st.receiverChains.map fun c => lenField 7 (encReceiverChain c)).flatten ++
  msgField 9 (if st.pendingPreKey then some (encPendingPreKeyX x.pending) else none) ++
  uint32Field 10 x.remoteRegistrationId ++
  uint32Field 11 x.localRegistrationId ++
  bytesField 13 x.aliceBaseKey ++
  msgField 14 (if st.pendingPreKey then x.kyber.map encPendingKyberX else none) ++
  bytesField 15 st.pqRatchetState

def encodeRecordUnderExtrasL95–98 ↗#

SessionRecord::serialize of a session-model state under extras E: RecordStructure { current_session = 1; } (no previous sessions).

def encodeRecordUnderExtras (E : Party → RecordExtras) (g : GhostState Bytes) : Bytes :=
  msgField 1 (some (encStateUnderExtras (E g.party) g.session))

def binStateOfUnderExtrasL100–106 ↗#

The binary state of a session-model state under extras E: the party, the record bytes encodeRecordUnderExtras E g, and the epoch ghost EpochGhost.ofGhost g.

def binStateOfUnderExtras (E : Party → RecordExtras) (g : GhostState Bytes) : BinState :=
  ⟨g.party, encodeRecordUnderExtras E g, EpochGhost.ofGhost g⟩

end CryptoVerification.E2E