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

use crate::prelude::*;
use std::result::Result;

impl Runtime {
    pub fn verify_and_fact(
        &mut self,
        and_fact: &AndFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(cached_result) =
            self.verify_fact_from_cache_using_display_string(&and_fact.clone().into())
        {
            return Ok(cached_result);
        }

        if !verify_state.well_defined_already_verified {
            if let Err(e) = self.verify_and_fact_well_defined(and_fact, verify_state) {
                return Err(RuntimeError::from(VerifyRuntimeError(
                    RuntimeErrorStruct::new(
                        Some(Fact::from(and_fact.clone()).into_stmt()),
                        String::new(),
                        and_fact.line_file(),
                        Some(e),
                        vec![],
                    ),
                )));
            }
        }

        let verify_state_for_children = verify_state.make_state_with_req_ok_set_to_true();

        let mut child_results: Vec<StmtResult> = Vec::with_capacity(and_fact.facts.len());
        for fact in &and_fact.facts {
            let result = self.verify_atomic_fact(fact, &verify_state_for_children)?;
            if result.is_unknown() {
                return Ok(result);
            }
            child_results.push(result);
        }
        Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
            and_fact.clone().into(),
            VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::fact_with_note(
                and_fact.clone().into(),
                Some("and: each conjunct verified in order".to_string()),
            )]),
            child_results,
        ))
        .into())
    }

    pub fn verify_chain_fact(
        &mut self,
        chain_fact: &ChainFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if let Some(cached_result) =
            self.verify_fact_from_cache_using_display_string(&chain_fact.clone().into())
        {
            return Ok(cached_result);
        }

        if !verify_state.well_defined_already_verified {
            if let Err(e) = self.verify_chain_fact_well_defined(chain_fact, verify_state) {
                return Err(RuntimeError::from(VerifyRuntimeError(
                    RuntimeErrorStruct::new(
                        Some(Fact::from(chain_fact.clone()).into_stmt()),
                        String::new(),
                        chain_fact.line_file(),
                        Some(e),
                        vec![],
                    ),
                )));
            }
        }

        let verify_state_for_children = verify_state.make_state_with_req_ok_set_to_true();

        let facts = chain_fact.facts().map_err(|e| {
            RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new(
                Some(Fact::ChainFact(chain_fact.clone()).into_stmt()),
                String::new(),
                chain_fact.line_file(),
                Some(e),
                vec![],
            )))
        })?;
        let mut child_results: Vec<StmtResult> = Vec::with_capacity(facts.len());
        for fact in &facts {
            let result = self.verify_atomic_fact(fact, &verify_state_for_children)?;
            if result.is_unknown() {
                return Ok((StmtUnknown::new_with_detail(format!(
                    "unverified chain step: {}",
                    fact
                )))
                .into());
            }

            child_results.push(result);
        }
        Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
            chain_fact.clone().into(),
            VerifiedByResult::wrap_bys(vec![VerifiedBysEnum::fact_with_note(
                chain_fact.clone().into(),
                Some("chain: each step verified in order".to_string()),
            )]),
            child_results,
        ))
        .into())
    }
}