cloning, cleaning

libs/lospecs/circuit_avx2.mli

@@ -0,0 +1,34 @@
+type symbol = string
+module type S =
+ sig
+ val get_specification : symbol -> Ast.adef option
+ val vpermd : Aig.reg -> Aig.reg -> Aig.reg
+ val vpermq : Aig.reg -> int -> Aig.reg
+ val vpbroadcast_16u16 : Aig.reg -> Aig.reg
+ val vpadd_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpadd_32u8 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpsub_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpsub_32u8 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpand_256 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpmaddubsw_256 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpmulh_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpmulhrs_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpsra_16u16 : Aig.reg -> int -> Aig.reg
+ val vpsrl_16u16 : Aig.reg -> int -> Aig.reg
+ val vpsrl_4u64 : Aig.reg -> int -> Aig.reg
+ val vpsll_4u64 : Aig.reg -> int -> Aig.reg
+ val vpackus_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpackss_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpshufb_256 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpcmpgt_16u16 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpmovmskb_u256u64 : Aig.reg -> Aig.reg
+ val vpunpckl_32u8 : Aig.reg -> Aig.reg -> Aig.reg
+ val vpextracti128 : Aig.reg -> int -> Aig.reg
+ val vpinserti128 : Aig.reg -> Aig.reg -> int -> Aig.reg
+ val vpblend_16u16 : Aig.reg -> Aig.reg -> int -> Aig.reg
+ val vpslldq_256 : Aig.reg -> int -> Aig.reg
+ val vpsrldq_256 : Aig.reg -> int -> Aig.reg
+ val vpslldq_128 : Aig.reg -> int -> Aig.reg
+ val vpsrldq_128 : Aig.reg -> int -> Aig.reg
+ end
+module FromSpec : functor () -> S

libs/lospecs/circuit_spec.mli

@@ -0,0 +1,19 @@
+val log2 : int -> int
+module Env :
+ sig
+ type env
+ val empty : env
+ module Fun :
+ sig
+ val get : env -> Ast.ident -> Ast.aargs * Ast.aexpr
+ val bind : env -> Ast.ident -> Ast.aargs * Ast.aexpr -> env
+ end
+ module Var :
+ sig
+ val get : env -> Ast.ident -> Aig.reg
+ val bind : env -> Ast.ident -> Aig.reg -> env
+ val bindall : env -> (Ast.ident * Aig.reg) list -> env
+ end
+ end
+type env = Env.env
+val circuit_of_spec : Aig.reg list -> Ast.adef -> Aig.reg

src/ecCircuits.ml

@@ -3,7 +3,6 @@ open EcUtils
 open EcBigInt
 open EcSymbols
 open EcPath
-open EcParsetree
 open EcEnv
 open EcAst
 open EcCoreFol
@@ -1306,32 +1305,3 @@ let insts_equiv (env: env) ((mem, mt): memenv) ?(pstate: _ = Map.empty) (insts_l
  let circ2 = {circ2 with inps=inps @ circ2.inps} in
  bacc && (circ_equiv circ circ2 None)) 
  pstate_left true
-
-(* -------------------------------------------------------------------- *)
-(* WIP *)
-let process_op (env : env) (f: pqsymbol) (f2: pqsymbol) : unit = 
- let f = EcEnv.Op.lookup f.pl_desc env |> snd in
- let f = match f.op_kind with
- | OB_oper (Some (OP_Plain f)) -> f
- | _ -> failwith "Invalid operator type" in
- let fc = circuit_of_form env f in
-
- let f2 = EcEnv.Op.lookup f2.pl_desc env |> snd in
- let f2 = match f2.op_kind with
- | OB_oper (Some (OP_Plain f)) -> f
- | _ -> failwith "Invalid operator type" in
- let fc2 = circuit_of_form env f2 in
-
- (* let fc = List.take 4 fc in (* FIXME: this needs to be removed *) *)
- (* let () = Format.eprintf "%a" (HL.pp_node hlenv) (List.hd fc) in *)
- (* DEBUG PRINTS FOR OP CIRCUIT *)
- let namer = fun id -> 
- List.find_opt (fun idn -> tag idn = id) (List.map ident_of_cinput fc.inps) 
- |> Option.map name |> Option.default (string_of_int id) in
- let () = Format.eprintf "Out len: %d @." (size_of_circ fc.circ) in
- (* let () = HL.inputs_of_reg fc.circ |> Set.to_list |> List.iter (fun x -> Format.eprintf "%s %d@." (fst x |> namer) (snd x)) in *)
- (* let () = Format.eprintf "%a@." (fun fmt -> HL.pp_deps ~namer fmt) (HL.deps fc.circ |> Array.to_list) in *)
- let () = Format.eprintf "Args for circuit: "; 
- List.iter (fun inp -> Format.eprintf "%s" (cinput_to_string inp)) fc.inps;
- Format.eprintf "@." in
- Format.eprintf "Circuits: %s@." (if circ_equiv fc fc2 None then "Equiv" else "Not equiv")

