diff --git a/bench/src/Main.ml b/bench/src/Main.ml
index 9e206be45..8fc9f491f 100644
--- a/bench/src/Main.ml
+++ b/bench/src/Main.ml
@@ -76,10 +76,12 @@ let compile compiler per_switch varorder tbl_opt debug filename =
     | "varorder-heuristic" -> `Heuristic
     | "varorder-fattree" ->
       `Static [ EthType; Switch; Location; EthSrc; EthDst; Vlan;
-                VlanPcp; IPProto;IP4Src; IP4Dst; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric; ]
+                VlanPcp; IPProto;IP4Src; IP4Dst; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric;
+                Meta0; Meta1; Meta2; Meta3; Meta4; ]
     | "varorder-zoo" ->
       `Static [ EthType; Switch; IP4Dst; Location; EthSrc; EthDst; Vlan;
-                VlanPcp; IPProto;IP4Src; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric; ]
+                VlanPcp; IPProto;IP4Src; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric;
+                Meta0; Meta1; Meta2; Meta3; Meta4; ]
     | _ -> assert false in
   let to_table sw fdd = match tbl_opt with
     | "tablegen-steffen" ->
@@ -133,7 +135,7 @@ let sdx filename =
   let order =
     let open Frenetic_NetKAT_Compiler.Field in
     `Static [ Location; EthDst; TCPSrcPort; TCPDstPort; IP4Src; EthType; Switch; IP4Dst;
-              EthSrc;  Vlan; VlanPcp; IPProto; VSwitch; VPort; VFabric ] in
+              EthSrc;  Vlan; VlanPcp; IPProto; VSwitch; VPort; VFabric; Meta0; Meta1; Meta2; Meta3; Meta4 ] in
   (* eprintf "Number of elements in disjoint union: %d\n%!" (List.length pols); *)
   let f pol =
     let opts = { Frenetic_NetKAT_Compiler.default_compiler_options with
diff --git a/examples/meta-fields/README.md b/examples/meta-fields/README.md
new file mode 100644
index 000000000..d7b1d5358
--- /dev/null
+++ b/examples/meta-fields/README.md
@@ -0,0 +1,8 @@
+# Meta Fields
+
+## Documentation
+see https://github.com/frenetic-lang/frenetic/pull/517
+
+## Runing the examples
+The examples in this directory can be run by executing `frenetic dump local <file>`.
+Some examples require adding the flag `--switch 1`.
diff --git a/examples/meta-fields/craig.kat b/examples/meta-fields/craig.kat
new file mode 100644
index 000000000..98438d06a
--- /dev/null
+++ b/examples/meta-fields/craig.kat
@@ -0,0 +1,3 @@
+var suspect:=0 in
+filter switch=1 and ip4Src=8.0.0.0/8; suspect:=1; port:=5 |
+filter switch=2 and suspect=1; drop
diff --git a/examples/meta-fields/default-port.kat b/examples/meta-fields/default-port.kat
new file mode 100644
index 000000000..faf4e5147
--- /dev/null
+++ b/examples/meta-fields/default-port.kat
@@ -0,0 +1,12 @@
+(* create immutable meta field that carries original port value *)
+let ingress := port in
+
+(* by default, forward packets to controller *)
+port := pipe("controller");
+
+(* overwrite default behavior ... *)
+begin
+  if ingress=1 then port:=2 else
+  if ethDst=1 then port:=1 else
+  id
+end
diff --git a/examples/meta-fields/meta-error1.kat b/examples/meta-fields/meta-error1.kat
new file mode 100644
index 000000000..f02512547
--- /dev/null
+++ b/examples/meta-fields/meta-error1.kat
@@ -0,0 +1,3 @@
+(* let declares immutable variables - hence this should not compile *)
+let meta:=0 in
+meta:=1
diff --git a/examples/meta-fields/meta-error2.kat b/examples/meta-fields/meta-error2.kat
new file mode 100644
index 000000000..b80849439
--- /dev/null
+++ b/examples/meta-fields/meta-error2.kat
@@ -0,0 +1,3 @@
+(* let declares immutable variables - hence this should not compile *)
+let meta:=switch in
+meta:=1
diff --git a/examples/meta-fields/meta1.kat b/examples/meta-fields/meta1.kat
new file mode 100644
index 000000000..a84a270fe
--- /dev/null
+++ b/examples/meta-fields/meta1.kat
@@ -0,0 +1,4 @@
+let x:=1 in
+filter x=0; port:=0 |
+filter x=1; port:=1 |
+filter x=2; port:=2
\ No newline at end of file
diff --git a/examples/meta-fields/multiple-error.kat b/examples/meta-fields/multiple-error.kat
new file mode 100644
index 000000000..1fa0fc2ca
--- /dev/null
+++ b/examples/meta-fields/multiple-error.kat
@@ -0,0 +1,8 @@
+(* this will fail since we currently only support up to 5 meta fields in scope at once *)
+let m1 := vlanId in
+let m2 := port in
+let m3 := 423 in
+let m4 := port in
+let m5 := 1 in
+let m6 := 2 in
+id
diff --git a/examples/meta-fields/multiple.kat b/examples/meta-fields/multiple.kat
new file mode 100644
index 000000000..f090f5e38
--- /dev/null
+++ b/examples/meta-fields/multiple.kat
@@ -0,0 +1,7 @@
+let m1 := vlanId in
+let m2 := port in
+let m3 := 423 in
+let m4 := port in
+filter m1=1 and m2=1 and m3=423; port:=pipe("success!") |
+filter m1=2 and m2=2 and m3=1;   port:=pipe("fail :(") |
+filter m1=2 and m2=2 and m4=3;   port:=pipe("fail :(")
diff --git a/frenetic/Dump.ml b/frenetic/Dump.ml
index 7030ce4d8..c81104f65 100644
--- a/frenetic/Dump.ml
+++ b/frenetic/Dump.ml
@@ -37,8 +37,14 @@ let time f =
   let t2 = Unix.gettimeofday () in
   (t2 -. t1, r)
 
-let print_time time =
-  printf "Compilation time: %.4f\n" time
+let print_time ?(prefix="") time =
+  printf "%scompilation time: %.4f\n" prefix time
+
+let print_order () =
+  Frenetic_NetKAT_Compiler.Field.(get_order ()
+    |> List.map ~f:to_string
+    |> String.concat ~sep:" > "
+    |> printf "FDD field ordering: %s\n")
 
 
 (*===========================================================================*)
@@ -85,6 +91,10 @@ module Flag = struct
     flag "--json" no_arg
       ~doc: " Parse input file as JSON."
 
+  let print_order =
+    flag "--print-order" no_arg
+      ~doc: " Print FDD field order used by the compiler."
+
   let vpol =
     flag "--vpol" (optional_with_default "vpol.dot" file)
       ~doc: "file Virtual policy. Must not contain links. \
@@ -137,9 +147,10 @@ module Local = struct
     +> Flag.dump_fdd
     +> Flag.no_tables
     +> Flag.json
+    +> Flag.print_order
   )
 
-  let run file nr_switches printfdd dumpfdd no_tables json () =
+  let run file nr_switches printfdd dumpfdd no_tables json printorder () =
     let pol = parse_pol ~json file in
     let (t, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_local pol) in
     let switches = match nr_switches with
@@ -150,6 +161,7 @@ module Local = struct
       printf "Number of switches not automatically recognized!\n\
               Use the --switch flag to specify it manually.\n"
     else
