From 5042768f542ed75a1ed4f870d4959a21a66a929a Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Thu, 30 Oct 2025 18:02:12 +0800
Subject: [PATCH 1/9] port arg parsing to cmdliner

---
 dune-project |  3 +-
 heifer.opam  |  1 +
 main/dune    |  4 +--
 main/hip.ml  | 86 +++++++++++++++++++++++++++++++++++++---------------
 4 files changed, 66 insertions(+), 28 deletions(-)

diff --git a/dune-project b/dune-project
index 16fe1c96..468c78f8 100644
--- a/dune-project
+++ b/dune-project
@@ -32,4 +32,5 @@
   (js_of_ocaml (>= 5.4.0))
   (unionFind (>= 20220122))
   (visitors (>= 20210608))
-  (pprint (>= 20230830))))
+  (pprint (>= 20230830))
+  (cmdliner (>= 2.0.0))))
diff --git a/heifer.opam b/heifer.opam
index 7b9f49dc..ca309fb0 100644
--- a/heifer.opam
+++ b/heifer.opam
@@ -21,6 +21,7 @@ depends: [
   "unionFind" {>= "20220122"}
   "visitors" {>= "20210608"}
   "pprint" {>= "20230830"}
+  "cmdliner" {>= "2.0.0"}
   "odoc" {with-doc}
 ]
 build: [
diff --git a/main/dune b/main/dune
index f2f31a4e..33a15539 100644
--- a/main/dune
+++ b/main/dune
@@ -1,7 +1,7 @@
 (executable
  (name hip)
  (modules hip)
- (libraries unix hiplib provers_native))
+ (libraries unix hiplib provers_native cmdliner))
 
 (executable
  (name hipjs)
@@ -11,4 +11,4 @@
 
 (install
  (section bin)
- (files (hip.exe as hip)))
\ No newline at end of file
+ (files (hip.exe as hip)))
diff --git a/main/hip.ml b/main/hip.ml
index f66fe27e..a8c71647 100644
--- a/main/hip.ml
+++ b/main/hip.ml
@@ -1,4 +1,7 @@
 
+open Cmdliner
+open Cmdliner.Term.Syntax
+
 let redirect_stdout f =
   let name = "out.org" in
   Format.printf "%s@." name;
@@ -11,30 +14,63 @@ let redirect_stdout f =
   Unix.close oldstdout;
   close_out newstdout
 
-let () =
-  Hiplib.(test_mode :=
-    (Option.bind (Sys.getenv_opt "TEST") int_of_string_opt
-    |> Option.value ~default:0) > 0);
-  Hiplib.(file_mode :=
-    (Option.bind (Sys.getenv_opt "FILE") int_of_string_opt
-    |> Option.value ~default:0) > 0);
-  begin
-  if Option.bind (Sys.getenv_opt "NOTYPES") int_of_string_opt |> Option.value ~default:0 > 0
-  then Hipcore_typed.Dynamic_typing.set_dynamic_typing ()
-  end;
-  let ctf =
-    Option.bind (Sys.getenv_opt "CTF") int_of_string_opt
-    |> Option.value ~default:0 > 0
-  in
+let in_test_mode =
+  let env = Cmd.Env.info "TEST" in
+  let doc = "Run in test mode." in
+  Arg.(value & flag & info ["test"] ~env ~doc ~docv:"TEST")
+
+let output_to_file =
+  let env = Cmd.Env.info "FILE" in
+  let doc = "Redirect all output to a file." in
+  Arg.(value & flag & info ["debug-file"] ~env ~doc ~docv:"DEBUG_FILE")
+
+let file_to_prove =
+  let doc = "The file with code to verify." in
+  Arg.(required & pos 0 (some string) None & info [] ~doc ~docv:"FILE")
+
+let show_types =
+  let env = Cmd.Env.info "SHOW_TYPES" in
+  let doc = "Insert type annotations in output." in
+  Arg.(value & flag & info ["show-types"] ~env ~doc ~docv:"SHOW_TYPES")
+
+let perfetto_trace =
+  let env = Cmd.Env.info "CTF" in
+  let doc = "Output a trace file viewable by Perfetto." in
+  Arg.(value & flag & info ["perfetto-trace"] ~env ~doc ~docv:"TRACE")
+
+let debug_query =
+  let env = Cmd.Env.info "DEBUG" in
+  let doc = "Enable and specify parameters to filter debug output." in
+  Arg.(value & opt (some string) None & info ["debug"] ~env ~doc ~docv:"DEBUG")
+
+let run_as_untyped =
+  let env = Cmd.Env.info "NOTYPES" in
+  let doc = "Ignore types when proving" in
+  Arg.(value & flag & info ["notypes"] ~env ~doc ~docv:"DEBUG")
+
+let cmd =
+  Cmd.make (Cmd.info "heifer" ~version:"0.1") @@
+  let+ file_to_prove and+ in_test_mode and+ output_to_file
+    and+ show_types and+ perfetto_trace and+ debug_query
+    and+ run_as_untyped in
+  Hiplib.test_mode := in_test_mode;
+  Hiplib.file_mode := output_to_file;
+  if show_types then
+    Hipcore_typed.Pretty.(set_current_config set_types_display);
+  if run_as_untyped then
+    Hipcore_typed.Dynamic_typing.set_dynamic_typing ();
+  Hiplib.Debug.init ~ctf:perfetto_trace ~org:!Hiplib.file_mode debug_query;
+  let file_to_prove = Sys.getcwd () ^ "/" ^ file_to_prove in
   begin
