cheri_cap_common.sail

/*=======================================================================================*/
/*  CHERI RISCV Sail Model                                                               */
/*                                                                                       */
/*  This CHERI Sail RISC-V architecture model here, comprising all files and             */
/*  directories except for the snapshots of the Lem and Sail libraries in the            */
/*  prover_snapshots directory (which include copies of their licenses), is subject      */
/*  to the BSD two-clause licence below.                                                 */
/*                                                                                       */
/*  Copyright (c) 2017-2021                                                              */
/*    Alasdair Armstrong                                                                 */
/*    Thomas Bauereiss                                                                   */
/*    Brian Campbell                                                                     */
/*    Jessica Clarke                                                                     */
/*    Nathaniel Wesley Filardo (contributions prior to July 2020, thereafter Microsoft)  */
/*    Alexandre Joannou                                                                  */
/*    Microsoft                                                                          */
/*    Prashanth Mundkur                                                                  */
/*    Robert Norton-Wright (contributions prior to March 2020, thereafter Microsoft)     */
/*    Alexander Richardson                                                               */
/*    Peter Rugg                                                                         */
/*    Peter Sewell                                                                       */
/*                                                                                       */
/*  All rights reserved.                                                                 */
/*                                                                                       */
/*  This software was developed by SRI International and the University of               */
/*  Cambridge Computer Laboratory (Department of Computer Science and                    */
/*  Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and                 */
/*  under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA                 */
/*  SSITH research programme.                                                            */
/*                                                                                       */
/*  This software was developed within the Rigorous Engineering of                       */
/*  Mainstream Systems (REMS) project, partly funded by EPSRC grant                      */
/*  EP/K008528/1, at the Universities of Cambridge and Edinburgh.                        */
/*                                                                                       */
/*  This project has received funding from the European Research Council                 */
/*  (ERC) under the European Union’s Horizon 2020 research and innovation                */
/*  programme (grant agreement 789108, ELVER).                                           */
/*                                                                                       */
/*  Redistribution and use in source and binary forms, with or without                   */
/*  modification, are permitted provided that the following conditions                   */
/*  are met:                                                                             */
/*  1. Redistributions of source code must retain the above copyright                    */
/*     notice, this list of conditions and the following disclaimer.                     */
/*  2. Redistributions in binary form must reproduce the above copyright                 */
/*     notice, this list of conditions and the following disclaimer in                   */
/*     the documentation and/or other materials provided with the                        */
/*     distribution.                                                                     */
/*                                                                                       */
/*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''                   */
/*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED                    */
/*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A                      */
/*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR                  */
/*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,                         */
/*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT                     */
/*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF                     */
/*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND                  */
/*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,                   */
/*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT                   */
/*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF                   */
/*  SUCH DAMAGE.                                                                         */
/*=======================================================================================*/

/* width of capability in bytes (excluding tag) */
type cap_size : Int = 8
let  cap_size = sizeof(cap_size)
type log2_cap_size : Int = 3
let  log2_cap_size = sizeof(log2_cap_size)
type CapBits = bits(8 * cap_size)
/*! Width of compressed perms field in bits */
type cap_cperms_width : Int = 6

/*! Width of architectural otype field in bits */
type cap_otype_width : Int = 4
let  cap_otype_width = sizeof(cap_otype_width)
/*! Width of compressed otype field in bits */
type cap_cotype_width : Int = 3
/*! Width of M field in bits */
type cap_cM_width : Int = 8
let  cap_cM_width = sizeof(cap_cM_width)
/*! Width of B field in bits */
type cap_B_width : Int = cap_cM_width + 1
let  cap_B_width = sizeof(cap_B_width)
/*! Width of expanded exponent field in bits */
type cap_E_width : Int = 5
let  cap_E_width = sizeof(cap_E_width)
type cap_addr_width : Int = xlen
let  cap_addr_width = sizeof(cap_addr_width)
/*! Cap length width is one larger than address space width in order to 
 represent maximum top / length of 2**xlen. */
type cap_len_width : Int = cap_addr_width + 1
let  cap_len_width = sizeof(cap_len_width)

/*!
 * There is one revocation bit for every 8 bytes.
 */
type log2_revocation_granule_size : Int = 3
let  log2_revocation_granule_size = sizeof(log2_revocation_granule_size)

