ovmi/prepare/
serializable_predicates.rs

1use crate::compiled_predicates::*;
2use crate::*;
3use codec::{Decode, Encode};
4#[cfg(feature = "std")]
5use serde::{Deserialize, Serialize};
6
7#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
8#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
9pub enum PredicateTypeSerializable {
10    CompiledPredicate,
11    IntermediateCompiledPredicate,
12    AtomicProposition,
13    AtomicPredicateCall,
14    InputPredicateCall,
15    VariablePredicateCall,
16    CompiledPredicateCall,
17    CompiledInput,
18    ConstantInput,
19    LabelInput,
20    NormalInput,
21    VariableInput,
22    SelfInput,
23}
24
25impl From<PredicateTypeSerializable> for PredicateType {
26    fn from(f: PredicateTypeSerializable) -> PredicateType {
27        match f {
28            PredicateTypeSerializable::CompiledPredicate => PredicateType::CompiledPredicate,
29            PredicateTypeSerializable::IntermediateCompiledPredicate => {
30                PredicateType::IntermediateCompiledPredicate
31            }
32            PredicateTypeSerializable::AtomicProposition => PredicateType::AtomicProposition,
33            PredicateTypeSerializable::AtomicPredicateCall => PredicateType::AtomicPredicateCall,
34            PredicateTypeSerializable::InputPredicateCall => PredicateType::InputPredicateCall,
35            PredicateTypeSerializable::VariablePredicateCall => {
36                PredicateType::VariablePredicateCall
37            }
38            PredicateTypeSerializable::CompiledPredicateCall => {
39                PredicateType::CompiledPredicateCall
40            }
41            PredicateTypeSerializable::CompiledInput => PredicateType::CompiledInput,
42            PredicateTypeSerializable::ConstantInput => PredicateType::ConstantInput,
43            PredicateTypeSerializable::LabelInput => PredicateType::LabelInput,
44            PredicateTypeSerializable::NormalInput => PredicateType::NormalInput,
45            PredicateTypeSerializable::VariableInput => PredicateType::VariableInput,
46            PredicateTypeSerializable::SelfInput => PredicateType::SelfInput,
47        }
48    }
49}
50
51#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
52#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
53#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
54pub enum VarTypeSerializable {
55    Address,
56    Bytes,
57}
58
59impl From<VarTypeSerializable> for VarType {
60    fn from(f: VarTypeSerializable) -> VarType {
61        match f {
62            VarTypeSerializable::Address => VarType::Address,
63            VarTypeSerializable::Bytes => VarType::Bytes,
64        }
65    }
66}
67
68/// Compiled Property definition
69#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
70#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
71#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
72pub struct CompiledPredicateSerializable {
73    pub r#type: PredicateTypeSerializable,
74    pub name: String,
75    pub input_defs: Vec<String>,
76    pub contracts: Vec<IntermediateCompiledPredicateSerializable>,
77    pub constants: Option<Vec<ConstantVariableSerializable>>,
78    pub entry_point: String,
79}
80
81impl From<CompiledPredicateSerializable> for CompiledPredicate {
82    fn from(f: CompiledPredicateSerializable) -> CompiledPredicate {
83        CompiledPredicate {
84            r#type: f.r#type.into(),
85            name: f.name.as_bytes().to_vec(),
86            input_defs: f.input_defs.iter().map(|a| a.as_bytes().to_vec()).collect(),
87            contracts: f.contracts.iter().map(|a| a.clone().into()).collect(),
88            constants: match f.constants {
89                Some(constants) => Some(constants.iter().map(|a| a.clone().into()).collect()),
90                None => None,
91            },
92            entry_point: f.entry_point.as_bytes().to_vec(),
93        }
94    }
95}
96
97#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
98#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
99#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
100pub struct ConstantVariableSerializable {
101    pub var_type: VarTypeSerializable,
102    pub name: String,
103}
104
105impl From<ConstantVariableSerializable> for ConstantVariable {
106    fn from(f: ConstantVariableSerializable) -> ConstantVariable {
107        ConstantVariable {
108            var_type: f.var_type.into(),
109            name: f.name.as_bytes().to_vec(),
110        }
111    }
112}
113
114/// IntermediateCompiledPredicate is core of compilation which has only atomic propositions as its inputs.
115/// When we have for a in B() {Foo(a) and Bar(a)},
116/// "for a in B() {...}" and "Foo(a) and Bar(a)" are IntermediateCompiledPredicate.
117#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
118#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
119#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
120pub struct IntermediateCompiledPredicateSerializable {
121    pub r#type: PredicateTypeSerializable,
122    pub name: String,
123    pub original_predicate_name: String,
124    // logical connective
125    pub connective: LogicalConnectiveSerializable,
126    pub input_defs: Vec<String>,
127    pub inputs: Vec<AtomicPropositionOrPlaceholderSerializable>,
128    pub property_inputs: Vec<NormalInputSerializable>,
129}
130
131impl From<IntermediateCompiledPredicateSerializable> for IntermediateCompiledPredicate {
132    fn from(f: IntermediateCompiledPredicateSerializable) -> IntermediateCompiledPredicate {
133        IntermediateCompiledPredicate {
134            r#type: f.r#type.into(),
135            name: f.name.as_bytes().to_vec(),
136            original_predicate_name: f.original_predicate_name.as_bytes().to_vec(),
137            connective: f.connective.into(),
138            input_defs: f.input_defs.iter().map(|a| a.as_bytes().to_vec()).collect(),
139            inputs: f.inputs.iter().map(|a| a.clone().into()).collect(),
140            property_inputs: f.property_inputs.iter().map(|a| a.clone().into()).collect(),
141        }
142    }
143}
144
145#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
146#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
147#[cfg_attr(feature = "std", serde(untagged))]
148pub enum AtomicPropositionOrPlaceholderSerializable {
149    AtomicProposition(AtomicPropositionSerializable),
150    Placeholder(String),
151}
152
153impl From<AtomicPropositionOrPlaceholderSerializable> for AtomicPropositionOrPlaceholder {
154    fn from(f: AtomicPropositionOrPlaceholderSerializable) -> AtomicPropositionOrPlaceholder {
155        match f {
156            AtomicPropositionOrPlaceholderSerializable::AtomicProposition(a) => {
157                AtomicPropositionOrPlaceholder::AtomicProposition(a.clone().into())
158            }
159            AtomicPropositionOrPlaceholderSerializable::Placeholder(a) => {
160                AtomicPropositionOrPlaceholder::Placeholder(a.as_bytes().to_vec())
161            }
162        }
163    }
164}
165
166#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
167#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
168#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
169pub struct AtomicPropositionSerializable {
170    pub r#type: PredicateTypeSerializable,
171    pub predicate: PredicateCallSerializable,
172    pub inputs: Vec<CompiledInputSerializable>,
173    pub is_compiled: Option<bool>,
174}
175
176impl From<AtomicPropositionSerializable> for AtomicProposition {
177    fn from(f: AtomicPropositionSerializable) -> AtomicProposition {
178        AtomicProposition {
179            r#type: f.r#type.into(),
180            predicate: f.predicate.into(),
181            inputs: f.inputs.iter().map(|a| a.clone().into()).collect(),
182            is_compiled: f.is_compiled,
183        }
184    }
185}
186
187#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
188#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
189#[cfg_attr(feature = "std", serde(untagged))]
190pub enum PredicateCallSerializable {
191    AtomicPredicateCall(AtomicPredicateCallSerializable),
192    InputPredicateCall(InputPredicateCallSerializable),
193    VariablePredicateCall(VariablePredicateCallSerializable),
194    CompiledPredicateCall(CompiledPredicateCallSerializable),
195}
196
197impl From<PredicateCallSerializable> for PredicateCall {
198    fn from(f: PredicateCallSerializable) -> PredicateCall {
199        match f {
200            PredicateCallSerializable::AtomicPredicateCall(a) => {
201                PredicateCall::AtomicPredicateCall(a.clone().into())
202            }
203            PredicateCallSerializable::InputPredicateCall(a) => {
204                PredicateCall::InputPredicateCall(a.clone().into())
205            }
206            PredicateCallSerializable::VariablePredicateCall(a) => {
207                PredicateCall::VariablePredicateCall(a.clone().into())
208            }
209            PredicateCallSerializable::CompiledPredicateCall(a) => {
210                PredicateCall::CompiledPredicateCall(a.clone().into())
211            }
212        }
213    }
214}
215
216/// e.g. IsValidSignature()
217#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
218#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
219pub struct AtomicPredicateCallSerializable {
220    pub r#type: PredicateTypeSerializable,
221    pub source: String,
222}
223
224impl From<AtomicPredicateCallSerializable> for AtomicPredicateCall {
225    fn from(f: AtomicPredicateCallSerializable) -> AtomicPredicateCall {
226        AtomicPredicateCall {
227            r#type: f.r#type.into(),
228            source: f.source.as_bytes().to_vec(),
229        }
230    }
231}
232
233/// e.g. a() of "def Foo(a) := a()"
234#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
235#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
236pub struct InputPredicateCallSerializable {
237    pub r#type: PredicateTypeSerializable,
238    pub source: NormalInputSerializable,
239}
240
241impl From<InputPredicateCallSerializable> for InputPredicateCall {
242    fn from(f: InputPredicateCallSerializable) -> InputPredicateCall {
243        InputPredicateCall {
244            r#type: f.r#type.into(),
245            source: f.source.into(),
246        }
247    }
248}
249
250/// e.g. su() of "def Foo(a) := with SU(a) as su {su()}"
251#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
252#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
253pub struct VariablePredicateCallSerializable {
254    pub r#type: PredicateTypeSerializable,
255}
256
257impl From<VariablePredicateCallSerializable> for VariablePredicateCall {
258    fn from(f: VariablePredicateCallSerializable) -> VariablePredicateCall {
259        VariablePredicateCall {
260            r#type: f.r#type.into(),
261        }
262    }
263}
264
265/// For predicates dynamic linking
266/// e.g. Confsig() user defined predicate
267#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
268#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
269pub struct CompiledPredicateCallSerializable {
270    pub r#type: PredicateTypeSerializable,
271    pub source: String,
272}
273
274impl From<CompiledPredicateCallSerializable> for CompiledPredicateCall {
275    fn from(f: CompiledPredicateCallSerializable) -> CompiledPredicateCall {
276        CompiledPredicateCall {
277            r#type: f.r#type.into(),
278            source: f.source.as_bytes().to_vec(),
279        }
280    }
281}
282
283/// CompiledInput indicates which value to pass to PredicateCall as input of predicate
284/// For example,parent_property.inputs[0].inputs[1] is NormalInput andinput_index is 0 and children is [1].
285#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
286#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
287#[cfg_attr(feature = "std", serde(untagged))]
288pub enum CompiledInputSerializable {
289    ConstantInput(ConstantInputSerializable),
290    LabelInput(LabelInputSerializable),
291    NormalInput(NormalInputSerializable),
292    VariableInput(VariableInputSerializable),
293    SelfInput(SelfInputSerializable),
294}
295
296impl From<CompiledInputSerializable> for CompiledInput {
297    fn from(f: CompiledInputSerializable) -> CompiledInput {
298        match f {
299            CompiledInputSerializable::ConstantInput(a) => {
300                CompiledInput::ConstantInput(a.clone().into())
301            }
302            CompiledInputSerializable::LabelInput(a) => CompiledInput::LabelInput(a.clone().into()),
303            CompiledInputSerializable::NormalInput(a) => {
304                CompiledInput::NormalInput(a.clone().into())
305            }
306            CompiledInputSerializable::VariableInput(a) => {
307                CompiledInput::VariableInput(a.clone().into())
308            }
309            CompiledInputSerializable::SelfInput(a) => CompiledInput::SelfInput(a.clone().into()),
310        }
311    }
312}
313
314#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
315#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
316pub struct ConstantInputSerializable {
317    pub r#type: PredicateTypeSerializable,
318    pub name: String,
319}
320
321impl From<ConstantInputSerializable> for ConstantInput {
322    fn from(f: ConstantInputSerializable) -> ConstantInput {
323        ConstantInput {
324            r#type: f.r#type.into(),
325            name: f.name.as_bytes().to_vec(),
326        }
327    }
328}
329
330#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
331#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
332pub struct LabelInputSerializable {
333    pub r#type: PredicateTypeSerializable,
334    pub label: String,
335}
336
337impl From<LabelInputSerializable> for LabelInput {
338    fn from(f: LabelInputSerializable) -> LabelInput {
339        LabelInput {
340            r#type: f.r#type.into(),
341            label: f.label.as_bytes().to_vec(),
342        }
343    }
344}
345
346#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
347#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
348#[cfg_attr(feature = "std", serde(rename_all = "camelCase"))]
349pub struct NormalInputSerializable {
350    pub r#type: PredicateTypeSerializable,
351    pub input_index: u8,
352    pub children: Vec<i8>,
353}
354
355impl From<NormalInputSerializable> for NormalInput {
356    fn from(f: NormalInputSerializable) -> NormalInput {
357        NormalInput {
358            r#type: f.r#type.into(),
359            input_index: f.input_index,
360            children: f.children,
361        }
362    }
363}
364
365#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
366#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
367pub struct VariableInputSerializable {
368    pub r#type: PredicateTypeSerializable,
369    pub placeholder: String,
370    pub children: Vec<i8>,
371}
372
373impl From<VariableInputSerializable> for VariableInput {
374    fn from(f: VariableInputSerializable) -> VariableInput {
375        VariableInput {
376            r#type: f.r#type.into(),
377            placeholder: f.placeholder.as_bytes().to_vec(),
378            children: f.children,
379        }
380    }
381}
382
383#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
384#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
385pub struct SelfInputSerializable {
386    pub r#type: PredicateTypeSerializable,
387    pub children: Vec<i8>,
388}
389
390impl From<SelfInputSerializable> for SelfInput {
391    fn from(f: SelfInputSerializable) -> SelfInput {
392        SelfInput {
393            r#type: f.r#type.into(),
394            children: f.children,
395        }
396    }
397}
398
399#[derive(Clone, Eq, PartialEq, Encode, Decode, Hash)]
400#[cfg_attr(feature = "std", derive(Serialize, Deserialize, Debug))]
401pub enum LogicalConnectiveSerializable {
402    And,
403    ForAllSuchThat,
404    Not,
405    Or,
406    ThereExistsSuchThat,
407}
408
409impl From<LogicalConnectiveSerializable> for LogicalConnective {
410    fn from(f: LogicalConnectiveSerializable) -> LogicalConnective {
411        match f {
412            LogicalConnectiveSerializable::And => LogicalConnective::And,
413            LogicalConnectiveSerializable::ForAllSuchThat => LogicalConnective::ForAllSuchThat,
414            LogicalConnectiveSerializable::Not => LogicalConnective::Not,
415            LogicalConnectiveSerializable::Or => LogicalConnective::Or,
416            LogicalConnectiveSerializable::ThereExistsSuchThat => {
417                LogicalConnective::ThereExistsSuchThat
418            }
419        }
420    }
421}