Make more updates for the Lean backend

4 files changed, 113 insertions, 61 deletions

diff --git a/Makefile b/Makefile
index c6fb7b46..26daadac 100644
--- a/Makefile
+++ b/Makefile
@@ -237,18 +237,29 @@ tcoqp-%:
 	$(AENEAS_CMD)
 
 .PHONY: tlean-%
-tlean-%: OPTIONS += -backend lean -test-trans-units
+# TODO: add  -test-trans-units once we remove all the sorry from Primitives.lean
+tlean-%: OPTIONS += -backend lean
 tlean-%: BACKEND_SUBDIR := lean
 tlean-%:
 	$(AENEAS_CMD)
 
+
+
 # "p" stands for "Polonius"
 .PHONY: tleanp-%
-tleanp-%: OPTIONS += -backend lean -test-trans-units
+
+# TODO: for now we don't extract the betree for Lean because we need to implement
+# proper support for the proofs of termination for the mutually recursive functions.
+tleanp-betree_main:
+	echo "Ignoring Lean betree"
+
+# TODO: add  -test-trans-units once we remove all the sorry from Primitives.lean
+tleanp-%: OPTIONS += -backend lean
 tleanp-%: BACKEND_SUBDIR := lean
 tleanp-%:
 	$(AENEAS_CMD)
 
+
 # Nix
 .PHONY: nix
 nix: nix-aeneas-tests nix-aeneas-verify-fstar nix-aeneas-verify-coq
diff --git a/backends/lean/Primitives.lean b/backends/lean/Primitives.lean
index e5634bfe..034f41b2 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Primitives.lean
@@ -112,17 +112,13 @@ macro "let" e:term " <-- " f:term : doElem =>
 -- MACHINE INTEGERS --
 ----------------------
 
--- NOTE: we reuse the fixed-width integer types from prelude.lean: UInt8, ...,
--- USize. They are generally defined in an idiomatic style, except that there is
--- not a single type class to rule them all (more on that below). The absence of
--- type class is intentional, and allows the Lean compiler to efficiently map
--- them to machine integers during compilation.
-
--- USize is designed properly: you cannot reduce `getNumBits` using the
--- simplifier, meaning that proofs do not depend on the compile-time value of
--- USize.size. (Lean assumes 32 or 64-bit platforms, and Rust doesn't really
--- support, at least officially, 16-bit microcontrollers, so this seems like a
--- fine design decision for now.)
+-- We redefine our machine integers types.
+
+-- For Isize/Usize, we reuse `getNumBits` from `USize`. You cannot reduce `getNumBits`
+-- using the simplifier, meaning that proofs do not depend on the compile-time value of
+-- USize.size. (Lean assumes 32 or 64-bit platforms, and Rust doesn't really support, at
+-- least officially, 16-bit microcontrollers, so this seems like a fine design decision
+-- for now.)
 
 -- Note from Chris Bailey: "If there's more than one salient property of your
 -- definition then the subtyping strategy might get messy, and the property part
@@ -134,20 +130,6 @@ macro "let" e:term " <-- " f:term : doElem =>
 -- Machine integer constants, done via `ofNatCore`, which requires a proof that
 -- the `Nat` fits within the desired integer type. We provide a custom tactic.
 
-syntax "intlit" : tactic
-
-macro_rules
-  | `(tactic| intlit) => `(tactic|
-    match USize.size, usize_size_eq with
-    | _, Or.inl rfl => decide
-    | _, Or.inr rfl => decide)
-
--- This is how the macro is expected to be used
-#eval USize.ofNatCore 0 (by intlit)
-
--- Also works for other integer types (at the expense of a needless disjunction)
-#eval UInt32.ofNatCore 0 (by intlit)
-
 open System.Platform.getNumBits
 
 -- TODO: is there a way of only importing System.Platform.getNumBits?
@@ -264,11 +246,19 @@ def Scalar.cMax (ty : ScalarTy) : Int :=
   | .Usize => U32.max
   | _ => Scalar.max ty
 
+theorem Scalar.cMin_bound ty : Scalar.min ty <= Scalar.cMin ty := by sorry
+theorem Scalar.cMax_bound ty : Scalar.min ty <= Scalar.cMin ty := by sorry
+
 structure Scalar (ty : ScalarTy) where
   val : Int
   hmin : Scalar.min ty <= val
   hmax : val <= Scalar.max ty
 
+theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
+  Scalar.cMin ty <= x && x <= Scalar.cMax ty ->
+  (decide (Scalar.min ty ≤ x) && decide (x ≤ Scalar.max ty)) = true
+  := by sorry
+
 def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
   (hmin : Scalar.min ty <= x) (hmax : x <= Scalar.max ty) : Scalar ty :=
   { val := x, hmin := hmin, hmax := hmax }
@@ -445,6 +435,12 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 
 def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
 
+-- Tactic to prove that integers are in bounds
+syntax "intlit" : tactic
+
+macro_rules
+  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices ; decide)
+
 -- -- We now define a type class that subsumes the various machine integer types, so
 -- -- as to write a concise definition for scalar_cast, rather than exhaustively
 -- -- enumerating all of the possible pairs. We remark that Rust has sane semantics
@@ -497,14 +493,22 @@ def vec_push_back (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
   else
     fail maximumSizeExceeded
 
-def vec_insert_fwd (α : Type u) (v: Vec α) (i: USize) (_: α): Result Unit :=
+def vec_insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def vec_insert_back (α : Type u) (v: Vec α) (i: USize) (x: α): Result (Vec α) :=
+def vec_insert_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
   if i.val < List.length v.val then
+    -- TODO: maybe we should redefine a list library which uses integers
+    -- (instead of natural numbers)
+    let i : Nat :=
+      match i.val with
+      | .ofNat n => n
+      | .negSucc n => by sorry -- TODO: we can't get here
+    let isLt: i < USize.size := by sorry
+    let i : Fin USize.size := { val := i, isLt := isLt }
     .ret ⟨ List.set v.val i.val x, by
       have h: List.length v.val <= Usize.max := v.property
       rewrite [ List.length_set v.val i.val x ]
@@ -513,26 +517,46 @@ def vec_insert_back (α : Type u) (v: Vec α) (i: USize) (x: α): Result (Vec α
   else
     .fail arrayOutOfBounds
 
-def vec_index_fwd (α : Type u) (v: Vec α) (i: USize): Result α :=
-  if h: i.val < List.length v.val then
+def vec_index_fwd (α : Type u) (v: Vec α) (i: Usize): Result α :=
+  if i.val < List.length v.val then
+    let i : Nat :=
+      match i.val with
+      | .ofNat n => n
+      | .negSucc n => by sorry -- TODO: we can't get here
+    let isLt: i < USize.size := by sorry
+    let i : Fin USize.size := { val := i, isLt := isLt }
+    let h: i < List.length v.val := by sorry
     .ret (List.get v.val ⟨i.val, h⟩)
   else
     .fail arrayOutOfBounds
 
-def vec_index_back (α : Type u) (v: Vec α) (i: USize) (_: α): Result Unit :=
+def vec_index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def vec_index_mut_fwd (α : Type u) (v: Vec α) (i: USize): Result α :=
-  if h: i.val < List.length v.val then
+def vec_index_mut_fwd (α : Type u) (v: Vec α) (i: Usize): Result α :=
+  if i.val < List.length v.val then
+    let i : Nat :=
+      match i.val with
+      | .ofNat n => n
+      | .negSucc n => by sorry -- TODO: we can't get here
+    let isLt: i < USize.size := by sorry
+    let i : Fin USize.size := { val := i, isLt := isLt }
+    let h: i < List.length v.val := by sorry
     .ret (List.get v.val ⟨i.val, h⟩)
   else
     .fail arrayOutOfBounds
 
-def vec_index_mut_back (α : Type u) (v: Vec α) (i: USize) (x: α): Result (Vec α) :=
+def vec_index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
   if i.val < List.length v.val then
+    let i : Nat :=
+      match i.val with
+      | .ofNat n => n
+      | .negSucc n => by sorry -- TODO: we can't get here
+    let isLt: i < USize.size := by sorry
+    let i : Fin USize.size := { val := i, isLt := isLt }
     .ret ⟨ List.set v.val i.val x, by
       have h: List.length v.val <= Usize.max := v.property
       rewrite [ List.length_set v.val i.val x ]
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index e5710394..03c256ec 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -197,14 +197,25 @@ let assumed_adts () : (assumed_ty * string) list =
             (Char.uppercase_ascii s.[0])
             (String.sub s 1 (String.length s - 1)) )
       else (t, s))
