litex-lang 0.9.65-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

use crate::prelude::*;

impl Runtime {
    pub fn exec_prove_stmt(&mut self, stmt: &ProveStmt) -> Result<StmtResult, RuntimeError> {
        let inside_results = self.run_in_local_env(|rt| {
            let mut inside_results: Vec<StmtResult> = Vec::new();
            for proof_stmt in &stmt.proof {
                let exec_stmt_result = rt.exec_stmt(proof_stmt);
                match exec_stmt_result {
                    Ok(result) => inside_results.push(result),
                    Err(statement_error) => {
                        return Err(short_exec_error(
                            stmt.clone().into(),
                            proof_stmt.to_string(),
                            Some(statement_error),
                            std::mem::take(&mut inside_results),
                        ));
                    }
                }
            }
            Ok(inside_results)
        });

        match inside_results {
            Ok(_) => {
                Ok(
                    (NonFactualStmtSuccess::new(stmt.clone().into(), InferResult::new(), vec![]))
                        .into(),
                )
            }
            Err(inside_results_error) => Err(inside_results_error),
        }
    }
}