Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Twp #16

Merged
merged 22 commits into from
Jan 26, 2024
Merged

Twp #16

Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 41 additions & 1 deletion theories/prob/countable_sum.v
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
From Coq Require Import Reals Psatz.
From Coquelicot Require Import Series Hierarchy Lim_seq Rbar Lub.
From stdpp Require Import option.
From stdpp Require Export countable finite.
From stdpp Require Export countable finite gmap.
From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical.
Set Default Proof Using "Type*".
Import Hierarchy.
@@ -472,6 +472,46 @@ Section filter.
+ intro a'; rewrite (bool_decide_ext (a = a') (a' = a)); done.
Qed.

Lemma ex_seriesC_list (l : list A) (f : A -> R):
ex_seriesC (λ (a : A), if bool_decide(a ∈ l) then f a else 0).
Proof.
induction l.
{ eapply ex_seriesC_ext; last apply ex_seriesC_0.
intros; done.
}
destruct (decide(a ∈ l)).
{ eapply ex_seriesC_ext; last done.
intros.
simpl.
erewrite bool_decide_ext; first done.
set_solver.
}
eapply ex_seriesC_ext; last apply ex_seriesC_plus.
2:{ apply IHl. }
2:{ eapply (ex_seriesC_singleton _ (f a)). }
intros x.
simpl.
repeat case_bool_decide; try set_solver.
all: try (by subst).
all: try lra.
- subst. apply Rplus_0_l.
- subst. set_solver.
Qed.

Lemma ex_seriesC_finite_from_option (l : list A) (f : B -> R) (g : A -> option B):
(∀ a : A, is_Some (g a) <-> a ∈ l) ->
ex_seriesC (λ (a : A), from_option f 0%R (g a)).
Proof.
intros Hl.
eapply ex_seriesC_ext; last apply (ex_seriesC_list l).
intros a.
simpl.
case_bool_decide as H1; first done.
destruct (g a) eqn:K.
{ exfalso. apply H1. apply Hl. done. }
done.
Qed.

Lemma is_seriesC_filter_pos f v P `{∀ x, Decision (P x)} :
(∀ n, 0 <= f n) →
is_seriesC f v →
16 changes: 16 additions & 0 deletions theories/prob/union_bounds.v
Original file line number Diff line number Diff line change
@@ -600,6 +600,22 @@ Section total_ub_theory.
- by apply Htotal.
Qed.

Lemma total_ub_lift_implies_ub_lift_strong (μ : distr A) f ε:
total_ub_lift μ f ε -> ub_lift μ f (ε - (1 - SeriesC μ)).
Proof.
rewrite /total_ub_lift /ub_lift /prob.
intros Htotal P HP.
rewrite (SeriesC_ext _ (λ a, if P a then 0 else μ a)); last first.
{ intros. by destruct (P n). }
eapply Rplus_le_reg_l.
rewrite <-SeriesC_split_pred; last first.
{ apply pmf_ex_seriesC. }
{ intros. apply pmf_pos. }
apply Rle_minus_l.
trans (1-ε).
- pose proof (pmf_SeriesC μ). lra.
- by apply Htotal.
Qed.


Lemma total_UB_mon_grading (μ : distr A) (f : A -> Prop) ε ε' :
8 changes: 4 additions & 4 deletions theories/ub_logic/lifting.v
Original file line number Diff line number Diff line change
@@ -147,10 +147,10 @@ Qed.
Lemma wp_lift_atomic_step {E Φ} e1 :
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))
⌜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 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
129 changes: 128 additions & 1 deletion theories/ub_logic/proofmode.v
Original file line number Diff line number Diff line change
@@ -6,20 +6,31 @@ From iris.program_logic Require Import atomic.
From clutch.common Require Import language ectx_language.
From clutch.prob_lang Require Import lang notation class_instances tactics.
From clutch.ub_logic Require Import ub_weakestpre primitive_laws.
From clutch.ub_logic Require Import total_lifting total_ectx_lifting.
From clutch.ub_logic Require Import ub_total_weakestpre total_primitive_laws.
From iris.prelude Require Import options.
Import uPred.

Lemma tac_wp_expr_eval `{!irisGS hlc Σ} Δ s E Φ e e' :
(∀ (e'':=e'), e = e'') →
envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
Lemma tac_twp_expr_eval `{!irisGS hlc Σ} Δ s E Φ e e' :
(∀ (e'':=e'), e = e'') →
envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.


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 _ _ _);
[let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
notypeclasses refine (tac_twp_expr_eval _ _ _ _ e _ _ _);
[let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]

| _ => fail "wp_expr_eval: not a 'wp'"
end.
Ltac wp_expr_simpl := wp_expr_eval simpl.
@@ -37,14 +48,35 @@ Proof.
rewrite HΔ' -lifting.wp_pure_step_later //.
(* iIntros "Hwp !> _" => //. *)
Qed.
Lemma tac_twp_pure `{!ub_clutchGS Σ} Δ E K e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
envs_entails Δ (WP (fill K e2) @ E [{ Φ }]) →
envs_entails Δ (WP (fill K e1) @ E [{ Φ }]).
Proof.
rewrite envs_entails_unseal=> ?? ->.
(* We want [pure_exec_fill] to be available to TC search locally. *)
pose proof @pure_exec_fill.
rewrite -total_lifting.twp_pure_step_fupd //.
Qed.



Lemma tac_wp_value_nofupd `{!ub_clutchGS Σ} Δ E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> ->. by apply ub_wp_value. Qed.
Lemma tac_twp_value_nofupd `{!ub_clutchGS Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> ->. by apply ub_twp_value. Qed.


Lemma tac_wp_value `{!ub_clutchGS Σ} Δ E (Φ : val → iPropI Σ) v :
envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> ->. by rewrite ub_wp_value_fupd. Qed.
Lemma tac_twp_value `{!ub_clutchGS Σ} Δ s E (Φ : val → iPropI Σ) v :
envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> ->. by rewrite ub_twp_value_fupd. Qed.


(** Simplify the goal if it is [WP] of a value.
If the postcondition already allows a fupd, do not add a second one.
@@ -57,7 +89,13 @@ Ltac wp_value_head :=
| |- envs_entails _ (wp ?s ?E (Val _) (λ _, wp _ ?E _ _)) =>
eapply tac_wp_value_nofupd
| |- envs_entails _ (wp ?s ?E (Val _) _) =>
eapply tac_wp_value
eapply tac_wp_value
| |- envs_entails _ (twp ?s ?E (Val _) (λ _, fupd ?E _ _)) =>
eapply tac_twp_value_nofupd
| |- envs_entails _ (twp ?s ?E (Val _) (λ _, twp _ ?E _ _)) =>
eapply tac_twp_value_nofupd
| |- envs_entails _ (twp ?s ?E (Val _) _) =>
eapply tac_twp_value
end.

Ltac wp_finish :=
@@ -179,19 +217,35 @@ Lemma tac_wp_bind `{!ub_clutchGS Σ} K Δ E Φ e f :
envs_entails Δ (WP e @ E {{ v, WP f (Val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite envs_entails_unseal=> -> ->. by apply: ub_wp_bind. Qed.
Lemma tac_twp_bind `{!ub_clutchGS Σ} K Δ s E Φ e f :
f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
Proof. rewrite envs_entails_unseal=> -> ->. by apply: ub_twp_bind. Qed.


Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => 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.

@@ -226,6 +280,26 @@ Proof.
rewrite wand_elim_r.
done.
Qed.
Lemma tac_twp_alloc Δ E j K v Φ :
(∀ l,
match envs_app false (Esnoc Enil j (l ↦ v)) Δ with
| Some Δ' =>
envs_entails Δ' (WP fill K (Val $ LitV $ l) @ E [{ Φ }])
| None => False
end) →
envs_entails Δ (WP fill K (Alloc (Val v)) @ E [{ Φ }]).
Proof.
rewrite envs_entails_unseal=> HΔ.
rewrite -ub_twp_bind. eapply wand_apply; first apply wand_entails.
{ iIntros "P Q". iApply (twp_alloc with "[P][Q]"); done. }
rewrite left_id. apply forall_intro=> l.
specialize (HΔ l).
destruct (envs_app _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
rewrite envs_app_sound //; simpl.
apply wand_intro_l.
iIntros "[?T]". iApply HΔ. iApply "T". iFrame.
Qed.


Lemma tac_wp_load Δ Δ' E i K b l q v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
@@ -241,6 +315,19 @@ Proof.
* iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
* by apply sep_mono_r, wand_mono.
Qed.
Lemma tac_twp_load Δ E i K b l q v Φ :
envs_lookup i Δ = Some (b, l ↦{q} v)%I →
envs_entails Δ (WP fill K (Val v) @ E [{ Φ }]) →
envs_entails Δ (WP fill K (Load (LitV l)) @ E [{ Φ }]).
Proof.
rewrite envs_entails_unseal=> ? Hi.
rewrite -ub_twp_bind. eapply wand_apply; first exact: 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_wp_store Δ Δ' E i K l v v' Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
@@ -257,6 +344,23 @@ Proof.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_twp_store Δ E i K l v v' Φ :
envs_lookup i Δ = Some (false, l ↦ v)%I →
match envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ with
| Some Δ' => envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ E [{ Φ }])
| None => False
end
envs_entails Δ (WP fill K (Store (LitV l) v') @ E [{ Φ }]).
Proof.
rewrite envs_entails_unseal. intros.
destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
rewrite -ub_twp_bind. eapply wand_apply; first by eapply twp_store.
rewrite envs_simple_replace_sound //; simpl.
rewrite right_id.
iIntros "[H?]". iSplitL "H"; first done.
by iApply wand_mono.
Qed.

End heap.

(** The tactic [wp_apply_core lem tac_suc tac_fail] evaluates [lem] to a
@@ -277,6 +381,10 @@ Ltac wp_apply_core lem tac_suc tac_fail := first
| |- 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' =>
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)
@@ -336,6 +444,13 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
[iSolveTC
|finish ()]
in (process_single ())
| |- 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 process_single ()
| _ => fail "wp_alloc: not a 'wp'"
end.

@@ -355,6 +470,12 @@ Tactic Notation "wp_load" :=
[iSolveTC
|solve_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_mapsto ()
|wp_finish]
| _ => fail "wp_load: not a 'wp'"
end.

@@ -371,5 +492,11 @@ Tactic Notation "wp_store" :=
[iSolveTC
|solve_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_mapsto ()
|pm_reduce; first [wp_seq|wp_finish]]
| _ => fail "wp_store: not a 'wp'"
end.
99 changes: 99 additions & 0 deletions theories/ub_logic/total_ectx_lifting.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
From iris.proofmode Require Import proofmode.
From clutch.common Require Import ectx_language.
From clutch.ub_logic Require Import ub_total_weakestpre total_lifting.

Local Open Scope R.

Section twp.
Context {Λ : ectxLanguage} `{!irisGS Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
Local Hint Resolve reducible_not_val_inhabitant : core.
Local Hint Resolve head_stuck_stuck : core.

Lemma twp_lift_head_step_exec_ub {E Φ} e1 :
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 [{ Φ }].
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 :
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 [{ Φ }].
Proof.
iIntros (?) "H". iApply twp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
iMod ("H" with "Hσ") as "[% H]"; iModIntro.
iSplit; [by eauto|].
iIntros (???) "!>". iApply "H"; auto.
Qed.

Lemma twp_lift_atomic_head_step_fupd {E1 Φ} e1 :
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 [{ Φ }].
Proof.
iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|].
iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by auto. iIntros (e2 σ2 Hstep).
iApply "H"; eauto.
Qed.

Lemma twp_lift_atomic_head_step {E Φ} e1 :
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 [{ Φ }].
Proof.
iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; [by auto|]. iIntros (e2 σ2 Hstep).
iApply "H"; eauto.
Qed.

Lemma twp_lift_pure_det_head_step {E Φ} e1 e2 :
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 [{ Φ }].
Proof using Hinh.
intros. erewrite !(twp_lift_pure_det_step e1 e2); eauto.
Qed.

Lemma twp_lift_pure_det_head_step' {E Φ} e1 e2 :
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 [{ Φ }].
Proof using Hinh.
intros. rewrite -[(WP e1 @ _ [{ _ }])%I] twp_lift_pure_det_head_step //.
iIntros. by iModIntro.
Qed.


End twp.
154 changes: 154 additions & 0 deletions theories/ub_logic/total_lifting.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,154 @@
(** Total lifting lemmas for the ub logic*)
From clutch.ub_logic Require Import ub_total_weakestpre.
From iris.proofmode Require Import tactics.
From clutch.prelude Require Import NNRbar.

Section total_lifting.
Context `{!irisGS Λ Σ}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
Local Open Scope R.

Lemma twp_lift_step_fupd_exec_ub E Φ e1 :
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 [{ Φ }].
Proof.
by rewrite ub_twp_unfold /ub_twp_pre =>->.
Qed.

Lemma twp_lift_step_fupd E Φ e1 :
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 [{ Φ }].
Proof.
intros Hval.
iIntros "H".
iApply twp_lift_step_fupd_exec_ub; [done|].
iIntros (σ1 ε) "[Hσ Hε]".
iMod ("H" with "Hσ") as "[%Hs H]". iModIntro.
iApply (exec_ub_prim_step e1 σ1).
iExists _.
iExists nnreal_zero.
iExists ε.
iSplit.
{ iPureIntro. simpl. done. }
iSplit.
{ iPureIntro. simpl. lra. }
iSplit.
{ iPureIntro.
eapply ub_lift_pos_R, ub_lift_trivial.
simpl; lra.
}
iIntros ([e2 σ2] (?&?)).
iMod ("H" with "[//]")as "H".
iModIntro. iMod "H". iModIntro. iFrame. done.
Qed.

(** Derived lifting lemmas. *)
Lemma twp_lift_step E Φ e1 :
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 [{ Φ }].
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 :
(∀ σ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 [{ Φ }].
Proof.
iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
{ specialize (Hsafe inhabitant). eauto using reducible_not_val. }
iIntros (σ1) "Hσ". iMod "H".
iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
iSplit; [done|].
iIntros (e2 σ2 Hprim).
destruct (Hstep _ _ _ Hprim).
iMod "Hclose" as "_". iModIntro.
iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
Qed.

Lemma twp_lift_atomic_step_fupd {E1 Φ} e1 :
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 [{ Φ }].
Proof.
iIntros (?) "H".
iApply (twp_lift_step_fupd E1 _ e1)=>//; iIntros (σ1) "Hσ1".
iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
iApply fupd_mask_intro; first set_solver.
iIntros "Hclose" (e2 σ2 Hs). iMod "Hclose" as "_".
iMod ("H" $! e2 σ2 with "[#]") as "[Hs ?]"; [done|].
iApply fupd_mask_intro; first set_solver. iIntros "Hclose".
iMod "Hclose" as "_". iModIntro.
destruct (to_val e2) eqn:?; last (simpl; by iExFalso).
iFrame.
iApply ub_twp_value; last done. by apply of_to_val.
Qed.

Lemma twp_lift_atomic_step {E Φ} e1 :
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 [{ Φ }].
Proof.
iIntros (?) "H". iApply twp_lift_atomic_step_fupd; [done|].
iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]".
iIntros "!> *". iIntros (Hstep).
by iApply "H".
Qed.

Lemma twp_lift_pure_det_step `{!Inhabited (state Λ)} {E Φ} e1 e2 :
(∀ σ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 [{ Φ }].
Proof.
iIntros (? Hpuredet) "H". iApply (twp_lift_pure_step E); try done.
{ naive_solver. }
iMod "H". iModIntro.
iIntros (e' σ (?&->)%Hpuredet); auto.
Qed.

Lemma twp_pure_step_fupd `{!Inhabited (state Λ)} E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
WP e2 @ E [{ Φ }] ⊢ WP e1 @ E [{ Φ }].
Proof.
iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
iApply twp_lift_pure_det_step.
- intros σ1 e2' σ2 Hpstep.
by injection (pmf_1_supp_eq _ _ _ (pure_step_det σ1) Hpstep).
- iModIntro. iApply "IH". iApply "Hwp".
Qed.

End total_lifting.
134 changes: 134 additions & 0 deletions theories/ub_logic/total_primitive_laws.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,134 @@
From iris.proofmode Require Import proofmode.
From clutch.ub_logic Require Export error_credits ub_total_weakestpre total_ectx_lifting primitive_laws.
From clutch.prob_lang Require Import tactics lang notation.
From clutch.prob_lang Require Export class_instances.

Section total_primitive_laws.
Context `{!ub_clutchGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val → iProp Σ.
Implicit Types σ : state.
Implicit Types v : val.
Implicit Types l : loc.


(** Heap *)
Lemma twp_alloc E v :
[[{ True }]] Alloc (Val v) @ 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]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
iIntros "!>". iFrame. by iApply "HΦ".
Qed.

Lemma twp_load E l dq v :
[[{ ▷ l ↦{dq} v }]] Load (Val $ LitV $ LitLoc l) @ E [[{ RET v; l ↦{dq} v }]].
Proof.
iIntros (Φ) ">Hl HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "[Hh Ht] !#".
iDestruct (ghost_map_lookup with "Hh Hl") as %?.
solve_red.
iIntros "/=" (e2 σ2 Hs); inv_head_step.
iFrame. iModIntro. by iApply "HΦ".
Qed.

Lemma twp_store E l v' v :
[[{ ▷ l ↦ v' }]] Store (Val $ LitV (LitLoc l)) (Val v) @ E
[[{ RET LitV LitUnit; l ↦ v }]].
Proof.
iIntros (Φ) ">Hl HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "[Hh Ht] !#".
iDestruct (ghost_map_lookup with "Hh Hl") as %?.
solve_red.
iIntros "/=" (e2 σ2 Hs); inv_head_step.
iMod (ghost_map_update with "Hh Hl") as "[$ Hl]".
iFrame. iModIntro. by iApply "HΦ".
Qed.

Lemma twp_rand (N : nat) (z : Z) E :
TCEq N (Z.to_nat z) →
[[{ True }]] rand #z @ E [[{ (n : fin (S N)), RET #n; True }]].
Proof.
iIntros (-> Φ) "_ HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "Hσ !#".
solve_red.
iIntros (e2 σ2 Hs).
inv_head_step.
iFrame.
by iApply ("HΦ" $! x) .
Qed.


(** Tapes *)
Lemma twp_alloc_tape N z E :
TCEq N (Z.to_nat z) →
[[{ True }]] alloc #z @ E [[{ α, RET #lbl:α; α ↪ (N; []) }]].
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.(tapes)) with "Ht") as "[$ Hl]".
{ apply not_elem_of_dom, fresh_loc_is_fresh. }
iFrame. iModIntro.
by iApply "HΦ".
Qed.

Lemma twp_rand_tape N α n ns z E :
TCEq N (Z.to_nat z) →
[[{ ▷ α ↪ (N; n :: ns) }]] rand(#lbl:α) #z @ E [[{ RET #(LitInt n); α ↪ (N; ns) }]].
Proof.
iIntros (-> Φ) ">Hl HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "(Hh & Ht) !#".
iDestruct (ghost_map_lookup with "Ht Hl") as %?.
solve_red.
iIntros (e2 σ2 Hs).
inv_head_step.
iMod (ghost_map_update with "Ht Hl") as "[$ Hl]".
iFrame. iModIntro.
by iApply "HΦ".
Qed.

Lemma twp_rand_tape_empty N z α E :
TCEq N (Z.to_nat z) →
[[{ ▷ α ↪ (N; []) }]] rand(#lbl:α) #z @ E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (N; []) }]].
Proof.
iIntros (-> Φ) ">Hl HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "(Hh & Ht) !#".
iDestruct (ghost_map_lookup with "Ht Hl") as %?.
solve_red.
iIntros (e2 σ2 Hs).
inv_head_step.
iFrame.
iModIntro. iApply ("HΦ" with "[$Hl //]").
Qed.

Lemma twp_rand_tape_wrong_bound N M z α E ns :
TCEq N (Z.to_nat z) →
N ≠ M →
[[{ ▷ α ↪ (M; ns) }]] rand(#lbl:α) #z @ E [[{ (n : fin (S N)), RET #(LitInt n); α ↪ (M; ns) }]].
Proof.
iIntros (-> ? Φ) ">Hl HΦ".
iApply twp_lift_atomic_head_step; [done|].
iIntros (σ1) "(Hh & Ht) !#".
iDestruct (ghost_map_lookup with "Ht Hl") as %?.
solve_red.
iIntros (e2 σ2 Hs).
inv_head_step.
iFrame.
iModIntro.
iApply ("HΦ" with "[$Hl //]").
Qed.

End total_primitive_laws.
540 changes: 502 additions & 38 deletions theories/ub_logic/ub_rules.v

Large diffs are not rendered by default.

26 changes: 26 additions & 0 deletions theories/ub_logic/ub_total_weakestpre.v
Original file line number Diff line number Diff line change
@@ -254,6 +254,32 @@ Section ub_twp.
iModIntro. iFrame. iApply "IH". done.
Qed.

Lemma ub_twp_ub_wp' E e Φ : WP e @ E [{ Φ }] -∗ WP e @ E {{ Φ }}.
Proof.
iIntros "H".
iApply ub_twp_ub_wp.
by destruct wp_default, twp_default.
Qed.

Lemma ub_twp_ub_wp_step s E e P Φ :
TCEq (to_val e) None →
▷ P -∗
WP e @ s; E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ s; E {{ Φ }}.
Proof.
iIntros (?) "HP Hwp".
iApply (ub_wp_step_fupd _ _ E _ P with "[HP]"); [auto..|]. by iApply ub_twp_ub_wp.
Qed.

Lemma ub_twp_ub_wp_step' E e P Φ :
TCEq (to_val e) None →
▷ P -∗
WP e @ E [{ v, P ={E}=∗ Φ v }] -∗ WP e @ E {{ Φ }}.
Proof.
iIntros (?) "HP Hwp".
iApply (ub_wp_step_fupd _ _ E _ P with "[HP]"); [auto..|]. by iApply ub_twp_ub_wp'.
Qed.


(** * Derived rules *)
Lemma ub_twp_mono s E e Φ Ψ :
(∀ v, Φ v ⊢ Ψ v) → WP e @ s; E [{ Φ }] ⊢ WP e @ s; E [{ Ψ }].

Unchanged files with check annotations Beta

Context `{!ub_clutchGS Σ}.
Variable val_size : nat.

Check warning on line 8 in theories/ub_logic/hash.v

GitHub Actions / build (8.16.1, 4.14.1-flambda)

Interpreting this declaration as if a global declaration prefixed by
(* A hash function's internal state is a map from previously queried keys to their hash value *)
Definition init_hash_state : val := init_map.
unused error credits
*)
Variable init_val_size : nat.

Check warning on line 22 in theories/ub_logic/cf_hash.v

GitHub Actions / build (8.16.1, 4.14.1-flambda)

Interpreting this declaration as if a global declaration prefixed by
Variable init_r : nat.

Check warning on line 23 in theories/ub_logic/cf_hash.v

GitHub Actions / build (8.16.1, 4.14.1-flambda)

Interpreting this declaration as if a global declaration prefixed by
Definition compute_cf_hash : val :=
λ: "hm" "vs" "s" "r" "v",