-  if Option.bind (Sys.getenv_opt "SHOW_TYPES") int_of_string_opt
-    |> Option.value ~default:0 > 0
-  then Hipcore_typed.Pretty.(set_current_config set_types_display)
-  end;
-  if Unix.isatty Unix.stdout && not !Hiplib.file_mode && not ctf then
-    Hipcore.Pretty.colours := `Ansi;
-  Hiplib.Debug.init ~ctf ~org:!Hiplib.file_mode (Sys.getenv_opt "DEBUG");
   if !Hiplib.file_mode then
-    redirect_stdout Hiplib.main
-  else
-    Hiplib.main ()
+    redirect_stdout (fun () -> Hiplib.run_file file_to_prove)
+  else 
+    Hiplib.run_file file_to_prove
+  end;
+  if !Hiplib.test_mode && not !Hiplib.tests_failed then Format.printf "ALL OK!@.";
+  let return_code = if !Hiplib.tests_failed then 1 else 0 in
+  return_code
+
+let main () = Cmd.eval' cmd
+
+let () = if !Sys.interactive then () else exit (main ())

From e47a22581287280cc342c69672e256c09eda5696 Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Mon, 3 Nov 2025 12:41:34 +0800
Subject: [PATCH 2/9] add certificate module

---
 lib/hipprover/certificate.ml  | 88 +++++++++++++++++++++++++++++++++++
 lib/hipprover/certificate.mli | 57 +++++++++++++++++++++++
 lib/hipprover/entail.ml       |  3 ++
 3 files changed, 148 insertions(+)
 create mode 100644 lib/hipprover/certificate.ml
 create mode 100644 lib/hipprover/certificate.mli

diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
new file mode 100644
index 00000000..c6dca119
--- /dev/null
+++ b/lib/hipprover/certificate.ml
@@ -0,0 +1,88 @@
+
+open Hipcore_typed.Typedhip
+
+exception Unsupported_term of string
+
+type constr = CVar of string
+  | CConst of const
+  | CApp of constr * constr list
+  | CFun of string * constr
+  (* these are only to make the output look nicer *)
+  | CInfix of constr * string * constr
+  | CSurround of string * constr * string
+
+let rec hprop_of_kappa (k : kappa) : constr =
+  match k with
+  | SepConj (k1, k2) -> CInfix (hprop_of_kappa k1, "\\*", hprop_of_kappa k2)
+  | EmptyHeap -> CVar "hempty"
+  | PointsTo (l, v) -> CInfix (CVar l, "~~>", constr_of_term v)
+and constr_of_term (t : term) : constr =
+  match t.term_desc with
+  | Const c -> CConst c
+  | Var v -> CVar v
+  | _ -> failwith "TODO a proper failure wrapper"
+and constr_of_pi (p : pi) : constr =
+  match p with
+  | True -> CVar "True"
+  | False -> CVar "False"
+  | And (lhs, rhs) -> CInfix (constr_of_pi lhs, "/\\", constr_of_pi rhs)
+  | Or (lhs, rhs) -> CInfix (constr_of_pi lhs, "\\/", constr_of_pi rhs)
+  | Imply (lhs, rhs) -> CInfix (constr_of_pi lhs, "->", constr_of_pi rhs)
+  | Atomic (op, lhs, rhs) ->
+      let operator = match op with
+        | EQ -> "="
+        | _ -> failwith "TODO a proper failure wrapper"
+      in
+      CInfix (constr_of_term lhs, operator, constr_of_term rhs)
+  | _ -> failwith "TODO a proper failure wrapper"
+and constr_of_state ((p, k) : state) =
+  CInfix (hprop_of_kappa k, "\\*", CSurround ("\\[", constr_of_pi p, "]"))
+and constr_of_staged_spec (ss : staged_spec) : constr =
+  match ss with
+  | Exists (v, ss) -> CApp (CVar "fex", [CFun (ident_of_binder v, constr_of_staged_spec ss)])
+  | ForAll (v, ss) -> CApp (CVar "fall", [CFun (ident_of_binder v, constr_of_staged_spec ss)])
+  | Require (p, k) -> CApp (CVar "req_", [constr_of_state (p, k)])
+  (* need to convert anything that says nothing about the result to an [ens_] ... *)
+  | NormalReturn (p, k) -> CApp (CVar "ens", [CFun ("res", constr_of_state (p, k))])
+  | Sequence (f1, f2) -> CInfix (constr_of_staged_spec f1, ";;", constr_of_staged_spec f2)
+  | Disjunction (f1, f2) -> CApp (CVar "disj", [constr_of_staged_spec f1; constr_of_staged_spec f2])
+  | Bind (v, f1, f2) -> CApp (CVar "bind", [constr_of_staged_spec f1; CFun (ident_of_binder v, constr_of_staged_spec f2)])
+  | _ -> failwith "TODO a proper failure wrapper"
+
+type 'a proof_log =
+  | Step of 'a
+  | Subproof of 'a proof_log list
+
+(* a zipper over a proof log *)
+type 'a partial_proof_log = {
+  current_proof : 'a proof_log list;
+  parent_env : 'a partial_proof_log option
+}
+
+let empty_partial_log = {current_proof = []; parent_env = None}
+
+let proof_step s = Step s
+
+let append ppl step =
+  { ppl with current_proof = step :: ppl.current_proof }
+
+let open_subproof ppl = {
+  current_proof = [];
+  parent_env = Some ppl
+}
+
+let close_subproof ppl = 
+  let parent_env = Option.get ppl.parent_env in
+  let current_proof = Subproof (List.rev ppl.current_proof) :: parent_env.current_proof in
+  { parent_env with current_proof }
+
+
+let finalize_proof_log ppl =
+  match ppl.parent_env with
+  | None -> Subproof ppl.current_proof
+  | Some _ -> failwith "Attempt to finalize unfinished proof log"
+
+let rec close_all_subproofs ppl =
+  match ppl.parent_env with
+  | None -> ppl
+  | Some _ -> close_all_subproofs (close_subproof ppl)
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
new file mode 100644
index 00000000..6faef6b2
--- /dev/null
+++ b/lib/hipprover/certificate.mli
@@ -0,0 +1,57 @@
+
+
+(* Complications:
+
+  - In the formalization, all closures must be placed in a separate store, unlike here,
+  where we can directly embed it into the specification as a TLambda.
+
+  - All primitive functions cannot directly be lifted to coq-level functions. to "assert"
+  a value is of a given type, we need to either add a (fex (fun typed_val : T => ens_ \[untyped_val = vconstructor typed_val] ;; ...))
+  -like condition to the spec, or admit lemmas that state exactly this. and this isn't taking into account
+  the fact that we won't always have types before smt!!!
+  
+  - i feel like it is safe to couple this to work specifically with coq since YAGNI
+  support for anything else?
+
+  *)
+
+open Hipcore_typed.Typedhip
+
+type 'a proof_log
+
+type 'a partial_proof_log
+
+val empty_partial_log : 'a partial_proof_log
+
+val proof_step : 'a -> 'a proof_log
+
+val append : 'a partial_proof_log -> 'a proof_log -> 'a partial_proof_log
+
+val open_subproof : 'a partial_proof_log -> 'a partial_proof_log
+
+val close_subproof : 'a partial_proof_log -> 'a partial_proof_log
+
+val finalize_proof_log : 'a partial_proof_log -> 'a proof_log
+
+(* type proof_step *)
+(**)
+(* val use_rewrite : string -> proof_step *)
+(**)
+(* val apply_lemma : string -> proof_step *)
+(**)
+(* val apply_named_tactic : string -> proof_step *)
+(**)
+(* val concat : proof_step -> proof_step -> proof_step *)
+(**)
+(* val subgoals : proof_step -> proof_step list -> proof_step *)
+(**)
+(* type theorem *)
+(**)
+(* val theorem_of_entailment : staged_spec -> staged_spec -> theorem *)
+(**)
+(* type certificate *)
+(**)
+(* val create_proof : theorem -> proof_step -> certificate *)
+(**)
+(* val export : certificate -> string *)
+(**)
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index b55c459c..87b58938 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -27,6 +27,7 @@ type pctx = {
   lemmas : (string * Rewriting.rule) list;
   unfolded : use list;
   assumptions : pi list;
+  proof_log : string Certificate.partial_proof_log
 }
 
 let string_of_pctx ctx =
@@ -38,6 +39,7 @@ let string_of_pctx ctx =
     unfolded;
     induction_hypotheses;
     lemmas;
+    _
   } =
     ctx
   in
@@ -80,6 +82,7 @@ let new_pctx () =
     unfolded = [];
     induction_hypotheses = [];
     lemmas = [];
+    proof_log = Certificate.empty_partial_log
   }
 
 let has_been_unfolded pctx name _lr =

From 27767b5f5be8b0a4a346fc1bde1882bf05113803 Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Tue, 4 Nov 2025 12:58:54 +0800
Subject: [PATCH 3/9] add infra for outputting cert file

currently non-functional
---
 lib/hiplib/hiplib.ml          |  33 ++++++--
 lib/hipprover/certificate.ml  |   4 +
 lib/hipprover/certificate.mli |  28 ++-----
 lib/hipprover/dune            |   2 +-
 lib/hipprover/entail.ml       | 144 +++++++++++++++++++---------------
 main/hip.ml                   |  10 ++-
 6 files changed, 125 insertions(+), 96 deletions(-)

diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml
index 35694cd0..7c8775dd 100644
--- a/lib/hiplib/hiplib.ml
+++ 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,16 @@ let check_lambda_obligation_ name params lemmas predicates obl =
   check_obligation_ name params lemmas preds (obl.lo_left, obl.lo_right)
 *)
 
+let certificate_output : out_channel option ref = ref None
+
+let print_certificate name constr proof_log =
+  ignore proof_log;
+  let open Hipprover.Certificate in
+  match !certificate_output with
+  | None -> ()
+  | Some out_chan ->
+      Printf.fprintf out_chan "Theorem %s_correctness : %s.\nProof.\nAdmitted." name (string_of_constr constr)
+
 let test_failed result name =
   if String.ends_with ~suffix:"_false" name then
     result
@@ -170,12 +182,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,9 +226,13 @@ 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 is_success = match result with
+    | None -> true
+    | Some result -> entailment_succeeded result
+  in
   let prog =
     (* let@ _ = Globals.Timing.(time overall) in *)
-    if not result then prog
+    if not is_success then prog
     else begin
       let@ _ = Debug.span (fun _ -> debug
         ~at:2
@@ -238,13 +254,13 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program =
     ~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 +495,11 @@ 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
+  match certificate_file with
+  | Some f -> certificate_output := Some (open_out f)
+  | None -> ();
   let chan = open_in input_file in
   let lines = input_lines chan in
   let content = String.concat "\n" lines in
@@ -512,7 +531,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 +541,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)
+*)
diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index c6dca119..11b8e3a5 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -49,6 +49,10 @@ and constr_of_staged_spec (ss : staged_spec) : constr =
   | Bind (v, f1, f2) -> CApp (CVar "bind", [constr_of_staged_spec f1; CFun (ident_of_binder v, constr_of_staged_spec f2)])
   | _ -> failwith "TODO a proper failure wrapper"
 
+let string_of_constr c = failwith "TODO"
+
+let statement_of_entailment f1 f2 = Some (CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2]))
+
 type 'a proof_log =
   | Step of 'a
   | Subproof of 'a proof_log list
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index 6faef6b2..0d5147a3 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -33,25 +33,9 @@ val close_subproof : 'a partial_proof_log -> 'a partial_proof_log
 
 val finalize_proof_log : 'a partial_proof_log -> 'a proof_log
 
-(* type proof_step *)
-(**)
-(* val use_rewrite : string -> proof_step *)
-(**)
-(* val apply_lemma : string -> proof_step *)
-(**)
-(* val apply_named_tactic : string -> proof_step *)
-(**)
-(* val concat : proof_step -> proof_step -> proof_step *)
-(**)
-(* val subgoals : proof_step -> proof_step list -> proof_step *)
-(**)
-(* type theorem *)
-(**)
-(* val theorem_of_entailment : staged_spec -> staged_spec -> theorem *)
-(**)
-(* type certificate *)
-(**)
-(* val create_proof : theorem -> proof_step -> certificate *)
-(**)
-(* val export : certificate -> string *)
-(**)
+type constr
+
+val string_of_constr : constr -> string
+
+(* this prototype version deliberately excludes calling functions from the context *)
+val statement_of_entailment : staged_spec -> staged_spec -> constr option
diff --git a/lib/hipprover/dune b/lib/hipprover/dune
index df0de526..23d7b55e 100644
--- a/lib/hipprover/dune
+++ b/lib/hipprover/dune
@@ -1,6 +1,6 @@
 (library
  (name hipprover)
- (modules ProversEx entail forward_rules infer_types normalize rewriting rewriting2 heap biab simpl reduce_shift_reset)
+ (modules ProversEx entail forward_rules infer_types normalize rewriting rewriting2 heap biab simpl reduce_shift_reset certificate)
  (libraries debug search hipcore provers utils iter provers_common z3 hipcore_typed)
  (inline_tests)
  (preprocess (pps ppx_expect)))
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index 87b58938..f2652f37 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -14,6 +14,65 @@ open Utils.Hstdlib
   | `Left -> Format.asprintf "%s, L" f
   | `Right -> Format.asprintf "%s, R" f *)
 
+type coq_tactic =
+  | Rewrite of string
+  | SRReduction
+  | Simplify
+  | Biab
+  | EntDisjL
+  | EntDisjR
+  | Focus of coq_tactic list
+
+type coq_tactics = coq_tactic list
+
+let rec string_of_coq_tactic t =
+  match t with
+  | EntDisjL -> "apply ent_disj_l."
+  | EntDisjR -> "apply ent_disj_l."
+  | Focus [] -> ""
+  | Focus [a] -> Format.asprintf "{ %s }" (string_of_coq_tactic a)
+  | Focus (a :: rest) ->
+    Format.asprintf "{ %s\n%s }" (string_of_coq_tactic a)
+      (string_of_list_ind_lines string_of_coq_tactic rest)
+  | Simplify -> "fsimpl."
+  | Biab -> "fbiabduction."
+  | SRReduction -> "freduction."
+  | Rewrite r -> Format.asprintf "rewrite %s." r
+
+and string_of_coq_tactics ts =
+  ts |> List.map string_of_coq_tactic |> String.concat "\n"
+
+let%expect_test _ =
+  Format.printf "%s@."
+    (string_of_coq_tactics
+       [
+         EntDisjL;
+         Focus
+           [
+             EntDisjR;
+             EntDisjL;
+             EntDisjR;
+             EntDisjL;
+             EntDisjR;
+             EntDisjL;
+             EntDisjR;
+             EntDisjL;
+           ];
+         Focus [EntDisjR];
+       ]);
+  [%expect
+    {|
+    apply ent_disj_l.
+    { apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l.
+      apply ent_disj_l. }
+    { apply ent_disj_l. }
+    |}]
 type use = Use of string [@@unboxed]
 
 let string_of_use (Use f) = f
@@ -27,7 +86,7 @@ type pctx = {
   lemmas : (string * Rewriting.rule) list;
   unfolded : use list;
   assumptions : pi list;
-  proof_log : string Certificate.partial_proof_log
+  proof_log : coq_tactic Certificate.partial_proof_log
 }
 
 let string_of_pctx ctx =
@@ -395,65 +454,6 @@ end = struct
       fmt
 end
 
-type coq_tactic =
-  | Rewrite of string
-  | SRReduction
-  | Simplify
-  | Biab
-  | EntDisjL
-  | EntDisjR
-  | Focus of coq_tactic list
-
-type coq_tactics = coq_tactic list
-
-let rec string_of_coq_tactic t =
-  match t with
-  | EntDisjL -> "apply ent_disj_l."
-  | EntDisjR -> "apply ent_disj_l."
-  | Focus [] -> ""
-  | Focus [a] -> Format.asprintf "{ %s }" (string_of_coq_tactic a)
-  | Focus (a :: rest) ->
-    Format.asprintf "{ %s\n%s }" (string_of_coq_tactic a)
-      (string_of_list_ind_lines string_of_coq_tactic rest)
-  | Simplify -> "fsimpl."
-  | Biab -> "fbiabduction."
-  | SRReduction -> "freduction."
-  | Rewrite r -> Format.asprintf "rewrite %s." r
-
-and string_of_coq_tactics ts =
-  ts |> List.map string_of_coq_tactic |> String.concat "\n"
-
-let%expect_test _ =
-  Format.printf "%s@."
-    (string_of_coq_tactics
-       [
-         EntDisjL;
-         Focus
-           [
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-           ];
-         Focus [EntDisjR];
-       ]);
-  [%expect
-    {|
-    apply ent_disj_l.
-    { apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l. }
-    { apply ent_disj_l. }
-    |}]
 
 let rec disj_left () : unit Tactic.t =
   let open Tactic in
@@ -593,6 +593,22 @@ let%expect_test _ =
     unfolded:
     |}]
 
+module Entail_result : sig 
+  type entailment_result
+  val entail_failure : entailment_result
+  val result_of_pctx : pctx -> staged_spec -> staged_spec -> entailment_result
+  val entailment_succeeded : entailment_result -> bool
+  val statement_of_entailment : entailment_result -> Certificate.constr option
+  val certificate_of_entailment : entailment_result -> coq_tactic Certificate.proof_log option
+end = struct 
+  type entailment_result = pstate option
+  let entail_failure = None
+  let result_of_pctx pctx f1 f2 = Some (pctx, f1, f2)
+  let entailment_succeeded = Option.is_some
+  let statement_of_entailment r = Option.bind r (fun (_, f1, f2) -> Certificate.statement_of_entailment f1 f2)
+  let certificate_of_entailment r = r |> Option.map (fun (pctx, _, _) -> Certificate.finalize_proof_log pctx.proof_log)
+end
+
 type tactic = pstate -> pstate Iter.t
 
 let fail = ()
@@ -1248,10 +1264,12 @@ let check_staged_spec_entailment ?name pctx inferred given =
         debug ~at:2 ~title:"entailment" "%s\n⊑\n%s\n%s"
           (string_of_staged_spec inferred)
           (string_of_staged_spec given)
-          (string_of_result string_of_bool r))
+          (string_of_result (fun x -> string_of_bool (Entail_result.entailment_succeeded x)) r))
   in
   match Iter.head (entailment_search ?name (pctx, inferred, given)) with
-  | None -> false
+  | None -> Entail_result.entail_failure
   | Some ps ->
     debug ~at:2 ~title:"proof found" "%s" (string_of_pstate ps);
-    true
+    let pctx_outcome, _, _ = ps in
+    let proof_log = pctx_outcome.proof_log in
+    Entail_result.result_of_pctx { pctx with proof_log } inferred given
diff --git a/main/hip.ml b/main/hip.ml
index a8c71647..ee0cfb9f 100644
--- a/main/hip.ml
+++ b/main/hip.ml
@@ -48,11 +48,15 @@ let run_as_untyped =
   let doc = "Ignore types when proving" in
   Arg.(value & flag & info ["notypes"] ~env ~doc ~docv:"DEBUG")
 
+let certificate_file =
+  let doc = "Output a Rocq certificate of any proved entailment. (Experimental)" in
+  Arg.(value & opt (some string) None & info ["certificate"] ~doc ~docv:"CERT_FILE")
+
 let cmd =
   Cmd.make (Cmd.info "heifer" ~version:"0.1") @@
   let+ file_to_prove and+ in_test_mode and+ output_to_file
     and+ show_types and+ perfetto_trace and+ debug_query
-    and+ run_as_untyped in
+    and+ run_as_untyped and+ certificate_file in
   Hiplib.test_mode := in_test_mode;
   Hiplib.file_mode := output_to_file;
   if show_types then
@@ -63,9 +67,9 @@ let cmd =
   let file_to_prove = Sys.getcwd () ^ "/" ^ file_to_prove in
   begin
   if !Hiplib.file_mode then
-    redirect_stdout (fun () -> Hiplib.run_file file_to_prove)
+    redirect_stdout (fun () -> Hiplib.run_file ~certificate_file file_to_prove)
   else 
-    Hiplib.run_file file_to_prove
+    Hiplib.run_file ~certificate_file file_to_prove
   end;
   if !Hiplib.test_mode && not !Hiplib.tests_failed then Format.printf "ALL OK!@.";
   let return_code = if !Hiplib.tests_failed then 1 else 0 in

From 0716d5dc3b80fc96fac01afea607d9c465ec97de Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Tue, 4 Nov 2025 14:59:27 +0800
Subject: [PATCH 4/9] fix bugs and extend constr converter

---
 lib/hiplib/hiplib.ml          | 49 ++++++++++++++++++++---------------
 lib/hipprover/certificate.ml  | 43 +++++++++++++++++++++++-------
 lib/hipprover/certificate.mli |  2 +-
 lib/hipprover/entail.ml       |  9 ++++---
 4 files changed, 67 insertions(+), 36 deletions(-)

diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml
index 7c8775dd..43a7598f 100644
--- a/lib/hiplib/hiplib.ml
+++ b/lib/hiplib/hiplib.ml
@@ -86,12 +86,12 @@ let check_lambda_obligation_ name params lemmas predicates obl =
 let certificate_output : out_channel option ref = ref None
 
 let print_certificate name constr proof_log =
-  ignore proof_log;
   let open Hipprover.Certificate in
+  ignore proof_log;
   match !certificate_output with
   | None -> ()
   | Some out_chan ->
-      Printf.fprintf out_chan "Theorem %s_correctness : %s.\nProof.\nAdmitted." name (string_of_constr constr)
+      Printf.fprintf out_chan "Theorem %s_correctness : %s.\nProof.\nAdmitted.\n\n" name (string_of_constr constr)
 
 let test_failed result name =
   if String.ends_with ~suffix:"_false" name then
@@ -230,23 +230,28 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program =
     | None -> true
     | Some result -> entailment_succeeded result
   in
-  let prog =
-    (* let@ _ = Globals.Timing.(time overall) in *)
-    if not is_success 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 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 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
@@ -497,9 +502,11 @@ let preprocess_spec_comments =
 
 let run_file ~certificate_file input_file =
   let open Utils.Io in
-  match certificate_file with
-  | Some f -> certificate_output := Some (open_out f)
-  | None -> ();
+  begin
+    match certificate_file with
+    | Some f -> certificate_output := Some (open_out f)
+    | None -> ()
+  end;
   let chan = open_in input_file in
   let lines = input_lines chan in
   let content = String.concat "\n" lines in
diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index 11b8e3a5..cbb14317 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -1,8 +1,11 @@
 
 open Hipcore_typed.Typedhip
+open Hipcore_typed.Pretty
 
 exception Unsupported_term of string
 
+let config = default_config |> set_single_line
+
 type constr = CVar of string
   | CConst of const
   | CApp of constr * constr list
@@ -10,17 +13,19 @@ type constr = CVar of string
   (* these are only to make the output look nicer *)
   | CInfix of constr * string * constr
   | CSurround of string * constr * string
+  (* invalid node, meant to allow for better context regarding incomplete constr generation *)
+  | CError of string
 
 let rec hprop_of_kappa (k : kappa) : constr =
   match k with
   | SepConj (k1, k2) -> CInfix (hprop_of_kappa k1, "\\*", hprop_of_kappa k2)
-  | EmptyHeap -> CVar "hempty"
+  | EmptyHeap -> CVar "\[]"
   | PointsTo (l, v) -> CInfix (CVar l, "~~>", constr_of_term v)
 and constr_of_term (t : term) : constr =
   match t.term_desc with
   | Const c -> CConst c
   | Var v -> CVar v
-  | _ -> failwith "TODO a proper failure wrapper"
+  | _ -> CError (string_of_term ~config t)
 and constr_of_pi (p : pi) : constr =
   match p with
   | True -> CVar "True"
@@ -31,10 +36,13 @@ and constr_of_pi (p : pi) : constr =
   | Atomic (op, lhs, rhs) ->
       let operator = match op with
         | EQ -> "="
-        | _ -> failwith "TODO a proper failure wrapper"
+        | GT -> ">"
+        | LT -> "<"
+        | GTEQ -> ">="
+        | LTEQ -> "<="
       in
       CInfix (constr_of_term lhs, operator, constr_of_term rhs)
-  | _ -> failwith "TODO a proper failure wrapper"
+  | _ -> CError (string_of_pi ~config p)
 and constr_of_state ((p, k) : state) =
   CInfix (hprop_of_kappa k, "\\*", CSurround ("\\[", constr_of_pi p, "]"))
 and constr_of_staged_spec (ss : staged_spec) : constr =
@@ -46,12 +54,27 @@ and constr_of_staged_spec (ss : staged_spec) : constr =
   | NormalReturn (p, k) -> CApp (CVar "ens", [CFun ("res", constr_of_state (p, k))])
   | Sequence (f1, f2) -> CInfix (constr_of_staged_spec f1, ";;", constr_of_staged_spec f2)
   | Disjunction (f1, f2) -> CApp (CVar "disj", [constr_of_staged_spec f1; constr_of_staged_spec f2])
-  | Bind (v, f1, f2) -> CApp (CVar "bind", [constr_of_staged_spec f1; CFun (ident_of_binder v, constr_of_staged_spec f2)])
-  | _ -> failwith "TODO a proper failure wrapper"
-
-let string_of_constr c = failwith "TODO"
-
-let statement_of_entailment f1 f2 = Some (CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2]))
+  | Bind (v, f1, f2) -> CApp (CVar "bind_t", [constr_of_staged_spec f1; CFun (ident_of_binder v, constr_of_staged_spec f2)])
+  | _ -> CError (string_of_staged_spec ~config ss)
+
+let rec string_of_constr c =
+  match c with
+  | CConst c -> begin match c with
+    | ValUnit -> "tt"
+    | TStr s -> "\"" ^ s ^ "\""
+    | Num n -> string_of_int n
+    | Nil -> "[]"
+    | TTrue -> "true"
+    | TFalse -> "false"
+    end
+  | CVar v -> v
+  | CFun (x, body) -> Printf.sprintf "(fun %s => %s)" x (string_of_constr body)
+  | CApp (f, args) -> Printf.sprintf "(%s %s)" (string_of_constr f) (List.map string_of_constr args |> String.concat " ")
+  | CInfix (lhs, op, rhs) -> Printf.sprintf "(%s %s %s)" (string_of_constr lhs) op (string_of_constr rhs)
+  | CSurround (lp, sub, rp) -> Printf.sprintf "%s %s %s" lp (string_of_constr sub) rp
+  | CError s -> Printf.sprintf "(* unsupported node: %s *) _" s
+
+let statement_of_entailment f1 f2 = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2])
 
 type 'a proof_log =
   | Step of 'a
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index 0d5147a3..eac298e4 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -38,4 +38,4 @@ type constr
 val string_of_constr : constr -> string
 
 (* this prototype version deliberately excludes calling functions from the context *)
-val statement_of_entailment : staged_spec -> staged_spec -> constr option
+val statement_of_entailment : staged_spec -> staged_spec -> constr
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index f2652f37..f7a6a6f8 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -598,15 +598,16 @@ module Entail_result : sig
   val entail_failure : entailment_result
   val result_of_pctx : pctx -> staged_spec -> staged_spec -> entailment_result
   val entailment_succeeded : entailment_result -> bool
-  val statement_of_entailment : entailment_result -> Certificate.constr option
-  val certificate_of_entailment : entailment_result -> coq_tactic Certificate.proof_log option
+  val theorem_of_entailment : entailment_result -> (Certificate.constr * coq_tactic Certificate.proof_log) option
 end = struct 
   type entailment_result = pstate option
   let entail_failure = None
   let result_of_pctx pctx f1 f2 = Some (pctx, f1, f2)
   let entailment_succeeded = Option.is_some
-  let statement_of_entailment r = Option.bind r (fun (_, f1, f2) -> Certificate.statement_of_entailment f1 f2)
-  let certificate_of_entailment r = r |> Option.map (fun (pctx, _, _) -> Certificate.finalize_proof_log pctx.proof_log)
+  let theorem_of_entailment r = 
+    match r with
+    | Some (pctx, f1, f2) -> Some (Certificate.(statement_of_entailment f1 f2, finalize_proof_log pctx.proof_log))
+    | None -> None
 end
 
 type tactic = pstate -> pstate Iter.t

From cb98e397b461fff4081b486c38feee8a7adb2d30 Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Tue, 4 Nov 2025 17:17:19 +0800
Subject: [PATCH 5/9] log basic proof steps

---
 lib/hiplib/hiplib.ml          |  13 ++--
 lib/hipprover/certificate.ml  | 119 +++++++++++++++++++++++-----------
 lib/hipprover/certificate.mli |   6 ++
 lib/hipprover/entail.ml       |  85 +++++++++---------------
 4 files changed, 127 insertions(+), 96 deletions(-)

diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml
index 43a7598f..e2b732dc 100644
--- a/lib/hiplib/hiplib.ml
+++ b/lib/hiplib/hiplib.ml
@@ -83,15 +83,19 @@ let check_lambda_obligation_ name params lemmas predicates obl =
   check_obligation_ name params lemmas preds (obl.lo_left, obl.lo_right)
 *)
 
-let certificate_output : out_channel option ref = ref None
+let certificate_output : Hipprover.Certificate.certificate_file option ref = ref None
 
 let print_certificate name constr proof_log =
   let open Hipprover.Certificate in
   ignore proof_log;
   match !certificate_output with
   | None -> ()
-  | Some out_chan ->
-      Printf.fprintf out_chan "Theorem %s_correctness : %s.\nProof.\nAdmitted.\n\n" name (string_of_constr constr)
+  | Some file ->
+      write_theorem ~out:file
+        ~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
@@ -503,8 +507,9 @@ let preprocess_spec_comments =
 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)
+    | Some f -> certificate_output := Some (open_out f |> make_certificate_file)
     | None -> ()
   end;
   let chan = open_in input_file in
diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index cbb14317..aa3b9b12 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -2,10 +2,49 @@
 open Hipcore_typed.Typedhip
 open Hipcore_typed.Pretty
 
-exception Unsupported_term of string
-
 let config = default_config |> set_single_line
 
+type 'a proof_log =
+  | Step of 'a
+  | Subproof of 'a proof_log list
+
+(* a zipper over a proof log *)
+type 'a partial_proof_log = {
+  current_proof : 'a proof_log list;
+  parent_env : 'a partial_proof_log option
+}
+
+let empty_partial_log = {current_proof = []; parent_env = None}
+
+let proof_step s = Step s
+
+let append ppl step =
+  { ppl with current_proof = step :: ppl.current_proof }
+
+let open_subproof ppl = {
+  current_proof = [];
+  parent_env = Some ppl
+}
+
+let close_subproof ppl = 
+  let parent_env = Option.get ppl.parent_env in
+  let current_proof = Subproof (List.rev ppl.current_proof) :: parent_env.current_proof in
+  { parent_env with current_proof }
+
+let rec finalize_proof_log ppl =
+  match ppl.parent_env with
+  | None -> Subproof (List.rev ppl.current_proof)
+  | Some _ -> finalize_proof_log (close_subproof ppl)
+
+let rec string_of_proof_log ?(indent = 0) log string_of_step =
+  let indent_string = String.init indent (Fun.const ' ') in
+  match log with
+  | Step s -> indent_string ^ (string_of_step s) ^ "\n"
+  | Subproof steps ->
+      indent_string ^ "{\n" ^ 
+      (steps |> List.map (fun s -> string_of_proof_log ~indent:(indent + 2) s string_of_step) |> String.concat "") ^
+      indent_string ^ "}\n"
+
 type constr = CVar of string
   | CConst of const
   | CApp of constr * constr list
@@ -16,10 +55,12 @@ type constr = CVar of string
   (* invalid node, meant to allow for better context regarding incomplete constr generation *)
   | CError of string
 
+(* Do not throw an exception when processing an invalid node. Instead, return a CError. *)
+
 let rec hprop_of_kappa (k : kappa) : constr =
   match k with
   | SepConj (k1, k2) -> CInfix (hprop_of_kappa k1, "\\*", hprop_of_kappa k2)
-  | EmptyHeap -> CVar "\[]"
+  | EmptyHeap -> CVar "\\[]"
   | PointsTo (l, v) -> CInfix (CVar l, "~~>", constr_of_term v)
 and constr_of_term (t : term) : constr =
   match t.term_desc with
@@ -76,40 +117,40 @@ let rec string_of_constr c =
 
 let statement_of_entailment f1 f2 = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2])
 
-type 'a proof_log =
-  | Step of 'a
-  | Subproof of 'a proof_log list
-
-(* a zipper over a proof log *)
-type 'a partial_proof_log = {
-  current_proof : 'a proof_log list;
-  parent_env : 'a partial_proof_log option
-}
-
-let empty_partial_log = {current_proof = []; parent_env = None}
-
-let proof_step s = Step s
-
-let append ppl step =
-  { ppl with current_proof = step :: ppl.current_proof }
-
-let open_subproof ppl = {
-  current_proof = [];
-  parent_env = Some ppl
-}
+type certificate_file = out_channel
+
+let make_certificate_file out =
+  let prelude = {|
+From ShiftReset Require Import Logic Entl Automation Norm Propriety.
+From ShiftReset.Mechanized Require Import State Normalization Entail_tactics.
+
+(* Due to deficiencies in the underlying model, this is necessary to get some of the
+  needed rewrite operations (in particular, those manipulating the body of a [bind])
+  to succeed. If this admit is undesired, it may be possible to prove the needed instances
+  of RewritableBinder individually. *)
+
+#[global]
+Instance RewritableBinder_anything : forall f, RewritableBinder f.
+Proof.
+Admitted.
+
+(* end prelude *)
+
+|}
+  in
+  Printf.fprintf out "%s" prelude;
+  out
+
+let write_theorem ~out ~name ~statement ~string_of_step log =
+  Printf.fprintf out "(* begin proof item %s *)\n" name;
+  Printf.fprintf out "Theorem %s : %s.\n" name (string_of_constr statement);
+  Printf.fprintf out "Proof. rew_hprop_to_state.\n";
+  begin match log with
+  | None -> Printf.fprintf out "Admitted.\n"
+  | Some log -> Printf.fprintf out "%s" (string_of_proof_log log string_of_step);
+    Printf.fprintf out "Qed.\n"
+  end;
+  Printf.fprintf out "(* end proof item %s *)\n\n" name;
+  Out_channel.flush out
+  
 
-let close_subproof ppl = 
-  let parent_env = Option.get ppl.parent_env in
-  let current_proof = Subproof (List.rev ppl.current_proof) :: parent_env.current_proof in
-  { parent_env with current_proof }
-
-
-let finalize_proof_log ppl =
-  match ppl.parent_env with
-  | None -> Subproof ppl.current_proof
-  | Some _ -> failwith "Attempt to finalize unfinished proof log"
-
-let rec close_all_subproofs ppl =
-  match ppl.parent_env with
-  | None -> ppl
-  | Some _ -> close_all_subproofs (close_subproof ppl)
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index eac298e4..8d4a0a96 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -39,3 +39,9 @@ val string_of_constr : constr -> string
 
 (* this prototype version deliberately excludes calling functions from the context *)
 val statement_of_entailment : staged_spec -> staged_spec -> constr
+
+type certificate_file
+
+val make_certificate_file : out_channel -> certificate_file
+
+val write_theorem : out:certificate_file -> name:string -> statement:constr -> string_of_step:('a -> string) -> 'a proof_log option -> unit
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index f7a6a6f8..aca7434b 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -15,64 +15,27 @@ open Utils.Hstdlib
   | `Right -> Format.asprintf "%s, R" f *)
 
 type coq_tactic =
