- Introduced a lemmas module divided in properties of capabilities, t…

…ranslation of capability manipulations to bitvector operations, and low-level results on mwords. - Added utility definitions for Morello capabilities: -- functions for checking alignment, obtaining all aligned addresses from a cap, etc -- comparators for caps and for bounds
rems-project · Nov 8, 2024 · 521c4b0 · 521c4b0
1 parent 49acd7f
commit 521c4b0
Show file tree

Hide file tree

Showing 4 changed files with 310 additions and 5 deletions.
diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam
@@ -6,7 +6,7 @@ maintainer: ["[email protected]"]
 authors: ["Ricardo Almeida" "Vadim Zaliva"]
 license: "BSD-3-clause"
 homepage: "https://github.com/rems-project/coq-cheri-capabilities"
-version: "20241030"
+version: "1.10.0"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
   "dune" {>= "3.7" & <= "3.16.0"}

diff --git a/theories/Common/Utils.v b/theories/Common/Utils.v
@@ -319,3 +319,14 @@ Proof.
   rewrite H0 H1.
   apply string_eq_refl.
 Qed.
+
+Lemma Z_eqb_is_eq (x y : Z) :
+  (x =? y ↔ x = y)%Z.
+Proof.
+  split.
+  + intros.
+    apply Z.eqb_eq.
+    by apply Is_true_eq_true.
+  + intros ->.
+    by rewrite Z.eqb_refl.
+Qed.
diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v
@@ -6,10 +6,10 @@ Require Import Coq.Strings.HexString.
 From Coq.Structures Require Import OrderedType OrderedTypeEx.
 From Coq Require Import ssreflect.
 
-From stdpp Require Import bitvector bitblast bitvector_tactics.
-
 From SailStdpp Require Import Base Values Values_lemmas Operators_mwords MachineWord Operators_mwords MachineWordInterface.
 
+From stdpp Require Import bitvector bitblast bitvector_tactics list_numbers.
+
 From CheriCaps.Common Require Import Utils Addr Capabilities.
 From CheriCaps Require Import CapFns.
 From CheriCaps.Morello Require Import Bv_extensions.
@@ -820,6 +820,21 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
 
   Definition eqb (cap1:t) (cap2:t) : bool := eqb_cap cap1 cap2.
 
+  Definition leq_bounds (c1 c2 : t) : bool :=
+    let (base1,top1) := cap_get_bounds c1 in 
+    let (base2,top2) := cap_get_bounds c2 in 
+    ((base1.(bv_unsigned) =? base2.(bv_unsigned))%Z && (top1.(bv_unsigned) =? top2.(bv_unsigned))%Z) ||
+    (bounds_contained c1 c2 && (base1.(bv_unsigned) <=? (top1.(bv_unsigned)))%Z).
+
+  (* If both caps are tagged and sealed but otherwise different, then leq_cap is false in both directions.  *)
+  Definition leq_cap (c1 c2 : t) : bool :=
+    (eqb c1 c2) || 
+    (cap_is_invalid c1) || 
+      ((cap_is_valid c2) && 
+        (cap_is_unsealed c1 && cap_is_unsealed c2) && 
+        (leq_bounds c1 c2) && 
+        (leq_perms c1 c2)).
+
   Definition is_sentry (c:t) : bool :=
     match cap_get_seal c with
     | SealType.Cap_SEntry => true
@@ -839,6 +854,24 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     | SealType.Cap_Indirect_SEntry_Pair => Some SealType.Cap_Indirect_SEntry_Pair
     | _                                 => None 
     end.
+
+  Definition cap_aligned (b : Z) := (0 =? b `mod` 16)%Z.
+
+  Definition cap_align (b : Z) := (b - (b `mod` 16))%Z.
+
+  Definition cap_all_addresses (c : t) : list Z :=
+    let (base, limit) := cap_get_bounds c in
+    seqZ (cap_align (bv_unsigned base)) (bv_unsigned limit - cap_align (bv_unsigned base)).
+
+  Definition cap_aligned_addresses (c : t) :=
+    filter cap_aligned (cap_all_addresses c).
+
+  Definition cap_addresses (c : t) : list Z :=
+    let (base, limit) := cap_get_bounds c in
+    seqZ (bv_unsigned base) (bv_unsigned limit - bv_unsigned base).
+
+  Definition access_in_bounds (c : t) (a : bv 64) (sz : Z) :=
+    seqZ (bv_unsigned a) sz ⊆ cap_addresses c.    
 
   Definition flags_as_str (c:t): string :=
     let attrs : list string :=
