chore(deps): bump ordeal from 0.18.0 to 0.19.0

[dependabot]

Bumps ordeal from 0.18.0 to 0.19.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.19.0

What's Changed

• chore(rivet): v0.18.0 shipped & verified — TR-033 verified on published assets by @​avrabe in pulseengine/ordeal#118
• docs: #48 design — single-source the trusted Lean models (design-doc gate) by @​avrabe in pulseengine/ordeal#119
• fix(cli): #120 — machine-quotable --version/-V + tag-version release assert by @​avrabe in pulseengine/ordeal#121
• feat(tcb): TR-034 — Lean models become build products (drift unrepresentable) by @​avrabe in pulseengine/ordeal#122
• chore(tcb): retire the drift workflow — TR-034 verified (gate swap recorded) by @​avrabe in pulseengine/ordeal#125
• fix(ci): regen.sh builds to GC roots — warm regen 20 min → 4 s by @​avrabe in pulseengine/ordeal#126
• fix(ci): salt the nix cache key with regen.sh (exact-key hits skip saves) by @​avrabe in pulseengine/ordeal#127
• feat(tcb): TR-035 — adversarial dual-mechanisation differential (Lean core LRAT.check vs ordeal-lrat) by @​avrabe in pulseengine/ordeal#128
• chore(release): v0.19.0 — TCB deepening (generation by construction + adversarial dual-mechanisation) by @​avrabe in pulseengine/ordeal#129

Full Changelog: pulseengine/ordeal@v0.18.0...v0.19.0

Changelog

Sourced from ordeal's changelog.

[0.19.0] - 2026-08-20

TCB deepening: drift made unrepresentable, and a second mechanisation run adversarially (FEAT-scope: TR-034, TR-035, TR-036, TR-033 verification; issues #48, #47, #120, #116 tail). The releases's theme is the verification-approach sweep: generation over checking, independence used adversarially.

Changed

• The trusted Lean models are build products, never committed (TR-034/VER-031, #48): lean/Kernel.lean and lean/BlastKernel.lean left the tree; the required Lean CI job regenerates both from the Rust sources (Charon/Aeneas pinned once, in lean/toolchain-pins.env) before every proof build. A proof about a stale model is now unrepresentable — and the previously UNGUARDED blaster model drift surface is closed by construction. The #44 drift workflow retired via an ordered branch-protection swap (never weaker at any commit). One-time mutation demonstrations recorded: a fail-open check_rup and an xor→or blast_kernel mutation — one line each, no manual model step — each turned the required Lean job red at exactly its own proof development.
• CI: the regenerating Lean job runs warm in ~28 s (three stacked cache defects found and fixed: nix run leaves no GC root; exact-key cache hits skip saves; PR-branch caches are invisible to main).

Added

• Adversarial dual-mechanisation differential (TR-035/VER-033, #47): ordeal's Aeneas-proven checker differenced against Lean core's independently verified Std.Tactic.BVDecide.LRAT.check on a deterministic 48-pristine + 16-mutant corpus (examples/ dump_lrat_corpus.rs, lake exe diffcheck), gated in CI — any verdict disagreement is a hard error. The differential immediately surfaced two real LRAT spec ambiguities (Lean core resolves hints positionally, ignoring declared step ids; its formula loader preloads original unit clauses) — both sides sound, ordeal strictly stricter, both documented in lean/DiffCheck.lean rather than papered over.
• CLI version baseline (TR-036/VER-032, #120, org survey pulseengine.eu#167): --version/-V/version print ordeal <semver> and exit 0; unknown flags keep the strict exit-2 reference behaviour; the help banner's honesty text is pinned by test; the release workflow asserts each freshly built native binary self-reports exactly the tagged version (first exercised by this release).
• TR-033 (cosign-signed checksums, shipped v0.18.0) verified against the published assets: cosign verify-blob Verified OK; varve layer 2026.08.2 re-added ordeal signed.

Scope

• TR-032 (seed-portfolio parallelism) deferred to v0.20.0 by explicit decision — its measure-first activation condition has not fired.

Commits

• 9655069 chore(release): v0.19.0 — TCB deepening: generation by construction + adversa...
• 6f2c192 feat(tcb): TR-035 — adversarial dual-mechanisation differential (Lean core LR...
• fec4847 fix(ci): salt the nix cache key with regen.sh — exact-key hits skip saves (#127)
• d4248fc fix(ci): regen.sh builds Charon/Aeneas to GC roots — warm regen 20min -> 4s (...
• 8f25fd6 chore(tcb): retire the #44 drift workflow — guarantee absorbed by constructio...
• 3f0d1e5 feat(tcb): TR-034 — the Lean models become build products; drift unrepresenta...
• 0df876a fix(cli): #120 — machine-quotable --version/-V, tag-version release assert (#...
• cd8ac5f docs: #48 design — single-source the trusted Lean models (TR-034/TR-035 draft...
• 24366cf chore(rivet): v0.18.0 shipped & verified — TR-033 verified on published asset...
• See full diff 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.18.0 -> 0.19.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.