Rules and supporting files for building aarch64_small monomorphised Isabelle

1 files changed, 8 insertions, 0 deletions

diff --git a/aarch64_small/mono-splices/LSR_C.sail b/aarch64_small/mono-splices/LSR_C.sail
new file mode 100644
index 00000000..5fed8ad6
--- /dev/null
+++ b/aarch64_small/mono-splices/LSR_C.sail
@@ -0,0 +1,8 @@
+val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bit) effect pure
+
+function LSR_C (x, shift) = {
+  result : bits('N) = x >> shift;
+  carry_out : bit = if shift > 'N then bitzero else x[shift - 1];
+  return((result, carry_out))
+}