Re-enabled Cap.of_bvn (and added test)

theories/Morello/Capabilities.v

@@ -524,6 +524,20 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
   Definition t := bv len.
 
   Definition of_Z (z:Z) : t := Z_to_bv len z.
+
+  Definition of_bvn (b:bvn) (tag:bool) : option t := 
+    if (b.(bvn_n) =? (len-1))%N then 
+      let bits : (list bool) := tag::(bools_of_int (Z.of_N len-1) b.(bvn_val).(bv_unsigned)) in
+      let bitsu := List.map bitU_of_bool bits in
+      let w : (mword _) := vec_of_bits bitsu in
+      let z : Z := int_of_mword false w in 
+      let c : option t := Z_to_bv_checked len z in 
+      match c with 
+        Some c => Some c
+      | None   => None
+      end
+    else 
+      None.
 
   Definition cap_SEAL_TYPE_UNSEALED : ObjType.t := ObjType.of_Z 0.
   Definition cap_SEAL_TYPE_RB : ObjType.t := ObjType.of_Z 1. 
@@ -907,20 +921,6 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou
             -- unfold bitsu. unfold length_list. rewrite map_length. rewrite R. reflexivity.
     Defined. *)  
 
-  (* Definition of_bvn (b:bvn) (tag:bool) : option t := 
-    if (b.(bvn_n) =? (len-1))%N then 
-      let bits : (list bool) := tag::(bools_of_int (Z.of_N len-1) b.(bvn_val).(bv_unsigned)) in
-      let bitsu := List.map bitU_of_bool bits in
-      let w : (mword _) := vec_of_bits bitsu in
-      let z : Z := mword_to_Z_unsigned w in 
-      let c : option t := Z_to_bv_checked len z in 
-      match c with 
-        Some c => Some c
-      | None   => None
-      end
-    else 
-      None. *)
-
   Definition eqb_cap (cap1:t) (cap2:t) : bool := cap1 =? cap2.
 
   Definition eqb (cap1:t) (cap2:t) : bool := eqb_cap cap1 cap2.

theories/Morello/MorelloTests.v

@@ -50,6 +50,12 @@ Module test_cap_getters_and_setters.
   Definition perm_Load_Store : Permissions.t := Permissions.make_permissions [Permissions.Load_perm; Permissions.Store_perm].
   Definition perm_Load_Execute : Permissions.t := Permissions.make_permissions [Permissions.Load_perm; Permissions.Execute_perm].
 
+  Example of_bvn_test_1 : 
+    let drop_tag c : mword 128 := of_bools (List.tail (List.rev (bv_to_bits c))) in
+    let drop_tag_bvn c := bv_to_bvn (drop_tag c) in
+    of_bvn (drop_tag_bvn c1) true = Some c1 /\ of_bvn (drop_tag_bvn c2) true = Some c2 /\ of_bvn (drop_tag_bvn c3) true = Some c3 /\ of_bvn (drop_tag_bvn c4) true = Some c4 /\ of_bvn (drop_tag_bvn c5) true = Some c5 /\ of_bvn (drop_tag_bvn c6) true = Some c6 /\ of_bvn (drop_tag_bvn c7) true = Some c7 /\ of_bvn (drop_tag_bvn c8) true = Some c8.
+  Proof. repeat (try split; try vm_compute; try (apply f_equal); try bv_solve). Qed.
+
   Example is_valid_test_1 : cap_is_valid c1 = true.
     Proof. reflexivity. Qed.