Commit 6f390922 authored by Dan Frumin's avatar Dan Frumin

Better a_alloc_ret rule and fix a test

parent e700c35b
......@@ -4,6 +4,15 @@ 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.
Class ValToNat (v : val) (n : nat) :=
val_to_nat : v = #n.
Global Instance val_to_nat_pos (o : positive) : ValToNat #(Zpos o) (Pos.to_nat o).
Proof. rewrite /ValToNat. by rewrite -positive_nat_Z. Qed.
Global Instance val_to_nat_zero : ValToNat #0 0%nat.
Proof. done. Qed.
Section derived.
Context `{amonadG Σ}.
......@@ -16,12 +25,14 @@ Section derived.
iExists cl, w. by iFrame.
Qed.
Lemma a_alloc_ret (n: nat) (e2: expr) (ev2: val) R Φ:
Lemma a_alloc_ret (n: nat) (e1 e2: expr) (ev1 ev2: val) R Φ:
IntoVal e1 ev1
ValToNat ev1 n
IntoVal e2 ev2
( l: loc, (l,O) C replicate n ev2 - Φ (cloc_to_val (l,O))) -
awp (a_alloc (a_ret #n) (a_ret e2)) R Φ.
awp (a_alloc (a_ret e1) (a_ret e2)) R Φ.
Proof.
iIntros (?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I (λ v, v = ev2)%I).
iIntros (? ? ?) "H". iApply (a_alloc_spec _ _ (λ v, v = #n)%I (λ v, v = ev2)%I).
- iApply awp_ret. by iApply wp_value.
- iApply awp_ret. by iApply wp_value.
- iNext. iIntros (? ? -> ->). iExists n; iSplit; eauto.
......
......@@ -358,6 +358,7 @@ Global Instance expr_into_dval_loc_unknown E l :
ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed.
(* TODO: use ValToNat for those two instance below *)
Global Instance expr_into_dval_cloc_pos E (l : loc) (o : positive) i :
LocLookup E (l,Pos.to_nat o) i ExprIntoDVal E (#l,#(Zpos o)) (dLocV (dLoc i)) | 1.
Proof. rewrite /LocLookup=> Hi. split; rewrite /= ?Hi -?positive_nat_Z //. Qed.
......
......@@ -6,37 +6,33 @@ From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Definition incr : val := λ: "l",
a_store (a_ret "l") (a_bin_op PlusOp (a_load (a_ret "l")) (a_ret #1)).
(a_ret "l") = (∗ᶜ (a_ret "l") + 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")))).
while ((∗ᶜ (a_ret "c")) < (a_ret "n"))
{ incr "c" ;
a_ret "r" = ((∗ᶜ (a_ret "r")) * (∗ᶜ (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)).
"r" ←ᶜ a_alloc 1 1;;
"k" ←ᶜ a_alloc 1 0;;
factorial_body "n" "k" "r" ;
∗ᶜ(a_ret "r").
Section factorial_spec.
Context `{amonadG Σ}.
Lemma incr_spec (l : loc) (n : Z) R Φ :
Lemma incr_spec (l : cloc) (n : Z) R Φ :
l C #n - (l C[LLvl] #(n+1) - Φ #(n+1)) -
awp (incr #l) R Φ.
AWP incr (cloc_to_val l) @ R {{ Φ }}.
Proof.
iIntros "Hl HΦ". awp_lam. vcg_solver. auto.
Qed.
Lemma factorial_body_spec (n k : nat) (c r: loc) R :
Lemma factorial_body_spec (n k : nat) (c r: cloc) R :
(k n c C[ULvl] #k r C #(fact k)) -
awp (factorial_body #n #c #r) R
(λ _, c C #n r C #(fact n))%I.
AWP factorial_body #n (cloc_to_val c) (cloc_to_val r) @ R
{{ _, c C #n r C #(fact n) }}.
Proof.
iIntros "(Hk & Hc & Hr)". do 3 awp_lam.
iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_while_spec'. iNext.
......@@ -57,27 +53,27 @@ Section factorial_spec.
Qed.
Lemma factorial_spec (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
AWP factorial #n @ R {{ v, v = #(fact n) }}%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext.
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
iApply (awp_wand _ (λ _, (c,O) C #n (r,O) C #(fact n))%I with "[Hr Hc]").
- iApply ((factorial_body_spec n 0 (c,O) (r,O)) with "[$Hr $Hc]"); eauto with lia.
- iIntros (?) "[Hc Hr]". iModIntro.
awp_load_ret r.
awp_load_ret (r,O).
Qed.
Lemma factorial_spec_with_inv (n: nat) R :
awp (factorial #n) R (λ v, v = #(fact n))%I.
Proof.
awp_lam.
iApply awp_bind. awp_alloc_ret r "Hr".
iApply awp_bind. awp_alloc_ret c "Hc".
iApply awp_bind. awp_alloc_ret r "[Hr _]".
iApply awp_bind. awp_alloc_ret c "[Hc _]".
iApply a_sequence_spec'. iNext. do 3 awp_lam.
iApply (a_while_inv_spec
(k:nat, k n c C #k r C #(fact k))%I with "[Hr Hc]").
(k:nat, k n (c,O) C #k (r,O) C #(fact k))%I with "[Hr Hc]").
- iExists O. eauto with iFrame lia.
- iModIntro. iIntros "H". iDestruct "H" as (k) "(H & Hc & Hr)".
vcg_solver. iIntros "Hr Hc".
......@@ -93,6 +89,6 @@ Section factorial_spec.
iExists (k+1)%nat. eauto with iFrame lia.
+ iLeft. iSplit; eauto. do 2 iModIntro.
iRevert "H". iIntros "%". assert (k = n) as -> by lia.
by awp_load_ret r.
awp_load_ret (r,O).
Qed.
End factorial_spec.
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