+      if printorder then print_order ();
       if printfdd then print_fdd fdd;
       if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
       print_all_tables ~no_tables fdd switches;
@@ -168,12 +180,14 @@ module Global = struct
     +> Flag.dump_auto
     +> Flag.no_tables
     +> Flag.json
+    +> Flag.print_order
   )
 
-  let run file printfdd dumpfdd printauto dumpauto no_tables json () =
+  let run file printfdd dumpfdd printauto dumpauto no_tables json printorder () =
     let pol = parse_pol ~json file in
     let (t, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_global pol) in
     let switches = Frenetic_NetKAT_Semantics.switches_of_policy pol in
+    if printorder then print_order ();
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
@@ -198,9 +212,12 @@ module Virtual = struct
     +> Flag.print_fdd
     +> Flag.dump_fdd
     +> Flag.print_global_pol
+    +> Flag.no_tables
+    +> Flag.print_order
   )
 
-  let run vpol_file vrel vtopo ving_pol ving veg ptopo ping peg printfdd dumpfdd printglobal () =
+  let run vpol_file vrel vtopo ving_pol ving veg ptopo ping peg printfdd dumpfdd printglobal
+    no_tables printorder () =
     (* parse files *)
     let vpol = parse_pol vpol_file in
     let vrel = parse_pred vrel in
@@ -214,10 +231,9 @@ module Virtual = struct
 
     (* compile *)
     let module Virtual = Frenetic_NetKAT_Virtual_Compiler in
-    let global_pol =
-      Virtual.compile vpol ~log:true ~vrel ~vtopo ~ving_pol ~ving ~veg ~ptopo ~ping ~peg
-    in
-    let fdd = Frenetic_NetKAT_Compiler.compile_global global_pol in
+    let (t1, global_pol) = time (fun () ->
+      Virtual.compile vpol ~log:true ~vrel ~vtopo ~ving_pol ~ving ~veg ~ptopo ~ping ~peg) in
+    let (t2, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_global global_pol) in
 
     (* print & dump *)
     let switches = Frenetic_NetKAT_Semantics.switches_of_policy global_pol in
@@ -225,10 +241,12 @@ module Virtual = struct
       Format.fprintf fmt "Global Policy:@\n@[%a@]@\n@\n"
         Frenetic_NetKAT_Pretty.format_policy global_pol
     end;
+    if printorder then print_order ();
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(vpol_file ^ ".dot");
-    print_all_tables fdd switches
-
+    print_all_tables ~no_tables fdd switches;
+    print_time ~prefix:"virtual " t1;
+    print_time ~prefix:"global " t2;
 end
 
 
diff --git a/lib/Frenetic_Fdd.ml b/lib/Frenetic_Fdd.ml
index 67b6baa77..03f1769a9 100644
--- a/lib/Frenetic_Fdd.ml
+++ b/lib/Frenetic_Fdd.ml
@@ -2,14 +2,24 @@ open Core.Std
 
 module SDN = Frenetic_OpenFlow
 
+
 module Field = struct
 
+  (** The order of the constructors defines the default variable ordering and has a massive
+      performance impact. Do not change unless you know what you are doing. *)
   type t
     = Switch
-    | Vlan
-    | VlanPcp
+    | Location
     | VSwitch
     | VPort
+    | Vlan
+    | VlanPcp
+    (* SJS: for simplicity, support only up to 5 meta fields for now *)
+    | Meta0
+    | Meta1
+    | Meta2
+    | Meta3
+    | Meta4
     | EthType
     | IPProto
     | EthSrc
@@ -18,13 +28,9 @@ module Field = struct
     | IP4Dst
     | TCPSrcPort
     | TCPDstPort
-    | Location
     | VFabric
     [@@deriving sexp, enumerate, enum]
-
-  (** The type of packet fields. This is an enumeration whose ordering has an
-      effect on the performance of Tdk operations, as well as the size of the
-      flowtables that the compiler will produce. *)
+  type field = t
 
   let num_fields = max + 1
 
@@ -39,8 +45,6 @@ module Field = struct
   let is_valid_order (lst : t list) : bool =
     Set.Poly.(equal (of_list lst) (of_list all))
 
-  (* order[i] = the position of field i in the current ordering.  Indexes are 1..15 assigned by Obj.magic,
-     so that order[1] is the index of the Switch field.  Initial order is the order in which fields appear in this file. *)
   let order = Array.init num_fields ~f:ident
 
   let set_order (lst : t list) : unit =
@@ -62,7 +66,42 @@ module Field = struct
     (* using Obj.magic instead of to_enum for bettter performance *)
     Int.compare order.(Obj.magic x) order.(Obj.magic y)
 
-  let field_of_header_val hv = match hv with
+  module type ENV = sig
+    type t
+    val empty : t
+    exception Full
+    val add : t -> string -> Frenetic_NetKAT.meta_init -> bool -> t (* may raise Full *)
+    val lookup : t -> string -> field * (Frenetic_NetKAT.meta_init * bool) (* may raise Not_found *)
+  end
+
+  module Env : ENV = struct
+
+    type t = { 
+      alist : (string * (field * (Frenetic_NetKAT.meta_init * bool))) list; 
+      depth : int
+    }
+
+    let empty = { alist = []; depth = 0 }
+
+    exception Full
+
+    let add env name init mut =
+      let field =
+        match env.depth with
+        | 0 -> Meta0
+        | 1 -> Meta1
+        | 2 -> Meta2
+        | 3 -> Meta3
+        | 4 -> Meta4
+        | _ -> raise Full
+      in
+      { alist = List.Assoc.add env.alist name (field, (init, mut)); depth = env.depth + 1}
+
+    let lookup env name =
+      List.Assoc.find_exn env.alist name
+  end
+
+  let of_hv ?(env=Env.empty) hv = match hv with
     | Frenetic_NetKAT.Switch _ -> Switch
     | Frenetic_NetKAT.Location _ -> Location
     | Frenetic_NetKAT.EthSrc _ -> EthSrc
@@ -78,6 +117,7 @@ module Field = struct
     | Frenetic_NetKAT.TCPSrcPort _ -> TCPSrcPort
     | Frenetic_NetKAT.TCPDstPort _ -> TCPDstPort
     | Frenetic_NetKAT.VFabric _ -> VFabric
+    | Frenetic_NetKAT.Meta (id,_) -> fst (Env.lookup env id)
 
   (* Heuristic to pick a variable order that operates by scoring the fields
      in a policy. A field receives a high score if, when a test field=X
@@ -93,46 +133,69 @@ module Field = struct
        field assignments to sizes. *)
   let auto_order (pol : Frenetic_NetKAT.policy) : unit =
     let open Frenetic_NetKAT in
-    (* Construct map of (field,score) pairs, where score starts at 0 for every field *)
-    let count_tbl =
-      match Hashtbl.Poly.of_alist (List.map all ~f:(fun f -> (f, 0))) with
-      | `Ok tbl -> tbl
-      | `Duplicate_key _ -> assert false in (* Should never happen because assert above will catch it *)
-    let rec f_pred size in_product pred = match pred with
+    (* Construct array of scores, where score starts at 0 for every field *)
+    let count_arr = Array.init num_fields ~f:(fun _ -> 0) in
+    let rec f_pred size (env, pred) = match pred with
       | True -> ()
       | False -> ()
