vela_protocol/
proof_verification.rs

1//! v0.151: signed verification records for Carina Proof artifacts.
2//!
3//! Substrate-honest split: the substrate stores attested
4//! verification records; the verifier (Lean kernel, Coq, etc.)
5//! runs outside the substrate. Consumers verify the attestation's
6//! signature against the verifier_actor's pubkey and trust the
7//! verifier's judgment for the named (tool, tool_version,
8//! lake_manifest_hash) tuple.
9//!
10//! See `docs/PROOF_VERIFICATION.md` (shipped at v0.153) for the
11//! end-to-end pipeline and `.github/workflows/verify-carina-proofs.yml`
12//! for the canonical GitHub Action implementation.
13
14use serde::{Deserialize, Serialize};
15use sha2::{Digest, Sha256};
16
17pub const VERIFICATION_SCHEMA: &str = "vela.proof_verification.v0.1";
18
19#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq)]
20pub struct ProofVerification {
21    pub schema: String,
22    pub verification_id: String,
23    pub proof_id: String,
24    pub tool: String,
25    pub tool_version: String,
26    pub script_locator: String,
27    #[serde(default, skip_serializing_if = "Option::is_none")]
28    pub lake_manifest_hash: Option<String>,
29    pub verifier_output_hash: String,
30    pub status: String,
31    pub verified_at: String,
32    pub verifier_actor: String,
33    pub verifier_pubkey: String,
34    pub signature: String,
35}
36
37#[derive(Debug, Clone)]
38pub struct VerificationDraft {
39    pub proof_id: String,
40    pub tool: String,
41    pub tool_version: String,
42    pub script_locator: String,
43    pub lake_manifest_hash: Option<String>,
44    pub verifier_output_hash: String,
45    pub status: String,
46    pub verified_at: String,
47    pub verifier_actor: String,
48}
49
50impl ProofVerification {
51    /// Build + sign a verification record. The signature covers
52    /// the canonical preimage with `signature` and `verification_id`
53    /// zeroed. The id is then derived from the signed body, so a
54    /// tampered signature surfaces as an id mismatch on `verify`.
55    pub fn build(
56        draft: VerificationDraft,
57        signing_key: &ed25519_dalek::SigningKey,
58    ) -> Result<Self, String> {
59        if !draft.proof_id.starts_with("vpf_") {
60            return Err(format!(
61                "proof_id must start with `vpf_`, got `{}`",
62                draft.proof_id
63            ));
64        }
65        if !matches!(
66            draft.tool.as_str(),
67            "lean4" | "coq" | "isabelle" | "agda" | "metamath" | "rocq" | "other"
68        ) {
69            return Err(format!(
70                "tool must be one of lean4|coq|isabelle|agda|metamath|rocq|other; got `{}`",
71                draft.tool
72            ));
73        }
74        if !matches!(
75            draft.status.as_str(),
76            "verified" | "failed" | "toolchain_mismatch"
77        ) {
78            return Err(format!(
79                "status must be one of verified|failed|toolchain_mismatch; got `{}`",
80                draft.status
81            ));
82        }
83        let mut record = ProofVerification {
84            schema: VERIFICATION_SCHEMA.to_string(),
85            verification_id: String::new(),
86            proof_id: draft.proof_id,
87            tool: draft.tool,
88            tool_version: draft.tool_version,
89            script_locator: draft.script_locator,
90            lake_manifest_hash: draft.lake_manifest_hash,
91            verifier_output_hash: draft.verifier_output_hash,
92            status: draft.status,
93            verified_at: draft.verified_at,
94            verifier_actor: draft.verifier_actor,
95            verifier_pubkey: hex::encode(signing_key.verifying_key().to_bytes()),
96            signature: String::new(),
97        };
98        let preimage = record.preimage_bytes()?;
99        use ed25519_dalek::Signer;
100        let sig = signing_key.sign(&preimage);
101        record.signature = hex::encode(sig.to_bytes());
102        record.verification_id = record.derive_id()?;
103        Ok(record)
104    }
105
106    pub fn preimage_bytes(&self) -> Result<Vec<u8>, String> {
107        let mut preimage = self.clone();
108        preimage.signature = String::new();
109        preimage.verification_id = String::new();
110        crate::canonical::to_canonical_bytes(&preimage)
111            .map_err(|e| format!("canonicalize verification preimage: {e}"))
112    }
113
114    pub fn derive_id(&self) -> Result<String, String> {
115        let mut preimage = self.clone();
116        preimage.verification_id = String::new();
117        let bytes = crate::canonical::to_canonical_bytes(&preimage)
118            .map_err(|e| format!("canonicalize verification id preimage: {e}"))?;
119        let digest = Sha256::digest(&bytes);
120        Ok(format!("vpv_{}", &hex::encode(digest)[..16]))
121    }
122
123    /// Verify the attestation: re-derive the id, verify the
124    /// Ed25519 signature against `verifier_pubkey`. Optional
125    /// caller check: the caller may additionally assert that the
126    /// `script_locator` matches a known proof artifact's locator
127    /// (the substrate does not have a global proof index at
128    /// v0.151; consumers cross-link manually).
129    pub fn verify(&self) -> Result<(), String> {
130        if self.schema != VERIFICATION_SCHEMA {
131            return Err(format!(
132                "verification.schema must be `{VERIFICATION_SCHEMA}`, got `{}`",
133                self.schema
134            ));
135        }
136        let derived = self.derive_id()?;
137        if derived != self.verification_id {
138            return Err(format!(
139                "verification_id mismatch: stored `{}`, derived `{}`",
140                self.verification_id, derived
141            ));
142        }
143        let pk_bytes = hex::decode(&self.verifier_pubkey)
144            .map_err(|e| format!("verifier_pubkey not hex: {e}"))?;
145        if pk_bytes.len() != 32 {
146            return Err(format!(
147                "verifier_pubkey must be 32 bytes (got {})",
148                pk_bytes.len()
149            ));
150        }
151        let pk = ed25519_dalek::VerifyingKey::from_bytes(
152            pk_bytes
153                .as_slice()
154                .try_into()
155                .map_err(|e| format!("verifier_pubkey: {e}"))?,
156        )
157        .map_err(|e| format!("verifier_pubkey malformed: {e}"))?;
158        let sig_bytes =
159            hex::decode(&self.signature).map_err(|e| format!("signature not hex: {e}"))?;
160        if sig_bytes.len() != 64 {
161            return Err(format!(
162                "signature must be 64 bytes (got {})",
163                sig_bytes.len()
164            ));
165        }
166        let sig = ed25519_dalek::Signature::from_bytes(
167            sig_bytes
168                .as_slice()
169                .try_into()
170                .map_err(|e| format!("signature: {e}"))?,
171        );
172        let preimage = self.preimage_bytes()?;
173        use ed25519_dalek::Verifier;
174        pk.verify(&preimage, &sig)
175            .map_err(|e| format!("verification signature does not verify: {e}"))?;
176        Ok(())
177    }
178}
179
180#[cfg(test)]
181mod tests {
182    use super::*;
183
184    fn make_key() -> ed25519_dalek::SigningKey {
185        use rand::rngs::OsRng;
186        ed25519_dalek::SigningKey::generate(&mut OsRng)
187    }
188
189    fn good_draft() -> VerificationDraft {
190        VerificationDraft {
191            proof_id: "vpf_egz_n2".to_string(),
192            tool: "lean4".to_string(),
193            tool_version: "4.29.1".to_string(),
194            script_locator:
195                "sha256:58dec20d4f8c474d222009c9d3b7cae2ef010bfac48fd5c2ad7c9c8d894428ec"
196                    .to_string(),
197            lake_manifest_hash: Some("sha256:0".repeat(64)),
198            verifier_output_hash: format!("sha256:{}", "0".repeat(64)),
199            status: "verified".to_string(),
200            verified_at: "2026-05-11T00:00:00+00:00".to_string(),
201            verifier_actor: "github-action:vela/.github/workflows/verify-carina-proofs.yml"
202                .to_string(),
203        }
204    }
205
206    #[test]
207    fn build_roundtrip() {
208        let sk = make_key();
209        let record = ProofVerification::build(good_draft(), &sk).unwrap();
210        assert!(record.verification_id.starts_with("vpv_"));
211        record.verify().unwrap();
212    }
213
214    #[test]
215    fn id_changes_when_status_changes() {
216        let sk = make_key();
217        let a = ProofVerification::build(good_draft(), &sk).unwrap();
218        let mut draft = good_draft();
219        draft.status = "failed".to_string();
220        let b = ProofVerification::build(draft, &sk).unwrap();
221        assert_ne!(a.verification_id, b.verification_id);
222    }
223
224    #[test]
225    fn tampered_signature_rejected() {
226        let sk = make_key();
227        let mut record = ProofVerification::build(good_draft(), &sk).unwrap();
228        record.signature = "0".repeat(128);
229        let err = record.verify().unwrap_err();
230        assert!(
231            err.contains("mismatch") || err.contains("does not verify"),
232            "got: {err}"
233        );
234    }
235
236    #[test]
237    fn invalid_status_rejected() {
238        let sk = make_key();
239        let mut draft = good_draft();
240        draft.status = "bogus".to_string();
241        let err = ProofVerification::build(draft, &sk).unwrap_err();
242        assert!(err.contains("status must be"), "got: {err}");
243    }
244}
vela_protocol/proof_verification.rs

vela_protocol/
proof_verification.rs
