int.v 19.7 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs.
Set Default Proof Using "Type".

Section int.
  Context `{!typeG Σ}.

  (* Separate definition such that we can make it typeclasses opaque later. *)
  Program Definition int_inner_type (it : int_type) (n : Z) : type := {|
    ty_own β l := ( v, val_of_int n it = Some v  l `has_layout_loc` it  l [β] v)%I
  |}.
  Next Obligation.
    iIntros (it n l). iDestruct 1 as (v Hv Hl) "H". iExists _. do 2 iSplitR => //. by iApply heap_mapsto_own_state_share.
  Qed.

  Program Definition int (it : int_type) : rtype := {|
    rty_type := Z;
    rty := int_inner_type it
  |}.

  Global Program Instance rmovable_int it : RMovable (int it) := {|
    rmovable n := {|
      ty_layout := it_layout it;
      ty_own_val v := val_of_int n it = Some v%I;
  |} |}.
  Next Obligation. iIntros (it n l). by iDestruct 1 as (???)"?". Qed.
  Next Obligation. by iIntros (it n v ?%val_of_int_length). Qed.
  Next Obligation.
    iIntros (it n l). iDestruct 1 as (v Hl Hv) "Hl".
    iExists _. by iFrame.
  Qed.
  Next Obligation. iIntros (it n l v Hly) "Hl". iIntros (?). iExists _. by iFrame. Qed.
  Next Obligation. iIntros (it x1 x2). done. Qed.

  (* TODO: make a simple type as in lambda rust such that we do not
  have to reprove this everytime? *)
  Global Program Instance int_copyable x it : Copyable (x @ int it).
  Next Obligation.
    iIntros (x it E l ?). iDestruct 1 as (v Hv Hl) "Hl".
    iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //. iSplitR => //.
    iExists _, _. iFrame. iModIntro. iSplit => //.
    by iIntros "_".
  Qed.

  Lemma int_val_to_int_Some n v it:
    v ◁ᵥ n @ int it - val_to_int v it = Some n.
  Proof. iIntros "%". iPureIntro. by apply val_to_of_int. Qed.

End int.
(* Typeclasses Opaque int. *)

(* TODO: move this to an extra file? *)
Section bool.
  Context `{!typeG Σ}.

  (* Separate definition such that we can make it typeclasses opaque later. *)
  Program Definition boolean_inner_type (it : int_type) (b : bool) : type := int_inner_type it (Z_of_bool b).

  Program Definition boolean (it : int_type) : rtype := {|
    rty_type := bool;
    rty := boolean_inner_type it
  |}.

  Global Program Instance rmovable_boolean it : RMovable (boolean it) := {|
    rmovable b := {|
      ty_layout := it_layout it;
      ty_own_val v := val_of_int (Z_of_bool b) it = Some v%I;
  |} |}.
  Next Obligation. iIntros (it n l). by iDestruct 1 as (???)"?". Qed.
  Next Obligation. by iIntros (it n v ?%val_of_int_length). Qed.
  Next Obligation.
    iIntros (it n l). iDestruct 1 as (v Hv Hl) "Hl".
    iExists _. by iFrame.
  Qed.
  Next Obligation. iIntros (it n l v ?) "Hl". iIntros (?). iExists _. by iFrame. Qed.
  Next Obligation. iIntros (it x1 x2). done. Qed.

End bool.

