litex-lang 0.9.6-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

use crate::prelude::*;

impl Runtime {
    pub fn parse_by_for_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
        tb.skip_token(FOR)?;
        tb.skip_token(COLON)?;
        if !tb.exceed_end_of_head() {
            return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: expected `:` immediately after `for`".to_string(),
                tb.line_file.clone(),
                None,
            ));
        }
        if tb.body.is_empty() {
            return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: expects a body".to_string(),
                tb.line_file.clone(),
                None,
            ));
        }

        let prove_block = tb.body.get_mut(0).ok_or_else(|| {
            RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: expected prove block".to_string(),
                tb.line_file.clone(),
                None,
            )
        })?;
        if prove_block.header.get(0).map(|s| s.as_str()) != Some(PROVE) {
            return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: first block must be `prove:`".to_string(),
                prove_block.line_file.clone(),
                None,
            ));
        }
        prove_block.skip_token_and_colon_and_exceed_end_of_head(PROVE)?;
        if prove_block.body.len() != 1 {
            return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: `prove:` must contain exactly one forall fact".to_string(),
                prove_block.line_file.clone(),
                None,
            ));
        }

        let forall_block = prove_block.body.get_mut(0).ok_or_else(|| {
            RuntimeError::new_parse_error_with_msg_position_previous_error(
                "by for: missing forall block".to_string(),
                tb.line_file.clone(),
                None,
            )
        })?;
        let fact = self.parse_fact(forall_block)?;
        let forall_fact = match fact {
            Fact::ForallFact(ff) => ff,
            Fact::ForallFactWithIff(_) => {
                return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                    "by for: forall with `<=>` is not allowed here".to_string(),
                    forall_block.line_file.clone(),
                    None,
                ));
            }
            _ => {
                return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                    "by for: `prove:` must be a single `forall` fact".to_string(),
                    forall_block.line_file.clone(),
                    None,
                ));
            }
        };

        for g in forall_fact.params_def_with_type.iter() {
            match &g.param_type {
                ParamType::Obj(Obj::Range(_)) | ParamType::Obj(Obj::ClosedRange(_)) => {}
                _ => {
                    return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                        "by for: each forall parameter type must be range or closed_range"
                            .to_string(),
                        forall_fact.line_file.clone(),
                        None,
                    ));
                }
            }
        }

        let mut proof: Vec<Stmt> = Vec::new();
        for b in tb.body.iter_mut().skip(1) {
            proof.push(self.parse_stmt(b)?);
        }

        Ok(ByForStmt::new(forall_fact, proof, tb.line_file.clone()).into())
    }
}