- Added comment about mask bits in cap_narrow_perms vs CLRPERM

- Test about Permissions.to_Z/of_Z
- Code simplifications

theories/Common/Capabilities.v

@@ -219,7 +219,7 @@ Module Type CAPABILITY
       The input permissions should be the ones to be kept.
         Related instructions:
         - CAndPerm in RISC V
-        - CLRPERM in Morello
+        - In Morello, CLRPERM c mask = cap_narrow_perms c ~mask
    *)
   Parameter cap_narrow_perms: t -> P.t -> t.
 

theories/Morello/Capabilities.v

@@ -375,7 +375,9 @@ Module Permissions <: PERMISSIONS.
   Definition to_string_hex (perms:t) : string :=      
     HexString.of_Z (bv_to_Z_unsigned perms). 
 
-  Definition to_raw (perms:t) : Z := bv_to_Z_unsigned perms.
+  Definition to_raw (perms:t) : Z := to_Z perms.
+
+  Definition of_raw (z:Z) : t := of_Z z.
 
   Definition of_list (l : list bool) : option t := 
     if ((List.length l) <? (N.to_nat len))%nat then
@@ -1002,9 +1004,8 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
   Definition encode (c : t) : option ((list ascii) * bool) :=
     let tag : bool := cap_is_valid c in 
     let c : (mword (Z.of_N len)) := c in  
-    let c : (mword (Z.of_N len)) := c in
     let cap_bits := bits_of c in 
-    let w : (mword _) := vec_of_bits (List.tail cap_bits) in
+    let w := vec_of_bits (List.tail cap_bits) in
     match mem_bytes_of_bits w with
     | Some bytes =>
         match try_map memory_byte_to_ascii bytes with
@@ -1019,7 +1020,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
       let bytes := List.rev bytes in (* TODO: bypassing rev could make this more efficient *)
       let bits : (list bool) := tag::(bool_bits_of_bytes bytes) in
       let bitsu := List.map bitU_of_bool bits in
-      let w : (mword _) := vec_of_bits bitsu in
+      let w := vec_of_bits bitsu in
       (* Some (mword_to_bv w) *) (* This requires the proof below, but makes tests harder *)
       let z : Z := uint w in 
       let c : option t := Z_to_bv_checked len z in 

theories/Morello/MorelloTests.v

@@ -1,4 +1,3 @@
-Require Export Morello.Capabilities.
 Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Lists.List.
 Require Import Coq.Strings.String.
@@ -8,9 +7,10 @@ Require Import Coq.Strings.HexString.
 From stdpp.unstable Require Import bitvector bitvector_tactics. 
 From stdpp Require Import bitvector.
 From SailStdpp Require Import Values Operators_mwords.
-Require Import CapFns.
 
 From CheriCaps.Common Require Import Utils Addr Capabilities.
+From CheriCaps.Morello Require Import CapFns.
+From CheriCaps.Morello Require Export Capabilities.
 
 Module test_cap_getters_and_setters.
 
@@ -113,6 +113,10 @@ Module test_cap_getters_and_setters.
     perms = cap_get_perms c9 /\ perms ≠ cap_get_perms c1.
     Proof. vm_compute. split. bv_solve. discriminate. Qed.    
 
+  Example permissions_test_7 : 
+    Permissions.of_Z (Permissions.to_Z perm_Load_Store) = perm_Load_Store.
+    Proof. reflexivity. 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);