From 4078f2569b362920a648622be73761cddde8a288 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 9 May 2023 10:37:49 +0200 Subject: Make more updates for the Lean backend --- Makefile | 15 +++++++- backends/lean/Primitives.lean | 90 +++++++++++++++++++++++++++---------------- compiler/Extract.ml | 41 +++++++++++++------- compiler/Translate.ml | 28 ++++++++------ 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 = -- cgit v1.2.3