karpal_verify/
trust.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4use core::marker::PhantomData;
5
6#[cfg(not(feature = "std"))]
7use alloc::{
8    format,
9    string::{String, ToString},
10};
11#[cfg(feature = "std")]
12use std::string::String;
13
14use crate::Obligation;
15
16use karpal_proof::Proven;
17
18/// Marker trait for external verification backends.
19pub trait VerificationBackend {
20    const NAME: &'static str;
21}
22
23/// SMT-LIB2 / solver-backed verification.
24pub struct SmtCertificate;
25impl VerificationBackend for SmtCertificate {
26    const NAME: &'static str = "smtlib2";
27}
28
29/// Lean 4 proof assistant verification.
30pub struct LeanCertificate;
31impl VerificationBackend for LeanCertificate {
32    const NAME: &'static str = "lean4";
33}
34
35/// Kani bounded model checking verification.
36pub struct KaniCertificate;
37impl VerificationBackend for KaniCertificate {
38    const NAME: &'static str = "kani";
39}
40
41/// `karpal-proof` / proptest-derived verification evidence.
42pub struct ProofTestCertificate;
43impl VerificationBackend for ProofTestCertificate {
44    const NAME: &'static str = "karpal-proof";
45}
46
47impl LeanCertificate {
48    pub fn witness_ref(module_name: &str, theorem_name: &str) -> String {
49        format!("{module_name}.{theorem_name}")
50    }
51
52    pub fn module_ref(module_name: &str) -> String {
53        module_name.to_string()
54    }
55}
56
57/// Metadata describing imported external evidence.
58#[derive(Debug, Clone, PartialEq, Eq)]
59pub struct Certificate {
60    pub backend: &'static str,
61    pub backend_version: Option<String>,
62    pub obligation: String,
63    pub obligation_digest: Option<String>,
64    pub witness_ref: String,
65    pub artifact_path: Option<String>,
66    pub notes: Option<String>,
67}
68
69impl Certificate {
70    pub fn new(
71        backend: &'static str,
72        obligation: impl Into<String>,
73        witness_ref: impl Into<String>,
74    ) -> Self {
75        Self {
76            backend,
77            backend_version: None,
78            obligation: obligation.into(),
79            obligation_digest: None,
80            witness_ref: witness_ref.into(),
81            artifact_path: None,
82            notes: None,
83        }
84    }
85
86    pub fn from_obligation<B: VerificationBackend>(
87        obligation: &Obligation,
88        witness_ref: impl Into<String>,
89    ) -> Self {
90        Self::new(B::NAME, obligation.summary(), witness_ref)
91            .with_obligation_digest(obligation_digest(obligation))
92    }
93
94    pub fn with_backend_version(mut self, version: impl Into<String>) -> Self {
95        self.backend_version = Some(version.into());
96        self
97    }
98
99    pub fn with_obligation_digest(mut self, digest: impl Into<String>) -> Self {
100        self.obligation_digest = Some(digest.into());
101        self
102    }
103
104    pub fn with_artifact_path(mut self, path: impl Into<String>) -> Self {
105        self.artifact_path = Some(path.into());
106        self
107    }
108
109    pub fn with_notes(mut self, notes: impl Into<String>) -> Self {
110        self.notes = Some(notes.into());
111        self
112    }
113}
114
115fn obligation_digest(obligation: &Obligation) -> String {
116    let mut hash: u64 = 0xcbf29ce484222325;
117    for byte in obligation.summary().bytes() {
118        hash ^= u64::from(byte);
119        hash = hash.wrapping_mul(0x100000001b3);
120    }
121    format!("fnv1a64:{hash:016x}")
122}
123
124/// Explicit trust boundary for externally-certified values.
125///
126/// This type does not silently become `Proven<P, T>`. Converting from
127/// external evidence into a Karpal proof witness is `unsafe`, making the
128/// trust boundary visible in code review.
129pub struct Certified<B, P, T> {
130    value: T,
131    certificate: Certificate,
132    _phantom: PhantomData<(B, P)>,
133}
134
135/// Alias emphasizing that the certificate crosses an external trust boundary.
136pub type ExternalTrust<B, P, T> = Certified<B, P, T>;
137
138impl<B, P, T> Certified<B, P, T> {
139    /// Import an externally checked value.
140    ///
141    /// # Safety
142    ///
143    /// The caller must ensure the certificate genuinely establishes property
144    /// `P` for `value`, according to backend `B`.
145    pub unsafe fn assume(value: T, certificate: Certificate) -> Self {
146        Self {
147            value,
148            certificate,
149            _phantom: PhantomData,
150        }
151    }
152
153    pub fn certificate(&self) -> &Certificate {
154        &self.certificate
155    }
156
157    pub fn value(&self) -> &T {
158        &self.value
159    }
160
161    pub fn into_inner(self) -> T {
162        self.value
163    }
164
165    /// Convert external evidence into `Proven<P, T>`.
166    ///
167    /// # Safety
168    ///
169    /// This is the explicit trust boundary: the caller accepts the imported
170    /// certificate as sound.
171    pub unsafe fn into_proven(self) -> Proven<P, T> {
172        unsafe { Proven::axiom(self.value) }
173    }
174}
175
176impl<B: VerificationBackend, P, T: core::fmt::Debug> core::fmt::Debug for Certified<B, P, T> {
177    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
178        f.debug_struct("Certified")
179            .field("backend", &B::NAME)
180            .field("value", &self.value)
181            .field("certificate", &self.certificate)
182            .finish()
183    }
184}
185
186#[cfg(test)]
187mod tests {
188    use super::*;
189    use crate::{Origin, Sort};
190    use karpal_proof::{IsAssociative, Proven};
191
192    #[test]
193    fn certificate_stores_metadata() {
194        let cert = Certificate::new(
195            "lean4",
196            "sum_assoc",
197            LeanCertificate::witness_ref("Sum", "assoc"),
198        )
199        .with_backend_version("4.15.0")
200        .with_artifact_path(".artifacts/SumAssoc.lean")
201        .with_notes("ported from generated module");
202        assert_eq!(cert.backend, "lean4");
203        assert_eq!(cert.backend_version.as_deref(), Some("4.15.0"));
204        assert_eq!(
205            cert.artifact_path.as_deref(),
206            Some(".artifacts/SumAssoc.lean")
207        );
208        assert!(cert.notes.as_deref().unwrap().contains("ported"));
209    }
210
211    #[test]
212    fn certified_wraps_value() {
213        let cert = Certificate::new("smtlib2", "sum_assoc", "z3:model:1");
214        let verified = unsafe { Certified::<SmtCertificate, IsAssociative, i32>::assume(7, cert) };
215        assert_eq!(*verified.value(), 7);
216        assert_eq!(verified.certificate().backend, "smtlib2");
217    }
218
219    #[test]
220    fn trust_boundary_can_be_crossed_explicitly() {
221        let cert = Certificate::new(
222            "lean4",
223            "sum_assoc",
224            LeanCertificate::witness_ref("Sum", "assoc"),
225        );
226        let verified =
227            unsafe { Certified::<LeanCertificate, IsAssociative, i32>::assume(11, cert) };
228        let proven: Proven<IsAssociative, i32> = unsafe { verified.into_proven() };
229        assert_eq!(*proven.value(), 11);
230    }
231
232    #[test]
233    fn certificate_can_be_derived_from_obligation() {
234        let obligation = Obligation::associativity(
235            "sum_assoc",
236            Origin::new("karpal-core", "Semigroup for i32"),
237            Sort::Int,
238            "combine",
239        );
240        let cert = Certificate::from_obligation::<SmtCertificate>(&obligation, "z3:proof:assoc")
241            .with_backend_version("4.13.0");
242        assert_eq!(cert.backend, "smtlib2");
243        assert!(cert.obligation.contains("associativity"));
244        assert!(
245            cert.obligation_digest
246                .as_deref()
247                .unwrap()
248                .starts_with("fnv1a64:")
249        );
250    }
251
252    #[test]
253    fn lean_module_ref_is_stable() {
254        assert_eq!(LeanCertificate::module_ref("KarpalVerify"), "KarpalVerify");
255    }
256
257    #[test]
258    fn kani_certificate_has_stable_backend_name() {
259        assert_eq!(KaniCertificate::NAME, "kani");
260    }
261
262    #[test]
263    fn proof_test_certificate_has_stable_backend_name() {
264        assert_eq!(ProofTestCertificate::NAME, "karpal-proof");
265    }
266}
karpal_verify/trust.rs

karpal_verify/
trust.rs
