Oak.v 8.09 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import ZArith.
2
From SmartContracts Require Import Monads.
3
From SmartContracts Require Import Containers.
4
5
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
6
From Coq Require Import List.
7
8

Import ListNotations.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
9
10
11
12
13
14

Inductive OakType :=
  | oak_unit : OakType
  | oak_int : OakType
  | oak_bool : OakType
  | oak_pair : OakType -> OakType -> OakType
15
  | oak_list : OakType -> OakType.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
16

17
18
19
20
21
22
23
24
25
Module OakType.
  Scheme Equality for OakType.
  Definition eqb := OakType_beq.
  Definition eq_dec := OakType_eq_dec.

  Fixpoint eqb_spec (a b : OakType) :
    Bool.reflect (a = b) (eqb a b).
  Proof.
    destruct a, b; simpl in *; try (left; congruence); try (right; congruence).
26
27
28
    - destruct (eqb_spec a1 b1), (eqb_spec a2 b2);
        try (left; congruence); try (right; congruence).
    - destruct (eqb_spec a b); try (left; congruence); try (right; congruence).
29
30
  Qed.
End OakType.
31

32
Fixpoint interp_type (t : OakType) : Type :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
33
  match t with
34
35
36
37
38
  | oak_unit => unit
  | oak_int => Z
  | oak_bool => bool
  | oak_pair a b => interp_type a * interp_type b
  | oak_list a => list (interp_type a)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
39
40
  end.

41
Set Primitive Projections.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
42
43
44
Record OakValue :=
  build_oak_value {
    oak_value_type : OakType;
45
    oak_value : interp_type oak_value_type;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
46
  }.
47
Unset Primitive Projections.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
48

49
Definition extract_oak_value (t : OakType) (value : OakValue) : option (interp_type t).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
50
51
Proof.
  destruct value as [ty val].
52
  destruct (OakType.eq_dec t ty).
53
54
  - subst. exact (Some val).
  - exact None.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
55
56
Defined.

57
58
59
60
61
62
(* Defines that a type can be serialized into OakValue and deserialized from it,
   and that these are inverses *)
Class OakTypeEquivalence (ty : Type) :=
  {
    serialize : ty -> OakValue;
    deserialize : OakValue -> option ty;
63
    deserialize_serialize : forall (x : ty), deserialize (serialize x) = Some x;
64
65
  }.

66
67
68
69
70
71
Global Opaque serialize deserialize deserialize_serialize.

Program Instance oak_unit_equivalence : OakTypeEquivalence unit :=
  {| serialize u := build_oak_value oak_unit u;
     deserialize := extract_oak_value oak_unit; |}.
Solve Obligations with reflexivity.
72

73
74
75
76
Program Instance oak_int_equivalence : OakTypeEquivalence Z :=
  {| serialize i := build_oak_value oak_int i;
     deserialize := extract_oak_value oak_int; |}.
Solve Obligations with reflexivity.
77

78
79
80
81
Program Instance oak_bool_equivalence : OakTypeEquivalence bool :=
  {| serialize b := build_oak_value oak_bool b;
     deserialize := extract_oak_value oak_bool; |}.
Solve Obligations with reflexivity.
82

83
84
85
86
Program Instance oak_nat_equivalence : OakTypeEquivalence nat :=
  {| serialize n := serialize (Z.of_nat n);
     deserialize z := do z' <- deserialize z; Some (Z.to_nat z'); |}.
Next Obligation.
87
  intros x.
88
  cbn.
89
  rewrite deserialize_serialize.
90
  cbn.
91
92
  rewrite Nat2Z.id.
  reflexivity.
93
Qed.
94

95
96
97
Program Instance oak_positive_equivalence : OakTypeEquivalence positive :=
  {| serialize p := serialize (Zpos p);
     deserialize z := do z' <- deserialize z; Some (Z.to_pos z'); |}.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
98
Next Obligation. auto. Qed.
99

100
Program Instance oak_value_equivalence : OakTypeEquivalence OakValue :=
101
  {| serialize v := v;
102
103
     deserialize v := Some v; |}.
Solve Obligations with reflexivity.
104

105
106
107
108
109
110
111
112
113
114
115
116
117
118
Program Instance BoundedN_equivalence {bound : N}
  : OakTypeEquivalence (BoundedN bound) :=
  {| serialize bn := serialize (countable.encode bn);
    deserialize v :=
      do p <- (deserialize v : option positive);
      countable.decode p |}.
Next Obligation.
  intros bound x.
  simpl.
  rewrite deserialize_serialize.
  simpl.
  now rewrite countable.decode_encode.
Qed.

119
120
121
122
(* Program Instance generates an insane amount of obligations for sums,
   so we define it by ourselves. *)
Section Sum.
  Context `{OakTypeEquivalence A} `{OakTypeEquivalence B}.
123

