ordeal v0.24.0

Falsification statement

The Lean shift and rotate theorems hold at every bit-width 1..128. The
reference blaster matches the shipped one (#201). A release's test evidence
is the tagged commit's own CI run, mapped to rivet measures (#203). ordeal
records its own certificate bundles and supply chain with its own rivet
types (#191). Kani proves the width-32/64 light rules on CI (#169).

Falsification: this release is wrong if its release run passes the gate
without reading this commit's own CI test results; or if a shift or rotate
at a non-power-of-two width gets a checker-validated unsat from ordeal
0.24.0 while Z3 reports sat; or if evidence/certs/*.json does not
regenerate byte-identically from its recorded recheck command.

Release note (rivet, from the trace)

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

Functionalities provided

sw-req

• TR-056 (verified) — The shift and rotate blaster proofs hold at every width, and the Lean-proven reference matches the shipped blaster there (#201)
• TR-057 (verified) — A release's test evidence comes from the tagged commit's own CI run, not from hand-written verdicts (#203)
• TR-058 (verified) — ordeal records its own certificates and release supply chain with the rivet evidence types it asks consumers to use (#191)

sw-verification

• VER-056 (verified) — Shift/rotate capstones proven at every width, axiom-clean; reference matches shipped blaster on the full rotr domain (TR-056)
• VER-057 (verified) — CI results map to measures and gate the release, with negative controls (TR-057)
• VER-058 (verified) — ordeal's own certificate and supply-chain evidence validates and re-checks (TR-058)

Limitations in relation to the committed scope

None — every artifact committed to v0.24.0 is release-ready.

Result of verification measures

1 of 6 delivered artifact(s) have NO verification evidence (neither a verifies link nor a source marker):

• VER-057

Changes since v0.23.0

• 9260a3ab feat(evidence): #191 ordeal dogfoods its own rivet evidence types; unsynced externals removed (TR-058) (#213) — refs #191, #213
• 9919657d feat(evidence): #203 test results come from the CI run — nextest JUnit mapped to rivet measures, gating the release (TR-057) (#211) — refs #203, #211
• 0ad7cd89 fix(blaster): #201 shift/rotate proofs hold at every width — the reference blaster matches the shipped one, hpow dropped, rotr reduces mod w (TR-056) (#210) — refs #201, #210

Not covered by this note

Automotive SPICE 11-03 names these release-note elements. rivet does not yet compute them, so they are declared rather than omitted:

• application parameters — not modelled
• configurations and variants — the variant subsystem exists but is not wired in here
• intended area and environment of usage — not modelled
• impact to other components linked to the release — needs the cross-repo externals graph
• upstream or downstream compatibility — not modelled
• copyright and license information — the cargo-deny licenses gate produces this but it is not read here
• approval for delivery by responsible roles — rivet check review-signoff enforces it but emits no record (REQ-333)
• dependencies to other linked products — not modelled

Prose

See CHANGELOG.md for the narrative of this release.