Define extz/s_vec in Sail for non-prover backends

1 files changed, 8 insertions, 2 deletions

diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 0702b374..1e7fe58f 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -8,9 +8,15 @@ $include <vector_dec.sail>
 
 /* External definitions not in the usual asl prelude */
 
-val extzv = "extz_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extzv = {lem: "extz_vec", coq: "extz_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+function extzv(m, v) = {
+  if m < 'n then truncate(v, m) else sail_zero_extend(v, m)
+}
 
-val extsv = "exts_vec" : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+val extsv = {lem: "exts_vec", coq: "exts_vec"} : forall 'n 'm, 'm >= 0. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure
+function extsv(m, v) = {
+  if m < 'n then truncate(v, m) else sail_sign_extend(v, m)
+}
 
 /* This is generated internally to deal with case splits which reveal the size
    of a bitvector */