From 7da1899215d992e65047f313fa9520782b4fc61c Mon Sep 17 00:00:00 2001
From: Darius Foo <darius.foo.tw@gmail.com>
Date: Thu, 5 Mar 2026 14:19:30 +0800
Subject: [PATCH 1/2] Revive OCaml frontend

---
 Makefile                            |   8 +-
 src/heifer/dune                     |   2 +-
 src/ocamlfrontend/core_lang.ml      |  73 ++++++++++++
 src/ocamlfrontend/core_lang.mli     |  31 +++++
 src/ocamlfrontend/dune              |   9 ++
 src/ocamlfrontend/forward_rules.ml  |  60 ++++++++++
 src/ocamlfrontend/forward_rules.mli |   4 +
 src/ocamlfrontend/frontend.ml       | 171 ++++++++++++++++++++++++++++
 src/ocamlfrontend/frontend.mli      |   4 +
 src/ocamlfrontend/frontend_test.ml  |  76 +++++++++++++
 src/ocamlfrontend/obligations.ml    | 110 ++++++++++++++++++
 src/ocamlfrontend/obligations.mli   |  23 ++++
 src/ocamlfrontend/ocamlfrontend.ml  |  14 +++
 src/ocamlfrontend/ocamlfrontend.mli |   4 +
 src/prover/dune                     |   2 +-
 src/prover/interactive.ml           |  39 +++++--
 src/prover/interactive.mli          |   1 +
 src/prover/interactive_test.ml      |  52 ++++-----
 src/prover/pctx.ml                  |   4 +-
 src/prover/pctx.mli                 |   3 +-
 20 files changed, 645 insertions(+), 45 deletions(-)
 create mode 100644 src/ocamlfrontend/core_lang.ml
 create mode 100644 src/ocamlfrontend/core_lang.mli
 create mode 100644 src/ocamlfrontend/dune
 create mode 100644 src/ocamlfrontend/forward_rules.ml
 create mode 100644 src/ocamlfrontend/forward_rules.mli
 create mode 100644 src/ocamlfrontend/frontend.ml
 create mode 100644 src/ocamlfrontend/frontend.mli
 create mode 100644 src/ocamlfrontend/frontend_test.ml
 create mode 100644 src/ocamlfrontend/obligations.ml
 create mode 100644 src/ocamlfrontend/obligations.mli
 create mode 100644 src/ocamlfrontend/ocamlfrontend.ml
 create mode 100644 src/ocamlfrontend/ocamlfrontend.mli

diff --git a/Makefile b/Makefile
index c2f62917..5dca3efa 100644
--- a/Makefile
+++ b/Makefile
@@ -4,19 +4,19 @@ export OCAMLRUNPARAM=b
 all:
 	@echo 'note: running unit tests only'
 	@echo 'use make test to run fast integration tests, and make test-all to run all tests'
-	dune build src test @runtest --display=short
+	dune build src test @runtest
 
 .PHONY: test
 test:
-	TEST=1 dune test --display=short
+	TEST=1 dune test
 
 .PHONY: test-all
 test-all:
-	TEST_ALL=1 dune test --display=short
+	TEST_ALL=1 dune test
 
 .PHONY: w
 w:
-	dune build src @runtest -w --display=short
+	dune build src @runtest -w
 
 debug-menhir:
 	echo 'parse_term: TRUE' | menhir --dump --explain --interpret --interpret-show-cst --trace src/parse/parser.mly
diff --git a/src/heifer/dune b/src/heifer/dune
index 0101cd7f..f4e898fc 100644
--- a/src/heifer/dune
+++ b/src/heifer/dune
@@ -4,4 +4,4 @@
  ; heifer is often used interactively, so linkall is given here.
  ; this also avoids having to list all transitive dependencies in mdx
  (library_flags (-linkall))
