vyre_conform/pipeline/certify/
implementation.rs

1//! Conformance certificate generation.
2//!
3//! A certificate is an archival proof document for one backend run against a
4//! concrete operation spec set. It records parity results, law verification,
5//! coverage counts, and the highest conformance level proven by this run.
6
7use crate::pipeline::{certificate_track_for_op, CertificateTrack};
8use crate::spec::law::LawViolation;
9use crate::spec::types::{OpSpec, ParityFailure, Strictness};
10use serde::Serialize;
11#[cfg(test)]
12use std::cell::RefCell;
13use std::collections::BTreeMap;
14use std::sync::atomic::{AtomicU64, Ordering};
15use std::time::{SystemTime, UNIX_EPOCH};
16
17use super::engine::run_engine_harnesses;
18use super::hash::compute_registry_hash;
19use super::ops::certify_op;
20use super::track::{build_track, coverage_for, optional_track, unsupported_ops};
21
22pub(crate) const MAX_RECORDED_PARITY_FAILURES: usize = 16;
23static CERTIFICATE_SEQUENCE: AtomicU64 = AtomicU64::new(0);
24#[cfg(test)]
25thread_local! {
26    static TEST_MUTATION_CATALOG: RefCell<Option<Vec<crate::adversarial::mutations::catalog::Mutation>>> =
27        const { RefCell::new(None) };
28}
29
30/// A single conformance failure emitted while certifying a backend.
31#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
32pub struct Violation {
33    /// Operation identifier being certified when the violation occurred.
34    pub(crate) op_id: String,
35    /// Algebraic law or conformance rule that was violated.
36    pub(crate) law: String,
37    /// Backend identifier that produced the violating output.
38    pub(crate) backend: String,
39    /// CPU reference bytes for the failing case.
40    pub(crate) reference_output: Vec<u8>,
41    /// Backend output bytes for the failing case.
42    pub(crate) backend_output: Vec<u8>,
43    /// Actionable remediation message. Must begin with `Fix: `.
44    pub(crate) message: String,
45}
46
47/// Verification strength selected for a certificate run.
48#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Default)]
49pub enum CertificateStrength {
50    /// Fast feedback mode, ten thousand witnesses per law.
51    FastCheck,
52    /// Standard conformance run with at least one million witnesses per law.
53    #[default]
54    Standard,
55    /// Nightly and release-gate mode with at least one hundred million witnesses per law.
56    Legendary,
57}
58
59impl CertificateStrength {
60    /// Return the required random u32 witness count for each declared law.
61    #[must_use]
62    pub const fn witness_count(self) -> u64 {
63        match self {
64            Self::FastCheck => 10_000,
65            Self::Standard => 1_000_000,
66            Self::Legendary => 100_000_000,
67        }
68    }
69
70    /// Whether this strength may publish an archival conformance claim.
71    #[must_use]
72    pub const fn can_claim_conformance(self) -> bool {
73        !matches!(self, Self::FastCheck)
74    }
75}
76
77/// Structured proof document for a backend conformance run.
78///
79/// ```compile_fail
80/// use vyre_conform::Certificate;
81/// fn seal(cert: &Certificate) {
82///     let _ = cert.backend_name;
83/// }
84/// ```
85#[derive(Debug, Clone, Serialize)]
86pub struct Certificate {
87    /// Human-readable backend name.
88    pub(crate) backend_name: String,
89    /// Human-readable backend version.
90    pub(crate) backend_version: String,
91    /// Maximum operation spec version covered by this certificate.
92    pub(crate) spec_version: u32,
93    /// Highest conformance levels proven by each certificate track.
94    pub(crate) level: CertificateLevels,
95    /// UTC issuance timestamp, encoded without external clock-format dependencies.
96    pub(crate) timestamp: String,
97    /// Process-local monotonic certificate sequence for concurrent certification runs.
98    pub(crate) monotonic_sequence: u64,
99    /// Deterministic certificate digest.
100    pub(crate) certificate_hash: [u8; 32],
101    /// Verification strength chosen by the caller for this certificate.
102    pub(crate) strength: CertificateStrength,
103    /// Random u32 witnesses evaluated per law at the selected strength.
104    pub(crate) witness_count: u64,
105    /// Per-operation random u32 witnesses evaluated per declared law.
106    pub(crate) witness_count_by_op: BTreeMap<String, u64>,
107    /// Human-readable proof status. FastCheck is explicitly exploratory.
108    pub(crate) proof_status: String,
109    /// Bit-exact integer and byte-oriented conformance evidence.
110    pub(crate) integer_track: TrackReport,
111    /// Bit-exact floating-point conformance evidence.
112    pub(crate) float_track: Option<TrackReport>,
113    /// ULP-tolerance approximate conformance evidence.
114    pub(crate) approximate_track: Option<TrackReport>,
115    /// Per-operation parity and algebra results.
116    pub(crate) ops: Vec<OpResult>,
117    /// Operation IDs explicitly unsupported by this backend.
118    pub(crate) unsupported_ops: Vec<String>,
119    /// Per-engine invariant results.
120    pub(crate) engines: Vec<EngineResult>,
121    /// Deterministic hash of the spec registry used for this run.
122    pub(crate) registry_hash: [u8; 32],
123    /// Count-based coverage metrics for the run.
124    pub(crate) coverage: CoverageMetrics,
125}
126
127/// Certificate evidence for one conformance track.
128#[derive(Debug, Clone, Serialize)]
129pub struct TrackReport {
130    /// Highest track-specific conformance level proven.
131    pub(crate) level: Option<ConformanceLevel>,
132    /// Operations routed to this track.
133    pub(crate) ops: Vec<OpResult>,
134    /// Operation IDs explicitly unsupported by this backend on this track.
135    pub(crate) unsupported_ops: Vec<String>,
136    /// Count-based coverage metrics for this track.
137    pub(crate) coverage: CoverageMetrics,
138}
139
140/// Per-operation backend conformance outcome.
141#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
142pub enum OpOutcome {
143    /// Backend matched the reference and verified declared laws.
144    Passed,
145    /// Backend produced a mismatch or law violation.
146    Failed,
147    /// Backend or operation carries an explicit pending strict-float gate.
148    Pending,
149    /// Backend explicitly does not support this Category C operation.
150    Unsupported,
151}
152
153/// Per-operation certificate evidence.
154#[derive(Debug, Clone, Serialize)]
155pub struct OpResult {
156    /// Operation ID.
157    pub(crate) id: String,
158    /// Archetype from the locked vocabulary.
159    pub(crate) archetype: String,
160    /// Three-state result for this operation on this backend.
161    pub(crate) outcome: OpOutcome,
162    /// Whether backend output matched the CPU reference for every generated parity case.
163    pub(crate) parity_passed: bool,
164    /// Declared laws that passed exhaustive and witnessed verification.
165    pub(crate) laws_verified: Vec<String>,
166    /// Concrete law violations found during verification.
167    pub(crate) laws_failed: Vec<LawViolation>,
168    /// First parity failures retained for forensic replay.
169    pub(crate) parity_failures: Vec<ParityFailure>,
170    /// Total parity and law cases evaluated for this operation.
171    pub(crate) cases_tested: u64,
172    /// Random u32 witnesses evaluated per declared law for this operation.
173    pub(crate) witness_count: u64,
174}
175
176/// Per-engine invariant evidence.
177#[derive(Debug, Clone, Serialize)]
178pub struct EngineResult {
179    /// Engine ID.
180    pub(crate) id: String,
181    /// Aggregate invariant status for this engine harness.
182    pub(crate) status: EngineStatus,
183    /// Invariants verified for this engine.
184    pub(crate) invariants_verified: Vec<String>,
185    /// Invariant failure diagnostics.
186    pub(crate) invariants_failed: Vec<String>,
187    /// Total invariant cases evaluated for this engine.
188    pub(crate) cases_tested: u64,
189}
190
191/// Per-engine invariant status.
192#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
193pub enum EngineStatus {
194    /// Every invariant checked by this engine passed.
195    Pass,
196    /// At least one invariant checked by this engine failed.
197    Fail,
198}
199
200/// Count-based coverage metrics for a certificate run.
201#[derive(Debug, Clone, Default, Serialize)]
202pub struct CoverageMetrics {
203    /// Number of operation specs included in the run.
204    pub ops_total: u64,
205    /// Number of operations with full parity pass.
206    pub ops_parity_passed: u64,
207    /// Number of operations explicitly unsupported by this backend.
208    pub ops_unsupported: u64,
209    /// Number of operations with all declared laws verified.
210    pub ops_laws_passed: u64,
211    /// Number of declared law checks.
212    pub laws_total: u64,
213    /// Number of declared law checks that passed.
214    pub laws_passed: u64,
215    /// Number of equivalence classes declared by the specs.
216    pub equivalence_classes_total: u64,
217    /// Number of boundary values declared by the specs.
218    pub boundary_values_total: u64,
219    /// Total parity and law cases evaluated.
220    pub cases_tested: u64,
221}
222
223/// Track-specific conformance strength level.
224#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
225pub enum ConformanceLevel {
226    /// L1 parity evidence.
227    L1,
228    /// L2 parity plus algebraic evidence.
229    L2,
230    /// L1f strict floating-point parity evidence.
231    L1f,
232    /// L2f strict floating-point algebraic evidence.
233    L2f,
234    /// L1a approximate parity evidence within declared tolerance.
235    L1a,
236}
237
238/// Top-level conformance claim split by independent tracks.
239#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
240pub struct CertificateLevels {
241    /// Integer track level.
242    pub integer: Option<ConformanceLevel>,
243    /// Strict floating-point track level, when float ops were certified.
244    pub float: Option<ConformanceLevel>,
245    /// Approximate track level, when approximate ops were certified.
246    pub approximate: Option<ConformanceLevel>,
247}
248
249pub(crate) struct ParitySummary {
250    pub(super) cases_tested: u64,
251    pub(super) failures: Vec<ParityFailure>,
252    pub(super) unsupported: bool,
253}
254
255/// Run parity and algebra checks and return a conformance certificate.
256#[inline]
257pub fn certify(
258    backend: &dyn vyre::VyreBackend,
259    specs: &[OpSpec],
260    strength: CertificateStrength,
261) -> Result<Certificate, String> {
262    // Law-0 / L.3.1: GPU-mandatory gate fires before any other check.
263    // After the L.3.2 refinements (cfg(all(test, feature="...")) and
264    // tests/-path exemptions + unconditional wgpu re-export), the
265    // enforcer runs inside certify() against the production surface
266    // only. Any remaining violation (cfg(feature="gpu") on a
267    // non-test item, swallowed GPU probe error, cpu_fn call outside
268    // conform/tests) triggers an unwaivable Cat-C error.
269    if specs.is_empty() {
270        return Err("Fix: certify requires at least one OpSpec, got empty list.".to_string());
271    }
272    run_layer4_mutation_gate()?;
273
274    reject_duplicate_or_mixed_specs(specs)?;
275
276    let mut routed_ops = Vec::with_capacity(specs.len());
277    for spec in specs {
278        routed_ops.push((
279            certificate_track_for_op(spec),
280            spec,
281            certify_op(backend, spec, strength),
282        ));
283    }
284
285    let mut integer_track = build_track(
286        &routed_ops,
287        CertificateTrack::Integer,
288        ConformanceLevel::L1,
289        ConformanceLevel::L2,
290    );
291    let mut float_track = optional_track(
292        &routed_ops,
293        CertificateTrack::Float,
294        ConformanceLevel::L1f,
295        ConformanceLevel::L2f,
296    );
297    let mut approximate_track = optional_track(
298        &routed_ops,
299        CertificateTrack::Approximate,
300        ConformanceLevel::L1a,
301        ConformanceLevel::L1a,
302    );
303    if !strength.can_claim_conformance() {
304        integer_track.level = None;
305        if let Some(track) = &mut float_track {
306            track.level = None;
307        }
308        if let Some(track) = &mut approximate_track {
309            track.level = None;
310        }
311    }
312
313    let ops: Vec<_> = routed_ops
314        .iter()
315        .map(|(_, _, op_result)| op_result.clone())
316        .collect();
317    let unsupported_ops = unsupported_ops(&ops);
318    let coverage = coverage_for(specs, &ops);
319    let engines = run_engine_harnesses(backend, specs);
320    let all_engines_passed = engines
321        .iter()
322        .all(|engine| engine.status == EngineStatus::Pass);
323
324    // Audit C1 remediation (L.1.2/L.1.9): run the L5 adversarial defender
325    // gauntlet for Standard and Legendary strengths. Skipping this for
326    // FastCheck is the only sanctioned fast path. Any defendant that
327    // escapes detection is a hard pre-certificate error, not just a
328    // claim downgrade.
329    //
330    // Prior behavior: certify() ran parity + law checks only; mutated
331    // backends passed. See audits/conform-gate-kimi-AUDIT.md finding 5.1.
332    let escaped_defendant_ids: Vec<String> = if matches!(
333        strength,
334        CertificateStrength::Standard | CertificateStrength::Legendary
335    ) {
336        let report = crate::adversarial::run_gauntlet(&crate::adversarial::full_catalog(), specs);
337        report
338            .escaped()
339            .into_iter()
340            .map(|finding| finding.defendant_id.clone())
341            .collect()
342    } else {
343        Vec::new()
344    };
345    if !escaped_defendant_ids.is_empty() {
346        return Err(format!(
347            "Cat-C: layer5_adversarial gate failed; escaped defendant(s): {}",
348            escaped_defendant_ids.join(", ")
349        ));
350    }
351
352    let level = if strength.can_claim_conformance() && all_engines_passed {
353        CertificateLevels {
354            integer: integer_track.level,
355            float: float_track.as_ref().and_then(|track| track.level),
356            approximate: approximate_track.as_ref().and_then(|track| track.level),
357        }
358    } else {
359        CertificateLevels {
360            integer: None,
361            float: None,
362            approximate: None,
363        }
364    };
365    let registry_hash = compute_registry_hash(specs);
366    let timestamp = certificate_timestamp()?;
367    let monotonic_sequence = next_certificate_sequence();
368    let witness_count = strength.witness_count();
369    let witness_count_by_op = ops
370        .iter()
371        .map(|op| (op.id.clone(), op.witness_count))
372        .collect();
373    let proof_status = proof_status(strength).to_string();
374
375    Ok(Certificate::new(
376        backend.id().to_string(),
377        "unspecified".to_string(),
378        specs
379            .iter()
380            .map(|spec| spec.version)
381            .max()
382            .unwrap_or_default(),
383        level,
384        timestamp,
385        monotonic_sequence,
386        strength,
387        witness_count,
388        witness_count_by_op,
389        proof_status,
390        integer_track,
391        float_track,
392        approximate_track,
393        ops,
394        unsupported_ops,
395        engines,
396        registry_hash,
397        coverage,
398    ))
399}
400
401fn certificate_timestamp() -> Result<String, String> {
402    let elapsed = SystemTime::now().duration_since(UNIX_EPOCH).map_err(|err| {
403        format!(
404            "Fix: system clock is before the Unix epoch, cannot issue a conformance certificate: {err}"
405        )
406    })?;
407    Ok(format!("unix:{}", elapsed.as_secs()))
408}
409
410fn next_certificate_sequence() -> u64 {
411    CERTIFICATE_SEQUENCE.fetch_add(1, Ordering::SeqCst)
412}
413
414fn run_layer4_mutation_gate() -> Result<(), String> {
415    let catalog = mutation_catalog_for_certify();
416    crate::enforce::enforcers::layer4_mutation_gate::validate_catalog(&catalog).map_err(
417        |messages| {
418            format!(
419                "Cat-C: layer4_mutation_gate failed and certificate emission is blocked.\n{}",
420                messages
421                    .into_iter()
422                    .map(|message| format!("Fix: {message}"))
423                    .collect::<Vec<_>>()
424                    .join("\n")
425            )
426        },
427    )
428}
429
430fn mutation_catalog_for_certify() -> Vec<crate::adversarial::mutations::catalog::Mutation> {
431    #[cfg(test)]
432    {
433        if let Some(catalog) = TEST_MUTATION_CATALOG.with(|catalog| catalog.borrow().clone()) {
434            return catalog;
435        }
436    }
437    crate::adversarial::mutations::catalog::MUTATION_CATALOG.to_vec()
438}
439
440#[cfg(test)]
441pub(crate) fn with_test_mutation_catalog<T>(
442    catalog: Vec<crate::adversarial::mutations::catalog::Mutation>,
443    f: impl FnOnce() -> T,
444) -> T {
445    TEST_MUTATION_CATALOG.with(|slot| *slot.borrow_mut() = Some(catalog));
446    let output = f();
447    TEST_MUTATION_CATALOG.with(|slot| *slot.borrow_mut() = None);
448    output
449}
450
451fn reject_duplicate_or_mixed_specs(specs: &[OpSpec]) -> Result<(), String> {
452    let mut seen = BTreeMap::new();
453    for spec in specs {
454        let is_approximate = matches!(spec.strictness, Strictness::Approximate { .. });
455        if let Some(previous_is_approximate) = seen.insert(spec.id, is_approximate) {
456            if previous_is_approximate != is_approximate {
457                return Err(format!(
458                    "Fix: op {} declared Strict AND Approximate. Split into two spec entries with different ids.",
459                    spec.id
460                ));
461            }
462            return Err(format!(
463                "Fix: duplicate op id {} in certificate input. Register every operation exactly once.",
464                spec.id
465            ));
466        }
467    }
468    Ok(())
469}
470
471fn proof_status(strength: CertificateStrength) -> &'static str {
472    match strength {
473        CertificateStrength::FastCheck => "EXPLORATORY -- NOT A PROOF",
474        CertificateStrength::Standard | CertificateStrength::Legendary => "CONFORMANCE PROOF",
475    }
476}
vyre_conform/pipeline/certify/implementation.rs

vyre_conform/pipeline/certify/
implementation.rs
