litex/execute/by_stmt/
commutative_prop_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_by_commutative_prop_stmt(
5        &mut self,
6        stmt: &ByCommutativePropStmt,
7    ) -> Result<StmtResult, RuntimeError> {
8        let (prop_name, gather) = stmt.commutative_prop_registration().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 forall_arity = stmt
15            .forall_fact
16            .params_def_with_type
17            .collect_param_names()
18            .len();
19        let prop_definition = self.get_abstract_prop_definition_by_name(&prop_name);
20        match prop_definition {
21            Some(definition) => {
22                if definition.params.len() != forall_arity {
23                    return Err(short_exec_error(
24                        stmt.clone().into(),
25                        format!(
26                            "by commutative_prop: `{}` must have arity {} to match the forall",
27                            prop_name, forall_arity
28                        ),
29                        None,
30                        vec![],
31                    ));
32                }
33            }
34            None => {
35                return Err(short_exec_error(
36                    stmt.clone().into(),
37                    format!(
38                        "by commutative_prop: `{}` must be an abstract_prop",
39                        prop_name
40                    ),
41                    None,
42                    vec![],
43                ));
44            }
45        }
46
47        let inside_results = self.run_in_local_env(|rt| {
48            let verify_state = VerifyState::new(0, false);
49            let mut infer_result =
50                rt.forall_assume_params_and_dom_in_current_env(&stmt.forall_fact, &verify_state)?;
51            let mut inside_results: Vec<StmtResult> = Vec::new();
52            for proof_stmt in stmt.proof.iter() {
53                inside_results.push(rt.exec_stmt(proof_stmt)?);
54            }
55            let result = rt.forall_verify_then_facts_in_current_env(
56                &stmt.forall_fact,
57                &verify_state,
58                &mut infer_result,
59                None,
60            )?;
61            if result.is_unknown() {
62                return Err(short_exec_error(
63                    stmt.clone().into(),
64                    format!(
65                        "by commutative_prop: failed to prove `{}`",
66                        stmt.forall_fact
67                    ),
68                    None,
69                    inside_results,
70                ));
71            }
72            inside_results.push(result);
73            Ok(inside_results)
74        })?;
75
76        self.top_level_env().store_commutative_prop_permutation(
77            prop_name.clone(),
78            gather.clone(),
79            stmt.line_file.clone(),
80        )?;
81
82        let mut infer_result = InferResult::new();
83        infer_result.new_with_msg(format!(
84            "registered commutative permutation {:?} for `{}`",
85            gather, prop_name
86        ));
87        Ok(NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, inside_results).into())
88    }
89}
litex/execute/by_stmt/commutative_prop_by_stmt.rs

litex/execute/by_stmt/
commutative_prop_by_stmt.rs
