lazaret/tools/lazaret_verify.py

#!/usr/bin/env python3
"""Run Lazaret's repository-owned verification and focused host audits."""

from __future__ import annotations

import argparse
import json
from pathlib import Path
import re
import shutil
import subprocess
import sys
import tempfile
import tomllib

ROOT = Path(__file__).resolve().parent.parent
VERIFICATION_TEMP_ROOT = ROOT / "target" / "verification"
MATERIALIZED_FUSER_MANIFEST = (
    ROOT / ".lazaret/vendor/fuser-0.17.0/Cargo.toml"
).resolve()
MODEL_CONFIGURATIONS = (
    (ROOT / "docs/protocol/Lazaret.tla", ROOT / "docs/protocol/Lazaret.cfg"),
    (
        ROOT / "docs/protocol/IgnoredWorkspaceRouting.tla",
        ROOT / "docs/protocol/IgnoredWorkspaceRouting.cfg",
    ),
    (ROOT / "docs/protocol/PreparedLower.tla", ROOT / "docs/protocol/PreparedLower.cfg"),
)
NEXTEST_COMMAND = (
    "cargo",
    "nextest",
    "run",
    "--offline",
    "--workspace",
    "--all-features",
    "--locked",
    "--filterset",
        (
            "not binary(capability-drop-helper) and not binary(acquisition) "
            "and not binary(state-anchor-lifecycle) and not binary(recovery-process) "
            "and not binary(runtime-composition) and not binary(escalation) "
            "and not binary(prepared-worker) and not binary(nofile) "
            "and not binary(network-runtime)"
        ),
)
DOCTEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "--workspace",
    "--all-features",
    "--locked",
    "--doc",
)
CAPABILITY_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-linux",
    "--test",
    "capability-drop-helper",
    "--locked",
)
ACQUISITION_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-linux",
    "--test",
    "acquisition",
    "--locked",
)
STATE_ANCHOR_LIFECYCLE_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-state-anchor",
    "--test",
    "state-anchor-lifecycle",
    "--locked",
)
RECOVERY_PROCESS_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-host-coordinator",
    "--test",
    "recovery-process",
    "--locked",
)
ESCALATION_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-host-coordinator",
    "--test",
    "escalation",
    "--locked",
)
PREPARED_WORKER_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-host-coordinator",
    "--test",
    "prepared-worker",
    "--locked",
)
NOFILE_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-host-coordinator",
    "--test",
    "nofile",
    "--locked",
)
RUNTIME_COMPOSITION_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-host-coordinator",
    "--test",
    "runtime-composition",
    "--locked",
)
NETWORK_RUNTIME_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "-p",
    "lazaret-runtime-supervisor",
    "--test",
    "network-runtime",
    "--locked",
)
FUSER_PATCH_TEST_COMMAND = (
    "cargo",
    "test",
    "--offline",
    "--locked",
    "--manifest-path",
    ".lazaret/vendor/fuser-0.17.0/Cargo.toml",
    "lock_request_preserves_kind_flags",
)
REQUIRED_TOOL_VERSIONS = (
    ("rustc", ("--version",), (0,), re.compile(r"^rustc 1\.97\.0 ")),
    ("cargo", ("--version",), (0,), re.compile(r"^cargo 1\.97\.0 ")),
    (
        "cargo-nextest",
        ("--version",),
        (0,),
        re.compile(r"^cargo-nextest 0\.9\.140 "),
    ),
    ("cargo-deny", ("--version",), (0,), re.compile(r"^cargo-deny 0\.20\.2$")),
    ("tlc", ("-h",), (0, 1), re.compile(r"Version 2\.19 ")),
    ("uv", ("--version",), (0,), re.compile(r"^uv 0\.11\.28(?: .*)?$")),
)
REQUIRED_DISALLOWED_TYPES = {
    "std::process::Child",
    "std::process::Command",
    "tokio::process::Child",
    "tokio::process::Command",
}
REQUIRED_DISALLOWED_METHODS = {
    "libc::clone",
    "libc::execve",
    "libc::execveat",
    "libc::fork",
    "libc::posix_spawn",
    "libc::sigaction",
    "libc::signal",
    "libc::vfork",
    "libc::wait",
    "libc::wait4",
    "libc::waitid",
    "libc::waitpid",
    "nix::sys::signal::sigaction",
    "nix::sys::wait::wait",
    "nix::sys::wait::waitid",
    "nix::sys::wait::waitpid",
    "nix::unistd::execve",
    "nix::unistd::execveat",
    "nix::unistd::fork",
    "nix::unistd::vfork",
    "rustix::process::kill_process",
    "rustix::process::kill_process_group",
    "rustix::process::pidfd_open",
    "rustix::process::pidfd_send_signal",
    "rustix::process::waitid",
    "rustix::process::waitpid",
    "std::process::Child::kill",
    "std::process::Child::try_wait",
    "std::process::Child::wait",
    "std::process::Child::wait_with_output",
    "std::process::Command::output",
    "std::process::Command::spawn",
    "std::process::Command::status",
}
PROCESS_LINT_ALLOWANCES = {
    "crates/lazaret-client/src/terminal.rs": {
        "signal_scope_restores_mask_and_default_termination"
    },
    "crates/lazaret-linux/src/process.rs": {
        "append_to",
        "send_signal",
    },
    "crates/lazaret-linux/src/process/broker.rs": {
        "acquire",
        "acquire_with_stdio",
        "acquire_with_stdio_after_ack",
        "acquire_with_stdio_in_user_namespace",
        "acquire_captured",
        "private_role_command",
        "mapped_wrapper_command",
        "reap",
        "reap_status",
        "fail_running_captured",
        "fail_running_mapped",
        "acquire_spawned_child",
        "verify_direct_child_pidfd",
        "fail_before_pidfd",
        "fail_after_pidfd_closed",
        "run_transient",
        "run_transient_in_user_namespace",
        "run_transient_with_stdout",
        "run_transient_captured",
        "run_mapping_helper",
        "spawn_bootstrap",
        "captured_process",
    },
    "crates/lazaret-linux/src/process/recovery.rs": {
        "recover_process",
        "current_process_identity",
        "match_recovery_process",
        "require_reapable_sigchld",
        "cleanup_sigchld_probe",
        "fail_sigchld_probe",
    },
    "crates/lazaret-linux/src/process/launch.rs": {
        "append_parent_identity",
        "exec_target",
        "suspend_current_process",
    },
    "crates/lazaret-host-coordinator/tests/runtime-composition.rs": {"run_benchmark_guest"},
    "crates/lazaret-client/tests/state_cli.rs": {
        "active_domain_reports_actionable_maintenance_contention",
        "machine_and_human_discovery_are_versioned_and_content_free",
        "missing_store_succeeds_only_when_the_complete_state_anchor_is_absent",
        "reset_refuses_an_arbitrary_container_or_host_path_before_state_access",
        "command",
    },
    "crates/lazaret-linux/tests/acquisition.rs": {
        "run_acquisition",
        "successful_acquisition",
        "acknowledged_transition_precedes_exact_wrapper_release",
        "failed_acknowledged_transition_refuses_exact_wrapper_release",
        "lifetime_pipe_descriptor_contract",
        "run_lifetime_pipe_target",
        "failed_stages_and_acknowledgments",
        "launch_wrapper_refuses_former_harness_path",
        "malformed_barriers_refuse",
        "sa_nocldwait_refuses",
        "foreign_non_child_refuses",
        "concurrent_acquisitions_serialize",
    },
    "crates/lazaret-linux/tests/capability-drop-helper.rs": {"main"},
    "crates/lazaret-prepared-lower/tests/prepared_lower.rs": {
        "retained_fixed_child_bind_mount_is_refused_when_mount_setup_is_available"
    },
}
RUST_FILE_LINE_LIMIT = 1000
RUST_FILE_SIZE_EXCEPTIONS = {
    "crates/lazaret-ignored-workspace/src/filesystem/operations.rs": (
        "complete FUSE Filesystem trait operation dispatch for ignored workspace routing"
    ),
    "crates/lazaret-prepared-lower/src/store.rs": (
        "prepared lower materialization verification and atomic publication"
    ),
    "crates/lazaret-runtime-supervisor/src/network.rs": (
        "rootless network topology construction readiness and teardown"
    ),
    "crates/lazaret-storage-catalog/src/lib.rs": (
        "typed shared artifact lease recovery and reclaim lifecycle"
    ),
}
FORBIDDEN_PROCESS_SYSCALLS = tuple(
    re.compile(pattern)
    for pattern in (
        r"^clone3?\(",
        r"^execveat\(",
        r"^fork\(",
        r"^vfork\(",
        r"^wait4\(",
        r"^waitid\(",
        r"^rt_sigaction\(SIGCHLD,",
    )
)
PROCESS_TRACE_EXIT_CODES = {
    "lazaret": 2,
    "lazaret-escalation-client": 2,
    "lazaret-git-sentry": 1,
    "lazaret-host-coordinator": 0,
    "lazaret-ignored-workspace": 1,
    "lazaret-launch-wrapper": 0,
    "lazaret-runtime-supervisor": 0,
    "lazaret-workspace-benchmark": 1,
}
LINT_BYPASS = re.compile(
    r"#\s*!?\s*\[[^]]*(?:allow|expect)\s*\([^]]*"
    r"(?:warnings|clippy\s*::\s*(?:all|style|restriction)|disallowed_methods|disallowed_types)"
)


