CliProcess.lean🔗

Tier 2 · definitions used by the symbolic proof 2 headline theorems depend on it 21 of 58 lines trusted trust banner B2, trusted: definitions used by the statement 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.

@[expose] public section

set_option autoImplicit false

namespace CryptoVerification.SignalSession

open Arm64 Arm64.Process

def sigAbrtL31–32 ↗#

SIGABRT, the signal of musl's abort (6).

def sigAbrt : BitVec 7 := 6#7

def abortOnPanicL34–40 ↗#

Run hook h; if it panicked (.Panicked), report the panic as death by SIGABRT (.Signaled 6, exit status 134). Every other result of h is unchanged.

def abortOnPanic (h : State → State) (s : State) : State :=
  let s' := h s
  match s'.status with
  | .Panicked => s'.setStatus (.Signaled sigAbrt)
  | _ => s'

def OutcomeMatchesProcessL43–50 ↗#

The engine's outcome observes o: exited code stdout files is a normal exit (no signal) whose exit code has low byte code, with stdout stdout and the regular files files (fsView); aborted is death by SIGABRT (signal = some 6, exit status 134).

def OutcomeMatchesProcess : Outcome → ProcessOutcome → Prop
  | .exited code stdout files, out =>
      out.signal = none ∧ out.exitCode.toNat % 256 = code ∧ out.stdout = stdout ∧
        fsView out.fs = files
  | .aborted, out => out.signal = some 6 ∧ out.exitCode = 134#64

def cliProcessInputsL52–59 ↗#

The process inputs of a run on i: argv = "libsignal-cli" :: i.argv, and i's stdin, files and directories, with an 8 MiB stack (processInputs, Process.lean; DEV-CLI7).

def cliProcessInputs (i : Inputs) : ProcessInputs :=
  processInputs ("libsignal-cli" :: i.argv) i.stdin i.files i.dirs

end CryptoVerification.SignalSession