/*! THIS represents capabilities as stored in memory. */
struct EncCapability = {
  reserved   : bits(1),
  cperms     : bits(cap_cperms_width),
  cotype     : bits(cap_cotype_width),
  E          : bits(cap_E_width),
  cM         : bits(cap_cM_width),
  B          : bits(cap_B_width),
  address    : bits(cap_addr_width)
}

function capBitsToEncCapability(c) : CapBits -> EncCapability = struct {
  reserved   = c[63..63],
  cperms     = c[62..57],
  cotype     = c[56..54],
  E          = c[53..49],
  cM         = c[48..41],
  B          = c[40..32],
  address    = c[31..0]
}

function encCapToBits(cap) : EncCapability -> CapBits =
  cap.reserved @
  cap.cperms @
  cap.cotype @
  cap.E @
  cap.cM @
  cap.B @
  cap.address

let cap_max_addr = MAX(cap_addr_width)
let cap_max_otype = MAX(cap_otype_width)

/*! Width of the architectural perms returned by CGetPerms. */
type cap_perms_width : Int = 12
let  cap_perms_width = sizeof(cap_perms_width)

type CapAddrBits  = bits(cap_addr_width)
type CapAddrInt   = range(0, (2 ^ cap_addr_width) - 1)
type CapLenBits   = bits(cap_len_width)
type CapLen       = range(0, (2 ^ cap_len_width) - 1)
type CapPermsBits = bits(cap_perms_width)

/*! Exponent chosen to permit representing the entire address space. */
type cap_max_E : Int = 24
let cap_max_E = sizeof(cap_max_E)
let cap_max_E_bits = to_bits(cap_E_width, sizeof(cap_max_E))
/* Value for M field that represents max value of top (2**32) when used with cap_max_E. */
let cap_reset_M = 0b1 @ zeros(cap_cM_width)

/*!
 * THIS represents a partially decompressed capability. The
 * permissions, E and otype are expanded from their compressed format by
 * [encCapabilityToCapability] and compressed by [capToEncCap].
 */
struct Capability = {
  tag                    : bool,
  perm_user0             : bool,
  permit_seal            : bool,
  permit_unseal          : bool,
  permit_execute         : bool,
  access_system_regs     : bool,
  permit_load_store_cap  : bool,
  permit_load            : bool,
  permit_store_local_cap : bool,
  permit_load_mutable    : bool,
  permit_store           : bool,
  permit_load_global     : bool,
  global                 : bool,
  reserved               : bits(1),
  E                      : bits(cap_E_width),
  B                      : bits(cap_B_width),
  M                      : bits(cap_B_width),
  otype                  : bits(cap_otype_width),
  address                : bits(cap_addr_width)
}

/* The null capability is defined as all zeros, with tag unset. */
let null_cap : Capability = struct {
  tag                    = false,
  perm_user0             = false,
  permit_seal            = false,
  permit_unseal          = false,
  permit_execute         = false,
  access_system_regs     = false,
  permit_load_store_cap  = false,
  permit_load            = false,
  permit_store_local_cap = false,
  permit_load_mutable    = false,
  permit_store           = false,
  permit_load_global     = false,
  global                 = false,
  reserved               = zeros(),
  E                      = zeros(),
  B                      = zeros(),
  M                      = zeros(),
  otype                  = to_bits(cap_otype_width, otype_unsealed),
  address                = zeros()
}

/* A capability from which to derive the root caps. E and M are set such that
  the bounds decode to the entire address space, and tag and global are set.
  These things are are common to all root caps. For convenience it is derived 
  from null_cap. */
let max_bounds_cap : Capability = {
  null_cap with
  E                      = cap_max_E_bits,
  M                      = cap_reset_M,
  tag                    = true,
  global                 = true
}

/* The capability root for executable format capabilities. */
let root_cap_exe : Capability = {
  max_bounds_cap with
  permit_execute         = true,
  access_system_regs     = true,
  permit_load_store_cap  = true,
  permit_load            = true,
  permit_load_mutable    = true,
  permit_load_global     = true
}

/* The capability root for memory format capabilities. */
let root_cap_mem : Capability = {
  max_bounds_cap with
  permit_load_store_cap  = true,
  permit_load            = true,
  permit_store_local_cap = true,
  permit_load_mutable    = true,
  permit_store           = true,
  permit_load_global     = true
}

/* The capability root for sealing format capabilities. */
let root_cap_seal : Capability = {
  max_bounds_cap with
  perm_user0             = true,
  permit_seal            = true,
  permit_unseal          = true
}