class VerificationError(RuntimeError):
    pass


def temporary_directory(prefix: str) -> tempfile.TemporaryDirectory[str]:
    VERIFICATION_TEMP_ROOT.mkdir(parents=True, exist_ok=True)
    return tempfile.TemporaryDirectory(prefix=prefix, dir=VERIFICATION_TEMP_ROOT)


def require(condition: bool, message: str) -> None:
    if not condition:
        raise VerificationError(message)


def load_toml(path: Path) -> dict:
    with path.open("rb") as source:
        return tomllib.load(source)


def run(command: list[str], cwd: Path = ROOT) -> None:
    print(f"RUN {' '.join(command)}", flush=True)
    subprocess.run(command, cwd=cwd, check=True)


def run_physical(command: list[str], cwd: Path = ROOT) -> None:
    print(f"RUN {' '.join(command)}", flush=True)
    result = subprocess.run(command, cwd=cwd, check=False)
    if result.returncode == 77:
        print(f"SKIP {' '.join(command)}: physical prerequisites unavailable")
        return
    require(result.returncode == 0, f"physical test exited {result.returncode}")


def check_tool_versions() -> None:
    require(sys.version_info >= (3, 11), "Python 3.11 or newer is required")
    for program, args, accepted_exit_codes, pattern in REQUIRED_TOOL_VERSIONS:
        executable = shutil.which(program)
        require(executable is not None, f"{program} must be installed on PATH")
        result = subprocess.run(
            [executable, *args],
            text=True,
            stdout=subprocess.PIPE,
            stderr=subprocess.STDOUT,
            check=False,
        )
        output = result.stdout.strip()
        require(
            result.returncode in accepted_exit_codes and pattern.search(output) is not None,
            f"unsupported {program} version: {output or 'no version output'}",
        )
    print("PASS pinned verification tool versions")