-  | Rewrite of string
-  | SRReduction
   | Simplify
   | Biab
-  | EntDisjL
-  | EntDisjR
-  | Focus of coq_tactic list
-
-type coq_tactics = coq_tactic list
-
-let rec string_of_coq_tactic t =
-  match t with
-  | EntDisjL -> "apply ent_disj_l."
-  | EntDisjR -> "apply ent_disj_l."
-  | Focus [] -> ""
-  | Focus [a] -> Format.asprintf "{ %s }" (string_of_coq_tactic a)
-  | Focus (a :: rest) ->
-    Format.asprintf "{ %s\n%s }" (string_of_coq_tactic a)
-      (string_of_list_ind_lines string_of_coq_tactic rest)
+  | Match_ens
+  | Solve_single
+  | Solve_empty
+  | Intro_exists of binder
+  | Inst_exists of term
+  | Inst_forall of term
+
+let string_of_coq_tactic tac =
+  let config = (default_config |> set_single_line) in
+  match tac with
   | Simplify -> "fsimpl."
   | Biab -> "fbiabduction."
-  | SRReduction -> "freduction."
-  | Rewrite r -> Format.asprintf "rewrite %s." r
+  | Match_ens -> "fmatch_ens."
+  | Solve_single -> "fsingle_ens."
+  | Solve_empty -> "fempty."
+  | Intro_exists t -> "fdestruct " ^ (ident_of_binder t) ^ "."
+  | Inst_exists t -> "fexists " ^ (string_of_term ~config t) ^ "."
+  | Inst_forall t -> "finst_lhs_all " ^ (string_of_term ~config t) ^ "."
 
