D.Dot.examples.sem.positive_div
From iris.proofmode Require Import proofmode.
From D.pure_program_logic Require Import lifting adequacy.
From iris.program_logic Require Import ectxi_language.
From D Require Import swap_later_impl.
From D.Dot Require Import ex_iris_utils sem_unstamped_typing.
Import dlang_adequacy.
Implicit Types (v w : vl) (d : dm) (ds : dms).
From D.pure_program_logic Require Import lifting adequacy.
From iris.program_logic Require Import ectxi_language.
From D Require Import swap_later_impl.
From D.Dot Require Import ex_iris_utils sem_unstamped_typing.
Import dlang_adequacy.
Implicit Types (v w : vl) (d : dm) (ds : dms).
Section examplesBodies.
Context `{HdlangG : !dlangG Ξ£}.
Import hoasNotation.
Definition hdivV := Ξ»: m n, m `div` (htskip n).
Definition hmkPosBodyV (n : hvl) := htif (n > 0) n hloopTm.
Definition hmkPosV := Ξ»: n, hmkPosBodyV n.
Definition hposModV : hvl := Ξ½: _ , {@
type "Pos" = π;
val "mkPos" = hmkPosV;
val "div" = hdivV
}.
Definition hposModTTail self : hty := {@
val "mkPos" : π β: self @; "Pos";
val "div" : π β: self @; "Pos" β: π
}.
Definition oposModTTail : clty Ξ£ :=
cAnd
(cVMem "mkPos" (oAll oInt (oSel x1 "Pos")))
(cAnd
(cVMem "div" (oAll oInt (oAll (oSel x1 "Pos") oInt)))
cTop).
Lemma hposModTTail_eq : C⦠hposModTTail hx0 ⧠①oposModTTail.
Proof. rw. done. Qed.
Definition hposModTBody self : hty := {@
type "Pos" >: β₯ <: π;
val "mkPos" : π β: self @; "Pos";
val "div" : π β: self @; "Pos" β: π
}.
Example hposModTBody_alt x :
hposModTBody x = hTAnd (type "Pos" >: β₯ <: π) (hposModTTail x) :=
reflexivity _.
Definition oposModTBody : clty Ξ£ :=
cAnd (cTMemL "Pos" oBot oInt)
oposModTTail.
Lemma hposModTBody_eq : C⦠hposModTBody hx0 ⧠①oposModTBody.
Proof.
rewrite hposModTBody_alt cinterp_TAnd hposModTTail_eq.
rw. done.
Qed.
Context `{HdlangG : !dlangG Ξ£}.
Import hoasNotation.
Definition hdivV := Ξ»: m n, m `div` (htskip n).
Definition hmkPosBodyV (n : hvl) := htif (n > 0) n hloopTm.
Definition hmkPosV := Ξ»: n, hmkPosBodyV n.
Definition hposModV : hvl := Ξ½: _ , {@
type "Pos" = π;
val "mkPos" = hmkPosV;
val "div" = hdivV
}.
Definition hposModTTail self : hty := {@
val "mkPos" : π β: self @; "Pos";
val "div" : π β: self @; "Pos" β: π
}.
Definition oposModTTail : clty Ξ£ :=
cAnd
(cVMem "mkPos" (oAll oInt (oSel x1 "Pos")))
(cAnd
(cVMem "div" (oAll oInt (oAll (oSel x1 "Pos") oInt)))
cTop).
Lemma hposModTTail_eq : C⦠hposModTTail hx0 ⧠①oposModTTail.
Proof. rw. done. Qed.
Definition hposModTBody self : hty := {@
type "Pos" >: β₯ <: π;
val "mkPos" : π β: self @; "Pos";
val "div" : π β: self @; "Pos" β: π
}.
Example hposModTBody_alt x :
hposModTBody x = hTAnd (type "Pos" >: β₯ <: π) (hposModTTail x) :=
reflexivity _.
Definition oposModTBody : clty Ξ£ :=
cAnd (cTMemL "Pos" oBot oInt)
oposModTTail.
Lemma hposModTBody_eq : C⦠hposModTBody hx0 ⧠①oposModTBody.
Proof.
rewrite hposModTBody_alt cinterp_TAnd hposModTTail_eq.
rw. done.
Qed.
Actual type
Definition hposModT := ΞΌ: self, hposModTBody self.
Definition oposModT := oMu oposModTBody.
Lemma hposModT_eq : V⦠hposModT ⧠①oposModT.
Proof.
rewrite /hposModT /oposModT interp_TMu.
apply oMu_proper, hposModTBody_eq.
Qed.
End examplesBodies.
#[local] Hint Constructors bin_op_syntype cond_bin_op_syntype : core.
#[local] Hint Extern 1000 β lia : core.
Ltac wp_bin_base := iApply wp_bin; first eapply cond_bin_op_syntype_sound; by [cbn; eauto|].
Ltac wp_bin := iApply wp_wand; [wp_bin_base | iIntros].
#[local] Open Scope Z_scope.
Import hoasNotation.
(* Generic useful lemmas β not needed for fundamental theorem,
but very useful for examples. *)
Section helpers.
Context `{HdlangG : !dlangG Ξ£}.
Lemma wp_ge m n (Hge : m > n) : β’ WP m > n {{ w, w β‘ vbool true }}.
Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed.
Lemma wp_nge m n (Hnge : Β¬ m > n) : β’ WP m > n {{ w, w β‘ vbool false }}.
Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed.
Lemma setp_value Ξ (T : olty Ξ£) v : Ξ sβ¨ v : T β£β’ <PB> β Ο, sGβ¦ Ξ β§* Ο β T anil Ο v.[Ο].
Proof.
rewrite /setp/=; properness β //; iSplit;
[rewrite wp_value_inv|rewrite -wp_value]; iIntros "#$".
Qed.
Lemma setp_value_eq (T : olty Ξ£) v : (<PB> β Ο, T anil Ο v.[Ο]) β£β’ [] sβ¨ v : T.
Proof.
iSplit; pupd.
- iIntros "#H !>" (? _).
rewrite /= -wp_value'. iApply "H".
- iIntros "/= #H !>" (Ο).
iSpecialize ("H" $! Ο with "[//]").
by rewrite /= wp_value_inv'.
Qed.
End helpers.
Definition pos v := β n, v = vint n β§ n > 0.
Definition ipos {Ξ£} : oltyO Ξ£ := olty0 (Ξ»I Ο v, β pos v β).
Definition s_is_pos `{!dlangG Ξ£} s : iProp Ξ£ := s βn ipos.
Section div_example.
Context `{HdlangG : !dlangG Ξ£} `{SwapPropI Ξ£}.
Lemma wp_if_ge :
β’@{iPropI _} |==> β (n : Z), WP hclose (hmkPosBodyV n) {{ w, β w =@{vl} n β§ n > 0 β}}.
Proof using TypeΓ.
iDestruct loopSemT as "#>#Hl"; iIntros "!> %n".
wp_bind (IfCtx _ _).
wp_bin; ev; simplify_eq/=.
case_decide; wp_pure; first by auto.
iApply wp_wand; [iApply "Hl" | naive_solver].
Qed.
Lemma ty_mkPos :
β’ [] sβ¨ hmkPosV : oAll Vβ¦ π β§ (olty0 (Ξ»I Ο v, β β n : Z, v = n β§ n > 0 β)).
Proof using TypeΓ.
rewrite -sT_All_I /setp /= /shead. iMod wp_if_ge as "#Hge".
pupd; iIntros "!>" (Ο). rewrite /hsubst/hsubst_hoEnvD. rw.
iDestruct 1 as %(_ & n & Hw); simplify_eq/=; rewrite Hw.
iApply wp_wand; [iApply "Hge" | naive_solver].
Qed.
Lemma wp_mkPos :
β’ |==> oAll Vβ¦ π β§ (olty0 (Ξ»I Ο v, β β n : Z, v = n β§ n > 0 β)) anil ids hmkPosV.
Proof using TypeΓ. iApply wp_value_inv'. iApply (ty_mkPos with "[//]"). Qed.
Lemma wp_div_spec (m : Z) w : ipos anil ids w -β WP m `div` w {{ oInt anil ids }}.
Proof. iDestruct 1 as %(n&?&?); simplify_eq. wp_bin. by iIntros "!%"; naive_solver. Qed.
Close Scope Z_scope.
Lemma sStp_ipos_nat Πi : ⒠Πs⨠ipos <:[ i ] oInt.
Proof. pupd; iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed.
Lemma posTMem_widen Ξ l i : β’ Ξ sβ¨ oTMemL l ipos ipos <:[ i ] oTMemL l β₯ oInt.
Proof using TypeΓ.
iApply sTyp_Stp_Typ; iApply sLater_Stp_Eq; [iApply sBot_Stp | iApply sStp_ipos_nat].
Qed.
Lemma suD_posDm_ipos l Π: ⒠Πsu⨠{ l := dtysyn TInt } : cTMemL l ipos ipos.
Proof.
by iApply (suD_Typ_Abs (Ο := []) (T := ipos) TInt); [|iApply sStp_Refl..].
Qed.
Lemma sD_posDm_abs l Ξ : β’ Ξ suβ¨ { l := dtysyn TInt } : cTMemL l β₯ oInt.
Proof using TypeΓ.
iApply (suD_Typ_Stp (oLater ipos)); last iApply suD_posDm_ipos; iApply sLater_Stp_Eq;
[iApply sBot_Stp | iApply sStp_ipos_nat].
Qed.
Definition oposModT := oMu oposModTBody.
Lemma hposModT_eq : V⦠hposModT ⧠①oposModT.
Proof.
rewrite /hposModT /oposModT interp_TMu.
apply oMu_proper, hposModTBody_eq.
Qed.
End examplesBodies.
#[local] Hint Constructors bin_op_syntype cond_bin_op_syntype : core.
#[local] Hint Extern 1000 β lia : core.
Ltac wp_bin_base := iApply wp_bin; first eapply cond_bin_op_syntype_sound; by [cbn; eauto|].
Ltac wp_bin := iApply wp_wand; [wp_bin_base | iIntros].
#[local] Open Scope Z_scope.
Import hoasNotation.
(* Generic useful lemmas β not needed for fundamental theorem,
but very useful for examples. *)
Section helpers.
Context `{HdlangG : !dlangG Ξ£}.
Lemma wp_ge m n (Hge : m > n) : β’ WP m > n {{ w, w β‘ vbool true }}.
Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed.
Lemma wp_nge m n (Hnge : Β¬ m > n) : β’ WP m > n {{ w, w β‘ vbool false }}.
Proof. wp_bin. ev; simplify_eq/=. case_decide; by [|lia]. Qed.
Lemma setp_value Ξ (T : olty Ξ£) v : Ξ sβ¨ v : T β£β’ <PB> β Ο, sGβ¦ Ξ β§* Ο β T anil Ο v.[Ο].
Proof.
rewrite /setp/=; properness β //; iSplit;
[rewrite wp_value_inv|rewrite -wp_value]; iIntros "#$".
Qed.
Lemma setp_value_eq (T : olty Ξ£) v : (<PB> β Ο, T anil Ο v.[Ο]) β£β’ [] sβ¨ v : T.
Proof.
iSplit; pupd.
- iIntros "#H !>" (? _).
rewrite /= -wp_value'. iApply "H".
- iIntros "/= #H !>" (Ο).
iSpecialize ("H" $! Ο with "[//]").
by rewrite /= wp_value_inv'.
Qed.
End helpers.
Definition pos v := β n, v = vint n β§ n > 0.
Definition ipos {Ξ£} : oltyO Ξ£ := olty0 (Ξ»I Ο v, β pos v β).
Definition s_is_pos `{!dlangG Ξ£} s : iProp Ξ£ := s βn ipos.
Section div_example.
Context `{HdlangG : !dlangG Ξ£} `{SwapPropI Ξ£}.
Lemma wp_if_ge :
β’@{iPropI _} |==> β (n : Z), WP hclose (hmkPosBodyV n) {{ w, β w =@{vl} n β§ n > 0 β}}.
Proof using TypeΓ.
iDestruct loopSemT as "#>#Hl"; iIntros "!> %n".
wp_bind (IfCtx _ _).
wp_bin; ev; simplify_eq/=.
case_decide; wp_pure; first by auto.
iApply wp_wand; [iApply "Hl" | naive_solver].
Qed.
Lemma ty_mkPos :
β’ [] sβ¨ hmkPosV : oAll Vβ¦ π β§ (olty0 (Ξ»I Ο v, β β n : Z, v = n β§ n > 0 β)).
Proof using TypeΓ.
rewrite -sT_All_I /setp /= /shead. iMod wp_if_ge as "#Hge".
pupd; iIntros "!>" (Ο). rewrite /hsubst/hsubst_hoEnvD. rw.
iDestruct 1 as %(_ & n & Hw); simplify_eq/=; rewrite Hw.
iApply wp_wand; [iApply "Hge" | naive_solver].
Qed.
Lemma wp_mkPos :
β’ |==> oAll Vβ¦ π β§ (olty0 (Ξ»I Ο v, β β n : Z, v = n β§ n > 0 β)) anil ids hmkPosV.
Proof using TypeΓ. iApply wp_value_inv'. iApply (ty_mkPos with "[//]"). Qed.
Lemma wp_div_spec (m : Z) w : ipos anil ids w -β WP m `div` w {{ oInt anil ids }}.
Proof. iDestruct 1 as %(n&?&?); simplify_eq. wp_bin. by iIntros "!%"; naive_solver. Qed.
Close Scope Z_scope.
Lemma sStp_ipos_nat Πi : ⒠Πs⨠ipos <:[ i ] oInt.
Proof. pupd; iIntros "!> % _ !%"; rewrite /pos /pure_interp_prim; naive_solver. Qed.
Lemma posTMem_widen Ξ l i : β’ Ξ sβ¨ oTMemL l ipos ipos <:[ i ] oTMemL l β₯ oInt.
Proof using TypeΓ.
iApply sTyp_Stp_Typ; iApply sLater_Stp_Eq; [iApply sBot_Stp | iApply sStp_ipos_nat].
Qed.
Lemma suD_posDm_ipos l Π: ⒠Πsu⨠{ l := dtysyn TInt } : cTMemL l ipos ipos.
Proof.
by iApply (suD_Typ_Abs (Ο := []) (T := ipos) TInt); [|iApply sStp_Refl..].
Qed.
Lemma sD_posDm_abs l Ξ : β’ Ξ suβ¨ { l := dtysyn TInt } : cTMemL l β₯ oInt.
Proof using TypeΓ.
iApply (suD_Typ_Stp (oLater ipos)); last iApply suD_posDm_ipos; iApply sLater_Stp_Eq;
[iApply sBot_Stp | iApply sStp_ipos_nat].
Qed.
Actual type
Show that our program is semantically well-typed,
using the semantic unstamped typing judgment.
Theorem posModTy : ⒠[] u⨠hposModV : hposModT.
Proof using TypeΓ.
rewrite /iuetp hposModT_eq fmap_nil.
have HctxSub :
sβ¨G oLater oPreciseBody :: [] <:* oLater <$> [oPreciseBody].
by iIntros "% $".
iApply (suT_Sub (T1 := oMu oPreciseBody)); first last. {
iApply sMu_Stp_Mu. rewrite oLaterN_0.
iApply sStp_And; [| iApply sAnd2_Stp ].
iApply sStp_Trans; first iApply sAnd1_Stp.
iApply posTMem_widen.
}
iApply suT_Obj_I.
iApply suD_Cons; [done|iApply suD_posDm_ipos|].
iApply suD_Cons; [done| iApply suD_Val|iApply suD_Sing; iApply suD_Val];
iApply (suT_All_I_Strong _ _ _ HctxSub).
- pupd; unstamp_goal_tm; iMod wp_if_ge as "#Hge".
pupd; iIntros "!> %Ο [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos.
case: Hnpos β [n Hw].
iApply wp_wand; [rewrite /= {}Hw; iApply "Hge" |
iIntros (v [-> Hnpos])].
iEval rewrite /= path_wp_pv_eq.
iApply (vl_sel_lb with "[] Hpos").
iIntros "!%"; hnf. naive_solver.
- iApply suT_All_I.
pupd; unstamp_goal_tm.
pupd; iIntros "!> %Ο #[[[_ [Hpos _]] %Hw] Harg]".
rewrite /shead /stail. iSimpl.
destruct Hw as [m ->].
setoid_rewrite path_wp_pv_eq.
iPoseProof (vl_sel_ub with "Harg Hpos") as "{Harg Hpos} Harg".
wp_bind (BinRCtx _ _); iSimpl.
wp_pure.
iApply (wp_div_spec with "Harg").
Qed.
End div_example.
Proof using TypeΓ.
rewrite /iuetp hposModT_eq fmap_nil.
have HctxSub :
sβ¨G oLater oPreciseBody :: [] <:* oLater <$> [oPreciseBody].
by iIntros "% $".
iApply (suT_Sub (T1 := oMu oPreciseBody)); first last. {
iApply sMu_Stp_Mu. rewrite oLaterN_0.
iApply sStp_And; [| iApply sAnd2_Stp ].
iApply sStp_Trans; first iApply sAnd1_Stp.
iApply posTMem_widen.
}
iApply suT_Obj_I.
iApply suD_Cons; [done|iApply suD_posDm_ipos|].
iApply suD_Cons; [done| iApply suD_Val|iApply suD_Sing; iApply suD_Val];
iApply (suT_All_I_Strong _ _ _ HctxSub).
- pupd; unstamp_goal_tm; iMod wp_if_ge as "#Hge".
pupd; iIntros "!> %Ο [[_ [#Hpos _]] %Hnpos]"; lazy in Hnpos.
case: Hnpos β [n Hw].
iApply wp_wand; [rewrite /= {}Hw; iApply "Hge" |
iIntros (v [-> Hnpos])].
iEval rewrite /= path_wp_pv_eq.
iApply (vl_sel_lb with "[] Hpos").
iIntros "!%"; hnf. naive_solver.
- iApply suT_All_I.
pupd; unstamp_goal_tm.
pupd; iIntros "!> %Ο #[[[_ [Hpos _]] %Hw] Harg]".
rewrite /shead /stail. iSimpl.
destruct Hw as [m ->].
setoid_rewrite path_wp_pv_eq.
iPoseProof (vl_sel_ub with "Harg Hpos") as "{Harg Hpos} Harg".
wp_bind (BinRCtx _ _); iSimpl.
wp_pure.
iApply (wp_div_spec with "Harg").
Qed.
End div_example.
An example of how to apply adequacy to get safety.
This theorem is actually not interesting, because safety of a value is trivial,
but thanks to semantic typing lemmas, we can instead show semantic typing of
closed clients of hposModV that aren't values, and then apply adequacy to
obtain their safety.
Lemma posModVSafe : safe hposModV.
Proof.
apply (unstamped_safety_dot_sem dlangΞ£ (T := hposModT))=>*.
apply posModTy.
Qed.
Proof.
apply (unstamped_safety_dot_sem dlangΞ£ (T := hposModT))=>*.
apply posModTy.
Qed.