def workspace_metadata() -> dict:
    result = subprocess.run(
        [
            "cargo",
            "metadata",
            "--locked",
            "--offline",
            "--all-features",
            "--format-version",
            "1",
        ],
        cwd=ROOT,
        text=True,
        stdout=subprocess.PIPE,
        check=True,
    )
    return json.loads(result.stdout)


def audit_workspace_lints(metadata: dict) -> None:
    workspace = load_toml(ROOT / "Cargo.toml")
    rust_lints = workspace.get("workspace", {}).get("lints", {}).get("rust", {})
    clippy_lints = workspace.get("workspace", {}).get("lints", {}).get("clippy", {})
    require(rust_lints.get("unsafe_code") == "forbid", "workspace must forbid unsafe Rust")
    require(
        clippy_lints.get("disallowed_methods") == "deny",
        "workspace must deny Clippy disallowed methods",
    )
    require(
        clippy_lints.get("disallowed_types") == "deny",
        "workspace must deny Clippy disallowed types",
    )
    clippy_config = load_toml(ROOT / ".clippy.toml")
    disallowed_types = {entry.get("path") for entry in clippy_config.get("disallowed-types", [])}
    disallowed_methods = {
        entry.get("path") for entry in clippy_config.get("disallowed-methods", [])
    }
    require(
        disallowed_types == REQUIRED_DISALLOWED_TYPES,
        "Clippy disallowed process types must match the reviewed boundary",
    )
    require(
        disallowed_methods == REQUIRED_DISALLOWED_METHODS,
        "Clippy disallowed process methods must match the reviewed boundary",
    )

    packages = {package["id"]: package for package in metadata["packages"]}
    for package_id in metadata["workspace_members"]:
        package = packages[package_id]
        manifest = load_toml(Path(package["manifest_path"]))
        require(
            manifest.get("lints") == {"workspace": True},
            f"{package['name']}: package must inherit workspace lints without override",
        )

    observed_allowances = {}
    for path in workspace_rust_sources(metadata):
        relative = str(path.relative_to(ROOT))
        source = path.read_text(errors="replace")
        functions = process_lint_allowances(relative, source)
        if functions:
            observed_allowances[relative] = functions
    require(
        observed_allowances == PROCESS_LINT_ALLOWANCES,
        "process-safety lint allowances must match exact reviewed functions",
    )
    print("PASS workspace unsafe and process-control lint boundary")


