Catch up with sail-riscv

CHERIoT-Platform · Jan 13, 2024 · 129fdc7 · 129fdc7
1 parent 14e5bb5
commit 129fdc7
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 10 deletions.
diff --git a/Makefile b/Makefile
@@ -60,7 +60,6 @@ SAIL_VM_SRCS += $(SAIL_$(ARCH)_VM_SRCS)
 
 # Non-instruction sources
 PRELUDE = $(SAIL_RISCV_MODEL_DIR)/prelude.sail \
-          $(SAIL_RISCV_MODEL_DIR)/prelude_mapping.sail \
           $(SAIL_XLEN) \
           $(SAIL_FLEN) \
           $(SAIL_VLEN) \

diff --git a/src/cheri_prelude.sail b/src/cheri_prelude.sail
@@ -68,15 +68,6 @@ val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
 val MAX : forall 'n, 'n >= 0 . atom('n) -> atom(2 ^ 'n - 1) effect pure
 function MAX(n) = pow2(n) - 1
 
-val not = {coq:"negb", _:"not"} : bool -> bool
-
-/*!
- * THIS converts a boolean to a bit in the conventional way by mapping `true` to
- * `bitone` and `false` to `bitzero`.
- */
-val bool_to_bit : bool -> bit
-function bool_to_bit x = if x then bitone else bitzero
-
 /*!
  * align_down(n, bv) returns the given bit vector, bv,  aligned down to a power
  * of two by clearing the least significant n bits.