- (libraries core parsing prover))
+ (libraries core ocamlfrontend parsing prover))
diff --git a/src/ocamlfrontend/core_lang.ml b/src/ocamlfrontend/core_lang.ml
new file mode 100644
index 00000000..04e63885
--- /dev/null
+++ b/src/ocamlfrontend/core_lang.ml
@@ -0,0 +1,73 @@
+type pattern =
+  | PVar of string
+  | PConstr of string * pattern list
+  | PAny
+  | PInt of int
+
+type expr =
+  | Var of string
+  | Int of int
+  | Fun of string list * expr
+  | Apply of expr * expr list
+  | Let of string * expr * expr
+  | If of expr * expr * expr
+  | Sequence of expr * expr
+  | Shift of string * expr
+  | Reset of expr
+  | Perform of string * expr option
+  | Resume of expr list
+  | Match of expr * (pattern * expr) list
+  | WithSpec of expr * string * string
+
+type verification_unit = {
+  pure_functions : (string * expr) list;
+  program_functions : (string * expr) list;
+}
+
+let rec dump_pattern ppf p =
+  match p with
+  | PVar x -> Format.fprintf ppf "%S" x
+  | PConstr (c, args) ->
+      Format.fprintf ppf "%s(%a)" c
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf ", ") dump_pattern)
+        args
+  | PAny -> Format.fprintf ppf "_"
+  | PInt i -> Format.fprintf ppf "%d" i
+
+let rec dump_term ppf t =
+  match t with
+  | Var x -> Format.fprintf ppf "Var %S" x
+  | Int i -> Format.fprintf ppf "Int %d" i
+  | Fun (xs, body) ->
+      Format.fprintf ppf "Fun ([%a], %a)"
+        (Format.pp_print_list
+           ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ")
+           (fun ppf x -> Format.fprintf ppf "%S" x))
+        xs dump_term body
+  | Apply (f, args) ->
+      Format.fprintf ppf "Apply (%a, [%a])" dump_term f
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") dump_term)
+        args
+  | Let (x, t1, t2) -> Format.fprintf ppf "Let (%S, %a, %a)" x dump_term t1 dump_term t2
+  | If (c, t1, t2) -> Format.fprintf ppf "If (%a, %a, %a)" dump_term c dump_term t1 dump_term t2
+  | Sequence (t1, t2) -> Format.fprintf ppf "Sequence (%a, %a)" dump_term t1 dump_term t2
+  | Shift (k, body) -> Format.fprintf ppf "Shift (%S, %a)" k dump_term body
+  | Reset t -> Format.fprintf ppf "Reset (%a)" dump_term t
+  | Perform (eff, arg) ->
+      Format.fprintf ppf "Perform (%S, %a)" eff
+        (fun ppf arg ->
+          match arg with
+          | None -> Format.fprintf ppf "None"
+          | Some t -> Format.fprintf ppf "Some (%a)" dump_term t)
+        arg
+  | Resume args ->
+      Format.fprintf ppf "Resume ([%a])"
+        (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") dump_term)
+        args
+  | Match (t, cases) ->
+      Format.fprintf ppf "Match (%a, [%a])" dump_term t
+        (Format.pp_print_list
+           ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ")
+           (fun ppf (p, e) -> Format.fprintf ppf "(%a, %a)" dump_pattern p dump_term e))
+        cases
+  | WithSpec (t, s, name) -> Format.fprintf ppf "WithSpec (%a, %S, %S)" dump_term t s name
diff --git a/src/ocamlfrontend/core_lang.mli b/src/ocamlfrontend/core_lang.mli
new file mode 100644
index 00000000..8a486f34
--- /dev/null
+++ b/src/ocamlfrontend/core_lang.mli
@@ -0,0 +1,31 @@
+
+type pattern =
+  | PVar of string
+  | PConstr of string * pattern list
+  | PAny  (** [_] *)
+  | PInt of int
+
+(** OCaml programs *)
+type expr =
+  | Var of string
+  | Int of int
+  | Fun of string list * expr
+  | Apply of expr * expr list
+  | Let of string * expr * expr
+  | If of expr * expr * expr
+  | Sequence of expr * expr
+  | Shift of string * expr
+  | Reset of expr
+  | Perform of string * expr option
+  | Resume of expr list
+  | Match of expr * (pattern * expr) list
+  | WithSpec of expr * string * string (* the :: operator, as an expr *)
+
+(** Analogous to a compilation unit; all the structure we get from a source file *)
+type verification_unit = {
+  pure_functions : (string * expr) list;
+  program_functions : (string * expr) list;
+}
+
+val dump_pattern : Format.formatter -> pattern -> unit
+val dump_term : Format.formatter -> expr -> unit
diff --git a/src/ocamlfrontend/dune b/src/ocamlfrontend/dune
new file mode 100644
index 00000000..23d92e95
--- /dev/null
+++ b/src/ocamlfrontend/dune
@@ -0,0 +1,9 @@
+
+(library
+ (name ocamlfrontend)
+ (public_name heifer.ocamlfrontend)
+ (inline_tests)
+ (libraries compiler-libs.common heifer.core bindlib str heifer.parsing)
+ (preprocess (pps ppx_expect)))
+
+(env (dev (flags (:standard -warn-error -A))))
\ No newline at end of file
diff --git a/src/ocamlfrontend/forward_rules.ml b/src/ocamlfrontend/forward_rules.ml
new file mode 100644
index 00000000..939d13da
--- /dev/null
+++ b/src/ocamlfrontend/forward_rules.ml
@@ -0,0 +1,60 @@
+open Core_lang
+open Core.Syntax
+
+let resolve_to_primitive f args =
+  match (f, args) with
+  | Core_lang.Var op, [arg1; arg2] ->
+      (match op with
+      | "+" -> Some (Mk.binop Plus arg1 arg2)
+      | "-" -> Some (Mk.binop Minus arg1 arg2)
+      | "*" | "*." ->
+          (* there is no separation logic in core lang, so this seems okay *)
+          Some (Mk.binop Times arg1 arg2)
+      | "=" -> Some (Mk.binop Eq arg1 arg2)
+      | "<>" -> Some (Mk.binop Neq arg1 arg2)
+      | "<" -> Some (Mk.binop Lt arg1 arg2)
+      | "<=" -> Some (Mk.binop Le arg1 arg2)
+      | ">" -> Some (Mk.binop Gt arg1 arg2)
+      | ">=" -> Some (Mk.binop Ge arg1 arg2)
+      | "::" -> Some (Mk.binop Cons arg1 arg2)
+      | _ -> None)
+  | Var op, [arg] ->
+      (match op with
+      | "not" -> Some (Mk.unop Not arg)
+      | "~-" | "-" -> Some (Mk.unop Neg arg)
+      | _ -> None)
+  | _ -> None
+
+let rec convert_box (env : (string * term Bindlib.var) list) (t : expr) : term Bindlib.box =
+  match t with
+  | Var x ->
+      (match List.assoc_opt x env with
+      | Some v -> Mk.var v
+      | None -> Mk.symbol { sym_name = x })
+  | Int i -> Mk.int i
+  | Fun (xs, body) ->
+      let vars = Array.map (fun x -> Bindlib.new_var (fun v -> Var v) x) (Array.of_list xs) in
+      let env' = List.combine xs (Array.to_list vars) @ env in
+      let body' = convert_box env' body in
+      Mk.fun_ (Bindlib.bind_mvar vars body')
+  | Apply (f, args) ->
+      let f_box = convert_box env f in
+      let args_box = List.map (convert_box env) args in
+      resolve_to_primitive f args_box
+      |> Option.value ~default:(Mk.apply f_box (Bindlib.box_list args_box))
+  | Let (x, t1, t2) ->
+      let v = Bindlib.new_var (fun v -> Var v) x in
+      let t1' = convert_box env t1 in
+      let t2' = convert_box ((x, v) :: env) t2 in
+      Mk.bind t1' (Bindlib.bind_var v t2')
+  | Sequence (t1, t2) -> Mk.sequence (convert_box env t1) (convert_box env t2)
+  | Shift (k, body) ->
+      let v = Bindlib.new_var (fun v -> Var v) k in
+      let body' = convert_box ((k, v) :: env) body in
+      Mk.shift (Bindlib.bind_var v body')
+  | Reset t1 -> Mk.reset (convert_box env t1)
+  | WithSpec (t, _spec, _name) -> convert_box env t
+  | Match _ | If _ | Perform _ | Resume _ ->
+      failwith "conversion to Syntax.term not yet supported for this construct"
+
+let apply (t : expr) : term = Bindlib.unbox (convert_box [] t)
diff --git a/src/ocamlfrontend/forward_rules.mli b/src/ocamlfrontend/forward_rules.mli
new file mode 100644
index 00000000..285a0cd5
--- /dev/null
+++ b/src/ocamlfrontend/forward_rules.mli
@@ -0,0 +1,4 @@
+open Core.Syntax
+open Core_lang
+
+val apply : expr -> term
diff --git a/src/ocamlfrontend/frontend.ml b/src/ocamlfrontend/frontend.ml
new file mode 100644
index 00000000..8d583280
--- /dev/null
+++ b/src/ocamlfrontend/frontend.ml
@@ -0,0 +1,171 @@
+open Parsetree
+open Asttypes
+open Core_lang
+
+let rec string_of_pattern_desc desc : string =
+  match desc with
+  | Ppat_any -> "_"
+  | Ppat_var str -> str.txt
+  | Ppat_constant { pconst_desc = Pconst_integer (i, _); _ } -> i
+  | Ppat_constant { pconst_desc = Pconst_string (s, _, _); _ } -> s
+  | Ppat_construct (l, _) -> List.fold_left (fun acc a -> acc ^ a) "" (Longident.flatten l.txt)
+  | _ -> failwith "string_of_pattern_desc: unsupported"
+
+and string_of_pattern p : string = string_of_pattern_desc p.ppat_desc
+
+let preprocess_spec_comments =
+  let spec_attr_pattern = {|let \(.+\)\([
+ ]*\)(\*@\([^@]+\)@\*)|} in
+  let spec_attr_regex = Str.regexp spec_attr_pattern in
+  fun text -> Str.global_replace spec_attr_regex "let [@spec {|\\3|}] \\1\\2" text
+
+let extract_spec_attribute attrs =
+  List.find_map
+    (fun a ->
+      if String.equal a.attr_name.txt "spec" then
+        match a.attr_payload with
+        | PStr
+            [
+              {
+                pstr_desc =
+                  Pstr_eval
+                    ( { pexp_desc = Pexp_constant { pconst_desc = Pconst_string (s, _, _); _ }; _ },
+                      _ );
+                _;
+              };
+            ] -> Some s
+        | _ -> None
+      else None)
+    attrs
+
+let rec pat_to_core_lang_pat pat =
+  match pat.ppat_desc with
+  | Ppat_any -> PAny
+  | Ppat_var { txt = x; _ } -> PVar x
+  | Ppat_construct ({ txt = c; _ }, None) -> PConstr (Longident.last c, [])
+  | Ppat_construct ({ txt = c; _ }, Some ([], { ppat_desc = Ppat_tuple args; _ })) ->
+      PConstr (Longident.last c, List.map pat_to_core_lang_pat args)
+  | Ppat_construct ({ txt = c; _ }, Some ([], arg)) ->
+      PConstr (Longident.last c, [pat_to_core_lang_pat arg])
+  | Ppat_constant { pconst_desc = Pconst_integer (i, _); _ } -> PInt (int_of_string i)
+  | _ -> failwith (Format.asprintf "Unsupported pattern %a" Pprintast.pattern pat)
+
+let rec expr_to_term (expr : expression) : expr =
+  let term =
+    match expr.pexp_desc with
+    | Pexp_ident { txt = Lident i; _ } -> Var i
+    | Pexp_constant { pconst_desc = c; _ } -> begin
+        match c with
+        | Pconst_integer (i, _) -> Int (int_of_string i)
+        | _ -> failwith "unsupported constant"
+      end
+    | Pexp_let (_rec, vbs, e) ->
+        let rec chain_vbs = function
+          | [] -> expr_to_term e
+          | vb :: rest ->
+              let var_name = string_of_pattern vb.pvb_pat in
+              let expr_in = expr_to_term vb.pvb_expr in
+              let expr_in_with_spec =
+                match extract_spec_attribute vb.pvb_attributes with
+                | Some s -> WithSpec (expr_in, s, var_name)
+                | None -> expr_in
+              in
+              Let (var_name, expr_in_with_spec, chain_vbs rest)
+        in
+        chain_vbs vbs
+    | Pexp_function (params, _constraint, body) ->
+        let names =
+          List.filter_map
+            (fun p ->
+              match p.pparam_desc with
+              | Pparam_val (Nolabel, None, pat) -> Some (string_of_pattern pat)
+              | _ -> None)
+            params
+        in
+        let body_term =
+          match body with
+          | Pfunction_body e -> expr_to_term e
+          | Pfunction_cases _ -> failwith "function cases not supported"
+        in
+        Fun (names, body_term)
+    | Pexp_apply ({ pexp_desc = Pexp_ident { txt = Lident name; _ }; _ }, args)
+      when List.mem name ["shift"; "shift0"] -> begin
+        match List.map snd args with
+        | [{ pexp_desc = Pexp_ident { txt = Lident k; _ }; _ }; body] -> Shift (k, expr_to_term body)
+        | _ -> failwith "invalid shift args"
+      end
+    | Pexp_apply ({ pexp_desc = Pexp_ident { txt = Lident "reset"; _ }; _ }, args) -> begin
+        match List.map snd args with
+        | [body] -> Reset (expr_to_term body)
+        | _ -> failwith "invalid reset args"
+      end
+    | Pexp_apply ({ pexp_desc = Pexp_ident { txt = Lident "perform"; _ }; _ }, args) -> begin
+        match args with
+        | [(_, { pexp_desc = Pexp_construct ({ txt = Lident eff; _ }, arg_opt); _ })] ->
+            Perform (eff, Option.map expr_to_term arg_opt)
+        | _ -> failwith "invalid perform args"
+      end
+    | Pexp_apply ({ pexp_desc = Pexp_ident { txt = Lident name; _ }; _ }, args)
+      when name = "continue" || name = "resume" ->
+        Resume (List.map (fun (_, a) -> expr_to_term a) args)
+    | Pexp_apply (f, args) ->
+        let f_term = expr_to_term f in
+        let args_term = List.map (fun (_, a) -> expr_to_term a) args in
+        Apply (f_term, args_term)
+    | Pexp_ifthenelse (if_, then_, Some else_) ->
+        If (expr_to_term if_, expr_to_term then_, expr_to_term else_)
+    | Pexp_sequence (a, b) -> Sequence (expr_to_term a, expr_to_term b)
+    | Pexp_match (e, cases) ->
+        let e_term = expr_to_term e in
+        let cases_term =
+          List.map
+            (fun c ->
+              if Option.is_some c.pc_guard then failwith "match guard not supported";
+              (pat_to_core_lang_pat c.pc_lhs, expr_to_term c.pc_rhs))
+            cases
+        in
+        Match (e_term, cases_term)
+    | _ ->
+        failwith (Format.asprintf "expression not in core language: %a" Pprintast.expression expr)
+  in
+  match extract_spec_attribute expr.pexp_attributes with
+  | Some s -> WithSpec (term, s, "")
+  | None -> term
+
+let transform_str (s : structure_item) : (string * expr * bool) option =
+  match s.pstr_desc with
+  | Pstr_value (_rec_flag, [vb]) ->
+      let fn_name = string_of_pattern vb.pvb_pat in
+      let fn = vb.pvb_expr in
+      let body = expr_to_term fn in
+      let is_pure = List.exists (fun a -> String.equal a.attr_name.txt "pure") vb.pvb_attributes in
+      let body_with_spec =
+        match extract_spec_attribute vb.pvb_attributes with
+        | Some s -> WithSpec (body, s, fn_name)
+        | None -> body
+      in
+      Some (fn_name, body_with_spec, is_pure)
+  | Pstr_eval (e, _) -> Some ("()", expr_to_term e, false)
+  | _ -> None
+
+let process_ocaml_structure (items : structure) : verification_unit =
+  let rec loop pure_acc prog_acc items =
+    match items with
+    | [] -> { pure_functions = List.rev pure_acc; program_functions = List.rev prog_acc }
+    | item :: rest ->
+        (match transform_str item with
+        | Some (name, body, true) -> loop ((name, body) :: pure_acc) prog_acc rest
+        | Some (name, body, false) -> loop pure_acc ((name, body) :: prog_acc) rest
+        | None -> loop pure_acc prog_acc rest)
+  in
+  loop [] [] items
+
+let parse_ocaml s : verification_unit =
+  try
+    let s = preprocess_spec_comments s in
+    let items = Parse.implementation (Lexing.from_string s) in
+    process_ocaml_structure items
+  with exn ->
+    let bt = Printexc.get_raw_backtrace () in
+    Format.printf "%a\n" Location.report_exception exn;
+    Printexc.raise_with_backtrace exn bt
diff --git a/src/ocamlfrontend/frontend.mli b/src/ocamlfrontend/frontend.mli
new file mode 100644
index 00000000..ef7213c1
--- /dev/null
+++ b/src/ocamlfrontend/frontend.mli
@@ -0,0 +1,4 @@
+open Core_lang
+
+(** Parses and interprets a OCaml file (identified by name) as a verification unit *)
+val parse_ocaml : string -> verification_unit
diff --git a/src/ocamlfrontend/frontend_test.ml b/src/ocamlfrontend/frontend_test.ml
new file mode 100644
index 00000000..46eca901
--- /dev/null
+++ b/src/ocamlfrontend/frontend_test.ml
@@ -0,0 +1,76 @@
+open Core_lang
+
+let dump_program ppf prog =
+  let pp_list name ppf li =
+    Format.fprintf ppf "%s: [@[" name;
+    Format.pp_print_list
+      ~pp_sep:(fun ppf () -> Format.fprintf ppf ";@ ")
+      (fun ppf (name, body) -> Format.fprintf ppf "(%S, %a)" name Core_lang.dump_term body)
+      ppf li;
+    Format.fprintf ppf "]]@]"
+  in
+  Format.fprintf ppf "{ @[%a;@ %a @] }" (pp_list "pure_functions") prog.pure_functions
+    (pp_list "program_functions") prog.program_functions
+
+let test s =
+  let prog = Frontend.parse_ocaml s in
+  Format.printf "%a" dump_program prog
+
+let%expect_test "basic let" =
+  test "let f x y = x + y in f 1 2";
+  [%expect
+    {|
+    { pure_functions: []];
+      program_functions: [("()", Let ("f", Fun (["x"; "y"], Apply (Var "+", [Var "x"; Var "y"])), Apply (Var "f", [Int 1; Int 2])))]]  }
+    |}]
+
+let%expect_test "if and sequence" =
+  test "let x = 1 in let f y = if y = 0 then x else x + y in f 2; f 0";
+  [%expect
+    {|
+    { pure_functions: []];
+      program_functions: [("()", Let ("x", Int 1, Let ("f", Fun (["y"], If (Apply (Var "=", [Var "y"; Int 0]), Var "x", Apply (Var "+", [Var "x"; Var "y"]))), Sequence (Apply (Var "f", [Int 2]), Apply (Var "f", [Int 0])))))]]  }
+    |}]
+
+let%expect_test "effects" =
+  test "let f x = reset (shift k (f x); f 0) in perform (Eff x); continue k 1";
+  [%expect
+    {|
+    { pure_functions: []];
+      program_functions: [("()", Let ("f", Fun (["x"], Reset (Sequence (Shift ("k", Apply (Var "f", [Var "x"])), Apply (Var "f", [Int 0])))), Sequence (Perform ("Eff", Some (Var "x")), Resume ([Var "k"; Int 1]))))]]  }
+    |}]
+
+let%expect_test "pure functions and match" =
+  let code =
+    {|
+let [@pure] rec length li =
+  match li with
+  | [] -> 0
+  | x :: xs -> 1 + length xs
+
+let rec foldr f li acc =
+  match li with
+  | [] -> acc
+  | x :: xs -> f x (foldr f xs acc)
+|}
+  in
+  test code;
+  [%expect
+    {|
+    { pure_functions: [("length", Fun (["li"], Match (Var "li", [([](), Int 0); (::("x", "xs"), Apply (Var "+", [Int 1; Apply (Var "length", [Var "xs"])]))])))]];
+      program_functions: [("foldr", Fun (["f"; "li"; "acc"], Match (Var "li", [([](), Var "acc"); (::("x", "xs"), Apply (Var "f", [Var "x"; Apply (Var "foldr", [Var "f"; Var "xs"; Var "acc"])]))])))]]  }
+    |}]
+
+let%expect_test "specifications in comments" =
+  let code = {|
+let foldr_sum xs k
+(*@ sum(xs)+k @*)
+= let g c t = c + t in
+  foldr g xs k
+|} in
+  test code;
+  [%expect
+    {|
+    { pure_functions: []];
+      program_functions: [("foldr_sum", WithSpec (Fun (["xs"; "k"], Let ("g", Fun (["c"; "t"], Apply (Var "+", [Var "c"; Var "t"])), Apply (Var "foldr", [Var "g"; Var "xs"; Var "k"]))), " sum(xs)+k ", "foldr_sum"))]]  }
+    |}]
diff --git a/src/ocamlfrontend/obligations.ml b/src/ocamlfrontend/obligations.ml
new file mode 100644
index 00000000..8084aa29
--- /dev/null
+++ b/src/ocamlfrontend/obligations.ml
@@ -0,0 +1,110 @@
+open Core_lang
+open Core.Syntax
+open Core.Pretty
+
+type t = (term list * term) list
+
+let with_spec_to_subsumption f s =
+  let spec = Parsing.Parse.parse_staged_spec s in
+  let open Bindlib in
+  match Forward_rules.apply f with
+  | Fun b ->
+      let xs, body = unmbind b in
+      Some (Forall (unbox (bind_mvar xs (box_term (Subsumes (body, spec))))))
+  | _ -> None
+
+let quantified_entailment_to_named name t =
+  let open Bindlib in
+  match t with
+  | Forall b ->
+      let xs, body = unmbind b in
+      (match body with
+      | Subsumes (_impl, spec) ->
+          let xs1 = List.map Tm.var (Array.to_list xs) in
+          Some
+            (Forall
+               (unbox
+                  (bind_mvar xs
+                     (box_term (Subsumes (Apply (Symbol { sym_name = name }, xs1), spec))))))
+      | _ -> None)
+  | _ -> None
+
+let rec collect_child_obl t =
+  match t with
+  | WithSpec (f, s, _name) -> with_spec_to_subsumption f s |> Option.to_list
+  | Fun (_, body) | Shift (_, body) | Reset body -> collect_child_obl body
+  | Let (_, b1, b2) | Sequence (b1, b2) -> collect_child_obl b1 @ collect_child_obl b2
+  | Apply (b1, b2) -> collect_child_obl b1 @ List.concat_map collect_child_obl b2
+  | Var _ | Int _ -> []
+  | If (_, _, _) | Perform (_, _) | Resume _ | Match (_, _) -> failwith "unsupported for now"
+
+let collect_from_term t =
+  match t with
+  | WithSpec (f, s, name) ->
+      let open Util.Options.Monad in
+      let* top_level = with_spec_to_subsumption f s in
+      pure (name, top_level, collect_child_obl f)
+  | _ -> None
+
+let collect_from_all (ts : (string * expr) list) : t =
+  let res, _ =
+    List.fold_left
+      (fun (res, acc) (_name, t) ->
+        (* res is the final result we are build, acc is whatever came before *)
+        match collect_from_term t with
+        | None ->
+            (* if a program function has no spec, it doesn't contribute anything *)
+            (* TODO we may want to consider child specs still *)
+            (res, acc)
+        | Some (name, top, child) ->
+            let overall = quantified_entailment_to_named name top |> Option.get in
+            (* each thing depends on whatever came before, as well as any child specs, and contributes to the next one *)
+            (* TODO when are the child specs proved and what do they depend on? *)
+            ((acc @ child, top) :: res, overall :: acc))
+      ([], []) ts
+  in
+  List.rev res
+
+let generate prog = collect_from_all prog.program_functions
+
+let test code =
+  let prog = Frontend.parse_ocaml code in
+  let obs = generate prog in
+  List.iter
+    (fun (ass, ob) ->
+      Format.printf "@[<v>%a@,-------------@,%a@,@,@]" (Fmt.list ~sep:Fmt.cut pp_term) ass pp_term
+        ob)
+    obs
+
+(* TODO symbols + *)
+let%expect_test "generate proof obligations" =
+  let code =
+    {|
+let [@pure] rec length li =
+  match li with
+  | [] -> 0
+  | x :: xs -> 1 + length xs
+
+let foldr_sum xs k
+(*@ sum xs + k @*)
+= let g c t = c + t in
+  foldr g xs k
+
+let foldr_length xs init
+(*@ length xs + init @*)
+= let g c t = 1 + t in
+  foldr g xs init
+|}
+  in
+  test code;
+  [%expect
+    {|
+    -------------
+    forall xs k. (fun c t -> c+t); g. foldr g xs k <: sum xs+k
+
+    forall xs k. foldr_sum xs k <: sum xs+k
+    -------------
+    forall xs init. (fun c t -> 1+t); g. foldr g xs init <: length xs+init
+    |}]
+
+(* TODO tests for child specs *)
diff --git a/src/ocamlfrontend/obligations.mli b/src/ocamlfrontend/obligations.mli
new file mode 100644
index 00000000..b45b1c45
--- /dev/null
+++ b/src/ocamlfrontend/obligations.mli
@@ -0,0 +1,23 @@
+open Core.Syntax
+open Core_lang
+
+type t = (term list * term) list
+
+(** Generates proof obligations in a "triangular" manner, e.g.
+
+    {[
+      let fn1 : f1 = e1
+      let fn2 : f2 = e2
+    ]}
+
+    produces two obligations
+
+    {v
+      forward e1 <: f1
+
+
+      forward e1 <: f1
+      --------------------
+      forward e2 <: f2
+    v} *)
+val generate : verification_unit -> t
diff --git a/src/ocamlfrontend/ocamlfrontend.ml b/src/ocamlfrontend/ocamlfrontend.ml
new file mode 100644
index 00000000..94c41adb
--- /dev/null
+++ b/src/ocamlfrontend/ocamlfrontend.ml
@@ -0,0 +1,14 @@
+open Core_lang
+
+let convert_functions_to_staged fns =
+  List.map
+    (fun (s, d) ->
+      match Forward_rules.apply d with
+      | Fun b -> (s, b)
+      | _ -> failwith "not a function?")
+    fns
+
+let get_definitions_and_obligations src =
+  let vu = Frontend.parse_ocaml src in
+  (* TODO convert pure functions to why3? *)
+  (convert_functions_to_staged vu.program_functions, Obligations.generate vu)
diff --git a/src/ocamlfrontend/ocamlfrontend.mli b/src/ocamlfrontend/ocamlfrontend.mli
new file mode 100644
index 00000000..44f28684
--- /dev/null
+++ b/src/ocamlfrontend/ocamlfrontend.mli
@@ -0,0 +1,4 @@
+open Core.Syntax
+
+(** Generates staged logic defintions and proof obligations from OCaml source *)
+val get_definitions_and_obligations : string -> (string * def) list * Obligations.t
diff --git a/src/prover/dune b/src/prover/dune
index 6edbc72a..b61b5978 100644
--- a/src/prover/dune
+++ b/src/prover/dune
@@ -2,5 +2,5 @@
  (name prover)
  (public_name heifer.prover)
  (inline_tests)
- (libraries core parsing util why3_prover printbox-text)
+ (libraries core parsing util why3_prover printbox-text ocamlfrontend)
  (preprocess (pps ppx_expect)))
