CliRun.lean🔗

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

Declarations on this page (17)

@[expose] public section

set_option autoImplicit false

namespace CryptoVerification.SignalSession

open Arm64 Arm64.Process ProofLib

Paths

def readPathL194–197 ↗#

The path argument (ptr, len) of an I/O function as an FsState.files key: one character per byte (Char.ofNat), as the engine reads a path of openat (readCString, ISA/Eval.lean).

def readPath (m : Memory) (ptr len : BitVec 64) : String :=
  String.ofList ((m.readBytes ptr len.toNat).map fun b => Char.ofNat b.toNat)

def pathCompsL199–201 ↗#

The components of path p: its characters split at / (List.splitOn). On a PathOk path they are the segments of the engine's canonical form (Arm64.normalizePath).

def pathComps (p : String) : List (List Char) := p.toList.splitOn '/'

def isUnmodelledPathComponentL203–205 ↗#

A component the specifications do not model: empty (a leading, trailing or doubled /, or the empty path), . or ...

def isUnmodelledPathComponent (c : List Char) : Bool := c.isEmpty || c == ['.'] || c == ['.', '.']

def PathOkL207–216 ↗#

The paths the I/O specifications model: relative and canonical (every component non-empty and neither . nor ..), no NUL byte (Rust's CString would reject it), and no component that fsView hides (stdioPaths, Run.lean), so every file a hook reads or writes is observable. The standard streams themselves are not in the file system (FsState.files): the loader opens file descriptors 0, 1, 2 as .stdio descriptors, and stdin's bytes are FsState.stdin. On such paths the engine's canonical lookup (FsState.files) agrees with the way Linux resolves them.

def PathOk (p : String) : Bool :=
  (pathComps p).all fun c =>
    !isUnmodelledPathComponent c && !c.contains '\x00' && !(stdioPaths.contains (String.ofList c))

def ancestorsL218–222 ↗#

The proper ancestors of p, shallowest first: "a/b/c" gives ["a", "a/b"]; a single component has none (its parent is the party's directory, which exists).

def ancestors (p : String) : List String :=
  let cs := pathComps p
  (List.range (cs.length - 1)).map fun i => String.ofList (['/'].intercalate (cs.take (i + 1)))

def blockingAncestor?L224–229 ↗#

The first proper ancestor of p that is not a directory, with what is there: some (some (.file _)) (Linux: ENOTDIR) or some none (missing: ENOENT); none if every proper ancestor is a directory. This is Linux's walk of the path's directories (link_path_walk).

def blockingAncestor? (fs : FsState) (p : String) : Option (Option FsEntry) :=
  ((ancestors p).find? fun q => match fs.files q with | some .dir => false | _ => true).map
    fs.files

3 declarations not shown (lines 233–267): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.SignalSession.vecErr, CryptoVerification.SignalSession.vecEmptyOk, CryptoVerification.SignalSession.vecOk

def unitResultL269–272 ↗#

Return Ok(()) (x0 := 0) or Err(IoError) (x0 := 1) of a Result<(), IoError> (measured on the compiled write_file / write_stdout: cset w0, ne).

def unitResult (ok : Bool) : State → State :=
  retHook fun s => s.writeReg64 .x0 (if ok then 0#64 else 1#64)

def unmodelledL274–276 ↗#

Stop with an .Exception (outcomeOf is then none): the hook's inputs are outside what it models.

def unmodelled (msg : String) (s : State) : State := s.setStatus (.Exception msg)

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

CryptoVerification.SignalSession.readFileHook

def writeFileHookL310–345 ↗#

libsignal_cli_io::write_file(path: &str = (x0, x1), bytes: &[u8] = (x2, x3)) -> Result<(), IoError> (x0): 0-allocation C-ABI musl open/write/close/__errno_location loop (O_WRONLY | O_CREAT | O_TRUNC | O_CLOEXEC, mode 0o666, < 4096-byte NUL-free stack path copy, EINTR retry on open and write, n == 0 treated as Err, close on every exit after open), i.e. create or truncate, then write all of bytes.

.Exception if the path or the bytes are not readable, or (after the length / interior-NUL check) the path is not PathOk;
path byte length ≥ cliPathMaxBytes (4096, PATH_MAX) or containing an interior 0 byte: Err (unitResult false, before openat and before emitting TraceEvent.fileChanged);
a proper ancestor is not a directory (a regular file: ENOTDIR; missing: ENOENT, the CLI never creates a directory): Err, nothing changes in fs.files;
fs.files path is a directory: Err (EISDIR), nothing changes in fs.files;
otherwise (a regular file, or nothing): fs.files path := file bytes, Ok. In the three PathOk < 4096-byte cases it first appends the event TraceEvent.fileChanged p to the trace (not output; module docstring).

def writeFileHook (s : State) : State :=
  let ptr := s.readReg64 .x0
  let len := s.readReg64 .x1
  let buf := s.readReg64 .x2
  let n := s.readReg64 .x3
  if !(s.mem.canRead ptr len.toNat && s.mem.canRead buf n.toNat) then
    unmodelled "write_file: unreadable path or bytes" s
  else
    let raw := s.mem.readBytes ptr len.toNat
    if cliPathMaxBytes ≤ len.toNat || raw.contains 0#8 then
      unitResult false s
    else
      let p := readPath s.mem ptr len
      if !PathOk p then unmodelled "write_file: path outside the model" s
      else
        let s := s.appendTrace [.fileChanged p]
        match blockingAncestor? s.fs p, s.fs.files p with
        | some _, _ => unitResult false s
        | none, some .dir => unitResult false s
        | none, _ =>
          unitResult true (s.setFs (s.fs.setFile p (some (.file (s.mem.readBytes buf n.toNat)))))

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

CryptoVerification.SignalSession.readStdinHook

def writeStdoutHookL366–377 ↗#

libsignal_cli_io::write_stdout(bytes: &[u8] = (x0, x1)) -> Result<(), IoError> (x0): 0-allocation C-ABI musl write(1, …) / __errno_location loop (EINTR retry, n == 0 treated as Err, and EBADF on a closed file descriptor 1 treated as Ok(()) matching std's handle_ebadf and read_stdin; in processInputs file descriptor 1 is open .stdio stdout), i.e. the engine's write(1, …), which appends the bytes to the trace as stdout events (TraceEvent.ofBytes .stdout) and leaves the file system unchanged. Ok. .Exception if the bytes are not readable.

def writeStdoutHook (s : State) : State :=
  let buf := s.readReg64 .x0
  let n := s.readReg64 .x1
  if !s.mem.canRead buf n.toNat then unmodelled "write_stdout: unreadable bytes" s
  else unitResult true (s.appendTrace (TraceEvent.ofBytes .stdout (s.mem.readBytes buf n.toNat)))

CLI-specific extern hooks

def strlenHookL381–389 ↗#

strlen(s = x0) -> size_t (x0): the least n such that the bytes [s, s + n] are readable and byte s + n is 0. .Exception if there is none (a real strlen faults or runs on). Caller: CStr::from_ptr on each argument of argv, which the loader writes NUL-terminated.

open Classical in
noncomputable def strlenHook (s : State) : State :=
  let p := s.readReg64 .x0
  if h : ∃ n, s.mem.canRead p (n + 1) = true ∧ s.mem.read8 (p + BitVec.ofNat 64 n) = 0#8 then
    retHook (fun s => s.writeReg64 .x0 (BitVec.ofNat 64 (Nat.find h))) s
  else unmodelled "strlen: no readable NUL" s

def memrchrHookL391–405 ↗#

core::slice::memchr::memrchr(x: u8 = w0, text: &[u8] = (x1, x2)) -> Option<usize> (x0 = tag, x1 = value): Some(i) (x0 := 1, x1 := i) for the largest i < len with text[i] = x (x: the low byte of x0), else None (x0 := 0, x1 unchanged). .Exception if the bytes are not readable. Caller: rsplit_once('.') in address (cli/src/lib.rs), which tests x0 = 1.

def memrchrHook (s : State) : State :=
  let x := (s.readReg64 .x0).setWidth 8
  let ptr := s.readReg64 .x1
  let len := s.readReg64 .x2
  if !s.mem.canRead ptr len.toNat then unmodelled "memrchr: unreadable bytes" s
  else
    let bs := s.mem.readBytes ptr len.toNat
    match ((List.range bs.length).filter fun i => bs[i]? == some x).getLast? with
    | some i => retHook (fun s => (s.writeReg64 .x0 1#64).writeReg64 .x1 (BitVec.ofNat 64 i)) s
    | none => retHook (fun s => s.writeReg64 .x0 0#64) s

def Utf8OkL407–412 ↗#

bs is well-formed UTF-8: the UTF-8 encoding (String.utf8EncodeChar, shortest form) of some list of Unicode scalar values (Char: no surrogates, at most U+10FFFF). This is Rust's definition (core::str::from_utf8); equivalently ∃ s : String, s.toUTF8.toList = bs up to UInt8.toBitVec.

def Utf8Ok (bs : List (BitVec 8)) : Prop :=
  ∃ cs : List Char, (cs.flatMap String.utf8EncodeChar).map UInt8.toBitVec = bs

def fromUtf8HookL414–435 ↗#

core::str::converts::from_utf8(v: &[u8] = (x0, x1)) -> Result<&str, Utf8Error> (sret x8, 24 bytes): if the bytes are well-formed UTF-8 (Utf8Ok), Ok(v): tag 0 @0, x0 @8, x1 @16. Otherwise Err: tag 1 @0, then err bs = (valid_up_to, error_len), a free choice, as the word @8 and the 16-bit field @16. .Exception if the bytes are not readable or the sret not writable. (Measured on the compiled from_utf8: str xzr, [x8]; stp x0, x1, [x8, #8] and str x9(=1), [x8]; str x9, [x8, #8]; strb, strb [x8, #16..17].)

open Classical in
noncomputable def fromUtf8Hook (err : List (BitVec 8) → BitVec 64 × BitVec 16) (s : State) :
    State :=
  let ptr := s.readReg64 .x0
  let len := s.readReg64 .x1
  let r := s.readReg64 .x8
  if !(s.mem.canRead ptr len.toNat && s.mem.canWrite r 24) then
    unmodelled "from_utf8: unreadable bytes or unwritable result" s
  else
    let bs := s.mem.readBytes ptr len.toNat
    if Utf8Ok bs then
      retHook (fun s => s.setMem (((s.mem.write64 r 0#64).write64 (r + 8#64) ptr).write64
        (r + 16#64) len)) s
    else
      retHook (fun s => s.setMem (((s.mem.write64 r 1#64).write64 (r + 8#64) (err bs).1).write16
        (r + 16#64) (err bs).2)) s

def durationSinceExactHookL437–464 ↗#

<SystemTime>::duration_since(&self = x0, earlier = (x1 = tv_sec, w2 = tv_nsec)) -> Result<Duration, SystemTimeError> (sret x8), exactly std's Timespec::sub_timespec. With t1 = self (tv_sec: i64 @0, tv_nsec: u32 @8) and t2 = earlier, each read as tv_sec · 10^9 + tv_nsec nanoseconds (an integer), and d = |t1 - t2|: tag @0 = 0 (Ok) if t1 ≥ t2, else 1 (Err); the Duration (d / 10^9, d % 10^9) as secs: u64 @8 and nanos: u32 @16. .Exception if self's 12 bytes are not readable, the 24 sret bytes are not writable, or a tv_nsec is ≥ 10^9 (not a Timespec: undefined behaviour in Rust). (Measured on the compiled duration_since / sub_timespec: ldr x9, [x1]; ldr w12, [x1, #8] with self in x1 after mov x1, x9(=x0), earlier stored from x1 / w2; stp xzr, x9, [x19]; str w8, [x19, #16] for Ok, the tag XOR-ed with 1 for Err.) Every call site passes UNIX_EPOCH as earlier.

def durationSinceExactHook (s : State) : State :=
  let a := s.readReg64 .x0
  let r := s.readReg64 .x8
  if !(s.mem.canRead a 12 && s.mem.canWrite r 24) then
    unmodelled "duration_since: unreadable self or unwritable result" s
  else
    let ns1 := (s.mem.read32 (a + 8#64)).toNat
    let ns2 := ((s.readReg64 .x2).setWidth 32).toNat
    if ns1 < 1000000000 ∧ ns2 < 1000000000 then
      let t1 : Int := (s.mem.read64 a).toInt * 1000000000 + ns1
      let t2 : Int := (s.readReg64 .x1).toInt * 1000000000 + ns2
      let d := (t1 - t2).natAbs
      let tag : BitVec 64 := if t2 ≤ t1 then 0#64 else 1#64
      retHook (fun s => s.setMem (((s.mem.write64 r tag).write64 (r + 8#64)
        (BitVec.ofNat 64 (d / 1000000000))).write32 (r + 16#64)
        (BitVec.ofNat 32 (d % 1000000000)))) s
    else unmodelled "duration_since: tv_nsec out of range" s

The free choices and the table

structure CliHooksL468–481 ↗#

What a CLI run is quantified over (the W of cliRunOf elf W and cliRunAbortOnPanic elf W): the abstract primitives and two results the CLI cannot observe.

structure CliHooks where
  /-- SHA-256 compression, AES-256-CBC, X25519 (`CryptoGames.LibsignalSession.Crypto`). -/
  C : CryptoGames.LibsignalSession.Crypto
  /-- SHA-512, the Ed25519 curve core, Kyber1024, SPQR's ML-KEM-768 (`E2E.PqxdhPrims`). -/
  Q : E2E.PqxdhPrims
  /-- `bcmp`'s `x0` on the two compared byte strings. -/
  bcmp : List (BitVec 8) → List (BitVec 8) → BitVec 64
  /-- On equal lengths, the low 32 bits are zero exactly when the strings are equal (C's
  contract). -/
  bcmp_ok : ∀ a b, a.length = b.length → ((bcmp a b).setWidth 32 = 0#32 ↔ a = b)
  /-- `from_utf8`'s `Err` payload `(valid_up_to, error_len)` on ill-formed bytes. -/
  utf8Err : List (BitVec 8) → BitVec 64 × BitVec 16

def cliBcmpHookL483–492 ↗#

bcmp(a = x0, b = x1, n = x2) -> int: x0 := bcmp (n bytes at a) (n bytes at b), return: the function-level (C-ABI) bcmp contract with the value function bcmp. Unlike the CLI-specific hooks above it checks no permission (it does not fail closed): on unreadable bytes it over-approximates, reading them anyway, as the function-level contract does, so that the function-level proofs' bcmp facts transfer unchanged.

def cliBcmpHook (bcmp : List (BitVec 8) → List (BitVec 8) → BitVec 64) : State → State :=
  retHook fun s =>
    let n := (s.readReg64 .x2).toNat
    s.writeReg64 .x0 (bcmp (s.mem.readBytes (s.readReg64 .x0) n)
      (s.mem.readBytes (s.readReg64 .x1) n))

end CryptoVerification.SignalSession