def process_lint_allowances(relative: str, source: str) -> set[str]:
    functions = set()
    for exemption in LINT_BYPASS.finditer(source):
        require(
            re.match(r"#\s*!", exemption.group()) is None,
            f"whole-file process lint exemption: {relative}",
        )
        following = source[exemption.end() : exemption.end() + 400]
        function = re.match(
            r"\s*\)\s*\]\s*(?:#\[[^]]+\]\s*)*(?:pub(?:\([^)]*\))?\s+)?fn\s+([A-Za-z0-9_]+)\s*[<(]",
            following,
        )
        require(function is not None, f"non-function process lint exemption: {relative}")
        functions.add(function.group(1))
    return functions


def workspace_rust_sources(metadata: dict) -> list[Path]:
    packages = {package["id"]: package for package in metadata["packages"]}
    target_directory = Path(metadata["target_directory"]).resolve()
    sources = set()
    for package_id in metadata["workspace_members"]:
        package_root = Path(packages[package_id]["manifest_path"]).resolve().parent
        require(
            package_root.is_relative_to(ROOT),
            f"workspace package is outside the repository: {package_root}",
        )
        require(
            not package_root.is_relative_to(target_directory),
            "Cargo target directory must not contain a workspace package",
        )
        sources.update(
            path.resolve()
            for path in package_root.rglob("*.rs")
            if not path.resolve().is_relative_to(target_directory)
        )
    return sorted(sources)


def audit_rust_module_boundaries(metadata: dict) -> None:
    included = []
    for path in workspace_rust_sources(metadata):
        source = path.read_text()
        if re.search(r"(?m)^\s*include!\s*\(", source):
            included.append(str(path.relative_to(ROOT)))
    require(
        not included,
        "Rust source uses lexical include! instead of a module boundary: "
        + ", ".join(included),
    )
    print("PASS Rust module boundaries")


