saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-03 19:53:49 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

lean-guard: surface clamp/kill diagnostics on stderr (operator incident 2026-07-24)

Browse source 
check.sh pipes lean-guard stdout to /dev/null, so the headroom-clamp warning
was invisible: on a loaded desktop (4.3GB avail) the clamp cut -M 4096 to
1263MB, TypesExternal died loading imports, and the bare FAIL read as a proof
regression. All human-facing diagnostics (floor refusal, clamp, TIMEOUT,
KILLED) now go to stderr, and a clamped memory-death prints an explicit 'this
is an environment condition, not a proof failure — free RAM and re-run' note
with the required headroom. Reproduced and verified through the >/dev/null
pipe. Infra only; no proof, model, or gate change.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-24 21:37:05 +02:00
parent 77d6b2c195
commit 62d7ed1209
1 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
verification/lean-guard
View file

@ -90,7 +90,8 @@ 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"
# >&2: callers (check.sh) pipe stdout to /dev/null — diagnostics must survive
echo "FATAL: only ${AVAIL_MB}MB available (< ${MIN_FREE_MB}MB floor) — refusing to compile" >&2
exit 1
fi
@ -106,13 +107,18 @@ REQ_MEM_MB=$MEM_MB
WAS_CLAMPED=0
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)"
# >&2 so the clamp is VISIBLE through check.sh's >/dev/null pipe — a clamped
# cap can abort even a light file while loading imports, and that failure is
# indistinguishable from a proof regression unless this line reaches the
# human (2026-07-24 operator incident: -M clamped to 1263MB on a loaded
# desktop, TypesExternal died at import-load, read as "FAIL: disturbing").
echo "lean-guard: clamping -M ${MEM_MB} -> ${MAX_AFFORD_MB}MB (avail=${AVAIL_MB}MB, floor=${MIN_FREE_MB}MB) — if this compile dies with a memory abort, free RAM and re-run" >&2
MEM_MB=$MAX_AFFORD_MB
CGROUP_MB=$(( MEM_MB + 1024 ))
WAS_CLAMPED=1
fi
if [ "$MEM_MB" -lt 1024 ]; then
echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely"
echo "FATAL: headroom clamp would leave lean < 1024MB — machine too loaded to compile safely" >&2
exit 1
fi
@ -179,10 +185,11 @@ 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" ;;
echo "TIMEOUT: $LEAN_FILE exceeded ${TIMEOUT_SEC}s" >&2 ;;
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" ;;
echo "KILLED: $LEAN_FILE hit the ${CGROUP_MB}MB cgroup cap (contained — machine unharmed)" >&2 ;;
*) echo " FAILED exit $EXIT_CODE (lean error, possibly '-M ${MEM_MB}MB exceeded')" >> "$LOG_FILE"
[ "$WAS_CLAMPED" -eq 1 ] && echo "lean-guard: NOTE — this run was memory-CLAMPED to -M ${MEM_MB}MB (machine was loaded); a memory abort here is an environment condition, not evidence of a proof failure. Free RAM (need ~$((REQ_MEM_MB + MIN_FREE_MB))MB available) and re-run." >&2 ;;
esac
# stale partial olean from a failed compile must not poison later imports
[ $EXIT_CODE -ne 0 ] && rm -f "$OLEAN_FILE"