/*! Partially decompress a capability from bits to a [Capability] struct.
  Permissions, otype and exponent are decompressed, but the bounds are left
  in the form of B and M fields. */
function encCapabilityToCapability(t,c) : (bool, EncCapability) -> Capability = {
  var perm_user0             : bool = false;
  var permit_seal            : bool = false;
  var permit_unseal          : bool = false;
  var permit_execute         : bool = false;
  var access_system_regs     : bool = false;
  var permit_load_store_cap  : bool = false;
  var permit_load            : bool = false;
  var permit_store_local_cap : bool = false;
  var permit_load_mutable    : bool = false;
  var permit_store           : bool = false;
  var permit_load_global     : bool = false;
  var global                 : bool = bit_to_bool(c.cperms[5]);
  var isExe : bool = false;
  match c.cperms[4..0] {
    0b11 @ [SL, LM, LG] => {
      /* mem-rw-cap format */
      permit_load = true;
      permit_load_store_cap = true;
      permit_store = true;
      permit_store_local_cap = bit_to_bool(SL);
      permit_load_mutable = bit_to_bool(LM);
      permit_load_global = bit_to_bool(LG);
    },
    0b101 @ [LM, LG] => {
      /* mem-ro-cap format */
      permit_load = true;
      permit_load_store_cap = true;
      permit_load_mutable = bit_to_bool(LM);
      permit_load_global = bit_to_bool(LG);
    },
    0b10000 => {
      /* mem-wo-cap */
      permit_store = true;
      permit_load_store_cap = true;
    },
    0b100 @ [LD, SD] => {
      /* mem-data */
      permit_load = bit_to_bool(LD);
      permit_store = bit_to_bool(SD);
    },
    0b01 @ [SR, LM, LG] => {
      /* Executable format */
      isExe = true;
      permit_execute = true;
      permit_load = true;
      permit_load_store_cap = true;
      access_system_regs  = bit_to_bool(SR);
      permit_load_mutable = bit_to_bool(LM);
      permit_load_global  = bit_to_bool(LG);
    },
    0b00 @ [U0, SE, US] => {
      /* Sealing format */
      perm_user0    = bit_to_bool(U0);
      permit_seal   = bit_to_bool(SE);
      permit_unseal = bit_to_bool(US);
    }
  };
  /* The otype of executable caps is mapped to 1-7 and others to 9-15. Unsealed
    is always 0. */
  let otype = (if isExe | c.cotype == 0b000 then 0b0 else 0b1) @ c.cotype;
  /* The 4-bit exponent is expanded to 5 bits, using 0xf to encode a cap_max_E
    value that enables representing the entire address space. */

  let E = if c.E == ones(cap_E_width) then zeros(cap_E_width) else c.E;
  let M = (if c.E == ones(cap_E_width) then 0b0 else 0b1) @ c.cM;

  return struct {
    tag                    = t,
    perm_user0             = perm_user0            ,
    permit_seal            = permit_seal           ,
    permit_unseal          = permit_unseal         ,
    permit_execute         = permit_execute        ,
    access_system_regs     = access_system_regs    ,
    permit_load_store_cap  = permit_load_store_cap ,
    permit_load            = permit_load           ,
    permit_store_local_cap = permit_store_local_cap,
    permit_load_mutable    = permit_load_mutable   ,
    permit_store           = permit_store          ,
    permit_load_global     = permit_load_global    ,
    global                 = global                ,
    reserved               = c.reserved,
    E                      = E,
    B                      = c.B,
    M                      = M,
    otype                  = otype,
    address                = c.address
  }
}

function capBitsToCapability(t, c) : (bool, CapBits) -> Capability = encCapabilityToCapability(t, capBitsToEncCapability(c))

/*!
 * Compress a [Capability] back to the bits representation. This is simply
 * the reverse of [encCapabilityToCapability], although it relies on the fields
 * having valid values. For the otype we rely on the fact that sealed
 * capabilities cannot be modified and unsealed is always encoded as zero. It
 * is mildy surprsing that [CAndPerm] on a sealed capability may result in a
 * untagged capability with a different otype, but otypes have no significance
 * on untagged capabilities anyway.
 */