+      | Test (Frenetic_NetKAT.Meta (id,_)) ->
+        begin match Env.lookup env id with
+        | (f, (Alias hv, false)) ->
+          let f = to_enum f in
+          let f' = to_enum (of_hv hv) in
+          count_arr.(f) <- count_arr.(f) + size;
+          count_arr.(f') <- count_arr.(f') + size
+        | (f,_) ->
+          let f = to_enum f in
+          count_arr.(f) <- count_arr.(f) + size
+        end
       | Test hv ->
-        if in_product then
-          let fld = field_of_header_val hv in
-          let n = Hashtbl.Poly.find_exn count_tbl fld in
-          Hashtbl.Poly.set count_tbl ~key:fld ~data:(n + size)
-      | Or (a, b) -> f_pred size false a; f_pred size false b
-      | And (a, b) -> f_pred size true a; f_pred size true b
-      | Neg a -> f_pred size in_product a in
-    let rec f_seq' pol lst = match pol with
-      | Mod _ -> (1, lst)
-      | Filter a -> (1, a :: lst)
+        let f = to_enum (of_hv hv) in
+        count_arr.(f) <- count_arr.(f) + size
+      | Or (a, b) -> f_pred size (env, a); f_pred size (env, b)
+      | And (a, b) -> f_pred size (env, a); f_pred size (env, b)
+      | Neg a -> f_pred size (env, a) in
+    let rec f_seq' pol lst env k = match pol with
+      | Mod _ -> k (1, lst)
+      | Filter a -> k (1, (env, a) :: lst)
       | Seq (p, q) ->
-        let (m, lst) = f_seq' p lst in
-        let (n, lst) = f_seq' q lst in
-        (m * n, lst)
-      | Union _ -> (f_union pol, lst)
-      | Star _ | Link _ | VLink _ -> (1, lst) (* bad, but it works *)
-    and f_seq pol =
-      let (size, preds) = f_seq' pol [] in
-      List.iter preds ~f:(f_pred size true);
+        f_seq' p lst env (fun (m, lst) -> 
+          f_seq' q lst env (fun (n, lst) ->
+            k (m * n, lst)))
+      | Union _ -> k (f_union pol env, lst)
+      | Let (id, init, mut, p) -> 
+        let env = Env.add env id init mut in 
+        f_seq' p lst env k
+      | Star p -> k (f_union p env, lst)
+      | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst)
+      | VLink (sw,pt,_,_) -> k (1, (env, Test (VSwitch sw)) :: (env, Test (VPort pt)) :: lst)
+    and f_seq pol env : int =
+      let (size, preds) = f_seq' pol [] env (fun x -> x) in
+      List.iter preds ~f:(f_pred size);
       size
-    and f_union' pol k = match pol with
-      | Mod _ -> k 1
-      | Filter _ -> k 1
+    and f_union' pol lst env k = match pol with
+      | Mod _ -> (1, lst)
+      | Filter a -> (1, (env, a) :: lst)
       | Union (p, q) ->
-        f_union' p (fun m -> f_union' q (fun n -> k (m + n)))
-      | Seq _ -> k (f_seq pol)
-      | Star _ | Link _ | VLink _ -> k 1 (* bad, but it works *)
-    and f_union pol = f_union' pol (fun n -> n) in
-    let _ = f_seq pol in
-    Hashtbl.Poly.to_alist count_tbl
-    |> List.sort ~cmp:(fun (_, x) (_, y) -> Int.compare y x)
+        f_union' p lst env (fun (m, lst) -> 
+          f_union' q lst env (fun (n, lst) ->
+            k (m + n, lst)))
+      | Seq _ -> k (f_seq pol env, lst)
+      | Let (id, init, mut, p) -> 
+        let env = Env.add env id init mut in 
+        k (f_seq p env, lst)
+      | Star p -> f_union' p lst env k
+      | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst)
+      | VLink (sw,pt,_,_) -> k (1, (env, Test (VSwitch sw)) :: (env, Test (VPort pt)) :: lst)
+    and f_union pol env : int =
+      let (size, preds) = f_union' pol [] env (fun x -> x) in
+      List.iter preds ~f:(f_pred size);
+      size
+    in
+    let _ = f_seq pol Env.empty in
+    Array.foldi count_arr ~init:[] ~f:(fun i acc n -> ((Obj.magic i, n) :: acc))
+    |> List.stable_sort ~cmp:(fun (_, x) (_, y) -> Int.compare x y)
+    |> List.rev (* SJS: do NOT remove & reverse order! Want stable sort *)
     |> List.map ~f:fst
     |> set_order
 
@@ -295,7 +358,7 @@ module Pattern = struct
   let to_int = Int64.to_int_exn
   let to_int32 = Int64.to_int32_exn
 
-  let of_hv hv =
+  let of_hv ?(env=Field.Env.empty) hv =
     let open Frenetic_NetKAT in
     match hv with
     | Switch sw_id -> (Field.Switch, Value.(Const sw_id))
@@ -319,6 +382,7 @@ module Pattern = struct
     | TCPSrcPort(tpPort) -> (Field.TCPSrcPort, Value.of_int tpPort)
     | TCPDstPort(tpPort) -> (Field.TCPDstPort, Value.of_int tpPort)
     | VFabric(vfab) -> (Field.VFabric, Value.(Const vfab))
+    | Meta(name,v) -> (fst (Field.Env.lookup env name), Value.(Const v))
 
   let to_hv (f, v) =
     let open Field in
@@ -385,7 +449,12 @@ module Pattern = struct
     | (Switch, Const _)
     | (VSwitch, Const _)
     | (VPort, Const _)
-    | (VFabric, Const _) -> assert false
+    | (VFabric, Const _)
+    | (Meta0, Const _)
+    | (Meta1, Const _)
+    | (Meta2, Const _)
+    | (Meta3, Const _)
+    | (Meta4, Const _) -> assert false
     | _, _ -> raise (FieldValue_mismatch(f, v))
 
 end
@@ -620,7 +689,7 @@ module FDD = struct
 
   include Frenetic_Vlr.Make(Field)(Value)(Action)
 
-  let mk_cont k = mk_leaf Action.(Par.singleton (Seq.singleton K (Value.of_int k)))
+  let mk_cont k = const Action.(Par.singleton (Seq.singleton K (Value.of_int k)))
 
   let conts fdd =
     fold
diff --git a/lib/Frenetic_Fdd.mli b/lib/Frenetic_Fdd.mli
index f1ea43af6..adf7abfd6 100644
--- a/lib/Frenetic_Fdd.mli
+++ b/lib/Frenetic_Fdd.mli
@@ -29,30 +29,41 @@ module Field : sig
    The constructors in type t are listed in the default order, which is acceptable for many
    NetKAT programs.
 
-    This module implements the the [HashCmp] signature from the Frenetic_Vlr package, so it
-    becomes the "V" in VLR. *)
+   This module implements the the [HashCmp] signature from the Frenetic_Vlr package, so it
+   becomes the "V" in VLR. *)
   type t
     = Switch
-      | Vlan
-      | VlanPcp
-      | VSwitch
-      | VPort
-      | EthType
-      | IPProto
-      | EthSrc
-      | EthDst
-      | IP4Src
-      | IP4Dst
-      | TCPSrcPort
-      | TCPDstPort
-      | Location
-      | VFabric
-  [@@deriving sexp]
-
+    | Location
+    | VSwitch
+    | VPort
+    | Vlan
+    | VlanPcp
+    (* SJS: for simplicity, support only up to 5 meta fields for now *)
+    | Meta0
+    | Meta1
+    | Meta2
+    | Meta3
+    | Meta4
+    | EthType
+    | IPProto
+    | EthSrc
+    | EthDst
+    | IP4Src
+    | IP4Dst
+    | TCPSrcPort
+    | TCPDstPort
+    | VFabric
+    [@@deriving sexp, enumerate, enum]
+  type field = t
   include Frenetic_Vlr.HashCmp with type t := t
