start annotating the arm prelude

Author: javra

aarch64/prelude.sail

@@ -5,23 +5,58 @@ $include <arith.sail>
 
 type bits ('n : Int) = bitvector('n, dec)
 
-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", interpreter: "eq_string", lem: "eq", c: "eq_string", coq: "generic_eq"} : (string, string) -> bool
+val eq_vec = {
+  ocaml: "eq_list",
+  interpreter: "eq_list",
+  lem: "eq_vec",
+  c: "eq_bits",
+  coq: "eq_vec"
+  lean: "BEq.beq"} : forall 'n. (bits('n), bits('n)) -> bool
+
+val eq_string = {
+  ocaml: "eq_string",
+  interpreter: "eq_string",
+  lem: "eq",
+  c: "eq_string",
+  coq: "generic_eq",
+  lean: "BEq.beq"} : (string, string) -> bool
 
-val eq_real = {ocaml: "eq_real", interpreter: "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",
+  lean: "BEq.beq"} : (real, real) -> bool
 
 val eq_anything = {
   ocaml: "(fun (x, y) -> x = y)",
   interpreter: "eq_anything",
   lem: "eq",
   c: "eq_anything",
-  coq: "generic_eq"
+  coq: "generic_eq",
+  lean: "BEq.beq"
 } : forall ('a : Type). ('a, 'a) -> bool
 
-val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
-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
+val bitvector_length = {
+  lean: "BitVec.length",
+  _: "length"} : forall 'n. bits('n) -> atom('n)
+
+val vector_length = {
+  ocaml: "length",
+  interpreter: "length",
+  lem: "length_list",
+  c: "length",
+  coq: "vec_length",
+  lean: "Vector.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",
+  lean: "List.length"} : forall ('a : Type). list('a) -> int
 
 overload length = {bitvector_length, vector_length, list_length}
 
@@ -32,15 +67,17 @@ val vector_subrange_A = {
   interpreter: "subrange",
   lem: "subrange_vec_dec",
   c: "vector_subrange",
-  coq: "subrange_vec_dec"
+  coq: "subrange_vec_dec",
+  lean: "BitVec.extractLsb"
 } : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
 
 val vector_subrange_B = {
   ocaml: "subrange",
   interpreter: "subrange",
   lem: "subrange_vec_dec",
-  c: "vector_subrange"
+  c: "vector_subrange",
+  lean: "BitVec.extractLsb"
 } : forall ('n : Int) ('m : Int) ('o : Int).
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
 
@@ -51,15 +88,17 @@ val bitvector_access_A = {
   interpreter: "access",
   lem: "access_vec_dec",
   c: "vector_access",
-  coq: "access_vec_dec"
+  coq: "access_vec_dec",
+  lean: "BitVec.access"
 } : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. (bits('n), atom('m)) -> bit
 
 val bitvector_access_B = {
   ocaml: "access",
   interpreter: "access",
   lem: "access_vec_dec",
   c: "vector_access",
-  coq: "access_vec_dec"
+  coq: "access_vec_dec",
+  lean: "BitVec.access"
 } : forall ('n : Int). (bits('n), int) -> bit
 
 val vector_access_A = {
@@ -74,12 +113,18 @@ val vector_access_B = {
   ocaml: "access",
   interpreter: "access",
   lem: "access_list_dec",
-  c: "vector_access"
+  c: "vector_access",
+  lean: "GetElem?.getElem!"
 } : 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", interpreter: "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", interpreter: "update", lem: "update_list_dec", c: "vector_update", coq: "vec_update_dec"} : forall 'n ('a : Type).
@@ -98,10 +143,21 @@ 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", interpreter: "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",
+  lean: "HAppend.hAppend"} : forall ('n : Int) ('m : Int).
   (bits('n), bits('m)) -> bits('n + 'm)
 
-val vector_concat = {ocaml: "append", interpreter: "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",
+  lean: "HAppend.hAppend"} : 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}
@@ -111,7 +167,8 @@ val not_vec = {
   interpreter: "not_vec",
   lem: "not_vec",
   c: "not_bits",
-  coq: "not_vec"
+  coq: "not_vec",
+  lean: "Complement.complement"
 } : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
@@ -147,11 +204,13 @@ val UInt = {
   lem: "uint",
   interpreter: "uint",
   c: "sail_unsigned",
-  coq: "uint"
+  coq: "uint",
+  lean: "BitVec.toNat"
 } : forall 'n. bits('n) -> {'m, 0 <= 'm <= 2 ^ 'n - 1. int('m)}
 
 val SInt = {
   c: "sail_signed",
+  lean: "BitVec.toInt",
   _: "sint"
 } : forall 'n. bits('n) -> {'m, (- (2 ^ ('n - 1))) <= 'm <= 2 ^ ('n - 1) - 1. int('m)}
 
@@ -232,58 +291,112 @@ val add_vec = {
   interpreter: "add_vec",
   lem: "add_vec",
   c: "add_bits",
-  coq: "add_vec"
+  coq: "add_vec",
+  lean: "HAdd.hAdd"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_vec_int = {
   ocaml: "add_vec_int",
   interpreter: "add_vec_int",
   lem: "add_vec_int",
   c: "add_bits_int",
-  coq: "add_vec_int"
+  coq: "add_vec_int",
+  lean: "BitVec.addInt"
 } : forall 'n. (bits('n), int) -> bits('n)
 
-val add_real = {ocaml: "add_real", interpreter: "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",
+  lean: "HAdd.hAdd"} : (real, real) -> real
 
 overload operator + = {add_vec, add_vec_int, add_real}
 
-val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val sub_vec = {
+  c: "sub_bits",
+  lean: "HSub.hSub",
+  _: "sub_vec"} : forall 'n. (bits('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"
+  coq: "sub_vec_int",
+  lean: "BitVec.subInt"
 } : forall 'n. (bits('n), int) -> bits('n)
 
-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", interpreter: "negate_real", lem: "realNegate", c: "neg_real", coq: "Ropp"} : real -> real
+val sub_real = {
+  ocaml: "sub_real",
+  interpreter: "sub_real",
+  lem: "realMinus",
+  c: "sub_real",
+  lean: "HSub.hSub",
+  coq: "Rminus"} : (real, real) -> real
+
+val negate_real = {
+  ocaml: "negate_real",
+  interpreter: "negate_real",
+  lem: "realNegate",
+  c: "neg_real",
+  lean: "Neg.neg",
+  coq: "Ropp"} : real -> real
 
 overload operator - = {sub_vec, sub_vec_int, sub_real}
 
 overload negate = {negate_real}
 
-val mult_real = {ocaml: "mult_real", interpreter: "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",
+  lean: "HMul.hMul",
+  coq: "Rmult"} : (real, real) -> real
 
 overload operator * = {mult_real}
 
 val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt", c: "sqrt_real", coq: "sqrt"} : real -> real
 
-val gteq_real = {ocaml: "gteq_real", interpreter: "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",
+  lean: "_lean_ge"} : (real, real) -> bool
 
 overload operator >= = {gteq_real}
 
-val lteq_real = {ocaml: "lteq_real", interpreter: "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",
+  lean: "_lean_ge"} : (real, real) -> bool
 
 overload operator <= = {lteq_real}
 
-val gt_real = {ocaml: "gt_real", interpreter: "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",
+  lean: "_lean_gt"} : (real, real) -> bool
 
 overload operator > = {gt_real}
 
-val lt_real = {ocaml: "lt_real", interpreter: "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",
+  lean: "_lean_lt"} : (real, real) -> bool
 
 overload operator < = {lt_real}