Commit 115acf17 authored by Dan Frumin's avatar Dan Frumin

Add tests

parent 1c1d4e0a
......@@ -33,4 +33,6 @@ theories/examples/stack/stack_rules.v
theories/examples/stack/CG_stack.v
theories/examples/stack/FG_stack.v
theories/examples/stack/refinement.v
theories/examples/typetest.v
theories/tests/typetest.v
theories/tests/tactics.v
theories/tests/tactics2.v
......@@ -141,27 +141,3 @@ Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_op" := wp_pure (BinOp _ _ _).
Ltac wp_value := iApply wp_value; eauto.
(* TODO: move to tests/ *)
From iris_logrel.F_mu_ref_conc Require Export notation.
Lemma wp_rec1 `{heapG Σ} Φ :
Φ #4
WP (λ: "y", (λ: "x", "x" + #3) "y") #1 {{ Φ }}.
Proof.
iIntros "Z".
wp_rec.
wp_rec.
wp_op.
wp_value.
Qed.
Lemma wp_proj2 `{heapG Σ} Φ :
Φ #1
WP Fst (Fst (#1,#2,#4)) {{ Φ }}.
Proof.
iIntros "HΦ".
wp_proj.
wp_proj.
wp_value.
Qed.
From iris_logrel.F_mu_ref_conc Require Export tactics notation.
Lemma wp_rec1 `{heapG Σ} Φ :
Φ #4
WP (λ: "y", (λ: "x", "x" + #3) "y") #1 {{ Φ }}.
Proof.
iIntros "Z".
wp_rec.
wp_rec.
wp_op.
wp_value.
Qed.
Lemma wp_proj2 `{heapG Σ} Φ :
Φ #1
WP Fst (Fst (#1,#2,#4)) {{ Φ }}.
Proof.
iIntros "HΦ".
wp_proj.
wp_proj.
wp_value.
Qed.
From iris.proofmode Require Import coq_tactics sel_patterns.
From iris_logrel.F_mu_ref_conc Require Export tactics.
From iris_logrel.logrel Require Export rules_threadpool
lang reflection proofmode.classes logrel_binary.
From iris_logrel.logrel Require Export rules_threadpool proofmode.tactics_threadpool logrel_binary.
Set Default Proof Using "Type".
Import lang.
(**************************)
(* / tp_apply *)
Section test.
Context `{logrelG Σ}.
Definition bot := App (TApp (TLam (Rec "f" "x" (App (Var "f") (Var "x"))))) Unit.
Definition bot := App (TApp (TLam (Rec "f" "x" (App (Var "f") (Var "x"))))) #().
Notation Lam x e := (Rec BAnon x e).
Notation LamV x e := (RecV BAnon x e).
......@@ -46,7 +43,7 @@ Qed.
Lemma test1 E1 j K l n ρ :
nclose specN E1
j fill K (App (Lam "x" (Store (Loc l) (BinOp Add (Nat 1) (Var "x")))) (Load (Loc l))) -
j fill K (App (Lam "x" (Store (Lit (Loc l)) (BinOp Add #1 (Var "x")))) (Load (# l))) -
spec_ctx ρ -
l ↦ₛ (#nv n) ={E1}= True.
Proof.
......@@ -58,13 +55,13 @@ Proof.
done.
Qed.
Lemma test2 E j K l n ρ :
Lemma test2 E j K (l : loc) (n : nat) ρ :
nclose specN E
j fill K
(Fork
(Fork
(App (If (CAS (Loc l) (Nat n) (Nat (n+1))) (Lam "x" (Fst (Var "x"))) (Lam "x" (Snd (Var "x"))))
(Pair (Nat 1) (Nat 2))))) -
(App (If (CAS (# l) (# n) (# (n+1))) (Lam "x" (Fst (Var "x"))) (Lam "x" (Snd (Var "x"))))
(Pair (# 1) (# 2))))) -
spec_ctx ρ -
l ↦ₛ (#nv n) ={E}= j, j (#n 1).
Proof.
......@@ -86,15 +83,15 @@ End test.
Section test2.
Context `{logrelG Σ}.
(* TODO: Coq complains if I make it a section variable *)
Axiom (steps_release_test : forall E ρ j K l b,
Axiom (steps_release_test : forall E ρ j K (l : loc) b,
nclose specN E
spec_ctx ρ - l ↦ₛ (#v b) - j fill K (App (Lit Unit) (Loc l))
spec_ctx ρ - l ↦ₛ (#v b) - j fill K (App (#tt) (# l))
={E}= j fill K (Lit Unit) l ↦ₛ (#v false)).
Theorem test_apply E ρ j b K l:
nclose specN E
spec_ctx ρ -
l ↦ₛ (#v b) - j fill K (App (Lit Unit) (Loc l))
l ↦ₛ (#v b) - j fill K (App (Lit Unit) (# l))
- |={E}=> True.
Proof.
iIntros (?) "#Hs Hst Hj".
......
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