wip: proper proof production using Proof_ser-based traces

src/base/Proof.ml

@@ -0,0 +1,165 @@
+
+open Base_types
+
+(* we store steps as binary chunks *)
+module CS = Chunk_stack
+
+module Config = struct
+  type storage =
+    | No_store
+    | In_memory
+    | On_disk_at of string
+
+  let pp_storage out = function
+    | No_store -> Fmt.string out "no-store"
+    | In_memory -> Fmt.string out "in-memory"
+    | On_disk_at file -> Fmt.fprintf out "(on-file :at %S)" file
+
+  type t = {
+    enabled: bool;
+    storage: storage;
+  }
+
+  let default = { enabled=true; storage=In_memory }
+  let empty = { enabled=false; storage=No_store }
+
+  let pp out (self:t) =
+    let { enabled; storage } = self in
+    Fmt.fprintf out
+      "(@[config@ :enabled %B@ :storage %a@])"
+      enabled pp_storage storage
+
+  let enable b self = {self with enabled=b}
+  let store_in_memory self = {self with storage=In_memory}
+  let store_on_disk_at file self = {self with storage=On_disk_at file}
+end
+
+(* where we store steps *)
+module Storage = struct
+  type t =
+    | No_store
+    | In_memory of CS.Buf.t
+    | On_disk of string * out_channel
+
+  let pp out = function
+    | No_store -> Fmt.string out "no-store"
+    | In_memory _ -> Fmt.string out "in-memory"
+    | On_disk (file,_) -> Fmt.fprintf out "(on-file %S)" file
+end
+
+(* a step is just a unique integer ID.
+   The actual step is stored in the chunk_stack. *)
+type proof_step = Proof_ser.ID.t
+
+type lit = Lit.t
+type term = Term.t
+
+type t = {
+  mutable enabled : bool;
+  config: Config.t;
+  mutable storage: Storage.t;
+  mutable dispose: unit -> unit;
+  mutable steps: CS.Writer.t;
+}
+type proof_rule = t -> proof_step
+
+module Step_vec = struct
+  type elt=proof_step
+  include VecI32
+  let get = get_i32
+  let set = set_i32
+end
+
+let disable (self:t) : unit =
+  self.enabled <- false;
+  self.storage <- Storage.No_store;
+  self.dispose();
+  self.steps <- CS.Writer.dummy;
+  ()
+
+let nop_ _ = ()
+
+let create ?(config=Config.default) () : t =
+  (* acquire resources for logging *)
+  let storage, steps, dispose =
+    match config.Config.storage with
+    | Config.No_store ->
+      Storage.No_store, CS.Writer.dummy, nop_
+
+    | Config.In_memory ->
+      let buf = CS.Buf.create ~cap:256 () in
+      Storage.In_memory buf, CS.Writer.into_buf buf, nop_
+
+    | Config.On_disk_at file ->
+      let oc =
+        open_out_gen [Open_creat; Open_wronly; Open_trunc; Open_binary] 0o644 file
+      in
+      let w = CS.Writer.into_channel oc in
+      let dispose () = close_out oc in
+      Storage.On_disk (file, oc), w, dispose
+  in
+  { enabled=config.Config.enabled;
+    config;
+    steps; storage; dispose; }
+
+let iter_chunks_ (r:CS.Reader.t) k =
+  let rec loop () =
+    CS.Reader.next r
+      ~finish:nop_
+      ~yield:(fun b i _len ->
+          let step =
+            Proof_ser.Bare.of_bytes_exn Proof_ser.Step.decode b ~off:i in
+          k step;
+          loop ()
+        )
+  in
+  loop ()
+
+let iter_steps_backward (self:t) : Proof_ser.Step.t Iter.t =
+  fun yield ->
+    begin match self.storage with
+      | Storage.No_store -> ()
+      | Storage.In_memory buf ->
+        let r = CS.Reader.from_buf buf in
+        iter_chunks_ r yield
+      | Storage.On_disk (file, _oc) ->
+        let ic = open_in file in
+        let iter = CS.Reader.from_channel_backward ~close_at_end:true ic in
+        iter_chunks_ iter yield
+    end
+
+let dummy_step : proof_step = -1l
+
+let[@inline] enabled (self:t) = self.enabled
+
+let begin_subproof _ = dummy_step
+let end_subproof _ = dummy_step
+let del_clause _ _ (_pr:t) = dummy_step
+let emit_redundant_clause _ ~hyps:_ _ = dummy_step
+let emit_input_clause _ _ = dummy_step
+let define_term _ _ _ = dummy_step
+let emit_unsat _ _ = dummy_step
+let proof_p1 _ _ (_pr:t) = dummy_step
+let emit_unsat_core _ (_pr:t) = dummy_step
+let lemma_preprocess _ _ ~using:_ (_pr:t) = dummy_step
+let lemma_true _ _ = dummy_step
+let lemma_cc _ _ = dummy_step
+let lemma_rw_clause _ ~using:_ (_pr:t) = dummy_step
+let with_defs _ _ (_pr:t) = dummy_step
+
+let lemma_lra _ _ = dummy_step
+
+let lemma_bool_tauto _ _ = dummy_step
+let lemma_bool_c _ _ _ = dummy_step
+let lemma_bool_equiv _ _ _ = dummy_step
+let lemma_ite_true ~ite:_ _ = dummy_step
+let lemma_ite_false ~ite:_ _ = dummy_step
+
+let lemma_isa_cstor ~cstor_t:_ _ (_pr:t) = dummy_step
+let lemma_select_cstor ~cstor_t:_ _ (_pr:t) = dummy_step
+let lemma_isa_split _ _ (_pr:t) = dummy_step
+let lemma_isa_sel _ (_pr:t) = dummy_step
+let lemma_isa_disj _ _ (_pr:t) = dummy_step
+let lemma_cstor_inj _ _ _ (_pr:t) = dummy_step
+let lemma_cstor_distinct _ _ (_pr:t) = dummy_step
+let lemma_acyclicity _ (_pr:t) = dummy_step

