Core.lean🔗

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

SPQR V1: shared core types (src/lib.rs) and constant-time helpers (src/util.rs)

Trusted in part. The theorems of Computational/Theorems/ use every definition in this file except Direction.A2B and Direction.B2A, which are checked by Lean (see Computational/docs/TRUSTED_BASE.md).

Shared SPQR V1 types (Epoch, Secret, EpochSecret, Direction with switch and toI32, Error with isStateDecode, SpqrPanic) and constant-time comparison helpers (inz, isNonZero, compare) from spqr (src/lib.rs, src/util.rs).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

Core types from src/lib.rs and src/proto/pq_ratchet.proto

abbrev EpochL32–33 ↗#

pub type Epoch = u64 (src/lib.rs:40).

abbrev Epoch := BitVec 64

abbrev SecretL35–36 ↗#

pub type Secret = Vec<u8> (src/lib.rs:41).

abbrev Secret := Bytes

structure EpochSecretL38–42 ↗#

pub struct EpochSecret (src/lib.rs:50–53).

structure EpochSecret where
  epoch : Epoch
  secret : Secret
  deriving DecidableEq, Repr, Inhabited

inductive DirectionL44–48 ↗#

pub enum Direction (src/proto/pq_ratchet.proto:218–221, src/lib.rs:28, 63–70).

inductive Direction where
  | a2b
  | b2a
  deriving DecidableEq, Repr, Inhabited

namespace Direction

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

CryptoVerification.LibsignalSpqrV1.Direction.A2B, CryptoVerification.LibsignalSpqrV1.Direction.B2A

def switchL56–58 ↗#

def switch : Direction → Direction
  | .a2b => .b2a
  | .b2a => .a2b

def toI32L60–63 ↗#

Protobuf i32 encoding (0 for a2b, 1 for b2a).

def toI32 : Direction → BitVec 32
  | .a2b => 0#32
  | .b2a => 1#32

def fromI32?L65–69 ↗#

Direction::try_from(v: i32) (src/proto/pq_ratchet.proto:218–221).

def fromI32? (v : BitVec 32) : Option Direction :=
  if v = 0#32 then some .a2b
  else if v = 1#32 then some .b2a
  else none

end Direction

inductive ErrorL73–91 ↗#

pub enum Error (src/lib.rs:96–130).

inductive Error where
  | stateDecode
  | notImplemented
  | msgDecode
  | macVerifyFailed
  | epochOutOfRange (epoch : Epoch)
  | encodingDecoding
  | serialization
  | versionMismatch
  | minimumVersion
  | keyJump (ctr atIdx : BitVec 32)
  | keyTrimmed (atIdx : BitVec 32)
  | keyAlreadyRequested (atIdx : BitVec 32)
  | erroneousDataReceived
  | sendKeyEpochDecreased (sendEpoch epoch : Epoch)
  | invalidParams (msg : String)
  | chainNotAvailable
  deriving DecidableEq, Repr, Inhabited

namespace Error

def isStateDecodeL95–97 ↗#

def isStateDecode : Error → Bool
  | .stateDecode => true
  | _ => false

end Error

Panics

inductive SpqrPanicL103–108 ↗#

Shared Rust panic sites (compareBounds at src/util.rs:29, or site for cited panics).

inductive SpqrPanic where
  /-- `src/util.rs:29`: `rhs[i]` out of bounds in `compare` when `rhs.len() < lhs.len()`. -/
  | compareBounds
  | site (loc : String)
  deriving DecidableEq, Repr, Inhabited

src/util.rs

def inzL112–116 ↗#

spqr::util::inz(value: u8) -> u8 (src/util.rs:7–13).

def inz (value : BitVec 8) : BitVec 8 :=
  let v16 : BitVec 16 := value.zeroExtend 16
  let result : BitVec 16 := ((v16 ||| ((~~~v16) + 1#16)) >>> 8) &&& 1#16
  result.truncate 8

def isNonZeroL118–119 ↗#

def isNonZero (value : BitVec 8) : BitVec 8 :=
  inz value

def compareL121–127 ↗#

spqr::util::compare(lhs: &[u8], rhs: &[u8]) -> u8 (src/util.rs:25–33): returns 0 iff lhs equals the first lhs.length bytes of rhs, or panics with compareBounds when lhs.length > rhs.length.

def compare (lhs rhs : Bytes) : Except SpqrPanic (BitVec 8) :=
  if lhs.length ≤ rhs.length then
    .ok (isNonZero ((lhs.zip rhs).foldl (fun r (a, b) => r ||| (a ^^^ b)) 0#8))
  else .error .compareBounds

end CryptoVerification.LibsignalSpqrV1