Commit ec27d524 authored by Ralf Jung's avatar Ralf Jung

add test with a closed proof

parent d04c9f7e
......@@ -40,3 +40,4 @@
| InjR "m" => assert: #m = "m"
end {{ _, True }}
Closed under the global context
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
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 adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
Definition one_shot_example : val := λ: <>,
......@@ -95,3 +96,35 @@ Proof.
- iIntros "!# _". wp_apply (wp_wand with "Hf2"). by iIntros (v) "#? !# _".
Qed.
End proof.
(* Have a client with a closed proof. *)
Definition client : expr :=
let: "ff" := one_shot_example #() in
(Fst "ff" #5 ||| let: "check" := Snd "ff" #() in "check" #()).
Section client.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
Lemma client_safe : WP client {{ _, True }}%I.
Proof.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
wp_let. wp_apply wp_par.
- wp_apply "Hf1".
- wp_proj. wp_bind (f2 _)%E. iApply wp_wand; first by iExact "Hf2".
iIntros (check) "Hcheck". wp_pures. iApply "Hcheck".
- auto.
Qed.
End client.
(** Put together all library functors. *)
Definition clientΣ : gFunctors := #[ heapΣ; one_shotΣ; spawnΣ ].
(** This lemma implicitly shows that these functors are enough to meet
all library assumptions. *)
Lemma client_adequate σ : adequate NotStuck client σ (λ _ _, True).
Proof. apply (heap_adequacy clientΣ)=> ?. apply client_safe. Qed.
(* Since we check the output of the test files, this means
our test suite will fail if we ever accidentally add an axiom
to anything used by this proof. *)
Print Assumptions client_adequate.
......@@ -683,6 +683,7 @@ Bind Scope cFunctor_scope with cFunctor.
Class cFunctorContractive (F : cFunctor) :=
cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
Hint Mode cFunctorContractive ! : typeclass_instances.
Definition cFunctor_diag (F: cFunctor) (A: ofeT) : ofeT := cFunctor_car F A A.
Coercion cFunctor_diag : cFunctor >-> Funclass.
......
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