Added bdep solve + example

Author: Gustavo2622

examples/mapreduce_paper.ec

@@ -106,3 +106,8 @@ bdep 8 8 [w] [w1] [w1] xor_left_spec predT_W8.
 admit.
 admit.
 qed.
+
+lemma xor_left_eq_xor_right : forall (w: W8.t),  xor_left w = xor_right w.
+    proof.
+      bdep solve.
+    qed.

libs/lospecs/hlaig.ml

@@ -50,9 +50,9 @@ end
 module type SMTInterface = sig
   val circ_equiv : ?inps:(int * int) list -> reg -> reg -> node ->  bool
 
-  val circ_sat : node -> bool
+  val circ_sat : ?inps:(int * int) list -> node -> bool
 
-  val circ_taut : node -> bool
+  val circ_taut : ?inps:(int * int) list -> node -> bool
 end
 
 (* TODO Add model printing for circ_sat and circ_taut *)
@@ -139,7 +139,7 @@ module MakeSMTInterface(SMT: SMTInstance) : SMTInterface = struct
     end
 
 
-  let circ_sat (n : Aig.node) : bool =
+  let circ_sat ?(inps: (int * int) list option) (n : Aig.node) : bool =
     let bvvars : SMT.bvterm Map.String.t ref = ref Map.String.empty in
 
     let rec bvterm_of_node : Aig.node -> SMT.bvterm =
@@ -175,6 +175,24 @@ module MakeSMTInterface(SMT: SMTInstance) : SMTInterface = struct
 
     let form = bvterm_of_node n in 
 
+    let inps = Option.bind inps (fun l -> 
+      if List.is_empty l then None
+      else Some l
+    ) in
+
+    let inps = Option.map (fun inps ->
+      List.map (fun (id,sz) -> 
+      List.init sz (fun i -> ("BV_" ^ (id |> string_of_int) ^ "_" ^ (Printf.sprintf "%X" (i))))) inps 
+    ) inps in
+    let inps = Option.map (fun inps ->
+    List.map (List.map (fun name -> match Map.String.find_opt name !bvvars with
+    | Some bv -> bv
+    | None -> SMT.bvterm_of_name 1 name)) inps) inps
+    in
+    let bvinp = Option.map (fun inps -> 
+      List.map (fun i -> List.reduce (SMT.bvterm_concat) i) inps) inps 
+    in
+
     begin
       SMT.assert' @@ form;
       if SMT.check_sat () = true then 
@@ -184,16 +202,19 @@ module MakeSMTInterface(SMT: SMTInstance) : SMTInterface = struct
         |> List.map (fun a -> snd a) in
         let term = List.reduce SMT.bvterm_concat terms in
         Format.eprintf "input: %a@."     SMT.pp_term (SMT.get_value term);
-        
+        Option.may (fun bvinp ->
+        List.iteri (fun i bv -> 
+        Format.eprintf "input[%d]: %a@." i SMT.pp_term (SMT.get_value bv)        
+        ) bvinp) bvinp;
         (* Format.eprintf "fc: %a@."     SMT.pp_term (SMT.get_value bvinpt1); *)
         (* Format.eprintf "block: %a@."  SMT.pp_term (SMT.get_value bvinpt2); *)
         true 
       end
       else false
     end
 
-  let circ_taut (n: Aig.node) : bool =
-    not @@ circ_sat (Aig.neg n)
+  let circ_taut ?inps (n: Aig.node) : bool =
+    not @@ circ_sat ?inps (Aig.neg n)
 
 end
 

src/ecCircuits.ml

@@ -189,8 +189,10 @@ module type CircuitInterface = sig
   val circuit_uninit : env -> ty -> circuit
   val circuit_has_uninitialized : circuit -> bool
 
-  (* Circuit equivalence call, should do some processing and then call some backend *)
+  (* Logical reasoning over circuits *)
   val circ_equiv : ?pcond:(cbool * (cinp list)) -> circuit -> circuit -> bool
