Fixed circuits being closed too soon

Author: Gustavo2622

flake.nix

@@ -133,7 +133,7 @@
           provers = pkgs.symlinkJoin {
             name = "provers";
             paths = [ 
-	    #  altErgo 
+	      altErgo 
 	      z3 
 	    #  cvc4 
 	      cvc5 

src/ecCircuits.ml

@@ -587,7 +587,7 @@ let circuit_of_form
         let t = doit st t_f in
         let f = doit st f_f in
         let c = doit st c_f in
-        circuit_ite ~c ~t ~f
+        circuit_ite ~strict:true ~c ~t ~f
 
     | Flocal idn -> 
         state_get st idn
@@ -769,6 +769,11 @@ let circuit_of_form
       EcPrinting.(pp_form ppe) f_ 
       (Printexc.to_string e);
       assert false
+    | e ->
+      Format.eprintf "Failed on %a with exception %s@." 
+      EcPrinting.(pp_form ppe) f_
+      (Printexc.to_string e);
+      assert false
 
   and trans_iter (st: state) (hyps: hyps) (f: form) (fs: form list) : circuit =
     (* FIXME: move auxiliary function out of the definitions *)
@@ -961,11 +966,13 @@ let instrs_equiv
 
 (* FIXME: remove variable list from the arguments *)
 (* FIXME: change memory -> memenv                 *)
-let state_of_prog ?me (hyps: hyps) (mem: memory) ?(st: state = empty_state) (proc: instr list)  : state =
+let state_of_prog ?(close = false) ?me (hyps: hyps) (mem: memory) ?(st: state = empty_state) (proc: instr list)  : state =
   let st = 
     List.fold_left (fun st -> process_instr ?me hyps mem ~st) st proc
   in
+  if close then 
   close_circ_lambda st 
+  else st
 
 let rec circ_simplify_form_bitstring_equality
   ?(st: state = empty_state) 

src/ecCircuits.mli

@@ -69,7 +69,7 @@ val circ_simplify_form_bitstring_equality :
   ?pres:circuit list -> hyps -> form -> form
 
 (* Proc processors *)
-val state_of_prog : ?me:memenv -> hyps -> memory -> ?st:state -> instr list -> state 
+val state_of_prog : ?close:bool -> ?me:memenv -> hyps -> memory -> ?st:state -> instr list -> state 
 val instrs_equiv : hyps -> memenv -> ?keep:EcPV.PV.t -> ?st:state -> instr list -> instr list -> bool
 val process_instr : ?me:memenv -> hyps -> memory -> st:state -> instr -> state
 (* val pstate_of_memtype : ?pstate:pstate -> env -> memtype -> pstate * cinput list *)

src/ecLowCircuits.ml

@@ -569,7 +569,7 @@ module type CircuitInterface = sig
   val circuit_is_free : circuit -> bool
 
   (* Direct circuuit constructions *)
-  val circuit_ite : c:circuit -> t:circuit -> f:circuit -> circuit
+  val circuit_ite : ?strict:bool -> c:circuit -> t:circuit -> f:circuit -> circuit
   val circuit_eq : circuit -> circuit -> circuit
   val circuit_eqs : circuit -> circuit -> circuit list
 
@@ -999,18 +999,22 @@ module MakeCircuitInterfaceFromCBackend(Backend: CBackend) : CircuitInterface =
 
   let circuit_is_free (f: circuit) : bool = List.is_empty @@ snd f 
 
-  let circuit_ite ~(c: circuit) ~(t: circuit) ~(f: circuit) : circuit =
-    assert ((circuit_is_free t) && (circuit_is_free f) && (circuit_is_free c));
+  let circuit_ite ?(strict = false) ~(c: circuit) ~(t: circuit) ~(f: circuit) : circuit =
+    let inps = match c, t, f with
+    | (_, []), (_, []), (_, []) when strict -> []
+    | (_, cinps), (_, tinps), (_, finps) when (not strict) && cinps = tinps && cinps = finps -> cinps
+    | _ -> assert false
+    in
     let c = match (fst c).type_ with
     | CBool -> Backend.node_of_reg (fst c).reg
     | _ -> assert false
     in
     let res_r = Backend.reg_ite c (fst t).reg (fst f).reg in
     match ((fst t).type_, (fst f).type_) with
-    | CBitstring nt, CBitstring nf when nt = nf -> {reg = res_r; type_ = (fst t).type_}, []   
-    | CArray {width=wt; count=nt}, CArray {width=wf; count=nf} when wt = wf && nt = nf -> {reg = res_r; type_ = (fst t).type_}, []  
-    | CTuple szs_t, CTuple szs_f when List.all2 (=) szs_t szs_f -> {reg = res_r; type_ = (fst t).type_}, [] 
-    | CBool, CBool -> {reg = res_r; type_ = (fst t).type_}, []
+    | CBitstring nt, CBitstring nf when nt = nf -> {reg = res_r; type_ = (fst t).type_}, inps
+    | CArray {width=wt; count=nt}, CArray {width=wf; count=nf} when wt = wf && nt = nf -> {reg = res_r; type_ = (fst t).type_}, inps  
+    | CTuple szs_t, CTuple szs_f when List.all2 (=) szs_t szs_f -> {reg = res_r; type_ = (fst t).type_}, inps 
+    | CBool, CBool -> {reg = res_r; type_ = (fst t).type_}, inps
     | _ -> raise CircConstructorInvalidArguments
 
   (* TODO: type check? *)

src/phl/ecPhlBDep.ml

@@ -210,8 +210,10 @@ let t_bdep_solve
       let st, cpres = process_pre tc hs_pr in
       let tm = time (toenv hyps) tm "Done with precondition processing" in
 
+      (* Get open state *)
       let st = state_of_prog hyps (fst hs_m) ~st hs_s.s_node in
       let _tm = time (toenv hyps) tm "Done with program circuit gen" in
+
       let res = solve_post ~st ~pres:cpres hyps hs_po in
       EcCircuits.clear_translation_caches ();
       if res then