assura_codegen/
metadata.rs

1//! Structured contract metadata for generated Rust projects.
2//!
3//! Produces a machine-readable `assura-contracts.json` sidecar that AI agents
4//! can parse to understand which contracts apply to which functions, what
5//! pre/post-conditions exist, and what types are involved.
6
7use assura_ast::{Clause, ClauseKind, ContractDecl, Decl, ExternDecl, FnDef, expr_to_string};
8use assura_types::TypedFile;
9
10use serde::Serialize;
11
12use crate::types_gen::map_type_token;
13
14/// Root metadata for a generated project.
15#[derive(Debug, Clone, Serialize)]
16pub struct ProjectMetadata {
17    /// Original source file name.
18    pub source: String,
19    /// Contract metadata entries.
20    pub contracts: Vec<ContractMeta>,
21}
22
23/// Metadata for a single contract, extern, or function.
24#[derive(Debug, Clone, Serialize)]
25pub struct ContractMeta {
26    /// Contract/function name.
27    pub name: String,
28    /// Kind of declaration.
29    pub kind: String,
30    /// Generated Rust function name.
31    pub function: String,
32    /// Parameters.
33    pub params: Vec<ParamMeta>,
34    /// Return type info.
35    pub return_type: ReturnTypeMeta,
36    /// Requires clauses as source expressions.
37    pub requires: Vec<String>,
38    /// Ensures clauses as source expressions.
39    pub ensures: Vec<String>,
40    /// Effect annotations.
41    pub effects: Vec<String>,
42}
43
44/// Parameter metadata.
45#[derive(Debug, Clone, Serialize)]
46pub struct ParamMeta {
47    pub name: String,
48    #[serde(rename = "type")]
49    pub assura_type: String,
50    pub rust_type: String,
51}
52
53/// Return type metadata.
54#[derive(Debug, Clone, Serialize)]
55pub struct ReturnTypeMeta {
56    pub assura: String,
57    pub rust: String,
58}
59
60/// Extract structured metadata from a typed file.
61pub fn extract_metadata(typed: &TypedFile, source_name: &str) -> ProjectMetadata {
62    let source = &typed.resolved.source;
63    let mut contracts = Vec::new();
64
65    for decl in &source.decls {
66        match &decl.node {
67            Decl::Contract(c) => {
68                contracts.push(contract_meta(c));
69            }
70            Decl::Extern(ext) => {
71                contracts.push(extern_meta(ext));
72            }
73            Decl::FnDef(f) => {
74                contracts.push(fndef_meta(f));
75            }
76            _ => {}
77        }
78    }
79
80    ProjectMetadata {
81        source: source_name.to_string(),
82        contracts,
83    }
84}
85
86fn contract_meta(c: &ContractDecl) -> ContractMeta {
87    let params: Vec<ParamMeta> = c
88        .fn_params
89        .iter()
90        .map(|p| {
91            let assura_type =
92                p.ty.as_ref()
93                    .map(|t| t.to_string())
94                    .unwrap_or_else(|| "?".to_string());
95            let rust_type =
96                p.ty.as_ref()
97                    .map(|t| map_type_token(&t.to_string()).to_string())
98                    .unwrap_or_else(|| "?".to_string());
99            ParamMeta {
100                name: p.name.clone(),
101                assura_type,
102                rust_type,
103            }
104        })
105        .collect();
106
107    let requires = extract_clause_bodies(&c.clauses, ClauseKind::Requires);
108    let ensures = extract_clause_bodies(&c.clauses, ClauseKind::Ensures);
109    let effects = extract_clause_bodies(&c.clauses, ClauseKind::Effects);
110
111    let return_type = infer_return_type(&c.clauses);
112
113    ContractMeta {
114        name: c.name.clone(),
115        kind: "contract".to_string(),
116        function: "check".to_string(),
117        params,
118        return_type,
119        requires,
120        ensures,
121        effects,
122    }
123}
124
125fn extern_meta(ext: &ExternDecl) -> ContractMeta {
126    let params: Vec<ParamMeta> = ext
127        .params
128        .iter()
129        .map(|p| {
130            let assura_type =
131                p.ty.as_ref()
132                    .map(|t| t.to_string())
133                    .unwrap_or_else(|| "?".to_string());
134            let rust_type =
135                p.ty.as_ref()
136                    .map(|t| map_type_token(&t.to_string()).to_string())
137                    .unwrap_or_else(|| "?".to_string());
138            ParamMeta {
139                name: p.name.clone(),
140                assura_type,
141                rust_type,
142            }
143        })
144        .collect();
145
146    let requires = extract_clause_bodies(&ext.clauses, ClauseKind::Requires);
147    let ensures = extract_clause_bodies(&ext.clauses, ClauseKind::Ensures);
148    let effects = extract_clause_bodies(&ext.clauses, ClauseKind::Effects);
149
150    let return_assura = ext
151        .return_ty
152        .as_ref()
153        .map(|t| t.to_string())
154        .unwrap_or_else(|| "Unit".to_string());
155    let return_rust = map_type_token(&return_assura).to_string();
156
157    ContractMeta {
158        name: ext.name.clone(),
159        kind: "extern".to_string(),
160        function: ext.name.clone(),
161        params,
162        return_type: ReturnTypeMeta {
163            assura: return_assura,
164            rust: return_rust,
165        },
166        requires,
167        ensures,
168        effects,
169    }
170}
171
172fn fndef_meta(f: &FnDef) -> ContractMeta {
173    let params: Vec<ParamMeta> = f
174        .params
175        .iter()
176        .map(|p| {
177            let assura_type =
178                p.ty.as_ref()
179                    .map(|t| t.to_string())
180                    .unwrap_or_else(|| "?".to_string());
181            let rust_type =
182                p.ty.as_ref()
183                    .map(|t| map_type_token(&t.to_string()).to_string())
184                    .unwrap_or_else(|| "?".to_string());
185            ParamMeta {
186                name: p.name.clone(),
187                assura_type,
188                rust_type,
189            }
190        })
191        .collect();
192
193    let requires = extract_clause_bodies(&f.clauses, ClauseKind::Requires);
194    let ensures = extract_clause_bodies(&f.clauses, ClauseKind::Ensures);
195    let effects = extract_clause_bodies(&f.clauses, ClauseKind::Effects);
196
197    let return_assura = f
198        .return_ty
199        .as_ref()
200        .map(|t| t.to_string())
201        .unwrap_or_else(|| "Unit".to_string());
202    let return_rust = map_type_token(&return_assura).to_string();
203
204    ContractMeta {
205        name: f.name.clone(),
206        kind: if f.is_ghost {
207            "ghost_fn"
208        } else if f.is_lemma {
209            "lemma"
210        } else {
211            "fn"
212        }
213        .to_string(),
214        function: f.name.clone(),
215        params,
216        return_type: ReturnTypeMeta {
217            assura: return_assura,
218            rust: return_rust,
219        },
220        requires,
221        ensures,
222        effects,
223    }
224}
225
226fn extract_clause_bodies(clauses: &[Clause], kind: ClauseKind) -> Vec<String> {
227    clauses
228        .iter()
229        .filter(|c| c.kind == kind)
230        .map(|c| expr_to_string(&c.body))
231        .collect()
232}
233
234fn infer_return_type(clauses: &[Clause]) -> ReturnTypeMeta {
235    // Look for output clause to determine return type
236    for clause in clauses {
237        if clause.kind == ClauseKind::Output {
238            let body_str = expr_to_string(&clause.body);
239            // Simple heuristic: if there are type annotations, extract them
240            if body_str.contains(':') {
241                let parts: Vec<&str> = body_str.split(':').collect();
242                if parts.len() >= 2 {
243                    let assura = parts[1].trim().to_string();
244                    let rust = map_type_token(&assura).to_string();
245                    return ReturnTypeMeta { assura, rust };
246                }
247            }
248        }
249    }
250    ReturnTypeMeta {
251        assura: "Unit".to_string(),
252        rust: "()".to_string(),
253    }
254}
255
256/// Generate structured implementation guidance comment for a contract.
257/// This appears above the `todo!()` placeholder in generated code.
258pub fn implementation_guidance_comment(c: &ContractDecl) -> String {
259    let mut lines = Vec::new();
260    lines.push(format!("// ASSURA CONTRACT: {}", c.name));
261
262    // Parameters
263    let params: Vec<String> = c
264        .fn_params
265        .iter()
266        .map(|p| {
267            let ty =
268                p.ty.as_ref()
269                    .map(|t| map_type_token(&t.to_string()).to_string())
270                    .unwrap_or_else(|| "?".to_string());
271            format!("{}: {ty}", p.name)
272        })
273        .collect();
274    if !params.is_empty() {
275        lines.push(format!("// PARAMETERS: {}", params.join(", ")));
276    }
277
278    // Requires
279    for clause in &c.clauses {
280        if clause.kind == ClauseKind::Requires {
281            lines.push(format!("// REQUIRES: {}", expr_to_string(&clause.body)));
282        }
283    }
284
285    // Ensures
286    for clause in &c.clauses {
287        if clause.kind == ClauseKind::Ensures {
288            lines.push(format!("// ENSURES: {}", expr_to_string(&clause.body)));
289        }
290    }
291
292    // Effects
293    let effect_strs: Vec<String> = c
294        .clauses
295        .iter()
296        .filter(|cl| cl.kind == ClauseKind::Effects)
297        .map(|cl| expr_to_string(&cl.body))
298        .collect();
299    if !effect_strs.is_empty() {
300        lines.push(format!("// EFFECTS: {}", effect_strs.join(", ")));
301    } else {
302        lines.push("// EFFECTS: pure".to_string());
303    }
304
305    lines.join("\n")
306}
307
308#[cfg(test)]
309mod tests {
310    use super::*;
311
312    fn typecheck_ok(source: &str) -> assura_types::TypedFile {
313        let file = assura_parser::parse_unwrap(source);
314        let resolved = assura_resolve::resolve(&file).expect("resolve should succeed");
315        assura_types::type_check(resolved).expect("type check should succeed")
316    }
317
318    #[test]
319    fn metadata_extracts_contract_info() {
320        let source = r#"
321contract SafeDiv {
322    input(a: Int, b: Int)
323    requires { b != 0 }
324    ensures { result == a / b }
325}
326"#;
327        let typed = typecheck_ok(source);
328        let meta = extract_metadata(&typed, "test.assura");
329
330        assert_eq!(meta.source, "test.assura");
331        assert!(!meta.contracts.is_empty());
332
333        let c = &meta.contracts[0];
334        assert_eq!(c.name, "SafeDiv");
335        assert_eq!(c.kind, "contract");
336        assert!(!c.requires.is_empty());
337        assert!(!c.ensures.is_empty());
338    }
339
340    #[test]
341    fn metadata_extracts_extern_info() {
342        let source = r#"
343extern fn compute(x: Int, y: Int) -> Int
344    requires { y > 0 }
345    effects { io }
346"#;
347        let typed = typecheck_ok(source);
348        let meta = extract_metadata(&typed, "test.assura");
349
350        assert!(!meta.contracts.is_empty());
351        let c = &meta.contracts[0];
352        assert_eq!(c.name, "compute");
353        assert_eq!(c.kind, "extern");
354        assert!(!c.requires.is_empty());
355    }
356
357    #[test]
358    fn guidance_comment_includes_contract_info() {
359        let source = r#"
360contract Bounded {
361    input(x: Int, max: Int)
362    requires { x >= 0 }
363    requires { x < max }
364    ensures { result >= 0 }
365}
366"#;
367        let (file, _) = assura_parser::parse(source);
368        let file = file.unwrap();
369        if let assura_ast::Decl::Contract(c) = &file.decls[0].node {
370            let comment = implementation_guidance_comment(c);
371            assert!(comment.contains("ASSURA CONTRACT: Bounded"));
372            assert!(comment.contains("REQUIRES:"));
373            assert!(comment.contains("ENSURES:"));
374        } else {
375            panic!("expected contract");
376        }
377    }
378
379    #[test]
380    fn metadata_serializes_to_json() {
381        let source = r#"
382contract Add {
383    input(a: Int, b: Int)
384    ensures { result == a + b }
385}
386"#;
387        let typed = typecheck_ok(source);
388        let meta = extract_metadata(&typed, "test.assura");
389        let json = serde_json::to_string_pretty(&meta).unwrap();
390        assert!(json.contains("\"name\": \"Add\""));
391        assert!(json.contains("\"contracts\""));
392        assert!(json.contains("\"ensures\""));
393    }
394}
assura_codegen/metadata.rs

assura_codegen/
metadata.rs