-and string_of_coq_tactics ts =
-  ts |> List.map string_of_coq_tactic |> String.concat "\n"
-
-let%expect_test _ =
-  Format.printf "%s@."
-    (string_of_coq_tactics
-       [
-         EntDisjL;
-         Focus
-           [
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-             EntDisjR;
-             EntDisjL;
-           ];
-         Focus [EntDisjR];
-       ]);
-  [%expect
-    {|
-    apply ent_disj_l.
-    { apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l.
-      apply ent_disj_l. }
-    { apply ent_disj_l. }
-    |}]
 type use = Use of string [@@unboxed]
 
 let string_of_use (Use f) = f
@@ -144,6 +107,15 @@ let new_pctx () =
     proof_log = Certificate.empty_partial_log
   }
 
+let log_proof_step pctx tactic = 
+  { pctx with proof_log = Certificate.(append pctx.proof_log (proof_step tactic)) }
+
+let open_subproof_log pctx =
+  { pctx with proof_log = Certificate.open_subproof pctx.proof_log }
+
+let close_subproof_log pctx =
+  { pctx with proof_log = Certificate.open_subproof pctx.proof_log }
+
 let has_been_unfolded pctx name _lr =
   pctx.unfolded
   |> List.find_opt
@@ -696,6 +668,7 @@ let rec repeat_simplify_lhs ?(limit = 5) (spec : staged_spec) : staged_spec =
 
 let simplify : total =
  fun (pctx, f1, f2) ->
