Skip to content

ordeal v0.2.0

Choose a tag to compare

@github-actions github-actions released this 02 Jul 11:56
v0.2.0
9ca687f

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.