OS

Safe-by-construction bindings around Python's ``os`` module. ``os`` is full of *partial* operations — calls that look innocent but blow up at runtime on a bad input: * ``os.environ[k]`` raises ``KeyError`` when ``k`` is unset; * ``os._exit(code)`` silently truncates ``code`` to a single byte; * ``os.kill(pid, sig)`` needs a live PID and a real signal number; * ``os.path.getsize(p)`` raises ``OSError`` on a missing path. This library attaches Liquid Types so the common mistakes become *compile* errors instead of runtime crashes. The headline is environment access: ``getEnv`` is only callable once the solver knows — via ``hasEnv`` — that the variable is set, mirroring the ``exists``/``read_text`` pattern in ``Path.ae``. See ``Sys.ae`` for the ``sys``-module companion (argv, stdin/stdout, the cleanup-running ``sys.exit``).
Imports
open Array; open Map; open Maybe;
Table of Contents

Functions

os

def os : Unit

hasEnv

Runtime witness: lifts environment membership into the type system. In the ``then`` branch of ``if hasEnv name then ...`` the solver learns ``envSet name``, which is exactly what ``getEnv`` requires.
def hasEnv (name : String | name ≠ "") : {b : Bool | b = envSet name}

getEnv

Unchecked lookup. The precondition ``envSet name`` makes a ``KeyError`` unrepresentable — you can only reach this call after testing ``hasEnv``.
def getEnv (name : String | name ≠ "" && envSet name) : String

getEnvOr

Total lookup with an explicit fallback; always safe to call.
def getEnvOr (name : String | name ≠ "") (fallback : String) : String

setEnv

Sets a variable and hands the value back so it can be threaded.
def setEnv (name : String | name ≠ "") (value : String) : String

unsetEnv

Removes a variable if present; a no-op when it is unset (so, KeyError-safe).
def unsetEnv (name : String | name ≠ "") : Unit

environ

A snapshot of the whole environment as a Map.
def environ (_ : Unit) : Map String String

getPid

The current process id. Always positive.
def getPid (_ : Unit) : {p : Int | p > 0}

getParentPid

The parent process id. Positive on every supported platform.
def getParentPid (_ : Unit) : {p : Int | p > 0}

cpuCount

Number of CPUs in the system, if the OS can report it. ``os.cpu_count()`` may return ``None``, so the result is a ``Maybe`` rather than a bare ``Int`` — forcing callers to handle the unknown case instead of dividing by it.
def cpuCount (_ : Unit) : Maybe Int

getCwd

The current working directory. Always non-empty.
def getCwd (_ : Unit) : {s : String | s ≠ ""}

chdir

Changes the working directory. The path must be non-empty; raises if it does not exist or is not a directory.
def chdir (path : String | path ≠ "") : Unit

pathExists

True if ``path`` refers to something that exists.
def pathExists (path : String | path ≠ "") : Bool

isFile

True if ``path`` is an existing regular file.
def isFile (path : String | path ≠ "") : Bool

isDir

True if ``path`` is an existing directory.
def isDir (path : String | path ≠ "") : Bool

fileSize

Size of a file in bytes. Non-negative. Raises if the path is missing.
def fileSize (path : String | path ≠ "") : {n : Int | n ≥ 0}

kill

Sends signal ``sig`` to process ``pid``. ``pid`` must be positive and ``sig`` a positive signal number. Raises if the process does not exist or you lack permission.
def kill (pid : Int | pid > 0) (sig : Int | sig > 0) : Unit

exitNow

Immediately terminates the process with a status byte, skipping cleanup handlers (the right call after ``fork()``). The portable status range is 0..255; values outside it wrap around at the OS level, so the refinement keeps the exit code honest. For a normal shutdown that runs ``atexit`` handlers, use ``Sys.exit`` instead.
def exitNow (code : Int | code ≥ 0 && code ≤ 255) : Unit

Uninterpreted

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

envSet

uninterpreted
def envSet : (name : String) → Bool