ModelTraces.lean🔗

Tier 2 · definitions used by the symbolic proof 3 headline theorems depend on it 393 of 504 lines trusted 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 (76)

Composed Model Steps, Traces, and Visible Entries

First-order step representation (Step), initial PKI/pre-key setup (ProtocolSetup, setupTrace), observable entry projection (stepView), and faithful run predicate (ModelRunWF) for the composed symbolic state machine Composed.reachability.

@[expose] public section

namespace DY.Libsignal.Composed.Refinement

open DY DY.Comparse

open CryptoProofLib.Refinement (ExternInterpretation)

open DY.Libsignal.Refinement (x25519PublicKeySymbol)

open PQXDH (PQXDHEvent BundleHandles BobKeyHandles PreKeyMsgHandles)

open TripleRatchet (TREvent TRState)

def setupActL38–45 ↗#

Provision Alice's and Bob's honest identities, Bob's signed X25519 and Kyber-1024 prekeys, and (when withOpk holds) one one-time prekey for Bob.

def setupAct (a b : Participant) (withOpk : Bool) : Traceful Unit := do
  let _ ← PQXDH.registerIdentity a
  let hB ← PQXDH.registerIdentity b
  let _ ← PQXDH.genSignedPrekey b hB
  let _ ← PQXDH.genPQPrekey b hB
  if withOpk then do let _ ← PQXDH.genOneTimePrekey b; pure ()

inductive StepL47–73 ↗#

First-order inductive mirror of the 23 transitions in Composed.reachability.

inductive Step where
  | network (msg : DY.Bytes)
  | registerIdentity (p : Participant)
  | registerCorruptIdentity (p : Participant) (skIdx : Nat)
  | genSignedPrekey (b : Participant) (idStateIdx : Nat)
  | genPQPrekey (b : Participant) (idStateIdx : Nat)
  | genOneTimePrekey (b : Participant)
  | aliceStart (a b : Participant) (idStateIdx regIdxB : Nat) (h : BundleHandles)
  | bobStart (b a : Participant) (kh : BobKeyHandles) (regIdxA : Nat) (mh : PreKeyMsgHandles)
      (pqIdx : Nat) (spqrMsgIdx : UInt32)
  | messageEncrypt (me : Participant) (stateIdx coinsLen pqIdx : Nat)
  | messageEncryptAbort (me : Participant) (stateIdx : Nat)
  | messageDecrypt (me : Participant) (stateIdx msgIdx pqIdx : Nat) (spqrMsgIdx : UInt32)
  | messageDecryptSkipped (me : Participant) (stateIdx msgIdx skippedKeyEventIdx pqIdx : Nat)
      (spqrMsgIdx : UInt32)
  | exposeKey (me : Participant) (stateIdx : Nat) (k : TripleRatchet.KeyComponent)
  | exposeSpqr (me : Participant) (stateIdx : Nat)
  | exposeSkipped (skippedKeyEventIdx : Nat)
  | compromiseIK (p : Participant) (stateIdx : Nat)
  | compromiseSPK (b : Participant) (stateIdx : Nat)
  | compromisePQSPK (b : Participant) (stateIdx : Nat)
  | compromiseOPK (b : Participant) (stateIdx : Nat)
  | breakDH
  | breakKEM
  | invertDH (pkIdx : Nat)
  | invertKEM (pkIdx : Nat)

abbrev stepInL75–77 ↗#

abbrev stepIn (c : ReachabilityConfig) [i : ReachabilityConfig.HasStep c reachability]
    (x : c.Input) : reachability.Input :=
  i.inj x

def Step.toInputL79–109 ↗#

