mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-04 20:03:44 +00:00
L1+L2: hashing shapes, domain separation, MTH/Root/ConsRec with termination
Accumulator pyramid layers 1-2, mechanizing paper SS5.3/SS6 groundwork: - gen/LTLAcc/HashExternal.lean: the single sanctioned axiom, opaque sha256 (no properties assumed - the soundness theorems downstream are constructive collision extractors). - Proofs/Basic.lean: hleaf/hnode (0x00/0x01 domain stamps); Lemma 1 (domsep) proven AXIOM-FREE; kbelow (largest power of two below n) with pos/lt/le-two bound lemmas; MTH, Root (Option = rejection), ConsRec (four cases, b-flag, pinned anchor) - all with kernel-checked termination via the kbelow bounds. - check.sh: estate discipline (stub audit, axiom-smuggling gate, lean-guard compilation, boundary-exact per-certificate cone audit). All green; observed cones pinned exactly. Zero contact with the live LTL: no appends, no server, accumulator frozen at 12 leaves throughout this project. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
commit
8d67e9519c
9 changed files with 499 additions and 0 deletions
33
README.md
Normal file
33
README.md
Normal file
|
|
@ -0,0 +1,33 @@
|
||||||
|
# ltl-accumulator-verified
|
||||||
|
|
||||||
|
Lean 4 mechanization of the security analysis (§6) of the paper
|
||||||
|
"The Lean Transparency Log" (https://ltl.zkdefi.org/paper): the Merkle
|
||||||
|
accumulator's own correctness and soundness theorems, kernel-checked, in
|
||||||
|
the same discipline as the four `*-ed25519-verified` subject corpora.
|
||||||
|
|
||||||
|
## Status: layer scaffold (work in progress — honest ledger below)
|
||||||
|
|
||||||
|
| layer | content | status |
|
||||||
|
|---|---|---|
|
||||||
|
| L1 | bytes, hleaf/hnode, domain separation (Lemma 1) | **done** (domsep: axiom-free) |
|
||||||
|
| L2 | MTH, Root, ConsRec definitions + termination | **done** (cones: propext, LTLAcc.sha256, Quot.sound) |
|
||||||
|
| L3 | inclusion completeness (Theorem 1) | pending |
|
||||||
|
| L4 | frontier hash-fold + root binding (Lemma 2) | pending |
|
||||||
|
| L5 | inclusion/consistency soundness as collision extractors (Theorems 2, 3) | pending |
|
||||||
|
| L6 | pin-store state machine safety (Proposition 1) | pending |
|
||||||
|
|
||||||
|
## Discipline (identical to the subject corpora)
|
||||||
|
|
||||||
|
- `verification/Proofs/` contains ZERO `axiom` declarations; the single
|
||||||
|
sanctioned axiom site is `verification/gen/` — here, one opaque
|
||||||
|
function: SHA-256. The theorems are constructive collision extractors,
|
||||||
|
so collision resistance is never assumed, only interpreted.
|
||||||
|
- `verification/check.sh` is THE button: compiles every file through
|
||||||
|
`lean-guard` (memory cap, core pinning, timeout, single-flight lock)
|
||||||
|
and axiom-audits every certificate against its documented exact cone.
|
||||||
|
- Expected boundary: `propext, Classical.choice, Quot.sound` plus
|
||||||
|
`LTLAcc.sha256` for hash-touching certificates — documented per
|
||||||
|
certificate in `check.sh`, audited both directions.
|
||||||
|
|
||||||
|
The finished certificates are destined for the LTL itself as attestation
|
||||||
|
leaves: the log carrying kernel-checked proofs of its own machinery.
|
||||||
9
verification/Proofs/AxiomCheck.lean
Normal file
9
verification/Proofs/AxiomCheck.lean
Normal file
|
|
@ -0,0 +1,9 @@
|
||||||
|
/- Axiom-cone observation for the audit (Phase 3 of check.sh). -/
|
||||||
|
import Proofs.Basic
|
||||||
|
#print axioms LTLAcc.domsep
|
||||||
|
#print axioms LTLAcc.kbelow_pos
|
||||||
|
#print axioms LTLAcc.kbelow_lt
|
||||||
|
#print axioms LTLAcc.le_two_kbelow
|
||||||
|
#print axioms LTLAcc.MTH
|
||||||
|
#print axioms LTLAcc.Root
|
||||||
|
#print axioms LTLAcc.ConsRec
|
||||||
BIN
verification/Proofs/AxiomCheck.olean
Normal file
BIN
verification/Proofs/AxiomCheck.olean
Normal file
Binary file not shown.
151
verification/Proofs/Basic.lean
Normal file
151
verification/Proofs/Basic.lean
Normal file
|
|
@ -0,0 +1,151 @@
|
||||||
|
/- L1 + L2 of the accumulator pyramid: byte-level hashing shapes, domain
|
||||||
|
separation (paper Lemma 1), the split point, and the three §5.3
|
||||||
|
definitions (MTH, Path-dual Root, ConsRec) with their termination.
|
||||||
|
|
||||||
|
Everything here is stated over the opaque `sha256` of gen/ — no
|
||||||
|
property of the hash is used anywhere in this file. -/
|
||||||
|
import LTLAcc.HashExternal
|
||||||
|
|
||||||
|
namespace LTLAcc
|
||||||
|
|
||||||
|
abbrev Bytes := List UInt8
|
||||||
|
|
||||||
|
/-- Leaf hash: `H(0x00 ‖ d)` (paper §5.3). -/
|
||||||
|
noncomputable def hleaf (d : Bytes) : Bytes := sha256 (0x00 :: d)
|
||||||
|
|
||||||
|
/-- Node hash: `H(0x01 ‖ x ‖ y)` (paper §5.3). -/
|
||||||
|
noncomputable def hnode (x y : Bytes) : Bytes := sha256 (0x01 :: (x ++ y))
|
||||||
|
|
||||||
|
/-- **Lemma 1 (Domain separation), preimage form**: no leaf preimage
|
||||||
|
equals a node preimage as a byte string — the first byte differs. -/
|
||||||
|
theorem domsep (d x y : Bytes) :
|
||||||
|
(0x00 : UInt8) :: d ≠ (0x01 : UInt8) :: (x ++ y) := by
|
||||||
|
intro h
|
||||||
|
injection h with h0 _
|
||||||
|
exact absurd h0 (by decide)
|
||||||
|
|
||||||
|
/-- Largest power of two STRICTLY below `n`, for `n ≥ 2` (RFC 9162's
|
||||||
|
split point `k`; values at `n ≤ 1` are irrelevant and default to 1). -/
|
||||||
|
def kbelow (n : Nat) : Nat :=
|
||||||
|
if n ≤ 2 then 1
|
||||||
|
else 2 * kbelow ((n + 1) / 2)
|
||||||
|
termination_by n
|
||||||
|
decreasing_by omega
|
||||||
|
|
||||||
|
theorem kbelow_pos (n : Nat) : 0 < kbelow n := by
|
||||||
|
induction n using kbelow.induct with
|
||||||
|
| case1 n h => rw [kbelow]; simp [h]
|
||||||
|
| case2 n h ih => rw [kbelow]; simp [h]; omega
|
||||||
|
|
||||||
|
theorem kbelow_lt (n : Nat) (h : 2 ≤ n) : kbelow n < n := by
|
||||||
|
induction n using kbelow.induct with
|
||||||
|
| case1 n hle => rw [kbelow]; simp only [if_pos hle]; omega
|
||||||
|
| case2 n hgt ih =>
|
||||||
|
rw [kbelow]
|
||||||
|
simp only [if_neg hgt]
|
||||||
|
have h2 : 2 ≤ (n + 1) / 2 := by omega
|
||||||
|
have := ih h2
|
||||||
|
omega
|
||||||
|
|
||||||
|
theorem le_two_kbelow (n : Nat) (h : 2 ≤ n) : n ≤ 2 * kbelow n := by
|
||||||
|
induction n using kbelow.induct with
|
||||||
|
| case1 n hle => rw [kbelow]; simp only [if_pos hle]; omega
|
||||||
|
| case2 n hgt ih =>
|
||||||
|
rw [kbelow]
|
||||||
|
simp only [if_neg hgt]
|
||||||
|
have h2 : 2 ≤ (n + 1) / 2 := by omega
|
||||||
|
have := ih h2
|
||||||
|
omega
|
||||||
|
|
||||||
|
/-- `MTH` (paper §5.3): the RFC 9162 tree head over a leaf-data list.
|
||||||
|
`MTH [] = H(ε)`, `MTH [d] = hleaf d`, and for `n ≥ 2` the split at
|
||||||
|
`k = kbelow n`. -/
|
||||||
|
noncomputable def MTH (D : List Bytes) : Bytes :=
|
||||||
|
if _h0 : D.length = 0 then sha256 []
|
||||||
|
else if _h1 : D.length = 1 then hleaf (D.headD [])
|
||||||
|
else
|
||||||
|
hnode (MTH (D.take (kbelow D.length))) (MTH (D.drop (kbelow D.length)))
|
||||||
|
termination_by D.length
|
||||||
|
decreasing_by
|
||||||
|
· -- take-branch: k < n
|
||||||
|
simp only [List.length_take]
|
||||||
|
have h2 : 2 ≤ D.length := by omega
|
||||||
|
have hk := kbelow_lt D.length h2
|
||||||
|
omega
|
||||||
|
· -- drop-branch: n - k < n
|
||||||
|
simp only [List.length_drop]
|
||||||
|
have h2 : 2 ≤ D.length := by omega
|
||||||
|
have hk := kbelow_lt D.length h2
|
||||||
|
have hp := kbelow_pos D.length
|
||||||
|
omega
|
||||||
|
|
||||||
|
/-- `Root` (paper §5.3 / Appendix B): the consumer's root reconstruction.
|
||||||
|
`none` = rejection on any length mismatch, exactly as deployed. -/
|
||||||
|
noncomputable def Root (v : Bytes) (m n : Nat) (P : List Bytes) : Option Bytes :=
|
||||||
|
if n = 1 then
|
||||||
|
match P with
|
||||||
|
| [] => some v
|
||||||
|
| _ => none
|
||||||
|
else if n = 0 then none
|
||||||
|
else
|
||||||
|
match P.getLast? with
|
||||||
|
| none => none
|
||||||
|
| some s =>
|
||||||
|
let k := kbelow n
|
||||||
|
if m < k then
|
||||||
|
match Root v m k P.dropLast with
|
||||||
|
| none => none
|
||||||
|
| some x => some (hnode x s)
|
||||||
|
else
|
||||||
|
match Root v (m - k) (n - k) P.dropLast with
|
||||||
|
| none => none
|
||||||
|
| some x => some (hnode s x)
|
||||||
|
termination_by n
|
||||||
|
decreasing_by
|
||||||
|
· have h2 : 2 ≤ n := by omega
|
||||||
|
exact kbelow_lt n h2
|
||||||
|
· have := kbelow_pos n
|
||||||
|
omega
|
||||||
|
|
||||||
|
/-- `ConsRec` (paper §5.3): the recursive consistency verifier. Returns
|
||||||
|
the reconstructed pair (old root, new root); `none` = shape
|
||||||
|
mismatch. The flag `b` records whether the size-`n₀` subtree root is
|
||||||
|
carried implicitly (the pinned root `r`) or explicitly in `C`. -/
|
||||||
|
noncomputable def ConsRec (n₀ n : Nat) (C : List Bytes) (b : Bool) (r : Bytes) :
|
||||||
|
Option (Bytes × Bytes) :=
|
||||||
|
if n₀ = n then
|
||||||
|
if b then
|
||||||
|
match C with
|
||||||
|
| [] => some (r, r)
|
||||||
|
| _ => none
|
||||||
|
else
|
||||||
|
match C with
|
||||||
|
| [s] => some (s, s)
|
||||||
|
| _ => none
|
||||||
|
else if n₀ > n ∨ n₀ = 0 ∨ n ≤ 1 then none
|
||||||
|
else
|
||||||
|
match C.getLast? with
|
||||||
|
| none => none
|
||||||
|
| some s =>
|
||||||
|
let k := kbelow n
|
||||||
|
if n₀ ≤ k then
|
||||||
|
match ConsRec n₀ k C.dropLast b r with
|
||||||
|
| none => none
|
||||||
|
| some (x, y) => some (x, hnode y s)
|
||||||
|
else
|
||||||
|
match ConsRec (n₀ - k) (n - k) C.dropLast false r with
|
||||||
|
| none => none
|
||||||
|
| some (x, y) => some (hnode s x, hnode s y)
|
||||||
|
termination_by n
|
||||||
|
decreasing_by
|
||||||
|
· have h2 : 2 ≤ n := by omega
|
||||||
|
exact kbelow_lt n h2
|
||||||
|
· have := kbelow_pos n
|
||||||
|
omega
|
||||||
|
|
||||||
|
/-- The consumer's acceptance predicate for a consistency proof between
|
||||||
|
pinned head `(n₀, r₀)` and offered head `(n₁, r₁)` (paper §5.3). -/
|
||||||
|
def acceptCons (n₀ n₁ : Nat) (r₀ r₁ : Bytes) (C : List Bytes) : Prop :=
|
||||||
|
n₀ = 0 ∨ ConsRec n₀ n₁ C true r₀ = some (r₀, r₁)
|
||||||
|
|
||||||
|
end LTLAcc
|
||||||
BIN
verification/Proofs/Basic.olean
Normal file
BIN
verification/Proofs/Basic.olean
Normal file
Binary file not shown.
105
verification/check.sh
Executable file
105
verification/check.sh
Executable file
|
|
@ -0,0 +1,105 @@
|
||||||
|
#!/usr/bin/env bash
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
# check.sh — THE button (accumulator corpus). Same discipline as the
|
||||||
|
# *-ed25519-verified repos: compiles every shipped .lean through lean-guard
|
||||||
|
# and axiom-audits every certificate against its DOCUMENTED exact cone,
|
||||||
|
# both directions.
|
||||||
|
#
|
||||||
|
# Phases: 0 resource/integrity · 1 stub+axiom-smuggling audit ·
|
||||||
|
# 2 compile manifest · 3 boundary-exact axiom audit
|
||||||
|
# ─────────────────────────────────────────────────────────────────────────────
|
||||||
|
set -euo pipefail
|
||||||
|
source ~/aeneas-toolchain/env.sh
|
||||||
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||||
|
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||||
|
TIMEOUT="${LEAN_TIMEOUT:-600}"
|
||||||
|
export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}"
|
||||||
|
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||||
|
|
||||||
|
GEN_MODULES=( LTLAcc/HashExternal )
|
||||||
|
PROOFS=( Basic )
|
||||||
|
|
||||||
|
# Certificates and their exact expected cones (observed at first green
|
||||||
|
# compile, 2026-07-10; any drift in EITHER direction is a failure).
|
||||||
|
declare -A CONES=(
|
||||||
|
[LTLAcc.domsep]=""
|
||||||
|
[LTLAcc.kbelow_pos]="propext, Quot.sound"
|
||||||
|
[LTLAcc.kbelow_lt]="propext, Quot.sound"
|
||||||
|
[LTLAcc.le_two_kbelow]="propext, Quot.sound"
|
||||||
|
[LTLAcc.MTH]="propext, LTLAcc.sha256, Quot.sound"
|
||||||
|
[LTLAcc.Root]="propext, LTLAcc.sha256, Quot.sound"
|
||||||
|
[LTLAcc.ConsRec]="propext, LTLAcc.sha256, Quot.sound"
|
||||||
|
)
|
||||||
|
|
||||||
|
free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'
|
||||||
|
echo "=== Phase 0: source integrity ==="
|
||||||
|
for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do
|
||||||
|
[ -f "$f" ] || continue
|
||||||
|
if ! grep -qE '^(/-|import |namespace |theorem |def |noncomputable |open |set_option |--|abbrev )' "$f"; then
|
||||||
|
echo "CORRUPTED: $f is not Lean source. Restore: git checkout HEAD -- $f"; exit 1
|
||||||
|
fi
|
||||||
|
done
|
||||||
|
echo " all sources valid"
|
||||||
|
|
||||||
|
echo "=== Phase 1: stub + axiom-smuggling audit ==="
|
||||||
|
if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
||||||
|
echo "STUB DETECTED"; exit 1; fi
|
||||||
|
if grep -rn ' : True :=' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
||||||
|
echo "STUB DETECTED: True-target theorem"; exit 1; fi
|
||||||
|
if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean 2>/dev/null; then
|
||||||
|
echo "AXIOM SMUGGLING DETECTED: axiom under Proofs/ — gen/ is the only sanctioned site."; exit 1
|
||||||
|
fi
|
||||||
|
echo " clean"
|
||||||
|
|
||||||
|
echo "=== Phase 2: compile ==="
|
||||||
|
LOG=$(mktemp /tmp/acc-check-XXXX.log)
|
||||||
|
cd "$AENEAS_LEAN"
|
||||||
|
lake env bash -c "
|
||||||
|
set -euo pipefail
|
||||||
|
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||||
|
compile() {
|
||||||
|
echo \" · \$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'
|
||||||
|
for m in ${PROOFS[*]}; do
|
||||||
|
[ -f \"Proofs/\$m.lean\" ] || { echo \"MISSING: Proofs/\$m.lean\"; exit 1; }
|
||||||
|
compile \"Proofs/\$m\"
|
||||||
|
done
|
||||||
|
for f in Proofs/*.lean; do
|
||||||
|
b=\$(basename \"\$f\" .lean)
|
||||||
|
[ \"\$b\" = AxiomCheck ] && continue
|
||||||
|
case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f\"; exit 1;; esac
|
||||||
|
done
|
||||||
|
"
|
||||||
|
if grep -q "uses 'sorry'" "$LOG"; then echo "STUB: sorry detected"; exit 1; fi
|
||||||
|
rm -f "$LOG"
|
||||||
|
|
||||||
|
echo "=== Phase 3: boundary-exact axiom audit ==="
|
||||||
|
AUD=$(mktemp /tmp/acc-audit-XXXX.log)
|
||||||
|
cd "$AENEAS_LEAN"
|
||||||
|
lake env bash -c "
|
||||||
|
cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
|
||||||
|
LEAN_TIMEOUT=300 LEAN_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/AxiomCheck.lean
|
||||||
|
" > "$AUD" 2>&1 || { cat "$AUD"; exit 1; }
|
||||||
|
FAIL=0
|
||||||
|
for cert in "${!CONES[@]}"; do
|
||||||
|
want="${CONES[$cert]}"
|
||||||
|
if [ -z "$want" ]; then
|
||||||
|
exp="'$cert' does not depend on any axioms"
|
||||||
|
else
|
||||||
|
exp="'$cert' depends on axioms: [$want]"
|
||||||
|
fi
|
||||||
|
if ! grep -qF "$exp" "$AUD"; then
|
||||||
|
echo " CONE DRIFT: $cert"
|
||||||
|
echo " expected: $exp"
|
||||||
|
echo " observed: $(grep -F "'$cert'" "$AUD" || echo '(missing)')"
|
||||||
|
FAIL=1
|
||||||
|
else
|
||||||
|
echo " ✓ $cert [$want]"
|
||||||
|
fi
|
||||||
|
done
|
||||||
|
rm -f "$AUD"
|
||||||
|
[ "$FAIL" = 0 ] || exit 1
|
||||||
|
echo "=== ALL GREEN ==="
|
||||||
12
verification/gen/LTLAcc/HashExternal.lean
Normal file
12
verification/gen/LTLAcc/HashExternal.lean
Normal file
|
|
@ -0,0 +1,12 @@
|
||||||
|
/- The single sanctioned axiom site of this corpus (mirrors the role of
|
||||||
|
gen/ in the *-ed25519-verified repos): SHA-256 as an opaque function.
|
||||||
|
No properties are assumed of it — in particular NOT collision
|
||||||
|
resistance. The soundness theorems downstream are constructive: they
|
||||||
|
EXHIBIT two distinct preimages with equal image. Believing such a
|
||||||
|
pair cannot be found is the reader's interpretation step, exactly as
|
||||||
|
documented in the paper (§6, Remark 1). -/
|
||||||
|
namespace LTLAcc
|
||||||
|
|
||||||
|
axiom sha256 : List UInt8 → List UInt8
|
||||||
|
|
||||||
|
end LTLAcc
|
||||||
BIN
verification/gen/LTLAcc/HashExternal.olean
Normal file
BIN
verification/gen/LTLAcc/HashExternal.olean
Normal file
Binary file not shown.
189
verification/lean-guard
Executable file
189
verification/lean-guard
Executable file
|
|
@ -0,0 +1,189 @@
|
||||||
|
#!/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 <MB> — 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 <file.lean> [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
|
||||||
|
|
||||||
|
# No core dumps: hitting the memory cap makes lean (and uutils `timeout`) abort;
|
||||||
|
# those aborts are EXPECTED and their core dumps only trigger Ubuntu apport
|
||||||
|
# popups and fill /var/crash. ulimit applies to this shell and every child.
|
||||||
|
ulimit -c 0 2>/dev/null || true
|
||||||
|
|
||||||
|
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 <file.lean> [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
|
||||||
|
|
||||||
|
|
||||||
|
# ── 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).
|
||||||
|
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)"
|
||||||
|
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"
|
||||||
|
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" "$@"
|
||||||
|
}
|
||||||
|
do_compile() {
|
||||||
|
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" "$@"
|
||||||
|
else
|
||||||
|
echo " (systemd-run unavailable — falling back to lean -M only)" >> "$LOG_FILE"
|
||||||
|
run_leancmd "$@"
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
do_compile "$@"
|
||||||
|
EXIT_CODE=$?
|
||||||
|
|
||||||
|
# ── Guard 3a: lazy wait-and-retry after a clamped memory abort (pass 3) ─────
|
||||||
|
# The clamp above protects the host, but under ambient memory pressure it
|
||||||
|
# can cut a KNOWN-NEEDED cap (ReduceSpec peaks ~6.5G) and guarantee an
|
||||||
|
# interpreter abort that reads like a proof regression. Lazy semantics keep
|
||||||
|
# light files free: only when a CLAMPED run dies on memory (134 abort /
|
||||||
|
# 137 cgroup kill) and LEAN_MEM_WAIT_SEC>0, wait — still under the
|
||||||
|
# single-flight lock — until the ORIGINAL request is affordable, then retry
|
||||||
|
# once at full cap. Default 0: behavior unchanged.
|
||||||
|
MEM_WAIT_SEC=${LEAN_MEM_WAIT_SEC:-0}
|
||||||
|
if [ "$WAS_CLAMPED" -eq 1 ] && [ "$MEM_WAIT_SEC" -gt 0 ]; then
|
||||||
|
WAITED=0
|
||||||
|
# Retry ladder: whenever headroom improves MATERIALLY (>= +1536MB over
|
||||||
|
# the cap that just died, or reaches the full request), retry at the
|
||||||
|
# new clamp. The full request may never be affordable on a loaded host
|
||||||
|
# even though the true peak is — climbing the ladder finds the passing
|
||||||
|
# clamp without knowing the peak. Monotone caps + deadline => bounded.
|
||||||
|
while { [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; } \
|
||||||
|
&& [ "$WAITED" -lt "$MEM_WAIT_SEC" ] && [ "$MEM_MB" -lt "$REQ_MEM_MB" ]; do
|
||||||
|
sleep 20; WAITED=$(( WAITED + 20 ))
|
||||||
|
AVAIL_MB=$(free -m | awk '/Mem:/{print $7}')
|
||||||
|
NEW_AFFORD=$(( AVAIL_MB - MIN_FREE_MB ))
|
||||||
|
if [ "$NEW_AFFORD" -ge "$REQ_MEM_MB" ] || [ "$NEW_AFFORD" -ge $(( MEM_MB + 1536 )) ]; then
|
||||||
|
MEM_MB=$(( NEW_AFFORD < REQ_MEM_MB ? NEW_AFFORD : REQ_MEM_MB ))
|
||||||
|
CGROUP_MB=$(( MEM_MB + 1024 ))
|
||||||
|
echo "lean-guard: clamped run died (rc=$EXIT_CODE); retrying at -M ${MEM_MB}MB after ${WAITED}s (avail=${AVAIL_MB}MB, request=${REQ_MEM_MB}MB)"
|
||||||
|
echo "[$(date -u +%F' '%T)] RETRY $LEAN_FILE (M=${MEM_MB}MB cg=${CGROUP_MB}MB avail=${AVAIL_MB}MB after ${WAITED}s)" >> "$LOG_FILE"
|
||||||
|
do_compile "$@"
|
||||||
|
EXIT_CODE=$?
|
||||||
|
fi
|
||||||
|
done
|
||||||
|
if [ "$EXIT_CODE" -eq 134 ] || [ "$EXIT_CODE" -eq 137 ]; then
|
||||||
|
echo "lean-guard: memory-death persists after ${WAITED}s of ladder retries (last -M ${MEM_MB}MB, request ${REQ_MEM_MB}MB) — keeping the failure"
|
||||||
|
fi
|
||||||
|
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
|
||||||
Loading…
Reference in a new issue