Subprocess

Safe-by-construction bindings around Python's ``subprocess`` module. ``subprocess`` is one of the most error-prone corners of the standard library, in two distinct ways: 1. **Shell injection.** ``subprocess.run("rm " + name, shell=True)`` hands an attacker-controlled string to ``/bin/sh``. The fix is to pass an *argument vector* (a list) and never invoke a shell — so there is no shell grammar to inject into. This binding exposes *only* the argv form: every entry point takes an ``Array String`` and runs it directly. There is deliberately no ``shell=True`` escape hatch. 2. **Ignored exit codes.** ``subprocess.run`` does not raise on failure; callers routinely read ``stdout`` of a command that never ran. Here the return code is reflected into an uninterpreted ``exitCode`` measure, and ``checkRun`` carries the postcondition ``exitCode p = 0`` so downstream code can rely — at the type level — on the command having succeeded. An ``Array String`` is backed by a Python ``list[str]`` at runtime, so it flows straight into ``subprocess.run`` with no marshalling.
Imports
open Array;
Table of Contents

Types

CompletedProcess

(type)
type CompletedProcess

Process

(type)
type Process

Functions

subprocess

def subprocess : Unit

run

Runs ``argv`` and captures its output. ``argv`` must be non-empty — its first element is the program to execute. No shell is involved.
def run (1 argv : Array String | Array.size argv ≥ 1) : CompletedProcess

runWithInput

Runs ``argv``, feeding ``stdin`` to the child's standard input.
def runWithInput (1 argv : Array String | Array.size argv ≥ 1) (stdin : String) : CompletedProcess

runWithTimeout

Runs ``argv`` but aborts the child after ``seconds``. Raises ``TimeoutExpired`` if the deadline passes; ``seconds`` must be positive.
def runWithTimeout (1 argv : Array String | Array.size argv ≥ 1) (seconds : Float | seconds > 0.0) : CompletedProcess

checkRun

Runs ``argv`` and raises ``CalledProcessError`` on a non-zero exit. Because control only returns here on success, the result is statically known to have ``exitCode p = 0`` — callers can read ``stdout`` without re-checking.
def checkRun (1 argv : Array String | Array.size argv ≥ 1) : {p : CompletedProcess | exitCode p = 0}

checkOutput

def checkOutput (1 argv : Array String | Array.size argv ≥ 1) : String

getExitCode

The exit code as a value, pinned to the ``exitCode`` measure so it can be threaded into later refinements.
def getExitCode (p : CompletedProcess) : {n : Int | n = exitCode p}

succeeded

True exactly when the command succeeded (exit code 0). The result is tied to the ``exitCode`` measure, so the ``then`` branch of a test on it can satisfy preconditions phrased as ``exitCode p = 0``.
def succeeded (p : CompletedProcess) : {b : Bool | b = exitCode p = 0}

stdout

Captured standard output (decoded text).
def stdout (p : CompletedProcess) : String

stderr

Captured standard error (decoded text).
def stderr (p : CompletedProcess) : String

spawn

Spawns a child running `argv` and returns immediately, without waiting. Bind the result to a linear binder. `argv` must be non-empty; no shell is involved.
def spawn (1 argv : Array String | Array.size argv ≥ 1) : Process

wait

Blocks until the child exits, reaps it, and returns its exit code. Consumes the handle, so the same process cannot be waited on twice or leaked.
def wait (1 p : Process) : Int

waitFor

Like `wait` but gives up after `seconds` (> 0), raising `TimeoutExpired`.
def waitFor (seconds : Float | seconds > 0.0) (1 p : Process) : Int

terminate

Sends SIGTERM, waits for the child to exit, and returns its exit code. Consumes the handle.
def terminate (1 p : Process) : Int

kill

Sends SIGKILL, waits, and returns the exit code. Consumes the handle.
def kill (1 p : Process) : Int

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

exitCode

uninterpreted
The process exit status. Uninterpreted: the solver only relates it across calls (e.g. a ``checkRun`` result is pinned to 0), it never computes it. On POSIX a negative value means the process was killed by ``-exitCode``.
def exitCode : (p : CompletedProcess) → Int