Blame for code/docs/LEAN_SANDBOX.md

# Lean REPL OS sandbox (H3)

Status: `align/verify/lean/sandbox.py` + `tests/test_lean_sandbox.py` exist and pass; **nothing
imports the sandbox yet**. Turning it on is the ~45-line patch at the end (not applied: the
P2 baseline run imports `repl_pool.py`, and its result must stay comparable to the post-SFT run).

## The gap this closes

`strict.py` and the `#print axioms` audit decide whether a proof is *accepted*. They do not limit
what Lean *does while checking it*. `#eval`, `run_cmd`, `initialize`, `elab`/`macro` run
arbitrary code as the RL job's user, on a box that holds checkpoints, `hf_cache/token`, `~/.ssh`
and a neighbouring training run (same uid: `kill(2)`, `ptrace(2)`, `/proc/<pid>/environ` all work).
Before this, containment was `prlimit` + a memory watchdog: resource limits, not capability limits.
The tests demonstrate each of these succeeding in the real REPL outside the sandbox and failing
inside (`test_real_lean_elaborator_io_is_contained`: read a secret, write outside scratch,
signal another process).

## Design (what is and is not a read-only `/`)

Probed on this host (kernel 6.1, `max_user_namespaces=764532`): `unshare -Urnm` works; remounting
the inherited `/` read-only works only per mount and the view would still *show* every secret.
Unprivileged `pivot_root` into a fresh tmpfs works, so the sandbox is an **allow-list root**
instead: the child sees only

| path | mode |
|---|---|
| `/usr` (+ `/bin /lib /lib64 /sbin` symlinks), `/etc/{ld.so.cache,ld.so.conf,nsswitch.conf,passwd,group,localtime}` | ro bind |
| `ro_paths` = `<lean>/elan`, `<lean>/repl`, `<lean>/workspace` | ro bind |
| `/dev/{null,zero,full,random,urandom}` | ro tmpfs + device binds |
| `/proc` | fresh procfs of the new pid ns |
| `/tmp` | private tmpfs, 64 MB, nosuid nodev **noexec** |
| `scratch_dir` (per worker) | **the only writable host directory** |
| root `/` | tmpfs remounted ro, old root detached (`umount2(MNT_DETACH)`) |

Everything else (`/home`, `/root`, `/apps/*` incl. checkpoints and `hf_cache`, `<lean>/tmp`,
`<lean>/logs`) does not exist. Paths leading to scratch exist as empty skeleton dirs.

Other properties: new **user** ns (uid/gid mapped 1:1, *not* fake root, so exec drops all caps:
`CapEff=0`; `setgroups` denied), **net** ns (loopback down: even 127.0.0.1 is unreachable;
abstract unix sockets of the host invisible), **pid** ns (neighbours invisible and unkillable;
when the REPL, pid 1, dies the kernel kills every descendant incl. double-fork daemons),
**ipc/uts** ns, `PR_SET_NO_NEW_PRIVS`, `RLIMIT_CORE=0`, own session/pgrp, minimal env
(`ENV_KEEP` allow-list; `HOME`=scratch, `TMPDIR`=/tmp, `PATH` pruned to dirs that exist).
`nice/prlimit/stdbuf` run *inside* the sandbox (`sandbox -- nice prlimit stdbuf repl`), so the pool's
rlimits are unchanged and `stdbuf`'s `LD_PRELOAD` still reaches the REPL (`/usr` is visible).

Fail closed: if any step of setup fails the command is **not** executed (exit 125/126, message in
the worker's stderr file -> `ReplCrash` with tail). `ReplPool.from_toolchain(sandbox=True)` raises
if namespaces are unavailable rather than falling back.

### Why a supervisor, and what `Popen.pid` means now

`ReplPool` spawns from `ThreadPoolExecutor` threads, so `preexec_fn` is unsafe and
`unshare(CLONE_NEWUSER)` needs a single-threaded caller. The launcher is a tiny `python -I -S`
process: unshare, fork the REPL into the new pid ns, stay outside and poll its parent *process*.
`Popen.pid` is the supervisor; the REPL's host pid is published in a pidfile **outside** the
sandbox (`inner_pid()`), which the memory watchdog uses (patch below; verified: identical `pss_anon`
readings). `killpg(Popen.pid)` still kills everything (tested). `PR_SET_PDEATHSIG` is not used:
prctl(2) ties it to the spawning *thread*; on this kernel 6.1 it was measured not to fire for a
non-leader thread, but it differs across kernels, so nothing depends on it.

## What is NOT claimed

* No seccomp filter. Namespaces are a capability boundary, not a proof; kernel bugs reachable from
  an unprivileged userns (the price of using one) are out of scope. The adversarial false-accept hunt
  is a separate task.
* The toolchain (`elan`, `repl`, `workspace`) is shared read-only between workers. A proof cannot
  modify it, but can read all of it (Mathlib is public).
* GPUs are not exposed. `/proc` of the new pid ns still shows the *kernel-global* files (`/proc/meminfo`,
  `/proc/cpuinfo`, `/proc/sys`, ...): host load and RAM are observable, not secret.
* A proof can still burn CPU/RAM up to the pool's limits and write `fsize_mb` into scratch (the
  scratch dir is on `/apps`: size it/clean it per worker; `.sandbox-root` is an empty dir the setup leaves in it).
