Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep

config/tests.config

@@ -8,7 +8,7 @@ exclude = theories/prelude
 
 [test-examples]
 okdirs  = !examples
-exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port
+exclude = examples/MEE-CBC examples/exclude examples/old examples/old/list-ddh !examples/incomplete examples/to-port
 
 [test-mee-cbc]
 okdirs = examples/MEE-CBC

dune-project

@@ -14,6 +14,7 @@
  (depends
   (ocaml (>= 4.08.0))
   (batteries (>= 3))
+  bitwuzla
   (camlp-streams (>= 5))
   camlzip
   cmdliner

easycrypt.opam

@@ -2,6 +2,7 @@
 depends: [
   "ocaml" {>= "4.08.0"}
   "batteries" {>= "3"}
+  "bitwuzla"
   "camlp-streams" {>= "5"}
   "camlzip"
   "cmdliner"

src/ecCircuits.ml

@@ -849,10 +849,13 @@ let circ_sat (f: circuit) (pcond: circuit option): bool =
 (* Refactor this later *)
 let op_cache = ref Mp.empty
 
+type pstate = (symbol, circuit) Map.t
+type cache  = (ident, (cinput * circuit)) Map.t
+
 (* TODO: simplify args and unify dealing with cache / vars *)
 let circuit_of_form 
-  ?(pstate : (symbol, circuit) Map.t = Map.empty) 
-  ?(cache  : (ident, (cinput * circuit))  Map.t = Map.empty) 
+  ?(pstate : pstate = Map.empty) 
+  ?(cache  : cache = Map.empty) 
    (env    : env) 
    (f      : EcAst.form) 
   : circuit =
@@ -1083,7 +1086,7 @@ let pstate_of_memtype ?(pstate = Map.empty) (env: env) (mt: memtype) =
   in pstate, inps
 
 
-let process_instr (env:env) (mem: memory) ?(cache: _ = Map.empty) (pstate: _) (inst: instr) =
+let process_instr (env:env) (mem: memory) ?(cache: cache = Map.empty) (pstate: _) (inst: instr) =
   try
     match inst.i_node with
     | Sasgn (LvVar (PVloc v, ty), e) -> Map.add v (form_of_expr mem e |> circuit_of_form ~pstate ~cache env) pstate

src/ecCircuits.mli

@@ -0,0 +1,35 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcIdent
+open EcSymbols
+open EcAst
+open EcEnv
+
+(* -------------------------------------------------------------------- *)
+module Map = Batteries.Map
+
+(* -------------------------------------------------------------------- *)
+type circ
+type cinput
+type circuit = { circ: circ; inps: cinput list; }
+type pstate = (symbol, circuit) Map.t
+type cache  = (EcIdent.t, (cinput * circuit)) Map.t
+
+(* -------------------------------------------------------------------- *)
+exception CircError of string
+
+(* -------------------------------------------------------------------- *)
+val cinput_to_string : cinput -> string
+val cinput_of_type : ?idn:ident -> env -> ty -> cinput
+val circuit_to_string : circuit -> string
+val circ_ident : cinput -> circuit
+val circuit_aggregate : circuit list -> circuit
+val circuit_mapreduce : circuit -> int -> int -> circuit list
+val circ_check : circuit -> circuit option -> bool
+val circ_equiv : circuit -> circuit -> circuit option -> bool
+val circuit_of_form : ?pstate:pstate -> ?cache:cache -> env -> form -> circuit
+val pstate_of_memtype : ?pstate:pstate -> env -> memtype -> pstate * cinput list
+val input_of_variable : env -> variable -> circuit * cinput
+val insts_equiv : env -> memenv -> ?pstate:pstate -> instr list -> instr list -> bool
+val process_op : env -> pqsymbol -> pqsymbol -> unit
+val process_instr : env -> memory -> ?cache:cache -> pstate -> instr -> (symbol, circuit) Map.t

src/ecParser.mly

@@ -660,6 +660,7 @@ _lident:
 | ABORT      { "abort"      }
 | ADMITTED   { "admitted"   }
 | ASYNC      { "async"      }
+| BIND       { "bind"       }
 | DEBUG      { "debug"      }
 | DUMP       { "dump"       }
 | EXPECT     { "expect"     }