Commit 81137d7c authored by Robbert Krebbers's avatar Robbert Krebbers

Properly handle functions.

parent 40b27d98
...@@ -135,7 +135,16 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e)) ...@@ -135,7 +135,16 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e))
(at level 10, cnd, e at level 99, (at level 10, cnd, e at level 99,
format "'[v' 'whileVᶜ' ( cnd ) { '/ ' '[' e ']' '/' } ']'") : expr_scope. format "'[v' 'whileVᶜ' ( cnd ) { '/ ' '[' e ']' '/' } ']'") : expr_scope.
Definition a_call: val := λ: "f" "arg", Definition a_fun (f : expr) : val := λ: "arg",
(* sequence point at the end of a function *)
"v" ←ᶜ f "arg" ;
a_ret "v".
(* TODO: Similar notation for recursive functions *)
Notation "'λᶜ' x , e" := (a_fun (λ: x, e)%V)
(at level 200, x at level 1, e at level 200,
format "'[' 'λᶜ' x , '/ ' e ']'") : val_scope.
Definition a_call : val := λ: "f" "arg",
(* sequence point before a function call *) (* sequence point before a function call *)
"fa" ←ᶜ ("f" ||| "arg"); "fa" ←ᶜ ("f" ||| "arg");
a_atomic (λ: <>, (Fst "fa") (Snd "fa")). a_atomic (λ: <>, (Fst "fa") (Snd "fa")).
...@@ -508,6 +517,15 @@ Section proofs. ...@@ -508,6 +517,15 @@ Section proofs.
iIntros "HI #Hinv". iApply a_while_spec. by iApply (a_whileV_inv_spec with "HI Hinv"). iIntros "HI #Hinv". iApply a_while_spec. by iApply (a_whileV_inv_spec with "HI Hinv").
Qed. Qed.
Lemma a_fun_spec R Φ e mx v :
AWP subst' mx v e @ R {{ λ w, U (Φ w) }} -
AWP (λᶜ mx, e)%V v @ R {{ Φ }}.
Proof.
iIntros "H". awp_lam. iApply a_seq_bind_spec; simpl. awp_lam.
iApply (awp_wand with "H"); iIntros (w) "H !>".
by iApply awp_ret; iApply wp_value.
Qed.
Lemma a_call_spec R Ψ1 Ψ2 Φ ef ea : Lemma a_call_spec R Ψ1 Ψ2 Φ ef ea :
AWP ef @ R {{ Ψ1 }} - AWP ef @ R {{ Ψ1 }} -
AWP ea @ R {{ Ψ2 }} - AWP ea @ R {{ Ψ2 }} -
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition incr : val := λ: "l", Definition inc : val := λᶜ "l",
(a_ret "l") += 1 ; a_ret "l" += 1 ; ().
().
Definition factorial : val := λ: "n", Definition factorial : val := λ "n",
"r" mut 1; "r" mut 1;
"c" mut 0; "c" mut 0;
while (∗ᶜ (a_ret "c") < a_ret "n") { while (∗ᶜ (a_ret "c") < a_ret "n") {
call (a_ret incr) (a_ret "c"); call (a_ret inc) (a_ret "c");
a_ret "r" = ∗ᶜ (a_ret "r") * ∗ᶜ (a_ret "c") a_ret "r" = ∗ᶜ (a_ret "r") * ∗ᶜ (a_ret "c")
}; };
∗ᶜ(a_ret "r"). ∗ᶜ(a_ret "r").
...@@ -16,15 +15,17 @@ Definition factorial : val := λ: "n", ...@@ -16,15 +15,17 @@ Definition factorial : val := λ: "n",
Section factorial_spec. Section factorial_spec.
Context `{amonadG Σ}. Context `{amonadG Σ}.
Lemma incr_spec l (n : Z) R Φ : Lemma inc_spec l (n : Z) R Φ :
l C #n - (l C #(1 + n) - Φ #()) - l C #n - (l C #(1 + n) - Φ #()) -
AWP incr (cloc_to_val l) @ R {{ Φ }}. AWP inc (cloc_to_val l) @ R {{ Φ }}.
Proof. iIntros "**". awp_lam. vcg. eauto. Qed. Proof.
iIntros "? H". iApply a_fun_spec; simpl. vcg; iIntros "? !>". by iApply "H".
Qed.
Lemma factorial_spec (n: nat) R : 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. Proof.
awp_lam. vcg. iIntros (r c) "**". iApply a_fun_spec; simpl. vcg. iIntros (r c) "**".
iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first. iApply (awp_wand _ (λ _, c C #n r C #(fact n))%I with "[-]"); last first.
{ iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. } { iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. }
iAssert ( k : nat, k n c C #k r C #(fact k))%I with "[-]" as (k Hk) "[??]". iAssert ( k : nat, k n c C #k r C #(fact k))%I with "[-]" as (k Hk) "[??]".
...@@ -32,7 +33,7 @@ Section factorial_spec. ...@@ -32,7 +33,7 @@ Section factorial_spec.
iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext. iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext.
vcg. iIntros "**". case_bool_decide. vcg. iIntros "**". case_bool_decide.
+ iLeft. iSplit; eauto. iModIntro. vcg. + iLeft. iSplit; eauto. iModIntro. vcg.
iIntros "Hc Hr !> $ !>". iApply (incr_spec with "Hc"); iIntros "Hc". iIntros "Hc Hr !> $ !>". iApply (inc_spec with "Hc"); iIntros "Hc".
vcg_continue. iIntros "Hc Hr !>". vcg_continue. iIntros "Hc Hr !>".
assert (fact k * S k = fact (S k)) as -> by (simpl; lia). assert (fact k * S k = fact (S k)) as -> by (simpl; lia).
iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia. iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia.
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition gcd : val := λ: "x", Definition gcd : val := λ "x",
"a" ←ᶜ a_ret (Fst "x"); "a" ←ᶜ a_ret (Fst "x");
"b" ←ᶜ a_ret (Snd "x"); "b" ←ᶜ a_ret (Snd "x");
while(∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) { while(∗ᶜ(a_ret "a") != ∗ᶜ(a_ret "b")) {
...@@ -19,7 +19,7 @@ Section gcd_spec. ...@@ -19,7 +19,7 @@ Section gcd_spec.
l C #a - r C #b - l C #a - r C #b -
AWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, v = #(Z.gcd a b) }}. AWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, v = #(Z.gcd a b) }}.
Proof. Proof.
iIntros (??) "**". awp_lam. vcg; iIntros. iIntros (??) "**". iApply a_fun_spec; simpl. vcg; iIntros.
iApply (a_whileV_inv_spec ( x y : Z, iApply (a_whileV_inv_spec ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[-]"). 0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[-]").
{ iExists a, b. eauto with iFrame. } { iExists a, b. eauto with iFrame. }
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition memcpy : val := λ: "arg", Definition memcpy : val := λ "arg",
"p" mut a_ret (Fst "arg"); "p" mut a_ret (Fst "arg");
"q" mut a_ret (Fst (Snd "arg")); "q" mut a_ret (Fst (Snd "arg"));
"n" ←ᶜ a_ret (Snd (Snd "arg")); "n" ←ᶜ a_ret (Snd (Snd "arg"));
...@@ -14,10 +14,10 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R : ...@@ -14,10 +14,10 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R :
lxs C xs - lys C ys - lxs C xs - lys C ys -
AWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys lys C ys }}. AWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys lys C ys }}.
Proof. Proof.
iIntros (Hlen <-) "**". awp_lam. vcg. iIntros (p q) "**". iIntros (Hlen <-) "**". iApply a_fun_spec; simpl. vcg. iIntros (p q) "**".
iApply (awp_wand _ (λ _, p' q', p C p' q C q' iApply (awp_wand _ (λ _, p' q', p C p' q C q'
lxs C ys lys C ys)%I with "[-]"); last first. lxs C ys lys C ys)%I with "[-]"); last first.
{ iIntros (v). iDestruct 1 as (p' q') "[??]". by vcg_continue. } { iIntros (v). iDestruct 1 as (p' q') "[??]". vcg_continue; auto. }
iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen); iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);
destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame. destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame.
vcg; iIntros "!> !> !> **". vcg; iIntros "!> !> !> **".
......
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
From iris.algebra Require Import frac_auth. From iris.algebra Require Import frac_auth.
Definition inc : val := λ: "l", Definition inc : val := λ "l",
a_ret "l" += 1 ; 1. a_ret "l" += 1 ; 1.
Definition par_inc : val := λ: "l", Definition par_inc : val := λ "l",
call (a_ret inc) (a_ret "l") + call (a_ret inc) (a_ret "l"). call (a_ret inc) (a_ret "l") + call (a_ret inc) (a_ret "l").
Section par_inc. Section par_inc.
...@@ -13,13 +13,15 @@ Section par_inc. ...@@ -13,13 +13,15 @@ Section par_inc.
Lemma inc_spec R cl (n : Z) Φ : Lemma inc_spec R cl (n : Z) Φ :
cl C #n - (cl C #(1 + n) - Φ #1) - cl C #n - (cl C #(1 + n) - Φ #1) -
AWP inc (cloc_to_val cl) @ R {{ Φ }}. AWP inc (cloc_to_val cl) @ R {{ Φ }}.
Proof. iIntros. awp_lam. by vcg. Qed. Proof.
iIntros "? H". iApply a_fun_spec; simpl. vcg; iIntros "? !>". by iApply "H".
Qed.
Lemma par_inc_spec R cl (n : Z) : Lemma par_inc_spec R cl (n : Z) :
cl C #n - cl C #n -
AWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}. AWP par_inc (cloc_to_val cl) @ R {{ v, v = #2 cl C #(2 + n) }}.
Proof. Proof.
iIntros "Hl". awp_lam. iIntros "Hl". iApply a_fun_spec.
iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|]. iMod (own_alloc (! 0%nat ! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (! n'))%I). set (par_inc_inv := ( n' : nat, cl C #(n' + n) own γ (! n'))%I).
iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
...@@ -39,6 +41,6 @@ Section par_inc. ...@@ -39,6 +41,6 @@ Section par_inc.
- by iApply "H". - by iApply "H".
- iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done. - iIntros (v1 v2) "[-> Hγ1] [-> Hγ2]". iExists #2; iSplit; first done.
iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'". iDestruct 1 as (n') ">[Hl Hγ]". iCombine "Hγ1 Hγ2" as "Hγ'".
iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. by iFrame. iDestruct (own_valid_2 with "Hγ Hγ'") as %->%frac_auth_agreeL. iFrame; auto.
Qed. Qed.
End par_inc. End par_inc.
\ No newline at end of file
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Section tests_vcg. Section swap.
Context `{amonadG Σ}. Context `{amonadG Σ}.
Definition swap : val := λ: "a", Definition swap : val := λ "a",
"l1" ←ᶜ a_ret (Fst "a"); "l1" ←ᶜ a_ret (Fst "a");
"l2" ←ᶜ a_ret (Fst (Snd "a")); "l2" ←ᶜ a_ret (Snd "a");
"r" ←ᶜ a_ret (Snd (Snd "a")); "r" mut ∗ᶜ (a_ret "l1") ;
(a_ret "r") = ∗ᶜ (a_ret "l1") ;
(a_ret "l1") = ∗ᶜ (a_ret "l2") ; (a_ret "l1") = ∗ᶜ (a_ret "l2") ;
(a_ret "l2") = ∗ᶜ (a_ret "r") ; (a_ret "l2") = ∗ᶜ (a_ret "r") ;
(). ().
Lemma swap_spec (l1 l2 r : cloc) (v1 v2: val) R : Lemma swap_spec l1 l2 v1 v2 R :
r C #0 - l1 C v1 l2 C v2 - l1 C v1 - l2 C v2 -
AWP swap (cloc_to_val l1, (cloc_to_val l2, cloc_to_val r))%V @ R AWP swap (cloc_to_val l1, cloc_to_val l2)%V @ R {{ _, l2 C v1 l1 C v2 }}.
{{ _, l2 C v1 l1 C v2 }}. Proof. iIntros. iApply a_fun_spec; simpl. vcg. eauto with iFrame. Qed.
Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed.
Definition swap_with_alloc : val := λ: "a", Definition swap_with_alloc : val := λ "a",
"l1" ←ᶜ a_ret (Fst "a"); "l1" ←ᶜ a_ret (Fst "a");
"l2" ←ᶜ a_ret (Snd "a"); "l2" ←ᶜ a_ret (Snd "a");
"r" ←ᶜ alloc (1, 0); "r" ←ᶜ alloc (1, 0);
...@@ -30,5 +28,5 @@ Section tests_vcg. ...@@ -30,5 +28,5 @@ Section tests_vcg.
Lemma swap_with_alloc_spec l1 l2 v1 v2 R : Lemma swap_with_alloc_spec l1 l2 v1 v2 R :
l1 C v1 - l2 C v2 - l1 C v1 - l2 C v2 -
AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2)%V @ R {{ _, l1 C v2 l2 C v1 }}. AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2)%V @ R {{ _, l1 C v2 l2 C v1 }}.
Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed. Proof. iIntros. iApply a_fun_spec; simpl. vcg; eauto with iFrame. Qed.
End tests_vcg. End swap.
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