From 0a1a5a0e0cd455bfc194f8cc098bbcc2ca5c4f2a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Frenot?= <leon.frenot@ens-lyon.fr>
Date: Fri, 6 Dec 2024 16:06:07 +0000
Subject: [PATCH] Adding features

---
 lib/arith.sail                            |  9 +++----
 src/bin/dune                              |  8 ++++++-
 src/sail_lean_backend/Sail/bitvec.lean    | 25 +++++++++++++++++++
 src/sail_lean_backend/Sail/registers.lean | 29 +++++++++++++++++++++++
 src/sail_lean_backend/Sail/sail.lean      | 27 ++-------------------
 5 files changed, 68 insertions(+), 30 deletions(-)
 create mode 100644 src/sail_lean_backend/Sail/bitvec.lean
 create mode 100644 src/sail_lean_backend/Sail/registers.lean

diff --git a/lib/arith.sail b/lib/arith.sail
index 7c3342bdb..46c48ba9b 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -51,19 +51,19 @@ $include <flow.sail>
 
 // ***** Addition *****
 
-val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : forall 'n 'm.
+val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", lean: "HAdd.hAdd", _: "add_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 
-val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add",  _: "add_int"} : (int, int) -> int
+val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add", lean: "HAdd.hAdd",  _: "add_int"} : (int, int) -> int
 
 overload operator + = {add_atom, add_int}
 
 // ***** Subtraction *****
 
-val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : forall 'n 'm.
+val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "HSub.hSub", _: "sub_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n - 'm)
 
-val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int
+val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", lean: "HSub.hSub", _: "sub_int"} : (int, int) -> int
 
 overload operator - = {sub_atom, sub_int}
 
@@ -71,6 +71,7 @@ val sub_nat = pure {
   ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
   lem: "integerMinus",
   coq: "Z.sub",
+  lean: "HSub.hSub",
   _: "sub_nat"
 } : (nat, nat) -> nat
 
diff --git a/src/bin/dune b/src/bin/dune
index 59d9f36af..dfb366bc7 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -242,4 +242,10 @@
    src/gen_lib/sail2_values.lem)
   (%{workspace_root}/src/sail_lean_backend/Sail/sail.lean
    as
-   src/sail_lean_backend/Sail/sail.lean)))
+   src/sail_lean_backend/Sail/sail.lean)
+   (%{workspace_root}/src/sail_lean_backend/Sail/bitvec.lean
+   as
+   src/sail_lean_backend/Sail/bitvec.lean)
+   (%{workspace_root}/src/sail_lean_backend/Sail/registers.lean
+   as
+   src/sail_lean_backend/Sail/registers.lean)))
diff --git a/src/sail_lean_backend/Sail/bitvec.lean b/src/sail_lean_backend/Sail/bitvec.lean
new file mode 100644
index 000000000..7a0ec1e06
--- /dev/null
+++ b/src/sail_lean_backend/Sail/bitvec.lean
@@ -0,0 +1,25 @@
+namespace Sail
+namespace BitVec
+
+def length {w: Nat} (_: BitVec w): Nat := w
+
+def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.signExtend w'
+
+def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.zeroExtend w'
+
+def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.truncate w'
+
+def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+  x.extractLsb' 0 w'
+
+def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
+  x.extractLsb hi lo
+
+def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
+  sorry
+
+end BitVec
+end Sail
diff --git a/src/sail_lean_backend/Sail/registers.lean b/src/sail_lean_backend/Sail/registers.lean
new file mode 100644
index 000000000..26d122546
--- /dev/null
+++ b/src/sail_lean_backend/Sail/registers.lean
@@ -0,0 +1,29 @@
+
+inductive register where
+  | Register : String → /- name -/
+               Nat → /- length -/
+               Nat → /- start index -/
+               Bool → /- is increasing -/
+               List register_field_index
+               → register
+  | UndefinedRegister : Nat → register /- length -/
+  | RegisterPair : register → register → register
+
+structure register_ref (regstate regval a: Type) where
+  name: String
+  read_from: regstate -> a
+  write_to: a -> regstate -> regstate
+  of_regval: regval -> Option a
+  regval_of: a -> regval
+
+def read_reg {s rv a e} (reg : register_ref s rv a) : Monad e :=
+  let k v :=
+    match reg.of_regval v with
+      | some v => some v
+      | none => none
+  Read_reg reg.(name) k.
+
+def reg_deref {s rv a e} := @read_reg s rv a e.
+
+def write_reg {s rv a e} (reg : register_ref s rv a) (v : a) : monad rv unit e :=
+ Write_reg reg.(name) (reg.(regval_of) v) (Done tt).
diff --git a/src/sail_lean_backend/Sail/sail.lean b/src/sail_lean_backend/Sail/sail.lean
index 7a0ec1e06..5b93ceeea 100644
--- a/src/sail_lean_backend/Sail/sail.lean
+++ b/src/sail_lean_backend/Sail/sail.lean
@@ -1,25 +1,2 @@
-namespace Sail
-namespace BitVec
-
-def length {w: Nat} (_: BitVec w): Nat := w
-
-def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.signExtend w'
-
-def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.zeroExtend w'
-
-def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.truncate w'
-
-def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.extractLsb' 0 w'
-
-def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
-  x.extractLsb hi lo
-
-def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
-  sorry
-
-end BitVec
-end Sail
+import Sail.bitvec
+import Sail.registers