sentri_generator_move/
generator.rs

1//! Move generator implementation.
2
3use sentri_core::model::{GenerationOutput, Invariant, ProgramModel};
4use sentri_core::traits::CodeGenerator;
5use sentri_core::Result;
6use tracing::info;
7
8/// Code generator for Move programs.
9pub struct MoveGenerator;
10
11impl CodeGenerator for MoveGenerator {
12    fn generate(
13        &self,
14        program: &ProgramModel,
15        invariants: &[Invariant],
16    ) -> Result<GenerationOutput> {
17        info!(
18            "Generating Move assertions for {} with {} invariants",
19            program.name,
20            invariants.len()
21        );
22
23        let mut assertions = Vec::new();
24        for inv in invariants {
25            assertions.push(format!(
26                "assert!({}, E_INVARIANT_{});",
27                inv.expression,
28                inv.name.to_uppercase()
29            ));
30        }
31
32        let code = format!(
33            "// Generated Move invariant checks for {}\n// {} assertions\n",
34            program.name,
35            assertions.len()
36        );
37
38        Ok(GenerationOutput {
39            code,
40            assertions,
41            tests: None,
42            coverage_percent: 0,
43        })
44    }
45
46    fn chain(&self) -> &str {
47        "move"
48    }
49}
sentri_generator_move/generator.rs

sentri_generator_move/
generator.rs