def Step.toInput : Step → reachability.Input
  | .network msg => stepIn Network.reachability msg
  | .registerIdentity p => stepIn PQXDH.registerIdentity.reachability p
  | .registerCorruptIdentity p skIdx => stepIn PQXDH.registerCorruptIdentity.reachability (p, skIdx)
  | .genSignedPrekey b i => stepIn PQXDH.genSignedPrekey.reachability (b, i)
  | .genPQPrekey b i => stepIn PQXDH.genPQPrekey.reachability (b, i)
  | .genOneTimePrekey b => stepIn PQXDH.genOneTimePrekey.reachability b
  | .aliceStart a b idStateIdx regIdxB h =>
    stepIn Composed.aliceStart.reachability (a, b, idStateIdx, regIdxB, h)
  | .bobStart b a kh regIdxA mh pqIdx spqrMsgIdx =>
    stepIn Composed.bobStart.reachability (b, a, kh, regIdxA, mh, pqIdx, spqrMsgIdx)
  | .messageEncrypt me stateIdx coinsLen pqIdx =>
    stepIn TripleRatchet.messageEncrypt.reachability (me, stateIdx, coinsLen, pqIdx)
  | .messageEncryptAbort me stateIdx =>
    stepIn TripleRatchet.messageEncryptAbort.reachability (me, stateIdx)
  | .messageDecrypt me stateIdx msgIdx pqIdx spqrMsgIdx =>
    stepIn TripleRatchet.messageDecrypt.reachability (me, stateIdx, msgIdx, pqIdx, spqrMsgIdx)
  | .messageDecryptSkipped me stateIdx msgIdx skIdx pqIdx spqrMsgIdx =>
    stepIn TripleRatchet.messageDecryptSkipped.reachability
      (me, stateIdx, msgIdx, skIdx, pqIdx, spqrMsgIdx)
  | .exposeKey me stateIdx k => stepIn TripleRatchet.exposeKey.reachability (me, stateIdx, k)
  | .exposeSpqr me stateIdx => stepIn TripleRatchet.exposeSpqr.reachability (me, stateIdx)
  | .exposeSkipped skIdx => stepIn TripleRatchet.exposeSkipped.reachability skIdx
  | .compromiseIK p stateIdx => stepIn PQXDH.compromiseIK.reachability (p, stateIdx)
  | .compromiseSPK b stateIdx => stepIn PQXDH.compromiseSPK.reachability (b, stateIdx)
  | .compromisePQSPK b stateIdx => stepIn PQXDH.compromisePQSPK.reachability (b, stateIdx)
  | .compromiseOPK b stateIdx => stepIn PQXDH.compromiseOPK.reachability (b, stateIdx)
  | .breakDH => stepIn PQXDH.breakDH.reachability ()
  | .breakKEM => stepIn PQXDH.breakKEM.reachability ()
  | .invertDH pkIdx => stepIn PQXDH.invertDH.reachability pkIdx
  | .invertKEM pkIdx => stepIn PQXDH.invertKEM.reachability pkIdx

def Step.nextL111–113 ↗#

Resulting trace after running s on tr.

def Step.next (s : Step) : ExecTrace → ExecTrace :=
  fun tr => ((reachability.step s.toInput).2.run tr).2.val

def Step.okL115–117 ↗#

Whether s succeeds on tr.

def Step.ok (s : Step) (tr : ExecTrace) : Bool :=
  ((reachability.step s.toInput).2.run tr).1.isSome

def Step.PreCondL119–120 ↗#

Reachability precondition of s on tr.

def Step.PreCond (s : Step) (tr : ExecTrace) : Prop := reachability.PreCond s.toInput tr

inductive StepClassL122–132 ↗#

Alignment category of a Step with respect to CLI trace events.

inductive StepClass where
  /-- Honest party transition matched by one exit-0 CLI `RunEvent`. -/
  | party
  /-- Compromise, exposure, break, inversion, or corrupt registration matched by one `EnvEvent`. -/
  | env
  /-- Attacker `network` deduction step matched by no CLI event. -/
  | invisible
  /-- Key-provisioning step permitted only in the initial setup prefix. -/
  | setup
  deriving DecidableEq