diff --git a/src/prover/interactive.ml b/src/prover/interactive.ml
index 871f8eeb..0cec0fac 100644
--- a/src/prover/interactive.ml
+++ b/src/prover/interactive.ml
@@ -48,11 +48,14 @@ module State = struct
   let get_lemma_opt name = SMap.find_opt name (get_lemmas ())
   let get_definition_opt sym = SymMap.find_opt sym (get_definitions ())
 
-  let declare decl =
-    let sym, def = open_dfun (Parsing.Parse.parse_decl decl) in
+  let declare_defn sym def =
     set_definitions (add_decl sym def !current_state.definitions);
     Format.printf "%s declared@." sym.sym_name
 
+  let declare decl =
+    let sym, def = open_dfun (Parsing.Parse.parse_decl decl) in
+    declare_defn sym def
+
   let axiom ~name term =
     let goal = Parsing.Parse.parse_term term in
     add_lemma name goal;
@@ -61,13 +64,32 @@ module State = struct
   let lemma ~name term =
     let goal = Parsing.Parse.parse_term term in
     set_mode (Mode_lemma (name, goal));
-    set_goal (Pctx.create ~goal);
+    set_goal (Pctx.create goal);
     print_proof_state ()
 
   let start_proof term =
     let goal = Parsing.Parse.parse_term term in
     set_mode Mode_goal;
