vcg_solver.v 3.77 KB
Newer Older
1 2
From iris_c.vcgen Require Export vcgen.
From iris_c.vcgen Require Import splitenv.
3 4
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
5

6 7 8
Section vcg_continue.
  Context `{amonadG Σ}.

Dan Frumin's avatar
Dan Frumin committed
9 10
  Class FromKnownLocs (Γls : penv) (E_old : known_locs) (E_new : known_locs).
  (*dom Γls ⊂ (elem_of E_old) disj_Union (elem_of E) *)
11 12 13 14 15 16 17 18 19 20 21 22

  Global Instance from_known_locs_Nil E_old:
    FromKnownLocs [] E_old [].

  Global Instance from_known_locs_old_cons Γls E_old E_new x q v l i:
    LocLookup E_old l i 
    FromKnownLocs Γls E_old E_new 
    FromKnownLocs (PenvItem l x q v :: Γls) E_old E_new.

  Global Instance from_known_locs_new_cons Γls E_old E_new x q v l:
    FromKnownLocs Γls E_old E_new 
    FromKnownLocs (PenvItem l x q v :: Γls) E_old (l :: E_new) | 100.
Léon Gondelman 's avatar
Léon Gondelman committed
23

Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27
  Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
    MapstoListFromEnv Γs_in Γs_out Γls 
    E = penv_to_known_locs Γls 
    ListOfMapsto Γls E m 
28
    IntoDCExpr E e de 
29
    dcexpr_wf [] E de 
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31 32
    denv_wf (penv_to_known_locs Γls) m 
    envs_entails (Envs Γp Γs_out c)
      (vcg_wp E m de R (λ E m dv,
33
        mapsto_wand_list E m (Φ (dval_interp E dv))) 1024 (*TODO: Fix this*)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
    envs_entails (Envs Γp Γs_in c) (awp e R Φ).
  Proof.
36
    intros Hsplit ->.
Léon Gondelman 's avatar
Léon Gondelman committed
37
    rewrite /ListOfMapsto. intros Hpenv -> Hwf Hmwf Hgoal.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39
    eapply tac_envs_split_mapsto; try eassumption.
    revert Hgoal. rewrite environments.envs_entails_eq.
Léon Gondelman 's avatar
Léon Gondelman committed
40
    rewrite (vcg_wp_correct R); try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43 44
    iIntros (->) "H1 H2".
    iSpecialize ("H2" with "H1"). iApply (awp_wand with "H2").
    iIntros (v). iDestruct 1 as (E' dv m' Hpre) "(% & % & % & Hm & Hwp)".
    rewrite Hpre.
Léon Gondelman 's avatar
Léon Gondelman committed
45
    rewrite mapsto_wand_list_spec. iApply ("Hwp" with "Hm").
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48
  Qed.

  Lemma tac_exists_known_locs Γs_in Γs_out Γls Γp c ps v dv E_old E_new (Φ: known_locs  denv  dval  iProp Σ):
49 50 51
    MapstoListFromEnv Γs_in Γs_out Γls 
    FromKnownLocs Γls E_old E_new 
    ListOfMapsto Γls (E_old ++ E_new) ps 
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54 55
    IntoDVal (E_old ++ E_new) v dv 
    denv_wf (E_old ++ E_new) ps 
    envs_entails (Envs Γp Γs_out c) (Φ (E_old ++ E_new) ps dv) 
    envs_entails (Envs Γp Γs_in c) (vcg_wp_continuation E_old Φ v).
56 57
  Proof.
    intros Hsplit. rewrite /ListOfMapsto environments.envs_entails_eq=> Hexhale.
58
    unfold of_envs. simpl. intros HGls [-> ?] ? Hgoal.
59 60
    rewrite mapsto_list_from_env.
    iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63 64 65 66 67 68 69
    iExists (E_old ++ E_new), dv, ps.
    repeat iSplit; eauto using prefix_app_r. iSplitL "Hls".
    { by iApply HGls. }
    iApply Hgoal. iIntros "{$Hp $Hs} !%". split; eauto.
    + apply Hwf.
    + apply Hsplit. apply Hwf.
    + intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
      * by left.
      * right. by apply Hsplit.
70 71
  Qed.
End vcg_continue.
72

Robbert Krebbers's avatar
Robbert Krebbers committed
73
Arguments vcg_wp_continuation {_ _ _ _}.
74

75 76 77 78 79 80 81
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;
82
  [ apply _              (* Separate the - ↦ - propositions out of the context*)
83
  | simpl; reflexivity   (* Compute the known locations *)
84 85
  | apply _              (* Compute the symbolic environment based on known locations *)
  | apply _              (* Reify the expression *)
Léon Gondelman 's avatar
Léon Gondelman committed
86
  | vm_compute[reflexivity]; try done (* Prove that the reified expression is well-formed *)
87
  | done                 (* Prove that the environment is well-formed  *)
Dan Frumin's avatar
Dan Frumin committed
88
  | simpl; simpl_subst ].
89 90 91 92 93 94

Ltac vcg_continue :=
  eapply tac_exists_known_locs;
  [ apply _  (* MapstoListFromEnv Γs_in Γs_out Γls *)
  | apply _  (* FromKnownLocs Γls E_old E_new *)
  | apply _  (* ListOfMapsto Γls (E_old ++ E_new) ps *)
Robbert Krebbers's avatar
Robbert Krebbers committed
95
  | apply _  (* IntoDVal (E_old ++ E_new) v dv *)
96
  | done     (* ps is well-formed *)
97
  | simpl; simpl_subst ].