wip: feat(proof): lib sidekick.proof with tracing

src/proof/core_rules.ml

@@ -0,0 +1,24 @@
+(* FIXME
+   open Proof_trace
+
+   type lit = Lit.t
+*)
+
+type lit = Lit.t
+
+let lemma_cc lits : Pterm.t = Pterm.apply_rule ~lits "core.lemma-cc"
+let define_term t1 t2 = Pterm.apply_rule ~terms:[ t1; t2 ] "core.define-term"
+let proof_r1 p1 p2 = Pterm.apply_rule ~premises:[ p1; p2 ] "core.r1"
+let proof_p1 p1 p2 = Pterm.apply_rule ~premises:[ p1; p2 ] "core.p1"
+
+let proof_res ~pivot p1 p2 =
+  Pterm.apply_rule ~terms:[ pivot ] ~premises:[ p1; p2 ] "core.res"
+
+let with_defs pr defs = Pterm.apply_rule ~premises:(pr :: defs) "core.with-defs"
+let lemma_true t = Pterm.apply_rule ~terms:[ t ] "core.true"
+
+let lemma_preprocess t1 t2 ~using =
+  Pterm.apply_rule ~terms:[ t1; t2 ] ~premises:using "core.preprocess"
+
+let lemma_rw_clause pr ~res ~using =
+  Pterm.apply_rule ~premises:(pr :: using) ~lits:res "core.rw-clause"

src/proof/core_rules.mli

@@ -0,0 +1,54 @@
+(** Core proofs for SMT and congruence closure. *)
+
+open Sidekick_core_logic
+
+type lit = Lit.t
+
+val lemma_cc : lit list -> Pterm.t
+(** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
+     of uninterpreted functions. *)
+
+val define_term : Term.t -> Term.t -> Pterm.t
+(** [define_term cst u proof] defines the new constant [cst] as being equal
+     to [u].
+     The result is a proof of the clause [cst = u] *)
+
+val proof_p1 : Pterm.step_id -> Pterm.step_id -> Pterm.t
+(** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
+     and [p2] proves [C \/ t], is the Pterm.t that produces [C \/ u],
+     i.e unit paramodulation. *)
+
+val proof_r1 : Pterm.step_id -> Pterm.step_id -> Pterm.t
+(** [proof_r1 p1 p2], where [p1] proves the unit clause [|- t] (t:bool)
+       and [p2] proves [C \/ ¬t], is the Pterm.t that produces [C \/ u],
+       i.e unit resolution. *)
+
+val proof_res : pivot:Term.t -> Pterm.step_id -> Pterm.step_id -> Pterm.t
+(** [proof_res ~pivot p1 p2], where [p1] proves the clause [|- C \/ l]
+     and [p2] proves [D \/ ¬l], where [l] is either [pivot] or [¬pivot],
+     is the Pterm.t that produces [C \/ D], i.e boolean resolution. *)
+
+val with_defs : Pterm.step_id -> Pterm.step_id list -> Pterm.t
+(** [with_defs pr defs] specifies that [pr] is valid only in
+       a context where the definitions [defs] are present. *)
+
+val lemma_true : Term.t -> Pterm.t
+(** [lemma_true (true) p] asserts the clause [(true)] *)
+
+val lemma_preprocess : Term.t -> Term.t -> using:Pterm.step_id list -> Pterm.t
+(** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
+     and that [t] has been preprocessed into [u].
+
+     The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
+     closure, and then resolved against the clauses [using] to obtain
+     a unit equality.
+
+     From now on, [t] and [u] will be used interchangeably.
+     @return a Pterm.t ID for the clause [(t=u)]. *)
+
+val lemma_rw_clause :
+  Pterm.step_id -> res:lit list -> using:Pterm.step_id list -> Pterm.t
+(** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
+     uses the equations [|- p_i = q_i] from [using]
+     to rewrite some literals of [c] into [res]. This is used to preprocess
+     literals of a clause (using {!lemma_preprocess} individually). *)

src/proof/dune

@@ -0,0 +1,5 @@
+(library
+ (name sidekick_proof)
+ (public_name sidekick.proof)
+ (flags :standard -open Sidekick_util -open Sidekick_core)
+ (libraries sidekick.core sidekick.trace))

