Certified feature-model / variant consistency via ordeal's SAT core (EU AI Act evidence)

[avrabe]

rivet's variant solve (rivet-cli serve/variant.rs, feature-model*.yaml, #128/#466) validates configurations but produces no certificate, while EU AI Act Art. 12 audits (#99, #104) demand per-configuration trace evidence.

Proposal (two parts):

1. Decide feature-model / variant consistency with ordeal's certified propositional-SAT core (exposed below the bit-blaster) and emit a cert.recheck()-able "config is valid / model is consistent" artifact — ordeal roadmap v0.14.0 (FEAT-011): the certificate as evidence — rules_ordeal + rivet artifact type + SAT front-end ordeal#67 (v0.13.0, propositional-SAT front-end).
2. Define an ordeal-certificate rivet evidence artifact type (same ci: VS Code extension test infrastructure #67) so every verified transform in the toolchain — loom rule proofs, synth codegen, sigil overflow, spar layout, gale bitvector — lands as a machine-re-checkable DO-178C/ISO-26262/EU-AI-Act artifact rivet ingests. This is the cross-cutting evidence-spine piece; rivet is the natural consumer.

Boundary: feature-model consistency is propositional SAT (in scope, certified); no new theory needed.

Acceptance Criteria — Part 2 (ordeal-certificate artifact type — unblocked by ordeal v0.17.0)

• New embedded schema (schemas/ordeal-certificate.yaml, or extend common.yaml) declares an ordeal-certificate artifact type carrying: produced-by (tool + version), checked-by (verifier + version), attests (claim: variant-consistent / variant-inconsistent / etc. + standards: DO-178C / ISO 26262 / EU-AI-Act-Art-12), cnf-sha256 + cnf-ref, proof-sha256 + proof-ref (LRAT for UNSAT / self-checked model for SAT per the honest boundary), and a structured recheck block (command, expect-exit).
• Typed attests link-field: attests-transform (link → the artifact whose transform this certificate attests — a variant config, a loom rule, a synth codegen, a sigil overflow, a spar layout, a gale bitvector). Allowed-target rule declared so rivet validate's link-target-type check catches misuse.
• rivet validate treats a re-checked certificate as a verification link, not a claimed status: a verifies link from a verification artifact to an ordeal-certificate whose recheck.command was run and exited 0 (recorded via verification-result or an equivalent field) counts toward coverage; a certificate whose recheck was never run does not.
• Honest SAT boundary baked into the schema: for attests.claim: variant-consistent (SAT), the proof-* fields hold the self-checked model — ordeal ships no independently re-checkable SAT witness yet (UNSAT is the certificate-carrying verdict). Documented in the schema + the docs topic.
• v1 reader boundary as an expected-error fixture: ordeal-cert/v1 is inline-payload-only — a bundle using cnf_ref/proof_ref indirection must surface as a legible Unsupported-class validation error, not a mystery deserialize failure (the boundary ordeal's from_cert_v1 enforces as BundleError::Unsupported).
• Golden-file test: an ordeal-certificate artifact serializes / parses round-trip byte-identical; a link-target-type fixture demonstrates the attests-transform allowed-targets enforcement; a coverage-rule fixture demonstrates the "re-checked → counts" vs. "never re-checked → does not count" split.
• rivet docs topic (e.g. docs/artifact-types/ordeal-certificate.md) explains the shape, the SAT boundary, and the recheck invocation contract, with ordeal-cert/v1 as shipped (ordeal v0.17.0, cert-bundle feature: Certificate::to_cert_v1 / from_cert_v1 with both content sha256s verified before parse returns, UnsatBundle::recheck()) linked as the upstream serialization contract.
• Commit trailers: Implements: REQ-NNN (new REQ for the certificate ingestion type) + Refs: ordeal#67, #693.
• Explicitly out of scope (Part 1, file separately): the --certify flag on rivet release check --variant / rivet variant solve that shells out to ordeal's propositional-SAT front-end and emits the certificate; the CI wiring; the rules_ordeal gate; the UNSAT-core surfacing as a variant validate diagnostic.

[avrabe]

Timely — rivet v0.26.0 (about to tag) shipped REQ-254 / DD-075: rivet release check <version> --variant <name>, which decides release ∩ variant consistency (in-scope / out-of-scope / variant-only) and cuttability scoped to the intersection. That's the uncertified baseline this issue proposes to certify — it's the natural CLI seam.

rivet-side boundary (what rivet owns)

Part 2 — the ordeal-certificate evidence artifact type is squarely rivet's, and can be co-designed now (it doesn't need the SAT core to exist, only the serialization contract):

• A new artifact type (embedded schema) that carries: the certificate blob (or a content-addressed pointer + hash), the transform it attests, the standard(s) it satisfies (DO-178C / ISO 26262 / EU AI Act Art. 12), and a recheck command/hash so rivet validate can treat "certificate re-checks" as a verification link, not just a claimed status.
• This generalizes beyond variants: loom rule proofs, synth codegen, sigil overflow, spar layout, gale bitvector all land as the same ingestible type. rivet is the consumer/spine.

Part 1 — certified variant decision hooks into the existing seam: a --certify flag on rivet release check --variant (and rivet variant solve) that shells the feature model + config to ordeal's propositional-SAT front-end and emits the cert.recheck()-able artifact. This part is blocked on ordeal#67 (the SAT front-end + a stable certificate serialization).

What I need from ordeal (#67) to unblock the rivet side

1. The certificate serialization (CNF+LRAT bundle format + envelope) — the exact bytes rivet ingests and re-checks. Define this and rivet can define the artifact type against it immediately.
2. The invocation contract — how rivet hands ordeal a feature model + variant config (rivet already resolves both: feature_model::solve + bindings) and what ordeal returns (valid+cert / UNSAT-core+cert).

Proposed sequencing

• Now (rivet, unblocked): file the rivet requirement + a design decision for the ordeal-certificate artifact type; draft the schema against ordeal's proposed serialization.
• When ordeal#67 lands: wire --certify into release check/variant solve, add rules_ordeal as the CI gate, and make rivet validate accept a re-checked certificate as verification evidence.

Filing this as a rivet requirement (backlog, blocked-by ordeal#67) and linking both ways. Boundary agreed: feature-model consistency is propositional SAT — in scope, certified, no new theory.

[avrabe]

Answered both contract questions on ordeal#67 (pulseengine/ordeal#67, comment). Summary so rivet Part 2 is unblocked now:

• Serialization: ordeal-cert/v1 — a JSON envelope over the trusted {cnf: Vec<Vec<i32>>, lrat} payload, with produced_by/checked_by provenance, attests (claim + standards), content-addressed *_sha256 (inline small / *_ref for MB-scale proofs), and a recheck block (ordeal-lrat check <problem> <proof>) so rivet validate treats "re-checks OK" as a verification link, not a claimed status. Define the ordeal-certificate artifact type + schema against that shape now.
• Honest boundary to bake into the schema: UNSAT verdicts carry a full re-checkable LRAT cert today; SAT (config-consistent) verdicts carry a self-checked model — a fully independent re-checkable SAT witness lands in ordeal FEAT-012 / v0.14.0. So variant consistent = verdict: sat + model for now.
• Invocation: rivet hands the lowered feature-model ∧ config CNF (you already resolve both via feature_model::solve + bindings); ordeal returns the bundle (sat+model / unsat+LRAT / unknown). UNSAT-core (minimal conflicting-requirement subset) is a fast-follow — say if you want it in v1.

If any envelope field/vocabulary needs to differ for rivet's ingestion, comment on ordeal#67 and I'll fold it into the v1 spec before it's implemented. The --certify wiring (Part 1) tracks ordeal#67 (v0.13.0).

[avrabe]

Triage from the scheduled issue-fixing routine (first pass on this issue).

The body + your 2026-07-11 comments trace a well-scoped, two-part design: Part 2 — the ordeal-certificate rivet evidence artifact type — is squarely rivet's (co-designable now against the ordeal-cert/v1 envelope shape you just pinned on ordeal#67); Part 1 — wiring --certify into rivet release check --variant / rivet variant solve — is blocked on ordeal#67 landing the SAT front-end + serialization. That's a natural first-slice boundary for a focused PR.

There's no ## Acceptance Criteria block on the body the routine can verify before opening a PR, so it's deferred until one is pinned. Sketch matching the kill-criterion shape used on adjacent design issues (feel free to revise / re-scope):

## Acceptance Criteria — Part 2 (ordeal-certificate artifact type — unblocked now)
- [ ] New embedded schema (`schemas/ordeal-certificate.yaml`, or extend `common.yaml`) declares an `ordeal-certificate` artifact type carrying: `produced-by` (tool + version), `checked-by` (verifier + version), `attests` (claim: `variant-consistent` / `variant-inconsistent` / etc. + `standards`: DO-178C / ISO 26262 / EU-AI-Act-Art-12), `cnf-sha256` + `cnf-ref`, `proof-sha256` + `proof-ref` (LRAT for UNSAT / self-checked model for SAT per the honest-boundary noted on ordeal#67), and a structured `recheck` block (`command`, `expect-exit`).
- [ ] Typed `attests` link-field: `attests-transform` (link → the artifact whose transform this certificate attests — a `variant` config, a loom rule, a synth codegen, a sigil overflow, a spar layout, a gale bitvector). Allowed-target rule declared so `rivet validate`'s `link-target-type` check catches misuse.
- [ ] `rivet validate` treats a re-checked certificate as a **verification link**, not a claimed status: a `verifies` link from a verification artifact to an `ordeal-certificate` whose `recheck.command` was run and exited 0 (recorded via `verification-result` or an equivalent field) counts toward coverage; a certificate whose `recheck` was never run does not.
- [ ] Honest SAT boundary baked into the schema: for `attests.claim: variant-consistent` (SAT), the `proof-*` fields hold the self-checked model until ordeal FEAT-012 / v0.14.0 ships an independent re-checkable SAT witness. Documented in the schema + the docs topic.
- [ ] Golden-file test: an `ordeal-certificate` artifact serializes / parses round-trip byte-identical; a `link-target-type` fixture demonstrates the `attests-transform` allowed-targets enforcement; a coverage-rule fixture demonstrates the "re-checked → counts" vs. "never re-checked → does not count" split.
- [ ] `rivet docs` topic (e.g. `docs/artifact-types/ordeal-certificate.md`) explains the shape, the SAT boundary, and the `recheck` invocation contract, with the [ordeal#67 comment](https://github.com/pulseengine/ordeal/issues/67) linked as the upstream serialization spec.
- [ ] Commit trailers: `Implements: REQ-NNN` (new REQ for the certificate ingestion type — the cross-cutting evidence-spine piece) + `Refs: ordeal#67, #693`.
- [ ] **Explicitly out of scope (file separately as Part 1 — blocked on ordeal#67):** the `--certify` flag on `rivet release check --variant` / `rivet variant solve` that shells out to ordeal's propositional-SAT front-end and emits the certificate; the CI wiring; the `rules_ordeal` gate; the UNSAT-core surfacing as a `variant validate` diagnostic.

If you'd rather scope Phase 0 to just a design-decision artifact recording the certificate shape (so the schema doesn't land until ordeal#67's ordeal-cert/v1 is implemented, not just specified), that's also a clean shape — the AC becomes "a decision-type artifact under artifacts/decisions/ records the schema draft with ordeal-cert/v1 cited, plus a follow-up REQ filed for the implementation slice."

Process side-rail: https://pulseengine.eu/blog/ is up today (200 OK — different from the long-running 503 the recent triage threads have all flagged). The spec-driven-development-is-half-the-loop (2026-04-23) and mythos-slop-hunt (2026-04-25) posts are the closest analogues to workflow guidance; neither speaks to per-issue AC shape, so the kill-criterion posture used across #468 / #508 / #557 remains the working convention.

Not implemented this run.

---

Generated by Claude Code — issue-triage agent run 2026-07-15.

---

Generated by Claude Code

[avrabe]

The ordeal-cert/v1 serialization from the pinned contract is now implemented on the ordeal side (pulseengine/ordeal#107, ships in v0.17.0): Certificate::to_cert_v1(attests) emits the envelope, from_cert_v1 parses with both content hashes verified before returning (tampered proof and tampered problem each rejected before the checker runs), and UnsatBundle::recheck() is your verification-link operation. SAT shape included per the contract. Behind a cert-bundle cargo feature — enable it from rivet; the default build stays dependency-free. One v1 reader boundary: inline payloads only, *_ref refused as Unsupported — say the word when your MB-class certs need the ref path and it gets added to the same envelope.

[avrabe]

Triage from the scheduled routine.

Picking up your 2026-07-29 05:54 comment: Part 2 is now unblocked. pulseengine/ordeal#107 shipped the ordeal-cert/v1 envelope in ordeal v0.17.0 with both content hashes verified before from_cert_v1 returns (tampered proof and tampered problem both rejected before the checker runs), Certificate::to_cert_v1(attests) for emit, and UnsatBundle::recheck() as the verification-link operation — behind a cert-bundle cargo feature so the default build stays dependency-free. The one v1 reader boundary you called out (inline payloads only, *_ref rejected as Unsupported) is worth baking into the rivet-side AC as an explicit expected-error test, so the day rivet sees an MB-class cert the failure mode is legible rather than a mystery deserialize error.

Two other pieces of state the routine picked up this pass:

• Prior AC sketch stands. The Part-2 AC block sketched on comment 4975345044 still maps cleanly to what ordeal now ships — the fields, the attests-transform typed link, the "re-checked → counts as verification" split, the honest SAT-boundary note. The one addition worth folding in is the *_ref → Unsupported expected-error test above (v1 inline-only reader boundary).
• Body-level AC still missing. The routine can't autopick without an explicit ## Acceptance Criteria block on the body itself — the sketch in a triage comment doesn't gate. If you paste the Part-2 sketch (or a revised version) into the body, the next routine pass can open the branch.

Process side-rail: https://pulseengine.eu/blog/ is up today (200 OK). Nothing on the blog speaks to per-issue AC shape; the closest workflow-guidance posts (spec-driven-development-is-half-the-loop, mythos-slop-hunt) hold up the kill-criterion posture the routine already uses across adjacent triage threads.

Not implemented this run.

---

Generated by Claude Code — issue-triage agent run 2026-07-29.

---

Generated by Claude Code

[avrabe]

Part 2 (the ordeal-certificate ingestion type) implemented in #744.

The schema (schemas/ordeal-certificate.yaml) ships with the flat envelope fields, the source-pinned attests-transform link, and two validation rules that mirror the honest boundaries from your 2026-07-29 ordeal-cert/v1 contract note:

• V-ordeal-cert-v1-inline-only (error) — rejects cnf-ref / proof-ref indirection at ingest, mirroring Certificate::from_cert_v1's BundleError::Unsupported so v2 envelopes in a v1 world surface as a legible schema violation rather than a mystery deserialize error.
• V-ordeal-cert-needs-recheck (warning) — a certificate whose recheck-exit-code is missing or != "0" is unverified evidence, not a verification link. Implements the "claimed vs re-checked → counts toward coverage" split.

REQ-255 flipped proposed → implemented, release v0.31.0. Part 1 (the --certify hook on rivet release check --variant) stays out of scope for this PR and will be filed as a separate REQ when picked up.

PR body walks each AC bullet from the issue → how the PR satisfies it.

---

Generated by Claude Code