* Tiny race: if the supervisor is SIGKILLed between `fork` and the child's `prctl(PDEATHSIG)`, the REPL
  survives until its stdin closes.
* Linux x86_64/aarch64 only (`pivot_root` syscall number); other arch -> setup fails closed.

## Evidence

All numbers from this host while the P2 baseline held the GPUs (1-2 Lean workers, one `import Mathlib`
header per worker, no heavy-job lock taken).

### Property tests (`tests/test_lean_sandbox.py`, 31 pass, ~13 s, plus 2 `slow` real-Lean tests)

Every property: probe run unsandboxed (control, must succeed) then inside (must fail).

| property | control outside | inside |
|---|---|---|
| connect to a live 127.0.0.1 listener | connects | `ENETUNREACH` (101) |
| connect to host abstract unix socket | connects | fails |
| write a host-writable file outside scratch / `/` / `/usr` / ro toolchain | OK | fails (`EROFS`/`ENOENT`), host file absent |
| write inside scratch | OK | OK, visible on host |
| read a host secret outside the allow-list; `/home`, `/root`, `~`, `/etc/shadow` | readable | does not exist |
| exec a binary dropped in `/tmp` | - | `EACCES` (noexec); `/tmp` not the host's |
| rename/modify an allow-listed file | - | fails; content unchanged |
| `mount()` remount-rw / bind (setuid `mount(8)` too) | - | `EPERM` / non-zero |
| `..`, `/proc/1/root`, `/proc/self/cwd/..` to reach old root; open fds | - | unreachable; <=4 fds |
| `NoNewPrivs`, `CapEff/CapPrm`, uid, core rlimit | 0, host caps, uid, unlimited | 1, 0, same non-zero uid, (0,0) |
| see/signal a live same-uid process, read its `environ` | visible, `kill 0` OK | pid 1 only, `ESRCH` |
| double-fork + setsid daemon | - | gone when the REPL exits |
| env: `HF_TOKEN`-style var, `LD_PRELOAD` | passes | dropped; `PATH` pruned |
| own session / pgrp (no `start_new_session`) | - | sid == pgid == supervisor |
| parent process SIGKILLed | - | REPL and supervisor gone <5 s |
| spawning *thread* exits (pool pattern) | - | REPL survives |
| `killpg(Popen.pid)` | - | REPL dies |
| setup failure (missing scratch) | - | command NOT run, exit 125/126 |

Real REPL (`slow`; run outside pytest because the instructions forbid `-m slow` while the baseline
runs): `#eval` that reads a host secret / writes outside scratch / `kill -0`s a neighbour
**succeeds without the sandbox and fails inside**; 10 known-good + `sorry_plain` + `eval_side_effect` +
`exit_after_theorem` verdicts are byte-identical inside and outside.

### Mutation record

Each line removed/flipped in `sandbox.py`, suite re-run (the file was restored; `diff` clean):

