Add a Tactics module in the bootstrapped plugin to make use of ERASEcast

Author: mattam82

.vscode/rocq-verified-extraction-main.code-workspace

@@ -4,5 +4,16 @@
 			"path": ".."
 		}
 	],
-	"settings": {}
+	"settings": {
+		"coqtop.args": [
+			"-Q", "theories", "Malfunction",
+			"-Q", "examples", "Malfunction.Examples",
+			"-Q", "plugin/plugin", "Malfunction.Plugin",
+			"-Q", "plugin/plugin-bootstrap", "VerifiedExtraction",
+			"-I", "plugin",
+			"-Q", "benchmarks", "VerifiedExtraction.Benchmarks"
+		],
+		"coqtop.binPath": "_opam/bin",
+		"coqtop.coqidetopExe": "coqidetop"
+	}
 }

examples/erase-conv/fib.v

@@ -0,0 +1,24 @@
+From VerifiedExtraction Require Import Loader.
+
+Set Verified Extraction Build Directory "_build".
+
+(* Set Debug "verified-extraction". *)
+
+Definition foo := (@eq_refl bool false <<<: (false = negb true)).
+
+From Stdlib Require Import Arith.
+
+Fixpoint fib (n : nat) := 
+  match n with
+  | 0 => 0
+  | 1 => 1
+  | S (S n as m) => fib m + fib n
+  end.
+
+Time Definition fib2 := Eval compute in fib 2.
+Check (@eq_refl nat fib2 <<<: (fib2 = fib 2)).
+
+Time Definition fib23 := Eval compute in fib 23.
+(* > 1.5s *)
+Time Definition efib23 := (@eq_refl nat fib23 <<<: (fib23 = fib 23)).
+(* Runtime is lower (< 1s ) even with compilation + dynlink + reification *)

lib/rocq_verified_extraction_plugin/lib/verified_extraction.ml

@@ -334,8 +334,9 @@ let push_line buf line =
 let string_of_buffer buf = Bytes.to_string (Buffer.to_bytes buf)
 
 let execute cmd =
-  debug Pp.(fun () -> str "Executing: " ++ str cmd ++ str " in environemt: " ++ 
-    prlist_with_sep spc str (Array.to_list (Unix.environment ())));
+  debug Pp.(fun () -> str "Executing: " ++ str cmd);
+   (* ++ str " in environemt: " ++  *)
+    (* prlist_with_sep spc str (Array.to_list (Unix.environment ()))); *)
   let (stdout, stdin, stderr) = Unix.open_process_full cmd (Unix.environment ()) in
   let continue = ref true in
   let outbuf, errbuf = Buffer.create 100, Buffer.create 100 in
@@ -575,7 +576,7 @@ struct
       let cstrs = apply_reordering qhd m cstrs in
       if Obj.is_block v then
         let ord = Obj.tag v in
-        let () = debug Pp.(fun () -> str (Printf.sprintf "Reifying constructor block of tag %i" ord)) in
+        (* let () = debug Pp.(fun () -> str (Printf.sprintf "Reifying constructor block of tag %i" ord)) in *)
         let coqidx = 
           try find_nth_non_constant ord cstrs 
           with Not_found -> ill_formed env sigma ty
@@ -585,28 +586,28 @@ struct
         let ctx = EConstr.Vars.smash_rel_context cstr.cs_args in
         let vargs = List.init (List.length ctx) (Obj.field v) in
         let args' = List.map2 (fun decl v -> 
-          let argty = check_reifyable_value env sigma 
+          let argty = check_reifyable_value_type env sigma 
           (Context.Rel.Declaration.get_type decl) in
           aux argty v) (List.rev ctx) vargs in
         Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args')
       else (* Constant constructor *)
         let ord = (Obj.magic v : int) in
