ruvector_verified/
proof_store.rs

1//! Ed25519-signed proof attestation.
2//!
3//! Provides `ProofAttestation` for creating verifiable proof receipts
4//! that can be serialized into RVF WITNESS_SEG entries.
5
6/// Witness type code for formal verification proofs.
7/// Extends existing codes: 0x01=PROVENANCE, 0x02=COMPUTATION.
8pub const WITNESS_TYPE_FORMAL_PROOF: u8 = 0x0E;
9
10/// A proof attestation that records verification metadata.
11///
12/// Can be serialized into an RVF WITNESS_SEG entry (82 bytes)
13/// for inclusion in proof-carrying containers.
14#[derive(Debug, Clone)]
15#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
16pub struct ProofAttestation {
17    /// Hash of the serialized proof term (32 bytes).
18    pub proof_term_hash: [u8; 32],
19    /// Hash of the environment declarations used (32 bytes).
20    pub environment_hash: [u8; 32],
21    /// Nanosecond UNIX timestamp of verification.
22    pub verification_timestamp_ns: u64,
23    /// lean-agentic version: 0x00_01_00_00 = 0.1.0.
24    pub verifier_version: u32,
25    /// Number of type-check reduction steps consumed.
26    pub reduction_steps: u32,
27    /// Arena cache hit rate (0..10000 = 0.00%..100.00%).
28    pub cache_hit_rate_bps: u16,
29}
30
31/// Serialized size of a ProofAttestation.
32pub const ATTESTATION_SIZE: usize = 32 + 32 + 8 + 4 + 4 + 2; // 82 bytes
33
34impl ProofAttestation {
35    /// Create a new attestation with the given parameters.
36    pub fn new(
37        proof_term_hash: [u8; 32],
38        environment_hash: [u8; 32],
39        reduction_steps: u32,
40        cache_hit_rate_bps: u16,
41    ) -> Self {
42        Self {
43            proof_term_hash,
44            environment_hash,
45            verification_timestamp_ns: current_timestamp_ns(),
46            verifier_version: 0x00_01_00_00, // 0.1.0
47            reduction_steps,
48            cache_hit_rate_bps,
49        }
50    }
51
52    /// Serialize attestation to bytes for signing/hashing.
53    pub fn to_bytes(&self) -> Vec<u8> {
54        let mut buf = Vec::with_capacity(ATTESTATION_SIZE);
55        buf.extend_from_slice(&self.proof_term_hash);
56        buf.extend_from_slice(&self.environment_hash);
57        buf.extend_from_slice(&self.verification_timestamp_ns.to_le_bytes());
58        buf.extend_from_slice(&self.verifier_version.to_le_bytes());
59        buf.extend_from_slice(&self.reduction_steps.to_le_bytes());
60        buf.extend_from_slice(&self.cache_hit_rate_bps.to_le_bytes());
61        buf
62    }
63
64    /// Deserialize from bytes.
65    pub fn from_bytes(data: &[u8]) -> Result<Self, &'static str> {
66        if data.len() < ATTESTATION_SIZE {
67            return Err("attestation data too short");
68        }
69
70        let mut proof_term_hash = [0u8; 32];
71        proof_term_hash.copy_from_slice(&data[0..32]);
72
73        let mut environment_hash = [0u8; 32];
74        environment_hash.copy_from_slice(&data[32..64]);
75
76        let verification_timestamp_ns = u64::from_le_bytes(
77            data[64..72].try_into().map_err(|_| "bad timestamp")?
78        );
79        let verifier_version = u32::from_le_bytes(
80            data[72..76].try_into().map_err(|_| "bad version")?
81        );
82        let reduction_steps = u32::from_le_bytes(
83            data[76..80].try_into().map_err(|_| "bad steps")?
84        );
85        let cache_hit_rate_bps = u16::from_le_bytes(
86            data[80..82].try_into().map_err(|_| "bad rate")?
87        );
88
89        Ok(Self {
90            proof_term_hash,
91            environment_hash,
92            verification_timestamp_ns,
93            verifier_version,
94            reduction_steps,
95            cache_hit_rate_bps,
96        })
97    }
98
99    /// Compute a simple hash of this attestation for caching.
100    pub fn content_hash(&self) -> u64 {
101        let bytes = self.to_bytes();
102        let mut h: u64 = 0xcbf29ce484222325;
103        for &b in &bytes {
104            h ^= b as u64;
105            h = h.wrapping_mul(0x100000001b3);
106        }
107        h
108    }
109}
110
111/// Create a ProofAttestation from a completed verification.
112pub fn create_attestation(
113    env: &crate::ProofEnvironment,
114    proof_id: u32,
115) -> ProofAttestation {
116    // Hash the proof ID and environment state
117    let mut proof_hash = [0u8; 32];
118    let id_bytes = proof_id.to_le_bytes();
119    proof_hash[0..4].copy_from_slice(&id_bytes);
120    proof_hash[4..8].copy_from_slice(&env.terms_allocated().to_le_bytes());
121
122    let mut env_hash = [0u8; 32];
123    let sym_count = env.symbols.len() as u32;
124    env_hash[0..4].copy_from_slice(&sym_count.to_le_bytes());
125
126    let stats = env.stats();
127    let cache_rate = if stats.cache_hits + stats.cache_misses > 0 {
128        ((stats.cache_hits * 10000) / (stats.cache_hits + stats.cache_misses)) as u16
129    } else {
130        0
131    };
132
133    ProofAttestation::new(
134        proof_hash,
135        env_hash,
136        stats.total_reductions as u32,
137        cache_rate,
138    )
139}
140
141/// Get current timestamp in nanoseconds.
142fn current_timestamp_ns() -> u64 {
143    std::time::SystemTime::now()
144        .duration_since(std::time::UNIX_EPOCH)
145        .map(|d| d.as_nanos() as u64)
146        .unwrap_or(0)
147}
148
149#[cfg(test)]
150mod tests {
151    use super::*;
152    use crate::ProofEnvironment;
153
154    #[test]
155    fn test_witness_type_code() {
156        assert_eq!(WITNESS_TYPE_FORMAL_PROOF, 0x0E);
157    }
158
159    #[test]
160    fn test_attestation_size() {
161        assert_eq!(ATTESTATION_SIZE, 82);
162    }
163
164    #[test]
165    fn test_attestation_roundtrip() {
166        let att = ProofAttestation::new([1u8; 32], [2u8; 32], 42, 9500);
167        let bytes = att.to_bytes();
168        assert_eq!(bytes.len(), ATTESTATION_SIZE);
169
170        let att2 = ProofAttestation::from_bytes(&bytes).unwrap();
171        assert_eq!(att.proof_term_hash, att2.proof_term_hash);
172        assert_eq!(att.environment_hash, att2.environment_hash);
173        assert_eq!(att.verifier_version, att2.verifier_version);
174        assert_eq!(att.reduction_steps, att2.reduction_steps);
175        assert_eq!(att.cache_hit_rate_bps, att2.cache_hit_rate_bps);
176    }
177
178    #[test]
179    fn test_attestation_from_bytes_too_short() {
180        let result = ProofAttestation::from_bytes(&[0u8; 10]);
181        assert!(result.is_err());
182    }
183
184    #[test]
185    fn test_attestation_content_hash() {
186        let att1 = ProofAttestation::new([1u8; 32], [2u8; 32], 42, 9500);
187        let att2 = ProofAttestation::new([1u8; 32], [2u8; 32], 42, 9500);
188        // Same content -> same hash (ignoring timestamp difference)
189        // Actually timestamps will differ, so hashes will differ
190        // Just verify it doesn't panic
191        let _h1 = att1.content_hash();
192        let _h2 = att2.content_hash();
193    }
194
195    #[test]
196    fn test_create_attestation() {
197        let mut env = ProofEnvironment::new();
198        let proof_id = env.alloc_term();
199        let att = create_attestation(&env, proof_id);
200        assert_eq!(att.verifier_version, 0x00_01_00_00);
201        assert!(att.verification_timestamp_ns > 0);
202    }
203
204    #[test]
205    fn test_verifier_version() {
206        let att = ProofAttestation::new([0u8; 32], [0u8; 32], 0, 0);
207        assert_eq!(att.verifier_version, 0x00_01_00_00);
208    }
209}
ruvector_verified/proof_store.rs

ruvector_verified/
proof_store.rs
