diff --git a/Makefile b/Makefile
index 8e744c17e..dcdf44df4 100644
--- a/Makefile
+++ b/Makefile
@@ -4,6 +4,7 @@ all:
 
 clean:
 	${MAKE} -C src clean
+	${MAKE} -C test clean
 
 .PHONY: test
 test:
diff --git a/src/client/embedded/bootstrap/client_proto_programs.ml b/src/client/embedded/bootstrap/client_proto_programs.ml
index 1ff02fa84..5620b123d 100644
--- a/src/client/embedded/bootstrap/client_proto_programs.ml
+++ b/src/client/embedded/bootstrap/client_proto_programs.ml
@@ -57,49 +57,47 @@ let parse_program s =
   with
   | exn -> report_parse_error "program: " exn lexbuf
 
-let rec print_ir ppf node =
+let rec print_ir locations ppf node =
   let open Script in
   let rec do_seq = function
     | [] -> assert false
-    | [ last ] -> Format.fprintf ppf "%a }@]" print_ir last
-    | fst :: rest -> Format.fprintf ppf "%a ;@ " print_ir fst ; do_seq rest in
+    | [ last ] -> Format.fprintf ppf "%a }@]" (print_ir locations) last
+    | fst :: rest -> Format.fprintf ppf "%a ;@ " (print_ir locations) fst ; do_seq rest in
   let rec do_args = function
     | [] -> assert false
-    | [ last ] -> Format.fprintf ppf "%a@]" print_ir last
-    | fst :: rest -> Format.fprintf ppf "%a@," print_ir fst ; do_args rest in
+    | [ last ] -> Format.fprintf ppf "%a@]" (print_ir locations) last
+    | fst :: rest -> Format.fprintf ppf "%a@," (print_ir locations) fst ; do_args rest in
+  let print_location ppf loc =
+    if locations loc then begin
+      Format.fprintf ppf " /* %d */" loc
+  end in
   match node with
   | String (_, s) -> Format.fprintf ppf "%S" s
   | Int (_, s) -> Format.fprintf ppf "%s" s
-  | Float (_, s) -> Format.fprintf ppf "%s" s
-  | Seq (_, [ one ]) -> print_ir ppf one
+  | Seq (_, [ one ]) -> print_ir locations ppf one
   | Seq (_, []) -> Format.fprintf ppf "{}" ;
   | Seq (_, seq) ->
       Format.fprintf ppf "{ @[<v>" ;
       do_seq seq
-  | Prim (_, "push", [ Prim (_, name, []) ]) ->
-      Format.fprintf ppf "push %s" name
-  | Prim (_, name, []) ->
-      Format.fprintf ppf "%s" name
-  | Prim (_, "push", [ Prim (_, name, seq) ]) ->
-      Format.fprintf ppf "push @[<v 2>%s@," name ;
-      do_args seq
-  | Prim (_, name, seq) ->
-      Format.fprintf ppf "@[<v 2>%s@," name ;
+  | Prim (loc, name, []) ->
+      Format.fprintf ppf "%s%a" name print_location loc
+  | Prim (loc, name, seq) ->
+      Format.fprintf ppf "@[<v 2>%s%a@," name print_location loc;
       do_args seq
 
-let print_program ppf c =
+let print_program locations ppf c =
   Format.fprintf ppf
     "@[<v 2>storage@,%a@]@."
-    print_ir (c : Script.code).Script.storage_type ;
+    (print_ir (fun _ -> false)) (c : Script.code).Script.storage_type ;
   Format.fprintf ppf
     "@[<v 2>parameter@,%a@]@."
-    print_ir (c : Script.code).Script.arg_type ;
+    (print_ir (fun _ -> false)) (c : Script.code).Script.arg_type ;
   Format.fprintf ppf
     "@[<v 2>return@,%a@]@."
-    print_ir (c : Script.code).Script.ret_type ;
+    (print_ir (fun _ -> false)) (c : Script.code).Script.ret_type ;
   Format.fprintf ppf
     "@[<v 2>code@,%a@]"
-    print_ir (c : Script.code).Script.code
+    (print_ir locations) (c : Script.code).Script.code
 
 let parse_data s =
   let lexbuf = Lexing.from_string s in
@@ -119,16 +117,65 @@ let parse_data_type s =
   with
   | exn -> report_parse_error "data_type: " exn lexbuf
 
+let unexpand_macros type_map program =
+  let open Script in
+  let rec caddr type_map acc = function
+    | [] -> Some (List.rev acc)
+    | Prim (loc, "car" , []) :: rest when List.mem_assoc loc type_map ->
+        caddr type_map ((loc, "a") :: acc) rest
+    | Prim (loc, "cdr" , []) :: rest when List.mem_assoc loc type_map ->
+        caddr type_map ((loc, "d") :: acc) rest
+    | _ -> None in
+  let rec unexpand type_map node =
+    match node with
+    | Seq (loc, l) ->
+        begin match caddr type_map [] l with
+          | None ->
+              let type_map, l =
+                List.fold_left
+                  (fun (type_map, acc) e ->
+                     let type_map, e = unexpand type_map e in
+                     type_map, e :: acc)
+                  (type_map, [])
+                  l in
+              type_map, Seq (loc, List.rev l)
+          | Some l ->
+              let locs, steps = List.split l in
+              let name = "c" ^ String.concat "" steps ^ "r" in
+              let first, last = List.hd locs, List.hd (List.rev locs) in
+              let (before, _) = List.assoc first type_map in
+              let (_, after) = List.assoc last type_map in
+              let type_map =
+                List.filter
+                  (fun (loc, _) -> not (List.mem loc locs))
+                  type_map in
+              let type_map = (loc, (before, after)):: type_map in
+              type_map, Prim (loc, name, [])
+        end
+    | oth -> type_map, oth in
+  let type_map, code = unexpand type_map program.code in
+  type_map, { program with code }
+
 module Program = Client_aliases.Alias (struct
     type t = Script.code
     let encoding = Script.code_encoding
     let of_source s = parse_program s
-    let to_source p = Lwt.return (Format.asprintf "%a" print_program p)
+    let to_source p = Lwt.return (Format.asprintf "%a" (print_program (fun _ -> false)) p)
     let name = "program"
   end)
 
 let commands () =
   let open Cli_entries in
+  let show_types = ref false in
+  let show_types_arg =
+    "-details",
+    Arg.Set show_types,
+    "Show the types of each instruction" in
+  let trace_stack = ref false in
+  let trace_stack_arg =
+    "-trace-stack",
+    Arg.Set trace_stack,
+    "Show the stack after each step" in
   register_group "programs" "Commands for managing the record of known programs" ;
   [
     command
@@ -162,17 +209,76 @@ let commands () =
          Program.to_source program >>= fun source ->
          Format.printf "%s\n" source ;
          Lwt.return ()) ;
+    command
+      ~group: "programs"
+      ~desc: "ask the node to run a program"
+      ~args: [ trace_stack_arg ]
+      (prefixes [ "run" ; "program" ]
+       @@ Program.source_param
+       @@ prefixes [ "on" ; "storage" ]
+       @@ Cli_entries.param ~name:"storage" ~desc:"the untagged storage data" parse_data
+       @@ prefixes [ "and" ; "input" ]
+       @@ Cli_entries.param ~name:"storage" ~desc:"the untagged input data" parse_data
+       @@ stop)
+      (fun program storage input () ->
+         let open Data_encoding in
+         if !trace_stack then
+           Client_proto_rpcs.Helpers.trace_code (block ()) program (storage, input) >>= function
+           | Ok (storage, output, trace) ->
+               Format.printf "@[<v 0>@[<v 2>storage@,%a@]@,@[<v 2>output@,%a@]@,@[<v 2>trace@,%a@]@]@."
+                 (print_ir (fun _ -> false)) storage
+                 (print_ir (fun _ -> false)) output
+                 (Format.pp_print_list
+                    (fun ppf (loc, gas, stack) ->
+                       Format.fprintf ppf
+                         "- @[<v 0>location: %d (remaining gas: %d)@,[ @[<v 0>%a ]@]@]"
+                         loc gas
+                         (Format.pp_print_list (print_ir (fun _ -> false)))
+                         stack))
+                 trace ;
+               Lwt.return ()
+           | Error errs ->
+               pp_print_error Format.err_formatter errs ;
+               error "error running program"
+         else
+           Client_proto_rpcs.Helpers.run_code (block ()) program (storage, input) >>= function
+           | Ok (storage, output) ->
+               Format.printf "@[<v 0>@[<v 2>storage@,%a@]@,@[<v 2>output@,%a@]@]@."
+                 (print_ir (fun _ -> false)) storage
+                 (print_ir (fun _ -> false)) output ;
+               Lwt.return ()
+           | Error errs ->
+               pp_print_error Format.err_formatter errs ;
+               error "error running program") ;
     command
       ~group: "programs"
       ~desc: "ask the node to typecheck a program"