+  val circ_sat   : circuit -> bool 
+  val circ_taut  : circuit -> bool 
 
   (* Composition of circuit functions, should deal with inputs and call some backend *)
   val circuit_compose : circuit -> circuit list -> circuit
@@ -248,6 +250,8 @@ module type CBackend = sig
   val applys : (inp -> node option) -> reg -> reg
   val circuit_from_spec : Lospecs.Ast.adef -> reg list -> reg 
   val equiv : ?inps:inp list -> pcond:node -> reg -> reg -> bool
+  val sat : ?inps:inp list -> node -> bool 
+  val taut : ?inps:inp list -> node -> bool 
 
   val slice : reg -> int -> int -> reg
   val insert : reg -> int -> reg -> reg
@@ -395,6 +399,16 @@ module TestBack : CBackend = struct
     let module BWZ = (val makeBWZinterface ()) in
     BWZ.circ_equiv ?inps (node_list_of_reg r1) (node_list_of_reg r2) pcond  
 
+  let sat ?(inps: inp list option) (n: node) : bool =
+    let open HL in
+    let module BWZ = (val makeBWZinterface ()) in
+    BWZ.circ_sat ?inps n 
+
+  let taut ?(inps: inp list option) (n: node) : bool =
+    let open HL in
+    let module BWZ = (val makeBWZinterface ()) in
+    BWZ.circ_taut ?inps n 
+
   let slice (r: reg) (idx: int) (len: int) : reg = 
     Array.sub r idx len
 
@@ -1397,7 +1411,28 @@ module MakeCircuitInterfaceFromCBackend(Backend: CBackend) : CircuitInterface =
     | `CBool b1, `CBool b2 ->
         Backend.equiv ~inps ~pcond:pcc (Backend.reg_of_node b1) (Backend.reg_of_node b2)
     | _ -> false
