summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64')
-rw-r--r--aarch64/aarch64_extras.lem2
-rw-r--r--aarch64/no_vector/spec.sail46
-rwxr-xr-xaarch64/prelude.sail81
3 files changed, 70 insertions, 59 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index d22ece00..b662e230 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -78,7 +78,7 @@ val write_ram : forall 'rv 'e.
integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e
let write_ram addrsize size hexRAM address value =
write_mem_ea Write_plain address size >>
- write_mem_val value >>= fun _ ->
+ write_mem Write_plain address size value >>= fun _ ->
return ()
val read_ram : forall 'rv 'e.
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index c91da297..149ddcd9 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -742,21 +742,21 @@ val __UNKNOWN_MemOp : unit -> MemOp
function __UNKNOWN_MemOp () = return(MemOp_LOAD)
-let MemHint_RWA : vector(2, dec, bit) = 0b11
+let MemHint_RWA : bits(2) = 0b11
-let MemHint_RA : vector(2, dec, bit) = 0b10
+let MemHint_RA : bits(2) = 0b10
-let MemHint_No : vector(2, dec, bit) = 0b00
+let MemHint_No : bits(2) = 0b00
val __UNKNOWN_MemBarrierOp : unit -> MemBarrierOp
function __UNKNOWN_MemBarrierOp () = return(MemBarrierOp_DSB)
-let MemAttr_WT : vector(2, dec, bit) = 0b10
+let MemAttr_WT : bits(2) = 0b10
-let MemAttr_WB : vector(2, dec, bit) = 0b11
+let MemAttr_WB : bits(2) = 0b11
-let MemAttr_NC : vector(2, dec, bit) = 0b00
+let MemAttr_NC : bits(2) = 0b00
val __UNKNOWN_MemAtomicOp : unit -> MemAtomicOp
@@ -782,23 +782,23 @@ register MAIR_EL2 : bits(64)
register MAIR_EL1 : bits(64)
-let M32_User : vector(5, dec, bit) = 0b10000
+let M32_User : bits(5) = 0b10000
-let M32_Undef : vector(5, dec, bit) = 0b11011
+let M32_Undef : bits(5) = 0b11011
-let M32_System : vector(5, dec, bit) = 0b11111
+let M32_System : bits(5) = 0b11111
-let M32_Svc : vector(5, dec, bit) = 0b10011
+let M32_Svc : bits(5) = 0b10011
-let M32_Monitor : vector(5, dec, bit) = 0b10110
+let M32_Monitor : bits(5) = 0b10110
-let M32_IRQ : vector(5, dec, bit) = 0b10010
+let M32_IRQ : bits(5) = 0b10010
-let M32_Hyp : vector(5, dec, bit) = 0b11010
+let M32_Hyp : bits(5) = 0b11010
-let M32_FIQ : vector(5, dec, bit) = 0b10001
+let M32_FIQ : bits(5) = 0b10001
-let M32_Abort : vector(5, dec, bit) = 0b10111
+let M32_Abort : bits(5) = 0b10111
val __UNKNOWN_LogicalOp : unit -> LogicalOp
@@ -1113,13 +1113,13 @@ register ELR_EL2 : bits(64)
register ELR_EL1 : bits(64)
-let EL3 : vector(2, dec, bit) = 0b11
+let EL3 : bits(2) = 0b11
-let EL2 : vector(2, dec, bit) = 0b10
+let EL2 : bits(2) = 0b10
-let EL1 : vector(2, dec, bit) = 0b01
+let EL1 : bits(2) = 0b01
-let EL0 : vector(2, dec, bit) = 0b00
+let EL0 : bits(2) = 0b00
register EDSCR : bits(32)
@@ -1149,13 +1149,13 @@ function DecodeRegExtend op = match op {
0b111 => return(ExtendType_SXTX)
}
-let DebugHalt_Watchpoint : vector(6, dec, bit) = 0b101011
+let DebugHalt_Watchpoint : bits(6) = 0b101011
-let DebugHalt_HaltInstruction : vector(6, dec, bit) = 0b101111
+let DebugHalt_HaltInstruction : bits(6) = 0b101111
-let DebugHalt_Breakpoint : vector(6, dec, bit) = 0b000111
+let DebugHalt_Breakpoint : bits(6) = 0b000111
-let DebugException_VectorCatch : vector(4, dec, bit) = 0x5
+let DebugException_VectorCatch : bits(4) = 0x5
val DataSynchronizationBarrier : (MBReqDomain, MBReqTypes) -> unit
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 431ad1f7..7bf0d9f9 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -2,15 +2,14 @@ default Order dec
$include <smt.sail>
$include <arith.sail>
-// $include <trace.sail>
-type bits ('n : Int) = vector('n, dec, bit)
+type bits ('n : Int) = bitvector('n, dec)
-val eq_vec = {ocaml: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-val eq_string = {ocaml: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
+val eq_string = {ocaml: "eq_string", interpreter: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
-val eq_real = {ocaml: "eq_real", lem: "eq", c: "eq_real", coq: "Reqb"} : (real, real) -> bool
+val eq_real = {ocaml: "eq_real", interpreter: "eq_real", lem: "eq", c: "eq_real", coq: "Reqb"} : (real, real) -> bool
val eq_anything = {
ocaml: "(fun (x, y) -> x = y)",
@@ -21,8 +20,8 @@ val eq_anything = {
} : forall ('a : Type). ('a, 'a) -> bool
val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
-val vector_length = {ocaml: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
-val list_length = {ocaml: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int
+val vector_length = {ocaml: "length", interpreter: "length", lem: "length_list", c: "length", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
+val list_length = {ocaml: "length", interpreter: "length", lem: "length_list", c: "length", coq: "length_list"} : forall ('a : Type). list('a) -> int
overload length = {bitvector_length, vector_length, list_length}
@@ -30,6 +29,7 @@ overload operator == = {eq_vec, eq_string, eq_real, eq_anything}
val vector_subrange_A = {
ocaml: "subrange",
+ interpreter: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange",
coq: "subrange_vec_dec"
@@ -38,6 +38,7 @@ val vector_subrange_A = {
val vector_subrange_B = {
ocaml: "subrange",
+ interpreter: "subrange",
lem: "subrange_vec_dec",
c: "vector_subrange"
} : forall ('n : Int) ('m : Int) ('o : Int).
@@ -47,6 +48,7 @@ overload vector_subrange = {vector_subrange_A, vector_subrange_B}
val bitvector_access_A = {
ocaml: "access",
+ interpreter: "access",
lem: "access_vec_dec",
c: "vector_access",
coq: "access_vec_dec"
@@ -54,6 +56,7 @@ val bitvector_access_A = {
val bitvector_access_B = {
ocaml: "access",
+ interpreter: "access",
lem: "access_vec_dec",
c: "vector_access",
coq: "access_vec_dec"
@@ -61,6 +64,7 @@ val bitvector_access_B = {
val vector_access_A = {
ocaml: "access",
+ interpreter: "access",
lem: "access_list_dec",
c: "vector_access",
coq: "vec_access_dec"
@@ -68,22 +72,24 @@ val vector_access_A = {
val vector_access_B = {
ocaml: "access",
+ interpreter: "access",
lem: "access_list_dec",
c: "vector_access"
} : forall ('n : Int) ('a : Type). (vector('n, dec, 'a), int) -> 'a
overload vector_access = {bitvector_access_A, bitvector_access_B, vector_access_A, vector_access_B}
-val bitvector_update_B = {ocaml: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n.
+val bitvector_update_B = {ocaml: "update", interpreter: "update", lem: "update_vec_dec", c: "vector_update", coq: "update_vec_dec"} : forall 'n.
(bits('n), int, bit) -> bits('n)
-val vector_update_B = {ocaml: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
+val vector_update_B = {ocaml: "update", interpreter: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
(vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
overload vector_update = {bitvector_update_B, vector_update_B}
val vector_update_subrange = {
ocaml: "update_subrange",
+ interpreter: "update_subrange",
lem: "update_subrange_vec_dec",
c: "vector_update_subrange",
coq: "update_subrange_vec_dec"
@@ -92,16 +98,17 @@ val vector_update_subrange = {
val vcons : forall ('n : Int) ('a : Type).
('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
-val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
+val bitvector_concat = {ocaml: "append", interpreter: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int).
(bits('n), bits('m)) -> bits('n + 'm)
-val vector_concat = {ocaml: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
+val vector_concat = {ocaml: "append", interpreter: "append", lem: "append_list", coq: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type).
(vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
overload append = {bitvector_concat, vector_concat}
val not_vec = {
ocaml: "not_vec",
+ interpreter: "not_vec",
lem: "not_vec",
c: "not_bits",
coq: "not_vec"
@@ -119,7 +126,7 @@ function neq_anything (x, y) = not_bool(x == y)
overload operator != = {neq_vec, neq_anything}
-val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec", interpreter: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -127,7 +134,7 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys)
overload operator & = {and_vec}
-val builtin_or_vec = {ocaml: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec", interpreter: "or_vec", c: "or_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n)
val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -194,7 +201,7 @@ val putchar = {
coq: "putchar"
} : int -> unit
-val concat_str = {ocaml: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string
+val concat_str = {ocaml: "concat_str", interpreter: "concat_str", lem: "stringAppend", c: "concat_str", coq: "String.append"} : (string, string) -> string
val DecStr = "dec_str" : int -> string
@@ -208,6 +215,7 @@ val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
val xor_vec = {
ocaml: "xor_vec",
+ interpreter: "xor_vec",
lem: "xor_vec",
c: "xor_bits",
coq: "xor_vec"
@@ -215,12 +223,13 @@ val xor_vec = {
val int_power = {lem: "pow"} : (int, int) -> int
-val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power", coq: "powerRZ"} : (real, int) -> real
+val real_power = {ocaml: "real_power", interpreter: "real_power", lem: "realPowInteger", c: "real_power", coq: "powerRZ"} : (real, int) -> real
overload operator ^ = {xor_vec, int_power, real_power}
val add_vec = {
ocaml: "add_vec",
+ interpreter: "add_vec",
lem: "add_vec",
c: "add_bits",
coq: "add_vec"
@@ -228,12 +237,13 @@ val add_vec = {
val add_vec_int = {
ocaml: "add_vec_int",
+ interpreter: "add_vec_int",
lem: "add_vec_int",
c: "add_bits_int",
coq: "add_vec_int"
} : forall 'n. (bits('n), int) -> bits('n)
-val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real", coq: "Rplus"} : (real, real) -> real
+val add_real = {ocaml: "add_real", interpreter: "add_real", lem: "realAdd", c: "add_real", coq: "Rplus"} : (real, real) -> real
overload operator + = {add_vec, add_vec_int, add_real}
@@ -241,64 +251,65 @@ val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) ->
val sub_vec_int = {
ocaml: "sub_vec_int",
+ interpreter: "sub_vec_int",
lem: "sub_vec_int",
c: "sub_bits_int",
coq: "sub_vec_int"
} : forall 'n. (bits('n), int) -> bits('n)
-val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real", coq: "Rminus"} : (real, real) -> real
+val sub_real = {ocaml: "sub_real", interpreter: "sub_real", lem: "realMinus", c: "sub_real", coq: "Rminus"} : (real, real) -> real
-val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real", coq: "Ropp"} : real -> real
+val negate_real = {ocaml: "negate_real", interpreter: "negate_real", lem: "realNegate", c: "neg_real", coq: "Ropp"} : real -> real
overload operator - = {sub_vec, sub_vec_int, sub_real}
overload negate = {negate_real}
-val mult_real = {ocaml: "mult_real", lem: "realMult", c: "mult_real", coq: "Rmult"} : (real, real) -> real
+val mult_real = {ocaml: "mult_real", interpreter: "mult_real", lem: "realMult", c: "mult_real", coq: "Rmult"} : (real, real) -> real
overload operator * = {mult_real}
-val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : real -> real
+val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : real -> real
-val gteq_real = {ocaml: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
+val gteq_real = {ocaml: "gteq_real", interpreter: "gteq_real", lem: "gteq", c: "gteq_real", coq: "gteq_real"} : (real, real) -> bool
overload operator >= = {gteq_real}
-val lteq_real = {ocaml: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
+val lteq_real = {ocaml: "lteq_real", interpreter: "lteq_real", lem: "lteq", c: "lteq_real", coq: "lteq_real"} : (real, real) -> bool
overload operator <= = {lteq_real}
-val gt_real = {ocaml: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
+val gt_real = {ocaml: "gt_real", interpreter: "gt_real", lem: "gt", c: "gt_real", coq: "gt_real"} : (real, real) -> bool
overload operator > = {gt_real}
-val lt_real = {ocaml: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
+val lt_real = {ocaml: "lt_real", interpreter: "lt_real", lem: "lt", c: "lt_real", coq: "lt_real"} : (real, real) -> bool
overload operator < = {lt_real}
-val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
+val RoundDown = {ocaml: "round_down", interpreter: "round_down", lem: "realFloor", c: "round_down", coq: "Zfloor"} : real -> int
-val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up", coq: "Zceil"} : real -> int
+val RoundUp = {ocaml: "round_up", interpreter: "round_up", lem: "realCeiling", c: "round_up", coq: "Zceil"} : real -> int
val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real
overload abs = {abs_atom, abs_real}
-val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
+val quotient_real = {ocaml: "quotient_real", interpreter: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
overload operator / = {ediv_int, quotient_real}
overload div = {ediv_int}
overload operator % = {emod_int}
-val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real
+val Real = {ocaml: "to_real", interpreter: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real
-val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
+val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
-val min_int = {ocaml: "min_int", lem: "min", c: "min_int", coq: "Z.min"} : (int, int) -> int
+val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", c: "min_int", coq: "Z.min"} : (int, int) -> int
-val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
+val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
-val max_int = {ocaml: "max_int", lem: "max", c: "max_int", coq: "Z.max"} : (int, int) -> int
+val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int", coq: "Z.max"} : (int, int) -> int
overload min = {min_nat, min_int}
@@ -355,11 +366,11 @@ union option ('a : Type) = {
}
*/
-val __SleepRequest = {ocaml: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {rreg, undef}
+val __SleepRequest = {ocaml: "sleep_request", interpreter: "sleep_request", lem: "sleep_request", smt: "sleep_request", interpreter: "sleep_request", c: "sleep_request"}: unit -> unit effect {rreg, undef}
-val __WakeupRequest = {ocaml: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {rreg, undef}
+val __WakeupRequest = {ocaml: "wakeup_request", interpreter: "wakeup_request", lem: "wakeup_request", smt: "wakeup_request", interpreter: "wakeup_request", c: "wakeup_request"}: unit -> unit effect {rreg, undef}
-val __Sleeping = {ocaml: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {rreg, undef}
+val __Sleeping = {ocaml: "sleeping", interpreter: "sleeping", lem: "sleeping", smt: "sleeping", interpreter: "sleeping", c: "sleeping"}: unit -> bool effect {rreg, undef}
val __GetVerbosity = {c: "sail_get_verbosity"}: unit -> bits(64) effect {rreg, undef}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:32:36 +0000