-    set_goal (Pctx.create ~goal);
+    set_goal (Pctx.create goal);
+    print_proof_state ()
+
+  let read_file filename =
+    let ic = open_in filename in
+    let s = In_channel.input_all ic in
+    close_in ic;
+    let sdefns, obs = Ocamlfrontend.get_definitions_and_obligations s in
+    List.iter (fun (s, d) -> declare_defn { sym_name = s } d) sdefns;
+    let new_goals =
+      List.map
+        (fun (ass, ob) ->
+          let assumptions =
+            List.mapi (fun i a -> (Format.asprintf "H%d" i, a)) ass |> SMap.of_list
+          in
+          Pctx.create ~assumptions ob)
+        obs
+    in
+    set_goals (new_goals @ get_goals ());
+    set_mode Mode_goal;
     print_proof_state ()
 
   let run_tactic tactic =
@@ -92,17 +114,16 @@ module State = struct
   let make_interactive (tac : 'b -> 'a Tactic.t) (arg : 'b) = run_tactic (tac arg)
 
   let when_goal_is_empty f =
-    if Pstate.is_empty (get_goals ()) then f ()
-    else Format.printf "error: proof is still open@."
+    if Pstate.is_empty (get_goals ()) then f () else Format.printf "error: proof is still open@."
 
   let qed () =
     match get_mode () with
     | Mode_goal -> when_goal_is_empty (fun () -> set_mode Mode_none)
     | Mode_lemma (name, goal) ->
         when_goal_is_empty (fun () ->
-          add_lemma name goal;
-          set_mode Mode_none;
-          Format.printf "lemma %s declared@." name)
+            add_lemma name goal;
+            set_mode Mode_none;
+            Format.printf "lemma %s declared@." name)
     | Mode_none -> Format.printf "error: no open proof@."
 end
 
