add minidag proof emitter; wire as default tracer replacing bencode

src/main/dune

@@ -8,7 +8,7 @@
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
    sidekick.smt-solver sidekick-base.smtlib sidekick.drup sidekick.memtrace
-   sidekick-bin.lib sidekick.proof_twp)
+   sidekick-bin.lib sidekick.proof_twp sidekick.proof-minidag)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (executable

src/main/main.ml

@@ -143,24 +143,17 @@ let run_with_tmp_file ~enable_proof k =
   else
     k ""
 
-let mk_smt_tracer ~trace_file () =
+(** Create a minidag proof tracer writing to [path]. *)
-  if !enable_trace || trace_file <> "" then (
+let mk_smt_tracer ~path ~tst () =
-    Log.debugf 1 (fun k -> k "(@[emit-trace-into@ %S@])" trace_file);
+  if path <> "" then (
-    let oc = open_out_bin trace_file in
+    Log.debugf 1 (fun k -> k "(@[emit-proof-minidag-into@ %S@])" path);
-    Sidekick_smt_solver.Tracer.make
+    Sidekick_proof_minidag.open_file ~path ~tst ()
-      ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc)
-      ()
   ) else
     Sidekick_smt_solver.Tracer.dummy
 
 let mk_sat_tracer () : Sidekick_sat.Tracer.t =
-  if !trace_file = "" then
+  (* SAT-only mode: no proof support yet for minidag *)
   Sidekick_sat.Tracer.dummy
-  else (
-    let oc = open_out_bin !trace_file in
-    let sink = Sidekick_trace.Sink.of_out_channel_using_bencode oc in
-    Pure_sat_solver.tracer ~sink ()
-  )
 
 let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
@@ -168,32 +161,25 @@ let main_smt ~config () : _ result =
   let enable_proof = !check || !p_proof || !proof_file <> "" || !proof_twp_file <> "" in
   Log.debugf 1 (fun k -> k "(@[proof-enable@ %B@])" enable_proof);
 
-  run_with_tmp_file ~enable_proof @@ fun trace_file ->
+  (* Determine the proof output path.
-  Log.debugf 1 (fun k -> k "(@[trace_file@ %S@])" trace_file);
+     Priority: --trace-file > --proof-twp (legacy) > auto-generate if needed.
+     We always use minidag format (.granite). *)
+  let proof_path =
+    if !trace_file <> "" then
+      !trace_file
+    else if !proof_twp_file <> "" then
+      (* Accept --proof-twp path but write minidag there instead *)
+      !proof_twp_file
+    else if enable_proof then (
+      (* Auto-generate a temp path so proofs are available for --check *)
+      let base = Filename.remove_extension !file in
+      base ^ ".granite"
+    ) else
+      ""
+  in
+  Log.debugf 1 (fun k -> k "(@[proof-path@ %S@])" proof_path);
 
-  (* FIXME
+  let tracer = mk_smt_tracer ~path:proof_path ~tst () in
-     let config =
-       if enable_proof_ then
-         Proof.Config.default |> Proof.Config.enable true
-         |> Proof.Config.store_on_disk_at temp_proof_file
-       else
-         Proof.Config.empty
-     in
-
-     (* main proof object *)
-     let proof = Proof.create ~config () in
-  *)
-  let twp_state_opt =
-    if !proof_twp_file <> "" then
-      Some (Sidekick_proof_twp.Twp_state.create ())
-    else
-      None
-  in
-  let tracer =
-    match twp_state_opt with
-    | Some st -> Sidekick_proof_twp.Twp_tracer.create st
-    | None -> mk_smt_tracer ~trace_file ()
-  in
   Proof.Tracer.enable tracer enable_proof;
 
   let solver =
@@ -244,16 +230,6 @@ let main_smt ~config () : _ result =
     try E.fold_l (fun () stmt -> Driver.process_stmt driver stmt) () input
     with Exit -> E.return ()
   in
-  (* If --proof-twp is set, write the accumulated .twp buffer to the file *)
-  (match twp_state_opt with
-  | None -> ()
-  | Some st ->
-    let buf = Sidekick_proof_twp.Twp_state.buffer st in
-    (try
-       CCIO.with_out !proof_twp_file (fun oc ->
-           Buffer.output_buffer oc buf)
-     with Sys_error msg ->
-       Log.debugf 0 (fun k -> k "proof-twp: cannot write file: %s" msg)));
   res
 
 let main_cnf () : _ result =

src/minidag/encode.ml

@@ -132,6 +132,8 @@ let ref self i =
   assert (i < abs_offset_ self);
   uint_ self ~high:7 i
 
+let offset_of_int (i : int) : offset = Obj.magic i
+
 let write_node (self : t) cmd (f : node_encoder -> unit) : offset =
   let offset = abs_offset_ self in
   string self cmd;

src/minidag/encode.mli

@@ -15,6 +15,10 @@ type node_encoder
 
 type offset = private int
 
+val offset_of_int : int -> offset
+(** Reinterpret an integer as an offset. Only safe when the integer was
+    originally returned by {!write_node}. *)
+
 val write_node : t -> string -> (node_encoder -> unit) -> offset
 (** [write_node enc command f] starts a new node with "command", calls [f] to
     add the arguments, and returns the offset of this new node. The node encoder

src/proof_minidag/dune

@@ -0,0 +1,7 @@
+(library
+ (name sidekick_proof_minidag)
+ (public_name sidekick.proof-minidag)
+ (synopsis "Minidag proof emitter for sidekick (granite-compatible)")
+ (libraries sidekick.core sidekick.proof sidekick.sat sidekick.smt-solver
+   sidekick.minidag containers)
+ (flags :standard -open Sidekick_util -open Sidekick_core))

src/proof_minidag/minidag_tracer.ml

@@ -0,0 +1,51 @@
+(** SMT tracer that writes proof steps as a minidag byte stream.
+
+    Implements [Sidekick_smt_solver.Tracer.t].  The output file uses the
+    [.granite] extension and contains a sequence of minidag nodes: first term
+    nodes, then proof nodes.  The last proof node is the root (empty clause).
+*)
+
+module Proof = Sidekick_proof
+module Smt_tracer = Sidekick_smt_solver.Tracer
+module E = Sidekick_minidag.Encode
+
+class oc_output (oc : out_channel) : E.output =
+  object
+    method write buf pos len = output_bytes oc (Bytes.sub buf pos len)
+  end
+
+let create ~(oc : out_channel) ~(tst : Term.store) () : Smt_tracer.t =
+  let enc = E.create ~out:(new oc_output oc) () in
+  let te = Term_encoder.create enc in
+  let pe = Proof_encoder.create te tst in
+  at_exit (fun () ->
+      (try E.flush enc with _ -> ());
+      (try close_out oc with _ -> ()));
+  object
+    val mutable enabled = true
+
+    method proof_enabled = enabled
+    method proof_enable b = enabled <- b
+
+    method emit_proof_step (p : Proof.Pterm.delayed) : Proof.Step.id =
+      if not enabled then Proof.Step.dummy
+      else begin
+        (* The step id IS the minidag byte offset of the emitted node. *)
+        let off = Proof_encoder.emit_step pe Proof.Step.dummy p in
+        Sidekick_trace.Entry_id.of_int_unsafe (off :> int)
+      end
+
+    method emit_proof_delete _id = ()
+    method emit_term (_t : Term.t) = Sidekick_trace.Entry_id.dummy
+
+    method sat_assert_clause ~id:_ _ _ = Sidekick_trace.Entry_id.dummy
+    method sat_delete_clause ~id:_ _ = ()
+    method sat_unsat_clause ~id:_ = Sidekick_trace.Entry_id.dummy
+    method sat_encode_lit _ = Ser_value.null
+
+    method emit_assert_term _ = Sidekick_trace.Entry_id.dummy
+  end
+
+(** Open [path] and return a tracer writing a minidag proof to it. *)
+let open_file ~path ~tst () : Smt_tracer.t =
+  create ~oc:(open_out_bin path) ~tst ()

src/proof_minidag/proof_encoder.ml

@@ -0,0 +1,190 @@
+(** Encode sidekick [Pterm.t] proof steps into minidag nodes.
+
+    Targeting the granite [ext-proof-fmt.json] command vocabulary:
+      p.hyp  p.res  p.eq  rs.a  rs.r  eq.u  eq.c  seq  clause
+
+    Sidekick-specific oracle steps use [sk.*] commands:
+      sk.cc_conflict  sk.sat_rup  sk.bool_ax  sk.r1  sk.p1
+      sk.lra  sk.preprocess  sk.rw-clause  sk.sorry
+
+    Step IDs ([Proof.Step.id] = [Entry_id.t] = int) are the minidag byte
+    offset of the corresponding proof node — no separate table needed.
+*)
+
+open Sidekick_proof
+module E = Sidekick_minidag.Encode
+open Term_encoder
+
+type t = {
+  te: Term_encoder.t;
+  tst: Term.store;
+}
+
+let create te tst : t = { te; tst }
+
+let enc self = self.te.enc
+let nd self cmd f = E.write_node (enc self) cmd f
+
+(* ---- Helpers ---------------------------------------------------- *)
+
+let encode_term' self = encode_term self.te
+let encode_lit' self = encode_lit self.te self.tst
+
+(** [seq self ~hyps ~concls] emits [seq hyp... null concl...] *)
+let emit_seq self ~hyps ~concls =
+  nd self "seq" (fun e ->
+      List.iter (E.ref e) hyps;
+      E.null e;
+      List.iter (E.ref e) concls)
+
+(** Emit [p.hyp] with the given conclusion offsets and no hypotheses. *)
+let emit_hyp self concls =
+  let seq = emit_seq self ~hyps:[] ~concls in
+  nd self "p.hyp" (fun e -> E.ref e seq)
+
+(** Emit [sk.sorry] with a descriptive message. *)
+let emit_sorry self msg =
+  nd self "sk.sorry" (fun e -> E.string e msg)
+
+(** Convert a step id (= byte offset stored as int) back to an [E.offset]. *)
+let step_off (_self : t) (sid : Step.id) : E.offset =
+  E.offset_of_int (Sidekick_trace.Entry_id.to_int sid)
+
+(* ---- Rule handlers ---------------------------------------------- *)
+
+let emit_hyp_lits self lits =
+  emit_hyp self (List.map (encode_lit' self) lits)
+
+(** Binary resolution: emit as [sk.r1] oracle (trusted by the checker). *)
+let emit_resolution self ~pivot ~p1 ~p2 =
+  nd self "sk.r1" (fun e -> E.ref e p1; E.ref e p2; E.ref e pivot)
+
+(** RUP (redundant by unit propagation): oracle step referencing all hyp proofs. *)
+let emit_sat_rup self hyp_sids =
+  let dag_offs = List.map (step_off self) hyp_sids in
+  nd self "sk.sat_rup" (fun e -> List.iter (E.ref e) dag_offs)
+
+(** CC conflict: oracle step referencing all conflicting lits. *)
+let emit_cc_conflict self lits =
+  let lit_offs = List.map (encode_lit' self) lits in
+  nd self "sk.cc_conflict" (fun e -> List.iter (E.ref e) lit_offs)
+
+(** Boolean axiom: any [bool.*] rule name. *)
+let emit_bool_ax self name term_args =
+  let term_offs = List.map (encode_term' self) term_args in
+  nd self "sk.bool_ax" (fun e ->
+      E.string e name;
+      List.iter (E.ref e) term_offs)
+
+(* ---- Main dispatch ---------------------------------------------- *)
+
+let rec encode_rule self (r : Pterm.rule_apply) : E.offset =
+  let { Pterm.rule_name; lit_args; term_args; premises; _ } = r in
+  match rule_name with
+
+  | "sat.input" ->
+    emit_hyp_lits self lit_args
+
+  | "sat.rc" ->
+    (* RUP redundant clause *)
+    (match premises with
+     | [] -> emit_hyp_lits self lit_args
+     | _  -> emit_sat_rup self premises)
+
+  | "core.res" ->
+    (match premises, term_args with
+     | [p1; p2], [pivot] ->
+       emit_resolution self
+         ~pivot:(encode_term' self pivot)
+         ~p1:(step_off self p1) ~p2:(step_off self p2)
+     | [p1; p2], [] ->
+       let o1 = step_off self p1 and o2 = step_off self p2 in
+       nd self "sk.sorry" (fun e ->
+           E.string e "core.res: no pivot"; E.ref e o1; E.ref e o2)
+     | _ -> emit_sorry self "core.res: bad args")
+
+  | "core.r1" ->
+    (match premises with
+     | [p1; p2] ->
+       let o1 = step_off self p1 and o2 = step_off self p2 in
+       nd self "sk.r1" (fun e -> E.ref e o1; E.ref e o2)
+     | _ -> emit_sorry self "core.r1: bad args")
+
+  | "core.p1" ->
+    (match premises with
+     | [p1; p2] ->
+       let o1 = step_off self p1 and o2 = step_off self p2 in
+       nd self "sk.p1" (fun e -> E.ref e o1; E.ref e o2)
+     | _ -> emit_sorry self "core.p1: bad args")
+
+  | "core.lemma-cc" ->
+    emit_cc_conflict self lit_args
+
+  | "core.define-term" ->
+    (match term_args with
+     | [c; rhs] -> emit_hyp self [encode_term' self (Term.eq self.tst c rhs)]
+     | _ -> emit_sorry self "core.define-term: bad args")
+
+  | "core.preprocess" ->
+    let prem_offs = List.map (step_off self) premises in
+    nd self "sk.preprocess" (fun e -> List.iter (E.ref e) prem_offs)
+
+  | "core.with-defs" ->
+    (match premises with
+     | p :: _ -> step_off self p
+     | []     -> emit_sorry self "core.with-defs: no premises")
+
+  | "core.rw-clause" ->
+    let prem_offs = List.map (step_off self) premises in
+    let lit_offs = List.map (encode_lit' self) lit_args in
+    nd self "sk.rw-clause" (fun e ->
+        List.iter (E.ref e) prem_offs;
+        E.null e;
+        List.iter (E.ref e) lit_offs)
+
+  | "core.true" ->
+    emit_hyp self [encode_term' self (Term.true_ self.tst)]
+
+  | "lra.lemma" ->
+    let lit_offs = List.map (encode_lit' self) lit_args in
+    nd self "sk.lra" (fun e -> List.iter (E.ref e) lit_offs)
+
+  | name when String.length name >= 5
+           && String.sub name 0 5 = "bool." ->
+    emit_bool_ax self name term_args
+
+  | name ->
+    let prem_offs = List.map (step_off self) premises in
+    let term_offs = List.map (encode_term' self) term_args in
+    nd self "sk.sorry" (fun e ->
+        E.string e name;
+        List.iter (E.ref e) prem_offs;
+        List.iter (E.ref e) term_offs)
+
+and encode_pterm ?(local_tbl : (int, E.offset) Hashtbl.t option)
+    self (pt : Pterm.t) : E.offset =
+  match pt with
+  | Pterm.P_ref sid -> step_off self sid
+  | Pterm.P_local id ->
+    (match local_tbl with
+     | Some t ->
+       (match Hashtbl.find_opt t id with
+        | Some off -> off
+        | None -> emit_sorry self (Printf.sprintf "P_local s%d (unresolved)" id))
+     | None -> emit_sorry self (Printf.sprintf "P_local s%d (no context)" id))
+  | Pterm.P_apply r -> encode_rule self r
+  | Pterm.P_let (bindings, body) ->
+    (* Evaluate each binding and store in a fresh local table. *)
+    let tbl =
+      match local_tbl with
+      | Some t -> t
+      | None -> Hashtbl.create 4
+    in
+    List.iter (fun (id, pt') ->
+        Hashtbl.replace tbl id (encode_pterm ~local_tbl:tbl self pt'))
+      bindings;
+    encode_pterm ~local_tbl:tbl self body
+
+(** Emit a proof step and return its minidag offset (= the new step id). *)
+let emit_step self (_sid : Step.id) (pt : Pterm.delayed) : E.offset =
+  encode_pterm self (pt ())

src/proof_minidag/sidekick_proof_minidag.ml

@@ -0,0 +1,12 @@
+(** Minidag proof emission for sidekick.
+
+    Provides a [Sidekick_smt_solver.Tracer.t] that writes a granite-compatible
+    minidag proof stream to a file (extension [.granite]).
+*)
+
+module Term_encoder = Term_encoder
+module Proof_encoder = Proof_encoder
+module Minidag_tracer = Minidag_tracer
+
+let create_tracer = Minidag_tracer.create
+let open_file = Minidag_tracer.open_file

src/proof_minidag/term_encoder.ml

@@ -0,0 +1,84 @@
+(** Encode sidekick [Term.t] values into minidag nodes.
+
+    Uses the term command vocabulary from [ext-term.json]:
+      t.type  t.v  t.bv  t.c  t.@  t.\  t.->
+      cst
+
+    Constants are encoded with the [cst] command (name + type).
+    Terms are memoized: [Term.Tbl] for terms, [Const_tbl] for constants.
+*)
+
+open Sidekick_core
+module E = Sidekick_minidag.Encode
+module Const_tbl = CCHashtbl.Make (Const)
+
+type t = {
+  enc: E.t;
+  term_cache: E.offset Term.Tbl.t;
+  const_cache: E.offset Const_tbl.t;
+}
+
+let create enc : t =
+  { enc; term_cache = Term.Tbl.create 256; const_cache = Const_tbl.create 64 }
+
+let rec encode_const (self : t) (c : Const.t) : E.offset =
+  match Const_tbl.find_opt self.const_cache c with
+  | Some off -> off
+  | None ->
+    let ty_off = encode_term self c.Const.c_ty in
+    let name = Format.asprintf "%a" Const.pp c in
+    let off =
+      E.write_node self.enc "cst" (fun nd ->
+          E.string nd name;
+          E.ref nd ty_off)
+    in
+    Const_tbl.replace self.const_cache c off;
+    off
+
+and encode_term (self : t) (t : Term.t) : E.offset =
+  match Term.Tbl.find_opt self.term_cache t with
+  | Some off -> off
+  | None ->
+    let off = encode_term_uncached self t in
+    Term.Tbl.replace self.term_cache t off;
+    off
+
+and encode_term_uncached (self : t) (t : Term.t) : E.offset =
+  let nd cmd f = E.write_node self.enc cmd f in
+  match Term.view t with
+  | Term.E_type _ -> nd "t.type" (fun _ -> ())
+
+  | Term.E_const c ->
+    let c_off = encode_const self c in
+    nd "t.c" (fun e -> E.ref e c_off)
+
+  | Term.E_app (f, a) ->
+    let f_off = encode_term self f and a_off = encode_term self a in
+    nd "t.@" (fun e -> E.ref e f_off; E.ref e a_off)
+
+  | Term.E_lam (name, ty, body) ->
+    let ty_off = encode_term self ty and body_off = encode_term self body in
+    nd "t.\\" (fun e -> E.string e name; E.ref e ty_off; E.ref e body_off)
+
+  | Term.E_pi (_name, dom, body) ->
+    let dom_off = encode_term self dom and body_off = encode_term self body in
+    nd "t.->" (fun e -> E.ref e dom_off; E.ref e body_off)
+
+  | Term.E_var v ->
+    let ty_off = encode_term self (Var.ty v) in
+    nd "t.v" (fun e -> E.string e (Var.name v); E.ref e ty_off)
+
+  | Term.E_bound_var bv ->
+    let ty_off = encode_term self bv.bv_ty in
+    nd "t.bv" (fun e -> E.int e bv.bv_idx; E.ref e ty_off)
+
+  | Term.E_app_fold { f; args; acc0 } ->
+    (* Left-spine of applications: (((f acc0) arg0) arg1) ... *)
+    let mk_app l r = nd "t.@" (fun e -> E.ref e l; E.ref e r) in
+    let base = mk_app (encode_term self f) (encode_term self acc0) in
+    List.fold_left (fun acc arg -> mk_app acc (encode_term self arg)) base args
+
+(** Encode a literal: positive → its term; negative → [not t]. *)
+let encode_lit (self : t) (tst : Term.store) (lit : Lit.t) : E.offset =
+  let t = if Lit.sign lit then Lit.term lit else Term.not tst (Lit.term lit) in
+  encode_term self t