From 1a0d412d80c2850a88e89eead85af59c99966871 Mon Sep 17 00:00:00 2001 From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com> Date: Wed, 4 Sep 2024 18:49:01 +0100 Subject: [PATCH] Simplified definition of `of_bvn` for capabilities --- coq-cheri-capabilities.opam | 2 +- theories/Morello/Capabilities.v | 13 +++---------- 2 files changed, 4 insertions(+), 11 deletions(-) diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam index 94872e2..efd8584 100644 --- a/coq-cheri-capabilities.opam +++ b/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: "20240611" +version: "20240904" bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues" depends: [ "dune" {>= "3.7"} diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index aca9b02..182bd94 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -649,15 +649,8 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou 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 + let tag_bv : (bv 1) := if tag then Z_to_bv 1 1 else Z_to_bv 1 0 in + Some (bv_concat len tag_bv b.(bvn_val)) else None. @@ -990,7 +983,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou Definition encode (isexact : bool) (c : t) : option ((list ascii) * bool) := let tag : bool := cap_is_valid c in - let c : (mword (Z.of_N len)) := c in (* why does Z.of_N len need to be specified? *) + 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 match mem_bytes_of_bits w with