ovmi/predicates/
there_exists.rs

1use crate::executor::*;
2use crate::predicates::*;
3
4pub struct ThereExistsPredicate<'a, Ext: ExternalCall> {
5    pub ext: &'a Ext,
6}
7
8impl<'a, Ext: ExternalCall> ThereExistsPredicate<'a, Ext> {
9    /// @dev Replace placeholder by quantified in propertyBytes
10    fn replace_variable(
11        &self,
12        property_bytes: &Vec<u8>,
13        placeholder: &Vec<u8>,
14        quantified: &Vec<u8>,
15    ) -> ExecResultT<Vec<u8>, AddressOf<Ext>> {
16        // Support property as the variable in ThereExistsSuchThatQuantifier.
17        // This code enables meta operation which we were calling eval without adding specific "eval" contract.
18        // For instance, we can write a property like `∀su ∈ SU: su()`.
19        if Ext::is_placeholder(property_bytes) {
20            if &Ext::get_input_value(property_bytes) == placeholder {
21                return Ok(quantified.clone());
22            }
23        }
24        let mut property: Property<AddressOf<Ext>> = Ext::bytes_to_property(&property_bytes)?;
25        if property.predicate_address == Ext::not_address() {
26            require!(property.inputs.len() > 0);
27            property.inputs[0] =
28                self.replace_variable(&property.inputs[0], placeholder, quantified)?;
29        } else if property.predicate_address == self.ext.ext_address() {
30            require!(property.inputs.len() > 2);
31            property.inputs[2] =
32                self.replace_variable(&property.inputs[2], placeholder, quantified)?;
33        } else if property.predicate_address == Ext::and_address()
34            || property.predicate_address == Ext::or_address()
35        {
36            property.inputs = property
37                .inputs
38                .iter()
39                .map(|input| self.replace_variable(input, placeholder, quantified))
40                .collect::<Result<Vec<_>, _>>()?;
41        } else {
42            property.inputs = property
43                .inputs
44                .iter()
45                .map(|input| {
46                    if Ext::is_placeholder(input) {
47                        if &Ext::get_input_value(input) == placeholder {
48                            return quantified.clone();
49                        }
50                    }
51                    input.clone()
52                })
53                .collect();
54        }
55        Ok(property.encode())
56    }
57}
58
59impl<'a, Ext: ExternalCall> LogicalConnectiveInterface<AddressOf<Ext>>
60    for ThereExistsPredicate<'a, Ext>
61{
62    /// @dev Validates a child node of ThereExists property in game tree.
63    fn is_valid_challenge(
64        &self,
65        inputs: Vec<Vec<u8>>,
66        _challenge_inputs: Vec<Vec<u8>>,
67        challenge: Property<AddressOf<Ext>>,
68    ) -> ExecResult<AddressOf<Ext>> {
69        // challenge must be for(, , not(p))
70        require_with_message!(
71            challenge.predicate_address == Ext::for_all_address(),
72            "challenge must be ForAllSuchThat"
73        );
74        require!(inputs.len() > 2);
75        let new_inputs = vec![inputs[2].clone()];
76        let p = Property::<AddressOf<Ext>> {
77            predicate_address: Ext::not_address().clone(),
78            inputs: new_inputs,
79        };
80
81        require!(challenge.inputs.len() > 2);
82        require_with_message!(inputs[1] == challenge.inputs[1], "variable must be same");
83        require_with_message!(p.encode() == challenge.inputs[2], "inputs must be same");
84        Ok(true)
85    }
86}
87
88impl<'a, Ext: ExternalCall> DecidablePredicateInterface<AddressOf<Ext>>
89    for ThereExistsPredicate<'a, Ext>
90{
91    /// @dev Can decide true when all child properties are decided true
92    fn decide_with_witness(
93        &self,
94        inputs: Vec<Vec<u8>>,
95        witness: Vec<Vec<u8>>,
96    ) -> ExecResult<AddressOf<Ext>> {
97        require!(inputs.len() > 2);
98        require!(witness.len() > 0);
99        let property_bytes = self.replace_variable(&inputs[2], &inputs[1], &witness[0])?;
100        let property: Property<AddressOf<Ext>> = Ext::bytes_to_property(&property_bytes)?;
101        Ok(Ext::bytes_to_bool(
102            &self.ext.ext_call(
103                &property.predicate_address,
104                PredicateCallInputs::DecidablePredicate(
105                    DecidablePredicateCallInputs::DecideWithWitness {
106                        inputs: property.inputs,
107                        witness: witness
108                            .as_slice()
109                            .get(1..)
110                            .unwrap_or(vec![].as_slice())
111                            .to_vec(),
112                    },
113                ),
114            )?,
115        )?)
116    }
117}
ovmi/predicates/there_exists.rs

ovmi/predicates/
there_exists.rs