diff --git a/src/prover/interactive.mli b/src/prover/interactive.mli
index 0d5df6ad..7b85ab95 100644
--- a/src/prover/interactive.mli
+++ b/src/prover/interactive.mli
@@ -2,6 +2,7 @@ open Core.Syntax
 
 module State : sig
   val start_proof : string -> unit
+  val read_file : string -> unit
   val print_proof_state : unit -> unit
   val reset_proof_state : unit -> unit
   val push_proof_state : unit -> unit
diff --git a/src/prover/interactive_test.ml b/src/prover/interactive_test.ml
index 85bb1370..9a4c9076 100644
--- a/src/prover/interactive_test.ml
+++ b/src/prover/interactive_test.ml
@@ -597,46 +597,44 @@ let%expect_test "rewrite" =
     error: H does not exist
     |}]
 
-let%expect_test "heap tactics" =
-  start_proof "ens emp <: forall x. req x->1; ens x->1";
+let%expect_test "read_file" =
+  let filename = "test_obs.ml" in
+  let oc = open_out filename in
+  output_string oc {|
+let f x
+(*@ 1 @*)
+= 1
+
+let g x
+(*@ 1 @*)
+= f x
+|};
+  close_out oc;
+  reset_proof_state ();
+  read_file filename;
   forall_intro ();
