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.

[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