litex/parse/
parse_witness.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn parse_witness_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
5        tb.skip_token(WITNESS)?;
6        if tb.current_token_is_equal_to(EXIST) {
7            self.parse_witness_exist_fact(tb)
8        } else if tb.current_token_is_equal_to(FACT_PREFIX) {
9            self.parse_witness_nonempty_set(tb)
10        } else {
11            return Err(RuntimeError::from(ParseRuntimeError(
12                RuntimeErrorStruct::new_with_msg_and_line_file(
13                    "witness expects a exist or nonempty set".to_string(),
14                    tb.line_file.clone(),
15                ),
16            )));
17        }
18    }
19
20    // witness exist x, y R st {x > y} from 1, 0:
21    // Or omit ':' and proof: witness exist ... from 1, 0
22    pub fn parse_witness_exist_fact(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
23        let exist_fact_in_witness = self.parse_exist_fact(tb)?;
24        tb.skip_token(FROM)?;
25        let equal_tos = self.parse_obj_list(tb)?;
26        let proof = if tb.exceed_end_of_head() {
27            if !tb.body.is_empty() {
28                return Err(RuntimeError::from(ParseRuntimeError(
29                    RuntimeErrorStruct::new_with_msg_and_line_file(
30                        "witness exist: indented proof body requires ':' at end of header line"
31                            .to_string(),
32                        tb.line_file.clone(),
33                    ),
34                )));
35            }
36            Vec::new()
37        } else {
38            tb.skip_token(COLON)?;
39            if !tb.exceed_end_of_head() {
40                return Err(RuntimeError::from(ParseRuntimeError(
41                    RuntimeErrorStruct::new_with_msg_and_line_file(
42                        "witness exist: unexpected tokens after ':' in header".to_string(),
43                        tb.line_file.clone(),
44                    ),
45                )));
46            }
47            let names = exist_fact_in_witness
48                .params_def_with_type()
49                .collect_param_names();
50            let lf = tb.line_file.clone();
51            self.parse_stmts_with_optional_free_param_scope(
52                ParamObjType::Exist,
53                &names,
54                lf,
55                |this| {
56                    tb.body
57                        .iter_mut()
58                        .map(|b| this.parse_stmt(b))
59                        .collect::<Result<_, _>>()
60                },
61            )?
62        };
63        Ok(WitnessExistFact::new(
64            equal_tos,
65            exist_fact_in_witness,
66            proof,
67            tb.line_file.clone(),
68        )
69        .into())
70    }
71
72    // witness $is_nonempty_set(R) from 1:
73    pub fn parse_witness_nonempty_set(
74        &mut self,
75        tb: &mut TokenBlock,
76    ) -> Result<Stmt, RuntimeError> {
77        tb.skip_token(FACT_PREFIX)?;
78        tb.skip_token(IS_NONEMPTY_SET)?;
79        tb.skip_token(LEFT_BRACE)?;
80        let set = self.parse_obj(tb)?;
81        tb.skip_token(RIGHT_BRACE)?;
82        tb.skip_token(FROM)?;
83        let obj = self.parse_obj(tb)?;
84
85        let mut proof = Vec::with_capacity(tb.body.len());
86        for block in tb.body.iter_mut() {
87            proof.push(self.parse_stmt(block)?);
88        }
89        Ok(WitnessNonemptySet::new(obj, set, proof, tb.line_file.clone()).into())
90    }
91}
litex/parse/parse_witness.rs

litex/parse/
parse_witness.rs
