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.13.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).