+      ~args: [ show_types_arg ]
       (prefixes [ "typecheck" ; "program" ]
        @@ Program.source_param
        @@ stop)
       (fun program () ->
          let open Data_encoding in
          Client_proto_rpcs.Helpers.typecheck_code (block ()) program >>= function
-         | Ok () ->
+         | Ok type_map ->
+             let type_map, program = unexpand_macros type_map program in
              message "Well typed" ;
+             if !show_types then begin
+               print_program
+                 (fun l -> List.mem_assoc l type_map)
+                 Format.std_formatter program ;
+               Format.printf "@." ;
+               List.iter
+                 (fun (loc, (before, after)) ->
+                    Format.printf
+                      "%3d@[<v 0> : [ @[<v 0>%a ]@]@,-> [ @[<v 0>%a ]@]@]@."
+                      loc
+                      (Format.pp_print_list (print_ir (fun _ -> false)))
+                      before
+                      (Format.pp_print_list (print_ir (fun _ -> false)))
+                      after)
+                 (List.sort compare type_map)
+             end ;
              Lwt.return ()
          | Error errs ->
              pp_print_error Format.err_formatter errs ;
diff --git a/src/client/embedded/bootstrap/client_proto_programs.mli b/src/client/embedded/bootstrap/client_proto_programs.mli
index dbec38b52..23e4b8664 100644
--- a/src/client/embedded/bootstrap/client_proto_programs.mli
+++ b/src/client/embedded/bootstrap/client_proto_programs.mli
@@ -11,8 +11,6 @@ val parse_program: string -> Script.code Lwt.t
 val parse_data: string -> Script.expr Lwt.t
 val parse_data_type: string -> Script.expr Lwt.t
 
-val print_program: Format.formatter -> Script.code -> unit
-
 module Program : Client_aliases.Alias with type t = Script.code
 
 val commands: unit -> Cli_entries.command list
diff --git a/src/client/embedded/bootstrap/client_proto_rpcs.ml b/src/client/embedded/bootstrap/client_proto_rpcs.ml
index 5649310d8..ee474b1fc 100644
--- a/src/client/embedded/bootstrap/client_proto_rpcs.ml
+++ b/src/client/embedded/bootstrap/client_proto_rpcs.ml
@@ -127,6 +127,14 @@ module Helpers = struct
 
   let typecheck_code = call_error_service1 Services.Helpers.typecheck_code
 
+  let run_code block code (storage, input) =
+    call_error_service1 Services.Helpers.run_code
+      block (code, storage, input, None, None)
+
+  let trace_code block code (storage, input) =
+    call_error_service1 Services.Helpers.trace_code
+      block (code, storage, input, None, None)
+
   let typecheck_tagged_data = call_error_service1 Services.Helpers.typecheck_tagged_data
 
   let typecheck_untagged_data = call_error_service1 Services.Helpers.typecheck_untagged_data
diff --git a/src/client/embedded/bootstrap/client_proto_rpcs.mli b/src/client/embedded/bootstrap/client_proto_rpcs.mli
index 0cbff7de6..307e8f386 100644
--- a/src/client/embedded/bootstrap/client_proto_rpcs.mli
+++ b/src/client/embedded/bootstrap/client_proto_rpcs.mli
@@ -92,7 +92,14 @@ end
 module Helpers : sig
   val minimal_time:
     block -> ?prio:int -> unit -> Time.t tzresult Lwt.t
-  val typecheck_code: block -> Script.code -> unit tzresult Lwt.t
+  val run_code: block -> Script.code ->
+    (Script.expr * Script.expr) ->
+    (Script.expr * Script.expr) tzresult Lwt.t
+  val trace_code: block -> Script.code ->
+    (Script.expr * Script.expr) ->
+    (Script.expr * Script.expr *
+     (Script.location * int * Script.expr list) list) tzresult Lwt.t
+  val typecheck_code: block -> Script.code -> Script_ir_translator.type_map tzresult Lwt.t
   val typecheck_tagged_data: block -> Script.expr -> unit tzresult Lwt.t
   val typecheck_untagged_data: block -> Script.expr * Script.expr -> unit tzresult Lwt.t
   val hash_data: block -> Script.expr -> string tzresult Lwt.t
diff --git a/src/client/embedded/bootstrap/concrete_lexer.mll b/src/client/embedded/bootstrap/concrete_lexer.mll
index 86a702153..cfaf3ad5b 100644
--- a/src/client/embedded/bootstrap/concrete_lexer.mll
+++ b/src/client/embedded/bootstrap/concrete_lexer.mll
@@ -73,22 +73,6 @@ let char_for_hexadecimal_code lexbuf i =
   in
   char_of_int (val1 * 16 + val2)
 
-
-(* Remove underscores from float literals *)
-
-let remove_underscores s =
-  let s = Bytes.of_string s in
-  let l = Bytes.length s in
-  let rec remove src dst =
-    if Compare.Int.(src >= l) then
-      if Compare.Int.(dst >= l) then s else Bytes.sub s 0 dst
-    else
-     match Bytes.get s src with
-        '_' -> remove (src + 1) dst
-      |  c  -> Bytes.set s dst c; remove (src + 1) (dst + 1)
-  in Bytes.to_string (remove 0 0)
-
-
 (** Lexer state *)
 
 type state = {
@@ -234,11 +218,6 @@ let bin_literal =
   '0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']*
 let int_literal =
   '-' ? ( decimal_literal | hex_literal | oct_literal | bin_literal)
-let float_literal =
-  '-' ?
-  ['0'-'9'] ['0'-'9' '_']*
-  ('.' ['0'-'9' '_']* )?
-    (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)?
 
 rule indent_tokens st nl = parse
 
@@ -332,9 +311,6 @@ and raw_token st = parse
 | int_literal
     { INT (Lexing.lexeme lexbuf) }
 
-| float_literal
-    { FLOAT (remove_underscores (Lexing.lexeme lexbuf)) }
-
 | "\""
     { reset_string_buffer st;
       let string_start = lexbuf.Lexing.lex_start_p in
diff --git a/src/client/embedded/bootstrap/concrete_parser.mly b/src/client/embedded/bootstrap/concrete_parser.mly
index f13270ac5..e5d137b0b 100644
--- a/src/client/embedded/bootstrap/concrete_parser.mly
+++ b/src/client/embedded/bootstrap/concrete_parser.mly
@@ -9,12 +9,11 @@
 %token RPAREN
 %token SEMICOLON
 
-%token <string> FLOAT
 %token <string> INT
 %token <string> PRIM
 %token <string> STRING
 
-%left PRIM INT FLOAT LPAREN LBRACE STRING
+%left PRIM INT LPAREN LBRACE STRING
 %left apply
 
 %start <Script_located_ir.node list> tree
@@ -127,7 +126,7 @@ let expand = function
 let apply node arg =
   match node with
   | Prim (loc, n, args) -> Prim (loc, n, args @ [arg])
-  | Int _ | Float _ | String _ | Seq _ as _node ->
+  | Int _ | String _ | Seq _ as _node ->
       raise (Invalid_application (node_location arg))
 
 let rec apply_seq node = function
@@ -166,7 +165,6 @@ line_node:
 | LBRACE nodes = nodes RBRACE { Seq (pos $startpos $endpos, nodes) }
 | prim = PRIM { Prim (pos $startpos $endpos, prim, []) }
 | i = INT { Int (pos $startpos $endpos, i) }
-| f = FLOAT { Float (pos $startpos $endpos, f) }
 | s = STRING { String (pos $startpos $endpos, s) }
 
 %%
diff --git a/src/client/embedded/bootstrap/script_located_ir.ml b/src/client/embedded/bootstrap/script_located_ir.ml
index dceb0d0b4..b3b123249 100644
--- a/src/client/embedded/bootstrap/script_located_ir.ml
+++ b/src/client/embedded/bootstrap/script_located_ir.ml
@@ -15,14 +15,12 @@ type location =
 
 type node =
   | Int of location * string
-  | Float of location * string
   | String of location * string
   | Prim of location * string * node list
   | Seq of location * node list
 
 let node_location = function
   | Int (loc, _)
-  | Float (loc, _)
   | String (loc, _)
   | Prim (loc, _, _)
   | Seq (loc, _) -> loc
@@ -57,8 +55,6 @@ let strip_locations root =
     match l with
     | Int (_, v) ->
         Script.Int (id, v)
-    | Float (_, v) ->
-        Script.Float (id, v)
     | String (_, v) ->
         Script.String (id, v)
     | Seq (_, seq) ->
diff --git a/src/proto/bootstrap/docs/json-notations.md b/src/proto/bootstrap/docs/json-notations.md
index 334c60d04..ede2933e9 100644
--- a/src/proto/bootstrap/docs/json-notations.md
+++ b/src/proto/bootstrap/docs/json-notations.md
@@ -102,8 +102,6 @@ with the following JSON script description.
       | { "left": [ /* tagged data */, /* type */ ] }
       | { "right": [ /* type */, /* tagged data */ ] }
       | { "or": [ /* type */, /* type */, /* untagged data */ ] }
-      | { "ref": [ /* tagged data */ ] }
-      | { "ref": [ /* type */, /* untagged data */ ] }
       | { "some": [ /* tagged data */ ] }
       | { "some": [ /* type */, /* untagged data */ ] }
       | { "none": [ /* type */ ] }
@@ -135,7 +133,6 @@ with the following JSON script description.
       | { "pair": [ /* untagged data */, /* untagged data */ ] }
       | { "left": [ /* untagged data */ ] }
       | { "right": [ /* untagged data */ ] }
-      | { "ref": [ /* untagged data */ ] }
       | { "some": [ /* untagged data */ ] }
       | "none"
       | { "list": [ /* untagged data */ ... ] }
@@ -161,15 +158,11 @@ with the following JSON script description.
       | { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
       | { "empty_set": [ /* type */ ] }
       | { "empty_map": [ /* comparable type */, /* type */ ] }
-      | "iter"
       | "map"
       | "reduce"
       | "mem"
       | "get"
       | "update"
-      | "ref"
-      | "deref"
-      | "set"
       | { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
       | { "loop": [ [ /* instruction */ ... ] ] }
       | { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] }
@@ -239,7 +232,6 @@ with the following JSON script description.
       | "key"
       | "timestamp"
       | "signature"
-      | { "ref": [ /* type */ ] }
       | { "option": [ /* type */ ] }
       | { "list": [ /* type */ ] }
       | { "set": [ /* comparable type */ ] }
diff --git a/src/proto/bootstrap/docs/language.md b/src/proto/bootstrap/docs/language.md
index e4e85946f..5b0acf825 100644
--- a/src/proto/bootstrap/docs/language.md
+++ b/src/proto/bootstrap/docs/language.md
@@ -32,7 +32,7 @@ I - Type system
 
 The types `T` of values in the stack are written using notations
 
-  * `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`,
+  * `bool`, `string`, `void`, `u?int{8|16|32|64}`,
     the core primitive types,
   * `identifier` for a primitive data-type,
   * `T identifier` for a parametric data-type with one parameter type `T`,
@@ -94,7 +94,6 @@ the form `variable = constant, ...`.
 The constants are of one of the following forms.
 
   * integers with their sign and size, e.g. `(Uint8 3)`,
-  * floats in libc-style notation, e.g. `(Float 4.5e2)`,
   * `Void`, the unique value of type `void`
   * booleans `True` and `False`,
   * string literals, as in `(String "contents")`,
@@ -274,7 +273,7 @@ combinators, and also for branching.
 IV - Data types
 ---------------
 
-   * `bool`, `string`, `void`, `u?int{8|16|32|64}`, `float`:
+   * `bool`, `string`, `void`, `u?int{8|16|32|64}`:
      The core primitive types.
 
    * `list 'a`:
@@ -292,11 +291,8 @@ IV - Data types
      A union of two types, a value holding either a value a of type 'a
      or a value b of type 'b, that we write (Left a) or (Right b).
 
-   * `ref 'a`:
-     Classical imperative stores, that we note (Ref const).
-
    * `set 'a`, `map 'a 'b`:
-     Imperative map and sets, optimized in the db.
+     Immutable map and sets.
 
 
 V - Operations
@@ -507,129 +503,6 @@ Bitwise logical operators are also available on unsigned integers.
 
         :: t : t : 'S   ->   int64 : 'S   where   t in uint{8|16|32|64}
 
-### Operations on Floats
-
-The float type uses double precision IEEE754 semantics, including NaN
-and infinite values.
-
-   * `ADD`
-
-        :: float : float : 'S   ->   float : 'S
-
-        > ADD ; C / x : y : S   =>   C / (x + y) : S
-
-   * `SUB`
-
-        :: float : float : 'S   ->   float : 'S
-
-        > SUB ; C / x : y : S   =>   C / (x - y) : S
-
-   * `MUL`
-
-        :: float : float : 'S   ->   float : 'S
-
-        > MUL ; C / x : y : S   =>   C / (x * y) : S
-
-   * `DIV`
-
-        :: float : float : 'S   ->   float : 'S
-
-        > DIV ; C / x : y : S   =>   C / (x / y) : S
-
-   * `MOD`
-
-        :: float : float : 'S   ->   float : 'S
-
-        > MOD ; C / x : y : S   =>   C / (fmod (x, y)) : S
-
-   * `ABS`
-
-        :: float : 'S   ->   float : 'S
-
-        > ABS ; C / x : S   =>   C / (abs (x)) : S
-
-   * `NEG`
-
-        :: float : 'S   ->   float : 'S
-
-        > NEG ; C / x : S   =>   C / (-x) : S
-
-   * `FLOOR`
-
-        :: float : 'S   ->   float : 'S
-
-        > FLOOR ; C / x : S   =>   C / (floor (x)) : S
-
-   * `CEIL`
-
-        :: float : 'S   ->   float : 'S
-
-        > CEIL ; C / x : S   =>   C / (ceil (x)) : S
-
-   * `INF`
-
-        :: 'S   ->   float : 'S
-
-        > INF ; C / S   =>   C / +Inf : S
-
-   * `NAN`
-
-        :: 'S   ->   float : 'S
-
-        > NAN ; C / S   =>   C / NaN : S
-
-   * `ISNAN`
-
-        :: float : 'S   ->   bool : 'S
-
-        > ISNAN ; C / NaN : S   =>   C / true : S
-        > ISNAN ; C / _ : S     =>   C / false : S
-
-   * `NANAN`
-
-        :: float : 'S   ->   'S
-
-        > NANAN ; C / NaN : S   =>   [FAIL]
-        > NANAN ; C / _ : S     =>   C / S
-
-   * `CAST float`:
-     Conversion from integers.
-
-        :: t_from : 'S   ->   float : 'S   where   t_from in u?int{8|16|32|64}
-
-        > CAST float ; C / x : S   =>   C / float (x) : S
-
-   * `CAST t_to` where `t_to in u?int{8|16|32|64}`:
-     Conversion to integers.
-
-        :: float : 'S   ->   t_to : 'S
-
-        > CAST t_to ; C / NaN : S      =>   C / t_to (0) : S
-        > CAST t_to ; C / +/-Inf : S   =>   C / t_to (0) : S
-        > CAST t_to ; C / x : S        =>   C / t_to (floor (x)) : S
-
-   * `CHECKED_CAST float`:
-     Conversion from integers with overflow checking.
-
-        :: t_from : 'S   ->   float : 'S   where   t_from in u?int{8|16|32|64}
-
-        > CHECKED_CAST float ; C / x : S   =>   [FAIL]   on overflow
-        > CHECKED_CAST float ; C / x : S   =>   C / float (x) : S
-
-   * `CHECKED_CAST t_to` where `t_to in u?int{8|16|32|64}`:
-     Conversion to integers with overflow checking.
-
-        :: float : 'S   ->   t_to : 'S
-
-        > CHECKED_CAST t_to ; C / x : S   =>   [FAIL]   on overflow or NaN
-        > CHECKED_CAST t_to ; C / x : S   =>   C / t_to (floor (x)) : S
-
-
-   * `COMPARE`:
-     IEEE754 comparison
-
-        :: float : float : 'S   ->   int64 : 'S
-
 ### Operations on strings
 
 Strings are mostly used for naming things without having to rely on
@@ -683,49 +556,10 @@ constants as is, concatenate them and use them as keys.
         > CD(\rest)R ; C / S   =>   CDR ; C(\rest)R ; C / S
         > CR ; C / S          =>   C / S
 
-### Operations on refs
-
-   * `REF`:
-     Build a ref from its initial contents.
-
-        :: 'a : 'S   ->   ref 'a : 'S
-
-        > REF ; C / a : S / M   =>   C / l : S / l = (Ref a), M
-
-   * `DEREF`:
-     Access the contents of a ref.
-
-        :: ref 'a : 'S   ->   'a : 'S
-
-        > DEREF ; C / l : S / l = (Ref a), M   =>   C / a : S / l = (Ref a), M
-
-   * `SET`
-     Update the contents of a ref.
-
-        :: 'a : ref 'a : 'S   ->   'S
-
-        > SET ; C / v :: l : S / l = (Ref _), M   =>   C / S / l = (Ref v), M
-
-   * `INCR step`:
-     Increments a counter.
-
-        :: ref 'a : 'S   ->   'S
-           iff   step :: 'a, operator ADD defined on 'a
-
-        > INCR step ; C / l : S / M   =>   DUP ; DEREF ; PUSH step ; ADD ; Set ; C / S / M
-
-   * `DECR step`:
-     Decrements a counter.
-
-        :: ref 'a : 'S   ->   'S
-           iff   step :: 'a, operator SUB defined on 'a
-
-        > DECR step ; C / l : S / M   =>   DUP ; DEREF ; PUSH step ; SUB ; Set ; C / S / M
-
 ### Operations on sets
 
    * `EMPTY_SET 'elt`:
-     Build a new, empty imperative set for elements of a given type.
+     Build a new, empty set for elements of a given type.
 
         :: 'S   ->   set 'elt : 'S
 
@@ -740,12 +574,7 @@ constants as is, concatenate them and use them as keys.
    * `UPDATE`:
      Inserts or removes an element in a set, replacing a previous value.
 
-        :: 'elt : bool : set 'elt : 'S   ->   'S
-
-   * `ITER`:
-     Apply an imperative function over all the elements of a set.
-
-        :: lambda 'elt void : set 'elt : 'S   ->   'S
+        :: 'elt : bool : set 'elt : 'S   ->   set 'elt : 'S
 
    * `REDUCE`:
      Apply a function on a set passing the result of each
@@ -756,7 +585,7 @@ constants as is, concatenate them and use them as keys.
 ### Operations on maps
 
    * `EMPTY_MAP 'key 'val`:
-     Build a new, empty imperative map.
+     Build a new, empty map.
 
      The `'key` type must be comparable (the `COMPARE` primitive must be
      defined over it).
@@ -777,12 +606,7 @@ constants as is, concatenate them and use them as keys.
    * `UPDATE`:
      Assign or remove an element in a map.
 
-        :: 'key : option 'val : map 'key 'val : 'S   ->   'S
-
-   * `ITER`:
-     Apply an imperative function over all the bindings of a map.
-
-        :: lambda (pair 'key 'val) void : map 'key 'val : 'S   ->   'S
+        :: 'key : option 'val : map 'key 'val : 'S   ->   map 'key 'val : 'S
 
    * `MAP`:
      Apply a function on a map and return the map of results under
@@ -874,11 +698,6 @@ constants as is, concatenate them and use them as keys.
         > IF_CONS ; C / (Cons a rest) : S   =>    bt ; C / a : rest : S
         > IF_CONS ; C / Nil : S   =>    bf ; C / S
 
-   * `ITER`:
-     Apply a function on a list from left to right.
-
-        :: lambda 'a void : list 'a : 'S -> 'S
-
    * `MAP`:
      Apply a function on a list from left to right and
      return the list of results in the same order.
@@ -1111,14 +930,11 @@ parsing policy is described just after.
 
 ### Constants
 
-There are three kinds of constants:
+There are two kinds of constants:
 
   1. Integers in decimal (no prefix), hexadecimal (0x prefix), octal
      (0o prefix) or binary (0b prefix).
-  2. Floating point IEEE754 doubles in libc-style notation, with a
-      mandatory period character. (`3` is an `int` but `3.` is a
-      `float`).
-  3. Strings with usual escapes `\n`, `\t`, `\b`, `\r`, `\\`, `\"`.
+  2. Strings with usual escapes `\n`, `\t`, `\b`, `\r`, `\\`, `\"`.
      Strings are encoding agnostic sequences of bytes. Non printable
      characters can be escaped by 3 digits decimal codes `\ddd` or
      2 digit hexadecimal codes `\xHH`.
@@ -1258,8 +1074,6 @@ Capitalised.
 
         Int8 1
 
-        Float 3.5e12
-
     Compound constants such as lists, in order not to repeat the same
     constant constructor for each element, take the type(s) of inner
     values as first argument(s), and then the values without their
@@ -1320,10 +1134,7 @@ data. For this, the code of the contract is checked to be of the
 following type lambda (pair (pair tez 'arg) 'global) -> (pair 'ret
 'global) where 'global is the type of the original global store given
 on origination. The contract also takes a parameter and an amount, and
-returns a value, hence the complete calling convention above.  The
-global values can be updated either by rewriting the object, or by
-putting mutable values in it and performing side effects on them,
-allowing both imperative and functional style.
+returns a value, hence the complete calling convention above.
 
 ### Empty contract
 
@@ -1675,7 +1486,6 @@ X - Full grammar
 
     <tagged data> ::=
       | <string constant>
-      | <float constant>
       | Int8 <int constant>
       | Int16 <int constant>
       | Int32 <int constant>
@@ -1694,8 +1504,6 @@ X - Full grammar
       | Left <tagged data> <type>
       | Right <type> <tagged data>
       | Or <type> <type> <untagged data>
-      | Ref <tagged data>
-      | Ref <type> <untagged data>
       | Some <tagged data>
       | Some <type> <untagged data>
       | None <type>
@@ -1710,7 +1518,6 @@ X - Full grammar
     <untagged data> ::=
       | <int constant>
       | <string constant>
-      | <float constant>
       | <timestamp string constant>
       | <signature string constant>
       | <key string constant>
@@ -1722,7 +1529,6 @@ X - Full grammar
       | Pair <untagged data> <untagged data>
       | Left <untagged data>
       | Right <untagged data>
-      | Ref <untagged data>
       | Some <untagged data>
       | None
       | List <untagged data> ...
@@ -1748,15 +1554,11 @@ X - Full grammar
       | IF_CONS { <instruction> ... } { <instruction> ... }
       | EMPTY_SET <type>
       | EMPTY_MAP <comparable type> <type>
-      | ITER
       | MAP
       | REDUCE
       | MEM
       | GET
       | UPDATE
-      | REF
-      | DEREF
-      | SET
       | IF { <instruction> ... } { <instruction> ... }
       | LOOP { <instruction> ... }
       | LAMBDA <type> <type> { <instruction> ... }
@@ -1820,13 +1622,11 @@ X - Full grammar
       | uint64
       | void
       | string
-      | float
       | tez
       | bool
       | key
       | timestamp
       | signature
-      | ref <type>
       | option <type>
       | list <type>
       | set <comparable type>
@@ -1845,7 +1645,6 @@ X - Full grammar
       | uint32
       | uint64
       | string
-      | float
       | tez
       | bool
       | key
@@ -1880,9 +1679,9 @@ The language is implemented in OCaml as follows:
     interpreting the If instruction.
 
   * The input, untyped internal representation is an OCaml ADT with
-    the only 5 grammar constructions: `String`, `Float`, `Int`, `Seq`
-    and `Prim`.  It is the target language for the parser, since not
-    all parsable programs are well typed, and thus could simply not be
+    the only 5 grammar constructions: `String`, `Int`, `Seq` and
+    `Prim`.  It is the target language for the parser, since not all
+    parsable programs are well typed, and thus could simply not be
     constructed using the GADT.
 
   * The typechecker is a simple function that recognizes the abstract
@@ -1890,7 +1689,7 @@ The language is implemented in OCaml as follows:
     well-typed, corresponding GADT expressions. It is mostly a
     checker, not a full inferer, and thus takes some annotations
     (basically the inpout and output of the program, of lambdas and of
-    uninitialized imperative structures). It works by performing a
+    uninitialized maps and sets). It works by performing a
     symbolic evaluation of the program, transforming a symbolic
     stack. It only needs one pass over the whole program.
 
diff --git a/src/proto/bootstrap/script_interpreter.ml b/src/proto/bootstrap/script_interpreter.ml
index 55bae920a..94f05e6cf 100644
--- a/src/proto/bootstrap/script_interpreter.ml
+++ b/src/proto/bootstrap/script_interpreter.ml
@@ -65,308 +65,246 @@ type 'tys stack =
   | Item : 'ty * 'rest stack -> ('ty * 'rest) stack
   | Empty : end_of_stack stack
 
-let is_nan x = match classify_float x with
-  | FP_nan -> true
-  | _ -> false
-
-let eq_comparable
-  : type a. a comparable_ty -> a -> a -> bool
-  = fun kind x v -> match kind with
-    | String_key -> Compare.String.(x = v)
-    | Bool_key -> Compare.Bool.(x = v)
-    | Float_key -> Compare.Float.(x = v)
-    | Tez_key -> Tez.(x = v)
-    | Key_key -> Ed25519.Public_key_hash.(equal x v)
-    | Int_key kind -> Script_int.(equal kind x v)
-    | Timestamp_key -> Timestamp.(x = v)
+let rec unparse_stack
+  : type a. a stack * a stack_ty -> Script.expr list
+  = function
+    | Empty, Empty_t -> []
+    | Item (v, rest), Item_t (ty, rest_ty) ->
+        unparse_tagged_data ty v :: unparse_stack (rest, rest_ty)
 
 let rec interp
   : type p r.
+    ?log: (Script.location * int * Script.expr list) list ref ->
     int -> Contract.t -> Contract.t -> Tez.t ->
     context -> (p, r) lambda -> p -> (r * int * context) tzresult Lwt.t
-  = fun qta orig source amount ctxt (Lam (code, _)) arg ->
+  = fun ?log qta orig source amount ctxt (Lam (code, _)) arg ->
     let rec step
       : type b a.
-        int -> context -> (b, a) instr -> b stack ->
+        int -> context -> (b, a) descr -> b stack ->
         (a stack * int * context) tzresult Lwt.t =
-      fun qta ctxt instr stack ->
+      fun qta ctxt ({ instr ; loc } as descr) stack ->
         if Compare.Int.(qta <= 0) then
           fail Quota_exceeded
-        else match instr, stack with
+        else
+          let logged_return ((ret, qta, _) as res) =
+            match log with
+            | None -> return res
+            | Some log ->
+                log := (descr.loc, qta, unparse_stack (ret, descr.aft)) :: !log ;
+                return res in
+          match instr, stack with
           (* stack ops *)
           | Drop, Item (_, rest) ->
-              return (rest, qta - 1, ctxt)
+              logged_return (rest, qta - 1, ctxt)
           | Dup, Item (v, rest) ->
-              return (Item (v, Item (v, rest)), qta - 1, ctxt)
+              logged_return (Item (v, Item (v, rest)), qta - 1, ctxt)
           | Swap, Item (vi, Item (vo, rest)) ->
-              return (Item (vo, Item (vi, rest)), qta - 1, ctxt)
+              logged_return (Item (vo, Item (vi, rest)), qta - 1, ctxt)
           | Const v, rest ->
-              return (Item (v, rest), qta - 1, ctxt)
+              logged_return (Item (v, rest), qta - 1, ctxt)
           (* options *)
           | Cons_some, Item (v, rest) ->
-              return (Item (Some v, rest), qta - 1, ctxt)
+              logged_return (Item (Some v, rest), qta - 1, ctxt)
           | Cons_none _, rest ->
-              return (Item (None, rest), qta - 1, ctxt)
+              logged_return (Item (None, rest), qta - 1, ctxt)
           | If_none (bt, _), Item (None, rest) ->
               step qta ctxt bt rest
           | If_none (_, bf), Item (Some v, rest) ->
               step qta ctxt bf (Item (v, rest))
           (* pairs *)
           | Cons_pair, Item (a, Item (b, rest)) ->
-              return (Item ((a, b), rest), qta - 1, ctxt)
+              logged_return (Item ((a, b), rest), qta - 1, ctxt)
           | Car, Item ((a, _), rest) ->
-              return (Item (a, rest), qta - 1, ctxt)
+              logged_return (Item (a, rest), qta - 1, ctxt)
           | Cdr, Item ((_, b), rest) ->
-              return (Item (b, rest), qta - 1, ctxt)
+              logged_return (Item (b, rest), qta - 1, ctxt)
           (* unions *)
           | Left, Item (v, rest) ->
-              return (Item (L v, rest), qta - 1, ctxt)
+              logged_return (Item (L v, rest), qta - 1, ctxt)
           | Right, Item (v, rest) ->
-              return (Item (R v, rest), qta - 1, ctxt)
+              logged_return (Item (R v, rest), qta - 1, ctxt)
           | If_left (bt, _), Item (L v, rest) ->
               step qta ctxt bt (Item (v, rest))
           | If_left (_, bf), Item (R v, rest) ->
               step qta ctxt bf (Item (v, rest))
           (* lists *)
           | Cons_list, Item (hd, Item (tl, rest)) ->
-              return (Item (hd :: tl, rest), qta - 1, ctxt)
+              logged_return (Item (hd :: tl, rest), qta - 1, ctxt)
           | Nil, rest ->
-              return (Item ([], rest), qta - 1, ctxt)
+              logged_return (Item ([], rest), qta - 1, ctxt)
           | If_cons (_, bf), Item ([], rest) ->
               step qta ctxt bf rest
           | If_cons (bt, _), Item (hd :: tl, rest) ->
               step qta ctxt bt (Item (hd, Item (tl, rest)))
-          | List_iter, Item (lam, Item (l, rest)) ->
-              fold_left_s (fun ((), qta, ctxt) arg ->
-                  interp qta orig source amount ctxt lam arg)
-                ((), qta, ctxt) l >>=? fun ((), qta, ctxt) ->
-              return (rest, qta, ctxt)
           | List_map, Item (lam, Item (l, rest)) ->
               fold_left_s (fun (tail, qta, ctxt) arg ->
-                  interp qta orig source amount ctxt lam arg
+                  interp ?log qta orig source amount ctxt lam arg
                   >>=? fun (ret, qta, ctxt) ->
                   return (ret :: tail, qta, ctxt))
                 ([], qta, ctxt) l >>=? fun (res, qta, ctxt) ->
-              return (Item (res, rest), qta, ctxt)
+              logged_return (Item (res, rest), qta, ctxt)
           | List_reduce, Item (lam, Item (l, Item (init, rest))) ->
               fold_left_s
                 (fun (partial, qta, ctxt) arg ->
-                   interp qta orig source amount ctxt lam (arg, partial)
+                   interp ?log qta orig source amount ctxt lam (arg, partial)
                    >>=? fun (partial, qta, ctxt) ->
                    return (partial, qta, ctxt))
                 (init, qta, ctxt) l >>=? fun (res, qta, ctxt) ->
-              return (Item (res, rest), qta, ctxt)
+              logged_return (Item (res, rest), qta, ctxt)
           (* sets *)
           | Empty_set t, rest ->
-              return (Item ((ref [], t), rest), qta - 1, ctxt)
-          | Set_iter, Item (lam, Item ((l, _), rest)) ->
-              fold_left_s (fun ((), qta, ctxt) arg ->
-                  interp qta orig source amount ctxt lam arg)
-                ((), qta, ctxt) !l >>=? fun ((), qta, ctxt) ->
-              return (rest, qta, ctxt)
-          | Set_map t, Item (lam, Item ((l, _), rest)) ->
+              logged_return (Item (empty_set t, rest), qta - 1, ctxt)
+          | Set_map t, Item (lam, Item (set, rest)) ->
+              let items =
+                List.rev (set_fold (fun e acc -> e :: acc) set []) in
               fold_left_s
-                (fun (tail, qta, ctxt) arg ->
-                   interp qta orig source amount ctxt lam arg >>=?
+                (fun (res, qta, ctxt) arg ->
+                   interp ?log qta orig source amount ctxt lam arg >>=?
                    fun (ret, qta, ctxt) ->
-                   return (ret :: tail, qta, ctxt))
-                ([], qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
-              return (Item ((ref res, t), rest), qta, ctxt)
-          | Set_reduce, Item (lam, Item ((l, _), Item (init, rest))) ->
+                   return (set_update ret true res, qta, ctxt))
+                (empty_set t, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
+              logged_return (Item (res, rest), qta, ctxt)
+          | Set_reduce, Item (lam, Item (set, Item (init, rest))) ->
+              let items =
+                List.rev (set_fold (fun e acc -> e :: acc) set []) in
               fold_left_s
                 (fun (partial, qta, ctxt) arg ->
-                   interp qta orig source amount ctxt lam (arg, partial)
+                   interp ?log qta orig source amount ctxt lam (arg, partial)
                    >>=? fun (partial, qta, ctxt) ->
                    return (partial, qta, ctxt))
-                (init, qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
-              return (Item (res, rest), qta, ctxt)
-          | Set_mem, Item (v, Item ((l, kind), rest)) ->
-              return (Item (List.exists (eq_comparable kind v) !l, rest), qta - 1, ctxt)
-          | Set_update, Item (v, Item (false, Item ((l, kind), rest))) ->
-              l := List.filter (fun x -> not (eq_comparable kind x v)) !l ;
-              return (rest, qta - 1, ctxt)
-          | Set_update, Item (v, Item (true, Item ((l, kind), rest))) ->
-              l := v :: List.filter (fun x -> not (eq_comparable kind x v)) !l ;
-              return (rest, qta - 1, ctxt)
+                (init, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
+              logged_return (Item (res, rest), qta, ctxt)
+          | Set_mem, Item (v, Item (set, rest)) ->
+              logged_return (Item (set_mem v set, rest), qta - 1, ctxt)
+          | Set_update, Item (v, Item (presence, Item (set, rest))) ->
+              logged_return (Item (set_update v presence set, rest), qta - 1, ctxt)
           (* maps *)
           | Empty_map (t, _), rest ->
-              return (Item ((ref [], t), rest), qta - 1, ctxt)
-          | Map_iter, Item (lam, Item ((l, _), rest)) ->
+              logged_return (Item (empty_map t, rest), qta - 1, ctxt)
+          | Map_map, Item (lam, Item (map, rest)) ->
+              let items =
+                List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
               fold_left_s
-                (fun ((), qta, ctxt) arg -> interp qta orig source amount ctxt lam arg)
-                ((), qta, ctxt) !l >>=? fun ((), qta, ctxt) ->
-              return (rest, qta, ctxt)
-          | Map_map, Item (lam, Item ((l, t), rest)) ->
-              fold_left_s
-                (fun (tail, qta, ctxt) (k, v) ->
-                   interp qta orig source amount ctxt lam (k, v)
+                (fun (acc, qta, ctxt) (k, v) ->
+                   interp ?log qta orig source amount ctxt lam (k, v)
                    >>=? fun (ret, qta, ctxt) ->
-                   return ((k, ret) :: tail, qta, ctxt))
-                ([], qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
-              return (Item ((ref res, t), rest), qta, ctxt)
-          | Map_reduce, Item (lam, Item ((l, _), Item (init, rest))) ->
+                   return (map_update k (Some ret) acc, qta, ctxt))
+                (empty_map (map_key_ty map), qta, ctxt) items >>=? fun (res, qta, ctxt) ->
+              logged_return (Item (res, rest), qta, ctxt)
+          | Map_reduce, Item (lam, Item (map, Item (init, rest))) ->
+              let items =
+                List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
               fold_left_s
                 (fun (partial, qta, ctxt) arg ->
-                   interp qta orig source amount ctxt lam (arg, partial)
+                   interp ?log qta orig source amount ctxt lam (arg, partial)
                    >>=? fun (partial, qta, ctxt) ->
                    return (partial, qta, ctxt))
-                (init, qta, ctxt) !l >>=? fun (res, qta, ctxt) ->
-              return (Item (res, rest), qta, ctxt)
-          | Map_mem, Item (v, Item ((l, kind), rest)) ->
-              let res = List.exists (fun (k, _) -> eq_comparable kind k v) !l in
-              return (Item (res, rest), qta - 1, ctxt)
-          | Map_get, Item (v, Item ((l, kind), rest)) ->
-              let res =
-                try Some (snd (List.find (fun (k, _) -> eq_comparable kind k v) !l))
-                with Not_found -> None in
-              return (Item (res, rest), qta - 1, ctxt)
-          | Map_update, Item (vk, Item (None, Item ((l, kind), rest))) ->
-              l := List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ;
-              return (rest, qta - 1, ctxt)
-          | Map_update, Item (vk, Item (Some v, Item ((l, kind), rest))) ->
-              l := (vk, v) :: List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ;
-              return (rest, qta - 1, ctxt)
-          (* reference cells *)
-          | Ref, Item (v, rest) ->
-              return (Item (ref v, rest), qta - 1, ctxt)
-          | Deref, Item ({ contents = v}, rest) ->
-              return (Item (v, rest), qta - 1, ctxt)
-          | Set, Item (r, Item (v, rest)) ->
-              r := v ;
-              return (rest, qta - 1, ctxt)
+                (init, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
+              logged_return (Item (res, rest), qta, ctxt)
+          | Map_mem, Item (v, Item (map, rest)) ->
+              logged_return (Item (map_mem v map, rest), qta - 1, ctxt)
+          | Map_get, Item (v, Item (map, rest)) ->
+              logged_return (Item (map_get v map, rest), qta - 1, ctxt)
+          | Map_update, Item (k, Item (v, Item (map, rest))) ->
+              logged_return (Item (map_update k v map, rest), qta - 1, ctxt)
           (* timestamp operations *)
-          | Add_period_to_timestamp, Item (p, Item (t, rest)) ->
-              Lwt.return
-                (Period.of_seconds (Int64.of_float p) >>? fun p ->
-                 Timestamp.(t +? p) >>? fun res ->
-                 Ok (Item (res, rest), qta - 1, ctxt))
-          | Add_seconds_to_timestamp (kind, _pos), Item (n, Item (t, rest)) ->
+          | Add_seconds_to_timestamp kind, Item (n, Item (t, rest)) ->
               let n = Script_int.to_int64 kind n in
               Lwt.return
                 (Period.of_seconds n >>? fun p ->
                  Timestamp.(t +? p) >>? fun res ->
-                 Ok (Item (res, rest), qta - 1, ctxt))
-          | Add_timestamp_to_period, Item (t, Item (p, rest)) ->
-              Lwt.return
-                (Period.of_seconds (Int64.of_float p) >>? fun p ->
-                 Timestamp.(t +? p) >>? fun res ->
-                 Ok (Item (res, rest), qta - 1, ctxt))
-          | Add_timestamp_to_seconds (kind, _pos), Item (t, Item (n, rest)) ->
+                 Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res ->
+              logged_return res
+          | Add_timestamp_to_seconds kind, Item (t, Item (n, rest)) ->
               let n = Script_int.to_int64 kind n in
               Lwt.return
                 (Period.of_seconds n >>? fun p ->
                  Timestamp.(t +? p) >>? fun res ->
-                 Ok (Item (res, rest), qta - 1, ctxt))
+                 Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res ->
+              logged_return res
           (* string operations *)
           | Concat, Item (x, Item (y, rest)) ->
-              return (Item (x ^ y, rest), qta - 1, ctxt)
+              logged_return (Item (x ^ y, rest), qta - 1, ctxt)
           (* currency operations *)
           | Add_tez, Item (x, Item (y, rest)) ->
               Lwt.return Tez.(x +? y) >>=? fun res ->
-              return (Item (res, rest), qta - 1, ctxt)
+              logged_return (Item (res, rest), qta - 1, ctxt)
           | Sub_tez, Item (x, Item (y, rest)) ->
               Lwt.return Tez.(x -? y) >>=? fun res ->
-              return (Item (res, rest), qta - 1, ctxt)
+              logged_return (Item (res, rest), qta - 1, ctxt)
           | Mul_tez kind, Item (x, Item (y, rest)) ->
               Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res ->
-              return (Item (res, rest), qta - 1, ctxt)
+              logged_return (Item (res, rest), qta - 1, ctxt)
           | Mul_tez' kind, Item (y, Item (x, rest)) ->
               Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res ->
-              return (Item (res, rest), qta - 1, ctxt)
-          (* float operations *)
-          | Floor, Item (x, rest) ->
-              return (Item (floor x, rest), qta - 1, ctxt)
-          | Ceil, Item (x, rest) ->
-              return (Item (ceil x, rest), qta - 1, ctxt)
-          | Inf, rest ->
-              return (Item (infinity, rest), qta - 1, ctxt)
-          | NaN, rest ->
-              return (Item (nan, rest), qta - 1, ctxt)
-          | IsNaN, Item (x, rest) ->
-              return (Item (is_nan x, rest), qta - 1, ctxt)
-          | NaNaN pos, Item (x, rest) ->
-              if is_nan x then fail (Reject pos) else return (rest, qta - 1, ctxt)
-          | Abs_float, Item (x, rest) ->
-              return (Item (abs_float x, rest), qta - 1, ctxt)
-          | Neg_float, Item (x, rest) ->
-              return (Item (0. -. x, rest), qta - 1, ctxt)
-          | Add_float, Item (x, Item (y, rest)) ->
-              return (Item (x +. y, rest), qta - 1, ctxt)
-          | Sub_float, Item (x, Item (y, rest)) ->
-              return (Item (x -. y, rest), qta - 1, ctxt)
-          | Mul_float, Item (x, Item (y, rest)) ->
-              return (Item (x *. y, rest), qta - 1, ctxt)
-          | Div_float, Item (x, Item (y, rest)) ->
-              return (Item (x /. y, rest), qta - 1, ctxt)
-          | Mod_float, Item (x, Item (y, rest)) ->
-              return (Item (mod_float x y, rest), qta - 1, ctxt)
+              logged_return (Item (res, rest), qta - 1, ctxt)
           (* boolean operations *)
           | Or, Item (x, Item (y, rest)) ->
-              return (Item (x || y, rest), qta - 1, ctxt)
+              logged_return (Item (x || y, rest), qta - 1, ctxt)
           | And, Item (x, Item (y, rest)) ->
-              return (Item (x && y, rest), qta - 1, ctxt)
+              logged_return (Item (x && y, rest), qta - 1, ctxt)
           | Xor, Item (x, Item (y, rest)) ->
-              return (Item (not x && y || x && not y, rest), qta - 1, ctxt)
+              logged_return (Item (not x && y || x && not y, rest), qta - 1, ctxt)
           | Not, Item (x, rest) ->
-              return (Item (not x, rest), qta - 1, ctxt)
+              logged_return (Item (not x, rest), qta - 1, ctxt)
           (* integer operations *)
-          | Checked_abs_int (kind, pos), Item (x, rest) ->
+          | Checked_abs_int kind, Item (x, rest) ->
               begin match Script_int.checked_abs kind x with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
-          | Checked_neg_int (kind, pos), Item (x, rest) ->
+          | Checked_neg_int kind, Item (x, rest) ->
               begin match Script_int.checked_neg kind x with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
-          | Checked_add_int (kind, pos), Item (x, Item (y, rest)) ->
+          | Checked_add_int kind, Item (x, Item (y, rest)) ->
               begin match Script_int.checked_add kind x y with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
-          | Checked_sub_int (kind, pos), Item (x, Item (y, rest)) ->
+          | Checked_sub_int kind, Item (x, Item (y, rest)) ->
               begin match Script_int.checked_sub kind x y with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
-          | Checked_mul_int (kind, pos), Item (x, Item (y, rest)) ->
+          | Checked_mul_int kind, Item (x, Item (y, rest)) ->
               begin match Script_int.checked_mul kind x y with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
           | Abs_int kind, Item (x, rest) ->
-              return (Item (Script_int.abs kind x, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.abs kind x, rest), qta - 1, ctxt)
           | Neg_int kind, Item (x, rest) ->
-              return (Item (Script_int.neg kind x, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.neg kind x, rest), qta - 1, ctxt)
           | Add_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.add kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.add kind x y, rest), qta - 1, ctxt)
           | Sub_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.sub kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.sub kind x y, rest), qta - 1, ctxt)
           | Mul_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.mul kind x y, rest), qta - 1, ctxt)
-          | Div_int (kind, pos), Item (x, Item (y, rest)) ->
+              logged_return (Item (Script_int.mul kind x y, rest), qta - 1, ctxt)
+          | Div_int kind, Item (x, Item (y, rest)) ->
               if Compare.Int64.(Script_int.to_int64 kind y = 0L) then
-                fail (Division_by_zero pos)
+                fail (Division_by_zero loc)
               else
-                return (Item (Script_int.div kind x y, rest), qta - 1, ctxt)
-          | Mod_int (kind, pos), Item (x, Item (y, rest)) ->
+                logged_return (Item (Script_int.div kind x y, rest), qta - 1, ctxt)
+          | Mod_int kind, Item (x, Item (y, rest)) ->
               if Compare.Int64.(Script_int.to_int64 kind y = 0L) then
-                fail (Division_by_zero pos)
+                fail (Division_by_zero loc)
               else
-                return (Item (Script_int.rem kind x y, rest), qta - 1, ctxt)
+                logged_return (Item (Script_int.rem kind x y, rest), qta - 1, ctxt)
           | Lsl_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.logsl kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.logsl kind x y, rest), qta - 1, ctxt)
           | Lsr_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.logsr kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.logsr kind x y, rest), qta - 1, ctxt)
           | Or_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.logor kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.logor kind x y, rest), qta - 1, ctxt)
           | And_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.logand kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.logand kind x y, rest), qta - 1, ctxt)
           | Xor_int kind, Item (x, Item (y, rest)) ->
