Instance.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 26 of 63 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.

Concrete Composed Protocol Instances

Concrete 12-theory term algebra (HasExecBytes) and 7-entry trace (HasExecTrace) instances for DY.Libsignal.Composed.

@[expose] public section

namespace DY.Libsignal.Composed

#combineL26–38 ↗#

#combine +toplevel into BytesFunctor, BytesLength, attackerKnowledge from
  Random,
  Literal,
  Concat,
  DiffieHellman,
  KdfExtract,
  SymEnc,
  Trunc,
  X25519,
  PQKem,
  Signature,
  Spqr,
  TrWire,

instanceL40 ↗#

instance: HasExecBytes where

end DY.Libsignal.Composed

namespace DY.Libsignal.Composed

open PQXDH (PQXDHState PQXDHEvent)

open TripleRatchet (TRState TREvent)

#combineL49–59 ↗#

#combine +toplevel into
  ExecEntryT,
  baseAttackerKnowledge,
from
  Network,
  Random,
  ProtocolEvent TREvent,
  ProtocolEvent PQXDHEvent,
  ProtocolEvent ComposedEvent,
  PersistentLocalState.CompromisableState TRState,
  PersistentLocalState.CompromisableState PQXDHState,

instanceL61 ↗#

instance: HasExecTrace where

end DY.Libsignal.Composed