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

use crate::prelude::*;

impl Runtime {
    pub fn parse_claim_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError> {
        tb.skip_token(CLAIM)?;
        Ok(self.parse_multiline_fact_claim(tb)?.into())
    }

    fn parse_multiline_fact_claim(
        &mut self,
        tb: &mut TokenBlock,
    ) -> Result<ClaimStmt, RuntimeError> {
        tb.skip_token(COLON)?;
        if tb.body.is_empty() {
            return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                "claim : expects at least one body block (=>: fact)".to_string(),
                tb.line_file.clone(),
                None,
            ));
        }
        let fact = {
            let first = tb.body.get_mut(0).ok_or_else(|| {
                RuntimeError::new_parse_error_with_msg_position_previous_error(
                    "claim : expects at least one body block (=>: fact)".to_string(),
                    tb.line_file.clone(),
                    None,
                )
            })?;

            first.skip_token(PROVE)?;
            first.skip_token(COLON)?;

            let body_block = first.body.get_mut(0).ok_or_else(|| {
                RuntimeError::new_parse_error_with_msg_position_previous_error(
                    "claim =>: expects exactly one body block (the fact)".to_string(),
                    first.line_file.clone(),
                    None,
                )
            })?;
            let f = self.parse_fact(body_block)?;
            if matches!(&f, Fact::ForallFactWithIff(_)) {
                return Err(RuntimeError::new_parse_error_with_msg_position_previous_error(
                    "claim multiline fact cannot be iff".to_string(),
                    first.line_file.clone(),
                    None,
                ));
            }
            Ok::<Fact, RuntimeError>(f)
        }?;

        let proof: Vec<Stmt> = tb
            .body
            .iter_mut()
            .skip(1)
            .map(|b| self.parse_stmt(b))
            .collect::<Result<_, _>>()?;
        Ok(ClaimStmt::new(fact, proof, tb.line_file.clone()))
    }
}