-              return (Item (Script_int.logxor kind x y, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.logxor kind x y, rest), qta - 1, ctxt)
           | Not_int kind, Item (x, rest) ->
-              return (Item (Script_int.lognot kind x, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.lognot kind x, rest), qta - 1, ctxt)
           (* control *)
           | Seq (hd, tl), stack ->
               step qta ctxt hd stack >>=? fun (trans, qta, ctxt) ->
@@ -377,93 +315,83 @@ let rec interp
               step qta ctxt bf rest
           | Loop body, Item (true, rest) ->
               step qta ctxt body rest >>=? fun (trans, qta, ctxt) ->
-              step (qta - 1) ctxt (Loop body) trans
+              step (qta - 1) ctxt descr trans
           | Loop _, Item (false, rest) ->
-              return (rest, qta, ctxt)
+              logged_return (rest, qta, ctxt)
           | Dip b, Item (ign, rest) ->
               step qta ctxt b rest >>=? fun (res, qta, ctxt) ->
-              return (Item (ign, res), qta, ctxt)
+              logged_return (Item (ign, res), qta, ctxt)
           | Exec, Item (arg, Item (lam, rest)) ->
-              interp qta orig source amount ctxt lam arg >>=? fun (res, qta, ctxt) ->
-              return (Item (res, rest), qta - 1, ctxt)
+              interp ?log qta orig source amount ctxt lam arg >>=? fun (res, qta, ctxt) ->
+              logged_return (Item (res, rest), qta - 1, ctxt)
           | Lambda lam, rest ->
-              return (Item (lam, rest), qta - 1, ctxt)
-          | Fail pos, _ ->
-              fail (Reject pos)
+              logged_return (Item (lam, rest), qta - 1, ctxt)
+          | Fail, _ ->
+              fail (Reject loc)
           | Nop, stack ->
-              return (stack, qta - 1, ctxt)
+              logged_return (stack, qta - 1, ctxt)
           (* comparison *)
           | Compare Bool_key, Item (a, Item (b, rest)) ->
               let cmpres = Compare.Bool.compare a b in
               let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Compare String_key, Item (a, Item (b, rest)) ->
               let cmpres = Compare.String.compare a b in
               let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
-          | Compare Float_key, Item (a, Item (b, rest)) ->
-              let cmpres = Compare.Float.compare a b in
-              let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Compare Tez_key, Item (a, Item (b, rest)) ->
               let cmpres = Tez.compare a b in
               let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Compare (Int_key kind), Item (a, Item (b, rest)) ->
               let cmpres = Script_int.compare kind a b in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Compare Key_key, Item (a, Item (b, rest)) ->
               let cmpres = Ed25519.Public_key_hash.compare a b in
               let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Compare Timestamp_key, Item (a, Item (b, rest)) ->
               let cmpres = Timestamp.compare a b in
               let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           (* comparators *)
           | Eq, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres = 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Neq, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres <> 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Lt, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres < 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Gt, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres > 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Le, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres <= 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           | Ge, Item (cmpres, rest) ->
               let cmpres = Script_int.to_int64 Int64 cmpres in
               let cmpres = Compare.Int64.(cmpres >= 0L) in
-              return (Item (cmpres, rest), qta - 1, ctxt)
+              logged_return (Item (cmpres, rest), qta - 1, ctxt)
           (* casts *)
-          | Checked_int_of_int (_, kt, pos), Item (v, rest) ->
+          | Checked_int_of_int (_, kt), Item (v, rest) ->
               begin match Script_int.checked_cast kt v with
-                | None -> fail (Overflow pos)
-                | Some res -> return (Item (res, rest), qta - 1, ctxt)
+                | None -> fail (Overflow loc)
+                | Some res -> logged_return (Item (res, rest), qta - 1, ctxt)
               end
           | Int_of_int (_, kt), Item (v, rest) ->
-              return (Item (Script_int.cast kt v, rest), qta - 1, ctxt)
-          | Int_of_float kt, Item (v, rest) ->
-              let v = Int64.of_float v in
-              return (Item (Script_int.of_int64 kt v, rest), qta - 1, ctxt)
-          | Float_of_int kf, Item (v, rest) ->
-              let v = Int64.to_float (Script_int.to_int64 kf v) in
-              return (Item (v, rest), qta - 1, ctxt)
+              logged_return (Item (Script_int.cast kt v, rest), qta - 1, ctxt)
           (* protocol *)
           | Manager, Item ((_, _, contract), rest) ->
               Contract.get_manager ctxt contract >>=? fun manager ->
-              return (Item (manager, rest), qta - 1, ctxt)
-          | Transfer_tokens (storage_type, loc),
+              logged_return (Item (manager, rest), qta - 1, ctxt)
+          | Transfer_tokens storage_type,
             Item (p, Item (amount, Item ((tp, Void_t, destination), Item (sto, Empty)))) -> begin
               Contract.unconditional_spend ctxt source amount >>=? fun ctxt ->
               Contract.credit ctxt destination amount >>=? fun ctxt ->
@@ -491,39 +419,39 @@ let rec interp
                   | No_script -> assert false
                   | Script { storage = { storage } } ->
                       parse_untagged_data ctxt storage_type storage >>=? fun sto ->
-                      return (Item ((), Item (sto, Empty)), qta - 1, ctxt))
-              end
-            | Transfer_tokens (storage_type, loc),
-              Item (p, Item (amount, Item ((tp, tr, destination), Item (sto, Empty)))) -> begin
-                Contract.unconditional_spend ctxt source amount >>=? fun ctxt ->
-                Contract.credit ctxt destination amount >>=? fun ctxt ->
-                Contract.get_script ctxt destination >>=? function
-                | No_script -> fail (Invalid_contract (loc, destination))
-                | Script { code ; storage } ->
-                    let sto = unparse_untagged_data storage_type sto in
-                    Contract.update_script_storage ctxt source sto >>=? fun ctxt ->
-                    let p = unparse_untagged_data tp p in
-                    execute source destination ctxt storage code amount p qta
-                    >>=? fun (sto, ret, qta, ctxt) ->
-                    Contract.update_script_storage
-                      ctxt destination sto >>=? fun ctxt ->
-                    trace
-                      (Invalid_contract (loc, destination))
-                      (parse_untagged_data ctxt tr ret) >>=? fun v ->
-                    Contract.get_script ctxt source >>=? (function
-                        | No_script -> assert false
-                        | Script { storage = { storage } } ->
-                            parse_untagged_data ctxt storage_type storage >>=? fun sto ->
-                            return (Item (v, Item (sto, Empty)), qta - 1, ctxt))
-              end
-            | Create_account,
-              Item (manager, Item (delegate, Item (delegatable, Item (credit, rest)))) ->
+                      logged_return (Item ((), Item (sto, Empty)), qta - 1, ctxt))
+            end
+          | Transfer_tokens storage_type,
+            Item (p, Item (amount, Item ((tp, tr, destination), Item (sto, Empty)))) -> begin
+              Contract.unconditional_spend ctxt source amount >>=? fun ctxt ->
+              Contract.credit ctxt destination amount >>=? fun ctxt ->
+              Contract.get_script ctxt destination >>=? function
+              | No_script -> fail (Invalid_contract (loc, destination))
+              | Script { code ; storage } ->
+                  let sto = unparse_untagged_data storage_type sto in
+                  Contract.update_script_storage ctxt source sto >>=? fun ctxt ->
+                  let p = unparse_untagged_data tp p in
+                  execute source destination ctxt storage code amount p qta
+                  >>=? fun (sto, ret, qta, ctxt) ->
+                  Contract.update_script_storage
+                    ctxt destination sto >>=? fun ctxt ->
+                  trace
+                    (Invalid_contract (loc, destination))
+                    (parse_untagged_data ctxt tr ret) >>=? fun v ->
+                  Contract.get_script ctxt source >>=? (function
+                      | No_script -> assert false
+                      | Script { storage = { storage } } ->
+                          parse_untagged_data ctxt storage_type storage >>=? fun sto ->
+                          logged_return (Item (v, Item (sto, Empty)), qta - 1, ctxt))
+            end
+          | Create_account,
+            Item (manager, Item (delegate, Item (delegatable, Item (credit, rest)))) ->
               Contract.unconditional_spend ctxt source credit >>=? fun ctxt ->
               Lwt.return Tez.(credit -? Constants.origination_burn) >>=? fun balance ->
               Contract.originate ctxt
                 ~manager ~delegate ~balance
                 ~script:No_script ~spendable:true ~delegatable >>=? fun (ctxt, contract) ->
-              return (Item ((Void_t, Void_t, contract), rest), qta - 1, ctxt)
+              logged_return (Item ((Void_t, Void_t, contract), rest), qta - 1, ctxt)
           | Create_contract (g, p, r),
             Item (manager, Item (delegate, Item (delegatable, Item (credit,
                                                                     Item (Lam (_, code), Item (init, rest)))))) ->
@@ -543,35 +471,43 @@ let rec interp
                 ~manager ~delegate ~balance
                 ~script:(Script { code ; storage }) ~spendable:true ~delegatable
               >>=? fun (ctxt, contract) ->
-              return (Item ((p, r, contract), rest), qta - 1, ctxt)
+              logged_return (Item ((p, r, contract), rest), qta - 1, ctxt)
           | Balance, rest ->
               Contract.get_balance ctxt source >>=? fun balance ->
-              return (Item (balance, rest), qta - 1, ctxt)
+              logged_return (Item (balance, rest), qta - 1, ctxt)
           | Now, rest ->
               Timestamp.get_current ctxt >>=? fun now ->
-              return (Item (now, rest), qta - 1, ctxt)
+              logged_return (Item (now, rest), qta - 1, ctxt)
           | Check_signature, Item (key, Item ((signature, message), rest)) ->
               Public_key.get ctxt key >>=? fun key ->
               let message = MBytes.of_string message in
               let res = Ed25519.check_signature key signature message in
-              return (Item (res, rest), qta - 1, ctxt)
+              logged_return (Item (res, rest), qta - 1, ctxt)
           | H ty, Item (v, rest) ->
               let hash = Script.hash_expr (unparse_untagged_data ty v) in
-              return (Item (hash, rest), qta - 1, ctxt)
+              logged_return (Item (hash, rest), qta - 1, ctxt)
           | Steps_to_quota, rest ->
               let steps = Script_int.of_int64 Uint32 (Int64.of_int qta) in
-              return (Item (steps, rest), qta - 1, ctxt)
+              logged_return (Item (steps, rest), qta - 1, ctxt)
           | Source (ta, tb), rest ->
-              return (Item ((ta, tb, orig), rest), qta - 1, ctxt)
+              logged_return (Item ((ta, tb, orig), rest), qta - 1, ctxt)
           | Amount, rest ->
-              return (Item (amount, rest), qta - 1, ctxt)
+              logged_return (Item (amount, rest), qta - 1, ctxt)
     in
-    step qta ctxt code (Item (arg, Empty)) >>=? fun (Item (ret, Empty), qta, ctxt) ->
+    let stack = (Item (arg, Empty)) in
+    begin match log with
+      | None -> ()
+      | Some log ->
+          log := (code.loc, qta, unparse_stack (stack, code.bef)) :: !log
+    end ;
+    step qta ctxt code stack >>=? fun (Item (ret, Empty), qta, ctxt) ->
     return (ret, qta, ctxt)
 
 (* ---- contract handling ---------------------------------------------------*)
 
-and execute orig source ctxt { storage; storage_type } { code; arg_type; ret_type } amount arg qta =
+and execute ?log orig source ctxt storage script amount arg qta =
+  let { Script.storage ; storage_type } = storage in
+  let { Script.code ; arg_type ; ret_type } = script in
   parse_ty arg_type >>=? fun (Ex arg_type) ->
   parse_ty ret_type >>=? fun (Ex ret_type) ->
   parse_ty storage_type >>=? fun (Ex storage_type) ->
@@ -580,8 +516,17 @@ and execute orig source ctxt { storage; storage_type } { code; arg_type; ret_typ
   parse_lambda ctxt arg_type_full ret_type_full code >>=? fun lambda ->
   parse_untagged_data ctxt arg_type arg >>=? fun arg ->
   parse_untagged_data ctxt storage_type storage >>=? fun storage ->
-  interp qta orig source amount ctxt lambda ((amount, arg), storage) >>=? fun (ret, qta, ctxt) ->
-              let ret, storage = ret in
-              return (unparse_untagged_data storage_type storage,
-                      unparse_untagged_data ret_type ret,
-                      qta, ctxt)
+  interp ?log qta orig source amount ctxt lambda ((amount, arg), storage)
+  >>=? fun (ret, qta, ctxt) ->
+  let ret, storage = ret in
+  return (unparse_untagged_data storage_type storage,
+          unparse_untagged_data ret_type ret,
+          qta, ctxt)
+
+let trace orig source ctxt storage script amount arg qta =
+  let log = ref [] in
+  execute ~log orig source ctxt storage script amount arg qta >>=? fun res ->
+  return (res, List.rev !log)
+
+let execute orig source ctxt storage script amount arg qta =
+  execute orig source ctxt storage script amount arg qta
diff --git a/src/proto/bootstrap/script_interpreter.mli b/src/proto/bootstrap/script_interpreter.mli
index 9a32c7987..3fbae676f 100644
--- a/src/proto/bootstrap/script_interpreter.mli
+++ b/src/proto/bootstrap/script_interpreter.mli
@@ -21,3 +21,9 @@ val execute: Contract.t -> Contract.t -> Tezos_context.t ->
   Script.storage -> Script.code -> Tez.t ->
   Script.expr -> int ->
   (Script.expr * Script.expr * int * context) tzresult Lwt.t
+
+val trace: Contract.t -> Contract.t -> Tezos_context.t ->
+  Script.storage -> Script.code -> Tez.t ->
+  Script.expr -> int ->
+  ((Script.expr * Script.expr * int * context) *
+   (Script.location * int * Script.expr list) list) tzresult Lwt.t
diff --git a/src/proto/bootstrap/script_ir_translator.ml b/src/proto/bootstrap/script_ir_translator.ml
index 944c91d21..285c14005 100644
--- a/src/proto/bootstrap/script_ir_translator.ml
+++ b/src/proto/bootstrap/script_ir_translator.ml
@@ -14,10 +14,6 @@ open Script_typed_ir
 
 (* ---- Error reporting -----------------------------------------------------*)
 
-type 'ty stack_ty =
-  | Item_t : 'ty ty * 'rest stack_ty -> ('ty * 'rest) stack_ty
-  | Empty_t : end_of_stack stack_ty
-
 (* Boxed existentials types to put in exception constructors *)
 type stack_ty_val = Stack_ty : _ stack_ty -> stack_ty_val
 type ty_val =
@@ -33,6 +29,7 @@ type error += Invalid_constant of Script.location * string
 type error += Invalid_primitive of Script.location * kind * string
 type error += Invalid_expression_kind of Script.location (* TODO: expected *)
 type error += Sequence_parameter_expected of Script.location * kind * string * int
+type error += Fail_not_in_tail_position of Script.location
 
 (* Instruction errors *)
 type error += Comparable_type_expected of Script.location
@@ -71,7 +68,6 @@ let () =
 
 let location = function
   | Prim (loc, _, _)
-  | Float (loc, _)
   | Int (loc, _)
   | String (loc, _)
   | Seq (loc, _) -> loc
@@ -132,7 +128,6 @@ let rec ty_eq
         record_trace (Inconsistent_types (Ty ta, Ty tb))
     | String_t, String_t -> eq ta tb
     | Signature_t, Signature_t -> eq ta tb
-    | Float_t, Float_t -> eq ta tb
     | Tez_t, Tez_t -> eq ta tb
     | Timestamp_t, Timestamp_t -> eq ta tb
     | Bool_t, Bool_t -> eq ta tb
@@ -156,10 +151,6 @@ let rec ty_eq
          ty_eq tar tbr >>? fun (Eq _) ->
          (eq ta tb : (ta ty, tb ty) eq tzresult)) |>
         record_trace (Inconsistent_types (Ty ta, Ty tb))