| mutant | killed by |
|---|---|
| no `CLONE_NEWNET` | `test_network_connect_fails_inside_succeeds_outside` |
| no `PR_SET_NO_NEW_PRIVS` | `test_no_new_privs_no_capabilities_same_uid` |
| no `CLONE_NEWPID` (host `/proc` bound) | `test_other_processes_are_invisible_and_unsignalable` |
| scratch bound read-only | `test_scratch_is_writable_and_shared_with_host` |
| toolchain bound read-write | `test_allow_listed_path_is_readable_but_read_only` |
| `/home` or a sibling dir bound in | `test_read_outside_allow_list_fails_inside_succeeds_outside` |
| old root not detached | `test_no_old_root_reachable` |
| parent-death poll disabled | `test_repl_dies_when_the_parent_process_dies` |
| uid mapped to fake root | `test_cannot_remount_or_mount_over_the_view` |
| no `setsid` | `test_own_session_and_process_group` |
| `/tmp` exec allowed | `test_tmp_is_private_noexec_and_not_the_host_tmp` |
| setup error falls through to exec | `test_setup_failure_never_runs_the_command` |
| scratch existence unchecked (host dirs created) | same test |
| env not filtered / PATH not pruned | `test_minimal_env_...` / `test_child_sees_only_the_spec_env_...` |
| `RLIMIT_CORE` left | `test_no_new_privs_no_capabilities_same_uid` |
| no pidfile | `test_pidfile_names_the_repl_host_pid` |
| root tmpfs left writable | `test_write_outside_scratch_...` |
| `/tmp` tmpfs without a size cap (defaults to 50% of RAM, box has no swap) | `test_tmp_tmpfs_is_size_capped` (review) |
| `closerange` removed (fd passed by a caller crosses the exec) | `test_inherited_fds_do_not_cross_the_exec` (review) |
| recursive bind (`MS_BIND\|MS_REC`) of a ro path | `test_nested_writable_mount_under_a_ro_path_is_not_carried` (review; before it, only caught by accident) |
| REPL's own `PDEATHSIG` removed (supervisor alone SIGKILLed) | `test_killing_only_the_supervisor_kills_the_repl` (review) |
| no alias for a symlinked `ro_paths` / `scratch_dir` | `test_toolchain_reached_through_a_symlink_is_usable` (review) |
| `inner_pid` trusts a stale pidfile | `test_inner_pid_ignores_a_stale_pidfile` (review) |
| launcher broken wholesale (3 variants) | `test_launcher_works_whenever_the_kernel_allows_namespaces` (before it existed the same mutants turned all 24 tests into SKIPS) |

Survivors, honestly: (a) `PR_SET_PDEATHSIG` on the supervisor: kernel 6.1 does not deliver it on
thread exit, so `test_repl_survives_the_spawning_thread_exiting` cannot fail here (it pins the
contract on kernels that do). (b) Deleting the supervisor's explicit "kill inner on parent death":
equivalent, the inner's own `PDEATHSIG` on the (single-threaded) supervisor covers it - kept as two layers.
Not mutation-tested: `MS_REC|MS_PRIVATE` propagation (new mount ns already does not propagate
upward here). Equivalent mutants noted by review: binding `/etc` files read-write (the host
forbids the write anyway).