-    [
-      (State, "state");
-      (Result, "result");
-      (Error, "error");
-      (Fuel, "nat");
-      (Option, "option");
-      (Vec, "vec");
-    ]
+    (match !backend with
+    | Lean ->
+        [
+          (State, "State");
+          (Result, "Result");
+          (Error, "Error");
+          (Fuel, "Nat");
+          (Option, "Option");
+          (Vec, "Vec");
+        ]
+    | Coq | FStar ->
+        [
+          (State, "state");
+          (Result, "result");
+          (Error, "error");
+          (Fuel, "nat");
+          (Option, "option");
+          (Vec, "vec");
+        ])
 
 let assumed_structs : (assumed_ty * string) list = []
 
@@ -1004,7 +1015,9 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       F.pp_print_string fmt (unit_name ()))
     else if !backend = Lean && fields = [] then ()
-    else if (not is_rec) || !backend <> Coq then (
+      (* If the definition is recursive, we may need to extract it as an inductive
+         (instead of a record) *)
+    else if (not is_rec) || (!backend <> Coq && !backend <> Lean) then (
       if !backend <> Lean then F.pp_print_space fmt ();
       (* If Coq: print the constructor name *)
       (* TODO: remove superfluous test not is_rec below *)
@@ -1044,9 +1057,9 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt "}"))
     else (
-      (* We extract for Coq, and we have a recursive record, or a record in
+      (* We extract for Coq or Lean, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type *)
-      assert (is_rec && !backend = Coq);
+      assert (is_rec && (!backend = Coq || !backend = Lean));
       let with_opaque_pre = false in
       let cons_name = ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx in
       let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
@@ -2224,7 +2237,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
-(** Extract templates for the [termination_by] and [decreases_by] clauses of a
+(** Extract templates for the [termination_by] and [decreasing_by] clauses of a
     recursive function definition.
 
     For Lean only.
@@ -2490,8 +2503,6 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ());
   (* Close the inner box for the definition *)
   F.pp_close_box fmt ();
-  (* Coq: add a "." *)
-  print_decl_end_delimiter fmt kind;
   (* Termination clause and proof for Lean *)
   if has_decreases_clause && !backend = Lean then (
     let def_body = Option.get def.body in
@@ -2558,6 +2569,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ();
     (* Close the box for the [decreasing by ...] *)
     F.pp_close_box fmt ());
+  (* Add the definition group end delimiter *)
+  print_decl_end_delimiter fmt kind;
   (* Close the outer box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8250f813..409fc5d3 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -716,8 +716,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
 
 let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
     (rust_module_name : string) (module_name : string) (custom_msg : string)
-    ?(custom_variables : string list = []) (custom_imports : string list)
-    (custom_includes : string list) : unit =
+    (custom_imports : string list) (custom_includes : string list) : unit =
   (* Open the file and create the formatter *)
   let out = open_out filename in
   let fmt = Format.formatter_of_out_channel out in
@@ -770,10 +769,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
-      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes;
-      if custom_variables <> [] then (
-        Printf.fprintf out "\n";
-        List.iter (fun m -> Printf.fprintf out "%s\n" m) custom_variables));
+      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes);
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -1066,6 +1062,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
          extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
        in
        let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
+       let opaque_imported_module =
+         (* In the case of Lean, we declare an interface (a record) containing
+            the opaque definitions, and we leave it to the user to provide an
+            instance of this module.
+
+            TODO: do the same for Coq.
+            TODO: do the same for the type definitions.
+         *)
+         if !Config.backend = Lean then
+           module_name ^ module_delimiter ^ "ExternalFuns"
+         else opaque_module
+       in
        let opaque_config =
          {
            base_gen_config with
@@ -1083,7 +1091,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        in
        extract_file opaque_config gen_ctx opaque_filename crate.A.name
          opaque_module ": opaque function definitions" [] [ types_module ];
-       [ opaque_module ])
+       [ opaque_imported_module ])
      else []
    in
 
@@ -1106,12 +1114,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
        [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
      else []
    in
-   let custom_variables =
-     if has_opaque_funs then [ "section variable (opaque_defs: OpaqueDefs)" ]
-     else []
-   in
    extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
-     ": function definitions" [] ~custom_variables
+     ": function definitions" []
      ([ types_module ] @ opaque_funs_module @ clauses_module))
   else
     let gen_config =