-  val auto_order : Frenetic_NetKAT.policy -> unit
-  val set_order : t list -> unit
-  val get_order : unit -> t list
+
+  module Env : sig
+    type t
+    val empty : t
+    exception Full
+    val add : t -> string -> Frenetic_NetKAT.meta_init -> bool -> t (* may raise Full *)
+    val lookup : t -> string -> field * (Frenetic_NetKAT.meta_init * bool) (* may raise Not_found *)
+  end
 
   (** [all] returns the default field field ordering *)
   val all : t list
@@ -62,6 +73,9 @@ module Field : sig
 
   val hash : t -> int
 
+  (** [of_hv header_value] converts a NetKAT header_value pair to a field *)
+  val of_hv : ?env:Env.t -> Frenetic_NetKAT.header_val -> t
+
   (** [of_string str] converts a field string to an abstract field.  Throws an exception for unrecognized strings. *)
   val of_string : string -> t
 
@@ -146,7 +160,7 @@ module Pattern : sig
   val equal : t -> t -> bool
 
   (** [of_hv header_value] converts a NetKAT header_value pair to a pattern *)
-  val of_hv : Frenetic_NetKAT.header_val -> t
+  val of_hv : ?env:Field.Env.t -> Frenetic_NetKAT.header_val -> t
 
   (** [to_hv p] converts a pattern to a NetKAT header_value pair *)
   val to_hv : t -> Frenetic_NetKAT.header_val
@@ -183,7 +197,7 @@ module Action : sig
     (* [equal_mod_k s1 s2] Compares two sequences for equality, ignoring K pseudo-field if it exists *)
     val equal_mod_k : Value.t t -> Value.t t -> bool
 
-    (** [to_hvs s] converts to a sequence to an HVS option list, removing K pseudo-field *)
+    (** [to_hvs s] converts to a sequence to an HVS list, removing K pseudo-field *)
     val to_hvs : Value.t t -> (Field.t * Value.t) list
   end
 
@@ -192,7 +206,7 @@ module Action : sig
      only once, which is why we use a Set here.  *)
     include Set.S with type Elt.t = Value.t Seq.t
 
-   (** [to_hvs s] converts to a sequence to an HVS option list applying sequences in the right order *)
+   (** [to_hvs s] converts to a sequence to an HVS list applying sequences in the right order *)
     val to_hvs : t -> (Field.t * Value.t) list
     val mod_k : t -> t
     val compare_mod_k : t -> t -> int
diff --git a/lib/Frenetic_NetKAT.ml b/lib/Frenetic_NetKAT.ml
index fbd8ee786..bbb61a80d 100644
--- a/lib/Frenetic_NetKAT.ml
+++ b/lib/Frenetic_NetKAT.ml
@@ -11,6 +11,7 @@ type payload = Frenetic_OpenFlow.payload [@@deriving sexp]
 type vswitchId = int64 [@@deriving sexp, compare, eq]
 type vportId = int64 [@@deriving sexp, compare, eq]
 type vfabricId = int64 [@@deriving sexp, compare, eq]
+type metaId = string [@@deriving sexp, compare, eq]
 
 let string_of_fastfail = Frenetic_OpenFlow.format_list ~to_string:Int32.to_string
 
@@ -37,6 +38,7 @@ type header_val =
   | VSwitch of vswitchId
   | VPort of vportId
   | VFabric of vfabricId
+  | Meta of metaId * int64
   [@@deriving sexp]
 
 type pred =
@@ -48,6 +50,11 @@ type pred =
   | Neg of pred
   [@@deriving sexp]
 
+type meta_init =
+  | Alias of header_val
+  | Const of int64
+  [@@deriving sexp]
+
 type policy =
   | Filter of pred
   | Mod of header_val
@@ -56,6 +63,10 @@ type policy =
   | Star of policy
   | Link of switchId * portId * switchId * portId
   | VLink of vswitchId * vportId * vswitchId * vportId