Review notes: a mount nested under a `ro_paths` entry makes setup REFUSE (kernel EINVAL on a
non-recursive bind over a locked child mount; fail closed, exit 126) -- list such a mount as its
own `ro_paths` entry. `test_pidfile_names_the_repl_host_pid` was flaky (the pidfile is written
before the child's exec; the test now waits for it). The pidfile is published BEFORE the exec, so
for a few ms `inner_pid` names the launcher's own child still running python.

### Overhead (real Lean 4.9 / Mathlib d1d1e4b72c REPL)

Single worker, 10 known-good ceiling proofs x3 reps: cold `import Mathlib` header **3.18 s -> 3.33 s**
(+0.15 s, once per worker); per-proof median **20.8 -> 20.4 ms**, mean 80.9 -> 79.8 ms (no measurable
difference). Pool of 2 workers via `ReplPool.from_toolchain(sandbox=True)` using the patched module
(patch applied to a COPY of the tree, not the repo), 10 proofs x5 over `map`:
warm **3.33 -> 3.67 s** (+0.33 s, once), median **23.9 -> 22.1 ms**, mean 85.2 -> 81.5 ms;
verdicts identical; `memory_report()` identical `pss_anon` (256/252 MB) through `inner_pid`;
`kill()` + respawn works; no leftover `sandbox.py` processes. Existing `tests/test_lean_verifier.py`
passes (198 passed with the sandbox tests) on the patched copy. Cost: one extra ~10 MB python per worker.

## The patch (NOT applied)

Touches only `align/verify/lean/repl_pool.py`; imports the sandbox lazily, default `sandbox=False` is
behaviour-identical. `sandbox_supported()` actually launches the helper once (a sysctl is not proof).

```diff
--- a/align/verify/lean/repl_pool.py	2026-10-13 04:43:15.450960951 +0530
+++ b/align/verify/lean/repl_pool.py	2026-10-13 04:43:15.460961181 +0530
@@ -54,7 +54,10 @@
 from concurrent.futures import ThreadPoolExecutor
 from contextlib import contextmanager
 from dataclasses import dataclass, field
-from typing import Any, Callable, Iterator, Optional, Sequence
+from typing import TYPE_CHECKING, Any, Callable, Iterator, Optional, Sequence
+
+if TYPE_CHECKING:  # the sandbox module is imported lazily, only when a pool opts in
+    from align.verify.lean.sandbox import SandboxSpec
 
 # --------------------------------------------------------------------------- errors
 
@@ -199,7 +202,10 @@
         limits: ReplLimits = ReplLimits(),
         stderr_path: Optional[str] = None,
         wrap: bool = True,
+        sandbox: Optional["SandboxSpec"] = None,
     ) -> None:
+        #: opt-in OS sandbox (align/verify/lean/sandbox.py); None = unchanged behaviour
+        self.sandbox = sandbox
         self.argv = list(argv)
         self.env = dict(env)
         self.cwd = cwd
@@ -216,6 +222,14 @@
     # -- lifecycle
 
     def _wrapped_argv(self) -> list[str]:
+        argv = self._limited_argv()
+        if self.sandbox is not None:  # sandbox OUTSIDE nice/prlimit/stdbuf: they run inside it
+            from align.verify.lean.sandbox import sandbox_argv
+
+            argv = sandbox_argv(self.sandbox, argv)
+        return argv
+
+    def _limited_argv(self) -> list[str]:
         if not self.wrap:
             return list(self.argv)
         lim = self.limits
@@ -237,6 +251,13 @@
             pre += [stdbuf, "-o0", "-e0"]
         return pre + self.argv
 
+    def _spawn_env(self) -> dict[str, str]:
+        if self.sandbox is None:
+            return self.env
+        from align.verify.lean.sandbox import helper_env
+
+        return helper_env()  # the launcher gets nothing; the REPL's env travels in sandbox.env
+
     def start(self) -> None:
         if self.alive:
             return
@@ -252,7 +273,7 @@
             stdin=subprocess.PIPE,
             stdout=subprocess.PIPE,
             stderr=err,
-            env=self.env,
+            env=self._spawn_env(),
             cwd=self.cwd,
             start_new_session=True,  # own process group => killpg reaps every descendant
             close_fds=True,
@@ -316,7 +337,12 @@
             return ""
 
     def memory(self) -> Optional[dict[str, float]]:
-        return process_memory(self.pid) if self.pid else None
+        pid = self.pid
+        if self.sandbox is not None:  # Popen.pid is the supervisor; the REPL is its child
+            from align.verify.lean.sandbox import inner_pid
+
+            pid = inner_pid(self.sandbox, self.pid)
+        return process_memory(pid) if pid else None
 
     # -- I/O
 
@@ -671,6 +697,7 @@
         max_requests: int = 1000,
         default_timeout_s: float = 120.0,
         preflight: bool = False,
+        sandbox: bool = False,
     ) -> "ReplPool":
         n = n_workers if n_workers is not None else default_workers()
         if preflight:
@@ -679,12 +706,29 @@
         os.makedirs(scratch, exist_ok=True)
 
         def launcher(idx: int) -> ReplProcess:
+            spec = None
+            if sandbox:
+                from align.verify.lean.sandbox import SandboxSpec, minimal_env, sandbox_supported
+
+                ok, why = sandbox_supported()
+                if not ok:  # fail closed: never silently fall back to no isolation
+                    raise RuntimeError(f"sandbox=True but namespaces are unavailable: {why}")
+                wdir = os.path.join(scratch, f"sandbox{idx}")
+                os.makedirs(wdir, exist_ok=True)
+                spec = SandboxSpec(
+                    scratch_dir=wdir,
+                    ro_paths=tuple(str(toolchain.root / d) for d in ("elan", "repl", "workspace")),
+                    cwd=toolchain.cwd,
+                    pidfile=os.path.join(scratch, f"worker{idx}.pid"),
+                    env=minimal_env(toolchain.child_env, wdir),
+                )
             return ReplProcess(
                 toolchain.argv(),
                 toolchain.child_env,
                 cwd=toolchain.cwd,
                 limits=limits,
                 stderr_path=os.path.join(scratch, f"worker{idx}.stderr"),
+                sandbox=spec,
             )
 
         return cls(launcher, n, max_requests, default_timeout_s)
```

To use: `ReplPool.from_toolchain(tc, n_workers=..., scratch_dir=".../pool", sandbox=True)`; pass
`scratch_dir` OUTSIDE the Lean root (the default `<lean>/tmp/pool` is fine because only `elan`, `repl`
and `workspace` are mapped, not `<lean>/tmp`). Remember to enable it for BOTH the baseline-comparable
pre-SFT and post-SFT runs, or neither: verdicts were identical in every case tested, but the
comparability argument should not rest on that.