litex/verify/
verify_arg_satisfy_param_def.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_obj_satisfies_param_type(
5        &mut self,
6        obj: Obj,
7        param_type: &ParamType,
8        verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        match param_type {
11            ParamType::Obj(set_obj) => {
12                let fact = InFact::new(obj, set_obj.clone(), default_line_file()).into();
13                self.verify_atomic_fact(&fact, verify_state)
14            }
15            ParamType::Set(_) => {
16                let fact = IsSetFact::new(obj, default_line_file()).into();
17                self.verify_atomic_fact(&fact, verify_state)
18            }
19            ParamType::NonemptySet(_) => {
20                let fact = IsNonemptySetFact::new(obj, default_line_file()).into();
21                self.verify_atomic_fact(&fact, verify_state)
22            }
23            ParamType::FiniteSet(_) => {
24                let fact = IsFiniteSetFact::new(obj, default_line_file()).into();
25                self.verify_atomic_fact(&fact, verify_state)
26            }
27            ParamType::Restrictive(fs) => {
28                let restrict_fact =
29                    RestrictFact::new(obj.clone(), fs.clone().into(), default_line_file()).into();
30                let restrict_res = self.verify_atomic_fact(&restrict_fact, verify_state)?;
31                if restrict_res.is_true() {
32                    return Ok(restrict_res);
33                }
34                // `restrictive (fn …)` is `$restrict_fn_in` shape. Proving the definition often
35                // repeats a `forall` that membership `f $in fn …` already encodes when the type is
36                // exactly this function space; the dedicated proof may still return unknown.
37                let membership = InFact::new(obj, fs.clone().into(), default_line_file()).into();
38                self.verify_atomic_fact(&membership, verify_state)
39            }
40        }
41    }
42
43    pub fn verify_args_satisfy_param_def_flat_types(
44        &mut self,
45        param_defs: &ParamDefWithType,
46        args: &Vec<Obj>,
47        verify_state: &VerifyState,
48        to_inst_param_type: ParamObjType,
49    ) -> Result<StmtResult, RuntimeError> {
50        let instantiated_types =
51            self.inst_param_def_with_type_one_by_one(param_defs, args, to_inst_param_type)?;
52        let flat_types = param_defs.flat_instantiated_types_for_args(&instantiated_types);
53        let mut infer_result = InferResult::new();
54        for (arg, param_type) in args.iter().zip(flat_types.iter()) {
55            let verify_result =
56                self.verify_obj_satisfies_param_type(arg.clone(), param_type, verify_state)?;
57            if verify_result.is_unknown() {
58                return Ok(verify_result);
59            }
60            match verify_result {
61                StmtResult::NonFactualStmtSuccess(x) => {
62                    infer_result.new_infer_result_inside(x.infers);
63                }
64                StmtResult::FactualStmtSuccess(x) => {
65                    infer_result.new_infer_result_inside(x.infers);
66                }
67                StmtResult::StmtUnknown(_) => unreachable!(),
68            }
69        }
70        Ok(NonFactualStmtSuccess::new(
71            DoNothingStmt::new(default_line_file()).into(),
72            infer_result,
73            Vec::new(),
74        )
75        .into())
76    }
77}
litex/verify/verify_arg_satisfy_param_def.rs

litex/verify/
verify_arg_satisfy_param_def.rs