src/ecCircuits.mli

@@ -1,5 +1,4 @@
 (* -------------------------------------------------------------------- *)
-open EcParsetree
 open EcIdent
 open EcSymbols
 open EcAst
@@ -38,5 +37,4 @@ 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/ecCommands.ml

@@ -706,12 +706,6 @@ and process_dump scope (source, tc) =
  scope
 
 (* -------------------------------------------------------------------- *)
-and process_bdep (scope : EcScope.scope) ((p, f, n, m, vs, pcond) : pgamepath * psymbol * int * int * (string list) * psymbol) =
- let env = EcScope.env scope in
- let p = EcTyping.trans_gamepath env p in
- assert false
- (* EcPhlBDep.bdep_xpath (EcScope.env scope) p f n m vs pcond *)
-
 and process_bind_bitstring (scope : EcScope.scope) (bs : pbind_bitstring) =
  EcScope.Circuit.add_bitstring scope bs
 
@@ -724,10 +718,6 @@ and process_bind_qfabvop (scope : EcScope.scope) (bop : pbind_qfabvop) =
 and process_bind_circuit (scope : EcScope.scope) (pc : pbind_circuit) =
  EcScope.Circuit.add_circuit scope pc
 
-and process_test (scope: EcScope.scope) (q: pqsymbol) (q2: pqsymbol) =
- let env = EcScope.env scope in
- EcCircuits.process_op env q q2
-
 (* -------------------------------------------------------------------- *)
 and process (ld : Loader.loader) (scope : EcScope.scope) g =
  let loc = g.pl_loc in
@@ -771,12 +761,10 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
  | Greduction red -> `Fct (fun scope -> process_reduction scope red)
  | Ghint hint -> `Fct (fun scope -> process_hint scope hint)
  | GdumpWhy3 file -> `Fct (fun scope -> process_dump_why3 scope file)
- | Gbdep (proc, f, n, m, vs, b) -> `State (fun scope -> process_bdep scope (proc, f, n, m, vs, b))
  | Gbbitstring bs -> `Fct (fun scope -> process_bind_bitstring scope bs)
  | Gbbsarray ba -> `Fct (fun scope -> process_bind_bsarray scope ba)
  | Gbcircuit oc -> `Fct (fun scope -> process_bind_circuit scope oc)
  | Gbqfabvop oc -> `Fct (fun scope -> process_bind_qfabvop scope oc)
