Assemble.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 112 of 667 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: concrete model assembly (spqrV1Assembled)

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

Instantiates the abstract dependency bundles (spqrPolyApi, spqrAuthApi, spqrDeps) to produce the concrete SPQR V1 models spqrV1Assembled and spqrV1RecvAssembled (DEV-SPQR2). Proves chain and receive key-length invariants (Chain.recvKey_key_length, recv_key_valid, recv_key_valid_unless_greater_index_zero, recv_some_key_length_32_unless_greater_index_zero) and receive-panic monotonicity (toSpqrModel_recvPanics_of_toSpqrRecvModel).

@[expose] public section

namespace CryptoVerification.LibsignalSpqrV1

open CryptoGames.HMAC (ShaState hmacWith)

open CryptoGames.HKDF (Salt hkdfBlocks hkdfExpand)

open CryptoGames.LibsignalSession (ShaCompress)

open CryptoVerification.LibsignalTripleRatchet (SpqrModel)

1. Concrete PolyApi and AuthApi instances

instanceL40–41 ↗#

instance : Repr Chunk where
  reprPrec c p := reprPrec (c.index, c.data.toList) p

instanceL43–44 ↗#

instance : Inhabited Chunk where
  default := { index := 0#16, data := List.Vector.replicate 32 0#8 }

def protoPolyEncoderToPbL46–47 ↗#

def protoPolyEncoderToPb (pb : ProtoPolynomialEncoder) : PolynomialEncoder :=
  { idx := pb.idx, pts := pb.pts, polys := pb.polys }

def pbToProtoPolyEncoderL49–50 ↗#

def pbToProtoPolyEncoder (pb : PolynomialEncoder) : ProtoPolynomialEncoder :=
  { idx := pb.idx, pts := pb.pts, polys := pb.polys }

def protoPolyDecoderToPbL52–53 ↗#

def protoPolyDecoderToPb (pb : ProtoPolynomialDecoder) : PolynomialDecoder :=
  { ptsNeeded := pb.ptsNeeded, polys := pb.polys, pts := pb.pts, isComplete := pb.isComplete }

def pbToProtoPolyDecoderL55–56 ↗#

def pbToProtoPolyDecoder (pb : PolynomialDecoder) : ProtoPolynomialDecoder :=
  { ptsNeeded := pb.ptsNeeded, polys := pb.polys, pts := pb.pts, isComplete := pb.isComplete }

def spqrPolyApiL58–85 ↗#

Concrete PolyApi instance backed by PolyEncoder and PolyDecoder (Poly.lean).

def spqrPolyApi : PolyApi where
  Chunk := Chunk
  PolynomialError := PolynomialError
  EncodingError := EncodingError
  PolyEncoder := PolyEncoder
  PolyDecoder := PolyDecoder
  mkChunk := Chunk.mk
  chunkIndex := Chunk.index
  chunkData := Chunk.data
  encode_bytes := fun msg =>
    (PolyEncoder.encodeBytes msg).mapError PolyPanic.toSpqrPanic
  next_chunk := fun enc =>
    enc.nextChunk.mapError PolyPanic.toSpqrPanic
  encoder_into_pb := fun enc =>
    protoPolyEncoderToPb enc.intoPb
  encoder_from_pb := fun pb =>
    (PolyEncoder.fromPb (pbToProtoPolyEncoder pb)).mapError PolyPanic.toSpqrPanic
  decoder_new := fun lenBytes =>
    (PolyDecoder.new lenBytes).mapError PolyPanic.toSpqrPanic
  add_chunk := fun dec chunk =>
    (dec.addChunk chunk).mapError PolyPanic.toSpqrPanic
  decoded_message := fun dec =>
    dec.decodedMessage.mapError PolyPanic.toSpqrPanic
  decoder_into_pb := fun dec =>
    protoPolyDecoderToPb dec.intoPb
  decoder_from_pb := fun pb =>
    (PolyDecoder.fromPb (pbToProtoPolyDecoder pb)).mapError PolyPanic.toSpqrPanic

def spqrAuthApiL87–98 ↗#

Concrete AuthApi instance backed by Authenticator (Auth.lean) and hkdfToVec F.

def spqrAuthApi (F : ShaCompress) : AuthApi where
  Authenticator := Authenticator
  new := fun rootKey ep => .ok (Authenticator.new F rootKey ep)
  update := fun auth ep k => .ok (auth.update F ep k)
  mac_hdr := fun auth ep hdr => auth.macHdr F ep hdr
  mac_ct := fun auth ep ct => auth.macCt F ep ct
  verify_hdr := fun auth ep hdr expectedMac => auth.verifyHdrError F ep hdr expectedMac
  verify_ct := fun auth ep ct expectedMac => auth.verifyCtError F ep ct expectedMac
  into_pb := Authenticator.intoPb
  from_pb := Authenticator.fromPb
  hkdf_to_vec := hkdfToVec F

2. Concrete SpqrApiDeps and Assembled Models (spqrV1Assembled, spqrV1RecvAssembled)

def liftStatesResultL102–106 ↗#

def liftStatesResult {α : Type} (r : StatesResult α) : SpqrApiResult α :=
  match r with
  | .ok v => .ok v
  | .error (.err e) => .error (.err e)
  | .error (.panic _) => .error (.panic .v1)

def pqRatchetStateToPbL108–111 ↗#

def pqRatchetStateToPb (st : PqRatchetState) : PqRatchetStatePB V1State :=
  { inner := st.inner.map fun (.v1 v) => v
    versionNegotiation := st.versionNegotiation
    chain := st.chain }

def pbToPqRatchetStateL113–116 ↗#

def pbToPqRatchetState (st : PqRatchetStatePB V1State) : PqRatchetState :=
  { inner := st.inner.map PqRatchetState.Inner.v1
    versionNegotiation := st.versionNegotiation
    chain := st.chain }

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

CryptoVerification.LibsignalSpqrV1.pqRatchetStateToPb_pbToPqRatchetState, CryptoVerification.LibsignalSpqrV1.pbToPqRatchetState_pqRatchetStateToPb

def spqrDepsL132–175 ↗#

Concrete SpqrApiDeps bundle wiring Proto.lean (V1State, Proto.decodeState, Proto.encodeState) and States.lean (States spqrPolyApi (spqrAuthApi F), Message spqrPolyApi) into Top.lean.

def spqrDeps (F : ShaCompress) (K : MlKem) : SpqrApiDeps where
  V1StatePB := V1State
  decodeState := fun bs =>
    match Proto.decodeState bs with
    | .ok st => .ok (pqRatchetStateToPb st)
    | .error _ => .error ()
  encodeState := fun st =>
    Proto.encodeState (pbToPqRatchetState st)
  States := States spqrPolyApi (spqrAuthApi F)
  statesFromPb := fun pb =>
    liftStatesResult (States.from_pb spqrPolyApi (spqrAuthApi F) pb)
  statesIntoPb := States.into_pb
  MessageV1 := Message spqrPolyApi
  statesSend := fun st tape =>
    match st.send K tape with
    | .ok (sOut, tape') => (.ok (sOut.msg, sOut.key, sOut.state), tape')
    | .error (.err e) => (.error (.err e), tape)
    -- On a panic the returned tape is irrelevant: `toSpqrModel`'s `onPanic` clause never reads
    -- `draws`.
    | .error (.panic _) => (.error (.panic .v1), tape)
  statesRecv := fun st msg =>
    match st.recv K msg with
    | .ok rOut => .ok (rOut.key, rOut.state)
    | .error (.err e) => .error (.err e)
    | .error (.panic _) => .error (.panic .v1)
  msgSerialize := Message.serialize
  msgDeserialize := fun ep rem =>
    match Message.deserialize spqrPolyApi ep rem with
    | .ok m => .ok m
    | .error e => .error (.err e)
  msgEpoch := Message.epoch
  -- `States.init_a` / `init_b` never return `.error`; `.error .v1` keeps the match total.
  initV1Inner := fun dir authKey =>
    match dir with
    | .a2b =>
      match States.init_a spqrPolyApi (spqrAuthApi F) authKey with
      | .ok st => .ok st.into_pb
      | .error _ => .error .v1
    | .b2a =>
      match States.init_b spqrPolyApi (spqrAuthApi F) authKey with
      | .ok st => .ok st.into_pb
      | .error _ => .error .v1

def spqrV1AssembledL177–179 ↗#

Assembled SPQR V1 SpqrModel (toSpqrModel (spqrDeps F K) (spqrHkdfWith F)).

def spqrV1Assembled (F : ShaCompress) (K : MlKem) : SpqrModel :=
  toSpqrModel (spqrDeps F K) (spqrHkdfWith F)

25 declarations not shown (lines 181–665): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.LibsignalSpqrV1.spqrV1RecvAssembled, _private.0.CryptoVerification.LibsignalSpqrV1.except_bind_eq_ok, CryptoVerification.LibsignalSpqrV1.ChainResult.ofPanic_eq_ok, CryptoVerification.LibsignalSpqrV1.ChainResult.ofError_eq_ok, CryptoVerification.LibsignalSpqrV1.SpqrApiResult.ofError_eq_ok, CryptoVerification.LibsignalSpqrV1.SpqrApiResult.ofPanic_eq_ok, CryptoVerification.LibsignalSpqrV1.SpqrApiResult.ofChainPanic_eq_ok, CryptoVerification.LibsignalSpqrV1.SpqrApiResult.ofChainResult_eq_ok, CryptoVerification.LibsignalSpqrV1.length_flatten_hkdfBlocks, CryptoVerification.LibsignalSpqrV1.length_hkdfExpand, CryptoVerification.LibsignalSpqrV1.length_spqrHkdfWith, _private.0.CryptoVerification.LibsignalSpqrV1.KeyHistory.getLoop_key_length_aux, CryptoVerification.LibsignalSpqrV1.KeyHistory.getLoop_key_length, CryptoVerification.LibsignalSpqrV1.KeyHistory.get_key_length, CryptoVerification.LibsignalSpqrV1.ChainEpochDirection.nextKeyInternal_key_length, CryptoVerification.LibsignalSpqrV1.ChainEpochDirection.key_key_length, CryptoVerification.LibsignalSpqrV1.Chain.recvKey_key_length, CryptoVerification.LibsignalSpqrV1.saltToMessageKey, CryptoVerification.LibsignalSpqrV1.saltToMessageKey_messageKeyToSalt?, CryptoVerification.LibsignalSpqrV1.recvKeyToSalt?_isSome_of_messageKeyToSalt?, CryptoVerification.LibsignalSpqrV1.toSpqrModel_recvPanics_of_toSpqrRecvModel, _private.0.CryptoVerification.LibsignalSpqrV1.recv_v1_tail_key_valid, CryptoVerification.LibsignalSpqrV1.recv_key_valid_unless_greater_index_zero, CryptoVerification.LibsignalSpqrV1.recv_some_key_length_32_unless_greater_index_zero, CryptoVerification.LibsignalSpqrV1.recv_key_valid

end CryptoVerification.LibsignalSpqrV1