Commit 60d82286 authored by Ralf Jung's avatar Ralf Jung

more restrictive Proof Using hints in heap_lang, proofmode, tests

parent 6db2ae8e
...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting. ...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG { Class heapPreG Σ := HeapPreG {
heap_preG_iris :> invPreG Σ; heap_preG_iris :> invPreG Σ;
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
From iris.prelude Require Import gmap. From iris.prelude Require Import gmap.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Module heap_lang. Module heap_lang.
Open Scope Z_scope. Open Scope Z_scope.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition assert : val := Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *) λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
......
From iris.heap_lang Require Export notation. From iris.heap_lang Require Export notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition newbarrier : val := λ: <>, ref #false. Definition newbarrier : val := λ: <>, ref #false.
Definition signal : val := λ: "x", "x" <- #true. Definition signal : val := λ: "x", "x" <- #true.
......
...@@ -5,7 +5,7 @@ From iris.prelude Require Import functions. ...@@ -5,7 +5,7 @@ From iris.prelude Require Import functions.
From iris.base_logic Require Import big_op lib.saved_prop lib.sts. From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib.barrier Require Import protocol. From iris.heap_lang.lib.barrier Require Import protocol.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
(** The CMRAs/functors we need. *) (** The CMRAs/functors we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
......
From iris.algebra Require Export sts. From iris.algebra Require Export sts.
From iris.base_logic Require Import lib.own. From iris.base_logic Require Import lib.own.
From iris.prelude Require Export gmap. From iris.prelude Require Export gmap.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
(** The STS describing the main barrier protocol. Every state has an index-set (** The STS describing the main barrier protocol. Every state has an index-set
associated with it. These indices are actually [gname], because we use them associated with it. These indices are actually [gname], because we use them
......
...@@ -2,11 +2,12 @@ From iris.program_logic Require Export hoare. ...@@ -2,11 +2,12 @@ From iris.program_logic Require Export hoare.
From iris.heap_lang.lib.barrier Require Export barrier. From iris.heap_lang.lib.barrier Require Export barrier.
From iris.heap_lang.lib.barrier Require Import proof. From iris.heap_lang.lib.barrier Require Import proof.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Section spec. Section spec.
Context `{!heapG Σ} `{!barrierG Σ}. Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ}.
Lemma barrier_spec (N : namespace) : Lemma barrier_spec (N : namespace) :
recv send : loc iProp Σ -n> iProp Σ, recv send : loc iProp Σ -n> iProp Σ,
......
...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang. ...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth. From iris.algebra Require Import frac auth.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition newcounter : val := λ: <>, ref #0. Definition newcounter : val := λ: <>, ref #0.
Definition incr : val := rec: "incr" "l" := Definition incr : val := rec: "incr" "l" :=
......
From iris.heap_lang Require Export lifting notation. From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock { Structure lock Σ `{!heapG Σ} := Lock {
(* -- operations -- *) (* -- operations -- *)
......
From iris.heap_lang Require Export spawn. From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Definition parN : namespace := nroot .@ "par". Definition parN : namespace := nroot .@ "par".
...@@ -14,6 +14,7 @@ Definition par : val := ...@@ -14,6 +14,7 @@ Definition par : val :=
Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope. Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
Section proof. Section proof.
Set Default Proof Using "Type*".
Context `{!heapG Σ, !spawnG Σ}. Context `{!heapG Σ, !spawnG Σ}.
(* Notice that this allows us to strip a later *after* the two Ψ have been (* Notice that this allows us to strip a later *after* the two Ψ have been
......
...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang. ...@@ -4,7 +4,7 @@ From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition spawn : val := Definition spawn : val :=
λ: "f", λ: "f",
......
...@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics. ...@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl. From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock. From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition newlock : val := λ: <>, ref #false. Definition newlock : val := λ: <>, ref #false.
Definition try_acquire : val := λ: "l", CAS "l" #false #true. Definition try_acquire : val := λ: "l", CAS "l" #false #true.
......
...@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics. ...@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth gset. From iris.algebra Require Import auth gset.
From iris.heap_lang.lib Require Export lock. From iris.heap_lang.lib Require Export lock.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Definition wait_loop: val := Definition wait_loop: val :=
......
...@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lang. ...@@ -5,7 +5,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics. From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.prelude Require Import fin_maps. From iris.prelude Require Import fin_maps.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
(** Basic rules for language operations. *) (** Basic rules for language operations. *)
......
From iris.program_logic Require Import language. From iris.program_logic Require Import language.
From iris.heap_lang Require Export lang tactics. From iris.heap_lang Require Export lang tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics lifting. From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
(** wp-specific helper tactics *) (** wp-specific helper tactics *)
......
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import heap_lang. Import heap_lang.
(** We define an alternative representation of expressions in which the (** We define an alternative representation of expressions in which the
......
...@@ -2,7 +2,7 @@ From iris.proofmode Require Export classes. ...@@ -2,7 +2,7 @@ From iris.proofmode Require Export classes.
From iris.algebra Require Import gmap. From iris.algebra Require Import gmap.
From iris.prelude Require Import gmultiset. From iris.prelude Require Import gmultiset.
From iris.base_logic Require Import big_op. From iris.base_logic Require Import big_op.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Section classes. Section classes.
......
From iris.base_logic Require Export base_logic. From iris.base_logic Require Export base_logic.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Section classes. Section classes.
......
...@@ -2,7 +2,7 @@ From iris.base_logic Require Export base_logic. ...@@ -2,7 +2,7 @@ From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics. From iris.base_logic Require Import big_op tactics.
From iris.proofmode Require Export environments classes. From iris.proofmode Require Export environments classes.
From iris.prelude Require Import stringmap hlist. From iris.prelude Require Import stringmap hlist.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Import env_notations. Import env_notations.
......
...@@ -2,7 +2,7 @@ From iris.prelude Require Export strings. ...@@ -2,7 +2,7 @@ From iris.prelude Require Export strings.
From iris.proofmode Require Import strings. From iris.proofmode Require Import strings.
From iris.algebra Require Export base. From iris.algebra Require Export base.
From iris.prelude Require Import stringmap. From iris.prelude Require Import stringmap.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Inductive env (A : Type) : Type := Inductive env (A : Type) : Type :=
| Enil : env A | Enil : env A
......
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Inductive intro_pat := Inductive intro_pat :=
| IName : string intro_pat | IName : string intro_pat
......
From iris.proofmode Require Import coq_tactics environments. From iris.proofmode Require Import coq_tactics environments.
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Delimit Scope proof_scope with env. Delimit Scope proof_scope with env.
Arguments Envs _ _%proof_scope _%proof_scope. Arguments Envs _ _%proof_scope _%proof_scope.
......
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Inductive sel_pat := Inductive sel_pat :=
| SelPure | SelPure
......
From iris.prelude Require Export strings. From iris.prelude Require Export strings.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Record spec_goal := SpecGoal { Record spec_goal := SpecGoal {
spec_goal_modal : bool; spec_goal_modal : bool;
......
From iris.prelude Require Import strings. From iris.prelude Require Import strings.
From iris.algebra Require Import base. From iris.algebra Require Import base.
From Coq Require Import Ascii. From Coq Require Import Ascii.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope. Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
......
...@@ -5,7 +5,7 @@ From iris.proofmode Require Export classes notation. ...@@ -5,7 +5,7 @@ From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances. From iris.proofmode Require Import class_instances.
From iris.prelude Require Import stringmap hlist. From iris.prelude Require Import stringmap hlist.
From iris.proofmode Require Import strings. From iris.proofmode Require Import strings.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Declare Reduction env_cbv := cbv [ Declare Reduction env_cbv := cbv [
beq ascii_beq string_beq beq ascii_beq string_beq
......
...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang. ...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang.lib.barrier Require Import proof. From iris.heap_lang.lib.barrier Require Import proof.
From iris.heap_lang Require Import par. From iris.heap_lang Require Import par.
From iris.heap_lang Require Import adequacy proofmode. From iris.heap_lang Require Import adequacy proofmode.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition worker (n : Z) : val := Definition worker (n : Z) : val :=
λ: "b" "y", wait "b" ;; !"y" #n. λ: "b" "y", wait "b" ;; !"y" #n.
...@@ -14,9 +14,10 @@ Definition client : expr := ...@@ -14,9 +14,10 @@ Definition client : expr :=
(worker 12 "b" "y" ||| worker 17 "b" "y"). (worker 12 "b" "y" ||| worker 17 "b" "y").
Section client. Section client.
Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}. Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
Local Definition N := nroot .@ "barrier". Definition N := nroot .@ "barrier".
Definition y_inv (q : Qp) (l : loc) : iProp Σ := Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I. ( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
......
...@@ -8,7 +8,7 @@ From iris.heap_lang Require Export lang. ...@@ -8,7 +8,7 @@ From iris.heap_lang Require Export lang.
From iris.program_logic Require Export hoare. From iris.program_logic Require Export hoare.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Import uPred. Import uPred.
Definition newcounter : val := λ: <>, ref #0. Definition newcounter : val := λ: <>, ref #0.
......
...@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare. ...@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import adequacy. From iris.heap_lang Require Import adequacy.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section LiftingTests. Section LiftingTests.
Context `{heapG Σ}. Context `{heapG Σ}.
......
...@@ -4,7 +4,7 @@ From iris.algebra Require Import excl agree csum. ...@@ -4,7 +4,7 @@ From iris.algebra Require Import excl agree csum.
From iris.heap_lang.lib.barrier Require Import proof specification. From iris.heap_lang.lib.barrier Require Import proof specification.
From iris.heap_lang Require Import notation par proofmode. From iris.heap_lang Require Import notation par proofmode.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "All". Set Default Proof Using "Type".
Definition one_shotR (Σ : gFunctors) (F : cFunctor) := Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)). csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
...@@ -24,6 +24,7 @@ Definition client eM eW1 eW2 : expr := ...@@ -24,6 +24,7 @@ Definition client eM eW1 eW2 : expr :=
(eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)). (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
Section proof. Section proof.
Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}. Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace). Context (N : namespace).
Local Notation X := (F (iProp Σ)). Local Notation X := (F (iProp Σ)).
...@@ -71,7 +72,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2 ...@@ -71,7 +72,7 @@ Lemma client_spec_new eM eW1 eW2 `{!Closed [] eM, !Closed [] eW1, !Closed [] eW2
( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) - ( x, {{ Φ1 x }} eW1 {{ _, Ψ1 x }}) -
( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) - ( x, {{ Φ2 x }} eW2 {{ _, Ψ2 x }}) -
WP client eM eW1 eW2 {{ _, γ, barrier_res γ Ψ }}. WP client eM eW1 eW2 {{ _, γ, barrier_res γ Ψ }}.
Proof. Proof using All.
iIntros "/= HP #He #He1 #He2"; rewrite /client. iIntros "/= HP #He #He1 #He2"; rewrite /client.
iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done. iMod (own_alloc (Pending : one_shotR Σ F)) as (γ) "Hγ"; first done.
wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto. wp_apply (newbarrier_spec N (barrier_res γ Φ)); auto.
......
...@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare. ...@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section list_reverse. Section list_reverse.
Context `{!heapG Σ}. Context `{!heapG Σ}.
......
...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang. ...@@ -3,7 +3,7 @@ From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum. From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation. From iris.heap_lang Require Import assert proofmode notation.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in ( let: "x" := ref NONE in (
...@@ -30,6 +30,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ. ...@@ -30,6 +30,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section proof. Section proof.
Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ}. Context `{!heapG Σ, !one_shotG Σ}.
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ := Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Lemma demo_0 {M : ucmraT} (P Q : uPred M) : Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
(P Q) - ( x, x = 0 x = 1) (Q P). (P Q) - ( x, x = 0 x = 1) (Q P).
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics. From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Inductive tree := Inductive tree :=
| leaf : Z tree | leaf : Z tree
......
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