function capToEncCap(cap) : Capability -> EncCapability = {
  var cperms : bits(cap_cperms_width) = zeros();
  cperms[5] = bool_to_bit(cap.global);
  if cap.permit_execute & cap.permit_load & cap.permit_load_store_cap then {
    /* Executable format */
    cperms[4..3] = 0b01;
    cperms[2] = bool_to_bit(cap.access_system_regs);
    cperms[1] = bool_to_bit(cap.permit_load_mutable);
    cperms[0] = bool_to_bit(cap.permit_load_global);
  } else if cap.permit_load & cap.permit_load_store_cap & cap.permit_store then {
    /* mem cap-rw */
    cperms[4..3] = 0b11;
    cperms[2] = bool_to_bit(cap.permit_store_local_cap);
    cperms[1] = bool_to_bit(cap.permit_load_mutable);
    cperms[0] = bool_to_bit(cap.permit_load_global);
  } else if cap.permit_load & cap.permit_load_store_cap then {
    /* mem cap-ro */
    cperms[4..2] = 0b101;
    cperms[1] = bool_to_bit(cap.permit_load_mutable);
    cperms[0] = bool_to_bit(cap.permit_load_global);
  } else if cap.permit_store & cap.permit_load_store_cap then {
    /* mem cap-wo */
    cperms[4..0] = 0b10000;
  } else if cap.permit_load | cap.permit_store then {
    /* mem rw data */
    cperms[4..2] = 0b100;
    cperms[1] = bool_to_bit(cap.permit_load);
    cperms[0] = bool_to_bit(cap.permit_store);
  } else {
    /* Sealing format */
    cperms[4..3] = 0b00;
    cperms[2] = bool_to_bit(cap.perm_user0);
    cperms[1] = bool_to_bit(cap.permit_seal);
    cperms[0] = bool_to_bit(cap.permit_unseal);
  };
  return struct {
    cperms = cperms,
    reserved = cap.reserved,
    cotype = cap.otype[2..0], /* truncate otype when compressing */
    E = if cap.E == zeros(cap_E_width) & cap.M[cap_cM_width..cap_cM_width] == 0b0 then ones(cap_E_width) else cap.E,
    cM = truncate(cap.M, cap_cM_width),
    B = cap.B,
    address = cap.address
  };
}

/*! Convert from capability struct to bits (no tag) */
function capToBits(cap) : Capability -> CapBits = encCapToBits(capToEncCap(cap))

let null_cap_bits : CapBits = capToBits(null_cap)

/*!
 * Returns the decoded base and top of the given Capability.
 */
function getCapBoundsBits(c) : Capability -> (CapAddrBits, CapLenBits, CapLenBits) = {
  let E = if c.E >=_u cap_max_E_bits then cap_max_E_bits else c.E;
  let a : CapAddrBits = c.address;
  let a_mid = truncate(a >> E, cap_B_width);
  let a_hi = if a_mid <_u c.B then 1 else 0;
  let a_top = a >> (E + cap_B_width);
  let base : CapAddrBits = truncate(((a_top - a_hi) @ c.B) << E, cap_addr_width);
  let length : CapLenBits  = truncate((zeros(24) @ c.M) << E, cap_len_width);
  let top : CapLenBits = (0b0 @ base) + length;
  (base, length, top)
}

function getCapBounds(cap) : Capability -> (CapAddrInt, CapLen, CapLen) =
  let (base : CapAddrBits, length: CapLenBits, top : CapLenBits) = getCapBoundsBits(cap) in
  (unsigned(base), unsigned(length), unsigned(top))

val count_ones : forall 'ni 'no, 'no >= 1. (int('no), bits('ni)) -> bits('no)
function count_ones (no, x) = {
  var out = zeros(no);
  let size = length(x) - 1;
  foreach (i from 0 to size) {
    out = out + zero_extend(x[i..i]);
  };
  out
}

/*!
 * Returns cap with E, B and M set such that the decoded bounds include the
 * region specified by base and length. If the region is not precisely
 * representable the base may be rounded down and the length up. Also returns a
 * boolean indicating whether the bounds are precisely representable, and sets
 * the address of the returned capability to the requested base.
 */
