saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

re-budget scalar caps post-optimization; guard 3b (headroom clamp)

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
saymrwulf 2026-07-03 17:51:14 +02:00
parent 1766544daf
commit 9479a2bcba
2 changed files with 19 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
verification/check-scalar.sh
View file

@ -19,7 +19,7 @@ lake env bash -c "
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" 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 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' 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 FAIL; exit 1; }
echo "=== Phase 3: axiom audit (kernel-level) ===" echo "=== Phase 3: axiom audit (kernel-level) ==="
cd "$AENEAS_LEAN" cd "$AENEAS_LEAN"

18
verification/lean-guard
View file

@ -94,6 +94,24 @@ if [ "$AVAIL_MB" -lt "$MIN_FREE_MB" ]; then
exit 1 exit 1
fi 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" 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 ────────────────────────────────────────────────── # ── Compile under both caps ──────────────────────────────────────────────────