3 files changed, 24 insertions, 0 deletions
diff --git a/lib/sail.c b/lib/sail.c
index f897fc11..0fcb5d55 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -741,6 +741,16 @@ void sail_truncate(lbits *rop, const lbits op, const sail_int len)
   normalize_lbits(rop);
 }
 
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len)
+{
+  uint64_t rlen = mpz_get_ui(len);
+  assert(op.len >= rlen);
+  rop->len = rlen;
+  // similar to vector_subrange_lbits above -- right shift LSBs away
+  mpz_fdiv_q_2exp(*rop->bits, *op.bits, op.len - rlen);
+  normalize_lbits(rop);
+}
+
 fbits bitvector_access(const lbits op, const sail_int n_mpz)
 {
   uint64_t n = mpz_get_ui(n_mpz);
diff --git a/lib/sail.h b/lib/sail.h
index 1310dd72..53b9c6be 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -256,6 +256,7 @@ void vector_subrange_lbits(lbits *rop,
 			       const sail_int m_mpz);
 
 void sail_truncate(lbits *rop, const lbits op, const sail_int len);
+void sail_truncateLSB(lbits *rop, const lbits op, const sail_int len);
 
 fbits bitvector_access(const lbits op, const sail_int n_mpz);
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 6953264f..4e4bad5a 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -35,6 +35,9 @@ val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('
 
 val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _least_ significant `n` bits.
+ */
 val truncate = {
   ocaml: "vector_truncate",
   lem: "vector_truncate",
@@ -42,6 +45,16 @@ val truncate = {
   c: "sail_truncate"
 } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
+/*!
+THIS`(v, n)` truncates `v`, keeping only the _most_ significant `n` bits.
+ */
+val truncateLSB = {
+  ocaml: "vector_truncateLSB",
+  lem: "vector_truncateLSB",
+  coq: "vector_truncateLSB",
+  c: "sail_truncateLSB"
+} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
+
 val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit)
 
 function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len)