+  let pctx = log_proof_step pctx Simplify in
   let@ _ =
     span (fun r -> log_proof_state_total ~title:"simplify" (pctx, f1, f2) r)
   in
@@ -869,6 +842,7 @@ let rec apply_ent_rule ?name : tactic =
   | NormalReturn (True, EmptyHeap), NormalReturn (True, EmptyHeap)
   | Require (True, EmptyHeap), Require (True, EmptyHeap) ->
     (* | Require (True, EmptyHeap), Require (True, EmptyHeap) -> *)
+    let pctx = log_proof_step pctx Solve_empty in
     k (pctx, ens (), ens ())
   (* | ( Sequence (NormalReturn (True, EmptyHeap), f1),
       Sequence (NormalReturn (True, EmptyHeap), f2) )
@@ -1043,6 +1017,7 @@ let rec apply_ent_rule ?name : tactic =
     let@ _ =
       span (fun _r -> log_proof_state ~title:"ent: ens ens" (pctx, f1, f2))
     in
+    let pctx = log_proof_step pctx Solve_single in
     let@ (ap, ah), (fp, fh) = biab h1 h2 in
     let valid =
       check_pure_obligation
@@ -1058,6 +1033,7 @@ let rec apply_ent_rule ?name : tactic =
     let@ _ =
       span (fun _r -> log_proof_state ~title:"ent: req req" (pctx, f1, f2))
     in
+    let pctx = log_proof_step pctx Solve_single in
     apply_ent_rule ?name (pctx, NormalReturn (p2, h2), NormalReturn (p1, h1)) k
   | Sequence (NormalReturn (p1, h1), f3), Sequence (NormalReturn (p2, h2), f4)
     ->
@@ -1070,6 +1046,7 @@ let rec apply_ent_rule ?name : tactic =
         (conj (pctx.assumptions @ [p1; Heap.xpure h1]))
         (conj [p2; ap; Heap.xpure h2])
     in
+    let pctx = log_proof_step pctx Match_ens in
     if valid then
       entailment_search ?name
         (pctx, seq [req ~h:ah (); f3], seq [req ~h:fh (); f4])
@@ -1134,6 +1111,7 @@ let rec apply_ent_rule ?name : tactic =
       in
       { pctx with constants = var_of_binder x :: pctx.constants }
     in
+    let pctx = log_proof_step pctx (Intro_exists x) in
     entailment_search ?name (pctx, f3, f2) k
   | f1, ForAll (x, f4) ->
     let pctx =
@@ -1165,6 +1143,7 @@ let rec apply_ent_rule ?name : tactic =
                 ~title:(Format.asprintf "ent: exists on the right; [%s/%s]" (string_of_term c) (string_of_binder x))
                 (pctx, f1, f2))
             in
+            let pctx = log_proof_step pctx (Inst_exists c) in
             entailment_search ?name (pctx, f1, f4) k1
           else (fun _ -> fail))
     in

From eccf924b2d03a72b6c935fb311b1e204252bed87 Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Wed, 5 Nov 2025 17:47:35 +0800
Subject: [PATCH 6/9] extend usable tactics

---
 lib/hipprover/certificate.ml  | 56 ++++++++++++++++++++++++++++-------
 lib/hipprover/certificate.mli |  1 +
 lib/hipprover/entail.ml       | 14 ++++-----
 3 files changed, 54 insertions(+), 17 deletions(-)

diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index aa3b9b12..2816476b 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -57,6 +57,8 @@ type constr = CVar of string
 
 (* Do not throw an exception when processing an invalid node. Instead, return a CError. *)
 
+let pi_mentions_result p = Hipcore_typed.(Syntax.conjuncts_of_pi p |> List.exists Variables.is_eq_res)
+
 let rec hprop_of_kappa (k : kappa) : constr =
   match k with
   | SepConj (k1, k2) -> CInfix (hprop_of_kappa k1, "\\*", hprop_of_kappa k2)
@@ -66,6 +68,12 @@ and constr_of_term (t : term) : constr =
   match t.term_desc with
   | Const c -> CConst c
   | Var v -> CVar v
