litex/verify/
verify_fn_equal_in_builtin.rs

1use crate::execute::exec_have_fn_equal_shared::{
2    build_curried_fn_value_apply_for_fn_eq, fn_set_to_fn_set_clause,
3    forall_binders_dom_and_curried_layers_from_fn_set_clause,
4};
5use crate::prelude::*;
6
7// Build f(x) as FnObj for a name or anonymous function.
8fn fn_obj_apply_one_arg(func: &Obj, arg: Obj) -> Option<Obj> {
9    match func {
10        Obj::AnonymousFn(af) => Some(
11            FnObj::new(
12                FnObjHead::AnonymousFnLiteral(Box::new(af.clone())),
13                vec![vec![Box::new(arg)]],
14            )
15            .into(),
16        ),
17        o => {
18            let h = FnObjHead::given_an_atom_return_a_fn_obj_head(o.clone())?;
19            Some(FnObj::new(h, vec![vec![Box::new(arg)]]).into())
20        }
21    }
22}
23
24impl Runtime {
25    // $fn_eq_in(f,g,S): forall x in S, f(x)=g(x); verified as a ForallFact in a local env.
26    pub fn verify_fn_equal_in_fact_with_builtin_rules(
27        &mut self,
28        f: &FnEqualInFact,
29        verify_state: &VerifyState,
30    ) -> Result<StmtResult, RuntimeError> {
31        let x_name = self.generate_random_unused_names(1)[0].clone();
32        // Use the same `Obj` shape as `define_params_with_type(..., Forall, ...)` and as parsed
33        // `forall` parameters, so `verify_equal` can match `f(x) = g(x)` from stored `forall` facts.
34        let x: Obj = param_binding_element_obj_for_store(x_name.clone(), ParamObjType::Forall);
35        let Some(left_ap) = fn_obj_apply_one_arg(&f.left, x.clone()) else {
36            return Ok(StmtUnknown::new().into());
37        };
38        let Some(right_ap) = fn_obj_apply_one_arg(&f.right, x) else {
39            return Ok(StmtUnknown::new().into());
40        };
41        let param_def = ParamDefWithType::new(vec![ParamGroupWithParamType::new(
42            vec![x_name],
43            ParamType::Obj(f.set.clone()),
44        )]);
45        let forall_f = ForallFact::new(
46            param_def,
47            vec![],
48            vec![EqualFact::new(left_ap, right_ap, f.line_file.clone()).into()],
49            f.line_file.clone(),
50        )?;
51        let forall_res = self.verify_forall_fact(&forall_f, verify_state)?;
52        if !forall_res.is_true() {
53            return Ok(forall_res);
54        }
55        let recorded: Fact = f.clone().into();
56        Ok(
57            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
58                recorded,
59                "fn_eq_in: pointwise equality on the given set (forall x in S, f(x)=g(x))"
60                    .to_string(),
61                vec![forall_res],
62            )
63            .into(),
64        )
65    }
66
67    // $fn_eq(f,g): mutual $in, then Forall with params+dom from FnSet and then f(..)=g(..). Name `f(x)` uses
68    // Forall binders in the curried apply (see exec_have_fn_equal_shared) so it cites user foralls.
69    pub fn verify_fn_equal_fact_with_builtin_rules(
70        &mut self,
71        f: &FnEqualFact,
72        verify_state: &VerifyState,
73    ) -> Result<StmtResult, RuntimeError> {
74        let left_t = match fn_set_type_of_function_value(self, &f.left) {
75            Some(fs) => fs,
76            None => return Ok(StmtUnknown::new().into()),
77        };
78        let right_t = match fn_set_type_of_function_value(self, &f.right) {
79            Some(fs) => fs,
80            None => return Ok(StmtUnknown::new().into()),
81        };
82
83        let in_left: AtomicFact = InFact::new(
84            f.left.clone(),
85            Obj::FnSet(right_t.clone()),
86            f.line_file.clone(),
87        )
88        .into();
89        if !self.verify_atomic_fact(&in_left, verify_state)?.is_true() {
90            return Ok(StmtUnknown::new().into());
91        }
92        let in_right: AtomicFact = InFact::new(
93            f.right.clone(),
94            Obj::FnSet(left_t.clone()),
95            f.line_file.clone(),
96        )
97        .into();
98        if !self.verify_atomic_fact(&in_right, verify_state)?.is_true() {
99            return Ok(StmtUnknown::new().into());
100        }
101
102        let clause = fn_set_to_fn_set_clause(&left_t);
103        let (param_def, dom_facts, layers) =
104            forall_binders_dom_and_curried_layers_from_fn_set_clause(&clause);
105        let left_ap = match build_curried_fn_value_apply_for_fn_eq(&f.left, &layers) {
106            Some(o) => o,
107            None => return Ok(StmtUnknown::new().into()),
108        };
109        let right_ap = match build_curried_fn_value_apply_for_fn_eq(&f.right, &layers) {
110            Some(o) => o,
111            None => return Ok(StmtUnknown::new().into()),
112        };
113        let forall_f = ForallFact::new(
114            param_def,
115            dom_facts,
116            vec![EqualFact::new(left_ap, right_ap, f.line_file.clone()).into()],
117            f.line_file.clone(),
118        )?;
119        let forall_res = self.verify_forall_fact(&forall_f, verify_state)?;
120        if !forall_res.is_true() {
121            return Ok(forall_res);
122        }
123        let recorded: Fact = f.clone().into();
124        Ok(
125            FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
126                recorded,
127                "fn_eq: mutual function-space membership and pointwise equality (forall+dom)"
128                    .to_string(),
129                vec![forall_res],
130            )
131            .into(),
132        )
133    }
134}
135
136// FnSet “type” for an anonymous fn, a bare FnSet obj, or a name in known_objs_in_fn_sets.
137fn fn_set_type_of_function_value(rt: &Runtime, obj: &Obj) -> Option<FnSet> {
138    match obj {
139        Obj::AnonymousFn(af) => FnSet::new(
140            af.body.params_def_with_set.clone(),
141            af.body.dom_facts.clone(),
142            (*af.body.ret_set).clone(),
143        )
144        .ok(),
145        Obj::FnSet(fs) => Some(fs.clone()),
146        o => rt
147            .get_cloned_object_in_fn_set(o)
148            .and_then(|body| FnSet::from_body(body).ok()),
149    }
150}
litex/verify/verify_fn_equal_in_builtin.rs

litex/verify/
verify_fn_equal_in_builtin.rs