src/proof/pterm.ml

@@ -0,0 +1,53 @@
+open Sidekick_core_logic
+
+type step_id = Step.id
+type lit = Lit.t
+type local_ref = Step.id
+
+type rule_apply = {
+  rule_name: string;
+  lit_args: lit list;
+  term_args: Term.t list;
+  subst_args: Subst.t list;
+  premises: step_id list;
+  indices: int list;
+}
+
+type t =
+  | P_ref of step_id
+  | P_local of local_ref
+  | P_let of (local_ref * t) list * t
+  | P_apply of rule_apply
+
+type delayed = unit -> t
+
+let rec pp out = function
+  | P_ref r -> Fmt.fprintf out "!%d" r
+  | P_local id -> Fmt.fprintf out "s%d" id
+  | P_apply r -> Fmt.fprintf out "%s" r.rule_name
+  | P_let (bs, bod) ->
+    let pp_b out (x, t) = Fmt.fprintf out "s%d := %a" x pp t in
+    Fmt.fprintf out "(@[let %a@ in %a@])"
+      (Util.pp_list ~sep:"; " pp_b)
+      bs pp bod
+
+let local_ref id = P_local id
+let ref id = P_ref id
+let[@inline] delay f = f
+
+let let_ bs r =
+  match bs with
+  | [] -> r
+  | _ -> P_let (bs, r)
+
+let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
+    ?(indices = []) rule_name : t =
+  P_apply
+    {
+      rule_name;
+      lit_args = lits;
+      subst_args = substs;
+      term_args = terms;
+      premises;
+      indices;
+    }

src/proof/pterm.mli

@@ -0,0 +1,46 @@
+(** Proof terms.
+
+  A proof term is the description of a reasoning step, that yields a clause. *)
+
+open Sidekick_core_logic
+
+type step_id = Step.id
+type lit = Lit.t
+
+type local_ref = Step.id
+(** A local reference is a step id that is only valid in the scope
+    of a {!P_let}. Typically one can use negative integers to avoid
+    accidental shadowing. *)
+
+type rule_apply = {
+  rule_name: string;
+  lit_args: lit list;
+  term_args: Term.t list;
+  subst_args: Subst.t list;
+  premises: step_id list;
+  indices: int list;
+}
+
+type t =
+  | P_ref of step_id
+  | P_local of local_ref  (** Local reference, in a let *)
+  | P_let of (local_ref * t) list * t
+  | P_apply of rule_apply
+
+type delayed = unit -> t
+
+include Sidekick_sigs.PRINT with type t := t
+
+val ref : step_id -> t
+val local_ref : local_ref -> t
+val let_ : (local_ref * t) list -> t -> t
+val delay : (unit -> t) -> delayed
+
+val apply_rule :
+  ?lits:lit list ->
+  ?terms:Term.t list ->
+  ?substs:Subst.t list ->
+  ?premises:step_id list ->
+  ?indices:int list ->
+  string ->
+  t

src/proof/sat_rules.ml

@@ -0,0 +1,12 @@
+let name_sat_input = "sat.input"
+let name_redundant_clause = "sat.rc"
+let name_unsat_core = "sat.uc"
+
+type lit = Lit.t
+
+let sat_input_clause lits : Pterm.t = Pterm.apply_rule name_sat_input ~lits
+
+let sat_redundant_clause lits ~hyps : Pterm.t =
+  Pterm.apply_rule name_redundant_clause ~lits ~premises:(Iter.to_rev_list hyps)
+
+let sat_unsat_core lits : Pterm.t = Pterm.apply_rule ~lits name_unsat_core

src/proof/sat_rules.mli

@@ -0,0 +1,13 @@
+(** SAT-solver proof emission. *)
+
+type lit = Lit.t
+
+val sat_input_clause : lit list -> Pterm.t
+(** Emit an input clause. *)
+
+val sat_redundant_clause : lit list -> hyps:Step.id Iter.t -> Pterm.t
+(** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
+    The clause must be RUP wrt [hyps]. *)
+
+val sat_unsat_core : lit list -> Pterm.t
+(** TODO: is this relevant here? *)

src/proof/sidekick_proof.ml