Section programs.
  Context `{!typeG Σ}.

Michael Sammler's avatar
Michael Sammler committed
83
  (*** int *)
Michael Sammler's avatar
Michael Sammler committed
84
  Lemma type_val_int n it T:
85
    (n  it  T (t2mt (n @ (int it)))) - typed_value (i2v n it) T.
Michael Sammler's avatar
Michael Sammler committed
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
  Proof. iDestruct 1 as ([v Hv]%val_of_int_is_some) "HT". iExists  _. iFrame. by rewrite /i2v Hv. Qed.
  Global Instance type_val_int_inst n it : TypedValue (i2v n it) :=
    λ T, i2p (type_val_int n it T).

  (* TODO: instead of adding it_in_range to the context here, have a
  SimplifyPlace/Val instance for int which adds it to the context if
  it does not yet exist (using check_hyp_not_exists)?! *)
  Lemma type_relop_int_int it v1 n1 v2 n2 T b op:
    match op with
    | EqOp => Some (bool_decide (n1 = n2))
    | NeOp => Some (bool_decide (n1  n2))
    | LtOp => Some (bool_decide (n1 < n2))
    | GtOp => Some (bool_decide (n1 > n2))
    | LeOp => Some (bool_decide (n1 <= n2))
    | GeOp => Some (bool_decide (n1 >= n2))
    | _ => None
    end = Some b 
103
    (n1  it - n2  it - T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -
Michael Sammler's avatar
Michael Sammler committed
104
105
      typed_bin_op v1 (v1 ◁ᵥ n1 @ int it) v2 (v2 ◁ᵥ n2 @ int it) op (IntOp it) (IntOp it) T.
  Proof.
106
    move => Hop. iIntros "HT" (Hv1 Hv2 Φ) "HΦ".
Michael Sammler's avatar
Michael Sammler committed
107
108
109
    iDestruct ("HT" with "[] []" ) as "HT".
    1-2: iPureIntro; by apply: val_of_int_in_range.
    move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2.
110
111
112
113
    iApply (wp_binop_det (i2v (Z_of_bool b) i32)). iSplit.
    { iIntros (σ v') "_ !%". split; last (move => ->; by econstructor).
      destruct op => //; inversion 1; by simplify_eq. }
    iIntros "!>". iApply "HΦ" => //. by destruct b.
Michael Sammler's avatar
Michael Sammler committed
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
  Qed.

  Global Program Instance type_eq_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I EqOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 = n2)) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_ne_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I NeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1  n2)) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_lt_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I LtOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 < n2)) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_gt_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I GtOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 > n2)) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_le_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I LeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 <= n2)) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_ge_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ (int it))%I v2 (n2 @ (int it))%I GeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_int_int it v1 n1 v2 n2 T (bool_decide (n1 >= n2)) _ _).
  Next Obligation. done. Qed.

  Lemma type_arithop_int_int it v1 n1 v2 n2 T n op:
   match op with
    | AddOp => Some (n1 + n2)
    | SubOp => Some (n1 - n2)
    | MulOp => Some (n1 * n2)
    | AndOp => Some (Z.land n1 n2)
    | OrOp => Some (Z.lor n1 n2)
    | XorOp => Some (Z.lxor n1 n2)
    | ShlOp => Some (n1  n2)
    | ShrOp => Some (n1  n2)
    | _ => None
    end = Some n 
147
    (n1  it - n2  it - n  it  T (i2v n it) (t2mt (n @ int it))) -
Michael Sammler's avatar
Michael Sammler committed
148
149
150
151
152
153
      typed_bin_op v1 (v1 ◁ᵥ n1 @ int it) v2 (v2 ◁ᵥ n2 @ int it) op (IntOp it) (IntOp it) T.
  Proof.
    iIntros (Hop) "HT". iIntros (Hv1 Hv2 Φ) "HΦ".
    iDestruct ("HT" with "[] []" ) as ([v Hv]%val_of_int_is_some) "HT".
    1-2: iPureIntro; by apply: val_of_int_in_range.
    move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. rewrite /i2v Hv/=.
154
155
156
157
    iApply (wp_binop_det v). iSplit.
    { iIntros (σ v') "_ !%". split; last (move => ->; destruct op; by econstructor).
      destruct op => //; inversion 1; by simplify_eq. }
    iIntros "!>". iApply "HΦ"; last done.  by iPureIntro.
Michael Sammler's avatar
Michael Sammler committed
158
159
160
161
162
163
164
  Qed.
  Lemma type_arithop_int_int_div_mod it v1 n1 v2 n2 T n op:
    match op with
    | DivOp => Some (n1 `quot` n2)
    | ModOp => Some (n1 `rem` n2)
    | _ => None
    end = Some n 
165
    (n1  it - n2  it - n2  0  n  it  T (i2v n it) (t2mt (n @ int it))) -
Michael Sammler's avatar
Michael Sammler committed
166
167
168
169
170
171
      typed_bin_op v1 (v1 ◁ᵥ n1 @ int it) v2 (v2 ◁ᵥ n2 @ int it) op (IntOp it) (IntOp it) T.
  Proof.
    iIntros (Hop) "HT". iIntros (Hv1 Hv2 Φ) "HΦ".
    iDestruct ("HT" with "[] []" ) as (Hn [v Hv]%val_of_int_is_some) "HT".
    1-2: iPureIntro; by apply: val_of_int_in_range.
    move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2. rewrite /i2v Hv/=.
172
173
174
175
176
    iApply (wp_binop_det v). iSplit.
    { iIntros (σ v') "_ !%".
      split; last (move => ->; destruct op; econstructor => //; by case_match).
      destruct op => //; inversion 1; simplify_eq; case_match; by simplify_eq. }
    iApply "HΦ"; last done. by iPureIntro.
Michael Sammler's avatar
Michael Sammler committed
177
178
179
180
181
182
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
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
  Qed.
  Global Program Instance type_add_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I AddOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1 + n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_sub_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I SubOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1 - n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_mul_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I MulOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1 * n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_div_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I DivOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int_div_mod it v1 n1 v2 n2 T (n1 `quot` n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_mod_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I ModOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int_div_mod it v1 n1 v2 n2 T (n1 `rem` n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_and_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I AndOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (Z.land n1 n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_or_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I OrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (Z.lor n1 n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_xor_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I XorOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (Z.lxor n1 n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_shl_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I ShlOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1  n2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_shr_int_int_inst it v1 n1 v2 n2:
    TypedBinOpVal v1 (n1 @ int it)%I v2 (n2 @ int it)%I ShrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_int it v1 n1 v2 n2 T (n1  n2) _ _).
  Next Obligation. done. Qed.

  Inductive destruct_hint_if_int :=
  | DestructHintIfInt (n : Z).

  Lemma type_if_int {B} n s1 s2 Q fn ls (fr : B  _) v :
    destruct_hint (DHintDecide (n  0)) (DestructHintIfInt n)
    (if decide (n  0) then typed_stmt s1 fn ls fr Q else typed_stmt s2 fn ls fr Q) -
    typed_if v (n @ int bool_it) s1 s2 fn ls fr Q.
  Proof. unfold destruct_hint. iIntros "Hs" (Hb%val_to_of_int) => /=. iExists _. iSplit => //. by do ! case_decide. Qed.
  Global Instance type_if_int_inst n v : TypedIf v (n @ int bool_it) :=
    λ B s1 s2 fn ls fr Q, i2p (type_if_int n s1 s2 Q fn ls fr v).

  Inductive destruct_hint_switch_int :=
  | DestructHintSwitchIntCase (n : Z)
  | DestructHintSwitchIntDefault.

  Lemma type_switch_int {B} n it m ss def Q fn ls (fr : B  _) v:
    ([ map] imi  m, destruct_hint DHintInfo (DestructHintSwitchIntCase i) (
             n = i -  s, ss !! mi = Some s  typed_stmt s fn ls fr Q)) 
    (destruct_hint DHintInfo (DestructHintSwitchIntDefault) (
                     n  (map_to_list m).*1 - typed_stmt def fn ls fr Q)) -
    typed_switch v (n @ int it) it m ss def fn ls fr Q.
  Proof.
    unfold destruct_hint. iIntros "HT" (Hv%val_to_of_int). iExists n. iSplit => //.
    iInduction m as [] "IH" using map_ind; simplify_map_eq => //.
    { iDestruct "HT" as "[_ HT]". iApply "HT". iPureIntro. rewrite map_to_list_empty. set_solver. }
    rewrite big_andM_insert //. destruct (decide (n = i)); subst.
    - rewrite lookup_insert. iDestruct "HT" as "[[HT _] _]". by iApply "HT".
    - rewrite lookup_insert_ne//. iApply "IH". iSplit; first by iDestruct "HT" as "[[_ HT] _]".
      iIntros (Hn). iDestruct "HT" as "[_ HT]". iApply "HT". iPureIntro.
      rewrite map_to_list_insert //. set_solver.
  Qed.
  Global Instance type_switch_int_inst n v it : TypedSwitch v (n @ int it) it :=
    λ B m ss def fn ls fr Q, i2p (type_switch_int n it m ss def Q fn ls fr v).

  Lemma type_neg_int n it v T:
244
    (n  it - it.(it_signed)  n  min_int it  T (i2v (-n) it) (t2mt ((-n) @ int it))) -
Michael Sammler's avatar
Michael Sammler committed
245
246
247
248
249
250
251
    typed_un_op v (v ◁ᵥ n @ int it)%I (NegOp) (IntOp it) T.
  Proof.
    iIntros "HT". iIntros (Hv Φ) "HΦ".
    move: Hv (Hv) => /val_to_of_int ? /val_of_int_in_range[Hl Hu].
    iDestruct ("HT" with "[//]") as (Hs Hn) "HT".
    have ? : val_of_int (- n) it = Some (i2v (- n) it). {
      have [|? Hv'] := val_of_int_is_some it (- n); last by rewrite /i2v Hv'.
252
      unfold elem_of, int_elem_of_it, max_int, min_int in *.
Michael Sammler's avatar
Michael Sammler committed
253
254
255
256
257
258
259
260
261
      destruct it as [?[]] => //; simpl in *; lia.
    }
    iApply wp_neg_int => //. by iApply ("HΦ" with "[] HT").
  Qed.
  Global Instance type_neg_int_inst n it v:
    TypedUnOpVal v (n @ int it)%I NegOp (IntOp it) :=
    λ T, i2p (type_neg_int n it v T).

  Lemma type_cast_int n it1 it2 v T:
262
    (n  it1 - n  it2  T (i2v n it2) (t2mt (n @ int it2))) -
Michael Sammler's avatar
Michael Sammler committed
263
264
265
266
267
268
269
270
271
272
273
274
    typed_un_op v (v ◁ᵥ n @ int it1)%I (CastOp (IntOp it2)) (IntOp it1) T.
  Proof.
    iIntros "HT". iIntros (Hv Φ) "HΦ".
    iDestruct ("HT" with "[]" ) as ([v' Hv']%val_of_int_is_some) "HT".
    1: iPureIntro; by apply: val_of_int_in_range.
    move: Hv => /val_to_of_int Hv. rewrite /i2v Hv'/=.
    iApply wp_cast_int => //. iApply ("HΦ" with "[] HT") => //.
  Qed.
  Global Instance type_cast_int_inst n it1 it2 v:
    TypedUnOpVal v (n @ int it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
    λ T, i2p (type_cast_int n it1 it2 v T).

Michael Sammler's avatar
Michael Sammler committed
275
  (*** bool *)
Michael Sammler's avatar
Michael Sammler committed
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
  Lemma type_val_bool b T:
    (T (t2mt (b @ boolean bool_it))) - typed_value (val_of_bool b) T.
  Proof. iIntros "HT". iExists _. iFrame. by destruct b. Qed.
  Global Instance type_val_bool_inst b : TypedValue (val_of_bool b) :=
    λ T, i2p (type_val_bool b T).

  Inductive destruct_hint_if_bool :=
  | DestructHintIfBool (b : bool).

  Lemma type_relop_bool_bool it v1 b1 v2 b2 T b op:
    match op with
    | EqOp => Some (eqb b1 b2)
    | NeOp => Some (negb (eqb b1 b2))
    | _ => None
    end = Some b 
    (T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -
      typed_bin_op v1 (v1 ◁ᵥ b1 @ boolean it) v2 (v2 ◁ᵥ b2 @ boolean it) op (IntOp it) (IntOp it) T.
  Proof.
    iIntros (Hop) "HT". iIntros (Hv1 Hv2 Φ) "HΦ".
    move: Hv1 Hv2 => /val_to_of_int Hv1 /val_to_of_int Hv2.
296
297
298
299
300
    iApply (wp_binop_det (i2v (Z_of_bool b) i32)). iSplit.
    { iIntros (σ v) "_ !%". destruct op, b1, b2; simplify_eq;
      (split; [ inversion 1 | move => -> ]); simplify_eq;
      econstructor => //; by case_bool_decide. }
    iApply "HΦ"; last done. iPureIntro. by destruct b.
Michael Sammler's avatar
Michael Sammler committed
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
  Qed.

  Global Program Instance type_eq_bool_bool_inst it v1 b1 v2 b2:
    TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I EqOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (eqb b1 b2) _ _).
  Next Obligation. done. Qed.
  Global Program Instance type_ne_bool_bool_inst it v1 b1 v2 b2:
    TypedBinOpVal v1 (b1 @ (boolean it))%I v2 (b2 @ (boolean it))%I NeOp (IntOp it) (IntOp it) := λ T, i2p (type_relop_bool_bool it v1 b1 v2 b2 T (negb (eqb b1 b2)) _ _).
  Next Obligation. done. Qed.

  Lemma type_if_bool {B} (b : bool) s1 s2 Q fn ls (fr : B  _) v :
    destruct_hint (DHintDestruct _ b) (DestructHintIfBool b)
    (if b then typed_stmt s1 fn ls fr Q else typed_stmt s2 fn ls fr Q) -
    typed_if v (b @ boolean bool_it) s1 s2 fn ls fr Q.
  Proof. unfold destruct_hint. iIntros "Hs" (Hb%val_to_of_int) => /=. iExists _. iSplit => //. by destruct b. Qed.
  Global Instance type_if_bool_inst b v : TypedIf v (b @ boolean bool_it) :=
    λ B s1 s2 fn ls fr Q, i2p (type_if_bool _ _ _ _ _ _ _ _).

  Lemma type_assert_bool {B} (b : bool) s Q fn ls (fr : B  _) v :
    (b  typed_stmt s fn ls fr Q) -
    typed_assert v (b @ boolean bool_it) s fn ls fr Q.
  Proof.
    iIntros "[% Hs]" (Hb%val_to_of_int) => /=. iExists _. iSplit => //. iFrame. by destruct b.
  Qed.
  Global Instance type_assert_bool_inst b v : TypedAssert v (b @ boolean bool_it) :=
    λ B s fn ls fr Q, i2p (type_assert_bool _ _ _ _ _ _ _).

  Lemma type_cast_bool b it1 it2 v T:
    (T (i2v (Z_of_bool b) it2) (t2mt (b @ boolean it2))) -
    typed_un_op v (v ◁ᵥ b @ boolean it1)%I (CastOp (IntOp it2)) (IntOp it1) T.
  Proof.
    iIntros "HT". iIntros (Hv Φ) "HΦ".
    move: Hv => /val_to_of_int Hv.
    iApply wp_cast_int => //=. by apply val_of_int_bool.
    iApply ("HΦ" with "[] HT") => //. iPureIntro => /=. by apply val_of_int_bool.
  Qed.
  Global Instance type_cast_bool_inst b it1 it2 v:
    TypedUnOpVal v (b @ boolean it1)%I (CastOp (IntOp it2)) (IntOp it1) :=
    λ T, i2p (type_cast_bool b it1 it2 v T).

Michael Sammler's avatar
Michael Sammler committed
340
  (*** int <-> bool *)
Michael Sammler's avatar
Michael Sammler committed
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
  Lemma subsume_int_bool_place l β n b it T:
    n = Z_of_bool b  T -
    subsume (l ◁ₗ{β} n @ int it) (l ◁ₗ{β} b @ boolean it) T.
  Proof. iIntros "[-> $] Hint". iDestruct "Hint" as (x Hx) "?". iExists _. by iFrame. Qed.
  Global Instance subsume_int_bool_place_inst l β n b it:
    SubsumePlace l β (n @ int it) (b @ boolean it) :=
    λ T, i2p (subsume_int_bool_place l β n b it T).

  Lemma subsume_int_bool_val v n b it T:
    n = Z_of_bool b  T -
    subsume (v ◁ᵥ n @ int it) (v ◁ᵥ b @ boolean it) T.
  Proof. by iIntros "[-> $] %". Qed.
  Global Instance subsume_int_bool_val_inst v n b it:
    SubsumeVal v (n @ int it) (b @ boolean it) :=
    λ T, i2p (subsume_int_bool_val v n b it T).

Michael Sammler's avatar
Michael Sammler committed
357
358
359
360
361
362

  Lemma type_binop_bool_int it1 it2 it3 it4 v1 b1 v2 n2 T op:
    typed_bin_op v1 (v1 ◁ᵥ (Z_of_bool b1) @ int it1) v2 (v2 ◁ᵥ n2 @ int it2) op (IntOp it3) (IntOp it4) T -
    typed_bin_op v1 (v1 ◁ᵥ b1 @ boolean it1) v2 (v2 ◁ᵥ n2 @ int it2) op (IntOp it3) (IntOp it4) T.
  Proof. iIntros "HT". iApply "HT". Qed.
  Global Instance type_binop_bool_int_inst it1 it2 it3 it4 v1 b1 v2 n2 op:
Michael Sammler's avatar
Michael Sammler committed
363
    TypedBinOpVal v1 (b1 @ boolean it1)%I v2 (n2 @ int it2)%I op (IntOp it3) (IntOp it4) :=
Michael Sammler's avatar
Michael Sammler committed
364
365
366
367
368
369
370
    λ T, i2p (type_binop_bool_int it1 it2 it3 it4 v1 b1 v2 n2 T op).

  Lemma type_binop_int_bool it1 it2 it3 it4 v1 b1 v2 n2 T op:
    typed_bin_op v1 (v1 ◁ᵥ n2 @ int it2) v2 (v2 ◁ᵥ (Z_of_bool b1) @ int it1) op (IntOp it3) (IntOp it4) T -
    typed_bin_op v1 (v1 ◁ᵥ n2 @ int it2) v2 (v2 ◁ᵥ b1 @ boolean it1) op (IntOp it3) (IntOp it4) T.
  Proof. iIntros "HT". iApply "HT". Qed.
  Global Instance type_binop_int_bool_inst it1 it2 it3 it4 v1 b1 v2 n2 op:
Michael Sammler's avatar
Michael Sammler committed
371
    TypedBinOpVal v1 (n2 @ int it2)%I v2 (b1 @ boolean it1)%I op (IntOp it3) (IntOp it4) :=
Michael Sammler's avatar
Michael Sammler committed
372
373
    λ T, i2p (type_binop_int_bool it1 it2 it3 it4 v1 b1 v2 n2 T op).

Michael Sammler's avatar
Michael Sammler committed
374
375
376
End programs.
Typeclasses Opaque int_inner_type boolean_inner_type.

Michael Sammler's avatar
Michael Sammler committed
377
378
379
380
381
Notation "'if' p " := (DestructHintIfBool p) (at level 100, only printing).
Notation "'if' p ≠ 0 " := (DestructHintIfInt p) (at level 100, only printing).
Notation "'case' n " := (DestructHintSwitchIntCase n) (at level 100, only printing).
Notation "'default'" := (DestructHintSwitchIntDefault) (at level 100, only printing).

Michael Sammler's avatar
Michael Sammler committed
382
383
384
385
386
(*** Tests *)
Section tests.
  Context `{!typeG Σ}.

  Example type_eq n1 n3 T:
387
388
    n1  size_t 
    n3  size_t 
Michael Sammler's avatar
Michael Sammler committed
389
390
391
392
393
394
395
396
     typed_val_expr ((i2v n1 size_t +{IntOp size_t, IntOp size_t} i2v 0 size_t) = {IntOp size_t, IntOp size_t} i2v n3 size_t ) T.
  Proof.
    move => Hn1 Hn2.
    iApply type_bin_op.
    iApply type_bin_op.
    iApply type_val. iApply type_val_int. iSplit => //.
    iApply type_val. iApply type_val_int. iSplit => //.
    iApply type_arithop_int_int => //. iIntros (??). iSplit. {
397
      iPureIntro. unfold elem_of, int_elem_of_it, min_int, max_int in *; lia.
Michael Sammler's avatar
Michael Sammler committed
398
399
400
401
402
    }
    iApply type_val. iApply type_val_int. iSplit => //.
    iApply type_relop_int_int => //.
  Abort.
End tests.