Process.lean🔗

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

@[expose] public section

set_option autoImplicit false

namespace CryptoVerification.SignalSession

open Arm64 Arm64.Process

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

CryptoVerification.SignalSession.ProcessResult.exited, CryptoVerification.SignalSession.ProcessResult.aborted, CryptoVerification.SignalSession.ProcessResult

def processInputsL48–67 ↗#

The inputs of one run: the argument vector argv (argv[0] included, ASCII), the bytes stdin on file descriptor 0, the regular files files and the directories dirs that exist at the start, with paths relative to the process's working directory (the party's). The stack is 8 MiB, Linux's default RLIMIT_STACK, instead of the engine's default 128 KiB (DEV-CLI7). Every other field is the engine's default (ProcessInputs); execfn is [], so AT_EXECFN points to "" (Linux passes the execve path); the only reader is musl's __init_libc, which uses it for __progname only when argv[0] is null, and argv[0] is always "libsignal-cli" here (and __progname is never read); auxv.hwcap is 0x3 (FP bit 0 and ASIMD bit 1 only; AES bit 3 and PMULL bit 4 are 0, see DEV-CLI10); in particular auxv keeps AuxvConfig's non-setuid ids and the loader sets AT_SECURE = 0 (DEV-CLI6).

def processInputs (argv : List String) (stdin : List (BitVec 8))
    (files : List (String × List (BitVec 8))) (dirs : List String) : ProcessInputs :=
  { argv := argv.map bytesOfString
    stdin := stdin
    files := files
    dirs := dirs
    init := { stackSize := 8388608 } }

end CryptoVerification.SignalSession