ordeal v0.4.2

What's Changed

• proof(lean): apply_delete simulation leaf toward kernel_refines_pure (#12) by @avrabe in #37
• release: v0.4.2 — Solver::prove_equiv layout oracle (spar #38) by @avrabe in #41

Full Changelog: v0.4.1...v0.4.2

ordeal v0.4.1

What's Changed

• release: v0.4.1 — SMT-LIB2 CLI front-end + README fix (loom #34) by @avrabe in #36

Full Changelog: v0.4.0...v0.4.1

ordeal v0.4.0

What's Changed

• chore(plan): re-sequence releases to unblock roadmap work by @avrabe in #27
• feat(lean): second simulation leaf — load_cnf_refines (sorry-free) by @avrabe in #28
• feat(field): synth ask 1 — BvTerm::Ite bool→BV bridge by @avrabe in #30
• feat(field): synth ask 3 — Solver::check_with_limit (conflict budget) by @avrabe in #31
• feat(field): synth ask 2 — ordeal::lowering derived-op helpers by @avrabe in #32
• release: v0.4.0 — synth field asks (ite, lowering, bounded check) by @avrabe in #33

Full Changelog: v0.3.0...v0.4.0

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

ordeal v0.2.0

What's Changed

• ci: fix Format job (rustfmt) + invalid @platforms loads in Bazel platforms by @avrabe in #2
• [temper] Configuration update by @temper-pulseengine[bot] in #3
• chore(deps): Bump actions/upload-artifact from 4 to 7 by @dependabot[bot] in #5
• chore(trace): reconcile rivet graph with architecture; rivet is source of truth by @avrabe in #8
• chore(trace): adopt rivet 0.23 release management; trailer-safe FEAT ids by @avrabe in #9
• feat(p1): QF_BV decision pipeline — blast, AIG, Tseitin, own CDCL, Z3-differential green by @avrabe in #10
• docs(roadmap): mirror P1 completion from rivet by @avrabe in #11
• chore(deps): Bump actions/checkout from 4 to 7 by @dependabot[bot] in #7
• chore(deps): Bump actions/download-artifact from 4 to 8 by @dependabot[bot] in #6
• chore(deps): Bump actions/attest-build-provenance from 1 to 4 by @dependabot[bot] in #4
• feat(p2): certificate-checked Unsat — LRAT emission validated by ordeal-lrat by @avrabe in #13
• chore(trace): verification evidence + verified-status closure; repro-build CI job by @avrabe in #14
• chore: drop committed bazel output symlinks by @avrabe in #15
• release: v0.2.0 — version bump, changelog roll, two-crate publish order by @avrabe in #16

New Contributors

• @avrabe made their first contribution in #2
• @temper-pulseengine[bot] made their first contribution in #3
• @dependabot[bot] made their first contribution in #5

Full Changelog: https://github.com/pulseengine/ordeal/commits/v0.2.0

Falsification statement

This release is wrong if any well-sorted query over the closed fragment yields: a Sat model that does not re-evaluate to true; an Unsat whose carried LRAT certificate the ordeal-lrat checker rejects on independent re-check; or any verdict that disagrees with Z3 on the same query.

Trust status

Unsat verdicts are validated by the dependency-free, mutation-tested ordeal-lrat checker before being returned. The checker's formal soundness proof (Rust → Lean 4 via Aeneas) is the tracked remaining obligation: #12.