def audit_rust_file_sizes(metadata: dict) -> None:
    sources = workspace_rust_sources(metadata)
    relative_sources = {str(path.relative_to(ROOT)): path for path in sources}
    line_counts = {
        relative: len(path.read_bytes().splitlines())
        for relative, path in relative_sources.items()
    }
    for relative, responsibility in RUST_FILE_SIZE_EXCEPTIONS.items():
        require(
            relative == Path(relative).as_posix()
            and not Path(relative).is_absolute()
            and relative.endswith(".rs"),
            f"malformed Rust file size exception path: {relative}",
        )
        require(
            "\n" not in responsibility and len(responsibility.split()) >= 3,
            f"malformed Rust file size exception responsibility: {relative}",
        )
        require(relative in relative_sources, f"stale Rust file size exception: {relative}")
        require(
            line_counts[relative] > RUST_FILE_LINE_LIMIT,
            f"stale Rust file size exception below threshold: {relative}",
        )

    oversized = {
        relative: lines
        for relative, lines in line_counts.items()
        if lines > RUST_FILE_LINE_LIMIT and relative not in RUST_FILE_SIZE_EXCEPTIONS
    }
    require(
        not oversized,
        "Rust files exceed the reviewed responsibility threshold: "
        + ", ".join(f"{path} ({lines})" for path, lines in sorted(oversized.items())),
    )
    print("PASS tracked Rust file responsibility size boundary")


def audit_dependencies(metadata: dict) -> None:
    policy = load_toml(ROOT / "deny.toml")
    allowed_licenses = set(policy["licenses"]["allow"])
    workspace_members = set(metadata["workspace_members"])
    client = next(package for package in metadata["packages"] if package["name"] == "lazaret-client")
    client_dependencies = {dependency["name"] for dependency in client["dependencies"]}
    require(
        client_dependencies.isdisjoint(
            {"lazaret-host-coordinator", "lazaret-runtime-supervisor"}
        ),
        "Lazaret Client depends on Host Coordinator or Runtime Supervisor implementation",
    )
    for package in metadata["packages"]:
        if package["id"] not in workspace_members:
            source = package.get("source") or ""
            require(
                source.startswith("registry+https://github.com/rust-lang/crates.io-index")
                or is_materialized_fuser(package),
                f"unapproved dependency source: {package['name']}",
            )
            license_expression = package.get("license") or ""
            require(
                license_permitted(license_expression, allowed_licenses),
                f"unapproved dependency license: {package['name']} {license_expression}",
            )
        for dependency in package["dependencies"]:
            dependency_source = dependency.get("source")
            if dependency_source is None:
                dependency_path = dependency.get("path")
                require(
                    dependency_path is not None
                    and Path(dependency_path).resolve().is_relative_to(ROOT),
                    f"external path dependency: {package['name']} -> {dependency['name']}",
                )
            else:
                require(
                    dependency_source.startswith(
                        "registry+https://github.com/rust-lang/crates.io-index"
                    ),
                    f"unapproved dependency source: {package['name']} -> {dependency['name']}",
                )
                require(
                    dependency["req"] != "*",
                    f"wildcard dependency: {package['name']} -> {dependency['name']}",
                )
    run(["cargo", "deny", "--frozen", "check", "bans", "licenses", "sources"])
    print("PASS dependency source, wildcard, and license audit")


def is_materialized_fuser(package: dict) -> bool:
    return (
        package.get("name") == "fuser"
        and package.get("version") == "0.17.0"
        and Path(package.get("manifest_path", "")).resolve() == MATERIALIZED_FUSER_MANIFEST
    )


def license_permitted(expression: str, allowed: set[str]) -> bool:
    expression = re.sub(r"\s+WITH\s+[A-Za-z0-9.-]+", "", expression)
    expression = re.sub(r"\s*/\s*", " OR ", expression)
    return bool(expression) and any(
        all(
            term.strip(" ()") in allowed
            for term in re.split(r"\s+AND\s+", alternative)
        )
        for alternative in re.split(r"\s+OR\s+", expression)
    )


