provable_contracts/
generate.rs

1//! End-to-end codegen — generates all artifacts to disk.
2//!
3//! Combines scaffold, kani, and probar generators into a single
4//! operation that writes files to a target directory.
5
6use std::path::{Path, PathBuf};
7
8use crate::binding::BindingRegistry;
9use crate::book_gen::generate_contract_page;
10use crate::coq_gen::generate_coq_spec;
11use crate::graph::{dependency_graph, DependencyGraph};
12use crate::invariant_gen::generate_invariants;
13use crate::kani_gen::generate_kani_harnesses;
14use crate::probar_gen::{generate_probar_tests, generate_wired_probar_tests};
15use crate::scaffold::generate_trait;
16use crate::schema::Contract;
17
18/// Manifest of generated files.
19#[derive(Debug, Clone)]
20pub struct GeneratedFiles {
21    /// Files that were generated.
22    pub files: Vec<GeneratedFile>,
23}
24
25/// A single generated file.
26#[derive(Debug, Clone)]
27pub struct GeneratedFile {
28    /// Path relative to the output directory.
29    pub relative_path: PathBuf,
30    /// Absolute path where the file was written.
31    pub absolute_path: PathBuf,
32    /// What kind of artifact this is.
33    pub kind: ArtifactKind,
34    /// Number of bytes written.
35    pub bytes: usize,
36}
37
38/// The kind of generated artifact.
39#[derive(Debug, Clone, Copy, PartialEq, Eq)]
40pub enum ArtifactKind {
41    Scaffold,
42    KaniHarness,
43    ProbarTest,
44    WiredProbarTest,
45    BookPage,
46    Invariants,
47    CoqSpec,
48}
49
50impl std::fmt::Display for ArtifactKind {
51    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
52        match self {
53            Self::Scaffold => write!(f, "scaffold"),
54            Self::KaniHarness => write!(f, "kani"),
55            Self::ProbarTest => write!(f, "probar"),
56            Self::WiredProbarTest => write!(f, "wired-probar"),
57            Self::BookPage => write!(f, "book-page"),
58            Self::Invariants => write!(f, "invariants"),
59            Self::CoqSpec => write!(f, "coq"),
60        }
61    }
62}
63
64/// Generate all artifacts from a contract and write to `output_dir`.
65///
66/// Creates the output directory if it doesn't exist. Generates:
67/// - `scaffold.rs` — trait + test stubs
68/// - `kani.rs` — `#[kani::proof]` harnesses
69/// - `probar.rs` — property-based tests
70/// - `wired_probar.rs` — wired tests (only if binding provided)
71///
72/// # Errors
73///
74/// Returns `io::Error` if directory creation or file writes fail.
75pub fn generate_all(
76    contract: &Contract,
77    stem: &str,
78    output_dir: &Path,
79    binding: Option<&BindingRegistry>,
80) -> Result<GeneratedFiles, std::io::Error> {
81    std::fs::create_dir_all(output_dir)?;
82
83    let mut files = Vec::new();
84
85    // Scaffold
86    let scaffold_content = generate_trait(contract);
87    let scaffold_path = output_dir.join(format!("{stem}_scaffold.rs"));
88    std::fs::write(&scaffold_path, &scaffold_content)?;
89    files.push(GeneratedFile {
90        relative_path: PathBuf::from(format!("{stem}_scaffold.rs")),
91        absolute_path: scaffold_path,
92        kind: ArtifactKind::Scaffold,
93        bytes: scaffold_content.len(),
94    });
95
96    // Kani harnesses
97    let kani_content = generate_kani_harnesses(contract);
98    let kani_path = output_dir.join(format!("{stem}_kani.rs"));
99    std::fs::write(&kani_path, &kani_content)?;
100    files.push(GeneratedFile {
101        relative_path: PathBuf::from(format!("{stem}_kani.rs")),
102        absolute_path: kani_path,
103        kind: ArtifactKind::KaniHarness,
104        bytes: kani_content.len(),
105    });
106
107    // Probar tests
108    let probar_content = generate_probar_tests(contract);
109    let probar_path = output_dir.join(format!("{stem}_probar.rs"));
110    std::fs::write(&probar_path, &probar_content)?;
111    files.push(GeneratedFile {
112        relative_path: PathBuf::from(format!("{stem}_probar.rs")),
113        absolute_path: probar_path,
114        kind: ArtifactKind::ProbarTest,
115        bytes: probar_content.len(),
116    });
117
118    // Wired probar tests (only if binding provided)
119    if let Some(reg) = binding {
120        let contract_file = format!("{stem}.yaml");
121        let wired_content = generate_wired_probar_tests(contract, &contract_file, reg);
122        let wired_path = output_dir.join(format!("{stem}_wired_probar.rs"));
123        std::fs::write(&wired_path, &wired_content)?;
124        files.push(GeneratedFile {
125            relative_path: PathBuf::from(format!("{stem}_wired_probar.rs")),
126            absolute_path: wired_path,
127            kind: ArtifactKind::WiredProbarTest,
128            bytes: wired_content.len(),
129        });
130    }
131
132    // Type invariants (only if contract has type_invariants)
133    let invariant_content = generate_invariants(contract);
134    if !invariant_content.is_empty() {
135        let inv_path = output_dir.join(format!("{stem}_invariants.rs"));
136        std::fs::write(&inv_path, &invariant_content)?;
137        files.push(GeneratedFile {
138            relative_path: PathBuf::from(format!("{stem}_invariants.rs")),
139            absolute_path: inv_path,
140            kind: ArtifactKind::Invariants,
141            bytes: invariant_content.len(),
142        });
143    }
144
145    // Coq theorem stubs
146    let coq_content = generate_coq_spec(contract, stem);
147    let coq_path = output_dir.join(format!("{stem}.v"));
148    std::fs::write(&coq_path, &coq_content)?;
149    files.push(GeneratedFile {
150        relative_path: PathBuf::from(format!("{stem}.v")),
151        absolute_path: coq_path,
152        kind: ArtifactKind::CoqSpec,
153        bytes: coq_content.len(),
154    });
155
156    // Book page (single-contract graph with just this contract)
157    let single_graph = build_single_contract_graph(contract, stem);
158    let book_content = generate_contract_page(contract, stem, &single_graph);
159    let book_path = output_dir.join(format!("{stem}_book.md"));
160    std::fs::write(&book_path, &book_content)?;
161    files.push(GeneratedFile {
162        relative_path: PathBuf::from(format!("{stem}_book.md")),
163        absolute_path: book_path,
164        kind: ArtifactKind::BookPage,
165        bytes: book_content.len(),
166    });
167
168    Ok(GeneratedFiles { files })
169}
170
171/// Build a minimal dependency graph for a single contract.
172/// Used by `generate_all` when the full graph isn't available.
173fn build_single_contract_graph(contract: &Contract, stem: &str) -> DependencyGraph {
174    let refs = vec![(stem.to_string(), contract)];
175    dependency_graph(&refs)
176}
177
178#[cfg(test)]
179mod tests {
180    use super::*;
181    use crate::schema::parse_contract_str;
182
183    fn minimal_contract() -> Contract {
184        parse_contract_str(
185            r#"
186metadata:
187  version: "1.0.0"
188  description: "Test"
189  references: ["Paper"]
190equations:
191  f:
192    formula: "f(x) = x"
193proof_obligations:
194  - type: invariant
195    property: "output finite"
196falsification_tests:
197  - id: FALSIFY-001
198    rule: "finiteness"
199    prediction: "output is always finite"
200    if_fails: "overflow"
201kani_harnesses:
202  - id: KANI-001
203    obligation: OBL-001
204    bound: 16
205"#,
206        )
207        .unwrap()
208    }
209
210    #[test]
211    fn generate_all_without_binding() {
212        let c = minimal_contract();
213        let dir = tempfile::tempdir().unwrap();
214        let result = generate_all(&c, "test-kernel-v1", dir.path(), None).unwrap();
215        assert_eq!(result.files.len(), 5); // scaffold + kani + probar + coq + book
216        assert!(result
217            .files
218            .iter()
219            .any(|f| f.kind == ArtifactKind::Scaffold));
220        assert!(result
221            .files
222            .iter()
223            .any(|f| f.kind == ArtifactKind::KaniHarness));
224        assert!(result
225            .files
226            .iter()
227            .any(|f| f.kind == ArtifactKind::ProbarTest));
228        assert!(result
229            .files
230            .iter()
231            .any(|f| f.kind == ArtifactKind::BookPage));
232        for f in &result.files {
233            assert!(f.absolute_path.exists());
234            assert!(f.bytes > 0);
235        }
236    }
237
238    #[test]
239    fn generate_all_with_binding() {
240        let c = minimal_contract();
241        let binding = crate::binding::parse_binding_str(
242            r#"
243version: "1.0.0"
244target_crate: test
245bindings:
246  - contract: test-kernel-v1.yaml
247    equation: f
248    module_path: "test::f"
249    function: f
250    signature: "fn f(x: &[f32]) -> Vec<f32>"
251    status: implemented
252"#,
253        )
254        .unwrap();
255        let dir = tempfile::tempdir().unwrap();
256        let result = generate_all(&c, "test-kernel-v1", dir.path(), Some(&binding)).unwrap();
257        assert_eq!(result.files.len(), 6); // scaffold + kani + probar + wired + coq + book
258        assert!(result
259            .files
260            .iter()
261            .any(|f| f.kind == ArtifactKind::WiredProbarTest));
262    }
263
264    #[test]
265    fn generates_into_subdir() {
266        let c = minimal_contract();
267        let dir = tempfile::tempdir().unwrap();
268        let sub = dir.path().join("deep").join("nested");
269        let result = generate_all(&c, "test-kernel-v1", &sub, None).unwrap();
270        assert_eq!(result.files.len(), 5); // scaffold + kani + probar + coq + book
271        assert!(sub.exists());
272    }
273
274    #[test]
275    fn artifact_kind_display() {
276        assert_eq!(ArtifactKind::Scaffold.to_string(), "scaffold");
277        assert_eq!(ArtifactKind::KaniHarness.to_string(), "kani");
278        assert_eq!(ArtifactKind::ProbarTest.to_string(), "probar");
279        assert_eq!(ArtifactKind::WiredProbarTest.to_string(), "wired-probar");
280        assert_eq!(ArtifactKind::BookPage.to_string(), "book-page");
281    }
282
283    #[test]
284    fn file_names_use_stem() {
285        let c = minimal_contract();
286        let dir = tempfile::tempdir().unwrap();
287        let result = generate_all(&c, "softmax-kernel-v1", dir.path(), None).unwrap();
288        let names: Vec<String> = result
289            .files
290            .iter()
291            .map(|f| f.relative_path.to_string_lossy().to_string())
292            .collect();
293        assert!(names.contains(&"softmax-kernel-v1_scaffold.rs".to_string()));
294        assert!(names.contains(&"softmax-kernel-v1_kani.rs".to_string()));
295        assert!(names.contains(&"softmax-kernel-v1_probar.rs".to_string()));
296    }
297}
provable_contracts/generate.rs

provable_contracts/
generate.rs
