From f8dd16550599f8c1205837ed7ad94f48a23974c7 Mon Sep 17 00:00:00 2001 From: gameboo Date: Tue, 28 Sep 2021 00:08:38 +0100 Subject: [PATCH] Can't cleanly use export mechanism at the moment apparently... + typo in comments --- CHERICap.bsv | 17 ++++------------- 1 file changed, 4 insertions(+), 13 deletions(-) diff --git a/CHERICap.bsv b/CHERICap.bsv index a52fe5b..287259c 100644 --- a/CHERICap.bsv +++ b/CHERICap.bsv @@ -29,16 +29,6 @@ package CHERICap; -export SoftPerms; -export HardPerms; -export Kind; -export BoundsInfo; -export Exact; -export SetBoundsReturn; -export showCHERICap; -export CHERICap :: *; -export Cast; - // CHERI capability types //////////////////////////////////////////////////////////////////////////////// @@ -208,6 +198,7 @@ typeclass CHERICap #( type t // capability in-memory architectural representation ////////////////////////////////////////////////////////////////////////////// // Note that the following rule is expected to hold: + // fromMem (toMem (cap)) == cap // fromMem (tuple2 (isValidCap (cap), {getMeta (cap), getAddr (cap)})) == cap // Get the in-memory architectural representation of the capability metadata @@ -246,9 +237,9 @@ typeclass CHERICap #( type t // capability architectural bounds queries ////////////////////////////////////////////////////////////////////////////// // Note that the following rules are expected to hold: - // getBase (cap) + getLength (cap) == getLength (cap) - // getRepBase (cap) + getRepLength (cap) == getRepLength (cap) - // isInRepBounds (cap) ==> isInRepBounds (cap) + // getBase (cap) + getLength (cap) == getTop (cap) + // getRepBase (cap) + getRepLength (cap) == getRepTop (cap) + // isInBounds (cap) ==> isInRepBounds (cap) // Get all architectural bound information for a capability function BoundsInfo#(n) getBoundsInfo (t cap);