124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
  Definition serialize_sum (v : A + B) :=
    let (is_left, ov) :=
        match v with
        | inl l => (true, serialize l)
        | inr r => (false, serialize r)
        end in
    build_oak_value (oak_pair oak_bool ov.(oak_value_type)) (is_left, ov.(oak_value)).

  Definition deserialize_sum
            `{OakTypeEquivalence A} `{OakTypeEquivalence B}
            (os : OakValue) :=
    match os with
    | build_oak_value (oak_pair oak_bool v) (b, val) =>
      if b then
        do a <- @deserialize A _ (build_oak_value v val);
        Some (inl a)
      else
        do b <- @deserialize B _ (build_oak_value v val);
        Some (inr b)
    | _ => None
    end.

  Lemma deserialize_serialize_sum (s : A + B)
    : deserialize_sum (serialize_sum s) = Some s.
  Proof.
    unfold serialize_sum, deserialize_sum.
    destruct s as [a | b]; simpl; rewrite deserialize_serialize; reflexivity.
  Qed.

  Global Instance oak_sum_equivalence : OakTypeEquivalence (A + B)%type :=
    {| serialize := serialize_sum;
       deserialize := deserialize_sum;
       deserialize_serialize := deserialize_serialize_sum; |}.
End Sum.

Section Product.
  Context `{OakTypeEquivalence A} `{OakTypeEquivalence B}.

  Definition serialize_product '(a, b) :=
    let 'build_oak_value a_oty a_val := @serialize A _ a in
    let 'build_oak_value b_oty b_val := @serialize B _ b in
    build_oak_value (oak_pair a_oty b_oty) (a_val, b_val).

  Definition deserialize_product op :=
    match op with
    | build_oak_value (oak_pair a_ty b_ty) (a_val, b_val) =>
      do a <- @deserialize A _ (build_oak_value a_ty a_val);
      do b <- @deserialize B _ (build_oak_value b_ty b_val);
      Some (a, b)
    | _ => None
    end.

  Lemma deserialize_serialize_product (p : A * B)
        : deserialize_product (serialize_product p) = Some p.
  Proof.
    unfold serialize_product, deserialize_product.
180
    destruct p.
181
    repeat rewrite deserialize_serialize.
182
    reflexivity.
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
  Qed.

  Global Instance oak_product_equivalence : OakTypeEquivalence (A * B) :=
    {| serialize := serialize_product;
       deserialize := deserialize_product;
       deserialize_serialize := deserialize_serialize_product; |}.
End Product.

Section List.
  Context `{OakTypeEquivalence A}.

  Definition serialize_list (l : list A) :=
    let go a acc :=
        let 'build_oak_value a_oty a_val := serialize a in
        let 'build_oak_value acc_oty acc_val := acc in
        build_oak_value (oak_pair a_oty acc_oty) (a_val, acc_val) in
    fold_right go (build_oak_value oak_unit tt) l.

  Definition deserialize_list (ol : OakValue) :=
    let fix aux (ty : OakType) (val : interp_type ty) : option (list A) :=
        match ty, val with
        | oak_pair hd_ty tl_ty, (hd_val, tl_val) =>
          do hd <- deserialize (build_oak_value hd_ty hd_val);
          do tl <- aux tl_ty tl_val;
          Some (hd :: tl)
        | oak_unit, _ => Some []
        | _, _ => None
        end in
    let 'build_oak_value ol_ty ol_val := ol in
    aux ol_ty ol_val.
213

214
215
216
217
218
219
  Lemma deserialize_serialize_list (l : list A)
        : deserialize_list (serialize_list l) = Some l.
  Proof.
    unfold serialize_list, deserialize_list.
    induction l as [| hd tl IHl].
    - reflexivity.
220
    - cbn in *.
221
222
223
224
225
226
227
228
229
230
231
232
      rewrite IHl; clear IHl.
      rewrite deserialize_serialize.
      reflexivity.
  Qed.

  Global Instance oak_list_equivalence : OakTypeEquivalence (list A) :=
    {| serialize := serialize_list;
       deserialize := deserialize_list;
       deserialize_serialize := deserialize_serialize_list; |}.
End List.

Program Instance oak_map_equivalence
233
        `{OakTypeEquivalence A}
234
        `{countable.Countable A}
235
        `{OakTypeEquivalence B}
236
237
238
239
240
241
242
243
244
  : OakTypeEquivalence (FMap A B) :=
  {| serialize m := serialize (@FMap.elements A B _ _ m);
     deserialize om :=
       do elems <- @deserialize (list (A * B)) _ om;
     Some (FMap.of_list elems); |}.
Next Obligation.
  intros A OTE_A Eq_A C_A B OTE_B m.
  simpl.
  rewrite deserialize_serialize.
245
246
247
  simpl.
  rewrite FMap.of_elements_eq.
  reflexivity.
248
Qed.
249

250
Program Instance oak_set_equivalence
251
        `{OakTypeEquivalence A}
252
253
254
255
256
257
258
259
260
261
        `{countable.Countable A}
  : OakTypeEquivalence (FMap A unit) :=
  {| serialize s := serialize (@FMap.elements A unit _ _ s);
     deserialize os :=
       do elems <- @deserialize (list (A * unit)) _ os;
       Some (FMap.of_list elems); |}.
Next Obligation.
  intros A OTE_A Eq_A C_A m.
  simpl.
  rewrite deserialize_serialize.
262
  simpl.
263
  rewrite FMap.of_elements_eq.
264
  reflexivity.
265
Qed.