From f094632afad73cbfa22bc497f140c6994799ce5e Mon Sep 17 00:00:00 2001
From: Bastien Rousseau <49273142+BastienRousseau@users.noreply.github.com>
Date: Thu, 3 Aug 2023 15:42:14 +0200
Subject: [PATCH] Sealing (#1)

* Add support for sealing

* Fixing parser + display style for interactive

* GetOType and GetWType instructions

* Modification of the internal model for permission: every kind of permission/word type is a constant that is encoded at parsing-time.

* Test cases for sealing + fixing/cleaning tests

* Non-trivial test case using sealing (sealing_counter)
---
 lib/ast.ml                                |  17 +-
 lib/encode.ml                             | 589 ++++++++--------------
 lib/interactive_ui.ml                     | 114 +++--
 lib/ir.ml                                 | 120 ++++-
 lib/irreg.ml                              |  27 +-
 lib/lexer.mll                             |  21 +-
 lib/lexer_regfile.mll                     |   9 +
 lib/machine.ml                            | 168 ++++--
 lib/parser.mly                            |  49 +-
 lib/parser_regfile.mly                    |  29 +-
 lib/pretty_printer.ml                     |  66 ++-
 lib/program.ml                            |   4 +-
 tests/dune                                |   4 +-
 tests/test_files/base.reg                 |   4 +
 tests/test_files/neg/bad_encoding1.s      |   3 +
 tests/test_files/neg/bad_encoding2.s      |   2 +
 tests/test_files/neg/bad_encoding3.s      |   2 +
 tests/test_files/neg/bad_flow1.s          |   2 +-
 tests/test_files/neg/bad_flow2.s          |   2 +-
 tests/test_files/neg/bad_flow3.s          |   2 +
 tests/test_files/neg/bad_flow_seal1.s     |   3 +
 tests/test_files/neg/bad_flow_seal2.s     |   3 +
 tests/test_files/neg/bad_perm_seal.s      |   3 +
 tests/test_files/neg/bad_perm_unseal.s    |   4 +
 tests/test_files/neg/bad_sealing_int.s    |   2 +
 tests/test_files/neg/bad_sealing_sealed.s |   3 +
 tests/test_files/neg/lea_perm_not_entry.s |   2 +-
 tests/test_files/pos/get_otype.s          |   9 +
 tests/test_files/pos/get_wtype.s          |  15 +
 tests/test_files/pos/seal_unseal.s        |   9 +
 tests/test_files/pos/sealing_counter.s    | 105 ++++
 tests/tester.ml                           |  66 ++-
 tests/{test.ml => tests.ml}               | 117 +++--
 33 files changed, 1019 insertions(+), 556 deletions(-)
 create mode 100644 tests/test_files/base.reg
 create mode 100644 tests/test_files/neg/bad_encoding1.s
 create mode 100644 tests/test_files/neg/bad_encoding2.s
 create mode 100644 tests/test_files/neg/bad_encoding3.s
 create mode 100644 tests/test_files/neg/bad_flow3.s
 create mode 100644 tests/test_files/neg/bad_flow_seal1.s
 create mode 100644 tests/test_files/neg/bad_flow_seal2.s
 create mode 100644 tests/test_files/neg/bad_perm_seal.s
 create mode 100644 tests/test_files/neg/bad_perm_unseal.s
 create mode 100644 tests/test_files/neg/bad_sealing_int.s
 create mode 100644 tests/test_files/neg/bad_sealing_sealed.s
 create mode 100644 tests/test_files/pos/get_otype.s
 create mode 100644 tests/test_files/pos/get_wtype.s
 create mode 100644 tests/test_files/pos/seal_unseal.s
 create mode 100644 tests/test_files/pos/sealing_counter.s
 rename tests/{test.ml => tests.ml} (59%)

diff --git a/lib/ast.ml b/lib/ast.ml
index 0b9d92a..296bdf6 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -1,9 +1,11 @@
 (* Type definitions for the syntax AST *)
 type regname = PC | Reg of int
 type perm = O | E | RO | RX | RW | RWX
-type const_perm = Const of Z.t | Perm of perm
-type reg_or_const = Register of regname | CP of const_perm (* TODO: separate into two types *)
-type word = I of Z.t | Cap of perm * Z.t * Z.t * Z.t
+type wtype = W_I | W_Cap | W_SealRange | W_Sealed
+type seal_perm = bool * bool
+type reg_or_const = Register of regname | Const of Z.t
+type sealable = Cap of perm * Z.t * Z.t * Z.t | SealRange of seal_perm * Z.t * Z.t * Z.t
+type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable
 type machine_op
   = Jmp of regname
   | Jnz of regname * regname
@@ -19,11 +21,14 @@ type machine_op
   | Lea of regname * reg_or_const
   | Restrict of regname * reg_or_const
   | SubSeg of regname * reg_or_const * reg_or_const
-  | IsPtr of regname * regname
-  | GetP of regname * regname
   | GetB of regname * regname
   | GetE of regname * regname
   | GetA of regname * regname
+  | GetP of regname * regname
+  | GetOType of regname * regname
+  | GetWType of regname * regname
+  | Seal of regname * regname * regname
+  | UnSeal of regname * regname * regname
   | Fail
   | Halt
 
@@ -37,4 +42,4 @@ let compare_regname (r1 : regname) (r2: regname) : int =
   | Reg _, PC -> 1
   | Reg i, Reg j -> Int.compare i j
 
-let const n = CP (Const (Z.of_int n))
+let const n = Const (Z.of_int n)
diff --git a/lib/encode.ml b/lib/encode.ml
index 0b8047c..0698fe9 100644
--- a/lib/encode.ml
+++ b/lib/encode.ml
@@ -2,20 +2,36 @@ open Ast
 
 exception DecodeException of string
 
-(* Encodings of permissions satisfy
- * lattice structure by:
- * - join : bitwise or
- * - meet : bitwise and
- * - x flowsto y : y join x = y *)
-let encode_perm (p : perm) : Z.t =
-  Z.of_int @@
-  match p with
-  | O -> 0b000
-  | E -> 0b001
-  | RO -> 0b100
-  | RX -> 0b101
-  | RW -> 0b110
-  | RWX -> 0b111
+let encode_wtype (w : wtype) =
+  Ir.encode_wtype
+  (match w with
+   | W_I -> Ir.W_I
+   | W_Cap -> Ir.W_Cap
+   | W_SealRange -> Ir.W_SealRange
+   | W_Sealed -> Ir.W_Sealed)
+
+let decode_wtype (z : Z.t) : wtype =
+  let decode_wt_exception = fun _ -> raise @@ DecodeException "Error decoding wtype: unexpected encoding" in
+  let b0 = Z.testbit z 0 in
+  let b1 = Z.testbit z 1 in
+  if Z.(z > (of_int 0b11))
+  then decode_wt_exception ()
+  else
+  match (b1,b0) with
+  | (false, false) -> W_I
+  | (false, true) -> W_Cap
+  | (true, false) -> W_SealRange
+  | (true, true) -> W_Sealed
+
+let encode_perm (p : perm) =
+  Ir.encode_perm
+    (match p with
+     | O -> Ir.O
+     | E -> Ir.E
+     | RO -> Ir.RO
+     | RX -> Ir.RX
+     | RW -> Ir.RW
+     | RWX -> Ir.RWX)
 
 let decode_perm (i : Z.t) : perm =
   let decode_perm_exception = fun _ -> raise @@ DecodeException "Error decoding permission: unexpected encoding" in
@@ -34,6 +50,16 @@ let decode_perm (i : Z.t) : perm =
   | (true, true, true)    -> RWX
   | _ -> decode_perm_exception ()
 
+let encode_seal_perm (sp : seal_perm) : Z.t = Ir.encode_seal_perm sp
+
+let decode_seal_perm (i : Z.t) : seal_perm =
+  let decode_perm_exception = fun _ -> raise @@ DecodeException "Error decoding sealing permission: unexpected encoding" in
+  let b0 = Z.testbit i 0 in
+  let b1 = Z.testbit i 1 in
+  if Z.(i > (of_int 0b11))
+  then decode_perm_exception ()
+  else (b1,b0)
+
 let encode_reg (r : regname) : Z.t =
   match r with
   | PC -> Z.zero
@@ -44,36 +70,6 @@ let decode_reg (i : Z.t) : regname =
   then PC
   else Reg (Z.to_int @@ Z.pred i)
 
-(* Interleave two integers bitwise. 
- * Example: x = 0b101 and y = 0b110
- * results in 0b111001. *)
-let rec interleave_int (x : Z.t) (y : Z.t) : Z.t =
-  let open Z in
-  if x = zero && y = zero
-  then zero
-  else
-    let x1 = x land one in
-    let y1 = (y land one) lsl 1 in
-    let x2 = x asr 1 in
-    let y2 = y asr 1 in
-    x1 + y1 + ((interleave_int x2 y2) lsl 2)
-
-(* Encode two integers by interleaving their 
- * absolute values bitwise, followed
- * by two bits representing signs.
- *)
-let encode_int_int (x : Z.t) (y : Z.t) =
-  let sign_bits = Z.of_int @@ begin
-    match (Z.sign y, Z.sign x) with
-      | (-1, -1) -> 0b11
-      | (-1, (0|1))  -> 0b10
-      | ((0|1), -1)  -> 0b01
-      | ((0|1), (0|1)) -> 0b00
-      | _ -> assert false
-  end in
-  let interleaved = interleave_int (Z.abs x) (Z.abs y) in
-  Z.(sign_bits + (interleaved lsl 2))
-
 let rec split_int (i : Z.t) : Z.t * Z.t =
   let open Z in
   if i = zero
@@ -93,6 +89,8 @@ let decode_int (i : Z.t) : Z.t * Z.t =
   | (true, false) -> (Z.neg x, y)
   | (false, true) -> (x, Z.neg y)
   | (false, false) -> (x, y)
+
+let encode_int_int = Ir.encode_int_int
                       
 let (~$) = Z.(~$)
 
@@ -101,15 +99,13 @@ let encode_machine_op (s : machine_op): Z.t =
   let const_convert opcode c = begin
     match c with
     | Register r -> opcode, encode_reg r
-    | CP (Const i) -> Z.(succ opcode, i)
-    | CP (Perm p) -> Z.(succ @@ succ opcode, encode_perm p)
+    | Const n ->  Z.(succ opcode, n)
   end in
   let two_const_convert opcode c1 c2 = begin
     let (opc1, c1_enc) = begin
       match c1 with
       | Register r -> opcode, encode_reg r
-      | CP (Const i) -> Z.(opcode + ~$3, i)
-      | CP (Perm p) -> Z.(opcode + ~$6, encode_perm p)
+      | Const i -> Z.(opcode + ~$2, i)
     end in
     let (opc2, c2_enc) = const_convert opc1 c2 in
     (opc2, encode_int_int c1_enc c2_enc)
@@ -117,62 +113,66 @@ let encode_machine_op (s : machine_op): Z.t =
   match s with
   | Jmp r -> ~$0x00 ^! (encode_reg r)
   | Jnz (r1, r2) -> ~$0x01 ^! encode_int_int (encode_reg r1) (encode_reg r2)
-  | Move (r, c) -> begin (* 0x02, 0x03, 0x04 *)
+  | Move (r, c) -> begin (* 0x02, 0x03 *)
       let (opc, c_enc) = const_convert ~$0x02 c in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Load (r1, r2) -> ~$0x05 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | Store (r, c) -> begin (* 0x06, 0x07, 0x08 *)
-      let (opc, c_enc) = const_convert ~$0x06 c in
+  | Load (r1, r2) -> ~$0x04 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | Store (r, c) -> begin (* 0x05, 0x06  *)
+      let (opc, c_enc) = const_convert ~$0x05 c in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Add (r, c1, c2) -> begin (* 0x09 to 0x11 *)
-      let (opc, c_enc) = two_const_convert ~$0x09 c1 c2 in
+  | Add (r, c1, c2) -> begin (* 0x07, 0x08, 0x09, 0x0a *)
+      let (opc, c_enc) = two_const_convert ~$0x07 c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Sub (r, c1, c2) -> begin (* 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1a *)
-      let (opc, c_enc) = two_const_convert ~$0x12 c1 c2 in
+  | Sub (r, c1, c2) -> begin (* 0x0b, 0x0c, 0x0d, 0x0e *)
+      let (opc, c_enc) = two_const_convert ~$0x0b c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
 
-  | Mul (r, c1, c2) -> begin (* 0x1b, 0x1c, 0x1d, 0x1e, 0x1f, 0x20, 0x21, 0x22, 0x23 *)
-      let (opc, c_enc) = two_const_convert ~$0x1b c1 c2 in
+  | Mul (r, c1, c2) -> begin (* 0x0f, 0x10, 0x11, 0x12 *)
+      let (opc, c_enc) = two_const_convert ~$0x0f c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Rem (r, c1, c2) -> begin (* 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2a, 0x2b, 0x2c *)
-      let (opc, c_enc) = two_const_convert ~$0x24 c1 c2 in
+  | Rem (r, c1, c2) -> begin (* 0x13, 0x14, 0x15, 0x16 *)
+      let (opc, c_enc) = two_const_convert ~$0x13 c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Div (r, c1, c2) -> begin (* 0x2d, 0x2e, 0x2f, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35 *)
-      let (opc, c_enc) = two_const_convert ~$0x2d c1 c2 in
+  | Div (r, c1, c2) -> begin (* 0x17, 0x18, 0x19, 0x1a *)
+      let (opc, c_enc) = two_const_convert ~$0x17 c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
 
-
-  | Lt (r, c1, c2) -> begin (* 0x36, 0x37, 0x38, 0x39, 0x3a, 0x3b, 0x3c, 0x3d, 0x3e *)
-      let (opc, c_enc) = two_const_convert ~$0x36 c1 c2 in
+  | Lt (r, c1, c2) -> begin (* 0x1b, 0x1c, 0x1d, 0x1e *)
+      let (opc, c_enc) = two_const_convert ~$0x1b c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Lea (r, c) -> begin (* 0x3f, 0x40, 0x41 *)
-      let (opc, c_enc) = const_convert ~$0x3f c in
+  | Lea (r, c) -> begin (* 0x1f, 0x20 *)
+      let (opc, c_enc) = const_convert ~$0x1f c in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | Restrict (r, c) -> begin (* 0x42, 0x43, 0x44 *)
-      let (opc, c_enc) = const_convert ~$0x42 c in
+  | Restrict (r, c) -> begin (* 0x21, 0x22 *)
+      let (opc, c_enc) = const_convert ~$0x21 c in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
 
-  | SubSeg (r, c1, c2) -> begin (* 0x45 to 0x4d *)
-      let (opc, c_enc) = two_const_convert ~$0x45 c1 c2 in
+  | SubSeg (r, c1, c2) -> begin (* 0x23, 0x24, 0x25, 0x26 *)
+      let (opc, c_enc) = two_const_convert ~$0x23 c1 c2 in
       opc ^! (encode_int_int (encode_reg r) c_enc)
     end
-  | IsPtr (r1, r2) -> ~$0x4e ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | GetP (r1, r2) -> ~$0x4f ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | GetB (r1, r2) -> ~$0x50 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | GetE (r1, r2) -> ~$0x51 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | GetA (r1, r2) -> ~$0x52 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
-  | Fail -> ~$0x53
-  | Halt -> ~$0x54
+  | GetB (r1, r2) -> ~$0x27 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | GetE (r1, r2) -> ~$0x28 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | GetA (r1, r2) -> ~$0x29 ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | GetP (r1, r2) -> ~$0x2a ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | GetOType (r1, r2) -> ~$0x2b ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | GetWType (r1, r2) -> ~$0x2c ^! (encode_int_int (encode_reg r1) (encode_reg r2))
+  | Seal (r1, r2, r3) ->
+      ~$0x2d ^! (encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)))
+  | UnSeal (r1, r2, r3) ->
+      ~$0x2e ^! (encode_int_int (encode_reg r1) (encode_int_int (encode_reg r2) (encode_reg r3)))
+  | Fail -> ~$0x2f
+  | Halt -> ~$0x30
 
 let decode_machine_op (i : Z.t) : machine_op =
   let opc = Z.extract i 0 8 in