def Step.clsL134–157 ↗#

def Step.cls : Step → StepClass
  | .network .. => .invisible
  | .registerIdentity .. => .setup
  | .genSignedPrekey .. => .setup
  | .genPQPrekey .. => .setup
  | .genOneTimePrekey .. => .setup
  | .aliceStart .. => .party
  | .bobStart .. => .party
  | .messageEncrypt .. => .party
  | .messageEncryptAbort .. => .party
  | .messageDecrypt .. => .party
  | .messageDecryptSkipped .. => .party
  | .exposeKey .. => .env
  | .exposeSpqr .. => .env
  | .exposeSkipped .. => .env
  | .compromiseIK .. => .env
  | .compromiseSPK .. => .env
  | .compromisePQSPK .. => .env
  | .compromiseOPK .. => .env
  | .breakDH => .env
  | .breakKEM => .env
  | .invertDH .. => .env
  | .invertKEM .. => .env
  | .registerCorruptIdentity .. => .env

def Step.party?L159–173 ↗#

Acting or compromised participant of a step (none for exposeSkipped and global steps).

def Step.party? : Step → Option Participant
  | .aliceStart a .. => some a
  | .bobStart b .. => some b
  | .messageEncrypt me .. => some me
  | .messageEncryptAbort me _ => some me
  | .messageDecrypt me .. => some me
  | .messageDecryptSkipped me .. => some me
  | .exposeKey me .. => some me
  | .exposeSpqr me _ => some me
  | .compromiseIK p _ => some p
  | .compromiseSPK b _ => some b
  | .compromisePQSPK b _ => some b
  | .compromiseOPK b _ => some b
  | _ => none

def Step.decryptMsgIdx?L175–179 ↗#

Network handle read by messageDecrypt or messageDecryptSkipped (none otherwise).

def Step.decryptMsgIdx? : Step → Option Nat
  | .messageDecrypt _ _ msgIdx .. => some msgIdx
  | .messageDecryptSkipped _ _ msgIdx .. => some msgIdx
  | _ => none

inductive VisEventKindL181–184 ↗#

Observable kind of a VisEntry (pt, send, rng, accept, recv, or leak).

inductive VisEventKind where
  | pt | send | rng | accept | recv | leak
  deriving DecidableEq

inductive VisByteLayoutL186–201 ↗#

Byte-level encoding layout relating concrete HwBytes to the symbolic terms in a VisEntry.

inductive VisByteLayout where
  | single
  | whisper
  | bundle
  | preKeySend
  | preKeyRecv
  /-- `0x03 || PreKeySignalMessage` decrypted on an existing Bob session whose base key lies in
  `eks` (`promote_matching_session`). -/
  | preKeyInner (eks : List DY.Bytes)
  | fresh (n : Nat)
  | kyberCoin (j : Nat)
  | unconstrained
  | leakPq (pq : Bool)
  | leakRecord
  deriving DecidableEq

structure VisEntryL203–208 ↗#

Observable entry emitted by a Step, with optional trace index anchor of its logged event.

structure VisEntry where
  kind : VisEventKind
  terms : List DY.Bytes
  layout : VisByteLayout
  anchor : Option Nat

def randTermL210 ↗#

def randTerm (i n : Nat) : DY.Bytes := ({timestamp := i, size := n} : DY.Random.Random DY.Bytes).pack

def newIndicesL212 ↗#

