litex-lang 0.9.69-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

use crate::prelude::*;

impl Runtime {
    /// If the fact string is in the known-facts cache, return the cached verification result.
    pub fn verify_fact_from_cache_using_display_string(&self, fact: &Fact) -> Option<StmtResult> {
        let key = fact.to_string();
        let (cache_ok, cache_line_file) = self.cache_known_facts_contains(&key);
        if cache_ok {
            Some(
                (FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
                    fact.clone(),
                    key,
                    None,
                    Some(cache_line_file),
                    Vec::new(),
                ))
                .into(),
            )
        } else {
            None
        }
    }

    /// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
    pub fn verify_param_type_nonempty_if_required(
        &mut self,
        param_type: &ParamType,
        check_type_nonempty: bool,
    ) -> Result<(), RuntimeError> {
        if !check_type_nonempty {
            return Ok(());
        }
        match param_type {
            ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
            ParamType::Obj(param_set) => match param_set {
                Obj::FnSet(fn_set) => {
                    let ret_nonempty = IsNonemptySetFact::new(
                        fn_set.body.ret_set.as_ref().clone(),
                        default_line_file(),
                    )
                    .into();
                    self.verify_fact_well_defined_and_store_and_infer(
                        ret_nonempty,
                        &VerifyState::new(2, false),
                    )?;
                    Ok(())
                }
                Obj::AnonymousFn(anon) => {
                    let ret_nonempty = IsNonemptySetFact::new(
                        anon.body.ret_set.as_ref().clone(),
                        default_line_file(),
                    )
                    .into();
                    self.verify_fact_well_defined_and_store_and_infer(
                        ret_nonempty,
                        &VerifyState::new(2, false),
                    )?;
                    Ok(())
                }
                Obj::SetBuilder(_) => Err(RuntimeError::ExecStmtError(RuntimeErrorStruct::new_with_just_msg("set builder param type is not supported yet in verify_param_type_nonempty_if_required"
                        .to_string()))),
                _ => {
                    let nonempty_fact =
                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
                    let ret=  self.verify_fact(
                        &nonempty_fact.into(),
                        &VerifyState::new(0, false),
                    )?;
                    if ret.is_unknown() {
                        return Err(RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new_with_just_msg("param type is not nonempty".to_string()))));
                    }
                    Ok(())
                }
            },
        }
    }
}