Serializable.v 8.14 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
15
16
17
18
19
20
21
22
Inductive SerializedType :=
  | ser_unit : SerializedType
  | ser_int : SerializedType
  | ser_bool : SerializedType
  | ser_pair : SerializedType -> SerializedType -> SerializedType
  | ser_list : SerializedType -> SerializedType.

Module SerializedType.
  Scheme Equality for SerializedType.
  Definition eqb := SerializedType_beq.
  Definition eq_dec := SerializedType_eq_dec.

  Fixpoint eqb_spec (a b : SerializedType) :
23
24
    Bool.reflect (a = b) (eqb a b).
  Proof.
25
    destruct a, b; cbn 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
  Qed.
30
End SerializedType.
31

32
Fixpoint interp_type (t : SerializedType) : Type :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
33
  match t with
34
35
36
37
38
  | ser_unit => unit
  | ser_int => Z
  | ser_bool => bool
  | ser_pair a b => interp_type a * interp_type b
  | ser_list a => list (interp_type a)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
39
40
  end.

41
Set Primitive Projections.
42
43
44
45
Record SerializedValue :=
  build_ser_value {
    ser_value_type : SerializedType;
    ser_value : interp_type ser_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_ser_value (t : SerializedType) (value : SerializedValue) : option (interp_type t).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
50
51
Proof.
  destruct value as [ty val].
52
  destruct (SerializedType.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
(* Defines that a type can be serialized into SerializedValue and deserialized from it,
   and that deserializing is a left inverse of serialziing. *)
Class Serializable (ty : Type) :=
60
  {
61
62
    serialize : ty -> SerializedValue;
    deserialize : SerializedValue -> option ty;
63
    deserialize_serialize x : deserialize (serialize x) = Some x;
64
65
  }.

66
67
Global Opaque serialize deserialize deserialize_serialize.

68
69
70
Program Instance unit_serializable : Serializable unit :=
  {| serialize u := build_ser_value ser_unit u;
     deserialize := extract_ser_value ser_unit; |}.
71
Solve Obligations with reflexivity.
72

73
74
75
Program Instance int_serializable : Serializable Z :=
  {| serialize i := build_ser_value ser_int i;
     deserialize := extract_ser_value ser_int; |}.
76
Solve Obligations with reflexivity.
77

78
79
80
Program Instance bool_serializable : Serializable bool :=
  {| serialize b := build_ser_value ser_bool b;
     deserialize := extract_ser_value ser_bool; |}.
81
Solve Obligations with reflexivity.
82

83
Program Instance nat_serializable : Serializable nat :=
84
85
86
  {| 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
Program Instance ser_positive_equivalence : Serializable positive :=
96
97
  {| 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 ser_value_equivalence : Serializable SerializedValue :=
101
  {| serialize v := v;
102
103
     deserialize v := Some v; |}.
Solve Obligations with reflexivity.
104

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

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

123
  Definition serialize_sum (v : A + B) :=
124
    let (is_left, ser) :=
125
126
127
128
        match v with
        | inl l => (true, serialize l)
        | inr r => (false, serialize r)
        end in
129
    build_ser_value (ser_pair ser_bool ser.(ser_value_type)) (is_left, ser.(ser_value)).
130

131
132
133
134
135
  Definition deserialize_sum (val : SerializedValue) : option (A + B) :=
    match val with
    | build_ser_value (ser_pair ser_bool v) (is_left, val) =>
      if is_left then
        do a <- deserialize (build_ser_value v val) : option A;
136
137
        Some (inl a)
      else
138
        do b <- deserialize (build_ser_value v val) : option B;
139
140
141
142
143
144
145
146
        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.
147
    destruct s as [a | b]; cbn; rewrite deserialize_serialize; reflexivity.
148
149
  Qed.

150
  Global Instance sum_serializable : Serializable (A + B) :=
151
152
153
154
155
156
    {| serialize := serialize_sum;
       deserialize := deserialize_sum;
       deserialize_serialize := deserialize_serialize_sum; |}.
End Sum.

Section Product.
157
  Context `{Serializable A} `{Serializable B}.
158

159
160
161
162
  Definition serialize_product (pair : A * B) : SerializedValue :=
    let (a, b) := pair in
    let (a_ty, a_val) := serialize a in
    let (b_ty, b_val) := serialize b in
163
    build_ser_value (ser_pair a_ty b_ty) (a_val, b_val).
164

165
166
  Definition deserialize_product (val : SerializedValue) : option (A * B) :=
    match val with
167
    | build_ser_value (ser_pair a_ty b_ty) (a_val, b_val) =>
168
169
      do a <- deserialize (build_ser_value a_ty a_val) : option A;
      do b <- deserialize (build_ser_value b_ty b_val) : option B;
170
171
172
173
174
175
176
177
      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.
178
    destruct p.
179
    repeat rewrite deserialize_serialize.
180
    reflexivity.
181
182
  Qed.

183
  Global Instance product_serializable : Serializable (A * B) :=
184
185
186
187
188
189
    {| serialize := serialize_product;
       deserialize := deserialize_product;
       deserialize_serialize := deserialize_serialize_product; |}.
End Product.

Section List.
190
  Context `{Serializable A}.
191

192
193
194
195
  Definition serialize_list (l : list A) : SerializedValue :=
    let go a (acc : SerializedValue) :=
        let (a_ty, a_val) := serialize a in
        let (acc_ty, acc_val) := acc in
196
197
        build_ser_value (ser_pair a_ty acc_ty) (a_val, acc_val) in
    fold_right go (build_ser_value ser_unit tt) l.
198

199
  Definition deserialize_list (val : SerializedValue) : option (list A) :=
200
    let fix aux (ty : SerializedType) (val : interp_type ty) : option (list A) :=
201
        match ty, val with
202
203
        | ser_pair hd_ty tl_ty, (hd_val, tl_val) =>
          do hd <- deserialize (build_ser_value hd_ty hd_val);
204
205
          do tl <- aux tl_ty tl_val;
          Some (hd :: tl)
206
        | ser_unit, _ => Some []
207
208
        | _, _ => None
        end in
209
    let (ty, uval) := val in
210
    aux ty uval.
211

212
213
214
215
216
217
  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.
218
    - cbn in *.
219
220
221
222
223
      rewrite IHl; clear IHl.
      rewrite deserialize_serialize.
      reflexivity.
  Qed.

224
  Global Instance list_serializable : Serializable (list A) :=
225
226
227
228
229
    {| serialize := serialize_list;
       deserialize := deserialize_list;
       deserialize_serialize := deserialize_serialize_list; |}.
End List.

230
231
Program Instance map_serializable
        `{Serializable A}
232
        `{countable.Countable A}
233
234
        `{Serializable B}
  : Serializable (FMap A B) :=
235
  {| serialize m := serialize (@FMap.elements A B _ _ m);
236
     deserialize val :=
237
238
       do elems <- deserialize val : option (list (A * B));
       Some (FMap.of_list elems); |}.
239
Next Obligation.
240
  intros.
241
  cbn.
242
  rewrite deserialize_serialize.
243
  cbn.
244
245
  rewrite FMap.of_elements_eq.
  reflexivity.
246
Qed.
247

248
249
Program Instance set_serializable
        `{Serializable A}
250
        `{countable.Countable A}
251
  : Serializable (FMap A unit) :=
252
  {| serialize s := serialize (@FMap.elements A unit _ _ s);
253
     deserialize val :=
254
       do elems <- deserialize val : option (list (A * unit));
255
256
       Some (FMap.of_list elems); |}.
Next Obligation.
257
  intros.
258
  cbn.
259
  rewrite deserialize_serialize.
260
  cbn.
261
  rewrite FMap.of_elements_eq.
262
  reflexivity.
263
Qed.