lang.v 47.4 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
2
3
4
5
6
7
8
From iris.program_logic Require Export language ectx_language ectxi_language.
From stdpp Require Export strings.
From stdpp Require Import gmap list.
From refinedc.lang Require Export base.
Set Default Proof Using "Type".

Open Scope Z_scope.

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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
(** Representation of a standard (8-bit) byte. *)
Section Byte.
  Definition bits_per_byte : Z := 8.

  Definition byte_modulus : Z :=
    Eval cbv in 2 ^ bits_per_byte.

  Record byte :=
    Byte {
      byte_val : Z;
      byte_constr : -1 < byte_val < byte_modulus;
    }.

  Global Instance byte_eq_dec : EqDecision byte.
  Proof.
    move => [b1 H1] [b2 H2]. destruct (decide (b1 = b2)) as [->|].
    - left. assert (H1 = H2) as ->; [|done]. apply proof_irrel.
    - right. naive_solver.
  Qed.
End Byte.

(** Representation of a type layout (byte size and alignment constraint). *)
Section Layout.
  Record layout :=
    Layout {
      ly_size : nat;
      ly_align_log : nat;
    }.

  Definition sizeof   (ly : layout) : nat := ly.(ly_size).
  Definition ly_align (ly : layout) : nat := 2 ^ ly.(ly_align_log).

  Global Instance layout_dec_eq : EqDecision layout.
  Proof. solve_decision. Defined.

  Global Instance layout_inhabited : Inhabited layout :=
    populate (Layout 0 0).

  Global Instance layout_countable : Countable layout.
  Proof.
    refine (inj_countable'
      (λ ly, (ly.(ly_size), ly.(ly_align_log)))
      (λ '(sz, a), Layout sz a) _); by intros [].
  Qed.

  Global Instance layout_le : SqSubsetEq layout := λ ly1 ly2,
    (ly1.(ly_size)  ly2.(ly_size))%nat 
    (ly1.(ly_align_log)  ly2.(ly_align_log))%nat.

  Global Instance layout_le_po : PreOrder layout_le.
  Proof.
    split => ?; rewrite /layout_le => *; repeat case_bool_decide => //; lia.
  Qed.

  Definition ly_offset (ly : layout) (n : nat) : layout := {|
    ly_size := ly.(ly_size) - n;
    (* Sadly we need to have the second argument to factor2 as we want
    that if l is aligned to x, then l + n * x is aligned to x for all n
    including 0. *)
    ly_align_log := ly.(ly_align_log) `min` factor2 n ly.(ly_align_log)
  |}.

  Definition ly_set_size (ly : layout) (n : nat) : layout := {|
    ly_size := n;
    ly_align_log := ly.(ly_align_log)
  |}.

  Definition ly_mult (ly : layout) (n : nat) : layout := {|
    ly_size := ly.(ly_size) * n;
    ly_align_log := ly.(ly_align_log)
  |}.

  Definition ly_with_align (sz : nat) (align : nat) : layout := {|
    ly_size := sz;
    ly_align_log := factor2 align 0
  |}.

  Definition layout_wf (ly : layout) : Prop := (ly_align ly | ly.(ly_size)).

  Lemma layout_wf_mod (ly : layout) :
    ly.(ly_size) `mod` ly_align ly = 0  layout_wf ly.
  Proof.
    move => ?. apply Z.mod_divide => //. have ->: 0 = O by [].
    move => /Nat2Z.inj/Nat.pow_nonzero. lia.
  Qed.

  Class LayoutWf (ly : layout) : Prop := layout_wf_wf : layout_wf ly.

  (* Class required because the combinators of layout are made typeclass opaque
     later, so TCEq does not work. *)
  Class LayoutEq (ly1 ly2 : layout) : Prop := layout_eq : ly1 = ly2.
End Layout.
Michael Sammler's avatar
Michael Sammler committed
101
102
103

Arguments ly_size : simpl never.
Arguments sizeof _ /.
104
(*Arguments ly_align_log : simpl never.*)
Michael Sammler's avatar
Michael Sammler committed
105
106
Arguments ly_align : simpl never.

107
108
109
110
111
112
113
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
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
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
Typeclasses Opaque layout_le ly_offset ly_set_size ly_mult ly_with_align.

Hint Extern 0 (LayoutWf _) => refine (layout_wf_mod _ _); done : typeclass_instances.
Hint Extern 0 (LayoutWf _) => unfold LayoutWf; done : typeclass_instances.
Hint Extern 0 (LayoutEq _ _) => exact: eq_refl : typeclass_instances.

(** Representation of an integer type (size and signedness). *)
Section IntType.
  Definition signed := bool.

  Record int_type :=
    IntType {
      it_byte_size_log : nat;
      it_signed : signed;
    }.

  Definition bytes_per_int (it : int_type) : nat :=
    2 ^ it.(it_byte_size_log).

  Lemma bytes_per_int_gt_0 it : bytes_per_int it > 0.
  Proof.
    rewrite /bytes_per_int. move: it => [log ?] /=.
    rewrite Z2Nat_inj_pow. assert (0 < 2%nat ^ log); last lia.
    apply Z.pow_pos_nonneg; lia.
  Qed.

  Definition bits_per_int (it : int_type) : Z :=
    bytes_per_int it * bits_per_byte.

  Definition int_modulus (it : int_type) : Z :=
    2 ^ bits_per_int it.

  Definition int_half_modulus (it : int_type) : Z :=
    2 ^ (bits_per_int it - 1).

  Lemma int_modulus_twice_half_modulus (it : int_type) :
    int_modulus it = 2 * int_half_modulus it.
  Proof.
    rewrite /int_modulus /int_half_modulus.
    rewrite -[X in X * _]Z.pow_1_r -Z.pow_add_r; try f_equal; try lia.
    rewrite /bits_per_int /bytes_per_int.
    apply Z.le_add_le_sub_l. rewrite Z.add_0_r.
    rewrite Z2Nat_inj_pow.
    assert (0 < 2%nat ^ it_byte_size_log it * bits_per_byte); last lia.
    apply Z.mul_pos_pos; last (rewrite /bits_per_byte; lia).
    apply Z.pow_pos_nonneg; lia.
  Qed.

  (* Minimal representable integer. *)
  Definition min_int (it : int_type) : Z :=
    if it.(it_signed) then - int_half_modulus it else 0.

  (* Maximal representable integer. *)
  Definition max_int (it : int_type) : Z :=
    (if it.(it_signed) then int_half_modulus it else int_modulus it) - 1.

  Lemma min_int_le_0 (it : int_type) : min_int it  0.
  Proof.
    have ? := bytes_per_int_gt_0 it. rewrite /min_int /int_half_modulus.
    destruct (it_signed it) => //. trans (- 2 ^ 7) => //.
    rewrite -Z.opp_le_mono. apply Z.pow_le_mono_r => //.
    rewrite /bits_per_int /bits_per_byte. lia.
  Qed.

  Lemma max_int_ge_127 (it : int_type) : 127  max_int it.
  Proof.
    have ? := bytes_per_int_gt_0 it.
    rewrite /max_int /int_modulus /int_half_modulus.
    rewrite /bits_per_int /bits_per_byte.
    have ->: (127 = 2 ^ 7 - 1) by []. apply Z.sub_le_mono => //.
    destruct (it_signed it); apply Z.pow_le_mono_r; lia.
  Qed.

  Global Instance int_elem_of_it : ElemOf Z int_type :=
    λ z it, min_int it  z  max_int it.

  Definition it_layout (it : int_type) :=
    Layout (bytes_per_int it) it.(it_byte_size_log).

  Definition i8  := IntType 0 true.
  Definition u8  := IntType 0 false.
  Definition i16 := IntType 1 true.
  Definition u16 := IntType 1 false.
  Definition i32 := IntType 2 true.
  Definition u32 := IntType 2 false.
  Definition i64 := IntType 3 true.
  Definition u64 := IntType 3 false.

  (* hardcoding 64bit pointers for now *)
  Definition bytes_per_addr_log : nat := 3%nat.
  Definition bytes_per_addr : nat := (2 ^ bytes_per_addr_log)%nat.

  Definition intptr_t  := IntType bytes_per_addr_log false.
  Definition uintptr_t := IntType bytes_per_addr_log true.

  Definition size_t  := intptr_t.
  Definition ssize_t := uintptr_t.
  Definition bool_it := u8.
End IntType.

Michael Sammler's avatar
Michael Sammler committed
207
Declare Scope loc_scope.
Michael Sammler's avatar
Michael Sammler committed
208
209
Delimit Scope loc_scope with L.
Open Scope loc_scope.
210

211
Definition alloc_id := Z.
212
Definition addr := Z.
213

214
Definition loc : Set := alloc_id * addr.
215
216
217
218
219
220
221
222
223
224
225
226
227
228
Bind Scope loc_scope with loc.

Inductive mbyte : Set :=
| MByte (b : byte)
| MPtrFrag (l : loc) (n : nat)
| MPoison.

Definition val : Set := list mbyte.
Bind Scope val_scope with val.

Inductive lock_state := WSt | RSt (n : nat).

Definition heap := gmap loc (lock_state * mbyte).

229
230
231
232
233
234
Record allocation :=
  Allocation {
    alloc_start : Z; (* First valid address. *)
    alloc_end : Z;   (* One-past-the-end address. *)
  }.

235
Definition allocs := gmap alloc_id allocation.
236
237
238



Michael Sammler's avatar
Michael Sammler committed
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
Notation "l +ₗ z" := (shift_loc l%L z%Z)
  (at level 50, left associativity) : loc_scope.
Definition offset_loc (l : loc) (ly : layout) (z : Z) : loc := (l + ly.(ly_size) * z).
Notation "l 'offset{' ly '}ₗ' z" := (offset_loc l%L ly z%Z)
  (at level 50, format "l  'offset{' ly '}ₗ'  z", left associativity) : loc_scope.

Definition aligned_to (l : loc) (n : nat) : Prop := (n | l.2).
Notation "l `aligned_to` n" := (aligned_to l n) (at level 50) : stdpp_scope.
Definition has_layout_loc (l : loc) (ly : layout) : Prop := l `aligned_to` ly_align ly.
Notation "l `has_layout_loc` n" := (has_layout_loc l n) (at level 50) : stdpp_scope.
Definition has_layout_val (v : val) (ly : layout) : Prop := length v = ly.(ly_size).
Notation "v `has_layout_val` n" := (has_layout_val v n) (at level 50) : stdpp_scope.

Arguments aligned_to : simpl never.
(* Arguments aligned_to_log : simpl never. *)
Arguments has_layout_loc : simpl never.
Arguments has_layout_val : simpl never.
257
Typeclasses Opaque aligned_to has_layout_loc has_layout_val.
Michael Sammler's avatar
Michael Sammler committed
258

259
260
261
262
263

(*** Definitions of the language *)
Definition label := string. (* make TC opaque and implement countable and eqdicision *)
Definition var_name := string.

Michael Sammler's avatar
Michael Sammler committed
264
265
266
267
268
269
Inductive op_type : Set :=
| IntOp (i : int_type) | PtrOp.

(* see http://compcert.inria.fr/doc/html/compcert.cfrontend.Cop.html#binary_operation *)
Inductive bin_op : Set :=
| AddOp | SubOp | MulOp | DivOp | ModOp | AndOp | OrOp | XorOp | ShlOp
270
| ShrOp | EqOp | NeOp | LtOp | GtOp | LeOp | GeOp
Michael Sammler's avatar
Michael Sammler committed
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
(* Ptr is the second argument and pffset the first *)
| PtrOffsetOp (ly : layout).

Inductive un_op : Set :=
| NotBoolOp | NotIntOp | NegOp | CastOp (ot : op_type).
Inductive order : Set :=
| ScOrd | Na1Ord | Na2Ord.

Inductive expr :=
| Var (x : var_name)
| Val (v : val)
| UnOp (op : un_op) (ot : op_type) (e : expr)
| BinOp (op : bin_op) (ot1 ot2 : op_type) (e1 e2 : expr)
| Deref (o : order) (ly : layout) (e : expr)
| CAS (ot : op_type) (e1 e2 e3 : expr)
| Concat (es : list expr)
| SkipE (e : expr)
| StuckE (* stuck expression *)
.

(** Note that there is no explicit Fork. Instead the initial state can
contain multiple threads (like a processor which has a fixed number of
hardware threads). *)
Inductive stmt :=
295
| Goto (b : label)
Michael Sammler's avatar
Michael Sammler committed
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
| Return (e : expr)
(* m: map from values of e to indices into bs, def: default *)
| Switch (it : int_type) (e : expr) (m : gmap Z nat) (bs : list stmt) (def : stmt)
| Assign (o : order) (ly : layout) (e1 e2 : expr) (s : stmt)
| Call (ret : var_name) (f : expr) (args : list expr) (s : stmt)
| SkipS (s : stmt)
| StuckS (* stuck statement *)
| ExprS (e : expr) (s : stmt)
.

Arguments Switch _%E _%E _%E.
Arguments Call _%E _%E _%E _%E.

Record function := {
  f_args : list (var_name * layout);
  f_local_vars : list (var_name * layout);
  (* TODO should we add this: f_ret : layout; ?*)
313
314
  f_code : gmap label stmt;
  f_init : label;
Michael Sammler's avatar
Michael Sammler committed
315
316
317
318
319
}.

(* TODO: put both function and bytes in the same heap or make pointers disjoint (current version is wrong)*)
Record state := {
  st_heap: heap;
320
  st_allocs: allocs;
Michael Sammler's avatar
Michael Sammler committed
321
  st_fntbl: gmap loc function;
322
  st_alloc_failure: bool;
Michael Sammler's avatar
Michael Sammler committed
323
324
}.

325
326
327
328
Definition st_set_alloc_failure (σ : state) : state :=
  {| st_heap := σ.(st_heap); st_allocs := σ.(st_allocs);
     st_fntbl := σ.(st_fntbl); st_alloc_failure := true; |}.

Michael Sammler's avatar
Michael Sammler committed
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
Record runtime_function := {
  (* locations of args and local vars are substitued in the body *)
  rf_fn : function;
  (* locations in the stack frame (locations of arguments and local
  vars allocated on Call, need to be freed by Return) *)
  rf_locs: list (loc * layout);
  (* current statement *)
  rf_stmt: stmt;
}.

Record continuation := {
  c_rfn: runtime_function;
  (* name of the variable in which the result should be returned *)
  c_rvar: var_name;
  (* TODO should we add this: c_rlayout: layout; ?*)
}.

Record thread_state := {
  ts_rfn: runtime_function;
  ts_conts: list continuation;
349
  ts_alloc_failure: bool;
Michael Sammler's avatar
Michael Sammler committed
350
351
}.

352
353
354
355
356
357
358
Definition set_alloc_failure (ts : thread_state) : thread_state :=
  {| ts_rfn := ts.(ts_rfn); ts_conts := ts.(ts_conts); ts_alloc_failure := true; |}.

Inductive val_or_alloc_failure :=
  | VOAF_val (v: val)
  | VOAF_fail (s : stmt) (ks: list continuation).

Michael Sammler's avatar
Michael Sammler committed
359
360
361
362
(* values for statements *)
Record stmt_val := {
  sv_fn : function;
  sv_locs: list (loc * layout);
363
  sv_val_or_alloc_failure: val_or_alloc_failure;
Michael Sammler's avatar
Michael Sammler committed
364
365
366
367
368
369
370
371
372
}.

Implicit Type (l : loc) (e : expr) (v : val) (sz : nat) (h : heap) (σ : state) (ly : layout) (s : stmt) (sgn : signed) (rf : runtime_function) (ts : thread_state) (co : continuation).

(*** Relating val to logical values *)
(* we use little endian *)
Fixpoint val_to_int_go v : option Z :=
match v with
| [] => Some 0
373
| (MByte b)::v' => z  val_to_int_go v'; Some (byte_modulus * z + b.(byte_val))
Michael Sammler's avatar
Michael Sammler committed
374
375
376
| _ => None
end.
Definition val_to_int (v : val) (it : int_type) : option Z :=
377
378
  if decide (length v = bytes_per_int it) then
    z  val_to_int_go v; if it.(it_signed) && bool_decide (int_half_modulus it  z) then Some (z - int_modulus it) else Some z
Michael Sammler's avatar
Michael Sammler committed
379
380
381
382
383
  else None.

Program Fixpoint val_of_int_go (n : Z) sz : val :=
  match sz return _ with
  | O => []
384
  | S sz' => (MByte ({| byte_val := (n `mod` byte_modulus) |}))::(val_of_int_go (n / byte_modulus) sz')
Michael Sammler's avatar
Michael Sammler committed
385
  end.
386
Next Obligation. move => n. have [] := Z_mod_lt n byte_modulus => //*. lia. Qed.
Michael Sammler's avatar
Michael Sammler committed
387
388

Definition val_of_int (z : Z) (it : int_type) : option val :=
389
390
391
  if bool_decide (z  it) then
    let p := if bool_decide (z < 0) then z + int_modulus it else z in
    Some (val_of_int_go p (bytes_per_int it))
Michael Sammler's avatar
Michael Sammler committed
392
393
394
395
396
397
398
399
  else
    None.

Lemma val_of_int_go_length z sz :
  length (val_of_int_go z sz) = sz.
Proof. elim: sz z => //= ? IH ?. by f_equal. Qed.

Lemma val_to_of_int_go z sz :
400
  0  z < 2 ^ (sz * bits_per_byte) 
Michael Sammler's avatar
Michael Sammler committed
401
402
  val_to_int_go (val_of_int_go z sz) = Some z.
Proof.
403
  rewrite /bits_per_byte.
Michael Sammler's avatar
Michael Sammler committed
404
  elim: sz z => /=. 1: rewrite /Z.of_nat; move => ??; f_equal; lia.
405
  move => sz IH z [? Hlt]. rewrite IH /byte_modulus /= -?Z_div_mod_eq //.
Michael Sammler's avatar
Michael Sammler committed
406
407
408
409
410
411
  split. apply Z_div_pos => //. apply Zdiv_lt_upper_bound => //.
  rewrite Nat2Z.inj_succ -Zmult_succ_l_reverse Z.pow_add_r // in Hlt.
  lia.
Qed.

Lemma val_of_int_length z it v:
412
  val_of_int z it = Some v  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
413
414
415
Proof. rewrite /val_of_int => Hv. case_bool_decide => //. simplify_eq. by rewrite val_of_int_go_length. Qed.

Lemma val_to_int_length v it z:
416
  val_to_int v it = Some z  length v = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
417
418
419
Proof. rewrite /val_to_int. by case_decide. Qed.

Lemma val_of_int_is_some it z:
420
  z  it  is_Some (val_of_int z it).
Michael Sammler's avatar
Michael Sammler committed
421
422
423
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_of_int_in_range it z v:
424
  val_of_int z it = Some v  z  it.
Michael Sammler's avatar
Michael Sammler committed
425
426
427
Proof. rewrite /val_of_int. case_bool_decide; by eauto. Qed.

Lemma val_to_of_int z it v:
428
  val_of_int z it = Some v  val_to_int v it = Some z.
Michael Sammler's avatar
Michael Sammler committed
429
430
Proof.
  rewrite /val_of_int /val_to_int => Ht.
431
432
433
434
  destruct (bool_decide (z  it)) eqn: Hr => //. simplify_eq.
  move: Hr => /bool_decide_eq_true[Hm HM].
  have Hlen := bytes_per_int_gt_0 it.
  rewrite /max_int in HM. rewrite /min_int in Hm.
Michael Sammler's avatar
Michael Sammler committed
435
  rewrite val_of_int_go_length val_to_of_int_go /=.
436
437
438
439
440
441
442
443
444
445
446
447
  - case_decide as H => //. clear H.
    destruct (it_signed it) eqn:Hs => /=.
    + case_decide => /=; last (rewrite bool_decide_false //; lia).
      rewrite bool_decide_true; [f_equal; lia|].
      rewrite int_modulus_twice_half_modulus. move: Hm HM.
      generalize (int_half_modulus it). move => n Hm HM. lia.
    + rewrite bool_decide_false //. lia.
  - case_bool_decide as Hneg; case_match; split; try lia.
    + rewrite int_modulus_twice_half_modulus. lia.
    + rewrite /int_modulus /bits_per_int. lia.
    + rewrite /int_half_modulus in HM.
      transitivity (2 ^ (bits_per_int it -1)); first lia.
448
      rewrite /bits_per_int /bytes_per_int /bits_per_byte /=.
449
450
      apply Z.pow_lt_mono_r; try lia.
    + rewrite /int_modulus /bits_per_int in HM. lia.
Michael Sammler's avatar
Michael Sammler committed
451
452
Qed.

453
454
455
456
457
458
459
460
461
Lemma it_in_range_mod n it:
  n  it  it_signed it = false 
  n `mod` int_modulus it = n.
Proof.
  move => [??] ?. rewrite Z.mod_small //.
  destruct it as [? []] => //. unfold min_int, max_int in *. simpl in *.
  lia.
Qed.

Michael Sammler's avatar
Michael Sammler committed
462
463
Fixpoint val_to_loc_go (v : val) (pos : nat) (l : loc) : option loc :=
  match v with
464
  | (MPtrFrag l' pos')::v' =>
Michael Sammler's avatar
Michael Sammler committed
465
    if bool_decide (pos = pos'  l = l') then
466
      if bool_decide (pos = bytes_per_addr - 1)%nat then (if v' is [] then Some l else None) else val_to_loc_go v' (S pos) l
Michael Sammler's avatar
Michael Sammler committed
467
468
469
470
471
    else None
  | _ => None
  end.
Definition val_to_loc (v : val) : option loc :=
  match v with
472
  | (MPtrFrag l 0)::v' => val_to_loc_go v' 1%nat l
Michael Sammler's avatar
Michael Sammler committed
473
474
  | _ => None
  end.
475
Definition val_of_loc (l : loc) : val := MPtrFrag l <$> seq 0 bytes_per_addr.
Michael Sammler's avatar
Michael Sammler committed
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491

Lemma val_to_of_loc l :
  val_to_loc (val_of_loc l) = Some l.
Proof. simpl. by case_decide. Qed.

Lemma val_of_to_loc v l :
  val_to_loc v = Some l  v = val_of_loc l.
Proof.
  destruct v => //=; case_match => //; case_match => //.
  repeat (match goal with
  | |- context [ val_to_loc_go ?v _ _ ] => destruct v
          end => //=;
                  case_match => //; repeat (case_decide; subst => //=)).
  by case_match => // [[->]].
Qed.

492
Definition i2v (n : Z) (it : int_type) : val := default [MPoison] (val_of_int n it).
Michael Sammler's avatar
Michael Sammler committed
493
494
495
496
497
498
499

Definition val_of_bool (b : bool) : val := i2v (Z_of_bool b) bool_it.

Lemma val_of_int_bool b it:
  val_of_int (Z_of_bool b) it = Some (i2v (Z_of_bool b) it).
Proof.
  have [|? Hv] := val_of_int_is_some it (Z_of_bool b); last by rewrite /i2v Hv.
500
501
  rewrite /elem_of /int_elem_of_it.
  have ? := min_int_le_0 it. have ? := max_int_ge_127 it.
Michael Sammler's avatar
Michael Sammler committed
502
503
504
  split; destruct b => /=; lia.
Qed.

Michael Sammler's avatar
Michael Sammler committed
505
Lemma i2v_bool_length b it:
506
  length (i2v (Z_of_bool b) it) = bytes_per_int it.
Michael Sammler's avatar
Michael Sammler committed
507
508
509
510
511
Proof. by have /val_of_int_length -> := val_of_int_bool b it. Qed.
Lemma i2v_bool_Some b it:
  val_to_int (i2v (Z_of_bool b) it) it = Some (Z_of_bool b).
Proof. apply val_to_of_int. apply val_of_int_bool. Qed.

Michael Sammler's avatar
Michael Sammler committed
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
Arguments val_to_int : simpl never.
Arguments val_of_int : simpl never.
Arguments val_to_loc : simpl never.
Arguments val_of_loc : simpl never.
Typeclasses Opaque val_to_loc val_of_loc val_to_int val_of_int val_of_bool.


Lemma val_to_int_bool b :
  val_to_int (val_of_bool b) bool_it = Some (Z_of_bool b).
Proof. by destruct b. Qed.

(*** Properties of layouts and alignment *)
Lemma ly_align_log_ly_align_eq_iff ly1 ly2:
  ly_align_log ly1 = ly_align_log ly2  ly_align ly1 = ly_align ly2.
Proof. rewrite /ly_align. split; first naive_solver. move => /Nat.pow_inj_r. lia. Qed.

Lemma ly_align_ly_with_align m n :
  ly_align (ly_with_align m n) = keep_factor2 n 1.
Proof. rewrite /ly_with_align/keep_factor2/factor2. by destruct (factor2' n). Qed.

Lemma ly_align_ly_offset ly n :
  ly_align (ly_offset ly n) = (ly_align ly `min` keep_factor2 n (ly_align ly))%nat.
Proof.
  rewrite /ly_align/keep_factor2/=/factor2. destruct (factor2' n) as [n'|] => /=; last by rewrite !Nat.min_id.
  destruct (decide (ly_align_log ly  n'))%nat;[rewrite !min_l|rewrite !min_r]; try lia;
    apply Nat.pow_le_mono_r; lia.
Qed.

Lemma ly_align_ly_set_size ly n:
  ly_align (ly_set_size ly n) = ly_align ly.
Proof. done. Qed.

Lemma ly_with_align_aligned_to l m n:
  l `aligned_to` n 
  is_power_of_two n 
  l `has_layout_loc` ly_with_align m n.
Proof. move => ??. by rewrite /has_layout_loc ly_align_ly_with_align keep_factor2_is_power_of_two. Qed.

Lemma has_layout_loc_trans l ly1 ly2 :
  l `has_layout_loc` ly2  (ly1.(ly_align_log)  ly2.(ly_align_log))%nat  l `has_layout_loc` ly1.
Proof. rewrite /has_layout_loc/aligned_to => Hl ?. etrans;[|by apply Hl]. by apply Zdivide_nat_pow. Qed.

Lemma has_layout_loc_1 l ly:
  ly_align ly = 1%nat 
  l `has_layout_loc` ly.
Proof. rewrite /has_layout_loc =>  ->. by apply Z.divide_1_l. Qed.

Lemma has_layout_ly_offset l (n : nat) ly:
  l `has_layout_loc` ly 
  (l + n) `has_layout_loc` ly_offset ly n.
Proof.
  move => Hl. apply Z.divide_add_r.
  - apply: has_layout_loc_trans => //. rewrite {1}/ly_align_log/=. destruct n; lia.
  - rewrite/ly_offset. destruct n;[by subst;apply Z.divide_0_r|]. etrans;[apply Zdivide_nat_pow, Min.le_min_r|]. by apply factor2_divide.
Qed.

Lemma has_layout_loc_ly_mult_offset l ly n:
  layout_wf ly 
  l `has_layout_loc` ly_mult ly (S n) 
  (l + ly_size ly) `has_layout_loc` ly_mult ly n.
Proof. move => ??. rewrite /ly_mult. by apply Z.divide_add_r. Qed.


Lemma aligned_to_offset l n off :
  l `aligned_to` n  (n | off)  (l + off) `aligned_to` n.
Proof. apply Z.divide_add_r. Qed.

Lemma aligned_to_add l (n : nat) x:
  (l + x * n) `aligned_to` n  l `aligned_to` n.
Proof.
582
  unfold aligned_to. destruct l => /=. rewrite Z.add_comm.
Michael Sammler's avatar
Michael Sammler committed
583
584
585
586
587
588
589
590
  split.
  - apply: Z.divide_add_cancel_r. by apply Z.divide_mul_r.
  - apply Z.divide_add_r. by apply Z.divide_mul_r.
Qed.

Lemma aligned_to_mult_eq l n1 n2 off:
  l `aligned_to` n2  (l + off) `aligned_to` (n1 * n2)  (n2 | off).
Proof.
591
  unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
Michael Sammler's avatar
Michael Sammler committed
592
593
594
595
596
  apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
Qed.

(*** Helper functions for accessing the heap *)

597
598
599
600
(* The address range between [l] and [l +ₗ n] (included) is in range of the
   allocation that contains [l]. Note that we consider the 1-past-the-end
   pointer to be in range of an allocation. *)
Definition heap_loc_in_bounds (l : loc) (n : nat) (st : state) : Prop :=
601
   alloc, st.(st_allocs) !! l.1 = Some alloc 
602
603
604
           alloc.(alloc_start)  l.2 
           l.2 + n  alloc.(alloc_end).

Michael Sammler's avatar
Michael Sammler committed
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
Fixpoint heap_at_go l v flk h : Prop :=
  match v with
  | [] => True
  | b::v' => ( lk, h !! l = Some (lk, b)  flk lk)  heap_at_go (l + 1) v' flk h
  end.

Definition heap_at l ly v flk h : Prop :=
  l `has_layout_loc` ly  v `has_layout_val` ly  heap_at_go l v flk h.

Definition heap_block_free h l : Prop :=  i, h !! (l + i) = None.

Fixpoint heap_upd l v flk h : heap :=
  match v with
  | b::v' => partial_alter (λ m, Some (flk (fst <$> m), b)) l (heap_upd (l + 1) v' flk h)
  | [] => h
  end.

Fixpoint heap_upd_list ls vs flk h : heap :=
  match ls, vs with
  | l::ls', v::vs' => heap_upd l v flk (heap_upd_list ls' vs' flk h)
  | _, _ => h
  end.

Fixpoint heap_free l n h : heap :=
  match n with
  | O => h
  | S n' => delete l (heap_free (l + 1) n' h)
  end.

Fixpoint heap_free_list ls h : heap :=
  match ls with
  | (l, ly)::ls' => heap_free l ly.(ly_size) (heap_free_list ls' h)
  | _ => h
  end.

Definition update_stmt ts s := {|
  ts_conts := ts.(ts_conts);
  ts_rfn := {| rf_fn := ts.(ts_rfn).(rf_fn); rf_stmt := s; rf_locs := ts.(ts_rfn).(rf_locs) |};
643
  ts_alloc_failure := ts.(ts_alloc_failure);
Michael Sammler's avatar
Michael Sammler committed
644
645
646
647
648
|}.

Definition heap_fmap f σ := {|
  st_heap := f σ.(st_heap);
  st_fntbl := σ.(st_fntbl);
649
650
  st_allocs := σ.(st_allocs);
  st_alloc_failure := σ.(st_alloc_failure);
Michael Sammler's avatar
Michael Sammler committed
651
652
653
654
655
656
657
658
659
|}.

Definition to_val (e : expr) : option val :=
  match e with
  | Val v => Some v
  | _ => None
  end.

Definition stmt_to_val (ts : thread_state) : option stmt_val :=
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
  if ts.(ts_alloc_failure) then
    Some {| sv_fn := ts.(ts_rfn).(rf_fn);
            sv_locs := ts.(ts_rfn).(rf_locs);
            sv_val_or_alloc_failure := VOAF_fail ts.(ts_rfn).(rf_stmt) ts.(ts_conts) |}
  else
    match ts.(ts_rfn).(rf_stmt), ts.(ts_conts) with
    | Return (Val v), [] => Some {| sv_fn := ts.(ts_rfn).(rf_fn);
                                    sv_locs := ts.(ts_rfn).(rf_locs);
                                    sv_val_or_alloc_failure := VOAF_val v |}
    | _             , _  => None
    end.

Definition stmt_of_val (sv : stmt_val) : thread_state :=
  match sv.(sv_val_or_alloc_failure) with
  | VOAF_val v => {|
      ts_rfn := {| rf_stmt := Return (Val v);
                   rf_locs := sv.(sv_locs);
                   rf_fn := sv.(sv_fn); |};
      ts_conts := [];
      ts_alloc_failure := false;
    |}
  | VOAF_fail s ks => {|
      ts_rfn := {| rf_stmt := s;
                   rf_locs := sv.(sv_locs);
                   rf_fn := sv.(sv_fn); |};
      ts_conts := ks;
      ts_alloc_failure := true;
    |}
Michael Sammler's avatar
Michael Sammler committed
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
  end.

(*** Evaluation of operations *)
(** Checks that the location [l] is allocated on the heap [h] *)
Definition valid_ptr l h : Prop :=
  is_Some (h !! l).
(** Checks whether location [l] is a weak valid pointer in heap [h].
[Some true] means [l] is a valid in bounds pointer, [Some false] means
[l] is a end of block pointer, [None] means [l] is not a valid pointer. *)
Definition weak_valid_ptr l h : option bool :=
  if decide (valid_ptr l h) then
    Some true
  else if decide (valid_ptr (l + -1) h  ¬valid_ptr l h) then
    Some false
  else None.
(** Checks equality between [l1] and [l2]. See
http://compcert.inria.fr/doc/html/compcert.common.Values.html#Val.cmplu_bool
*)
Definition ptr_eq l1 l2 h : option bool :=
  eob1  weak_valid_ptr l1 h;
  eob2  weak_valid_ptr l2 h;
  if decide (l1.1 = l2.2) then
    Some (bool_decide (l1 = l2))
  else
    if eob1 || eob2 then None else Some false.

(* evaluation can be non-deterministic for comparing pointers *)
(* TODO: implement *)
716
717
Inductive eval_bin_op : bin_op  op_type  op_type  state  val  val  val  Prop :=
| AddOpPI v1 v2 σ o l:
Michael Sammler's avatar
Michael Sammler committed
718
719
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some o 
720
721
    eval_bin_op AddOp PtrOp (IntOp size_t) σ v1 v2 (val_of_loc (l + o))
| PtrOffsetOpIP v1 v2 σ o l ly it:
Michael Sammler's avatar
Michael Sammler committed
722
723
724
725
    val_to_int v1 it = Some o 
    val_to_loc v2 = Some l 
    (* TODO: should we have an alignment check here? *)
    0  o 
726
727
728
    eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly} o))
| EqOpPNull v1 v2 σ l v:
    heap_loc_in_bounds l 0%nat σ 
Michael Sammler's avatar
Michael Sammler committed
729
730
731
732
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some 0 
    (* TODO ( see below ): Should we really hard code i32 here because of C? *)
    i2v (Z_of_bool false) i32 = v 
733
734
735
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
    heap_loc_in_bounds l 0%nat σ 
Michael Sammler's avatar
Michael Sammler committed
736
737
738
    val_to_loc v1 = Some l 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
739
740
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
741
742
743
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool true) i32 = v 
744
745
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
Michael Sammler's avatar
Michael Sammler committed
746
747
748
    val_to_int v1 size_t = Some 0 
    val_to_int v2 size_t = Some 0 
    i2v (Z_of_bool false) i32 = v 
749
750
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpPP v1 v2 σ l1 l2 v b:
Michael Sammler's avatar
Michael Sammler committed
751
752
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
753
    ptr_eq l1 l2 σ.(st_heap) = Some b 
Michael Sammler's avatar
Michael Sammler committed
754
    i2v (Z_of_bool b) i32 = v 
755
756
    eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPP v1 v2 σ l1 l2 v b:
Michael Sammler's avatar
Michael Sammler committed
757
758
    val_to_loc v1 = Some l1 
    val_to_loc v2 = Some l2 
759
    ptr_eq l1 l2 σ.(st_heap) = Some b 
Michael Sammler's avatar
Michael Sammler committed
760
    i2v (Z_of_bool (negb b)) i32 = v 
761
762
    eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| RelOpII op v1 v2 σ n1 n2 it b:
Michael Sammler's avatar
Michael Sammler committed
763
764
765
766
767
768
769
770
771
772
773
774
775
    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 
    val_to_int v1 it = Some n1 
    val_to_int v2 it = Some n2 
    (* TODO: What is the right int type of the result here? C seems to
    use i32 but maybe we don't want to hard code that. *)
776
777
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
| ArithOpII op v1 v2 σ n1 n2 it n v:
Michael Sammler's avatar
Michael Sammler committed
778
779
780
781
782
783
784
785
786
    match op with
    | AddOp => Some (n1 + n2)
    | SubOp => Some (n1 - n2)
    | MulOp => Some (n1 * n2)
    (* we need to take `quot` and `rem` here for the correct rounding
    behavior, i.e. rounding towards 0 (instead of `div` and `mod`,
    which round towards floor)*)
    | DivOp => if n2 is 0 then None else Some (n1 `quot` n2)
    | ModOp => if n2 is 0 then None else Some (n1 `rem` n2)
787
    (* TODO: Figure out if these are the operations we want and what sideconditions they have *)
Michael Sammler's avatar
Michael Sammler committed
788
789
790
791
792
793
794
795
796
    | 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 
    val_to_int v1 it = Some n1 
    val_to_int v2 it = Some n2 
797
    val_of_int (if it_signed it then n else n `mod` int_modulus it) it = Some v 
798
    eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
Michael Sammler's avatar
Michael Sammler committed
799
800
801
.


802
803
Inductive eval_un_op : un_op  op_type  state  val  val  Prop :=
| CastOpII itt its σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
804
805
    val_to_int vs its = Some n 
    val_of_int n itt = Some vt 
806
807
    eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
Michael Sammler's avatar
Michael Sammler committed
808
809
    val_to_loc vs = Some l 
    val_of_loc l = vt 
810
811
    eval_un_op (CastOp PtrOp) PtrOp σ vs vt
| NegOpI it σ vs vt n:
Michael Sammler's avatar
Michael Sammler committed
812
813
    val_to_int vs it = Some n 
    val_of_int (-n) it = Some vt 
814
    eval_un_op NegOp (IntOp it) σ vs vt
Michael Sammler's avatar
Michael Sammler committed
815
816
817
818
819
820
821
822
.

(*** Evaluation of Expressions *)

Inductive expr_step : expr  state  list Empty_set  expr  state  list expr  Prop :=
| SkipES v σ:
    expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
823
    eval_un_op op ot σ v v' 
Michael Sammler's avatar
Michael Sammler committed
824
825
    expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
826
    eval_bin_op op ot1 ot2 σ v1 v2 v' 
Michael Sammler's avatar
Michael Sammler committed
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
    expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
| DerefS o v l ly v' σ:
    let start_st st :=  n, st = if o is Na2Ord then RSt (S n) else RSt n in
    let end_st st := match o, st with
                     | Na1Ord, Some (RSt n) => RSt (S n)
                     | Na2Ord, Some (RSt (S n)) => RSt n
                     | ScOrd, Some st => st
                     (* unreachable *)
                     |  _, _ => WSt end in
    let end_expr := if o is Na1Ord then Deref Na2Ord ly (Val v) else Val v' in
    val_to_loc v = Some l 
    heap_at l ly v' start_st σ.(st_heap) 
    expr_step (Deref o ly (Val v)) σ [] end_expr (heap_fmap (heap_upd l v' end_st) σ) []
(* TODO: look at CAS and see whether it makes sense. Also allow
comparing pointers? (see lambda rust) *)
(* corresponds to atomic_compare_exchange_strong, see https://en.cppreference.com/w/c/atomic/atomic_compare_exchange *)
| CasFailS l1 l2 vo ve σ z1 z2 v1 v2 v3 it:
    val_to_loc v1 = Some l1 
    heap_at l1 (it_layout it) vo (λ st,  n, st = RSt n) σ.(st_heap) 
    val_to_loc v2 = Some l2 
    heap_at l2 (it_layout it) ve (λ st, st = RSt 0%nat) σ.(st_heap) 
    val_to_int vo it = Some z1 
    val_to_int ve it = Some z2 
    v3 `has_layout_val` it_layout it 
851
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
852
853
854
855
856
857
858
859
860
861
862
    z1  z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool false)) (heap_fmap (heap_upd l2 vo (λ _, RSt 0%nat)) σ) []
| CasSucS l1 l2 it vo ve σ z1 z2 v1 v2 v3:
    val_to_loc v1 = Some l1 
    heap_at l1 (it_layout it) vo (λ st, st = RSt 0%nat) σ.(st_heap) 
    val_to_loc v2 = Some l2 
    heap_at l2 (it_layout it) ve (λ st,  n, st = RSt n) σ.(st_heap) 
    val_to_int vo it = Some z1 
    val_to_int ve it = Some z2 
    v3 `has_layout_val` it_layout it 
863
    (bytes_per_int it  bytes_per_addr)%nat 
Michael Sammler's avatar
Michael Sammler committed
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
    z1 = z2 
    expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
              (Val (val_of_bool true)) (heap_fmap (heap_upd l1 v3 (λ _, RSt 0%nat)) σ) []
| ConcatS vs σ:
    expr_step (Concat (Val <$> vs)) σ [] (Val (mjoin vs)) σ []
(* no rule for StuckE *)
.

(*** evaluation contexts *)
(** for expressions*)
Inductive ectx_item :=
| UnOpCtx (op : un_op) (ot : op_type)
| BinOpLCtx (op : bin_op) (ot1 ot2 : op_type) (e2 : expr)
| BinOpRCtx (op : bin_op) (ot1 ot2 : op_type) (v1 : val)
| DerefCtx (o : order) (l : layout)
| CASLCtx (ot : op_type) (e2 e3 : expr)
| CASMCtx (ot : op_type) (v1 : val) (e3 : expr)
| CASRCtx (ot : op_type) (v1 v2 : val)
| ConcatCtx (vs : list val) (es : list expr)
| SkipECtx
.

Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
  match Ki with
  | UnOpCtx op ot => UnOp op ot e
  | BinOpLCtx op ot1 ot2 e2 => BinOp op ot1 ot2 e e2
  | BinOpRCtx op ot1 ot2 v1 => BinOp op ot1 ot2 (Val v1) e
  | DerefCtx o l => Deref o l e
  | CASLCtx ot e2 e3 => CAS ot e e2 e3
  | CASMCtx ot v1 e3 => CAS ot (Val v1) e e3
  | CASRCtx ot v1 v2 => CAS ot (Val v1) (Val v2) e
  | ConcatCtx vs es => Concat ((Val <$> vs) ++ e :: es)
  | SkipECtx => SkipE e
  end.

Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
  to_val e1 = None  to_val e2 = None 
  (Val <$> vl1) ++ e1 :: el1 = (Val <$> vl2) ++ e2 :: el2 
  vl1 = vl2  e1 = e2  el1 = el2.
Proof.
  revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
  - done.
  - subst. by inversion H1.
  - subst. by inversion H2.
  - destruct (IHvl1 vl2); auto. split; f_equal; auto.
Qed.

Lemma list_expr_val_eq_false vl1 vl2 e el :
  to_val e = None  Val <$> vl1 = (Val <$> vl2) ++ e :: el  False.
Proof.
  move => He. elim: vl2 vl1 => [[]//=*|v vl2 IH [|??]?]; csimpl in *; simplify_eq; eauto.
Qed.

(** Statements *)
Inductive stmt_ectx :=
(* Assignment is evalutated right to left, otherwise we need to split contexts *)
| AssignRCtx (o : order) (ly : layout) (e1 : expr) (s : stmt)
| AssignLCtx (o : order) (ly : layout) (v2 : val) (s : stmt)
| ReturnCtx
| SwitchCtx (it : int_type) (m: gmap Z nat) (bs : list stmt) (def : stmt)
| CallLCtx (r : var_name) (args : list expr) (s : stmt)
| CallRCtx (r : var_name) (f : val) (vl : list val) (el : list expr) (s : stmt)
| ExprSCtx (s : stmt)
.

Definition stmt_fill (Ki : stmt_ectx) (e : expr) : stmt :=
  match Ki with
  | AssignRCtx o ly e1 s => Assign o ly e1 e s
  | AssignLCtx o ly v2 s => Assign o ly e (Val v2) s
  | ReturnCtx => Return e
  | SwitchCtx it m bs def => Switch it e m bs def
  | CallLCtx r args s => Call r e args s
  | CallRCtx r f vl el s => Call r (Val f) ((Val <$> vl) ++ e :: el) s
  | ExprSCtx s => ExprS e s
  end.

(*** Language instance for expressions *)

Lemma of_to_val e v : to_val e = Some v  Val v = e.
Proof. move: e => []; naive_solver. Qed.

Lemma val_stuck e1 σ1 κ e2 σ2 ef :
  expr_step e1 σ1 κ e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.

Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.

Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.

Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
  to_val e1 = None  to_val e2 = None 
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
Proof.
  move: Ki1 Ki2 => [ ^ Ki1] [ ^Ki2] He1 He2 HEQ //; simplify_eq; try done.
  apply list_expr_val_eq_inv in HEQ; [ by destruct HEQ as (-> & _ & ->) | done | done ].
Qed.

Lemma expr_ctx_step_val Ki e σ1 κ e2 σ2 ef :
  expr_step (fill_item Ki e) σ1 κ e2 σ2 ef  is_Some (to_val e).
Proof.
  destruct Ki; inversion 1; simplify_eq; decompose_Forall_hyps; simplify_option_eq; try by eauto.
  apply not_eq_None_Some; intros ?; by eapply list_expr_val_eq_false.
Qed.

Lemma expr_lang_mixin : EctxiLanguageMixin Val to_val fill_item expr_step.
Proof.
  split => //; eauto using of_to_val, val_stuck, fill_item_inj, fill_item_val, fill_item_no_val_inj, expr_ctx_step_val.
Qed.
Canonical Structure expr_ectxi_lang := EctxiLanguage expr_lang_mixin.
Canonical Structure expr_ectx_lang := EctxLanguageOfEctxi expr_ectxi_lang.
Canonical Structure expr_lang := LanguageOfEctx expr_ectx_lang.

(*** Substitution *)
Fixpoint subst (x : var_name) (v : val) (e : expr)  : expr :=
  match e with
  | Var y => if bool_decide (x = y) then Val v else Var y
  | Val v => Val v
  | UnOp op ot e => UnOp op ot (subst x v e)
  | BinOp op ot1 ot2 e1 e2 => BinOp op ot1 ot2 (subst x v e1) (subst x v e2)
  | Deref o l e => Deref o l (subst x v e)
  | CAS ly e1 e2 e3 => CAS ly (subst x v e1) (subst x v e2) (subst x v e3)
  | Concat el => Concat (subst x v <$> el)
  | SkipE e => SkipE (subst x v e)
  | StuckE => StuckE
  end.

Fixpoint subst_l (xs : list var_name) (vs : list val) (e : expr)  : expr :=
  match xs, vs with
  | x::xs', v::vs' => subst x v (subst_l xs' vs' e)
  | _, _ => e
  end.

Fixpoint subst_stmt (xs : list var_name) (vs : list val) (s : stmt) : stmt :=
  match s with
For faster browsing, not all history is shown. View entire blame