litex/execute/by_stmt/
contra_by_stmt.rs

1use super::helpers_by_stmt::impossible_proof_error_message;
2use crate::prelude::*;
3
4impl Runtime {
5    pub fn exec_by_contra_stmt(&mut self, stmt: &ByContraStmt) -> Result<StmtResult, RuntimeError> {
6        let to_prove_fact: Fact = stmt.to_prove.clone().into();
7        self.verify_fact_well_defined(&to_prove_fact, &VerifyState::new(0, false))
8            .map_err(|verify_error| {
9                short_exec_error(
10                    stmt.clone().into(),
11                    format!("by contra: failed to prove `{}`", to_prove_fact),
12                    Some(verify_error),
13                    vec![],
14                )
15            })?;
16
17        let (exec_proof_inside_results, last_error) = self.run_in_local_env(|rt| {
18            let mut inside_results: Vec<StmtResult> = Vec::new();
19
20            let reverse_to_prove_fact = stmt.to_prove.make_reversed();
21            rt.store_atomic_fact_without_well_defined_verified_and_infer(reverse_to_prove_fact)
22                .map_err(|store_fact_error| {
23                    short_exec_error(
24                        stmt.clone().into(),
25                        format!("by contra: failed to know reverse of `{}`", to_prove_fact),
26                        Some(store_fact_error),
27                        vec![],
28                    )
29                })?;
30
31            let mut last_error: Option<RuntimeError> = None;
32            for proof_stmt in stmt.proof.iter() {
33                let exec_stmt_result = rt.exec_stmt(proof_stmt);
34                match exec_stmt_result {
35                    Ok(result) => inside_results.push(result),
36                    Err(statement_error) => {
37                        last_error = Some(statement_error);
38                        break;
39                    }
40                }
41            }
42
43            if last_error.is_some() {
44                return Ok((inside_results, last_error));
45            }
46
47            let verify_impossible_fact_result =
48                rt.verify_atomic_fact(&stmt.impossible_fact, &VerifyState::new(0, false))?;
49            if verify_impossible_fact_result.is_unknown() {
50                return Err(short_exec_error(
51                    stmt.clone().into(),
52                    impossible_proof_error_message(&stmt.impossible_fact, None),
53                    None,
54                    inside_results,
55                ));
56            }
57
58            let verify_reversed_impossible_fact_result = rt.verify_atomic_fact(
59                &stmt.impossible_fact.make_reversed(),
60                &VerifyState::new(0, false),
61            )?;
62            if verify_reversed_impossible_fact_result.is_unknown() {
63                return Err(short_exec_error(
64                    stmt.clone().into(),
65                    impossible_proof_error_message(&stmt.impossible_fact, None),
66                    None,
67                    vec![],
68                ));
69            }
70
71            Ok((inside_results, last_error))
72        })?;
73
74        if let Some(last_error) = last_error {
75            return Err(short_exec_error(
76                stmt.clone().into(),
77                "by contra: failed to execute proof".to_string(),
78                Some(last_error),
79                exec_proof_inside_results,
80            ));
81        }
82
83        let to_prove_fact_display_string = to_prove_fact.to_string();
84        let infer_result = self
85            .verify_well_defined_and_store_and_infer_with_default_verify_state(to_prove_fact)
86            .map_err(|store_fact_error| {
87                short_exec_error(
88                    stmt.clone().into(),
89                    format!(
90                        "by contra: failed to release `{}`",
91                        to_prove_fact_display_string
92                    ),
93                    Some(store_fact_error),
94                    vec![],
95                )
96            })?;
97
98        Ok((NonFactualStmtSuccess::new(
99            stmt.clone().into(),
100            infer_result,
101            exec_proof_inside_results,
102        ))
103        .into())
104    }
105}
litex/execute/by_stmt/contra_by_stmt.rs

litex/execute/by_stmt/
contra_by_stmt.rs
