diff --git a/Makefile b/Makefile
index 2f39dd618b..4be44c3254 100644
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,7 @@ default: build
 
 build:
 	rm -f src/ec.exe ec.native
-	dune build -p easycrypt
+	dune build
 	ln -sf src/ec.exe ec.native
 ifeq ($(UNAME_P)-$(UNAME_S),arm-Darwin)
 	-codesign -f -s - src/ec.exe
diff --git a/dune b/dune
index c588ae3ca4..337c7a9941 100644
--- a/dune
+++ b/dune
@@ -1,4 +1,9 @@
-(dirs src theories examples scripts)
+(env
+ (dev     (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69))
+ (release (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69)
+          (ocamlopt_flags -O3 -unbox-closures)))
+
+(dirs src libs theories examples scripts)
 
 (install
   (section (site (easycrypt commands)))
diff --git a/libs/lospecs/deps.ml b/libs/lospecs/deps.ml
new file mode 100644
index 0000000000..ad6138767b
--- /dev/null
+++ b/libs/lospecs/deps.ml
@@ -0,0 +1,216 @@
+(* -------------------------------------------------------------------- *)
+type symbol = string
+
+(* -------------------------------------------------------------------- *)
+type dep1 = Set.Int.t Map.String.t
+type deps = dep1 Map.Int.t
+
+(* -------------------------------------------------------------------- *)
+let eq_dep1 (d1 : dep1) (d2 : dep1) : bool =
+  Map.String.equal Set.Int.equal d1 d2
+
+(* -------------------------------------------------------------------- *)
+let eq_deps (d1 : deps) (d2 : deps) : bool =
+  Map.Int.equal eq_dep1 d1 d2
+
+(* -------------------------------------------------------------------- *)
+let empty ~(size : int) : deps =
+     (0 --^ size)
+  |> (Enum.map (fun i -> (i, Map.String.empty)))
+  |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let enlarge ~(min : int) ~(max : int) (d : deps) : deps =
+  let change = function None -> Some Map.String.empty | Some _ as v -> v in
+
+     (min --^ max)
+  |> Enum.fold (fun d i -> Map.Int.modify_opt i change d) d
+
+(* -------------------------------------------------------------------- *)
+let clearout ~(min : int) ~(max : int) (d : deps) : deps =
+  Map.Int.filter_map (fun i d1 ->
+    Some (if min <= i && i < max then d1 else Map.String.empty)
+  ) d
+
+(* -------------------------------------------------------------------- *)
+let restrict ~(min : int) ~(max : int) (d : deps) : deps =
+  Map.Int.filter (fun i _ -> min <= i && i < max) d
+
+(* -------------------------------------------------------------------- *)
+let recast ~(min : int) ~(max : int) (d : deps) : deps =
+  d |> restrict ~min ~max |> enlarge ~min ~max
+
+(* -------------------------------------------------------------------- *)
+let merge1 (d1 : dep1) (d2 : dep1) : dep1 =
+  Map.String.merge (fun _ i1 i2 ->
+    Some (Set.Int.union
+           (i1 |? Set.Int.empty)
+           (i2 |? Set.Int.empty)))
+    d1 d2
+
+(* -------------------------------------------------------------------- *)
+let merge (d1 : deps) (d2 : deps) : deps =
+  Map.Int.merge (fun _ m1 m2 ->
+    Some (merge1 (m1 |? Map.String.empty) (m2 |? Map.String.empty))
+  ) d1 d2
+
+(* -------------------------------------------------------------------- *)
+let merge1_all (ds : dep1 Enum.t) : dep1 =
+  Enum.reduce merge1 ds
+
+(* -------------------------------------------------------------------- *)
+let merge_all (ds : deps Enum.t) : deps =
+  Enum.reduce merge ds
+
+(* -------------------------------------------------------------------- *)
+let copy ~(offset : int) ~(size : int) (x : symbol) : deps =
+     (0 --^ size)
+  |> Enum.map (fun i ->
+       let di = Map.String.singleton x (Set.Int.singleton (i + offset)) in
+       (i, di)
+     )
+  |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let chunk ~(csize : int) ~(count : int) (d : deps) : deps =
+     (0 --^ count)
+  |> Enum.map (fun ci ->
+       let d1 =
+            (0 --^ csize)
+         |> Enum.map (fun i -> i + ci * csize)
+         |> Enum.map (fun i -> Map.Int.find i d)
+         |> merge1_all
+       in
+            (0 --^ csize)
+         |> Enum.map (fun i -> (i + ci * csize, d1))
+     )
+  |> Enum.flatten
+  |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let perm ~(csize : int) ~(perm : int list) (d : deps) : deps =
+     List.enum perm
+  |> Enum.mapi (fun ci x ->
+       Enum.map (fun i ->
+         (i + ci * csize, Map.Int.find (i + x * csize) d)
+       ) (0 --^ csize)
+     )
+  |> Enum.flatten
+  |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let collapse ~(csize : int) ~(count : int) (d : deps) : deps =
+     (0 --^ count)
+  |> Enum.map (fun ci ->
+       let d1 =
+            (0 --^ csize)
+         |> Enum.map (fun i -> i + ci * csize)
+         |> Enum.map (fun i -> Map.Int.find i d)
+         |> merge1_all
+       in (ci, d1)
+     )
+   |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let merge_all_deps (d : deps) : dep1 =
+  Map.Int.enum d |> Enum.map snd |> merge1_all
+
+(* -------------------------------------------------------------------- *)
+let constant ~(size : int) (d : dep1) : deps =
+  (0 --^ size) |> Enum.map (fun i -> (i, d)) |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let offset ~(offset : int) (d : deps) : deps =
+     Map.Int.enum d
+  |> Enum.map (fun (i, x) -> (i + offset, x))
+  |> Map.Int.of_enum
+
+(* -------------------------------------------------------------------- *)
+let split ~(csize : int) ~(count : int) (d : deps) : deps Enum.t =
+    (0 --^ count)
+  |> Enum.map (fun i ->
+         Map.Int.filter
+           (fun x _ -> csize * i <= x && x < csize * (i + 1))
+           d
+       |> offset ~offset:(-i * csize)
+     )
+
+(* -------------------------------------------------------------------- *)
+let aggregate ~(csize : int) (ds : deps Enum.t) =
+  Enum.foldi
+    (fun i d1 d -> merge (offset ~offset:(i * csize) d1) d)
+    (empty ~size:0)
+    ds
+
+(* ==================================================================== *)
+type 'a pp = Format.formatter -> 'a -> unit
+
+(* -------------------------------------------------------------------- *)
+let pp_bitset (fmt : Format.formatter) (d : Set.Int.t) =
+  Format.fprintf fmt "{%a}"
+    (Format.pp_print_list
+       ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
+       Format.pp_print_int)
+    (Set.Int.elements d)
+
+(* -------------------------------------------------------------------- *)
+let pp_bitintv (fmt : Format.formatter) (d : (int * int) list) =
+  Format.fprintf fmt "%a"
+    (Format.pp_print_list
+       ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
+       (fun fmt (i, j) -> Format.fprintf fmt "[%d..%d](%d)" i j (j-i+1)))
+    d
+
+(* -------------------------------------------------------------------- *)
+let bitintv_of_bitset (d : Set.Int.t) =
+  let aout = ref [] in
+  let current = ref None in
+
+  d |> Set.Int.iter (fun i ->
+    match !current with
+    | None ->
+       current := Some (i, i)
+    | Some (v1, v2) ->
+       if i = v2 + 1 then
+         current := Some (v1, i)
+       else begin
+         aout := (v1, v2) :: !aout;
+         current := Some (i, i)
+       end
+  );
+
+  Option.may
+    (fun (v1, v2) -> aout := (v1, v2) :: !aout)
+    !current;
+
+  List.rev !aout
+
+(* -------------------------------------------------------------------- *)
+let pp_dep1 (fmt : Format.formatter) (d : dep1) =
+  Map.String.iter (fun x bits ->
+    Format.fprintf fmt "%s -> %a@\n" x pp_bitintv (bitintv_of_bitset bits)
+  ) d
+
+(* -------------------------------------------------------------------- *)
+let pp_deps (fmt : Format.formatter) (d : deps) =
+  let display (v1, v2, d) =
+    Format.fprintf
+      fmt "[%d..%d](%d) -> @[@\n%a@]@\n"
+      v1 v2 (v2-v1+1) pp_dep1 d in
+
+  let current = ref None in
+
+  Map.Int.iter (fun i d ->
+    match !current with
+    | None ->
+       current := Some (i, i, d)
+    | Some (v1, v2, d') ->
+       if i = v2+1 && eq_dep1 d d' then
+         current := Some (v1, i, d')
+       else begin
+         display (v1, v2, d');
+         current := Some (i, i, d)
+       end
+  ) d;
+
+  Option.may display !current
diff --git a/libs/lospecs/deps.mli b/libs/lospecs/deps.mli
new file mode 100644
index 0000000000..569d214a27
--- /dev/null
+++ b/libs/lospecs/deps.mli
@@ -0,0 +1,56 @@
+(* -------------------------------------------------------------------- *)
+type symbol =
+  string
+
+type dep1 = Set.Int.t Map.String.t
+type deps = dep1 Map.Int.t
+
+(* -------------------------------------------------------------------- *)
+val empty : size:int -> deps
+
+val enlarge : min:int -> max:int -> deps -> deps
+
+val clearout : min:int -> max:int -> deps -> deps
+
+val restrict : min:int -> max:int -> deps -> deps
+
+val recast : min:int -> max:int -> deps -> deps
+
+val merge1 : dep1 -> dep1 -> dep1
+
+val merge : deps -> deps -> deps
+
+val merge1_all : dep1 Enum.t -> dep1
+
+val merge_all : deps Enum.t -> deps
+
+val copy : offset:int -> size:int -> symbol -> deps
+
+val chunk : csize:int -> count:int -> deps -> deps
+
+val perm : csize:int -> perm:int list -> deps -> deps
+
+val collapse : csize:int -> count:int -> deps -> deps
+
+val merge_all_deps : deps -> dep1
+
+val constant : size:int -> dep1 -> deps
+
+val offset : offset:int -> deps -> deps
+
+val split : csize:int -> count:int -> deps -> deps Enum.t
+
+val aggregate : csize:int -> deps Enum.t -> deps
+
+(* -------------------------------------------------------------------- *)
+type 'a pp = Format.formatter -> 'a -> unit
+
+val bitintv_of_bitset : Set.Int.t -> (int * int) list
+
+val pp_bitset : Set.Int.t pp
+
+val pp_bitintv : (int * int) list pp
+
+val pp_dep1 : dep1 pp
+
+val pp_deps : deps pp
diff --git a/libs/lospecs/dune b/libs/lospecs/dune
new file mode 100644
index 0000000000..f50008050a
--- /dev/null
+++ b/libs/lospecs/dune
@@ -0,0 +1,20 @@
+(library 
+ (name lospecs)
+ (public_name easycrypt.lospecs)
+ (flags (:standard -open Batteries))
+ (modules :standard \ lospecs_test)
+ (libraries batteries menhirLib)
+)
+
+(executable
+ (name lospecs_test)
+ (flags (:standard -open Batteries))
+ (modules lospecs_test)
+ (promote (until-clean))
+ (libraries batteries lospecs))
+
+(ocamllex lexer)
+
+(menhir
+ (modules parser)
+ (flags --table --explain))
diff --git a/libs/lospecs/examples/out.ec b/libs/lospecs/examples/out.ec
new file mode 100644
index 0000000000..f069821cc0
--- /dev/null
+++ b/libs/lospecs/examples/out.ec
@@ -0,0 +1,429 @@
+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/spec.txt b/libs/lospecs/examples/spec.txt
new file mode 100644
index 0000000000..6a4b205a76
--- /dev/null
+++ b/libs/lospecs/examples/spec.txt
@@ -0,0 +1,63 @@
+VPERMD(w@256, widx@256) -> @256 =
+  map<32, 8>(
+    fun idx@32 . let i = (unsigned) idx[0:2] in w[i:1:32],
+    widx
+  )
+
+VPSUB_16u16(w1@256, w2@256) -> @256 =
+  map<16, 16>(
+    fun x@16 y@16 . sub<16>(x, y),
+    w1,
+    w2
+  )
+
+Fq / <X^256 + 1>
+
+zeta : Fq = 17
+
+zeta^128 = -1
+
+P mod (X^256 - zeta^128)
+Q mod (X^256 - zeta^128)
+
+PQ mod (X^256 - zeta^128)
+
+P1 mod (X^128 - zeta^64)
+
+P mod (X^128 - zeta^64)
+
+P = sum_(i < 256) X^i * ai
+  = sum_(i < 128) X^i * (ai + a_(i+128) * zeta^64)
+
+P mod (X^128 + zeta^64)
+
+P = sum_(i < 256) X^i * ai
+  = sum_(i < 128) X^i * (ai - a_(i+128) * zeta^64)
+
+
+
+P2 mod (X^128 + zeta^64)
+
+P1 mod (X^128 - zeta^64)
+P2 mod (X^128 - zeta^192)
+
+P0 mod (X^2 - zeta^r0)
+P1 mod (X^2 - zeta^r1)
+.
+.
+.
+P127 mod (X^2 - zeta^r127)
+
+Q1 mod (X^128 - zeta^64)
+Q2 mod (X^128 + zeta^64)
+
+Q1 mod (X^128 - zeta^64)
+Q2 mod (X^128 - zeta^192)
+
+Q0 mod (X^2 - zeta^r0)
+Q1 mod (X^2 - zeta^r1)
+.
+.
+.
+Q127 mod (X^2 - zeta^r127)
+
diff --git a/libs/lospecs/io.ml b/libs/lospecs/io.ml
new file mode 100644
index 0000000000..cd9578f9d7
--- /dev/null
+++ b/libs/lospecs/io.ml
@@ -0,0 +1,5 @@
+(* -------------------------------------------------------------------- *)
+let parse (input : IO.input) : Ptree.pprogram =
+  Parser.program
+    Lexer.main
+    (Lexing.from_channel input)
diff --git a/libs/lospecs/lexer.mll b/libs/lospecs/lexer.mll
new file mode 100644
index 0000000000..0158484c40
--- /dev/null
+++ b/libs/lospecs/lexer.mll
@@ -0,0 +1,62 @@
+{
+  open Parser
+
+  let keywords = [
+    ("fun"     , FUN     );
+    ("let"     , LET     );
+    ("in"      , IN      );
+    ("signed"  , SIGNED  );
+    ("unsigned", UNSIGNED);
+  ]
+
+  let keywords =
+    let table = Hashtbl.create 0 in
+    List.iter (fun (x, k) -> Hashtbl.add table x k) keywords;
+    table
+}
+
+let lower = ['a'-'z']
+let upper = ['A'-'Z']
+let alpha = lower | upper
+let digit = ['0'-'9']
+let alnum = alpha | digit
+
+let ident = (alpha | '_') (alnum | '_')*
+
+let decnum = digit+
+
+let whitespace = [' ' '\t' '\r' '\n']
+
+rule main = parse
+  | '<'  { LT       }
+  | '>'  { GT       }
+  | '('  { LPAREN   }
+  | ')'  { RPAREN   }
+  | '['  { LBRACKET }
+  | ']'  { RBRACKET }
+  | '@'  { AT       }
+  | "->" { RARROW   }
+  | ','  { COMMA    }
+  | '='  { EQUAL    }
+  | ':'  { COLON    }
+  | '.'  { DOT      }
+
+  | ident as x
+      { Hashtbl.find_default keywords x (IDENT x) }
+
+  | decnum as d
+      { NUMBER (int_of_string d) }
+
+  | whitespace+
+      { main lexbuf }
+
+  | '#' _* ['\r' '\n']*
+      { main lexbuf }
+
+  | eof
+      { EOF }
+
+  | _ as c {
+      Format.eprintf "%c@." c;
+      assert false
+    }
diff --git a/libs/lospecs/lospecs_test.exe b/libs/lospecs/lospecs_test.exe
new file mode 100755
index 0000000000..701109443f
Binary files /dev/null and b/libs/lospecs/lospecs_test.exe differ
diff --git a/libs/lospecs/lospecs_test.ml b/libs/lospecs/lospecs_test.ml
new file mode 100644
index 0000000000..2d2d51e298
--- /dev/null
+++ b/libs/lospecs/lospecs_test.ml
@@ -0,0 +1,147 @@
+(* -------------------------------------------------------------------- *)
+open Lospecs
+
+(* -------------------------------------------------------------------- *)
+let _ =
+  let p = Io.parse IO.stdin in
+  Typing.tt_program Typing.Env.empty p
+
+(* -------------------------------------------------------------------- *)
+module List : sig
+  include module type of List
+
+  val as_seq2 : 'a list -> 'a * 'a
+
+  val paired : 'a list -> ('a * 'a) list
+end = struct
+  include List
+
+  let as_seq2 (xs : 'a list) : 'a * 'a =
+    match xs with [x; y] -> (x, y) | _ -> assert false
+
+  let rec paired (xs : 'a list) : ('a * 'a) list =
+    match xs with
+    | [] -> []
+    | v1 :: v2 :: xs -> (v1, v2) :: paired xs
+    | _ -> assert false
+end
+
+(* -------------------------------------------------------------------- *)
+module Enum : sig
+  include module type of Enum
+
+  val paired : 'a t -> ('a * 'a) t
+end = struct
+  include Enum
+
+  let paired (e : 'a t) : ('a * 'a) t =
+    let next () =
+      try
+        let v1 = Enum.get_exn e in
+        let v2 = Enum.get_exn e in
+        (v1, v2)
+      with Not_found -> raise Enum.No_more_elements
+  in Enum.from next
+end
+
+
+(* -------------------------------------------------------------------- *)
+let () =
+  let open Deps in
+
+  let f0 = copy ~offset:(0 * 256) ~size:256 "a" in (* f0 = a[u256 4*i    ]; *)
+  let f1 = copy ~offset:(1 * 256) ~size:256 "a" in (* f1 = a[u256 4*i + 1]; *)
+  let f2 = copy ~offset:(2 * 256) ~size:256 "a" in (* f2 = a[u256 4*i + 2]; *)
+  let f3 = copy ~offset:(3 * 256) ~size:256 "a" in (* f3 = a[u256 4*i + 3]; *)
+
+  (* v = 2^16 inv mod q *)
+
+  let f0 = chunk ~csize:16 ~count:16 f0 in (* f0 = #VPMULH_16u16(f0, v); // v indep from inputs *)
+  let f1 = chunk ~csize:16 ~count:16 f1 in (* f1 = #VPMULH_16u16(f1, v); // v indep from inputs *)
+  let f2 = chunk ~csize:16 ~count:16 f2 in (* f2 = #VPMULH_16u16(f2, v); // v indep from inputs *)
+  let f3 = chunk ~csize:16 ~count:16 f3 in (* f3 = #VPMULH_16u16(f3, v); // v indep from inputs *)
+
+  (* shift1 is statically known and equal to (1 << 9) *)
+  let shift1 (d : deps) =
+    let do1 (d : deps) (* 16 -> 16 *) =
+      d |> offset ~offset:(9-15) |> recast ~min:0 ~max:16 in
+
+       split ~csize:16 ~count:16 d
+    |> Enum.map do1
+    |> aggregate ~csize:16 in
+
+  (* Parallel right-shift of 6 bits *)
+  let f0 = shift1 f0 in (* f0 = #VPMULHRS_16u16(f0, shift1); // shift1 indep from inputs *)
+  let f1 = shift1 f1 in (* f1 = #VPMULHRS_16u16(f1, shift1); // shift1 indep from inputs *)
+  let f2 = shift1 f2 in (* f2 = #VPMULHRS_16u16(f2, shift1); // shift1 indep from inputs *)
+  let f3 = shift1 f3 in (* f3 = #VPMULHRS_16u16(f3, shift1); // shift1 indep from inputs *)
+
+  (* mask is statically known. We remove the clear bits *)
+  (* mask if 0x000F repeated 16 times *)
+  let and_mask (d : deps) =
+       split ~csize:16 ~count:16 d
+    |> Enum.map (clearout ~min:0 ~max:4)
+    |> aggregate ~csize:16 in
+
+  let f0 = and_mask f0 in (* f0 = #VPAND_256(f0, mask); // mask indep from inputs *)
+  let f1 = and_mask f1 in (* f0 = #VPAND_256(f0, mask); // mask indep from inputs *)
+  let f2 = and_mask f2 in (* f0 = #VPAND_256(f0, mask); // mask indep from inputs *)
+  let f3 = and_mask f3 in (* f0 = #VPAND_256(f0, mask); // mask indep from inputs *)
+
+  let packus_8u16 (d : deps) = (* 128 -> 64 *)
+       split ~csize:16 ~count:8 d
+    |> Enum.map merge_all_deps
+    |> Enum.map (constant ~size:8)
+    |> aggregate ~csize:8 in
+
+  let vpackus_8u16 (d1 : deps) (d2 : deps) : deps =
+    merge (packus_8u16 d1) (offset ~offset:64 (packus_8u16 d2)) in
+
+  let vpackus_16u16 (d1 : deps) (d2 : deps) : deps =
+    let d1 = List.of_enum (split ~csize:128 ~count:2 d1) in
+    let d2 = List.of_enum (split ~csize:128 ~count:2 d2) in
+
+    let d1, d2 = List.as_seq2 (List.map2 vpackus_8u16 d1 d2) in
+
+    merge d1 (offset ~offset:128 d2) in
+
+  let f0 = vpackus_16u16 f0 f1 in (* f0 = #VPACKUS_16u16(f0, f1); *)
+  let f2 = vpackus_16u16 f2 f3 in (* f2 = #VPACKUS_16u16(f2, f3); *)
+
+  let vpmaddubsw_256 (d1 : deps) (d2 : deps) : deps =
+    let d1 = split ~csize:8 ~count:32 d1 in
+    let d2 = split ~csize:8 ~count:32 d2 in
+
+       Enum.combine d1 d2
+    |> Enum.map (fun (x1, x2) ->
+         merge1 (merge_all_deps x1) (merge_all_deps x2)
+       )
+    |> Enum.paired
+    |> Enum.map (fun (d1, d2) -> merge1 d1 d2)
+    |> Enum.map (fun d -> constant ~size:16 d)
+    |> Enum.foldi (fun i d1 d ->
+         merge d (offset ~offset:(i * 16) d1)
+       ) (empty ~size:256)
+  in
+
+(*
+  let vpmaddubsw_256_shift2 (d : deps) : deps =
+       split ~csize:8 ~count:32 d
+    |> List.enum
+    |> Enum.paired
+    |> Enum.map (fun (d1, d2) -> merge d1 (offset ~offset:4 d2))
+    |> Enum.map (enlarge ~min:0 ~max:16)
+    |> Enum.mapi (fun i d -> offset ~offset:(i * 16) d)
+    |> merge_all
+  in
+*)
+
+  let f0 = vpmaddubsw_256 f0 (empty ~size:256) in (* f0 = #VPMADDUBSW_256(f0, shift2); *)
+  let f2 = vpmaddubsw_256 f2 (empty ~size:256) in (* f2 = #VPMADDUBSW_256(f2, shift2); *)
+
+  let f0 = vpackus_16u16 f0 f2 in (* f0 = #VPACKUS_16u16(f0, f2); *)
+
+  (* The permutation is statically known *)
+  let f0 = perm ~csize:32 ~perm:[0; 4; 1; 5; 2; 6; 3; 7] f0 in (* f0 = #VPERMD(permidx, f0); *)
+
+  Format.eprintf "%a@." pp_deps f0
diff --git a/libs/lospecs/parser.mly b/libs/lospecs/parser.mly
new file mode 100644
index 0000000000..bde1201542
--- /dev/null
+++ b/libs/lospecs/parser.mly
@@ -0,0 +1,107 @@
+%{
+  open Ptree
+%}
+
+%token AT
+%token COLON
+%token COMMA
+%token DOT
+%token EOF
+%token EQUAL
+%token FUN
+%token GT
+%token LBRACKET
+%token LET
+%token LPAREN
+%token LT
+%token IN
+%token RARROW
+%token RBRACKET
+%token RPAREN
+%token SIGNED
+%token UNSIGNED
+
+%token<string> IDENT
+%token<int>    NUMBER
+
+%type <Ptree.pprogram> program
+
+%start program
+
+%%
+
+(*
+%inline empty:
+| (* empty *) { () }
+*)
+
+%inline wname:
+| x=IDENT t=wtype
+    { (x, t) }
+
+%inline wtype:
+| AT x=NUMBER
+    { W x }
+
+type_:
+| x=wtype
+    { let W x = x in Word x }
+
+| UNSIGNED
+    { Unsigned }
+
+| SIGNED
+    { Signed }
+
+fname:
+| f=IDENT
+    { (f, None) }
+
+| f=IDENT p=angled(list0(NUMBER, COMMA))
+    { (f, Some (List.map (fun x -> W x) p)) }
+
+sexpr:
+| f=fname args=parens(list0(expr, COMMA))?
+    { PEApp (f, Option.default [] args) }
+
+| e=parens(expr)
+    { PEParens e }
+
+| i=NUMBER
+    { PEInt i }
+
+expr:
+| e=sexpr
+    { e }
+
+| FUN args=wname* DOT body=expr
+    { PEFun (args, body) }
+
+| LET x=IDENT EQUAL e1=expr IN e2=expr
+    { PELet ((x, e1), e2) }
+
+| e=sexpr LBRACKET i1=expr COLON i2=expr RBRACKET
+    { PESlice (e, (i1, i2, None)) }
+
+| e=sexpr LBRACKET i1=expr COLON i2=expr COLON i3=expr RBRACKET
+    { PESlice (e, (i1, i2, Some i3)) }
+
+| LPAREN t=type_ RPAREN e=expr
+    { PECast (t, e) }
+
+def:
+| name=IDENT args=parens(list0(wname, COMMA)) RARROW rty=wtype EQUAL body=expr
+    { { name; args; rty; body; } }
+
+program:
+| defs=def* EOF
+    { defs }
+
+%inline parens(X):
+| LPAREN x=X RPAREN { x }
+
+%inline angled(X):
+| LT x=X GT { x }
+
+%inline list0(X, S):
+| x=separated_list(S, X) { x }
diff --git a/libs/lospecs/ptree.ml b/libs/lospecs/ptree.ml
new file mode 100644
index 0000000000..aba4fc59a7
--- /dev/null
+++ b/libs/lospecs/ptree.ml
@@ -0,0 +1,39 @@
+(* -------------------------------------------------------------------- *)
+type symbol =
+  string
+
+type pword =
+  W of int
+
+type ptype =
+  | Unsigned
+  | Signed
+  | Word of int
+
+type parg =
+  symbol * pword
+
+type pargs =
+  parg list
+
+type pfname =
+  symbol * pword list option
+
+type pexpr =
+  | PEParens of pexpr
+  | PEInt    of int
+  | PECast   of ptype * pexpr
+  | PEFun    of pargs * pexpr
+  | PELet    of (symbol * pexpr) * pexpr
+  | PESlice  of pexpr * (pexpr * pexpr * pexpr option)
+  | PEApp    of pfname * pexpr list
+
+type pdef = {
+  name : symbol;
+  args : pargs;
+  rty  : pword;
+  body : pexpr;
+}
+
+type pprogram =
+  pdef list
diff --git a/libs/lospecs/typing.ml b/libs/lospecs/typing.ml
new file mode 100644
index 0000000000..a1a533960c
--- /dev/null
+++ b/libs/lospecs/typing.ml
@@ -0,0 +1,104 @@
+(* -------------------------------------------------------------------- *)
+open Ptree
+
+(* -------------------------------------------------------------------- *)
+module Ident : sig
+  type ident
+
+  val create : string -> ident
+
+  val name : ident -> string
+end = struct
+  type ident = symbol * int
+
+  let create (x : string) : ident =
+    (x, 0)
+
+  let name ((x, _) : ident) : string =
+    x
+end
+
+(* -------------------------------------------------------------------- *)
+type ident = Ident.ident
+
+(* -------------------------------------------------------------------- *)
+type aword =
+  | W of int
+
+(* -------------------------------------------------------------------- *)
+type atype =
+  | W of int
+  | Signed
+  | Unsigned
+
+(* -------------------------------------------------------------------- *)
+type aarg =
+  ident * aword
+
+(* -------------------------------------------------------------------- *)
+type aargs =
+  aarg list
+
+(* -------------------------------------------------------------------- *)
+module Env : sig
+  type env
+
+  val empty : env
+
+  val lookup : env -> symbol -> (ident * atype) option
+
+  val push : env -> symbol -> atype -> env * ident
+end = struct
+  type env = {
+    vars : (symbol, ident * atype) Map.t;
+  }
+
+  let empty : env =
+    { vars = Map.empty; }
+
+  let lookup (env : env) (x : symbol) =
+    Map.find_opt x env.vars
+
+  let push (env : env) (x : symbol) (ty : atype) =
+    let idx = Ident.create x in
+    let env = { vars = Map.add x (idx, ty) env.vars } in
+    (env, idx)
+end
+
+(* -------------------------------------------------------------------- *)
+type env = Env.env
+
+(* -------------------------------------------------------------------- *)
+let tt_pword (_ : env) (W ty : pword) : atype =
+  W ty
+
+(* -------------------------------------------------------------------- *)
+let rec tt_expr (env : env) ?(check : atype option) (e : pexpr) =
+  match e with
+  | PEParens _e ->
+      tt_expr env ?check e
+
+  | PEInt _i ->
+      assert false
+
+  | _ ->
+     assert false
+
+(* -------------------------------------------------------------------- *)
+let tt_arg (env : env) ((x, W ty) : parg) : env * aarg =
+  let env, idx = Env.push env x (W ty) in
+  (env, (idx, W ty))
+
+(* -------------------------------------------------------------------- *)
+let tt_args (env : env) (args : pargs) : env * aargs =
+  List.fold_left_map tt_arg env args
+
+(* -------------------------------------------------------------------- *)
+let tt_def (env : env) (p : pdef) =
+  let _env, _args = tt_args env p.args in
+  let _body = tt_expr env ~check:(tt_pword env p.rty) p.body in
+  assert false
+
+(* -------------------------------------------------------------------- *)
+let tt_program (env : env) (p : pprogram) =
+  List.fold_left_map tt_def env p
diff --git a/src/ecBDep.ml b/src/ecBDep.ml
new file mode 100644
index 0000000000..107e5d9d2a
--- /dev/null
+++ b/src/ecBDep.ml
@@ -0,0 +1,173 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcBigInt
+open EcSymbols
+open EcPath
+open EcParsetree
+open EcEnv
+open EcTypes
+open EcModules
+
+(* -------------------------------------------------------------------- *)
+type width = int
+
+type bprgm =
+  bstmt list
+
+and bstmt =
+  symbol * brhs
+
+and brhs =
+  | Const of width * zint
+  | Copy  of symbol
+  | Op    of symbol * barg list
+
+
+and barg =
+  | Const of width * zint
+  | Var   of symbol
+
+(* -------------------------------------------------------------------- *)
+let pp_barg (fmt : Format.formatter) (b : barg) =
+  match b with
+  | Const (w, i) ->
+     Format.fprintf fmt "%a@%d" EcBigInt.pp_print i w
+
+  | Var x ->
+     Format.fprintf fmt "%s" x
+
+(* -------------------------------------------------------------------- *)
+let pp_brhs (fmt : Format.formatter) (rhs : brhs) =
+  match rhs with
+  | Const (w, i) ->
+     Format.fprintf fmt "%a@%d" EcBigInt.pp_print i w
+
+  | Copy x ->
+     Format.fprintf fmt "%s" x
+
+  | Op (op, args) ->
+     Format.fprintf fmt "%s%a"
+       op
+       (Format.pp_print_list
+          (fun fmt a -> Format.fprintf fmt "@ %a" pp_barg a))
+       args
+
+(* -------------------------------------------------------------------- *)
+let pp_bstmt (fmt : Format.formatter) ((x, rhs) : bstmt) =
+  Format.fprintf fmt "%s = %a" x pp_brhs rhs
+
+(* -------------------------------------------------------------------- *)
+let pp_bprgm (fmt : Format.formatter) (bprgm : bprgm) =
+  List.iter (Format.fprintf fmt "%a;@." pp_bstmt) bprgm
+
+(* -------------------------------------------------------------------- *)
+exception BDepError
+
+(* -------------------------------------------------------------------- *)
+let decode_op (p : path) : symbol =
+  match EcPath.toqsymbol p with
+  | ["Top"; "JWord"; "W16u16"], ("VPSUB_16u16"       as op)
+  | ["Top"; "JWord"; "W16u16"], ("VPSRA_16u16"       as op)
+  | ["Top"; "JWord"; "W16u16"], ("VPADD_16u16"       as op)
+  | ["Top"; "JWord"; "W16u16"], ("VPBROADCAST_16u16" as op)
+  | ["Top"; "JWord"; "W16u16"], ("VPMULH_16u16"      as op)
+
+     -> op
+
+  | ["Top"; "JModel_x86"], ("VPMULHRS_16u16" as op)
+  | ["Top"; "JModel_x86"], ("VPACKUS_16u16"  as op)
+  | ["Top"; "JModel_x86"], ("VPMADDUBSW_256" as op)
+  | ["Top"; "JModel_x86"], ("VPERMD"         as op)
+
+     -> op
+
+  | ["Top"; "JWord"; "W256"], "andw" -> "AND_u256"
+
+  | _ ->
+     Format.eprintf "%s@." (EcPath.tostring p);
+     raise BDepError
+
+(* -------------------------------------------------------------------- *)
+let bdep (env : env) (p : pgamepath) : unit =
+  let proc = EcTyping.trans_gamepath env p in
+  let proc = EcEnv.Fun.by_xpath proc env in
+  let pdef = match proc.f_def with FBdef def -> def | _ -> assert false in
+
+  let trans_int (p : path) : width =
+    match EcPath.toqsymbol p with
+    | (["Top"; "JWord"; "W256"], "of_int") -> 256
+    | (["Top"; "JWord"; "W128"], "of_int") -> 128
+    | (["Top"; "JWord"; "W64" ], "of_int") ->  64
+    | (["Top"; "JWord"; "W32" ], "of_int") ->  32
+    | (["Top"; "JWord"; "W16" ], "of_int") ->  16
+    | (["Top"; "JWord"; "W8"  ], "of_int") ->   8
+    | _ -> raise BDepError in
+
+  let trans_wtype (ty : ty) : width =
+    match (EcEnv.Ty.hnorm ty env).ty_node with
+    | Tconstr (p, []) -> begin
+        match EcPath.toqsymbol p with
+        | (["Top"; "JWord"; "W256"], "t") -> 256
+        | (["Top"; "JWord"; "W128"], "t") -> 128
+        | (["Top"; "JWord"; "W64" ], "t") ->  64
+        | (["Top"; "JWord"; "W32" ], "t") ->  32
+        | (["Top"; "JWord"; "W16" ], "t") ->  16
+        | (["Top"; "JWord"; "W8"  ], "t") ->   8
+        | _ -> raise BDepError
+      end
+
+    | _ ->
+       raise BDepError in
+
+  let trans_arg (e : expr) : barg =
+    match e.e_node with
+    | Evar (PVloc y) ->
+       Var y
+
+     | Eapp ({ e_node = Eop (p, []) }, [{ e_node = Eint i }]) ->
+        Const (trans_int p, i)
+
+    | _ ->
+       let ppe = EcPrinting.PPEnv.ofenv env in
+       Format.eprintf "%a@." (EcPrinting.pp_expr ppe) e;
+       raise BDepError
+
+  in
+
+  let trans_instr (i : instr) : bstmt =
+    match i.i_node with
+    | Sasgn (LvVar (PVloc x, _), e) ->
+       let rhs =
+         match e.e_node with
+         | Evar (PVloc y) ->
+            Copy y
+
+         | Eapp ({ e_node = Eop (p, []) }, [{ e_node = Eint i }]) ->
+            Const (trans_int p, i)
+
+         | Eapp ({ e_node = Eop (p, []) }, args) ->
+            Op (decode_op p, List.map trans_arg args)
+
+         | _ ->
+            raise BDepError
+
+       in (x, rhs)
+
+    | _ -> raise BDepError in
+
+  let trans_arg (x : ovariable) =
+    (oget ~exn:BDepError x.ov_name, trans_wtype x.ov_type) in
+
+  let trans_local (x : variable) =
+    (x.v_name, trans_wtype x.v_type) in
+
+  let _locals =
+    (List.map trans_arg proc.f_sig.fs_anames) @
+    (List.map trans_local pdef.f_locals) in
+
+  let body = List.map trans_instr pdef.f_body.s_node in
+
+  if not (List.is_unique (List.fst body)) then
+    raise BDepError;
+
+  Format.eprintf "%a" pp_bprgm body
diff --git a/src/ecBDep.mli b/src/ecBDep.mli
new file mode 100644
index 0000000000..e30ea851f4
--- /dev/null
+++ b/src/ecBDep.mli
@@ -0,0 +1,6 @@
+(* -------------------------------------------------------------------- *)
+open EcParsetree
+open EcEnv
+
+(* -------------------------------------------------------------------- *)
+val bdep : env -> pgamepath -> unit
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 0133996972..5951e1bd96 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -634,6 +634,10 @@ and process_dump scope (source, tc) =
 
   scope
 
+(* -------------------------------------------------------------------- *)
+and process_bdep (scope : EcScope.scope) (p : pgamepath) =
+  EcBDep.bdep (EcScope.env scope) p
+
 (* -------------------------------------------------------------------- *)
 and process (ld : Loader.loader) (scope : EcScope.scope) g =
   let loc = g.pl_loc in
@@ -676,6 +680,7 @@ 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 -> `State (fun scope -> process_bdep       scope proc)
     with
     | `Fct   f -> Some (f scope)
     | `State f -> f scope; None
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
index 2a507a5cd8..e1306b4149 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -163,6 +163,7 @@
     "kill"        , KILL       ;        (* KW: tactic *)
     "eager"       , EAGER      ;        (* KW: tactic *)
 
+    "bdep"        , BDEP       ;        (* KW: global *)
     "axiom"       , AXIOM      ;        (* KW: global *)
     "schema"      , SCHEMA     ;        (* KW: global *)
     "axiomatized" , AXIOMATIZED;        (* KW: global *)
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 088b846550..93d1b8fbb9 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -398,6 +398,7 @@
 %token AXIOMATIZED
 %token BACKS
 %token BACKSLASH
+%token BDEP
 %token BETA
 %token BY
 %token BYEQUIV
@@ -3999,6 +4000,9 @@ global_action:
 | LOCATE x=qident  { Glocate      x  }
 | WHY3 x=STRING    { GdumpWhy3    x  }
 
+| BDEP f=loc(fident)
+    { Gbdep f }
+
 | PRAGMA       x=pragma { Gpragma x }
 | PRAGMA PLUS  x=pragma { Goption (x, `Bool true ) }
 | PRAGMA MINUS x=pragma { Goption (x, `Bool false) }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 51f26759c5..bdfd7e391a 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1276,6 +1276,7 @@ type global_action =
   | Gpragma      of psymbol
   | Goption      of (psymbol * [`Bool of bool | `Int of int])
   | GdumpWhy3    of string
+  | Gbdep        of pgamepath
 
 type global = {
   gl_action : global_action located;