litex/execute/by_stmt/
transitive_prop_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_by_transitive_prop_stmt(
5        &mut self,
6        stmt: &ByTransitivePropStmt,
7    ) -> Result<StmtResult, RuntimeError> {
8        let prop_name = stmt.transitive_prop_name().map_err(|msg| {
9            RuntimeError::from(VerifyRuntimeError(
10                RuntimeErrorStruct::new_with_msg_and_line_file(msg, stmt.line_file.clone()),
11            ))
12        })?;
13
14        let prop_definition = self.get_abstract_prop_definition_by_name(&prop_name);
15        match prop_definition {
16            Some(definition) => {
17                if definition.params.len() != 2 {
18                    return Err(short_exec_error(
19                        stmt.clone().into(),
20                        format!(
21                            "by transitive_prop: `{}` must be a binary abstract_prop",
22                            prop_name
23                        ),
24                        None,
25                        vec![],
26                    ));
27                }
28            }
29            None => {
30                return Err(short_exec_error(
31                    stmt.clone().into(),
32                    format!(
33                        "by transitive_prop: `{}` must be an abstract_prop",
34                        prop_name
35                    ),
36                    None,
37                    vec![],
38                ));
39            }
40        }
41
42        let inside_results = self.run_in_local_env(|rt| {
43            let verify_state = VerifyState::new(0, false);
44            let mut infer_result =
45                rt.forall_assume_params_and_dom_in_current_env(&stmt.forall_fact, &verify_state)?;
46            let mut inside_results: Vec<StmtResult> = Vec::new();
47            for proof_stmt in stmt.proof.iter() {
48                inside_results.push(rt.exec_stmt(proof_stmt)?);
49            }
50            let result = rt.forall_verify_then_facts_in_current_env(
51                &stmt.forall_fact,
52                &verify_state,
53                &mut infer_result,
54                None,
55            )?;
56            if result.is_unknown() {
57                return Err(short_exec_error(
58                    stmt.clone().into(),
59                    format!("by transitive_prop: failed to prove `{}`", stmt.forall_fact),
60                    None,
61                    inside_results,
62                ));
63            }
64            inside_results.push(result);
65            Ok(inside_results)
66        })?;
67
68        self.top_level_env()
69            .store_transitive_prop_name(prop_name.clone());
70
71        let mut infer_result = InferResult::new();
72        infer_result.new_with_msg(format!("registered `{}` as transitive", prop_name));
73        Ok(NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, inside_results).into())
74    }
75}
litex/execute/by_stmt/transitive_prop_by_stmt.rs

litex/execute/by_stmt/
transitive_prop_by_stmt.rs