src/base/Proof.mli

@@ -0,0 +1,75 @@
+
+(** Proof representation *)
+
+open Base_types
+
+(** Configuration of proofs *)
+module Config : sig
+  type t
+
+  val pp : t Fmt.printer
+
+  val default : t
+  (** Default proof config, enabled *)
+
+  val empty : t
+  (** Disabled proof, without storage *)
+
+  val enable : bool -> t -> t
+  (** Enable/disable proof storage *)
+
+  val store_in_memory : t -> t
+  (** Store proof in memory *)
+
+  val store_on_disk_at : string -> t -> t
+  (** [store_on_disk_at file] stores temporary proof in file [file] *)
+end
+
+(** {2 Main Proof API} *)
+
+type t
+(** A container for the whole proof *)
+
+type proof_step
+(** A proof step in the trace.
+
+    The proof will store all steps, and at the end when we find the empty clause
+    we can filter them to keep only the relevant ones. *)
+
+include Sidekick_core.PROOF
+  with type t := t
+   and type proof_step := proof_step
+   and type lit = Lit.t
+   and type term = Term.t
+
+val lemma_lra : Lit.t Iter.t -> proof_rule
+
+include Sidekick_th_data.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
+
+include Sidekick_th_bool_static.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
+
+(** {2 Creation} *)
+
+val create : ?config:Config.t -> unit -> t
+(** Create new proof.
+    @param config modifies the proof behavior *)
+
+val disable : t -> unit
+(** Disable proof, even if the config would enable it *)
+
+(** {2 Use the proof} *)
+
+val iter_steps_backward : t -> Proof_ser.Step.t Iter.t
+(** Iterates on all the steps of the proof, from the end.
+
+    This will yield nothing if the proof was disabled or used
+    a dummy backend. *)
+

src/base/Proof_quip.ml

@@ -1,5 +1,4 @@
 