-  ens_heap_elim ();
-  req_heap_intro ();
-  ens_heap_intro ();
   refl ();
+  Sys.remove filename;
   [%expect
     {|
-    ────────────────────────────────────────────────────────────
-       ens emp
-    <: forall x. req x->1; ens x->1
-
+    f declared
+    g declared
 
-    x
-    ────────────────────────────────────────────────────────────
-       ens emp
-    <: req x->1; ens x->1
-
-
-    x
     ────────────────────────────────────────────────────────────
-       ()
-    <: req x->1; ens x->1
+    forall x. 1 <: 1
+    (1 more goals)
 
 
     x
     ────────────────────────────────────────────────────────────
-    x->1
-    ───────────────────────────────────────────────────────────*
-       ()
-    <: ens x->1
+       1
+    <: 1
+    (1 more goals)
 
 
-    x
+    H0: forall x. f x <: 1
     ────────────────────────────────────────────────────────────
-       ()
-    <: ()
-
-    no more goals
+    forall x. f x <: 1
     |}]
 
 (* start_proof "ens emp <: forall x v. req v=1; req x->v; ens x->1";
diff --git a/src/prover/pctx.ml b/src/prover/pctx.ml
index fb0d48b1..b224f558 100644
--- a/src/prover/pctx.ml
+++ b/src/prover/pctx.ml
@@ -14,11 +14,11 @@ type t = {
   goal : term;
 }
 
-let create ~goal =
+let create ?(assumptions = SMap.empty) goal =
   {
     rename_ctxt = Rename.empty_ctxt;
     constants = SMap.empty;
-    assumptions = SMap.empty;
+    assumptions;
     heap_assumptions = [];
     goal;
   }
diff --git a/src/prover/pctx.mli b/src/prover/pctx.mli
index 86c0c616..1d8b23b6 100644
--- a/src/prover/pctx.mli
+++ b/src/prover/pctx.mli
@@ -1,3 +1,4 @@
+open Util.Strings
 open Core.Syntax
 open Core
 
@@ -9,5 +10,5 @@ type t = {
   goal : term;
 }
 
-val create : goal:term -> t
+val create : ?assumptions:term SMap.t -> term -> t
 val pp : Format.formatter -> t -> unit

From 608f7504bc1ab5d58eb9a9733cac370611a0d209 Mon Sep 17 00:00:00 2001
From: Darius Foo <darius.foo.tw@gmail.com>
Date: Mon, 9 Mar 2026 14:47:53 +0800
Subject: [PATCH 2/2] Remove dependency on ocamlfrontend from prover

---
 src/heifer/dune                  |  2 ++
 src/heifer/extra_tactics.ml      | 20 +++++++++++++++
 src/heifer/extra_tactics_test.ml | 43 ++++++++++++++++++++++++++++++++
 src/heifer/heifer.ml             |  2 ++
 src/prover/dune                  |  2 +-
 src/prover/interactive.ml        | 22 +---------------
 src/prover/interactive.mli       |  9 ++++++-
 src/prover/interactive_test.ml   | 40 -----------------------------
 8 files changed, 77 insertions(+), 63 deletions(-)
 create mode 100644 src/heifer/extra_tactics.ml
 create mode 100644 src/heifer/extra_tactics_test.ml

diff --git a/src/heifer/dune b/src/heifer/dune
index f4e898fc..7c7622f7 100644
--- a/src/heifer/dune
+++ b/src/heifer/dune
@@ -3,5 +3,7 @@
  (public_name heifer)
  ; heifer is often used interactively, so linkall is given here.
  ; this also avoids having to list all transitive dependencies in mdx
+ (inline_tests)
+ (preprocess (pps ppx_expect))
  (library_flags (-linkall))
  (libraries core ocamlfrontend parsing prover))
