litex/execute/
exec_claim_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_claim_stmt(&mut self, stmt: &ClaimStmt) -> Result<StmtResult, RuntimeError> {
5        match &stmt.fact {
6            Fact::ForallFactWithIff(_) => unreachable!("claim forall with iff is not supported"),
7            Fact::ForallFact(forall_fact) => {
8                self.verify_fact_well_defined(&stmt.fact, &VerifyState::new(0, false))
9                    .map_err(|e| {
10                        short_exec_error(
11                            stmt.clone().into(),
12                            "claim: fact is not well defined".to_string(),
13                            Some(e),
14                            vec![],
15                        )
16                    })?;
17
18                let body_exec_result = self.run_in_local_env(|rt| {
19                    rt.define_params_with_type(
20                        &forall_fact.params_def_with_type,
21                        false,
22                        ParamObjType::Forall,
23                    )
24                        .map_err(|define_params_error| {
25                            exec_stmt_error_with_stmt_and_cause(
26                                stmt.clone().into(),
27                                define_params_error,
28                            )
29                        })?;
30
31                    for dom_fact in forall_fact.dom_facts.iter() {
32                        rt.verify_well_defined_and_store_and_infer_with_default_verify_state(dom_fact.clone())?;
33                    }
34
35                    let mut inside_results = vec![];
36                    let proof_len = stmt.proof.len();
37                    for (proof_index, proof_stmt) in stmt.proof.iter().enumerate() {
38                        let result = rt.exec_stmt(proof_stmt)?;
39                        if result.is_unknown() {
40                            return Err(
41                                UnknownRuntimeError(RuntimeErrorStruct::new(
42                                    Some(proof_stmt.clone()),
43                                    format!(
44                                        "claim failed: proof step {}/{} is unknown: `{}`\n{}",
45                                        proof_index + 1,
46                                        proof_len,
47                                        proof_stmt,
48                                        result.body_string()
49                                    ),
50                                    proof_stmt.line_file(),
51                                    None,
52                                    vec![],
53                                ))
54                                .into(),
55                            );
56                        }
57                        inside_results.push(result);
58                    }
59
60                    let then_count = forall_fact.then_facts.len();
61                    for (then_index, then_fact) in forall_fact.then_facts.iter().enumerate() {
62                        let result = rt.verify_exist_or_and_chain_atomic_fact(
63                            then_fact,
64                            &VerifyState::new(0, false),
65                        )?;
66                        if result.is_unknown() {
67                            return Err(
68                                UnknownRuntimeError(RuntimeErrorStruct::new(
69                                    Some(Stmt::Fact(then_fact.clone().to_fact())),
70                                    format!(
71                                        "claim failed: cannot prove goal `{}`; then-clause {}/{} `{}` is unknown\n{}",
72                                        stmt.fact,
73                                        then_index + 1,
74                                        then_count,
75                                        then_fact,
76                                        result.body_string()
77                                    ),
78                                    then_fact.line_file(),
79                                    None,
80                                    vec![],
81                                ))
82                                .into(),
83                            );
84                        }
85
86                        inside_results.push(result);
87                    }
88
89                    Ok(NonFactualStmtSuccess::new(
90                            stmt.clone().into(),
91                            InferResult::new(),
92                            inside_results,
93                        )
94                        .into())
95                });
96
97                let non_err_after_body: StmtResult = match body_exec_result {
98                    Ok(non_err_stmt_exec_result) => non_err_stmt_exec_result,
99                    Err(runtime_error) => return Err(runtime_error),
100                };
101                if non_err_after_body.is_unknown() {
102                    return Err(UnknownRuntimeError(RuntimeErrorStruct::new(
103                        Some(stmt.clone().into()),
104                        format!(
105                            "claim failed: cannot prove `{}`\n{}",
106                            stmt.fact,
107                            non_err_after_body.body_string()
108                        ),
109                        stmt.line_file.clone(),
110                        None,
111                        vec![],
112                    ))
113                    .into());
114                }
115
116                let infer_result_after_store = self
117                    .verify_well_defined_and_store_and_infer_with_default_verify_state(
118                        stmt.fact.clone(),
119                    )?;
120
121                let mut result = non_err_after_body;
122                if let StmtResult::NonFactualStmtSuccess(ref mut nfs) = result {
123                    nfs.inside_results.clear();
124                }
125                Ok(result.with_infers(infer_result_after_store))
126            }
127            _ => {
128                self.verify_fact_well_defined(&stmt.fact, &VerifyState::new(0, false))
129                    .map_err(|e| {
130                        short_exec_error(
131                            stmt.clone().into(),
132                            "claim: fact is not well defined".to_string(),
133                            Some(e),
134                            vec![],
135                        )
136                    })?;
137
138                let body_exec_result = self.run_in_local_env(|rt| {
139                    let mut inside_results: Vec<StmtResult> = Vec::new();
140                    for proof_stmt in stmt.proof.iter() {
141                        let proof_exec_result = rt.exec_stmt(proof_stmt)?;
142                        inside_results.push(proof_exec_result);
143                    }
144
145                    rt.verify_fact_return_err_if_not_true(&stmt.fact, &VerifyState::new(0, false))?;
146
147                    Ok(NonFactualStmtSuccess::new(
148                        stmt.clone().into(),
149                        InferResult::new(),
150                        inside_results,
151                    )
152                    .into())
153                });
154
155                let non_err_after_body: StmtResult = match body_exec_result {
156                    Ok(non_err_stmt_exec_result) => non_err_stmt_exec_result,
157                    Err(runtime_error) => return Err(runtime_error),
158                };
159                let infer_result_after_store = self
160                    .verify_well_defined_and_store_and_infer_with_default_verify_state(
161                        stmt.fact.clone(),
162                    )?;
163
164                Ok(non_err_after_body.with_infers(infer_result_after_store))
165            }
166        }
167    }
168}
litex/execute/exec_claim_stmt.rs

litex/execute/
exec_claim_stmt.rs