-(*
 open Base_types
 
 module T = Term
@@ -197,13 +196,12 @@ module Compress = struct
 
   (* is [t] too small to be shared? *)
   let rec is_small_ t =
-    let open Term_cell in
     match T.view t with
-    | Bool _ -> true
-    | App_fun (_, a) -> IArray.is_empty a (* only constants are small *)
-    | Not u -> is_small_ u
-    | Eq (_, _) | Ite (_, _, _) -> false
-    | LRA _ -> false
+    | T.Bool _ -> true
+    | T.App_fun (_, a) -> IArray.is_empty a (* only constants are small *)
+    | T.Not u -> is_small_ u
+    | T.Eq (_, _) | T.Ite (_, _, _) -> false
+    | T.LRA _ -> false
 
   type name = N_s of string | N_t of T.t
   type sharing_info = {
@@ -533,4 +531,6 @@ let pp_debug ~sharing out p =
   in
   let module M = Quip.Make(Out) in
   M.pp_debug ~sharing p out
-   *)
+
+
+let of_proof _ : t = assert false

src/base/Proof_quip.mli

@@ -0,0 +1,20 @@
+
+(** Proofs of unsatisfiability exported in Quip
+
+    Proofs are used in sidekick when the problem is found {b unsatisfiable}.
+    A proof collects inferences made by the solver into a list of steps,
+    each with its own kind of justification (e.g. "by congruence"),
+    and outputs it in some kind of format.
+
+    Currently we target {{: https://c-cube.github.io/quip-book/ } Quip}
+    as an {b experimental} proof backend.
+*)
+
+open Base_types
+
+type t
+(** The state holding the whole proof. *)
+
+val pp_debug : sharing:bool -> t Fmt.printer
+
+val of_proof : Proof.t -> t

src/base/Sidekick_base.ml

@@ -33,9 +33,11 @@ module Form = Form
 
 module Solver_arg = Solver_arg
 module Lit = Lit
-module Proof_stub = Proof_stub
 
+module Proof_dummy = Proof_dummy
 module Proof_ser = Proof_ser
+module Proof = Proof
+module Proof_quip = Proof_quip
 
 (* re-export *)
 module IArray = IArray

src/base/proof_ser.bare

@@ -1,7 +1,6 @@
 
-type ProofID int
+type ID i32
 type Lit int
-type ExprID int
 
 type Clause {
   lits: []Lit
@@ -10,36 +9,37 @@ type Clause {
 # clause, RUP with previous steps
 type Step_rup {
   res: Clause
-  steps: []ProofID
+  steps: []ID
 }
 
 # lit <-> expr
 type Step_bridge_lit_expr {
   lit: Lit
-  expr: ExprID
+  expr: ID
 }
 
 # prove congruence closure lemma `\/_{e\in eqns} e`
 type Step_cc {
-  eqns: []ExprID
+  eqns: []ID
 }
 
 # prove t=u using some previous steps and unit equations,
 # and add clause (t=u) with given ID
 type Step_preprocess {
-  t: ExprID
-  u: ExprID
-  using: ProofID
+  t: ID
+  u: ID
+  using: []ID
 }
 
 type Step_view
   ( Step_rup
   | Step_bridge_lit_expr
   | Step_cc
+  | Step_preprocess
   )
 
 type Step {
-  id: ProofID
+  id: ID
   view: Step_view
 }
 

src/base/proof_ser.ml

@@ -239,15 +239,15 @@ let of_string dec s = of_bytes dec (Bytes.unsafe_of_string s)
 
 end
 
-module ProofID = struct
-  type t = int64
+module ID = struct
+  type t = int32
   
   (** @raise Bare.Decode.Error in case of error. *)
   let decode (dec: Bare.Decode.t) : t =
-    Bare.Decode.int dec
+    Bare.Decode.i32 dec
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
-    Bare.Encode.int enc self
+    Bare.Encode.i32 enc self
   
 end
 
@@ -263,18 +263,6 @@ module Lit = struct
   
 end
 
-module ExprID = struct
-  type t = int64
-  
-  (** @raise Bare.Decode.Error in case of error. *)
-  let decode (dec: Bare.Decode.t) : t =
-    Bare.Decode.int dec
-  
-  let encode (enc: Bare.Encode.t) (self: t) : unit =
-    Bare.Encode.int enc self
-  
-end
-
 module Clause = struct
   type t = {
     lits: Lit.t array;
@@ -300,7 +288,7 @@ end
 module Step_rup = struct
   type t = {
     res: Clause.t;
-    steps: ProofID.t array;
+    steps: ID.t array;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
@@ -309,7 +297,7 @@ module Step_rup = struct
     let steps =
       (let len = Bare.Decode.uint dec in
        if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
-       Array.init (Int64.to_int len) (fun _ -> ProofID.decode dec)) in
+       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
     {res; steps; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
@@ -317,7 +305,7 @@ module Step_rup = struct
       Clause.encode enc self.res;
       (let arr = self.steps in
        Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ProofID.encode enc xi) arr);
+       Array.iter (fun xi -> ID.encode enc xi) arr);
     end
   
 end
@@ -325,21 +313,21 @@ end
 module Step_bridge_lit_expr = struct
   type t = {
     lit: Lit.t;
-    expr: ExprID.t;
+    expr: ID.t;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
   let decode (dec: Bare.Decode.t) : t =
-    let lit = Lit.decode dec in let expr = ExprID.decode dec in {lit; expr; }
+    let lit = Lit.decode dec in let expr = ID.decode dec in {lit; expr; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin Lit.encode enc self.lit; ExprID.encode enc self.expr; end
+    begin Lit.encode enc self.lit; ID.encode enc self.expr; end
   
 end
 
 module Step_cc = struct
   type t = {
-    eqns: ExprID.t array;
+    eqns: ID.t array;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
@@ -347,37 +335,42 @@ module Step_cc = struct
     let eqns =
       (let len = Bare.Decode.uint dec in
        if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
-       Array.init (Int64.to_int len) (fun _ -> ExprID.decode dec)) in
+       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
     {eqns; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
     begin
       (let arr = self.eqns in
        Bare.Encode.uint enc (Int64.of_int (Array.length arr));
-       Array.iter (fun xi -> ExprID.encode enc xi) arr);
+       Array.iter (fun xi -> ID.encode enc xi) arr);
     end
   
 end
 
 module Step_preprocess = struct
   type t = {
-    t: ExprID.t;
-    u: ExprID.t;
-    using: ProofID.t;
+    t: ID.t;
+    u: ID.t;
+    using: ID.t array;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
   let decode (dec: Bare.Decode.t) : t =
-    let t = ExprID.decode dec in
-    let u = ExprID.decode dec in
-    let using = ProofID.decode dec in
+    let t = ID.decode dec in
+    let u = ID.decode dec in
+    let using =
+      (let len = Bare.Decode.uint dec in
+       if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
+       Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
     {t; u; using; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
     begin
-      ExprID.encode enc self.t;
-      ExprID.encode enc self.u;
-      ProofID.encode enc self.using;
+      ID.encode enc self.t;
+      ID.encode enc self.u;
+      (let arr = self.using in
+       Bare.Encode.uint enc (Int64.of_int (Array.length arr));
+       Array.iter (fun xi -> ID.encode enc xi) arr);
     end
   
 end
@@ -387,6 +380,7 @@ module Step_view = struct
     | Step_rup of Step_rup.t
     | Step_bridge_lit_expr of Step_bridge_lit_expr.t
     | Step_cc of Step_cc.t
+    | Step_preprocess of Step_preprocess.t
     
   
   (** @raise Bare.Decode.Error in case of error. *)
@@ -396,6 +390,7 @@ module Step_view = struct
     | 0L -> Step_rup (Step_rup.decode dec)
     | 1L -> Step_bridge_lit_expr (Step_bridge_lit_expr.decode dec)
     | 2L -> Step_cc (Step_cc.decode dec)
+    | 3L -> Step_preprocess (Step_preprocess.decode dec)
     | _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
     
   
@@ -410,24 +405,25 @@ module Step_view = struct
     | Step_cc x ->
       Bare.Encode.uint enc 2L;
       Step_cc.encode enc x
+    | Step_preprocess x ->
+      Bare.Encode.uint enc 3L;
+      Step_preprocess.encode enc x
     
     
 end
 
 module Step = struct
   type t = {
-    id: ProofID.t;
+    id: ID.t;
     view: Step_view.t;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
   let decode (dec: Bare.Decode.t) : t =
-    let id = ProofID.decode dec in
-    let view = Step_view.decode dec in
-    {id; view; }
+    let id = ID.decode dec in let view = Step_view.decode dec in {id; view; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
-    begin ProofID.encode enc self.id; Step_view.encode enc self.view; end
+    begin ID.encode enc self.id; Step_view.encode enc self.view; end
   
 end
 

src/proof/Proof.mli

@@ -1,31 +0,0 @@
-
-(*
-(** Proofs of unsatisfiability
-
-    Proofs are used in sidekick when the problem is found {b unsatisfiable}.
-    A proof collects inferences made by the solver into a list of steps,
-    each with its own kind of justification (e.g. "by congruence"),
-    and outputs it in some kind of format.
-
-    Currently we target {{: https://c-cube.github.io/quip-book/ } Quip}
-    as an experimental proof backend.
-*)
-
-open Base_types
-
-include Sidekick_core.PROOF
-  with type term = Term.t
-   and type ty = Ty.t
-
-val isa_split : ty -> term Iter.t -> t
-val isa_disj : ty -> term -> term -> t
-val cstor_inj : Cstor.t -> int -> term list -> term list -> t
-
-val bool_eq : term -> term -> t
-val bool_c : string -> term list -> t
-val ite_true : term -> t
-val ite_false : term -> t
-
-val lra : lit Iter.t -> t
-val lra_l : lit list -> t
-   *)

src/util/Chunk_stack.ml

@@ -106,7 +106,7 @@ module Reader = struct
     in
     { read; }
 
-  let from_channel_backward ic =
+  let from_channel_backward ?(close_at_end=false) ic =
     let len = in_channel_length ic in
     seek_in ic len;
 
@@ -131,6 +131,7 @@ module Reader = struct
 
         yield buf.Buf.b 0 buf.Buf.len
       ) else (
+        if close_at_end then close_in_noerr ic;
         finish()
       )
     in
@@ -138,7 +139,7 @@ module Reader = struct
 
   let with_file_backward (filename:string) f =
     CCIO.with_in ~flags:[Open_binary; Open_rdonly] filename @@ fun ic ->
-    let r = from_channel_backward ic in
+    let r = from_channel_backward ~close_at_end:false ic in
     f r
 end
 

src/util/Chunk_stack.mli

@@ -56,7 +56,7 @@ module Reader : sig
 
   val from_buf : Buf.t -> t
 
-  val from_channel_backward : in_channel -> t
+  val from_channel_backward : ?close_at_end:bool -> in_channel -> t
   (** Read channel from the end, assuming that is possible. *)
 
   val with_file_backward : string -> (t -> 'a) -> 'a