- Bv_extensions: new lemmas to extend the simplification tactics on b…

…itvectors, plus light versions of these tactics

- Extended Capability module with Translation definitions and lemmas from manipulations on capabilities to bitvector operations
- New lemma cap_seal_preserves_value

coq-cheri-capabilities.opam

@@ -6,7 +6,7 @@ maintainer: ["ricardo.almeida@ed.ac.uk"]
 authors: ["Ricardo Almeida" "Vadim Zaliva"]
 license: "BSD-3-clause"
 homepage: "https://github.com/rems-project/coq-cheri-capabilities"
-version: "20240605"
+version: "20240610"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
  "dune" {>= "3.7"}

theories/Morello/Bv_extensions.v

@@ -0,0 +1,73 @@
+From stdpp.unstable Require Import bitvector bitvector_tactics.
+
+
+Lemma bv_wrap_of_smaller_wrap n m b:
+ (m <= n)%N ->
+ bv_wrap n (bv_wrap m b) = bv_wrap m b.
+Proof.
+ intros ?. rewrite bv_wrap_small; [ reflexivity |].
+ assert (0 ≤ bv_wrap m b < bv_modulus m)%Z by apply bv_wrap_in_range.
+ assert (P: (m <= n)%N) by lia. 
+ apply bv_modulus_le_mono in P. 
+ lia. 
+ Qed.
+
+Lemma bv_wrap_of_larger_wrap_sum n m (b : bv 129) :
+ (m < n)%N -> 
+ bv_wrap m (bv_wrap n (bv_unsigned b) + 16) = bv_wrap m (bv_unsigned b + 16).
+Proof.
+ intros ?.
+ replace (bv_wrap m (bv_wrap n (bv_unsigned b) + 16)) with (bv_wrap m (bv_wrap n ((bv_wrap n (bv_unsigned b) + 16))));
+ [ rewrite bv_wrap_add_idemp_l; rewrite bv_wrap_bv_wrap; [ reflexivity | lia ] 
+ | rewrite bv_wrap_bv_wrap; [ reflexivity | lia ]; reflexivity ].
+ Qed.
+
+Lemma bv_extract_idemp n m (b : bv n) : 
+ bv_extract 0 m (bv_extract 0 m b) = bv_extract 0 m b.
+Proof. 
+ apply bv_eq_wrap. rewrite bv_extract_0_unsigned. 
+ apply bv_wrap_bv_wrap. lia.
+ Qed.
+
+Lemma bv_extract_full n (b : bv n) :
+ bv_extract 0 n b = b.
+Proof. 
+ apply bv_eq_wrap. rewrite bv_extract_0_unsigned. 
+ apply bv_wrap_bv_wrap. lia.
+ Qed.
+
+Global Hint Rewrite bv_wrap_of_smaller_wrap using lia : bv_simplify.
+Global Hint Rewrite bv_wrap_of_larger_wrap_sum using lia : bv_simplify.
+Global Hint Rewrite bv_extract_idemp : bv_simplify.
+Global Hint Rewrite bv_extract_full : bv_simplify.
+Global Hint Rewrite @bv_extract_0_unsigned : bv_simplify.
+Global Hint Rewrite @bv_and_unsigned : bv_simplify.
+
+
+(** * Light versions of the [bv_simplify], [bv_simplify_arith] and [bv_solve] tactics from stdpp's bitvector *)
+
+Tactic Notation "bv_simplify_light" :=
+ autorewrite with bv_simplify;
+ lazymatch goal with
+ | |- _ =@{bv _} _ => apply bv_eq_wrap
+ | |- not (_ =@{bv _} _) => apply bv_neq_wrap
+ | _ => idtac
+ end;
+ bv_unfold;
+ autorewrite with bv_unfolded_simplify.
+
+Tactic Notation "bv_simplify_arith_light" :=
+ bv_simplify_light;
+ autorewrite with bv_unfolded_to_arith.
+
+Ltac bv_solve_light :=
+ bv_simplify_arith_light;
+ unfold bv_signed, bv_swrap, bv_wrap, bv_half_modulus, bv_modulus, bv_unsigned;
+ simpl;
+ lia.
+
+Ltac bv_simp_r := repeat bv_simplify.
+Tactic Notation "bv_simp_r" := bv_simp_r.
+Tactic Notation "bv_simp_r" ident(H) :=
+ repeat (bv_simplify H).
+

theories/Morello/Capabilities.v

@@ -11,6 +11,7 @@ From SailStdpp Require Import Base Values Values_lemmas Operators_mwords Machine
 
 From CheriCaps.Common Require Import Utils Addr Capabilities.
 From CheriCaps Require Import CapFns.
+From CheriCaps.Morello Require Import Bv_extensions.
 
 
 (** Notations and their definitions **)
@@ -1145,33 +1146,175 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
  - intro H. rewrite H. apply eqb_refl.
  Defined. 
 
+(* Beginning of Translation definitions and lemmas from Capabilities to bitvectors. *)
+
+ Ltac simpl_arith :=
+ (* repeat ( *)
+ change (63 - 0 + 1)%Z with 64%Z in *;
+ change (63 + 1)%positive with 64%positive in *;
+ change (95 - 1)%Z with 94%Z in *;
+ change (63 + 1)%nat with 64%nat in *;
+ change (109 - 95 + 1)%Z with 15%Z in *;
+ change (-95 + 95)%Z with 0%Z in *;
+ change (0+64-1+1)%Z with 64%Z in *;
+ change (0+64-1)%Z with 63%Z in *; 
+ change (Z.to_nat 0) with 0%nat in *;
+ change (Z.to_nat 64) with 64%nat in *;
+ change (Z.to_nat 15) with 15%nat in *;
+ change (Z.to_nat 95) with 95%nat in *;
+ change (Z.to_nat 110) with 110%nat in *;
+ change (Z.to_nat 128) with 128%nat in *;
+ change (Z.to_nat 129) with 129%nat in *;
+ change (Z.to_nat (109 - 94)%Z) with 15%nat in *;
+ change (Z.of_N 95) with 95%Z in *;
+ change (Z.of_nat 128) with 128%Z in *;
+ change (Z.of_N (0+0)) with 0%Z in *;
+ change (N.of_nat (Z.to_nat (127 - 110 + 1 - 1 - 0 + 1))) with 18%N in *;
+ change (Pos.to_nat 1) with 1%nat in *;
+ change (Pos.to_nat 64) with 64%nat in *;
+ change (N.of_nat 0) with 0%N in *;
+ change (N.of_nat 1) with 1%N in *;
+ change (N.of_nat 15) with 15%N in *;
+ change (N.of_nat 18) with 18%N in *;
+ change (N.of_nat 19) with 19%N in *;
+ change (N.of_nat 64) with 64%N in *;
+ change (N.of_nat 110) with 110%N in *;
+ change (N.of_nat 15) with 15%N in *;
+ change (N.of_nat 64) with 64%N in *; 
+ change (N.of_nat 95) with 95%N in *;
+ change (N.of_nat 129) with 129%N in *;
+ (* try (change (S `{?x}) with (x+1)%nat); *)
+ try (change (Pos.succ `{?x}) with 110%positive)
+ .
+
+ Ltac simpl_arith_r := repeat simpl_arith.
+
  Ltac unfold_cap :=
- repeat 
- (unfold Capability.cap_permits_load, Capability.cap_permits_store, Capability.cap_get_perms, Capability.cap_is_unsealed, Capability.cap_is_sealed, Capability.cap_get_value, Capability.cap_set_value; simpl;
+ repeat (
+ unfold Capability.cap_permits_load, Capability.cap_permits_store, Capability.cap_get_perms, Capability.cap_is_unsealed, Capability.cap_is_sealed, Capability.cap_get_value, Capability.cap_set_value, cap_set_objtype; 
  unfold Capabilities.Permissions.has_load_perm, Capabilities.Permissions.has_store_perm, len, Capabilities.Permissions.has_perm; 
  unfold AddressValue.t, AddressValue.len in *;
- unfold CapFns.CapGetValue, CapFns.CapSetValue, CapFns.CapPermsInclude, CapFns.CapGetPermissions, CapFns.CAP_PERM_LOAD, CapFns.CAP_PERM_STORE, CapFns.CAP_PERMS_NUM_BITS, CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT, CapFns.integer_subrange, CapFns.CapIsSealed, CapFns.Zeros, CapFns.CapGetObjectType, CapFns.CAP_VALUE_NUM_BITS, CapFns.CAP_VALUE_HI_BIT, CapFns.CAP_VALUE_LO_BIT, CapFns.CAP_OTYPE_LO_BIT in *; simpl;
- unfold Operators_mwords.get_slice_int, Operators_mwords.subrange_vec_dec, Operators_mwords.neq_vec, Operators_mwords.eq_vec, Operators_mwords.update_subrange_vec_dec; simpl;
- unfold MachineWord.update_slice, MachineWord.MachineWord.slice, MachineWord.MachineWord.Z_to_word, MachineWord.MachineWord.and, MachineWord.MachineWord.eqb, MachineWord.MachineWord.eq_dec, MachineWord.MachineWord.zero_extend, MachineWord.MachineWord.zeros; simpl;
- unfold Values.shl_int, Values.to_word_nat, Values.to_word, Values.get_word; simpl;
- unfold TypeCasts.autocast; simpl; 
- bv_simplify; 
- change (63 - 0 + 1) with 64;
- change (63 + 1)%positive with 64%positive;
- change (Z.to_nat 0) with 0%nat;
- change (Z.to_nat 64) with 64%nat;
- change (Z.to_nat 110) with 110%nat;
- change (Pos.to_nat 64) with 64%nat;
- change (N.of_nat 0) with 0%N;
- change (N.of_nat 18) with 18%N;
- change (N.of_nat 64) with 64%N;
- change (N.of_nat 110) with 110%N;
- change (Z.to_nat 95) with 95%nat;
- change (N.of_nat 15) with 15%N;
- change (N.of_nat 95) with 95%N;
+ unfold ObjType.t, ObjType.len in *;
+ unfold CapFns.CapGetValue, CapFns.CapSetValue, CapFns.CapPermsInclude, CapFns.CapGetPermissions, CapFns.CAP_PERM_LOAD, CapFns.CAP_PERM_STORE, CapFns.CAP_PERMS_NUM_BITS, CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT, CapFns.CapSetObjectType, CapFns.integer_subrange, CapFns.CapIsSealed, CapFns.Zeros, CapFns.CapGetObjectType, CapFns.CAP_VALUE_NUM_BITS, CapFns.CAP_VALUE_HI_BIT, CapFns.CAP_VALUE_LO_BIT, CapFns.CAP_OTYPE_HI_BIT, CapFns.CAP_OTYPE_LO_BIT in *; 
+ unfold Operators_mwords.get_slice_int, Operators_mwords.subrange_vec_dec, Operators_mwords.neq_vec, Operators_mwords.eq_vec, Operators_mwords.update_subrange_vec_dec; 
+ unfold MachineWord.update_slice, MachineWord.MachineWord.slice, MachineWord.MachineWord.Z_to_word, MachineWord.MachineWord.and, MachineWord.MachineWord.eqb, MachineWord.MachineWord.eq_dec, MachineWord.MachineWord.zero_extend, MachineWord.MachineWord.zeros; 
+ unfold Values.shl_int, Values.to_word_nat, Values.to_word, Values.get_word; 
+ unfold TypeCasts.autocast; 
+ simpl_arith;
  simpl;
  bv_simplify).
 
+ Lemma subrange_vec_dec_after_clear_tag (c:t) (hi lo : Z) :
+ let c : mword 129 := c in
+ (hi <? 128)%Z -> (lo <? hi)%Z ->
+ subrange_vec_dec c hi lo = subrange_vec_dec (CapWithTagClear c) hi lo.
+ Proof.
+ intros x H J. 
+ assert (Hp: (hi < 128)%Z); [ apply Is_true_eq_true in H; lia |].
+ unfold subrange_vec_dec, CapWithTagClear, CapSetTag, CAP_TAG_BIT, autocast. 
+ simpl. bv_simplify.
+ destruct (Z.eq_dec _ _); [| reflexivity].
+ unfold MachineWord.slice, MachineWord.zero_extend, MachineWord.N_to_word. simpl.
+ change (Bit (vec_of_bits [access_vec_dec _ 0])) with B0.
+ unfold update_vec_dec, update_mword_dec. simpl. 
+ unfold MachineWord.set_bit, MachineWord.update_slice, MachineWord.slice. simpl.
+ replace (bv_extract _ 0 _) with (bv_0 0); [| bv_simplify; bitblast].
+ bv_simplify. 
+ rewrite bv_zero_extend_idemp.
+ change (bv_zero_extend _ _) with (bv_concat 129 (bv_0 1) (bv_extract 0 128 c)).
+ replace (N.of_nat (Z.to_nat lo)) with (Z.to_N lo); [| rewrite Z_nat_N; reflexivity].
+ replace (bv_extract _ _ (bv_concat _ _ _)) with (bv_extract (Z.to_N lo) (N.of_nat (Z.to_nat hi - Z.to_nat lo + 1)) (bv_extract 0 128 c)); [| bv_simplify; reflexivity].
+ set (len := (N.of_nat (Z.to_nat hi - Z.to_nat lo + 1))).
+ replace (bv_extract _ _ (bv_extract _ _ _)) with (bv_extract (Z.to_N lo) len c). reflexivity.
+ bv_simplify. rewrite bv_extract_unsigned. rewrite bv_extract_unsigned. bv_simplify. bitblast. 
+ Qed. 
+
+ Lemma cap_value_bv (c:t) : cap_get_value c = @bv_extract 129 0 64 c. 
+ Proof. done. Qed.
+
+ Lemma cap_seal_indirect_entry_bv (c:t) :
+ cap_is_valid c ->
+ cap_is_unsealed c ->
+ cap_seal_indirect_entry c = bv_concat 129 (bv_extract (n:=129) 110 19 c) (bv_concat 110 (BV 15 3) (bv_extract (n:=129) 0 95 c)).
+ Proof. 
+ intros H1 H2. 
+ unfold cap_seal_indirect_entry, cap_seal_immediate.
+ assert (H3: cap_is_valid c /\ cap_is_unsealed c); [ split; assumption |]; 
+ apply andb_prop_intro in H3; destruct (_ && _); try contradiction.
+ reflexivity.
+ Qed.
+
+ Lemma cap_is_valid_bv_and (c:t) : (* could this be moved to SimplAnd? *)
+ cap_is_valid c ->
+ bv_and c (BV 129 (2^128)) = BV 129 (2^128).
+ Proof. 
+ unfold cap_is_valid, CapFns.CapIsTagClear, CapFns.CapGetTag, CapFns.CAP_TAG_BIT. unfold Operators_mwords.access_vec_dec. simpl. unfold Values.access_mword_dec. unfold get_word, MachineWord.get_bit.
+ simpl_arith_r.
+ destruct (Z.testbit (@bv_unsigned 129 c) 128) eqn:U.
+ + intros. bv_simplify. unfold len. bv_simplify. bitblast as m. replace m with 128%Z; [ assumption | lia ].
+ + done.
+ Qed.
+
+ Lemma cap_is_unsealed_bv_and (c:t) : 
+ cap_is_unsealed c ->
+ bv_and c (BV 129 0x3FFF800000000000000000000000) = BV 129 0.
+ Proof.
+ unfold_cap.
+ simpl_arith_r.
+ intro H.
+ case_decide.
+ - apply bv_eq_wrap. unfold len. bv_simplify.
+ bitblast as n.
+ apply bv_eq_wrap in H0. 
+ simpl_arith_r.
+ repeat bv_simplify H0. 
+ replace (bv_wrap 64 (bv_unsigned _)) with (bv_unsigned (bv_extract 95 15 c)) in H0; [| bv_simp_r; bitblast].
+ rewrite <- (@Z.mul_cancel_r _ _ (2^95)) in H0; [| lia].
+ rewrite <- (@Z.shiftl_mul_pow2 _ 95) in H0; [| lia].
+ change (bv_wrap 64 0 * 2 ^ 95)%Z with 0%Z in H0.
+ bitblast H0 with n as H1.
+ rewrite bv_extract_unsigned in H1.
+ rewrite bv_wrap_spec_low in H1; [| lia ].
+ rewrite Z.shiftr_spec in H1; [| lia ]. 
+ simpl_arith_r.
+ rewrite <- H1. apply f_equal. lia.
+ - done. 
+ Qed. 
+
+ Lemma cap_valid_and_unsealed_bv_and (c:t) : 
+ cap_is_valid c -> 
+ cap_is_unsealed c -> 
+ bv_and c (BV 129 0x100003FFF800000000000000000000000) =
+ BV 129 (2^128).
+ Proof. 
+ intros Htag Hotype. apply cap_is_valid_bv_and in Htag. apply cap_is_unsealed_bv_and in Hotype. bv_simp_r.
+ bv_simp_r Htag. bv_simp_r Hotype. unfold len. 
+ bitblast as n. 
+ change (bv_unsigned (BV 129 (2 ^ 128))) with (2 ^ 128)%Z in *. 
+ change (bv_unsigned 0) with 0%Z in Hotype.
+ bitblast Htag with n as Htag'. bitblast Hotype with n as Hotype'. 
+ case_bool_decide.
+ - replace n with 128%Z in *; [ | lia ]. done. 
+ - assert (Hn: (n < Z.of_N 128)%Z); [ lia |]. 
+ replace (Z.testbit (2 ^ 128) n) with false.
+ { replace (Z.testbit (bv_unsigned (BV 129 340283664955539015913149571259078541312)) n) with (Z.testbit (bv_unsigned (BV 129 1298034600552449774963827310329856)) n); 
+ [ | replace (bv_unsigned 1298034600552449774963827310329856) with 1298034600552449774963827310329856%Z; 
+ [ replace (bv_unsigned 340283664955539015913149571259078541312) with 340283664955539015913149571259078541312%Z; [ bitblast | bv_solve ] | bv_solve ] ].
+ exact Hotype'. }
+ { rewrite Z.pow2_bits_false; [ reflexivity | lia ]. } 
+ Qed.
+
+ Lemma cap_is_unsealed_eq_vec (c : t ): 
+ cap_is_unsealed c <-> Operators_mwords.eq_vec (CapFns.CapGetObjectType c) (MachineWord.MachineWord.zeros (Pos.to_nat (63 + 1))) = true.
+ Proof. 
+ split.
+ - intro H. unfold cap_is_unsealed, cap_is_sealed, CapFns.CapIsSealed, CapFns.Zeros, Operators_mwords.neq_vec, CapFns.CAP_VALUE_NUM_BITS, CapFns.CAP_VALUE_HI_BIT, CapFns.CAP_VALUE_LO_BIT in H. apply Is_true_true_1. simpl in H. 
+ rewrite negb_involutive in H. done. 
+ - intro H. unfold cap_is_unsealed, cap_is_sealed, CapFns.CapIsSealed, CapFns.Zeros, Operators_mwords.neq_vec. simpl. rewrite H. done.
+ Qed.
+
+(* End of Translation definitions. *)
+
  Lemma cap_invalidate_invalidates (c:t) : cap_is_valid (cap_invalidate c) = false.
  Proof.
  unfold cap_invalidate, cap_is_valid.
@@ -1218,31 +1361,6 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
  reflexivity.
  Qed.
 
- Lemma subrange_vec_dec_after_clear_tag (c:t) (hi lo : Z) :
- let c : mword 129 := c in
- (hi <? 128)%Z -> (lo <? hi)%Z ->
- subrange_vec_dec c hi lo = subrange_vec_dec (CapWithTagClear c) hi lo.
- Proof.
- intros x H J. 
- assert (Hp: (hi < 128)%Z); [ apply Is_true_eq_true in H; lia |].
- unfold subrange_vec_dec, CapWithTagClear, CapSetTag, CAP_TAG_BIT, autocast. 
- simpl. bv_simplify.
- destruct (Z.eq_dec _ _); [| reflexivity].
- unfold MachineWord.slice, MachineWord.zero_extend, MachineWord.N_to_word. simpl.
- change (Bit (vec_of_bits [access_vec_dec _ 0])) with B0.
- unfold update_vec_dec, update_mword_dec. simpl. 
- unfold MachineWord.set_bit, MachineWord.update_slice, MachineWord.slice. simpl.
- replace (bv_extract _ 0 _) with (bv_0 0); [| bv_simplify; bitblast].
- bv_simplify. 
- rewrite bv_zero_extend_idemp.
- change (bv_zero_extend _ _) with (bv_concat 129 (bv_0 1) (bv_extract 0 128 c)).
- replace (N.of_nat (Z.to_nat lo)) with (Z.to_N lo); [| rewrite Z_nat_N; reflexivity].
- replace (bv_extract _ _ (bv_concat _ _ _)) with (bv_extract (Z.to_N lo) (N.of_nat (Z.to_nat hi - Z.to_nat lo + 1)) (bv_extract 0 128 c)); [| bv_simplify; reflexivity].
- set (len := (N.of_nat (Z.to_nat hi - Z.to_nat lo + 1))).
- replace (bv_extract _ _ (bv_extract _ _ _)) with (bv_extract (Z.to_N lo) len c). reflexivity.
- bv_simplify. rewrite bv_extract_unsigned. rewrite bv_extract_unsigned. bv_simplify. bitblast. 
- Qed. 
-
  Lemma cap_get_set_value (c:t) (a:AddressValue.t) :
  cap_get_value (cap_set_value c a) = a.
  Proof.
@@ -1254,9 +1372,14 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
  bitblast.
  Qed. 
 
- (* Lemma cap_invalidate_preserves_bounds (c:t) : cap_get_bounds c = cap_get_bounds (cap_invalidate c).
+ Lemma cap_seal_preserves_value (c:t) (ot : ObjType.t) `{ArithFact ((bv_to_Z_unsigned ot >? 0)%Z && (bv_to_Z_unsigned ot <=? 4)%Z)} : 
+ cap_get_value c = cap_get_value (cap_seal_immediate c ot).
  Proof.
- Admitted. *)
+ unfold cap_seal_immediate, cap_get_value.
+ destruct (cap_is_valid c && cap_is_unsealed c).
+ { unfold_cap. bitblast. }
+ { fold (cap_get_value c). fold (cap_get_value (cap_invalidate (cap_set_objtype c ot))). rewrite <- cap_invalidate_preserves_value. unfold_cap. bitblast. }
+ Qed.
 
 End Capability.