litex-lang 0.9.68-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

use crate::prelude::*;

impl Runtime {
    pub fn verify_obj_satisfies_family(
        &mut self,
        obj: Obj,
        family_ty: &FamilyObj,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        let family_name = family_ty.name.to_string();
        let def = match self.get_cloned_family_definition_by_name(&family_name) {
            Some(d) => d,
            None => {
                return Err(
                    VerifyRuntimeError(RuntimeErrorStruct::new(
                None,
                format!("family `{}` is not defined", family_name),
                default_line_file(),
                None,
                vec![],
            ))
            .into(),
                );
            }
        };
        let expected_count = def.params_def_with_type.number_of_params();
        if family_ty.params.len() != expected_count {
            return Err(
                VerifyRuntimeError(RuntimeErrorStruct::new(
                None,
                format!(
                        "family `{}` expects {} type argument(s), got {}",
                        family_name,
                        expected_count,
                        family_ty.params.len()
                    ),
                default_line_file(),
                None,
                vec![],
            ))
            .into(),
            );
        }
        let param_to_arg_map = def
            .params_def_with_type
            .param_defs_and_args_to_param_to_arg_map(family_ty.params.as_slice());
        let member_set = self.inst_obj(&def.equal_to, &param_to_arg_map, ParamObjType::DefHeader)?;
        let fact = InFact::new(obj, member_set, default_line_file()).into();
        self.verify_atomic_fact(&fact, verify_state)
    }
}