MachineEvents.lean🔗

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

Cited in the paper

Hardware Events, §B.2: RunEvent, EnvEvent

Concrete Byte Strings and CLI Trace Events

Concrete byte strings (HwBytes) and the event alphabet (CliEvent) for signal-session CLI execution traces.

@[expose] public section

namespace DY.Libsignal

abbrev HwBytesL26–27 ↗#

Concrete byte string, as opposed to symbolic DY.Bytes terms.

abbrev HwBytes := List (BitVec 8)

end DY.Libsignal

namespace DY.Libsignal.HwEvents

open DY (Participant)

open CryptoVerification.SignalSession (Cmd)

structure RunEventL36–43 ↗#

One signal-session CLI invocation: caller party, command cmd, input bytes (bundle blob for init, stdin otherwise), coins file, and exit (some (code, stdout) or none on abort).

structure RunEvent where
  party : Participant
  cmd : Cmd
  input : HwBytes
  coins : HwBytes
  exit : Option (Nat × HwBytes)

inductive EnvEventL45–53 ↗#

Environment events emitted between CLI runs: directory secret leaks, primitive breaks, public-key inversions, and corrupt identity registrations.

inductive EnvEvent where
  | leak (party : Participant) (secret : HwBytes)
  | breakDH
  | breakKEM
  | invertDH (pk sk : HwBytes)
  | invertKEM (pk sk : HwBytes)
  | registerCorrupt (party : Participant) (ikPk : HwBytes)

def EnvEvent.IsBreakInvertL55–58 ↗#

Whether an environment event is a primitive break or key inversion.

def EnvEvent.IsBreakInvert : EnvEvent → Prop
  | .breakDH | .breakKEM | .invertDH .. | .invertKEM .. => True
  | .leak .. | .registerCorrupt .. => False

inductive CliEventL60–62 ↗#

inductive CliEvent where
  | run (e : RunEvent)
  | env (e : EnvEvent)

end DY.Libsignal.HwEvents