-        let () = debug Pp.(fun () -> str @@ Printf.sprintf "Reifying constant constructor: %i" ord) in
+        (* let () = debug Pp.(fun () -> str @@ Printf.sprintf "Reifying constant constructor: %i" ord) in *)
         let coqidx = 
           try find_nth_constant ord cstrs 
           with Not_found -> ill_formed env sigma ty 
         in
         let coqidx = find_reverse_mapping qhd m coqidx in
-        let () = debug Pp.(fun () -> str @@ Printf.sprintf "Reifying constant constructor: %i is %i in Rocq" ord coqidx) in
+        (* let () = debug Pp.(fun () -> str @@ Printf.sprintf "Reifying constant constructor: %i is %i in Rocq" ord coqidx) in *)
         Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params
     | IsPrimitive (c, u, _args) -> 
       if Environ.is_array_type env c then 
-        CErrors.user_err Pp.(str "Primitive arrays are not supported yet in MetaRocq r Extractioneification")
+        CErrors.user_err Pp.(str "Primitive arrays are not supported yet in MetaRocq reification")
       else if Environ.is_float64_type env c then
         Constr.mkFloat (Obj.magic v)
       else if Environ.is_int63_type env c then
         Constr.mkInt (Obj.magic v)
-      else CErrors.user_err Pp.(str "Unsupported primitive type in MetaRocq r Extractioneification")
+      else CErrors.user_err Pp.(str "Unsupported primitive type in MetaRocq reification")
     in aux ty v
 
   let reify opts env sigma tyinfo result =
@@ -647,28 +648,32 @@ let compile opts names tyinfos fname =
         Printf.sprintf "%s cmx %s -shared -package %s %s" malfunction optimize 
           (String.concat "," packages) fname
       in
-      let _out, _err = execute opts compile_cmd in (* we now have fname . cmx *)
+      let _out, _err = time opts Pp.(str"Malfunction Compilation") (execute opts) compile_cmd in (* we now have fname . cmx *)
       let cmxfile =  Filename.chop_extension fname ^ ".cmx" in
       let cmxsfile = Filename.chop_extension fname ^ ".cmxs" in
       (* Build the shared library *)
       let link_cmd = 
         Printf.sprintf "%s opt -shared -package %s -o %s %s" ocamlfind 
          (String.concat "," packages) cmxsfile cmxfile
       in
-      let _out, _err = execute opts link_cmd in
+      let _out, _err = time opts Pp.(str "Compilation to a dynamically loadable library") (execute opts) link_cmd in
       Some (SharedLib (names, tyinfos, cmxsfile))
     | Standalone link_coq -> 
       let output = Filename.chop_extension fname in
       let flags, packages =
         if link_coq then 
-          "-thread -linkpkg", String.concat "," (statically_linked_pkgs @ packages)
-        else "-thread -linkpkg", String.concat "," packages
+          "-thread -linkpkg", statically_linked_pkgs @ packages
+        else "-thread -linkpkg", packages
+      in
+      let packagesopt = 
+        if CList.is_empty packages then ""
+        else "-package " ^ String.concat "," packages
       in
       let compile_cmd = 
-        Printf.sprintf "%s compile %s %s -package %s -o %s %s" 
-          malfunction optimize flags packages output fname
+        Printf.sprintf "%s compile %s %s %s -o %s %s" 
+          malfunction optimize flags packagesopt output fname
       in
-      let _out, _err = time opts Pp.(str "Compilation") (execute opts) compile_cmd in (* we now have fname . cmx *)
+      let _out, _err = time opts Pp.(str "Malfunction Compilation") (execute opts) compile_cmd in (* we now have fname . cmx *)
       notice opts Pp.(fun () -> str "Compiled to " ++ str output);
       Some (StandaloneProgram output)
 
@@ -709,18 +714,6 @@ type malfunction_compilation_function =
   malfunction_pipeline_config -> malfunction_program_type -> TemplateProgram.template_program -> 
   string list * string
 
-let decompose_argument env sigma c =
-  let rec aux c =
-    let fn, args = EConstr.decompose_app sigma c in
-    match EConstr.kind sigma fn with
-    | Construct (cstr, u) when Environ.QGlobRef.equal env (ConstructRef cstr) (Rocqlib.lib_ref "core.prod.intro") ->
-      (match CArray.to_list args with
-       | [ _; _; fst; snd ]
-          -> aux fst @ [Reify.check_reifyable_thunk_or_value env sigma snd]
-       |_ ->  [Reify.check_reifyable_thunk_or_value env sigma c])
-    | _ -> [Reify.check_reifyable_thunk_or_value env sigma c]
-  in aux c
-
 let set_opam_env opts =
   let path = Unix.getenv "PATH" in
   let opam_binpath = 
@@ -738,18 +731,13 @@ let set_opam_env opts =
 
 let extract_and_run
   (compile_malfunction : malfunction_compilation_function)
-  ?loc opts env sigma c dest : (Constr.t list) option =
-  let opts = make_options loc opts in
-  let () = set_opam_env opts in 
-  let prog = time opts Pp.(str"Quoting") (Ast_quoter.quote_term_rec ~bypass:opts.bypass_qeds env) sigma (EConstr.to_constr sigma c) in
+  ?loc opts env sigma (c: EConstr.t) (tyinfos : Reify.reifyable_type list) dest : Constr.t list option =
+  let () = time opts Pp.(str"Setting opam env") set_opam_env opts in 
+  let prog = time opts Pp.(str"Quoting") (Ast_quoter.quote_term_rec ~bypass:opts.bypass_qeds ~with_universes:false env sigma) (EConstr.to_constr sigma c) in
   let pt = match opts.program_type with 
     | Some (Standalone _) | None -> Standalone_binary 
     | Some Plugin -> Shared_library ("Rocq_verified_extraction_plugin__Verified_extraction", "register_plugin")
   in
-  let tyinfos =
-    try decompose_argument env sigma c
-    with e -> if not (opts.load || opts.run) then [] else raise e
-  in
   let run_pipeline opts prog = compile_malfunction opts.malfunction_pipeline_config pt prog in
   let names, eprog = time opts Pp.(str"Extraction") (run_pipeline opts) prog in
   let names = if opts.load then 
@@ -770,13 +758,15 @@ let extract_and_run
   let dest = match dest with
   | None -> Feedback.msg_notice Pp.(str eprog); None
   | Some fname ->
-    let fname = build_fname fname in
-    let oc = open_out fname in (* Does not raise? *)
-    let () = output_string oc eprog in
-    let () = output_char oc '\n' in
-    close_out oc;
-    notice opts Pp.(fun () -> str"Extracted code written to " ++ str fname);
-    Some fname
+    let write () =
+      let fname = build_fname fname in
+      let oc = open_out fname in (* Does not raise? *)
+      let () = output_string oc eprog in
+      let () = output_char oc '\n' in
+      close_out oc;
+      notice opts Pp.(fun () -> str"Extracted code written to " ++ str fname);
+      Some fname
+    in time opts Pp.(str"Serializing code") write ()
   in
   match dest with
   | None -> None
@@ -786,9 +776,9 @@ let extract_and_run
       let temp = fname ^ ".tmp" in
       ignore (execute opts (Printf.sprintf "%s fmt < %s > %s && mv %s %s" malfunction fname temp temp fname))
     else ();
-    match compile opts names tyinfos fname with
+    match time opts Pp.(str"Compiling") (compile opts names tyinfos) fname with
     | None -> None
-    | Some result -> run opts env sigma result
+    | Some result -> time opts Pp.(str"Running") (run opts env sigma) result
 
 let print_results env sigma = function
   | None -> ()
@@ -824,6 +814,46 @@ let eval ?loc opts gr =
   let env, sigma, c = eval_plugin_gen ?loc opts gr in
   c
 
+let prc = Printer.pr_constr_env
+
+let erase_eval_function compile_malfunction : Eraseconv.erase_evaluation_function =
+  fun env term ty -> 
+    let sigma = Evd.from_env env in
+    debug Pp.(fun () -> str"Erasure evaluation called on term: " ++ prc env sigma term ++ str" of type " ++ 
+      prc env sigma ty);
+    let opts = [ProgramType Plugin; Time; Load; Run] in 
+    let opts = make_options None opts in
+    let tyinfo = time opts Pp.(str"Checking reifyability") (Reify.check_reifyable_thunk_or_value_type env sigma) (EConstr.of_constr ty) in
+    let res = time opts Pp.(str"Extracting, running and reifying") (extract_and_run compile_malfunction opts env sigma (EConstr.of_constr term) [tyinfo]) None in
+    match res with
+    | None ->
+      debug Pp.(fun () -> str"Didn't reify to a value");
+      Error ()
+    | Some [res] -> 
+      debug Pp.(fun () -> str"Reified to value: " ++ Printer.pr_constr_env env sigma res);
+      Ok res
+    | Some l -> assert false
+
+let install_erase_conv compile_malfunction = 
+  Eraseconv.install_erase_conv (erase_eval_function compile_malfunction)
+
+let decompose_argument env sigma c : Reify.reifyable_type list =
+  let rec aux c =
+    let fn, args = EConstr.decompose_app sigma c in
+    match EConstr.kind sigma fn with
+    | Construct (cstr, u) when Environ.QGlobRef.equal env (ConstructRef cstr) (Rocqlib.lib_ref "core.prod.intro") ->
+      (match CArray.to_list args with
+       | [ _; _; fst; snd ]
+          -> aux fst @ [Reify.check_reifyable_thunk_or_value env sigma snd]
+       |_ ->  [Reify.check_reifyable_thunk_or_value env sigma c])
+    | _ -> [Reify.check_reifyable_thunk_or_value env sigma c]
+  in aux c
+
 let extract compile_malfunction ?loc opts env sigma c dest = 
-  let res = extract_and_run compile_malfunction ?loc opts env sigma c dest in
+  let opts = make_options loc opts in
+  let tyinfos =
+    try decompose_argument env sigma c
+    with e -> if not (opts.load || opts.run) then [] else raise e
+  in
+  let res = extract_and_run compile_malfunction ?loc opts env sigma c tyinfos dest in
   print_results env sigma res

lib/rocq_verified_extraction_plugin/lib/verified_extraction.mli

@@ -87,4 +87,6 @@ val extract :
 
 val eval_plugin : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> unit
 
-val eval : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> Constr.t
+val eval : ?loc:Loc.t -> malfunction_command_args list -> Libnames.qualid -> Constr.t
+
+val install_erase_conv : malfunction_compilation_function -> unit

plugin/plugin-bootstrap/Tactics.v

@@ -0,0 +1,80 @@
+From VerifiedExtraction Require Import Loader.
+
+Inductive value_of {A} : A -> Type := 
+  | value_is a : value_of a.
+Definition get_value_of {A} {a : A} (c : value_of a) : A := 
+  let 'value_is a := c in a.
+
+Lemma value_of_eq {A} {a : A} (c : value_of a) : get_value_of c = a.
+Proof. destruct c. reflexivity. Defined. 
+
+From Ltac2 Require Import Ltac2.
+
+(** Runs erasure evaluation only once, in the kernel (if paired with Std.exact). 
+  Beware that no check is performed that the cast is correct when using this in a tactic.
+  It will be checked at Qed-time only. *)
+Ltac2 erase_nocheck c v := 
+  let vty := Constr.type c in
+  let c := Constr.Unsafe.make (Constr.Unsafe.Cast constr:(@value_is $vty $v) Constr.Cast.erase constr:(@value_of $vty $c)) in
+  c.
+
+(** Runs erasure evaluation twice, first to find the value during elaboration, 
+    then to check in the kernel *)
+Ltac2 erase_compute c := 
+  let vty := Constr.type c in
+  let c := Constr.pretype preterm:(@value_is $vty _ <<<: @value_of $vty $c) in
+  c.
+
+(** Helper to extract the value from an `value_of` term and apply `value_of_eq` to 
+  produce an equality. *)
+Ltac2 show_value c :=
+  let ty := Constr.type c in
+  match Constr.Unsafe.kind ty with
+  | Constr.Unsafe.App _ args =>
+    let car := Array.get args 0 in
+    let computed := Array.get args 1 in
+    let term := constr:(@get_value_of $car $computed $c) in
+    let cres := eval hnf in $term in
+    Std.exact_no_check constr:(value_of_eq $c : $computed = $cres)
+  | _ => Control.throw (Invalid_argument None)
+  end.
+
+(** Wrappers and notations for the primitives. *)
+
+(** Use `erase_nocheck t v` to get a proof through erasure evaluation that `t` is equal to `v`. 
+  The evaluation will happen only when this proof is typechecked by the kernel.
+  If `v` is not a value, standard conversion will apply to convert it to `t`'s value found by erased evaluation. *)
+Ltac2 erase_nocheck0 t v := show_value (erase_nocheck t v).
+Ltac2 Notation "erase_nocheck" t(constr) v(constr) := erase_nocheck0 t v.
+
+(** Use `erase_compute t` to find out the value `v` through erasure evaluation and get a proof that `t` equals `v`. 
+  This requires running evaluation twice. I.e. if used in a proof it will run evaluation at the tactic call and again at 
+  qed time.
+*)
+Ltac2 erase_compute0 t := show_value (erase_compute t).
+Ltac2 Notation "erase_compute" t(constr) := erase_compute0 t.
+
+(** Just compute the value associated to `t` during elaboration and throw away the proof that it comes from `t`. 
+  This runs evaluation only once. *)
+Ltac2 erase_forget0 t := 
+  let vty := Constr.type t in
+  let c := Constr.pretype preterm:(@value_is $vty _ <<<: @value_of $vty $t) in
+  match Constr.Unsafe.kind_nocast c with 
+  | Constr.Unsafe.App _compute args => Std.exact_no_check (Array.get args 1)
+  | _ => Control.throw (Invalid_argument None)
+  end.
+Ltac2 Notation "erase_forget" t(constr) := erase_forget0 t.
+
+Ltac2 Notation "value_of" c(constr) := show_value c.
+
+(* Tests *)
+Definition foo (x : unit) := true.
+
+Definition test := ltac2:(erase_nocheck (foo tt) true).
+Check test : foo tt = true.
+
+Definition testevar := ltac2:(erase_compute (foo tt)).
+Check testevar : foo tt = true.
+
+Definition foo_tt_value := ltac2:(erase_forget (foo tt)).
+Check eq_refl : foo_tt_value = true.

plugin/plugin-bootstrap/g_verified_extraction_malfunction.mlg

@@ -292,6 +292,8 @@ let compile_malfunction conf pt p =
 
 let extract = extract compile_malfunction
 
+let () = install_erase_conv compile_malfunction
+
 }
 
 VERNAC COMMAND EXTEND Malfunction_Verified_Extraction CLASSIFIED AS QUERY

plugin/plugin/g_verified_extraction_ocaml.mlg

@@ -79,6 +79,8 @@ let compile_malfunction conf pt p =
 
 let extract = extract compile_malfunction
 
+let () = install_erase_conv compile_malfunction
+
 }
 
 VERNAC COMMAND EXTEND Verified_Extraction CLASSIFIED AS QUERY

theories/PrintMli.v

@@ -1,4 +1,4 @@
-Require Import Nat List.
+From Stdlib Require Import Nat List.
 From Stdlib Require Import Strings.Ascii.
 From MetaRocq.Template Require Import Loader All Checker.
 From MetaRocq.Utils Require Import bytestring.