input-output-hk / input-output-hk/Lean-blaster
Reconstruction module audit
Open
area: proof reconstruction
- Dominant language
- Lean
- Stars
- 57
- Forks
- 11
- Avg merge
- 1d 5h
- Merged PRs (30d)
- 10
Description
**Goal:** Open, exploratory review of the whole proof reconstruction module.
**DoD:**
- [ ] `#print axioms` on every theorem reconstructed from the core-type reductions (Int/relational, Bool, Prop, Decide, Eq) shows only the expected axioms, no `blasterProven` / `sorryAx`.
- [ ] Every in-scope (M1) optimization rule is actually exercised by at least one test, including proof reconstruction.
- [ ] Findings logged.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.