From 9479a2bcba8caf8813e06460d23bf2bdf5360d8c Mon Sep 17 00:00:00 2001 From: saymrwulf Date: Fri, 3 Jul 2026 17:51:14 +0200 Subject: [PATCH] re-budget scalar caps post-optimization; guard 3b (headroom clamp) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit check-scalar.sh proofs phase back to 300s/4096MB: the sub_val_spec assembly's true peak is 753MB after the atomic-scLimbs fix — the 8192 cap was inflation left over from the slow draft and caused the 2026-07-03 swap-pressure incident (see control repo FAILURES.md). lean-guard updated to master with Guard 3b. Button green at the honest budget, 4/4 audits. Co-Authored-By: Claude Fable 5 --- verification/check-scalar.sh | 2 +- verification/lean-guard | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh index ddb56c2..a727b72 100755 --- a/verification/check-scalar.sh +++ b/verification/check-scalar.sh @@ -19,7 +19,7 @@ lake env bash -c " cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done cd '$HERE' - for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=600 LEAN_MEM_MB=8192 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done + for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done " || { echo FAIL; exit 1; } echo "=== Phase 3: axiom audit (kernel-level) ===" cd "$AENEAS_LEAN" diff --git a/verification/lean-guard b/verification/lean-guard index 10a0af3..54e1ace 100755 --- a/verification/lean-guard +++ b/verification/lean-guard @@ -94,6 +94,24 @@ if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then exit 1 fi +# ── Guard 3b: global-headroom clamp (2026-07-03 swap-pressure incident) ───── +# A cap is a PROMISE of memory to lean; never promise more than the machine +# can afford right now. Requested caps that exceed (available − floor) are +# clamped, so raising LEAN_MEM_MB can no longer starve the rest of the system +# into swap even when lean itself stays within its cap. Clamp, don't fail: +# most compiles peak far below their cap (measure before raising — the +# incident's 9G scopes served a file whose true peak was 753MB). +MAX_AFFORD_MB=$(( AVAIL_MB - MIN_FREE_MB )) +if [ "$MEM_MB" -gt "$MAX_AFFORD_MB" ]; then + echo "lean-guard: clamping -M ${MEM_MB} -> ${MAX_AFFORD_MB}MB (avail=${AVAIL_MB}MB, floor=${MIN_FREE_MB}MB)" + MEM_MB=$MAX_AFFORD_MB + CGROUP_MB=$(( MEM_MB + 1024 )) +fi +if [ "$MEM_MB" -lt 1024 ]; then + echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely" + 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 ──────────────────────────────────────────────────