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

litex/execute/
exec_claim_stmt.rs