function setCapBounds(cap, b, l) : (Capability, CapAddrBits, CapAddrBits) -> (bool, Capability) = {
  let lenTrunc = truncateLSB(l, cap_addr_width - cap_B_width);
  let eCeilPlus1 : bits(cap_E_width) = to_bits(cap_E_width, cap_addr_width - cap_B_width) - count_leading_zeros(lenTrunc);
  let e : bits(cap_E_width) = eCeilPlus1 - (if count_ones(cap_E_width, lenTrunc) == to_bits(cap_E_width, 1) then to_bits(cap_E_width, 1) else zeros(cap_E_width));
  let d : bits(cap_B_width + 2) = truncate(l >> e, cap_B_width + 2);
  let mask2e = ~(ones(cap_addr_width) << e);
  let bmod2e = b & mask2e;
  let lmod2e = l & mask2e;
  let sumMod2e = bmod2e + lmod2e;
  let iInit = (sumMod2e >> e)[1..0];
  let lostSum = unsigned(sumMod2e & mask2e) != 0;
  let i : bits(2) = iInit + (if lostSum then 0b01 else 0b00);
  let m : bits(cap_B_width + 2) = d + zero_extend(i);
  let m1 : bits(cap_B_width + 1) = if m[(cap_B_width + 1)..(cap_B_width + 1)] == 0b1 then m[(cap_B_width + 1)..1] + zero_extend(m[0..0]) else truncate(m, cap_B_width + 1);
  let e1 : bits(cap_E_width) = if m[(cap_B_width + 1)..(cap_B_width + 1)] == 0b1 then e+1 else e;
  let m2 : bits(cap_B_width + 1) = if m1[cap_B_width..cap_B_width] == 0b1 then zero_extend(m1[cap_B_width..1]) + zero_extend(m1[0..0]) else truncate(m1, cap_B_width + 1);
  let e2 : bits(cap_E_width) = if m1[cap_B_width..cap_B_width] == 0b1 then e1+1 else e1;
  let m3 : bits(cap_B_width) = if m2[cap_B_width..cap_B_width] == 0b1 then (m2[cap_B_width..1]) + zero_extend(m2[0..0]) else truncate(m2, cap_B_width);
  let e3 : bits(cap_E_width) = if m2[cap_B_width..cap_B_width] == 0b1 then e2+1 else e2;
  let maskLo : CapAddrBits = ~(ones(cap_addr_width) << e3);
  lostSignificantLength  = unsigned(l & maskLo) != 0;
  lostSignificantBase  = unsigned(b & maskLo) != 0;
  let exact = not(lostSignificantBase | lostSignificantLength);
  let newCap = {cap with address=b, E=e3, B=truncate((b >> e3), cap_B_width), M=m3};
  (exact, newCap)
}

function getCapPerms(cap) : Capability -> CapPermsBits = [
  bool_to_bit(cap.perm_user0),
  bool_to_bit(cap.permit_seal),
  bool_to_bit(cap.permit_unseal),
  bool_to_bit(cap.permit_execute),
  bool_to_bit(cap.access_system_regs),
  bool_to_bit(cap.permit_load_store_cap),
  bool_to_bit(cap.permit_load),
  bool_to_bit(cap.permit_store_local_cap),
  bool_to_bit(cap.permit_load_mutable),
  bool_to_bit(cap.permit_store),
  bool_to_bit(cap.permit_load_global),
  bool_to_bit(cap.global)
]

 function setCapPerms(cap, perms) : (Capability, CapPermsBits) -> Capability =
  { cap with
    perm_user0             = bit_to_bool(perms[11]),
    permit_seal            = bit_to_bool(perms[10]),
    permit_unseal          = bit_to_bool(perms[9]),
    permit_execute         = bit_to_bool(perms[8]),
    access_system_regs     = bit_to_bool(perms[7]),
    permit_load_store_cap  = bit_to_bool(perms[6]),
    permit_load            = bit_to_bool(perms[5]),
    permit_store_local_cap = bit_to_bool(perms[4]),
    permit_load_mutable    = bit_to_bool(perms[3]),
    permit_store           = bit_to_bool(perms[2]),
    permit_load_global     = bit_to_bool(perms[1]),
    global                 = bit_to_bool(perms[0])
  }

/*!
 * Returns whether the given capability is sealed i.e. whether its otype is zero.
 */
val isCapSealed : Capability -> bool
function isCapSealed(cap) = signed(cap.otype) != otype_unsealed

/*!
 * Returns true if the given capability has one of the sentry otypes, otherwise false.
 */
val isCapSentry : Capability -> bool
function isCapSentry(cap) =
  match unsigned(cap.otype) {
    otype if otype == otype_sentry     => true,
    otype if otype == otype_sentry_id  => true,
    otype if otype == otype_sentry_ie  => true,
    otype if otype == otype_sentry_bid => true,
    otype if otype == otype_sentry_bie => true,
    _  => false
  }