diff --git a/src/heifer/extra_tactics.ml b/src/heifer/extra_tactics.ml
new file mode 100644
index 00000000..e47ff6ca
--- /dev/null
+++ b/src/heifer/extra_tactics.ml
@@ -0,0 +1,20 @@
+open Util.Strings
+open Prover.Interactive.State
+open Prover
+
+let read_file filename =
+  let ic = open_in filename in
+  let s = In_channel.input_all ic in
+  close_in ic;
+  let sdefns, obs = Ocamlfrontend.get_definitions_and_obligations s in
+  List.iter (fun (s, d) -> declare_defn { sym_name = s } d) sdefns;
+  let new_goals =
+    List.map
+      (fun (ass, ob) ->
+        let assumptions = List.mapi (fun i a -> (Format.asprintf "H%d" i, a)) ass |> SMap.of_list in
+        Pctx.create ~assumptions ob)
+      obs
+  in
+  add_goals new_goals;
+  set_mode Mode_goal;
+  print_proof_state ()
diff --git a/src/heifer/extra_tactics_test.ml b/src/heifer/extra_tactics_test.ml
new file mode 100644
index 00000000..46d15a3a
--- /dev/null
+++ b/src/heifer/extra_tactics_test.ml
@@ -0,0 +1,43 @@
+open Prover.Interactive.State
+open Prover.Interactive
+open Extra_tactics
+
+let%expect_test "read_file" =
+  let filename = "test_obs.ml" in
+  let oc = open_out filename in
+  output_string oc {|
+let f x
+(*@ 1 @*)
+= 1
+
+let g x
+(*@ 1 @*)
+= f x
+|};
+  close_out oc;
+  reset_proof_state ();
+  read_file filename;
+  forall_intro ();
+  refl ();
+  Sys.remove filename;
+  [%expect
+    {|
+    f declared
+    g declared
+
+    ────────────────────────────────────────────────────────────
+    forall x. 1 <: 1
+    (1 more goals)
+
+
+    x
+    ────────────────────────────────────────────────────────────
+       1
+    <: 1
+    (1 more goals)
+
+
+    H0: forall x. f x <: 1
+    ────────────────────────────────────────────────────────────
+    forall x. f x <: 1
+    |}]
diff --git a/src/heifer/heifer.ml b/src/heifer/heifer.ml
index 551290be..2ddc8d6f 100644
--- a/src/heifer/heifer.ml
+++ b/src/heifer/heifer.ml
@@ -10,11 +10,13 @@ module Interactive = struct
 
   include Prover.Interactive.State
   include Prover.Interactive