- | Gtest (p1, p2) -> `State (fun scope -> process_test scope p1 p2)
  with
  | `Fct f -> Some (f scope)
  | `State f -> f scope; None

src/ecParser.mly

@@ -3943,12 +3943,6 @@ global_action:
 | local=is_local BIND CIRCUIT operator=qoident circuit=loc(STRING)
  { Gbcircuit { local; operator; circuit; } }
 
-| BDEP p=loc(fident) f=oident n=uint m=uint LBRACKET vl=plist0(STRING, SEMICOLON) RBRACKET pc=oident
- { Gbdep (p, f, (BI.to_int n), (BI.to_int m), vl, pc) }
-
-| BIND BDEP t1=qoident t2=qoident
- { Gtest (t1, t2) }
-
 | PRAGMA x=pragma { Gpragma x }
 | PRAGMA PLUS x=pragma { Goption (x, `Bool true ) }
 | PRAGMA MINUS x=pragma { Goption (x, `Bool false) }

src/ecParsetree.ml

@@ -1336,12 +1336,10 @@ type global_action =
  | Gpragma of psymbol
  | Goption of (psymbol * [`Bool of bool | `Int of int])
  | GdumpWhy3 of string
- | Gbdep of pgamepath * psymbol * int * int * (string list) * psymbol
  | Gbbitstring of pbind_bitstring
  | Gbbsarray of pbind_array
  | Gbcircuit of pbind_circuit
  | Gbqfabvop of pbind_qfabvop
- | Gtest of pqsymbol * pqsymbol
 
 type global = {
  gl_action : global_action located;

src/ecTheoryReplay.ml

@@ -312,6 +312,41 @@ let rename ove subst (kind, name) =
 
  with Not_found -> (subst, name)
 
+(* -------------------------------------------------------------------- *)
+exception InvInstPath
+
+(* -------------------------------------------------------------------- *)
+let forpath ~(opath : EcPath.path) ~(npath : EcPath.path) ~(ops : _ Mp.t) (p : EcPath.path) =
+ match EcPath.remprefix ~prefix:opath ~path:p |> omap List.rev with
+ | None | Some [] -> None
+ | Some (x::px) ->
+ let q = EcPath.fromqsymbol (List.rev px, x) in
+
+ match Mp.find_opt q ops with
+ | None ->
+ Some (EcPath.pappend npath q)
+ | Some (op, alias) ->
+ match alias with
+ | true -> Some (EcPath.pappend npath q)
+ | false ->
+ match op.EcDecl.op_kind with
+ | OB_pred _
+ | OB_nott _ -> assert false
+ | OB_oper None -> None
+ | OB_oper (Some (OP_Constr _))
+ | OB_oper (Some (OP_Record _))
+ | OB_oper (Some (OP_Proj _))
+ | OB_oper (Some (OP_Fix _))
+ | OB_oper (Some (OP_TC )) ->
+ Some (EcPath.pappend npath q)
+ | OB_oper (Some (OP_Plain f)) ->
+ match f.f_node with
+ | Fop (r, _) -> Some r
+ | _ -> raise InvInstPath
+
+let forpath ~opath ~npath ~ops p =
+ odfl p (forpath ~opath ~npath ~ops p)
+
 (* -------------------------------------------------------------------- *)
 let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd) =
  let scenv = ove.ovre_hooks.henv scope in
@@ -872,39 +907,7 @@ and replay_instance
 =
  let opath = ove.ovre_opath in
  let npath = ove.ovre_npath in
-
- let module E = struct exception InvInstPath end in
-
- let forpath (p : EcPath.path) =
- match EcPath.remprefix ~prefix:opath ~path:p |> omap List.rev with
- | None | Some [] -> None
- | Some (x::px) ->
- let q = EcPath.fromqsymbol (List.rev px, x) in
-
- match Mp.find_opt q ops with
- | None ->
- Some (EcPath.pappend npath q)
- | Some (op, alias) ->
- match alias with
- | true -> Some (EcPath.pappend npath q)
- | false ->
- match op.EcDecl.op_kind with
- | OB_pred _
- | OB_nott _ -> assert false
- | OB_oper None -> None
- | OB_oper (Some (OP_Constr _))
- | OB_oper (Some (OP_Record _))
- | OB_oper (Some (OP_Proj _))
- | OB_oper (Some (OP_Fix _))
- | OB_oper (Some (OP_TC )) ->
- Some (EcPath.pappend npath q)
- | OB_oper (Some (OP_Plain f)) ->
- match f.f_node with
- | Fop (r, _) -> Some r
- | _ -> raise E.InvInstPath
- in
-
- let forpath p = odfl p (forpath p) in
+ let forpath = forpath ~npath ~opath ~ops in
 
  try
  let (typ, ty) = EcSubst.subst_genty subst (typ, ty) in
@@ -940,7 +943,88 @@ and replay_instance
  let scope = ove.ovre_hooks.hadd_item scope import (Th_instance ((typ, ty), tc, lc)) in
  (subst, ops, proofs, scope)
 
- with E.InvInstPath ->
+ with InvInstPath ->
+ (subst, ops, proofs, scope)
+
+(* -------------------------------------------------------------------- *)
+and replay_bitstring (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bs, lc) =
+ let opath = ove.ovre_opath in
+ let npath = ove.ovre_npath in
+ let forpath = forpath ~npath ~opath ~ops in
+
+ try
+ let to_ = forpath bs.to_ in
+ let from_ = forpath bs.from_ in
+ let type_ = bs.type_ in (* FIXME *)
+ let theory = bs.theory in (* FIXME *)
+ let size = bs.size in
+
+ let bs : bitstring = { to_; from_; type_; theory; size; } in
+ let scope = ove.ovre_hooks.hadd_item scope import (Th_bitstring (bs, lc)) in
+
+ (subst, ops, proofs, scope)
+
+ with InvInstPath ->
+ (subst, ops, proofs, scope)
+
+(* -------------------------------------------------------------------- *)
+and replay_bsarray (ove : _ ovrenv) (subst, ops, proofs, scope) (import, ba, lc) =
+ let opath = ove.ovre_opath in
+ let npath = ove.ovre_npath in
+ let forpath = forpath ~npath ~opath ~ops in
+
+ try
+ let get = forpath ba.get in
+ let set = forpath ba.set in
+ let tolist = forpath ba.tolist in
+ let type_ = ba.type_ in (* FIXME*)
+ let size = ba.size in
+
+ let ba : bsarray = { get; set; tolist; type_; size; } in
+ let scope = ove.ovre_hooks.hadd_item scope import (Th_bsarray (ba, lc)) in
+
+ (subst, ops, proofs, scope)
+
+ with InvInstPath ->
+ (subst, ops, proofs, scope)
+
+(* -------------------------------------------------------------------- *)
+and replay_qfabvop (ove : _ ovrenv) (subst, ops, proofs, scope) (import, op, lc) =
+ let opath = ove.ovre_opath in
+ let npath = ove.ovre_npath in
+ let forpath = forpath ~npath ~opath ~ops in
+
+ try
+ let kind = op.kind in
+ let operator = forpath op.operator in
+ let type_ = op.type_ in (* FIXME *)
+ let theory = op.theory in (* FIXME *)
+
+ let op : qfabvop = { kind; operator; type_; theory; } in
+ let scope = ove.ovre_hooks.hadd_item scope import (Th_qfabvop (op, lc)) in
+
+ (subst, ops, proofs, scope)
+
+ with InvInstPath ->
+ (subst, ops, proofs, scope)
+
+(* -------------------------------------------------------------------- *)
+and replay_circuit (ove : _ ovrenv) (subst, ops, proofs, scope) (import, cr, lc) =
+ let opath = ove.ovre_opath in
+ let npath = ove.ovre_npath in
+ let forpath = forpath ~npath ~opath ~ops in
+
+ try
+ let name = cr.name in
+ let circuit = cr.circuit in
+ let operator = forpath cr.operator in
+
+ let cr : circuit = { name; circuit; operator; } in
+ let scope = ove.ovre_hooks.hadd_item scope import (Th_circuit (cr, lc)) in
+
+ (subst, ops, proofs, scope)
+
+ with InvInstPath ->
  (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -988,6 +1072,18 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) item =
  | Th_instance ((typ, ty), tc, lc) ->
  replay_instance ove (subst, ops, proofs, scope) (item.ti_import, (typ, ty), tc, lc)
 
+ | Th_bitstring (bs, lc) ->
+ replay_bitstring ove (subst, ops, proofs, scope) (item.ti_import, bs, lc)
+
+ | Th_bsarray (ba, lc) ->
+ replay_bsarray ove (subst, ops, proofs, scope) (item.ti_import, ba, lc)
+
+ | Th_qfabvop (op, lc) ->
+ replay_qfabvop ove (subst, ops, proofs, scope) (item.ti_import, op, lc)
+
+ | Th_circuit (cr, lc) ->
+ replay_circuit ove (subst, ops, proofs, scope) (item.ti_import, cr, lc)
+
  | Th_theory (ox, cth) -> begin
  let thmode = cth.cth_mode in
  let (subst, x) = rename ove subst (`Theory, ox) in