checking in in-progress translation of Shaked's handwritten sail1 ARM model to sail2

1 files changed, 36 insertions, 0 deletions

diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
new file mode 100644
index 00000000..75fdc129
--- /dev/null
+++ b/aarch64_small/prelude.sail
@@ -0,0 +1,36 @@
+default Order dec
+
+union option ('a : Type) = {None : unit, Some : 'a}
+
+type bits ('n : Int) = vector('n, dec, bit)
+
+infix 7 >>
+infix 7 <<
+
+val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
+
+
+infix 7 ^^
+
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
+
+
+infix 4 <_s
+infix 4 >=_s
+infix 4 <_u
+infix 4 >=_u
+infix 4 <=_u
+
+val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
+
+function operator <_s  (x, y) = signed(x) < signed(y)
+function operator >=_s (x, y) = signed(x) >= signed(y)
+function operator <_u  (x, y) = unsigned(x) < unsigned(y)
+function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
+function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
\ No newline at end of file