+  | BinOp (op, lhs, rhs) ->
+      let op_fun = match op with
+        | Plus -> CVar "vplus"
+        | _ -> CError "[binary operation]"
+      in
+      CApp (op_fun, [constr_of_term lhs; constr_of_term rhs])
   | _ -> CError (string_of_term ~config t)
 and constr_of_pi (p : pi) : constr =
   match p with
@@ -75,14 +83,20 @@ and constr_of_pi (p : pi) : constr =
   | Or (lhs, rhs) -> CInfix (constr_of_pi lhs, "\\/", constr_of_pi rhs)
   | Imply (lhs, rhs) -> CInfix (constr_of_pi lhs, "->", constr_of_pi rhs)
   | Atomic (op, lhs, rhs) ->
-      let operator = match op with
-        | EQ -> "="
-        | GT -> ">"
-        | LT -> "<"
-        | GTEQ -> ">="
-        | LTEQ -> "<="
-      in
-      CInfix (constr_of_term lhs, operator, constr_of_term rhs)
+      (* if this is a result comparison, insert a cast to [val] *)
+      begin
+      match Hipcore_typed.Variables.eq_res_term p with
+      | Some t -> CInfix (CVar "res", "=", CApp (CVar "into", [constr_of_term t]))
+      | None ->
+        let operator = match op with
+          | EQ -> "="
+          | GT -> ">"
+          | LT -> "<"
+          | GTEQ -> ">="
+          | LTEQ -> "<="
+        in
+        CInfix (constr_of_term lhs, operator, constr_of_term rhs)
+      end
   | _ -> CError (string_of_pi ~config p)
 and constr_of_state ((p, k) : state) =
   CInfix (hprop_of_kappa k, "\\*", CSurround ("\\[", constr_of_pi p, "]"))
@@ -92,10 +106,23 @@ and constr_of_staged_spec (ss : staged_spec) : constr =
   | ForAll (v, ss) -> CApp (CVar "fall", [CFun (ident_of_binder v, constr_of_staged_spec ss)])
   | Require (p, k) -> CApp (CVar "req_", [constr_of_state (p, k)])
   (* need to convert anything that says nothing about the result to an [ens_] ... *)
-  | NormalReturn (p, k) -> CApp (CVar "ens", [CFun ("res", constr_of_state (p, k))])
+  | NormalReturn (p, k) -> 
+      if pi_mentions_result p
+      then CApp (CVar "ens", [CFun ("res", constr_of_state (p, k))])
+      else CApp (CVar "ens_", [constr_of_state (p, k)])
+  | Sequence (Require (p, k), f) -> CApp (CVar "req", [constr_of_state (p, k); constr_of_staged_spec f])
   | Sequence (f1, f2) -> CInfix (constr_of_staged_spec f1, ";;", constr_of_staged_spec f2)
   | Disjunction (f1, f2) -> CApp (CVar "disj", [constr_of_staged_spec f1; constr_of_staged_spec f2])
-  | Bind (v, f1, f2) -> CApp (CVar "bind_t", [constr_of_staged_spec f1; CFun (ident_of_binder v, constr_of_staged_spec f2)])
+  | Bind (v, f1, f2) -> 
+      let bind f fk = match type_of_binder v with
+        | Int -> CApp (CVar "@bind_t", [CVar "int"; CVar "_"; f; fk])
+        | TConstr ("ref", _) -> CApp (CVar "@bind_t", [CVar "loc"; CVar "_"; f; fk])
+        (* let Coq infer the underlying type *)
+        (* if the bound variable is unused, it infers Int, which breaks some of the rewriting rules *)
+        (* there might need to be a better special case for that scenario... *)
+        | _ -> CApp (CVar "bind_t", [f; fk])
+      in
+      bind (constr_of_staged_spec f1) (CFun (ident_of_binder v, constr_of_staged_spec f2))
   | _ -> CError (string_of_staged_spec ~config ss)
 
 let rec string_of_constr c =
@@ -115,6 +142,7 @@ let rec string_of_constr c =
   | CSurround (lp, sub, rp) -> Printf.sprintf "%s %s %s" lp (string_of_constr sub) rp
   | CError s -> Printf.sprintf "(* unsupported node: %s *) _" s
 
+(* TODO quantify all free vars *)
 let statement_of_entailment f1 f2 = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2])
 
 type certificate_file = out_channel
@@ -134,6 +162,14 @@ Instance RewritableBinder_anything : forall f, RewritableBinder f.
 Proof.
 Admitted.
 
+(* primitive function declarations *)
+
+Definition vplus (a b:val) : val :=
+  match a, b with
+  | vint a, vint b => vint (a + b)
+  | _, _ => vunit
+  end.
+
 (* end prelude *)
 
 |}
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index 8d4a0a96..c2f08adc 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -37,6 +37,7 @@ type constr
 
 val string_of_constr : constr -> string
 
+val constr_of_term : term -> constr
 (* this prototype version deliberately excludes calling functions from the context *)
 val statement_of_entailment : staged_spec -> staged_spec -> constr
 
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index aca7434b..567cc478 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -25,16 +25,15 @@ type coq_tactic =
   | Inst_forall of term
 
 let string_of_coq_tactic tac =
-  let config = (default_config |> set_single_line) in
   match tac with
   | Simplify -> "fsimpl."
-  | Biab -> "fbiabduction."
+  | Biab -> "fbiab_state."
   | Match_ens -> "fmatch_ens."
   | Solve_single -> "fsingle_ens."
   | Solve_empty -> "fempty."
   | Intro_exists t -> "fdestruct " ^ (ident_of_binder t) ^ "."
-  | Inst_exists t -> "fexists " ^ (string_of_term ~config t) ^ "."
-  | Inst_forall t -> "finst_lhs_all " ^ (string_of_term ~config t) ^ "."
+  | Inst_exists t -> "fexists " ^ (Certificate.(string_of_constr (constr_of_term t))) ^ "."
+  | Inst_forall t -> "finst_lhs_all " ^ Certificate.(string_of_constr (constr_of_term t)) ^ "."
 
 type use = Use of string [@@unboxed]
 
@@ -973,7 +972,7 @@ let rec apply_ent_rule ?name : tactic =
       | Atomic (EQ, t1, t2) when t2.term_desc = Var (ident_of_binder y) -> Some t1
       | _ -> None
     in
-    let f1 =
+    let f1, pctx =
       match Lists.find_delete_map find_equality eqs with
       | None ->
         seq
@@ -981,7 +980,7 @@ let rec apply_ent_rule ?name : tactic =
             Require (conj (p2 :: eqs), sep_conj a);
             NormalReturn (p1, sep_conj f);
             f3;
-          ]
+          ], pctx
       | Some (t, eqs) ->
         debug ~at:5 ~title:"ent: biab f inst with" "[%s/%s]" (string_of_term t) (string_of_binder y);
         seq
@@ -989,8 +988,9 @@ let rec apply_ent_rule ?name : tactic =
             Require (conj (p2 :: eqs), sep_conj a);
             NormalReturn (p1, sep_conj f);
             Subst.subst_free_vars [(ident_of_binder y, t)] f3;
-          ]
+          ], log_proof_step pctx (Inst_forall t)
     in
