litex-lang 0.9.68-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
35
36
37
38
39
40
41
42
43
44
45
46
47
48

use crate::prelude::*;

impl Runtime {
    pub fn exec_def_prop_stmt(
        &mut self,
        def_prop_stmt: &DefPropStmt,
    ) -> Result<StmtResult, RuntimeError> {
        self.run_in_local_env(|rt| rt.def_prop_stmt_check_well_defined(def_prop_stmt))
            .map_err(|e| {
                short_exec_error(def_prop_stmt.clone().into(), "", Some(e), vec![])
            })?;
        self.store_def_prop(def_prop_stmt)?;
        Ok(
            (NonFactualStmtSuccess::new(def_prop_stmt.clone().into(), InferResult::new(), vec![]))
                .into(),
        )
    }

    fn def_prop_stmt_check_well_defined(
        &mut self,
        def_prop_stmt: &DefPropStmt,
    ) -> Result<(), RuntimeError> {
        self.define_params_with_type(
            &def_prop_stmt.params_def_with_type,
            false,
            ParamObjType::DefHeader,
        )
            .map_err(|e| {
                short_exec_error(def_prop_stmt.clone().into(), "", Some(e), vec![])
            })?;

        for fact in def_prop_stmt.iff_facts.iter() {
            self.verify_fact_well_defined_and_store_and_infer(
                fact.clone(),
                &VerifyState::new(0, false),
            )
            .map_err(|inner_exec_error| {
                short_exec_error(
                    def_prop_stmt.clone().into(),
                    "",
                    Some(inner_exec_error),
                    vec![],
                )
            })?;
        }
        Ok(())
    }
}