Commit 185b5980 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove derived file.

parent 85997565
......@@ -10,7 +10,6 @@ theories/lib/U.v
theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/vcgen/dcexpr.v
theories/vcgen/denv.v
theories/vcgen/splitenv.v
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation.
(* TODO: this should be subsumbed by the deep embedding of the integers *)
Class ValToNat (v : val) (n : nat) :=
val_to_nat : v = #n.
Global Instance val_to_nat_pos (o : positive) : ValToNat #(Zpos o) (Pos.to_nat o).
Proof. rewrite /ValToNat. by rewrite -positive_nat_Z. Qed.
Global Instance val_to_nat_zero : ValToNat #0 0%nat.
Proof. done. Qed.
Section derived.
Context `{amonadG Σ}.
Lemma a_load_ret (cl: cloc) (q : Qp) (w: val) R Φ:
cl C{q} w (cl C{q} w - Φ w) -
awp (a_load (a_ret (cloc_to_val cl)%E)) R Φ.
Proof.
iIntros "H". iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists cl, w. by iFrame.
Qed.
Lemma a_alloc_ret (n: nat) (e1 e2: expr) (ev1 ev2: val) R Φ:
IntoVal e1 ev1
ValToNat ev1 n
IntoVal e2 ev2
( l: cloc, l C replicate n ev2 - Φ (cloc_to_val l)) -
awp (a_alloc (a_ret e1) (a_ret e2)) R Φ.
Proof.
iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I (λ v, v = ev2)%I).
- iApply awp_ret. by iApply wp_value.
- iApply awp_ret. by iApply wp_value.
- iIntros "!>" (?? -> ->). iExists n; iSplit; eauto.
Qed.
Lemma a_store_ret (cl:cloc) (e: expr) `{Closed [] e} R Φ :
awp e R (λ w, v, cl C v (cl C[LLvl] w - Φ w)) -
awp (a_store (a_ret (cloc_to_val cl)) e) R Φ.
Proof.
iIntros "H".
iApply ((a_store_spec _ _
(λ l1, l1 = cloc_to_val cl)%I
(λ w, v, (cl C v (cl C[LLvl] w - Φ w)))%I ) with "[] [$H] []").
- iApply awp_ret; iApply wp_value; eauto.
- iNext. iIntros (? w) "-> H".
iDestruct "H" as (v) "H".
eauto with iFrame.
Qed.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
Lemma awp_bin_op_load_load op (l r : cloc) (v1 v2: val) R Φ :
l C v1 - r C v2 -
(l C v1 - r C v2 - w : val, cbin_op_eval op v1 v2 = Some w Φ w) -
awp (a_bin_op op (a_load (a_ret (cloc_to_val l))) (a_load (a_ret (cloc_to_val r)))) R Φ.
Proof.
iIntros "Hl Hr HΦ".
iApply (a_bin_op_spec _ _
(λ x, x = v1 l C v1 )%I
(λ x, x = v2 r C v2)%I with "[Hl] [Hr] [HΦ]").
- awp_load_ret l.
- awp_load_ret r.
- iNext. iIntros (??) "[-> Hl] [-> Hr]".
iApply ("HΦ" with "[$Hl] [$Hr]").
Qed.
Lemma a_pre_bin_op_spec' R Φ Ψ1 Ψ2 e1 e2 op v l :
l C v -
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - v1 = cloc_to_val l
w, cbin_op_eval op v v2 = Some w
(l C[LLvl] w - Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "Hl He1 He2 HΦ".
iApply (a_pre_bin_op_spec with "He1 He2 [-]").
iNext. iIntros (v1 v2) "HΨ1 HΨ2 $".
iDestruct ("HΦ" with "HΨ1 HΨ2") as (->) "HΦ".
iDestruct "HΦ" as (w ?) "HΦ".
iExists _,_,_; iFrame. eauto.
Qed.
Lemma a_pre_incr R Φ e1 l (z : Z) :
l C #z -
AWP e1 @ R {{ v, v = cloc_to_val l (l C[LLvl] #(z+1) - Φ #z) }} -
AWP e1 += 1 @ R {{ Φ }}.
Proof.
iIntros "Hl He1".
iApply (a_pre_bin_op_spec' _ _ _ (λ v, v = #1)%I with "Hl He1 [] [-]").
{ iApply awp_ret. by wp_value_head. }
iNext. iIntros (v1 v2) "[% HΦ] %". simplify_eq/=. eauto.
Qed.
Lemma a_move_spec (s t :cloc) (v w: val) R Φ :
s C v t C w (t C w - s C[LLvl] w - Φ w) -
awp (a_store (a_ret (cloc_to_val s)) (a_load (a_ret (cloc_to_val t)))) R Φ.
Proof.
iIntros "(Hs & Ht & H)".
iApply a_store_ret. awp_load_ret t. iIntros "Ht".
iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
Qed.
Lemma a_invoke_simpl (ef ea : expr) R Φ (f : val) :
IntoVal ef f
awp ea R (λ a, U (awp (ef a) R Φ)) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (?) "Ha".
iApply (a_invoke_spec with "Ha").
iIntros (a) "Hfa". iModIntro.
iIntros "HR". iExists R. iFrame.
iApply (awp_wand with "Hfa"). eauto with iFrame.
Qed.
Lemma a_invoke_full (ef ea : expr) R Φ (f : val) :
IntoVal ef f
awp ea R (λ a, U (R - awp (ef a) True%I (λ v, R Φ v))) -
awp (a_invoke ef ea) R Φ.
Proof.
iIntros (?) "Ha".
iApply (a_invoke_spec with "Ha").
iIntros (a) "HΨ". iModIntro.
iIntros "HR".
iExists True%I. iSplit; first done.
iSpecialize ("HΨ" with "HR").
iApply (awp_wand with "HΨ"). eauto with iFrame.
Qed.
End derived.
Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.
Ltac awp_ret_value := iApply awp_ret; iApply wp_value; eauto.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
......@@ -3,7 +3,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section test.
......
......@@ -2,7 +2,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section test.
......
......@@ -2,7 +2,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Definition incr : val := λ: "l",
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
From iris_c.c_translation Require Import proofmode translation.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
Require Import Coq.ZArith.Znumtheory.
......
......@@ -3,7 +3,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation derived proofmode.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......@@ -16,7 +16,7 @@ Section tests_vcg.
AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof.
iIntros "Hl". vcg_solver.
iIntros "Hl". awp_lam. awp_ret_value.
iIntros "Hl". awp_lam. vcg_solver. iIntros "?".
vcg_continue. eauto.
Qed.
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import locking_heap mset flock U.
From iris_c.c_translation Require Import proofmode translation derived.
From iris_c.c_translation Require Import proofmode translation.
Definition a_list_nil : val := λ:<>, a_ret NONEV.
......
......@@ -2,7 +2,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section memcpy.
......
......@@ -2,7 +2,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......
......@@ -3,7 +3,7 @@ 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 vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
......
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