litex-lang 0.9.6-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
75
76
77
78
79

use crate::prelude::*;

impl Runtime {
    pub fn verify_non_equational_atomic_fact_with_builtin_rules(
        &mut self,
        atomic_fact: &AtomicFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        match atomic_fact {
            AtomicFact::EqualFact(_) => unreachable!(),
            AtomicFact::NotEqualFact(not_equal_fact) => {
                self._verify_not_equal_fact_with_builtin_rules(not_equal_fact, verify_state)
            }
            AtomicFact::InFact(in_fact) => {
                self.verify_in_fact_with_builtin_rules(in_fact, verify_state)
            }
            AtomicFact::NotInFact(not_in_fact) => {
                self.verify_not_in_fact_with_builtin_rules(not_in_fact, verify_state)
            }
            AtomicFact::SubsetFact(subset_fact) => {
                self.verify_subset_fact_with_builtin_rules(subset_fact, verify_state)
            }
            AtomicFact::SupersetFact(superset_fact) => {
                self.verify_superset_fact_with_builtin_rules(superset_fact, verify_state)
            }
            AtomicFact::NotSubsetFact(not_subset_fact) => {
                self.verify_not_subset_fact_with_builtin_rules(not_subset_fact, verify_state)
            }
            AtomicFact::NotSupersetFact(not_superset_fact) => {
                self.verify_not_superset_fact_with_builtin_rules(not_superset_fact, verify_state)
            }
            AtomicFact::NotLessFact(_)
            | AtomicFact::NotGreaterFact(_)
            | AtomicFact::NotLessEqualFact(_)
            | AtomicFact::NotGreaterEqualFact(_)
            | AtomicFact::LessFact(_)
            | AtomicFact::GreaterFact(_)
            | AtomicFact::LessEqualFact(_)
            | AtomicFact::GreaterEqualFact(_) => Ok(
                self.verify_order_atomic_fact_numeric_builtin_only(atomic_fact),
            ),
            AtomicFact::IsSetFact(is_set_fact) => Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::IsSetFact(is_set_fact.clone())),
                    "Every object is a set.".to_string(),
                    Vec::new(),
                )).into()),
            AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => self
                ._verify_is_nonempty_set_fact_with_builtin_rules(
                    is_nonempty_set_fact,
                    verify_state,
                ),
            AtomicFact::IsFiniteSetFact(is_finite_set_fact) => {
                self._verify_is_finite_set_fact_with_builtin_rules(is_finite_set_fact, verify_state)
            }
            AtomicFact::IsCartFact(is_cart_fact) => {
                self._verify_is_cart_fact_with_builtin_rules(is_cart_fact, verify_state)
            }
            AtomicFact::IsTupleFact(is_tuple_fact) => {
                self._verify_is_tuple_fact_with_builtin_rules(is_tuple_fact, verify_state)
            }
            AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => self
                ._verify_not_is_nonempty_set_fact_with_builtin_rules(
                    not_is_nonempty_set_fact,
                    verify_state,
                ),
            _ => Ok((StmtUnknown::new()).into()),
        }
    }

    pub(crate) fn non_equational_atomic_fact_holds_by_full_verify_pipeline(
        &mut self,
        atomic_fact: &AtomicFact,
        verify_state: &VerifyState,
    ) -> Result<bool, RuntimeError> {
        let verify_result =
            self.verify_non_equational_atomic_fact(atomic_fact, verify_state, true)?;
        Ok(verify_result.is_true())
    }
}