From 7b28d6e8ae6f9befd21dc89daba5b185d69b467c Mon Sep 17 00:00:00 2001 From: Alejandro Aguirre Date: Mon, 12 Feb 2024 14:29:00 +0100 Subject: [PATCH] Build fixed (thanks Simon!) --- theories/app_rel_logic/primitive_laws.v | 67 +- theories/app_rel_logic/spec_rules.v | 2 + theories/ctx_logic/derived_laws.v | 2 +- theories/ctx_logic/primitive_laws.v | 2 +- theories/ctx_logic/proofmode.v | 9 +- theories/prob_lang/wp_tactics.v | 787 ++++++++++++++++++++++- theories/tpref_logic/examples/flip.v | 2 +- theories/tpref_logic/examples/lib/list.v | 12 +- theories/tpref_logic/primitive_laws.v | 76 ++- theories/tpref_logic/proofmode.v | 31 +- theories/ub_logic/ectx_lifting.v | 30 +- theories/ub_logic/lifting.v | 44 +- theories/ub_logic/primitive_laws.v | 96 ++- theories/ub_logic/proofmode.v | 73 +++ theories/ub_logic/total_ectx_lifting.v | 30 +- theories/ub_logic/total_lifting.v | 40 +- theories/ub_logic/total_primitive_laws.v | 107 ++- theories/ub_logic/ub_rules.v | 14 +- theories/ub_logic/ub_weakestpre.v | 3 +- 19 files changed, 1264 insertions(+), 163 deletions(-) diff --git a/theories/app_rel_logic/primitive_laws.v b/theories/app_rel_logic/primitive_laws.v index 604da63f..aa3a2fc3 100644 --- a/theories/app_rel_logic/primitive_laws.v +++ b/theories/app_rel_logic/primitive_laws.v @@ -79,7 +79,9 @@ Proof. iApply ("IH" with "HΨ"). Qed. + (** Heap *) + Lemma wp_alloc E v : {{{ True }}} Alloc (Val v) @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. Proof. @@ -88,9 +90,68 @@ Proof. iIntros (σ1) "[Hh Ht] !#". solve_red. iIntros "!> /=" (e2 σ2 Hs); inv_head_step. - iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[$ Hl]". + iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]". { apply not_elem_of_dom, fresh_loc_is_fresh. } - iIntros "!>". iFrame. by iApply "HΦ". + iFrame. + rewrite map_union_empty -insert_union_singleton_l. + iFrame. + iIntros "!>". by iApply "HΦ". +Qed. + +Lemma wp_allocN (N : nat) (z : Z) E v: + TCEq N (Z.to_nat z) → + (0 < N)%Z → + {{{ True }}} + AllocN (Val $ LitV $ LitInt $ z) (Val v) @ E + {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v }}}. +Proof. + iIntros (-> Hn Φ) "_ HΦ". + iApply wp_lift_atomic_head_step; [done|]. + iIntros (σ1) "[Hh Ht] !#". + iSplit. + { iPureIntro. + rewrite /head_reducible. + eexists. + apply head_step_support_equiv_rel. + econstructor; eauto. + lia. + } + iIntros "!> /=" (e2 σ2 Hs); inv_head_step. + iMod ((ghost_map_insert_big _ _ with "Hh")) as "[$ Hl]". + iIntros "!>". iFrame. + iApply "HΦ". + iInduction (H) as [ | ?] "IH" forall (σ1). + - simpl. + iSplit; auto. + rewrite map_union_empty. + rewrite loc_add_0. + by rewrite big_sepM_singleton. + - rewrite seq_S. + rewrite heap_array_replicate_S_end. + iPoseProof (big_sepM_union _ _ _ _ with "Hl") as "[H1 H2]". + iApply big_sepL_app. + iSplitL "H1". + + iApply "IH". + { iPureIntro. lia. } + iApply "H1". + + simpl. iSplit; auto. + by rewrite big_sepM_singleton. + Unshelve. + { + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + by apply fresh_loc_offset_is_fresh. + } + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + rewrite dom_singleton. + apply not_elem_of_singleton_2. + intros H2. + apply loc_add_inj in H2. + rewrite replicate_length in H1. + lia. Qed. Lemma wp_load E l dq v : @@ -195,7 +256,7 @@ Proof. iFrame. iModIntro. iApply ("HΦ" with "[$Hl //]"). -Qed. +Qed. End lifting. diff --git a/theories/app_rel_logic/spec_rules.v b/theories/app_rel_logic/spec_rules.v index ddabb98d..7f1d09bc 100644 --- a/theories/app_rel_logic/spec_rules.v +++ b/theories/app_rel_logic/spec_rules.v @@ -54,6 +54,8 @@ Section rules. eapply exec_det_step_ctx; [apply _| |done]. subst l. solve_step. + rewrite state_upd_heap_singleton. + solve_distr. Qed. Lemma step_load E K l q v: diff --git a/theories/ctx_logic/derived_laws.v b/theories/ctx_logic/derived_laws.v index 40f59e4d..fe224d99 100644 --- a/theories/ctx_logic/derived_laws.v +++ b/theories/ctx_logic/derived_laws.v @@ -119,7 +119,7 @@ Lemma wp_allocN s E v n : l ↦∗ replicate (Z.to_nat n) v }}}. Proof. iIntros (? Φ) "_ HΦ". - iApply wp_allocN; auto; try lia. + iApply wp_allocN_seq; auto; try lia. iModIntro. iIntros (l) "Hlm". iApply "HΦ". diff --git a/theories/ctx_logic/primitive_laws.v b/theories/ctx_logic/primitive_laws.v index b4cf7520..29494a8c 100644 --- a/theories/ctx_logic/primitive_laws.v +++ b/theories/ctx_logic/primitive_laws.v @@ -94,7 +94,7 @@ Proof. Qed. -Lemma wp_allocN (N : nat) (z : Z) E v s: +Lemma wp_allocN_seq (N : nat) (z : Z) E v s: TCEq N (Z.to_nat z) → (0 < N)%Z → {{{ True }}} diff --git a/theories/ctx_logic/proofmode.v b/theories/ctx_logic/proofmode.v index 44ebf43f..2cfd174a 100644 --- a/theories/ctx_logic/proofmode.v +++ b/theories/ctx_logic/proofmode.v @@ -3,16 +3,17 @@ From clutch.prob_lang Require Export wp_tactics. From clutch.ctx_logic Require Import primitive_laws derived_laws. From iris.prelude Require Import options. -#[global] Program Instance rel_logic_wptactics_base `{!clutchGS Σ} : @WpTacticsBase Σ unit wp' _ _. + +#[global] Program Instance rel_logic_wptactics_base `{!clutchGS Σ} : @GwpTacticsBase Σ unit _ _ wp. Next Obligation. intros. by apply wp_value. Qed. Next Obligation. intros. by apply wp_fupd. Qed. Next Obligation. intros. by apply wp_bind. Qed. -#[global] Program Instance rel_logic_wptactics_pure `{!clutchGS Σ} : @WpTacticsPure Σ unit wp' true. +#[global] Program Instance rel_logic_wptactics_pure `{!clutchGS Σ} : @GwpTacticsPure Σ unit true wp. Next Obligation. intros. by eapply lifting.wp_pure_step_later. Qed. -#[global] Program Instance rel_logic_wptactics_heap `{!clutchGS Σ} : @WpTacticsHeap Σ unit wp' true := - Build_WpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _. +#[global] Program Instance rel_logic_wptactics_heap `{!clutchGS Σ} : @GwpTacticsHeap Σ unit true wp := + Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _. Next Obligation. intros. by apply wp_alloc. Qed. Next Obligation. intros. by apply wp_allocN. Qed. Next Obligation. intros. by apply wp_load. Qed. diff --git a/theories/prob_lang/wp_tactics.v b/theories/prob_lang/wp_tactics.v index 5c6a64b3..f1ab6702 100644 --- a/theories/prob_lang/wp_tactics.v +++ b/theories/prob_lang/wp_tactics.v @@ -3,41 +3,179 @@ From iris.base_logic.lib Require Import fancy_updates. From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.proofmode Require Export tactics. -From clutch.bi Require Import weakestpre. +(*From clutch.bi Require Import weakestpre.*) From clutch.prob_lang Require Import lang tactics notation class_instances. Set Default Proof Using "Type*". +(* +(* A generic WP *) +Class Gwp (PROP EXPR VAL A : Type) := { + gwp : A → coPset → EXPR → (VAL → PROP) → PROP; + gwp_default : A + }. +Global Arguments gwp {_ _ _ _ _} _ _ _%E _%I. +Global Instance: Params (@gwp) 9 := {}. +Global Arguments gwp_default : simpl never. + +(** Notations for generic weakest preconditions *) +(** Notations without binder -- only parsing because they overlap with the +notations with binder. *) +Local Notation "'WP' e @ s ; E {{ Φ } }" := (gwp s E e%E Φ) + (at level 20, e, Φ at level 200, only parsing) : bi_scope. +Local Notation "'WP' e @ E {{ Φ } }" := (gwp gwp_default E e%E Φ) + (at level 20, e, Φ at level 200, only parsing) : bi_scope. +Local Notation "'WP' e {{ Φ } }" := (gwp gwp_default ⊤ e%E Φ) + (at level 20, e, Φ at level 200, only parsing) : bi_scope. + +(** Notations with binder. *) +Local Notation "'WP' e @ s ; E {{ v , Q } }" := (gwp s E e%E (λ v, Q)) + (at level 20, e, Q at level 200, + format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope. +Local Notation "'WP' e @ E {{ v , Q } }" := (gwp gwp_default E e%E (λ v, Q)) + (at level 20, e, Q at level 200, + format "'[hv' 'WP' e '/' @ E '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope. +Local Notation "'WP' e {{ v , Q } }" := (gwp gwp_default ⊤ e%E (λ v, Q)) + (at level 20, e, Q at level 200, + format "'[hv' 'WP' e '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope. + +(** Texan triples w/one later *) +Local Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' s ; '/' E ']' '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ E '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. + +Local Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ '[' s ; '/' E ']' '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' @ E '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. + +(** Texan triples with [n] laters *) +Local Notation "'{{{' P } } } e 'at' n @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' @ '[' s ; '/' E ']' '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e 'at' n @ E {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' @ E '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e 'at' n {{{ x .. y , 'RET' pat ; Q } } }" := + (□ ∀ Φ, + P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I + (at level 20, x closed binder, y closed binder, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' {{{ '[' x .. y , RET pat ; '/' Q ']' } } } ']'") : bi_scope. + +Local Notation "'{{{' P } } } e 'at' n @ s ; E {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' @ '[' s ; '/' E ']' '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e 'at' n @ E {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' @ E '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. +Local Notation "'{{{' P } } } e 'at' n {{{ 'RET' pat ; Q } } }" := + (□ ∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I + (at level 20, + format "'[hv' {{{ '[' P ']' } } } '/ ' e 'at' n '/' {{{ '[' RET pat ; '/' Q ']' } } } ']'") : bi_scope. + +(** Aliases for stdpp scope -- they inherit the levels and format from above. *) +Local Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope. + +Local Notation "'{{{' P } } } e 'at' n @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e 'at' n @ E {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e 'at' n {{{ x .. y , 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e 'at' n @ s ; E {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e 'at' n @ E {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope. +Local Notation "'{{{' P } } } e 'at' n {{{ 'RET' pat ; Q } } }" := + (∀ Φ, P -∗ ▷^n (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope. + +*) (** A basic set of requirements for a weakest precondition *) -Class WpTacticsBase (Σ : gFunctors) (A : Type) `{Wp (iProp Σ) expr val A} `{!invGS_gen hlc Σ} := { - wptac_wp_value E Φ v a : Φ v ⊢ WP (of_val v) @ a; E {{ Φ }}; - wptac_wp_fupd E Φ e a : WP e @ a; E {{ v, |={E}=> Φ v }} ⊢ WP e @ a; E {{ Φ }}; - wptac_wp_bind K `{!LanguageCtx K} E e Φ a : - WP e @ a; E {{ v, WP K (of_val v) @ a; E {{ Φ }} }} ⊢ WP (K e) @ a; E {{ Φ }}; +Class GwpTacticsBase (Σ : gFunctors) (A : Type) `{!invGS_gen hlc Σ} (gwp : A → coPset → expr → (val → iProp Σ) → iProp Σ) := { + + wptac_wp_value E Φ v a : Φ v ⊢ gwp a E (of_val v) Φ; + wptac_wp_fupd E Φ e a : gwp a E e (λ v, |={E}=> Φ v) ⊢ gwp a E e Φ; + wptac_wp_bind K `{!LanguageCtx K} E e Φ a : + gwp a E e (λ v, gwp a E (K (of_val v)) Φ ) ⊢ gwp a E (K e) Φ ; }. -(** Pure evaluation steps with or without laters *) -Class WpTacticsPure Σ A `{Wp (iProp Σ) expr val A} (laters : bool) := { +Class GwpTacticsPure Σ A (laters : bool) (gwp : A → coPset → expr → (val → iProp Σ) → iProp Σ) := { wptac_wp_pure_step E e1 e2 φ n Φ a : PureExec φ n e1 e2 → φ → - ▷^(if laters then n else 0) WP e2 @ a; E {{ Φ }} ⊢ WP e1 @ a; E {{ Φ }}; + ▷^(if laters then n else 0) (gwp a E e2 Φ) ⊢ (gwp a E e1 Φ); }. (** Heap *) -Class WpTacticsHeap Σ A `{Wp (iProp Σ) expr val A} (laters : bool) := { +Class GwpTacticsHeap Σ A (laters : bool) (gwp : A → coPset → expr → (val → iProp Σ) → iProp Σ):= { wptac_mapsto : loc → dfrac → val → iProp Σ; wptac_mapsto_array : loc → dfrac → (list val) → iProp Σ; wptac_wp_alloc E v a : - {{{ True }}} - (Alloc (Val v)) at (if laters then 1 else 0) @ a; E - {{{ l, RET LitV (LitLoc l); wptac_mapsto l (DfracOwn 1) v }}}; - wptac_wp_allocN E v n a : + ∀ Φ, True -∗ (▷^(if laters then 1 else 0) (∀ l, (wptac_mapsto l (DfracOwn 1) v) -∗ Φ (LitV (LitLoc l))%V)) -∗ + gwp a E (Alloc (Val v)) Φ; + + wptac_wp_allocN E v n a : (0 < n)%Z → - {{{ True }}} - (AllocN (Val $ LitV $ LitInt $ n) (Val v)) at (if laters then 1 else 0) @ a; E - {{{ l, RET LitV (LitLoc l); wptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v) }}}; - wptac_wp_load E v l dq a : + ∀ Φ, True -∗ (▷^(if laters then 1 else 0) (∀ l, (wptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v)) -∗ Φ (LitV (LitLoc l))%V)) -∗ + gwp a E (AllocN (Val $ LitV $ LitInt $ n) (Val v)) Φ ; + + wptac_wp_load E v l dq a : + ∀ Φ, (▷ wptac_mapsto l dq v) -∗ (▷^(if laters then 1 else 0) ((wptac_mapsto l dq v) -∗ Φ v%V)) -∗ + gwp a E (Load (Val $ LitV $ LitLoc l)) Φ; + + wptac_wp_store E v v' l a : + ∀ Φ, (▷ wptac_mapsto l (DfracOwn 1) v') -∗ (▷^(if laters then 1 else 0) ((wptac_mapsto l (DfracOwn 1) v) -∗ Φ (LitV (LitUnit))%V)) -∗ + gwp a E (Store (Val $ LitV $ LitLoc l) (Val v)) Φ; + + }. + +(* +{{{ True }}} + (Alloc (Val v)) at (if laters then 1 else 0) @ a; E + {{{ l, RET LitV (LitLoc l); wptac_mapsto l (DfracOwn 1) v }}}; +wptac_wp_allocN E v n a : + (0 < n)%Z → + {{{ True }}} + (AllocN (Val $ LitV $ LitInt $ n) (Val v)) at (if laters then 1 else 0) @ a; E + {{{ l, RET LitV (LitLoc l); wptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v) }}}; +wptac_wp_load E v l dq a : {{{ ▷ wptac_mapsto l dq v }}} Load (Val $ LitV $ LitLoc l) at (if laters then 1 else 0) @ a; E {{{ RET v; wptac_mapsto l dq v }}}; @@ -46,16 +184,26 @@ Class WpTacticsHeap Σ A `{Wp (iProp Σ) expr val A} (laters : bool) := { Store (Val $ LitV (LitLoc l)) (Val v) at (if laters then 1 else 0) @ a; E {{{ RET LitV LitUnit; wptac_mapsto l (DfracOwn 1) v }}}; }. +*) Section wp_tactics. - Context `{WpTacticsBase Σ A}. + + Context `{GwpTacticsBase Σ A hlc gwp}. + +Local Notation "'WP' e @ s ; E {{ Φ } }" := (gwp s E e%E Φ) + (at level 20, e, Φ at level 200, only parsing) : bi_scope. + +(** Notations with binder. *) +Local Notation "'WP' e @ s ; E {{ v , Q } }" := (gwp s E e%E (λ v, Q)) + (at level 20, e, Q at level 200, + format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope. Lemma tac_wp_expr_eval Δ a E Φ e e' : (∀ (e'':=e'), e = e'') → envs_entails Δ (WP e' @ a; E {{ Φ }}) → envs_entails Δ (WP e @ a; E {{ Φ }}). Proof. by intros ->. Qed. - Lemma tac_wp_pure_later laters `{!WpTacticsPure Σ A laters} Δ Δ' E K e1 e2 φ n Φ a : + Lemma tac_wp_pure_later laters `{!GwpTacticsPure Σ A laters gwp} Δ Δ' E K e1 e2 φ n Φ a : PureExec φ n e1 e2 → φ → MaybeIntoLaterNEnvs (if laters then n else 0) Δ Δ' → @@ -84,14 +232,482 @@ Section wp_tactics. End wp_tactics. + +Tactic Notation "wp_expr_eval" tactic3(t) := + iStartProof; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _ ); + [apply _|let x := fresh in intros x; simpl; unfold x; notypeclasses refine eq_refl|] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _ ); + [apply _|let x := fresh in intros x; simpl; unfold x; notypeclasses refine eq_refl|] + | _ => fail "wp_expr_eval: not a 'wp'" + end. +Ltac wp_expr_simpl := wp_expr_eval simpl. + +(** Simplify the goal if it is [wp] of a value. + If the postcondition already allows a fupd, do not add a second one. + But otherwise, *do* add a fupd. This ensures that all the lemmas applied + here are bidirectional, so we never will make a goal unprovable. *) +Ltac wp_value_head := + lazymatch goal with + | |- envs_entails _ (wp ?s ?E (of_val _) (λ _, fupd ?E _ _)) => + eapply tac_wp_value_nofupd + | |- envs_entails _ (wp ?s ?E (of_val _) (λ _, wp _ ?E _ _)) => + eapply tac_wp_value_nofupd + | |- envs_entails _ (wp ?s ?E (of_val _) _) => + eapply tac_wp_value' + | |- envs_entails _ (twp ?s ?E (of_val _) (λ _, fupd ?E _ _)) => + eapply tac_wp_value_nofupd + | |- envs_entails _ (twp ?s ?E (of_val _) (λ _, twp _ ?E _ _)) => + eapply tac_wp_value_nofupd + | |- envs_entails _ (twp ?s ?E (of_val _) _) => + eapply tac_wp_value' + end. + +Ltac wp_finish := + (* simplify occurences of [wptac_mapsto] projections *) + rewrite ?[wptac_mapsto _ _ _]/=; + (* simplify occurences of subst/fill *) + wp_expr_simpl; + (* in case we have reached a value, get rid of the wp *) + try wp_value_head; + (* prettify ▷s caused by [MaybeIntoLaterNEnvs] and λs caused by wp_value *) + pm_prettify. + +Ltac solve_vals_compare_safe := + (* The first branch is for when we have [vals_compare_safe] in the context. + The other two branches are for when either one of the branches reduces to + [True] or we have it in the context. *) + fast_done || (left; fast_done) || (right; fast_done). + +(** The argument [efoc] can be used to specify the construct that should be +reduced. For example, you can write [wp_pure (EIf _ _ _)], which will search +for an [EIf _ _ _] in the expression, and reduce it. + +The use of [open_constr] in this tactic is essential. It will convert all holes +(i.e. [_]s) into evars, that later get unified when an occurences is found +(see [unify e' efoc] in the code below). *) +Tactic Notation "wp_pure" open_constr(efoc) := + iStartProof; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + let e := eval simpl in e in + reshape_expr e ltac:(fun K e' => + unify e' efoc; + eapply (tac_wp_pure_later _ _ _ _ K e'); + [iSolveTC (* PureExec *) + |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *) + |iSolveTC (* IntoLaters *) + |wp_finish (* new goal *) + ]) + || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex" + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + let e := eval simpl in e in + reshape_expr e ltac:(fun K e' => + unify e' efoc; + eapply (tac_wp_pure_later _ _ _ _ K e'); + [iSolveTC (* PureExec *) + |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *) + |iSolveTC (* IntoLaters *) + |wp_finish (* new goal *) + ]) + || fail "Hello! wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex" + | _ => fail "wp_pure: not a 'wp'" + end. + +Tactic Notation "wp_pure" := + wp_pure _. + +Ltac wp_pures := + iStartProof; + first [ (* The `;[]` makes sure that no side-condition magically spawns. *) + progress repeat (wp_pure _; []) + | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *) + ]. + + +(** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce + lambdas/recs that are hidden behind a definition, i.e. they should use + [AsRecV_recv] as a proper instance instead of a [Hint Extern]. + + We achieve this by putting [AsRecV_recv] in the current environment so that it + can be used as an instance by the typeclass resolution system. We then perform + the reduction, and finally we clear this new hypothesis. *) +Tactic Notation "wp_rec" := + let H := fresh in + assert (H := AsRecV_recv); + wp_pure (App _ _); + clear H. + +Tactic Notation "wp_if" := wp_pure (If _ _ _). +Tactic Notation "wp_if_true" := wp_pure (If (LitV (LitBool true)) _ _). +Tactic Notation "wp_if_false" := wp_pure (If (LitV (LitBool false)) _ _). +Tactic Notation "wp_unop" := wp_pure (UnOp _ _). +Tactic Notation "wp_binop" := wp_pure (BinOp _ _ _). +Tactic Notation "wp_op" := wp_unop || wp_binop. +Tactic Notation "wp_lam" := wp_rec. +Tactic Notation "wp_let" := wp_pure (Rec BAnon (BNamed _) _); wp_lam. +Tactic Notation "wp_seq" := wp_pure (Rec BAnon BAnon _); wp_lam. +Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _). +Tactic Notation "wp_case" := wp_pure (Case _ _ _). +Tactic Notation "wp_match" := wp_case; wp_pure (Rec _ _ _); wp_lam. +Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _). +Tactic Notation "wp_pair" := wp_pure (Pair _ _). +Tactic Notation "wp_closure" := wp_pure (Rec _ _ _). + +Ltac wp_bind_core K := + lazymatch eval hnf in K with + | [] => idtac + | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify] + end. + +Tactic Notation "wp_bind" open_constr(efoc) := + iStartProof; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) + | fail 1 "wp_bind: cannot find" efoc "in" e ] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) + | fail 1 "wp_bind: cannot find" efoc "in" e ] + | _ => fail "wp_bind: not a 'wp'" + end. + +(** The tactic [wp_apply_core lem tac_suc tac_fail] evaluates [lem] to a + hypothesis [H] that can be applied, and then runs [wp_bind_core K; tac_suc H] + for every possible evaluation context [K]. + + - The tactic [tac_suc] should do [iApplyHyp H] to actually apply the hypothesis, + but can perform other operations in addition (see [wp_apply] and [awp_apply] + below). + - The tactic [tac_fail cont] is called when [tac_suc H] fails for all evaluation + contexts [K], and can perform further operations before invoking [cont] to + try again. + + TC resolution of [lem] premises happens *after* [tac_suc H] got executed. *) + +Ltac wp_apply_core lem tac_suc tac_fail := first + [iPoseProofCore lem as false (fun H => + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + reshape_expr e ltac:(fun K e' => wp_bind_core K; tac_suc H) + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + reshape_expr e ltac:(fun K e' => wp_bind_core K; tac_suc H) + | _ => fail 1 "wp_apply: not a 'wp'" + end) + |tac_fail ltac:(fun _ => wp_apply_core lem tac_suc tac_fail) + |let P := type of lem in + fail "wp_apply: cannot apply" lem ":" P ]. + +Tactic Notation "wp_apply" open_constr(lem) := + wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl) + ltac:(fun cont => fail). +Tactic Notation "wp_smart_apply" open_constr(lem) := + wp_apply_core lem ltac:(fun H => iApplyHyp H; try iNext; try wp_expr_simpl) + ltac:(fun cont => wp_pure _; []; cont ()). + +Section heap_tactics. + + Context `{GwpTacticsBase Σ A hlc gwp, !GwpTacticsHeap Σ A laters gwp}. + + +Local Notation "'WP' e @ s ; E {{ Φ } }" := (gwp s E e%E Φ) + (at level 20, e, Φ at level 200, only parsing) : bi_scope. + +(** Notations with binder. *) +Local Notation "'WP' e @ s ; E {{ v , Q } }" := (gwp s E e%E (λ v, Q)) + (at level 20, e, Q at level 200, + format "'[hv' 'WP' e '/' @ '[' s ; '/' E ']' '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope. + + Lemma tac_wp_alloc Δ Δ' E j K v Φ a : + MaybeIntoLaterNEnvs (if laters then 1 else 0) Δ Δ' → + (∀ (l : loc), + match envs_app false (Esnoc Enil j (wptac_mapsto l (DfracOwn 1) v)) Δ' with + | Some Δ'' => + envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ a ; E {{ Φ }}) + | None => False + end) → + envs_entails Δ (WP fill K (Alloc (Val v)) @ a; E {{ Φ }}). + Proof. + rewrite envs_entails_unseal=> ? HΔ. + rewrite -wptac_wp_bind. + eapply bi.wand_apply; first exact: wptac_wp_alloc. + rewrite left_id into_laterN_env_sound. + apply bi.laterN_mono, bi.forall_intro=> l. + specialize (HΔ l). + destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [| contradiction]. + rewrite envs_app_sound //; simpl. + apply bi.wand_intro_l. + rewrite right_id. + rewrite bi.wand_elim_r //. + Qed. + + Lemma tac_wp_allocN Δ Δ' E j K v n Φ a : + (0 < n)%Z → + MaybeIntoLaterNEnvs (if laters then 1 else 0) Δ Δ' → + (∀ l, + match envs_app false (Esnoc Enil j (wptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ' with + | Some Δ'' => + envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ a; E {{ Φ }}) + | None => False + end) → + envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ a; E {{ Φ }}). + Proof. + rewrite envs_entails_unseal=> ? ? HΔ. + rewrite -wptac_wp_bind. + eapply bi.wand_apply; first exact: wptac_wp_allocN. + rewrite left_id into_laterN_env_sound. + apply bi.laterN_mono, bi.forall_intro=> l. + specialize (HΔ l). + destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. + rewrite envs_app_sound //; simpl. + apply bi.wand_intro_l. + rewrite right_id. + rewrite bi.wand_elim_r //. + Qed. + + + Lemma tac_wp_load Δ Δ' E i K b l dq v Φ a : + MaybeIntoLaterNEnvs (if laters then 1 else 0) Δ Δ' → + envs_lookup i Δ' = Some (b, wptac_mapsto l dq v) → + envs_entails Δ' (WP fill K (Val v) @ a; E {{ Φ }}) → + envs_entails Δ (WP fill K (Load (Val $ LitV $ LitLoc l)) @ a; E {{ Φ }}). + Proof. + rewrite envs_entails_unseal=> ?? Hi. + rewrite -wptac_wp_bind. eapply bi.wand_apply; [exact: wptac_wp_load|]. + rewrite into_laterN_env_sound. + destruct laters. + - rewrite -bi.later_sep. + rewrite envs_lookup_split //; simpl. + apply bi.later_mono. + destruct b; simpl. + * iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#". + * by apply bi.sep_mono_r, bi.wand_mono. + - rewrite envs_lookup_split //; simpl. + destruct b; simpl. + * iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#". + * iIntros "[$ He] H". iApply Hi. by iApply "He". + Qed. + + Lemma tac_wp_store Δ Δ' E i K l v v' Φ a : + MaybeIntoLaterNEnvs (if laters then 1 else 0) Δ Δ' → + envs_lookup i Δ' = Some (false, wptac_mapsto l (DfracOwn 1) v)%I → + match envs_simple_replace i false (Esnoc Enil i (wptac_mapsto l (DfracOwn 1) v')) Δ' with + | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ a; E {{ Φ }}) + | None => False + end → + envs_entails Δ (WP fill K (Store (Val $ LitV $ LitLoc l) (Val v')) @ a; E {{ Φ }}). + Proof. + rewrite envs_entails_unseal=> ?? Hcnt. + destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ]. + rewrite -wptac_wp_bind. eapply bi.wand_apply; [by eapply wptac_wp_store|]. + rewrite into_laterN_env_sound. + destruct laters. + - rewrite -bi.later_sep envs_simple_replace_sound //; simpl. + rewrite right_id. by apply bi.later_mono, bi.sep_mono_r, bi.wand_mono. + - rewrite envs_simple_replace_sound //; simpl. + rewrite right_id. + iIntros "[$ He] H". iApply Hcnt. by iApply "He". + Qed. + +End heap_tactics. + +Tactic Notation "wp_alloc" ident(l) "as" constr(H) := + let Htmp := iFresh in + let finish _ := + first [intros l | fail 1 "wp_alloc:" l "not fresh"]; + pm_reduce; + lazymatch goal with + | |- False => fail 1 "wp_alloc:" H "not fresh" + | _ => iDestructHyp Htmp as H; wp_finish + end in + wp_pures; + (** The code first tries to use allocation lemma for a single reference, + ie, [tac_wp_alloc] (respectively, [tac_twp_alloc]). + If that fails, it tries to use the lemma [tac_wp_allocN] + (respectively, [tac_twp_allocN]) for allocating an array. + Notice that we could have used the array allocation lemma also for single + references. However, that would produce the resource l ↦∗ [v] instead of + l ↦ v for single references. These are logically equivalent assertions + but are not equal. *) +lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + let process_single _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + [iSolveTC + |finish ()] + in + let process_array _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + [idtac| iSolveTC + |finish ()] + in (process_single ()) || (process_array ()) +| |- envs_entails _ (twp ?s ?E ?e ?Q) => + let process_single _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + [iSolveTC + |finish ()] + in + let process_array _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + [idtac| iSolveTC + |finish ()] + in (process_single ()) || (process_array ()) + | _ => fail "wp_alloc: not a 'wp'" + end. + + +Tactic Notation "wp_alloc" ident(l) := + wp_alloc l as "?". + +Tactic Notation "wp_load" := + let solve_wptac_mapsto _ := + let l := match goal with |- _ = Some (_, (wptac_mapsto ?l _ _)%I) => l end in + iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in + wp_pures; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K)) + |fail 1 "wp_load: cannot find 'Load' in" e]; + [iSolveTC + |solve_wptac_mapsto () + |wp_finish] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K)) + |fail 1 "wp_load: cannot find 'Load' in" e]; + [iSolveTC + |solve_wptac_mapsto () + |wp_finish] + | _ => fail "wp_load: not a 'wp'" + end. + +Tactic Notation "wp_store" := + let solve_wptac_mapsto _ := + let l := match goal with |- _ = Some (_, (wptac_mapsto ?l _ _)%I) => l end in + iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in + wp_pures; + lazymatch goal with + | |- envs_entails _ (wp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ K)) + |fail 1 "wp_store: cannot find 'Store' in" e]; + [iSolveTC + |solve_wptac_mapsto () + |pm_reduce; first [wp_seq|wp_finish]] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_wp_store _ _ _ _ K)) + |fail 1 "wp_store: cannot find 'Store' in" e]; + [iSolveTC + |solve_wptac_mapsto () + |pm_reduce; first [wp_seq|wp_finish]] + | _ => fail "wp_store: not a 'wp'" + end. + +(* + + +(** A basic set of requirements for a weakest precondition *) +Class TwpTacticsBase (Σ : gFunctors) (A : Type) `{Twp (iProp Σ) expr val A} `{!invGS_gen hlc Σ} := { + twptac_twp_value E Φ v a : Φ v ⊢ WP (of_val v) @ a; E [{ Φ }]; + twptac_twp_fupd E Φ e a : WP e @ a; E [{ v, |={E}=> Φ v }] ⊢ WP e @ a; E [{ Φ }]; + twptac_twp_bind K `{!LanguageCtx K} E e Φ a : + WP e @ a; E [{ v, WP K (of_val v) @ a; E [{ Φ }] }] ⊢ WP (K e) @ a; E [{ Φ }]; +}. + +(** Pure evaluation steps with or without laters *) +Class TwpTacticsPure Σ A `{Twp (iProp Σ) expr val A} := { + twptac_twp_pure_step E e1 e2 φ n Φ a : + PureExec φ n e1 e2 → + φ → + WP e2 @ a; E [{ Φ }] ⊢ WP e1 @ a; E [{ Φ }]; +}. + +(** Heap *) +Class TwpTacticsHeap Σ A `{Twp (iProp Σ) expr val A} := { + twptac_mapsto : loc → dfrac → val → iProp Σ; + twptac_mapsto_array : loc → dfrac → (list val) → iProp Σ; + + twptac_twp_alloc E v a : + [[{ True }]] + (Alloc (Val v)) @ a; E + [[{ l, RET LitV (LitLoc l); twptac_mapsto l (DfracOwn 1) v }]]; + twptac_twp_allocN E v n a : + (0 < n)%Z → + [[{ True }]] + (AllocN (Val $ LitV $ LitInt $ n) (Val v)) @ a; E + [[{ l, RET LitV (LitLoc l); twptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v) }]]; + twptac_twp_load E v l dq a : + [[{ twptac_mapsto l dq v }]] + Load (Val $ LitV $ LitLoc l) @ a; E + [[{ RET v; twptac_mapsto l dq v }]]; + twptac_twp_store E v v' l a : + [[{ twptac_mapsto l (DfracOwn 1) v' }]] + Store (Val $ LitV (LitLoc l)) (Val v) @ a; E + [[{ RET LitV LitUnit; twptac_mapsto l (DfracOwn 1) v }]] + }. + +Section twp_tactics. + Context `{TwpTacticsBase Σ A}. + + Lemma tac_twp_expr_eval Δ a E Φ e e' : + (∀ (e'':=e'), e = e'') → + envs_entails Δ (WP e' @ a; E [{ Φ }]) → envs_entails Δ (WP e @ a; E [{ Φ }]). + Proof. by intros ->. Qed. + + Lemma tac_twp_pure_later `{!TwpTacticsPure Σ A} Δ E K e1 e2 φ n Φ a : + PureExec φ n e1 e2 → + φ → + envs_entails Δ (WP (fill K e2) @ a; E [{ Φ }]) → + envs_entails Δ (WP (fill K e1) @ a; E [{ Φ }]). + Proof. + rewrite envs_entails_unseal. + intros ?? HΔ'. + (* We want [pure_exec_fill] to be available to TC search locally. *) + pose proof @pure_exec_fill. + rewrite HΔ' -twptac_twp_pure_step //. + Qed. + + Lemma tac_twp_value_nofupd Δ E Φ v a : + envs_entails Δ (Φ v) → envs_entails Δ (WP (of_val v) @ a; E [{ Φ }]). + Proof. rewrite envs_entails_unseal=> ->. apply twptac_twp_value. Qed. + + Lemma tac_twp_value' Δ E Φ v a : + envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (of_val v) @ a; E [{ Φ }]). + Proof. rewrite envs_entails_unseal=> ->. by rewrite -twptac_twp_fupd -twptac_twp_value. Qed. + + Lemma tac_twp_bind K Δ E Φ e f a : + f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *) + envs_entails Δ (WP e @ a; E [{ v, WP f (Val v) @ a; E [{ Φ }] }])%I → + envs_entails Δ (WP fill K e @ a; E [{ Φ }]). + Proof. rewrite envs_entails_unseal=> -> ->. by apply: twptac_twp_bind. Qed. + +End twp_tactics. + Tactic Notation "wp_expr_eval" tactic3(t) := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => notypeclasses refine (tac_wp_expr_eval _ _ _ _ e _ _ _ ); [apply _|let x := fresh in intros x; simpl; unfold x; notypeclasses refine eq_refl|] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + notypeclasses refine (tac_twp_expr_eval _ _ _ _ e _ _ _ ); + [apply _|let x := fresh in intros x; simpl; unfold x; notypeclasses refine eq_refl|] | _ => fail "wp_expr_eval: not a 'wp'" end. + Ltac wp_expr_simpl := wp_expr_eval simpl. (** Simplify the goal if it is [wp] of a value. @@ -106,11 +722,18 @@ Ltac wp_value_head := eapply tac_wp_value_nofupd | |- envs_entails _ (wp ?s ?E (of_val _) _) => eapply tac_wp_value' + | |- envs_entails _ (twp ?s ?E (of_val _) (λ _, fupd ?E _ _)) => + eapply tac_twp_value_nofupd + | |- envs_entails _ (twp ?s ?E (of_val _) (λ _, twp _ ?E _ _)) => + eapply tac_twp_value_nofupd + | |- envs_entails _ (twp ?s ?E (of_val _) _) => + eapply tac_twp_value' end. Ltac wp_finish := (* simplify occurences of [wptac_mapsto] projections *) rewrite ?[wptac_mapsto _ _ _]/=; + rewrite ?[twptac_mapsto _ _ _]/=; (* simplify occurences of subst/fill *) wp_expr_simpl; (* in case we have reached a value, get rid of the wp *) @@ -145,6 +768,16 @@ Tactic Notation "wp_pure" open_constr(efoc) := |wp_finish (* new goal *) ]) || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex" + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + let e := eval simpl in e in + reshape_expr e ltac:(fun K e' => + unify e' efoc; + eapply (tac_twp_pure_later _ _ K e'); + [iSolveTC (* PureExec *) + |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals *) + |wp_finish (* new goal *) + ]) + || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex" | _ => fail "wp_pure: not a 'wp'" end. @@ -194,12 +827,21 @@ Ltac wp_bind_core K := | _ => eapply (tac_wp_bind K); [simpl; reflexivity|reduction.pm_prettify] end. +Ltac twp_bind_core K := + lazymatch eval hnf in K with + | [] => idtac + | _ => eapply (tac_twp_bind K); [simpl; reflexivity|reduction.pm_prettify] + end. + Tactic Notation "wp_bind" open_constr(efoc) := iStartProof; lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K) | fail 1 "wp_bind: cannot find" efoc "in" e ] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first [ reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K) + | fail 1 "wp_bind: cannot find" efoc "in" e ] | _ => fail "wp_bind: not a 'wp'" end. @@ -219,7 +861,9 @@ Ltac wp_apply_core lem tac_suc tac_fail := first [iPoseProofCore lem as false (fun H => lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => - reshape_expr e ltac:(fun K e' => wp_bind_core K; tac_suc H) + reshape_expr e ltac:(fun K e' => wp_bind_core K; tac_suc H) + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + reshape_expr e ltac:(fun K e' => twp_bind_core K; tac_suc H) | _ => fail 1 "wp_apply: not a 'wp'" end) |tac_fail ltac:(fun _ => wp_apply_core lem tac_suc tac_fail) @@ -236,6 +880,8 @@ Tactic Notation "wp_smart_apply" open_constr(lem) := Section heap_tactics. Context `{WpTacticsBase Σ A, !WpTacticsHeap Σ A laters}. + Context `{TwpTacticsBase Σ A, !TwpTacticsHeap Σ A}. + Lemma tac_wp_alloc Δ Δ' E j K v Φ a : MaybeIntoLaterNEnvs (if laters then 1 else 0) Δ Δ' → (∀ (l : loc), @@ -327,6 +973,79 @@ Section heap_tactics. iIntros "[$ He] H". iApply Hcnt. by iApply "He". Qed. + + Lemma tac_twp_alloc Δ E j K v Φ a : + (∀ (l : loc), + match envs_app false (Esnoc Enil j (twptac_mapsto l (DfracOwn 1) v)) Δ with + | Some Δ'' => + envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ a ; E [{ Φ }]) + | None => False + end) → + envs_entails Δ (WP fill K (Alloc (Val v)) @ a; E [{ Φ }]). + Proof. + rewrite envs_entails_unseal=> HΔ. + rewrite -twptac_twp_bind. + eapply bi.wand_apply; first exact: twptac_twp_alloc. + rewrite left_id. apply bi.forall_intro=> l. + specialize (HΔ l). + destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. + rewrite envs_app_sound //; simpl. + apply bi.wand_intro_l. + rewrite right_id. + rewrite bi.wand_elim_r //. + Qed. + + Lemma tac_twp_allocN Δ E j K v n Φ a : + (0 < n)%Z → + (∀ l, + match envs_app false (Esnoc Enil j (twptac_mapsto_array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ with + | Some Δ'' => + envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ a; E [{ Φ }]) + | None => False + end) → + envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ a; E [{ Φ }]). + Proof. + rewrite envs_entails_unseal=> ? HΔ. + rewrite -twptac_twp_bind. + eapply bi.wand_apply; first exact: twptac_twp_allocN. + rewrite left_id. + apply bi.forall_intro=> l. + specialize (HΔ l). + destruct (envs_app _ _ _) as [Δ''|] eqn:HΔ'; [ | contradiction ]. + rewrite envs_app_sound //; simpl. + apply bi.wand_intro_l. + rewrite right_id. + rewrite bi.wand_elim_r //. + Qed. + + Lemma tac_twp_load Δ E i K b l dq v Φ a : + envs_lookup i Δ = Some (b, twptac_mapsto l dq v)%I → + envs_entails Δ (WP fill K (Val v) @ a; E [{ Φ }]) → + envs_entails Δ (WP fill K (Load (Val $ LitV $ LitLoc l)) @ a; E [{ Φ }]). + Proof. + rewrite envs_entails_unseal=> ? Hi. + rewrite -twptac_twp_bind. eapply bi.wand_apply; [exact: twptac_twp_load|]. + rewrite envs_lookup_split //; simpl. + destruct b; simpl. + - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#". + - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl". + Qed. + + Lemma tac_twp_store Δ E i K l v v' Φ a : + envs_lookup i Δ = Some (false, twptac_mapsto l (DfracOwn 1) v)%I → + match envs_simple_replace i false (Esnoc Enil i (twptac_mapsto l (DfracOwn 1) v')) Δ with + | Some Δ'' => envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ a; E [{ Φ }]) + | None => False + end → + envs_entails Δ (WP fill K (Store (Val $ LitV $ LitLoc l) (Val v')) @ a; E [{ Φ }]). + Proof. + rewrite envs_entails_unseal=> ? Hcnt. + destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ]. + rewrite -twptac_twp_bind. eapply bi.wand_apply; [by eapply twptac_twp_store|]. + rewrite envs_simple_replace_sound //; simpl. + rewrite right_id. by apply bi.sep_mono_r, bi.wand_mono. + Qed. + End heap_tactics. Tactic Notation "wp_alloc" ident(l) "as" constr(H) := @@ -363,6 +1082,19 @@ lazymatch goal with [idtac| iSolveTC |finish ()] in (process_single ()) || (process_array ()) +| |- envs_entails _ (twp ?s ?E ?e ?Q) => + let process_single _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + finish () + in + let process_array _ := + first + [reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K)) + |fail 1 "wp_alloc: cannot find 'Alloc' in" e]; + [idtac |finish ()] + in (process_single ()) || (process_array ()) | _ => fail "wp_alloc: not a 'wp'" end. @@ -383,6 +1115,12 @@ Tactic Notation "wp_load" := [iSolveTC |solve_wptac_mapsto () |wp_finish] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K)) + |fail 1 "wp_load: cannot find 'Load' in" e]; + [solve_wptac_mapsto () + |wp_finish] | _ => fail "wp_load: not a 'wp'" end. @@ -399,5 +1137,12 @@ Tactic Notation "wp_store" := [iSolveTC |solve_wptac_mapsto () |pm_reduce; first [wp_seq|wp_finish]] + | |- envs_entails _ (twp ?s ?E ?e ?Q) => + first + [reshape_expr e ltac:(fun K e' => eapply (tac_twp_store _ _ _ _ K)) + |fail 1 "wp_store: cannot find 'Store' in" e]; + [solve_wptac_mapsto () + |pm_reduce; first [wp_seq|wp_finish]] | _ => fail "wp_store: not a 'wp'" end. +*) diff --git a/theories/tpref_logic/examples/flip.v b/theories/tpref_logic/examples/flip.v index e7d913be..fb71a04c 100644 --- a/theories/tpref_logic/examples/flip.v +++ b/theories/tpref_logic/examples/flip.v @@ -1,6 +1,6 @@ From clutch.prob Require Import distribution markov. From clutch.prob_lang Require Import lang notation. -From clutch.tpref_logic Require Import weakestpre spec primitive_laws proofmode. +From clutch.tpref_logic Require Import weakestpre spec primitive_laws derived_laws proofmode. Section coupl. Context `{!tprG δ Σ}. diff --git a/theories/tpref_logic/examples/lib/list.v b/theories/tpref_logic/examples/lib/list.v index 90eb2bde..9d9ee071 100644 --- a/theories/tpref_logic/examples/lib/list.v +++ b/theories/tpref_logic/examples/lib/list.v @@ -2,6 +2,9 @@ From clutch.prob Require Import distribution markov. From clutch.prob_lang Require Import lang notation. From clutch.tpref_logic Require Import weakestpre spec primitive_laws proofmode. + +From iris.proofmode Require Import proofmode. + (** * Linked list *) Definition list_create : val := λ: <>, NONEV. @@ -22,7 +25,7 @@ Section list. | [] => ⌜v = NONEV⌝ | x :: xs => ∃ (l : loc) (v' : val), ⌜v = SOMEV #l⌝ ∗ l ↦ (x, v')%V ∗ is_list v' xs - end. + end. #[global] Instance timeless_is_list l vs : Timeless (is_list l vs). @@ -31,9 +34,12 @@ Section list. Lemma wp_list_create E : ⟨⟨⟨ True ⟩⟩⟩ list_create #() @ E - ⟨⟨⟨ (l : val), RET l; is_list l [] ⟩⟩⟩. + ⟨⟨⟨ (l : val), RET l; is_list l [] ⟩⟩⟩. Proof. - iIntros (Φ) "_ HΦ". wp_rec. iModIntro. iApply "HΦ". eauto. + iIntros (Φ) "_ HΦ". + Set Printing All. + wp_rec. + iModIntro. iApply "HΦ". eauto. Qed. Lemma wp_list_cons v x xs E : diff --git a/theories/tpref_logic/primitive_laws.v b/theories/tpref_logic/primitive_laws.v index 5ad12922..de2f0aeb 100644 --- a/theories/tpref_logic/primitive_laws.v +++ b/theories/tpref_logic/primitive_laws.v @@ -81,11 +81,70 @@ Section rwp. iIntros (σ1) "[Hh Ht] !# !>". iSplit; [by eauto with head_step|]. iIntros (e2 σ2 Hs); inv_head_step. - iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[$ Hl]". + iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]". { apply not_elem_of_dom, fresh_loc_is_fresh. } - iIntros "!>". iFrame. by iApply "HΦ". + iFrame. + rewrite map_union_empty -insert_union_singleton_l. + iFrame. + iIntros "!>". by iApply "HΦ". Qed. +Lemma rswp_allocN_seq (N : nat) (z : Z) k E v a: + TCEq N (Z.to_nat z) → + (0 < N)%Z → + ⟨⟨⟨ True ⟩⟩⟩ + AllocN (Val $ LitV $ LitInt $ z) (Val v) at k @ a; E + ⟨⟨⟨ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v ⟩⟩⟩. +Proof. + iIntros (-> Hn Φ) "_ HΦ". + iApply rswp_lift_atomic_head_step. + iIntros (σ1) "[Hh Ht] !# !>". + iSplit. + { iPureIntro. + rewrite /head_reducible. + eexists. + apply head_step_support_equiv_rel. + econstructor; eauto. + lia. + } + iIntros (e2 σ2 Hs); inv_head_step. + iMod ((ghost_map_insert_big _ _ with "Hh")) as "[$ Hl]". + iIntros "!>". iFrame. + iApply "HΦ". + iInduction (H0) as [ | ?] "IH" forall (σ1). + - simpl. + iSplit; auto. + rewrite map_union_empty. + rewrite loc_add_0. + by rewrite big_sepM_singleton. + - rewrite seq_S. + rewrite heap_array_replicate_S_end. + iPoseProof (big_sepM_union _ _ _ _ with "Hl") as "[H1 H2]". + iApply big_sepL_app. + iSplitL "H1". + + iApply "IH". + { iPureIntro. lia. } + iApply "H1". + + simpl. iSplit; auto. + by rewrite big_sepM_singleton. + Unshelve. + { + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + by apply fresh_loc_offset_is_fresh. + } + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + rewrite dom_singleton. + apply not_elem_of_singleton_2. + intros H2. + apply loc_add_inj in H2. + rewrite replicate_length in H1. + lia. +Qed. + Lemma rswp_load k E l q v a : ⟨⟨⟨ ▷ l ↦{q} v ⟩⟩⟩ ! #l at k @ a; E ⟨⟨⟨ RET v; l ↦{q} v ⟩⟩⟩. Proof. @@ -197,6 +256,19 @@ Section rwp. by iApply (rswp_alloc with "H HΦ"). Qed. + Lemma rwp_allocN_seq (N : nat) (z : Z) E v a: + TCEq N (Z.to_nat z) → + (0 < N)%Z → + ⟨⟨⟨ True ⟩⟩⟩ + AllocN (Val $ LitV $ LitInt $ z) (Val v) @ a; E + ⟨⟨⟨ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v ⟩⟩⟩. + Proof. + intros HN Hz. + iIntros (Φ) "H HΦ". + iApply rwp_no_step. + by iApply (rswp_allocN_seq with "H HΦ"). + Qed. + Lemma rwp_load E l q v a : ⟨⟨⟨ ▷ l ↦{q} v ⟩⟩⟩ ! #l @ a; E ⟨⟨⟨ RET v; l ↦{q} v ⟩⟩⟩. Proof. diff --git a/theories/tpref_logic/proofmode.v b/theories/tpref_logic/proofmode.v index 33ee502f..ff6f467a 100644 --- a/theories/tpref_logic/proofmode.v +++ b/theories/tpref_logic/proofmode.v @@ -1,22 +1,39 @@ From clutch.prob_lang Require Import lang notation class_instances tactics. From clutch.prob_lang Require Export wp_tactics. -From clutch.tpref_logic Require Import weakestpre primitive_laws. +From clutch.tpref_logic Require Import weakestpre primitive_laws derived_laws. From iris.prelude Require Import options. + #[local] Definition rwp' `{!tprG δ Σ} := (rwp' _ _ _ _ _). +(* +#[local] Program Instance rwp' `{!spec δ Σ} `{!tprwpG prob_lang Σ} : Gwp (iProp Σ) (expr) (val ) () . +Next Obligation. + intros δ Σ s lang. + pose proof (rwp') as [wp ?]; [exact lang | exact s |]. + apply wp. +Defined. +Next Obligation. + intros δ Σ s lang. + pose proof (rwp') as [wp u]; [exact lang | exact s |]. + exact u. +Defined. +*) + + #[global] Program Instance rel_logic_wptactics_base `{!tprG δ Σ} : - @WpTacticsBase Σ unit rwp' _ _. -Next Obligation. intros. by apply: rwp_value. Qed. -Next Obligation. intros. by apply: rwp_fupd. Qed. -Next Obligation. intros. by apply: rwp_bind. Qed. + @GwpTacticsBase Σ unit _ _ wp. +Next Obligation. intros. by apply rwp_value. Qed. +Next Obligation. intros. by apply rwp_fupd. Qed. +Next Obligation. intros. by apply rwp_bind. Qed. #[global] Program Instance rel_logic_wptactics_pure `{!tprG δ Σ} : - @WpTacticsPure Σ unit rwp' false. + @GwpTacticsPure Σ unit false wp. Next Obligation. intros. by eapply lifting.rwp_pure_step. Qed. #[global] Program Instance rel_logic_wptactics_heap `{!tprG δ Σ} : - @WpTacticsHeap Σ unit rwp' false := Build_WpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) _ _ _. + @GwpTacticsHeap Σ unit false wp := Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _. Next Obligation. intros. by apply rwp_alloc. Qed. +Next Obligation. intros. by apply rwp_allocN. Qed. Next Obligation. intros. by apply rwp_load. Qed. Next Obligation. intros. by apply rwp_store. Qed. diff --git a/theories/ub_logic/ectx_lifting.v b/theories/ub_logic/ectx_lifting.v index 92f39515..dc4c0fa6 100644 --- a/theories/ub_logic/ectx_lifting.v +++ b/theories/ub_logic/ectx_lifting.v @@ -15,28 +15,28 @@ Implicit Types e : expr Λ. Local Hint Resolve head_prim_reducible head_reducible_prim_step : core. Local Hint Resolve head_stuck_stuck : core. -Lemma wp_lift_head_step_fupd_couple {E Φ} e1 : +Lemma wp_lift_head_step_fupd_couple {E Φ} e1 s : to_val e1 = None → (∀ σ1 ε, state_interp σ1 ∗ err_interp ε ={E,∅}=∗ ⌜head_reducible e1 σ1⌝ ∗ exec_ub e1 σ1 (λ ε2 '(e2, σ2), - ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ E {{ Φ }}) ε ) - ⊢ WP e1 @ E {{ Φ }}. + ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}) ε ) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_step_fupd_exec_ub; [done|]. iIntros (σ1 ε) "Hσε". iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto. Qed. -Lemma wp_lift_head_step {E Φ} e1 : +Lemma wp_lift_head_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜head_reducible e1 σ1⌝ ∗ ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗ - state_interp σ2 ∗ WP e2 @ E {{ Φ }}) - ⊢ WP e1 @ E {{ Φ }}. + state_interp σ2 ∗ WP e2 @ s; E {{ Φ }}) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ". iMod ("H" with "Hσ") as "[% H]"; iModIntro. @@ -45,14 +45,14 @@ Proof. iIntros (???) "!> !>". iApply "H"; auto. Qed. -Lemma wp_lift_atomic_head_step_fupd {E1 E2 Φ} e1 : +Lemma wp_lift_atomic_head_step_fupd {E1 E2 Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E1}=∗ ⌜head_reducible e1 σ1⌝ ∗ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E1}[E2]▷=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E1 {{ Φ }}. + ⊢ WP e1 @ s; E1 {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|]. iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro. @@ -62,14 +62,14 @@ Proof. iApply "H"; eauto. Qed. -Lemma wp_lift_atomic_head_step {E Φ} e1 : +Lemma wp_lift_atomic_head_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝ ∗ ▷ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E {{ Φ }}. + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_atomic_step; eauto. iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro. @@ -79,25 +79,25 @@ Proof. iApply "H"; eauto. Qed. -Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 : +Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 s : to_val e1 = None → (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2' σ2, head_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - (|={E}[E']▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}. + (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}. Proof using Hinh. intros. erewrite !(wp_lift_pure_det_step e1 e2); eauto. intros. by apply head_prim_reducible. Qed. -Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 : +Lemma wp_lift_pure_det_head_step' {E Φ} e1 e2 s : to_val e1 = None → (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2' σ2, head_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}. + ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}. Proof using Hinh. - intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step //. + intros. rewrite -[(WP e1 @ _; _ {{ _ }})%I]wp_lift_pure_det_head_step //. rewrite -step_fupd_intro //. Qed. End wp. diff --git a/theories/ub_logic/lifting.v b/theories/ub_logic/lifting.v index 4b7a52ef..4a38e655 100644 --- a/theories/ub_logic/lifting.v +++ b/theories/ub_logic/lifting.v @@ -16,29 +16,29 @@ Implicit Types Φ : val Λ → iProp Σ. #[local] Open Scope R. -Lemma wp_lift_step_fupd_exec_ub E Φ e1 : +Lemma wp_lift_step_fupd_exec_ub E Φ e1 s : to_val e1 = None → (∀ σ1 ε, state_interp σ1 ∗ err_interp ε ={E,∅}=∗ exec_ub e1 σ1 (λ ε2 '(e2, σ2), - ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ E {{ Φ }}) ε) - ⊢ WP e1 @ E {{ Φ }}. + ▷ |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E {{ Φ }}) ε) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. by rewrite ub_wp_unfold /ub_wp_pre =>->. Qed. -Lemma wp_lift_step_fupd E Φ e1 : +Lemma wp_lift_step_fupd E Φ e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0 ⌝ ={∅}=∗ ▷ |={∅,E}=> - state_interp σ2 ∗ WP e2 @ E {{ Φ }}) - ⊢ WP e1 @ E {{ Φ }}. + state_interp σ2 ∗ WP e2 @ s; E {{ Φ }}) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_step_fupd_exec_ub; [done|]. @@ -64,25 +64,25 @@ Proof. Qed. (** Derived lifting lemmas. *) -Lemma wp_lift_step E Φ e1 : +Lemma wp_lift_step E Φ e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜reducible (e1, σ1)⌝ ∗ ▷ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗ state_interp σ2 ∗ - WP e2 @ E {{ Φ }}) - ⊢ WP e1 @ E {{ Φ }}. + WP e2 @ s; E {{ Φ }}) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>" (???) "!>!>" . by iApply "H". Qed. -Lemma wp_lift_pure_step `{!Inhabited (state Λ)} E E' Φ e1 : +Lemma wp_lift_pure_step `{!Inhabited (state Λ)} E E' Φ e1 s : (∀ σ1, reducible (e1, σ1)) → (∀ σ1 e2 σ2, prim_step e1 σ1 (e2, σ2) > 0 → σ2 = σ1) → - (|={E}[E']▷=> ∀ e2 σ, ⌜prim_step e1 σ (e2, σ) > 0⌝ → WP e2 @ E {{ Φ }}) - ⊢ WP e1 @ E {{ Φ }}. + (|={E}[E']▷=> ∀ e2 σ, ⌜prim_step e1 σ (e2, σ) > 0⌝ → WP e2 @ s; E {{ Φ }}) + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (Hsafe Hstep) "H". iApply wp_lift_step. { by eapply (to_final_None_1 (e1, inhabitant)), reducible_not_final. } @@ -97,14 +97,14 @@ Qed. (* Atomic steps don't need any mask-changing business here, one can *) (* use the generic lemmas here. *) -Lemma wp_lift_atomic_step_fupd {E1 E2 Φ} e1 : +Lemma wp_lift_atomic_step_fupd {E1 E2 Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E1}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E1}[E2]▷=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E1 {{ Φ }}. + ⊢ WP e1 @ s; E1 {{ Φ }}. Proof. iIntros (?) "H". iApply (wp_lift_step_fupd E1 _ e1)=>//; iIntros (σ1) "Hσ1". @@ -118,14 +118,14 @@ Proof. iApply ub_wp_value; last done. by apply of_to_val. Qed. -Lemma wp_lift_atomic_step {E Φ} e1 : +Lemma wp_lift_atomic_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E}=∗ ⌜reducible (e1, σ1)⌝ ∗ ▷ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E {{ Φ }}. + ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|]. iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]". @@ -133,10 +133,10 @@ Proof. by iApply "H". Qed. -Lemma wp_lift_pure_det_step `{!Inhabited (state Λ)} {E E' Φ} e1 e2 : +Lemma wp_lift_pure_det_step `{!Inhabited (state Λ)} {E E' Φ} e1 e2 s : (∀ σ1, reducible (e1, σ1)) → (∀ σ1 e2' σ2, prim_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - (|={E}[E']▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}. + (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E E'); try done. { naive_solver. } @@ -144,10 +144,10 @@ Proof. iIntros (e' σ (?&->)%Hpuredet); auto. Qed. -Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} E E' e1 e2 φ n Φ : +Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} E E' e1 e2 φ n Φ s : PureExec φ n e1 e2 → φ → - (|={E}[E']▷=>^n WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}. + (|={E}[E']▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}. Proof. iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ). iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done. @@ -158,10 +158,10 @@ Proof. - by iApply (step_fupd_wand with "Hwp"). Qed. -Lemma wp_pure_step_later `{!Inhabited (state Λ)} E e1 e2 φ n Φ : +Lemma wp_pure_step_later `{!Inhabited (state Λ)} E e1 e2 φ n Φ s : PureExec φ n e1 e2 → φ → - ▷^n WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}. + ▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}. Proof. intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec. induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH. diff --git a/theories/ub_logic/primitive_laws.v b/theories/ub_logic/primitive_laws.v index fcd170f0..6aaa51e3 100644 --- a/theories/ub_logic/primitive_laws.v +++ b/theories/ub_logic/primitive_laws.v @@ -84,21 +84,81 @@ Qed. *) (** Heap *) -Lemma wp_alloc E v : - {{{ True }}} Alloc (Val v) @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. + +Lemma wp_alloc E v s : + {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}. Proof. iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step; [done|]. iIntros (σ1) "[Hh Ht] !#". solve_red. iIntros "!> /=" (e2 σ2 Hs); inv_head_step. - iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[$ Hl]". + iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]". { apply not_elem_of_dom, fresh_loc_is_fresh. } - iIntros "!>". iFrame. by iApply "HΦ". + iFrame. + rewrite map_union_empty -insert_union_singleton_l. + iFrame. + iIntros "!>". by iApply "HΦ". +Qed. + +Lemma wp_allocN_seq (N : nat) (z : Z) E v s: + TCEq N (Z.to_nat z) → + (0 < N)%Z → + {{{ True }}} + AllocN (Val $ LitV $ LitInt $ z) (Val v) @ s; E + {{{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v }}}. +Proof. + iIntros (-> Hn Φ) "_ HΦ". + iApply wp_lift_atomic_head_step; [done|]. + iIntros (σ1) "[Hh Ht] !#". + iSplit. + { iPureIntro. + rewrite /head_reducible. + eexists. + apply head_step_support_equiv_rel. + econstructor; eauto. + lia. + } + iIntros "!> /=" (e2 σ2 Hs); inv_head_step. + iMod ((ghost_map_insert_big _ _ with "Hh")) as "[$ Hl]". + iIntros "!>". iFrame. + iApply "HΦ". + iInduction (H) as [ | ?] "IH" forall (σ1). + - simpl. + iSplit; auto. + rewrite map_union_empty. + rewrite loc_add_0. + by rewrite big_sepM_singleton. + - rewrite seq_S. + rewrite heap_array_replicate_S_end. + iPoseProof (big_sepM_union _ _ _ _ with "Hl") as "[H1 H2]". + iApply big_sepL_app. + iSplitL "H1". + + iApply "IH". + { iPureIntro. lia. } + iApply "H1". + + simpl. iSplit; auto. + by rewrite big_sepM_singleton. + Unshelve. + { + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + by apply fresh_loc_offset_is_fresh. + } + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + rewrite dom_singleton. + apply not_elem_of_singleton_2. + intros H2. + apply loc_add_inj in H2. + rewrite replicate_length in H1. + lia. Qed. -Lemma wp_load E l dq v : - {{{ ▷ l ↦{dq} v }}} Load (Val $ LitV $ LitLoc l) @ E {{{ RET v; l ↦{dq} v }}}. +Lemma wp_load E l dq v s : + {{{ ▷ l ↦{dq} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l ↦{dq} v }}}. Proof. iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step; [done|]. @@ -109,8 +169,8 @@ Proof. iFrame. iModIntro. by iApply "HΦ". Qed. -Lemma wp_store E l v' v : - {{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ E +Lemma wp_store E l v' v s : + {{{ ▷ l ↦ v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E {{{ RET LitV LitUnit; l ↦ v }}}. Proof. iIntros (Φ) ">Hl HΦ". @@ -123,9 +183,9 @@ Proof. iFrame. iModIntro. by iApply "HΦ". Qed. -Lemma wp_rand (N : nat) (z : Z) E : +Lemma wp_rand (N : nat) (z : Z) E s : TCEq N (Z.to_nat z) → - {{{ True }}} rand #z @ E {{{ (n : fin (S N)), RET #n; True }}}. + {{{ True }}} rand #z @ s; E {{{ (n : fin (S N)), RET #n; True }}}. Proof. iIntros (-> Φ) "_ HΦ". iApply wp_lift_atomic_head_step; [done|]. @@ -139,9 +199,9 @@ Qed. (** Tapes *) -Lemma wp_alloc_tape N z E : +Lemma wp_alloc_tape N z E s : TCEq N (Z.to_nat z) → - {{{ True }}} alloc #z @ E {{{ α, RET #lbl:α; α ↪ (N; []) }}}. + {{{ True }}} alloc #z @ s; E {{{ α, RET #lbl:α; α ↪ (N; []) }}}. Proof. iIntros (-> Φ) "_ HΦ". iApply wp_lift_atomic_head_step; [done|]. @@ -154,9 +214,9 @@ Proof. by iApply "HΦ". Qed. -Lemma wp_rand_tape N α n ns z E : +Lemma wp_rand_tape N α n ns z E s : TCEq N (Z.to_nat z) → - {{{ ▷ α ↪ (N; n :: ns) }}} rand(#lbl:α) #z @ E {{{ RET #(LitInt n); α ↪ (N; ns) }}}. + {{{ ▷ α ↪ (N; n :: ns) }}} rand(#lbl:α) #z @ s; E {{{ RET #(LitInt n); α ↪ (N; ns) }}}. Proof. iIntros (-> Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step; [done|]. @@ -170,9 +230,9 @@ Proof. by iApply "HΦ". Qed. -Lemma wp_rand_tape_empty N z α E : +Lemma wp_rand_tape_empty N z α E s : TCEq N (Z.to_nat z) → - {{{ ▷ α ↪ (N; []) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}. + {{{ ▷ α ↪ (N; []) }}} rand(#lbl:α) #z @ s; E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }}}. Proof. iIntros (-> Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step; [done|]. @@ -185,10 +245,10 @@ Proof. iModIntro. iApply ("HΦ" with "[$Hl //]"). Qed. -Lemma wp_rand_tape_wrong_bound N M z α E ns : +Lemma wp_rand_tape_wrong_bound N M z α E ns s : TCEq N (Z.to_nat z) → N ≠ M → - {{{ ▷ α ↪ (M; ns) }}} rand(#lbl:α) #z @ E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}. + {{{ ▷ α ↪ (M; ns) }}} rand(#lbl:α) #z @ s; E {{{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }}}. Proof. iIntros (-> ? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step; [done|]. diff --git a/theories/ub_logic/proofmode.v b/theories/ub_logic/proofmode.v index 522035d5..e5e112a9 100644 --- a/theories/ub_logic/proofmode.v +++ b/theories/ub_logic/proofmode.v @@ -1,3 +1,75 @@ +From clutch.prob_lang Require Import lang notation class_instances tactics. +From clutch.prob_lang Require Export wp_tactics. +From clutch.ub_logic Require Import ub_weakestpre primitive_laws derived_laws. +From clutch.ub_logic Require Import ub_total_weakestpre total_primitive_laws total_derived_laws. +From iris.prelude Require Import options. + + +(* +#[local] Definition ub_wp' `{!irisGS prob_lang Σ} := (ub_wp'). +*) +(* +#[local] Program Instance ub_wp' `{!irisGS prob_lang Σ} : Gwp (iProp Σ) (expr) (val) () . +Next Obligation. + intros Σ lang. + pose proof ub_wp' as [wp ?]. + apply wp. +Defined. +Next Obligation. + intros Σ lang. + pose proof ub_wp' as [wp u]. + exact u. +Defined. +*) + + + +#[global] Program Instance rel_logic_wptactics_base `{!ub_clutchGS Σ} : @GwpTacticsBase Σ unit _ _ wp. +Next Obligation. intros. by apply ub_wp_value. Qed. +Next Obligation. intros. by apply ub_wp_fupd. Qed. +Next Obligation. intros. by apply ub_wp_bind. Qed. + +#[global] Program Instance rel_logic_wptactics_pure `{!ub_clutchGS Σ} : @GwpTacticsPure Σ unit true wp. +Next Obligation. intros. by eapply lifting.wp_pure_step_later. Qed. + +#[global] Program Instance rel_logic_wptactics_heap `{!ub_clutchGS Σ} : @GwpTacticsHeap Σ unit true wp := + Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _. +Next Obligation. intros. by apply wp_alloc. Qed. +Next Obligation. intros. by apply wp_allocN. Qed. +Next Obligation. intros. by apply wp_load. Qed. +Next Obligation. intros. by apply wp_store. Qed. + + +(* +#[global] Program Instance ub_twp' `{!irisGS prob_lang Σ} : Gwp (iProp Σ) (expr) (val) () . +Next Obligation. + intros Σ lang. + pose proof ub_twp' as [wp ?]. + apply wp. +Defined. +Next Obligation. + intros Σ lang. + pose proof ub_twp' as [wp u]. + exact u. +Defined. +*) + +#[global] Program Instance rel_logic_twptactics_base `{!ub_clutchGS Σ} : @GwpTacticsBase Σ unit _ _ twp. +Next Obligation. intros. by apply ub_twp_value. Qed. +Next Obligation. intros. by apply ub_twp_fupd. Qed. +Next Obligation. intros. by apply ub_twp_bind. Qed. + +#[global] Program Instance rel_logic_twptactics_pure `{!ub_clutchGS Σ} : @GwpTacticsPure Σ unit false twp. +Next Obligation. intros. by eapply total_lifting.twp_pure_step_fupd. Qed. + +#[global] Program Instance rel_logic_twptactics_heap `{!ub_clutchGS Σ} : @GwpTacticsHeap Σ unit false twp := + Build_GwpTacticsHeap _ _ _ _ (λ l q v, (l ↦{q} v)%I) (λ l q vs, (l ↦∗{q} vs)%I) _ _ _ _. +Next Obligation. intros. by apply twp_alloc. Qed. +Next Obligation. intros. by apply twp_allocN. Qed. +Next Obligation. intros. iIntros ">H H2". iApply (twp_load with "[H //] [H2 //]"). Qed. +Next Obligation. intros. iIntros ">H H2". iApply (twp_store with "[H //] [H2 //]"). Qed. + +(* From iris.bi Require Export bi updates. From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.proofmode Require Export tactics. @@ -500,3 +572,4 @@ Tactic Notation "wp_store" := |pm_reduce; first [wp_seq|wp_finish]] | _ => fail "wp_store: not a 'wp'" end. +*) diff --git a/theories/ub_logic/total_ectx_lifting.v b/theories/ub_logic/total_ectx_lifting.v index aeb5fe22..94a1f71f 100644 --- a/theories/ub_logic/total_ectx_lifting.v +++ b/theories/ub_logic/total_ectx_lifting.v @@ -13,28 +13,28 @@ Implicit Types e : expr Λ. Local Hint Resolve head_prim_reducible head_reducible_prim_step : core. Local Hint Resolve head_stuck_stuck : core. -Lemma twp_lift_head_step_exec_ub {E Φ} e1 : +Lemma twp_lift_head_step_exec_ub {E Φ} e1 s : to_val e1 = None → (∀ σ1 ε, state_interp σ1 ∗ err_interp ε ={E,∅}=∗ ⌜head_reducible e1 σ1⌝ ∗ exec_ub e1 σ1 (λ ε2 '(e2, σ2), - |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ E [{ Φ }]) ε ) - ⊢ WP e1 @ E [{ Φ }]. + |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]) ε ) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_step_fupd_exec_ub; [done|]. iIntros (σ1 ε) "Hσε". iMod ("H" with "Hσε") as "[% H]"; iModIntro; auto. Qed. -Lemma twp_lift_head_step {E Φ} e1 : +Lemma twp_lift_head_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜head_reducible e1 σ1⌝ ∗ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗ - state_interp σ2 ∗ WP e2 @ E [{ Φ }]) - ⊢ WP e1 @ E [{ Φ }]. + state_interp σ2 ∗ WP e2 @ s; E [{ Φ }]) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (?) "Hσ". iMod ("H" with "Hσ") as "[% H]"; iModIntro. @@ -43,14 +43,14 @@ Proof. iIntros (???) "!>". iApply "H"; auto. Qed. -Lemma twp_lift_atomic_head_step_fupd {E1 Φ} e1 : +Lemma twp_lift_atomic_head_step_fupd {E1 Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E1}=∗ ⌜head_reducible e1 σ1⌝ ∗ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E1}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E1 [{ Φ }]. + ⊢ WP e1 @ s; E1 [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|]. iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro. @@ -60,14 +60,14 @@ Proof. iApply "H"; eauto. Qed. -Lemma twp_lift_atomic_head_step {E Φ} e1 : +Lemma twp_lift_atomic_head_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E}=∗ ⌜head_reducible e1 σ1⌝ ∗ ∀ e2 σ2, ⌜head_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E [{ Φ }]. + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_atomic_step; eauto. iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro. @@ -77,25 +77,25 @@ Proof. iApply "H"; eauto. Qed. -Lemma twp_lift_pure_det_head_step {E Φ} e1 e2 : +Lemma twp_lift_pure_det_head_step {E Φ} e1 e2 s : to_val e1 = None → (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2' σ2, head_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - (|={E}=> WP e2 @ E [{ Φ }]) ⊢ WP e1 @ E [{ Φ }]. + (|={E}=> WP e2 @ s; E [{ Φ }]) ⊢ WP e1 @ s; E [{ Φ }]. Proof using Hinh. intros. erewrite !(twp_lift_pure_det_step e1 e2); eauto. intros. by apply head_prim_reducible. Qed. -Lemma twp_lift_pure_det_head_step' {E Φ} e1 e2 : +Lemma twp_lift_pure_det_head_step' {E Φ} e1 e2 s : to_val e1 = None → (∀ σ1, head_reducible e1 σ1) → (∀ σ1 e2' σ2, head_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - WP e2 @ E [{ Φ }] ⊢ WP e1 @ E [{ Φ }]. + WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }]. Proof using Hinh. - intros. rewrite -[(WP e1 @ _ [{ _ }])%I] twp_lift_pure_det_head_step //. + intros. rewrite -[(WP e1 @ _; _ [{ _ }])%I] twp_lift_pure_det_head_step //. iIntros. by iModIntro. Qed. diff --git a/theories/ub_logic/total_lifting.v b/theories/ub_logic/total_lifting.v index cc98404f..9d46d534 100644 --- a/theories/ub_logic/total_lifting.v +++ b/theories/ub_logic/total_lifting.v @@ -12,27 +12,27 @@ Section total_lifting. Implicit Types Φ : val Λ → iProp Σ. Local Open Scope R. - Lemma twp_lift_step_fupd_exec_ub E Φ e1 : + Lemma twp_lift_step_fupd_exec_ub E Φ e1 s : to_val e1 = None → (∀ σ1 ε, state_interp σ1 ∗ err_interp ε ={E,∅}=∗ exec_ub e1 σ1 (λ ε2 '(e2, σ2), - |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ E [{ Φ }]) ε) - ⊢ WP e1 @ E [{ Φ }]. + |={∅,E}=> state_interp σ2 ∗ err_interp ε2 ∗ WP e2 @ s; E [{ Φ }]) ε) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. by rewrite ub_twp_unfold /ub_twp_pre =>->. Qed. - Lemma twp_lift_step_fupd E Φ e1 : + Lemma twp_lift_step_fupd E Φ e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0 ⌝ ={∅}=∗ |={∅,E}=> - state_interp σ2 ∗ WP e2 @ E [{ Φ }]) - ⊢ WP e1 @ E [{ Φ }]. + state_interp σ2 ∗ WP e2 @ s; E [{ Φ }]) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. intros Hval. iIntros "H". @@ -58,26 +58,26 @@ Section total_lifting. Qed. (** Derived lifting lemmas. *) - Lemma twp_lift_step E Φ e1 : + Lemma twp_lift_step E Φ e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E,∅}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={∅,E}=∗ state_interp σ2 ∗ - WP e2 @ E [{ Φ }]) - ⊢ WP e1 @ E [{ Φ }]. + WP e2 @ s; E [{ Φ }]) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (?) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>" (???) "!>" . iMod ("H" with "[]"); first done. iModIntro; done. Qed. - Lemma twp_lift_pure_step `{!Inhabited (state Λ)} E Φ e1 : + Lemma twp_lift_pure_step `{!Inhabited (state Λ)} E Φ e1 s : (∀ σ1, reducible (e1, σ1)) → (∀ σ1 e2 σ2, prim_step e1 σ1 (e2, σ2) > 0 → σ2 = σ1) → - (|={E}=> ∀ e2 σ, ⌜prim_step e1 σ (e2, σ) > 0⌝ → WP e2 @ E [{ Φ }]) - ⊢ WP e1 @ E [{ Φ }]. + (|={E}=> ∀ e2 σ, ⌜prim_step e1 σ (e2, σ) > 0⌝ → WP e2 @ s; E [{ Φ }]) + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (Hsafe Hstep) "H". iApply twp_lift_step. { by eapply (to_final_None_1 (e1, inhabitant)), reducible_not_final. } @@ -90,14 +90,14 @@ Section total_lifting. iDestruct ("H" with "[//]") as "H". simpl. by iFrame. Qed. - Lemma twp_lift_atomic_step_fupd {E1 Φ} e1 : + Lemma twp_lift_atomic_step_fupd {E1 Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E1}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E1}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E1 [{ Φ }]. + ⊢ WP e1 @ s; E1 [{ Φ }]. Proof. iIntros (?) "H". iApply (twp_lift_step_fupd E1 _ e1)=>//; iIntros (σ1) "Hσ1". @@ -112,14 +112,14 @@ Section total_lifting. iApply ub_twp_value; last done. by apply of_to_val. Qed. - Lemma twp_lift_atomic_step {E Φ} e1 : + Lemma twp_lift_atomic_step {E Φ} e1 s : to_val e1 = None → (∀ σ1, state_interp σ1 ={E}=∗ ⌜reducible (e1, σ1)⌝ ∗ ∀ e2 σ2, ⌜prim_step e1 σ1 (e2, σ2) > 0⌝ ={E}=∗ state_interp σ2 ∗ from_option Φ False (to_val e2)) - ⊢ WP e1 @ E [{ Φ }]. + ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|]. iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]". @@ -127,10 +127,10 @@ Section total_lifting. by iApply "H". Qed. - Lemma twp_lift_pure_det_step `{!Inhabited (state Λ)} {E Φ} e1 e2 : + Lemma twp_lift_pure_det_step `{!Inhabited (state Λ)} {E Φ} e1 e2 s : (∀ σ1, reducible (e1, σ1)) → (∀ σ1 e2' σ2, prim_step e1 σ1 (e2', σ2) > 0 → σ2 = σ1 ∧ e2' = e2) → - (|={E}=> WP e2 @ E [{ Φ }]) ⊢ WP e1 @ E [{ Φ }]. + (|={E}=> WP e2 @ s; E [{ Φ }]) ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (? Hpuredet) "H". iApply (twp_lift_pure_step E); try done. { naive_solver. } @@ -138,10 +138,10 @@ Section total_lifting. iIntros (e' σ (?&->)%Hpuredet); auto. Qed. - Lemma twp_pure_step_fupd `{!Inhabited (state Λ)} E e1 e2 φ n Φ : + Lemma twp_pure_step_fupd `{!Inhabited (state Λ)} E e1 e2 φ n Φ s : PureExec φ n e1 e2 → φ → - WP e2 @ E [{ Φ }] ⊢ WP e1 @ E [{ Φ }]. + WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }]. Proof. iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ). iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done. diff --git a/theories/ub_logic/total_primitive_laws.v b/theories/ub_logic/total_primitive_laws.v index 081ae492..91699801 100644 --- a/theories/ub_logic/total_primitive_laws.v +++ b/theories/ub_logic/total_primitive_laws.v @@ -13,23 +13,84 @@ Implicit Types l : loc. (** Heap *) -Lemma twp_alloc E v : - [[{ True }]] Alloc (Val v) @ E [[{ l, RET LitV (LitLoc l); l ↦ v }]]. + + +Lemma twp_alloc E v s : + [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]]. Proof. iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "[Hh Ht] !#". solve_red. iIntros "/=" (e2 σ2 Hs); inv_head_step. - iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[$ Hl]". + iMod ((ghost_map_insert (fresh_loc σ1.(heap)) v) with "Hh") as "[? Hl]". { apply not_elem_of_dom, fresh_loc_is_fresh. } - iIntros "!>". iFrame. by iApply "HΦ". + iFrame. + rewrite map_union_empty -insert_union_singleton_l. + iFrame. + iIntros "!>". by iApply "HΦ". +Qed. + +Lemma twp_allocN_seq (N : nat) (z : Z) E v s: + TCEq N (Z.to_nat z) → + (0 < N)%Z → + [[{ True }]] + AllocN (Val $ LitV $ LitInt $ z) (Val v) @ s; E + [[{ l, RET LitV (LitLoc l); [∗ list] i ∈ seq 0 N, (l +ₗ (i : nat)) ↦ v }]]. +Proof. + iIntros (-> Hn Φ) "_ HΦ". + iApply twp_lift_atomic_head_step; [done|]. + iIntros (σ1) "[Hh Ht] !#". + iSplit. + { iPureIntro. + rewrite /head_reducible. + eexists. + apply head_step_support_equiv_rel. + econstructor; eauto. + lia. + } + iIntros "/=" (e2 σ2 Hs); inv_head_step. + iMod ((ghost_map_insert_big _ _ with "Hh")) as "[$ Hl]". + iIntros "!>". iFrame. + iApply "HΦ". + iInduction (H) as [ | ?] "IH" forall (σ1). + - simpl. + iSplit; auto. + rewrite map_union_empty. + rewrite loc_add_0. + by rewrite big_sepM_singleton. + - rewrite seq_S. + rewrite heap_array_replicate_S_end. + iPoseProof (big_sepM_union _ _ _ _ with "Hl") as "[H1 H2]". + iApply big_sepL_app. + iSplitL "H1". + + iApply "IH". + { iPureIntro. lia. } + iApply "H1". + + simpl. iSplit; auto. + by rewrite big_sepM_singleton. + Unshelve. + { + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + by apply fresh_loc_offset_is_fresh. + } + apply heap_array_map_disjoint. + intros. + apply not_elem_of_dom_1. + rewrite dom_singleton. + apply not_elem_of_singleton_2. + intros H2. + apply loc_add_inj in H2. + rewrite replicate_length in H1. + lia. Qed. -Lemma twp_load E l dq v : - [[{ ▷ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ E [[{ RET v; l ↦{dq} v }]]. +Lemma twp_load E l dq v s : + [[{ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l ↦{dq} v }]]. Proof. - iIntros (Φ) ">Hl HΦ". + iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "[Hh Ht] !#". iDestruct (ghost_map_lookup with "Hh Hl") as %?. @@ -38,11 +99,11 @@ Proof. iFrame. iModIntro. by iApply "HΦ". Qed. -Lemma twp_store E l v' v : - [[{ ▷ l ↦ v' }]] Store (Val $ LitV (LitLoc l)) (Val v) @ E +Lemma twp_store E l v' v s : + [[{ l ↦ v' }]] Store (Val $ LitV (LitLoc l)) (Val v) @ s; E [[{ RET LitV LitUnit; l ↦ v }]]. Proof. - iIntros (Φ) ">Hl HΦ". + iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "[Hh Ht] !#". iDestruct (ghost_map_lookup with "Hh Hl") as %?. @@ -52,9 +113,9 @@ Proof. iFrame. iModIntro. by iApply "HΦ". Qed. -Lemma twp_rand (N : nat) (z : Z) E : +Lemma twp_rand (N : nat) (z : Z) E s : TCEq N (Z.to_nat z) → - [[{ True }]] rand #z @ E [[{ (n : fin (S N)), RET #n; True }]]. + [[{ True }]] rand #z @ s; E [[{ (n : fin (S N)), RET #n; True }]]. Proof. iIntros (-> Φ) "_ HΦ". iApply twp_lift_atomic_head_step; [done|]. @@ -68,9 +129,9 @@ Qed. (** Tapes *) -Lemma twp_alloc_tape N z E : +Lemma twp_alloc_tape N z E s : TCEq N (Z.to_nat z) → - [[{ True }]] alloc #z @ E [[{ α, RET #lbl:α; α ↪ (N; []) }]]. + [[{ True }]] alloc #z @ s; E [[{ α, RET #lbl:α; α ↪ (N; []) }]]. Proof. iIntros (-> Φ) "_ HΦ". iApply twp_lift_atomic_head_step; [done|]. @@ -83,11 +144,11 @@ Proof. by iApply "HΦ". Qed. -Lemma twp_rand_tape N α n ns z E : +Lemma twp_rand_tape N α n ns z E s : TCEq N (Z.to_nat z) → - [[{ ▷ α ↪ (N; n :: ns) }]] rand(#lbl:α) #z @ E [[{ RET #(LitInt n); α ↪ (N; ns) }]]. + [[{ α ↪ (N; n :: ns) }]] rand(#lbl:α) #z @ s; E [[{ RET #(LitInt n); α ↪ (N; ns) }]]. Proof. - iIntros (-> Φ) ">Hl HΦ". + iIntros (-> Φ) "Hl HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "(Hh & Ht) !#". iDestruct (ghost_map_lookup with "Ht Hl") as %?. @@ -99,11 +160,11 @@ Proof. by iApply "HΦ". Qed. -Lemma twp_rand_tape_empty N z α E : +Lemma twp_rand_tape_empty N z α E s : TCEq N (Z.to_nat z) → - [[{ ▷ α ↪ (N; []) }]] rand(#lbl:α) #z @ E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }]]. + [[{ α ↪ (N; []) }]] rand(#lbl:α) #z @ s; E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }]]. Proof. - iIntros (-> Φ) ">Hl HΦ". + iIntros (-> Φ) "Hl HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "(Hh & Ht) !#". iDestruct (ghost_map_lookup with "Ht Hl") as %?. @@ -114,12 +175,12 @@ Proof. iModIntro. iApply ("HΦ" with "[$Hl //]"). Qed. -Lemma twp_rand_tape_wrong_bound N M z α E ns : +Lemma twp_rand_tape_wrong_bound N M z α E ns s : TCEq N (Z.to_nat z) → N ≠ M → - [[{ ▷ α ↪ (M; ns) }]] rand(#lbl:α) #z @ E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }]]. + [[{ α ↪ (M; ns) }]] rand(#lbl:α) #z @ s; E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }]]. Proof. - iIntros (-> ? Φ) ">Hl HΦ". + iIntros (-> ? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step; [done|]. iIntros (σ1) "(Hh & Ht) !#". iDestruct (ghost_map_lookup with "Ht Hl") as %?. diff --git a/theories/ub_logic/ub_rules.v b/theories/ub_logic/ub_rules.v index 0c52a4ee..c2443dfc 100644 --- a/theories/ub_logic/ub_rules.v +++ b/theories/ub_logic/ub_rules.v @@ -157,11 +157,11 @@ Section rules. Implicit Types v : val. Implicit Types l : loc. -Lemma twp_rand_err (N : nat) (z : Z) (m : fin (S N)) E Φ : +Lemma twp_rand_err (N : nat) (z : Z) (m : fin (S N)) E Φ s : TCEq N (Z.to_nat z) → € (nnreal_inv(nnreal_nat(N+1))) ∗ (∀ x, ⌜x ≠ m⌝ -∗ Φ #x) - ⊢ WP rand #z @ E [{ Φ }]. + ⊢ WP rand #z @ s; E [{ Φ }]. Proof. iIntros (->) "[Herr Hwp]". iApply twp_lift_step_fupd_exec_ub; [done|]. @@ -224,11 +224,11 @@ Proof. Qed. -Lemma twp_rand_err_nat (N : nat) (z : Z) (m : nat) E Φ : +Lemma twp_rand_err_nat (N : nat) (z : Z) (m : nat) E Φ s : TCEq N (Z.to_nat z) → € (nnreal_inv(nnreal_nat(N+1))) ∗ (∀ x : fin (S N), ⌜(fin_to_nat x) ≠ m⌝ -∗ Φ #x) - ⊢ WP rand #z @ E [{ Φ }]. + ⊢ WP rand #z @ s; E [{ Φ }]. Proof. iIntros (->) "[Herr Hwp]". iApply twp_lift_step_fupd_exec_ub; [done|]. @@ -664,8 +664,9 @@ Proof. iMod "Hclose'". iFrame. iMod (ec_increase_supply _ (ε2 (nat_to_fin l)) with "Hε2") as "[Hε2 Hfoo]". - iFrame. iModIntro. wp_pures. - iModIntro. iApply "HΨ". + iFrame. iModIntro. + wp_pures. + iApply "HΨ". assert (nat_to_fin l = n) as ->; [|done]. apply fin_to_nat_inj. rewrite fin_to_nat_to_fin. @@ -673,6 +674,7 @@ Proof. reflexivity. Qed. + Lemma wp_couple_rand_adv_comp (N : nat) z E (ε1 : nonnegreal) (ε2 : fin (S N) -> nonnegreal) : TCEq N (Z.to_nat z) → (exists r, ∀ n, (ε2 n <= r)%R) → diff --git a/theories/ub_logic/ub_weakestpre.v b/theories/ub_logic/ub_weakestpre.v index 4e09460d..dcaf45ac 100644 --- a/theories/ub_logic/ub_weakestpre.v +++ b/theories/ub_logic/ub_weakestpre.v @@ -1,9 +1,10 @@ From Coq Require Export Reals Psatz. From iris.proofmode Require Import base proofmode. From iris.base_logic.lib Require Export fancy_updates. -From iris.bi Require Export weakestpre fixpoint big_op. +From iris.bi Require Export fixpoint big_op. From iris.prelude Require Import options. +From clutch.bi Require Export weakestpre. From clutch.prelude Require Import stdpp_ext NNRbar. From clutch.prob Require Export couplings distribution union_bounds. From clutch.common Require Export language.