/*!
 * Returns true if the given capability has one of the forward sentry otypes, otherwise false.
 */
val isCapForwardSentry : Capability -> bool
function isCapForwardSentry(cap) =
  match unsigned(cap.otype) {
    otype if otype == otype_sentry    => true,
    otype if otype == otype_sentry_id => true,
    otype if otype == otype_sentry_ie => true,
    _  => false
  }

/*!
 * Returns true if the given capability has one of the forward interrupt-control sentry otypes, otherwise false.
 */
val isCapForwardControlSentry : Capability -> bool
function isCapForwardControlSentry(cap) =
  match unsigned(cap.otype) {
    otype if otype == otype_sentry_id => true,
    otype if otype == otype_sentry_ie => true,
    _  => false
  }

/*!
 * Returns true if the given capability has one of the backward sentry otypes, otherwise false.
 */
val isCapBackwardSentry : Capability -> bool
function isCapBackwardSentry(cap) =
  match unsigned(cap.otype) {
    otype if otype == otype_sentry_bid => true,
    otype if otype == otype_sentry_bie => true,
    _  => false
  }

/*!
 * Returns true if the given capability has one of the forward interrupt-inherited sentry otype, otherwise false.
 */
val isCapForwardInheritSentry : Capability -> bool
function isCapForwardInheritSentry(cap) =
  match unsigned(cap.otype) {
    otype if otype == otype_sentry => true,
    _  => false
  }

function sealCap(cap, otyp) : (Capability, bits(cap_otype_width)) -> Capability =
    {cap with otype=otyp}

function unsealCap(cap) : Capability -> Capability =
    {cap with otype=to_bits(cap_otype_width, otype_unsealed)}

function getCapBaseBits(c) : Capability -> CapAddrBits =
    let (base, _, _) = getCapBoundsBits(c) in
    base

function getCapBase(c) : Capability -> CapAddrInt =
    unsigned(getCapBaseBits(c))

function getCapTopBits(c) : Capability -> CapLenBits =
    let (_, _, top) = getCapBoundsBits(c) in {
      top
    }

function getCapTop (c) : Capability -> CapLen =
    unsigned(getCapTopBits(c))

function getCapOffsetBits(c) : Capability -> CapAddrBits =
    let base : CapAddrBits = getCapBaseBits(c) in
    c.address - base

function getCapOffset(c) : Capability -> CapAddrInt =
    unsigned(getCapOffsetBits(c))

function getCapLength(c) : Capability -> CapLen =
    let (_, length, _) = getCapBoundsBits(c) in
      unsigned(length)

/*!
 * THIS(cap, addr, len) checks whether the capability cap includes the region
 * specified by addr and len. Specifically it checks whether
 * cap.base $\le$ addr AND addr + len $\le$ cap.top. Note that this definition
 * returns true if len is zero and addr $=$ cap.top.
 */
val inCapBounds  : (Capability, CapAddrBits, CapLen) -> bool
function inCapBounds (cap, addr, size) = {
  let (base, length, top) = getCapBounds(cap);
  let a = unsigned(addr);
  (a >= base) & (a + size <= top)
}

function int_to_cap (offset) : CapAddrBits -> Capability =
    {null_cap with address = offset}

/*!
 * Returns the given capability with the tag cleared if the second argument is
 * true, otherwise returns it with the original tag value preserved.
 */
val clearTagIf : (Capability, bool) -> Capability
function clearTagIf(cap, cond) =
    {cap with tag = cap.tag & not(cond)}

/*!
 * Returns the given capability with the tag cleared if the capability
 * is sealed, otherwise returns it with the original tag value preserved.
 */
val clearTagIfSealed : Capability -> Capability
function clearTagIfSealed(cap) : Capability -> Capability =
    clearTagIf(cap, isCapSealed(cap))

/*!
 * Returns the given capability with the tag set to false.
 */
val clearTag : Capability -> Capability
function clearTag(cap) : Capability -> Capability =
    clearTagIf(cap, true)

function capBoundsEqual (c1, c2) : (Capability, Capability) -> bool =
    let (base1, length1, _) = getCapBounds(c1) in
    let (base2, length2, _) = getCapBounds(c2) in
    (base1 == base2) & (length1 == length2)

/*!
 * Returns the given capability with the address set to the given value and a boolean
 * indicating whether the new address is within representable range (decoded
 * bounds remain the same).
 */
