summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-05-09 10:37:49 +0200
committerSon HO2023-06-04 21:44:33 +0200
commit4078f2569b362920a648622be73761cddde8a288 (patch)
treefe60e568cbf782d513e3d5fea9e07b3d6e81c373
parent12dcc49c3199dcd1b2acf4a650a9adc375781306 (diff)
Make more updates for the Lean backend
Diffstat (limited to '')
-rw-r--r--Makefile15
-rw-r--r--backends/lean/Primitives.lean90
-rw-r--r--compiler/Extract.ml41
-rw-r--r--compiler/Translate.ml28
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 =