+
+  let circ_sat (c: circuit) : bool =
+    let `CBool c, inps = cbool_of_circuit ~strict:false c in
+    let inps = List.map (function 
+      | { type_ = `CIBool; id } -> (id, 1)
+      | { type_ = `CIBitstring w; id } -> (id, w) 
+      | { type_ = `CIArray (w1, w2); id } -> (id, w1*w2)
+      | { type_ = `CITuple szs; id } -> (id, List.sum szs) 
+
+    ) inps in
+    Backend.sat ~inps c 
 
+  let circ_taut (c: circuit) : bool = 
+    let `CBool c, inps = cbool_of_circuit ~strict:false c in
+    let inps = List.map (function 
+      | { type_ = `CIBool; id } -> (id, 1)
+      | { type_ = `CIBitstring w; id } -> (id, w) 
+      | { type_ = `CIArray (w1, w2); id } -> (id, w1*w2)
+      | { type_ = `CITuple szs; id } -> (id, List.sum szs) 
+
+    ) inps in
+    Backend.taut ~inps c 
 
   module CircuitSpec = struct
     let circuit_from_spec env (c : [`Path of path | `Bind of EcDecl.crb_circuit ] ) : [> `CBitstring of cbitstring_type] cfun = 
@@ -1788,10 +1823,8 @@ let circuit_of_form
         begin match EcFol.op_kind (destr_op f_ |> fst) with
           | Some `True -> 
             hyps, (circuit_true :> circuit)
-            (*hyps, {circ = BWCirc([C.true_]); inps=[]}*)
           | Some `False ->
             hyps, (circuit_false :> circuit)
-            (*hyps, {circ = BWCirc([C.false_]); inps=[]}*)
           | _ -> 
             let err = Format.sprintf "Unsupported op kind%s@." (EcPath.tostring pth) in
             raise (CircError err)
@@ -1848,8 +1881,8 @@ let circuit_of_form
       let cache = open_circ_lambda_cache env cache binds in
       let hyps, circ = doit cache hyps f in
       begin match qnt with
-      | Llambda -> hyps, close_circ_lambda env binds circ 
       | Lforall 
+      | Llambda -> hyps, close_circ_lambda env binds circ 
       | Lexists -> raise (CircError "Universal/Existential quantification not supported ")
       (* TODO: figure out how to handle quantifiers *)
       end
@@ -2078,6 +2111,9 @@ let circ_equiv ?(pcond: circuit option) c1 c2 =
   in
   circ_equiv ?pcond c1 c2
 
+let circ_sat = circ_sat
+let circ_taut = circ_taut
+
 let circuit_permute (bsz: int) (perm: int -> int) (c: circuit) : circuit =
   let c = match c with
   | (`CBitstring r, inps) as c -> c

src/ecCircuits.mli

@@ -36,8 +36,10 @@ val circuit_permute : int -> (int -> int) -> circuit -> circuit
 val circuit_mapreduce : ?perm:(int -> int)  -> circuit -> int -> int -> circuit list
 
 (* Use circuits *)
-val compute : sign:bool -> circuit -> BI.zint list -> BI.zint
+val compute    : sign:bool -> circuit -> BI.zint list -> BI.zint
 val circ_equiv : ?pcond:circuit -> circuit -> circuit -> bool
+val circ_sat   : circuit -> bool 
+val circ_taut  : circuit -> bool 
 
 (* Generate circuits *)
 (* Form processors *)

src/ecHiTacticals.ml

@@ -235,6 +235,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pbdep bdinfo              -> EcPhlBDep.process_bdep bdinfo
     | Pbdepeval bdeinfo         -> EcPhlBDep.process_bdep_eval bdeinfo
     | Pbdepeq bdeinfo           -> EcPhlBDep.process_bdepeq bdeinfo
+    | Pbdepsolve                -> EcPhlBDep.t_bdep_solve
     | Pcirc (invs, f, v)        -> EcPhlBDep.process_bdep_form invs f v
     | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
   in

src/ecParser.mly

@@ -3264,6 +3264,9 @@ bdepeq_out_info:
 | BDEP BITSTRING invs=bracket(bd_vars) f=bracket(form) v=lident 
   { Pcirc (invs, f, (`Var v :> bdepvar)) }
 
+| BDEP SOLVE
+  { Pbdepsolve }
+
 bdhoare_split:
 | b1=sform b2=sform b3=sform?
     { BDH_split_bop (b1,b2,b3) }

src/ecParsetree.ml

@@ -831,6 +831,7 @@ type phltactic =
   | Pbdepeval of bdep_eval_info
   | Pbdepeq of bdepeq_info
   | Pcirc of (bdepvar list * pformula * bdepvar)
+  | Pbdepsolve
 
     (* Program rewriting *)
   | Prwprgm of rwprgm

src/phl/ecPhlBDep.ml

@@ -1000,4 +1000,10 @@ let process_bdep_eval (bdeinfo: bdep_eval_info) (tc: tcenv1) =
   let tc = EcPhlConseq.t_hoareS_conseq_nm pre post tc in
   FApi.t_last (t_bdep_eval n m inpvs outvs lane frange sign) tc 
 
+let t_bdep_solve
+  (tc : tcenv1) =
+  if circ_taut (circuit_of_form (FApi.tc1_hyps tc) (FApi.tc1_goal tc)) then
+  FApi.close (!@ tc) VBdep
+  else 
+  tc_error (FApi.tc1_penv tc) "Failed to solve goal through circuit reasoning@\n"  
 

src/phl/ecPhlBDep.mli

@@ -13,6 +13,8 @@ val t_bdep : int -> int -> variable list -> variable list -> psymbol -> psymbol
 val t_bdepeq : variable list * variable list -> int -> (int * variable list * variable list) list -> form option -> bool -> tcenv1 -> tcenv
 
 val t_bdep_eval :  int ->  int ->  variable list ->  variable list ->  psymbol ->  form list -> bool -> tcenv1 -> tcenv
+
+val t_bdep_solve : tcenv1 -> tcenv 
 
 val process_bdep : bdep_info -> tcenv1 -> tcenv