+  (* TODO: move to inline records, as soon as derriving sexp supports them, see
+     https://github.com/janestreet/ppx_sexp_conv/issues/9 *)
+  (* | Let of { id : metaId; init : meta_init; body : policy; mut : bool } *)
+  | Let of metaId * meta_init * bool * policy
   [@@deriving sexp]
 
 let id = Filter True
diff --git a/lib/Frenetic_NetKAT.mli b/lib/Frenetic_NetKAT.mli
index c0f6574ec..527089204 100644
--- a/lib/Frenetic_NetKAT.mli
+++ b/lib/Frenetic_NetKAT.mli
@@ -1,8 +1,8 @@
-(** NetKAT Syntax 
+(** NetKAT Syntax
 
   The NetKAT language is central to Frenetic, and we factor out the central types here.  The big actors
   on NetKAT structures are Frenetic_NetKAT_Compiler which compiles NetKAT into flow tables,
-  Frenetic_NetKAT_Parser which turns NetKAT strings (e.g "TcpSrcPort(8080); port := 2") into NetKAT, and 
+  Frenetic_NetKAT_Parser which turns NetKAT strings (e.g "TcpSrcPort(8080); port := 2") into NetKAT, and
   Frenetic_NetKAT_Json which turns JSON-formatted NetKAT into NetKAT
 
 *)
@@ -22,6 +22,7 @@ type payload = Frenetic_OpenFlow.payload [@@deriving sexp]
 type vswitchId = int64 [@@deriving sexp, compare, eq]
 type vportId = int64 [@@deriving sexp, compare, eq]
 type vfabricId = int64 [@@deriving sexp, compare, eq]
+type metaId = string [@@deriving sexp, compare, eq]
 
 (** {2 Policies} *)
 
@@ -50,6 +51,7 @@ type header_val =
   | VSwitch of vswitchId
   | VPort of vportId
   | VFabric of vfabricId
+  | Meta of metaId * int64
   [@@deriving sexp]
 
 type pred =
@@ -61,6 +63,11 @@ type pred =
   | Neg of pred
   [@@deriving sexp]
 
+type meta_init =
+  | Alias of header_val
+  | Const of int64
+  [@@deriving sexp]
+
 type policy =
   | Filter of pred
   | Mod of header_val
@@ -69,6 +76,10 @@ type policy =
   | Star of policy
   | Link of switchId * portId * switchId * portId
   | VLink of vswitchId * vportId * vswitchId * vportId
+  (* TODO: move to inline records, as soon as derriving sexp supports them, see
+     https://github.com/janestreet/ppx_sexp_conv/issues/9 *)
+  (* | Let of { id : metaId; init : meta_init; body : policy; mut : bool } *)
+  | Let of metaId * meta_init * bool * policy
   [@@deriving sexp]
 
 val id : policy
diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml
index 6049efb44..18f196a75 100644
--- a/lib/Frenetic_NetKAT_Compiler.ml
+++ b/lib/Frenetic_NetKAT_Compiler.ml
@@ -15,7 +15,6 @@ module Value = Frenetic_Fdd.Value
 module Par = Action.Par
 module Seq = Action.Seq
 
-
 (*==========================================================================*)
 (* LOCAL COMPILATION                                                        *)
 (*==========================================================================*)
@@ -25,21 +24,28 @@ module FDD = struct
 
   include FDD
 
-  let of_test hv =
-    atom (Pattern.of_hv hv) Action.one Action.zero
-
-  let of_mod hv =
-    let k, v = Pattern.of_hv hv in
+  let of_test env hv =
+    atom (Pattern.of_hv ~env hv) Action.one Action.zero
+
+  let of_mod env hv =
+    let k, v = Pattern.of_hv ~env hv in
+    (* ensure the field is mutable *)
+    begin match hv with
+      | Meta (id,_) ->
+        let _,(_,mut) = Field.Env.lookup env id in
+        if not mut then failwith "cannot modify immutable field"
+      | _ -> ()
+    end;
     const Action.(Par.singleton (Seq.singleton (F k) v))
 
-  let rec of_pred p =
+  let rec of_pred env p =
     match p with
     | True      -> id
     | False     -> drop
-    | Test(hv)  -> of_test hv
-    | And(p, q) -> prod (of_pred p) (of_pred q)
-    | Or (p, q) -> sum (of_pred p) (of_pred q)
-    | Neg(q)    -> map_r Action.negate (of_pred q)
+    | Test(hv)  -> of_test env hv
+    | And(p, q) -> prod (of_pred env p) (of_pred env q)
+    | Or (p, q) -> sum (of_pred env p) (of_pred env q)
+    | Neg(q)    -> map_r Action.negate (of_pred env q)
 
   let seq_tbl = BinTbl.create ~size:1000 ()
 
@@ -81,24 +87,44 @@ module FDD = struct
 
   let star t = star' id t
 
-  let rec of_local_pol_k p k =
+  let hide env t meta_field init =
+    match init with
+    | Const v ->
+      let constr = Pattern.of_hv ~env (Meta (meta_field, v)) in
+      restrict [constr] t
+    | Alias hv ->
+      let alias = Field.of_hv ~env hv in
+      let meta,_ = Field.Env.lookup env meta_field in
+      fold
+        const
+        (fun (field,v) tru fls ->
+          if field = meta then
+            cond (alias, v) tru fls
+          else
+            cond (field,v) tru fls)
+        t
+
+  let rec of_local_pol_k env p k =
     let open Frenetic_NetKAT in
     match p with
-    | Filter   p  -> k (of_pred p)
-    | Mod      m  -> k (of_mod  m)
-    | Union (p, q) -> of_local_pol_k p (fun p' ->
-                        of_local_pol_k q (fun q' ->
+    | Filter   p  -> k (of_pred env p)
+    | Mod      m  -> k (of_mod  env m)
+    | Union (p, q) -> of_local_pol_k env p (fun p' ->
+                        of_local_pol_k env q (fun q' ->
                           k (union p' q')))
-    | Seq (p, q) -> of_local_pol_k p (fun p' ->
+    | Seq (p, q) -> of_local_pol_k env p (fun p' ->
                       if FDD.equal p' FDD.drop then
                         k FDD.drop
                       else
-                        of_local_pol_k q (fun q' ->
+                        of_local_pol_k env q (fun q' ->
                           k (seq p' q')))
-    | Star p -> of_local_pol_k p (fun p' -> k (star p'))
+    | Star p -> of_local_pol_k env p (fun p' -> k (star p'))
+    | Let (field, init, mut, p) ->
+      let env = Field.Env.add env field init mut in
+      of_local_pol_k env p (fun p' -> k (hide env p' field init))
     | Link _ | VLink _ -> raise Non_local
 
-  let rec of_local_pol p = of_local_pol_k p ident
+  let rec of_local_pol ?(env=Field.Env.empty) p = of_local_pol_k env p ident
 
   let to_local_pol =
     fold
@@ -124,7 +150,7 @@ module FDD = struct
             Action.Seq.to_hvs seq |> List.map ~f:fst |> FS.of_list in
           FS.union acc (FS.diff fields seq_fields)) in
         let mods = List.filter mods ~f:(fun (f,_) -> FS.mem harmful f) in
-        List.fold mods ~init:(mk_leaf par) ~f:(fun fdd test ->
+        List.fold mods ~init:(const par) ~f:(fun fdd test ->
           cond test (map_r (Action.demod test) fdd) fdd))
       cond
       fdd
@@ -257,27 +283,31 @@ let to_action ?group_tbl (in_port : Int64.t option) r tests =
   List.fold tests ~init:r ~f:(fun a t -> Action.demod t a)
   |> Action.to_sdn ?group_tbl in_port
 
-let remove_local_fields = FDD.fold
-  (fun r -> mk_leaf (Action.Par.map r ~f:(fun s -> Action.Seq.filteri s ~f:(fun ~key ~data ->
+let erase_meta_fields = FDD.fold
+  (fun r -> const (Action.Par.map r ~f:(fun s -> Action.Seq.filteri s ~f:(fun ~key ~data ->
     match key with
-    | Action.F VPort | Action.F VSwitch -> false
+    | Action.F VPort | Action.F VSwitch
+    | Action.F Meta0 | Action.F Meta1 | Action.F Meta2
+    | Action.F Meta3 | Action.F Meta4 -> false
     | _ -> true))))
   (fun v t f ->
     match v with
-    | Field.VSwitch, _ | Field.VPort, _ -> failwith "uninitialized local field"
-    | _, _ -> mk_branch v t f)
+    | VSwitch, _ | VPort, _
+    | Meta0, _ | Meta1, _ | Meta2, _ | Meta3, _ | Meta4, _  ->
+      failwith "uninitialized meta field"
+    | _, _ -> unchecked_cond v t f)
 
 let mk_branch_or_leaf test t f =
   match t with
   | None -> Some f
-  | Some t -> Some (FDD.mk_branch test t f)
+  | Some t -> Some (FDD.unchecked_cond test t f)
 
 let opt_to_table ?group_tbl options sw_id t =
   let t =
     t
     |> restrict [(Field.Switch, Value.Const sw_id)
                 ;(Field.VFabric, Value.Const (Int64.of_int 1))]
-    |> remove_local_fields
+    |> erase_meta_fields
   in
   let rec next_table_row true_tests all_tests mk_rest t =
     match FDD.unget t with
@@ -299,7 +329,7 @@ let opt_to_table ?group_tbl options sw_id t =
   (loop t [] []) |> List.concat
 
 let rec naive_to_table ?group_tbl options sw_id (t : FDD.t) =
-  let t = FDD.(restrict [(Field.Switch, Value.Const sw_id)] t) |> remove_local_fields in
+  let t = FDD.(restrict [(Field.Switch, Value.Const sw_id)] t) |> erase_meta_fields in
   let rec dfs true_tests all_tests t = match FDD.unget t with
   | Leaf actions ->
     let openflow_instruction = [to_action ?group_tbl (get_inport true_tests) actions true_tests] in
@@ -378,7 +408,7 @@ let eval_pipes (p:Frenetic_NetKAT_Semantics.packet) (t:FDD.t) =
   Frenetic_NetKAT_Semantics.eval_pipes p Action.(to_policy (eval_to_action p t))
 
 let to_dotfile t filename =
-  let t = remove_local_fields t in
+  let t = erase_meta_fields t in
   Out_channel.with_file filename ~f:(fun chan ->
     Out_channel.output_string chan (FDD.to_dot t))
 
@@ -696,9 +726,11 @@ module NetKAT_Automaton = struct
     map_reachable automaton ~order:`Pre ~f:(fun _ (e,d) -> (e, dedup_fdd d))
 
   let rec split_pol (automaton : t0) (pol: Pol.t) : FDD.t * FDD.t * ((int * Pol.t) list) =
+    (* SJS: temporary hack *)
+    let env = Field.Env.empty in
     match pol with
-    | Filter pred -> (FDD.of_pred pred, FDD.drop, [])
-    | Mod hv -> (FDD.of_mod hv, FDD.drop, [])
+    | Filter pred -> (FDD.of_pred env pred, FDD.drop, [])
+    | Mod hv -> (FDD.of_mod env hv, FDD.drop, [])
     | Union (p,q) ->
       let (e_p, d_p, k_p) = split_pol automaton p in
       let (e_q, d_q, k_q) = split_pol automaton q in
diff --git a/lib/Frenetic_NetKAT_Lexer.ml b/lib/Frenetic_NetKAT_Lexer.ml
index e3c156ab0..ab42bf412 100644
--- a/lib/Frenetic_NetKAT_Lexer.ml
+++ b/lib/Frenetic_NetKAT_Lexer.ml
@@ -22,6 +22,7 @@ type token =
   | IP4ADDR of string
   | ANTIQUOT of string
   | STRING_CONSTANT of string
+  | METAID of string
   | EOI
 
 module Token = struct
@@ -40,6 +41,7 @@ module Token = struct
       | INT64 s -> sf "INT64 %s" s
       | ANTIQUOT s -> sf "ANTIQUOT %s" s
       | STRING_CONSTANT s -> sf "STRING_CONSTANT %s" s
+      | METAID s -> sf "METAID %s" s
       | EOI -> sf "EOI"
 
   let print ppf x = Format.pp_print_string ppf (to_string x)
@@ -52,7 +54,7 @@ module Token = struct
   let extract_string =
     function
       | KEYWORD s | INT s | INT64 s | INT32 s |
-        IP4ADDR s | STRING_CONSTANT s -> s
+        IP4ADDR s | STRING_CONSTANT s | METAID s -> s
       | tok ->
           invalid_arg
             ("Cannot extract a string from this token: " ^
@@ -146,10 +148,13 @@ let rec token c = lexer
     | "vlanId" | "vlanPcp" | "ethTyp" | "ipProto" | "tcpSrcPort" | "tcpDstPort"
     | "ethSrc" | "ethDst" | "ip4Src"| "ip4Dst" | "and" | "or" | "not" | "id"
     | "drop" | "if" | "then" | "else" | "filter"  | "pipe" | "query"
-    | "begin" | "end" ->
+    | "begin" | "end" | "let" | "var" | "in" ->
       KEYWORD (L.latin1_lexeme c.lexbuf)
   | "\"" arbitrary_string_without_dbl_quote "\"" ->
+      (* SJS: this looks like an off-by-one bug... *)
       STRING_CONSTANT(L.latin1_sub_lexeme c.lexbuf 1 (L.lexeme_length c.lexbuf - 1))
+  | ident ->
+    METAID (L.latin1_lexeme c.lexbuf)
   | _ -> illegal c
 
 (* Swallow all characters in comments *)
diff --git a/lib/Frenetic_NetKAT_Lexer.mli b/lib/Frenetic_NetKAT_Lexer.mli
index f568ae79a..dad8e69ab 100644
--- a/lib/Frenetic_NetKAT_Lexer.mli
+++ b/lib/Frenetic_NetKAT_Lexer.mli
@@ -1,14 +1,14 @@
-(** Lexical analyzer for NetKAT  
+(** Lexical analyzer for NetKAT
 
-  Mostly the definitions here are used to placate the Camlp4 parser, which wants parsing functions in a 
-  certain way.   So see camlp4 documentation for descriptions of the functions here.   
+  Mostly the definitions here are used to placate the Camlp4 parser, which wants parsing functions in a
+  certain way.   So see camlp4 documentation for descriptions of the functions here.
 *)
 
 module Loc = Camlp4.PreCast.Loc
 
 module Error : sig
   type t
-  exception E of t 
+  exception E of t
 
   val print : Format.formatter -> t -> unit
   val to_string : t -> string
@@ -22,6 +22,7 @@ type token =
   | IP4ADDR of string
   | ANTIQUOT of string
   | STRING_CONSTANT of string
+  | METAID of string
   | EOI
 
 module Token : sig
@@ -48,4 +49,4 @@ module Token : sig
   val extract_string : t -> string
 end
 
-val mk : unit -> Loc.t -> char Stream.t -> (token * Loc.t) Stream.t
\ No newline at end of file
+val mk : unit -> Loc.t -> char Stream.t -> (token * Loc.t) Stream.t
diff --git a/lib/Frenetic_NetKAT_Parser.cppo.ml b/lib/Frenetic_NetKAT_Parser.cppo.ml
index 4218ae99e..58c5072a9 100644
--- a/lib/Frenetic_NetKAT_Parser.cppo.ml
+++ b/lib/Frenetic_NetKAT_Parser.cppo.ml
@@ -1,12 +1,12 @@
 #ifdef AST
   #define MK(arg) <:expr< arg >>
   #define ID(arg) $arg$
-  #define STR(val) $`str:val$
+  #define STR(arg) $`str:arg$
   #define AQ | `ANTIQUOT s -> Syntax.AntiquotSyntax.parse_expr _loc s
 #else
   #define MK(arg) arg
   #define ID(arg) arg
-  #define STR(val) val
+  #define STR(arg) arg
   #define AQ
 #endif
 
@@ -16,6 +16,9 @@ module Gram = MakeGram(Frenetic_NetKAT_Lexer)
 open Frenetic_NetKAT_Lexer
 open Frenetic_NetKAT
 
+(* SJS: hack, but does the job. Reading [undef] will cause sefgault. *)
+let undef : 'a = Obj.magic 0
+
 let nk_pred_eoi = Gram.Entry.mk "nk_pred_eoi"
 let nk_pred = Gram.Entry.mk "nk_pred"
 let nk_pred_atom = Gram.Entry.mk "nk_pred_atom"
@@ -29,6 +32,8 @@ let nk_pol_seq = Gram.Entry.mk "nk_pol_seq"
 let nk_pol_star = Gram.Entry.mk "nk_pol_star"
 let nk_pol_union = Gram.Entry.mk "nk_pol_union"
 let nk_pol_cond = Gram.Entry.mk "nk_pol_cond"
+let nk_pol_meta = Gram.Entry.mk "nk_pol_meta"
+let nk_let = Gram.Entry.mk "nk_let"
 let nk_int64 = Gram.Entry.mk "nk_int64"
 let nk_int32 = Gram.Entry.mk "nk_int32"
 let nk_int = Gram.Entry.mk "nk_int"
@@ -114,6 +119,8 @@ EXTEND Gram
       MK(Test (IP4Dst (ID(n), ID(m))))
     | "ip4Dst"; "="; n = nk_ipv4 ->
       MK(Test (IP4Dst (ID(n), 32l)))
+    | id=METAID; "="; n = nk_int64 ->
+      MK(Test (Meta (STR(id), ID(n))))
     AQ
   ]];
 
@@ -186,6 +193,8 @@ EXTEND Gram
       MK(Mod (TCPSrcPort ID(n)))
     | "tcpDstPort"; ":="; n = nk_int ->
       MK(Mod (TCPDstPort ID(n)))
+    | id=METAID; ":="; n = nk_int64 ->
+      MK(Mod (Meta (STR(id), ID(n))))
     | loc1 = nk_loc; "=>"; loc2 = nk_loc -> MK(
       let (sw1, pt1) = ID(loc1) in
       let (sw2, pt2) = ID(loc2) in
@@ -225,7 +234,42 @@ EXTEND Gram
       MK(Union(Seq(Filter ID(a), ID(p)), Seq(Filter (Neg ID(a)), ID(q))))
   ]];
 
-  nk_pol : [[ p = nk_pol_cond -> p ]];
+  nk_let : [[
+      "let" -> MK(false)
+    | "var" -> MK(true)
+  ]];
+
+  nk_pol_meta : [[
+      p = nk_pol_cond -> p
+    | mut=nk_let; id=METAID; ":="; v=nk_int64; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Const ID(v), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "switch" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (Switch undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "port" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (Location undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ethSrc" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (EthSrc undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ethDst" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (EthDst undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "vlanId" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (Vlan undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "vlanPcp" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (VlanPcp undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ethTyp" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (EthType undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ipProto" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (IPProto undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ip4Src" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (IP4Src (Obj.magic 0, Obj.magic 0)), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "ip4Dst" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (IP4Dst (Obj.magic 0, Obj.magic 0)), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "tcpSrcPort" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (TCPSrcPort undef), ID(mut), ID(p)))
+    | mut=nk_let; id=METAID; ":="; "tcpDstPort" ; "in"; p = nk_pol_meta ->
+      MK(Let (STR(id), Alias (TCPDstPort undef), ID(mut), ID(p)))
+  ]];
+
+  nk_pol : [[ p = nk_pol_meta -> p ]];
 
   nk_pol_eoi: [[ x = nk_pol; `EOI -> x ]];
   nk_pred_eoi: [[ x = nk_pred; `EOI -> x ]];
diff --git a/lib/Frenetic_NetKAT_Semantics.ml b/lib/Frenetic_NetKAT_Semantics.ml
index fdc4f295e..b59a740b0 100644
--- a/lib/Frenetic_NetKAT_Semantics.ml
+++ b/lib/Frenetic_NetKAT_Semantics.ml
@@ -253,5 +253,9 @@ let switches_of_policy (p:policy) =
        collect q acc
     | Link(sw1,_,sw2,_) ->
        sw1 :: sw2 :: acc
-    | VLink _ -> acc in
+    | VLink _ ->
+      acc
+    | Let(_,_,_,p) ->
+      collect p acc
+  in
   collect p [] |> List.dedup |> List.to_list
diff --git a/lib/Frenetic_Vlr.ml b/lib/Frenetic_Vlr.ml
index 3f50e28e1..c0f4d5bb5 100644
--- a/lib/Frenetic_Vlr.ml
+++ b/lib/Frenetic_Vlr.ml
@@ -82,6 +82,8 @@ module Make(V:HashCmp)(L:Lattice)(R:Result) = struct
     else
       T.get (Branch((v, l), t, f))
 
+  let unchecked_cond = mk_branch
+
   let drop = mk_leaf (R.zero)
   let id = mk_leaf (R.one)
 
diff --git a/lib/Frenetic_Vlr.mli b/lib/Frenetic_Vlr.mli
index b6a7ddc10..1a2ebd5da 100644
--- a/lib/Frenetic_Vlr.mli
+++ b/lib/Frenetic_Vlr.mli
@@ -27,7 +27,7 @@ module type Lattice = sig
 
       In other words, elements related to the greatest lower bound should be
       related transitively through [a] and [b], or be equal to the greatest
-      lower bound itself. 
+      lower bound itself.
 
       TODO: tightness doesn't seem to be used anywhere in Frenetic, and can probably
       be removed.  *)
@@ -136,14 +136,6 @@ module Make(V:HashCmp)(L:Lattice)(R:Result) : sig
 
   val get_uid : t -> int (* get_uid t is equivalent to (t : t :> int) *)
 
-  val mk_branch : v -> t -> t -> t
-  (** [mkbranch v t f] Creates (or looks up if it's already been created) a diagram with pattern
-    v, true-branch t and false-branch f.  The t and f branches should already have been created,
-    so you pass indexes here. *)
-
-  val mk_leaf : r -> t
-  (** [mkleaf r] Creates (or looks up) a leaf.  *)
-
   val drop : t (* zero *)
   (** [drop] returns the leaf for a drop operation, which is always present as a leaf node *)
 
@@ -158,6 +150,14 @@ module Make(V:HashCmp)(L:Lattice)(R:Result) : sig
       [v] holds and returns the result [t] if it does hold, and the result [f]
       otherwise. *)
 
+  val cond : v -> t -> t -> t
+  (** [cond v t f] creates a diagram with pattern v, true-branch t and false-branch f. *)
+
+  val unchecked_cond : v -> t -> t -> t
+  (** Unsafe!! [unchecked_cond v t f] behaves like [cond v t f], but always puts the pattern [v]
+      in the root node, without ensuring the FDD-ordering invariant is enforced. Only use this if you know what you are doing! *)
+
+
   val restrict : v list -> t -> t
   (** [restrict vs t] returns a diagram derived from [t] and that agrees with
       [t] when every variable assignment [v] in [vs] is true. This will eliminate
@@ -175,8 +175,6 @@ module Make(V:HashCmp)(L:Lattice)(R:Result) : sig
   (** [prod a b] returns the conjunction of the two diagrams. The [prod]
       operation on the [r] type is used to combine leaf nodes. *)
 
-  val cond : v -> t -> t -> t
-
   val map : (r -> t) -> (v -> t -> t -> t) -> t -> t
   (** [map f h t] traverses t in post order and first maps the leaves using
       f, and then the internal nodes using h, producing a modified diagram. *)
diff --git a/lib_test/Test_Frenetic_Fdd.ml b/lib_test/Test_Frenetic_Fdd.ml
index c3e3039ae..a02013f65 100644
--- a/lib_test/Test_Frenetic_Fdd.ml
+++ b/lib_test/Test_Frenetic_Fdd.ml
@@ -29,7 +29,7 @@ let%test_module _ = (module struct
 
   let all_fields_alpha_order =
     [ EthDst; EthSrc; EthType; IP4Src; IP4Dst; IPProto; Location; Switch; TCPSrcPort;
-      TCPDstPort; Vlan; VlanPcp; VFabric; VPort; VSwitch ]
+      TCPDstPort; Vlan; VlanPcp; VFabric; VPort; VSwitch; Meta0; Meta1; Meta2; Meta3; Meta4 ]
 
   let string_of_list to_string l =
     let strs = List.map l to_string in
@@ -53,7 +53,7 @@ let%test_module _ = (module struct
 
   let%test "Field.get_order gets currently stored field order" =
     let () = set_order all in  (* Set back to default order *)
-    List.nth_exn (get_order ()) 6 = IPProto
+    List.nth_exn (get_order ()) 11 = IPProto
 
   let%test "Field.auto_order sorts referenced Test field to top" =
     let open Frenetic_NetKAT in
diff --git a/lib_test/Test_Frenetic_Vlr.ml b/lib_test/Test_Frenetic_Vlr.ml
index 89c017b5e..88e808093 100644
--- a/lib_test/Test_Frenetic_Vlr.ml
+++ b/lib_test/Test_Frenetic_Vlr.ml
@@ -4,16 +4,16 @@ open Frenetic_Vlr
 
 (* There's very little guidance on how to test Functors in isolation.  The Pa_ounit documentation says
    to place the tests inside the functor itself.  Then the tests are executed when you test concrete modules,
-   but I don't really care for that.  It blends tests into production code, bloating the executable, etc.  
+   but I don't really care for that.  It blends tests into production code, bloating the executable, etc.
 
    I decided to make easy types that fit the signatures, and test the module I get from passing those
    to the functor *)
 
 module PlainLabel = struct
   type t = Var1 | Var2 | Var3  [@@deriving sexp]
-  let to_string = function | Var1 -> "Var1"| Var2 -> "Var2"| Var3 -> "Var3" 
+  let to_string = function | Var1 -> "Var1"| Var2 -> "Var2"| Var3 -> "Var3"
   let compare = Pervasives.compare
-  let hash = function | Var1 -> 1 | Var2 -> 2 | Var3 -> 3 
+  let hash = function | Var1 -> 1 | Var2 -> 2 | Var3 -> 3
 end
 
 module IntUnderDivision = struct
@@ -31,10 +31,10 @@ module IntUnderDivision = struct
     (* I don't think this is correct, but it seems to work as long as numbers are relatively prime, *)
     (gcd a b) > 1
 
-  let meet ?(tight=false) a b = 
-    Some (gcd a b)    
+  let meet ?(tight=false) a b =
+    Some (gcd a b)
 
-  let join ?(tight=false) m n = 
+  let join ?(tight=false) m n =
     (* least common multiple of a and b *)
     match m, n with
     | 0, _ | _, 0 -> Some 0
@@ -56,7 +56,7 @@ end
 
 module TestableVLR = Make(PlainLabel)(IntUnderDivision)(IntUnderAddAndMult)
 
-let%test_module _ = (module struct 
+let%test_module _ = (module struct
   open TestableVLR
 
   let init = clear_cache Int.Set.empty
@@ -69,36 +69,36 @@ let%test_module _ = (module struct
     unget (get (Leaf 3)) = Leaf 3
 
   let%test "S.unget throws an exception if you try to get a diagram not in the cache" =
-    try 
+    try
       init;
       unget (3) = Leaf 3
     with Not_found -> true | _ -> false
 *)
   let%test "S.equal returns true if two subdiagrams are equal" =
     (* S.equal really depends on the diagram-creating procedures doing their job correctly *)
-    let one_idx = mk_leaf 60 in
-    let two_idx = mk_leaf 60 in
-    equal one_idx two_idx    
+    let one_idx = const 60 in
+    let two_idx = const 60 in
+    equal one_idx two_idx
 (*
-  let%test "S.mk_branch is a primitive to create an if-then-else node for the diagram" = 
+  let%test "S.cond is a primitive to create an if-then-else node for the diagram" =
     let () = init in
-    let ten_idx = mk_leaf 10 in
-    let twenty_idx = mk_leaf 20 in
-    unget (mk_branch (Var1,30) ten_idx twenty_idx) = Branch ((Var1,30), ten_idx, twenty_idx)
+    let ten_idx = const 10 in
+    let twenty_idx = const 20 in
+    unget (cond (Var1,30) ten_idx twenty_idx) = Branch ((Var1,30), ten_idx, twenty_idx)
 
-  let%test "S.mk_branch does a quick optimization if the true and false branches are equal" = 
+  let%test "S.cond does a quick optimization if the true and false branches are equal" =
     let () = init in
-    let ten_idx = mk_leaf 10 in
-    unget (mk_branch (Var1,30) ten_idx ten_idx) = Leaf 10
+    let ten_idx = const 10 in
+    unget (cond (Var1,30) ten_idx ten_idx) = Leaf 10
 
-  let%test "S.mk_leaf is a primitive to create a leaf node for the diagram" = 
+  let%test "S.const is a primitive to create a leaf node for the diagram" =
     init;
-    unget (mk_leaf 60) = Leaf 60 
+    unget (const 60) = Leaf 60
 *)
-  let%test "S.mk_leaf doesn't make the same leaf node twice" = 
+  let%test "S.const doesn't make the same leaf node twice" =
     let () = init in
-    let one_idx = mk_leaf 60 in
-    let two_idx = mk_leaf 60 in
+    let one_idx = const 60 in
+    let two_idx = const 60 in
     one_idx = two_idx
 
   let%test "S.drop returns leaf with zero element" =
@@ -112,15 +112,15 @@ let%test_module _ = (module struct
     unget (const 3) = Leaf 3
 
   let%test "S.atom makes a single branch with constant leaves" =
-    let () = init in 
-    let ten_idx = mk_leaf 10 in
-    let twenty_idx = mk_leaf 20 in
-    unget (atom (Var2,3) 10 20) = Branch ((Var2,3), ten_idx, twenty_idx) 
-*)  
+    let () = init in
+    let ten_idx = const 10 in
+    let twenty_idx = const 20 in
+    unget (atom (Var2,3) 10 20) = Branch ((Var2,3), ten_idx, twenty_idx)
+*)
   let two_level_tree =
     let () = init in
     (* Note 17 and 23 below are relatively prime.  If they weren't, the tree wouldn't work *)
-    mk_branch (Var1, 17) (atom (Var2,10) 300 600) (atom (Var1, 23) 100 200)
+    cond (Var1, 17) (atom (Var2,10) 300 600) (atom (Var1, 23) 100 200)
 (*
   let%test "S.restrict returns a smaller decision tree where the given pattern is true" =
     let fdd = two_level_tree in
@@ -142,8 +142,8 @@ let%test_module _ = (module struct
   let%test "S.map_r does the normal map operation, applying function to all leaf nodes and ignoring branch nodes" =
     let fdd = two_level_tree in
     let double x = x * 2 in
-    let expected_fdd = mk_branch (Var1, 17) (atom (Var2,10) 600 1200) (atom (Var1, 23) 200 400) in
-    map_r double fdd = expected_fdd 
+    let expected_fdd = cond (Var1, 17) (atom (Var2,10) 600 1200) (atom (Var1, 23) 200 400) in
+    map_r double fdd = expected_fdd
 
   (* TODO: TEST "sum" *)
 
@@ -156,21 +156,21 @@ let%test_module _ = (module struct
     clear_cache Int.Set.empty;
     zero_idx = drop && one_idx = id
 
-  let%test "S.compressed_size returns number of leaves and branches, not counting duplicates" = 
+  let%test "S.compressed_size returns number of leaves and branches, not counting duplicates" =
     let () = init in
-    let fdd = mk_branch (Var1, 17) (atom (Var2,10) 100 200) (atom (Var1, 23) 100 200) in
+    let fdd = cond (Var1, 17) (atom (Var2,10) 100 200) (atom (Var1, 23) 100 200) in
     (* The two leaves 100 and 200 are counted only once apiece *)
     compressed_size fdd = 5
 
-  let%test "S.uncompressed_size returns number of leaves and branches, counting duplicates" = 
+  let%test "S.uncompressed_size returns number of leaves and branches, counting duplicates" =
     let () = init in
-    let fdd = mk_branch (Var1, 17) (atom (Var2,10) 100 200) (atom (Var1, 23) 100 200) in
+    let fdd = cond (Var1, 17) (atom (Var2,10) 100 200) (atom (Var1, 23) 100 200) in
     uncompressed_size fdd = 7
 end)
   (* TODO: TEST "to_dot" *)
 (*
   let%test "S.refs returns set of diagrams" =
-    let () = init in 
+    let () = init in
     let fdd = atom (Var1, 23) 100 200 in
     let first_child = const 100 in
     let second_child = const 200 in