...
 
Commits (22)
*.vo
*.vio
*.v.d
*.vok
*.vos
.Makefile.coq.d
.coqdeps.d
*.glob
*.cache
......
......@@ -27,24 +27,14 @@ variables:
## Build jobs
build-coq.dev:
build-coq.8.10.1:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
OPAM_PINS: "coq version 8.10.1"
build-iris.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
except:
only:
......
All files in this development are distributed under the terms of the BSD
license, included below.
------------------------------------------------------------------------------
Copyright: Iris-C developers and contributors
BSD LICENCE
------------------------------------------------------------------------------
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
......@@ -12,17 +12,17 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
* Neither the name of the copyright holder nor the names of its contributors
may be used to endorse or promote products derived from this software
without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
......@@ -9,7 +9,7 @@ all: Makefile.coq
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq
rm -f Makefile.coq .lia.cache
.PHONY: clean
# Create Coq Makefile.
......@@ -29,14 +29,8 @@ build-dep: build-dep/opam phony
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything itself.
@echo "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
......@@ -7,6 +7,8 @@
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/lib/list.v
theories/lib/mset.v
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-28.2.5b3f7de1") | (= "dev") }
"coq-iris" { (= "dev.2020-04-04.2.c2367a65") | (= "dev") }
]
......@@ -129,7 +129,8 @@ Section cwp_rules.
iIntros (γ env l I) "#Hflock Hres #Heq".
iMod (flock_res_alloc_cofinite _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
pose (I' := <[ρ:=(1%Qp,R1)]>I).
assert (I !! ρ = None) by by eapply not_elem_of_dom.
assert (I !! ρ = None)
by (by eapply (not_elem_of_dom (D:=gset lock_res_gname))).
iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
{ rewrite /flock_resources /I'.
rewrite big_sepM_insert //. iFrame. }
......@@ -210,7 +211,7 @@ Section cwp_rules.
iIntros (γ env l I) "#Hlock1 Hres #Heq1". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq1" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
......@@ -244,7 +245,7 @@ Section cwp_rules.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
wp_apply (acquire_flock_spec with "[$]").
iIntros "Hfl".
iMod (flocked_inv_open with "Hfl") as "[HI Hcl]"; first done.
iMod (flocked_inv_acc with "Hfl") as "[HI Hcl]"; first done.
iRewrite "Heq" in "HI".
iDestruct "HI" as "[Henv HR]".
wp_pures; simpl.
......
......@@ -62,7 +62,7 @@ Tactic Notation "cwp_pure" open_constr(efoc) :=
eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
[tac_bind_helper (* e = fill K e' *)
|apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|try solve_vals_compare_safe (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|simpl
])
......
This diff is collapsed.
......@@ -212,7 +212,7 @@ Lemma to_heap_block_info_valid τ : ✓ to_heap_block_info τ.
Proof. intros l. rewrite lookup_fmap. by destruct (τ !! l) as [[]|]. Qed.
Lemma locking_heap_init `{locking_heapPreG Σ, !heapG Σ} :
(|==> _ : locking_heapG Σ, full_locking_heap )%I.
|==> _ : locking_heapG Σ, full_locking_heap .
Proof.
iMod (own_alloc ( to_locking_heap )) as (γ1) "Hh1".
{ by apply auth_auth_valid. }
......@@ -323,9 +323,6 @@ Section properties.
Qed.
Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.
Lemma cloc_to_val_for_compare cl :
val_for_compare (cloc_to_val cl) = cloc_to_val cl.
Proof. rewrite /cloc_to_val. unlock. done. Qed.
Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
......@@ -371,7 +368,7 @@ Section properties.
{[cl := (q, lv, to_agree v)]} to_locking_heap σ
lv', lv lv' σ !! cl = Some (lv', v).
Proof.
rewrite singleton_included=> -[[[q' lv'] av] []].
rewrite singleton_included_l=> -[[[q' lv'] av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
......@@ -381,7 +378,7 @@ Section properties.
{[l := to_agree (k,n)]} to_heap_block_info τ
b, τ !! l = Some b heap_block_info b = (k,n).
Proof.
rewrite singleton_included=> -[mn].
rewrite singleton_included_l=> -[mn].
rewrite /to_heap_block_info lookup_fmap fmap_Some_equiv=> -[[b [-> ->]]] /=.
move=> /Some_included_total /to_agree_included /leibniz_equiv_iff; eauto.
Qed.
......@@ -504,7 +501,7 @@ Section properties.
Lemma alloc_heap_lookup σ l vs (i j : nat) :
( i, σ !! CLoc l i = None)
alloc_heap σ l vs j !! CLoc l (j + i) = ((ULvl,) <$> vs) !! i.
alloc_heap σ l vs j !! CLoc l (j + i) = ((ULvl,.) <$> vs) !! i.
Proof.
intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
{ by rewrite Hσi. }
......@@ -570,7 +567,7 @@ Section properties.
(alloc_singleton_local_update _ l (to_agree (k, length vs)))=> //.
by rewrite /to_heap_block_info lookup_fmap Hτi. }
iModIntro. iSplit; first done. iSplitL "Hσ H Hτ Hll".
{ iExists (<[l:=ActiveBlock k ((ULvl,) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iExists (<[l:=ActiveBlock k ((ULvl,.) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iPureIntro. split.
{ clear -Hnat. generalize 0. induction vs as [|v vs IH]=> j //=.
apply map_Forall_insert_2; simpl; eauto with lia. }
......
......@@ -23,7 +23,7 @@ Section factorial_spec.
Qed.
Lemma factorial_spec (n: nat) R :
CWP factorial #n @ R {{ v, v = #(fact n) }}%I.
CWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
iApply cwp_fun; simpl. vcg. iIntros (r c) "**".
iApply (cwp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first.
......
......@@ -51,7 +51,7 @@ Section gcd_spec.
Qed.
Lemma gcd_robbert_thesis_spec (a b : nat) R :
CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, v = #(Nat.gcd a b) }}%I.
CWP gcd_robbert_thesis (#a, #b)%V @ R {{ v, v = #(Nat.gcd a b) }}%I.
Proof.
iApply cwp_fun; simpl. vcg; iIntros (p q) "**". iApply (cwp_wand _ (λ _,
p C #(Nat.gcd a b) q C #0)%I with "[-]"); last first.
......
......@@ -20,7 +20,7 @@ Section tests_vcg.
(c_ret "v1") + (c_ret "v2").
Lemma test_invoke_2 R :
CWP call (c_ret plus_pair) (21 ||| 21) @ R {{ v, v = #42 }}%I.
CWP call (c_ret plus_pair) (21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof.
iIntros. vcg. iIntros "$ !> !>". cwp_lam. vcg. by vcg_continue.
Qed.
......
From stdpp Require Import namespaces.
From iris_c.vcgen Require Import proofmode.
From iris_c.lib Require Import mset list.
From iris.algebra Require Import frac_auth csum excl agree.
From iris.algebra Require Import lib.excl_auth.
(** This example is meant to demonstrate the usage of atomic rules for
the primitive operations, as well as for function calls. In this file
......@@ -52,35 +52,9 @@ Section test.
iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
Qed.
(** Ghost state definitions and lemmas *)
Definition gpointsto γ (b : bool) := own γ ( (Excl' b)).
Notation "γ '≔' b" := (gpointsto γ b) (at level 80).
Definition gauth γ b := own γ ( (Excl' b)).
Lemma gagree γ b1 b2 :
γ b1 - gauth γ b2 - b1 = b2.
Proof.
iIntros "H1 H2".
by iDestruct (own_valid_2 with "H2 H1")
as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Qed.
Lemma gnew : (|==> γ, gauth γ false γ false)%I.
Proof.
iMod (own_alloc ( (Excl' false) (Excl' false)))%I as (γ) "[H1 H2]";
first by apply auth_both_valid.
eauto with iFrame.
Qed.
Lemma gupdate b3 γ b1 b2 :
γ b1 - gauth γ b2 == γ b3 gauth γ b3.
Proof.
iIntros "H1 H2".
iMod (own_update_2 with "H2 H1") as "[? ?]".
{ apply auth_update, option_local_update.
by apply (exclusive_local_update (Excl b2) (Excl b3)). }
by iFrame.
Qed.
(** The correctness of the test function. *)
Definition test_inv cl γl γr : iProp Σ := ( b1 b2, gauth γl b1 gauth γr b2
(** The correctness of the test function. *)
Definition test_inv cl γl γr : iProp Σ := ( b1 b2,
own γl (E b1) own γr (E b2)
match b1, b2 with
| false, false => cl C #0
| true, false => cl C #10
......@@ -94,52 +68,55 @@ Section test.
(cl C #10 cl C #11) }}.
Proof.
iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl.
iMod gnew as (γl) "[H1 lb]".
iMod gnew as (γr) "[H2 rb]".
iMod (own_alloc (E false E false)) as (γl) "[H1 lb]"; first by apply excl_auth_valid.
iMod (own_alloc (E false E false)) as (γr) "[H2 rb]"; first by apply excl_auth_valid.
iApply (cwp_insert_res _ _ (test_inv cl γl γr) with "[H1 H2 Hl]").
{ iNext. iExists false,false. iFrame. }
iApply (cwp_bin_op _ _ (λ v, v = #10 γl true)%I
(λ v, v = #11 γr true)%I
iApply (cwp_bin_op _ _ (λ v, v = #10 own γl (E true))%I
(λ v, v = #11 own γr (E true))%I
with "[lb] [rb]").
- vcg. unfold test_inv. iIntros "[H R]".
iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
iDestruct (gagree with "lb H1") as %<-.
iDestruct (own_valid_2 with "H1 lb") as %->%excl_auth_agreeL.
destruct b2; iNext; iModIntro.
+ iMod (gupdate true with "lb H1") as "[lb H1]".
+ iMod (own_update_2 with "H1 lb") as "[H1 lb]";
first by apply (excl_auth_update _ _ true).
iApply (storeme_spec with "H").
iIntros "Hl". iFrame "R".
iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
iExists _,_; eauto with iFrame.
+ iMod (gupdate true with "lb H1") as "[lb H1]".
iSplitR "lb"; first by (iExists _,_; eauto with iFrame).
vcg_continue; auto.
+ iMod (own_update_2 with "H1 lb") as "[H1 lb]";
first by apply (excl_auth_update _ _ true).
iApply (storeme_spec with "H").
iIntros "Hl". iFrame "R".
iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
iExists _,_; eauto with iFrame.
iSplitR "lb"; first by (iExists _,_; eauto with iFrame).
vcg_continue; auto.
- iApply (cwp_store _ _ (λ v, v = cloc_to_val cl)%I
(λ v, v = #11)%I).
1,2: vcg; eauto.
iIntros (? ? -> ->) "[H R]". unfold test_inv.
iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
iDestruct (gagree with "rb H2") as %<-.
iDestruct (own_valid_2 with "H2 rb") as %->%excl_auth_agreeL.
iModIntro.
destruct b1; iEval (simpl) in "H".
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl".
iMod (gupdate true with "rb H2") as "[rb H2]".
iMod (own_update_2 with "H2 rb") as "[H2 rb]";
first by apply (excl_auth_update _ _ true).
iModIntro. iSplitR "rb"; last by eauto with iFrame.
iExists _,_; eauto with iFrame.
+ iExists cl, _. iFrame. iSplit; first done.
iIntros "Hl".
iMod (gupdate true with "rb H2") as "[rb H2]".
iMod (own_update_2 with "H2 rb") as "[H2 rb]";
first by apply (excl_auth_update _ _ true).
iModIntro. iSplitR "rb"; last by eauto with iFrame.
iExists _,_; eauto with iFrame.
- iIntros (v1 v2) "[% lb] [% rb]"; simplify_eq/=.
iExists #21; simpl. iSplit; first done.
iIntros "H". iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
do 3 iModIntro.
iDestruct (gagree with "lb H1") as %<-.
iDestruct (gagree with "rb H2") as %<-.
iDestruct (own_valid_2 with "lb H1") as %->%excl_auth_agreeL.
iDestruct (own_valid_2 with "rb H2") as %->%excl_auth_agreeL.
iDestruct "H" as "[H|H]"; iModIntro; vcg; eauto with iFrame.
Qed.
End test.
......@@ -31,7 +31,7 @@ Section tests_vcg.
implementation-defined behaviour *)
Lemma test3 (n : nat) (m : Z) :
1 n
CWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }}%I.
CWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }}%I.
Proof.
intros. vcg. iExists (n). repeat iSplit; eauto.
{ iPureIntro. lia. }
......@@ -42,7 +42,7 @@ Section tests_vcg.
Lemma test3_NOMATCH (n m : Z) :
1 n
CWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }}%I.
CWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }}%I.
Proof.
intros. vcg.
match goal with
......
......@@ -396,7 +396,7 @@ Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool :=
| dLitInt _, (dLitUnit | dLitBool _)
| dLitBool _, (dLitInt _ | dLitUnit)
| dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)))
| _, _ => dBoolUnknown (bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2))
end.
Arguments dbase_lit_eq !_ !_ / : simpl nomatch.
......@@ -410,12 +410,30 @@ Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool :=
| dNone, (dLitV _ | dPairV _ _ | dLocV _)
| dPairV _ _, (dNone | dLitV _ | dLocV _)
| dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)))
| _, _ => dBoolUnknown (bool_decide (dval_interp E dv1 = dval_interp E dv2))
end.
Arguments dval_eq _ !_ !_ / : simpl nomatch.
Definition dbase_lit_unboxed (dl : dbase_lit) : bool :=
match dl with
| dLitUnknown l => bool_decide (lit_is_unboxed l)
| _ => true
end.
Definition dval_unboxed (dv : dval) : bool :=
match dv with
| dLitV dl => dbase_lit_unboxed dl
| dValUnknown v => bool_decide (val_is_unboxed v)
| _ => false
end.
Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
if decide (op = EqOp) then Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2 else
if decide (op = EqOp) then
if dval_unboxed dv1 || dval_unboxed dv2 then
Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2
else
None
else
match dv1, dv2 with
| dLitV (dLitInt di1), dLitV (dLitInt di2) => dLitV <$> dbin_op_eval_int op di1 di2
| dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2
......@@ -568,6 +586,32 @@ Proof.
rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
Lemma dbase_lit_unboxed_correct dl :
dbase_lit_unboxed dl = true
lit_is_unboxed (dbase_lit_interp dl).
Proof.
destruct dl; intros; simplify_eq/=; [done..|].
eapply bool_decide_eq_true_1. done.
Qed.
Lemma dval_unboxed_correct E dv :
dval_unboxed dv = true
val_is_unboxed (dval_interp E dv).
Proof.
destruct dv; intros; simplify_eq/=.
- exact: dbase_lit_unboxed_correct.
- exact: bool_decide_eq_true_1.
Qed.
Lemma dvals_compare_safe_correct E dv1 dv2 :
dval_unboxed dv1 || dval_unboxed dv2 = true
vals_compare_safe (dval_interp E dv1) (dval_interp E dv2).
Proof.
destruct (dval_unboxed dv1) eqn:Hdv1.
- intros _. left. exact: dval_unboxed_correct.
- simpl. intros Hdv2. right. exact: dval_unboxed_correct.
Qed.
Lemma dbin_op_eval_int_correct op di1 di2 dl :
dbin_op_eval_int op di1 di2 = Some dl
bin_op_eval_int op (dint_interp di1) (dint_interp di2) = Some (dbase_lit_interp dl).
......@@ -588,7 +632,7 @@ Qed.
Lemma dbase_lit_eq_correct dl1 dl2 :
dbool_interp (dbase_lit_eq dl1 dl2) =
bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)).
bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2).
Proof.
destruct dl1, dl2=> //=.
- rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence.
......@@ -597,13 +641,13 @@ Qed.
Lemma dval_eq_correct E dv1 dv2 :
dbool_interp (dval_eq E dv1 dv2) =
bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)).
bool_decide (dval_interp E dv1 = dval_interp E dv2).
Proof.
revert dv1. induction dv2; intros []=> //=; try by rewrite cloc_to_val_eq.
- rewrite dbase_lit_eq_correct. apply bool_decide_iff. naive_solver congruence.
- rewrite dbool_and_correct. rewrite IHdv2_1 IHdv2_2.
repeat case_bool_decide; intuition congruence.
- rewrite dloc_eq_correct !cloc_to_val_for_compare.
- rewrite dloc_eq_correct.
apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
......@@ -611,8 +655,10 @@ Lemma dbin_op_eval_correct E op dv1 dv2 dw :
dbin_op_eval E op dv1 dv2 = Some dw
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw).
Proof.
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)); simplify_eq/=.
{ by rewrite dval_eq_correct. }
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)). simplify_eq/=.
{ destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
rewrite decide_True; last exact: dvals_compare_safe_correct.
simplify_eq/=. by rewrite dval_eq_correct. }
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq.
- by erewrite dbin_op_eval_int_correct by done.
- by erewrite dbin_op_eval_bool_correct by done.
......@@ -677,7 +723,9 @@ Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2 dval_wf E dw.
Proof.
rewrite /dbin_op_eval; intros; simplify_option_eq; auto.
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
- destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
simplify_eq/=. done.
- destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
Qed.
Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
......
......@@ -764,7 +764,7 @@ Section denv.
Lemma denv_delete_frac_stack_interp E i ms ms' q dv :
denv_delete_frac_stack i ms = Some (ms', q, dv) Forall (denv_wf E) ms
denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
Proof.
intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' Hi); simplify_eq/=.
destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:?; simplify_eq/=.
......@@ -779,7 +779,7 @@ Section denv.
Lemma denv_delete_full_stack_interp E i ms ms' q dv :
denv_delete_full_stack_aux i ms = Some (ms', q, dv)
Forall (denv_wf E) ms
denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
denv_stack_interp E ms ms' (dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
Proof.
intros Hi Hms. iInduction Hms as [|m ms] "IH" forall (ms' q dv Hi); simplify_eq/=.
destruct (denv_delete_full_aux i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=.
......@@ -805,7 +805,7 @@ Section denv.
Lemma denv_delete_frac_2_interp E i ms m ms' m' q dv :
denv_delete_frac_2 i ms m = Some (ms', m', q, dv)
Forall (denv_wf E) ms denv_wf E m
denv_stack_interp E ms ms' (denv_interp E m -
denv_stack_interp E ms ms' (denv_interp E m -
denv_interp E m' dloc_var_interp E i C{Q_to_Qp q} dval_interp E dv).
Proof.
rewrite /denv_delete_frac_2 /denv_wf. intros ?? [??]%andb_True.
......@@ -823,7 +823,7 @@ Section denv.
Lemma denv_delete_full_2_interp E i ms m ms' m' dv :
denv_delete_full_2 i ms m = Some (ms', m', dv)
Forall (denv_wf E) ms denv_wf E m
denv_stack_interp E ms ms' (denv_interp E m -
denv_stack_interp E ms ms' (denv_interp E m -
denv_interp E m' dloc_var_interp E i C dval_interp E dv).
Proof.
rewrite /denv_delete_full_2 /denv_wf. intros ???.
......
......@@ -171,7 +171,7 @@ Section forward_spec.
Lemma dexpr_eval_correct E de dv :
dexpr_eval de = Some dv
WP dexpr_interp E de {{ v, v = dval_interp E dv }}%I.
WP dexpr_interp E de {{ v, v = dval_interp E dv }}%I.
Proof.
iIntros (Hde). iInduction de as [] "IH" forall (dv Hde); simplify_option_eq.
- by iApply wp_value.
......@@ -189,7 +189,7 @@ Section forward_spec.
Lemma forward_aux_correct E de ms ms' mNew dv R n :
forward_aux E n ms de = Some (ms', mNew, dv)
Forall (denv_wf E) ms dcexpr_wf E de
denv_stack_interp E ms ms' (CWP dcexpr_interp E de @ R
denv_stack_interp E ms ms' (CWP dcexpr_interp E de @ R
{{ v, v = dval_interp E dv denv_interp E mNew }})%I.
Proof.
iIntros (Hsp Hms Hde).
......@@ -209,8 +209,8 @@ Section forward_spec.
{ apply (Forall_cons (denv_wf E)); eauto 10. }
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ (_ :: ms1) with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [H1 H2]".
iApply cwp_seq_bind. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
iDestruct (denv_unlock_interp with "Hm") as "Hm"; do 2 iModIntro.
iDestruct ("H2" with "Hm") as "[Hm2 H]". rewrite -dcexpr_interp_subst'.
......@@ -221,7 +221,7 @@ Section forward_spec.
destruct (dloc_var_of_dval _) as [i|] eqn:?; simplify_eq/=.
destruct (denv_delete_frac_2 i _ _) as [[[[ms2 mNew2] q] dv2]|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_frac_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply cwp_load. iApply (cwp_wand with "H1"); iIntros (v1) "[-> Hm]".
......@@ -236,10 +236,10 @@ Section forward_spec.
destruct (denv_delete_full_2 i ms2 _) as [[[ms3 mNew3] dv3]|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [[H1 H2] H]".
iApply (cwp_store with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
......@@ -253,7 +253,7 @@ Section forward_spec.
destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply (cwp_bin_op with "H1 H2"); iIntros (v1 v2) "[-> Hm1] [-> Hm2]".
iExists _. repeat (iSplit; first by eauto).
......@@ -267,10 +267,10 @@ Section forward_spec.
destruct (dcbin_op_eval _ _ _ _) eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H []") as "H".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iDestruct (denv_stack_interp_trans with "H []") as "{H} H".
{ iApply denv_delete_full_2_interp; eauto. }
iApply (denv_stack_interp_wand with "H"); iIntros "[[H1 H2] H]".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} [[H1 H2] H]".
iApply (cwp_pre_bin_op with "H1 H2").
iIntros (v1 v2) "[-> Hm1] [-> Hm2] $ !>".
iDestruct ("H" with "[Hm1 Hm2]") as "[Hm Hi]".
......@@ -282,14 +282,14 @@ Section forward_spec.
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
destruct (dun_op_eval _ _ _) as [dw|] eqn:?; simplify_eq/=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H".
iApply (denv_stack_interp_wand with "H"); iIntros "H".
iApply (denv_stack_interp_wand with "H"); iIntros "{H} H".
iApply cwp_un_op. iApply (cwp_wand with "H"); iIntros (v1) "[-> $]"; eauto.
- (* par *)
destruct (forward_aux _ _ ms _) as [[[ms1 mNew1] dv1]|] eqn:?; simplify_eq /=.
destruct (forward_aux _ _ ms1 _) as [[[ms2 mNew2] dv2]|] eqn:?; simplify_eq /=.
iDestruct ("IH" $! _ ms with "[//] [//] [//]") as "H1".
iDestruct ("IH" $! _ ms1 with "[//] [] []") as "H2 /="; eauto 10.
iDestruct (denv_stack_interp_trans with "H1 H2") as "H".
iDestruct (denv_stack_interp_trans with "H1 H2") as "{H1 H2} H".
iApply (denv_stack_interp_wand with "H"); iIntros "[H1 H2]".
iApply (cwp_par with "H1 H2"); iIntros "!>" (v1 v2) "[-> Hm1] [-> Hm2] !>".
iSplit; first done. iApply denv_merge_interp; eauto 10 with iFrame.
......