def run_models() -> None:
    tlc = shutil.which("tlc")
    require(tlc is not None, "TLC must be installed on PATH")
    with temporary_directory("tlc-") as directory:
        workdir = Path(directory)
        for module, config in MODEL_CONFIGURATIONS:
            require(module.is_file(), f"missing model: {module.relative_to(ROOT)}")
            require(config.is_file(), f"missing model config: {config.relative_to(ROOT)}")
            metadata = workdir / module.stem
            run(
                [
                    tlc,
                    "-workers",
                    "1",
                    "-metadir",
                    str(metadata),
                    "-config",
                    str(config),
                    str(module),
                ],
                workdir,
            )


def workspace_binary_targets(metadata: dict) -> dict[str, str]:
    workspace_members = set(metadata["workspace_members"])
    targets = [
        (target["name"], package["id"])
        for package in metadata["packages"]
        if package["id"] in workspace_members
        for target in package["targets"]
        if "bin" in target["kind"]
    ]
    names = [name for name, _ in targets]
    require(len(names) == len(set(names)), "workspace binary target names must be unique")
    return dict(targets)


def binary_artifacts(metadata: dict, messages: str) -> dict[str, Path]:
    expected = workspace_binary_targets(metadata)
    artifacts = {}
    for line in messages.splitlines():
        message = json.loads(line)
        if message.get("reason") != "compiler-artifact" or message.get("executable") is None:
            continue
        target = message["target"]
        name = target["name"]
        if "bin" not in target["kind"] or expected.get(name) != message["package_id"]:
            continue
        require(name not in artifacts, f"duplicate executable artifact for {name}")
        artifacts[name] = Path(message["executable"])
    require(
        set(artifacts) == set(expected),
        f"binary artifact coverage mismatch; expected={sorted(expected)}, actual={sorted(artifacts)}",
    )
    return artifacts


def build_workspace_binaries(metadata: dict) -> dict[str, Path]:
    command = [
        "cargo",
        "build",
        "--offline",
        "--workspace",
        "--all-features",
        "--bins",
        "--locked",
        "--message-format=json",
    ]
    print(f"RUN {' '.join(command)}", flush=True)
    result = subprocess.run(
        command,
        cwd=ROOT,
        text=True,
        stdout=subprocess.PIPE,
        check=True,
    )
    return binary_artifacts(metadata, result.stdout)


def validate_process_trace(binary: str, lines: list[str]) -> None:
    execve_count = sum(line.startswith("execve(") for line in lines)
    expected_execve = 2 if binary == "lazaret-launch-wrapper" else 1
    require(
        execve_count == expected_execve,
        f"{binary}: unexpected execve surface count {execve_count}",
    )
    for line in lines:
        matches = [pattern.pattern for pattern in FORBIDDEN_PROCESS_SYSCALLS if pattern.search(line)]
        require(not matches, f"{binary}: forbidden process syscall surface {line}: {matches}")


def audit_process_syscalls(metadata: dict) -> None:
    strace = shutil.which("strace")
    require(strace is not None, "strace must be installed for --process-syscalls")
    require(sys.platform == "linux", "--process-syscalls requires Linux")
    binaries = build_workspace_binaries(metadata)
    require(binaries, "workspace has no binaries to trace")
    with temporary_directory("process-syscalls-") as directory:
        for binary, executable in sorted(binaries.items()):
            trace_base = Path(directory) / binary
            command = [
                    strace,
                    "-ff",
                    "-qq",
                    "-e",
                    "trace=process,wait4,waitid,rt_sigaction",
                    "-o",
                    str(trace_base),
                    "--",
                    str(executable),
                ]
            if binary == "lazaret-launch-wrapper":
                command.append("--trace-self-test")
            result = subprocess.run(
                command,
                cwd=ROOT,
                check=False,
            )
            validate_trace_exit(binary, result.returncode)
            traces = sorted(Path(directory).glob(f"{binary}.*"))
            require(traces, f"{binary}: strace produced no output")
            lines = [
                line
                for trace in traces
                for line in trace.read_text(errors="replace").splitlines()
            ]
            validate_process_trace(binary, lines)
    print("PASS final-binary exercised-path process-syscall audit")


