From 81137d7ca13ae26836697d607446f7b69307b67c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 15 Nov 2018 13:05:35 +0100 Subject: [PATCH] Properly handle functions. --- theories/c_translation/translation.v | 20 +++++++++++++++++++- theories/tests/fact.v | 21 +++++++++++---------- theories/tests/gcd.v | 4 ++-- theories/tests/memcpy.v | 6 +++--- theories/tests/par_inc.v | 12 +++++++----- theories/tests/swap.v | 24 +++++++++++------------- 6 files changed, 53 insertions(+), 34 deletions(-) diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 92e23c2..31ce753 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -135,7 +135,16 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e)) (at level 10, cnd, e at level 99, 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 *) "fa" ←ᶜ ("f" |||ᶜ "arg");ᶜ a_atomic (λ: <>, (Fst "fa") (Snd "fa")). @@ -508,6 +517,15 @@ Section proofs. iIntros "HI #Hinv". iApply a_while_spec. by iApply (a_whileV_inv_spec with "HI Hinv"). 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 : AWP ef @ R {{ Ψ1 }} -∗ AWP ea @ R {{ Ψ2 }} -∗ diff --git a/theories/tests/fact.v b/theories/tests/fact.v index cb74c37..9f37232 100644 --- a/theories/tests/fact.v +++ b/theories/tests/fact.v @@ -1,14 +1,13 @@ From iris_c.vcgen Require Import proofmode. -Definition incr : val := λ: "l", - (a_ret "l") +=ᶜ ♯1 ;ᶜ - ♯(). +Definition inc : val := λᶜ "l", + a_ret "l" +=ᶜ ♯1 ;ᶜ ♯ (). -Definition factorial : val := λ: "n", +Definition factorial : val := λᶜ "n", "r" ←mutᶜ ♯1;ᶜ "c" ←mutᶜ ♯0;ᶜ 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"). @@ -16,15 +15,17 @@ Definition factorial : val := λ: "n", Section factorial_spec. Context `{amonadG Σ}. - Lemma incr_spec l (n : Z) R Φ : + Lemma inc_spec l (n : Z) R Φ : l ↦C #n -∗ (l ↦C #(1 + n) -∗ Φ #()) -∗ - AWP incr (cloc_to_val l) @ R {{ Φ }}. - Proof. iIntros "**". awp_lam. vcg. eauto. Qed. + AWP inc (cloc_to_val l) @ R {{ Φ }}. + Proof. + iIntros "? H". iApply a_fun_spec; simpl. vcg; iIntros "? !>". by iApply "H". + Qed. Lemma factorial_spec (n: nat) R : AWP factorial #n @ R {{ v, ⌜v = #(fact n)⌝ }}%I. 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. { 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) "[??]". @@ -32,7 +33,7 @@ Section factorial_spec. iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext. vcg. iIntros "**". case_bool_decide. + 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 !>". assert (fact k * S k = fact (S k)) as -> by (simpl; lia). iApply ("IH" \$! n (S k) with "[%] Hc Hr"). lia. diff --git a/theories/tests/gcd.v b/theories/tests/gcd.v index aeef3f2..c680d38 100644 --- a/theories/tests/gcd.v +++ b/theories/tests/gcd.v @@ -1,6 +1,6 @@ From iris_c.vcgen Require Import proofmode. -Definition gcd : val := λ: "x", +Definition gcd : val := λᶜ "x", "a" ←ᶜ a_ret (Fst "x");ᶜ "b" ←ᶜ a_ret (Snd "x");ᶜ whileᶜ(∗ᶜ(a_ret "a") !=ᶜ ∗ᶜ(a_ret "b")) { @@ -19,7 +19,7 @@ Section gcd_spec. l ↦C #a -∗ r ↦C #b -∗ AWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, ⌜v = #(Z.gcd a b)⌝ }}. Proof. - iIntros (??) "**". awp_lam. vcg; iIntros. + iIntros (??) "**". iApply a_fun_spec; simpl. vcg; iIntros. 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 "[-]"). { iExists a, b. eauto with iFrame. } diff --git a/theories/tests/memcpy.v b/theories/tests/memcpy.v index a1199e1..98f9aaf 100644 --- a/theories/tests/memcpy.v +++ b/theories/tests/memcpy.v @@ -1,6 +1,6 @@ From iris_c.vcgen Require Import proofmode. -Definition memcpy : val := λ: "arg", +Definition memcpy : val := λᶜ "arg", "p" ←mutᶜ a_ret (Fst "arg");ᶜ "q" ←mutᶜ a_ret (Fst (Snd "arg"));ᶜ "n" ←ᶜ a_ret (Snd (Snd "arg"));ᶜ @@ -14,10 +14,10 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R : 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 }}. 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' ∗ 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); destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame. vcg; iIntros "!> !> !> **". diff --git a/theories/tests/par_inc.v b/theories/tests/par_inc.v index b242cde..edec2eb 100644 --- a/theories/tests/par_inc.v +++ b/theories/tests/par_inc.v @@ -1,10 +1,10 @@ From iris_c.vcgen Require Import proofmode. From iris.algebra Require Import frac_auth. -Definition inc : val := λ: "l", +Definition inc : val := λᶜ "l", 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"). Section par_inc. @@ -13,13 +13,15 @@ Section par_inc. Lemma inc_spec R cl (n : Z) Φ : cl ↦C #n -∗ (cl ↦C #(1 + n) -∗ Φ #1) -∗ 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) : cl ↦C #n -∗ AWP par_inc (cloc_to_val cl) @ R {{ v, ⌜ v = #2 ⌝ ∧ cl ↦C #(2 + n) }}. 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|]. set (par_inc_inv := (∃ n' : nat, cl ↦C #(n' + n) ∗ own γ (●! n'))%I). iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). @@ -39,6 +41,6 @@ Section par_inc. - by iApply "H". - 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 (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. End par_inc. \ No newline at end of file diff --git a/theories/tests/swap.v b/theories/tests/swap.v index 1b5b1b6..2e17686 100644 --- a/theories/tests/swap.v +++ b/theories/tests/swap.v @@ -1,24 +1,22 @@ From iris_c.vcgen Require Import proofmode. -Section tests_vcg. +Section swap. Context `{amonadG Σ}. - Definition swap : val := λ: "a", + Definition swap : val := λᶜ "a", "l1" ←ᶜ a_ret (Fst "a");ᶜ - "l2" ←ᶜ a_ret (Fst (Snd "a"));ᶜ - "r" ←ᶜ a_ret (Snd (Snd "a"));ᶜ - (a_ret "r") =ᶜ ∗ᶜ (a_ret "l1") ;ᶜ + "l2" ←ᶜ a_ret (Snd "a");ᶜ + "r" ←mutᶜ ∗ᶜ (a_ret "l1") ;ᶜ (a_ret "l1") =ᶜ ∗ᶜ (a_ret "l2") ;ᶜ (a_ret "l2") =ᶜ ∗ᶜ (a_ret "r") ;ᶜ ♯(). - Lemma swap_spec (l1 l2 r : cloc) (v1 v2: val) R : - r ↦C #0 -∗ l1 ↦C v1 ∗ l2 ↦C v2 -∗ - AWP swap (cloc_to_val l1, (cloc_to_val l2, cloc_to_val r))%V @ R - {{ _, l2 ↦C v1 ∗ l1 ↦C v2 }}. - Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed. + Lemma swap_spec l1 l2 v1 v2 R : + l1 ↦C v1 -∗ l2 ↦C v2 -∗ + AWP swap (cloc_to_val l1, cloc_to_val l2)%V @ R {{ _, l2 ↦C v1 ∗ l1 ↦C v2 }}. + Proof. iIntros. iApply a_fun_spec; simpl. vcg. eauto with iFrame. Qed. - Definition swap_with_alloc : val := λ: "a", + Definition swap_with_alloc : val := λᶜ "a", "l1" ←ᶜ a_ret (Fst "a");ᶜ "l2" ←ᶜ a_ret (Snd "a");ᶜ "r" ←ᶜ allocᶜ (♯1, ♯0);ᶜ @@ -30,5 +28,5 @@ Section tests_vcg. Lemma swap_with_alloc_spec l1 l2 v1 v2 R : 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 }}. - Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed. -End tests_vcg. + Proof. iIntros. iApply a_fun_spec; simpl. vcg; eauto with iFrame. Qed. +End swap. -- GitLab