diff --git a/dune-project b/dune-project
index 38cfbe826c..6bb46899b3 100644
--- a/dune-project
+++ b/dune-project
@@ -1,5 +1,5 @@
-(lang dune 3.6)
-(using menhir 2.0)
+(lang dune 3.13)
+(using menhir 3.0)
 (using dune_site 0.1)
 
 (wrapped_executables false)
diff --git a/easycrypt.opam b/easycrypt.opam
index 04889b6e92..2d010589c9 100644
--- a/easycrypt.opam
+++ b/easycrypt.opam
@@ -6,7 +6,7 @@ depends: [
   "camlp-streams" {>= "5"}
   "camlzip"
   "cmdliner"
-  "dune" {>= "3.6" & >= "3.6"}
+  "dune" {>= "3.13" & >= "3.6"}
   "dune-build-info"
   "dune-site"
   "hex"
diff --git a/libs/lospecs/ast.ml b/libs/lospecs/ast.ml
index 06baff6f7d..50a1fe537b 100644
--- a/libs/lospecs/ast.ml
+++ b/libs/lospecs/ast.ml
@@ -16,7 +16,10 @@ end = struct
   let id ((_, i) : ident) : int = i
 end
 
-module IdentMap = Map.Make(struct type t = Ident.ident let compare a b = (Ident.id a) - (Ident.id b) end) 
+module IdentMap = Map.Make(struct
+  type t = Ident.ident
+  let compare a b = (Ident.id a) - (Ident.id b)
+end) 
 
 (* -------------------------------------------------------------------- *)
 type ident = Ident.ident [@@deriving yojson]
diff --git a/libs/lospecs/circuit_avx2.mli b/libs/lospecs/circuit_avx2.mli
deleted file mode 100644
index 06bb8d1d73..0000000000
--- a/libs/lospecs/circuit_avx2.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-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
diff --git a/libs/lospecs/circuit_spec.ml b/libs/lospecs/circuit_spec.ml
index 45f9bc8c9b..30182bdacf 100644
--- a/libs/lospecs/circuit_spec.ml
+++ b/libs/lospecs/circuit_spec.ml
@@ -6,6 +6,13 @@ open Aig
 let rec log2 n =
   if n <= 1 then 0 else 1 + log2 (n asr 1)
   
+
+(* ==================================================================== *)
+let load_from_file ~(filename : string) =
+  let specs = File.with_file_in filename (Io.parse filename) in
+  let specs = Typing.tt_program Typing.Env.empty specs in
+  specs
+
 (* ==================================================================== *)
 module Env : sig
   type env
@@ -60,7 +67,7 @@ end
 type env = Env.env
 
 (* ==================================================================== *)
-let circuit_of_spec (rs : reg list) (p : adef) : reg =
+let circuit_of_specification (rs : reg list) (p : adef) : reg =
   assert (List.length rs = List.length p.arguments);
   assert (List.for_all2 (fun r (_, `W n) -> List.length r = n) rs p.arguments);
 
diff --git a/libs/lospecs/circuit_spec.mli b/libs/lospecs/circuit_spec.mli
index 11bba0a87a..89a558c677 100644
--- a/libs/lospecs/circuit_spec.mli
+++ b/libs/lospecs/circuit_spec.mli
@@ -1,19 +1,3 @@
-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
+(* ==================================================================== *)
+val circuit_of_specification : Aig.reg list -> Ast.adef -> Aig.reg
+val load_from_file : filename:string -> (string * Ast.adef) list
diff --git a/libs/lospecs/dune b/libs/lospecs/dune
index 4e344c9f46..ca22167921 100644
--- a/libs/lospecs/dune
+++ b/libs/lospecs/dune
@@ -3,37 +3,18 @@
  (sites easycrypt))
 
 (library
- (name lospecs)
- (public_name easycrypt.lospecs)
- (flags
-  (:standard -open Batteries))
- (modules :standard config \ lospecs_test circuit_test)
- (preprocess
-  (pps ppx_deriving_yojson))
- (foreign_stubs
-  (language cxx)
-  (flags :standard -std=c++17 -mavx -mavx2)
-  (names avx2_runtime))
- (libraries batteries dune-site menhirLib zarith ppx_deriving_yojson.runtime bitwuzla))
-
-(executable
- (name lospecs_test)
- (flags
-  (:standard -open Batteries))
- (modules lospecs_test)
- (promote (until-clean))
- (libraries batteries cmdliner lospecs))
-
-(executable
- (name circuit_test)
- (flags
-  (:standard -open Batteries))
- (modules circuit_test)
- (promote (until-clean))
- (libraries batteries hex iter lospecs progress))
+  (name lospecs)
+  (public_name easycrypt.lospecs)
+  (flags
+    (:standard -open Batteries))
+  (modules :standard config)
+  (preprocess
+    (pps ppx_deriving_yojson))
+  (libraries batteries dune-site menhirLib zarith ppx_deriving_yojson.runtime bitwuzla))
 
 (ocamllex lexer)
 
 (menhir
- (modules parser)
- (flags --table --explain))
+  (modules parser)
+  (explain true)
+  (flags --table))
diff --git a/libs/lospecs/examples/inst_list.txt b/libs/lospecs/examples/inst_list.txt
deleted file mode 100644
index 77cb724bd3..0000000000
--- a/libs/lospecs/examples/inst_list.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-VPACKUS_16u16
-VPADD_16u16
-VPAND_256
-VPBROADCAST_16u16
-VPERMD
-VPMADDUBSW_256
-VPMULH_16u16
-VPMULHRS_16u16
-VPSRA_16u16
-VPSUB_16u16
diff --git a/libs/lospecs/examples/out.ec b/libs/lospecs/examples/out.ec
deleted file mode 100644
index f069821cc0..0000000000
--- a/libs/lospecs/examples/out.ec
+++ /dev/null
@@ -1,429 +0,0 @@
-require import AllCore IntDiv CoreMap List Distr.
-from Jasmin require import JModel.
-
-abbrev pc_permidx_s = W256.of_int 25108406943008224694375472445797499139581786974313141764103.
-
-
-abbrev pc_shift2_s = W16.of_int 4097.
-
-
-abbrev pc_mask_s = W16.of_int 15.
-
-
-abbrev pc_shift1_s = W16.of_int 512.
-
-
-abbrev jvx16 = W256.of_int 35618413472725370924601624884262448072237272005411583588485930205470676438719.
-
-
-abbrev jqx16 = W256.of_int 5881923629679188442283784376194736327817742869488325897419002016668082834689.
-
-
-module M = {
-  proc _poly_compress_1 (rp_0:W256.t, rp_1:W256.t, rp_2:W256.t, rp_3:W256.t,
-                         a_0:W256.t, a_1:W256.t, a_2:W256.t, a_3:W256.t,
-                         a_4:W256.t, a_5:W256.t, a_6:W256.t, a_7:W256.t,
-                         a_8:W256.t, a_9:W256.t, a_10:W256.t, a_11:W256.t,
-                         a_12:W256.t, a_13:W256.t, a_14:W256.t, a_15:W256.t) : 
-  W256.t * W256.t * W256.t * W256.t * W256.t * W256.t * W256.t * W256.t *
-  W256.t * W256.t * W256.t * W256.t * W256.t * W256.t * W256.t * W256.t *
-  W256.t * W256.t * W256.t * W256.t = {
-    
-    var qx16:W256.t;
-    var r:W256.t;
-    var r_0:W256.t;
-    var t:W256.t;
-    var t_0:W256.t;
-    var r_1:W256.t;
-    var a_0_0:W256.t;
-    var r_2:W256.t;
-    var r_3:W256.t;
-    var t_1:W256.t;
-    var t_2:W256.t;
-    var r_4:W256.t;
-    var a_1_0:W256.t;
-    var r_5:W256.t;
-    var r_6:W256.t;
-    var t_3:W256.t;
-    var t_4:W256.t;
-    var r_7:W256.t;
-    var a_2_0:W256.t;
-    var r_8:W256.t;
-    var r_9:W256.t;
-    var t_5:W256.t;
-    var t_6:W256.t;
-    var r_10:W256.t;
-    var a_3_0:W256.t;
-    var r_11:W256.t;
-    var r_12:W256.t;
-    var t_7:W256.t;
-    var t_8:W256.t;
-    var r_13:W256.t;
-    var a_4_0:W256.t;
-    var r_14:W256.t;
-    var r_15:W256.t;
-    var t_9:W256.t;
-    var t_10:W256.t;
-    var r_16:W256.t;
-    var a_5_0:W256.t;
-    var r_17:W256.t;
-    var r_18:W256.t;
-    var t_11:W256.t;
-    var t_12:W256.t;
-    var r_19:W256.t;
-    var a_6_0:W256.t;
-    var r_20:W256.t;
-    var r_21:W256.t;
-    var t_13:W256.t;
-    var t_14:W256.t;
-    var r_22:W256.t;
-    var a_7_0:W256.t;
-    var r_23:W256.t;
-    var r_24:W256.t;
-    var t_15:W256.t;
-    var t_16:W256.t;
-    var r_25:W256.t;
-    var a_8_0:W256.t;
-    var r_26:W256.t;
-    var r_27:W256.t;
-    var t_17:W256.t;
-    var t_18:W256.t;
-    var r_28:W256.t;
-    var a_9_0:W256.t;
-    var r_29:W256.t;
-    var r_30:W256.t;
-    var t_19:W256.t;
-    var t_20:W256.t;
-    var r_31:W256.t;
-    var a_10_0:W256.t;
-    var r_32:W256.t;
-    var r_33:W256.t;
-    var t_21:W256.t;
-    var t_22:W256.t;
-    var r_34:W256.t;
-    var a_11_0:W256.t;
-    var r_35:W256.t;
-    var r_36:W256.t;
-    var t_23:W256.t;
-    var t_24:W256.t;
-    var r_37:W256.t;
-    var a_12_0:W256.t;
-    var r_38:W256.t;
-    var r_39:W256.t;
-    var t_25:W256.t;
-    var t_26:W256.t;
-    var r_40:W256.t;
-    var a_13_0:W256.t;
-    var r_41:W256.t;
-    var r_42:W256.t;
-    var t_27:W256.t;
-    var t_28:W256.t;
-    var r_43:W256.t;
-    var a_14_0:W256.t;
-    var r_44:W256.t;
-    var r_45:W256.t;
-    var t_29:W256.t;
-    var t_30:W256.t;
-    var r_46:W256.t;
-    var a_15_0:W256.t;
-    var x16p:W256.t;
-    var v:W256.t;
-    var shift1:W256.t;
-    var mask:W256.t;
-    var shift2:W256.t;
-    var permidx:W256.t;
-    var f0:W256.t;
-    var f1:W256.t;
-    var f2:W256.t;
-    var f3:W256.t;
-    var f0_0:W256.t;
-    var f1_0:W256.t;
-    var f2_0:W256.t;
-    var f3_0:W256.t;
-    var f0_1:W256.t;
-    var f1_1:W256.t;
-    var f2_1:W256.t;
-    var f3_1:W256.t;
-    var f0_2:W256.t;
-    var f1_2:W256.t;
-    var f2_2:W256.t;
-    var f3_2:W256.t;
-    var f0_3:W256.t;
-    var f2_3:W256.t;
-    var f0_4:W256.t;
-    var f2_4:W256.t;
-    var f0_5:W256.t;
-    var f0_6:W256.t;
-    var rp_0_0:W256.t;
-    var f0_7:W256.t;
-    var f1_3:W256.t;
-    var f2_5:W256.t;
-    var f3_3:W256.t;
-    var f0_8:W256.t;
-    var f1_4:W256.t;
-    var f2_6:W256.t;
-    var f3_4:W256.t;
-    var f0_9:W256.t;
-    var f1_5:W256.t;
-    var f2_7:W256.t;
-    var f3_5:W256.t;
-    var f0_10:W256.t;
-    var f1_6:W256.t;
-    var f2_8:W256.t;
-    var f3_6:W256.t;
-    var f0_11:W256.t;
-    var f2_9:W256.t;
-    var f0_12:W256.t;
-    var f2_10:W256.t;
-    var f0_13:W256.t;
-    var f0_14:W256.t;
-    var rp_1_0:W256.t;
-    var f0_15:W256.t;
-    var f1_7:W256.t;
-    var f2_11:W256.t;
-    var f3_7:W256.t;
-    var f0_16:W256.t;
-    var f1_8:W256.t;
-    var f2_12:W256.t;
-    var f3_8:W256.t;
-    var f0_17:W256.t;
-    var f1_9:W256.t;
-    var f2_13:W256.t;
-    var f3_9:W256.t;
-    var f0_18:W256.t;
-    var f1_10:W256.t;
-    var f2_14:W256.t;
-    var f3_10:W256.t;
-    var f0_19:W256.t;
-    var f2_15:W256.t;
-    var f0_20:W256.t;
-    var f2_16:W256.t;
-    var f0_21:W256.t;
-    var f0_22:W256.t;
-    var rp_2_0:W256.t;
-    var f0_23:W256.t;
-    var f1_11:W256.t;
-    var f2_17:W256.t;
-    var f3_11:W256.t;
-    var f0_24:W256.t;
-    var f1_12:W256.t;
-    var f2_18:W256.t;
-    var f3_12:W256.t;
-    var f0_25:W256.t;
-    var f1_13:W256.t;
-    var f2_19:W256.t;
-    var f3_13:W256.t;
-    var f0_26:W256.t;
-    var f1_14:W256.t;
-    var f2_20:W256.t;
-    var f3_14:W256.t;
-    var f0_27:W256.t;
-    var f2_21:W256.t;
-    var f0_28:W256.t;
-    var f2_22:W256.t;
-    var f0_29:W256.t;
-    var f0_30:W256.t;
-    var rp_3_0:W256.t;
-    
-    qx16 <- jqx16;
-    r <- a_0;
-    r_0 <- VPSUB_16u16 r qx16;
-    t <- VPSRA_16u16 r_0 (W8.of_int 15);
-    t_0 <- VPAND_256 t qx16;
-    r_1 <- VPADD_16u16 t_0 r_0;
-    a_0_0 <- r_1;
-    r_2 <- a_1;
-    r_3 <- VPSUB_16u16 r_2 qx16;
-    t_1 <- VPSRA_16u16 r_3 (W8.of_int 15);
-    t_2 <- VPAND_256 t_1 qx16;
-    r_4 <- VPADD_16u16 t_2 r_3;
-    a_1_0 <- r_4;
-    r_5 <- a_2;
-    r_6 <- VPSUB_16u16 r_5 qx16;
-    t_3 <- VPSRA_16u16 r_6 (W8.of_int 15);
-    t_4 <- VPAND_256 t_3 qx16;
-    r_7 <- VPADD_16u16 t_4 r_6;
-    a_2_0 <- r_7;
-    r_8 <- a_3;
-    r_9 <- VPSUB_16u16 r_8 qx16;
-    t_5 <- VPSRA_16u16 r_9 (W8.of_int 15);
-    t_6 <- VPAND_256 t_5 qx16;
-    r_10 <- VPADD_16u16 t_6 r_9;
-    a_3_0 <- r_10;
-    r_11 <- a_4;
-    r_12 <- VPSUB_16u16 r_11 qx16;
-    t_7 <- VPSRA_16u16 r_12 (W8.of_int 15);
-    t_8 <- VPAND_256 t_7 qx16;
-    r_13 <- VPADD_16u16 t_8 r_12;
-    a_4_0 <- r_13;
-    r_14 <- a_5;
-    r_15 <- VPSUB_16u16 r_14 qx16;
-    t_9 <- VPSRA_16u16 r_15 (W8.of_int 15);
-    t_10 <- VPAND_256 t_9 qx16;
-    r_16 <- VPADD_16u16 t_10 r_15;
-    a_5_0 <- r_16;
-    r_17 <- a_6;
-    r_18 <- VPSUB_16u16 r_17 qx16;
-    t_11 <- VPSRA_16u16 r_18 (W8.of_int 15);
-    t_12 <- VPAND_256 t_11 qx16;
-    r_19 <- VPADD_16u16 t_12 r_18;
-    a_6_0 <- r_19;
-    r_20 <- a_7;
-    r_21 <- VPSUB_16u16 r_20 qx16;
-    t_13 <- VPSRA_16u16 r_21 (W8.of_int 15);
-    t_14 <- VPAND_256 t_13 qx16;
-    r_22 <- VPADD_16u16 t_14 r_21;
-    a_7_0 <- r_22;
-    r_23 <- a_8;
-    r_24 <- VPSUB_16u16 r_23 qx16;
-    t_15 <- VPSRA_16u16 r_24 (W8.of_int 15);
-    t_16 <- VPAND_256 t_15 qx16;
-    r_25 <- VPADD_16u16 t_16 r_24;
-    a_8_0 <- r_25;
-    r_26 <- a_9;
-    r_27 <- VPSUB_16u16 r_26 qx16;
-    t_17 <- VPSRA_16u16 r_27 (W8.of_int 15);
-    t_18 <- VPAND_256 t_17 qx16;
-    r_28 <- VPADD_16u16 t_18 r_27;
-    a_9_0 <- r_28;
-    r_29 <- a_10;
-    r_30 <- VPSUB_16u16 r_29 qx16;
-    t_19 <- VPSRA_16u16 r_30 (W8.of_int 15);
-    t_20 <- VPAND_256 t_19 qx16;
-    r_31 <- VPADD_16u16 t_20 r_30;
-    a_10_0 <- r_31;
-    r_32 <- a_11;
-    r_33 <- VPSUB_16u16 r_32 qx16;
-    t_21 <- VPSRA_16u16 r_33 (W8.of_int 15);
-    t_22 <- VPAND_256 t_21 qx16;
-    r_34 <- VPADD_16u16 t_22 r_33;
-    a_11_0 <- r_34;
-    r_35 <- a_12;
-    r_36 <- VPSUB_16u16 r_35 qx16;
-    t_23 <- VPSRA_16u16 r_36 (W8.of_int 15);
-    t_24 <- VPAND_256 t_23 qx16;
-    r_37 <- VPADD_16u16 t_24 r_36;
-    a_12_0 <- r_37;
-    r_38 <- a_13;
-    r_39 <- VPSUB_16u16 r_38 qx16;
-    t_25 <- VPSRA_16u16 r_39 (W8.of_int 15);
-    t_26 <- VPAND_256 t_25 qx16;
-    r_40 <- VPADD_16u16 t_26 r_39;
-    a_13_0 <- r_40;
-    r_41 <- a_14;
-    r_42 <- VPSUB_16u16 r_41 qx16;
-    t_27 <- VPSRA_16u16 r_42 (W8.of_int 15);
-    t_28 <- VPAND_256 t_27 qx16;
-    r_43 <- VPADD_16u16 t_28 r_42;
-    a_14_0 <- r_43;
-    r_44 <- a_15;
-    r_45 <- VPSUB_16u16 r_44 qx16;
-    t_29 <- VPSRA_16u16 r_45 (W8.of_int 15);
-    t_30 <- VPAND_256 t_29 qx16;
-    r_46 <- VPADD_16u16 t_30 r_45;
-    a_15_0 <- r_46;
-    x16p <- jvx16;
-    v <- x16p;
-    shift1 <- VPBROADCAST_16u16 pc_shift1_s;
-    mask <- VPBROADCAST_16u16 pc_mask_s;
-    shift2 <- VPBROADCAST_16u16 pc_shift2_s;
-    permidx <- pc_permidx_s;
-    f0 <- a_0_0;
-    f1 <- a_1_0;
-    f2 <- a_2_0;
-    f3 <- a_3_0;
-    f0_0 <- VPMULH_16u16 f0 v;
-    f1_0 <- VPMULH_16u16 f1 v;
-    f2_0 <- VPMULH_16u16 f2 v;
-    f3_0 <- VPMULH_16u16 f3 v;
-    f0_1 <- VPMULHRS_16u16 f0_0 shift1;
-    f1_1 <- VPMULHRS_16u16 f1_0 shift1;
-    f2_1 <- VPMULHRS_16u16 f2_0 shift1;
-    f3_1 <- VPMULHRS_16u16 f3_0 shift1;
-    f0_2 <- VPAND_256 f0_1 mask;
-    f1_2 <- VPAND_256 f1_1 mask;
-    f2_2 <- VPAND_256 f2_1 mask;
-    f3_2 <- VPAND_256 f3_1 mask;
-    f0_3 <- VPACKUS_16u16 f0_2 f1_2;
-    f2_3 <- VPACKUS_16u16 f2_2 f3_2;
-    f0_4 <- VPMADDUBSW_256 f0_3 shift2;
-    f2_4 <- VPMADDUBSW_256 f2_3 shift2;
-    f0_5 <- VPACKUS_16u16 f0_4 f2_4;
-    f0_6 <- VPERMD permidx f0_5;
-    rp_0_0 <- f0_6;
-    f0_7 <- a_4_0;
-    f1_3 <- a_5_0;
-    f2_5 <- a_6_0;
-    f3_3 <- a_7_0;
-    f0_8 <- VPMULH_16u16 f0_7 v;
-    f1_4 <- VPMULH_16u16 f1_3 v;
-    f2_6 <- VPMULH_16u16 f2_5 v;
-    f3_4 <- VPMULH_16u16 f3_3 v;
-    f0_9 <- VPMULHRS_16u16 f0_8 shift1;
-    f1_5 <- VPMULHRS_16u16 f1_4 shift1;
-    f2_7 <- VPMULHRS_16u16 f2_6 shift1;
-    f3_5 <- VPMULHRS_16u16 f3_4 shift1;
-    f0_10 <- VPAND_256 f0_9 mask;
-    f1_6 <- VPAND_256 f1_5 mask;
-    f2_8 <- VPAND_256 f2_7 mask;
-    f3_6 <- VPAND_256 f3_5 mask;
-    f0_11 <- VPACKUS_16u16 f0_10 f1_6;
-    f2_9 <- VPACKUS_16u16 f2_8 f3_6;
-    f0_12 <- VPMADDUBSW_256 f0_11 shift2;
-    f2_10 <- VPMADDUBSW_256 f2_9 shift2;
-    f0_13 <- VPACKUS_16u16 f0_12 f2_10;
-    f0_14 <- VPERMD permidx f0_13;
-    rp_1_0 <- f0_14;
-    f0_15 <- a_8_0;
-    f1_7 <- a_9_0;
-    f2_11 <- a_10_0;
-    f3_7 <- a_11_0;
-    f0_16 <- VPMULH_16u16 f0_15 v;
-    f1_8 <- VPMULH_16u16 f1_7 v;
-    f2_12 <- VPMULH_16u16 f2_11 v;
-    f3_8 <- VPMULH_16u16 f3_7 v;
-    f0_17 <- VPMULHRS_16u16 f0_16 shift1;
-    f1_9 <- VPMULHRS_16u16 f1_8 shift1;
-    f2_13 <- VPMULHRS_16u16 f2_12 shift1;
-    f3_9 <- VPMULHRS_16u16 f3_8 shift1;
-    f0_18 <- VPAND_256 f0_17 mask;
-    f1_10 <- VPAND_256 f1_9 mask;
-    f2_14 <- VPAND_256 f2_13 mask;
-    f3_10 <- VPAND_256 f3_9 mask;
-    f0_19 <- VPACKUS_16u16 f0_18 f1_10;
-    f2_15 <- VPACKUS_16u16 f2_14 f3_10;
-    f0_20 <- VPMADDUBSW_256 f0_19 shift2;
-    f2_16 <- VPMADDUBSW_256 f2_15 shift2;
-    f0_21 <- VPACKUS_16u16 f0_20 f2_16;
-    f0_22 <- VPERMD permidx f0_21;
-    rp_2_0 <- f0_22;
-    f0_23 <- a_12_0;
-    f1_11 <- a_13_0;
-    f2_17 <- a_14_0;
-    f3_11 <- a_15_0;
-    f0_24 <- VPMULH_16u16 f0_23 v;
-    f1_12 <- VPMULH_16u16 f1_11 v;
-    f2_18 <- VPMULH_16u16 f2_17 v;
-    f3_12 <- VPMULH_16u16 f3_11 v;
-    f0_25 <- VPMULHRS_16u16 f0_24 shift1;
-    f1_13 <- VPMULHRS_16u16 f1_12 shift1;
-    f2_19 <- VPMULHRS_16u16 f2_18 shift1;
-    f3_13 <- VPMULHRS_16u16 f3_12 shift1;
-    f0_26 <- VPAND_256 f0_25 mask;
-    f1_14 <- VPAND_256 f1_13 mask;
-    f2_20 <- VPAND_256 f2_19 mask;
-    f3_14 <- VPAND_256 f3_13 mask;
-    f0_27 <- VPACKUS_16u16 f0_26 f1_14;
-    f2_21 <- VPACKUS_16u16 f2_20 f3_14;
-    f0_28 <- VPMADDUBSW_256 f0_27 shift2;
-    f2_22 <- VPMADDUBSW_256 f2_21 shift2;
-    f0_29 <- VPACKUS_16u16 f0_28 f2_22;
-    f0_30 <- VPERMD permidx f0_29;
-    rp_3_0 <- f0_30;
-    return (rp_0_0, rp_1_0, rp_2_0, rp_3_0, a_0_0, a_1_0, a_2_0, a_3_0,
-    a_4_0, a_5_0, a_6_0, a_7_0, a_8_0, a_9_0, a_10_0, a_11_0, a_12_0, a_13_0,
-    a_14_0, a_15_0);
-  }
-}.
-
-bdep M._poly_compress_1.
diff --git a/libs/lospecs/examples/shift.ec b/libs/lospecs/examples/shift.ec
deleted file mode 100644
index 0dafa24dd4..0000000000
--- a/libs/lospecs/examples/shift.ec
+++ /dev/null
@@ -1,55 +0,0 @@
-require import AllCore IntDiv CoreMap List Distr.
-from Jasmin require import JModel_x86.
-import SLH64.
-
-
-
-abbrev SWAP_BYTES_256 = W256.of_int 1780731860627700044960722568376592179391279163832551066649583786025356815.
-
-
-abbrev SWAP_BYTES_128 = W128.of_int 5233100606242806050955395731361295.
-
-abbrev six_i = W8.of_int 40.
-
-print W8.([-]).
-
-module M = {
-  proc shift_left_i_256 (w:W256.t, i:W8.t) : W256.t = {
-
-  var h:W128.t;
-    var l:W128.t;
-    var hl:W256.t;
-  var hli:W256.t;
-    var hli2:W256.t;
-    var hl64i:W256.t;
-    var hl64il:W256.t;
-  var l64ir:W128.t;
-  var aux:W128.t;
-    var h2:W128.t;
-  var six_i:W8.t;
-    var mi:W8.t;
-
-    mi <- -i;
-    six_i <- (W8.of_int 64) + mi;
-  hli <- VPSLL_4u64 w i;
-    hl64i <- VPSRL_4u64 w six_i;
-    hl64il <- VPSLLDQ_256 hl64i (W8.of_int 64);
-  hli2 <- VPXOR_256 hli hl64il;
-    aux <- truncateu128 hl64i;
-    l64ir <- VPSRLDQ_128 aux (W8.of_int 64);
-    h <- VEXTRACTI128 hli2 (W8.of_int 1);
-    h2 <- VPXOR_128 h l64ir;
-    l <- truncateu128 hli2;
-    hl <- concat_2u128 h2 l;
-    return hl;
-  }
-}.
-
-print VPXOR_256.
-
-print truncateu128.
-
-op shift_left_i (w: W256.t, i: W8.t) : W256.t =
-  w `<<` i.
-
-bdep M.shift_left_i_256 shift_left_i 0 0 ["hl"] 16.
diff --git a/libs/lospecs/lospecs_test.ml b/libs/lospecs/lospecs_test.ml
deleted file mode 100644
index 90a7a0c2f9..0000000000
--- a/libs/lospecs/lospecs_test.ml
+++ /dev/null
@@ -1,80 +0,0 @@
-(* -------------------------------------------------------------------- *)
-open Lospecs
-
-
-(* -------------------------------------------------------------------- *)
-type options = {
-  pp_pst : bool;
-  pp_ast : bool;
-  input  : string;
-}
-
-(* -------------------------------------------------------------------- *)
-let entry (options : options) =
-  try
-    let prog = File.with_file_in options.input (Io.parse options.input) in
-
-    if options.pp_pst then begin
-      Format.eprintf "%a@."
-        (Yojson.Safe.pretty_print ~std:true)
-        (Ptree.pprogram_to_yojson prog)
-    end;
-  
-    let ast = Typing.tt_program Typing.Env.empty prog in
-
-    if options.pp_ast then begin
-      List.iter (fun (name, def) ->
-        Format.eprintf "%s:@.%a@."
-        name
-          (Yojson.Safe.pretty_print ~std:true)
-          (Ast.adef_to_yojson def)
-      ) ast
-    end;
-
-    (* let _dep = List.map Bitdep.bd_adef (List.map snd ast) in *)
-
-    ()
-
-  with
-  | Typing.TypingError (range, msg) ->
-      Format.eprintf "%a: %s@." Ptree.Lc.pp_range range msg;
-      Format.eprintf "@.";
-      Io.print_source_for_range Format.err_formatter range options.input;
-      exit 1
-  | Ptree.ParseError range ->
-      Format.eprintf "%a: %s@." Ptree.Lc.pp_range range "parse error";
-      Format.eprintf "@.";
-      Io.print_source_for_range Format.err_formatter range options.input;
-      exit 1
-  | Not_found ->
-      Format.eprintf "Something is missing"
-
-(* -------------------------------------------------------------------- *)
-let main () : unit =
-  let open Cmdliner in
-
-  let cmd =
-    let mk (pp_pst : bool) (pp_ast : bool) (input : string) =
-      entry { pp_pst; pp_ast; input; }
-    in
-
-    let print_pst =
-      let doc = "Print the parse tree" in
-      Arg.(value & flag & info ["print-pst"] ~doc) in
-
-    let print_ast =
-      let doc = "Print the abstract syntax tree" in
-      Arg.(value & flag & info ["print-ast"] ~doc) in
-
-    let input =
-      let doc = "The specification file" in
-      Arg.(required & pos 0 (some string) None & info [] ~docv:"SPEC" ~doc) in
-
-    let info = Cmd.info "lospec" in
-    Cmd.v info Term.(const mk $ print_pst $ print_ast $ input)
-  in
-
-  exit (Cmd.eval cmd)
-
-(* -------------------------------------------------------------------- *)
-let () = main ()
diff --git a/libs/lospecs/avx2.ml b/libs/lospecs/tests/avx2.ml
similarity index 100%
rename from libs/lospecs/avx2.ml
rename to libs/lospecs/tests/avx2.ml
diff --git a/libs/lospecs/avx2.mli b/libs/lospecs/tests/avx2.mli
similarity index 100%
rename from libs/lospecs/avx2.mli
rename to libs/lospecs/tests/avx2.mli
diff --git a/libs/lospecs/avx2_runtime.cpp b/libs/lospecs/tests/avx2_runtime.cpp
similarity index 100%
rename from libs/lospecs/avx2_runtime.cpp
rename to libs/lospecs/tests/avx2_runtime.cpp
diff --git a/libs/lospecs/avx2_runtime.h b/libs/lospecs/tests/avx2_runtime.h
similarity index 100%
rename from libs/lospecs/avx2_runtime.h
rename to libs/lospecs/tests/avx2_runtime.h
diff --git a/libs/lospecs/circuit_avx2.ml b/libs/lospecs/tests/circuit_avx2.ml
similarity index 77%
rename from libs/lospecs/circuit_avx2.ml
rename to libs/lospecs/tests/circuit_avx2.ml
index 0e591ca111..c24951911e 100644
--- a/libs/lospecs/circuit_avx2.ml
+++ b/libs/lospecs/tests/circuit_avx2.ml
@@ -1,11 +1,11 @@
 (* ==================================================================== *)
+open Lospecs
 open Aig
 
 type symbol = string
 
 (* ==================================================================== *)
 module type S = sig
-  val get_specification : symbol -> Ast.adef option
   val vpermd : reg -> reg -> reg
   val vpermq : reg -> int -> reg
   val vpbroadcast_16u16 : reg -> reg
@@ -41,9 +41,9 @@ module FromSpec () : S = struct
   (* ------------------------------------------------------------------ *)
   let specs =
     let specs = Filename.concat (List.hd Config.Sites.specs) "avx2.spec" in
-    let specs = File.with_file_in specs (Io.parse specs) in
-    let specs = Typing.tt_program Typing.Env.empty specs in
-    BatMap.of_seq (List.to_seq specs)
+    let specs = Circuit_spec.load_from_file ~filename:specs in
+    let specs = BatMap.of_seq (List.to_seq specs) in
+    specs
 
   let get_specification (name : symbol) : Ast.adef option =
     BatMap.find_opt name specs
@@ -52,167 +52,167 @@ module FromSpec () : S = struct
   let vpermd = Option.get (get_specification "VPERMD")
 
   let vpermd (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpermd
+    Circuit_spec.circuit_of_specification [r1; r2] vpermd
 
   (* ------------------------------------------------------------------ *)
   let vpermq = Option.get (get_specification "VPERMQ")
 
   let vpermq (r : reg) (i : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 i] vpermq
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 i] vpermq
 
   (* ------------------------------------------------------------------ *)
   let vpbroadcast_16u16 = Option.get (get_specification "VPBROADCAST_16u16")
 
   let vpbroadcast_16u16 (r : reg) : reg =
-    Circuit_spec.circuit_of_spec [r] vpbroadcast_16u16
+    Circuit_spec.circuit_of_specification [r] vpbroadcast_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpadd_16u16 = Option.get (get_specification "VPADD_16u16")
 
   let vpadd_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpadd_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpadd_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpadd_32u8 = Option.get (get_specification "VPADD_32u8")
 
   let vpadd_32u8 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpadd_32u8
+    Circuit_spec.circuit_of_specification [r1; r2] vpadd_32u8
 
   (* ----------------------------------------------------------------- *)
   let vpsub_16u16 = Option.get (get_specification "VPSUB_16u16")
 
   let vpsub_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpsub_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpsub_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpsub_32u8 = Option.get (get_specification "VPSUB_32u8")
 
   let vpsub_32u8 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpsub_32u8
+    Circuit_spec.circuit_of_specification [r1; r2] vpsub_32u8
 
   (* ------------------------------------------------------------------ *)
   let vpand_256 = Option.get (get_specification "VPAND_256")
 
   let vpand_256 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpand_256
+    Circuit_spec.circuit_of_specification [r1; r2] vpand_256
 
   (* ------------------------------------------------------------------ *)
   let vpmaddubsw_256 = Option.get (get_specification "VPMADDUBSW_256")
 
   let vpmaddubsw_256 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpmaddubsw_256
+    Circuit_spec.circuit_of_specification [r1; r2] vpmaddubsw_256
 
   (* ------------------------------------------------------------------ *)
   let vpmulh_16u16 = Option.get (get_specification "VPMULH_16u16")
 
   let vpmulh_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpmulh_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpmulh_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpmulhrs_16u16 = Option.get (get_specification "VPMULHRS_16u16")
 
   let vpmulhrs_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpmulhrs_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpmulhrs_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpsra_16u16 = Option.get (get_specification "VPSRA_16u16")
 
   let vpsra_16u16 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 n] vpsra_16u16
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 n] vpsra_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpsrl_16u16 = Option.get (get_specification "VPSRL_16u16")
 
   let vpsrl_16u16 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 n] vpsrl_16u16
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 n] vpsrl_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpsrl_4u64 = Option.get (get_specification "VPSRL_4u64")
 
   let vpsrl_4u64 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 n] vpsrl_4u64
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 n] vpsrl_4u64
 
   (* ------------------------------------------------------------------ *)
   let vpsll_4u64 = Option.get (get_specification "VPSLL_4u64")
 
   let vpsll_4u64 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 n] vpsll_4u64
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 n] vpsll_4u64
 
   (* ------------------------------------------------------------------ *)
   let vpslldq_256 = Option.get (get_specification "VPSLLDQ_256")
 
   let vpslldq_256 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 (8 * n)] vpslldq_256
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 (8 * n)] vpslldq_256
 
   (* ------------------------------------------------------------------ *)
   let vpsrldq_256 = Option.get (get_specification "VPSRLDQ_256")
 
   let vpsrldq_256 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 (8 * n)] vpsrldq_256
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 (8 * n)] vpsrldq_256
 
   (* ------------------------------------------------------------------ *)
   let vpslldq_128 = Option.get (get_specification "VPSLLDQ_128")
 
   let vpslldq_128 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 (8 * n)] vpslldq_128
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 (8 * n)] vpslldq_128
 
   (* ------------------------------------------------------------------ *)
   let vpsrldq_128 = Option.get (get_specification "VPSRLDQ_128")
 
   let vpsrldq_128 (r : reg) (n : int) : reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 (8 * n)] vpsrldq_128
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 (8 * n)] vpsrldq_128
 
   (* ------------------------------------------------------------------ *)
   let vpackus_16u16 = Option.get (get_specification "VPACKUS_16u16")
 
   let vpackus_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpackus_16u16  
+    Circuit_spec.circuit_of_specification [r1; r2] vpackus_16u16  
 
   (* ------------------------------------------------------------------ *)
   let vpackss_16u16 = Option.get (get_specification "VPACKSS_16u16")
 
   let vpackss_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpackss_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpackss_16u16
     
   (* ------------------------------------------------------------------ *)
   let vpshufb_256 = Option.get (get_specification "VPSHUFB_256")
 
   let vpshufb_256 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpshufb_256
+    Circuit_spec.circuit_of_specification [r1; r2] vpshufb_256
 
   (* ------------------------------------------------------------------ *)
   let vpcmpgt_16u16 = Option.get (get_specification "VPCMPGT_16u16")
 
   let vpcmpgt_16u16 (r1 : reg) (r2 : reg) : reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpcmpgt_16u16
+    Circuit_spec.circuit_of_specification [r1; r2] vpcmpgt_16u16
 
   (* ------------------------------------------------------------------ *)
   let vpmovmskb_u256u64 = Option.get (get_specification "VPMOVMSKB_u256u64")
 
   let vpmovmskb_u256u64 (r : reg) : reg =
-    Circuit_spec.circuit_of_spec [r] vpmovmskb_u256u64
+    Circuit_spec.circuit_of_specification [r] vpmovmskb_u256u64
 
   (* ------------------------------------------------------------------ *)
   let vpunpckl_32u8 = Option.get (get_specification "VPUNPCKL_32u8")
 
   let vpunpckl_32u8 (r1 : reg) (r2 : reg): reg =
-    Circuit_spec.circuit_of_spec [r1; r2] vpunpckl_32u8
+    Circuit_spec.circuit_of_specification [r1; r2] vpunpckl_32u8
 
   (* ------------------------------------------------------------------ *)
   let vpextracti128 = Option.get (get_specification "VPEXTRACTI128")
 
   let vpextracti128 (r : reg) (i : int): reg =
-    Circuit_spec.circuit_of_spec [r; Circuit.w8 i] vpextracti128
+    Circuit_spec.circuit_of_specification [r; Circuit.w8 i] vpextracti128
 
   (* ------------------------------------------------------------------ *)
   let vpinserti128 = Option.get (get_specification "VPINSERTI128")
 
   let vpinserti128 (r1 : reg) (r2 : reg) (i : int): reg =
-    Circuit_spec.circuit_of_spec [r1; r2; Circuit.w8 i] vpinserti128
+    Circuit_spec.circuit_of_specification [r1; r2; Circuit.w8 i] vpinserti128
 
   (* ------------------------------------------------------------------ *)
   let vpblend_16u16 = Option.get (get_specification "VPBLEND_16u16")
 
   let vpblend_16u16 (r1 : reg) (r2 : reg) (i : int): reg =
-    Circuit_spec.circuit_of_spec [r1; r2; Circuit.w8 i] vpblend_16u16
+    Circuit_spec.circuit_of_specification [r1; r2; Circuit.w8 i] vpblend_16u16
 end
diff --git a/libs/lospecs/circuit_test.ml b/libs/lospecs/tests/circuit_test.ml
similarity index 72%
rename from libs/lospecs/circuit_test.ml
rename to libs/lospecs/tests/circuit_test.ml
index fa48a870d8..2c6b09c64b 100644
--- a/libs/lospecs/circuit_test.ml
+++ b/libs/lospecs/tests/circuit_test.ml
@@ -5,7 +5,7 @@ open Lospecs
 module C = struct
   include Lospecs.Aig
   include Lospecs.Circuit
-  include Lospecs.Circuit_avx2.FromSpec ()
+  include Circuit_avx2.FromSpec ()
 end
 (* -------------------------------------------------------------------- *)
 let as_seq1 (type t) (xs : t list) =
@@ -954,343 +954,5 @@ let main () =
 
   List.iter (fun f -> f ()) tests
 
-(* ==================================================================== *)
-module PolyCompress() = struct
-  let pc_permidx_s =
-    C.w256
-      "0x00000000_00000004_00000001_00000005_00000002_00000006_00000003_00000007"
-
-  let pc_shift2_s =
-    C.w16 0x1001
-
-  let pc_mask_s =
-    C.w16 0x000f
-
-  let pc_shift1_s =
-    C.w16 0x0200
-
-  let jvx16 =
-    C.w256
-      "0x4ebf4ebf_4ebf4ebf_4ebf4ebf_4ebf4ebf_4ebf4ebf_4ebf4ebf_4ebf4ebf_4ebf4ebf"
-
-  let jqx16 =
-    C.w256
-      "0xd010d010_d010d010_d010d010_d010d010_d010d010_d010d010_d010d010_d010d01"
-
-  let poly_compress
-    (rp_0 : C.reg)
-    (rp_1 : C.reg)
-    (rp_2 : C.reg)
-    (rp_3 : C.reg)
-    (a_0  : C.reg)
-    (a_1  : C.reg)
-    (a_2  : C.reg)
-    (a_3  : C.reg)
-    (a_4  : C.reg)
-    (a_5  : C.reg)
-    (a_6  : C.reg)
-    (a_7  : C.reg)
-    (a_8  : C.reg)
-    (a_9  : C.reg)
-    (a_10 : C.reg)
-    (a_11 : C.reg)
-    (a_12 : C.reg)
-    (a_13 : C.reg)
-    (a_14 : C.reg)
-    (a_15 : C.reg)
-  : C.reg
-  =
-    let open C in
-
-    let qx16 = jqx16 in
-    let r = a_0 in
-    let r_0 = vpsub_16u16 r qx16 in
-    let t = vpsra_16u16 r_0 0x0f in
-    let t_0 = vpand_256 t qx16 in
-    let r_1 = vpadd_16u16 t_0 r_0 in
-    let a_0_0 = r_1 in
-    let r_2 = a_1 in
-    let r_3 = vpsub_16u16 r_2 qx16 in
-    let t_1 = vpsra_16u16 r_3 0x0f in
-    let t_2 = vpand_256 t_1 qx16 in
-    let r_4 = vpadd_16u16 t_2 r_3 in
-    let a_1_0 = r_4 in
-    let r_5 = a_2 in
-    let r_6 = vpsub_16u16 r_5 qx16 in
-    let t_3 = vpsra_16u16 r_6 0x0f in
-    let t_4 = vpand_256 t_3 qx16 in
-    let r_7 = vpadd_16u16 t_4 r_6 in
-    let a_2_0 = r_7 in
-    let r_8 = a_3 in
-    let r_9 = vpsub_16u16 r_8 qx16 in
-    let t_5 = vpsra_16u16 r_9 0x0f in
-    let t_6 = vpand_256 t_5 qx16 in
-    let r_10 = vpadd_16u16 t_6 r_9 in
-    let a_3_0 = r_10 in
-    let r_11 = a_4 in
-    let r_12 = vpsub_16u16 r_11 qx16 in
-    let t_7 = vpsra_16u16 r_12 0x0f in
-    let t_8 = vpand_256 t_7 qx16 in
-    let r_13 = vpadd_16u16 t_8 r_12 in
-    let a_4_0 = r_13 in
-    let r_14 = a_5 in
-    let r_15 = vpsub_16u16 r_14 qx16 in
-    let t_9 = vpsra_16u16 r_15 0x0f in
-    let t_10 = vpand_256 t_9 qx16 in
-    let r_16 = vpadd_16u16 t_10 r_15 in
-    let a_5_0 = r_16 in
-    let r_17 = a_6 in
-    let r_18 = vpsub_16u16 r_17 qx16 in
-    let t_11 = vpsra_16u16 r_18 0x0f in
-    let t_12 = vpand_256 t_11 qx16 in
-    let r_19 = vpadd_16u16 t_12 r_18 in
-    let a_6_0 = r_19 in
-    let r_20 = a_7 in
-    let r_21 = vpsub_16u16 r_20 qx16 in
-    let t_13 = vpsra_16u16 r_21 0x0f in
-    let t_14 = vpand_256 t_13 qx16 in
-    let r_22 = vpadd_16u16 t_14 r_21 in
-    let a_7_0 = r_22 in
-    let r_23 = a_8 in
-    let r_24 = vpsub_16u16 r_23 qx16 in
-    let t_15 = vpsra_16u16 r_24 0x0f in
-    let t_16 = vpand_256 t_15 qx16 in
-    let r_25 = vpadd_16u16 t_16 r_24 in
-    let a_8_0 = r_25 in
-    let r_26 = a_9 in
-    let r_27 = vpsub_16u16 r_26 qx16 in
-    let t_17 = vpsra_16u16 r_27 0x0f in
-    let t_18 = vpand_256 t_17 qx16 in
-    let r_28 = vpadd_16u16 t_18 r_27 in
-    let a_9_0 = r_28 in
-    let r_29 = a_10 in
-    let r_30 = vpsub_16u16 r_29 qx16 in
-    let t_19 = vpsra_16u16 r_30 0x0f in
-    let t_20 = vpand_256 t_19 qx16 in
-    let r_31 = vpadd_16u16 t_20 r_30 in
-    let a_10_0 = r_31 in
-    let r_32 = a_11 in
-    let r_33 = vpsub_16u16 r_32 qx16 in
-    let t_21 = vpsra_16u16 r_33 0x0f in
-    let t_22 = vpand_256 t_21 qx16 in
-    let r_34 = vpadd_16u16 t_22 r_33 in
-    let a_11_0 = r_34 in
-    let r_35 = a_12 in
-    let r_36 = vpsub_16u16 r_35 qx16 in
-    let t_23 = vpsra_16u16 r_36 0x0f in
-    let t_24 = vpand_256 t_23 qx16 in
-    let r_37 = vpadd_16u16 t_24 r_36 in
-    let a_12_0 = r_37 in
-    let r_38 = a_13 in
-    let r_39 = vpsub_16u16 r_38 qx16 in
-    let t_25 = vpsra_16u16 r_39 0x0f in
-    let t_26 = vpand_256 t_25 qx16 in
-    let r_40 = vpadd_16u16 t_26 r_39 in
-    let a_13_0 = r_40 in
-    let r_41 = a_14 in
-    let r_42 = vpsub_16u16 r_41 qx16 in
-    let t_27 = vpsra_16u16 r_42 0x0f in
-    let t_28 = vpand_256 t_27 qx16 in
-    let r_43 = vpadd_16u16 t_28 r_42 in
-    let a_14_0 = r_43 in
-    let r_44 = a_15 in
-    let r_45 = vpsub_16u16 r_44 qx16 in
-    let t_29 = vpsra_16u16 r_45 0x0f in
-    let t_30 = vpand_256 t_29 qx16 in
-    let r_46 = vpadd_16u16 t_30 r_45 in
-    let a_15_0 = r_46 in
-    let x16p = jvx16 in
-    let v = x16p in
-    let shift1 = vpbroadcast_16u16 pc_shift1_s in
-    let mask = vpbroadcast_16u16 pc_mask_s in
-    let shift2 = vpbroadcast_16u16 pc_shift2_s in
-    let permidx = pc_permidx_s in
-    let f0 = a_0_0 in
-    let f1 = a_1_0 in
-    let f2 = a_2_0 in
-    let f3 = a_3_0 in
-    let f0_0 = vpmulh_16u16 f0 v in
-    let f1_0 = vpmulh_16u16 f1 v in
-    let f2_0 = vpmulh_16u16 f2 v in
-    let f3_0 = vpmulh_16u16 f3 v in
-    let f0_1 = vpmulhrs_16u16 f0_0 shift1 in
-    let f1_1 = vpmulhrs_16u16 f1_0 shift1 in
-    let f2_1 = vpmulhrs_16u16 f2_0 shift1 in
-    let f3_1 = vpmulhrs_16u16 f3_0 shift1 in
-    let f0_2 = vpand_256 f0_1 mask in
-    let f1_2 = vpand_256 f1_1 mask in
-    let f2_2 = vpand_256 f2_1 mask in
-    let f3_2 = vpand_256 f3_1 mask in
-    let f0_3 = vpackus_16u16 f0_2 f1_2 in
-    let f2_3 = vpackus_16u16 f2_2 f3_2 in
-    let f0_4 = vpmaddubsw_256 f0_3 shift2 in
-    let f2_4 = vpmaddubsw_256 f2_3 shift2 in
-    let f0_5 = vpackus_16u16 f0_4 f2_4 in
-    let f0_6 = vpermd permidx f0_5 in
-    let rp_0_0 = f0_6 in
-    let f0_7 = a_4_0 in
-    let f1_3 = a_5_0 in
-    let f2_5 = a_6_0 in
-    let f3_3 = a_7_0 in
-    let f0_8 = vpmulh_16u16 f0_7 v in
-    let f1_4 = vpmulh_16u16 f1_3 v in
-    let f2_6 = vpmulh_16u16 f2_5 v in
-    let f3_4 = vpmulh_16u16 f3_3 v in
-    let f0_9 = vpmulhrs_16u16 f0_8 shift1 in
-    let f1_5 = vpmulhrs_16u16 f1_4 shift1 in
-    let f2_7 = vpmulhrs_16u16 f2_6 shift1 in
-    let f3_5 = vpmulhrs_16u16 f3_4 shift1 in
-    let f0_10 = vpand_256 f0_9 mask in
-    let f1_6 = vpand_256 f1_5 mask in
-    let f2_8 = vpand_256 f2_7 mask in
-    let f3_6 = vpand_256 f3_5 mask in
-    let f0_11 = vpackus_16u16 f0_10 f1_6 in
-    let f2_9 = vpackus_16u16 f2_8 f3_6 in
-    let f0_12 = vpmaddubsw_256 f0_11 shift2 in
-    let f2_10 = vpmaddubsw_256 f2_9 shift2 in
-    let f0_13 = vpackus_16u16 f0_12 f2_10 in
-    let f0_14 = vpermd permidx f0_13 in
-    let rp_1_0 = f0_14 in
-    let f0_15 = a_8_0 in
-    let f1_7 = a_9_0 in
-    let f2_11 = a_10_0 in
-    let f3_7 = a_11_0 in
-    let f0_16 = vpmulh_16u16 f0_15 v in
-    let f1_8 = vpmulh_16u16 f1_7 v in
-    let f2_12 = vpmulh_16u16 f2_11 v in
-    let f3_8 = vpmulh_16u16 f3_7 v in
-    let f0_17 = vpmulhrs_16u16 f0_16 shift1 in
-    let f1_9 = vpmulhrs_16u16 f1_8 shift1 in
-    let f2_13 = vpmulhrs_16u16 f2_12 shift1 in
-    let f3_9 = vpmulhrs_16u16 f3_8 shift1 in
-    let f0_18 = vpand_256 f0_17 mask in
-    let f1_10 = vpand_256 f1_9 mask in
-    let f2_14 = vpand_256 f2_13 mask in
-    let f3_10 = vpand_256 f3_9 mask in
-    let f0_19 = vpackus_16u16 f0_18 f1_10 in
-    let f2_15 = vpackus_16u16 f2_14 f3_10 in
-    let f0_20 = vpmaddubsw_256 f0_19 shift2 in
-    let f2_16 = vpmaddubsw_256 f2_15 shift2 in
-    let f0_21 = vpackus_16u16 f0_20 f2_16 in
-    let f0_22 = vpermd permidx f0_21 in
-    let rp_2_0 = f0_22 in
-    let f0_23 = a_12_0 in
-    let f1_11 = a_13_0 in
-    let f2_17 = a_14_0 in
-    let f3_11 = a_15_0 in
-    let f0_24 = vpmulh_16u16 f0_23 v in
-    let f1_12 = vpmulh_16u16 f1_11 v in
-    let f2_18 = vpmulh_16u16 f2_17 v in
-    let f3_12 = vpmulh_16u16 f3_11 v in
-    let f0_25 = vpmulhrs_16u16 f0_24 shift1 in
-    let f1_13 = vpmulhrs_16u16 f1_12 shift1 in
-    let f2_19 = vpmulhrs_16u16 f2_18 shift1 in
-    let f3_13 = vpmulhrs_16u16 f3_12 shift1 in
-    let f0_26 = vpand_256 f0_25 mask in
-    let f1_14 = vpand_256 f1_13 mask in
-    let f2_20 = vpand_256 f2_19 mask in
-    let f3_14 = vpand_256 f3_13 mask in
-    let f0_27 = vpackus_16u16 f0_26 f1_14 in
-    let f2_21 = vpackus_16u16 f2_20 f3_14 in
-    let f0_28 = vpmaddubsw_256 f0_27 shift2 in
-    let f2_22 = vpmaddubsw_256 f2_21 shift2 in
-    let f0_29 = vpackus_16u16 f0_28 f2_22 in
-    let f0_30 = vpermd permidx f0_29 in
-    let rp_3_0 = f0_30 in
-
-    let out = [
-      rp_0_0; rp_1_0; rp_2_0; rp_3_0;
-       a_0_0;  a_1_0;  a_2_0;  a_3_0;
-       a_4_0;  a_5_0;  a_6_0;  a_7_0;
-       a_8_0;  a_9_0; a_10_0; a_11_0;
-      a_12_0; a_13_0; a_14_0; a_15_0;
-    ] in
-
-    List.flatten out
-end
-
 (* -------------------------------------------------------------------- *)
-let poly_compress () : C.reg =
-  let module M = PolyCompress() in
-
-  let rp_0 = C.reg ~size:256 ~name:0x00 in
-  let rp_1 = C.reg ~size:256 ~name:0x01 in
-  let rp_2 = C.reg ~size:256 ~name:0x02 in
-  let rp_3 = C.reg ~size:256 ~name:0x03 in
-  let a_0  = C.reg ~size:256 ~name:0x04 in
-  let a_1  = C.reg ~size:256 ~name:0x05 in
-  let a_2  = C.reg ~size:256 ~name:0x06 in
-  let a_3  = C.reg ~size:256 ~name:0x07 in
-  let a_4  = C.reg ~size:256 ~name:0x08 in
-  let a_5  = C.reg ~size:256 ~name:0x09 in
-  let a_6  = C.reg ~size:256 ~name:0x0a in
-  let a_7  = C.reg ~size:256 ~name:0x0b in
-  let a_8  = C.reg ~size:256 ~name:0x0c in
-  let a_9  = C.reg ~size:256 ~name:0x0d in
-  let a_10 = C.reg ~size:256 ~name:0x0e in
-  let a_11 = C.reg ~size:256 ~name:0x0f in
-  let a_12 = C.reg ~size:256 ~name:0x10 in
-  let a_13 = C.reg ~size:256 ~name:0x11 in
-  let a_14 = C.reg ~size:256 ~name:0x12 in
-  let a_15 = C.reg ~size:256 ~name:0x13 in
-
-  M.poly_compress
-    (rp_0 : C.reg) (rp_1 : C.reg) (rp_2 : C.reg) (rp_3 : C.reg)
-    (a_0  : C.reg) (a_1  : C.reg) (a_2  : C.reg) (a_3  : C.reg)
-    (a_4  : C.reg) (a_5  : C.reg) (a_6  : C.reg) (a_7  : C.reg)
-    (a_8  : C.reg) (a_9  : C.reg) (a_10 : C.reg) (a_11 : C.reg)
-    (a_12 : C.reg) (a_13 : C.reg) (a_14 : C.reg) (a_15 : C.reg)
-
-(* -------------------------------------------------------------------- *)
-let poly_compress () =
-  Format.eprintf "%s@." "Constructing circuit...";
-
-  let circuit = poly_compress () in
-
-  let names = Array.of_list [
-    "rp_0";
-    "rp_1";
-    "rp_2";
-    "rp_3";
-    "a_0" ;
-    "a_1" ;
-    "a_2" ;
-    "a_3" ;
-    "a_4" ;
-    "a_5" ;
-    "a_6" ;
-    "a_7" ;
-    "a_8" ;
-    "a_9" ;
-    "a_10";
-    "a_11";
-    "a_12";
-    "a_13";
-    "a_14";
-    "a_15";
-  ] in
-
-
-  Format.eprintf "%s@." "Computing dependencies...";
-
-  let deps = C.deps circuit in
-
-  List.iter (fun ((lo, hi), deps) ->
-    let vs =
-         Iter.(--) lo hi
-      |> Iter.fold (fun vs i ->
-           let name = Format.sprintf "out_%03d" (i / 256) in
-           C.VarRange.push vs (name, i mod 256)
-         ) C.VarRange.empty in
-
-    Format.eprintf "%a: %a@."
-      (C.VarRange.pp Format.pp_print_string) vs
-      (C.VarRange.pp
-         (fun fmt i -> Format.fprintf fmt "%s" names.(i)))
-      deps
-  ) deps
-
-
-(* -------------------------------------------------------------------- *)
-(* let () = main () *)
-let () = test_smod ()
+let () = main ()
diff --git a/libs/lospecs/tests/dune b/libs/lospecs/tests/dune
new file mode 100644
index 0000000000..c67d95903f
--- /dev/null
+++ b/libs/lospecs/tests/dune
@@ -0,0 +1,9 @@
+(tests
+  (names circuit_test)
+  (flags (:standard -open Batteries))
+  (modules :standard)
+  (libraries batteries hex iter lospecs progress)
+  (foreign_stubs
+    (language cxx)
+    (flags :standard -std=c++17 -mavx -mavx2)
+    (names avx2_runtime)))
diff --git a/src/dune b/src/dune
index ddcf9460de..fa0947c5e3 100644
--- a/src/dune
+++ b/src/dune
@@ -29,4 +29,5 @@
 
 (menhir
  (modules ecParser)
- (flags --table --explain))
+ (explain true)
+ (flags --table))
diff --git a/src/ecCircuits.ml b/src/ecCircuits.ml
index 81c804f4cd..57249394b2 100644
--- a/src/ecCircuits.ml
+++ b/src/ecCircuits.ml
@@ -18,12 +18,11 @@ module Option = Batteries.Option
 module C = struct
   include Lospecs.Aig
   include Lospecs.Circuit
-  include Lospecs.Circuit_avx2.FromSpec ()
   include Lospecs.Circuit_spec
 end
 
 module HL = struct
-  include Lospecs.HLAig
+  include Lospecs.Hlaig
 end
 
 (* List of size n*w into list of n lists of size w *)
@@ -574,14 +573,22 @@ let circuit_permutation (n: int) (w: int) (f: int -> int) : circuit =
   
 (* -------------------------------------------------------------------- *)
 (* Basis for hardcoded circuit gen *)
-let load_specification (name : string) =
-  C.get_specification name
+let specifications : (string, Lospecs.Ast.adef) Map.t Lazy.t =
+  Lazy.from_fun (fun () ->
+    let specs = Filename.concat (List.hd Lospecs.Config.Sites.specs) "avx2.spec" in
+    let specs = C.load_from_file ~filename:specs in
+    Map.of_seq (List.to_seq specs)
+  )
+
+let get_specification_by_name (name : string) : Lospecs.Ast.adef option =
+  let lazy specifications = specifications in
+  Map.find_opt name specifications
 
 let circuit_from_spec_ (env: env) (p : path) : C.reg list -> C.reg  =
   (* | "OPP_8" -> C.opp (args |> registers_of_bargs env |> List.hd) (* FIXME: Needs to be in spec *) *)
   match EcEnv.Circuit.lookup_circuit_path env p with
   | Some circuit ->
-    (fun regs -> C.circuit_of_spec regs circuit) 
+    (fun regs -> C.circuit_of_specification regs circuit) 
   | None -> Format.eprintf "No operator for path: %s@."
     (let a,b = EcPath.toqsymbol p in List.fold_right (fun a b -> a ^ "." ^ b) a b);
     assert false 
diff --git a/src/ecCircuits.mli b/src/ecCircuits.mli
index 3208908ac1..8b102b470e 100644
--- a/src/ecCircuits.mli
+++ b/src/ecCircuits.mli
@@ -21,7 +21,7 @@ type cache  = (EcIdent.t, (cinput * circuit)) Map.t
 exception CircError of string
 
 (* -------------------------------------------------------------------- *)
-val load_specification : string -> Lospecs.Ast.adef option
+val get_specification_by_name : string -> Lospecs.Ast.adef option
 val cinput_to_string : cinput -> string
 val cinput_of_type : ?idn:ident -> env -> ty -> cinput
 val size_of_circ : circ -> int 
diff --git a/src/ecScope.ml b/src/ecScope.ml
index c25291d07c..468285641b 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -2527,7 +2527,7 @@ module Circuit = struct
     if not (List.is_empty opdecl.op_tparams) then
       hierror ~loc:(loc pc.operator) "operator must be monomorphic";
 
-    match EcCircuits.load_specification (unloc pc.circuit) with
+    match EcCircuits.get_specification_by_name (unloc pc.circuit) with
     | None ->
       hierror ~loc:(loc pc.circuit)
         "unknown circuit: %s" (unloc pc.circuit)
diff --git a/src/phl/ecPhlBDep.ml b/src/phl/ecPhlBDep.ml
index f8a0eb8db5..d54724fd9b 100644
--- a/src/phl/ecPhlBDep.ml
+++ b/src/phl/ecPhlBDep.ml
@@ -21,12 +21,11 @@ module Set = Batteries.Set
 module C = struct
   include Lospecs.Aig
   include Lospecs.Circuit
-  include Lospecs.Circuit_avx2.FromSpec ()
   include Lospecs.Circuit_spec
 end
 
 module HL = struct
-  include Lospecs.HLAig
+  include Lospecs.Hlaig
 end