+  include Extra_tactics
 
   let () = Format.set_margin !Prover.Prover_options.line_length
 
   module Statistics = struct
     let start_time = ref (Unix.gettimeofday ())
+
     let reset () =
       start_time := Unix.gettimeofday ();
       Why3_prover.reset_statistics ()
diff --git a/src/prover/dune b/src/prover/dune
index b61b5978..6edbc72a 100644
--- a/src/prover/dune
+++ b/src/prover/dune
@@ -2,5 +2,5 @@
  (name prover)
  (public_name heifer.prover)
  (inline_tests)
- (libraries core parsing util why3_prover printbox-text ocamlfrontend)
+ (libraries core parsing util why3_prover printbox-text)
  (preprocess (pps ppx_expect)))
diff --git a/src/prover/interactive.ml b/src/prover/interactive.ml
index 0cec0fac..d15d758b 100644
--- a/src/prover/interactive.ml
+++ b/src/prover/interactive.ml
@@ -4,8 +4,6 @@ open Core.Syntax_util
 open Util.Strings
 open Tactics
 
-(* TODO: refactor into some top-level module, with a different name. The current
-   name clashes with Pstate -> proof_state *)
 module State = struct
   type mode =
     | Mode_lemma of string * term
@@ -44,6 +42,7 @@ module State = struct
   let set_mode mode = current_state := { !current_state with mode }
   let set_goals goals = current_state := { !current_state with goals }
   let set_goal goal = set_goals [goal]
+  let add_goals goals = set_goals (goals @ get_goals ())
   let add_lemma name term = set_lemmas (SMap.add name term (get_lemmas ()))
   let get_lemma_opt name = SMap.find_opt name (get_lemmas ())
   let get_definition_opt sym = SymMap.find_opt sym (get_definitions ())
@@ -73,25 +72,6 @@ module State = struct
     set_goal (Pctx.create goal);
     print_proof_state ()
 
-  let read_file filename =
-    let ic = open_in filename in
-    let s = In_channel.input_all ic in
-    close_in ic;
-    let sdefns, obs = Ocamlfrontend.get_definitions_and_obligations s in
-    List.iter (fun (s, d) -> declare_defn { sym_name = s } d) sdefns;
-    let new_goals =
-      List.map
-        (fun (ass, ob) ->
-          let assumptions =
-            List.mapi (fun i a -> (Format.asprintf "H%d" i, a)) ass |> SMap.of_list
-          in
-          Pctx.create ~assumptions ob)
-        obs
-    in
-    set_goals (new_goals @ get_goals ());
-    set_mode Mode_goal;
-    print_proof_state ()
-
   let run_tactic tactic =
     match Tactic.run_pstate tactic (get_goals ()) with
     | Ok new_goals ->
diff --git a/src/prover/interactive.mli b/src/prover/interactive.mli
index 7b85ab95..e92ddbbd 100644
--- a/src/prover/interactive.mli
+++ b/src/prover/interactive.mli
@@ -1,12 +1,19 @@
 open Core.Syntax
 
 module State : sig
+  type mode =
+    | Mode_lemma of string * term
+    | Mode_goal
+    | Mode_none
+
+  val set_mode : mode -> unit
   val start_proof : string -> unit
-  val read_file : string -> unit
   val print_proof_state : unit -> unit
   val reset_proof_state : unit -> unit
   val push_proof_state : unit -> unit
+  val add_goals : Pctx.t list -> unit
   val pop_proof_state : unit -> unit
+  val declare_defn : symbol -> def -> unit
   val declare : string -> unit
   val axiom : name:string -> string -> unit
   val lemma : name:string -> string -> unit
diff --git a/src/prover/interactive_test.ml b/src/prover/interactive_test.ml
index 9a4c9076..b5fbd3a1 100644
--- a/src/prover/interactive_test.ml
+++ b/src/prover/interactive_test.ml
@@ -597,46 +597,6 @@ let%expect_test "rewrite" =
     error: H does not exist
     |}]
 
-let%expect_test "read_file" =
-  let filename = "test_obs.ml" in
-  let oc = open_out filename in
-  output_string oc {|
-let f x
-(*@ 1 @*)
-= 1
-
-let g x
-(*@ 1 @*)
-= f x
-|};
-  close_out oc;
-  reset_proof_state ();
-  read_file filename;
-  forall_intro ();
-  refl ();
-  Sys.remove filename;
-  [%expect
-    {|
-    f declared
-    g declared
-
-    ────────────────────────────────────────────────────────────
-    forall x. 1 <: 1
-    (1 more goals)
-
-
-    x
-    ────────────────────────────────────────────────────────────
-       1
-    <: 1
-    (1 more goals)
-
-
-    H0: forall x. f x <: 1
-    ────────────────────────────────────────────────────────────
-    forall x. f x <: 1
-    |}]
-
 (* start_proof "ens emp <: forall x v. req v=1; req x->v; ens x->1";
    forall_intro ();
    intro_pure "Hv";