-    | Ref_t tva, Ref_t tvb ->
-        (ty_eq tva tvb >>? fun (Eq _) ->
-         (eq ta tb : (ta ty, tb ty) eq tzresult)) |>
-        record_trace (Inconsistent_types (Ty ta, Ty tb))
     | Option_t tva, Option_t tvb ->
         (ty_eq tva tvb >>? fun (Eq _) ->
          (eq ta tb : (ta ty, tb ty) eq tzresult)) |>
@@ -182,13 +173,139 @@ let rec stack_ty_eq
   | Empty_t, Empty_t -> eq ta tb
   | _, _ -> error Inconsistent_stack_lengths
 
+(* ---- Sets and Maps -------------------------------------------------------*)
+
+let compare_comparable
+  : type a. a comparable_ty -> a -> a -> int
+  = fun kind x y -> match kind with
+    | String_key -> Compare.String.compare x y
+    | Bool_key -> Compare.Bool.compare x y
+    | Tez_key -> Tez.compare x y
+    | Key_key -> Ed25519.Public_key_hash.compare x y
+    | Int_key kind ->
+        let res =
+          Script_int.to_int64 Script_int.Int64
+            (Script_int.compare kind x y) in
+        if Compare.Int64.(res = 0L) then 0
+        else if Compare.Int64.(res > 0L) then 1
+        else -1
+    | Timestamp_key -> Timestamp.compare x y
+
+let empty_set
+  : type a. a comparable_ty -> a set
+  = fun ty ->
+    let module OPS = Set.Make (struct
+        type t = a
+        let compare = compare_comparable ty
+      end) in
+    (module struct
+      type elt = a
+      module OPS = OPS
+      let boxed = OPS.empty
+    end)
+
+let set_update
+  : type a. a -> bool -> a set -> a set
+  = fun v b (module Box) ->
+    (module struct
+      type elt = a
+      module OPS = Box.OPS
+      let boxed =
+        if b then
+          Box.OPS.add v Box.boxed
+        else
+          Box.OPS.remove v Box.boxed
+    end)
+
+let set_mem
+  : type elt. elt -> elt set -> bool
+  = fun v (module Box) ->
+    Box.OPS.mem v Box.boxed
+
+let set_fold
+  : type elt acc. (elt -> acc -> acc) -> elt set -> acc -> acc
+  = fun f (module Box) ->
+    Box.OPS.fold f Box.boxed
+
+let map_key_ty
+  : type a b. (a, b) map -> a comparable_ty
+  = fun (module Box) -> Box.key_ty
+
+let empty_map
+  : type a b. a comparable_ty -> (a, b) map
+  = fun ty ->
+    let module OPS = Map.Make (struct
+        type t = a
+        let compare = compare_comparable ty
+      end) in
+    (module struct
+      type key = a
+      type value = b
+      let key_ty = ty
+      module OPS = OPS
+      let boxed = OPS.empty
+    end)
+
+let map_get
+  : type key value. key -> (key, value) map -> value option
+  = fun k (module Box) ->
+    try Some (Box.OPS.find k Box.boxed) with Not_found -> None
+
+let map_update
+  : type a b. a -> b option -> (a, b) map -> (a, b) map
+  = fun k v (module Box) ->
+    (module struct
+      type key = a
+      type value = b
+      let key_ty = Box.key_ty
+      module OPS = Box.OPS
+      let boxed =
+        match v with
+        | Some v -> Box.OPS.add k v Box.boxed
+        | None -> Box.OPS.remove k Box.boxed
+    end)
+
+let map_mem
+  : type key value. key -> (key, value) map -> bool
+  = fun k (module Box) ->
+    Box.OPS.mem k Box.boxed
+
+let map_fold
+  : type key value acc. (key -> value -> acc -> acc) -> (key, value) map -> acc -> acc
+  = fun f (module Box) ->
+    Box.OPS.fold f Box.boxed
+
 (* ---- Type checker resuls -------------------------------------------------*)
 
 type 'bef judgement =
-  | Typed : ('bef, 'aft) instr * 'aft stack_ty -> 'bef judgement
+  | Typed : ('bef, 'aft) descr -> 'bef judgement
+  | Failed : { descr : 'aft. 'aft stack_ty -> ('bef, 'aft) descr } -> 'bef judgement
 
 (* ---- type checker --------------------------------------------------------*)
 
+type ('t, 'f, 'b) branch =
+  { branch : 'r. ('t, 'r) descr -> ('f, 'r) descr -> ('b, 'r) descr } [@@unboxed]
+
+let merge_branches
+  : type bef a b. int -> a judgement -> b judgement ->
+    (a, b, bef) branch ->
+    bef judgement tzresult Lwt.t
+  = fun loc btr bfr { branch } ->
+    match btr, bfr with
+    | Typed ({ aft = aftbt } as dbt), Typed ({ aft = aftbf } as dbf) ->
+        trace
+          (Unmatched_branches (loc, Stack_ty aftbt, Stack_ty aftbf))
+          (Lwt.return (stack_ty_eq 0 aftbt aftbf)) >>=? fun (Eq _) ->
+        return (Typed (branch dbt dbf))
+    | Failed { descr = descrt }, Failed { descr = descrf } ->
+        let descr ret =
+          branch (descrt ret) (descrf ret) in
+        return (Failed { descr })
+    | Typed dbt, Failed { descr = descrf } ->
+        return (Typed (branch dbt (descrf dbt.aft)))
+    | Failed { descr = descrt }, Typed dbf ->
+        return (Typed (branch (descrt dbf.aft) dbf))
+
 type ex_comparable_ty = Ex : 'a comparable_ty -> ex_comparable_ty
 
 let parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult Lwt.t = function
@@ -201,15 +318,14 @@ let parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult Lwt.t = funct
   | Prim (_, "uint32", []) -> return @@ Ex (Int_key Uint32)
   | Prim (_, "uint64", []) -> return @@ Ex (Int_key Uint64)
   | Prim (_, "string", []) -> return @@ Ex String_key
-  | Prim (_, "float", []) -> return @@ Ex Float_key
   | Prim (_, "tez", []) -> return @@ Ex Tez_key
   | Prim (_, "bool", []) -> return @@ Ex Bool_key
   | Prim (_, "key", []) -> return @@ Ex Key_key
   | Prim (_, "timestamp", []) -> return @@ Ex Timestamp_key
   | Prim (loc, ("int8" | "int16" | "int32" | "int64"
-             | "uint8" | "uint16" | "uint32" | "uint64"
-             | "string" | "float" | "tez" | "bool"
-             | "key" | "timestamp" as prim), l) ->
+               | "uint8" | "uint16" | "uint32" | "uint64"
+               | "string" | "tez" | "bool"
+               | "key" | "timestamp" as prim), l) ->
       fail @@ Invalid_arity (loc, Type, prim, 0, List.length l)
   | Prim (loc, ("pair" | "union" | "set" | "map"
                | "list" | "ref"  | "option"  | "lambda"
@@ -217,7 +333,7 @@ let parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult Lwt.t = funct
       fail @@ Comparable_type_expected loc
   | Prim (loc, prim, _) ->
       fail @@ Invalid_primitive (loc, Type, prim)
-  | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)  ->
+  | Int (loc, _) | String (loc, _) | Seq (loc, _)  ->
       fail @@ Invalid_expression_kind loc
 
 type ex_ty = Ex : 'a ty -> ex_ty
@@ -233,7 +349,6 @@ let rec parse_ty : Script.expr -> ex_ty tzresult Lwt.t = function
   | Prim (_, "uint32", []) -> return @@ Ex (Int_t Uint32)
   | Prim (_, "uint64", []) -> return @@ Ex (Int_t Uint64)
   | Prim (_, "string", []) -> return @@ Ex String_t
-  | Prim (_, "float", []) -> return @@ Ex Float_t
   | Prim (_, "tez", []) -> return @@ Ex Tez_t
   | Prim (_, "bool", []) -> return @@ Ex Bool_t
   | Prim (_, "key", []) -> return @@ Ex Key_t
@@ -255,9 +370,6 @@ let rec parse_ty : Script.expr -> ex_ty tzresult Lwt.t = function
       parse_ty uta >>=? fun (Ex ta) ->
       parse_ty utr >>=? fun (Ex tr) ->
       return @@ Ex (Lambda_t (ta, tr))
-  | Prim (_, "ref", [ ut ]) ->
-      parse_ty ut >>=? fun (Ex t) ->
-      return @@ Ex (Ref_t t)
   | Prim (_, "option", [ ut ]) ->
       parse_ty ut >>=? fun (Ex t) ->
       return @@ Ex (Option_t t)
@@ -276,19 +388,18 @@ let rec parse_ty : Script.expr -> ex_ty tzresult Lwt.t = function
                | "void" | "signature"  | "contract"
                | "int8" | "int16" | "int32" | "int64"
                | "uint8" | "uint16" | "uint32" | "uint64"
-               | "string" | "float" | "tez" | "bool"
+               | "string" | "tez" | "bool"
                | "key" | "timestamp" as prim), l) ->
       fail @@ Invalid_arity (loc, Type, prim, 0, List.length l)
   | Prim (loc, prim, _) ->
       fail @@ Invalid_primitive (loc, Type, prim)
-  | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)  ->
+  | Int (loc, _) | String (loc, _) | Seq (loc, _)  ->
       fail @@ Invalid_expression_kind loc
 
 let ty_of_comparable_ty
   : type a. a comparable_ty -> a ty = function
   | Int_key k -> Int_t k
   | String_key -> String_t
-  | Float_key -> Float_t
   | Tez_key -> Tez_t
   | Bool_key -> Bool_t
   | Key_key -> Key_t
@@ -298,7 +409,6 @@ let comparable_ty_of_ty
   : type a. a ty -> a comparable_ty tzresult = function
   | Int_t k -> ok (Int_key k)
   | String_t -> ok String_key
-  | Float_t -> ok Float_key
   | Tez_t -> ok Tez_key
   | Bool_t -> ok Bool_key
   | Key_t -> ok Key_key
@@ -335,16 +445,6 @@ let rec parse_tagged_data
         return @@ Ex (Bool_t, v)
     | Prim (loc, "bool", l) ->
         fail @@ Invalid_arity (loc, Constant, "bool", 1, List.length l)
-    | Float (loc, v) -> begin try
-          return (Ex (Float_t, float_of_string v))
-        with _ ->
-          fail @@ Invalid_constant (loc, "float")
-      end
-    | Prim (_, "float", [ arg ]) ->
-        parse_untagged_data ctxt Float_t arg >>=? fun v ->
-        return @@ Ex (Float_t, v)
-    | Prim (loc, "float", l) ->
-        fail @@ Invalid_arity (loc, Constant, "float", 1, List.length l)
     | Prim (_, "timestamp", [ arg ]) ->
         parse_untagged_data ctxt Timestamp_t arg >>=? fun v ->
         return @@ Ex (Timestamp_t, v)
@@ -424,15 +524,6 @@ let rec parse_tagged_data
         return @@ Ex (Union_t (tl, tr), v)
     | Prim (loc, "or", l) ->
         fail @@ Invalid_arity (loc, Constant, "or", 3, List.length l)
-    | Prim (_, "ref", [ r ]) ->
-        parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) ->
-        return @@ Ex (Ref_t tr, ref r)
-    | Prim (_, "ref", [ tr; r ]) ->
-        parse_ty tr >>=? fun (Ex tr) ->
-        parse_untagged_data ctxt tr r >>=? fun r ->
-        return @@ Ex (Ref_t tr, ref r)
-    | Prim (loc, "ref", l) ->
-        fail @@ Invalid_arity (loc, Constant, "ref", 1, List.length l)
     | Prim (_, "some", [ r ]) ->
         parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) ->
         return @@ Ex (Option_t tr, Some r)
@@ -513,24 +604,16 @@ and parse_untagged_data
     match ty, script_data with
     (* Void *)
     | Void_t, Prim (_, "void", []) -> return ()
-    | Void_t, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Float (loc, _) | Seq (loc, _)) ->
+    | Void_t, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "void")
     (* Strings *)
     | String_t, String (_, v) -> return v
-    | String_t, (Prim (loc, _, _) | Int (loc, _) | Float (loc, _) | Seq (loc, _)) ->
+    | String_t, (Prim (loc, _, _) | Int (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "string")
-    (* Floats *)
-    | Float_t, Float (loc, v) -> begin try
-          return (float_of_string v)
-        with _ ->
-          fail @@ Invalid_constant (loc, "float")
-      end
-    | Float_t, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
-        fail @@ Invalid_constant (loc, "float")
     (* Booleans *)
     | Bool_t, Prim (_, "true", []) -> return true
     | Bool_t, Prim (_, "false", []) -> return false
-    | Bool_t, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+    | Bool_t, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "bool")
     (* Integers *)
     | Int_t k, Int (loc, v) -> begin try
@@ -539,7 +622,7 @@ and parse_untagged_data
           | Some i -> return i
         with _ -> fail @@ Invalid_constant (loc, string_of_int_kind k)
       end
-    | Int_t k, (Float (loc, _) | Prim (loc, _, _) | String (loc, _) | Seq (loc, _)) ->
+    | Int_t k, (Prim (loc, _, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, string_of_int_kind k)
     (* Tez amounts *)
     | Tez_t, String (loc, v) -> begin try
@@ -549,19 +632,19 @@ and parse_untagged_data
         with _ ->
           fail @@ Invalid_constant (loc, "tez")
       end
-    | Tez_t, (Float (loc, _) | Int (loc, _) | Prim (loc, _, _) | Seq (loc, _)) ->
+    | Tez_t, (Int (loc, _) | Prim (loc, _, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "tez")
     (* Timestamps *)
-    | Timestamp_t, (Float (loc, v) | Int (loc, v)) -> begin
+    | Timestamp_t, (Int (loc, v)) -> begin
         match (Timestamp.of_seconds v) with
         | Some v -> return v
         | None -> fail @@ Invalid_constant (loc, "timestamp")
       end
     | Timestamp_t, String (loc, s) -> begin try
-        match Timestamp.of_notation s with
+          match Timestamp.of_notation s with
           | Some v -> return v
           | None-> fail @@ Invalid_constant (loc, "timestamp")
-      with _ -> fail @@ Invalid_constant (loc, "timestamp")
+        with _ -> fail @@ Invalid_constant (loc, "timestamp")
       end
     | Timestamp_t, (Prim (loc, _, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "timestamp")
@@ -570,7 +653,7 @@ and parse_untagged_data
           return (Ed25519.Public_key_hash.of_b48check s)
         with _ -> fail @@ Invalid_constant (loc, "key")
       end
-    | Key_t, (Prim (loc, _, _) | Seq (loc, _) | Int (loc, _) | Float (loc, _)) ->
+    | Key_t, (Prim (loc, _, _) | Seq (loc, _) | Int (loc, _)) ->
         fail @@ Invalid_constant (loc, "key")
     (* Signatures *)
     | Signature_t, String (loc, s) -> begin try
@@ -582,7 +665,7 @@ and parse_untagged_data
         with _ ->
           fail @@ Invalid_constant (loc, "signature")
       end
-    | Signature_t, (Prim (loc, _, _) | Int (loc, _) | Float (loc, _) | Seq (loc, _)) ->
+    | Signature_t, (Prim (loc, _, _) | Int (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "signature")
     (* Contracts *)
     | Contract_t (ty1, ty2), String (loc, s) ->
@@ -591,7 +674,7 @@ and parse_untagged_data
           (Lwt.return (Contract.of_b48check s)) >>=? fun c ->
         parse_contract ctxt ty1 ty2 loc c >>=? fun _ ->
         return (ty1, ty2, c)
-    | Contract_t _, (Prim (loc, _, _) | Int (loc, _) | Float (loc, _) | Seq (loc, _)) ->
+    | Contract_t _, (Prim (loc, _, _) | Int (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "contract")
     (* Pairs *)
     | Pair_t (ta, tb), Prim (_, "pair", [ va; vb ]) ->
@@ -600,7 +683,7 @@ and parse_untagged_data
         return (va, vb)
     | Pair_t _, Prim (loc, "pair", l) ->
         fail @@ Invalid_arity (loc, Constant, "pair", 2, List.length l)
-    | Pair_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+    | Pair_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "pair")
     (* Unions *)
     | Union_t (tl, _), Prim (_, "left", [ v ]) ->
@@ -613,21 +696,13 @@ and parse_untagged_data
         return (R v)
     | Union_t _, Prim (loc, "right", l) ->
         fail @@ Invalid_arity (loc, Constant, "right", 1, List.length l)
-    | Union_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+    | Union_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "union")
     (* Lambdas *)
     | Lambda_t (ta, tr), (Seq _ as script_instr) ->
         parse_lambda ctxt ta tr script_instr
-    | Lambda_t (_, _), (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _)) ->
+    | Lambda_t (_, _), (Prim (loc, _, _) | Int (loc, _) | String (loc, _)) ->
         fail @@ Invalid_constant (loc, "lambda")
-    (* References *)
-    | Ref_t t, Prim (_, "ref", [ v ]) ->
-        parse_untagged_data ctxt t v >>=? fun v ->
-        return (ref v)
-    | Ref_t _, Prim (loc, "ref", l) ->
-        fail @@ Invalid_arity (loc, Constant, "ref", 1, List.length l)
-    | Ref_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
-        fail @@ Invalid_constant (loc, "ref")
     (* Options *)
     | Option_t t, Prim (_, "some", [ v ]) ->
         parse_untagged_data ctxt t v >>=? fun v ->
@@ -638,7 +713,7 @@ and parse_untagged_data
         return None
     | Option_t _, Prim (loc, "none", l) ->
         fail @@ Invalid_arity (loc, Constant, "none", 0, List.length l)
-    | Option_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+    | Option_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "option")
     (* Lists *)
     | List_t t, Prim (_, "list", vs) ->
@@ -647,33 +722,31 @@ and parse_untagged_data
              parse_untagged_data ctxt t v >>=? fun v ->
              return (v :: rest))
           [] vs
-    | List_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+    | List_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "list")
     (* Sets *)
     | Set_t t, Prim (_, "set", vs) ->
-      fold_left_s
-        (fun rest v ->
-          parse_untagged_comparable_data ctxt t v >>=? fun v ->
-          return (v :: rest))
-        [] vs >>=? fun v ->
-      return (ref v, t)
-    | Set_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+        fold_left_s
+          (fun acc v ->
+             parse_untagged_comparable_data ctxt t v >>=? fun v ->
+             return (set_update v true acc))
+          (empty_set t) vs
+    | Set_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "set")
     (* Maps *)
     | Map_t (tk, tv), Prim (_, "map", vs) ->
