- Added lemma subrange_vec_dec_after_clear_tag with proof

- Fixed bug in perm_clear_global and added test

theories/Morello/Capabilities.v

@@ -630,9 +630,9 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
  let new_cap := CapClearPerms c mask_inv in 
  if (cap_is_sealed c) then (cap_invalidate new_cap) else new_cap.
 
- Definition cap_clear_global_perm (cap:t) : t := 
- cap_narrow_perms cap ((Permissions.make_permissions [Permissions.Global_perm])).
-
+ Definition cap_clear_global_perm (cap:t) : t :=  
+ cap_narrow_perms cap (Permissions.perm_clear_global (cap_get_perms cap)).
+ 
  Definition cap_set_bounds (c : t) (bounds : Bounds.t) (exact : bool) : t :=
  (* CapSetBounds sets the lower bound to the value of the input cap,
  so we first have to set the value of cap to bounds.base. *)
@@ -1041,7 +1041,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
  unfold CapGetTag, CapSetTag, CAP_TAG_BIT. 
  change (Bit (vec_of_bits [access_vec_dec _ 0])) with B0. 
  unfold update_vec_dec, access_vec_dec, access_mword_dec.
- simpl (get_word _).
+ simpl (get_word _). 
  unfold MachineWord.set_bit, MachineWord.get_bit, MachineWord.update_slice, MachineWord.slice, MachineWord.zero_extend.
  bv_simplify.
  bitblast.
@@ -1078,12 +1078,33 @@ 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_invalidate_preserves_bounds (c:t) : cap_get_bounds c = cap_get_bounds (cap_invalidate c).
  Proof.
- unfold cap_get_bounds, cap_get_bounds_, cap_invalidate.
- assert (H: CapGetBounds c = CapGetBounds (CapWithTagClear c)).
- { unfold CapGetBounds. destruct (CapGetExponent c =? CAP_MAX_ENCODEABLE_EXPONENT)%Z eqn:P.
- - simpl. 
  Admitted.
 
 End Capability. 

theories/Morello/MorelloTests.v

@@ -40,6 +40,7 @@ Module test_cap_getters_and_setters.
  Definition c6:Capability.t := Capability.of_Z 0x1fb0000007a4700000000000000003333. (* Cap breakdown: https://www.morello-project.org/capinfo?c=0x1%3Afb0000007a470000%3A0000000000003333 *)
  Definition c7:Capability.t := Capability.of_Z 0x14C0000007F1CFF1500000000FFFFFF15.
  Definition c8:Capability.t := Capability.of_Z 0x1900000007f1cff1500000000ffffff15.
+ Definition c9:Capability.t := Capability.of_Z 0x1ffffb000000000000000000000000000. (* Cap breakdown: https://www.morello-project.org/capinfo?c=0x1ffffb000000000000000000000000000 *)
 
  Program Definition flags1:Flags.t := exist _ [false; false; false; false; false; false; false; false] _. 
  Next Obligation. reflexivity. Defined.
@@ -119,11 +120,15 @@ Module test_cap_getters_and_setters.
  let perms := perm_clear_user3 perms in 
  let perms := perm_clear_user2 perms in 
  let perms := perm_clear_user1 perms in 
- let perms := Permissions.of_list ((Permissions.to_list perms)) in
- let capB := (cap_narrow_perms c1 (match perms with Some p => p | None => Permissions.perm_Universal end)) in
+ let capB := (cap_narrow_perms c1 perms) in
  capA = capB.
  Proof. vm_compute. reflexivity. Qed.
 
+ Example permissions_test_6 : 
+ let perms := perm_clear_global (cap_get_perms c1) in 
+ perms = cap_get_perms c9 /\ perms ≠ cap_get_perms c1.
+ Proof. vm_compute. split. bv_solve. discriminate. Qed. 
+
  Example get_and_user_perms_test_1 : 
  let user_perms_A : (list bool) := get_user_perms (cap_get_perms (cap_cU ())) in 
  let user_perms_A := [ nth 0 user_perms_A false; negb (nth 1 user_perms_A false);