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

use super::helpers_by_stmt::impossible_proof_error_message;
use crate::prelude::*;

impl Runtime {
    pub fn exec_by_contra_stmt(&mut self, stmt: &ByContraStmt) -> Result<StmtResult, RuntimeError> {
        let to_prove_fact: Fact = stmt.to_prove.clone().into();
        self.verify_fact_well_defined(&to_prove_fact, &VerifyState::new(0, false))
            .map_err(|verify_error| {
                short_exec_error(
 stmt.clone().into(),
                    format!("by contra: failed to prove `{}`", to_prove_fact),
                    Some(verify_error),
                    vec![],
                )
            })?;

        let (exec_proof_inside_results, last_error) = self.run_in_local_env(|rt| {
            let mut inside_results: Vec<StmtResult> = Vec::new();

            let reverse_to_prove_fact = stmt.to_prove.make_reversed();
            rt.store_atomic_fact_without_well_defined_verified_and_infer(reverse_to_prove_fact)
                .map_err(|store_fact_error| {
                    short_exec_error(
 stmt.clone().into(),
                    format!("by contra: failed to know reverse of `{}`", to_prove_fact),
                    Some(store_fact_error),
                    vec![],
                )
                })?;

            let mut last_error: Option<RuntimeError> = None;
            for proof_stmt in stmt.proof.iter() {
                let exec_stmt_result = rt.exec_stmt(proof_stmt);
                match exec_stmt_result {
                    Ok(result) => inside_results.push(result),
                    Err(statement_error) => {
                        last_error = Some(statement_error);
                        break;
                    }
                }
            }

            if last_error.is_some() {
                return Ok((inside_results, last_error));
            }

            let verify_impossible_fact_result =
                rt.verify_atomic_fact(&stmt.impossible_fact, &VerifyState::new(0, false))?;
            if verify_impossible_fact_result.is_unknown() {
                return Err(short_exec_error(
 stmt.clone().into(),
                    impossible_proof_error_message(&stmt.impossible_fact, None),
                    None,
                    inside_results,
                ));
            }

            let verify_reversed_impossible_fact_result = rt.verify_atomic_fact(
                &stmt.impossible_fact.make_reversed(),
                &VerifyState::new(0, false),
            )?;
            if verify_reversed_impossible_fact_result.is_unknown() {
                return Err(short_exec_error(
 stmt.clone().into(),
                    impossible_proof_error_message(&stmt.impossible_fact, None),
                    None,
                    vec![],
                ));
            }

            Ok((inside_results, last_error))
        })?;

        if let Some(last_error) = last_error {
            return Err(short_exec_error(
 stmt.clone().into(),
                    "by contra: failed to execute proof".to_string(),
                    Some(last_error),
                    exec_proof_inside_results,
                ));
        }

        let to_prove_fact_display_string = to_prove_fact.to_string();
        let infer_result = self
            .store_fact_without_well_defined_verified_and_infer(to_prove_fact)
            .map_err(|store_fact_error| {
                short_exec_error(
 stmt.clone().into(),
                    format!(
                        "by contra: failed to release `{}`",
                        to_prove_fact_display_string
                    ),
                    Some(store_fact_error),
                    vec![],
                )
            })?;

        Ok((NonFactualStmtSuccess::new(
            stmt.clone().into(),
            infer_result,
            exec_proof_inside_results,
        ))
        .into())
    }
}