Commit 642186f8 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

add the vcg_wp_unknown function (which is never simplified)

parent 9be882d3
......@@ -8,9 +8,10 @@ From iris_c.lib Require Import locking_heap U.
(*
TODO
- Fix all the unknown cases, introduce a function for that (which should be
[DONE] Fix all the unknown cases, introduce a function for that (which should be
simpl never)
- Write more tests with unknown stuff in it
add tests like `!(l := 10;;;; l)`
- Support alloc in `vcg_wp`
- Automatically come up with the new `E`, `m` and `dv` and stuff in the
unknown case
......@@ -96,9 +97,6 @@ Section vcg.
Definition mapsto_wand_list (m : denv) (Φ : wp_expr) : wp_expr :=
mapsto_wand_list_aux m Φ O.
(*
TODO: add to tests fine: `!(l := 10;;;; l)`
*)
Fixpoint vcg_sp (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
match de with
| dCRet dv => Some (m, nil, dv)
......@@ -133,7 +131,7 @@ Section vcg.
| dCAlloc _ | dCUnknown _ => None
end.
(* TODO: change the fail though cases, in the same way as the unknown case
(* TODO: change the fail though cases, in the same way as the unknown case
of vcg_wp. Also factor that out in a function vcg_unknown *)
Definition vcg_wp_load (E : known_locs) (dv : dval) (m : denv)
(Φ : denv dval wp_expr) : wp_expr :=
......@@ -234,23 +232,21 @@ Section vcg_spec.
Context `{amonadG Σ}.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof. (*
Proof.
generalize dependent E.
induction a.
- done.
- simpl. iIntros (E) "He". iDestruct "He" as (q v) "[H1 H2]".
iExists q, (dValUnknown v).
iFrame. by (iApply H0).
iExists q, (dValUnknown v). iFrame. by (iApply H0).
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists (dValUnknown v). simpl. iFrame.
- simpl. iIntros (E) "(He & H)". iFrame. by iApply IHa.
iExists (dValUnknown v). simpl. iFrame. by (iApply H0).
- simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists v. iFrame. by iApply H0.
- simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
- simpl. intros E. by apply U_mono.
Qed. *) Admitted.
Qed.
(*
Lemma mapsto_star_list_spec E m t :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment