diff --git a/theories/Combined.v b/theories/Combined.v index b57b5e7588ca5c77d4bbb0cd7d62f8a1b7c92de7..998b176e72f69b9685f6008c0664a4d86a7790b5 100644 --- a/theories/Combined.v +++ b/theories/Combined.v @@ -5,7 +5,7 @@ * time credits and time receipts, including proof-mode tactics. *) -From iris.heap_lang Require Import proofmode notation adequacy lang. +From iris_time.heap_lang Require Import proofmode notation adequacy lang. From iris.base_logic Require Import invariants. From iris_time Require Import Auth_nat Auth_mnat Misc Reduction Tactics. @@ -283,13 +283,12 @@ Section Definitions. iApply "InvClose". auto with iFrame. Qed. - Theorem tick_spec s E e v n : + Theorem tick_spec s E (v : val) n : ↑tctrN ⊆ E → - IntoVal e v → TCTR_invariant -∗ - {{{ ▷ TC 1 ∗ ▷ TRdup n }}} tick e @ s ; E {{{ RET v ; TR 1 ∗ TRdup (n+1) }}}. + {{{ ▷ TC 1 ∗ ▷ TRdup n }}} tick v @ s ; E {{{ RET v ; TR 1 ∗ TRdup (n+1) }}}. Proof using max_tr. - intros ? <-. iIntros "#Inv" (Ψ) "!# [Hγ◯ Hγ2◯] HΨ". + intros ?. iIntros "#Inv" (Ψ) "!# [Hγ◯ Hγ2◯] HΨ". iLöb as "IH". wp_lam. (* open the invariant, in order to read the value m of location ℓ: *) @@ -380,9 +379,8 @@ Section Tactics. Implicit Types Φ : val → iProp Σ. Implicit Types Δ : envs (uPredI (iResUR Σ)). - Lemma tac_wp_tick `{tctrHeapG Σ} Δ Δ1 Δ2 Δ3 Δ' i j1 j2 j3 max_tc m n p s E K e v Φ : + Lemma tac_wp_tick `{tctrHeapG Σ} Δ Δ1 Δ2 Δ3 Δ' i j1 j2 j3 max_tc m n p s E K (v : val) Φ : ↑tctrN ⊆ E → - IntoVal e v → MaybeIntoLaterNEnvs 1 Δ Δ1 → envs_lookup i Δ = Some (true, TCTR_invariant max_tc) → envs_lookup j1 Δ1 = Some (false, TC (S m)) → @@ -392,7 +390,7 @@ Section Tactics. envs_simple_replace j3 false (Esnoc Enil j3 (TR (S n))) Δ3 = Some Δ2 → envs_simple_replace j2 false (Esnoc Enil j2 (TRdup (S p))) Δ2 = Some Δ' → envs_entails Δ' (WP fill K v @ s; E {{ Φ }}) → - envs_entails Δ (WP fill K (App tick e) @ s; E {{ Φ }}). + envs_entails Δ (WP fill K (App tick v) @ s; E {{ Φ }}). Admitted. End Tactics. @@ -402,8 +400,8 @@ Ltac wp_tick := lazymatch goal with | |- envs_entails _ (wp ?s ?E ?e ?Q) => first - [ reshape_expr e ltac:(fun K e' => - eapply (tac_wp_tick _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ K) ; [ | exact _ | ..] + [ 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 diff --git a/theories/TimeCredits.v b/theories/TimeCredits.v index 94f0e4c4f3b227873e200a3f4f75ebb9ec9c6445..ee61afa80f3d9df6a84cf862aaf6520e4a580555 100644 --- a/theories/TimeCredits.v +++ b/theories/TimeCredits.v @@ -552,7 +552,7 @@ Section Tactics. End Tactics. -Ltac wp_tick := +Ltac wp_tick ::= let solve_TICKCTXT _ := iAssumptionCore || fail "wp_tick: cannot find TC_invariant" in let solve_TC _ := @@ -574,21 +574,3 @@ Ltac wp_tick := | wp_expr_simpl ] | _ => fail "wp_tick: not a 'wp'" end. - -Ltac wp_tick_closure := wp_closure; wp_tick. -Ltac wp_tick_pair := wp_tick; wp_pair. -Ltac wp_tick_inj := wp_tick; wp_inj. - -Ltac wp_tick_rec := wp_tick ; wp_rec; simpl_trans. -Ltac wp_tick_lam := wp_tick_rec. -Ltac wp_tick_let := wp_tick_closure; wp_tick_lam. -Ltac wp_tick_seq := wp_tick_let. -Ltac wp_tick_op := wp_tick ; wp_op. -Ltac wp_tick_if := wp_tick ; wp_if. -Ltac wp_tick_match := - wp_tick; wp_match; (wp_let || wp_seq); wp_lam; - wp_closure; wp_tick; wp_tick; wp_lam. -Ltac wp_tick_proj := wp_tick ; wp_proj. -Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc. -Ltac wp_tick_load := wp_tick ; wp_load. -Ltac wp_tick_store := wp_tick ; wp_store. diff --git a/theories/Translation.v b/theories/Translation.v index 441700ca8ebde7bd403eca781360a250f9dd2ab9..402124bfdf17b7caa55040509a9aee5a472b1c36 100644 --- a/theories/Translation.v +++ b/theories/Translation.v @@ -581,3 +581,29 @@ Section ClosureFree. Qed. End ClosureFree. + +(* + * Proofmode wp_* tactics. + *) + +(* wp_tick is a stub to be redefined for each particular definition of + the tick function. *) +Ltac wp_tick := idtac. + +Ltac wp_tick_closure := wp_closure; wp_tick. +Ltac wp_tick_pair := wp_tick; wp_pair. +Ltac wp_tick_inj := wp_tick; wp_inj. + +Ltac wp_tick_rec := wp_tick ; wp_rec; simpl_trans. +Ltac wp_tick_lam := wp_tick_rec. +Ltac wp_tick_let := wp_tick_closure; wp_tick_lam. +Ltac wp_tick_seq := wp_tick_let. +Ltac wp_tick_op := wp_tick ; wp_op. +Ltac wp_tick_if := wp_tick ; wp_if. +Ltac wp_tick_match := + wp_tick; wp_match; (wp_let || wp_seq); wp_lam; + wp_closure; wp_tick; wp_tick; wp_lam. +Ltac wp_tick_proj := wp_tick ; wp_proj. +Ltac wp_tick_alloc loc := wp_tick ; wp_alloc loc. +Ltac wp_tick_load := wp_tick ; wp_load. +Ltac wp_tick_store := wp_tick ; wp_store.