litex-lang 0.9.70-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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

use crate::prelude::*;

impl Runtime {
    pub fn verify_exist_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: &ExistOrAndChainAtomicFact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeError> {
        let stmt_for_fact_errors: Stmt = fact.clone().to_fact().into();
        self.verify_exist_or_and_chain_atomic_fact_well_defined(fact, verify_state)
            .map_err(|well_defined_error| {
                short_exec_error(
                    stmt_for_fact_errors.clone(),
                    "",
                    Some(well_defined_error),
                    vec![],
                )
            })?;
        self.store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(
            fact.clone(),
        )
        .map_err(|store_fact_error| {
            short_exec_error(
                stmt_for_fact_errors,
                "",
                Some(store_fact_error),
                vec![],
            )
        })
    }

    pub fn verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: &OrAndChainAtomicFact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeError> {
        let stmt_for_fact_errors: Stmt = fact.clone().to_fact().into();
        self.verify_or_and_chain_atomic_fact_well_defined(fact, verify_state)
            .map_err(|well_defined_error| {
                short_exec_error(
                    stmt_for_fact_errors.clone(),
                    "",
                    Some(well_defined_error),
                    vec![],
                )
            })?;
        self.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(fact.clone())
            .map_err(|store_fact_error| {
                short_exec_error(
                    stmt_for_fact_errors,
                    "",
                    Some(store_fact_error),
                    vec![],
                )
            })
    }

    pub fn verify_fact_well_defined_and_store_and_infer(
        &mut self,
        fact: Fact,
        verify_state: &VerifyState,
    ) -> Result<InferResult, RuntimeError> {
        let stmt_for_fact_errors: Stmt = fact.clone().into();
        self.verify_well_defined_and_store_and_infer(fact, verify_state)
            .map_err(|e| {
                short_exec_error(
                    stmt_for_fact_errors,
                    "",
                    Some(e),
                    vec![],
                )
            })
    }
}