From 7f68a6447cbc95811de4a23561e7c005af81c1cd Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 2 Jul 2026 16:10:55 +0200 Subject: [PATCH] controls: route all compiles through lean-guard (memory-capped, single-flight) Co-Authored-By: Claude Fable 5 --- verification/check.sh | 4 +- verification/lean-guard | 125 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 127 insertions(+), 2 deletions(-) create mode 100755 verification/lean-guard diff --git a/verification/check.sh b/verification/check.sh index 7c5ce9c..045a03e 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -98,7 +98,7 @@ lake env bash -c " cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" compile() { echo \" · \$1\" - taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -o \"\${1}.olean\" \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; } + LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' \"\${1}.lean\" 2>&1 | tee -a '$LOG' || { echo \"FAIL: \$1\"; exit 1; } } for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done cd '$HERE' @@ -130,7 +130,7 @@ lake env bash -c " for i in ${AUDIT_IMPORTS[*]}; do echo \"import \$i\"; done for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done } > \"\$AUD\" - OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean \"\$AUD\" 2>&1) + OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -M \${LEAN_MEM_MB:-4096} \"\$AUD\" 2>&1) echo \"\$OUT\" rm -f \"\$AUD\" N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true) diff --git a/verification/lean-guard b/verification/lean-guard new file mode 100755 index 0000000..60d98bc --- /dev/null +++ b/verification/lean-guard @@ -0,0 +1,125 @@ +#!/usr/bin/env bash +# ──────────────────────────────────────────────────────────────────────────── +# lean-guard — HARD-CAPPED Lean compiler wrapper. +# +# Successor to lean-safe after the 2026-07-02 OOM incident: a single `lean` +# elaboration (tactic-search blowup: simp[*]/scalar_tac over a ~60-hypothesis +# context with 2^256-scale literals) grew to 12.2GB RSS and was killed by the +# GLOBAL kernel OOM killer, taking the driving session down with it. +# lean-safe's guards (timeout + affinity + PREFLIGHT headroom) cannot stop +# that: the process passes preflight, then balloons inside its timeout. +# +# NEW GUARDS (in addition to all lean-safe guards): +# A. lean -M — Lean's internal cap: elaboration aborts +# with a clean "maximum memory exceeded" +# error. First line of defense; graceful. +# B. systemd-run --user --scope +# -p MemoryMax / MemorySwapMax — kernel cgroup cap around the process: +# if Lean's own accounting misses (C-level +# allocations), the cgroup kills ONLY this +# lean, never the session, never the box. +# C. flock on /tmp/lean-guard.lock — machine-wide single-flight: at most ONE +# lean compile at a time, regardless of +# how many agents/scripts are active. +# +# Env knobs (defaults for this 14GB / 8-core ThinkPad): +# LEAN_TIMEOUT per-file wall clock seconds (default 400) +# LEAN_MEM_MB lean -M internal cap, MB (default 4096) +# LEAN_CGROUP_MB cgroup MemoryMax, MB (default LEAN_MEM_MB+1024) +# LEAN_MAX_CORES taskset core range (default 0-3) +# LEAN_MIN_FREE_MB preflight available-RAM floor (default 3072) +# LEAN_LOCK_WAIT max seconds to wait for the lock (default 7200) +# +# Usage: lean-guard [extra lean args...] +# The .olean output path is always computed as ${file%.lean}.olean. +# Requires: lean on PATH (caller sources the toolchain env; typically run +# inside `lake env` so LEAN_PATH is set — this wrapper does NOT clobber env). +# ──────────────────────────────────────────────────────────────────────────── +set -uo pipefail + +TIMEOUT_SEC=${LEAN_TIMEOUT:-400} +MEM_MB=${LEAN_MEM_MB:-4096} +CGROUP_MB=${LEAN_CGROUP_MB:-$((MEM_MB + 1024))} +CORES=${LEAN_MAX_CORES:-0-3} +MIN_FREE_MB=${LEAN_MIN_FREE_MB:-3072} +LOCK_WAIT=${LEAN_LOCK_WAIT:-7200} +LOCK_FILE=/tmp/lean-guard.lock +LOG_FILE="${HOME}/.lean-guard.log" + +if ! command -v lean &>/dev/null; then + echo "FATAL: lean not on PATH — source ~/aeneas-toolchain/env.sh (and run inside lake env)" + exit 1 +fi +if [ $# -eq 0 ]; then + echo "Usage: lean-guard [lean args...]" + exit 1 +fi + +LEAN_FILE="$1"; shift || true + +# ── Guard 1: source integrity (anti olean-clobber) ────────────────────────── +if [ ! -f "$LEAN_FILE" ]; then + echo "MISSING: $LEAN_FILE"; exit 1 +fi +if ! grep -qE '^[[:space:]]*(/-|import |namespace |theorem |def |open |set_option |--)' "$LEAN_FILE" 2>/dev/null; then + echo "FATAL: $LEAN_FILE is not Lean source (binary/olean data?)." + echo " Restore: git checkout HEAD -- $LEAN_FILE" + exit 1 +fi + +# ── Guard 2: output path ───────────────────────────────────────────────────── +case "$LEAN_FILE" in + *.lean) ;; + *) echo "FATAL: input lacks .lean extension"; exit 1 ;; +esac +OLEAN_FILE="${LEAN_FILE%.lean}.olean" +[ "$OLEAN_FILE" = "$LEAN_FILE" ] && { echo "FATAL: output would clobber source"; exit 1; } + +# ── Guard C: machine-wide single-flight ───────────────────────────────────── +exec 9>"$LOCK_FILE" +if ! flock -w "$LOCK_WAIT" 9; then + echo "FATAL: could not acquire lean-guard lock within ${LOCK_WAIT}s (another compile stuck?)" + exit 1 +fi + +# ── Guard 3: preflight headroom (after lock: serialized measurement) ──────── +AVAIL_MB=$(free -m | awk '/Mem:/{print $7}') +if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then + echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile" + exit 1 +fi + +echo "[$(date -u +%F' '%T)] $LEAN_FILE (t=${TIMEOUT_SEC}s M=${MEM_MB}MB cg=${CGROUP_MB}MB cores=$CORES avail=${AVAIL_MB}MB)" >> "$LOG_FILE" + +# ── Compile under both caps ────────────────────────────────────────────────── +run_leancmd() { + taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" +} +if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null; then + # --scope runs the command as a child of THIS shell (env inherited), + # merely placing it in a fresh cgroup with the hard caps below. + systemd-run --user --scope --quiet \ + -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \ + -- taskset -c "$CORES" \ + timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \ + lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@" + EXIT_CODE=$? +else + echo " (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE" + run_leancmd "$@" + EXIT_CODE=$? +fi + +case $EXIT_CODE in + 0) echo " OK" >> "$LOG_FILE" ;; + 124) echo " TIMEOUT ${TIMEOUT_SEC}s" >> "$LOG_FILE" + echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" ;; + 137) echo " KILLED (cgroup MemoryMax ${CGROUP_MB}MB hit)" >> "$LOG_FILE" + echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" ;; + *) echo " FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE" ;; +esac +# stale partial olean from a failed compile must not poison later imports +[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE" +exit $EXIT_CODE