logicaffeine_compile/codegen_sva/
z3_synth.rs

1//! Sprint 4A: Z3 Synthesis Constraint Builder
2//!
3//! Converts a kernel spec type (Term) into a synthesis constraint.
4//! When tactics can't construct a proof term directly, we ask Z3 to find one.
5//!
6//! For a spec like `Pi(a:Bit). Pi(b:Bit). Bit`, this extracts:
7//! - Inputs: [(a, Bit), (b, Bit)]
8//! - Output: Bit
9//! - Constraint: the function must map all 2^n inputs to valid outputs
10
11use logicaffeine_kernel::Term;
12
13/// Configuration for synthesis constraint building.
14#[derive(Debug, Clone)]
15pub struct SynthesisConstraintConfig {
16    /// Maximum number of Bit inputs to enumerate.
17    pub max_inputs: usize,
18    /// Timeout for Z3 in milliseconds.
19    pub timeout_ms: u64,
20}
21
22impl Default for SynthesisConstraintConfig {
23    fn default() -> Self {
24        Self {
25            max_inputs: 8,
26            timeout_ms: 10000,
27        }
28    }
29}
30
31/// Result of building a synthesis constraint.
32#[derive(Debug, Clone)]
33pub enum SynthesisConstraint {
34    /// A satisfiable constraint — the spec term can be synthesized.
35    /// Contains the normalized spec type with extracted IO information.
36    Satisfiable(Term),
37    /// The spec is unrealizable — no implementation exists.
38    Unrealizable,
39    /// Could not translate the spec type.
40    Unsupported(String),
41}
42
43/// Convert a kernel Pi-typed specification into a synthesis constraint.
44///
45/// Given a spec like `Pi(a:Bit). Pi(b:Bit). Bit`,
46/// this determines whether the spec can be synthesized by:
47/// 1. Extracting input/output types
48/// 2. Checking all types are hardware types (Bit, BVec, Unit)
49/// 3. Returning Satisfiable if the spec is well-formed
50pub fn build_synthesis_constraint(
51    spec_type: &Term,
52    config: &SynthesisConstraintConfig,
53) -> SynthesisConstraint {
54    let (inputs, output) = extract_io_from_spec(spec_type);
55
56    if inputs.is_empty() && output.is_none() {
57        return SynthesisConstraint::Unsupported(
58            "spec has no Pi binders — not a function type".to_string(),
59        );
60    }
61
62    // Check all inputs are hardware types
63    for (name, ty) in &inputs {
64        if !is_hardware_type(ty) {
65            return SynthesisConstraint::Unsupported(format!(
66                "input '{}' has non-hardware type: {:?}",
67                name, ty
68            ));
69        }
70    }
71
72    // Check input count is within bounds
73    let bit_count = inputs.iter().filter(|(_, ty)| is_bit_type(ty)).count();
74    if bit_count > config.max_inputs {
75        return SynthesisConstraint::Unsupported(format!(
76            "too many Bit inputs ({}) exceeds max_inputs ({})",
77            bit_count, config.max_inputs
78        ));
79    }
80
81    // Check output is a hardware type
82    if let Some(ref out_ty) = output {
83        if !is_hardware_type(out_ty) {
84            return SynthesisConstraint::Unsupported(format!(
85                "output has non-hardware type: {:?}",
86                out_ty
87            ));
88        }
89    }
90
91    // If we got here, the spec is synthesizable
92    SynthesisConstraint::Satisfiable(spec_type.clone())
93}
94
95/// Extract input/output signal types from a kernel spec type.
96///
97/// Walks Pi binders to find input names and types. The final non-Pi
98/// type is the output type.
99///
100/// Example: `Pi(a:Bit). Pi(b:Bit). Bit` → inputs=[(a,Bit),(b,Bit)], output=Some(Bit)
101pub fn extract_io_from_spec(spec_type: &Term) -> (Vec<(String, Term)>, Option<Term>) {
102    let mut inputs = Vec::new();
103    let mut current = spec_type;
104
105    loop {
106        match current {
107            Term::Pi {
108                param,
109                param_type,
110                body_type,
111            } => {
112                inputs.push((param.clone(), *param_type.clone()));
113                current = body_type;
114            }
115            other => {
116                // This is the output type (or the body of a dependent type)
117                return (inputs, Some(other.clone()));
118            }
119        }
120    }
121}
122
123/// Check if a Term represents a hardware type (Bit, BVec, Unit, Circuit).
124fn is_hardware_type(ty: &Term) -> bool {
125    match ty {
126        Term::Global(name) => matches!(
127            name.as_str(),
128            "Bit" | "Unit" | "BVec" | "Circuit"
129        ),
130        // BVec n — application of BVec to a Nat
131        Term::App(func, _) => {
132            if let Term::Global(name) = func.as_ref() {
133                name == "BVec" || name == "Circuit"
134            } else {
135                false
136            }
137        }
138        _ => false,
139    }
140}
141
142/// Check if a Term is specifically the Bit type.
143fn is_bit_type(ty: &Term) -> bool {
144    matches!(ty, Term::Global(name) if name == "Bit")
145}
logicaffeine_compile/codegen_sva/z3_synth.rs

logicaffeine_compile/codegen_sva/
z3_synth.rs
