Serializable.v 8.39 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
3
4
5
(* This file defines a common storage format for countable types.
This format, SerializedValue, is either a unit/int/bool or a pair/list
of these. We also define Serializable as a type class capturing that a
type can be converted from and to this format. *)

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
6
From Coq Require Import ZArith.
7
From SmartContracts Require Import Monads.
8
From SmartContracts Require Import Containers.
9
10
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
11
From Coq Require Import List.
12
13

Import ListNotations.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
14

15
16
17
18
19
20
21
22
23
24
25
26
27
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) :
28
29
    Bool.reflect (a = b) (eqb a b).
  Proof.
30
    destruct a, b; cbn in *; try (left; congruence); try (right; congruence).
31
32
33
    - 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).
34
  Qed.
35
End SerializedType.
36

37
Fixpoint interp_type (t : SerializedType) : Type :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
38
  match t with
39
40
41
42
43
  | 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
44
45
  end.

46
Set Primitive Projections.
47
48
49
50
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
51
  }.
52
Unset Primitive Projections.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
53

54
Definition extract_ser_value (t : SerializedType) (value : SerializedValue) : option (interp_type t).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
55
56
Proof.
  destruct value as [ty val].
57
  destruct (SerializedType.eq_dec t ty).
58
59
  - subst. exact (Some val).
  - exact None.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
60
61
Defined.

62
63
64
(* 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) :=
65
  {
66
67
    serialize : ty -> SerializedValue;
    deserialize : SerializedValue -> option ty;
68
    deserialize_serialize x : deserialize (serialize x) = Some x;
69
70
  }.

71
72
Global Opaque serialize deserialize deserialize_serialize.

73
74
75
Program Instance unit_serializable : Serializable unit :=
  {| serialize u := build_ser_value ser_unit u;
     deserialize := extract_ser_value ser_unit; |}.
76
Solve Obligations with reflexivity.
77

78
79
80
Program Instance int_serializable : Serializable Z :=
  {| serialize i := build_ser_value ser_int i;
     deserialize := extract_ser_value ser_int; |}.
81
Solve Obligations with reflexivity.
82

83
84
85
Program Instance bool_serializable : Serializable bool :=
  {| serialize b := build_ser_value ser_bool b;
     deserialize := extract_ser_value ser_bool; |}.
86
Solve Obligations with reflexivity.
87

88
Program Instance nat_serializable : Serializable nat :=
89
90
91
  {| serialize n := serialize (Z.of_nat n);
     deserialize z := do z' <- deserialize z; Some (Z.to_nat z'); |}.
Next Obligation.
92
  intros x.
93
  cbn.
94
  rewrite deserialize_serialize.
95
  cbn.
96
97
  rewrite Nat2Z.id.
  reflexivity.
98
Qed.
99

100
Program Instance ser_positive_equivalence : Serializable positive :=
101
102
  {| 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
103
Next Obligation. auto. Qed.
104

105
Program Instance ser_value_equivalence : Serializable SerializedValue :=
106
  {| serialize v := v;
107
108
     deserialize v := Some v; |}.
Solve Obligations with reflexivity.
109

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

123
124
125
(* Program Instance generates an insane amount of obligations for sums,
   so we define it by ourselves. *)
Section Sum.
126
  Context `{Serializable A} `{Serializable B}.
127

128
  Definition serialize_sum (v : A + B) :=
129
    let (is_left, ser) :=
130
131
132
133
        match v with
        | inl l => (true, serialize l)
        | inr r => (false, serialize r)
        end in
134
    build_ser_value (ser_pair ser_bool ser.(ser_value_type)) (is_left, ser.(ser_value)).
135

136
137
138
139
140
  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;
141
142
        Some (inl a)
      else
143
        do b <- deserialize (build_ser_value v val) : option B;
144
145
146
147
148
149
150
151
        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.
152
    destruct s as [a | b]; cbn; rewrite deserialize_serialize; reflexivity.
153
154
  Qed.

155
  Global Instance sum_serializable : Serializable (A + B) :=
156
157
158
159
160
161
    {| serialize := serialize_sum;
       deserialize := deserialize_sum;
       deserialize_serialize := deserialize_serialize_sum; |}.
End Sum.

Section Product.
162
  Context `{Serializable A} `{Serializable B}.
163

164
165
166
167
  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
168
    build_ser_value (ser_pair a_ty b_ty) (a_val, b_val).
169

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

188
  Global Instance product_serializable : Serializable (A * B) :=
189
190
191
192
193
194
    {| serialize := serialize_product;
       deserialize := deserialize_product;
       deserialize_serialize := deserialize_serialize_product; |}.
End Product.

Section List.
195
  Context `{Serializable A}.
196

197
198
199
200
  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
201
202
        build_ser_value (ser_pair a_ty acc_ty) (a_val, acc_val) in
    fold_right go (build_ser_value ser_unit tt) l.
203

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

217
218
219
220
221
222
  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.
223
    - cbn in *.
224
225
226
227
228
      rewrite IHl; clear IHl.
      rewrite deserialize_serialize.
      reflexivity.
  Qed.

229
  Global Instance list_serializable : Serializable (list A) :=
230
231
232
233
234
    {| serialize := serialize_list;
       deserialize := deserialize_list;
       deserialize_serialize := deserialize_serialize_list; |}.
End List.

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

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