def validate_trace_exit(binary: str, returncode: int) -> None:
    expected = PROCESS_TRACE_EXIT_CODES.get(binary)
    require(
        returncode == expected,
        f"{binary}: exercised path exited {returncode}, expected {expected}",
    )


def refresh_advisories() -> None:
    run(["cargo", "deny", "fetch"])
    run(["cargo", "deny", "--frozen", "check", "advisories"])


def run_rust_tests() -> None:
    run(list(FUSER_PATCH_TEST_COMMAND))
    run(list(NEXTEST_COMMAND))
    run(list(ACQUISITION_TEST_COMMAND))
    run(list(STATE_ANCHOR_LIFECYCLE_TEST_COMMAND))
    run(list(RECOVERY_PROCESS_TEST_COMMAND))
    run(list(CAPABILITY_TEST_COMMAND))
    run(list(ESCALATION_TEST_COMMAND))
    run(list(PREPARED_WORKER_TEST_COMMAND))
    run(list(NOFILE_TEST_COMMAND))
    run_physical(list(RUNTIME_COMPOSITION_TEST_COMMAND))
    run_physical(list(NETWORK_RUNTIME_TEST_COMMAND))
    run(list(DOCTEST_COMMAND))


def run_ignored_workspace_corpus(metadata: dict) -> None:
    binaries = build_workspace_binaries(metadata)
    with temporary_directory("ignored-workspace-corpus-") as directory:
        root = Path(directory)
        run_physical(
            [
                sys.executable,
                str(ROOT / "tools/ignored_workspace_verifier.py"),
                "corpus",
                "--router",
                str(binaries["lazaret-ignored-workspace"]),
                "--git-sentry",
                str(binaries["lazaret-git-sentry"]),
                "--work-root",
                str(root / "work"),
                "--output",
                str(root / "result.json"),
            ]
        )


def verify(process_syscalls: bool) -> None:
    check_tool_versions()
    metadata = workspace_metadata()
    run(["cargo", "fmt", "--all", "--", "--check"])
    run(
        [
            "cargo",
            "clippy",
            "--offline",
            "--workspace",
            "--all-targets",
            "--all-features",
            "--locked",
            "--",
            "-D",
            "warnings",
        ]
    )
    run_rust_tests()
    run_ignored_workspace_corpus(metadata)
    run([sys.executable, "-m", "unittest", "discover", "-s", "tests/tooling"])
    audit_workspace_lints(metadata)
    audit_rust_module_boundaries(metadata)
    audit_rust_file_sizes(metadata)
    audit_dependencies(metadata)
    run_models()
    if process_syscalls:
        audit_process_syscalls(metadata)


def main() -> int:
    parser = argparse.ArgumentParser(
        prog="tools/verify",
        description=(
            "Run formatting, Clippy, cargo-nextest, documentation tests, dependency "
            "policy, process-control policy, and both TLA+ models. Cargo operations "
            "are offline and locked; tests use exact cargo-nextest 0.9.140 and "
            "orchestration uses exact uv 0.11.28 with Python 3.11 or newer."
        )
    )
    actions = parser.add_mutually_exclusive_group()
    actions.add_argument(
        "--process-syscalls",
        action="store_true",
        help="also trace every current binary's no-argument path with strace",
    )
    actions.add_argument(
        "--refresh-advisories",
        action="store_true",
        help="update the RustSec database and check advisories instead of the default suite",
    )
    args = parser.parse_args()
    try:
        if args.refresh_advisories:
            check_tool_versions()
            refresh_advisories()
        else:
            verify(args.process_syscalls)
    except (OSError, subprocess.CalledProcessError, VerificationError) as error:
        print(f"ERROR: {error}", file=sys.stderr)
        return 1
    return 0


if __name__ == "__main__":
    sys.exit(main())