@@ -0,0 +1,11 @@
+module Step = Step
+module Step_vec = Step_vec
+module Sat_rules = Sat_rules
+module Core_rules = Core_rules
+module Pterm = Pterm
+module Tracer = Tracer
+module Arg = Arg
+
+type term = Pterm.t
+type term_ref = Step.id
+type step_id = Step.id

src/proof/step.ml

@@ -0,0 +1,3 @@
+type id = Sidekick_trace.Entry_id.t
+
+let pp : id Fmt.printer = Fmt.int

src/proof/step_vec.ml

@@ -0,0 +1,19 @@
+type elt = Step.id
+type t = elt Vec.t
+
+let get = Vec.get
+let size = Vec.size
+let iter = Vec.iter
+let iteri = Vec.iteri
+let create ?cap:_ () = Vec.create ()
+let clear = Vec.clear
+let copy = Vec.copy
+let is_empty = Vec.is_empty
+let push = Vec.push
+let fast_remove = Vec.fast_remove
+let filter_in_place = Vec.filter_in_place
+let ensure_size v len = Vec.ensure_size v ~elt:0 len
+let pop = Vec.pop_exn
+let set = Vec.set
+let shrink = Vec.shrink
+let to_iter = Vec.to_iter

src/proof/step_vec.mli

@@ -0,0 +1,3 @@
+(** A vector indexed by steps. *)
+
+include Vec_sig.BASE with type elt = Step.id

src/proof/tracer.ml

@@ -0,0 +1,35 @@
+module Tr = Sidekick_trace
+
+type step_id = Step.id
+
+class type t =
+  object
+    method proof_enabled : bool
+    method emit_proof_step : Pterm.delayed -> step_id
+    method emit_proof_delete : step_id -> unit
+  end
+
+let[@inline] enabled (self : #t) : bool = self#proof_enabled
+let[@inline] add_step (self : #t) rule : step_id = self#emit_proof_step rule
+let[@inline] delete (self : #t) s : unit = self#emit_proof_delete s
+let dummy_step_id : step_id = Sidekick_trace.Entry_id.dummy
+
+class dummy : t =
+  object
+    method proof_enabled = false
+    method emit_proof_step _ = dummy_step_id
+    method emit_proof_delete _ = ()
+  end
+
+let dummy : t = new dummy
+
+class concrete ~sink : t =
+  object
+    method proof_enabled = true
+
+    method emit_proof_delete id : unit =
+      Tr.Sink.emit' sink ~tag:"Pd" (Ser_value.int id)
+
+    method emit_proof_step (p : Pterm.delayed) : step_id = assert false
+    (* TODO *)
+  end

src/proof/tracer.mli

@@ -0,0 +1,50 @@
+(** Proof traces.
+
+    A proof trace is a log of all the deductive reasoning steps made by
+    the SMT solver and other reasoning components. It essentially stores
+    a DAG of all these steps, where each step points (via {!step_id})
+    to its premises.
+*)
+
+type step_id = Step.id
+(** Identifier for a tracing step (like a unique ID for a clause previously
+    added/proved) *)
+
+(** A proof tracer.
+
+    A proof tracer builds a log of all deductive steps taken by the solver,
+    so we can later reconstruct a certificate for proof-checking.
+
+    Each step in the proof trace should be a {b valid
+    lemma} (of its theory) or a {b valid consequence} of previous steps.
+*)
+class type t =
+  object
+    method proof_enabled : bool
+    (** If proof tracing enabled? *)
+
+    method emit_proof_step : Pterm.delayed -> step_id
+    (** Create a new step in the trace. *)
+
+    method emit_proof_delete : step_id -> unit
+    (** Forget a step that won't be used in the rest of the trace.
+        Only useful for performance/memory considerations. *)
+  end
+
+val enabled : #t -> bool
+(** Is proof tracing enabled? *)
+
+val add_step : #t -> Pterm.delayed -> step_id
+(** Create a new step in the trace. *)
+
+val delete : #t -> step_id -> unit
+(** Forget a step that won't be used in the rest of the trace.
+    Only useful for performance/memory considerations. *)
+
+class dummy : t
+(** Dummy proof trace, logs nothing. *)
+
+val dummy : t
+
+class concrete : sink:Sidekick_trace.Sink.t -> t
+(** Concrete implementation of [t] *)