@@ -202,428 +202,275 @@ let decode_machine_op (i : Z.t) : machine_op =
     let (r_enc, c_enc) = decode_int payload in
     let r = decode_reg r_enc in
     let c = Const c_enc in
-    Move (r, CP c)
-  end else
-  if opc = ~$0x04 (* register perm *)
-  then begin
-    let (r_enc, c_enc) = decode_int payload in
-    let r = decode_reg r_enc in
-    (* let p = Perm (decode_perm c_enc) in  *)
-    let p = decode_perm c_enc in
-    Move (r, CP (Perm p))
+    Move (r, c)
   end else
+
   (* Load *)
-  if opc = ~$0x05
+  if opc = ~$0x04
   then begin
     let (r1_enc, r2_enc) = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
     Load (r1, r2)
   end else
+
   (* Store *)
-  if opc = ~$0x06 (* register register *)
+  if opc = ~$0x05 (* register register *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r1 = decode_reg r_enc in
     let r2 = Register (decode_reg c_enc) in
     Store (r1, r2)
   end else
-  if opc = ~$0x07 (* register const *)
+  if opc = ~$0x06 (* register const *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r = decode_reg r_enc in
     let c = Const c_enc in
-    Store (r, CP c)
-  end else
-  if opc = ~$0x08 (* register perm *)
-  then begin
-    let (r_enc, c_enc) = decode_int payload in
-    let r = decode_reg r_enc in
-    let p = Perm (decode_perm c_enc) in
-    Store (r, CP p)
+    Store (r, c)
   end else
+
   (* Add *)
-  if ~$0x08 < opc && opc < ~$0x0c
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x09 then Register (decode_reg c2_enc) else
-      if opc = ~$0x0a then CP (Const c2_enc) else
-      CP (Perm (decode_perm c2_enc))
-    end in
-    Add (r, c1, c2)
-  end else
-  if ~$0x0b < opc && opc < ~$0x0f
+  if ~$0x07 <= opc && opc <= ~$0x0a
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x0c then Register (decode_reg c2_enc) else
-      if opc = ~$0x0d then CP (Const c2_enc) else
-      CP (Perm (decode_perm c2_enc))
-    end in
-    Add (r, c1, c2)
-  end else
-  if ~$0x0e < opc && opc < ~$0x12
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x0f then Register (decode_reg c2_enc) else
-      if opc = ~$0x10 then CP (Const c2_enc) else
-      CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x07 || opc = ~$0x08
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x07 || opc = ~$0x09
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Add (r, c1, c2)
   end else
+
   (* Sub *)
-  if ~$0x11 < opc && opc < ~$0x15
+  if ~$0x0b <= opc && opc <= ~$0x0e
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x12 then Register (decode_reg c2_enc) else
-      if opc = ~$0x13 then CP (Const c2_enc) else
-      CP (Perm (decode_perm c2_enc))
-    end in
-    Sub (r, c1, c2)
-  end else
-  if ~$0x14 < opc && opc < ~$0x18
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x15 then Register (decode_reg c2_enc) else
-      if opc = ~$0x16 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Sub (r, c1, c2)
-  end else
-  if ~$0x17 < opc && opc < ~$0x1b
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x18 then Register (decode_reg c2_enc) else
-      if opc = ~$0x19 then CP (Const c2_enc) else
-      CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x0b || opc = ~$0x0c
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x0b || opc = ~$0x0d
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Sub (r, c1, c2)
   end else
 
-
-
-
-
-
-(* Mul *)
-  if ~$0x1a < opc && opc < ~$0x1e
+  (* Mul *)
+  if ~$0x0f <= opc && opc <= ~$0x12
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x1b then Register (decode_reg c2_enc) else
-      if opc = ~$0x1c then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Mul (r, c1, c2)
-  end else
-  if ~$0x1d < opc && opc < ~$0x21
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x1e then Register (decode_reg c2_enc) else
-      if opc = ~$0x1f then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Mul (r, c1, c2)
-  end else
-  if ~$0x20 < opc && opc < ~$0x24
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x21 then Register (decode_reg c2_enc) else
-      if opc = ~$0x22 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x0f || opc = ~$0x10
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x0f || opc = ~$0x11
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Mul (r, c1, c2)
   end else
 
   (* Rem *)
-  if ~$0x23 < opc && opc < ~$0x27
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x24 then Register (decode_reg c2_enc) else
-      if opc = ~$0x25 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Rem (r, c1, c2)
-  end else
-  if ~$0x26 < opc && opc < ~$0x2a
+  if ~$0x13 <= opc && opc <= ~$0x16
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x27 then Register (decode_reg c2_enc) else
-      if opc = ~$0x28 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x13 || opc = ~$0x14
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x13 || opc = ~$0x15
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Rem (r, c1, c2)
   end else
-  if ~$0x29 < opc && opc < ~$0x2d
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x2a then Register (decode_reg c2_enc) else
-      if opc = ~$0x2b then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Rem (r, c1, c2)
-  end
-  else
+
   (* Div *)
-  if ~$0x2c < opc && opc < ~$0x30
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x2d then Register (decode_reg c2_enc) else
-      if opc = ~$0x2e then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Div (r, c1, c2)
-  end else
-  if ~$0x2f < opc && opc < ~$0x33
+  if ~$0x17 <= opc && opc <= ~$0x1a
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x30 then Register (decode_reg c2_enc) else
-      if opc = ~$0x31 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x17 || opc = ~$0x18
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x17 || opc = ~$0x19
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Div (r, c1, c2)
   end else
-  if ~$0x32 < opc && opc < ~$0x36
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x33 then Register (decode_reg c2_enc) else
-      if opc = ~$0x34 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Div (r, c1, c2)
-  end
-  else
 
   (* Lt *)
-  if ~$0x35 < opc && opc < ~$0x39
+  if ~$0x1b <= opc && opc <= ~$0x1e
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x36 then Register (decode_reg c2_enc) else
-      if opc = ~$0x37 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Lt (r, c1, c2)
-  end else
-  if ~$0x37 < opc && opc < ~$0x3c
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x39 then Register (decode_reg c2_enc) else
-      if opc = ~$0x3a then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    Lt (r, c1, c2)
-  end else
-  if ~$0x3b < opc && opc < ~$0x3f
-  then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x3c then Register (decode_reg c2_enc) else
-      if opc = ~$0x3d then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x1b || opc = ~$0x1c
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x1b || opc = ~$0x1d
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     Lt (r, c1, c2)
   end else
+
   (* Lea *)
-  if opc = ~$0x3f (* register register *)
+  if opc = ~$0x1f (* register register *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r1 = decode_reg r_enc in
     let r2 = Register (decode_reg c_enc) in
     Lea (r1, r2)
   end else
-  if opc = ~$0x40 (* register const *)
+  if opc = ~$0x20 (* register const *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r = decode_reg r_enc in
     let c = Const c_enc in
-    Lea (r, CP c)
-  end else
-  if opc = ~$0x41 (* register perm *)
-  then begin
-    let (r_enc, c_enc) = decode_int payload in
-    let r = decode_reg r_enc in
-    let p = Perm (decode_perm c_enc) in
-    Lea (r, CP p)
+    Lea (r, c)
   end else
+
   (* Restrict *)
-  if opc = ~$0x42 (* register register *)
+  if opc = ~$0x21 (* register register *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r1 = decode_reg r_enc in
     let r2 = Register (decode_reg c_enc) in
     Restrict (r1, r2)
   end else
-  if opc = ~$0x43 (* register const *)
+  if opc = ~$0x22 (* register const *)
   then begin
     let (r_enc, c_enc) = decode_int payload in
     let r = decode_reg r_enc in
     let c = Const c_enc in
-    Restrict (r, CP c)
-  end else
-  if opc = ~$0x44 (* register perm *)
-  then begin
-    let (r_enc, c_enc) = decode_int payload in
-    let r = decode_reg r_enc in
-    let p = Perm (decode_perm c_enc) in
-    Restrict (r, CP p)
+    Restrict (r, c)
   end else
-  (* SubSeg *)
-  if ~$0x44 < opc && opc < ~$0x48
+
+  (* Subseg *)
+  if ~$0x23 <= opc && opc <= ~$0x26
   then begin
     let (r_enc, payload') = decode_int payload in
     let (c1_enc, c2_enc) = decode_int payload' in
     let r = decode_reg r_enc in
-    let c1 = Register (decode_reg c1_enc) in
-    let c2 = begin
-      if opc = ~$0x45 then Register (decode_reg c2_enc) else
-      if opc = ~$0x46 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
+    let c1 =
+      if opc = ~$0x23 || opc = ~$0x24
+      then Register (decode_reg c1_enc)
+      else Const c1_enc
+    in
+    let c2 =
+      if opc = ~$0x23 || opc = ~$0x25
+      then Register (decode_reg c2_enc)
+      else Const c2_enc
+    in
     SubSeg (r, c1, c2)
   end else
-  if ~$0x47 < opc && opc < ~$0x4b
+
+  (* GetB *)
+  if opc = ~$0x27
   then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Const c1_enc) in
-    let c2 = begin
-      if opc = ~$0x48 then Register (decode_reg c2_enc) else
-      if opc = ~$0x49 then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    SubSeg (r, c1, c2)
+    let (r1_enc, r2_enc) = decode_int payload in
+    let r1 = decode_reg r1_enc in
+    let r2 = decode_reg r2_enc in
+    GetB (r1, r2)
   end else
-  if ~$0x4a < opc && opc < ~$0x4e
+  (* GetE *)
+  if opc = ~$0x28
   then begin
-    let (r_enc, payload') = decode_int payload in
-    let (c1_enc, c2_enc) = decode_int payload' in
-    let r = decode_reg r_enc in
-    let c1 = CP (Perm (decode_perm c1_enc)) in
-    let c2 = begin
-      if opc = ~$0x4b then Register (decode_reg c2_enc) else
-      if opc = ~$0x4c then CP (Const c2_enc) else
-        CP (Perm (decode_perm c2_enc))
-    end in
-    SubSeg (r, c1, c2)
+    let (r1_enc, r2_enc) = decode_int payload in
+    let r1 = decode_reg r1_enc in
+    let r2 = decode_reg r2_enc in
+    GetE (r1, r2)
   end else
-  (* IsPtr *)
-  if opc = ~$0x4e
+  (* GetA *)
+  if opc = ~$0x29
   then begin
     let (r1_enc, r2_enc) = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
-    IsPtr (r1, r2)
+    GetA (r1, r2)
   end else
-
 (* GetP *)
-  if opc = ~$0x4f
+  if opc = ~$0x2a
   then begin
     let (r1_enc, r2_enc) = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
     GetP (r1, r2)
   end else
-  (* GetB *)
-  if opc = ~$0x50
+(* GetOType *)
+  if opc = ~$0x2b
   then begin
     let (r1_enc, r2_enc) = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
-    GetB (r1, r2)
+    GetOType (r1, r2)
   end else
-  (* GetE *)
-  if opc = ~$0x51
+(* GetWType *)
+  if opc = ~$0x2c
   then begin
     let (r1_enc, r2_enc) = decode_int payload in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
-    GetE (r1, r2)
+    GetWType (r1, r2)
   end else
-  (* GetA *)
-  if opc = ~$0x52
+
+  (* Seal *)
+  if opc = ~$0x2d
   then begin
-    let (r1_enc, r2_enc) = decode_int payload in
+    let (r1_enc, payload') = decode_int payload in
+    let (r2_enc, r3_enc) = decode_int payload' in
     let r1 = decode_reg r1_enc in
     let r2 = decode_reg r2_enc in
-    GetA (r1, r2)
+    let r3 = decode_reg r3_enc in
+    Seal (r1, r2, r3)
+  end else
+  (* UnSeal *)
+  if opc = ~$0x2e
+  then begin
+    let (r1_enc, payload') = decode_int payload in
+    let (r2_enc, r3_enc) = decode_int payload' in
+    let r1 = decode_reg r1_enc in
+    let r2 = decode_reg r2_enc in
+    let r3 = decode_reg r3_enc in
+    UnSeal (r1, r2, r3)
   end else
 
  (* Fail *)
-  if opc = ~$0x53
+  if opc = ~$0x2f
   then Fail
   else
   (* Halt *)
-  if opc = ~$0x54
+  if opc = ~$0x30
   then Halt
   else raise @@
     DecodeException
diff --git a/lib/interactive_ui.ml b/lib/interactive_ui.ml
index 3debab8..d4a03b9 100644
--- a/lib/interactive_ui.ml
+++ b/lib/interactive_ui.ml
@@ -23,6 +23,13 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
         (I.string attr (Pretty_printer.string_of_perm p))
   end
 
+  module SealPerm = struct
+    let width = 5
+    let ui ?(attr = A.empty) (p: Ast.seal_perm) =
+      I.hsnap ~align:`Left width
+        (I.string attr (Pretty_printer.string_of_seal_perm p))
+  end
+
   module Addr = struct
     (* width of an address as a number of hex digits *)
     let width =
@@ -83,27 +90,73 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
       ) else s
   end
 
+  let sealed_style = A.fg (A.gray 14)
+  let cap_style = A.fg A.lightmagenta
+  let sealed_cap_style = A.fg A.magenta
+   (* TODO use rgb_888 to define the right colors *)
+  let sealrange_style = A.fg A.lightcyan
+  let sealed_sealrange_style = A.fg A.cyan
+
+  module Sealable = struct
+    let width =
+      Perm.width + 1 (* space *) +
+      Addr_range.width + 1 (* space *) +
+      Addr.width
+
+    let ui ?(attr = A.empty) (sb: Ast.sealable) =
+      (* - <perm> <range> <addr> if it's a capability
+         (with padding after the range to right-align <addr>)
+         - <perm> <range> <otype> if it's a sealrange
+           (with padding after the range to right-align <addr>) *)
+      match sb with
+      | Cap (p, b, e, a) ->
+        let attr =
+          if attr = sealed_style then sealed_cap_style else cap_style
+        in
+        (I.hsnap ~align:`Left width
+           (Perm.ui ~attr p
+            <|> I.string A.empty " "
+            <|> Addr_range.ui ~attr (b, e))
+         </>
+         I.hsnap ~align:`Right width (Addr.ui ~attr a))
+      | SealRange (p, b, e, a) ->
+        let attr =
+          if attr = sealed_style then sealed_sealrange_style else sealrange_style
+        in
+        (I.hsnap ~align:`Left width
+           (SealPerm.ui ~attr p
+            <|> I.string A.empty " "
+            <|> Addr_range.ui ~attr (b, e))
+         </>
+         I.hsnap ~align:`Right width (Addr.ui ~attr a))
+  end
+
   module Word = struct
     (* a word is printed as:
-       - <perm> <range> <addr> if it's a capability
+       - <sealable> if it's a sealable
+       - { _<otype>: <sealable> } if it's a sealed
          (with padding after the range to right-align <addr>)
        - <int> if it's an integer
     *)
     let width =
-      Perm.width + 1 (* space *) +
-      Addr_range.width + 1 (* space *) +
-      Addr.width
+      1 (* { *)
+      + Addr.width (* otype *)
+      + 2 (* colon and space  *)
+      + Sealable.width
+      + 1 (* } *)
 
-    let ui ?(attr = A.empty) (w: Machine.word) =
+    let ui ?(attr = A.empty) (w: Ast.word) =
       match w with
-      | I z -> I.hsnap ~align:`Right width (I.string attr (Int.ui width z))
-      | Cap (p, b, e, a) ->
-          (I.hsnap ~align:`Left width
-             (Perm.ui ~attr p
-              <|> I.string A.empty " "
-              <|> Addr_range.ui ~attr (b, e))
-           </>
-           I.hsnap ~align:`Right width (Addr.ui a))
+      | I z -> I.hsnap ~align:`Right width (I.string attr (Int.ui width z) <|> I.string A.empty " ")
+      | Sealable sb -> I.hsnap ~align:`Right width ((Sealable.ui ~attr sb) <|> I.string A.empty " ")
+      | Sealed (o,sb) ->
+        let attr = sealed_style in
+        I.hsnap ~align:`Right width
+           (I.string attr "{"
+           <|> (I.string attr (Int.ui width o))
+           <|> I.string attr ": "
+           <|> (Sealable.ui ~attr sb)
+           <|> I.string attr "}")
   end
 
   module Regname = struct
@@ -153,26 +206,27 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
 
     let is_in_r_range r a =
       match r with
-      | Machine.I _ -> `No
-      | Cap (_, b, e, _) ->
-        if a >= b && a < e then (
-          if a = b then `AtStart
-          else if a = Z.(e- ~$1) then `AtLast
-          else `InRange
-        ) else `No
+      | Ast.Sealable (Cap (_, b, e, _)) ->
+         if a >= b && a < e then (
+           if a = b then `AtStart
+           else if a = Z.(e- ~$1) then `AtLast
+           else `InRange
+         ) else `No
+      | _ -> `No
 
-    let at_reg r a = match r with Machine.I _ -> false | Cap (_, _, _, r) -> a = r
+    let at_reg r a = match r with
+         Ast.Sealable (Cap (_, _, _, r)) -> a = r | _ -> false
 
     let img_instr in_range a w =
       (match w with
-       | Machine.I z when in_range a <> `No ->
+       | Ast.I z when in_range a <> `No ->
          begin match Encode.decode_machine_op z with
            | i -> Instr.ui i
            | exception Encode.DecodeException _ -> I.string A.(fg green) "???"
          end
        | _ -> I.empty)
 
-    let render_prog width (pc: Machine.word) data_range =
+    let render_prog width (pc: Ast.word) data_range =
       let is_in_pc_range a = is_in_r_range pc a in
       let at_pc a = at_reg pc a in
       let img_of_prog a w =
@@ -197,8 +251,7 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
 
     let follow_addr r (height : int) start_addr (off : int)=
       match r with
-      | Machine.I _ -> start_addr
-      | Cap (_, _, _, r) ->
+      | Ast.Sealable (Cap (_, _, _, r)) ->
         Z.(
         if r <= start_addr && start_addr > ~$0 then
           r - ~$off
@@ -206,17 +259,18 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
           r - ~$off
         else
           start_addr)
-    let next_page n (_ : Machine.word) height start_addr off  =
+      | _ -> start_addr
+    let next_page n (_ : Ast.word) height start_addr off  =
       Z.(let new_addr = start_addr + (~$n * ~$height) - ~$off in
       if new_addr > Cfg.addr_max then start_addr else new_addr)
-    let previous_page n (_ : Machine.word) height start_addr off  =
+    let previous_page n (_ : Ast.word) height start_addr off  =
       Z.(let new_addr = start_addr - (~$n * ~$height) + ~$off in
       if new_addr < ~$0 then ~$0 else new_addr)
-    let next_addr (_ : Machine.word) (_:int) start_addr (_:int) =
+    let next_addr (_ : Ast.word) (_:int) start_addr (_:int) =
       Z.(let new_addr = start_addr + ~$1 in
       if new_addr > Cfg.addr_max
       then start_addr else new_addr)
-    let previous_addr (_ : Machine.word) (_:int) start_addr (_:int) =
+    let previous_addr (_ : Ast.word) (_:int) start_addr (_:int) =
       Z.(let new_addr = start_addr - ~$1 in
       if new_addr < ~$0 then ~$0 else new_addr)
 
@@ -224,7 +278,7 @@ module MkUi (Cfg: MachineConfig) : Ui = struct
         ?(upd_prog = follow_addr)
         height width
         (mem: Machine.mem_state)
-        (pc: Machine.word)
+        (pc: Ast.word)
         (start_prog: Z.t)
       =
 
diff --git a/lib/ir.ml b/lib/ir.ml
index 558f0f7..78b8c68 100644
--- a/lib/ir.ml
+++ b/lib/ir.ml
@@ -10,9 +10,12 @@ type expr
   | SubOp of expr * expr
 
 type perm = O | E | RO | RX | RW | RWX
-type const_perm = Const of expr | Perm of perm
-type reg_or_const = Register of regname | CP of const_perm (* TODO: separate into two types *)
-type word = I of expr | Cap of perm * expr * expr * expr
+type seal_perm = bool * bool
+type wtype = W_I | W_Cap | W_SealRange | W_Sealed
+type const_encoded = ConstExpr of expr | Perm of perm | SealPerm of seal_perm | Wtype of wtype
+type reg_or_const = Register of regname | Const of const_encoded
+type sealable = Cap of perm * expr * expr * expr | SealRange of seal_perm * expr * expr * expr
+type word = I of expr | Sealable of sealable | Sealed of expr * sealable
 exception WordException of word
 
 type machine_op
@@ -30,11 +33,14 @@ type machine_op
   | Lea of regname * reg_or_const
   | Restrict of regname * reg_or_const
   | SubSeg of regname * reg_or_const * reg_or_const
-  | IsPtr of regname * regname
-  | GetP of regname * regname
   | GetB of regname * regname
   | GetE of regname * regname
   | GetA of regname * regname
+  | GetP of regname * regname
+  | GetOType of regname * regname
+  | GetWType of regname * regname
+  | Seal of regname * regname * regname
+  | UnSeal of regname * regname * regname
   | Fail
   | Halt
   | Lbl of string
@@ -75,26 +81,99 @@ let translate_regname (r : regname) : Ast.regname =
   | PC -> Ast.PC
   | Reg i -> Ast.Reg i
 
-let translate_const_perm (envr : env) (cp : const_perm) : Ast.const_perm =
-  match cp with
-  | Const e -> Ast.Const (eval_expr envr e)
-  | Perm p -> Ast.Perm (translate_perm p)
+
+(* Interleave two integers bitwise.
+ * Example: x = 0b101 and y = 0b110
+ * results in 0b111001. *)
+let rec interleave_int (x : Z.t) (y : Z.t) : Z.t =
+  let open Z in
+  if x = zero && y = zero
+  then zero
+  else
+    let x1 = x land one in
+    let y1 = (y land one) lsl 1 in
+    let x2 = x asr 1 in
+    let y2 = y asr 1 in
+    x1 + y1 + ((interleave_int x2 y2) lsl 2)
+
+(* Encode two integers by interleaving their
+ * absolute values bitwise, followed
+ * by two bits representing signs.
+ *)
+let encode_int_int (x : Z.t) (y : Z.t) =
+  let sign_bits = Z.of_int @@ begin
+    match (Z.sign y, Z.sign x) with
+      | (-1, -1) -> 0b11
+      | (-1, (0|1))  -> 0b10
+      | ((0|1), -1)  -> 0b01
+      | ((0|1), (0|1)) -> 0b00
+      | _ -> assert false
+  end in
+  let interleaved = interleave_int (Z.abs x) (Z.abs y) in
+  Z.(sign_bits + (interleaved lsl 2))
+
+let encode_perm (p : perm) : Z.t =
+  Z.of_int @@
+  match p with
+  | O -> 0b000
+  | E -> 0b001
+  | RO -> 0b100
+  | RX -> 0b101
+  | RW -> 0b110
+  | RWX -> 0b111
+
+let encode_seal_perm (p : seal_perm) : Z.t =
+  Z.of_int @@
+  match p with
+  | (false, false) -> 0b00
+  | (false, true) -> 0b01
+  | (true, false) -> 0b10
+  | (true, true) -> 0b11
+
+let encode_wtype (w : wtype) : Z.t =
+  Z.of_int @@
+  match w with
+  | W_I -> 0b00
+  | W_Cap -> 0b01
+  | W_SealRange -> 0b10
+  | W_Sealed -> 0b11
+
+let encode_const (envr : env) (c : const_encoded) : Z.t =
+  (* TODO should be some global parameters *)
+  let _CONST_ENC       = 0b00 in
+  let _PERM_ENC        = 0b01 in
+  let _SEAL_PERM_ENC   = 0b10 in
+  let _WTYPE_ENC       = 0b11 in
+  let encode t z = encode_int_int (Z.of_int t) z in
+  match c with
+  | ConstExpr e -> encode _CONST_ENC (eval_expr envr e)
+  | Perm p -> encode _PERM_ENC (encode_perm p)
+  | SealPerm sp -> encode _SEAL_PERM_ENC (encode_seal_perm sp)
+  | Wtype wt -> encode _WTYPE_ENC (encode_wtype wt)
 
 let translate_reg_or_const (envr : env) (roc : reg_or_const) : Ast.reg_or_const =
   match roc with
   | Register r -> Ast.Register (translate_regname r)
-  | CP cp -> Ast.CP (translate_const_perm envr cp)
+  | Const c -> Ast.Const (encode_const envr c)
+
+let translate_sealable (envr : env) (s : sealable) : Ast.sealable =
+  match s with
+  | Cap (p,b,e,a) ->
+    Ast.Cap ((translate_perm p),
+             (eval_expr envr b),
+             (eval_expr envr e),
+             (eval_expr envr a))
+  | SealRange (p, b, e, a) ->
+    Ast.SealRange (p,
+                   (eval_expr envr b),
+                   (eval_expr envr e),
+                   (eval_expr envr a))
 
 let translate_word (envr : env) (w : word) : Ast.statement =
   match w with
   | I e -> Ast.Word (Ast.I (eval_expr envr e))
-  | Cap (p,b,e,a) ->
-    Ast.Word (Ast.Cap
-                ((translate_perm p),
-                 (eval_expr envr b),
-                 (eval_expr envr e),
-                 (eval_expr envr a)
-                ))
+  | Sealable sb -> Ast.Word (Ast.Sealable (translate_sealable envr sb))
+  | Sealed (o,sb) -> Ast.Word (Ast.Sealed (eval_expr envr o, (translate_sealable envr sb)))
 
 let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
   match instr with
@@ -130,11 +209,14 @@ let translate_instr (envr : env) (instr : machine_op) : Ast.machine_op =
   | SubSeg (r, c1, c2) -> Ast.SubSeg (translate_regname r,
                                       translate_reg_or_const envr c1,
                                       translate_reg_or_const envr c2)
-  | IsPtr (r1, r2) -> Ast.IsPtr (translate_regname r1, translate_regname r2)
-  | GetP (r1, r2) -> Ast.GetP (translate_regname r1, translate_regname r2)
   | GetB (r1, r2) -> Ast.GetB (translate_regname r1, translate_regname r2)
   | GetE (r1, r2) -> Ast.GetE (translate_regname r1, translate_regname r2)
   | GetA (r1, r2) -> Ast.GetA (translate_regname r1, translate_regname r2)
+  | GetP (r1, r2) -> Ast.GetP (translate_regname r1, translate_regname r2)
+  | GetOType (r1, r2) -> Ast.GetOType (translate_regname r1, translate_regname r2)
+  | GetWType (r1, r2) -> Ast.GetWType (translate_regname r1, translate_regname r2)
+  | Seal (r1, r2, r3) -> Ast.Seal (translate_regname r1, translate_regname r2, translate_regname r3)
+  | UnSeal (r1, r2, r3) -> Ast.UnSeal (translate_regname r1, translate_regname r2, translate_regname r3)
   | Fail -> Ast.Fail
   | Halt -> Ast.Halt
   | Word w -> raise (WordException w)
diff --git a/lib/irreg.ml b/lib/irreg.ml
index 54c33e8..95bf612 100644
--- a/lib/irreg.ml
+++ b/lib/irreg.ml
@@ -9,16 +9,18 @@ type expr
   | MaxAddr
 
 type perm = O | E | RO | RX | RW | RWX
+type seal_perm = bool * bool
 
 (* TODO special addresses: min_addr, max_addr, stk_addr ... *)
 type addr = Addr of expr
 
-type word = WI of expr | WCap of perm * addr * addr * addr
+type sealable = WCap of perm * addr * addr * addr | WSealRange of seal_perm * addr * addr * addr
+type word = WI of expr | WSealable of sealable | WSealed of addr * sealable
 
 type t = (regname * word) list
 
 
-let rec eval_expr  (e : expr) (max_addr : Z.t) : Z.t =
+let rec eval_expr (e : expr) (max_addr : Z.t) : Z.t =
   match e with
   | IntLit i -> Z.(~$i)
   | MaxAddr -> max_addr
@@ -44,18 +46,29 @@ let translate_addr (a : addr) (max_addr : Z.t) : Z.t =
   | Addr e -> (eval_expr e max_addr)
 
 
-let translate_word (w : word) (max_addr : Z.t) : Machine.word =
-  match w with
-  | WI e -> Machine.I (eval_expr e max_addr)
+let translate_sealable (sb : sealable) (max_addr : Z.t) : Ast.sealable =
+  match sb with
   | WCap (p,b,e,a) ->
     let p = translate_perm p in
     let b = translate_addr b max_addr in
     let e = translate_addr e max_addr in
     let a = translate_addr a max_addr in
-    Machine.Cap (p,b,e,a)
+    Cap (p,b,e,a)
+  | WSealRange (p,b,e,a) ->
+    let b = translate_addr b max_addr in
+    let e = translate_addr e max_addr in
+    let a = translate_addr a max_addr in
+    SealRange (p,b,e,a)
+
+
+let translate_word (w : word) (max_addr : Z.t) : Ast.word =
+  match w with
+  | WI e -> Ast.I (eval_expr e max_addr)
+  | WSealable sb -> Ast.Sealable (translate_sealable sb max_addr)
+  | WSealed (o,sb) -> Ast.Sealed (translate_addr o max_addr, translate_sealable sb max_addr)
 
 let rec translate_regfile (regfile : t) (max_addr : Z.t):
-  (Machine.word Machine.RegMap.t) =
+  (Ast.word Machine.RegMap.t) =
   let init_regfile =
     Machine.RegMap.empty in
   match regfile with
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 36b8d17..3f135ae 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -44,20 +44,28 @@ rule token = parse
 | "lea" { LEA }
 | "restrict" { RESTRICT }
 | "subseg" { SUBSEG }
-| "isptr" { ISPTR }
-| "getp" { GETP }
 | "getb" { GETB }
 | "gete" { GETE }
 | "geta" { GETA }
+| "getp" { GETP }
+| "getotype" { GETOTYPE }
+| "getwtype" { GETWTYPE }
+| "seal" { SEAL }
+| "unseal" { UNSEAL }
 | "fail" { FAIL }
 | "halt" { HALT }
 
 (* single-character tokens *)
 | '(' { LPAREN }
 | ')' { RPAREN }
+| '{' { LCBRK }
+| '}' { RCBRK }
+| '[' { LSBRK }
+| ']' { RSBRK }
 | '+' { PLUS }
 | '-' { MINUS }
 | ',' { COMMA }
+| ':' { COLON }
 | '#' { SHARP }
 
 (* permissions *)
@@ -67,6 +75,15 @@ rule token = parse
 | "RX" { RX }
 | "RW" { RW }
 | "RWX" { RWX }
+| 'S' { S }
+| 'U' { U }
+| "SU" { SU }
+
+(* word type *)
+| "Int" { Int }
+| "Cap" { Cap }
+| "SealRange" { SealRange }
+| "Sealed" { Sealed }
 
 (* labels *)
 | label as lbl ':' { LABELDEF (lbl) }
diff --git a/lib/lexer_regfile.mll b/lib/lexer_regfile.mll
index 087de36..43d28b0 100644
--- a/lib/lexer_regfile.mll
+++ b/lib/lexer_regfile.mll
@@ -34,12 +34,18 @@ rule token = parse
 (* single-character tokens *)
 | '(' { LPAREN }
 | ')' { RPAREN }
+| '{' { LCBRK }
+| '}' { RCBRK }
+| '[' { LSBRK }
+| ']' { RSBRK }
 | '+' { PLUS }
 | '-' { MINUS }
 | ',' { COMMA }
+| ':' { COLON }
 | ":=" { AFFECT }
 
 
+
 (* permissions *)
 | 'O' { O }
 | 'E' { E }
@@ -47,6 +53,9 @@ rule token = parse
 | "RX" { RX }
 | "RW" { RW }
 | "RWX" { RWX }
+| 'S' { S }
+| 'U' { U }
+| "SU" { SU }
 
 and comment = parse
 | eof { EOF }
diff --git a/lib/machine.ml b/lib/machine.ml
index ee037aa..4cd9345 100644
--- a/lib/machine.ml
+++ b/lib/machine.ml
@@ -12,7 +12,7 @@ module RegMap =
   end)
     
 type exec_state = Running | Halted | Failed
-type word = I of Z.t | Cap of perm * Z.t * Z.t * Z.t
+(* type word = I of Z.t | Sealable of sealable | Sealed of Z.t * sealable *)
 type reg_state = word RegMap.t
 type mem_state = word MemMap.t
 type exec_conf = { reg : reg_state; mem : mem_state } (* using a record to have notation similar to the paper *)
@@ -22,11 +22,13 @@ let init_reg_state (addr_max : Z.t) : reg_state =
   let start_heap_addr = ~$0 in
   let max_heap_addr = Z.(addr_max / ~$2) in
 
-  let l = List.init 32 (fun i -> Reg i, I Z.zero) in
+  let l = List.init 31 (fun i -> Reg (i+1), I Z.zero) in
+  (* let l = List.init 32 (fun i -> Reg i, I Z.zero) in *)
 
   (* The PC register starts with full permission over the entire "heap" segment *)
-  let pc_init = (PC, Cap (RWX, start_heap_addr, max_heap_addr, start_heap_addr)) in
-  let seq = List.to_seq (pc_init :: l) in
+  let pc_init = (PC, Sealable (Cap (RWX, start_heap_addr, max_heap_addr, start_heap_addr))) in
+  let pc_sealing = (Reg 0, Sealable (SealRange ((true,true), start_heap_addr, max_heap_addr, start_heap_addr))) in
+  let seq = List.to_seq (pc_init :: pc_sealing :: l) in
   RegMap.of_seq seq
 
 let get_reg (r : regname) ({reg ; _} : exec_conf) : word = RegMap.find r reg
@@ -50,7 +52,9 @@ let init_mem_state (addr_start: Z.t) (addr_max : Z.t) (prog : t) : mem_state =
                   match x with
                   | Op op -> I (Encode.encode_machine_op op)
                   | Word (Ast.I z) -> I z
-                  | Word (Ast.Cap (p,b,e,a)) -> Cap (p, b, e, a))
+                  | Word (Ast.Sealable sb) -> Sealable sb
+                    (* Cap (p, b, e, a)) *)
+                  | Word (Ast.Sealed (o, sb)) -> Sealed (o, sb))
       prog in
   MemMap.add_seq enc_prog zeroed_mem
 
@@ -67,33 +71,37 @@ let init
 let get_word (conf : exec_conf) (roc : reg_or_const) : word =
   match roc with
   | Register r -> get_reg r conf
-  | CP (Const i) -> I i
-  | CP (Perm p) -> I (Encode.encode_perm p) (* A permission is just an integer in the model *)
+  | Const i -> let (_, c) = Encode.decode_int i in I c
+
+let get_word_type (roc : reg_or_const) : Z.t option =
+  match roc with
+  | Register _ -> None
+  | Const i -> let (wt, _) = Encode.decode_int i in Some wt
 
 let upd_pc (conf : exec_conf) : mchn =
   match PC @! conf with
-  | Cap (p, b, e, a) -> (Running, upd_reg PC (Cap (p, b, e, Z.(a + ~$1))) conf)
+  | Sealable (Cap (p, b, e, a)) -> (Running, upd_reg PC (Sealable (Cap (p, b, e, Z.(a + ~$1)))) conf)
   | _ -> (Failed, conf)
 let (!>) conf = upd_pc conf
 
 let upd_pc_perm (w : word) =
   match w with
-  | Cap (E, b, e, a) -> Cap (RX, b, e, a)
+  | Sealable (Cap (E, b, e, a)) -> Sealable (Cap (RX, b, e, a))
   | _ -> w
 
 let fetch_decode (conf : exec_conf) : machine_op option =
   match PC @! conf with
-  | I _ -> None
-  | Cap (_, _, _, addr) ->
-    match get_mem addr conf with
+  | Sealable (Cap (_, _, _, addr)) ->
+    (match get_mem addr conf with
     | Some (I enc) ->
       (try Some (Encode.decode_machine_op enc)
         with Encode.DecodeException _ -> None)
-    | _ -> None
+    | _ -> None)
+  | _ -> None
 
 let is_pc_valid (conf : exec_conf) : bool =
   match PC @! conf with
-  | Cap ((RX|RWX), b, e, a) -> begin
+  | Sealable (Cap ((RX|RWX), b, e, a)) -> begin
       if b <= a && a < e
       then Option.is_some @@ a @? conf
       else false
@@ -124,6 +132,17 @@ let perm_flowsto (p1 : perm) (p2 : perm) : bool =
     | RW | RWX -> true
     | _ -> false)
 
+let sealperm_flowsto (p1 : seal_perm) (p2 : seal_perm) : bool =
+  let p_flows p p' =
+    match p,p' with
+    | false, _ -> true
+    | true, true -> true
+    | _,_ -> false
+  in
+  let (s1, u1) = p1 in
+  let (s2, u2) = p2 in
+  (p_flows s1 s2) && (p_flows u1 u2)
+
 let can_write (p : perm) : bool =
   match p with
   | RW | RWX -> true
@@ -135,8 +154,14 @@ let can_read (p : perm) : bool =
   | _ -> false
 
 let exec_single (conf : exec_conf) : mchn =
+  (* TODO should be some global parameters *)
+  let _CONST_ENC       = 0b00 in
+  let _PERM_ENC        = 0b01 in
+  let _SEAL_PERM_ENC   = 0b10 in
+  let _WTYPE_ENC       = 0b11 in
+
   let fail_state = (Failed, conf) in
-  if is_pc_valid conf 
+  if is_pc_valid conf
   then match fetch_decode conf with
     | None -> fail_state
     | Some instr -> begin
@@ -149,7 +174,7 @@ let exec_single (conf : exec_conf) : mchn =
           end
         | Load (r1, r2) -> begin
             match r2 @! conf with
-            | Cap (p, b, e, a) ->
+            | Sealable (Cap (p, b, e, a)) ->
               if can_read p then
                 match a @? conf with
                 | Some w when (b <= a && a < e) -> !> (upd_reg r1 w conf)
@@ -160,7 +185,7 @@ let exec_single (conf : exec_conf) : mchn =
         | Store (r, c) -> begin
             let w = get_word conf c in
             match r @! conf with
-            | Cap (p, b, e, a) when (b <= a && a < e) ->
+            | Sealable (Cap (p, b, e, a)) when (b <= a && a < e) ->
               if can_write p
               then !> (upd_mem a w conf)
               else fail_state
@@ -180,13 +205,33 @@ let exec_single (conf : exec_conf) : mchn =
           end
         | Restrict (r, c) -> begin
             match r @! conf with
-            | Cap (p, b, e, a) -> begin
+            | Sealable (Cap (p, b, e, a)) -> begin
+                match get_word conf c with
+                | I i -> begin
+                    match get_word_type c with
+                     (* Shouldn't happen, because we already know from get_word that c is a Int *)
+                    | None -> fail_state
+                    | Some wt when wt = Z.(~$_PERM_ENC) -> (* we can safely decode i as a normal permission *)
+                        let p' = Encode.decode_perm i in
+                        if perm_flowsto p' p
+                        then !> (upd_reg r (Sealable (Cap (p', b, e, a))) conf)
+                        else fail_state
+                    | _ -> (* wt is expected to be a permission *) fail_state
+                  end
+                | _ -> fail_state
+              end
+            | Sealable (SealRange (sp, b, e, a)) -> begin
                 match get_word conf c with
                 | I i -> begin
-                    let p' = Encode.decode_perm i in
-                    if perm_flowsto p' p
-                    then !> (upd_reg r (Cap (p', b, e, a)) conf)
-                    else fail_state
+                    match get_word_type c with
+                    (* Shouldn't happen, because we already know from get_word that c is a Int *)
+                    | None -> fail_state
+                    | Some wt when wt = Z.(~$_SEAL_PERM_ENC) -> (* we can safely decode i as a seal permission *)
+                      let sp' = Encode.decode_seal_perm i in
+                      if sealperm_flowsto sp' sp
+                      then !> (upd_reg r (Sealable (SealRange (sp', b, e, a))) conf)
+                      else fail_state
+                    | _ -> (* wt is expected to be a seal permission *) fail_state
                   end
                 | _ -> fail_state
               end
@@ -194,14 +239,26 @@ let exec_single (conf : exec_conf) : mchn =
           end
         | SubSeg (r, c1, c2) -> begin
             match r @! conf with
-            | Cap (p, b, e, a) -> begin
+            | Sealable (Cap (p, b, e, a)) -> begin
                 let w1 = get_word conf c1 in
                 let w2 = get_word conf c2 in
                 match w1, w2 with
                 | I z1, I z2 ->
                   if b <= z1 && Z.(~$0 <= z2) && Z.(~$0 <= e) && p <> E
                   then
-                    let w = Cap (p, z1, z2, a) in
+                    let w = Sealable (Cap (p, z1, z2, a)) in
+                    !> (upd_reg r w conf)
+                  else fail_state
+                | _ -> fail_state
+              end
+            | Sealable (SealRange (p, b, e, a)) -> begin
+                let w1 = get_word conf c1 in
+                let w2 = get_word conf c2 in
+                match w1, w2 with
+                | I z1, I z2 ->
+                  if b <= z1 && Z.(~$0 <= z2) && Z.(~$0 <= e)
+                  then
+                    let w = Sealable (SealRange (p, z1, z2, a)) in
                     !> (upd_reg r w conf)
                   else fail_state
                 | _ -> fail_state
@@ -210,10 +267,16 @@ let exec_single (conf : exec_conf) : mchn =
           end
         | Lea (r, c) -> begin
             match r @! conf with
-            | Cap (p, b, e, a) -> begin
+            | Sealable (Cap (p, b, e, a)) -> begin
                 let w = get_word conf c in
                 match w with
-                | I z when p <> E -> !> (upd_reg r (Cap (p, b, e, Z.(a + z))) conf)
+                | I z when p <> E -> !> (upd_reg r (Sealable (Cap (p, b, e, Z.(a + z)))) conf)
+                | _ -> fail_state
+              end
+            | Sealable (SealRange (p, b, e, a)) -> begin
+                let w = get_word conf c in
+                match w with
+                | I z -> !> (upd_reg r (Sealable (SealRange (p, b, e, Z.(a + z)))) conf)
                 | _ -> fail_state
               end
             | _ -> fail_state
@@ -262,31 +325,60 @@ let exec_single (conf : exec_conf) : mchn =
             | I _, I _ -> !> (upd_reg r (I Z.zero) conf)
             | _ -> fail_state
           end
-        | GetP (r1, r2) -> begin
-            match r2 @! conf with
-            | Cap (p, _, _, _) -> !> (upd_reg r1 (I (Encode.encode_perm p)) conf)
-            | _ -> fail_state
-          end
         | GetB (r1, r2) -> begin
             match r2 @! conf with
-            | Cap (_, b, _, _) -> !> (upd_reg r1 (I b) conf)
+            | Sealable (SealRange (_, b, _, _))
+            | Sealable (Cap (_, b, _, _)) -> !> (upd_reg r1 (I b) conf)
             | _ -> fail_state
           end
         | GetE (r1, r2) -> begin
             match r2 @! conf with
-            | Cap (_, _, e, _) -> !> (upd_reg r1 (I e) conf)
+            | Sealable (SealRange (_, _, e, _))
+            | Sealable (Cap (_, _, e, _)) -> !> (upd_reg r1 (I e) conf)
             | _ -> fail_state
           end
         | GetA (r1, r2) -> begin
             match r2 @! conf with
-            | Cap (_, _, _, a) -> !> (upd_reg r1 (I a) conf)
+            | Sealable (SealRange (_, _, _, a))
+            | Sealable (Cap (_, _, _, a)) -> !> (upd_reg r1 (I a) conf)
             | _ -> fail_state
           end
-        | IsPtr (r1, r2) -> begin
+        | GetP (r1, r2) -> begin
             match r2 @! conf with
-            | Cap (_, _, _, _) -> !> (upd_reg r1 (I ~$1) conf)
-            | _ -> !> (upd_reg r1 (I ~$0) conf)
-          end    
+            | Sealable (Cap (p, _, _, _)) -> !> (upd_reg r1 (I (Encode.encode_perm p)) conf)
+            | Sealable (SealRange (p, _, _, _)) -> !> (upd_reg r1 (I (Encode.encode_seal_perm p)) conf)
+            | _ -> fail_state
+          end
+        | GetOType (r1, r2) -> begin
+            match r2 @! conf with
+            | Sealed (o,_) -> !> (upd_reg r1 (I o) conf)
+            | _ -> !> (upd_reg r1 (I ~$(-1)) conf)
+          end
+        | GetWType (r1, r2) -> begin
+            let wtype_enc =
+              Encode.encode_wtype
+                (match r2 @! conf with
+                 | I _ -> W_I
+                 | Sealable (Cap _) -> W_Cap
+                 | Sealable (SealRange _) -> W_SealRange
+                 | Sealed _ -> W_Sealed)
+            in !> (upd_reg r1 (I wtype_enc) conf)
+          end
+
+        | Seal (dst, r1, r2) -> begin
+            match r1 @! conf, r2 @! conf with
+            | Sealable (SealRange ((true,_),b,e,a)), Sealable sb when (b <= a && a < e) ->
+              !> (upd_reg dst (Sealed (a, sb)) conf)
+            | _ -> fail_state
+          end
+        | UnSeal (dst, r1, r2) -> begin
+            match r1 @! conf, r2 @! conf with
+            | Sealable (SealRange ((_,true),b,e,a)), (Sealed (a', sb))->
+              if (b <= a && a < e && a = a')
+              then !> (upd_reg dst (Sealable sb) conf)
+              else fail_state
+            | _ -> fail_state
+          end
       end
   else fail_state
 
diff --git a/lib/parser.mly b/lib/parser.mly
index 4a22b73..390ffc7 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -4,11 +4,13 @@
 %token <int> INT
 %token <string> LABELDEF
 %token <string> LABEL
-%token LPAREN RPAREN
-%token PLUS MINUS COMMA SHARP
+%token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK
+%token PLUS MINUS COMMA SHARP COLON
 %token JMP JNZ MOVE LOAD STORE ADD SUB MUL REM DIV LT LEA RESTRICT SUBSEG
-%token ISPTR GETP GETB GETE GETA FAIL HALT
+%token GETB GETE GETA GETP GETOTYPE GETWTYPE SEAL UNSEAL FAIL HALT
 %token O E RO RX RW RWX
+%token S U SU
+%token Int Cap SealRange Sealed
 
 %left PLUS MINUS EXPR
 %left UMINUS
@@ -34,20 +36,33 @@ main:
   | LEA; r = reg; c = reg_const; p = main; { Lea (r, c) :: p }
   | RESTRICT; r = reg; c = reg_const; p = main; { Restrict (r, c) :: p }
   | SUBSEG; r = reg; c1 = reg_const; c2 = reg_const; p = main; { SubSeg (r, c1, c2) :: p }
-  | ISPTR; r1 = reg; r2 = reg; p = main; { IsPtr (r1, r2) :: p }
-  | GETP; r1 = reg; r2 = reg; p = main; { GetP (r1, r2) :: p }
   | GETB; r1 = reg; r2 = reg; p = main; { GetB (r1, r2) :: p }
   | GETE; r1 = reg; r2 = reg; p = main; { GetE (r1, r2) :: p }
   | GETA; r1 = reg; r2 = reg; p = main; { GetA (r1, r2) :: p }
+  | GETP; r1 = reg; r2 = reg; p = main; { GetP (r1, r2) :: p }
+  | GETOTYPE; r1 = reg; r2 = reg; p = main; { GetOType (r1, r2) :: p }
+  | GETWTYPE; r1 = reg; r2 = reg; p = main; { GetWType (r1, r2) :: p }
+  | SEAL; r1 = reg; r2 = reg; r3 = reg; p = main; { Seal (r1, r2, r3) :: p }
+  | UNSEAL; r1 = reg; r2 = reg; r3 = reg; p = main; { UnSeal (r1, r2, r3) :: p }
   | FAIL; p = main; { Fail :: p }
   | HALT; p = main; { Halt :: p }
   | lbl = LABELDEF; p = main; { Lbl lbl :: p }
-  | SHARP ; cap = cap_def; p = main; { Word cap :: p }
-  | SHARP ; z = expr; p = main; { Word (I z) :: p }
+  | SHARP ; w = word_def; p = main { Word w :: p }
+
+word_def:
+  | sb = sealable_def; { Sealable sb }
+  | sealed = sealed_def; { sealed }
+  | z = expr; { I z }
 
-cap_def:
+sealable_def:
   | LPAREN; p = perm; COMMA; b = expr; COMMA; e = expr; COMMA; a = expr; RPAREN;
     { Cap (p, b, e, a) }
+  | LSBRK; p = seal_perm; COMMA; b = expr; COMMA; e = expr; COMMA; a = expr; RSBRK;
+    { SealRange (p, b, e, a) }
+
+sealed_def:
+  | LCBRK; o = expr; COLON; sb = sealable_def ; RCBRK
+    { Sealed (o, sb) }
 
 reg:
   | PC; { PC }
@@ -55,8 +70,22 @@ reg:
 
 reg_const:
   | r = reg; { Register r }
-  | c = expr %prec EXPR { CP (Const (c)) }
-  | p = perm; { CP (Perm p) }
+  | c = expr %prec EXPR { Const (ConstExpr c) }
+  | p = perm; { Const (Perm p) }
+  | p = seal_perm; { Const (SealPerm p) }
+  | w = wtype; { Const (Wtype w) }
+
+seal_perm:
+  | O; { (false, false) }
+  | S; { (true, false) }
+  | U; { (false, true) }
+  | SU; { (true, true) }
+
+wtype:
+  | Int ; { W_I }
+  | Cap ; { W_Cap }
+  | SealRange ; { W_SealRange }
+  | Sealed ; { W_Sealed }
 
 perm:
   | O; { O }
diff --git a/lib/parser_regfile.mly b/lib/parser_regfile.mly
index ae2fd58..367533c 100644
--- a/lib/parser_regfile.mly
+++ b/lib/parser_regfile.mly
@@ -3,9 +3,10 @@
 %token <int> REG
 %token <int> INT
 %token MAX_ADDR
-%token LPAREN RPAREN
-%token PLUS MINUS AFFECT COMMA
+%token LPAREN RPAREN LSBRK RSBRK LCBRK RCBRK
+%token PLUS MINUS AFFECT COMMA COLON
 %token O E RO RX RW RWX
+%token S U SU
 
 %left PLUS MINUS EXPR
 %left UMINUS
@@ -25,17 +26,29 @@ reg:
 
 word:
   | e = expr %prec EXPR { WI (e) }
-  | LPAREN
-; p = perm ; COMMA ;
-; b = addr ; COMMA
-; e = addr ; COMMA
-; a = addr
-; RPAREN  { WCap (p, b, e, a) }
+  | sb = sealable_def {WSealable sb}
+  | s = sealed_def {s}
+
+sealable_def:
+  | LPAREN; p = perm; COMMA; b = addr; COMMA; e = addr; COMMA; a = addr; RPAREN;
+    { WCap (p, b, e, a) }
+  | LSBRK; p = seal_perm; COMMA; b = addr; COMMA; e = addr; COMMA; a = addr; RSBRK;
+    { WSealRange (p, b, e, a) }
+
+sealed_def:
+  | LCBRK; o = addr; COLON; sb = sealable_def ; RCBRK
+    { WSealed (o, sb) }
 
 addr:
   | e = expr %prec EXPR { Addr (e) }
 (* TODO support hexa addresses *)
 
+seal_perm:
+  | O; { (false, false) }
+  | S; { (true, false) }
+  | U; { (false, true) }
+  | SU; { (true, true) }
+
 perm:
   | O; { O }
   | E; { E }
diff --git a/lib/pretty_printer.ml b/lib/pretty_printer.ml
index 39fe2d6..a8cf395 100644
--- a/lib/pretty_printer.ml
+++ b/lib/pretty_printer.ml
@@ -8,6 +8,14 @@ let string_of_regname (r: regname) : string =
   | PC -> "pc"
   | Reg i -> "r" ^ (string_of_int i)
 
+(* TODO is there any better way to print it ? *)
+let string_of_seal_perm (p : seal_perm) : string =
+  match p with
+  | (false, false) -> "O"
+  | (true, false) -> "S"
+  | (false, true) -> "U"
+  | (true, true) -> "SU"
+
 let string_of_perm (p: perm): string =
   match p with
   | O -> "O"
@@ -17,15 +25,37 @@ let string_of_perm (p: perm): string =
   | RW -> "RW"
   | RWX -> "RWX"
 
+let string_of_wtype (w : wtype) : string =
+  match w with
+  | W_I -> "Int"
+  | W_Cap -> "Cap"
+  | W_SealRange -> "SealRange"
+  | W_Sealed -> "Sealed"
+
+exception DecodeException of string
 let string_of_reg_or_const (c: reg_or_const) : string =
   match c with
   | Register r -> string_of_regname r
-  | CP (Const c) -> (Z.to_string c)
-  | CP (Perm p) -> string_of_perm p
+  | Const c ->
+    let decode_const_exception = fun _ -> raise @@ DecodeException "Error decoding constant: unexpected encoding" in
+    let (t, z) = Encode.decode_int c in
+    let b0 = Z.testbit t 0 in
+    let b1 = Z.testbit t 1 in
+    if Z.(t > (of_int 0b11))
+    then decode_const_exception ()
+    else
+      match (b1,b0) with
+      | (false, false) -> (Z.to_string z)
+      | (false, true) -> string_of_perm (Encode.decode_perm z)
+      | (true, false) -> string_of_seal_perm (Encode.decode_seal_perm z)
+      | (true, true) -> string_of_wtype (Encode.decode_wtype z)
+
 
 let string_of_machine_op (s: machine_op): string =
   let string_of_rr r1 r2 =
     string_of_regname r1 ^- string_of_regname r2
+  and string_of_rrr r1 r2 r3 =
+    string_of_regname r1 ^- string_of_regname r2 ^- string_of_regname r3
   and string_of_rc r c =
     string_of_regname r ^- string_of_reg_or_const c
   and string_of_rcc r c1 c2  =
@@ -45,26 +75,44 @@ let string_of_machine_op (s: machine_op): string =
   | Lea (r, c) -> "lea" ^- string_of_rc r c
   | Restrict (r, c) -> "restrict" ^- string_of_rc r c
   | SubSeg (r, c1, c2) -> "subseg" ^- string_of_rcc r c1 c2
-  | IsPtr (r1, r2) -> "isptr" ^- string_of_rr r1 r2
-  | GetP (r1, r2) -> "getp" ^- string_of_rr r1 r2
   | GetB (r1, r2) -> "getb" ^- string_of_rr r1 r2
   | GetE (r1, r2) -> "gete" ^- string_of_rr r1 r2
   | GetA (r1, r2) -> "geta" ^- string_of_rr r1 r2
+  | GetP (r1, r2) -> "getp" ^- string_of_rr r1 r2
+  | GetOType (r1, r2) -> "getotype" ^- string_of_rr r1 r2
+  | GetWType (r1, r2) -> "getwtype" ^- string_of_rr r1 r2
+  | Seal (r1, r2, r3) -> "seal" ^- string_of_rrr r1 r2 r3
+  | UnSeal (r1, r2, r3) -> "unseal" ^- string_of_rrr r1 r2 r3
   | Fail -> "fail"
   | Halt -> "halt"
 
-let string_of_word (w : word) : string =
-  match w with
+
+let string_of_sealable (sb : sealable) : string =
+  match sb with
   | Cap (p, b, e, a) ->
     Printf.sprintf "Cap (%s, %s, %s, %s)" (string_of_perm p) (Z.to_string b) (Z.to_string e) (Z.to_string a)
+  | SealRange (p, b, e, a) ->
+    Printf.sprintf "SRange [%s, %s, %s, %s]" (string_of_seal_perm p) (Z.to_string b) (Z.to_string e) (Z.to_string a)
+
+let string_of_word (w : word) : string =
+  match w with
   | I z -> Z.to_string z
+  | Sealable sb -> string_of_sealable sb
+  | Sealed (o, sb) -> Printf.sprintf "{%s, %s}" (Z.to_string o) (string_of_sealable sb)
+
+
+let string_of_ast_sealable (sb : Ast.sealable) : string =
+  match sb with
+  | Ast.Cap (p, b, e, a) ->
+    Printf.sprintf "Cap (%s, %s, %s, %s)" (string_of_perm p) (Z.to_string b) (Z.to_string e) (Z.to_string a)
+  | Ast.SealRange (p, b, e, a) ->
+    Printf.sprintf "SRange [%s, %s, %s, %s]" (string_of_seal_perm p) (Z.to_string b) (Z.to_string e) (Z.to_string a)
 
 let string_of_ast_word (w : Ast.word) : string =
   match w with
-  | Ast.Cap (p, b, e, a) ->
-    Printf.sprintf "Cap (%s,  %s, %s, %s)"
-    (string_of_perm p) (Z.to_string b) (Z.to_string e) (Z.to_string a)
   | Ast.I z -> Z.to_string z
+  | Ast.Sealable sb -> string_of_sealable sb
+  | Ast.Sealed (o, sb) -> Printf.sprintf "{%s, %s}" (Z.to_string o) (string_of_sealable sb)
 
 let string_of_statement (s : statement) : string =
   match s with
diff --git a/lib/program.ml b/lib/program.ml
index 4aaa022..135caf6 100644
--- a/lib/program.ml
+++ b/lib/program.ml
@@ -7,7 +7,7 @@ let parse_prog (filename: string): (Ast.t, string) Result.t =
   with Failure _ -> close_in input; Result.Error "Parsing Failed"
 
 let parse_regfile (filename: string) (max_addr : Z.t)
-  : (Machine.word Machine.RegMap.t, string) Result.t =
+  : (Ast.word Machine.RegMap.t, string) Result.t =
   let input = open_in filename in
   try
     let filebuf = Lexing.from_channel input in
@@ -21,7 +21,7 @@ let parse_regfile (filename: string) (max_addr : Z.t)
 let init_machine
     (prog : Ast.t)
     (addr_max : Z.t option)
-    (init_regs : Machine.word Machine.RegMap.t)
+    (init_regs : Ast.word Machine.RegMap.t)
   : Machine.mchn =
   let addr_max =
     match addr_max with
diff --git a/tests/dune b/tests/dune
index d402d58..3678bdd 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,3 +1,3 @@
-(tests (names test tester)
+(tests (names tests tester)
 	(libraries alcotest libinterp)
-)
\ No newline at end of file
+)
diff --git a/tests/test_files/base.reg b/tests/test_files/base.reg
new file mode 100644
index 0000000..807a3ac
--- /dev/null
+++ b/tests/test_files/base.reg
@@ -0,0 +1,4 @@
+PC := (RWX, 0, MAX_ADDR, 0)
+R0 := [SU, 0, MAX_ADDR, 0]
+R1 := {0: (RO, 0, 1, 0)}
+R2 := {0: [SU, 0, 1, 0]}
diff --git a/tests/test_files/neg/bad_encoding1.s b/tests/test_files/neg/bad_encoding1.s
new file mode 100644
index 0000000..5f69de2
--- /dev/null
+++ b/tests/test_files/neg/bad_encoding1.s
@@ -0,0 +1,3 @@
+	mov r1 pc
+	restrict r1 Sealed 			; FAIL: attempt to restrict SCap with a WType
+	halt
diff --git a/tests/test_files/neg/bad_encoding2.s b/tests/test_files/neg/bad_encoding2.s
new file mode 100644
index 0000000..db9f8a2
--- /dev/null
+++ b/tests/test_files/neg/bad_encoding2.s
@@ -0,0 +1,2 @@
+	restrict r0 Int				; FAIL: attempt to restrict SCap with a WType
+	halt
diff --git a/tests/test_files/neg/bad_encoding3.s b/tests/test_files/neg/bad_encoding3.s
new file mode 100644
index 0000000..e615886
--- /dev/null
+++ b/tests/test_files/neg/bad_encoding3.s
@@ -0,0 +1,2 @@
+	restrict r0 10 ; FAIL: attempt to restrict SealRange with a WType
+	halt
diff --git a/tests/test_files/neg/bad_flow1.s b/tests/test_files/neg/bad_flow1.s
index 4959fed..e77d9e6 100644
--- a/tests/test_files/neg/bad_flow1.s
+++ b/tests/test_files/neg/bad_flow1.s
@@ -1,4 +1,4 @@
 	mov r1 pc
 	restrict r1 E
-	restrict r1 RWX
+	restrict r1 RWX				; FAIL: attempt to flow from E to RWX
 	halt
diff --git a/tests/test_files/neg/bad_flow2.s b/tests/test_files/neg/bad_flow2.s
index 51aa5b1..372f3c3 100644
--- a/tests/test_files/neg/bad_flow2.s
+++ b/tests/test_files/neg/bad_flow2.s
@@ -1,4 +1,4 @@
 	mov r1 pc
 	restrict r1 O
-	restrict r1 E
+	restrict r1 E 				; FAIL: attempt to flow from O to E
 	halt
diff --git a/tests/test_files/neg/bad_flow3.s b/tests/test_files/neg/bad_flow3.s
new file mode 100644
index 0000000..d9019ae
--- /dev/null
+++ b/tests/test_files/neg/bad_flow3.s
@@ -0,0 +1,2 @@
+	restrict r0 RO 				; FAIL: attempt to restrict a SealRange with a Regular permission
+	halt
diff --git a/tests/test_files/neg/bad_flow_seal1.s b/tests/test_files/neg/bad_flow_seal1.s
new file mode 100644
index 0000000..cdd05a6
--- /dev/null
+++ b/tests/test_files/neg/bad_flow_seal1.s
@@ -0,0 +1,3 @@
+	mov r1 pc
+	restrict r1 SU              ; FAIL: attempt to restrict SCap with a Seal Permission
+	halt
diff --git a/tests/test_files/neg/bad_flow_seal2.s b/tests/test_files/neg/bad_flow_seal2.s
new file mode 100644
index 0000000..4a6c8b6
--- /dev/null
+++ b/tests/test_files/neg/bad_flow_seal2.s
@@ -0,0 +1,3 @@
+	mov r1 pc
+	restrict r1 U 				; FAIL: attempt to restrict SCap with a Seal Permission
+	halt
diff --git a/tests/test_files/neg/bad_perm_seal.s b/tests/test_files/neg/bad_perm_seal.s
new file mode 100644
index 0000000..8bcb796
--- /dev/null
+++ b/tests/test_files/neg/bad_perm_seal.s
@@ -0,0 +1,3 @@
+    restrict r0 U
+    seal r1 r0 pc               ; FAIL: attempt to seal without the (S)eal permission
+    halt
diff --git a/tests/test_files/neg/bad_perm_unseal.s b/tests/test_files/neg/bad_perm_unseal.s
new file mode 100644
index 0000000..9ecdedb
--- /dev/null
+++ b/tests/test_files/neg/bad_perm_unseal.s
@@ -0,0 +1,4 @@
+    restrict r0 S
+    seal r1 r0 pc
+    unseal r1 r0 r1             ; FAIL: attempt to unseal without the (U)nseal permission
+    halt
diff --git a/tests/test_files/neg/bad_sealing_int.s b/tests/test_files/neg/bad_sealing_int.s
new file mode 100644
index 0000000..a9e7831
--- /dev/null
+++ b/tests/test_files/neg/bad_sealing_int.s
@@ -0,0 +1,2 @@
+    seal r1 r0 r1 ; FAIL: attempt to seal an integer, but it is not sealable
+    halt
diff --git a/tests/test_files/neg/bad_sealing_sealed.s b/tests/test_files/neg/bad_sealing_sealed.s
new file mode 100644
index 0000000..727a0c5
--- /dev/null
+++ b/tests/test_files/neg/bad_sealing_sealed.s
@@ -0,0 +1,3 @@
+    seal r1 r0 pc
+    seal r1 r0 r1               ; FAIL: attempt to seal a sealed capability, but it is not sealable
+    halt
diff --git a/tests/test_files/neg/lea_perm_not_entry.s b/tests/test_files/neg/lea_perm_not_entry.s
index fa3c21d..906584a 100644
--- a/tests/test_files/neg/lea_perm_not_entry.s
+++ b/tests/test_files/neg/lea_perm_not_entry.s
@@ -1,4 +1,4 @@
 	mov r1 pc
 	restrict r1 E
-	lea r1 15
+	lea r1 15 					; FAIL: attempt to modify the address of a E-capability
 	halt
diff --git a/tests/test_files/pos/get_otype.s b/tests/test_files/pos/get_otype.s
new file mode 100644
index 0000000..ed5f05f
--- /dev/null
+++ b/tests/test_files/pos/get_otype.s
@@ -0,0 +1,9 @@
+    mov r1 pc
+    mov r2 12
+    lea r0 10
+    seal r3 r0 pc
+    getotype r0 r0
+    getotype r1 r1
+    getotype r2 r2
+    getotype r3 r3
+    halt
diff --git a/tests/test_files/pos/get_wtype.s b/tests/test_files/pos/get_wtype.s
new file mode 100644
index 0000000..a97143b
--- /dev/null
+++ b/tests/test_files/pos/get_wtype.s
@@ -0,0 +1,15 @@
+    mov r1 pc
+    mov r2 12
+    lea r0 10
+    seal r3 r0 pc
+
+    getwtype r0 r0
+    getwtype r1 r1
+    getwtype r2 r2
+    getwtype r3 r3
+
+    sub r0 r0 SealRange
+    sub r1 r1 Cap
+    sub r2 r2 Int
+    sub r3 r3 Sealed
+    halt
diff --git a/tests/test_files/pos/seal_unseal.s b/tests/test_files/pos/seal_unseal.s
new file mode 100644
index 0000000..b5a2d14
--- /dev/null
+++ b/tests/test_files/pos/seal_unseal.s
@@ -0,0 +1,9 @@
+    subseg r0 0 2
+    mov r1 r0
+    restrict r0 S
+    restrict r1 U
+    seal r2 r0 pc
+    seal r3 r0 r1
+    unseal r2 r1 r2
+    unseal r3 r1 r3
+    halt
diff --git a/tests/test_files/pos/sealing_counter.s b/tests/test_files/pos/sealing_counter.s
new file mode 100644
index 0000000..0024d69
--- /dev/null
+++ b/tests/test_files/pos/sealing_counter.s
@@ -0,0 +1,105 @@
+;;; Sealing counter example
+
+;;; Defines a counter library using seal: the client has access to a global pointer for the counter
+;;; via a sealed capability. The otype of this seal is required to be the same than the actual value
+;;; of the counter to be valid.
+;;; The call to `get` returns the current value of the counter, provided that the sealed pointer is valid.
+;;; The call to `incr` increments both the value of the counter and the otype (the sealed pointer
+;;; doesn't have to be valid).
+
+;;; In this running example, the client checks that the initial counter is valid, then increments it
+;;; 3 times, and finally checks that the counter is still valid.
+
+init:
+	;; prepare the sealed_counter in r1
+	mov r0 pc             	; r0 = (RWX, init, end, init)
+	mov r1 r0             	; r1 = (RWX, init, end, init)
+	lea r1 (data-init)		; r1 = (RWX, init, end, data)
+	load r1 r1				; r1 = {0: (RO, counter, counter+1, counter)}
+
+	;; prepare the main capability in r0
+	lea r0 (main+1-init)   	; r0 = (RWX, init, end, main+1)
+	subseg r0 main data		; r0 = (RWX, main, data, main+1)
+	restrict r0 E			; r0 = (E, main, data, main+1)
+	jmp r0   				; jump to main main
+
+main:
+	;; r0 = pc / r1 = {0: (RO, counter, counter+1, counter)}
+	#(RO, linking_table, end, linking_table)
+
+	;; prepare the sentry for get and incr in r30 and r31
+	mov r0 pc
+	lea r0 (-1)				; r0 = (RX, main, data, main+1)
+	load r31 r0				; r30 = (RO, linking_table, end, linking_table)
+	load r30 r31 			; r30 = #(E, get, incr, get+1)
+	lea r31 1
+	load r31 r31 			; r31 = #(E, incr, end, incr+1)
+
+	;; call get
+	mov r0 pc
+	lea r0 3				; r0 = callback
+	jmp r30					; call get
+
+	;; call incr 3 times
+	mov r0 pc
+	lea r0 3				; r0 = callback
+	jmp r31					; call incr
+	mov r0 pc
+	lea r0 3				; r0 = callback
+	jmp r31					; call incr
+	mov r0 pc
+	lea r0 3				; r0 = callback
+	jmp r31					; call incr
+	mov r0 pc
+
+	;; call get
+	mov r0 pc
+	lea r0 3				; r0 = callback
+	jmp r30					; call get
+
+	halt
+data:
+	#{0: (RW, counter, counter+1, counter)}
+linking_table:
+	#(E, get, incr, get+1) 		; get
+	#(E, incr, end, incr+2)		; incr
+counter:
+	#0
+get: 							; check whether the otype matches with the actual value
+	#[SU, 0, 10, 0]
+	;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)}
+	mov r2 pc 					; r2 = (RX, get, incr, get+1)
+	lea r2 (-1)					; r2 = (RX, get, incr, get)
+	load r2 r2					; r2 = #[SU, 0, 10, 0]
+	getotype r3 r1				; r3 = ot
+	lea r2 r3					; r2 = #[SU, 0, 10, ot]
+	unseal r2 r2 r1				; r2 = (RO, counter, counter+1, counter)
+	load r2 r2					; r2 = val_counter
+	sub r3 r2 r3				; r3 = val_counter - ot
+	mov r2 pc
+	lea r2 5					; prepare jump to the fail instruction
+	jnz r2 r3					; if r3 != 0, then fail, else return
+	getotype r2 r1				; Case r3 = 0, then get_value and jmp to callback
+	jmp r0						; r2 contains the return value
+	fail 						; Case r3 != 0, then fail
+incr:
+	#[SU, 0, 10, 0]
+	#(RW, incr, incr+1, incr)
+	;; r0 contains callback / r1 = {ot: (RO, counter, counter+1, counter)}
+	mov r2 pc 					; r2 = (RX, incr, end, incr+2)
+	lea r2 (-2)					; r2 = (RX, incr, end, incr)
+	load r3 r2					; r3 = #[SU, 0, 10, ot]
+	unseal r1 r3 r1				; r1 = (RO, counter, counter+1, counter)
+	load r4 r1					; r4 = val_counter
+	add r4 r4 1					; r4 = val_counter + 1
+	store r1 r4					; stores new counter value
+	lea r3 1					; r3 = #[SU, 0, 10, ot+1]
+	lea r2 1					; r2 = (RX, incr, end, incr+1)
+	load r2 r2					; r2 = (RW, incr, incr+1, incr)
+	store r2 r3					; stores new sealrange
+	seal r1 r3 r1				; r1 = {ot+1: (RO, counter, counter+1, counter)}
+	mov r2 0
+	mov r3 0
+	mov r4 0
+	jmp r0
+end:
diff --git a/tests/tester.ml b/tests/tester.ml
index 613981d..03d90ba 100644
--- a/tests/tester.ml
+++ b/tests/tester.ml
@@ -51,7 +51,7 @@ let get_reg_int_word (r : Ast.regname) (m : mchn) (d : Z.t) =
 
 let get_reg_cap_perm (r : regname) (m : mchn) (d : perm) =
   match r @! snd m with
-  | Cap (p, _, _, _) -> p
+  | Sealable (Cap (p, _, _, _)) -> p
   | _ -> d
 
 let test_negatives =
@@ -69,7 +69,7 @@ let test_mov_test =
   let m = run_prog "../../../tests/test_files/pos/mov_test.s" in
   let pc_a = begin
     match get_reg PC @@ snd m with
-    | Cap (_, _, _, a) -> a
+    | Sealable (Cap (_, _, _, a)) -> a
     | _ -> Z.(~$(-1))
   end in
   let r2_res = begin
@@ -111,9 +111,69 @@ let test_jmper =
       `Quick (test_perm E (get_reg_cap_perm (Reg 1) m O));
   ]
 
+let test_getotype =
+  let open Alcotest in
+  let m = run_prog "../../../tests/test_files/pos/get_otype.s" in [
+    test_case
+      "get_otype.s should end in halted state"
+      `Quick (test_state Halted (fst m));
+    test_case
+      "get_otype.s should end with r0 containing (-1)"
+      `Quick (test_const_word Z.(~$(-1)) (get_reg_int_word (Ast.Reg 0) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r1 containing (-1)"
+      `Quick (test_const_word Z.(~$(-1)) (get_reg_int_word (Ast.Reg 1) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r2 containing (-1)"
+      `Quick (test_const_word Z.(~$(-1)) (get_reg_int_word (Ast.Reg 2) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r3 containing 10"
+      `Quick (test_const_word Z.(~$(10)) (get_reg_int_word (Ast.Reg 3) m (Z.zero)));
+  ]
+
+let test_getwtype =
+  let open Alcotest in
+  let m = run_prog "../../../tests/test_files/pos/get_wtype.s" in [
+    test_case
+      "get_otype.s should end in halted state"
+      `Quick (test_state Halted (fst m));
+    test_case
+      "get_otype.s should end with r0 containing 0"
+      `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 0) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r1 containing 0"
+      `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 1) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r2 containing 0"
+      `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 2) m (Z.zero)));
+    test_case
+      "get_otype.s should end with r3 containing 0"
+      `Quick (test_const_word Z.zero (get_reg_int_word (Ast.Reg 3) m (Z.zero)));
+  ]
+
+let test_sealing =
+  let open Alcotest in
+  let m = run_prog "../../../tests/test_files/pos/seal_unseal.s" in [
+    test_case
+      "get_otype.s should end in halted state"
+      `Quick (test_state Halted (fst m));
+  ]
+
+let test_sealing_counter =
+  let open Alcotest in
+  let m = run_prog "../../../tests/test_files/pos/sealing_counter.s" in [
+    test_case
+      "sealing_counter.s should end in halted state"
+      `Quick (test_state Halted (fst m));
+    test_case
+      "sealing_counter.s should end with r2 containing 3"
+      `Quick (test_const_word Z.(~$3) (get_reg_int_word (Ast.Reg 2) m (Z.zero)));
+  ]
+
+
 let () =
   let open Alcotest in
   run "Run" [
-    "Pos", test_mov_test @ test_jmper;
+    "Pos", test_mov_test @ test_jmper @ test_getotype @ test_getwtype @ test_sealing @ test_sealing_counter;
     "Neg", test_negatives;
   ]
diff --git a/tests/test.ml b/tests/tests.ml
similarity index 59%
rename from tests/test.ml
rename to tests/tests.ml
index ffa9bc5..81c0ae0 100644
--- a/tests/test.ml
+++ b/tests/tests.ml
@@ -2,6 +2,7 @@ open Libinterp
 open Libinterp.Pretty_printer
 open Libinterp.Ast
 
+
 let statement_eq (a : statement) (b : statement) = (a = b)
 let pprint_statement = Fmt.of_to_string string_of_statement
 
@@ -14,7 +15,7 @@ let machine_op_tst = Alcotest.testable pprint_machine_op machine_op_eq
 module To_test = struct
   let lex_parse = fun x ->
     List.hd @@ Ir.translate_prog @@ Parser.main Lexer.token @@ Lexing.from_string x
-  let enc_interleave a b = Encode.interleave_int (Z.of_string a) (Z.of_string b)
+  let enc_interleave a b = Ir.interleave_int (Z.of_string a) (Z.of_string b)
   let enc_int a b = Encode.encode_int_int a b
   let enc_split = Encode.split_int
   let enc_dec_int a b = Encode.decode_int @@ Encode.encode_int_int a b
@@ -28,27 +29,46 @@ let make_op_test ((input, expect) : string * statement) =
       expect
       (To_test.lex_parse input))
 
+let encode_const c =
+  Const (Ir.encode_const [] (ConstExpr (IntLit c)))
+let encode_perm p =
+  Const (Ir.encode_const [] (Perm p))
+let encode_seal_perm sp =
+  Const (Ir.encode_const [] (SealPerm sp))
+let encode_wtype wt =
+  Const (Ir.encode_const [] (Wtype wt))
+
 (* TODO add test cases for mul/rem/div *)
 let instr_tests = [
   ("jmp pc", Op (Jmp PC));
-  ("jmp r21", Op (Jmp (Reg 21)));
-  ("jnz r11 r9", Op (Jnz (Reg 11, Reg 9)));
-  ("mov pc -25", Op (Move (PC, const (-25))));
-  ("load r0 r1", Op (Load (Reg 0, Reg 1)));
-  ("store r2 r3", Op (Store (Reg 2, Register (Reg 3))));
-  ("add r4 (10-15) (-37)", Op (Add (Reg 4, const (-5), const (-37))));
-  ("sub r5 6 28", Op (Sub (Reg 5, const 6, const 28)));
-  ("lt r6 496 8128 ; perfect numbers are cool!", Op (Lt (Reg 6, const 496, const 8128)));
-  ("lea r7 r8", Op (Lea (Reg 7, Register (Reg 8))));
-  ("restrict r9 RX", Op (Restrict (Reg 9, CP (Perm RX))));
-  ("subseg r10 pc r11", Op (SubSeg (Reg 10, Register PC, Register (Reg 11))));
-  ("isptr r12 r13", Op (IsPtr (Reg 12, Reg 13)));
-  ("getp r14 r15", Op (GetP (Reg 14, Reg 15)));
-  ("getb r16 r17", Op (GetB (Reg 16, Reg 17)));
-  ("gete r18 r19", Op (GetE (Reg 18, Reg 19)));
-  ("geta r20 r21", Op (GetA (Reg 20, Reg 21)));
+  ("jmp r0", Op (Jmp (Reg 0)));
+  ("jnz r1 r2", Op (Jnz (Reg 1, Reg 2)));
+  ("mov pc 25", Op (Move (PC, encode_const (25))));
+  ("mov r3 -25", Op (Move (Reg 3, encode_const (-25))));
+  ("load r4 r5", Op (Load (Reg 4, Reg 5)));
+  ("store r6 r7", Op (Store (Reg 6, Register (Reg 7))));
+  ("add r8 (10-15) (-37)", Op (Add (Reg 8, encode_const (-5), encode_const (-37))));
+  ("sub r9 6 28", Op (Sub (Reg 9, encode_const 6, encode_const 28)));
+  ("lt r10 496 8128 ; perfect numbers are cool!",
+   Op (Lt (Reg 10, encode_const 496, encode_const 8128)));
+  ("lea r11 r12", Op (Lea (Reg 11, Register (Reg 12))));
+  ("restrict r13 RX", Op (Restrict (Reg 13, (encode_perm RX))));
+  ("restrict r14 S", Op (Restrict (Reg 14, (encode_seal_perm (true,false)))));
+  ("subseg r15 pc r16", Op (SubSeg (Reg 15, Register PC, Register (Reg 16))));
+  ("getb r21 r17", Op (GetB (Reg 21, Reg 17)));
+  ("gete r22 r18", Op (GetE (Reg 22, Reg 18)));
+  ("geta r23 r19", Op (GetA (Reg 23, Reg 19)));
+  ("getp r24 r20", Op (GetP (Reg 24, Reg 20)));
+  ("getotype r25 r26", Op (GetOType (Reg 25, Reg 26)));
+  ("getwtype r27 r28", Op (GetWType (Reg 27, Reg 28)));
+  ("seal r22 r29 r30", Op (Seal (Reg 22, Reg 29, Reg 30)));
+  ("unseal r31 r26 r27", Op (UnSeal (Reg 31, Reg 26, Reg 27)));
   ("fail", Op (Fail));
   ("halt", Op (Halt));
+  ("mov r3 Sealed", Op (Move (Reg 3, encode_wtype W_Sealed)));
+  ("mov r13 SealRange", Op (Move (Reg 13, encode_wtype W_SealRange)));
+  ("mov r23 Cap", Op (Move (Reg 23, encode_wtype W_Cap)));
+  ("mov r30 Int", Op (Move (Reg 30, encode_wtype W_I)));
 ]
 
 let z_tst =
@@ -134,58 +154,63 @@ let test_enc_dec_stm_list = [
   (Jnz (Reg 6, Reg 28), "encode-decode Jnz R6 R28");
   (Move (PC, Register (Reg 7)), "encode-decode Move PC R7");
   (Move (PC, const (-35)), "encode-decode Move PC (-35)");
-  (Move (PC, CP (Perm E)), "encode-decode Move PC E");
+  (Move (PC, (encode_perm E)), "encode-decode Move PC E");
+  (Move (PC, (encode_seal_perm (false, true))), "encode-decode Move PC U");
+  (Move (PC, (encode_wtype W_Cap)), "encode-decode Move PC Cap");
   (Load (Reg 9, PC), "encode-decode Load R9 PC");
   (Store (PC, Register (Reg 7)), "encode-decode Store PC R7");
   (Store (PC, const (-35)), "encode-decode Store PC (-35)");
-  (Store (PC, CP (Perm E)), "encode-decode Store PC E");
+  (Store (PC, (encode_perm E)), "encode-decode Store PC E");
   (Add (Reg 5, Register (Reg 6), Register PC), "encode-decode Add R5 R6 PC");
   (Add (Reg 5, Register (Reg 6), const 8128), "encode-decode Add R5 R6 8128");
-  (Add (Reg 5, Register (Reg 6), CP (Perm RO)), "encode-decode Add R5 R6 RO");
+  (Add (Reg 5, Register (Reg 6), (encode_perm RO)), "encode-decode Add R5 R6 RO");
   (Add (Reg 5, const (-549), Register PC), "encode-decode Add R5 (-549) PC");
   (Add (Reg 5, const (102), const 8128), "encode-decode Add R5 102 8128");
-  (Add (Reg 5, const (83), CP (Perm RO)), "encode-decode Add R5 83 RO");
-  (Add (Reg 5, CP (Perm E), Register PC), "encode-decode Add R5 E PC");
-  (Add (Reg 5, CP (Perm O), const 8128), "encode-decode Add R5 O 8128");
-  (Add (Reg 5, CP (Perm RWX), CP (Perm RO)), "encode-decode Add R5 RWX RO");
+  (Add (Reg 5, const (83), (encode_perm RO)), "encode-decode Add R5 83 RO");
+  (Add (Reg 5, (encode_perm E), Register PC), "encode-decode Add R5 E PC");
+  (Add (Reg 5, (encode_perm O), const 8128), "encode-decode Add R5 O 8128");
+  (Add (Reg 5, (encode_perm RWX), (encode_perm RO)), "encode-decode Add R5 RWX RO");
   (Sub (Reg 5, Register (Reg 6), Register PC), "encode-decode Sub R5 R6 PC");
   (Sub (Reg 5, Register (Reg 6), const 8128), "encode-decode Sub R5 R6 8128");
-  (Sub (Reg 5, Register (Reg 6), CP (Perm RO)), "encode-decode Sub R5 R6 RO");
+  (Sub (Reg 5, Register (Reg 6), (encode_perm RO)), "encode-decode Sub R5 R6 RO");
   (Sub (Reg 5, const (-549), Register PC), "encode-decode Sub R5 (-549) PC");
   (Sub (Reg 5, const (102), const 8128), "encode-decode Sub R5 102 8128");
-  (Sub (Reg 5, const (83), CP (Perm RO)), "encode-decode Sub R5 83 RO");
-  (Sub (Reg 5, CP (Perm E), Register PC), "encode-decode Sub R5 E PC");
-  (Sub (Reg 5, CP (Perm O), const 8128), "encode-decode Sub R5 O 8128");
-  (Sub (Reg 5, CP (Perm RWX), CP (Perm RO)), "encode-decode Sub R5 RWX RO");
+  (Sub (Reg 5, const (83), (encode_perm RO)), "encode-decode Sub R5 83 RO");
+  (Sub (Reg 5, (encode_perm E), Register PC), "encode-decode Sub R5 E PC");
+  (Sub (Reg 5, (encode_perm O), const 8128), "encode-decode Sub R5 O 8128");
+  (Sub (Reg 5, (encode_perm RWX), (encode_perm RO)), "encode-decode Sub R5 RWX RO");
   (Lt (Reg 5, Register (Reg 6), Register PC), "encode-decode Lt R5 R6 PC");
   (Lt (Reg 5, Register (Reg 6), const 8128), "encode-decode Lt R5 R6 8128");
-  (Lt (Reg 5, Register (Reg 6), CP (Perm RO)), "encode-decode Lt R5 R6 RO");
+  (Lt (Reg 5, Register (Reg 6), (encode_perm RO)), "encode-decode Lt R5 R6 RO");
   (Lt (Reg 5, const (-549), Register PC), "encode-decode Lt R5 (-549) PC");
   (Lt (Reg 5, const (102), const 8128), "encode-decode Lt R5 102 8128");
-  (Lt (Reg 5, const (83), CP (Perm RO)), "encode-decode Lt R5 83 RO");
-  (Lt (Reg 5, CP (Perm E), Register PC), "encode-decode Lt R5 E PC");
-  (Lt (Reg 5, CP (Perm O), const 8128), "encode-decode Lt R5 O 8128");
-  (Lt (Reg 5, CP (Perm RWX), CP (Perm RO)), "encode-decode Lt R5 RWX RO");
+  (Lt (Reg 5, const (83), (encode_perm RO)), "encode-decode Lt R5 83 RO");
+  (Lt (Reg 5, (encode_perm E), Register PC), "encode-decode Lt R5 E PC");
+  (Lt (Reg 5, (encode_perm O), const 8128), "encode-decode Lt R5 O 8128");
+  (Lt (Reg 5, (encode_perm RWX), (encode_perm RO)), "encode-decode Lt R5 RWX RO");
   (Lea (PC, Register (Reg 7)), "encode-decode Lea PC R7");
   (Lea (PC, const (-35)), "encode-decode Lea PC (-35)");
-  (Lea (PC, CP (Perm E)), "encode-decode Lea PC E");
+  (Lea (PC, (encode_perm E)), "encode-decode Lea PC E");
   (Restrict (PC, Register (Reg 7)), "encode-decode Restrict PC R7");
   (Restrict (PC, const (-35)), "encode-decode Restrict PC (-35)");
-  (Restrict (PC, CP (Perm E)), "encode-decode Restrict PC E");
+  (Restrict (PC, (encode_perm E)), "encode-decode Restrict PC E");
   (SubSeg (Reg 5, Register (Reg 6), Register PC), "encode-decode SubSeg R5 R6 PC");
   (SubSeg (Reg 5, Register (Reg 6), const 8128), "encode-decode SubSeg R5 R6 8128");
-  (SubSeg (Reg 5, Register (Reg 6), CP (Perm RO)), "encode-decode SubSeg R5 R6 RO");
+  (SubSeg (Reg 5, Register (Reg 6), (encode_perm RO)), "encode-decode SubSeg R5 R6 RO");
   (SubSeg (Reg 5, const (-549), Register PC), "encode-decode SubSeg R5 (-549) PC");
   (SubSeg (Reg 5, const (102), const 8128), "encode-decode SubSeg R5 102 8128");
-  (SubSeg (Reg 5, const (83), CP (Perm RO)), "encode-decode SubSeg R5 83 RO");
-  (SubSeg (Reg 5, CP (Perm E), Register PC), "encode-decode SubSeg R5 E PC");
-  (SubSeg (Reg 5, CP (Perm O), const 8128), "encode-decode SubSeg R5 O 8128");
-  (SubSeg (Reg 5, CP (Perm RWX), CP (Perm RO)), "encode-decode SubSeg R5 RWX RO");
-  (IsPtr (Reg 6, Reg 28), "encode-decode IsPtr R6 R28");
-  (GetP (Reg 6, Reg 28), "encode-decode GetP R6 R28");
-  (GetB (Reg 6, Reg 28), "encode-decode GetB R6 R28");
-  (GetE (Reg 6, Reg 28), "encode-decode GetE R6 R28");
-  (GetA (Reg 6, Reg 28), "encode-decode GetA R6 R28");
+  (SubSeg (Reg 5, const (83), (encode_perm RO)), "encode-decode SubSeg R5 83 RO");
+  (SubSeg (Reg 5, (encode_perm E), Register PC), "encode-decode SubSeg R5 E PC");
+  (SubSeg (Reg 5, (encode_perm O), const 8128), "encode-decode SubSeg R5 O 8128");
+  (SubSeg (Reg 5, (encode_perm RWX), (encode_perm RO)), "encode-decode SubSeg R5 RWX RO");
+  (GetB (Reg 6, Reg 31), "encode-decode GetB R6 R31");
+  (GetE (Reg 7, Reg 30), "encode-decode GetE R7 R30");
+  (GetA (Reg 8, Reg 29), "encode-decode GetA R8 R29");
+  (GetP (Reg 9, Reg 28), "encode-decode GetP R9 R28");
+  (GetOType (Reg 10, Reg 27), "encode-decode GetOType R10 R27");
+  (GetWType (Reg 11, Reg 26), "encode-decode GetWType R11 R26");
+  (Seal (Reg 12, Reg 25, Reg 14), "encode-decode Seal R12 R25 R15");
+  (UnSeal (Reg 13, Reg 24, Reg 15), "encode-decode UnSeal R13 R24 R14");
   (Fail, "encode-decode Fail");
   (Halt, "encode-decode Halt");
 ]