+    let pctx = log_proof_step pctx Biab in
     entailment_search ?name (pctx, f1, f2) k
   (*
   | ( Sequence

From a33e35a12ab150ef36b70a0ace08933c8997c3ad Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Fri, 7 Nov 2025 12:44:25 +0800
Subject: [PATCH 7/9] add intro tactic and previously proven functions

---
 lib/hipcore_typed/subst.ml    | 10 +++++
 lib/hiplib/hiplib.ml          |  5 ++-
 lib/hipprover/certificate.ml  | 81 +++++++++++++++++++++++++++++------
 lib/hipprover/certificate.mli |  4 +-
 lib/hipprover/entail.ml       | 10 ++++-
 5 files changed, 94 insertions(+), 16 deletions(-)

diff --git a/lib/hipcore_typed/subst.ml b/lib/hipcore_typed/subst.ml
index ed12a439..80d1d854 100644
--- a/lib/hipcore_typed/subst.ml
+++ b/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
diff --git a/lib/hiplib/hiplib.ml b/lib/hiplib/hiplib.ml
index e2b732dc..5aced0b3 100644
--- a/lib/hiplib/hiplib.ml
+++ b/lib/hiplib/hiplib.ml
@@ -85,13 +85,14 @@ let check_lambda_obligation_ name params lemmas predicates obl =
 
 let certificate_output : Hipprover.Certificate.certificate_file option ref = ref None
 
-let print_certificate name constr proof_log =
+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
@@ -253,7 +254,7 @@ let analyze_method (prog : core_program) (meth : meth_def) : core_program =
         let open Hipprover.Entail.Entail_result in
         match theorem_of_entailment result with
         | Some (statement, proof) ->
-            print_certificate meth.m_name statement proof;
+            print_certificate prog meth.m_name statement proof;
             add_predicate prog meth.m_name meth.m_params inferred_spec
         | None -> prog
   in
diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index 2816476b..5b232e22 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -54,6 +54,7 @@ type constr = CVar of string
   | CSurround of string * constr * string
   (* invalid node, meant to allow for better context regarding incomplete constr generation *)
   | CError of string
+  | CQuantify of string * string list * constr
 
 (* Do not throw an exception when processing an invalid node. Instead, return a CError. *)
 
@@ -88,15 +89,17 @@ and constr_of_pi (p : pi) : constr =
       match Hipcore_typed.Variables.eq_res_term p with
       | Some t -> CInfix (CVar "res", "=", CApp (CVar "into", [constr_of_term t]))
       | None ->
+        (* NOTE: these are currently implemented to only compare integers! *)
         let operator = match op with
-          | EQ -> "="
-          | GT -> ">"
-          | LT -> "<"
-          | GTEQ -> ">="
-          | LTEQ -> "<="
+          | EQ -> "veq"
+          | GT -> "vgt"
+          | LT -> "vlt"
+          | GTEQ -> "vge"
+          | LTEQ -> "vle"
         in
-        CInfix (constr_of_term lhs, operator, constr_of_term rhs)
+        CApp (CVar operator, [constr_of_term lhs; constr_of_term rhs])
       end
+  | Not p -> CSurround ("~", constr_of_pi p, "")
   | _ -> CError (string_of_pi ~config p)
 and constr_of_state ((p, k) : state) =
   CInfix (hprop_of_kappa k, "\\*", CSurround ("\\[", constr_of_pi p, "]"))
@@ -105,6 +108,8 @@ and constr_of_staged_spec (ss : staged_spec) : constr =
   | Exists (v, ss) -> CApp (CVar "fex", [CFun (ident_of_binder v, constr_of_staged_spec ss)])
   | ForAll (v, ss) -> CApp (CVar "fall", [CFun (ident_of_binder v, constr_of_staged_spec ss)])
   | Require (p, k) -> CApp (CVar "req_", [constr_of_state (p, k)])
+  (* support only one argument for now, pack multiple arguments via vtup...? *)
+  | HigherOrder (f, [arg]) -> CApp (CVar "unk", [CConst (TStr f); constr_of_term arg])
   (* need to convert anything that says nothing about the result to an [ens_] ... *)
   | NormalReturn (p, k) -> 
       if pi_mentions_result p
@@ -128,7 +133,7 @@ and constr_of_staged_spec (ss : staged_spec) : constr =
 let rec string_of_constr c =
   match c with
   | CConst c -> begin match c with
-    | ValUnit -> "tt"
+    | ValUnit -> "vunit"
     | TStr s -> "\"" ^ s ^ "\""
     | Num n -> string_of_int n
     | Nil -> "[]"
@@ -141,9 +146,48 @@ let rec string_of_constr c =
   | CInfix (lhs, op, rhs) -> Printf.sprintf "(%s %s %s)" (string_of_constr lhs) op (string_of_constr rhs)
   | CSurround (lp, sub, rp) -> Printf.sprintf "%s %s %s" lp (string_of_constr sub) rp
   | CError s -> Printf.sprintf "(* unsupported node: %s *) _" s
+  | CQuantify (q, vars, body) -> Printf.sprintf "%s %s, %s" q (String.concat " " vars) (string_of_constr body)
+
+let quantify vars constr =
+  match vars with
+  | [] -> constr
+  | free_vars -> CQuantify ("forall", free_vars, constr)
+
+let remove_nonterm_variables free_var_mapping =
+  free_var_mapping
+  |> Utils.Hstdlib.SMap.to_list
+  |> List.filter_map (fun (fv, ty) ->
+      match ty with
+      | None -> None
+      | Some _ -> Some fv)
 
 (* TODO quantify all free vars *)
-let statement_of_entailment f1 f2 = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2])
+let statement_of_entailment f1 f2 = 
+  let free_vars = 
+    let open Utils.Hstdlib in
+    let open Hipcore_typed.Subst in
+    SMap.merge_arbitrary (types_of_free_vars Sctx_staged f1) (types_of_free_vars Sctx_staged f2)
+    |> SMap.remove "res"
+    |> remove_nonterm_variables
+  in
+  (* Printf.printf "SOE fv [%s] end\n" (String.concat "; " free_vars); *)
+  let entailment = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2]) in
+  quantify free_vars entailment
+
+let statement_of_method name params spec =
+  match params with
+  | [p] -> 
+    let free_vars =
+      let open Hipcore_typed.Subst in
+      let open Utils.Hstdlib in
+      types_of_free_vars Sctx_staged spec
+      |> SMap.add (ident_of_binder p) (Some (type_of_binder p))
+      |> remove_nonterm_variables
+    in
+    (* Printf.printf "SOM %s fv [%s] end\n" name (String.concat "; " free_vars); *)
+    CQuantify ("forall", free_vars,
+    CApp (CVar "entails", [CApp (CVar "unk", [CConst (TStr name); CVar (ident_of_binder p)]); constr_of_staged_spec spec]))
+  | _ -> CError ("unsupported method " ^ name)
 
 type certificate_file = out_channel
 
@@ -152,6 +196,8 @@ let make_certificate_file out =
 From ShiftReset Require Import Logic Entl Automation Norm Propriety.
 From ShiftReset.Mechanized Require Import State Normalization Entail_tactics.
 
