Skip to content

Releases: Manuel0921/lambdasat-lean

LambdaSat v1.2.0: ILP Certificate Verification

25 Feb 15:41
@Manuel0921 Manuel0921
v1.2.0
945a579

Choose a tag to compare

View all tags
LambdaSat v1.2.0: ILP Certificate Verification Latest
Latest

Highlights

  • 15 new theorems for ILP certificate verification pipeline
  • checkSolution soundness: checkRootActive_sound, checkExactlyOne_sound, checkChildDeps_sound, checkAcyclicity_sound
  • Encoding properties: encodeEGraph_rootClassId, encodeEGraph_numClasses
  • Fuel sufficiency: extractILP_fuel_mono, mapOption_mono
  • Certificate evaluation: evalVar simp lemmas, checkBounds_sound, isFeasible_sound
  • 9 new edge-case tests (T15-T23) for ILP pipeline — 23/23 total PASS
  • TESTS_OUTSOURCE.md: full QA test specifications (32 properties, 49 integration tests)

Stats

Metric Value
Theorems 248
LOC 8,956
Sorry 0
Custom axioms 0
External hypotheses 0
Integration tests 23/23 PASS
Phases complete 9/9

What's new since v1.1.0

v1.1.0 achieved zero external hypotheses in full_pipeline_soundness. v1.2.0 adds formal verification of the ILP extraction pipeline — proving that checkSolution correctly validates solver certificates, that encodeEGraph preserves structural properties, and that extractILP is monotone in fuel.

The ILP solver remains outside the TCB. Its output is validated by checkSolution (now with proven soundness) before extraction.

Build

git clone https://github.com/Manuel0921/lambdasat-lean.git
cd lambdasat-lean
lake build
lake env lean Tests/IntegrationTests.lean  # 23/23 PASS

Requires elan + Lean 4 toolchain leanprover/lean4:v4.26.0. No Mathlib dependency.

Assets 2
Loading