Commit 90285dac authored by Léon Gondelman's avatar Léon Gondelman

fix the definition of while loop; add factorial example

parent 55f0efa1
......@@ -9,3 +9,4 @@ theories/c_translation/monad.v
theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/tests/test1.v
theories/tests/fact.v
\ No newline at end of file
......@@ -46,13 +46,64 @@ Notation "e1 ;;;; e2" :=
Definition a_if : val := λ: "cnd" "e1" "e2",
a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd".
Definition a_while: val :=
rec: "while" "cnd" "bdy" :=
a_if ("cnd" #()) ("bdy" ;;;; "while" "cnd" "bdy").
a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E.
Section proofs.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma a_while_spec R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
awp (a_if c
(λ:<>, (#() ;; b) ;;;; a_while (λ:<>, c) (λ:<>, b))
a_seq)%E R Φ -
awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
Proof.
iIntros "H".
awp_lam. awp_lam. awp_seq.
iApply "H".
Qed.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
AsVal e1 ->
AsVal e2 ->
awp e R Ψ -
( v, Ψ v - (v = #true awp (e1 #()) R Φ)
(v = #false awp (e2 #()) R Φ)) -
awp (a_if e e1 e2) R Φ.
Proof.
iIntros ([v1 <-%of_to_val] [v2 <-%of_to_val]) "H HΦ".
awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v) "HΨ". awp_lam.
iDestruct ("HΦ" with "HΨ") as "[[% H] | [% H]]";
simplify_eq/=; by (awp_pure _).
Qed.
Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #true)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iLeft. iSplit; eauto. by awp_seq.
Qed.
Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e2 R Φ - awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #false)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iRight. iSplit; eauto. by awp_seq.
Qed.
Lemma a_seq_spec R Φ :
U (Φ #()) -
awp (a_seq #()) R Φ.
......@@ -97,6 +148,8 @@ Section proofs.
iModIntro. by awp_lam.
Qed.
Lemma a_load_spec R Φ Ψ e :
awp e R (λ v, l : loc, v = #l Ψ l) -
( l : loc, Ψ l - v, l U v (l U v - Φ v)) -
......@@ -162,7 +215,7 @@ Section proofs.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
awp e1 R Ψ1 - awp e2 R Ψ2 -
( v1 v2, Ψ1 v1 - Ψ2 v2 -
w, bin_op_eval op v1 v2 = Some w Φ w)-
w, bin_op_eval op v1 v2 = Some w Φ w)-
awp (a_bin_op op e1 e2) R Φ.
Proof.
iIntros "H1 H2 HΦ".
......@@ -226,44 +279,5 @@ Section proofs.
- iApply "HΦ". iFrame.
Qed.
Lemma a_if_spec R Φ Ψ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
awp e R Ψ -
( v, Ψ v - (v = #true awp e1 R Φ) (v = #false awp e2 R Φ)) -
awp (a_if e (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "H HΦ". awp_apply (a_wp_awp with "H"); iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v) "HΨ". awp_lam.
iDestruct ("HΦ" with "HΨ") as "[[% H] | [% H]]"; simplify_eq/=;
by do 2 (awp_pure _).
Qed.
Lemma a_if_true_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #true)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iLeft. eauto.
Qed.
Lemma a_if_false_spec R (e1 e2 : val) `{Closed [] e1, Closed [] e2} Φ :
awp e2 R Φ - awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof.
iIntros "HΦ".
iApply (a_if_spec _ _ (λ v, v = #false)%I).
{ iApply awp_ret. iApply wp_value. eauto. }
iIntros (? ->). iRight. eauto.
Qed.
Lemma a_while_spec (cnd bdy : val) R Φ :
awp (a_if (cnd #()) (bdy ;;;; a_while cnd bdy)) R Φ -
awp (a_while cnd bdy) R Φ.
Proof.
iIntros "HAWP".
rewrite {2}/a_while.
awp_lam. awp_lam.
rewrite /a_while.
iApply "HAWP".
Qed.
End proofs.
From iris.heap_lang Require Export proofmode notation.
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.
Section factorial.
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.
Section factorial_spec.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
l U #n - (l L #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
Proof.
iIntros "Hl HΦ".
awp_lam.
iApply (a_store_spec _ _
(λ r, r = l)%I (λ v, v = #(n+1) l U #n)%I with "[] [Hl]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_bin_op_spec _ _
(λ v, v = #n l U #n )%I (λ v, v = #1)%I with "[-]").
+ iApply (a_load_spec _ _ (λ v, v = l)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (l1) "%"; subst. iExists #n. iFrame. eauto.
+ iApply awp_ret. by wp_value_head.
+ iIntros (? ?) "(% & Hc) %"; subst. iExists #(n+1). by iFrame. }
iIntros (? ? ->) "[% Hl1]"; subst.
iExists _; iFrame.
Qed.
Lemma factorial_body_spec (n: nat) (c r: loc) R :
k: nat, (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.
iIntros (k) "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec. iNext.
iAssert (k < n k = n)%I with "[Hk]" as "Hk".
{ iRevert "Hk"; iIntros "%"; iPureIntro; by lia. }
iDestruct "Hk" as "[Hk | Hk]".
- iApply (a_if_spec _ _
((λ v, (v = #true k < n c U #k))%I) with "[Hk Hc]").
+ iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc] [] [Hk]").
* iApply (a_load_spec _ _ (λ v, v = c)%I).
** iApply awp_ret. wp_value_head. eauto.
** iIntros (l) "%"; subst. iExists #k. iFrame. eauto.
* iApply awp_ret. by wp_value_head.
* iIntros (? ?) "(% & Hc) %"; subst. iExists #true.
iFrame "Hc". admit.
+ iIntros (v) "(% & % & Hc)"; subst.
iLeft. iSplit; first by eauto.
do 2 (awp_seq; iApply a_sequence_spec).
iApply (incr_spec with "[$Hc]").
iIntros "Hc". iModIntro. awp_seq.
iApply (a_store_spec _ _
(λ l, l = r)%I
(λ v, v = #(fact (k+1))
c U #(k + 1)
r U #(fact k))%I with "[] [Hr Hc]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ 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]").
+ iApply (a_load_spec _ _ (λ v, v = r)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (l1) "%"; subst. iExists #(fact k). iFrame. eauto.
+ iApply (a_load_spec _ _ (λ v, v = c)%I).
* iApply awp_ret. wp_value_head. eauto.
* iIntros (l1) "%"; subst. iExists #(k+1). iFrame. eauto.
+ iIntros (? ?) "(% & Hc) (% & Hr)"; subst.
iExists #(fact (k+1)). iFrame. iSplit; last by auto. admit. }
iIntros (? ? ->) "[% (Hc & Hr)]"; subst. iExists (#(fact k)); iFrame.
iIntros "Hr". iModIntro. awp_seq.
assert ( Z_of_nat' (k + 1)%nat = (k + 1)) by lia. rewrite- H3; clear H3.
iApply ("IH" with "[] [$Hc] [$Hr]"). iPureIntro. lia.
- iApply (a_if_spec _ _
((λ v, (v = #false k = n c U #k))%I) with "[Hk Hc]").
iApply (a_bin_op_spec _ _
(λ v, v = #k c U #k )%I (λ v, v = #n)%I with "[Hc] [] [Hk]").
* iApply (a_load_spec _ _ (λ v, v = c)%I).
** iApply awp_ret. wp_value_head. eauto.
** iIntros (l) "%"; subst. iExists #k. iFrame. eauto.
* iApply awp_ret. by wp_value_head.
* iIntros (? ?) "(% & Hc) %"; subst. iExists #false.
iFrame "Hc". admit.
* iIntros (v) "(% & % & Hc)"; subst.
iRight. iSplit; first by eauto.
iApply a_seq_spec. iModIntro. by iFrame.
Admitted.
Lemma factorial_spec (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam. iApply awp_bind. iApply (a_alloc_spec _ _ (λ v, v = #1)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? r ->) "Hr". awp_lam. iApply awp_bind.
iApply (a_alloc_spec _ _ (λ v, v = #0)%I).
{ iApply awp_ret. by iApply wp_value. }
iIntros (? c ->) "Hc". awp_lam.
iApply a_sequence_spec.
iApply ((awp_wand _ (λ _, c U #n r U #(fact n))%I) with "[Hr Hc]").
- iApply (factorial_body_spec n c r R 0). iFrame. iPureIntro. lia.
- iIntros (?) "[Hc Hr]". iModIntro. awp_seq.
iApply (a_load_spec _ _ (λ v, v = r)%I).
+ iApply awp_ret. iApply wp_value; eauto.
+ iIntros (? ->). iExists _; iFrame. eauto.
Qed.
End factorial_spec.
......@@ -7,15 +7,6 @@ From iris_c.c_translation Require Import proofmode translation.
Section test.
Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
Definition factorial_body : val := λ: "n" "c" "r",
a_while
(λ:<>, a_bin_op LeOp (a_load (a_ret "c")) (a_ret "n"))
(λ:<>, a_store (a_ret "c")
( a_bin_op PlusOp (a_load (a_ret "c")) (a_ret #1)) ;;;;
a_store (a_ret "r")
(a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c"))) ;;;
a_seq #()).
Lemma test1 (l : loc) :
l L #1 -
......@@ -31,6 +22,7 @@ Section test.
iIntros (? ->). iExists #1. iFrame. 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⌝). *)
......@@ -47,38 +39,6 @@ Section test.
(* Qed. *)
Definition swap_aform (l1 l2 : loc) : val := λ: <>,
(a_bind (λ: "r",
((a_bind (λ: "v", (a_store (a_ret "r")) (a_ret "v"))) (a_load (a_ret #l1))) ;;;
a_seq #();;;
((a_bind (λ: "v", (a_store (a_ret #l1)) (a_ret "v"))) (a_load (a_ret #l2))) ;;;
a_seq #();;;
((a_bind (λ: "v", (a_store (a_ret #l2)) (a_ret "v"))) (a_load (a_ret "r"))) ;;;
a_seq #()))
(a_alloc (a_ret #0)).
(* Lemma swap_spec_aform (l1 l2 : loc) (v1 v2: val) R : *)
(* l1 ↦U v1 -∗ l2 ↦U v2 -∗ *)
(* awp (swap_aform l1 l2 #()) R (λ _, l1 ↦U v2 ∗ l2 ↦U v1). *)
(* Proof. *)
(* iIntros "Hl1 Hl2". *)
(* (* let r = ref 0 in *) *)
(* awp_lam; iApply awp_bind; iApply (a_alloc_spec R #0); iIntros (r) "Hr". *)
(* (* r <- !l1 ; *) *)
(* awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl1]"); iIntros "Hl1". *)
(* awp_lam; iApply (a_store_spec with "Hr"); iIntros "Hr"; awp_seq. *)
(* iApply awp_bind. iApply a_seq_spec; iUnlock. *)
(* (* l1 <- !l2 ; *) *)
(* awp_lam; do 2 iApply awp_bind; iApply (a_load_spec with "[$Hl2]"); iIntros "Hl2". *)
(* awp_lam; iApply (a_store_spec with "Hl1"); iIntros "Hl1"; awp_seq. *)
(* iApply awp_bind. iApply a_seq_spec. iUnlock. *)
(* (* l2 <- !r ; *) *)
(* awp_lam. do 2 iApply awp_bind. iApply (a_load_spec with "[$Hr]"); iIntros "Hr". *)
(* awp_lam; iApply (a_store_spec with "Hl2"); iIntros "Hl2"; awp_seq. *)
(* iApply a_seq_spec; iUnlock. *)
(* (* Post-condition*) *)
(* by iFrame. *)
(* Qed. *)
Definition swap : val := λ: "l1" "l2",
a_bind (λ: "r",
......@@ -99,7 +59,8 @@ Section test.
iIntros (? r ->) "Hr". awp_lam.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = r)%I (λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
iApply (a_store_spec _ _ (λ l, l = r)%I
(λ v, v = v1 l1 U v1)%I with "[] [Hl1]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l1)%I).
- iApply awp_ret. iApply wp_value; eauto.
......@@ -109,7 +70,8 @@ Section test.
awp_seq.
iApply a_sequence_spec.
iApply (a_store_spec _ _ (λ l, l = l1)%I (λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
iApply (a_store_spec _ _ (λ l, l = l1)%I
(λ v, v = v2 l2 U v2)%I with "[] [Hl2]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = l2)%I).
- iApply awp_ret. iApply wp_value; eauto.
......@@ -119,7 +81,8 @@ Section test.
awp_seq.
iApply awp_bind.
iApply (a_store_spec _ _ (λ l, l = l2)%I (λ v, v = v1 r U v1)%I with "[] [Hr]").
iApply (a_store_spec _ _ (λ l, l = l2)%I
(λ v, v = v1 r U v1)%I with "[] [Hr]").
{ iApply awp_ret. iApply wp_value; eauto. }
{ iApply (a_load_spec _ _ (λ v, v = r)%I).
- iApply awp_ret. iApply wp_value; eauto.
......@@ -131,11 +94,4 @@ Section test.
Qed.
Definition incr1 : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load "l") (a_ret #1)).
Lemma incr1_spec (l : loc) (n : Z) R :
l U #n -
awp (incr1 #l) R (λ _, l L #(n+1)).
Proof.
Admitted.
End test.
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