ordeal v0.3.0
What's Changed
- feat(lrat): split the checker into a string-free kernel and an untrusted parser by @avrabe in #17
- feat(lean): Aeneas translates the kernel with zero errors — Lean model committed by @avrabe in #18
- feat(lean): the checker model elaborates — lake package, spec stated, CI gate by @avrabe in #19
- ci: publish with the org-wide CRATES_IO_TOKEN secret by @avrabe in #20
- feat(lean): pure-checker soundness proved (sorry-free); #12 reduced to simulation by @avrabe in #21
- feat(lean): first verified simulation leaf (chil_total); Aeneas WP idiom established by @avrabe in #22
- feat(p3): sliver foundation — extended-term layer + preprocessing contract by @avrabe in #23
- feat(p3): sliver lowering — read-over-write + Ackermannization, Z3-differential green by @avrabe in #24
- feat(p3): Solver::check_sliver — public entry for array/UF queries by @avrabe in #25
- release: v0.3.0 — array/UF sliver trial release by @avrabe in #26
Full Changelog: v0.2.0...v0.3.0