-      fold_left_s
-        (fun rest -> function
-           | Prim (_, "item", [ k; v ]) ->
-               parse_untagged_comparable_data ctxt tk k >>=? fun k ->
-               parse_untagged_data ctxt tv v >>=? fun v ->
-               return ((k, v) :: rest)
-           | Prim (loc, "item", l) ->
-               fail @@ Invalid_arity (loc, Constant, "item", 2, List.length l)
-           | Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _) ->
-               fail @@ Invalid_constant (loc, "item"))
-        [] vs >>=? fun v ->
-      return (ref v, tk)
-    | Map_t _, (Prim (loc, _, _) | Float (loc, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
+        fold_left_s
+          (fun acc -> function
+             | Prim (_, "item", [ k; v ]) ->
+                 parse_untagged_comparable_data ctxt tk k >>=? fun k ->
+                 parse_untagged_data ctxt tv v >>=? fun v ->
+                 return (map_update k (Some v) acc)
+             | Prim (loc, "item", l) ->
+                 fail @@ Invalid_arity (loc, Constant, "item", 2, List.length l)
+             | Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _) ->
+                 fail @@ Invalid_constant (loc, "item"))
+          (empty_map tk) vs
+    | Map_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
         fail @@ Invalid_constant (loc, "map")
 
 and parse_untagged_comparable_data
@@ -686,15 +759,16 @@ and parse_lambda
     ?storage_type: storage ty ->
     arg ty -> ret ty -> Script.expr -> (arg, ret) lambda tzresult Lwt.t =
   fun ctxt ?storage_type arg ret script_instr ->
-    let loc = location script_instr in
     parse_instr ctxt ?storage_type script_instr (Item_t (arg, Empty_t)) >>=? function
-    | Typed (instr, (Item_t (ty, Empty_t) as stack_ty)) ->
+    | Typed ({ loc ; aft = (Item_t (ty, Empty_t) as stack_ty) } as descr) ->
         trace
           (Bad_return (loc, Stack_ty stack_ty, Ty ret))
           (Lwt.return (ty_eq ty ret)) >>=? fun (Eq _) ->
-        return (Lam (instr, script_instr) : (arg, ret) lambda)
-    | Typed (_, stack_ty) ->
+        return (Lam (descr, script_instr) : (arg, ret) lambda)
+    | Typed { loc ; aft = stack_ty } ->
         fail (Bad_return (loc, Stack_ty stack_ty, Ty ret))
+    | Failed { descr } ->
+        return (Lam (descr (Item_t (ret, Empty_t)), script_instr) : (arg, ret) lambda)
 
 and parse_instr
   : type bef storage. context ->
@@ -704,419 +778,534 @@ and parse_instr
     let return : bef judgement -> bef judgement tzresult Lwt.t = return in
     let check_item_ty got exp pos n =
       ty_eq got exp |> record_trace (Bad_stack_item (pos, n)) |> Lwt.return in
-    (* TODO: macros *)
+    let typed loc (instr, aft) =
+      Typed { loc ; instr ; bef = stack_ty ; aft } in
     match script_instr, stack_ty with
     (* stack ops *)
-    | Prim (_, "drop", []), Item_t (_, rest) ->
-        return (Typed (Drop, rest))
-    | Prim (_, "dup", []), Item_t (v, rest) ->
-        return (Typed (Dup, Item_t (v, Item_t (v, rest))))
-    | Prim (_, "swap", []), Item_t (v,  Item_t (w, rest)) ->
-        return (Typed (Swap, Item_t (w, Item_t (v, rest))))
-    | Prim (_, "push", [ td ]), rest ->
+    | Prim (loc, "drop", []),
+      Item_t (_, rest) ->
+        return (typed loc (Drop, rest))
+    | Prim (loc, "dup", []),
+      Item_t (v, rest) ->
+        return (typed loc (Dup, Item_t (v, Item_t (v, rest))))
+    | Prim (loc, "swap", []),
+      Item_t (v,  Item_t (w, rest)) ->
+        return (typed loc (Swap, Item_t (w, Item_t (v, rest))))
+    | Prim (loc, "push", [ td ]),
+      stack ->
         parse_tagged_data ctxt td >>=? fun (Ex (t, v)) ->
-        return (Typed (Const v, Item_t (t, rest)))
+        return (typed loc (Const v, Item_t (t, stack)))
     (* options *)
-    | Prim (_, "some", []), Item_t (t, rest) ->
-        return (Typed (Cons_some, Item_t (Option_t t, rest)))
-    | Prim (_, "none", [ t ]), rest ->
+    | Prim (loc, "some", []),
+      Item_t (t, rest) ->
+        return (typed loc (Cons_some, Item_t (Option_t t, rest)))
+    | Prim (loc, "none", [ t ]),
+      stack ->
         parse_ty t >>=? fun (Ex t) ->
-        return (Typed (Cons_none t, Item_t (Option_t t, rest)))
-    | Prim (loc, "if_none", [ bt ; bf ]), Item_t (Option_t t, rest) ->
+        return (typed loc (Cons_none t, Item_t (Option_t t, stack)))
+    | Prim (loc, "if_none", [ bt ; bf ]),
+      (Item_t (Option_t t, rest) as bef) ->
         expect_sequence_parameter loc Instr "if_none" 0 bt >>=? fun () ->
         expect_sequence_parameter loc Instr "if_none" 1 bf >>=? fun () ->
-        parse_instr ?storage_type ctxt bt rest >>=? fun (Typed (ibt, aftbt)) ->
-        parse_instr ?storage_type ctxt bf (Item_t (t, rest)) >>=? fun (Typed (ibf, aftbf)) ->
-        trace
-          (Unmatched_branches (loc, Stack_ty aftbt, Stack_ty aftbf))
-          (Lwt.return (stack_ty_eq 0 aftbt aftbf)) >>=? fun (Eq _) ->
-        return (Typed (If_none (ibt, ibf), aftbt))
+        parse_instr ?storage_type ctxt bt rest >>=? fun btr ->
+        parse_instr ?storage_type ctxt bf (Item_t (t, rest)) >>=? fun bfr ->
+        let branch ibt ibf =
+          { loc ; instr = If_none (ibt, ibf) ; bef ; aft = ibt.aft } in
+        merge_branches loc btr bfr { branch }
     (* pairs *)
-    | Prim (_, "pair", []), Item_t (a, Item_t (b, rest)) ->
-        return (Typed (Cons_pair, Item_t (Pair_t(a, b), rest)))
-    | Prim (_, "car", []), Item_t (Pair_t (a, _), rest) ->
-        return (Typed (Car, Item_t (a, rest)))
-    | Prim (_, "cdr", []), Item_t (Pair_t (_, b), rest) ->
-        return (Typed (Cdr, Item_t (b, rest)))
+    | Prim (loc, "pair", []),
+      Item_t (a, Item_t (b, rest)) ->
+        return (typed loc (Cons_pair, Item_t (Pair_t(a, b), rest)))
+    | Prim (loc, "car", []),
+      Item_t (Pair_t (a, _), rest) ->
+        return (typed loc (Car, Item_t (a, rest)))
+    | Prim (loc, "cdr", []),
+      Item_t (Pair_t (_, b), rest) ->
+        return (typed loc (Cdr, Item_t (b, rest)))
     (* unions *)
-    | Prim (_, "left", [ tr ]), Item_t (tl, rest) ->
+    | Prim (loc, "left", [ tr ]),
+      Item_t (tl, rest) ->
         parse_ty tr >>=? fun (Ex tr) ->
-        return (Typed (Left, Item_t (Union_t (tl, tr), rest)))
-    | Prim (_, "right", [ tl ]), Item_t (tr, rest) ->
+        return (typed loc (Left, Item_t (Union_t (tl, tr), rest)))
+    | Prim (loc, "right", [ tl ]),
+      Item_t (tr, rest) ->
         parse_ty tl >>=? fun (Ex tl) ->
-        return (Typed (Right, Item_t (Union_t (tl, tr), rest)))
-    | Prim (loc, "if_left", [ bt ; bf ]), Item_t (Union_t (tl, tr), rest) ->
+        return (typed loc (Right, Item_t (Union_t (tl, tr), rest)))
+    | Prim (loc, "if_left", [ bt ; bf ]),
+      (Item_t (Union_t (tl, tr), rest) as bef) ->
         expect_sequence_parameter loc Instr "if_left" 0 bt >>=? fun () ->
         expect_sequence_parameter loc Instr "if_left" 1 bf >>=? fun () ->
-        parse_instr ?storage_type ctxt bt (Item_t (tl, rest)) >>=? fun (Typed (ibt, aftbt)) ->
-        parse_instr ?storage_type ctxt bf (Item_t (tr, rest)) >>=? fun (Typed (ibf, aftbf)) ->
-        trace
-          (Unmatched_branches (loc, Stack_ty aftbt, Stack_ty aftbf))
-          (Lwt.return (stack_ty_eq 0 aftbt aftbf)) >>=? fun (Eq _) ->
-        return (Typed (If_left (ibt, ibf), aftbt))
+        parse_instr ?storage_type ctxt bt (Item_t (tl, rest)) >>=? fun btr ->
+        parse_instr ?storage_type ctxt bf (Item_t (tr, rest)) >>=? fun bfr ->
+        let branch ibt ibf =
+          { loc ; instr = If_left (ibt, ibf) ; bef ; aft = ibt.aft } in
+        merge_branches loc btr bfr { branch }
     (* lists *)
-    | Prim (_, "nil", [ t ]), rest ->
+    | Prim (loc, "nil", [ t ]),
+      stack ->
         parse_ty t >>=? fun (Ex t) ->
-        return (Typed (Nil, Item_t (List_t t, rest)))
-    | Prim (loc, "cons", []), Item_t (tv, Item_t (List_t t, rest)) ->
+        return (typed loc (Nil, Item_t (List_t t, stack)))
+    | Prim (loc, "cons", []),
+      Item_t (tv, Item_t (List_t t, rest)) ->
         trace
           (Bad_stack_item (loc, 2))
           (Lwt.return (ty_eq t tv)) >>=? fun (Eq _) ->
-        return (Typed (Cons_list, Item_t (List_t t, rest)))
-    | Prim (loc, "if_cons", [ bt ; bf ]), Item_t (List_t t, rest) ->
+        return (typed loc (Cons_list, Item_t (List_t t, rest)))
+    | Prim (loc, "if_cons", [ bt ; bf ]),
+      (Item_t (List_t t, rest) as bef) ->
         expect_sequence_parameter loc Instr "if_cons" 0 bt >>=? fun () ->
         expect_sequence_parameter loc Instr "if_cons" 1 bf >>=? fun () ->
-        parse_instr ?storage_type ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun (Typed (ibt, aftbt)) ->
-        parse_instr ?storage_type ctxt bf rest >>=? fun (Typed (ibf, aftbf)) ->
-        trace
-          (Unmatched_branches (loc, Stack_ty aftbt, Stack_ty aftbf))
-          (Lwt.return (stack_ty_eq 0 aftbt aftbf)) >>=? fun (Eq _) ->
-        return (Typed (If_cons (ibt, ibf), aftbt))
-    | Prim (loc, "iter", []), Item_t (Lambda_t (param, Void_t), Item_t (List_t elt, rest)) ->
+        parse_instr ?storage_type ctxt bt (Item_t (t, Item_t (List_t t, rest))) >>=? fun btr ->
+        parse_instr ?storage_type ctxt bf rest >>=? fun bfr ->
+        let branch ibt ibf =
+          { loc ; instr = If_cons (ibt, ibf) ; bef ; aft = ibt.aft } in
+        merge_branches loc btr bfr { branch }
+    | Prim (loc, "map", []),
+      Item_t (Lambda_t (param, ret), Item_t (List_t elt, rest)) ->
         check_item_ty elt param loc 2 >>=? fun (Eq _) ->
-        return (Typed (List_iter, rest))
-    | Prim (loc, "map", []), Item_t (Lambda_t (param, ret), Item_t (List_t elt, rest)) ->
-        check_item_ty elt param loc 2 >>=? fun (Eq _) ->
-        return (Typed (List_map, Item_t (List_t ret, rest)))
-    | Prim (loc, "reduce", []), Item_t (Lambda_t (Pair_t (pelt, pr), r),
-                      Item_t (List_t elt, Item_t (init, rest))) ->
+        return (typed loc (List_map, Item_t (List_t ret, rest)))
+    | Prim (loc, "reduce", []),
+      Item_t (Lambda_t (Pair_t (pelt, pr), r),
+              Item_t (List_t elt, Item_t (init, rest))) ->
         check_item_ty r pr loc 1 >>=? fun (Eq _) ->
         check_item_ty elt pelt loc 2 >>=? fun (Eq _) ->
         check_item_ty init r loc 3 >>=? fun (Eq _) ->
-        return (Typed (List_reduce, Item_t (r, rest)))
+        return (typed loc (List_reduce, Item_t (r, rest)))
     (* sets *)
-    | Prim (_, "empty_set", [ t ]), rest ->
+    | Prim (loc, "empty_set", [ t ]),
+      rest ->
         parse_comparable_ty t >>=? fun (Ex t) ->
-        return (Typed (Empty_set t, Item_t (Set_t t, rest)))
-    | Prim (loc, "iter", []), Item_t (Lambda_t (param, Void_t), Item_t (Set_t elt, rest)) ->
-        let elt = ty_of_comparable_ty elt in
-        check_item_ty elt param loc 2 >>=? fun (Eq _) ->
-        return (Typed (Set_iter, rest))
-    | Prim (loc, "map", []), Item_t (Lambda_t (param, ret), Item_t (Set_t elt, rest)) ->
+        return (typed loc (Empty_set t, Item_t (Set_t t, rest)))
+    | Prim (loc, "map", []),
+      Item_t (Lambda_t (param, ret), Item_t (Set_t elt, rest)) ->
         let elt = ty_of_comparable_ty elt in
         trace (Bad_stack_item (loc, 1)) (Lwt.return (comparable_ty_of_ty ret)) >>=? fun ret ->
         check_item_ty elt param loc 2 >>=? fun (Eq _) ->
-        return (Typed (Set_map ret, Item_t (Set_t ret, rest)))
-    | Prim (loc, "reduce", []), Item_t (Lambda_t (Pair_t (pelt, pr), r),
-                      Item_t (Set_t elt, Item_t (init, rest))) ->
+        return (typed loc (Set_map ret, Item_t (Set_t ret, rest)))
+    | Prim (loc, "reduce", []),
+      Item_t (Lambda_t (Pair_t (pelt, pr), r),
+              Item_t (Set_t elt, Item_t (init, rest))) ->
         let elt = ty_of_comparable_ty elt in
         check_item_ty r pr loc 1 >>=? fun (Eq _) ->
         check_item_ty elt pelt loc 2 >>=? fun (Eq _) ->
         check_item_ty init r loc 3 >>=? fun (Eq _) ->
-        return (Typed (Set_reduce, Item_t (r, rest)))
-    | Prim (loc, "mem", []), Item_t (v, Item_t (Set_t elt, rest)) ->
+        return (typed loc (Set_reduce, Item_t (r, rest)))
+    | Prim (loc, "mem", []),
+      Item_t (v, Item_t (Set_t elt, rest)) ->
         let elt = ty_of_comparable_ty elt in
         check_item_ty elt v loc 2 >>=? fun (Eq _) ->
-        return (Typed (Set_mem, Item_t (Bool_t, rest)))
-    | Prim (loc, "update", []), Item_t (v, Item_t (Bool_t, Item_t (Set_t elt, rest))) ->
-        let elt = ty_of_comparable_ty elt in
-        check_item_ty elt v loc 3 >>=? fun (Eq _) ->
-        return (Typed (Set_update, rest))
+        return (typed loc (Set_mem, Item_t (Bool_t, rest)))
+    | Prim (loc, "update", []),
+      Item_t (v, Item_t (Bool_t, Item_t (Set_t elt, rest))) ->
+        let ty = ty_of_comparable_ty elt in
+        check_item_ty ty v loc 3 >>=? fun (Eq _) ->
+        return (typed loc (Set_update, Item_t (Set_t elt, rest)))
     (* maps *)
-    | Prim (_, "empty_map", [ tk ; tv ]), rest ->
+    | Prim (loc, "empty_map", [ tk ; tv ]),
+      stack ->
         parse_comparable_ty tk >>=? fun (Ex tk) ->
         parse_ty tv >>=? fun (Ex tv) ->
-        return (Typed (Empty_map (tk, tv), Item_t (Map_t (tk, tv), rest)))
-    | Prim (loc, "iter", []), Item_t (Lambda_t (Pair_t (pk, pv), Void_t), Item_t (Map_t (k, v), rest)) ->
-        let k = ty_of_comparable_ty k in
-        check_item_ty pk k loc 2 >>=? fun (Eq _) ->
-        check_item_ty pv v loc 2 >>=? fun (Eq _) ->
-        return (Typed (Map_iter, rest))
-    | Prim (loc, "map", []), Item_t (Lambda_t (Pair_t (pk, pv), ret), Item_t (Map_t (ck, v), rest)) ->
+        return (typed loc (Empty_map (tk, tv), Item_t (Map_t (tk, tv), stack)))
+    | Prim (loc, "map", []),
+      Item_t (Lambda_t (Pair_t (pk, pv), ret), Item_t (Map_t (ck, v), rest)) ->
         let k = ty_of_comparable_ty ck in
         check_item_ty pk k loc 2 >>=? fun (Eq _) ->
         check_item_ty pv v loc 2 >>=? fun (Eq _) ->
-        return (Typed (Map_map, Item_t (Map_t (ck, ret), rest)))
-    | Prim (loc, "reduce", []), Item_t (Lambda_t (Pair_t (Pair_t (pk, pv), pr), r),
-                      Item_t (Map_t (ck, v), Item_t (init, rest))) ->
+        return (typed loc (Map_map, Item_t (Map_t (ck, ret), rest)))
+    | Prim (loc, "reduce", []),
+      Item_t (Lambda_t (Pair_t (Pair_t (pk, pv), pr), r),
+              Item_t (Map_t (ck, v), Item_t (init, rest))) ->
         let k = ty_of_comparable_ty ck in
         check_item_ty pk k loc 2 >>=? fun (Eq _) ->
         check_item_ty pv v loc 2 >>=? fun (Eq _) ->
         check_item_ty r pr loc 1 >>=? fun (Eq _) ->
         check_item_ty init r loc 3 >>=? fun (Eq _) ->
-        return (Typed (Map_reduce, Item_t (r, rest)))
-    | Prim (loc, "mem", []), Item_t (vk, Item_t (Map_t (ck, _), rest)) ->
+        return (typed loc (Map_reduce, Item_t (r, rest)))
+    | Prim (loc, "mem", []),
+      Item_t (vk, Item_t (Map_t (ck, _), rest)) ->
         let k = ty_of_comparable_ty ck in
         check_item_ty vk k loc 1 >>=? fun (Eq _) ->
-        return (Typed (Map_mem, Item_t (Bool_t, rest)))
-    | Prim (loc, "get", []), Item_t (vk, Item_t (Map_t (ck, elt), rest)) ->
+        return (typed loc (Map_mem, Item_t (Bool_t, rest)))
+    | Prim (loc, "get", []),
+      Item_t (vk, Item_t (Map_t (ck, elt), rest)) ->
         let k = ty_of_comparable_ty ck in
         check_item_ty vk k loc 1 >>=? fun (Eq _) ->
-        return (Typed (Map_get, Item_t (Option_t elt, rest)))
-    | Prim (loc, "update", []), Item_t (vk, Item_t (Option_t vv, Item_t (Map_t (ck, v), rest))) ->
+        return (typed loc (Map_get, Item_t (Option_t elt, rest)))
+    | Prim (loc, "update", []),
+      Item_t (vk, Item_t (Option_t vv, Item_t (Map_t (ck, v), rest))) ->
         let k = ty_of_comparable_ty ck in
         check_item_ty vk k loc 1 >>=? fun (Eq _) ->
         check_item_ty vv v loc 2 >>=? fun (Eq _) ->
-        return (Typed (Map_update, rest))
-    (* reference cells *)
-    | Prim (_, "ref", []), Item_t (t, rest) ->
-        return (Typed (Ref, Item_t (Ref_t t, rest)))
-    | Prim (_, "deref", []), Item_t (Ref_t t, rest) ->
-        return (Typed (Deref, Item_t (t, rest)))
-    | Prim (loc, "set", []), Item_t (Ref_t t, Item_t (tv, rest)) ->
-        check_item_ty tv t loc 2 >>=? fun (Eq _) ->
-        return (Typed (Set, rest))
+        return (typed loc (Map_update, Item_t (Map_t (ck, v), rest)))
     (* control *)
-    | Seq (_, []), rest ->
-        return (Typed (Nop, rest))
-    | Seq (_, [ single ]), stack_ty ->
-        parse_instr ?storage_type ctxt single stack_ty
-    | Seq (loc, hd :: tl), stack_ty ->
-        parse_instr ?storage_type ctxt hd stack_ty >>=? fun (Typed (ihd, trans)) ->
-        parse_instr ?storage_type ctxt (Seq (loc, tl)) trans >>=? fun (Typed (itl, aft)) ->
-        return (Typed (Seq (ihd, itl), aft))
-    | Prim (loc, "if", [ bt ; bf ]), Item_t (Bool_t, rest) ->
+    | Seq (loc, []),
+      stack ->
+        return (typed loc (Nop, stack))
+    | Seq (_, [ single ]),
+      stack ->
+        parse_instr ?storage_type ctxt single stack
+    | Seq (loc, hd :: tl),
+      stack ->
+        parse_instr ?storage_type ctxt hd stack >>=? begin function
+          | Failed _ ->
+              fail (Fail_not_in_tail_position loc)
+          | Typed ({ aft = middle } as ihd) ->
+              parse_instr ?storage_type ctxt (Seq (loc, tl)) middle >>=? function
+              | Failed { descr } ->
+                  let descr ret =
+                    { loc ; instr = Seq (ihd, descr ret) ;
+                      bef = stack ; aft = ret } in
+                  return (Failed { descr })
+              | Typed itl ->
+                  return (typed loc (Seq (ihd, itl), itl.aft))
+        end
+    | Prim (loc, "if", [ bt ; bf ]),
+      (Item_t (Bool_t, rest) as bef) ->
         expect_sequence_parameter loc Instr "if" 0 bt >>=? fun () ->
         expect_sequence_parameter loc Instr "if" 1 bf >>=? fun () ->
-        parse_instr ?storage_type ctxt bt rest >>=? fun (Typed (ibt, aftbt)) ->
-        parse_instr ?storage_type ctxt bf rest >>=? fun (Typed (ibf, aftbf)) ->
-        trace
-          (Unmatched_branches (loc, Stack_ty aftbt, Stack_ty aftbf))
-          (Lwt.return (stack_ty_eq 0 aftbt aftbf)) >>=? fun (Eq _) ->
-        return (Typed (If (ibt, ibf), aftbt))
-    | Prim (loc, "loop", [ body ]), Item_t (Bool_t, rest) ->
+        parse_instr ?storage_type ctxt bt rest >>=? fun btr ->
+        parse_instr ?storage_type ctxt bf rest >>=? fun bfr ->
+        let branch ibt ibf =
+          { loc ; instr = If (ibt, ibf) ; bef ; aft = ibt.aft } in
+        merge_branches loc btr bfr { branch }
+    | Prim (loc, "loop", [ body ]),
+      (Item_t (Bool_t, rest) as stack) ->
         expect_sequence_parameter loc Instr "loop" 0 body >>=? fun () ->
-        parse_instr ?storage_type ctxt body rest >>=? fun (Typed (ibody, aftbody)) ->
-        trace
-          (Unmatched_branches (loc, Stack_ty aftbody, Stack_ty stack_ty))
-          (Lwt.return (stack_ty_eq 0 aftbody stack_ty)) >>=? fun (Eq _) ->
-        return (Typed (Loop ibody, rest))
-    | Prim (loc, "lambda", [ arg ; ret ; code ]), rest ->
+        parse_instr ?storage_type ctxt body rest >>=? begin function
+          | Typed ibody ->
+              trace
+                (Unmatched_branches (loc, Stack_ty ibody.aft, Stack_ty stack))
+                (Lwt.return (stack_ty_eq 0 ibody.aft stack)) >>=? fun (Eq _) ->
+              return (typed loc (Loop ibody, rest))
+          | Failed { descr } ->
+              let ibody = descr (Item_t (Bool_t, rest)) in
+              return (typed loc (Loop ibody, rest))
+        end
+    | Prim (loc, "lambda", [ arg ; ret ; code ]),
+      stack ->
         parse_ty arg >>=? fun (Ex arg) ->
         parse_ty ret >>=? fun (Ex ret) ->
         expect_sequence_parameter loc Instr "lambda" 2 code >>=? fun () ->
-        parse_lambda ctxt arg ret code >>=? fun (lambda) ->
-        return (Typed (Lambda lambda, Item_t (Lambda_t (arg, ret), rest)))
-    | Prim (loc, "exec", []), Item_t (arg, Item_t (Lambda_t (param, ret), rest)) ->
+        parse_lambda ctxt arg ret code >>=? fun lambda ->
+        return (typed loc (Lambda lambda, Item_t (Lambda_t (arg, ret), stack)))
+    | Prim (loc, "exec", []),
+      Item_t (arg, Item_t (Lambda_t (param, ret), rest)) ->
         check_item_ty arg param loc 1 >>=? fun (Eq _) ->
-        return (Typed (Exec, Item_t (ret, rest)))
-    | Prim (loc, "dip", [ code ]), Item_t (v, rest) ->
+        return (typed loc (Exec, Item_t (ret, rest)))
+    | Prim (loc, "dip", [ code ]),
+      Item_t (v, rest) ->
         expect_sequence_parameter loc Instr "dip" 0 code >>=? fun () ->
-        parse_instr ctxt code rest >>=? fun (Typed (instr, aft_rest)) ->
-        return (Typed (Dip instr, Item_t (v, aft_rest)))
-    | Prim (loc, "fail", []), rest ->
-        return (Typed (Fail loc, rest)) (* FIXME *)
-    | Prim (_, "nop", []), rest ->
-        return (Typed (Nop, rest))
+        parse_instr ctxt code rest >>=? begin function
+          | Typed descr ->
+              return (typed loc (Dip descr, Item_t (v, descr.aft)))
+          | Failed _ ->
+              fail (Fail_not_in_tail_position loc)
+        end
+    | Prim (loc, "fail", []),
+      bef ->
+        let descr aft = { loc ; instr = Fail ; bef ; aft } in
+        return (Failed { descr })
+    | Prim (loc, "nop", []),
+      stack ->
+        return (typed loc (Nop, stack))
     (* timestamp operations *)
-    | Prim (_, "add", []), Item_t (Timestamp_t, Item_t (Float_t, rest)) ->
-        return (Typed (Add_timestamp_to_period, Item_t (Timestamp_t, rest)))
-    | Prim (loc, "add", []), Item_t (Timestamp_t, Item_t (Int_t kind, rest)) ->
-        trace (Bad_stack_item (loc, 2)) (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
-        return (Typed (Add_timestamp_to_seconds (kind, loc), Item_t (Timestamp_t, rest)))
-    | Prim (_, "add", []), Item_t (Float_t, Item_t (Timestamp_t, rest)) ->
-        return (Typed (Add_period_to_timestamp, Item_t (Timestamp_t, rest)))
-    | Prim (loc, "add", []), Item_t (Int_t kind, Item_t (Timestamp_t, rest)) ->
+    | Prim (loc, "add", []),
+      Item_t (Timestamp_t, Item_t (Int_t kind, rest)) ->
+        trace
+          (Bad_stack_item (loc, 2))
+          (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
+        return (typed loc (Add_timestamp_to_seconds kind, Item_t (Timestamp_t, rest)))
+    | Prim (loc, "add", []),
+      Item_t (Int_t kind, Item_t (Timestamp_t, rest)) ->
         trace
           (Bad_stack_item (loc, 1))
           (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
-        return (Typed (Add_seconds_to_timestamp (kind, loc), Item_t (Timestamp_t, rest)))
+        return (typed loc (Add_seconds_to_timestamp kind, Item_t (Timestamp_t, rest)))
     (* string operations *)
-    | Prim (_, "concat", []), Item_t (String_t, Item_t (String_t, rest)) ->
-        return (Typed (Concat, Item_t (String_t, rest)))
+    | Prim (loc, "concat", []),
+      Item_t (String_t, Item_t (String_t, rest)) ->
+        return (typed loc (Concat, Item_t (String_t, rest)))
     (* currency operations *)
-    | Prim (_, "add", []), Item_t (Tez_t, Item_t (Tez_t, rest)) ->
-        return (Typed (Add_tez, Item_t (Tez_t, rest)))
-    | Prim (_, "sub", []), Item_t (Tez_t, Item_t (Tez_t, rest)) ->
-        return (Typed (Sub_tez, Item_t (Tez_t, rest)))
-    | Prim (loc, "mul", []), Item_t (Tez_t, Item_t (Int_t kind, rest)) ->
-        trace (Bad_stack_item (loc, 2)) (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
-        return (Typed (Mul_tez kind, Item_t (Tez_t, rest)))
-    | Prim (loc, "mul", []), Item_t (Int_t kind, Item_t (Tez_t, rest)) ->
+    | Prim (loc, "add", []),
+      Item_t (Tez_t, Item_t (Tez_t, rest)) ->
+        return (typed loc (Add_tez, Item_t (Tez_t, rest)))
+    | Prim (loc, "sub", []),
+      Item_t (Tez_t, Item_t (Tez_t, rest)) ->
+        return (typed loc (Sub_tez, Item_t (Tez_t, rest)))
+    | Prim (loc, "mul", []),
+      Item_t (Tez_t, Item_t (Int_t kind, rest)) ->
+        trace
+          (Bad_stack_item (loc, 2))
+          (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
+        return (typed loc (Mul_tez kind, Item_t (Tez_t, rest)))
+    | Prim (loc, "mul", []),
+      Item_t (Int_t kind, Item_t (Tez_t, rest)) ->
         trace
           (Bad_stack_item (loc, 1))
           (Lwt.return (unsigned_int_kind kind)) >>=? fun (Eq _) ->
-        return (Typed (Mul_tez' kind, Item_t (Tez_t, rest)))
-    (* float operations *)
-    | Prim (_, "floor", []), Item_t (Float_t, rest) ->
-        return (Typed (Floor, Item_t (Float_t, rest)))
-    | Prim (_, "ceil", []), Item_t (Float_t, rest) ->
-        return (Typed (Ceil, Item_t (Float_t, rest)))
-    | Prim (_, "inf", []), rest ->
-        return (Typed (Inf, Item_t (Float_t, rest)))
-    | Prim (_, "nan", []), rest ->
-        return (Typed (NaN, Item_t (Float_t, rest)))
-    | Prim (_, "isnan", []), Item_t (Float_t, rest) ->
-        return (Typed (IsNaN, Item_t (Bool_t, rest)))
-    | Prim (loc, "nanan", []), Item_t (Float_t, rest) ->
-        return (Typed (NaNaN loc, rest))
-    | Prim (_, "abs", []), Item_t (Float_t, rest) ->
-        return (Typed (Abs_float, Item_t (Float_t, rest)))
-    | Prim (_, "neg", []), Item_t (Float_t, rest) ->
-        return (Typed (Neg_float, Item_t (Float_t, rest)))
-    | Prim (_, "add", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Add_float, Item_t (Float_t, rest)))
-    | Prim (_, "sub", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Sub_float, Item_t (Float_t, rest)))
-    | Prim (_, "mul", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Mul_float, Item_t (Float_t, rest)))
-    | Prim (_, "div", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Div_float, Item_t (Float_t, rest)))
-    | Prim (_, "mod", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Mod_float, Item_t (Float_t, rest)))
+        return (typed loc (Mul_tez' kind, Item_t (Tez_t, rest)))
     (* boolean operations *)
-    | Prim (_, "or", []), Item_t (Bool_t, Item_t (Bool_t, rest)) ->
-        return (Typed (Or, Item_t (Bool_t, rest)))
-    | Prim (_, "and", []), Item_t (Bool_t, Item_t (Bool_t, rest)) ->
-        return (Typed (And, Item_t (Bool_t, rest)))
-    | Prim (_, "xor", []), Item_t (Bool_t, Item_t (Bool_t, rest)) ->
-        return (Typed (Xor, Item_t (Bool_t, rest)))
-    | Prim (_, "not", []), Item_t (Bool_t, rest) ->
-        return (Typed (Not, Item_t (Bool_t, rest)))
+    | Prim (loc, "or", []),
+      Item_t (Bool_t, Item_t (Bool_t, rest)) ->
+        return (typed loc (Or, Item_t (Bool_t, rest)))
+    | Prim (loc, "and", []),
+      Item_t (Bool_t, Item_t (Bool_t, rest)) ->
+        return (typed loc (And, Item_t (Bool_t, rest)))
+    | Prim (loc, "xor", []),
+      Item_t (Bool_t, Item_t (Bool_t, rest)) ->
+        return (typed loc (Xor, Item_t (Bool_t, rest)))
+    | Prim (loc, "not", []),
+      Item_t (Bool_t, rest) ->
+        return (typed loc (Not, Item_t (Bool_t, rest)))
     (* integer operations *)
-    | Prim (loc, "checked_abs", []), Item_t (Int_t k, rest) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Checked_abs_int (k, loc), Item_t (Int_t k, rest)))
-    | Prim (loc, "checked_neg", []), Item_t (Int_t k, rest) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Checked_neg_int (k, loc), Item_t (Int_t k, rest)))
-    | Prim (loc, "checked_add", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Checked_add_int (kl, loc), Item_t (Int_t kl, rest)))
-    | Prim (loc, "checked_sub", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Checked_sub_int (kl, loc), Item_t (Int_t kl, rest)))
-    | Prim (loc, "checked_mul", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Checked_mul_int (kl, loc), Item_t (Int_t kl, rest)))
-    | Prim (loc, "abs", []), Item_t (Int_t k, rest) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Abs_int k, Item_t (Int_t k, rest)))
-    | Prim (loc, "neg", []), Item_t (Int_t k, rest) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Neg_int k, Item_t (Int_t k, rest)))
-    | Prim (loc, "add", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Add_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "sub", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Sub_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "mul", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Mul_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "div", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Div_int (kl, loc), Item_t (Int_t kl, rest)))
-    | Prim (loc, "mod", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Mod_int (kl, loc), Item_t (Int_t kl, rest)))
-    | Prim (loc, "lsl", []), Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Lsl_int k, Item_t (Int_t k, rest)))
-    | Prim (loc, "lsr", []), Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Lsr_int k, Item_t (Int_t k, rest)))
-    | Prim (loc, "or", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
-        trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Or_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "and", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
-        trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (And_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "xor", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
-        trace (Bad_stack_item (loc, 2)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Xor_int kl, Item_t (Int_t kl, rest)))
-    | Prim (loc, "not", []), Item_t (Int_t k, rest) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
-        return (Typed (Not_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "checked_abs", []),
+      Item_t (Int_t k, rest) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Checked_abs_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "checked_neg", []),
+      Item_t (Int_t k, rest) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Checked_neg_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "checked_add", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Checked_add_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "checked_sub", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Checked_sub_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "checked_mul", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Checked_mul_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "abs", []),
+      Item_t (Int_t k, rest) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Abs_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "neg", []),
+      Item_t (Int_t k, rest) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (signed_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Neg_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "add", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Add_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "sub", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Sub_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "mul", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Mul_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "div", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Div_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "mod", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Mod_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "lsl", []),
+      Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Lsl_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "lsr", []),
+      Item_t (Int_t k, Item_t (Int_t Uint8, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Lsr_int k, Item_t (Int_t k, rest)))
+    | Prim (loc, "or", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
+        trace
+          (Bad_stack_item (loc, 2))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Or_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "and", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
+        trace
+          (Bad_stack_item (loc, 2))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (And_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "xor", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind kl)) >>=? fun (Eq _) ->
+        trace
+          (Bad_stack_item (loc, 2))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Xor_int kl, Item_t (Int_t kl, rest)))
+    | Prim (loc, "not", []),
+      Item_t (Int_t k, rest) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (unsigned_int_kind k)) >>=? fun (Eq _) ->
+        return (typed loc (Not_int k, Item_t (Int_t k, rest)))
     (* comparison *)
