Commit 30e7f81d authored by Robbert Krebbers's avatar Robbert Krebbers

Remove tons of useless imports.

parent 185b5980
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From iris_c.lib Require Export locking_heap.
From iris.heap_lang Require Import adequacy spin_lock assert par. From iris.heap_lang Require Import adequacy spin_lock assert par.
From iris.algebra Require Import frac. From iris.algebra Require Import frac.
From iris_c.lib Require Import mset flock locking_heap. From iris_c.lib Require Import mset flock.
From iris.bi Require Import fractional.
(* M A := ref (list loc) → Mutex → A *) (* M A := ref (list loc) → Mutex → A *)
......
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import spin_lock assert par.
From iris_c.lib Require Import locking_heap mset flock.
From iris_c.c_translation Require Export monad. From iris_c.c_translation Require Export monad.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
......
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert par.
From iris.algebra Require Import frac auth.
From iris_c.lib Require Import mset flock list.
From iris_c.lib Require Export locking_heap U.
From iris_c.c_translation Require Export monad. From iris_c.c_translation Require Export monad.
From iris_c.c_translation Require Import proofmode. From iris_c.lib Require Export U.
From iris_c.c_translation Require Export proofmode.
From iris.heap_lang Require Export assert.
From iris_c.lib Require Import mset flock list.
Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l"). Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope. Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
...@@ -459,7 +457,7 @@ Section proofs. ...@@ -459,7 +457,7 @@ Section proofs.
unfold cloc_lt; simpl. case_bool_decide as Hp; subst; awp_op. unfold cloc_lt; simpl. case_bool_decide as Hp; subst; awp_op.
- rewrite (bool_decide_true (LitV ql = LitV ql)) //. awp_if. do 2 awp_proj. - rewrite (bool_decide_true (LitV ql = LitV ql)) //. awp_if. do 2 awp_proj.
iApply awp_ret. wp_op. iApply awp_ret. wp_op.
rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt. rewrite (bool_decide_iff (pi < qi) (pi < qi)%Z); eauto using Nat2Z.inj_lt.
- rewrite bool_decide_false; last congruence. - rewrite bool_decide_false; last congruence.
awp_if. iApply awp_ret. by iApply wp_value. awp_if. iApply awp_ret. by iApply wp_value.
Qed. Qed.
......
(** Testing basic connectives *) (** Testing basic connectives *)
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
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.
From iris_c.lib Require Import locking_heap U.
Section test. Section test.
Context `{amonadG Σ}. Context `{amonadG Σ}.
...@@ -187,5 +182,4 @@ Section test. ...@@ -187,5 +182,4 @@ Section test.
iLeft. iSplitR; eauto. iLeft. iSplitR; eauto.
vcg_solver. iIntros "Hl". iModIntro. by iApply "IH". vcg_solver. iIntros "Hl". iModIntro. by iApply "IH".
Qed. Qed.
End test. End test.
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
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.
From iris_c.lib Require Import locking_heap U.
Section test. Section test.
Context `{amonadG Σ}. Context `{amonadG Σ}.
...@@ -18,5 +13,4 @@ Section test. ...@@ -18,5 +13,4 @@ Section test.
rewrite Qp_half_half. rewrite Qp_half_half.
eauto with iFrame. eauto with iFrame.
Qed. Qed.
End test. End test.
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
From iris.algebra Require Import frac. Local Open Scope Z_scope.
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.
From iris_c.lib Require Import locking_heap U.
Definition incr : val := λ: "l", Definition incr : val := λ: "l",
(a_ret "l") = (∗ᶜ (a_ret "l") + 1). (a_ret "l") = (∗ᶜ (a_ret "l") + 1).
...@@ -91,5 +87,4 @@ Section factorial_spec. ...@@ -91,5 +87,4 @@ Section factorial_spec.
iRevert "H". iIntros "%". assert (k = n) as -> by lia. iRevert "H". iIntros "%". assert (k = n) as -> by lia.
vcg_continue. eauto. vcg_continue. eauto.
Qed. Qed.
End factorial_spec. End factorial_spec.
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
From iris.heap_lang Require Import spin_lock assert par. Local Open Scope Z_scope.
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.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
Require Import Coq.ZArith.Znumtheory.
(* TODO: Notation, get rid of parenthesis around the while loop *) (* TODO: Notation, get rid of parenthesis around the while loop *)
Definition gcd : val := λ: "a" "b", Definition gcd : val := λ: "a" "b",
......
(** Testing function calls and AWP resources *) (** Testing function calls and AWP resources *)
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
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.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg. Section tests_vcg.
Context `{amonadG Σ}. Context `{amonadG Σ}.
......
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
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.
Definition a_list_nil : val := λ:<>, a_ret NONEV. Definition a_list_nil : val := λ:<>, a_ret NONEV.
...@@ -64,7 +60,7 @@ Section list_spec. ...@@ -64,7 +60,7 @@ Section list_spec.
end%I. end%I.
Lemma a_list_nil_spec R Φ: Lemma a_list_nil_spec R Φ:
(Φ NONEV) - awp (a_list_nil #()) R Φ. Φ NONEV - awp (a_list_nil #()) R Φ.
Proof. iIntros "H"; awp_lam; by awp_ret_value. Qed. Proof. iIntros "H"; awp_lam; by awp_ret_value. Qed.
Lemma a_list_next_spec (e: expr) R Φ : Lemma a_list_next_spec (e: expr) R Φ :
......
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
From iris.algebra Require Import frac. Local Open Scope Z_scope.
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.
From iris_c.lib Require Import locking_heap U.
Section memcpy. Section memcpy.
Context `{amonadG Σ}. Context `{amonadG Σ}.
...@@ -117,6 +113,4 @@ Section memcpy. ...@@ -117,6 +113,4 @@ Section memcpy.
repeat vcg_continue. (* TODO WTF?? *) repeat vcg_continue. (* TODO WTF?? *)
eauto with iFrame. eauto with iFrame.
Qed. Qed.
End memcpy. End memcpy.
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
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.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg. Section tests_vcg.
Context `{amonadG Σ}. Context `{amonadG Σ}.
......
(** Testing vcgen on expressions contaning unknown subexpressions *) (** Testing vcgen on expressions contaning unknown subexpressions *)
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Import vcg_solver.
From iris.algebra Require Import frac. Local Open Scope Z_scope.
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.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg. Section tests_vcg.
Context `{amonadG Σ}. Context `{amonadG Σ}.
...@@ -38,7 +34,7 @@ Section tests_vcg. ...@@ -38,7 +34,7 @@ Section tests_vcg.
According to the standrad, malloc'ing zero bytes is According to the standrad, malloc'ing zero bytes is
implementation-defined behaviour *) implementation-defined behaviour *)
Lemma test3 (n : nat) (m : Z) : Lemma test3 (n : nat) (m : Z) :
n 1 1 n
(AWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }})%I. (AWP ∗ᶜ(alloc (n,m)) {{ v, v = #m }})%I.
Proof. Proof.
intros ?. iStartProof. intros ?. iStartProof.
......
From iris.heap_lang Require Export proofmode notation. From iris_c.c_translation Require Export translation.
From iris.bi Require Import big_op. Local Open Scope Z_scope.
From iris_c.c_translation Require Export translation proofmode.
Definition known_locs := list cloc. Definition known_locs := list cloc.
......
(** * Reified environments *) (** * Reified environments *)
From iris.proofmode Require Import environments coq_tactics. From iris_c.vcgen Require Export dcexpr.
From iris_c.vcgen Require Import dcexpr.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac. From iris.algebra Require Import frac.
Local Open Scope nat_scope.
(** The reification process is done in two steps. First, we split the (** The reification process is done in two steps. First, we split the
main environment into a 'partial environment' (`penv`), that main environment into a 'partial environment' (`penv`), that
...@@ -37,7 +36,6 @@ Section denv. ...@@ -37,7 +36,6 @@ Section denv.
}. }.
Definition denv := list (option denv_item). Definition denv := list (option denv_item).
Definition penv_to_known_locs : penv known_locs := fmap penv_loc. Definition penv_to_known_locs : penv known_locs := fmap penv_loc.
(** A reified environment is well-formed if every item is well (** A reified environment is well-formed if every item is well
...@@ -956,7 +954,7 @@ Section denv_spec. ...@@ -956,7 +954,7 @@ Section denv_spec.
Proof. Proof.
revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//. revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//.
destruct i. destruct i.
- destruct dio as [[]|]; naive_solver. - destruct dio as [[]|]; by auto with lia.
- destruct (denv_delete_frac i m) as [[[? ?] ?]|] eqn:Hm =>//. - destruct (denv_delete_frac i m) as [[[? ?] ?]|] eqn:Hm =>//.
simpl. naive_solver lia. simpl. naive_solver lia.
Qed. Qed.
...@@ -967,7 +965,7 @@ Section denv_spec. ...@@ -967,7 +965,7 @@ Section denv_spec.
Proof. Proof.
revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//. revert i m' q dv. induction m as [|dio m] =>i m' q dv/=//.
destruct i. destruct i.
- destruct dio as [[]|]; naive_solver. - destruct dio as [[]|]; by auto with lia.
- destruct (denv_delete_full_aux i m) as [[[? ?] ?]|] eqn:Hm =>//. - destruct (denv_delete_full_aux i m) as [[[? ?] ?]|] eqn:Hm =>//.
simpl. naive_solver lia. simpl. naive_solver lia.
Qed. Qed.
...@@ -1032,7 +1030,7 @@ Section denv_spec. ...@@ -1032,7 +1030,7 @@ Section denv_spec.
Qed. Qed.
Lemma denv_insert_length i x q dv m: Lemma denv_insert_length i x q dv m:
(length (denv_insert i x q dv m) = max (S i) (length m))%nat. length (denv_insert i x q dv m) = max (S i) (length m).
Proof. Proof.
revert m. induction i as [|i']=>m. revert m. induction i as [|i']=>m.
+ destruct m as [|dio m]; simpl. omega. + destruct m as [|dio m]; simpl. omega.
...@@ -1221,5 +1219,4 @@ Section denv_spec. ...@@ -1221,5 +1219,4 @@ Section denv_spec.
omega. } omega. }
by eapply denv_wf_mono. by eapply denv_wf_mono.
Qed. Qed.
End denv_spec. End denv_spec.
From iris.proofmode Require Import environments coq_tactics. From iris.proofmode Require Import environments coq_tactics.
From iris_c.vcgen Require Export denv.
Import env_notations. Import env_notations.
From iris_c.vcgen Require Export dcexpr denv.
From iris.algebra Require Import frac.
Section splitenv. Section splitenv.
Context `{amonadG Σ}. Context `{amonadG Σ}.
......
From iris.heap_lang Require Export proofmode notation. From iris_c.vcgen Require Export vcgen.
From iris.algebra Require Import frac. From iris_c.vcgen Require Import splitenv.
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.
From iris_c.lib Require Import locking_heap U.
From iris.proofmode Require Import environments coq_tactics. From iris.proofmode Require Import environments coq_tactics.
Import env_notations. Import env_notations.
...@@ -72,7 +68,6 @@ Section vcg_continue. ...@@ -72,7 +68,6 @@ Section vcg_continue.
* by left. * by left.
* right. by apply Hsplit. * right. by apply Hsplit.
Qed. Qed.
End vcg_continue. End vcg_continue.
Arguments vcg_wp_continuation {_ _ _ _}. Arguments vcg_wp_continuation {_ _ _ _}.
......
From iris.heap_lang Require Export proofmode notation. From iris_c.c_translation Require Export translation.
From iris.algebra Require Import frac. From iris.algebra Require Import frac.
From iris.bi Require Import big_op. From iris_c.vcgen Require Import denv.
From iris_c.vcgen Require Import dcexpr denv.
From iris_c.c_translation Require Import monad translation proofmode.
Section vcg. Section vcg.
Context `{amonadG Σ}. Context `{amonadG Σ}.
......
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