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

1 files changed, 0 insertions, 23 deletions

diff --git a/cheri/sail_latexcc/sailccfnfastRepCheck.tex b/cheri/sail_latexcc/sailccfnfastRepCheck.tex
deleted file mode 100644
index 3e4d2111..00000000
--- a/cheri/sail_latexcc/sailccfnfastRepCheck.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-function #\hyperref[zfastRepCheck]{fastRepCheck}#(c, i) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> bool=
-    let 'E = #\hyperref[zunsigned]{unsigned}#(c.E) in
-    if (E >= 44) then
-        true /* in this case representable region is whole address space */
-    else
-        let E'       = #\hyperref[zmin]{min}#(E, 43) in
-        let i_top    = #\hyperref[zsigned]{signed}#(i[63..E+20]) in
-        let i_mid : #\hyperref[zbits]{bits}#(20) = i[E+19..E] in
-        let a_mid : #\hyperref[zbits]{bits}#(20) = (c.address)[E+19..E] in
-        let R : #\hyperref[zbits]{bits}#(20)     = (c.B) - 0x01000 in
-        let diff : #\hyperref[zbits]{bits}#(20)  = R - a_mid in
-        let diff1 : #\hyperref[zbits]{bits}#(20) = diff - 1 in
-        /* i_top determines 1. whether the increment is inRange
-           i.e. less than the size of the representable region
-           (2**(E+20)) and 2. whether it is positive or negative. To
-           satisfy 1. all top bits must be the same so we are
-           interested in the cases i_top is 0 or -1 */
-        if (i_top == 0) then
-          i_mid <_u diff1
-        else if (i_top == -1) then
-          (i_mid >=_u diff) & (R != a_mid)
-        else
-          false