litex/parse/
parse_claim_stmt.rs

1use crate::parse::parse_helpers::collect_forall_param_names_from_facts;
2use crate::prelude::*;
3
4impl Runtime {
5    pub fn parse_claim_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
6        tb.skip_token(CLAIM)?;
7        if tb.current()? == COLON {
8            Ok(self.parse_multiline_fact_claim(tb)?.into())
9        } else {
10            let fact = self.parse_header_fact_before_trailing_colon(
11                tb,
12                "claim",
13                "claim => <fact>:",
14                "claim <fact>:",
15            )?;
16            if matches!(&fact, Fact::ForallFactWithIff(_)) {
17                return Err(RuntimeError::from(ParseRuntimeError(
18                    RuntimeErrorStruct::new_with_msg_and_line_file(
19                        "claim multiline fact cannot be iff".to_string(),
20                        tb.line_file.clone(),
21                    ),
22                )));
23            }
24            let names = collect_forall_param_names_from_facts(std::slice::from_ref(&fact));
25            let lf = tb.line_file.clone();
26            let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
27                ParamObjType::Forall,
28                &names,
29                lf,
30                |this| {
31                    tb.body
32                        .iter_mut()
33                        .map(|b| this.parse_stmt(b))
34                        .collect::<Result<_, _>>()
35                },
36            )?;
37            Ok(ClaimStmt::new(fact, proof, tb.line_file.clone()).into())
38        }
39    }
40
41    fn parse_multiline_fact_claim(
42        &mut self,
43        tb: &mut TokenBlock,
44    ) -> Result<ClaimStmt, RuntimeError> {
45        tb.skip_token(COLON)?;
46        if tb.body.is_empty() {
47            return Err(RuntimeError::from(ParseRuntimeError(
48                RuntimeErrorStruct::new_with_msg_and_line_file(
49                    "claim: expects a `prove:` block and optional proof body".to_string(),
50                    tb.line_file.clone(),
51                ),
52            )));
53        }
54        let fact = {
55            let first = tb.body.get_mut(0).ok_or_else(|| {
56                RuntimeError::from(ParseRuntimeError(
57                    RuntimeErrorStruct::new_with_msg_and_line_file(
58                        "claim: expects a `prove:` block and optional proof body".to_string(),
59                        tb.line_file.clone(),
60                    ),
61                ))
62            })?;
63
64            first.skip_token(PROVE)?;
65            first.skip_token(COLON)?;
66
67            let body_block = first.body.get_mut(0).ok_or_else(|| {
68                RuntimeError::from(ParseRuntimeError(
69                    RuntimeErrorStruct::new_with_msg_and_line_file(
70                        "claim: `prove:` expects exactly one body block (the fact)".to_string(),
71                        first.line_file.clone(),
72                    ),
73                ))
74            })?;
75            let f = self.parse_fact(body_block)?;
76            if matches!(&f, Fact::ForallFactWithIff(_)) {
77                return Err(RuntimeError::from(ParseRuntimeError(
78                    RuntimeErrorStruct::new_with_msg_and_line_file(
79                        "claim multiline fact cannot be iff".to_string(),
80                        first.line_file.clone(),
81                    ),
82                )));
83            }
84            Ok::<Fact, RuntimeError>(f)
85        }?;
86
87        let names = collect_forall_param_names_from_facts(std::slice::from_ref(&fact));
88        let lf = tb.line_file.clone();
89        let proof: Vec<Stmt> = self.parse_stmts_with_optional_free_param_scope(
90            ParamObjType::Forall,
91            &names,
92            lf,
93            |this| {
94                tb.body
95                    .iter_mut()
96                    .skip(1)
97                    .map(|b| this.parse_stmt(b))
98                    .collect::<Result<_, _>>()
99            },
100        )?;
101        Ok(ClaimStmt::new(fact, proof, tb.line_file.clone()))
102    }
103}
litex/parse/parse_claim_stmt.rs

litex/parse/
parse_claim_stmt.rs