-    | Prim (loc, "compare", []), Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
-        trace (Bad_stack_item (loc, 1)) (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
-        return (Typed (Compare (Int_key kl), Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (Bool_t, Item_t (Bool_t, rest)) ->
-        return (Typed (Compare Bool_key, Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (String_t, Item_t (String_t, rest)) ->
-        return (Typed (Compare String_key, Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (Float_t, Item_t (Float_t, rest)) ->
-        return (Typed (Compare Float_key, Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (Tez_t, Item_t (Tez_t, rest)) ->
-        return (Typed (Compare Tez_key, Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (Key_t, Item_t (Key_t, rest)) ->
-        return (Typed (Compare Key_key, Item_t (Int_t Int64, rest)))
-    | Prim (_, "compare", []), Item_t (Timestamp_t, Item_t (Timestamp_t, rest)) ->
-        return (Typed (Compare Timestamp_key, Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (Int_t kl, Item_t (Int_t kr, rest)) ->
+        trace
+          (Bad_stack_item (loc, 1))
+          (Lwt.return (int_kind_eq kl kr)) >>=? fun (Eq _) ->
+        return (typed loc (Compare (Int_key kl), Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (Bool_t, Item_t (Bool_t, rest)) ->
+        return (typed loc (Compare Bool_key, Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (String_t, Item_t (String_t, rest)) ->
+        return (typed loc (Compare String_key, Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (Tez_t, Item_t (Tez_t, rest)) ->
+        return (typed loc (Compare Tez_key, Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (Key_t, Item_t (Key_t, rest)) ->
+        return (typed loc (Compare Key_key, Item_t (Int_t Int64, rest)))
+    | Prim (loc, "compare", []),
+      Item_t (Timestamp_t, Item_t (Timestamp_t, rest)) ->
+        return (typed loc (Compare Timestamp_key, Item_t (Int_t Int64, rest)))
     (* comparators *)
-    | Prim (_, "eq", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Eq, Item_t (Bool_t, rest)))
-    | Prim (_, "neq", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Neq, Item_t (Bool_t, rest)))
-    | Prim (_, "lt", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Lt, Item_t (Bool_t, rest)))
-    | Prim (_, "gt", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Gt, Item_t (Bool_t, rest)))
-    | Prim (_, "le", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Le, Item_t (Bool_t, rest)))
-    | Prim (_, "ge", []), Item_t (Int_t Int64, rest) ->
-        return (Typed (Ge, Item_t (Bool_t, rest)))
+    | Prim (loc, "eq", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Eq, Item_t (Bool_t, rest)))
+    | Prim (loc, "neq", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Neq, Item_t (Bool_t, rest)))
+    | Prim (loc, "lt", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Lt, Item_t (Bool_t, rest)))
+    | Prim (loc, "gt", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Gt, Item_t (Bool_t, rest)))
+    | Prim (loc, "le", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Le, Item_t (Bool_t, rest)))
+    | Prim (loc, "ge", []),
+      Item_t (Int_t Int64, rest) ->
+        return (typed loc (Ge, Item_t (Bool_t, rest)))
     (* casts *)
-    | Prim (loc, "checked_cast", [ t ]), stack_ty ->
-        parse_ty t >>=? fun (Ex ty) -> begin match ty, stack_ty with
-        | Int_t kt, Item_t (Int_t kf, rest) ->
-            return (Typed (Checked_int_of_int (kf, kt, loc), Item_t (Int_t kt, rest)))
-        | ty, Item_t (ty', _) ->
-            fail (Undefined_cast (loc, Ty ty', Ty ty))
-        | _, Empty_t ->
-            fail (Bad_stack (loc, 1, Stack_ty stack_ty))
-      end
-    | Prim (loc, "cast", [ t ]), stack_ty ->
-        parse_ty t >>=? fun (Ex ty) -> begin match ty,stack_ty with
-        | Int_t kt, Item_t (Int_t kf, rest)  ->
-            return (Typed (Int_of_int (kf, kt), Item_t (Int_t kt, rest)))
-        | Float_t, Item_t (Int_t kf, rest)  ->
-            return (Typed (Float_of_int kf, Item_t (Float_t, rest)))
-        | Int_t kt, Item_t (Float_t, rest)  ->
-            return (Typed (Int_of_float kt, Item_t (Int_t kt, rest)))
-        | ty, Item_t (ty', _) ->
-            fail (Undefined_cast (loc, Ty ty', Ty ty))
-        | _, Empty_t ->
-            fail (Bad_stack (loc, 1, Stack_ty stack_ty))
-      end
+    | Prim (loc, "checked_cast", [ t ]),
+      stack ->
+        parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with
+          | Int_t kt,
+            Item_t (Int_t kf, rest) ->
+              return (typed loc (Checked_int_of_int (kf, kt),
+                                 Item_t (Int_t kt, rest)))
+          | ty, Item_t (ty', _) ->
+              fail (Undefined_cast (loc, Ty ty', Ty ty))
+          | _, Empty_t ->
+              fail (Bad_stack (loc, 1, Stack_ty stack))
+        end
+    | Prim (loc, "cast", [ t ]),
+      stack ->
+        parse_ty t >>=? fun (Ex ty) -> begin match ty, stack with
+          | Int_t kt, Item_t (Int_t kf, rest)  ->
+              return (typed loc (Int_of_int (kf, kt),
+                                 Item_t (Int_t kt, rest)))
+          | ty, Item_t (ty', _) ->
+              fail (Undefined_cast (loc, Ty ty', Ty ty))
+          | _, Empty_t ->
+              fail (Bad_stack (loc, 1, Stack_ty stack))
+        end
     (* protocol *)
-    | Prim (_, "manager", []), Item_t (Contract_t _, rest) ->
-        return (Typed (Manager, Item_t (Key_t, rest)))
+    | Prim (loc, "manager", []),
+      Item_t (Contract_t _, rest) ->
+        return (typed loc (Manager, Item_t (Key_t, rest)))
     | Prim (loc, "transfer_tokens", []),
-      Item_t (p, Item_t (Tez_t, Item_t (Contract_t (cp, cr), Item_t (storage, Empty_t)))) ->
+      Item_t (p, Item_t
+                (Tez_t, Item_t
+                   (Contract_t (cp, cr), Item_t
+                      (storage, Empty_t)))) ->
         check_item_ty p cp loc 1 >>=? fun (Eq _) ->
         begin match storage_type with
           | Some storage_type ->
               check_item_ty storage storage_type loc 3 >>=? fun (Eq _) ->
-              return (Typed (Transfer_tokens (storage, loc), Item_t (cr, Item_t (storage, Empty_t))))
+              return (typed loc (Transfer_tokens storage,
+                                 Item_t (cr, Item_t (storage, Empty_t))))
           | None ->
               fail (Transfer_in_lambda loc)
         end
-    | Prim (_, "create_account", []),
-      Item_t (Key_t, Item_t (Option_t Key_t, Item_t (Bool_t, Item_t (Tez_t, rest)))) ->
-        return (Typed (Create_account, Item_t (Contract_t (Void_t, Void_t), rest)))
+    | Prim (loc, "create_account", []),
+      Item_t
+        (Key_t, Item_t
+           (Option_t Key_t, Item_t
+              (Bool_t, Item_t
+                 (Tez_t, rest)))) ->
+        return (typed loc (Create_account,
+                           Item_t (Contract_t (Void_t, Void_t), rest)))
     | Prim (loc, "create_contract", []),
-      Item_t (Key_t, Item_t (Option_t Key_t, Item_t (Bool_t, Item_t (Tez_t,
-        Item_t (Lambda_t (Pair_t (Pair_t (Tez_t, p), gp), Pair_t (r, gr)),
-          Item_t (ginit, rest)))))) ->
+      Item_t
+        (Key_t, Item_t
+           (Option_t Key_t, Item_t
+              (Bool_t, Item_t
+                 (Tez_t, Item_t
+                    (Lambda_t (Pair_t (Pair_t (Tez_t, p), gp),
+                               Pair_t (r, gr)), Item_t
+                       (ginit, rest)))))) ->
         check_item_ty gp gr loc 5 >>=? fun (Eq _) ->
         check_item_ty ginit gp loc 6 >>=? fun (Eq _) ->
-        return (Typed (Create_contract (gp, p, r),
-                   Item_t (Contract_t (p, r), rest)))
-    | Prim (_, "now", []), rest ->
-        return (Typed (Now, Item_t (Timestamp_t, rest)))
-    | Prim (_, "amount", []), rest ->
-        return (Typed (Amount, Item_t (Tez_t, rest)))
-    | Prim (_, "balance", []), rest ->
-        return (Typed (Balance, Item_t (Tez_t, rest)))
-    | Prim (_, "check_signature", []), Item_t (Key_t, Item_t (Pair_t (Signature_t, String_t), rest)) ->
-        return (Typed (Check_signature, Item_t (Bool_t, rest)))
-    | Prim (_, "h", []), Item_t (t, rest) ->
-        return (Typed (H t, Item_t (String_t, rest)))
-    | Prim (_, "steps_to_quota", []), rest ->
-        return (Typed (Steps_to_quota, Item_t (Int_t Uint32, rest)))
-    | Prim (_, "source", [ ta; tb ]), rest ->
+        return (typed loc (Create_contract (gp, p, r),
+                           Item_t (Contract_t (p, r), rest)))
+    | Prim (loc, "now", []),
+      stack ->
+        return (typed loc (Now, Item_t (Timestamp_t, stack)))
+    | Prim (loc, "amount", []),
+      stack ->
+        return (typed loc (Amount, Item_t (Tez_t, stack)))
+    | Prim (loc, "balance", []),
+      stack ->
+        return (typed loc (Balance, Item_t (Tez_t, stack)))
+    | Prim (loc, "check_signature", []),
+      Item_t (Key_t, Item_t (Pair_t (Signature_t, String_t), rest)) ->
+        return (typed loc (Check_signature, Item_t (Bool_t, rest)))
+    | Prim (loc, "h", []),
+      Item_t (t, rest) ->
+        return (typed loc (H t, Item_t (String_t, rest)))
+    | Prim (loc, "steps_to_quota", []),
+      stack ->
+        return (typed loc (Steps_to_quota, Item_t (Int_t Uint32, stack)))
+    | Prim (loc, "source", [ ta; tb ]),
+      stack ->
         parse_ty ta >>=? fun (Ex ta) ->
         parse_ty tb >>=? fun (Ex tb) ->
-        return (Typed (Source (ta, tb), Item_t (Contract_t (ta, tb), rest)))
+        return (typed loc (Source (ta, tb), Item_t (Contract_t (ta, tb), stack)))
     (* Primitive parsing errors *)
     | Prim (loc, ("drop" | "dup" | "swap" | "some"
                  | "pair" | "car" | "cdr" | "cons"
-                 | "mem" | "update" | "iter" | "map" | "reduce"
+                 | "mem" | "update" | "map" | "reduce"
                  | "get" | "ref" | "deref"
                  | "set" | "exec" | "fail" | "nop"
                  | "concat" | "add" | "sub"
@@ -1131,17 +1320,18 @@ and parse_instr
                  | "manager" | "transfer_tokens" | "create_account"
                  | "create_contract" | "now" | "amount" | "balance"
                  | "check_signature" | "h" | "steps_to_quota"
-                  as name), (_ :: _ as l)), _ ->
+                 as name), (_ :: _ as l)), _ ->
         fail (Invalid_arity (loc, Instr, name, 0, List.length l))
     | Prim (loc, ( "push" | "none" | "left" | "right" | "nil"
                  | "empty_set" | "dip" | "checked_cast" | "cast" | "loop"
-                   as name), ([] | _ :: _ :: _ as l)), _ ->
+                 as name), ([] | _ :: _ :: _ as l)), _ ->
         fail (Invalid_arity (loc, Instr, name, 1, List.length l))
     | Prim (loc, ("if_none" | "if_left" | "if_cons"
                  | "empty_map" | "if" | "source"
-                  as name), ([] | [ _ ] | _ :: _ :: _ :: _ as l)), _ ->
+                 as name), ([] | [ _ ] | _ :: _ :: _ :: _ as l)), _ ->
         fail (Invalid_arity (loc, Instr, name, 2, List.length l))
-    | Prim (loc, "lambda", ([] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ :: _ as l)), _ ->
+    | Prim (loc, "lambda", ([] | [ _ ] | [ _; _ ]
+                           | _ :: _ :: _ :: _ :: _ as l)), _ ->
         fail (Invalid_arity (loc, Instr, "lambda", 3, List.length l))
     (* Stack errors *)
     | Prim (loc, ("add" | "sub" | "mul" | "div" | "mod"
@@ -1156,32 +1346,38 @@ and parse_instr
                  | "neq" | "lt" | "gt" | "le" | "ge" as name), []),
       Item_t (t, _) ->
         fail (Undefined_unop (loc, name, Ty t))
-    | Prim (loc, ("reduce" | "update"), []), _ ->
-        fail (Bad_stack (loc, 3, Stack_ty stack_ty))
-    | Prim (loc, "create_contract", []), _ ->
-        fail (Bad_stack (loc, 6, Stack_ty stack_ty))
-    | Prim (loc, "create_account", []), _ ->
-        fail (Bad_stack (loc, 4, Stack_ty stack_ty))
-    | Prim (loc, "transfer_tokens", []), _ ->
-        fail (Bad_stack (loc, 3, Stack_ty stack_ty))
+    | Prim (loc, ("reduce" | "update"), []),
+      stack ->
+        fail (Bad_stack (loc, 3, Stack_ty stack))
+    | Prim (loc, "create_contract", []),
+      stack ->
+        fail (Bad_stack (loc, 6, Stack_ty stack))
+    | Prim (loc, "create_account", []),
+      stack ->
+        fail (Bad_stack (loc, 4, Stack_ty stack))
+    | Prim (loc, "transfer_tokens", []),
+      stack ->
+        fail (Bad_stack (loc, 3, Stack_ty stack))
     | Prim (loc, ("drop" | "dup" | "car" | "cdr" | "some" | "h" | "dip"
                  | "if_none" | "left" | "right" | "if_left" | "if"
                  | "loop" | "if_cons" | "ref" | "deref" | "manager"
                  | "neg" | "abs" | "not" | "floor" | "ceil" | "isnan" | "nanan"
-                 | "eq" | "neq" | "lt" | "gt" | "le" | "ge"), _), _ ->
-        fail (Bad_stack (loc, 1, Stack_ty stack_ty))
+                 | "eq" | "neq" | "lt" | "gt" | "le" | "ge"), _),
+      stack ->
+        fail (Bad_stack (loc, 1, Stack_ty stack))
     | Prim (loc, ("swap" | "pair" | "cons" | "set" | "incr" | "decr"
-                 | "map" | "iter" | "get" | "mem" | "exec"
+                 | "map" | "get" | "mem" | "exec"
                  | "check_signature" | "add" | "sub" | "mul"
                  | "div" | "mod" | "and" | "or" | "xor"
                  | "lsl" | "lsr" | "concat"
                  | "checked_abs" | "checked_neg" | "checked_add"
-                 | "checked_sub" | "checked_mul" | "compare"), _), _ ->
-        fail (Bad_stack (loc, 2, Stack_ty stack_ty))
+                 | "checked_sub" | "checked_mul" | "compare"), _),
+      stack ->
+        fail (Bad_stack (loc, 2, Stack_ty stack))
     (* Generic parsing errors *)
     | Prim (loc, prim, _), _ ->
         fail @@ Invalid_primitive (loc, Instr, prim)
-    | (Float (loc, _) | Int (loc, _) | String (loc, _)), _ ->
+    | (Int (loc, _) | String (loc, _)), _ ->
         fail @@ Invalid_expression_kind loc
 
 and parse_contract
@@ -1224,7 +1420,6 @@ let unparse_comparable_ty
   | Int_key Uint32 -> Prim (-1, "uint32", [])
   | Int_key Uint64 -> Prim (-1, "uint64", [])
   | String_key -> Prim (-1, "string", [])
-  | Float_key -> Prim (-1, "float", [])
   | Tez_key -> Prim (-1, "tez", [])
   | Bool_key -> Prim (-1, "bool", [])
   | Key_key -> Prim (-1, "key", [])
@@ -1242,7 +1437,6 @@ let rec unparse_ty
   | Int_t Uint32 -> Prim (-1, "uint32", [])
   | Int_t Uint64 -> Prim (-1, "uint64", [])
   | String_t -> Prim (-1, "string", [])
-  | Float_t -> Prim (-1, "float", [])
   | Tez_t -> Prim (-1, "tez", [])
   | Bool_t -> Prim (-1, "bool", [])
   | Key_t -> Prim (-1, "key", [])
@@ -1264,9 +1458,6 @@ let rec unparse_ty
       let ta = unparse_ty uta in
       let tr = unparse_ty utr in
       Prim (-1, "lambda", [ ta; tr ])
-  | Ref_t ut ->
-      let t = unparse_ty ut in
-      Prim (-1, "ref", [ t ])
   | Option_t ut ->
       let t = unparse_ty ut in
       Prim (-1, "option", [ t ])
@@ -1290,8 +1481,6 @@ let rec unparse_untagged_data
         Int (-1, Int64.to_string (to_int64 k v))
     | String_t, s ->
         String (-1, s)
-    | Float_t, f ->
-        Float (-1, string_of_float f)
     | Bool_t, true ->
         Prim (-1, "true", [])
     | Bool_t, false ->
@@ -1319,9 +1508,6 @@ let rec unparse_untagged_data
     | Union_t (_, tr), R r ->
         let r = unparse_untagged_data tr r in
         Prim (-1, "right", [ r ])
-    | Ref_t t, { contents } ->
-        let contents = unparse_untagged_data t contents in
-        Prim (-1, "ref", [ contents ])
     | Option_t t, Some v ->
         let v = unparse_untagged_data t v in
         Prim (-1, "some", [ v ])
@@ -1330,18 +1516,23 @@ let rec unparse_untagged_data
     | List_t t, items ->
         let items = List.map (unparse_untagged_data t) items in
         Prim (-1, "list", items)
-    | Set_t t, ({ contents = items }, _) ->
+    | Set_t t, set ->
         let t = ty_of_comparable_ty t in
-        let items = List.map (unparse_untagged_data t) items in
+        let items =
+          set_fold
+            (fun item acc ->
+               unparse_untagged_data t item :: acc )
+            set [] in
         Prim (-1, "set", items)
-    | Map_t (kt, vt), ({ contents = items }, _) ->
+    | Map_t (kt, vt), map ->
         let kt = ty_of_comparable_ty kt in
         let items =
-          List.map (fun (k, v) ->
+          map_fold (fun k v acc ->
               Prim (-1, "item",
                     [ unparse_untagged_data kt k;
-                      unparse_untagged_data vt v ]))
-            items in
+                      unparse_untagged_data vt v ])
+              :: acc)
+            map [] in
         Prim (-1, "map", items)
     | Lambda_t _, Lam (_, original_code) ->
         original_code
@@ -1355,8 +1546,6 @@ let rec unparse_tagged_data
         Prim (-1, string_of_int_kind k, [ String (-1, Int64.to_string (to_int64 k v))])
     | String_t, s ->
         Prim (-1, "string", [ String (-1, s) ])
-    | Float_t, f ->
-        Prim (-1, "float", [ String (-1, string_of_float f) ])
     | Bool_t, true ->
         Prim (-1, "bool", [ Prim (-1, "true", []) ])
     | Bool_t, false ->
@@ -1390,9 +1579,6 @@ let rec unparse_tagged_data
         let r = unparse_tagged_data tr r in
         let tl = unparse_ty tl in
         Prim (-1, "right", [ tl; r ])
-    | Ref_t t, { contents } ->
-        let contents = unparse_tagged_data t contents in
-        Prim (-1, "ref", [ contents ])
     | Option_t t, Some v ->
         let v = unparse_tagged_data t v in
         Prim (-1, "some", [ v ])
@@ -1403,19 +1589,24 @@ let rec unparse_tagged_data
         let items = List.map (unparse_untagged_data t) items in
         let t = unparse_ty t in
         Prim (-1, "list", t :: items)
-    | Set_t t, ({ contents = items }, _) ->
+    | Set_t t, set ->
         let t = ty_of_comparable_ty t in
-        let items = List.map (unparse_untagged_data t) items in
+        let items =
+          set_fold
+            (fun item acc ->
+               unparse_untagged_data t item :: acc )
+            set [] in
         let t = unparse_ty t in
         Prim (-1, "set", t :: items)
-    | Map_t (kt, vt), ({ contents = items }, _) ->
+    | Map_t (kt, vt), map ->
         let kt = ty_of_comparable_ty kt in
         let items =
-          List.map (fun (k, v) ->
+          map_fold (fun k v acc ->
               Prim (-1, "item",
                     [ unparse_untagged_data kt k;
-                      unparse_untagged_data vt v ]))
-            items in
+                      unparse_untagged_data vt v ])
+              :: acc)
+            map [] in
         let kt = unparse_ty kt in
         let vt = unparse_ty vt in
         Prim (-1, "map", kt :: vt :: items)
@@ -1429,25 +1620,80 @@ type ex_script = Ex : ('a, 'b, 'c) script -> ex_script
 let parse_script
   : context -> Script.storage -> Script.code -> ex_script tzresult Lwt.t
   = fun ctxt { storage; storage_type } { code; arg_type; ret_type } ->
-  parse_ty arg_type >>=? fun (Ex arg_type) ->
-  parse_ty ret_type >>=? fun (Ex ret_type) ->
-  parse_ty storage_type >>=? fun (Ex storage_type) ->
-  let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in
-  let ret_type_full = Pair_t (ret_type, storage_type) in
-  parse_untagged_data ctxt storage_type storage >>=? fun storage ->
-  parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun code ->
-  return (Ex { code; arg_type; ret_type; storage; storage_type })
+    parse_ty arg_type >>=? fun (Ex arg_type) ->
+    parse_ty ret_type >>=? fun (Ex ret_type) ->
+    parse_ty storage_type >>=? fun (Ex storage_type) ->
+    let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in
+    let ret_type_full = Pair_t (ret_type, storage_type) in
+    parse_untagged_data ctxt storage_type storage >>=? fun storage ->
+    parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun code ->
+    return (Ex { code; arg_type; ret_type; storage; storage_type })
+
+type type_map =
+  (int * (Script.expr list * Script.expr list)) list
+
+let type_map_enc =
+  let open Data_encoding in
+  list
+    (tup2
+       int31
+       (tup2
+          (list Script.expr_encoding)
+          (list Script.expr_encoding)))
+
+let type_map descr =
+  let rec unparse_stack
+    : type a. a stack_ty -> Script.expr list
+    = function
+      | Empty_t -> []
+      | Item_t (ty, rest) -> unparse_ty ty :: unparse_stack rest in
+  let rec type_map
+    : type bef aft. type_map -> (bef, aft) descr -> type_map
+    = fun acc { loc ; instr ; bef ; aft } ->
+      let self acc =
+        (loc, (unparse_stack bef, unparse_stack aft)) :: acc in
+      match instr with
+      | If_none (dbt, dbf) ->
+          let acc = type_map acc dbt in
+          let acc = type_map acc dbf in
+          self acc
+      | If_left (dbt, dbf) ->
+          let acc = type_map acc dbt in
+          let acc = type_map acc dbf in
+          self acc
+      | If_cons (dbt, dbf) ->
+          let acc = type_map acc dbt in
+          let acc = type_map acc dbf in
+          self acc
+      | Seq (dl, dr) ->
+          let acc = type_map acc dl in
+          let acc = type_map acc dr in
+          acc
+      | If (dbt, dbf) ->
+          let acc = type_map acc dbt in
+          let acc = type_map acc dbf in
+          self acc
+      | Loop body ->
+          let acc = type_map acc body in
+          self acc
+      | Dip body ->
+          let acc = type_map acc body in
+          self acc
+      | _ ->
+          self acc in
+  type_map [] descr
 
 let typecheck_code
-  : context -> Script.code -> unit tzresult Lwt.t
+  : context -> Script.code -> type_map tzresult Lwt.t
   = fun ctxt { code; arg_type; ret_type; storage_type } ->
-  parse_ty arg_type >>=? fun (Ex arg_type) ->
-  parse_ty ret_type >>=? fun (Ex ret_type) ->
-  parse_ty storage_type >>=? fun (Ex storage_type) ->
-  let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in
-  let ret_type_full = Pair_t (ret_type, storage_type) in
-  parse_lambda ctxt ~storage_type arg_type_full ret_type_full code >>=? fun _ ->
-  return ()
+    parse_ty arg_type >>=? fun (Ex arg_type) ->
+    parse_ty ret_type >>=? fun (Ex ret_type) ->
+    parse_ty storage_type >>=? fun (Ex storage_type) ->
+    let arg_type_full = Pair_t (Pair_t (Tez_t, arg_type), storage_type) in
+    let ret_type_full = Pair_t (ret_type, storage_type) in
+    parse_lambda ctxt ~storage_type arg_type_full ret_type_full code
+    >>=? fun (Lam (descr,_)) ->
+    return (type_map descr)
 
 let typecheck_tagged_data
   : context -> Script.expr -> unit tzresult Lwt.t
diff --git a/src/proto/bootstrap/script_repr.ml b/src/proto/bootstrap/script_repr.ml
index da69098a2..a77cf9e04 100644
--- a/src/proto/bootstrap/script_repr.ml
+++ b/src/proto/bootstrap/script_repr.ml
@@ -29,7 +29,6 @@ let location_encoding =
 
 type expr = (* TODO: turn the location into an alpha ? *)
   | Int of location * string
-  | Float of location * string
   | String of location * string
   | Prim of location * string * expr list
   | Seq of location * expr list
@@ -38,8 +37,6 @@ let expr_encoding =
   let open Data_encoding in
   let int_encoding =
     obj1 (req "int" string) in
-  let float_encoding =
-    obj1 (req "float" string) in
   let string_encoding =
     obj1 (req "string" string) in
   let prim_encoding expr_encoding =
@@ -65,25 +62,21 @@ let expr_encoding =
         [ case ~tag:0 int_encoding
             (function Int (_, v) -> Some v | _ -> None)
             (fun v -> Int (-1, v)) ;
-          case ~tag:1 float_encoding
-            (function Float (_, v) -> Some v | _ -> None)
-            (fun v -> Float (-1, v)) ;
-          case ~tag:2 string_encoding
+          case ~tag:1 string_encoding
             (function String (_, v) -> Some v | _ -> None)
             (fun v -> String (-1, v)) ;
-          case ~tag:3 (prim_encoding expr_encoding)
+          case ~tag:2 (prim_encoding expr_encoding)
             (function
               | Prim (_, v, args) -> Some (v, args)
               | _ -> None)
             (function (prim, args) -> Prim (-1, prim, args)) ;
-          case ~tag:4 (seq_encoding expr_encoding)
+          case ~tag:3 (seq_encoding expr_encoding)
             (function Seq (_, v) -> Some v | _ -> None)
             (fun args -> Seq (-1, args)) ])
 
 let update_locations ir =
   let rec update_locations i = function
     | Int (_, v) -> (Int (i, v), succ i)
-    | Float (_, v) -> (Float (i, v), succ i)
     | String (_, v) -> (String (i, v), succ i)
     | Prim (_, name, args) ->
         let (nargs, ni) =
@@ -99,7 +92,7 @@ let update_locations ir =
               (narg :: nargs, ni))
             ([], succ i) args in
         (Seq (i, List.rev nargs), ni) in
-  fst (update_locations 0 ir)
+  fst (update_locations 1 ir)
 
 let expr_encoding =
   Data_encoding.conv
diff --git a/src/proto/bootstrap/script_repr.mli b/src/proto/bootstrap/script_repr.mli
index ae1936bea..1626022bb 100644
--- a/src/proto/bootstrap/script_repr.mli
+++ b/src/proto/bootstrap/script_repr.mli
@@ -14,7 +14,6 @@ type location =
 
 type expr =
   | Int of location * string
-  | Float of location * string
   | String of location * string
   | Prim of location * string * expr list
   | Seq of location * expr list
diff --git a/src/proto/bootstrap/script_typed_ir.ml b/src/proto/bootstrap/script_typed_ir.ml
index 476b15c77..864372364 100644
--- a/src/proto/bootstrap/script_typed_ir.ml
+++ b/src/proto/bootstrap/script_typed_ir.ml
@@ -10,6 +10,35 @@
 open Tezos_context
 open Script_int
 
+
+(* ---- Auxiliary types -----------------------------------------------------*)
+
+type 'ty comparable_ty =
+  | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
+  | String_key : string comparable_ty
+  | Tez_key : Tez.t comparable_ty
+  | Bool_key : bool comparable_ty
+  | Key_key : public_key_hash comparable_ty
+  | Timestamp_key : Timestamp.t comparable_ty
+
+module type Boxed_set = sig
+  type elt
+  module OPS : Set.S with type elt = elt
+  val boxed : OPS.t
+end
+
+type 'elt set = (module Boxed_set with type elt = 'elt)
+
+module type Boxed_map = sig
+  type key
+  type value
+  val key_ty : key comparable_ty
+  module OPS : Map.S with type key = key
+  val boxed : value OPS.t
+end
+
+type ('key, 'value) map = (module Boxed_map with type key = 'key and type value = 'value)
+
 type ('arg, 'ret, 'storage) script =
   { code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ;
     arg_type : 'arg ty ;
@@ -17,8 +46,6 @@ type ('arg, 'ret, 'storage) script =
     storage : 'storage ;
     storage_type : 'storage ty }
 
-(* ---- Auxiliary types -----------------------------------------------------*)
-
 and ('a, 'b) pair = 'a * 'b
 
 and ('a, 'b) union = L of 'a | R of 'b
@@ -26,26 +53,16 @@ and ('a, 'b) union = L of 'a | R of 'b
 and end_of_stack = unit
 
 and ('arg, 'ret) lambda =
-    Lam of ('arg * end_of_stack, 'ret * end_of_stack) instr * Script.expr
+    Lam of ('arg * end_of_stack, 'ret * end_of_stack) descr * Script.expr
 
 and ('arg, 'ret) typed_contract =
   'arg ty * 'ret ty * Contract.t
 
-and 'ty comparable_ty =
-  | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
-  | String_key : string comparable_ty
-  | Float_key : float comparable_ty
-  | Tez_key : Tez.t comparable_ty
-  | Bool_key : bool comparable_ty
-  | Key_key : public_key_hash comparable_ty
-  | Timestamp_key : Timestamp.t comparable_ty
-
 and 'ty ty =
   | Void_t : unit ty
   | Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty
   | Signature_t : signature ty
   | String_t : string ty
-  | Float_t : float ty
   | Tez_t : Tez.t ty
   | Key_t : public_key_hash ty
   | Timestamp_t : Timestamp.t ty
@@ -54,17 +71,14 @@ and 'ty ty =
   | Union_t : 'a ty * 'b ty -> ('a, 'b) union ty
   | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
   | Option_t : 'v ty -> 'v option ty
-  | Ref_t : 'v ty -> 'v ref ty
   | List_t : 'v ty -> 'v list ty
   | Set_t : 'v comparable_ty -> 'v set ty
   | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
   | Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty
 
-and 'a set =
-  'a list ref * 'a comparable_ty (* FIXME: ok, this is bad *)
-
-and ('a, 'b) map =
-  ('a * 'b) list ref * 'a comparable_ty (* FIXME: we'll have to do better *)
+and 'ty stack_ty =
+  | Item_t : 'ty ty * 'rest stack_ty -> ('ty * 'rest) stack_ty
+  | Empty_t : end_of_stack stack_ty
 
 (* ---- Instructions --------------------------------------------------------*)
 
@@ -97,24 +111,22 @@ and ('bef, 'aft) instr =
       ('v * 'rest, 'v option * 'rest) instr
   | Cons_none : 'a ty ->
     ('rest, 'a option * 'rest) instr
-  | If_none : ('bef, 'aft) instr * ('a * 'bef, 'aft) instr ->
+  | If_none : ('bef, 'aft) descr * ('a * 'bef, 'aft) descr ->
     ('a option * 'bef, 'aft) instr
   (* unions *)
   | Left :
       ('l * 'rest, (('l, 'r) union * 'rest)) instr
   | Right :
       ('r * 'rest, (('l, 'r) union * 'rest)) instr
-  | If_left : ('l * 'bef, 'aft) instr * ('r * 'bef, 'aft) instr ->
+  | If_left : ('l * 'bef, 'aft) descr * ('r * 'bef, 'aft) descr ->
     (('l, 'r) union * 'bef, 'aft) instr
   (* lists *)
   | Cons_list :
       ('a * ('a list * 'rest), ('a list * 'rest)) instr
   | Nil :
       ('rest, ('a list * 'rest)) instr
-  | If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr ->
+  | If_cons : ('a * ('a list * 'bef), 'aft) descr * ('bef, 'aft) descr ->
     ('a list * 'bef, 'aft) instr
-  | List_iter :
-      (('param, unit) lambda * ('param list * 'rest), 'rest) instr
   | List_map :
       (('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr
   | List_reduce :
@@ -123,8 +135,6 @@ and ('bef, 'aft) instr =
   (* sets *)
   | Empty_set : 'a comparable_ty ->
     ('rest, 'a set * 'rest) instr
-  | Set_iter :
-      (('param, unit) lambda * ('param set * 'rest), 'rest) instr
   | Set_map : 'ret comparable_ty ->
     (('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr
   | Set_reduce :
@@ -133,12 +143,10 @@ and ('bef, 'aft) instr =
   | Set_mem :
       ('elt * ('elt set * 'rest), bool * 'rest) instr
   | Set_update :
-      ('elt * (bool * ('elt set * 'rest)), 'rest) instr
+      ('elt * (bool * ('elt set * 'rest)), 'elt set * 'rest) instr
   (* maps *)
   | Empty_map : 'a comparable_ty * 'v ty ->
     ('rest, ('a, 'v) map * 'rest) instr
-  | Map_iter :
-      (('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr
   | Map_map :
       (('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr
   | Map_reduce :
@@ -149,25 +157,14 @@ and ('bef, 'aft) instr =
   | Map_get :
       ('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr
   | Map_update :
-      ('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr
-  (* reference cells *)
-  | Ref :
-      ('v * 'rest, 'v ref * 'rest) instr
-  | Deref :
-      ('v ref * 'rest, 'v * 'rest) instr
-  | Set :
-      ('v ref * ('v * 'rest), 'rest) instr
+      ('a * ('v option * (('a, 'v) map * 'rest)), ('a, 'v) map * 'rest) instr
   (* string operations *)
   | Concat :
       (string * (string * 'rest), string * 'rest) instr
   (* timestamp operations *)
-  | Add_period_to_timestamp :
-      (float * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr
-  | Add_seconds_to_timestamp : (unsigned, 'l) int_kind * Script.location ->
+  | Add_seconds_to_timestamp : (unsigned, 'l) int_kind ->
     ((unsigned, 'l) int_val * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr
-  | Add_timestamp_to_period :
-      (Timestamp.t * (float * 'rest), Timestamp.t * 'rest) instr
-  | Add_timestamp_to_seconds : (unsigned, 'l) int_kind * Script.location ->
+  | Add_timestamp_to_seconds : (unsigned, 'l) int_kind ->
     (Timestamp.t * ((unsigned, 'l) int_val * 'rest), Timestamp.t * 'rest) instr
   (* currency operations *)
   | Add_tez :
@@ -178,33 +175,6 @@ and ('bef, 'aft) instr =
     (Tez.t * ((unsigned, 'l) int_val * 'rest), Tez.t * 'rest) instr
   | Mul_tez' : (unsigned, 'l) int_kind ->
     ((unsigned, 'l) int_val * (Tez.t * 'rest), Tez.t * 'rest) instr
-  (* float operations *)
-  | Neg_float :
-      (float * 'rest, float * 'rest) instr
-  | Abs_float :
-      (float * 'rest, float * 'rest) instr
-  | Add_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Sub_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Mul_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Div_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Mod_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Floor :
-      (float * 'rest, float * 'rest) instr
-  | Ceil :
-      (float * 'rest, float * 'rest) instr
-  | Inf :
-      ('rest, float * 'rest) instr
-  | NaN :
-      ('rest, float * 'rest) instr
-  | IsNaN :
-      (float * 'rest, bool * 'rest) instr
-  | NaNaN : Script.location ->
-    (float * 'rest, 'rest) instr
   (* boolean operations *)
   | Or :
       (bool * (bool * 'rest), bool * 'rest) instr
@@ -215,15 +185,15 @@ and ('bef, 'aft) instr =
   | Not :
       (bool * 'rest, bool * 'rest) instr
   (* integer operations *)
-  | Checked_neg_int : (signed, 'l) int_kind * Script.location ->
+  | Checked_neg_int : (signed, 'l) int_kind ->
     ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Checked_abs_int : (signed, 'l) int_kind * Script.location ->
+  | Checked_abs_int : (signed, 'l) int_kind ->
     ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Checked_add_int : ('s, 'l) int_kind * Script.location ->
+  | Checked_add_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Checked_sub_int : ('s, 'l) int_kind * Script.location ->
+  | Checked_sub_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Checked_mul_int : ('s, 'l) int_kind * Script.location ->
+  | Checked_mul_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
   | Neg_int : (signed, 'l) int_kind ->
     ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
@@ -235,9 +205,9 @@ and ('bef, 'aft) instr =
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
   | Mul_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Div_int : ('s, 'l) int_kind * Script.location ->
+  | Div_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Mod_int : ('s, 'l) int_kind * Script.location ->
+  | Mod_int : ('s, 'l) int_kind ->
     (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
   | Lsl_int : (unsigned, 'l) int_kind ->
     ((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
@@ -252,20 +222,20 @@ and ('bef, 'aft) instr =
   | Not_int : (unsigned, 'l) int_kind ->
     ((unsigned, 'l) int_val * 'rest, (unsigned, 'l) int_val * 'rest) instr
   (* control *)
-  | Seq : ('bef, 'trans) instr * ('trans, 'aft) instr ->
+  | Seq : ('bef, 'trans) descr * ('trans, 'aft) descr ->
     ('bef, 'aft) instr
-  | If : ('bef, 'aft) instr * ('bef, 'aft) instr ->
+  | If : ('bef, 'aft) descr * ('bef, 'aft) descr ->
     (bool * 'bef, 'aft) instr
-  | Loop : ('rest, bool * 'rest) instr ->
+  | Loop : ('rest, bool * 'rest) descr ->
     (bool * 'rest, 'rest) instr
-  | Dip : ('bef, 'aft) instr ->
+  | Dip : ('bef, 'aft) descr ->
     ('top * 'bef, 'top * 'aft) instr
   | Exec :
       ('arg * (('arg, 'ret) lambda * 'rest), 'ret * 'rest) instr
   | Lambda : ('arg, 'ret) lambda ->
     ('rest, ('arg, 'ret) lambda * 'rest) instr
-  | Fail : Script.location ->
-    ('rest, 'rest) instr
+  | Fail :
+    ('bef, 'aft) instr
   | Nop :
       ('rest, 'rest) instr
   (* comparison *)
@@ -287,16 +257,12 @@ and ('bef, 'aft) instr =
   (* casts *)
   | Int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
     (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind * Script.location ->
+  | Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
     (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Int_of_float : ('st, 'lt) int_kind ->
-    (float * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Float_of_int : ('sf, 'lf) int_kind ->
-    (('sf, 'lf) int_val * 'rest, float * 'rest) instr
   (* protocol *)
   | Manager :
       (('arg, 'ret) typed_contract * 'rest, public_key_hash * 'rest) instr
-  | Transfer_tokens : 'sto ty * Script.location ->
+  | Transfer_tokens : 'sto ty ->
     ('arg * (Tez.t * (('arg, 'ret) typed_contract * ('sto * end_of_stack))), 'ret * ('sto * end_of_stack)) instr
   | Create_account :
       (public_key_hash * (public_key_hash option * (bool * (Tez.t * 'rest))),
@@ -319,3 +285,9 @@ and ('bef, 'aft) instr =
     ('rest, ('p, 'r) typed_contract * 'rest) instr
   | Amount :
       ('rest, Tez.t * 'rest) instr
+
+and ('bef, 'aft) descr =
+  { loc : Script.location ;
+    bef : 'bef stack_ty ;
+    aft : 'aft stack_ty ;
+    instr : ('bef, 'aft)  instr }
diff --git a/src/proto/bootstrap/script_typed_ir.mli b/src/proto/bootstrap/script_typed_ir.mli
deleted file mode 100644
index 4be436835..000000000
--- a/src/proto/bootstrap/script_typed_ir.mli
+++ /dev/null
@@ -1,321 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*    Copyright (c) 2014 - 2016.                                          *)
-(*    Dynamic Ledger Solutions, Inc. <contact@tezos.com>                  *)
-(*                                                                        *)
-(*    All rights reserved. No warranty, explicit or implicit, provided.   *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Tezos_context
-open Script_int
-
-type ('arg, 'ret, 'storage) script =
-  { code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ;
-    arg_type : 'arg ty ;
-    ret_type : 'ret ty ;
-    storage : 'storage ;
-    storage_type : 'storage ty }
-
-(* ---- Auxiliary types -----------------------------------------------------*)
-
-and ('a, 'b) pair = 'a * 'b
-
-and ('a, 'b) union = L of 'a | R of 'b
-
-and end_of_stack = unit
-
-and ('arg, 'ret) lambda =
-    Lam of ('arg * end_of_stack, 'ret * end_of_stack) instr * Script.expr
-
-and ('arg, 'ret) typed_contract =
-  'arg ty * 'ret ty * Contract.t
-
-and 'ty comparable_ty =
-  | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty
-  | String_key : string comparable_ty
-  | Float_key : float comparable_ty
-  | Tez_key : Tez.t comparable_ty
-  | Bool_key : bool comparable_ty
-  | Key_key : public_key_hash comparable_ty
-  | Timestamp_key : Time.t comparable_ty
-
-and 'ty ty =
-  | Void_t : unit ty
-  | Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty
-  | Signature_t : signature ty
-  | String_t : string ty
-  | Float_t : float ty
-  | Tez_t : Tez.t ty
-  | Key_t : public_key_hash ty
-  | Timestamp_t : Time.t ty
-  | Bool_t : bool ty
-  | Pair_t : 'a ty * 'b ty -> ('a, 'b) pair ty
-  | Union_t : 'a ty * 'b ty -> ('a, 'b) union ty
-  | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
-  | Option_t : 'v ty -> 'v option ty
-  | Ref_t : 'v ty -> 'v ref ty
-  | List_t : 'v ty -> 'v list ty
-  | Set_t : 'v comparable_ty -> 'v set ty
-  | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
-  | Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty
-
-and 'a set =
-  'a list ref * 'a comparable_ty (* FIXME: ok, this is bad *)
-
-and ('a, 'b) map =
-  ('a * 'b) list ref * 'a comparable_ty (* FIXME: we'll have to do better *)
-
-(* ---- Instructions --------------------------------------------------------*)
-
-(* The low-level, typed instructions, as a GADT whose parameters
-   encode the typing rules. The eft parameter is the typed shape of
-   the stack before the instruction, the right one the shape
-   after. Any program whose construction is accepted by OCaml's
-   type-checker is guaranteed to be type-safe.  Overloadings of the
-   concrete syntax are already resolved in this representation, either
-   by using different constructors or type witness parameters. *)
-and ('bef, 'aft) instr =
-  (* stack ops *)
-  | Drop :
-      (_ * 'rest, 'rest) instr
-  | Dup :
-      ('top * 'rest, 'top * ('top * 'rest)) instr
-  | Swap :
-      ('tip * ('top * 'rest), 'top * ('tip * 'rest)) instr
-  | Const : 'ty ->
-    ('rest, ('ty * 'rest)) instr
-  (* pairs *)
-  | Cons_pair :
-      (('car * ('cdr * 'rest)), (('car, 'cdr) pair * 'rest)) instr
-  | Car :
-      (('car, _) pair * 'rest, 'car * 'rest) instr
-  | Cdr :
-      ((_, 'cdr) pair * 'rest, 'cdr * 'rest) instr
-  (* options *)
-  | Cons_some :
-      ('v * 'rest, 'v option * 'rest) instr
-  | Cons_none : 'a ty ->
-    ('rest, 'a option * 'rest) instr
-  | If_none : ('bef, 'aft) instr * ('a * 'bef, 'aft) instr ->
-    ('a option * 'bef, 'aft) instr
-  (* unions *)
-  | Left :
-      ('l * 'rest, (('l, 'r) union * 'rest)) instr
-  | Right :
-      ('r * 'rest, (('l, 'r) union * 'rest)) instr
-  | If_left : ('l * 'bef, 'aft) instr * ('r * 'bef, 'aft) instr ->
-    (('l, 'r) union * 'bef, 'aft) instr
-  (* lists *)
-  | Cons_list :
-      ('a * ('a list * 'rest), ('a list * 'rest)) instr
-  | Nil :
-      ('rest, ('a list * 'rest)) instr
-  | If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr ->
-    ('a list * 'bef, 'aft) instr
-  | List_iter :
-      (('param, unit) lambda * ('param list * 'rest), 'rest) instr
-  | List_map :
-      (('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr
-  | List_reduce :
-      (('param * 'res, 'res) lambda *
-       ('param list * ('res * 'rest)), 'res * 'rest) instr
-  (* sets *)
-  | Empty_set : 'a comparable_ty ->
-    ('rest, 'a set * 'rest) instr
-  | Set_iter :
-      (('param, unit) lambda * ('param set * 'rest), 'rest) instr
-  | Set_map : 'ret comparable_ty ->
-    (('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr
-  | Set_reduce :
-      (('param * 'res, 'res) lambda *
-       ('param set * ('res * 'rest)), 'res * 'rest) instr
-  | Set_mem :
-      ('elt * ('elt set * 'rest), bool * 'rest) instr
-  | Set_update :
-      ('elt * (bool * ('elt set * 'rest)), 'rest) instr
-  (* maps *)
-  | Empty_map : 'a comparable_ty * 'v ty ->
-    ('rest, ('a, 'v) map * 'rest) instr
-  | Map_iter :
-      (('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr
-  | Map_map :
-      (('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr
-  | Map_reduce :
-      ((('a * 'v) * 'res, 'res) lambda *
-       (('a, 'v) map * ('res * 'rest)), 'res * 'rest) instr
-  | Map_mem :
-      ('a * (('a, 'v) map * 'rest), bool * 'rest) instr
-  | Map_get :
-      ('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr
-  | Map_update :
-      ('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr
-  (* reference cells *)
-  | Ref :
-      ('v * 'rest, 'v ref * 'rest) instr
-  | Deref :
-      ('v ref * 'rest, 'v * 'rest) instr
-  | Set :
-      ('v ref * ('v * 'rest), 'rest) instr
-  (* string operations *)
-  | Concat :
-      (string * (string * 'rest), string * 'rest) instr
-  (* timestamp operations *)
-  | Add_period_to_timestamp :
-      (float * (Time.t * 'rest), Time.t * 'rest) instr
-  | Add_seconds_to_timestamp : (unsigned, 'l) int_kind * Script.location ->
-    ((unsigned, 'l) int_val * (Time.t * 'rest), Time.t * 'rest) instr
-  | Add_timestamp_to_period :
-      (Time.t * (float * 'rest), Time.t * 'rest) instr
-  | Add_timestamp_to_seconds : (unsigned, 'l) int_kind * Script.location ->
-    (Time.t * ((unsigned, 'l) int_val * 'rest), Time.t * 'rest) instr
-  (* currency operations *)
-  | Add_tez :
-      (Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr
-  | Sub_tez :
-      (Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr
-  | Mul_tez : (unsigned, 'l) int_kind ->
-    (Tez.t * ((unsigned, 'l) int_val * 'rest), Tez.t * 'rest) instr
-  | Mul_tez' : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * (Tez.t * 'rest), Tez.t * 'rest) instr
-  (* float operations *)
-  | Neg_float :
-      (float * 'rest, float * 'rest) instr
-  | Abs_float :
-      (float * 'rest, float * 'rest) instr
-  | Add_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Sub_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Mul_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Div_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Mod_float :
-      (float * (float * 'rest), float * 'rest) instr
-  | Floor :
-      (float * 'rest, float * 'rest) instr
-  | Ceil :
-      (float * 'rest, float * 'rest) instr
-  | Inf :
-      ('rest, float * 'rest) instr
-  | NaN :
-      ('rest, float * 'rest) instr
-  | IsNaN :
-      (float * 'rest, bool * 'rest) instr
-  | NaNaN : Script.location ->
-    (float * 'rest, 'rest) instr
-  (* boolean operations *)
-  | Or :
-      (bool * (bool * 'rest), bool * 'rest) instr
-  | And :
-      (bool * (bool * 'rest), bool * 'rest) instr
-  | Xor :
-      (bool * (bool * 'rest), bool * 'rest) instr
-  | Not :
-      (bool * 'rest, bool * 'rest) instr
-  (* integer operations *)
-  | Checked_neg_int : (signed, 'l) int_kind * Script.location ->
-    ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Checked_abs_int : (signed, 'l) int_kind * Script.location ->
-    ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Checked_add_int : ('s, 'l) int_kind * Script.location ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Checked_sub_int : ('s, 'l) int_kind * Script.location ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Checked_mul_int : ('s, 'l) int_kind * Script.location ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Neg_int : (signed, 'l) int_kind ->
-    ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Abs_int : (signed, 'l) int_kind ->
-    ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr
-  | Add_int : ('s, 'l) int_kind ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Sub_int : ('s, 'l) int_kind ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Mul_int : ('s, 'l) int_kind ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Div_int : ('s, 'l) int_kind * Script.location ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Mod_int : ('s, 'l) int_kind * Script.location ->
-    (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr
-  | Lsl_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
-  | Lsr_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
-  | Or_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
-  | And_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
-  | Xor_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr
-  | Not_int : (unsigned, 'l) int_kind ->
-    ((unsigned, 'l) int_val * 'rest, (unsigned, 'l) int_val * 'rest) instr
-  (* control *)
-  | Seq : ('bef, 'trans) instr * ('trans, 'aft) instr ->
-    ('bef, 'aft) instr
-  | If : ('bef, 'aft) instr * ('bef, 'aft) instr ->
-    (bool * 'bef, 'aft) instr
-  | Loop : ('rest, bool * 'rest) instr ->
-    (bool * 'rest, 'rest) instr
-  | Dip : ('bef, 'aft) instr ->
-    ('top * 'bef, 'top * 'aft) instr
-  | Exec :
-      ('arg * (('arg, 'ret) lambda * 'rest), 'ret * 'rest) instr
-  | Lambda : ('arg, 'ret) lambda ->
-    ('rest, ('arg, 'ret) lambda * 'rest) instr
-  | Fail : Script.location ->
-    ('rest, 'rest) instr
-  | Nop :
-      ('rest, 'rest) instr
-  (* comparison *)
-  | Compare : 'a comparable_ty ->
-    ('a * ('a * 'rest), (signed, sixtyfour) int_val * 'rest) instr
-  (* comparators *)
-  | Eq :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  | Neq :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  | Lt :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  | Gt :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  | Le :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  | Ge :
-      ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr
-  (* casts *)
-  | Int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind ->
-    (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind * Script.location ->
-    (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Int_of_float : ('st, 'lt) int_kind ->
-    (float * 'rest, ('st, 'lt) int_val * 'rest) instr
-  | Float_of_int : ('sf, 'lf) int_kind ->
-    (('sf, 'lf) int_val * 'rest, float * 'rest) instr
-  (* protocol *)
-  | Manager :
-      (('arg, 'ret) typed_contract * 'rest, public_key_hash * 'rest) instr
-  | Transfer_tokens : 'sto ty * Script.location ->
-    ('arg * (Tez.t * (('arg, 'ret) typed_contract * ('sto * end_of_stack))), 'ret * ('sto * end_of_stack)) instr
-  | Create_account :
-      (public_key_hash * (public_key_hash option * (bool * (Tez.t * 'rest))),
-       (unit, unit) typed_contract * 'rest) instr
-  | Create_contract : 'g ty * 'p ty * 'r ty ->
-    (public_key_hash * (public_key_hash option * (bool * (Tez.t *
-                                                          (((Tez.t * 'p) * 'g, 'r * 'g) lambda * ('g * 'rest))))),
-     ('p, 'r) typed_contract * 'rest) instr
-  | Now :
-      ('rest, Time.t * 'rest) instr
-  | Balance :
-      ('rest, Tez.t * 'rest) instr
-  | Check_signature :
-      (public_key_hash * ((signature * string) * 'rest), bool * 'rest) instr
-  | H : 'a ty ->
-    ('a * 'rest, string * 'rest) instr
-  | Steps_to_quota :
-      ('rest, (unsigned, thirtytwo) int_val * 'rest) instr
-  | Source : 'p ty * 'r ty ->
-    ('rest, ('p, 'r) typed_contract * 'rest) instr
-  | Amount :
-      ('rest, Tez.t * 'rest) instr
diff --git a/src/proto/bootstrap/services.ml b/src/proto/bootstrap/services.ml
index 7054f08d8..e40fb3191 100644
--- a/src/proto/bootstrap/services.ml
+++ b/src/proto/bootstrap/services.ml
@@ -327,11 +327,45 @@ module Helpers = struct
                 obj1 (req "timestamp" Timestamp.encoding))
       RPC.Path.(custom_root / "helpers" / "minimal_timestamp")
 
+  let run_code_input_encoding =
+    (obj5
+       (req "script" Script.code_encoding)
+       (req "storage" Script.expr_encoding)
+       (req "input" Script.expr_encoding)
+       (opt "amount" Tez.encoding)
+       (opt "contract" Contract.encoding))
+
+  let run_code custom_root =
+    RPC.service
+      ~description: "Run a piece of code in the current context"
+      ~input: run_code_input_encoding
+      ~output: (wrap_tzerror
+                  (obj2
+                     (req "storage" Script.expr_encoding)
+                     (req "output" Script.expr_encoding)))
+      RPC.Path.(custom_root / "helpers" / "run_code")
+
+  let trace_code custom_root =
+    RPC.service
+      ~description: "Run a piece of code in the current context, \
+                     keeping a trace"
+      ~input: run_code_input_encoding
+      ~output: (wrap_tzerror
+                  (obj3
+                     (req "storage" Script.expr_encoding)
+                     (req "output" Script.expr_encoding)
+                     (req "trace"
+                        (list @@ obj3
+                           (req "location" Script.location_encoding)
+                           (req "gas" int31)
+                           (req "stack" (list (Script.expr_encoding)))))))
+      RPC.Path.(custom_root / "helpers" / "trace_code")
+
   let typecheck_code custom_root =
     RPC.service
       ~description: "Typecheck a piece of code in the current context"
       ~input: Script.code_encoding
-      ~output: (wrap_tzerror empty)
+      ~output: (wrap_tzerror Script_ir_translator.type_map_enc)
       RPC.Path.(custom_root / "helpers" / "typecheck_code")
 
   let typecheck_tagged_data custom_root =
diff --git a/src/proto/bootstrap/services_registration.ml b/src/proto/bootstrap/services_registration.ml
index edbfeea33..653a0656c 100644
--- a/src/proto/bootstrap/services_registration.ml
+++ b/src/proto/bootstrap/services_registration.ml
@@ -179,6 +179,47 @@ let minimal_timestamp ctxt prio =
 
 let () = register1 Services.Helpers.minimal_timestamp minimal_timestamp
 
+let () =
+  let run_parameters ctxt (script, storage, input, amount, contract) =
+    let amount =
+      match amount with
+      | Some amount -> amount
+      | None ->
+          match Tez.of_cents 100_00L with
+          | Some tez -> tez
+          | None -> Tez.zero in
+    let contract =
+      match contract with
+      | Some contract -> contract
+      | None ->
+          Contract.default_contract
+            (List.hd Bootstrap.accounts).Bootstrap.public_key_hash in
+    let storage : Script.storage =
+      { storage ; storage_type = (script : Script.code).storage_type } in
+    let qta =
+      Constants.instructions_per_transaction ctxt in
+    (script, storage, input, amount, contract, qta) in
+  register1 Services.Helpers.run_code
+    (fun ctxt parameters ->
+       let (script, storage, input, amount, contract, qta) =
+         run_parameters ctxt parameters in
+       Script_interpreter.execute
+         contract (* transaction initiator *)
+         contract (* script owner *)
+         ctxt storage script amount input
+         qta >>=? fun (sto, ret, _qta, _ctxt) ->
+       Error_monad.return (sto, ret)) ;
+  register1 Services.Helpers.trace_code
+    (fun ctxt parameters ->
+       let (script, storage, input, amount, contract, qta) =
+         run_parameters ctxt parameters in
+       Script_interpreter.trace
+         contract (* transaction initiator *)
+         contract (* script owner *)
+         ctxt storage script amount input
+         qta >>=? fun ((sto, ret, _qta, _ctxt), trace) ->
+       Error_monad.return (sto, ret, trace))
+
 let () =
   register1 Services.Helpers.typecheck_code
     Script_ir_translator.typecheck_code
diff --git a/src/proto/bootstrap/tezos_context.mli b/src/proto/bootstrap/tezos_context.mli
index 2da485bf6..61b654084 100644
--- a/src/proto/bootstrap/tezos_context.mli
+++ b/src/proto/bootstrap/tezos_context.mli
@@ -109,7 +109,6 @@ module Script : sig
 
   type expr =
     | Int of location * string
-    | Float of location * string
     | String of location * string
     | Prim of location * string * expr list
     | Seq of location * expr list