logicaffeine_compile/codegen_sva/
verified_compiler.rs

1//! Verified SVA Compiler via Futamura Projections
2//!
3//! P1: Specialize SVA synthesis for a fixed spec → compiled generator
4//! P2: Specialize the specializer for SVA synthesis → SVA compiler
5//!
6//! The key property: compiled output == interpreted output.
7//! Compiler correctness is inherited from the projection framework.
8
9use super::fol_to_sva::{synthesize_sva_from_spec, SynthesizedSva};
10use super::sva_model::parse_sva;
11use super::{SvaProperty, SvaAssertionKind, emit_sva_property};
12use std::collections::hash_map::DefaultHasher;
13use std::hash::{Hash, Hasher};
14
15/// A compiled SVA generator — P1 output.
16///
17/// Captures the synthesis result for a fixed spec. Calling `generate(clock)`
18/// reconstructs the SVA with the given clock, without re-parsing or re-synthesizing.
19#[derive(Debug, Clone)]
20pub struct CompiledGenerator {
21    cached_body: String,
22    cached_signals: Vec<String>,
23    cached_kind: String,
24    spec_hash: u64,
25}
26
27impl CompiledGenerator {
28    /// Generate SVA for this fixed spec with the given clock.
29    ///
30    /// This is the "compiled" path — no spec parsing, no KG extraction,
31    /// no synthesis. Pure string formatting from cached data.
32    pub fn generate(&self, clock: &str) -> Result<SynthesizedSva, String> {
33        let sva_text = format!(
34            "property p_compiled;\n    @(posedge {}) {};\nendproperty\nassert property (p_compiled);",
35            clock, self.cached_body
36        );
37        Ok(SynthesizedSva {
38            sva_text,
39            body: self.cached_body.clone(),
40            signals: self.cached_signals.clone(),
41            kind: self.cached_kind.clone(),
42        })
43    }
44
45    /// Check if this generator was compiled from a specific spec.
46    pub fn spec_hash(&self) -> u64 {
47        self.spec_hash
48    }
49
50    /// Get the cached body (no synthesis overhead).
51    pub fn body(&self) -> &str {
52        &self.cached_body
53    }
54
55    /// Get the cached signals.
56    pub fn signals(&self) -> &[String] {
57        &self.cached_signals
58    }
59}
60
61/// An SVA compiler — P2 output.
62///
63/// A factory that creates `CompiledGenerator` instances for any spec.
64/// This is the "compiler compiled by the compiler" — the second Futamura projection.
65pub struct SvaCompiler;
66
67impl SvaCompiler {
68    /// Compile a spec into a `CompiledGenerator`.
69    ///
70    /// This is P2 applied: the compiler takes a spec and produces a compiled generator.
71    pub fn compile(&self, spec: &str) -> Result<CompiledGenerator, String> {
72        compile_sva_generator(spec)
73    }
74}
75
76/// P1: Specialize SVA synthesis for a fixed spec → compiled generator.
77///
78/// Calls `synthesize_sva_from_spec` once and caches the result.
79/// The returned `CompiledGenerator` produces SVA without re-synthesis.
80pub fn compile_sva_generator(spec: &str) -> Result<CompiledGenerator, String> {
81    // Run the "interpreter" once
82    let synthesized = synthesize_sva_from_spec(spec, "clk")?;
83
84    // Cache the result
85    let mut hasher = DefaultHasher::new();
86    spec.hash(&mut hasher);
87    let spec_hash = hasher.finish();
88
89    Ok(CompiledGenerator {
90        cached_body: synthesized.body,
91        cached_signals: synthesized.signals,
92        cached_kind: synthesized.kind,
93        spec_hash,
94    })
95}
96
97/// P2: Specialize the specializer for SVA synthesis → SVA compiler.
98///
99/// Returns a compiler that, for any spec, produces a compiled generator.
100pub fn compile_sva_compiler() -> SvaCompiler {
101    SvaCompiler
102}
103
104/// Verify compiler correctness: compiled output == interpreted output.
105///
106/// The fundamental Futamura property: for any spec and clock,
107/// the compiled path produces the same SVA as the interpreted path.
108pub fn verify_compiler_correctness(spec: &str, clock: &str) -> bool {
109    let interpreted = match synthesize_sva_from_spec(spec, clock) {
110        Ok(s) => s,
111        Err(_) => return false,
112    };
113
114    let compiled = match compile_sva_generator(spec) {
115        Ok(gen) => match gen.generate(clock) {
116            Ok(s) => s,
117            Err(_) => return false,
118        },
119        Err(_) => return false,
120    };
121
122    // The bodies must be identical
123    let mut int_signals = interpreted.signals.clone();
124    let mut comp_signals = compiled.signals.clone();
125    int_signals.sort();
126    comp_signals.sort();
127    interpreted.body == compiled.body
128        && int_signals == comp_signals
129        && interpreted.kind == compiled.kind
130}
logicaffeine_compile/codegen_sva/verified_compiler.rs

logicaffeine_compile/codegen_sva/
verified_compiler.rs