@@ -989,7 +1022,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
     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].
+    case_match; [| 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. 
@@ -1419,7 +1452,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
         [ apply try_map_length in H_ascii as H_ascii;
           rewrite app_length rev_length H_bytes_len in H_ascii; simpl in H_ascii; lia |].
         assert (H_ascii_app: (∃ l4 last, l3 = l4 ++ [last])%list);
-        [ exists (removelast l3), (last l3 "000"%char); rewrite <- app_removelast_last; try done; 
+        [ exists (removelast l3), (List.last l3 "000"%char); rewrite <- app_removelast_last; try done; 
           intro H'; rewrite H' in H_ascii_len; simpl in H_ascii_len; lia |]. 
         destruct H_ascii_app as [l4 [last H_ascii_app]]. 
         subst. 

diff --git a/theories/Morello/Lemmas.v b/theories/Morello/Lemmas.v
@@ -0,0 +1,261 @@
+From SailStdpp Require Import Base Values Values_lemmas Operators_mwords MachineWord Operators_mwords MachineWordInterface.
+
+From stdpp Require Import list_numbers bitvector bitvector_tactics bitblast.
+
+From CheriCaps.Common Require Import Utils.
+From CheriCaps.Morello Require Import CapFns Bv_extensions Capabilities.
+
+(** More automation for modular arithmetics. *)
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
+
+Section mword_lemmas.
+  Open Scope Z.
+
+  Lemma mword_eq_vec_bv_unsigned n (x y : Values.mword n) :
+    (Operators_mwords.eq_vec x y) = (bv_unsigned (Values.get_word x) =? bv_unsigned (Values.get_word y))%Z.
+  Proof.
+    unfold Operators_mwords.eq_vec, MachineWord.MachineWord.eqb, MachineWord.MachineWord.eq_dec.
+    set (a := Values.get_word x). 
+    set (b := Values.get_word y).
+    destruct (base.decide (a = b)) as [e | e].
+    { apply bv_eq in e. by rewrite <- Z.eqb_eq in e. }
+    unfold not in e.
+    symmetry. apply not_true_is_false.
+    unfold not. intro H.   
+    apply e.
+    apply Z.eqb_eq in H. by apply bv_eq.
+  Qed.
+
+  Lemma mword_neq_vec_bv_unsigned n {x y : Values.mword n} :
+    (Operators_mwords.neq_vec x y) = negb (bv_unsigned (Values.get_word x) =? bv_unsigned (Values.get_word y))%Z.
+  Proof.
+    unfold Operators_mwords.neq_vec.
+    by rewrite mword_eq_vec_bv_unsigned.
+  Qed.
+
+  Lemma mwords_update_subrange_bv (c : (*Capability.t*) bv 129) hi lo (o : Values.mword (hi-(lo-1))) :
+    hi < 129 ->
+    hi >= lo ->
+    lo >= 0 ->
+    Operators_mwords.update_subrange_vec_dec (c : Values.mword 129) hi lo o
+    = bv_concat 129 
+        (bv_extract (Z.to_N (hi+1)) (129 - Z.to_N (hi+1)) c) 
+        (@bv_concat (Z.to_N (hi+1)) _ _ (mword_to_bv o) (bv_extract 0 (Z.to_N lo) c)).
+  Proof.
+    intros H_hi_max H_hi_min H_lo.
+    unfold Operators_mwords.update_subrange_vec_dec, MachineWord.MachineWord.update_slice, MachineWord.MachineWord.slice.
+    replace (N.of_nat (Z.to_nat lo + Z.to_nat (hi - (lo - 1)))) with (Z.to_N (hi + 1)); [| lia]. 
+    replace (N.of_nat (Z.to_nat 129 - Z.to_nat (hi - (lo - 1)) - Z.to_nat lo)) with (129 - Z.to_N (hi + 1))%N; [| lia].
+    replace (N.of_nat (Z.to_nat lo)) with (Z.to_N lo); [| lia].
+    reflexivity.
+  Qed.
+
+  Lemma mwords_objtype_update_subrange_bv (c : (*Capability.t*) bv 129) (o : bv 15) :
+    Operators_mwords.update_subrange_vec_dec (c : Values.mword 129) CapFns.CAP_OTYPE_HI_BIT CapFns.CAP_OTYPE_LO_BIT o
+    = bv_concat 129 (bv_extract 110 19 c) (bv_concat 110 o (bv_extract 0 95 c)).
+  Proof.
+    unfold CapFns.CAP_OTYPE_HI_BIT, CapFns.CAP_OTYPE_LO_BIT. rewrite mwords_update_subrange_bv; done.
+  Qed.
+
+  Lemma mwords_perms_update_subrange_bv (c : (*Capability.t*) bv 129) (p : bv 18) :
+    Operators_mwords.update_subrange_vec_dec (c : Values.mword 129) CapFns.CAP_PERMS_HI_BIT CapFns.CAP_PERMS_LO_BIT p 
+    = bv_concat 129 (bv_extract 128 1 c) (bv_concat 128 p (bv_extract 0 110 c)).
+  Proof. 
+    unfold CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT. rewrite mwords_update_subrange_bv; done.
+  Qed.
+
+  Lemma mwords_perms_subrange_bv (c : bv 18) : 
+    Operators_mwords.subrange_vec_dec (c : Values.mword 18) (CapFns.CAP_PERMS_NUM_BITS-1) 0 
+    = bv_extract 0 18 c.
+  Proof.  
+    unfold CapFns.CAP_PERMS_NUM_BITS, CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT. 
+    unfold Operators_mwords.subrange_vec_dec, MachineWord.MachineWord.slice. reflexivity.
+  Qed.
+
+  Lemma mwords_permsext_subrange_bv (c : bv 64) : 
+    Operators_mwords.subrange_vec_dec (c : Values.mword 64) (CapFns.CAP_PERMS_NUM_BITS-1) 0 
+    = bv_extract 0 18 c.
+  Proof.  
+    unfold CapFns.CAP_PERMS_NUM_BITS, CapFns.CAP_PERMS_HI_BIT, CapFns.CAP_PERMS_LO_BIT. 
+    unfold Operators_mwords.subrange_vec_dec, MachineWord.MachineWord.slice. reflexivity.
+  Qed.
+
+End mword_lemmas.
+
+Section Cap_translation_lemmas.
+
+  Lemma cap_permits_store_bv_and (c:Capability.t) : 
+    Capability.cap_permits_store c →  
+    bv_and c (BV 129 (2^126)) = BV 129 (2^126).
+  Proof. 
+    Capability.unfold_cap. unfold Capability.t, Capability.len in c.
+    intro H. case_decide; [| done ]. repeat bv_simplify.    
+    apply bv_eq_wrap in H0. bv_simplify H0. 
+    change (N.of_nat (Z.to_nat (127 - 110 + 1 - 1 - 0 + 1))) with 18%N in H0. replace (bv_wrap 18
+    (Z.land
+       (bv_wrap 18
+          (@bv_unsigned 64
+             (@bv_zero_extend (N.of_nat (Z.to_nat 18)) 64 (@bv_extract 129 110 18 c))))
+       (bv_wrap 18 (1 ≪ 16)))) with (bv_wrap 18 (Z.land (bv_wrap 18 (@bv_unsigned 129 c ≫ Z.of_N 110)) (bv_wrap 18 (1 ≪ 16)))) in H0.
+    2:{ change (Z.of_N 110) with 110%Z. 
+        change (N.of_nat (Z.to_nat 18)) with 18%N. 
+        bv_simp_r. 
+        replace (bv_wrap 18 (@bv_unsigned 18 (@bv_extract 129 110 18 c))) with (bv_wrap 18 (bv_unsigned c ≫ 110)).
+        2:{ bv_simp_r. bitblast. }
+    bitblast. } 
+    rewrite <- (@Z.mul_cancel_r _ _ (2^110) ) in H0; [| lia].
+    rewrite <- (@Z.shiftl_mul_pow2 _ 110) in H0; [| lia].
+    rewrite <- (@Z.shiftl_mul_pow2 _ 110) in H0; [| lia].  
+    bitblast as m.
+    bitblast H0 with m as H1.
+    exact H1.
+  Qed.
+
+  Lemma cap_permits_load_bv_and (c:Capability.t) : 
+    Capability.cap_permits_load c -> 
+    bv_and c (BV 129 (2^127)) = BV 129 (2^127).
+  Proof. 
+    Capability.unfold_cap. unfold Capability.t, Capability.len in c.
+    intro H. case_decide; [| done ]. bv_simp_r.   
+    apply bv_eq_wrap in H0. bv_simplify H0. 
+    change (N.of_nat (Z.to_nat (127 - 110 + 1 - 1 - 0 + 1))) with 18%N in H0.
+    rewrite <- (@Z.mul_cancel_r _ _ (2^110) ) in H0; [| lia].
+    rewrite <- (@Z.shiftl_mul_pow2 _ 110) in H0; [| lia].
+    rewrite <- (@Z.shiftl_mul_pow2 _ 110) in H0; [| lia].  
+    bitblast as m. 
+    bitblast H0 with m as H1.
+    rewrite <- H1. change (N.of_nat (Z.to_nat 18)) with 18%N.
+    bv_simp_r. 
+    bitblast.
+  Qed.
+
+  Lemma cap_is_unsealed_eq_vec (c : Capability.t ): 
+    Capability.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 Capability.cap_is_unsealed, Capability.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 Capability.cap_is_unsealed, Capability.cap_is_sealed, CapFns.CapIsSealed, CapFns.Zeros, Operators_mwords.neq_vec. simpl. rewrite H. done.
+  Qed.
+
+End Cap_translation_lemmas.
+
+Section Cap_properties.
+
+  Lemma perm_leq_executable c c':
+    Capability.leq_perms c c' ->
+    Capability.cap_permits_execute c ->
+    Capability.cap_permits_execute c'.
+  Proof.
+    intros Hleq Hc.
+    unfold Capability.leq_perms in Hleq.
+    destruct (Capability.cap_permits_execute c), (Capability.cap_permits_execute c'); [ done | | done | done].
+    + simpl in Hleq. by rewrite !Tauto.if_same in Hleq.
+  Qed.
+
+  Lemma perm_leq_unseal c c':
+    Capability.leq_perms c c' ->
+    Capability.cap_permits_unseal c ->
+    Capability.cap_permits_unseal c'.
+  Proof.
+    intros Hleq Hc.
+    unfold Capability.leq_perms in Hleq.
+    destruct (Capability.cap_permits_unseal c), (Capability.cap_permits_unseal c'); [ done | | done | done].
+    + simpl in Hleq. by rewrite !Tauto.if_same in Hleq.
+  Qed.
+
+  Lemma perm_leq_read c c':
+    Capability.leq_perms c c' ->
+    Capability.cap_permits_load c ->
+    Capability.cap_permits_load c'.
+  Proof.
+    intros Hleq Hc.
+    unfold Capability.leq_perms in Hleq.
+    destruct (Capability.cap_permits_load c), (Capability.cap_permits_load c'); [ done | | done | done].
+    + simpl in Hleq. by rewrite !Tauto.if_same in Hleq.
+  Qed.
+
+  Lemma perm_leq_write c c':
+    Capability.leq_perms c c' ->
+    Capability.cap_permits_store c ->
+    Capability.cap_permits_store c'.
+  Proof.
+    intros Hleq Hc.
+    unfold Capability.leq_perms in Hleq.
+    destruct (Capability.cap_permits_store c), (Capability.cap_permits_store c'); [ done | | done | done].
+    + simpl in Hleq. by rewrite !Tauto.if_same in Hleq.
+  Qed.
+
+  Lemma leq_bounds_spec {c c' b1 b2 b3 b4} :
+    Capability.leq_bounds c' c ->
+    Capability.cap_get_bounds c = (b1, b2) ->
+    Capability.cap_get_bounds c' = (b3, b4) ->
+    (bv_unsigned b1 ≤ bv_unsigned b3)%Z ∧
+    (bv_unsigned b4 ≤ bv_unsigned b2)%Z.
+  Proof.
+    intros Hbounds Hc Hc'.
+    unfold Capability.leq_bounds in Hbounds.
+    rewrite Hc, Hc' in Hbounds.
+    destruct (orb_prop_elim _ _ Hbounds) as [Hbounds' | Hbounds'].
+    + destruct (andb_prop_elim _ _ Hbounds') as [Heq Heq'].
+      rewrite !Z_eqb_is_eq in Heq, Heq'.
+      lia.
+    + destruct (andb_prop_elim _ _ Hbounds') as [Heq _].
+      unfold Capability.bounds_contained, Capabilities.Bounds.contained in Heq.
+      rewrite Hc, Hc' in Heq.
+      destruct (andb_prop_elim _ _ Heq) as [Heq' Heq''].
+      unfold geb, gtb, leb, ltb in Heq', Heq''.
+      split.
+      - apply orb_prop_elim in Heq'. destruct Heq' as [Heq' | Heq'].
+        { apply Is_true_true_1, Z.ltb_lt in Heq'. lia. }
+        apply Is_true_eq_true in Heq'.
+        apply bv_eqb_eq in Heq'. apply bv_eq in Heq'. 
+        lia.
+      - apply orb_prop_elim in Heq''. destruct Heq'' as [Heq'' | Heq'']; apply Is_true_eq_true in Heq''.
+        { rewrite Z.ltb_lt in Heq''. lia. }
+        rewrite bv_eqb_eq in Heq''. apply bv_eq in Heq''. lia.
+  Qed.
+
+  Lemma leq_bounds_to_cap_aligned_addresses_subset c c' a:
+    Capability.leq_bounds c' c ->
+    a ∈ Capability.cap_aligned_addresses c' ->
+    a ∈ Capability.cap_aligned_addresses c.
+  Proof.
+    intros Hbounds Hc'.
+    unfold Capability.cap_aligned_addresses, Capability.cap_all_addresses in *.
+    destruct (Capability.cap_get_bounds c) as [b1 b2] eqn:H1, (Capability.cap_get_bounds c') as [b3 b4] eqn:H2.
+    destruct (leq_bounds_spec Hbounds H1 H2) as [Hb1 Hb2].
+    rewrite !elem_of_list_filter in Hc'. rewrite !elem_of_list_filter.
+    destruct Hc' as [? Hc'].
+    split; [assumption| ].
+    rewrite !elem_of_seqZ in *.
+    assert (Capability.cap_align (bv_unsigned b1) ≤ Capability.cap_align (bv_unsigned b3))%Z as Halign.
+    { unfold Capability.cap_align. lia. }
+    lia.
+  Qed.
+
+  Lemma leq_bounds_to_cap_addresses_subset c c' a:
+    Capability.leq_bounds c' c ->
+    a ∈ Capability.cap_addresses c' ->
+    a ∈ Capability.cap_addresses c.
+  Proof.  
+    intros Hbounds Hc'.
+    unfold Capability.cap_addresses in *.
+    destruct (Capability.cap_get_bounds c) as [b1 b2] eqn:H1, (Capability.cap_get_bounds c') as [b3 b4] eqn:H2.
+    destruct (leq_bounds_spec Hbounds H1 H2) as [Hb1 Hb2].
+    rewrite !elem_of_seqZ in *.
+    assert (Capability.cap_align (bv_unsigned b1) ≤ Capability.cap_align (bv_unsigned b3))%Z as Halign.
+    { unfold Capability.cap_align. lia. }
+    lia.
+  Qed.
+
+  Lemma equal_bounds_to_equal_cap_aligned_addresses c c':
+    Capability.cap_get_bounds c = Capability.cap_get_bounds c' ->
+    Capability.cap_aligned_addresses c = Capability.cap_aligned_addresses c'.
+  Proof.
+    intros Hbounds.
+    unfold Capability.cap_aligned_addresses, Capability.cap_all_addresses.
+    by rewrite Hbounds.
+  Qed.
+
+End Cap_properties.