val setCapAddr : (Capability, CapAddrBits) -> (bool, Capability)
function setCapAddr(c, addr) =
    let newCap = { c with address = addr } in
    let representable = capBoundsEqual(c, newCap) in
    (representable, newCap)

/*!
 * Returns the given capability with the address set to given value. If the new
 * address is not in the representable range or the capability is sealed then
 * the tag is cleared.
 */
val setCapAddrChecked : (Capability, CapAddrBits) -> Capability
function setCapAddrChecked (cap, addr) =
    let (representable, newCap) = setCapAddr(cap, addr) in
    clearTagIf(newCap, not(representable) | isCapSealed(cap))

infix 1 >>_s
overload operator >> = {sail_shiftright}
overload operator << = {sail_shiftleft}
overload operator >>_s = {sail_arith_shiftright}

function setCapOffset(c, offset) : (Capability, CapAddrBits) -> (bool, Capability) =
    let base = getCapBaseBits(c) in
    let newAddress = base + offset in
    let newCap     = { c with address = newAddress } in
    let representable = capBoundsEqual(c, newCap) in
    /* let representable = fastRepCheck(c, (newAddress - c.address)) in */
    (representable, newCap)

function setCapOffsetChecked (cap, offset) : (Capability, CapAddrBits) -> Capability =
    let (representable, newCap) = setCapOffset(cap, offset) in
    clearTagIf(newCap, not(representable) | isCapSealed(cap))

/*!
 * Returns the given capability with the address incremented by the given value 
 * and a boolean indicating whether the new address is within representable 
 * range (decoded bounds remain the same).
 */
val incCapAddr : (Capability, CapAddrBits) -> (bool, Capability)
function incCapAddr(c, delta) =
    let newAddress : CapAddrBits = c.address + delta in
    let newCap     = { c with address = newAddress } in
    let representable = capBoundsEqual(c, newCap) in
    /* let representable = fastRepCheck(c, delta) in */
    (representable, newCap)


val capToString : (Capability) -> string
function capToString (cap) = {
  let (base, length, top) = getCapBoundsBits(cap);
  let top_str = BitStr(0b000 @ top);
  let len_str = BitStr(0b000 @ length);
  BitStr(cap.address)
    ^ " (v:" ^ (if cap.tag then "1 " else "0 ")
    ^ BitStr(base) ^ "-" ^ top_str
    ^ " l:" ^ len_str
    ^ " o:" ^ BitStr(cap.otype)
    ^ " p:"
    ^ (if cap.global then "G " else "- ")
    ^ (if cap.permit_load then "R" else "-")
    ^ (if cap.permit_store then "W" else "-")
    ^ (if cap.permit_load_store_cap then "c" else "-")
    ^ (if cap.permit_load_mutable then "m" else "-")
    ^ (if cap.permit_load_global then "g" else "-")
    ^ (if cap.permit_store_local_cap then "l " else "- ")
    ^ (if cap.permit_execute then "X" else "-")
    ^ (if cap.access_system_regs then "a " else "- ")
    ^ (if cap.permit_seal then "S" else "-")
    ^ (if cap.permit_unseal then "U" else "-")
    ^ (if cap.perm_user0 then "0)" else "-)")
}

/*!
 * For a given length computes the exponent, $e$, that would be used to represent
 * a capability of that length and returns a mask consisting of $e$ zeros in the
 * least significant bits and ones in the upper bits.
 */
val getRepresentableAlignmentMask: xlenbits -> xlenbits
/*!
 * The representable alignment mask for a given length depends on the exponent
 * that would be used to represent a region of that length, assuming the base
 * is sufficiently aligned. To compute this we resuse the implementation of
 * [setCapBounds]
 */
function getRepresentableAlignmentMask(len) = {
  let (exact, c) = setCapBounds(root_cap_mem, to_bits(sizeof(xlen), 0), len);
  var e = unsigned(c.E);
  ones(sizeof(xlen)) << e
}

/*!
 * For a given length, $l$, returns a value greater than or equal to $l$ that
 * will result in a precisely representable capability when used with a
 * base that is suitably aligned as per [getRepresentableAlignmentMask].
 */
val getRepresentableLength : xlenbits -> xlenbits
/*!
 * Given the required alignment mask returned by [getRepresentableAlignmentMask]
 * we can round up the length by bit twiddling.
 */
function getRepresentableLength(len) = {
  let m = getRepresentableAlignmentMask(len);
  (len + ~(m)) & m
}