[dependabot]

Bumps ordeal from 0.22.1 to 0.36.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.36.0

Falsification statement

ordeal-recheck (TR-075, #277) re-checks ordeal-cert/v1..v4 bundles through the trusted ordeal-lrat checks. Its dependency closure contains no solver, which the required Test job checks. It ships as native binaries and a wasm32-wasip2 component. The certificate types moved to the new ordeal-cert crate, re-exported at their old paths. Bundles are byte-identical to v0.35.0's on 64-bit hosts.

Both wasm components are also published keyless-signed with wsc, under the release workflow's OIDC identity (TR-076, #278). The unsigned, reproducible modules are unchanged.

An MC/DC ratchet with witness gates coverage of ordeal-lrat against a committed baseline (TR-077, #279).

Kani (TR-078, #280, #169) is a confidence change only, and no solver behaviour changed. A verdict job now turns the run red when a proof job fails. 16 wide harnesses run nightly. The four that lose the hosted runner, and the width-8 divider, are unscheduled for measured reasons.

Falsification: this release is wrong if ordeal-recheck accepts a bundle whose CNF/LRAT, SAT witness or query binding does not check, or rejects one that ordeal 0.36.0 emitted and that checks. It is also wrong if a published *.signed.wasm passes wsc verify against this tag's release.yml identity while its detached module differs from the published .wasm. It is also wrong if a Kani tier job fails on a run whose conclusion is success.

Release note (rivet, from the trace)

8 artifact(s) in scope: 8 delivered, 0 withheld.

Functionalities provided

sw-req

• TR-075 (verified) — ordeal-recheck: standalone signed binary + wasm component that re-checks ordeal-cert bundles
• TR-076 (verified) — The wasm32-wasip2 components are wsc keyless-signed and the signature is verified on the published bytes
• TR-077 (verified) — witness MC/DC truth table for ordeal-lrat's checker decisions as release evidence, ratcheted in CI
• TR-078 (verified) — Every 32/64 Kani harness is measured and tiered by its measured cost, and the Kani run conclusion reports a failed proof job

sw-verification

• VER-075 (verified) — ordeal-recheck accepts every v1-v4 solver bundle and rejects each mutant by the recheck; solver-free closure gated and negative-controlled; bundles byte-identical across the extraction (TR-075)
• VER-076 (verified) — wsc keyless signatures on the wasm components: accepted for the release identity, detach to the published bytes, rejected for a wrong identity, a byte mismatch and a flipped byte (TR-076)
• VER-077 (verified) — MC/DC ratchet over ordeal-lrat — gate on the pristine tree, two negative controls restored byte for byte, the CI workflow (TR-077)

... (truncated)

Changelog

Sourced from ordeal's changelog.

[0.36.0] - 2026-11-05

Added

• ordeal-recheck, a standalone bundle re-checker with no solver in it (TR-075, #277). ordeal-recheck [--format text|json] <bundle.json>... reads each bundle's declared format (ordeal-cert/v1..v4) and verdict (unsat / sat), decodes it with the matching hash-verifying reader and runs that format's full recheck through the trusted ordeal-lrat checks. It prints accepted or rejected (with the reason) per file and exits 0 iff every bundle is accepted, 1 if any is rejected or malformed, and 2 on a bad flag. --version prints ordeal-recheck <semver>. Its normal dependency tree contains no ordeal (nor cadical-sys / z3); scripts/recheck_closure.sh checks this in the required Test job, and a negative control (ordeal added as a dependency) was seen to turn it red. The release workflow builds it as a native binary per release target (ordeal-recheck-vX.Y.Z-<target>.tar.gz) and as a wasm32-wasip2 component. Both go into the cosign-signed SHA256SUMS.txt with SLSA provenance, are smoke-tested on committed real-solver bundles, and are checked by scripts/verify_release.sh.

• ordeal-cert, the certificate crate (TR-075). The certificate data types and their recheck() methods (Certificate, Model, the SAT witness, QueryDag / QueryInputs / QueryTerm / SliverBlock / ExtQuery / SliverModel and the v2–v4 certificate types), the encoding constants and node spellings, the in-tree SHA-256 and, behind its json feature, the ordeal-cert/v1..v4 bundle codec moved verbatim out of ordeal. It depends on ordeal-lrat only (serde with json). New in it: cert_bundle::bundle_header (the declared format and verdict, for dispatch). Published to crates.io in the order ordeal-lrat → ordeal-cert → ordeal → ordeal-recheck.

• Keyless-signed wasm components (TR-076, #278). The release workflow signs ordeal-vX.Y.Z-wasm32-wasip2.wasm and ordeal-recheck-vX.Y.Z-wasm32-wasip2.wasm with wsc sign --keyless (sigil, Sigstore keyless with the release workflow's GitHub OIDC identity). It publishes each as *.signed.wasm next to the unsigned, reproducible module, which is unchanged. Before upload the workflow verifies each signature against the exact workflow identity and checks that wsc detach returns the published .wasm byte for byte. The signed files are listed in the cosign-signed SHA256SUMS.txt. scripts/verify_release.sh repeats both checks on the published assets. Its negative control is one flipped byte, which wsc verify must reject.

• MC/DC ratchet over the trusted checker (TR-077, #279). scripts/mcdc_gate.sh measures MC/DC over ordeal-lrat with witness 0.45.0 and compares the per-file numbers with mcdc/baseline.txt. A drop in coverage fails the mcdc.yml job. Two negative controls were each seen to turn the gate red: 50 sliver reject rows removed, and an uncovered branch in a scratch copy of the checker.

Changed

... (truncated)

Commits

• 8dc8046 Merge pull request #292 from pulseengine/chore/release-v0.36.0
• a4091ed chore(release): bump the MC/DC harness lockfile to ordeal-lrat 0.36.0
• 66f598f chore(release): v0.36.0 — a re-checker with no solver in it, signed wasm, a c...
• a64a19e Merge pull request #291 from pulseengine/feat/v0.36.0-kani-wide
• 6b9061d trace(kani): VER-078 with execution VE-068 and verdict VV-142
• 0892b3a Merge origin/main (#290) into feat/v0.36.0-kani-wide
• 8808634 Merge pull request #290 from pulseengine/feat/v0.36.0-wsc-signing
• 5cb8a5a kani: four wide harnesses back to unscheduled; a verdict job makes the run te...
• 8776211 test(cli_term): tolerate EPIPE when ordeal exits before reading stdin
• 41f3ca6 feat(release): wsc keyless signatures on the wasm components (TR-076)
• Additional commits viewable in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

[github-actions]

🔒 HELD — not auto-mergeable (class: zerox-minor). 0.22.1 -> 0.36.0: for a 0.x crate the MINOR is the de-facto major (ordeal 0.9->0.12; object 0.39->0.40 / #938)

Auto-merge has been actively disabled and asserted off by the hold gate (#965). For a 0.x crate the MINOR component is the de-facto major (and for 0.0.x, the patch): ordeal 0.9→0.12 auto-merged as "minor" and hung Test+Z3 for days; object 0.39→0.40 (#938) broke 16 call sites across three unrelated newtype surfaces. Merge this BY HAND only once the FULL suite is green, including the separate --features z3-solver path (required context "Z3 Verification") — the discriminator is CI, not a read of the diff.