+Local Open Scope string_scope.
+
 (* Due to deficiencies in the underlying model, this is necessary to get some of the
   needed rewrite operations (in particular, those manipulating the body of a [bind])
   to succeed. If this admit is undesired, it may be possible to prove the needed instances
@@ -177,10 +223,19 @@ Definition vplus (a b:val) : val :=
   Printf.fprintf out "%s" prelude;
   out
 
-let write_theorem ~out ~name ~statement ~string_of_step log =
+let write_theorem ~out ~program ~name ~statement ~string_of_step log =
+  (* Printf.printf "writing theorem for %s\n" name; *)
+  (* Printf.printf "statement: %s\n" (string_of_constr statement); *)
+  let theorem_params =
+    program.cp_predicates
+    |> Utils.Hstdlib.SMap.to_list
+    |> List.map (fun (_, pred_def) -> 
+        let statement = statement_of_method pred_def.p_name pred_def.p_params pred_def.p_body in
+        Printf.sprintf "(%s_rewrite_rule : %s)" pred_def.p_name (string_of_constr statement))
+  in
   Printf.fprintf out "(* begin proof item %s *)\n" name;
-  Printf.fprintf out "Theorem %s : %s.\n" name (string_of_constr statement);
-  Printf.fprintf out "Proof. rew_hprop_to_state.\n";
+  Printf.fprintf out "Theorem %s %s\n : %s.\n" name (String.concat "\n  " theorem_params) (string_of_constr statement);
+  Printf.fprintf out "Proof. intros. rew_hprop_to_state.\n";
   begin match log with
   | None -> Printf.fprintf out "Admitted.\n"
   | Some log -> Printf.fprintf out "%s" (string_of_proof_log log string_of_step);
@@ -189,4 +244,6 @@ let write_theorem ~out ~name ~statement ~string_of_step log =
   Printf.fprintf out "(* end proof item %s *)\n\n" name;
   Out_channel.flush out
   
-
+let write_assumption ~out ~name ~statement =
+  Printf.fprintf out "Parameter %s: %s.\n\n" name (string_of_constr statement);
+  Out_channel.flush out;
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index c2f08adc..a29e79f6 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -45,4 +45,6 @@ type certificate_file
 
 val make_certificate_file : out_channel -> certificate_file
 
-val write_theorem : out:certificate_file -> name:string -> statement:constr -> string_of_step:('a -> string) -> 'a proof_log option -> unit
+val write_theorem : out:certificate_file -> program:core_program -> name:string -> statement:constr -> string_of_step:('a -> string) -> 'a proof_log option -> unit
+
+val write_assumption : out:certificate_file -> name:string -> statement:constr -> unit
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index 567cc478..531fe710 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -16,6 +16,8 @@ open Utils.Hstdlib
 
 type coq_tactic =
   | Simplify
+  | Unfold_nonrec
+  | Intro_pure_assumption
   | Biab
   | Match_ens
   | Solve_single
@@ -27,6 +29,8 @@ type coq_tactic =
 let string_of_coq_tactic tac =
   match tac with
   | Simplify -> "fsimpl."
+  | Unfold_nonrec -> "funfold_from_ctx."
+  | Intro_pure_assumption -> "fpure_assumption."
   | Biab -> "fbiab_state."
   | Match_ens -> "fmatch_ens."
   | Solve_single -> "fsingle_ens."
@@ -667,11 +671,13 @@ let rec repeat_simplify_lhs ?(limit = 5) (spec : staged_spec) : staged_spec =
 
 let simplify : total =
  fun (pctx, f1, f2) ->
-  let pctx = log_proof_step pctx Simplify in
+   (* TODO apply this simplify step after folding recursive definitions *)
   let@ _ =
     span (fun r -> log_proof_state_total ~title:"simplify" (pctx, f1, f2) r)
   in
+  let pctx = log_proof_step pctx Unfold_nonrec in
   let pctx, f1, f2 = unfold_nonrecursive_definitions (pctx, f1, f2) in
+  let pctx = log_proof_step pctx Simplify in
   let f1 = repeat_simplify_lhs f1 in
   let f2 = Normalize.normalize_spec_rhs f2 in
   (pctx, f1, f2)
@@ -915,6 +921,7 @@ let rec apply_ent_rule ?name : tactic =
         span (fun _r ->
             log_proof_state ~title:"ent: pure assumption" (pctx, f1, f2))
       in
+      let pctx = log_proof_step pctx Intro_pure_assumption in
       { pctx with assumptions = p1 :: pctx.assumptions }
     in
     entailment_search ?name (pctx, f3, f2) k
@@ -924,6 +931,7 @@ let rec apply_ent_rule ?name : tactic =
         span (fun _r ->
             log_proof_state ~title:"ent: pure assumption" (pctx, f1, f2))
       in
+      let pctx = log_proof_step pctx Intro_pure_assumption in
       { pctx with assumptions = p2 :: pctx.assumptions }
     in
     entailment_search ?name (pctx, f1, f4) k

From de049998e1444d12d24c4d4998564e123f6b646a Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Mon, 10 Nov 2025 13:49:00 +0800
Subject: [PATCH 8/9] implement disj tactics

---
 lib/hipprover/certificate.ml | 44 +++++++++++++++++++++++++++++++-----
 lib/hipprover/entail.ml      | 28 ++++++++++++++++++++---
 2 files changed, 63 insertions(+), 9 deletions(-)

diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index 5b232e22..5d2ea7b9 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -45,6 +45,37 @@ let rec string_of_proof_log ?(indent = 0) log string_of_step =
       (steps |> List.map (fun s -> string_of_proof_log ~indent:(indent + 2) s string_of_step) |> String.concat "") ^
       indent_string ^ "}\n"
 
+let%expect_test "proof logging" =
+  let output_log log = 
+    Printf.printf "%s\n" (string_of_proof_log log Fun.id)
+  in 
+  let log = empty_partial_log in
+  let log = append log (proof_step "intros.") in
+  let log = append log (proof_step "split.") in
+  let log = open_subproof log in
+    let log = append log (proof_step "exfalso.") in
+    let log = append log (proof_step "assumption.") in
+  let log = close_subproof log in
+  let log = open_subproof log in
+    let log = append log (proof_step "auto.") in
+  let log = close_subproof log in
+  output_log (finalize_proof_log log);
+  [%expect {|
+    {
+      intros.
+      split.
+      {
+        exfalso.
+        assumption.
+      }
+      {
+        auto.
+      }
+    }
+    |}];;
+  
+
+
 type constr = CVar of string
   | CConst of const
   | CApp of constr * constr list
@@ -69,6 +100,7 @@ and constr_of_term (t : term) : constr =
   match t.term_desc with
   | Const c -> CConst c
   | Var v -> CVar v
+  | TNot t -> CApp (CVar "vnot", [constr_of_term t])
   | BinOp (op, lhs, rhs) ->
       let op_fun = match op with
         | Plus -> CVar "vplus"
@@ -91,13 +123,13 @@ and constr_of_pi (p : pi) : constr =
       | None ->
         (* NOTE: these are currently implemented to only compare integers! *)
         let operator = match op with
-          | EQ -> "veq"
-          | GT -> "vgt"
-          | LT -> "vlt"
-          | GTEQ -> "vge"
-          | LTEQ -> "vle"
+          | EQ -> "="
+          | GT -> ">"
+          | LT -> "<"
+          | GTEQ -> ">="
+          | LTEQ -> "<="
         in
-        CApp (CVar operator, [constr_of_term lhs; constr_of_term rhs])
+        CInfix (constr_of_term lhs, operator, constr_of_term rhs)
       end
   | Not p -> CSurround ("~", constr_of_pi p, "")
   | _ -> CError (string_of_pi ~config p)
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index 531fe710..5e5f16a3 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -18,6 +18,8 @@ type coq_tactic =
   | Simplify
   | Unfold_nonrec
   | Intro_pure_assumption
+  | Split_disjunction
+  | Choose_disj_branch of [`Left | `Right]
   | Biab
   | Match_ens
   | Solve_single
@@ -31,6 +33,9 @@ let string_of_coq_tactic tac =
   | Simplify -> "fsimpl."
   | Unfold_nonrec -> "funfold_from_ctx."
   | Intro_pure_assumption -> "fpure_assumption."
+  | Split_disjunction -> "fsplit_disj."
+  | Choose_disj_branch `Left -> "fdisj_left_state."
+  | Choose_disj_branch `Right -> "fdisj_right_state."
   | Biab -> "fbiab_state."
   | Match_ens -> "fmatch_ens."
   | Solve_single -> "fsingle_ens."
@@ -117,7 +122,7 @@ let open_subproof_log pctx =
   { pctx with proof_log = Certificate.open_subproof pctx.proof_log }
 
 let close_subproof_log pctx =
-  { pctx with proof_log = Certificate.open_subproof pctx.proof_log }
+  { pctx with proof_log = Certificate.close_subproof pctx.proof_log }
 
 let has_been_unfolded pctx name _lr =
   pctx.unfolded
@@ -792,6 +797,7 @@ let prove_pure_fact (pctx : pctx) (p : pi) =
 
 let rec handle_pure_ens_lhs (pctx : pctx) f =
   debug ~at:5 ~title:"handle_pure_ens_lhs" "%s " (string_of_staged_spec f);
+  let pctx = log_proof_step pctx Intro_pure_assumption in
   match f with
   | NormalReturn (p, EmptyHeap) when not (Variables.is_eq_res p) ->
       add_assumption pctx p, NormalReturn (True, EmptyHeap)
@@ -1068,24 +1074,27 @@ let rec apply_ent_rule ?name : tactic =
       k
   | Disjunction (f3, f4), f2 ->
     let tag = Variables.fresh_variable () in
+    let pctx = log_proof_step pctx Split_disjunction in
     let@ _ =
       span (fun _r ->
           debug ~at:4 ~title:(Format.asprintf "disj on the left [[%s]]" tag) "")
     in
-    let@ _ = entailment_search ?name (pctx, f3, f2) in
+    let@ (pctx, _, _) = entail_subgoal ?name (pctx, f3, f2) in
     let@ _ =
       span (fun _r ->
           debug ~at:4 ~title:(Format.asprintf "right disjunct <<%s>>" tag) "")
     in
-    entailment_search ?name (pctx, f4, f2) k
+    entail_subgoal ?name (pctx, f4, f2) k
   | f1, Disjunction (f3, f4) ->
     debug ~at:4 ~title:"disj on the right" "";
     or_
       (fun k1 ->
         let@ _ = span (fun _r -> debug ~at:4 ~title:"left disjunct" "") in
+        let pctx = log_proof_step pctx (Choose_disj_branch `Left) in
         entailment_search ?name (pctx, f1, f3) k1)
       (fun k1 ->
         let@ _ = span (fun _r -> debug ~at:4 ~title:"right disjunct" "") in
+        let pctx = log_proof_step pctx (Choose_disj_branch `Right) in
         entailment_search ?name (pctx, f1, f4) k1)
       k
   (* two functions with equal terms *)
@@ -1235,6 +1244,19 @@ let rec apply_ent_rule ?name : tactic =
           then k (pctx, ens (), ens ())
           else (log_proof_state ~title:"STUCK" ps; fail)
 
+(** A wrapper for [entailment_search] that delineates this entailment as a focused subgoal
+  in the proof log. Note that unlike [entailment_search], the context this tactic outputs
+  must not be ignored. since the proof log of the subgoal is stored there. *)
+and entail_subgoal : ?name:string -> tactic =
+  fun ?name ps k ->
+    let (pctx, lhs, rhs) = ps in
+    let pctx_original = pctx in
+    let pctx = open_subproof_log pctx in
+    let@ (pctx, _, _) = entailment_search ?name (pctx, lhs, rhs) in
+    let pctx = close_subproof_log pctx in
+    (* preserve the original context, but copy over the proof log *)
+    k ({pctx_original with proof_log = pctx.proof_log}, lhs, rhs)
+
 and entailment_search : ?name:string -> tactic =
   let prev_state = ref None in
   fun ?name ps k ->

From 2dd4ea4387fd171efecb94a5651552bf37127b93 Mon Sep 17 00:00:00 2001
From: Dan Baterisna <alden.baterisna@yahoo.com>
Date: Mon, 10 Nov 2025 15:58:25 +0800
Subject: [PATCH 9/9] cleanup

---
 lib/hipprover/certificate.ml  | 3 ---
 lib/hipprover/certificate.mli | 2 +-
 lib/hipprover/entail.ml       | 1 -
 3 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/lib/hipprover/certificate.ml b/lib/hipprover/certificate.ml
index 5d2ea7b9..696ab472 100644
--- a/lib/hipprover/certificate.ml
+++ b/lib/hipprover/certificate.ml
@@ -193,7 +193,6 @@ let remove_nonterm_variables free_var_mapping =
       | None -> None
       | Some _ -> Some fv)
 
-(* TODO quantify all free vars *)
 let statement_of_entailment f1 f2 = 
   let free_vars = 
     let open Utils.Hstdlib in
@@ -202,7 +201,6 @@ let statement_of_entailment f1 f2 =
     |> SMap.remove "res"
     |> remove_nonterm_variables
   in
-  (* Printf.printf "SOE fv [%s] end\n" (String.concat "; " free_vars); *)
   let entailment = CApp (CVar "entails", [constr_of_staged_spec f1; constr_of_staged_spec f2]) in
   quantify free_vars entailment
 
@@ -216,7 +214,6 @@ let statement_of_method name params spec =
       |> SMap.add (ident_of_binder p) (Some (type_of_binder p))
       |> remove_nonterm_variables
     in
-    (* Printf.printf "SOM %s fv [%s] end\n" name (String.concat "; " free_vars); *)
     CQuantify ("forall", free_vars,
     CApp (CVar "entails", [CApp (CVar "unk", [CConst (TStr name); CVar (ident_of_binder p)]); constr_of_staged_spec spec]))
   | _ -> CError ("unsupported method " ^ name)
diff --git a/lib/hipprover/certificate.mli b/lib/hipprover/certificate.mli
index a29e79f6..81cfac99 100644
--- a/lib/hipprover/certificate.mli
+++ b/lib/hipprover/certificate.mli
@@ -38,7 +38,7 @@ type constr
 val string_of_constr : constr -> string
 
 val constr_of_term : term -> constr
-(* this prototype version deliberately excludes calling functions from the context *)
+
 val statement_of_entailment : staged_spec -> staged_spec -> constr
 
 type certificate_file
diff --git a/lib/hipprover/entail.ml b/lib/hipprover/entail.ml
index 5e5f16a3..d0a09dc3 100644
--- a/lib/hipprover/entail.ml
+++ b/lib/hipprover/entail.ml
@@ -676,7 +676,6 @@ let rec repeat_simplify_lhs ?(limit = 5) (spec : staged_spec) : staged_spec =
 
 let simplify : total =
  fun (pctx, f1, f2) ->
-   (* TODO apply this simplify step after folding recursive definitions *)
   let@ _ =
     span (fun r -> log_proof_state_total ~title:"simplify" (pctx, f1, f2) r)
   in