Proto.lean
Declarations on this page (10)
Protobuf Record Codecs for Identity and Pre-Key Stores
Trusted in part. SignalSession/ (encodeDir) encodes identity and pre-key store files with IdentityKeyPairStructure, SignedPreKeyRecordStructure, and PreKeyRecordStructure (encode) via encodeProto3BytesField, encodeProto3Uint32Field, encodeProto3Fixed64Field, and le64Bytes; the decoders (empty, mergeField, decode, decodeFieldsLoop, skipUnknown, mergeFixed64, le64) and record wrappers (PreKeyRecord, SignedPreKeyRecord, KyberPreKeyRecord, deserialize, serialize) are checked by Lean. See Computational/.
Models prost 0.14.4's proto3 encoders (tag-ordered fields, omitting default 0 / empty values) and decoders (Message::merge from default with last-write-wins field merging and unknown-field skipping up to recursion limit 100) for storage. messages.
@[expose] public sectionnamespace CryptoVerification.RecordCodecsopen CryptoGames.LibsignalSession CryptoVerification.LibsignalProtoCodec3 declarations not shown (lines 38–64): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification.
def le64Bytes
BufMut::put_u64_le: the 8 little-endian bytes of v.
def le64Bytes (v : BitVec 64) : List (BitVec 8) :=
[v.extractLsb' 0 8, v.extractLsb' 8 8, v.extractLsb' 16 8, v.extractLsb' 24 8,
v.extractLsb' 32 8, v.extractLsb' 40 8, v.extractLsb' 48 8, v.extractLsb' 56 8]1 declaration not shown (lines 71–78): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification.
proto3 field encoders (omit the default value, D/)
def encodeProto3BytesField
A proto3 bytes field: nothing when empty, else bytes::encode(tag, value) (P/).
def encodeProto3BytesField (tag : ℕ) (v : List (BitVec 8)) : List (BitVec 8) :=
if v = [] then [] else encodeBytesField tag (some v)def encodeProto3Uint32Field
A proto3 uint32 field: nothing when 0, else uint32::encode(tag, value).
def encodeProto3Uint32Field (tag : ℕ) (v : BitVec 32) : List (BitVec 8) :=
if v = 0 then [] else encodeUint32Field tag (some v)def encodeProto3Fixed64Field
A proto3 fixed64 field: nothing when 0, else the key and put_u64_le(value).
def encodeProto3Fixed64Field (tag : ℕ) (v : BitVec 64) : List (BitVec 8) :=
if v = 0 then [] else encodeKey tag .sixtyFourBit ++ le64Bytes v
PreKeyRecordStructure (storage.)
structure PreKeyRecordStructure
message PreKeyRecordStructure { uint32 id = 1; bytes public_key = 2; bytes private_key = 3; } (prost struct proto::storage::PreKeyRecordStructure).
structure PreKeyRecordStructure where
/-- `uint32 id = 1`. -/
id : BitVec 32
/-- `bytes public_key = 2` (libsignal writes `PublicKey::serialize`, 33 bytes). -/
publicKey : List (BitVec 8)
/-- `bytes private_key = 3` (libsignal writes `PrivateKey::serialize`, 32 bytes). -/
privateKey : List (BitVec 8)
deriving DecidableEq, Reprnamespace PreKeyRecordStructure3 declarations not shown (lines 110–124): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification.
def encode
<PreKeyRecordStructure as Message>::encode_to_vec.
def encode (m : PreKeyRecordStructure) : List (BitVec 8) :=
encodeProto3Uint32Field 1 m.id ++ encodeProto3BytesField 2 m.publicKey ++ encodeProto3BytesField 3 m.privateKeyend PreKeyRecordStructure
SignedPreKeyRecordStructure (storage.)
structure SignedPreKeyRecordStructure
message SignedPreKeyRecordStructure { uint32 id = 1; bytes public_key = 2; bytes private_key = 3; bytes signature = 4; fixed64 timestamp = 5; }. Both SignedPreKeyRecord (X25519 keys) and KyberPreKeyRecord (KEM keys) store one.
structure SignedPreKeyRecordStructure where
/-- `uint32 id = 1`. -/
id : BitVec 32
/-- `bytes public_key = 2`. -/
publicKey : List (BitVec 8)
/-- `bytes private_key = 3`. -/
privateKey : List (BitVec 8)
/-- `bytes signature = 4`. -/
signature : List (BitVec 8)
/-- `fixed64 timestamp = 5` (milliseconds since the epoch). -/
timestamp : BitVec 64
deriving DecidableEq, Reprnamespace SignedPreKeyRecordStructure3 declarations not shown (lines 152–168): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification.
def encode
<SignedPreKeyRecordStructure as Message>::encode_to_vec.
def encode (m : SignedPreKeyRecordStructure) : List (BitVec 8) :=
encodeProto3Uint32Field 1 m.id ++ encodeProto3BytesField 2 m.publicKey ++ encodeProto3BytesField 3 m.privateKey ++
encodeProto3BytesField 4 m.signature ++ encodeProto3Fixed64Field 5 m.timestampend SignedPreKeyRecordStructure
IdentityKeyPairStructure (storage.)
structure IdentityKeyPairStructure
message IdentityKeyPairStructure { bytes public_key = 1; bytes private_key = 2; }.
structure IdentityKeyPairStructure where
/-- `bytes public_key = 1`. -/
publicKey : List (BitVec 8)
/-- `bytes private_key = 2`. -/
privateKey : List (BitVec 8)
deriving DecidableEq, Reprnamespace IdentityKeyPairStructure3 declarations not shown (lines 189–202): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification.
def encode
<IdentityKeyPairStructure as Message>::encode_to_vec.
def encode (m : IdentityKeyPairStructure) : List (BitVec 8) :=
encodeProto3BytesField 1 m.publicKey ++ encodeProto3BytesField 2 m.privateKeyend IdentityKeyPairStructure9 declarations not shown (lines 212–269): theorems, which Lean checks, or definitions that no headline statement uses
CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification., CryptoVerification.
end CryptoVerification.RecordCodecs