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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

use crate::prelude::*;

impl Runtime {
    /// Verify subset by duality: `a subset b` iff `b superset a`.
    pub(crate) fn verify_subset_fact_with_builtin_rules(
        &mut self,
        subset_fact: &SubsetFact,
        _verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if subset_fact.left.to_string() == subset_fact.right.to_string() {
            return Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::SubsetFact(subset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into());
        }

        let converted_superset_fact = AtomicFact::SupersetFact(SupersetFact::new(
            subset_fact.right.clone(),
            subset_fact.left.clone(),
            subset_fact.line_file.clone(),
        ));
        let verify_result = self
            .verify_non_equational_atomic_fact_with_known_atomic_non_equational_facts(
                &converted_superset_fact,
            )?;
        if verify_result.is_true() {
            Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::SubsetFact(subset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into())
        } else {
            Ok((StmtUnknown::new()).into())
        }
    }

    /// Verify superset by duality: `a superset b` iff `b subset a`.
    pub(crate) fn verify_superset_fact_with_builtin_rules(
        &mut self,
        superset_fact: &SupersetFact,
        _verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if superset_fact.left.to_string() == superset_fact.right.to_string() {
            return Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::SupersetFact(superset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into());
        }
        let converted_subset_fact = AtomicFact::SubsetFact(SubsetFact::new(
            superset_fact.right.clone(),
            superset_fact.left.clone(),
            superset_fact.line_file.clone(),
        ));
        let verify_result = self
            .verify_non_equational_atomic_fact_with_known_atomic_non_equational_facts(
                &converted_subset_fact,
            )?;
        if verify_result.is_true() {
            Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::SupersetFact(superset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into())
        } else {
            Ok((StmtUnknown::new()).into())
        }
    }

    /// Verify `not subset` by converting to the dual `not superset`.
    pub(crate) fn verify_not_subset_fact_with_builtin_rules(
        &mut self,
        not_subset_fact: &NotSubsetFact,
        _verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let converted_not_superset_fact = AtomicFact::NotSupersetFact(NotSupersetFact::new(
            not_subset_fact.right.clone(),
            not_subset_fact.left.clone(),
            not_subset_fact.line_file.clone(),
        ));
        let verify_result = self
            .verify_non_equational_atomic_fact_with_known_atomic_non_equational_facts(
                &converted_not_superset_fact,
            )?;
        if verify_result.is_true() {
            Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::NotSubsetFact(not_subset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into())
        } else {
            Ok((StmtUnknown::new()).into())
        }
    }

    /// Verify `not superset` by converting to the dual `not subset`.
    pub(crate) fn verify_not_superset_fact_with_builtin_rules(
        &mut self,
        not_superset_fact: &NotSupersetFact,
        _verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let converted_not_subset_fact = AtomicFact::NotSubsetFact(NotSubsetFact::new(
            not_superset_fact.right.clone(),
            not_superset_fact.left.clone(),
            not_superset_fact.line_file.clone(),
        ));
        let verify_result = self
            .verify_non_equational_atomic_fact_with_known_atomic_non_equational_facts(
                &converted_not_subset_fact,
            )?;
        if verify_result.is_true() {
            Ok((FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
                    Fact::AtomicFact(AtomicFact::NotSupersetFact(not_superset_fact.clone())),
                    "subset_superset_duality".to_string(),
                    Vec::new(),
                )).into())
        } else {
            Ok((StmtUnknown::new()).into())
        }
    }
}