vcg_solver.v 1015 Bytes
Newer Older
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
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
From iris_c.c_translation Require Import monad translation proofmode notation.
From iris_c.lib Require Import locking_heap U.

Arguments vcg_wp_unknown : simpl never.
(* TODO: How to avoid computing mapsto_wand and dloc under vcg_wp_unknown ? *)
(* Arguments dloc_interp : simpl never. *)
Declare Reduction vcg_cbv := cbv [ vcg_wp vcg_wp_bin_op vcg_wp_store vcg_wp_load mapsto_wand_list].

Ltac vcg_compute :=
  match goal with
    |- ?u => let v := eval vcg_cbv in u in change v
  end.

Ltac vcg_solver :=
  eapply tac_vcg_sound;
  [ apply _    (*  MapstoListFromEnv Γs_in Γs_out Γls *)
  | compute; reflexivity (*  E = penv_to_known_locs Γls *)
  |       (* dcexpr_wf E de *)
  |       (* denv_wf E m *)
  | apply _ (* ListOfMapsto Γls E m *)
  | apply _ (* IntoDCexpr E e dce *)
  | vcg_compute; simpl ]; intuition.