litex-lang 0.9.82-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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

use crate::prelude::*;
use std::collections::HashMap;

impl Runtime {
    pub(crate) fn infer_not_forall_fact(
        &mut self,
        not_forall: &NotForallFact,
    ) -> Result<InferResult, RuntimeError> {
        let Some(exist_fact) = self.build_not_forall_counterexample_exist_fact(not_forall)? else {
            return Ok(InferResult::new());
        };

        let inferred_fact: Fact = exist_fact.into();
        let mut out = InferResult::new();
        out.new_fact(&inferred_fact);
        out.new_infer_result_inside(
            self.store_fact_without_forall_coverage_check_and_infer(inferred_fact)?,
        );
        Ok(out)
    }

    fn build_not_forall_counterexample_exist_fact(
        &self,
        not_forall: &NotForallFact,
    ) -> Result<Option<ExistFactEnum>, RuntimeError> {
        let forall = &not_forall.forall_fact;
        if forall.params_def_with_type.number_of_params() == 0 || forall.then_facts.is_empty() {
            return Ok(None);
        }

        let mut param_to_exist_obj: HashMap<String, Obj> = HashMap::new();
        let mut exist_groups: Vec<ParamGroupWithParamType> = Vec::new();
        for group in forall.params_def_with_type.groups.iter() {
            for name in group.params.iter() {
                param_to_exist_obj.insert(
                    name.clone(),
                    obj_for_bound_param_in_scope(name.clone(), ParamObjType::Exist),
                );
            }
            let param_type =
                self.inst_param_type(&group.param_type, &param_to_exist_obj, ParamObjType::Forall)?;
            exist_groups.push(ParamGroupWithParamType::new(
                group.params.clone(),
                param_type,
            ));
        }

        let mut body_facts: Vec<ExistBodyFact> = Vec::new();
        for dom_fact in forall.dom_facts.iter() {
            let Some(dom_body_fact) =
                self.fact_to_exist_body_fact(dom_fact, &param_to_exist_obj)?
            else {
                return Ok(None);
            };
            body_facts.push(dom_body_fact.into());
        }

        let mut negated_then_branches: Vec<AndChainAtomicFact> = Vec::new();
        for then_fact in forall.then_facts.iter() {
            let Some(then_body_fact) =
                self.then_fact_to_exist_body_fact(then_fact, &param_to_exist_obj)?
            else {
                return Ok(None);
            };
            let Ok(mut branches) = Self::demorgan_negate_exist_body_conjunct(&then_body_fact)
            else {
                return Ok(None);
            };
            negated_then_branches.append(&mut branches);
        }
        if negated_then_branches.is_empty() {
            return Ok(None);
        }

        body_facts.push(if negated_then_branches.len() == 1 {
            and_chain_atomic_to_or_and_chain_atomic(negated_then_branches.remove(0)).into()
        } else {
            OrAndChainAtomicFact::OrFact(OrFact::new(
                negated_then_branches,
                forall.line_file.clone(),
            ))
            .into()
        });

        Ok(Some(ExistFactEnum::ExistFact(ExistFactBody::new(
            ParamDefWithType::new(exist_groups),
            body_facts,
            forall.line_file.clone(),
        )?)))
    }

    fn fact_to_exist_body_fact(
        &self,
        fact: &Fact,
        param_to_exist_obj: &HashMap<String, Obj>,
    ) -> Result<Option<OrAndChainAtomicFact>, RuntimeError> {
        let instantiated = self.inst_fact(fact, param_to_exist_obj, ParamObjType::Forall, None)?;
        Ok(match instantiated {
            Fact::AtomicFact(f) => Some(OrAndChainAtomicFact::AtomicFact(f)),
            Fact::AndFact(f) => Some(OrAndChainAtomicFact::AndFact(f)),
            Fact::ChainFact(f) => Some(OrAndChainAtomicFact::ChainFact(f)),
            Fact::OrFact(f) => Some(OrAndChainAtomicFact::OrFact(f)),
            Fact::ExistFact(_)
            | Fact::ForallFact(_)
            | Fact::ForallFactWithIff(_)
            | Fact::NotForall(_) => None,
        })
    }

    fn then_fact_to_exist_body_fact(
        &self,
        fact: &ExistOrAndChainAtomicFact,
        param_to_exist_obj: &HashMap<String, Obj>,
    ) -> Result<Option<OrAndChainAtomicFact>, RuntimeError> {
        let instantiated = self.inst_exist_or_and_chain_atomic_fact(
            fact,
            param_to_exist_obj,
            ParamObjType::Forall,
            None,
        )?;
        Ok(match instantiated {
            ExistOrAndChainAtomicFact::AtomicFact(f) => Some(OrAndChainAtomicFact::AtomicFact(f)),
            ExistOrAndChainAtomicFact::AndFact(f) => Some(OrAndChainAtomicFact::AndFact(f)),
            ExistOrAndChainAtomicFact::ChainFact(f) => Some(OrAndChainAtomicFact::ChainFact(f)),
            ExistOrAndChainAtomicFact::OrFact(f) => Some(OrAndChainAtomicFact::OrFact(f)),
            ExistOrAndChainAtomicFact::ExistFact(_) => None,
        })
    }
}

fn and_chain_atomic_to_or_and_chain_atomic(fact: AndChainAtomicFact) -> OrAndChainAtomicFact {
    match fact {
        AndChainAtomicFact::AtomicFact(f) => OrAndChainAtomicFact::AtomicFact(f),
        AndChainAtomicFact::AndFact(f) => OrAndChainAtomicFact::AndFact(f),
        AndChainAtomicFact::ChainFact(f) => OrAndChainAtomicFact::ChainFact(f),
    }
}