Commit 0a8217ea authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

wp_tick for TimeReceipts.

parent 89d9714d
...@@ -22,7 +22,7 @@ Section clock_int. ...@@ -22,7 +22,7 @@ Section clock_int.
Lemma clock_int_add_spec (n1 n2 : mach_int) : Lemma clock_int_add_spec (n1 n2 : mach_int) :
TR_invariant nmax - TR_invariant nmax -
{{{ is_clock_int (`n1) is_clock_int (`n2) }}} {{{ is_clock_int (`n1) is_clock_int (`n2) }}}
#n1 + #n2 «#n1 + #n2»
{{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_clock_int (`n1+`n2) }}}. {{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_clock_int (`n1+`n2) }}}.
Proof. Proof.
iIntros "#Htrinv" (Φ) "!# ([% H1] & [% H2]) Post". iIntros "#Htrinv" (Φ) "!# ([% H1] & [% H2]) Post".
...@@ -36,9 +36,10 @@ Section clock_int. ...@@ -36,9 +36,10 @@ Section clock_int.
{ apply bool_decide_pack. split; [|done]. { apply bool_decide_pack. split; [|done].
(* FIXME : why isn't lia able to do this directly? *) (* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. } trans 0. unfold min_mach_int; lia. lia. }
wp_op. iDestruct ("Post" with "[H]") as "Post".
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. } { iIntros "{$H} !%". lia. }
iApply "Post". iIntros "{$H} /= !%". lia. simpl_trans. wp_tick_op=>//.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
Qed. Qed.
End clock_int. End clock_int.
...@@ -52,7 +53,7 @@ Section snapclock_int. ...@@ -52,7 +53,7 @@ Section snapclock_int.
Context `{timeReceiptHeapG Σ}. Context `{timeReceiptHeapG Σ}.
Context (nmax : nat). Context (nmax : nat).
Context `(nmax max_mach_int). Context `(nmax < max_mach_int).
Definition is_snapclock_int (n : Z) : iProp Σ := Definition is_snapclock_int (n : Z) : iProp Σ :=
(0 n TRdup (Z.to_nat n))%I. (0 n TRdup (Z.to_nat n))%I.
...@@ -66,24 +67,22 @@ Section snapclock_int. ...@@ -66,24 +67,22 @@ Section snapclock_int.
Lemma snapclock_int_incr_spec (n1 : mach_int) : Lemma snapclock_int_incr_spec (n1 : mach_int) :
TR_invariant nmax - TR_invariant nmax -
{{{ is_snapclock_int (`n1) }}} {{{ is_snapclock_int (`n1) }}}
tick #() ;; #n1 + #mach_int_1 «#n1 + #mach_int_1»
{{{ H, RET #(LitMachInt ((`n1+1) H)) ; is_snapclock_int (`n1+1) }}}. {{{ H, RET #(LitMachInt ((`n1+1) H)) ; is_snapclock_int (`n1+1) }}}.
Proof. Proof.
iIntros "#Htrinv" (Φ) "!# [% H1] Post". iIntros "#Htrinv" (Φ) "!# [% H] Post".
wp_apply (tick_spec_simple nmax #() with "Htrinv H1"). iIntros "(_ & H)".
iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; first done. iDestruct (TRdup_lt_nmax with "Htrinv H") as ">(H & Hnmax)" ; first done.
iDestruct "Hnmax" as %Hnmax. wp_seq. iDestruct "Hnmax" as %Hnmax.
assert (`n1 + 1 < max_mach_int). assert (`n1 + 1 < max_mach_int).
{ rewrite -(Nat2Z.id nmax) (_:1%nat = Z.to_nat 1) // -Z2Nat.inj_add // in Hnmax. { rewrite -(Nat2Z.id nmax) in Hnmax. apply Z2Nat.inj_lt in Hnmax; lia. }
apply Z2Nat.inj_lt in Hnmax; lia. }
assert (bool_decide (mach_int_bounded (`n1 + 1))). assert (bool_decide (mach_int_bounded (`n1 + 1))).
{ apply bool_decide_pack. split; [|done]. { apply bool_decide_pack. split; [|done].
(* FIXME : why isn't lia able to do this directly? *) (* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. } trans 0. unfold min_mach_int; lia. lia. }
wp_op. simpl_trans. wp_tick_op.
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. } { by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. }
iApply "Post". iSplit. auto with lia. iApply "Post". iSplit. auto with lia.
by rewrite Z2Nat.inj_add //. rewrite Z2Nat.inj_add // Nat.add_comm //.
Qed. Qed.
(* Snapclock integers also support a limited form of addition: *) (* Snapclock integers also support a limited form of addition: *)
...@@ -91,7 +90,7 @@ Section snapclock_int. ...@@ -91,7 +90,7 @@ Section snapclock_int.
TR_invariant nmax - TR_invariant nmax -
{{{ is_snapclock_int (`n1) is_snapclock_int (`n2) {{{ is_snapclock_int (`n1) is_snapclock_int (`n2)
is_snapclock_int m `n1+`n2 m }}} is_snapclock_int m `n1+`n2 m }}}
#n1 + #n2 «#n1 + #n2»
{{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_snapclock_int (`n1+`n2) }}}. {{{ H, RET #(LitMachInt ((`n1+`n2) H)) ; is_snapclock_int (`n1+`n2) }}}.
Proof. Proof.
iIntros "#Htrinv" (Φ) "!# ([% _] & [% _] & [% Hm] & %) Post". iIntros "#Htrinv" (Φ) "!# ([% _] & [% _] & [% Hm] & %) Post".
...@@ -105,9 +104,10 @@ Section snapclock_int. ...@@ -105,9 +104,10 @@ Section snapclock_int.
{ apply bool_decide_pack. split; [|lia]. { apply bool_decide_pack. split; [|lia].
(* FIXME : why isn't lia able to do this directly? *) (* FIXME : why isn't lia able to do this directly? *)
trans 0. unfold min_mach_int; lia. lia. } trans 0. unfold min_mach_int; lia. lia. }
wp_op. iDestruct ("Post" with "[H]") as "Post".
{ by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left. } { iSplit; auto with lia. }
iApply "Post". iSplit; [|done]. auto with lia. simpl_trans. wp_tick_op=>//.
by rewrite /bin_op_eval /= /to_mach_int /mach_int_bounded decide_left.
Qed. Qed.
End snapclock_int. End snapclock_int.
...@@ -12,7 +12,6 @@ From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics. ...@@ -12,7 +12,6 @@ From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation. From iris_time Require Export Translation Simulation.
From iris.proofmode Require Import coq_tactics. From iris.proofmode Require Import coq_tactics.
Import uPred.
Implicit Type e : expr. Implicit Type e : expr.
Implicit Type v : val. Implicit Type v : val.
......
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris.base_logic Require Import invariants. From iris.base_logic Require Import invariants.
From iris.proofmode Require Import coq_tactics.
From iris_time.heap_lang Require Import proofmode notation adequacy lang.
From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics. From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics.
From iris_time Require Export Translation Simulation. From iris_time Require Export Translation Simulation.
...@@ -78,8 +79,7 @@ Global Instance receipts_tick `{TickCounter} : Tick := ...@@ -78,8 +79,7 @@ Global Instance receipts_tick `{TickCounter} : Tick :=
Section TickSpec. Section TickSpec.
Context `{timeReceiptHeapG Σ}. Context `{timeReceiptHeapG Σ} (nmax : nat).
Context (nmax : nat).
Definition TR (n : nat) : iProp Σ := Definition TR (n : nat) : iProp Σ :=
own γ1 (nat n). own γ1 (nat n).
...@@ -137,19 +137,21 @@ Section TickSpec. ...@@ -137,19 +137,21 @@ Section TickSpec.
Definition TR_invariant : iProp Σ := Definition TR_invariant : iProp Σ :=
inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (mnat n) (n < nmax)%nat)%I. inv timeReceiptN ( (n:nat), #(nmax-n-1) own γ1 (nat n) own γ2 (mnat n) (n < nmax)%nat)%I.
Lemma zero_TR : Lemma zero_TR E :
TR_invariant ={}= TR 0. timeReceiptN E
TR_invariant ={E}= TR 0.
Proof. Proof.
iIntros "#Htickinv". iIntros (?) "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose". iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & H)" "Hclose".
iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]". iDestruct (own_auth_nat_null with "Hγ1●") as "[Hγ1● $]".
iApply "Hclose" ; eauto with iFrame. iApply "Hclose" ; eauto with iFrame.
Qed. Qed.
Lemma zero_TRdup : Lemma zero_TRdup E :
TR_invariant ={}= TRdup 0. timeReceiptN E
TR_invariant ={E}= TRdup 0.
Proof. Proof.
iIntros "#Htickinv". iIntros (?) "#Htickinv".
iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose". iInv timeReceiptN as (m) ">(Hcounter & Hγ1● & Hγ2● & Im)" "Hclose".
iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]". iDestruct (own_auth_mnat_null with "Hγ2●") as "[Hγ2● $]".
iApply "Hclose" ; eauto with iFrame. iApply "Hclose" ; eauto with iFrame.
...@@ -380,17 +382,79 @@ Section Soundness. ...@@ -380,17 +382,79 @@ Section Soundness.
End Soundness. End Soundness.
(* (*
* Proof-mode tactics for proving WP of translated expressions * Proof-mode tactics for proving WP of translated expressions
*) *)
Section Tactics. Lemma tac_wp_tick `{timeReceiptHeapG Σ} Δ pe Δ1 Δ2 Δ' i max_tc s E K (v : val) Φ :
timeReceiptN E
(* TODO *) MaybeIntoLaterNEnvs 1 Δ Δ1
End Tactics. envs_lookup i Δ = Some (pe, TR_invariant max_tc)
Ltac wp_tock := ( j pe' p, envs_lookup j Δ1 = Some (pe', TRdup p)
idtac. envs_simple_replace j pe' (Esnoc Enil j (TRdup (S p))) Δ1 = Some Δ2)
Δ1 = Δ2
( j n, envs_lookup j Δ2 = Some (false, TR n)
envs_simple_replace j false (Esnoc Enil j (TR (S n))) Δ2 = Some Δ')
Δ2 = Δ'
envs_entails Δ' (WP fill K v @ s; E {{ Φ }})
envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=>??? HTRdup HTR HWP.
iIntros "HΔ".
iAssert (TR_invariant max_tc) as "#Hinv".
{ destruct pe.
iDestruct (envs_lookup_sound _ i true with "HΔ") as "[? _]"=>//.
iDestruct (envs_lookup_sound _ i false with "HΔ") as "[? _]"=>//. }
iDestruct (into_laterN_env_sound with "HΔ") as "HΔ1"=>//.
iApply wp_bind.
destruct HTR as [(j & n & HTR1 & HTR2)| ->],
HTRdup as [(j' & pe'' & p & HTRDup1 & HTRDup2)| ->].
- iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTRdup HΔ2]"=>//.
rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if.
iDestruct "HTRdup" as "#>HTRdup".
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [HTR #HTRdup']". iApply HWP.
rewrite Nat.add_comm. iSpecialize ("HΔ2" with "[//]").
iDestruct (envs_simple_replace_singleton_sound with "HΔ2") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [HTR _]". iApply HWP.
iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTR' HΔ']"=>//=.
iCombine "HTR HTR'" as "HTR". iDestruct ("HΔ'" with "HTR") as "$".
- iDestruct (envs_simple_replace_singleton_sound with "HΔ1") as "[HTRdup HΔ']"=>//.
rewrite bi.intuitionistically_if_elim -bi.intuitionistically_intuitionistically_if.
iDestruct "HTRdup" as "#>HTRdup".
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". iApply HWP.
rewrite Nat.add_comm. iDestruct ("HΔ'" with "[//]") as "$".
- iMod (zero_TRdup with "Hinv") as "HTRdup"=>//.
iApply (tick_spec with "[//] HTRdup")=>//. iIntros "!> [_ #HTRdup']". by iApply HWP.
Qed.
Ltac wp_tick ::=
iStartProof ;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
first
[ reshape_expr false e ltac:(fun K e' =>
eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ K)
)
| fail 1 "wp_tick: cannot find 'tick ?v' in" e ] ;
[ try solve_ndisj
| exact _
| (* lookup invariant: *) (iAssumptionCore || fail "wp_tick: cannot find TR_invariant")
| (* lookup TRdup: *) (
left; eexists _, _, _; split;
[iAssumptionCore | proofmode.reduction.pm_reflexivity]
|| right; reflexivity)
| (* lookup TR: *) (
left; eexists _, _; split;
[iAssumptionCore | proofmode.reduction.pm_reflexivity]
|| right; reflexivity)
| wp_expr_simpl ]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
fail "wp_tick is not implemented for twp"
| _ => fail "wp_tick: not a 'wp'"
end.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment