Implement prototype for certificate generation

dune-project

@@ -32,4 +32,5 @@
   (js_of_ocaml (>= 5.4.0))
   (unionFind (>= 20220122))
   (visitors (>= 20210608))
-  (pprint (>= 20230830))))
+  (pprint (>= 20230830))
+  (cmdliner (>= 2.0.0))))

heifer.opam

@@ -21,6 +21,7 @@ depends: [
   "unionFind" {>= "20220122"}
   "visitors" {>= "20210608"}
   "pprint" {>= "20230830"}
+  "cmdliner" {>= "2.0.0"}
   "odoc" {with-doc}
 ]
 build: [

lib/hipcore_typed/subst.ml

@@ -61,6 +61,16 @@ let types_of_free_vars (type ctx_type) (ctx_type : ctx_type subst_context) (ctx
       method zero = SMap.empty
       method plus = SMap.merge_right_priority
 
+      (* ens binds 'res', remove it as a free var *)
+      method! visit_NormalReturn () p k =
+        let free_p = super#visit_pi () p in
+        let free_k = super#visit_kappa () k in
+        SMap.merge_arbitrary free_p free_k |> SMap.remove "res"
+
+      method! visit_PointsTo () loc v =
+        let b = super#visit_term () v in
+        SMap.add loc (Some (TConstr ("ref", [v.term_type]))) b
+
       method! visit_Exists () x f =
         let b = super#visit_Exists () x f in
         SMap.remove (ident_of_binder x) b

lib/hiplib/hiplib.ml

@@ -31,6 +31,8 @@ let ocaml_prelude = "
 
 "
 
+let entailment_succeeded = Hipprover.Entail.Entail_result.entailment_succeeded
+
 (*
 let debug_tokens str =
   let lb = Lexing.from_string str in
@@ -81,6 +83,21 @@ let check_lambda_obligation_ name params lemmas predicates obl =
   check_obligation_ name params lemmas preds (obl.lo_left, obl.lo_right)
 *)
 
+let certificate_output : Hipprover.Certificate.certificate_file option ref = ref None
+
+let print_certificate program name constr proof_log =
+  let open Hipprover.Certificate in
+  ignore proof_log;
+  match !certificate_output with
+  | None -> ()
+  | Some file ->
+      write_theorem ~out:file
+        ~program
+        ~name:(name ^ "_correctness")
+        ~statement:constr
+        ~string_of_step:Hipprover.Entail.string_of_coq_tactic
+        (Some proof_log)
+
 let test_failed result name =
   if String.ends_with ~suffix:"_false" name then
     result
@@ -170,12 +187,12 @@ let infer_spec (prog : core_program) (meth : meth_def) =
 
 let check_method prog inferred given =
   match given with
-  | None -> true
+  | None -> None
   | Some given_spec ->
     let open Hipprover.Entail in
     (* likely that we need some env or extra setup later *)
     let pctx = create_pctx prog in
-    check_staged_spec_entailment pctx inferred given_spec
+    Some (check_staged_spec_entailment pctx inferred given_spec)
 
 let infer_and_check_method (prog : core_program) (meth : meth_def) (given_spec : staged_spec option) =
   let inferred_spec = infer_spec prog meth in
@@ -214,37 +231,46 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program =
   let updated_meth = {meth with m_spec = Some choosen_spec} in
   (* we always add the method into the program, regardless of whether it is verified or not? *)
   let prog = {prog with cp_methods = updated_meth :: prog.cp_methods} in
-  let prog =
-    (* let@ _ = Globals.Timing.(time overall) in *)
-    if not result then prog
-    else begin
-      let@ _ = Debug.span (fun _ -> debug
-        ~at:2
-        ~title:(Format.asprintf "remembering predicate for %s" meth.m_name)
-        "")
-      in
-      let pred = Hipprover.Entail.derive_predicate meth.m_name 
-      meth.m_params
-      inferred_spec in
-      (* let pred = todo () in *)
-      let cp_predicates = SMap.add meth.m_name pred prog.cp_predicates in
-      {prog with cp_predicates}
+  let is_success = match result with
+    | None -> true
+    | Some result -> entailment_succeeded result
+  in
+  let add_predicate prog name params spec =
+    let@ _ = Debug.span (fun _ -> debug
+      ~at:2
+      ~title:(Format.asprintf "remembering predicate for %s" name)
+      "")
+    in
+    let pred = Hipprover.Entail.derive_predicate name params spec in
+    (* let pred = todo () in *)
+    let cp_predicates = SMap.add name pred prog.cp_predicates in
+    {prog with cp_predicates}
+  in
       (* prog *)
-    end
+  let prog = match result with
+    (* let@ _ = Globals.Timing.(time overall) in *)
+    | None -> add_predicate prog meth.m_name meth.m_params inferred_spec
+    | Some result ->
+        let open Hipprover.Entail.Entail_result in
+        match theorem_of_entailment result with
+        | Some (statement, proof) ->
+            print_certificate prog meth.m_name statement proof;
+            add_predicate prog meth.m_name meth.m_params inferred_spec
+        | None -> prog
   in
   (* potentially report the normalized spec as well. Refactor *)
   report_result
     ~kind:"Function"
     ~name:meth.m_name
     ~inferred_spec
     ~given_spec
-    ~result;
+    ~result:is_success;
   prog
 
 let check_lemma (prog : core_program) (l : lemma) : bool =
   let open Hipprover.Entail in
   let pctx = create_pctx prog in
-  check_staged_spec_entailment pctx l.l_left l.l_right
+  entailment_succeeded (check_staged_spec_entailment pctx l.l_left l.l_right)
 
 let analyze_lemma (prog : core_program) (l : lemma) : core_program =
   let result = check_lemma prog l in
@@ -479,8 +505,14 @@ let preprocess_spec_comments =
     let output = Str.global_replace lemma_attr_regex "@@@lemma" output in
     output
 
-let run_file input_file =
+let run_file ~certificate_file input_file =
   let open Utils.Io in
+  begin
+    let open Hipprover.Certificate in
+    match certificate_file with
+    | Some f -> certificate_output := Some (open_out f |> make_certificate_file)
+    | None -> ()
+  end;
   let chan = open_in input_file in
   let lines = input_lines chan in
   let content = String.concat "\n" lines in
@@ -512,7 +544,6 @@ let run_file input_file =
   let lexbuf = Lexing.from_string content in
   let staged_spec = Parser.parse_staged_spec Lexer.token lexbuf in
   print_endline (Pretty.string_of_staged_spec staged_spec)
-*)
 
 let main () =
   if Array.length (Sys.argv) < 2 then begin
@@ -523,3 +554,4 @@ let main () =
   run_file inputfile;
   if !test_mode && not !tests_failed then Format.printf "ALL OK!@.";
   exit (if !tests_failed then 1 else 0)
+*)