Skip to content

GitLab

Commit d22c6803 authored by Dan Frumin's avatar Dan Frumin
Browse files
Options

Simplify the tactics and clean up the examples

parent 0f6567ec
Hide whitespace changes
Inline Side-by-side
Showing with 67 additions and 86 deletions
theories/c_translation/derived.v
View file @ d22c6803
......@@ -39,9 +39,9 @@ Section Derived.
- iIntros (? w) "-> H". eauto with iFrame.
Qed.
Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
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 w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
Lemma awp_bin_op_load_load op (l r : loc) (v1 v2: val) R Φ :
l ↦U v1 -∗ r ↦U v2 -∗
......@@ -52,14 +52,14 @@ Section Derived.
iApply (a_bin_op_spec _ _
(λ x, ⌜x = v1⌝ ∧ l ↦U v1 )%I
(λ x, ⌜x = v2⌝ ∧ r ↦U v2)%I with "[Hl] [Hr] [HΦ]").
- awp_load_ret l v1.
- awp_load_ret r v2.
- awp_load_ret l.
- awp_load_ret r.
- iIntros (??) "[-> Hl] [-> Hr]".
iApply ("HΦ" with "[$Hl] [$Hr]").
Qed.
End Derived.
Ltac awp_load_ret l w := iApply (a_load_ret l w); iFrame; eauto.
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 w r h := iApply (a_alloc_ret w); iIntros (r) h; awp_lam.
Ltac awp_alloc_ret r h := iApply a_alloc_ret; iIntros (r) h; awp_lam.
theories/tests/fact.v
View file @ d22c6803
......@@ -4,33 +4,26 @@ 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.
Definition incr : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load (a_ret "l")) (a_ret #1)).
Section factorial.
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LtOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, incr "c" ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c")))).
Definition incr : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load (a_ret "l")) (a_ret #1)).
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LtOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, incr "c" ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c")))).
Definition factorial : val := λ: "n",
a_bind ( λ: "r",
a_bind (λ: "k",
factorial_body "n" "k" "r" ;;;;
(a_load (a_ret "r")))
(a_alloc (a_ret #0%V)))
(a_alloc (a_ret #1%V)).
End factorial.
Definition factorial : val := λ: "n",
a_bind ( λ: "r",
a_bind (λ: "k",
factorial_body "n" "k" "r" ;;;;
(a_load (a_ret "r")))
(a_alloc (a_ret #0%V)))
(a_alloc (a_ret #1%V)).
Section factorial_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
......@@ -42,14 +35,14 @@ Section factorial_spec.
iApply (a_store_ret with "[Hl HΦ]").
iApply (a_bin_op_spec _ _
(λ v, ⌜v = #n⌝ ∗ l ↦U #n )%I (λ v, ⌜v = #1⌝)%I with "[Hl] [] [HΦ]").
+ awp_load_ret l #n.
+ awp_load_ret l.
+ awp_ret_value.
+ iIntros (? ?) "(% & Hc) %"; subst.
iExists #(n+1). iSplit; eauto with iFrame.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
(⌜k <= n⌝ ∧ c ↦U #k ∗ r ↦U #(fact k)) -∗
(⌜k ≤ n⌝ ∧ c ↦U #k ∗ r ↦U #(fact k)) -∗
awp (factorial_body #n #c #r) R
(λ _, c ↦U #n ∗ r ↦U #(fact n))%I.
Proof.
......@@ -59,7 +52,7 @@ Section factorial_spec.
iApply a_if_spec.
iApply (a_bin_op_spec _ _
(λ v, ⌜v = #k⌝ ∧ c ↦U #k )%I (λ v, ⌜v = #n⌝)%I with "[Hc]").
- awp_load_ret c #k.
- awp_load_ret c.
- awp_ret_value.
- iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
......@@ -72,8 +65,8 @@ Section factorial_spec.
iApply (a_bin_op_spec _ _
(λ v, ⌜v = #(fact k)⌝ ∗ r ↦U #(fact k))%I
(λ v, ⌜v = #(k + 1)⌝ ∗ c ↦U #(k+1))%I with "[Hr] [Hc]").
* awp_load_ret r #(fact k).
* awp_load_ret c #(k + 1).
* awp_load_ret r.
* awp_load_ret c.
* iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
......@@ -92,13 +85,13 @@ Section factorial_spec.
awp (factorial #n) R (λ v, ⌜v = #(fact n)⌝)%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret #1 r "Hr".
iApply awp_bind. awp_alloc_ret #0 c "Hc".
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec.
iApply (awp_wand _ (λ _, c ↦U #n ∗ r ↦U #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
awp_load_ret r #(fact n).
awp_load_ret r.
Qed.
......@@ -106,16 +99,16 @@ Section factorial_spec.
awp (factorial #n) R (λ v, ⌜v = #(fact n)⌝)%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret #1 r "Hr".
iApply awp_bind. awp_alloc_ret #0 c "Hc".
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply a_sequence_spec. do 3 awp_lam.
iApply (a_while_inv_spec
(∃k:nat, ⌜k <= n⌝ ∧ c ↦U #k ∗ r ↦U #(fact k))%I with "[Hr Hc]").
(∃k:nat, ⌜k ≤ n⌝ ∧ c ↦U #k ∗ r ↦U #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
iApply (a_bin_op_spec _ _
(λ v, ⌜v = #k⌝ ∧ c ↦U #k )%I (λ v, ⌜v = #n⌝)%I with "[Hc]").
+ awp_load_ret c #k.
+ awp_load_ret c.
+ awp_ret_value.
+ iIntros (v1 v2) "[% Hc] %"; subst.
rewrite /bin_op_eval /=. iExists _; iSplit; eauto.
......@@ -128,8 +121,8 @@ Section factorial_spec.
iApply (a_bin_op_spec _ _
(λ v, ⌜v = #(fact k)⌝ ∗ r ↦U #(fact k))%I
(λ v, ⌜v = #(k + 1)⌝ ∗ c ↦U #(k+1))%I with "[Hr] [Hc]").
** awp_load_ret r #(fact k).
** awp_load_ret c #(k + 1).
** awp_load_ret r.
** awp_load_ret c.
** iIntros (? ?) "[% Hr] [% Hc]". simplify_eq.
rewrite /bin_op_eval /=.
assert ((fact k) * (k + 1) = fact (k + 1)) as ->.
......@@ -140,8 +133,6 @@ Section factorial_spec.
iExists (k+1)%nat. eauto with iFrame lia.
* iLeft. iSplit; eauto. do 2 iModIntro. awp_seq.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r #(fact n).
by awp_load_ret r.
Qed.
End factorial_spec.
theories/tests/gcd.v
View file @ d22c6803
......@@ -3,31 +3,23 @@ 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.
Require Import Coq.ZArith.Znumtheory.
Section gcd.
Definition gcd : val := λ: "a" "b",
(a_while
(λ:<>, a_un_op NegOp
(a_bin_op EqOp (a_load (a_ret "a")) (a_load (a_ret "b"))))
(λ:<>, a_if (a_bin_op LtOp (a_load (a_ret "a")) (a_load (a_ret "b")))
(λ:<>, a_store (a_ret "b")
((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
(λ:<>, a_store (a_ret "a")
((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
;;;; a_load (a_ret "a").
End gcd.
Definition gcd : val := λ: "a" "b",
(a_while
(λ:<>, a_un_op NegOp
(a_bin_op EqOp (a_load (a_ret "a")) (a_load (a_ret "b"))))
(λ:<>, a_if (a_bin_op LtOp (a_load (a_ret "a")) (a_load (a_ret "b")))
(λ:<>, a_store (a_ret "b")
((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
(λ:<>, a_store (a_ret "a")
((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
;;;; a_load (a_ret "a").
Section gcd_spec.
Require Import Coq.ZArith.Znumtheory.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma gcd_spec (a b : Z) (l r: loc) R:
⌜a >= 0⌝ -∗ ⌜b >= 0⌝ -∗
l ↦U #a -∗ r ↦U #b -∗
......@@ -48,7 +40,7 @@ Section gcd_spec.
+ iExists #true. simplify_eq /=. iSplit.
{ rewrite/ bin_op_eval //=; case_bool_decide; eauto. }
iExists #false; iSplit; first done. iLeft; iSplit; first done.
do 2 iModIntro. awp_seq. awp_load_ret l #y. iIntros.
do 2 iModIntro. awp_seq. awp_load_ret l. iIntros.
rewrite- H5. iPureIntro. symmetry. rewrite Z.gcd_diag.
rewrite Z.abs_eq; eauto with lia.
+ iExists #false. simplify_eq /=. iSplit.
......@@ -84,5 +76,4 @@ Section gcd_spec.
do 2 (split; first by lia).
rewrite -H5 Z.gcd_comm (Z.gcd_comm x); apply Z.gcd_sub_diag_r.
Qed.
End gcd_spec.
theories/tests/test1.v
View file @ d22c6803
......@@ -17,25 +17,24 @@ Section test.
iApply a_seq_spec.
iModIntro.
awp_lam.
awp_load_ret l #1.
awp_load_ret l.
Qed.
(* Lemma test2 (l r : loc) R : *)
(* l ↦U #3 -∗ r ↦L #0 -∗ *)
(* awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => ⌜v = #1⌝). *)
(* Proof. *)
(* iIntros "Hl Hr". *)
(* iApply awp_bind. *)
(* iApply (a_store_spec with "Hl"). iIntros "Hl". *)
(* awp_lam. *)
(* iApply awp_bind. *)
(* iApply a_seq_spec. *)
(* iUnlock. *)
(* awp_lam. *)
(* iApply (a_load_spec with "Hl"). iIntros "Hl". eauto. *)
(* Qed. *)
Lemma test2 (l r : loc) R :
l ↦U #3 -∗ r ↦L #0 -∗
awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (fun v => ⌜v = #1⌝).
Proof.
iIntros "Hl Hr".
iApply awp_bind.
iApply a_store_ret.
iApply awp_ret. iApply wp_value. iExists _; iFrame.
iIntros "Hl". awp_seq.
iApply awp_bind.
iApply a_seq_spec.
iModIntro. awp_seq.
awp_load_ret l.
Qed.
Definition swap : val := λ: "l1" "l2",
......@@ -50,19 +49,19 @@ Section test.
awp (swap #l1 #l2) R (λ _, l1 ↦U v2 ∗ l2 ↦U v1).
Proof.
iIntros "Hl1 Hl2".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret #0 r "Hr".
do 2 awp_lam. iApply awp_bind. awp_alloc_ret r "Hr".
iApply a_sequence_spec.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l1 v1. iIntros "Hl1". iExists #0. iFrame.
awp_load_ret l1. iIntros "Hl1". iExists #0. iFrame.
iIntros "Hr". iModIntro. awp_seq. iApply a_sequence_spec.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret l2 v2. iIntros "Hl2". iExists v1. iFrame.
awp_load_ret l2. iIntros "Hl2". iExists v1. iFrame.
iIntros "Hl1". iModIntro. awp_seq. iApply awp_bind.
iApply (a_store_ret with "[Hl1 Hl2 Hr]").
awp_load_ret r v1. iIntros "Hr". iExists v2. iFrame.
awp_load_ret r. iIntros "Hr". iExists v2. iFrame.
iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
Qed.
......
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