def newIndices (tr tr' : ExecTrace) : List Nat := List.range' tr.length (tr'.length - tr.length)

def newRandomsL214–216 ↗#

def newRandoms (tr tr' : ExecTrace) : List (DY.Bytes × Nat) :=
  (newIndices tr tr').filterMap fun i =>
    (tr'.at? i : Option DY.Random.ExecEntryT).map fun e => (randTerm i e.length, e.length)

def receivedL218–219 ↗#

def received (tr : ExecTrace) (hs : List Nat) : List DY.Bytes :=
  hs.filterMap fun i => tr.getMessageSentAt i

def rngEntryL221 ↗#

def rngEntry (t : DY.Bytes) : VisEntry := ⟨.rng, [t], .single, none⟩

def eventIdxL223–224 ↗#

def eventIdx (p : PQXDHEvent → Bool) (tr tr' : ExecTrace) : Option Nat :=
  (newIndices tr tr').find? fun i => ((tr'.getEventAt PQXDHEvent i).map p).getD false

def isAliceDoneL226–228 ↗#

def isAliceDone : PQXDHEvent → Bool
  | .AliceDone .. => true
  | _ => false

def isBobDoneL230–232 ↗#

def isBobDone : PQXDHEvent → Bool
  | .BobDone .. => true
  | _ => false

def receivedPlaintextL234–238 ↗#

def receivedPlaintext (tr tr' : ExecTrace) : Option DY.Bytes :=
  (newIndices tr tr').findSome? fun i =>
    match tr'.getEventAt TREvent i with
    | some (.Received _ _ _ _ m) => some m
    | _ => none

def lastSentL240–241 ↗#

def lastSent (tr tr' : ExecTrace) : Option DY.Bytes :=
  if tr.length < tr'.length then tr'.getMessageSentAt (tr'.length - 1) else none

def kyberCoinEntriesL243–244 ↗#

def kyberCoinEntries (entropy : DY.Bytes) : List VisEntry :=
  (List.range 32).map fun j => ⟨.rng, [entropy], .kyberCoin j, none⟩

def aliceDrawsL246–251 ↗#

def aliceDraws (done : Option Nat) : List DY.Bytes → List VisEntry
  | [] => []
  | [ek] => [rngEntry ek]
  | ek :: entropy :: rest =>
    rngEntry ek :: kyberCoinEntries entropy ++
      (rest.take 1).map fun dhsA => ({ rngEntry dhsA with anchor := done } : VisEntry)

def aliceVisL253–255 ↗#

def aliceVis (tr tr' : ExecTrace) (h : BundleHandles) : List VisEntry :=
  ⟨.recv, received tr ([h.spk, h.spkSig, h.pqpk, h.pqpkSig] ++ h.opk.toList), .bundle, none⟩ ::
    aliceDraws (eventIdx isAliceDone tr tr') ((newRandoms tr tr').map (·.1))

def bobOpkPkL257–258 ↗#

def bobOpkPk (b : Participant) (h : BobKeyHandles) (tr : ExecTrace) : Option DY.Bytes :=
  h.opk.bind fun i => ((PQXDH.getKey b i .oneTimePrekey).run tr).1.map DY.DiffieHellman.dhPk

def bobVisL260–265 ↗#

def bobVis (tr tr' : ExecTrace) (mh : PreKeyMsgHandles) (opk : Option DY.Bytes) :
    List VisEntry :=
  ⟨.recv, received tr [mh.ek, mh.ct, mh.msg] ++ opk.toList, .preKeyRecv, none⟩ ::
    (newRandoms tr tr').map (fun r => rngEntry r.1) ++
    ((receivedPlaintext tr tr').map fun m =>
      (⟨.accept, [m], .single, eventIdx isBobDone tr tr'⟩ : VisEntry)).toList

def encDrawsL267–270 ↗#

def encDraws : List (DY.Bytes × Nat) → List VisEntry
  | [] => []
  | (m, _) :: rest =>
    ⟨.pt, [m], .single, none⟩ :: (rest.filter (·.2 != 0)).map fun r => rngEntry r.1

def _root_.DY.ExecTrace.getLocalStateAtL272–277 ↗#

def _root_.DY.ExecTrace.getLocalStateAt (StateT : Type) [ExecTraceTypes]
    [ExecTraceTypes.Has (PersistentGlobalState.State.ExecEntryT
      (PersistentLocalState.LocalState StateT))]
    (tr : ExecTrace) (i : Nat) : Option (PersistentLocalState.LocalState StateT) :=
  (tr.at? i : Option (PersistentGlobalState.State.ExecEntryT
    (PersistentLocalState.LocalState StateT))).map (·.st)

def sessionHandshakeEventsL279–283 ↗#

def sessionHandshakeEvents (tr : ExecTrace) (s0 : TripleRatchet.SessionInfo) : List PQXDHEvent :=
  (List.range tr.length).filterMap fun i =>
    match tr.getEventAt ComposedEvent i with
    | some (.HandshakeSession s d) => if s = s0 then tr.getEventAt PQXDHEvent d else none
    | none => none

def sessionBaseKeysL285–293 ↗#

Base keys (alice_base_key) recorded by BobDone events linked to the session stored at stateIdx on tr.

def sessionBaseKeys (tr : ExecTrace) (stateIdx : Nat) : List DY.Bytes :=
  match tr.getLocalStateAt TRState stateIdx with
  | some ls =>
    (sessionHandshakeEvents tr (ls.state.sessionInfo ls.participant)).filterMap fun
      | .BobDone _ _ _ _ _ _ _ ek _ _ => some ek
      | _ => none
  | none => []

def decVisL295–300 ↗#

def decVis (tr tr' : ExecTrace) (stateIdx msgIdx : Nat) (wrapped : Bool) : List VisEntry :=
  ((tr.getMessageSentAt msgIdx).map fun b =>
    (⟨.recv, [b], if wrapped then .preKeyInner (sessionBaseKeys tr stateIdx) else .whisper,
      none⟩ : VisEntry)).toList ++
    (newRandoms tr tr').map (fun r => rngEntry r.1) ++
    ((receivedPlaintext tr tr').map fun m => (⟨.accept, [m], .single, none⟩ : VisEntry)).toList

def pqExposureAtL302–308 ↗#

def pqExposureAt (tr' : ExecTrace) (j : Nat) : Option VisEntry :=
  let term := (tr'.getMessageSentAt (j + 1)).toList
  match tr'.getEventAt PQXDHEvent j with
  | some (.CompromisedIK ..) | some (.CompromisedSPK ..) | some (.CompromisedOPK ..) =>
    some ⟨.leak, term, .leakPq false, some j⟩
  | some (.CompromisedPQSPK ..) => some ⟨.leak, term, .leakPq true, some j⟩
  | _ => none

def trExposureAtL310–316 ↗#

def trExposureAt (tr' : ExecTrace) (j : Nat) : Option VisEntry :=
  let term := (tr'.getMessageSentAt (j + 1)).toList
  match tr'.getEventAt TREvent j with
  | some (.ExposedRK ..) | some (.ExposedDHs ..) | some (.ExposedCKs ..)
  | some (.ExposedCKr ..) | some (.ExposedMK ..) | some (.ExposedSpqr ..) =>
    some ⟨.leak, term, .leakRecord, some j⟩
  | _ => none

def exposuresL318–319 ↗#

def exposures (tr tr' : ExecTrace) : List VisEntry :=
  (newIndices tr tr').filterMap (pqExposureAt tr') ++ (newIndices tr tr').filterMap (trExposureAt tr')

structure ProtocolSetupL321–335 ↗#

Provisioned setup parameters: Alice and Bob identities, registration and prekey IDs, Bob's 3169-byte Kyber secret key, and concrete bytes for setup draws (fresh) and opaque public terms (opaqueBytes).

structure ProtocolSetup where
  alice : Participant
  bob : Participant
  withOpk : Bool
  regIdA : BitVec 32
  regIdB : BitVec 32
  spkId : BitVec 32
  kpkId : BitVec 32
  opkId : BitVec 32
  kyberSecB : HwBytes
  fresh : Nat → Nat → HwBytes
  opaqueBytes : DY.Bytes → HwBytes

def setupTraceL337–338 ↗#

Initial model trace produced by running setupAct on the empty trace.

def setupTrace (r : ProtocolSetup) : ExecTrace := ((setupAct r.alice r.bob r.withOpk).run Trace.nil).2.val

def setupRandomsL340 ↗#

def setupRandoms (r : ProtocolSetup) : List DY.Bytes := (newRandoms Trace.nil (setupTrace r)).map (·.1)

def setupSentL342–343 ↗#

def setupSent (r : ProtocolSetup) : List DY.Bytes :=
  (newIndices Trace.nil (setupTrace r)).filterMap fun i => (setupTrace r).getMessageSentAt i

def setupSecretL345 ↗#

def setupSecret (r : ProtocolSetup) (k : Nat) : DY.Bytes := ((setupRandoms r)[k]?).getD (randTerm 0 0)

def setupPublicL347 ↗#

def setupPublic (r : ProtocolSetup) (k : Nat) : DY.Bytes := ((setupSent r)[k]?).getD (randTerm 0 0)

def ecKeyL349 ↗#

def ecKey (b : HwBytes) : HwBytes := 0x05#8 :: b

def kyberKeyL351 ↗#

def kyberKey (b : HwBytes) : HwBytes := 0x08#8 :: b

def pubBytesL353–355 ↗#

X25519 public key bytes computed from clamped private key bytes b.

def pubBytes (interpretation : ExternInterpretation) (b : HwBytes) : HwBytes :=
  (interpretation x25519PublicKeySymbol [clamp b]).getD []

def setupRandomsAtL357–359 ↗#

def setupRandomsAt (r : ProtocolSetup) : List (Nat × Nat) :=
  (newIndices Trace.nil (setupTrace r)).filterMap fun i =>
    ((setupTrace r).at? i : Option DY.Random.ExecEntryT).map fun e => (i, e.length)

def secretBytesL361–362 ↗#

def secretBytes (r : ProtocolSetup) (k : Nat) : HwBytes :=
  (((setupRandomsAt r)[k]?).map fun p => r.fresh p.1 p.2).getD []

namespace ProtocolSetup

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

DY.Libsignal.Composed.Refinement.ProtocolSetup.ikASecTerm

def ikBSecTermL367 ↗#

def ikBSecTerm (r : ProtocolSetup) : DY.Bytes := setupSecret r 1

def spkSecTermL368 ↗#

def spkSecTerm (r : ProtocolSetup) : DY.Bytes := setupSecret r 2

def pqskSecTermL369 ↗#

def pqskSecTerm (r : ProtocolSetup) : DY.Bytes := setupSecret r 4

def opkSecTermL370 ↗#

def opkSecTerm (r : ProtocolSetup) : DY.Bytes := setupSecret r 6

def ikAPubTermL372 ↗#

def ikAPubTerm (r : ProtocolSetup) : DY.Bytes := setupPublic r 0

def ikBPubTermL373 ↗#

def ikBPubTerm (r : ProtocolSetup) : DY.Bytes := setupPublic r 2

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

DY.Libsignal.Composed.Refinement.ProtocolSetup.spkPubTerm

def spkSigTermL375 ↗#

def spkSigTerm (r : ProtocolSetup) : DY.Bytes := setupPublic r 5

def pqpkPubTermL376 ↗#

def pqpkPubTerm (r : ProtocolSetup) : DY.Bytes := setupPublic r 6

def pqpkSigTermL377 ↗#

def pqpkSigTerm (r : ProtocolSetup) : DY.Bytes := setupPublic r 7

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

DY.Libsignal.Composed.Refinement.ProtocolSetup.opkPubTerm

def ikASecBytesL380 ↗#

def ikASecBytes (r : ProtocolSetup) : HwBytes := secretBytes r 0

def ikBSecBytesL381 ↗#

def ikBSecBytes (r : ProtocolSetup) : HwBytes := secretBytes r 1

def spkSecBytesL382 ↗#

def spkSecBytes (r : ProtocolSetup) : HwBytes := secretBytes r 2

def opkSecBytesL383 ↗#

def opkSecBytes (r : ProtocolSetup) : HwBytes := secretBytes r 6

end ProtocolSetup

def storedStatesL387–389 ↗#

def storedStates (r : ProtocolSetup) (tr : ExecTrace) :
    List (PersistentLocalState.LocalState TRState) :=
  (newIndices (setupTrace r) tr).filterMap (tr.getLocalStateAt TRState)

def sessionHasDecryptedL391–396 ↗#

Whether session s has decrypted any incoming message before stateIdx.

def sessionHasDecrypted (tr : ExecTrace) (s : TripleRatchet.SessionInfo) (stateIdx : Nat) : Bool :=
  (List.range stateIdx).any fun j =>
    match tr.getEventAt TREvent j with
    | some (.MessageKey s' .receiver ..) => decide (s' = s)
    | _ => false

def pendingPreKeyL398–409 ↗#

Pending (ek, ct) pre-key items for an Alice session at stateIdx prior to decrypting a reply (none once acknowledged or for Bob sessions).

def pendingPreKey (tr : ExecTrace) (stateIdx : Nat) : Option (DY.Bytes × DY.Bytes) :=
  match tr.getLocalStateAt TRState stateIdx with
  | some ls =>
    let s0 := ls.state.sessionInfo ls.participant
    if sessionHasDecrypted tr s0 stateIdx then none
    else
      (sessionHandshakeEvents tr s0).findSome? fun
        | .AliceDone _ _ _ _ _ _ _ ek ct _ => some (ek, ct)
        | _ => none
  | none => none

def encSendEntryL411–420 ↗#

Observable send entry of an encryption step on stateIdx, matching wrapped against pendingPreKey tr stateIdx.

def encSendEntry (tr tr' : ExecTrace) (stateIdx : Nat) (wrapped : Bool) : List VisEntry :=
  match lastSent tr tr' with
  | some w =>
    match wrapped, pendingPreKey tr stateIdx with
    | true, some (ek, ct) => [⟨.send, [ek, ct, w], .preKeySend, none⟩]
    | false, none => [⟨.send, [w], .whisper, none⟩]
    | _, _ => []
  | none => []

def stepViewL422–437 ↗#

Observable VisEntry sequence emitted by running s from tr (suppressing send and accept entries when s.ok tr = false).

def stepView (s : Step) (tr : ExecTrace) (wrapped : Bool) : List VisEntry :=
  let tr' := s.next tr
  let own : List VisEntry :=
    match s with
    | .aliceStart _ _ _ _ h => aliceVis tr tr' h
    | .bobStart b _ kh _ mh _ _ => bobVis tr tr' mh (bobOpkPk b kh tr)
    | .messageEncrypt _ stateIdx .. =>
      encDraws (newRandoms tr tr') ++ encSendEntry tr tr' stateIdx wrapped
    | .messageEncryptAbort .. => encDraws (newRandoms tr tr')
    | .messageDecrypt _ stateIdx msgIdx .. => decVis tr tr' stateIdx msgIdx wrapped
    | .messageDecryptSkipped _ stateIdx msgIdx .. => decVis tr tr' stateIdx msgIdx wrapped
    | _ => []
  (if s.ok tr then own else own.filter fun v => v.kind != .send && v.kind != .accept) ++
    exposures tr tr'

def runStepsL439–441 ↗#

def runSteps : List Step → ExecTrace → ExecTrace
  | [], tr => tr
  | s :: ss, tr => runSteps ss (s.next tr)

def runTraceL443–444 ↗#

Trace produced by running ss starting from setupTrace r.

def runTrace (r : ProtocolSetup) (ss : List Step) : ExecTrace := runSteps ss (setupTrace r)

def encryptOwnSpqrKeyIdxL446–447 ↗#

Trace handle at which messageEncrypt run from tr publishes its SPQR send key.

def encryptOwnSpqrKeyIdx (tr : ExecTrace) : Nat := tr.length + 2

def encryptAbortAfterSpqrIdxL449–451 ↗#

Out-of-range pqIdx handle modeling an spqr::send failure after coin draw and key publication.

def encryptAbortAfterSpqrIdx (tr : ExecTrace) : Nat := tr.length + 3

def Step.publishedSpqrKey?L453–459 ↗#

SPQR send key published by a non-aborting messageEncrypt step s on tr.

def Step.publishedSpqrKey? (s : Step) (tr : ExecTrace) : Option DY.Bytes :=
  match s with
  | .messageEncrypt _ _ _ pqIdx =>
    if pqIdx = encryptAbortAfterSpqrIdx tr then none
    else (s.next tr).getMessageSentAt (encryptOwnSpqrKeyIdx tr)
  | _ => none

def Step.LocalOkL461–473 ↗#

Step-local refinement invariants on s at tr: exposures target current snapshots/chains, and messageEncrypt draws coinsLen ∈ {0, 32, 64} and reads its own SPQR key handle (or aborts via encryptAbortAfterSpqrIdx tr).

def Step.LocalOk (s : Step) (tr : ExecTrace) : Prop :=
  match s with
  | .exposeKey _ stateIdx _ | .exposeSpqr _ stateIdx =>
    TripleRatchet.isCurrentSnapshot tr stateIdx = true
  | .exposeSkipped skIdx =>
    TripleRatchet.isSkippedChainCurrent tr skIdx = true
  | .messageEncrypt _ _ coinsLen pqIdx =>
    (coinsLen = 0 ∨ coinsLen = 32 ∨ coinsLen = 64) ∧
      (pqIdx = encryptOwnSpqrKeyIdx tr ∨ pqIdx = encryptAbortAfterSpqrIdx tr)
  | _ => True

def StepsWFL475–477 ↗#

def StepsWF : List Step → ExecTrace → Prop
  | [], _ => True
  | s :: ss, tr => s.PreCond tr ∧ s.LocalOk tr ∧ StepsWF ss (s.next tr)

def Step.stateLoad?L479–485 ↗#

(me, stateIdx, storesSuccessor) for steps that load a stored TRState snapshot.

def Step.stateLoad? : Step → Option (Participant × Nat × Bool)
  | .messageEncrypt me stateIdx .. => some (me, stateIdx, true)
  | .messageEncryptAbort me stateIdx => some (me, stateIdx, false)
  | .messageDecrypt me stateIdx .. => some (me, stateIdx, true)
  | .messageDecryptSkipped me stateIdx .. => some (me, stateIdx, true)
  | _ => none

def StepsStateFaithfulL487–494 ↗#

Linear consumption of stored session snapshots: once a step loads snapshot k and succeeds in storing a successor, no later step loads k.

def StepsStateFaithful (r : ProtocolSetup) (ss : List Step) : Prop :=
  ∀ (i j : Nat) (si sj : Step) (p : Participant) (k : Nat) (b : Bool), i < j →
    ss[i]? = some si → ss[j]? = some sj →
    si.stateLoad? = some (p, k, true) →
    si.ok (runTrace r (ss.take i)) = true →
    sj.stateLoad? = some (p, k, b) → False

def ModelRunWFL496–505 ↗#

Faithful model run ss from ProtocolSetup r: setup draws succeed and are reachable, every step satisfies PreCond and LocalOk, and stored session snapshots are consumed linearly.

def ModelRunWF (r : ProtocolSetup) (ss : List Step) : Prop :=
  (setupRandoms r).length = (if r.withOpk then 7 else 6) ∧
  (setupTrace r).Reachable reachability ∧
  StepsWF ss (setupTrace r) ∧
  StepsStateFaithful r ss

end DY.Libsignal.Composed.Refinement