More simpl instances for bf_cons

linux/casestudies/pgtable.c

@@ -208,7 +208,6 @@ static bool kvm_pte_valid(kvm_pte_t pte)
 [[rc::returns("{if bool_decide (level = max_level - 1) then false \
     else if negb (pte_valid pte) then false \
     else bool_decide (pte_type pte = pte_type_table)} @ boolean<bool_it>")]]
-[[rc::tactics("all: simpl_bool_hyp.")]]
 static bool kvm_pte_table(kvm_pte_t pte, u32 level)
 {
     if (level == KVM_PGTABLE_MAX_LEVELS - 1)
@@ -266,7 +265,6 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
 [[rc::requires("{pte1 = {| pte_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
 [[rc::returns("{if pte_valid pte then bool_decide (bitfield_repr pte = bitfield_repr pte1) else true} @ boolean<bool_it>")]]
 [[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
-[[rc::tactics("all: simpl_bool_hyp.")]]
 static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
                    u32 level)
 {
@@ -305,8 +303,6 @@ struct [[rc::refined_by("phys : Z", "attr : Attr", "mm_ops : mm_callbacks", "o :
 [[rc::requires("{attr = {| attr_lo_s1_attridx := mtype; attr_lo_s1_ap := ap; attr_lo_s1_sh := sh_is; attr_lo_s1_af := true; attr_hi_s1_xn := xn |} }")]]
 [[rc::returns("{if err then -err_code else 0} @ int<i32>")]]
 [[rc::ensures("own d : {if err then (phys, a, mm_ops, o) else (phys, attr, mm_ops, o)} @ hyp_map_data")]]
-[[rc::tactics("all: try congruence.")]]
-[[rc::tactics("all: simpl_bool_hyp.")]]
 static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data)
 {
     // TODO: remove 0 != once issue #45 is fixed

linux/casestudies/proofs/pgtable/pgtable_lemmas.v

@@ -53,30 +53,29 @@ Global Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
   bitfield_repr := pte_repr;
   bitfield_wf := pte_wf;
 |}.
-(*
+
 Global Instance simpl_exist_Pte P : SimplExist Pte P
-   (∃ valid type leaf_attr_lo addr undef leaf_attr_hi,
-       P {|
-           pte_valid := valid;
-           pte_type := type;
-           pte_leaf_attr_lo := leaf_attr_lo;
-           pte_addr := addr;
-           pte_undef := undef;
-           pte_leaf_attr_hi := leaf_attr_hi;
-         |}).
+  (∃ valid type leaf_attr_lo addr undef leaf_attr_hi,
+    P {|
+      pte_valid := valid;
+      pte_type := type;
+      pte_leaf_attr_lo := leaf_attr_lo;
+      pte_addr := addr;
+      pte_undef := undef;
+      pte_leaf_attr_hi := leaf_attr_hi;
+    |}).
 Proof. unfold SimplExist. naive_solver. Qed.
 Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
-   (∀ valid type leaf_attr_lo addr undef leaf_attr_hi,
-       P {|
-           pte_valid := valid;
-           pte_type := type;
-           pte_leaf_attr_lo := leaf_attr_lo;
-           pte_addr := addr;
-           pte_undef := undef;
-           pte_leaf_attr_hi := leaf_attr_hi;
-         |}).
+  (∀ valid type leaf_attr_lo addr undef leaf_attr_hi,
+    P {|
+      pte_valid := valid;
+      pte_type := type;
+      pte_leaf_attr_lo := leaf_attr_lo;
+      pte_addr := addr;
+      pte_undef := undef;
+      pte_leaf_attr_hi := leaf_attr_hi;
+    |}).
 Proof. unfold SimplForall => ? []. naive_solver. Qed.
- *)
 
 Definition addr_of (n : Z) : Z :=
   bf_slice 12 36 n.
@@ -143,9 +142,11 @@ Global Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
   bitfield_repr := prot_repr;
   bitfield_wf := prot_wf;
 |}.
-Global Instance simpl_exist_Prot P : SimplExist Prot P (∃ x w r device, P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
+Global Instance simpl_exist_Prot P : SimplExist Prot P (∃ x w r device,
+  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
 Proof. unfold SimplExist. naive_solver. Qed.
-Global Instance simpl_forall_Prot P : SimplForall Prot 4 P (∀ x w r device, P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
+Global Instance simpl_forall_Prot P : SimplForall Prot 4 P (∀ x w r device,
+  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
 Proof. unfold SimplForall => ? []. naive_solver. Qed.
 
 (* struct, const *)
@@ -164,19 +165,3 @@ Definition ap_rw : Z := 1.
 Definition ap_ro : Z := 3.
 Definition sh_is : Z := 3.
 Definition err_code : Z := 22.
-
-(* tactics TODO: SimplImpl *)
-
-Ltac simpl_bool_hyp :=
-  repeat (match goal with
-  | [ H : negb ?b = true  |- _ ] =>
-    assert (b = false) by apply negb_true_iff; clear H
-  | [ H : negb ?b = false |- _ ] =>
-    assert (b = true) by apply negb_false_iff; clear H
-  | [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil = 0 |- _ ] =>
-    assert (b = false) by (by apply (bf_cons_bool_singleton_false_iff a b)); clear H
-  | [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil ≠ 0 |- _ ] =>
-    assert (b = true) by (by apply (bf_cons_bool_singleton_true_iff a b)); clear H
-  | [ H : ?b = false |- _ ] => try (rewrite !H; clear H)
-  | [ H : ?b = true  |- _ ] => try (rewrite !H; clear H)
-  end; try solve_goal).

theories/lang/bitfield.v

@@ -26,25 +26,35 @@ Proof.
   bitblast.
 Qed.
 
+Lemma bf_cons_singleton_z_iff a k x :
+  0 ≤ a →
+  bf_cons a k x bf_nil = 0 ↔ x = 0.
+Proof.
+  move => ?. rewrite /bf_cons /bf_nil Z.lor_0_r.
+  by apply Z.shiftl_eq_0_iff.
+Qed.
+
+Lemma bf_cons_singleton_nz_iff a k x :
+  0 ≤ a →
+  bf_cons a k x bf_nil ≠ 0 ↔ x ≠ 0.
+Proof.
+  move => ?. by apply not_iff_compat, bf_cons_singleton_z_iff.
+Qed.
+
 Lemma bf_cons_bool_singleton_false_iff a b :
   0 ≤ a →
   bf_cons a 1 (Z_of_bool b) bf_nil = 0 ↔ b = false.
 Proof.
-  intros. rewrite /bf_cons /bf_nil Z.lor_0_r.
-  split.
-  - destruct b; last done.
-    simplify_eq/=. rewrite Z.shiftl_1_l.
-    have ? : 2 ^ a ≠ 0 by apply Z.pow_nonzero.
-    contradiction.
-  - move => ->. simplify_eq/=. by rewrite Z.shiftl_0_l.
+  move => ?. rewrite bf_cons_singleton_z_iff; last done.
+  by destruct b.
 Qed.
 
 Lemma bf_cons_bool_singleton_true_iff a b :
   0 ≤ a →
   bf_cons a 1 (Z_of_bool b) bf_nil ≠ 0 ↔ b = true.
 Proof.
-  intros. rewrite /not bf_cons_bool_singleton_false_iff //.
-  destruct b; naive_solver.
+  move => ?. rewrite bf_cons_singleton_nz_iff; last done.
+  by destruct b.
 Qed.
 
 Lemma bf_mask_cons_singleton a k :
@@ -321,6 +331,37 @@ Proof.
   split; naive_solver.
 Qed.
 
+(* Simplify singleton data list =/≠ 0 *)
+
+Global Instance bf_cons_singleton_z a k x `{!CanSolve (0 ≤ a)} :
+  SimplBothRel (=) 0 (bf_cons a k x bf_nil) (x = 0).
+Proof.
+  have := (bf_cons_singleton_z_iff a k x).
+  split; naive_solver.
+Qed.
+
+Global Instance bf_cons_singleton_nz_1 a k x `{!CanSolve (0 ≤ a)} :
+  SimplBoth (bf_cons a k x bf_nil ≠ 0) (x ≠ 0).
+Proof.
+  have := (bf_cons_singleton_nz_iff a k x).
+  split; naive_solver.
+Qed.
+Global Instance bf_cons_singleton_nz_2 a k x `{!CanSolve (0 ≤ a)} :
+  SimplBoth (0 ≠ bf_cons a k x bf_nil) (x ≠ 0).
+Proof.
+  have := (bf_cons_singleton_nz_iff a k x).
+  split; naive_solver.
+Qed.
+
+(* Simplify data list eq *)
+
+Global Instance bf_cons_eq a k x1 l1 x2 l2 :
+  SimplAndUnsafe true (bf_cons a k x1 l1 = bf_cons a k x2 l2) (λ T, x1 = x2 ∧ l1 = l2 ∧ T).
+Proof.
+  unfold CanSolve, SimplAndUnsafe in *.
+  naive_solver.
+Qed.
+
 (* Linux macros for bits *)
 
 Lemma Z_shl_bound a k x N :