Remove cheri and mips specs -- they now have their own repository.

1 files changed, 0 insertions, 649 deletions

diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
deleted file mode 100644
index 6babfd19..00000000
--- a/mips/mips_prelude.sail
+++ /dev/null
@@ -1,649 +0,0 @@
-/*========================================================================*/
-/*                                                                        */
-/*  Copyright (c) 2015-2017 Robert M. Norton                              */
-/*  Copyright (c) 2015-2017 Kathyrn Gray                                  */
-/*  All rights reserved.                                                  */
-/*                                                                        */
-/*  This software was developed by the University of Cambridge Computer   */
-/*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  */
-/*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   */
-/*                                                                        */
-/*  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.                                                          */
-/*========================================================================*/
-
-/* mips_prelude.sail: declarations of mips registers, and functions common 
-   to mips instructions (e.g. address translation) */
-
-register PC : bits(64)
-register nextPC : bits(64)
-
-/* CP0 Registers */
-
-bitfield CauseReg : bits(32) = {
-  BD : 31, /* branch delay */
-  /*Z0 : 30,*/
-  CE : 29.. 28, /* for coprocessor enable exception */
-  /*Z1 : 27.. 24,*/
-  IV : 23, /* special interrupt vector not supported */
-  WP : 22, /* watchpoint exception occurred */
-  /*Z2 : 21.. 16, */
-  IP : 15.. 8, /* interrupt pending bits */
-  /*Z3 : 7,*/
-  ExcCode : 6.. 2, /* code of last exception */
-  /*Z4 : 1.. 0,*/
-}
-
-bitfield TLBEntryLoReg : bits(64) = {
-  CapS : 63,
-  CapL : 62,
-  PFN : 29.. 6,
-  C : 5.. 3,
-  D : 2,
-  V : 1,
-  G : 0,
-}
-
-bitfield TLBEntryHiReg : bits(64) = {
-  R : 63.. 62,
-  VPN2 : 39.. 13,
-  ASID : 7..  0,
-}
-
-bitfield ContextReg : bits(64) = {
-  PTEBase : 63.. 23,
-  BadVPN2 : 22.. 4,
-  /*ZR : 3.. 0,*/
-}
-
-bitfield XContextReg : bits(64) = {
-  XPTEBase : 63.. 33,
-  XR : 32.. 31,
-  XBadVPN2 : 30..  4,
-}
-
-let TLBNumEntries = 64
-type TLBIndexT = (bits(6))
-let TLBIndexMax : TLBIndexT = 0b111111
-
-val MAX : forall 'n. atom('n) -> atom(2 ^ 'n - 1) effect pure
-function MAX(n) = pow2(n) - 1
-
-let MAX_U64 = MAX(64) /*unsigned(0xffffffffffffffff)*/
-let MAX_VA  = MAX(40) /*unsigned(0xffffffffff)*/
-let MAX_PA  = MAX(36) /*unsigned(0xfffffffff)*/
-
-bitfield TLBEntry : bits(117) = {
-  pagemask : 116..  101,
-  r        : 100..  99,
-  vpn2     : 98..  72,
-  asid     : 71..  64,
-  g        : 63,
-  valid    : 62,
-  caps1    : 61,
-  capl1    : 60,
-  pfn1     : 59..  36,
-  c1       : 35..  33,
-  d1       : 32,
-  v1       : 31,
-  caps0    : 30,
-  capl0    : 29,
-  pfn0     : 28..  5,
-  c0       : 4..  2,
-  d0       : 1,
-  v0       : 0,
-}
-
-register TLBProbe : bits(1)
-register TLBIndex : TLBIndexT
-register TLBRandom : TLBIndexT
-register TLBEntryLo0 : TLBEntryLoReg
-register TLBEntryLo1 : TLBEntryLoReg
-register TLBContext : ContextReg
-register TLBPageMask : bits(16)
-register TLBWired : TLBIndexT
-register TLBEntryHi : TLBEntryHiReg
-register TLBXContext : XContextReg
-
-register TLBEntry00 : TLBEntry
-register TLBEntry01 : TLBEntry
-register TLBEntry02 : TLBEntry
-register TLBEntry03 : TLBEntry
-register TLBEntry04 : TLBEntry
-register TLBEntry05 : TLBEntry
-register TLBEntry06 : TLBEntry
-register TLBEntry07 : TLBEntry
-register TLBEntry08 : TLBEntry
-register TLBEntry09 : TLBEntry
-register TLBEntry10 : TLBEntry
-register TLBEntry11 : TLBEntry
-register TLBEntry12 : TLBEntry
-register TLBEntry13 : TLBEntry
-register TLBEntry14 : TLBEntry
-register TLBEntry15 : TLBEntry
-register TLBEntry16 : TLBEntry
-register TLBEntry17 : TLBEntry
-register TLBEntry18 : TLBEntry
-register TLBEntry19 : TLBEntry
-register TLBEntry20 : TLBEntry
-register TLBEntry21 : TLBEntry
-register TLBEntry22 : TLBEntry
-register TLBEntry23 : TLBEntry
-register TLBEntry24 : TLBEntry
-register TLBEntry25 : TLBEntry
-register TLBEntry26 : TLBEntry
-register TLBEntry27 : TLBEntry
-register TLBEntry28 : TLBEntry
-register TLBEntry29 : TLBEntry
-register TLBEntry30 : TLBEntry
-register TLBEntry31 : TLBEntry
-register TLBEntry32 : TLBEntry
-register TLBEntry33 : TLBEntry
-register TLBEntry34 : TLBEntry
-register TLBEntry35 : TLBEntry
-register TLBEntry36 : TLBEntry
-register TLBEntry37 : TLBEntry
-register TLBEntry38 : TLBEntry
-register TLBEntry39 : TLBEntry
-register TLBEntry40 : TLBEntry
-register TLBEntry41 : TLBEntry
-register TLBEntry42 : TLBEntry
-register TLBEntry43 : TLBEntry
-register TLBEntry44 : TLBEntry
-register TLBEntry45 : TLBEntry
-register TLBEntry46 : TLBEntry
-register TLBEntry47 : TLBEntry
-register TLBEntry48 : TLBEntry
-register TLBEntry49 : TLBEntry
-register TLBEntry50 : TLBEntry
-register TLBEntry51 : TLBEntry
-register TLBEntry52 : TLBEntry
-register TLBEntry53 : TLBEntry
-register TLBEntry54 : TLBEntry
-register TLBEntry55 : TLBEntry
-register TLBEntry56 : TLBEntry
-register TLBEntry57 : TLBEntry
-register TLBEntry58 : TLBEntry
-register TLBEntry59 : TLBEntry
-register TLBEntry60 : TLBEntry
-register TLBEntry61 : TLBEntry
-register TLBEntry62 : TLBEntry
-register TLBEntry63 : TLBEntry
-
-let TLBEntries : vector(64, dec, register(TLBEntry)) = [
-    ref TLBEntry63,
-    ref TLBEntry62,
-    ref TLBEntry61,
-    ref TLBEntry60,
-    ref TLBEntry59,
-    ref TLBEntry58,
-    ref TLBEntry57,
-    ref TLBEntry56,
-    ref TLBEntry55,
-    ref TLBEntry54,
-    ref TLBEntry53,
-    ref TLBEntry52,
-    ref TLBEntry51,
-    ref TLBEntry50,
-    ref TLBEntry49,
-    ref TLBEntry48,
-    ref TLBEntry47,
-    ref TLBEntry46,
-    ref TLBEntry45,
-    ref TLBEntry44,
-    ref TLBEntry43,
-    ref TLBEntry42,
-    ref TLBEntry41,
-    ref TLBEntry40,
-    ref TLBEntry39,
-    ref TLBEntry38,
-    ref TLBEntry37,
-    ref TLBEntry36,
-    ref TLBEntry35,
-    ref TLBEntry34,
-    ref TLBEntry33,
-    ref TLBEntry32,
-    ref TLBEntry31,
-    ref TLBEntry30,
-    ref TLBEntry29,
-    ref TLBEntry28,
-    ref TLBEntry27,
-    ref TLBEntry26,
-    ref TLBEntry25,
-    ref TLBEntry24,
-    ref TLBEntry23,
-    ref TLBEntry22,
-    ref TLBEntry21,
-    ref TLBEntry20,
-    ref TLBEntry19,
-    ref TLBEntry18,
-    ref TLBEntry17,
-    ref TLBEntry16,
-    ref TLBEntry15,
-    ref TLBEntry14,
-    ref TLBEntry13,
-    ref TLBEntry12,
-    ref TLBEntry11,
-    ref TLBEntry10,
-    ref TLBEntry09,
-    ref TLBEntry08,
-    ref TLBEntry07,
-    ref TLBEntry06,
-    ref TLBEntry05,
-    ref TLBEntry04,
-    ref TLBEntry03,
-    ref TLBEntry02,
-    ref TLBEntry01,
-    ref TLBEntry00
-]
-
-register CP0Compare : bits(32)
-register CP0Cause : CauseReg
-register CP0EPC : bits(64)
-register CP0ErrorEPC : bits(64)
-register CP0LLBit : bits(1)
-register CP0LLAddr : bits(64)
-register CP0BadVAddr : bits(64)
-register CP0Count : bits(32)
-register CP0HWREna : bits(32)
-register CP0UserLocal : bits(64)
-register CP0ConfigK0 : bits(3)
-
-bitfield StatusReg : bits(32) = {
-  CU : 31.. 28,  /* co-processor enable bits */
-  /* RP/FR/RE/MX/PX not implemented */
-  BEV : 22, /* use boot exception vectors (initialised to one) */
-  /* TS/SR/NMI not implemented */
-  IM : 15.. 8,  /* Interrupt mask */
-  KX : 7,  /* kernel 64-bit enable */
-  SX : 6,  /* supervisor 64-bit enable */
-  UX : 5,  /* user 64-bit enable */
-  KSU : 4.. 3, /* Processor mode */
-  ERL : 2, /* error level (should be initialised to one, but BERI is different) */
-  EXL : 1, /* exception level */
-  IE : 0,  /* interrupt enable */
-}
-register CP0Status : StatusReg
-
-/* Implementation registers -- not ISA defined */
-register branchPending : bits(1)      /* Set by branch instructions to implement branch delay */
-register inBranchDelay : bits(1)      /* Needs to be set by outside world when in branch delay slot */
-register delayedPC : bits(64)          /* Set by branch instructions to implement branch delay */
-
-val execute_branch : bits(64) -> unit effect {wreg}
-function execute_branch(pc) = {
-  delayedPC = pc;
-  branchPending = 0b1;
-}
-
-/* General purpose registers */
-
-
-/* Special registers For MUL/DIV */
-register HI : bits(64)
-register LO : bits(64)
-
-register GPR : vector(32, dec, bits(64))
-
-/* JTAG Uart registers */
-
-register UART_WDATA : bits(8)
-register UART_WRITTEN : bits(1)
-register UART_RDATA : bits(8)
-register UART_RVALID : bits(1)
-
-/* Check whether a given 64-bit vector is a properly sign extended 32-bit word */
-val NotWordVal : bits(64) -> bool effect pure
-function NotWordVal (word) =
-    (word[31] ^^ 32) != word[63..32]
-
-/* Read numbered GP reg. (r0 is always zero) */
-val rGPR : bits(5) -> bits(64) effect {rreg}
-function rGPR idx = {
-         let i as atom(_) = unsigned(idx) in
-         if i == 0 then 0x0000000000000000 else GPR[i]
-}
-
-/* Write numbered GP reg. (writes to r0 ignored) */
-val wGPR : (bits(5), bits(64)) -> unit effect {wreg}
-function wGPR (idx, v) = {
-  let i as atom(_) = unsigned(idx) in
-  if i != 0 then {
-    /*prerr_string(string_of_int(i));
-    prerr_bits(" <- ", v);*/
-    GPR[i] = v;
-  };
-}
-
-val MEMr = {lem: "MEMr"} : forall 'n, 'n >= 0.
-  ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n, 'n >= 0.
-  ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-val MEM_sync = {lem: "MEM_sync"} :
-  unit -> unit effect { barr }
-
-val MEMea = {lem: "MEMea"} : forall 'n.
-  ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMea_conditional = {lem: "MEMea_conditional"} : forall 'n.
-  ( bits(64) , atom('n)) -> unit effect { eamem }
-val MEMval = {lem: "MEMval"} : forall 'n.
-  ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv }
-val MEMval_conditional = {lem: "MEMval_conditional"} : forall 'n.
-  ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv }
-
-/* Extern nops with effects, sometimes useful for faking effect */
-val skip_eamem = "skip" : unit -> unit effect {eamem}
-val skip_barr = "skip" : unit -> unit effect {barr}
-val skip_wreg = "skip" : unit -> unit effect {wreg}
-val skip_rreg = "skip" : unit -> unit effect {rreg}
-val skip_wmvt = "skip" : unit -> unit effect {wmvt}
-val skip_rmemt = "skip" : unit -> unit effect {rmemt}
-val skip_escape = "skip" : unit -> unit effect {escape}
-
-function MEMr (addr, size) = __MIPS_read(addr, size)
-function MEMr_reserve (addr, size) = __MIPS_read(addr, size)
-function MEM_sync () = skip_barr()
-
-function MEMea (addr, size) = skip_eamem()
-function MEMea_conditional (addr, size) = skip_eamem()
-function MEMval (addr, size, data) = __MIPS_write(addr, size, data)
-function MEMval_conditional (addr, size, data) = { __MIPS_write(addr, size, data); true }
-
-enum Exception =
-{
-   Interrupt, TLBMod, TLBL, TLBS, AdEL, AdES, Sys, Bp, ResI, CpU, Ov, Tr, C2E, C2Trap,
-   XTLBRefillL, XTLBRefillS, XTLBInvL, XTLBInvS, MCheck
-}
-
-/* Return the ISA defined code for an exception condition */
-function ExceptionCode (ex) : Exception -> bits(5)=
-   let x : bits(8) = match ex
-   {
-      Interrupt    => 0x00, /* Interrupt */
-      TLBMod       => 0x01, /* TLB modification exception */
-      TLBL         => 0x02, /* TLB exception (load or fetch) */
-      TLBS         => 0x03, /* TLB exception (store) */
-      AdEL         => 0x04, /* Address error (load or fetch) */
-      AdES         => 0x05, /* Address error (store) */
-      Sys          => 0x08, /* Syscall */
-      Bp           => 0x09, /* Breakpoint */
-      ResI         => 0x0a, /* Reserved instruction */
-      CpU          => 0x0b, /* Coprocessor Unusable */
-      Ov           => 0x0c, /* Arithmetic overflow */
-      Tr           => 0x0d, /* Trap */
-      C2E          => 0x12, /* C2E coprocessor 2 exception */
-      C2Trap       => 0x12, /* C2Trap maps to same exception code, different vector */
-      XTLBRefillL  => 0x02,
-      XTLBRefillS  => 0x03,
-      XTLBInvL     => 0x02,
-      XTLBInvS     => 0x03,
-      MCheck       => 0x18
-   } in x[4..0]
-
-
-val SignalExceptionMIPS : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
-function SignalExceptionMIPS (ex, kccBase) = 
-  {
-    /* Only update EPC and BD if not already in EXL mode */
-    if (~ (CP0Status.EXL())) then 
-      {
-        if (inBranchDelay[0]) then
-          {
-            CP0EPC = PC - 4;
-            CP0Cause->BD() = 0b1;
-          }
-        else
-          {
-            CP0EPC = PC;
-            CP0Cause->BD() = 0b0;
-          }
-      };
-
-      /* choose an exception vector to branch to. Some are not supported 
-         e.g. Reset */
-      vectorOffset = 
-        if (CP0Status.EXL()) then
-          0x180 /* Always use common vector if in exception mode already */
-        else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then 
-          0x080
-        else if (ex == C2Trap) then
-          0x280 /* Special vector for CHERI traps */
-        else
-          0x180; /* Common vector */
-      vectorBase : bits(64) = if CP0Status.BEV() then
-                   0xFFFFFFFFBFC00200
-                else
-                   0xFFFFFFFF80000000;
-      /* On CHERI we have to subtract KCC.base so that we end up at the 
-         right absolute vector address after indirecting via new PCC */
-      nextPC = vectorBase + sign_extend(vectorOffset) - kccBase;
-      CP0Cause->ExcCode() = ExceptionCode(ex);
-      CP0Status->EXL()    = 0b1;
-      throw (ISAException());
-  }
-
-/* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */
-val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg}
-
-val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
-function  SignalExceptionBadAddr(ex, badAddr) =
-  {
-    CP0BadVAddr = badAddr;
-    SignalException(ex);
-  }
-
-val SignalExceptionTLB : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
-function SignalExceptionTLB(ex, badAddr) = {
-  CP0BadVAddr = badAddr;
-  TLBContext->BadVPN2()  = (badAddr[31..13]);
-  TLBXContext->XBadVPN2()= (badAddr[39..13]);
-  TLBXContext->XR()      = (badAddr[63..62]);
-  TLBEntryHi->R()        = (badAddr[63..62]);
-  TLBEntryHi->VPN2()     = (badAddr[39..13]);
-  SignalException(ex);
-}
-
-enum MemAccessType = {Instruction, LoadData, StoreData}
-enum AccessLevel = {User, Supervisor, Kernel} 
-
-val int_of_AccessLevel : AccessLevel -> {|0, 1, 2|} effect pure
-function int_of_AccessLevel level =
-  match level {
-    User        => 0,
-    Supervisor  => 1,
-    Kernel      => 2
-  }
-
-/*!
-Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level.
- */
-val grantsAccess : (AccessLevel, AccessLevel) -> bool
-function grantsAccess (currentLevel, requiredLevel) =
-  int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel)
-
-/*!
-Returns the current effective access level determined by accessing the relevant parts of the MIPS status register.
- */
-val getAccessLevel : unit -> AccessLevel effect {rreg}
-function getAccessLevel() =
-  if ((CP0Status.EXL()) | (CP0Status.ERL())) then
-    Kernel
-  else match CP0Status.KSU()
-    {
-      0b00  => Kernel,
-      0b01  => Supervisor,
-      0b10  => User,
-      _     => User /* behaviour undefined, assume user */
-    }
-
-val checkCP0Access : unit->unit effect{escape, rreg, wreg}
-function checkCP0Access () =
-  {
-    let accessLevel = getAccessLevel() in
-    if ((accessLevel != Kernel) & (~(CP0Status.CU()[0]))) then
-      {
-        CP0Cause->CE() = 0b00;
-        SignalException(CpU);
-      }
-  }
-
-val incrementCP0Count : unit -> unit effect {rreg,wreg,escape}
-function incrementCP0Count() = {
-  TLBRandom = (if (TLBRandom == TLBWired)
-    then (TLBIndexMax) else (TLBRandom - 1));
-
-  CP0Count = (CP0Count + 1);
-  if (CP0Count == CP0Compare) then {
-    CP0Cause->IP() = CP0Cause.IP() | 0x80; /* IP7 is timer interrupt  */
-  };
-
-  let ims = CP0Status.IM() in
-  let ips = CP0Cause.IP() in
-  let ie  = CP0Status.IE() in
-  let exl = CP0Status.EXL() in
-  let erl = CP0Status.ERL() in
-  if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then
-    SignalException(Interrupt);
-}
-
-type regno = bits(5)                      /* a register number */
-type imm16 = bits(16)                     /* 16-bit immediate */
-/* a commonly used instruction format with three register operands */
-type regregreg = (regno, regno, regno)
-/* a commonly used instruction format with two register operands and 16-bit immediate */
-type regregimm16 = (regno, regno, imm16)
-
-enum decode_failure = { 
-  no_matching_pattern, 
-  unsupported_instruction, 
-  illegal_instruction, 
-  internal_error
-}
-
-/* Used by branch and trap instructions */
-enum Comparison = { 
-  EQ, /* equal */
-  NE, /* not equal */
-  GE, /* signed greater than or equal */
-  GEU,/* unsigned greater than or equal */ 
-  GT, /* signed strictly greater than */ 
-  LE, /* signed less than or equal */ 
-  LT, /* signed strictly less than */ 
-  LTU /* unsigned less than or qual */ 
-}
-
-val compare : (Comparison, bits(64), bits(64)) -> bool
-function compare (cmp, valA, valB) =
-  match cmp {
-    EQ   => valA ==   valB,
-    NE   => valA !=   valB,
-    GE   => valA >=_s valB,
-    GEU  => valA >=_u valB,
-    GT   => valB <_s  valA,
-    LE   => valB >=_s valA,
-    LT   => valA <_s  valB,
-    LTU  => valA <_u  valB
-  }
-enum WordType = { B, H, W, D}
-enum WordTypeUnaligned = { WL, WR, DL, DR }
-
-val wordWidthBytes : WordType -> range(1, 8)
-function wordWidthBytes(w) =
-  match w {
-    B  => 1,
-    H  => 2,
-    W  => 4,
-    D  => 8
-  }
-
-/* This function checks that memory accesses are naturally aligned
-   -- it is disabled in favour of BERI specific behaviour below.
-function bool isAddressAligned(addr, (WordType) wordType) =
-  match wordType {
-    B  => true
-    H  => (addr[0]    == 0)
-    W  => (addr[1..0] == 0b00)
-    D  => (addr[2..0] == 0b000)
-  }
-*/
-
-/* BERI relaxes the natural alignment requirement for loads and stores
-   but still throws an exception if an access spans a cache line
-   boundary.  Here we assume this is 32 bytes so that we don't have to
-   worry about clearing multiple tags when an access spans more than
-   one capability. Capability load/stores are still naturally
-   aligned. Provided this is a factor of smallest supported page size
-   (4k) we don't need to worry about accesses spanning page boundaries
-   either.
-*/
-let alignment_width = 16
-val isAddressAligned : (bits(64), WordType) -> bool
-function isAddressAligned (addr, wordType) =
-  let a = unsigned(addr) in
-  a / alignment_width == (a + wordWidthBytes(wordType) - 1) / alignment_width
-
-val reverse_endianness = "reverse_endianness" : forall 'W, 'W >= 1. bits(8 * 'W) -> bits(8 * 'W) effect pure
-
-/*
-function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness' (w, value) =
-{
-    ([:8 * 'W:]) width = length(value);
-    if width <= 8
-    then value
-    else value[7..0] : reverse_endianness'(w - 1, value[(width - 1) .. 8])
-}
-
-
-
-function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * 'W)) value) =
-{
-    reverse_endianness'(sizeof 'W, value)
-}*/
-
-val MEMr_wrapper : forall 'n, 1 <= 'n <= 8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg}
-function MEMr_wrapper (addr, size) =
-    if (addr == 0x000000007f000000) then
-      {
-        let rvalid = UART_RVALID in
-        {
-          UART_RVALID = [bitzero];
-          mask(0x00000000 @ UART_RDATA @ rvalid @ 0b0000000 @ 0x0000)
-        }
-      }
-    else if (addr == 0x000000007f000004) then
-      mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */
-    else
-      reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */
-
-val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
-function MEMr_reserve_wrapper (addr , size) =
-    reverse_endianness(MEMr_reserve(addr, size))
-
-
-function init_cp0_state () : unit -> unit = {
-  CP0Status->BEV() = bitone;
-}
-
-val init_cp2_state : unit -> unit effect {wreg}
-val cp2_next_pc:     unit -> unit effect {rreg, wreg}
-val dump_cp2_state : unit -> unit effect {rreg, escape}