Add tactic_hint

linux/casestudies/pgtable.c

@@ -72,9 +72,9 @@ u64 GENMASK(int h, int l)
 [[rc::parameters("r : Z", "a : Z", "k : Z", "res : Z")]]
 [[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
 [[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
-[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]]
+[[rc::requires("{normalize_bitfield_eq (bf_slice a k r) res}")]]
 [[rc::returns("res @ int<u64>")]]
-[[rc::tactics("all: unfold normalize_bitfield in *; subst.")]]
+[[rc::tactics("all: unfold normalize_bitfield_eq in *; subst.")]]
 [[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]]
 [[rc::tactics("all: try solve_goal.")]]
 [[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]]

theories/lang/bitfield.v

 From refinedc.lang Require Import base int_type builtins_specs.
-From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast.
+From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast classes.
 
+Local Open Scope Z_scope.
 (* raw bit vector constructors *)
 
 Definition bf_nil : Z := 0.
@@ -299,18 +300,40 @@ Create HintDb bitfield_rewrite discriminated.
 #[export] Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
 #[export] Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
 
-Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
+(* Tactic to normalize a bitfield *)
+Ltac normalize_bitfield :=
+  autorewrite with bitfield_rewrite; exact: eq_refl.
+
+(* enable using normalize_bitfield with tactic_hint *)
+Definition normalize_bitfield {Σ} (bv : Z) (T : Z → iProp Σ) : iProp Σ := T bv.
 Typeclasses Opaque normalize_bitfield.
 
+Program Definition normalize_bitfield_hint {Σ} bv norm :
+  bv = norm →
+  TacticHint (normalize_bitfield (Σ:=Σ) bv) := λ H, {|
+    tactic_hint_P T := T norm;
+|}.
+Next Obligation. move => ??? -> ?. unfold normalize_bitfield. iIntros "$". Qed.
+
+Global Hint Extern 10 (TacticHint (normalize_bitfield _)) =>
+  eapply normalize_bitfield_hint; normalize_bitfield : typeclass_instances.
+
+(* enable using normalize_bitfield in function call specifications
+where one cannot use tactic_hint *)
+(* TODO: figure out how to make the following unnecessary *)
+Definition normalize_bitfield_eq (bv norm : Z) : Prop := bv = norm.
+Typeclasses Opaque normalize_bitfield_eq.
+
 Class NormalizeBitfield (bv norm : Z) : Prop :=
   normalize_bitfield_proof : bv = norm.
 
 Global Instance simpl_and_normalize_bitfield bv norm `{!NormalizeBitfield bv norm'} `{!IsProtected norm} :
-  SimplAnd (normalize_bitfield bv norm) (λ T, norm' = norm ∧ T).
+  SimplAnd (normalize_bitfield_eq bv norm) (λ T, norm' = norm ∧ T).
 Proof. erewrite normalize_bitfield_proof. done. Qed.
 
 Global Hint Extern 10 (NormalizeBitfield _ _) =>
-  autorewrite with bitfield_rewrite; exact: eq_refl : typeclass_instances.
+  normalize_bitfield : typeclass_instances.
+
 
 (* Side cond: ∀ i ∈ I, Z.testbit bv i = false. *)
 Global Instance bf_range_empty_nil_inst a k :

theories/lithium/classes.v

 (** Main typeclasses of Lithium *)
 From iris.base_logic.lib Require Export iprop.
 From iris.proofmode Require Export tactics.
-From refinedc.lithium Require Import base infrastructure.
+From refinedc.lithium Require Export base infrastructure.
 
 (** * [iProp_to_Prop] *)
 Record iProp_to_Prop {Σ} (P : iProp Σ) : Type := i2p {
@@ -52,10 +52,34 @@ Definition destruct_hint {Σ B} (hint : destruct_hint_info) (info : B) (T : iPro
 Typeclasses Opaque destruct_hint.
 Arguments destruct_hint : simpl never.
 
-(** * [vm_compute_hint] *)
+(** * [tactic_hint] *)
+Class TacticHint {Σ A} (t : (A → iProp Σ) → iProp Σ) := MkTacticHint {
+  tactic_hint_P : (A → iProp Σ) → iProp Σ;
+  tactic_hint_proof T : tactic_hint_P T -∗ t T;
+}.
+Arguments MkTacticHint {_ _ _} _ _.
+Arguments tactic_hint_proof {_ _ _} _ _.
+
+Definition tactic_hint {Σ A} (t : (A → iProp Σ) → iProp Σ) (T : A → iProp Σ) : iProp Σ :=
+  t T.
+Arguments tactic_hint : simpl never.
+
+(** ** [vm_compute_hint] *)
 Definition vm_compute_hint {Σ A B} (f : A → option B) (x : A) (T : B → iProp Σ) : iProp Σ :=
   ∃ y, ⌜f x = Some y⌝ ∗ T y.
 Arguments vm_compute_hint : simpl never.
+Typeclasses Opaque vm_compute_hint.
+
+Program Definition vm_compute_hint_hint {Σ A B} (f : A → option B) x a :
+  (∀ y, Some x = y → f a = y) →
+  TacticHint (vm_compute_hint (Σ:=Σ) f a) := λ H, {|
+    tactic_hint_P T := T x;
+|}.
+Next Obligation. move => ????????. iIntros "HT". iExists _. iFrame. iPureIntro. naive_solver. Qed.
+
+Global Hint Extern 10 (TacticHint (vm_compute_hint _ _)) =>
+  eapply vm_compute_hint_hint;
+  let H := fresh in intros ? H; vm_compute; apply H : typeclass_instances.
 
 (** * [RelatedTo] *)
 Class RelatedTo {Σ} (pat : iProp Σ) : Type := {

theories/lithium/interpreter.v

@@ -28,16 +28,6 @@ Section coq_tactics.
     (P1 -∗ P2) → envs_entails Δ (P1 ∗ T) → envs_entails Δ (P2 ∗ T).
   Proof. by rewrite envs_entails_eq => -> HP. Qed.
 
-  Lemma tac_vm_compute_hint {A B} Δ (f : A → option B) a (Q : B → iProp Σ) x:
-    (∀ y, Some x = y → f a = y) →
-    envs_entails Δ (Q x) →
-    envs_entails Δ (vm_compute_hint f a Q).
-  Proof.
-    rewrite envs_entails_eq. intros ? HQ.
-    etrans; [done|]. etrans; [ |apply: bi.exist_intro].
-    iIntros "$ !%". naive_solver.
-  Qed.
-
   Lemma tac_protected_eq_app {A} (f : A → Prop) a :
     f a → f (protected a).
   Proof. by rewrite protected_eq. Qed.
@@ -689,11 +679,11 @@ Ltac liDestructHint :=
     end
   end; repeat (liForall || liImpl); try by [exfalso; can_solve_tac].
 
-Ltac liVmComputeHint :=
+Ltac liTacticHint :=
   lazymatch goal with
-  | |- envs_entails ?Δ (vm_compute_hint ?f ?a _) =>
-      refine (tac_vm_compute_hint _ _ _ _ _ _ _);
-        [let H := fresh in intros ? H; vm_compute; apply H|]
+  | |- envs_entails ?Δ (tactic_hint ?t ?T) =>
+      let x := constr:(_ : TacticHint t) in
+      refine (tac_fast_apply (x.(tactic_hint_proof) T) _)
   end.
 
 Ltac liAccu :=
@@ -792,7 +782,7 @@ Ltac liStep :=
     | liSideCond
     | liFindInContext
     | liDestructHint
-    | liVmComputeHint
+    | liTacticHint
     | liTrue
     | liFalse
     | liAccu

theories/typing/bitfield.v

@@ -129,15 +129,15 @@ Section programs.
 
   Lemma type_arithop_bitfield_raw it v1 bv1 v2 bv2 T bv op:
     arith_op_result it bv1 bv2 op = Some bv →
-    (⌜bv1 ∈ it⌝ -∗ ⌜bv2 ∈ it⌝ -∗ ⌜arith_op_sidecond it bv1 bv2 bv op⌝ ∗ ∃ norm,
-      (⌜normalize_bitfield bv norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗
+    (⌜bv1 ∈ it⌝ -∗ ⌜bv2 ∈ it⌝ -∗ ⌜arith_op_sidecond it bv1 bv2 bv op⌝ ∗
+      (tactic_hint (normalize_bitfield bv) (λ norm, T (i2v norm it) (t2mt (norm @ bitfield_raw it))))) -∗
     typed_bin_op v1 (v1 ◁ᵥ bv1 @ bitfield_raw it) v2 (v2 ◁ᵥ bv2 @ bitfield_raw it) op (IntOp it) (IntOp it) T.
   Proof.
-    iIntros "%Hop HT Hv1 Hv2".
+    iIntros "%Hop HT Hv1 Hv2". unfold tactic_hint, normalize_bitfield.
     iApply type_val_expr_mono_strong.
     iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
     iIntros "Hbv1 Hbv2".
-    iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
+    iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
     iSplitR => //.
     iExists _. by iFrame.
   Qed.
@@ -206,15 +206,15 @@ Section programs.
 
   Lemma type_arithop_bitfield_raw_int it v1 bv v2 n T bv' op:
     arith_op_result it bv n op = Some bv' →
-    (⌜bv ∈ it⌝ -∗ ⌜n ∈ it⌝ -∗ ⌜arith_op_sidecond it bv n bv' op⌝ ∗ ∃ norm,
-      (⌜normalize_bitfield bv' norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗
+    (⌜bv ∈ it⌝ -∗ ⌜n ∈ it⌝ -∗ ⌜arith_op_sidecond it bv n bv' op⌝ ∗
+      (tactic_hint (normalize_bitfield bv') (λ norm, T (i2v norm it) (t2mt (norm @ bitfield_raw it))))) -∗
       typed_bin_op v1 (v1 ◁ᵥ bv @ bitfield_raw it) v2 (v2 ◁ᵥ n @ int it) op (IntOp it) (IntOp it) T.
   Proof.
-    iIntros "%Hop HT Hv1 Hv2".
+    iIntros "%Hop HT Hv1 Hv2". unfold tactic_hint, normalize_bitfield.
     iApply type_val_expr_mono_strong.
     iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
     iIntros "Hbv1 Hbv2".
-    iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
+    iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
     iSplitR => //.
     iExists _. by iFrame.
   Qed.
@@ -227,15 +227,15 @@ Section programs.
 
   Lemma type_arithop_int_bitfield_raw it v1 n v2 bv T bv' op:
     arith_op_result it n bv op = Some bv' →
-    (⌜n ∈ it⌝ -∗ ⌜bv ∈ it⌝ -∗ ⌜arith_op_sidecond it n bv bv' op⌝ ∗ ∃ norm,
-      (⌜normalize_bitfield bv' norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗
+    (⌜n ∈ it⌝ -∗ ⌜bv ∈ it⌝ -∗ ⌜arith_op_sidecond it n bv bv' op⌝ ∗
+      (tactic_hint (normalize_bitfield bv') (λ norm, T (i2v norm it) (t2mt (norm @ bitfield_raw it))))) -∗
     typed_bin_op v1 (v1 ◁ᵥ n @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) op (IntOp it) (IntOp it) T.
   Proof.
-    iIntros "%Hop HT Hv1 Hv2".
+    iIntros "%Hop HT Hv1 Hv2". unfold tactic_hint, normalize_bitfield.
     iApply type_val_expr_mono_strong.
     iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
     iIntros "Hbv1 Hbv2".
-    iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]".
+    iDestruct ("HT" with "Hbv1 Hbv2") as "[% ?]".
     iSplitR => //.
     iExists _. by iFrame.
   Qed.