diff --git a/src/lib_utils/PP.ml b/src/lib_utils/PP.ml
index b82249812..49063c2d4 100644
--- a/src/lib_utils/PP.ml
+++ b/src/lib_utils/PP.ml
@@ -1,6 +1,7 @@
 open Format
 let string : formatter -> string -> unit = fun ppf s -> fprintf ppf "%s" s
 let tag tag : formatter -> unit -> unit = fun ppf () -> fprintf ppf tag
+let bool ppf b = fprintf ppf "%b" b
 let new_line : formatter -> unit -> unit = tag "@;"
 let rec new_lines n ppf () =
   match n with
@@ -23,6 +24,11 @@ let option = fun f ppf opt ->
   | Some x -> fprintf ppf "Some(%a)" f x
   | None -> fprintf ppf "None"
 
+let lr = fun ppf lr ->
+  match lr with
+  | `Left -> fprintf ppf "left"
+  | `Right -> fprintf ppf "right"
+
 let int = fun ppf n -> fprintf ppf "%d" n
 
 let map = fun f pp ppf x ->
diff --git a/src/lib_utils/function.ml b/src/lib_utils/function.ml
index f567d55ee..57179077f 100644
--- a/src/lib_utils/function.ml
+++ b/src/lib_utils/function.ml
@@ -1,3 +1,5 @@
+let constant x _ = x
+
 let compose = fun f g x -> f (g x)
 let (>|) = compose
 
diff --git a/src/lib_utils/logger.ml b/src/lib_utils/logger.ml
new file mode 100644
index 000000000..76f536175
--- /dev/null
+++ b/src/lib_utils/logger.ml
@@ -0,0 +1,11 @@
+module Stateful () : sig
+  val log : string -> unit
+  val get : unit -> string
+end = struct
+
+  let logger = ref ""
+  let log : string -> unit =
+    fun s -> logger := !logger ^ s
+  let get () : string = !logger
+
+end
diff --git a/src/lib_utils/tezos_utils.ml b/src/lib_utils/tezos_utils.ml
index 3b7158df3..63dcd2c9d 100644
--- a/src/lib_utils/tezos_utils.ml
+++ b/src/lib_utils/tezos_utils.ml
@@ -10,6 +10,7 @@ module Micheline = X_tezos_micheline
 module Function = Function
 module Error_monad = X_error_monad
 module Trace = Trace
+module Logger = Logger
 module PP_helpers = PP
 module Location = Location
 
diff --git a/src/lib_utils/trace.ml b/src/lib_utils/trace.ml
index c2f9c6a33..6dc7a7093 100644
--- a/src/lib_utils/trace.ml
+++ b/src/lib_utils/trace.ml
@@ -128,6 +128,10 @@ let trace_option error = function
   | None -> fail error
   | Some s -> ok s
 
+let bind_map_option f = function
+  | None -> ok None
+  | Some s -> f s >>? fun x -> ok (Some x)
+
 let rec bind_list = function
   | [] -> ok []
   | hd :: tl -> (
@@ -175,6 +179,16 @@ let bind_fold_list f init lst =
   in
   List.fold_left aux (ok init) lst
 
+let bind_fold_map_list = fun f acc lst ->
+  let rec aux (acc , prev) f = function
+    | [] -> ok (acc , prev)
+    | hd :: tl ->
+        f acc hd >>? fun (acc' , hd') ->
+        aux (acc' , hd' :: prev) f tl
+  in
+  aux (acc , []) f (List.rev lst) >>? fun (_acc' , lst') ->
+  ok lst'
+
 let bind_fold_right_list f init lst =
   let aux x y =
     x >>? fun x ->
@@ -342,6 +356,10 @@ let pp_to_string pp () x =
 let errors_to_string = pp_to_string errors_pp
 
 module Assert = struct
+  let assert_fail ?(msg="didn't fail") = function
+    | Ok _ -> simple_fail msg
+    | _ -> ok ()
+
   let assert_true ?(msg="not true") = function
     | true -> ok ()
     | false -> simple_fail msg
diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml
index 6439e7f1f..2c28dd98f 100644
--- a/src/lib_utils/x_list.ml
+++ b/src/lib_utils/x_list.ml
@@ -7,6 +7,16 @@ let map ?(acc = []) f lst =
   in
   aux acc f (List.rev lst)
 
+let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list -> ret list =
+  fun f acc lst ->
+  let rec aux (acc , prev) f = function
+    | [] -> (acc , prev)
+    | hd :: tl ->
+        let (acc' , hd') = f acc hd in
+        aux (acc' , hd' :: prev) f tl
+  in
+  snd @@ aux (acc , []) f (List.rev lst)
+
 let fold_right' f init lst = List.fold_left f init (List.rev lst)
 
 let filter_map f =
diff --git a/src/lib_utils/x_memory_proto_alpha.ml b/src/lib_utils/x_memory_proto_alpha.ml
index 0fedfbd4f..7e383da7c 100644
--- a/src/lib_utils/x_memory_proto_alpha.ml
+++ b/src/lib_utils/x_memory_proto_alpha.ml
@@ -44,6 +44,29 @@ let parse_michelson (type aft)
     )
   | _ -> Lwt.return @@ error_exn (Failure "Typing instr failed")
 
+let parse_michelson_fail (type aft)
+    ?(tezos_context = dummy_environment.tezos_context)
+    ?(top_level = Lambda) (michelson:Michelson.t)
+    ?type_logger
+    (bef:'a Script_typed_ir.stack_ty) (aft:aft Script_typed_ir.stack_ty)
+  =
+  let michelson = Michelson.strip_annots michelson in
+  let michelson = Michelson.strip_nops michelson in
+  parse_instr
+    ?type_logger
+    top_level tezos_context
+    michelson bef >>=?? fun (j, _) ->
+  match j with
+  | Typed descr -> (
+      Lwt.return (
+        alpha_wrap (Script_ir_translator.stack_ty_eq tezos_context 0 descr.aft aft) >>? fun (Eq, _) ->
+        let descr : (_, aft) Script_typed_ir.descr = {descr with aft} in
+        Ok descr
+      )
+    )
+  | Failed { descr } ->
+      Lwt.return (Ok (descr aft))
+
 let parse_michelson_data
     ?(tezos_context = dummy_environment.tezos_context)
     michelson ty =
@@ -79,7 +102,8 @@ let interpret
     ?(source = (List.nth dummy_environment.identities 0).implicit_contract)
     ?(self = (List.nth dummy_environment.identities 0).implicit_contract)
     ?(payer = (List.nth dummy_environment.identities 1).implicit_contract)
+    ?(amount = Alpha_context.Tez.one)
     ?visitor
     (instr:('a, 'b) descr) (bef:'a stack) : 'b stack tzresult Lwt.t  =
-  Script_interpreter.step tezos_context ~source ~self ~payer ?visitor Alpha_context.Tez.one instr bef >>=??
+  Script_interpreter.step tezos_context ~source ~self ~payer ?visitor amount instr bef >>=??
   fun (stack, _) -> return stack
diff --git a/src/ligo/TODO.txt b/src/ligo/TODO.txt
index ea687b9ba..ef5f79d1e 100644
--- a/src/ligo/TODO.txt
+++ b/src/ligo/TODO.txt
@@ -1,2 +1,19 @@
-- Unify gets in Ast_simplified
-- Unify assignments in Ast_simplified
+# Main
+
+## Back-end
+
+- Replace Mini_c environments with stacks
+- Think about Coq
+
+## Amendments
+
+- Bubble_n
+- Partial application
+- Type size limit (1.000 -> 10.000)
+
+# PPX
+
+## Deriving
+
+- Generate ADT helpers (this removes 90% of Combinators and a lot of maintenance when modifying ASTs)
+- Generate option helpers (this makes writing main much easier, much like one would in an untyped language)
diff --git a/src/ligo/ast_simplified/PP.ml b/src/ligo/ast_simplified/PP.ml
index 36e339209..028f9b5bc 100644
--- a/src/ligo/ast_simplified/PP.ml
+++ b/src/ligo/ast_simplified/PP.ml
@@ -21,6 +21,7 @@ let literal ppf (l:literal) = match l with
   | Literal_tez n -> fprintf ppf "%dtz" n
   | Literal_string s -> fprintf ppf "%S" s
   | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
+  | Literal_address s -> fprintf ppf "@%S" s
 
 let rec expression ppf (e:expression) = match e with
   | E_literal l -> literal ppf l
@@ -50,6 +51,7 @@ and access ppf (a:access) =
   match a with
   | Access_tuple n -> fprintf ppf "%d" n
   | Access_record s -> fprintf ppf "%s" s
+  | Access_map s -> fprintf ppf "(%a)" annotated_expression s
 
 and access_path ppf (p:access_path) =
   fprintf ppf "%a" (list_sep access (const ".")) p
@@ -69,6 +71,9 @@ and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
 and single_record_patch ppf ((p, ae) : string * ae) =
   fprintf ppf "%s <- %a" p annotated_expression ae
 
+and single_tuple_patch ppf ((p, ae) : int * ae) =
+  fprintf ppf "%d <- %a" p annotated_expression ae
+
 and matching_variant_case : type a . (_ -> a -> unit) -> _ -> (constructor_name * name) * a -> unit =
   fun f ppf ((c,n),a) ->
   fprintf ppf "| %s %s -> %a" c n f a
@@ -90,6 +95,7 @@ and instruction ppf (i:instruction) = match i with
   | I_skip -> fprintf ppf "skip"
   | I_do ae -> fprintf ppf "do %a" annotated_expression ae
   | I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
+  | I_tuple_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_tuple_patch) lst
   | I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
   | I_assignment {name;annotated_expression = ae} ->
       fprintf ppf "%s := %a" name annotated_expression ae
diff --git a/src/ligo/ast_simplified/combinators.ml b/src/ligo/ast_simplified/combinators.ml
index c8a1257b3..0ce8bc97b 100644
--- a/src/ligo/ast_simplified/combinators.ml
+++ b/src/ligo/ast_simplified/combinators.ml
@@ -26,17 +26,15 @@ let t_bytes     : type_expression = T_constant ("bytes", [])
 let t_int       : type_expression = T_constant ("int", [])
 let t_operation : type_expression = T_constant ("operation", [])
 let t_nat       : type_expression = T_constant ("nat", [])
+let t_tez       : type_expression = T_constant ("tez", [])
 let t_unit      : type_expression = T_constant ("unit", [])
+let t_address      : type_expression = T_constant ("address", [])
 let t_option  o : type_expression = T_constant ("option", [o])
 let t_list  t : type_expression = T_constant ("list", [t])
 let t_variable n : type_expression = T_variable n
 let t_tuple lst : type_expression = T_tuple lst
 let t_pair (a , b) = t_tuple [a ; b]
 let t_record m  : type_expression = (T_record m)
-let t_ez_record (lst:(string * type_expression) list) : type_expression =
-  let aux prev (k, v) = SMap.add k v prev in
-  let map = List.fold_left aux SMap.empty lst in
-  T_record map
 
 let t_record_ez lst =
   let m = SMap.of_list lst in
@@ -63,6 +61,8 @@ let e_int n : expression = E_literal (Literal_int n)
 let e_nat n : expression = E_literal (Literal_nat n)
 let e_bool   b : expression = E_literal (Literal_bool b)
 let e_string s : expression = E_literal (Literal_string s)
+let e_address s : expression = E_literal (Literal_address s)
+let e_tez s : expression = E_literal (Literal_tez s)
 let e_bytes  b : expression = E_literal (Literal_bytes (Bytes.of_string b))
 let e_record map : expression = E_record map
 let e_tuple lst : expression = E_tuple lst
@@ -84,6 +84,8 @@ let e_a_int n : annotated_expression = make_e_a_full (e_int n) t_int
 let e_a_nat n : annotated_expression = make_e_a_full (e_nat n) t_nat
 let e_a_bool b : annotated_expression = make_e_a_full (e_bool b) t_bool
 let e_a_constructor s a : annotated_expression = make_e_a (e_constructor s a)
+let e_a_address x = make_e_a_full (e_address x) t_address
+let e_a_tez x = make_e_a_full (e_tez x) t_tez
 
 let e_a_record r =
   let type_annotation = Option.(
@@ -163,3 +165,9 @@ let get_a_accessor = fun t ->
 let assert_a_accessor = fun t ->
   let%bind _ = get_a_accessor t in
   ok ()
+
+let get_access_record : access -> string result = fun a ->
+  match a with
+  | Access_tuple _
+  | Access_map _ -> simple_fail "not an access record"
+  | Access_record s -> ok s
diff --git a/src/ligo/ast_simplified/misc.ml b/src/ligo/ast_simplified/misc.ml
index 49baa1820..8e7eadaf2 100644
--- a/src/ligo/ast_simplified/misc.ml
+++ b/src/ligo/ast_simplified/misc.ml
@@ -23,6 +23,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
   | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
   | Literal_unit, Literal_unit -> ok ()
   | Literal_unit, _ -> simple_fail "unit vs non-unit"
+  | Literal_address a, Literal_address b when a = b -> ok ()
+  | Literal_address _, Literal_address _ -> simple_fail "different addresss"
+  | Literal_address _, _ -> simple_fail "address vs non-address"
 
 let rec assert_value_eq (a, b: (value*value)) : unit result =
   let error_content () =
diff --git a/src/ligo/ast_simplified/types.ml b/src/ligo/ast_simplified/types.ml
index 4df0d9fda..117acc62b 100644
--- a/src/ligo/ast_simplified/types.ml
+++ b/src/ligo/ast_simplified/types.ml
@@ -75,6 +75,7 @@ and expression =
 and access =
   | Access_tuple of int
   | Access_record of string
+  | Access_map of ae
 
 and access_path = access list
 
@@ -86,6 +87,7 @@ and literal =
   | Literal_tez of int
   | Literal_string of string
   | Literal_bytes of bytes
+  | Literal_address of string
 
 and block = instruction list
 and b = block
@@ -96,7 +98,8 @@ and instruction =
   | I_loop of ae * b
   | I_skip
   | I_do of ae
-  | I_record_patch of name * access_path * (string * ae) list
+  | I_record_patch of (name * access_path * (string * ae) list)
+  | I_tuple_patch of (name * access_path * (int * ae) list)
 
 and 'a matching =
   | Match_bool of {
diff --git a/src/ligo/ast_typed/PP.ml b/src/ligo/ast_typed/PP.ml
index 4363c3490..dfb410432 100644
--- a/src/ligo/ast_typed/PP.ml
+++ b/src/ligo/ast_typed/PP.ml
@@ -62,6 +62,7 @@ and literal ppf (l:literal) : unit =
   | Literal_tez n -> fprintf ppf "%dtz" n
   | Literal_string s -> fprintf ppf "%s" s
   | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
+  | Literal_address s -> fprintf ppf "@%s" s
 
 and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
 
@@ -87,6 +88,7 @@ and matching : type a . (formatter -> a -> unit) -> _ -> a matching -> unit = fu
 and pre_access ppf (a:access) = match a with
   | Access_record n -> fprintf ppf ".%s" n
   | Access_tuple i -> fprintf ppf ".%d" i
+  | Access_map n -> fprintf ppf ".%a" annotated_expression n
 
 and instruction ppf (i:instruction) = match i with
   | I_skip -> fprintf ppf "skip"
diff --git a/src/ligo/ast_typed/combinators.ml b/src/ligo/ast_typed/combinators.ml
index dfa538634..e86848066 100644
--- a/src/ligo/ast_typed/combinators.ml
+++ b/src/ligo/ast_typed/combinators.ml
@@ -91,13 +91,21 @@ let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' wi
 
 let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
   | T_record m -> ok m
-  | _ -> simple_fail "not a record"
+  | _ -> simple_fail "not a record type"
 
 let get_t_map (t:type_value) : (type_value * type_value) result =
   match t.type_value' with
   | T_constant ("map", [k;v]) -> ok (k, v)
   | _ -> simple_fail "get: not a map"
 
+let get_t_map_key : type_value -> type_value result = fun t ->
+  let%bind (key , _) = get_t_map t in
+  ok key
+
+let get_t_map_value : type_value -> type_value result = fun t ->
+  let%bind (_ , value) = get_t_map t in
+  ok value
+
 let assert_t_tez :type_value -> unit result = get_t_tez
 
 let assert_t_map (t:type_value) : unit result =
@@ -143,16 +151,20 @@ let e_map lst : expression = E_map lst
 let e_unit : expression = E_literal (Literal_unit)
 let e_int n : expression = E_literal (Literal_int n)
 let e_nat n : expression = E_literal (Literal_nat n)
+let e_tez n : expression = E_literal (Literal_tez n)
 let e_bool b : expression = E_literal (Literal_bool b)
 let e_string s : expression = E_literal (Literal_string s)
+let e_address s : expression = E_literal (Literal_address s)
 let e_pair a b : expression = E_tuple [a; b]
 let e_list lst : expression = E_list lst
 
 let e_a_unit = make_a_e e_unit (t_unit ())
 let e_a_int n = make_a_e (e_int n) (t_int ())
 let e_a_nat n = make_a_e (e_nat n) (t_nat ())
+let e_a_tez n = make_a_e (e_tez n) (t_tez ())
 let e_a_bool b = make_a_e (e_bool b) (t_bool ())
 let e_a_string s = make_a_e (e_string s) (t_string ())
+let e_a_address s = make_a_e (e_address s) (t_address ())
 let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
 let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
 let e_a_none t = make_a_e e_none (t_option t ())
diff --git a/src/ligo/ast_typed/combinators_environment.ml b/src/ligo/ast_typed/combinators_environment.ml
index e30bb233f..3d715c588 100644
--- a/src/ligo/ast_typed/combinators_environment.ml
+++ b/src/ligo/ast_typed/combinators_environment.ml
@@ -6,8 +6,10 @@ let make_a_e_empty expression type_annotation = make_a_e expression type_annotat
 let e_a_empty_unit = e_a_unit Environment.full_empty
 let e_a_empty_int n = e_a_int n Environment.full_empty
 let e_a_empty_nat n = e_a_nat n Environment.full_empty
+let e_a_empty_tez n = e_a_tez n Environment.full_empty
 let e_a_empty_bool b = e_a_bool b Environment.full_empty
 let e_a_empty_string s = e_a_string s Environment.full_empty
+let e_a_empty_address s = e_a_address s Environment.full_empty
 let e_a_empty_pair a b = e_a_pair a b Environment.full_empty
 let e_a_empty_some s = e_a_some s Environment.full_empty
 let e_a_empty_none t = e_a_none t Environment.full_empty
diff --git a/src/ligo/ast_typed/misc.ml b/src/ligo/ast_typed/misc.ml
index ff02c0b4c..70df407d0 100644
--- a/src/ligo/ast_typed/misc.ml
+++ b/src/ligo/ast_typed/misc.ml
@@ -226,8 +226,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
       let rb' = SMap.to_kv_list rb in
       let aux ((ka, va), (kb, vb)) =
         let%bind _ =
-          Assert.assert_true ~msg:"different keys in record types"
-          @@ (ka = kb) in
+          let error =
+            let title () = "different props in record" in
+            let content () = Format.asprintf "%s vs %s" ka kb in
+            error title content in
+          trace_strong error @@
+          Assert.assert_true (ka = kb) in
         assert_type_value_eq (va, vb)
       in
       let%bind _ =
@@ -269,6 +273,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
   | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
   | Literal_unit, Literal_unit -> ok ()
   | Literal_unit, _ -> simple_fail "unit vs non-unit"
+  | Literal_address a, Literal_address b when a = b -> ok ()
+  | Literal_address _, Literal_address _ -> simple_fail "different addresss"
+  | Literal_address _, _ -> simple_fail "address vs non-address"
 
 
 let rec assert_value_eq (a, b: (value*value)) : unit result =
diff --git a/src/ligo/ast_typed/types.ml b/src/ligo/ast_typed/types.ml
index 55e3fb482..89051aaf6 100644
--- a/src/ligo/ast_typed/types.ml
+++ b/src/ligo/ast_typed/types.ml
@@ -106,6 +106,7 @@ and literal =
   | Literal_tez of int
   | Literal_string of string
   | Literal_bytes of bytes
+  | Literal_address of string
 
 and block = instruction list
 and b = block
@@ -119,9 +120,12 @@ and instruction =
   | I_skip
   | I_patch of named_type_value * access_path * ae
 
-and access = Ast_simplified.access
+and access =
+  | Access_tuple of int
+  | Access_record of string
+  | Access_map of ae
 
-and access_path = Ast_simplified.access_path
+and access_path = access list
 
 and 'a matching =
   | Match_bool of {
diff --git a/src/ligo/compiler/compiler_program.ml b/src/ligo/compiler/compiler_program.ml
index 3ef3478c4..16d19547f 100644
--- a/src/ligo/compiler/compiler_program.ml
+++ b/src/ligo/compiler/compiler_program.ml
@@ -402,95 +402,7 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
 
 and translate_statement ((s', w_env) as s:statement) : michelson result =
   let error_message () = Format.asprintf "%a" PP.statement s in
-  let%bind (code : michelson) =
-    trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
-    | S_environment_extend ->
-        ok @@ Compiler_environment.to_michelson_extend w_env.pre_environment
-    | S_environment_restrict ->
-        Compiler_environment.to_michelson_restrict w_env.pre_environment
-    | S_environment_add _ ->
-        simple_fail "add not ready yet"
-    (* | S_environment_add (name, tv) ->
-     *     Environment.to_michelson_add (name, tv) w_env.pre_environment *)
-    | S_declaration (s, expr) ->
-        let tv = Combinators.Expression.get_type expr in
-        let%bind expr = translate_expression expr in
-        let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
-        ok (seq [
-            i_comment "declaration" ;
-            seq [
-              i_comment "expr" ;
-              i_push_unit ; expr ; i_car ;
-            ] ;
-            seq [
-              i_comment "env <- env . expr" ;
-              add ;
-            ];
-          ])
-    | S_assignment (s, expr) ->
-        let%bind expr = translate_expression expr in
-        let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
-        ok (seq [
-            i_comment "assignment" ;
-            seq [
-              i_comment "expr" ;
-              i_push_unit ; expr ; i_car ;
-            ] ;
-            seq [
-              i_comment "env <- env . expr" ;
-              set ;
-            ];
-          ])
-    | S_cond (expr, a, b) ->
-        let%bind expr = translate_expression expr in
-        let%bind a' = translate_regular_block a in
-        let%bind b' = translate_regular_block b in
-        ok @@ (seq [
-            i_push_unit ;
-            expr ;
-            prim I_CAR ;
-            prim ~children:[seq [a'];seq [b']] I_IF ;
-          ])
-    | S_if_none (expr, none, ((name, tv), some)) ->
-        let%bind expr = translate_expression expr in
-        let%bind none' = translate_regular_block none in
-        let%bind some' = translate_regular_block some in
-        let%bind add =
-          let env' = Environment.extend w_env.pre_environment in
-          Compiler_environment.to_michelson_add (name, tv) env' in
-        ok @@ (seq [
-            i_push_unit ; expr ; i_car ;
-            prim ~children:[
-              seq [none'] ;
-              seq [add ; some'] ;
-            ] I_IF_NONE
-          ])
-    | S_while (expr, block) ->
-        let%bind expr = translate_expression expr in
-        let%bind block' = translate_regular_block block in
-        let%bind restrict_block =
-          let env_while = (snd block).pre_environment in
-          Compiler_environment.to_michelson_restrict env_while in
-        ok @@ (seq [
-            i_push_unit ; expr ; i_car ;
-            prim ~children:[seq [
-                Compiler_environment.to_michelson_extend w_env.pre_environment;
-                block' ;
-                restrict_block ;
-                i_push_unit ; expr ; i_car]] I_LOOP ;
-          ])
-    | S_patch (name, lrs, expr) ->
-        let%bind expr' = translate_expression expr in
-        let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
-        let path = name_path @ lrs in
-        let set_code = Compiler_environment.path_to_michelson_set path in
-        ok @@ seq [
-          i_push_unit ; expr' ; i_car ;
-          set_code ;
-        ]
-  in
-
-  let%bind () =
+  let return code =
     let%bind (Ex_ty pre_ty) = Compiler_environment.to_ty w_env.pre_environment in
     let input_stack_ty = Stack.(pre_ty @: nil) in
     let%bind (Ex_ty post_ty) = Compiler_environment.to_ty w_env.post_environment in
@@ -510,14 +422,130 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
                                    ok (fun () -> error (thunk "error parsing statement code")
                                                  (fun () -> error_message)
                                                  ())) @@
-      Tezos_utils.Memory_proto_alpha.parse_michelson code
+      Tezos_utils.Memory_proto_alpha.parse_michelson_fail code
         input_stack_ty output_stack_ty
     in
-    ok ()
+    ok code
   in
 
-
-  ok code
+  trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
+  | S_environment_extend ->
+      return @@ Compiler_environment.to_michelson_extend w_env.pre_environment
+  | S_environment_restrict ->
+      let%bind code = Compiler_environment.to_michelson_restrict w_env.pre_environment in
+      return code
+  | S_environment_add _ ->
+      simple_fail "add not ready yet"
+  (* | S_environment_add (name, tv) ->
+   *     Environment.to_michelson_add (name, tv) w_env.pre_environment *)
+  | S_declaration (s, expr) ->
+      let tv = Combinators.Expression.get_type expr in
+      let%bind expr = translate_expression expr in
+      let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
+      return @@ seq [
+        i_comment "declaration" ;
+        seq [
+          i_comment "expr" ;
+          i_push_unit ; expr ; i_car ;
+        ] ;
+        seq [
+          i_comment "env <- env . expr" ;
+          add ;
+        ];
+      ]
+  | S_assignment (s, expr) ->
+      let%bind expr = translate_expression expr in
+      let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
+      return @@ seq [
+        i_comment "assignment" ;
+        seq [
+          i_comment "expr" ;
+          i_push_unit ; expr ; i_car ;
+        ] ;
+        seq [
+          i_comment "env <- env . expr" ;
+          set ;
+        ];
+      ]
+  | S_cond (expr, a, b) ->
+      let%bind expr = translate_expression expr in
+      let%bind a' = translate_regular_block a in
+      let%bind b' = translate_regular_block b in
+      return @@ seq [
+        i_push_unit ;
+        expr ;
+        prim I_CAR ;
+        prim ~children:[seq [a'];seq [b']] I_IF ;
+      ]
+  | S_do expr -> (
+      match Combinators.Expression.get_content expr with
+      | E_constant ("FAILWITH" , [ fw ] ) -> (
+          let%bind fw' = translate_expression fw in
+          return @@ seq [
+            i_push_unit ;
+            fw' ;
+            i_car ;
+            i_failwith ;
+          ]
+        )
+      | _ -> (
+          let%bind expr' = translate_expression expr in
+          return @@ seq [
+            i_push_unit ;
+            expr' ;
+            i_drop ;
+          ]
+        )
+    )
+  | S_if_none (expr, none, ((name, tv), some)) ->
+      let%bind expr = translate_expression expr in
+      let%bind none' = translate_regular_block none in
+      let%bind some' = translate_regular_block some in
+      let%bind add =
+        let env' = Environment.extend w_env.pre_environment in
+        Compiler_environment.to_michelson_add (name, tv) env' in
+      return @@ seq [
+        i_push_unit ; expr ; i_car ;
+        prim ~children:[
+          seq [none'] ;
+          seq [add ; some'] ;
+        ] I_IF_NONE
+      ]
+  | S_while (expr, block) ->
+      let%bind expr = translate_expression expr in
+      let%bind block' = translate_regular_block block in
+      let%bind restrict_block =
+        let env_while = (snd block).pre_environment in
+        Compiler_environment.to_michelson_restrict env_while in
+      return @@ seq [
+        i_push_unit ; expr ; i_car ;
+        prim ~children:[seq [
+            Compiler_environment.to_michelson_extend w_env.pre_environment;
+            block' ;
+            restrict_block ;
+            i_push_unit ; expr ; i_car]] I_LOOP ;
+      ]
+  | S_patch (name, lrs, expr) ->
+      let%bind expr' = translate_expression expr in
+      let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
+      let path = name_path @ lrs in
+      let set_code = Compiler_environment.path_to_michelson_set path in
+      let error =
+        let title () = "michelson type-checking patch" in
+        let content () =
+          let aux ppf = function
+            | `Left -> Format.fprintf ppf "left"
+            | `Right -> Format.fprintf ppf "right" in
+          Format.asprintf "Name path: %a\nSub path: %a\n"
+            PP_helpers.(list_sep aux (const " , ")) name_path
+            PP_helpers.(list_sep aux (const " , ")) lrs
+        in
+        error title content in
+      trace error @@
+      return @@ seq [
+        i_push_unit ; expr' ; i_car ;
+        set_code ;
+      ]
 
 and translate_regular_block ((b, env):block) : michelson result =
   let aux prev statement =
diff --git a/src/ligo/compiler/compiler_type.ml b/src/ligo/compiler/compiler_type.ml
index cc2726a38..294253085 100644
--- a/src/ligo/compiler/compiler_type.ml
+++ b/src/ligo/compiler/compiler_type.ml
@@ -18,8 +18,10 @@ module Ty = struct
     | Base_unit -> fail (not_comparable "unit")
     | Base_bool -> fail (not_comparable "bool")
     | Base_nat -> return nat_k
+    | Base_tez -> return tez_k
     | Base_int -> return int_k
     | Base_string -> return string_k
+    | Base_address -> return address_k
     | Base_bytes -> return bytes_k
     | Base_operation -> fail (not_comparable "operation")
 
@@ -43,7 +45,9 @@ module Ty = struct
     | Base_bool -> return bool
     | Base_int -> return int
     | Base_nat -> return nat
+    | Base_tez -> return tez
     | Base_string -> return string
+    | Base_address -> return address
     | Base_bytes -> return bytes
     | Base_operation -> return operation
 
@@ -113,7 +117,9 @@ let base_type : type_base -> O.michelson result =
   | Base_bool -> ok @@ O.prim T_bool
   | Base_int -> ok @@ O.prim T_int
   | Base_nat -> ok @@ O.prim T_nat
+  | Base_tez -> ok @@ O.prim T_mutez
   | Base_string -> ok @@ O.prim T_string
+  | Base_address -> ok @@ O.prim T_address
   | Base_bytes -> ok @@ O.prim T_bytes
   | Base_operation -> ok @@ O.prim T_operation
 
diff --git a/src/ligo/compiler/uncompiler.ml b/src/ligo/compiler/uncompiler.ml
index ce811b67b..cd3d32c21 100644
--- a/src/ligo/compiler/uncompiler.ml
+++ b/src/ligo/compiler/uncompiler.ml
@@ -29,10 +29,17 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
         trace_option (simple_error "too big to fit an int") @@
         Alpha_context.Script_int.to_int n in
       ok @@ D_nat n
+  | (Mutez_t _), n ->
+      let%bind n =
+        generic_try (simple_error "too big to fit an int") @@
+        (fun () -> Int64.to_int @@ Alpha_context.Tez.to_mutez n) in
+      ok @@ D_nat n
   | (Bool_t _), b ->
       ok @@ D_bool b
   | (String_t _), s ->
       ok @@ D_string s
+  | (Address_t _), s ->
+      ok @@ D_string (Alpha_context.Contract.to_b58check s)
   | (Unit_t _), () ->
       ok @@ D_unit
   | (Option_t _), None ->
diff --git a/src/ligo/contracts/coase.ligo b/src/ligo/contracts/coase.ligo
index 56f1ee4ce..0a381adaf 100644
--- a/src/ligo/contracts/coase.ligo
+++ b/src/ligo/contracts/coase.ligo
@@ -4,7 +4,6 @@ type card_pattern_id is nat
 type card_pattern is record [
   coefficient : tez ;
   quantity : nat ;
-  last_id : nat ;
 ]
 
 type card_patterns is map(card_pattern_id , card_pattern)
@@ -18,6 +17,7 @@ type cards is map(card_id , card)
 type storage_type is record [
   cards : cards ;
   card_patterns : card_patterns ;
+  next_id : nat ;
 ]
 
 type action_buy_single is record [
@@ -38,14 +38,24 @@ type action is
 
 function buy_single(const action : action_buy_single ; const s : storage_type) : (list(operation) * storage_type) is
   begin
-    const pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
+    // Check funds
+    const card_pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
     const price : tez = card_pattern.coefficient * (card_pattern.quantity + 1n) ;
     if (price > amount) then fail "Not enough money" else skip ;
+    // Administrative procedure
     const operations : list(operation) = nil ;
-    pattern.quantity := pattern.quantity + 1n ;
+    // Increase quantity
+    card_pattern.quantity := card_pattern.quantity + 1n ;
     const card_patterns : card_patterns = s.card_patterns ;
-    card_patterns[action.card_to_buy] := pattern ;
+    card_patterns[action.card_to_buy] := card_pattern ;
     s.card_patterns := card_patterns ;
+    // Add card
+    const cards : cards = s.cards ;
+    cards[s.next_id] := record
+      card_owner = source ;
+    end ;
+    s.cards := cards ;
+    s.next_id := s.next_id + 1n ;
   end with (operations , s)
 
 function main(const action : action ; const s : storage_type) : (list(operation) * storage_type) is
diff --git a/src/ligo/contracts/record.ligo b/src/ligo/contracts/record.ligo
index 69ef05bb4..e0fbb5d04 100644
--- a/src/ligo/contracts/record.ligo
+++ b/src/ligo/contracts/record.ligo
@@ -8,11 +8,37 @@ const fb : foobar = record
   bar = 0 ;
 end
 
+type abc is record
+  a : int ;
+  b : int ;
+  c : int ;
+end
+
+const abc : abc = record
+  a = 42 ;
+  b = 142 ;
+  c = 242 ;
+end
+
+const a : int = abc.a ;
+const b : int = abc.b ;
+const c : int = abc.c ;
+
 function projection (const r : foobar) : int is
   begin
     skip
   end with r.foo + r.bar
 
+function modify (const r : foobar) : foobar is
+  block {
+    r.foo := 256 ;
+  } with r
+
+function modify_abc (const r : abc) : abc is
+  block {
+    r.b := 2048 ;
+  } with r
+
 type big_record is record
      a : int ;
      b : int ;
diff --git a/src/ligo/contracts/tuple.ligo b/src/ligo/contracts/tuple.ligo
index 6b190f4c0..aebdc7b87 100644
--- a/src/ligo/contracts/tuple.ligo
+++ b/src/ligo/contracts/tuple.ligo
@@ -10,3 +10,13 @@ function projection (const tpl : foobar) : int is
 type big_tuple is (int * int * int * int * int)
 
 const br : big_tuple = (23, 23, 23, 23, 23)
+
+type abc is (int * int * int)
+
+function projection_abc (const tpl : abc) : int is
+  block { skip } with tpl.1
+
+function modify_abc (const tpl : abc) : abc is
+  block {
+    tpl.1 := 2048 ;
+  } with tpl
diff --git a/src/ligo/main/main.ml b/src/ligo/main/main.ml
index ec6f4bf3a..7c2b839b7 100644
--- a/src/ligo/main/main.ml
+++ b/src/ligo/main/main.ml
@@ -87,8 +87,17 @@ let easy_evaluate_typed_simplified (entry:string) (program:AST_Typed.program) :
 let easy_evaluate_typed = trace_f_2_ez easy_evaluate_typed (thunk "easy evaluate typed")
 
 let easy_run_typed
-    ?(debug_mini_c = false) (entry:string)
+    ?(debug_mini_c = false) ?amount (entry:string)
     (program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
+  let%bind () =
+    let open Ast_typed in
+    let%bind (Declaration_constant (d , _)) = get_declaration_by_name program entry in
+    let%bind (arg_ty , _) =
+      trace_strong (simple_error "entry-point doesn't have a function type") @@
+      get_t_function @@ get_type_annotation d.annotated_expression in
+    Ast_typed.assert_type_value_eq (arg_ty , (Ast_typed.get_type_annotation input))
+  in
+
   let%bind mini_c_main =
     trace (simple_error "transpile mini_c entry") @@
     transpile_entry program entry in
@@ -106,7 +115,7 @@ let easy_run_typed
       in
       error title content in
     trace error @@
-    Run_mini_c.run_entry mini_c_main mini_c_value in
+    Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
   let%bind typed_result =
     let%bind main_result_type =
       let%bind typed_main = Ast_typed.get_functional_entry program entry in
@@ -117,7 +126,7 @@ let easy_run_typed
   ok typed_result
 
 let easy_run_typed_simplified
-    ?(debug_mini_c = false) (entry:string)
+    ?(debug_mini_c = false) ?amount (entry:string)
     (program:AST_Typed.program) (input:Ast_simplified.annotated_expression) : Ast_simplified.annotated_expression result =
   let%bind mini_c_main =
     trace (simple_error "transpile mini_c entry") @@
@@ -143,7 +152,7 @@ let easy_run_typed_simplified
       in
       error title content in
     trace error @@
-    Run_mini_c.run_entry mini_c_main mini_c_value in
+    Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
   let%bind typed_result =
     let%bind main_result_type =
       let%bind typed_main = Ast_typed.get_functional_entry program entry in
diff --git a/src/ligo/main/run_mini_c.ml b/src/ligo/main/run_mini_c.ml
index 9919b73b4..3947a0e0e 100644
--- a/src/ligo/main/run_mini_c.ml
+++ b/src/ligo/main/run_mini_c.ml
@@ -3,7 +3,7 @@ open Mini_c
 open Compiler.Program
 open Memory_proto_alpha.Script_ir_translator
 
-let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
+let run_aux ?amount (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
   let Compiler.Program.{input;output;body} : compiled_program = program in
   let (Ex_ty input_ty) = input in
   let (Ex_ty output_ty) = output in
@@ -18,7 +18,7 @@ let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_
   let open! Memory_proto_alpha.Script_interpreter in
   let%bind (Item(output, Empty)) =
     Trace.trace_tzresult_lwt (simple_error "error of execution") @@
-    Tezos_utils.Memory_proto_alpha.interpret descr (Item(input, Empty)) in
+    Tezos_utils.Memory_proto_alpha.interpret ?amount descr (Item(input, Empty)) in
   ok (Ex_typed_value (output_ty, output))
 
 let run_node (program:program) (input:Michelson.t) : Michelson.t result =
@@ -29,7 +29,7 @@ let run_node (program:program) (input:Michelson.t) : Michelson.t result =
     Tezos_utils.Memory_proto_alpha.unparse_michelson_data output_ty output in
   ok output
 
-let run_entry (entry:anon_function) (input:value) : value result =
+let run_entry ?amount (entry:anon_function) (input:value) : value result =
   let%bind compiled =
     let error =
       let title () = "compile entry" in
@@ -40,7 +40,7 @@ let run_entry (entry:anon_function) (input:value) : value result =
     trace error @@
     translate_entry entry in
   let%bind input_michelson = translate_value input in
-  let%bind ex_ty_value = run_aux compiled input_michelson in
+  let%bind ex_ty_value = run_aux ?amount compiled input_michelson in
   let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in
   ok result
 
diff --git a/src/ligo/meta_michelson/contract.ml b/src/ligo/meta_michelson/contract.ml
index b2df55022..8ec3bc02e 100644
--- a/src/ligo/meta_michelson/contract.ml
+++ b/src/ligo/meta_michelson/contract.ml
@@ -245,8 +245,10 @@ module Types = struct
   let bytes_k = Bytes_key None
 
   let nat = Nat_t None
+  let tez = Mutez_t None
   let int = Int_t None
   let nat_k = Nat_key None
+  let tez_k = Mutez_key None
   let int_k = Int_key None
 
   let big_map k v = Big_map_t (k, v, None)
@@ -260,6 +262,7 @@ module Types = struct
 
   let string = String_t None
   let string_k = String_key None
+  let address_k = Address_key None
 
   let key = Key_t None
 
diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml
index 410a228e4..c20198de2 100644
--- a/src/ligo/mini_c/PP.ml
+++ b/src/ligo/mini_c/PP.ml
@@ -6,12 +6,17 @@ let list_sep_d x = list_sep x (const " , ")
 
 let space_sep ppf () = fprintf ppf " "
 
+let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R"
+
+
 let type_base ppf : type_base -> _ = function
   | Base_unit -> fprintf ppf "unit"
   | Base_bool -> fprintf ppf "bool"
   | Base_int -> fprintf ppf "int"
   | Base_nat -> fprintf ppf "nat"
+  | Base_tez -> fprintf ppf "tez"
   | Base_string -> fprintf ppf "string"
+  | Base_address -> fprintf ppf "address"
   | Base_bytes -> fprintf ppf "bytes"
   | Base_operation -> fprintf ppf "operation"
 
@@ -109,10 +114,10 @@ and statement ppf ((s, _) : statement) = match s with
   | S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv
   | S_declaration ass -> declaration ppf ass
   | S_assignment ass -> assignment ppf ass
+  | S_do e -> fprintf ppf "do %a" expression e
   | S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
   | S_patch (r, path, e) ->
-      let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in
-      fprintf ppf "%s%a := %a" r (list aux) path expression e
+      fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
   | S_if_none (expr, none, ((name, _), some)) -> fprintf ppf "if_none (%a) %a %s->%a" expression expr block none name block some
   | S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b
 
diff --git a/src/ligo/mini_c/combinators_smart.ml b/src/ligo/mini_c/combinators_smart.ml
index 5733089cf..a95e12149 100644
--- a/src/ligo/mini_c/combinators_smart.ml
+++ b/src/ligo/mini_c/combinators_smart.ml
@@ -12,6 +12,7 @@ let statement s' env : statement =
   | S_environment_restrict -> s', environment_wrap env (Environment.restrict env)
   | S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env)
   | S_cond _ -> s' , id_environment_wrap env
+  | S_do _ -> s' , id_environment_wrap env
   | S_if_none _ -> s' , id_environment_wrap env
   | S_while _ -> s' , id_environment_wrap env
   | S_patch _ -> s' , id_environment_wrap env
diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml
index 7a443742e..172e2d7d2 100644
--- a/src/ligo/mini_c/types.ml
+++ b/src/ligo/mini_c/types.ml
@@ -5,8 +5,8 @@ type type_name = string
 type type_base =
   | Base_unit
   | Base_bool
-  | Base_int | Base_nat
-  | Base_string | Base_bytes
+  | Base_int | Base_nat | Base_tez
+  | Base_string | Base_bytes | Base_address
   | Base_operation
 
 type type_value =
@@ -84,6 +84,7 @@ and statement' =
   | S_environment_add of (var_name * type_value)
   | S_declaration of assignment (* First assignment *)
   | S_assignment of assignment
+  | S_do of expression
   | S_cond of expression * block * block
   | S_patch of string * [`Left | `Right] list * expression
   | S_if_none of expression * block * ((var_name * type_value) * block)
diff --git a/src/ligo/operators/operators.ml b/src/ligo/operators/operators.ml
index f756ce5ae..61afb2e2e 100644
--- a/src/ligo/operators/operators.ml
+++ b/src/ligo/operators/operators.ml
@@ -24,6 +24,9 @@ module Simplify = struct
     ("get_force" , 2) ;
     ("size" , 1) ;
     ("int" , 1) ;
+    ("amount" , 0) ;
+    ("unit" , 0) ;
+    ("source" , 0) ;
   ]
 
   module Camligo = struct
@@ -132,7 +135,10 @@ module Typer = struct
   let comparator : string -> typer = fun s -> s , 2 , [
       (eq_2 (t_int ()), constant_2 s (t_bool ())) ;
       (eq_2 (t_nat ()), constant_2 s (t_bool ())) ;
+      (eq_2 (t_tez ()), constant_2 s (t_bool ())) ;
       (eq_2 (t_bytes ()), constant_2 s (t_bool ())) ;
+      (eq_2 (t_string ()), constant_2 s (t_bool ())) ;
+      (eq_2 (t_address ()), constant_2 s (t_bool ())) ;
     ]
 
   let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ())
@@ -211,6 +217,10 @@ module Typer = struct
       predicate_0 , typer_constant ("UNIT", t_unit ())
     ]
 
+  let amount = "amount" , 0 , [
+      predicate_0 , typer_constant ("AMOUNT", t_tez ())
+    ]
+
   let transaction = "Operation.transaction" , 3 , [
       true_3 , typer'_3 (
         fun param contract amount ->
@@ -236,12 +246,6 @@ module Typer = struct
       )
     ]
 
-  (* let record_assign = "RECORD_ASSIGN" , 2 , [
-   *     true_2 , typer'_2 (fun path new_value ->
-   *         let%bind (a , b) = get_a_record_accessor path in
-   *       )
-   *   ] *)
-
   let num_2 : typer_predicate =
     let aux = fun a b ->
       (type_value_eq (a , t_int ()) || type_value_eq (a , t_nat ())) &&
@@ -252,6 +256,17 @@ module Typer = struct
       num_2 , constant_2 "MOD" (t_nat ()) ;
     ]
 
+  let times = "TIMES" , 2 , [
+      (eq_2 (t_nat ()) , constant_2 "TIMES_NAT" (t_nat ())) ;
+      (num_2 , constant_2 "TIMES_INT" (t_int ())) ;
+      (
+        let aux a b =
+          (type_value_eq (a , t_nat ()) && type_value_eq (b , t_tez ())) ||
+          (type_value_eq (b , t_nat ()) && type_value_eq (a , t_tez ())) in
+       predicate_2 aux , constant_2 "TIMES_TEZ" (t_tez ())
+     ) ;
+    ]
+
   let constant_typers =
     let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
     Map.String.of_list
@@ -261,10 +276,7 @@ module Typer = struct
         ("ADD_NAT" , t_nat ()) ;
         ("CONCAT" , t_string ()) ;
       ] ;
-      same_2 "TIMES" [
-        ("TIMES_INT" , t_int ()) ;
-        ("TIMES_NAT" , t_nat ()) ;
-      ] ;
+      times ;
       same_2 "DIV" [
         ("DIV_INT" , t_int ()) ;
         ("DIV_NAT" , t_nat ()) ;
@@ -292,6 +304,7 @@ module Typer = struct
       sender ;
       source ;
       unit ;
+      amount ;
       transaction ;
       get_contract ;
     ]
@@ -324,6 +337,7 @@ module Compiler = struct
     ("SUB_NAT" , simple_binary @@ prim I_SUB) ;
     ("TIMES_INT" , simple_binary @@ prim I_MUL) ;
     ("TIMES_NAT" , simple_binary @@ prim I_MUL) ;
+    ("TIMES_TEZ" , simple_binary @@ prim I_MUL) ;
     ("DIV_INT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
     ("DIV_NAT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
     ("MOD" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr]) ;
@@ -344,8 +358,14 @@ module Compiler = struct
     ("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
     ("GET" , simple_binary @@ prim I_GET) ;
     ("SIZE" , simple_unary @@ prim I_SIZE) ;
+    ("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
+    ("ASSERT" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
     ("INT" , simple_unary @@ prim I_INT) ;
     ("CONS" , simple_binary @@ prim I_CONS) ;
+    ("UNIT" , simple_constant @@ prim I_UNIT) ;
+    ("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
+    ("SOURCE" , simple_constant @@ prim I_SOURCE) ;
+    ("SENDER" , simple_constant @@ prim I_SENDER) ;
     ( "MAP_UPDATE" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
   ]
 
diff --git a/src/ligo/simplify/pascaligo.ml b/src/ligo/simplify/pascaligo.ml
index 20f017751..c4a0684ca 100644
--- a/src/ligo/simplify/pascaligo.ml
+++ b/src/ligo/simplify/pascaligo.ml
@@ -90,14 +90,16 @@ let rec simpl_expression (t:Raw.expr) : ae result =
         | Component index -> Access_tuple (Z.to_int (snd index.value))
       in
       List.map aux @@ npseq_to_list path in
-
     ok @@ make_e_a @@ E_accessor (var, path')
   in
   match t with
-  | EVar c ->
-      if c.value = "unit"
-      then ok @@ make_e_a @@ E_literal Literal_unit
-      else ok @@ make_e_a @@ E_variable c.value
+  | EVar c -> (
+      let c' = c.value in
+      match List.assoc_opt c' constants with
+      | None -> return @@ E_variable c.value
+      | Some 0 -> return @@ E_constant (c' , [])
+      | Some _ -> simple_fail "non nullary constant without parameters"
+    )
   | ECall x -> (
       let (name, args) = x.value in
       let f = name.value in
@@ -426,12 +428,18 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
         | NoneExpr _ -> simple_fail "no none assignments yet"
       in
       match a.lhs with
-        | Path (Name name) -> (
-            ok @@ I_assignment {name = name.value ; annotated_expression = value_expr}
-          )
         | Path path -> (
-            let err_content () = Format.asprintf "%a" (PP_helpers.printer Parser.Pascaligo.ParserLog.print_path) path in
-            fail @@ (fun () -> error (thunk "no path assignments") err_content ())
+            let (name , path') = simpl_path path in
+            match List.rev_uncons_opt path' with
+            | None -> (
+                ok @@ I_assignment {name ; annotated_expression = value_expr}
+              )
+            | Some (hds , last) -> (
+                match last with
+                | Access_record property -> ok @@ I_record_patch (name , hds , [(property , value_expr)])
+                | Access_tuple index -> ok @@ I_tuple_patch (name , hds , [(index , value_expr)])
+                | _ -> simple_fail "no map assignment in this weird case yet"
+              )
           )
         | MapPath v -> (
             let v' = v.value in
diff --git a/src/ligo/test/coase_tests.ml b/src/ligo/test/coase_tests.ml
index 7e02496b4..36dc4db49 100644
--- a/src/ligo/test/coase_tests.ml
+++ b/src/ligo/test/coase_tests.ml
@@ -14,49 +14,114 @@ let get_program =
         ok program
       )
 
-let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) =
-  let open AST_Typed.Combinators in
-  let content =
-    let aux = fun (x, y) -> e_a_empty_nat x, y in
-    List.map aux content in
-  let value_type = match value_type, content with
-    | None, hd :: _ -> (snd hd).type_annotation
-    | Some s, _ -> s
-    | _ -> raise (Failure "no value type and heap empty when building heap") in
-  e_a_empty_map content (t_nat ()) value_type
+open Ast_simplified
 
-let ez lst =
-  let open AST_Typed.Combinators in
-  let value_type = t_pair
-      (t_int ())
-      (t_string ())
-      ()
-  in
-  let lst' =
-    let aux (i, (j, s)) =
-      (i, e_a_empty_pair (e_a_empty_int j) (e_a_empty_string s)) in
-    List.map aux lst in
-  a_heap_ez ~value_type lst'
+let card owner =
+  ez_e_a_record [
+    ("card_owner" , owner) ;
+  ]
 
-let dummy n =
-  ez List.(
-    map (fun n -> (n, (n, string_of_int n)))
-    @@ tl
-    @@ range (n + 1)
-  )
+let card_ty = t_record_ez [
+    ("card_owner" , t_address) ;
+  ]
+
+let card_ez owner = card (e_a_address owner)
+
+let make_cards assoc_lst =
+  let card_id_ty = t_nat in
+  e_a_map assoc_lst card_id_ty card_ty
+
+let card_pattern (coeff , qtt) =
+  ez_e_a_record [
+    ("coefficient" , coeff) ;
+    ("quantity" , qtt) ;
+  ]
+
+let card_pattern_ty =
+  t_record_ez [
+    ("coefficient" , t_tez) ;
+    ("quantity" , t_nat) ;
+  ]
+
+let card_pattern_ez (coeff , qtt) =
+  card_pattern (e_a_tez coeff , e_a_nat qtt)
+
+let make_card_patterns lst =
+  let card_pattern_id_ty = t_nat  in
+  let assoc_lst = List.mapi (fun i x -> (e_a_nat i , x)) lst in
+  e_a_map assoc_lst card_pattern_id_ty card_pattern_ty
+
+let storage cards_patterns cards next_id =
+  ez_e_a_record [
+    ("cards" , cards) ;
+    ("card_patterns" , cards_patterns) ;
+    ("next_id" , next_id) ;
+  ]
+
+let storage_ez cps cs next_id =
+  storage (make_card_patterns cps) (make_cards cs) (e_a_nat next_id)
+
+let cards_ez owner n =
+  List.mapi (fun i x -> (e_a_nat i , x))
+  @@ List.map card_ez
+  @@ List.map (Function.constant owner)
+  @@ List.range n
+
+let first_owner =
+  let open Tezos_utils.Memory_proto_alpha in
+  let id = List.nth dummy_environment.identities 0 in
+  let kt = id.implicit_contract in
+  Alpha_context.Contract.to_b58check kt
+
+let second_owner =
+  let open Tezos_utils.Memory_proto_alpha in
+  let id = List.nth dummy_environment.identities 1 in
+  let kt = id.implicit_contract in
+  Alpha_context.Contract.to_b58check kt
+
+let basic a b cards next_id =
+  let card_patterns = List.map card_pattern_ez [
+    (100 , a) ;
+    (20 , b) ;
+  ] in
+  storage_ez card_patterns cards next_id
 
 let buy () =
   let%bind program = get_program () in
-  let aux n =
-    let open AST_Typed.Combinators in
-    let input = dummy n in
-    let%bind result = easy_run_typed "is_empty" program input in
-    let expected = e_a_empty_bool (n = 0) in
-    AST_Typed.assert_value_eq (expected, result)
+  let%bind () =
+    let make_input = fun n ->
+      let buy_action = ez_e_a_record [
+          ("card_to_buy" , e_a_nat 0) ;
+        ] in
+      let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
+      e_a_pair buy_action storage
+    in
+    let make_expected = fun n ->
+      let ops = e_a_list [] t_operation in
+      let storage =
+        let cards =
+          cards_ez first_owner n @
+          [(e_a_nat (2 * n) , card (e_a_address second_owner))]
+        in
+        basic 101 1000 cards ((2 * n) + 1) in
+      e_a_pair ops storage
+    in
+    let%bind () =
+      let%bind amount =
+        trace_option (simple_error "getting amount for run") @@
+        Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 10000000000 in
+      let options = make_options ~amount () in
+      expect_n_pos_small ~options program "buy_single" make_input make_expected in
+    let%bind () =
+      let%bind amount =
+        trace_option (simple_error "getting amount for run") @@
+        Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 0 in
+      let options = make_options ~amount () in
+      trace_strong (simple_error "could buy without money") @@
+      Assert.assert_fail
+      @@ expect_n_pos_small ~options program "buy_single" make_input make_expected in
+    ok ()
   in
-  let%bind _ = bind_list
-    @@ List.map aux
-    @@ [0 ; 2 ; 7 ; 12] in
   ok ()
 
 let main = "Coase (End to End)", [
diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml
index e73e084da..c32055762 100644
--- a/src/ligo/test/integration_tests.ml
+++ b/src/ligo/test/integration_tests.ml
@@ -140,11 +140,31 @@ let record () : unit result  =
     let expected = record_ez_int ["foo" ; "bar"] 0 in
     expect_evaluate program "fb" expected
   in
+  let%bind () =
+    let%bind () = expect_evaluate program "a" (e_a_int 42) in
+    let%bind () = expect_evaluate program "b" (e_a_int 142) in
+    let%bind () = expect_evaluate program "c" (e_a_int 242) in
+    ok ()
+  in
   let%bind () =
     let make_input = record_ez_int ["foo" ; "bar"] in
     let make_expected = fun n -> e_a_int (2 * n) in
     expect_n program "projection" make_input make_expected
   in
+  let%bind () =
+    let make_input = record_ez_int ["foo" ; "bar"] in
+    let make_expected = fun n -> ez_e_a_record [("foo" , e_a_int 256) ; ("bar" , e_a_int n) ] in
+    expect_n program "modify" make_input make_expected
+  in
+  let%bind () =
+    let make_input = record_ez_int ["a" ; "b" ; "c"] in
+    let make_expected = fun n -> ez_e_a_record [
+        ("a" , e_a_int n) ;
+        ("b" , e_a_int 2048) ;
+        ("c" , e_a_int n)
+      ] in
+    expect_n program "modify_abc" make_input make_expected
+  in
   let%bind () =
     let expected = record_ez_int ["a";"b";"c";"d";"e"] 23 in
     expect_evaluate program "br" expected
@@ -164,6 +184,21 @@ let tuple () : unit result  =
     let make_expected = fun n -> e_a_int (2 * n) in
     expect_n program "projection" make_input make_expected
   in
+  let%bind () =
+    let make_input = fun n -> ez [n ; 2 * n ; n] in
+    let make_expected = fun n -> e_a_int (2 * n) in
+    expect_n program "projection_abc" make_input make_expected
+  in
+  let%bind () =
+    let make_input = fun n -> ez [n ; n ; n] in
+    let make_expected = fun n -> ez [n ; 2048 ; n] in
+    expect program "modify_abc" (make_input 12) (make_expected 12)
+  in
+  let%bind () =
+    let make_input = fun n -> ez [n ; n ; n] in
+    let make_expected = fun n -> ez [n ; 2048 ; n] in
+    expect_n program "modify_abc" make_input make_expected
+  in
   let%bind () =
     let expected = ez [23 ; 23 ; 23 ; 23 ; 23] in
     expect_evaluate program "br" expected
@@ -372,6 +407,8 @@ let main = "Integration (End to End)", [
     test "complex function" complex_function ;
     test "variant" variant ;
     test "variant matching" variant_matching ;
+    test "tuple" tuple ;
+    test "record" record ;
     test "closure" closure ;
     test "shared function" shared_function ;
     test "shadow" shadow ;
@@ -379,8 +416,6 @@ let main = "Integration (End to End)", [
     test "bool" bool_expression ;
     test "arithmetic" arithmetic ;
     test "unit" unit_expression ;
-    test "record" record ;
-    test "tuple" tuple ;
     test "option" option ;
     test "map" map ;
     test "list" list ;
diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml
index 3dbd250cb..2cb1ec87d 100644
--- a/src/ligo/test/test.ml
+++ b/src/ligo/test/test.ml
@@ -9,6 +9,6 @@ let () =
     Transpiler_tests.main ;
     Typer_tests.main ;
     Heap_tests.main ;
-    (* Coase_tests.main ; *)
+    Coase_tests.main ;
   ] ;
   ()
diff --git a/src/ligo/test/test_helpers.ml b/src/ligo/test/test_helpers.ml
index 73ca16e7a..6754d1e78 100644
--- a/src/ligo/test/test_helpers.ml
+++ b/src/ligo/test/test_helpers.ml
@@ -13,14 +13,22 @@ let test name f =
 
 open Ast_simplified.Combinators
 
-let expect program entry_point input expected =
+type options = {
+  amount : Memory_proto_alpha.Alpha_context.Tez.t option ;
+}
+
+let make_options ?amount () = {
+  amount ;
+}
+
+let expect ?(options = make_options ()) program entry_point input expected =
   let%bind result =
     let run_error =
       let title () = "expect run" in
       let content () = Format.asprintf "Entry_point: %s" entry_point in
       error title content in
     trace run_error @@
-    Ligo.easy_run_typed_simplified entry_point program input in
+    Ligo.easy_run_typed_simplified ?amount:options.amount entry_point program input in
   let expect_error =
     let title () = "expect result" in
     let content () = Format.asprintf "Expected %a, got %a"
@@ -39,22 +47,22 @@ let expect_evaluate program entry_point expected =
   let%bind result = Ligo.easy_evaluate_typed_simplified entry_point program in
   Ast_simplified.assert_value_eq (expected , result)
 
-let expect_n_aux lst program entry_point make_input make_expected =
+let expect_n_aux ?options lst program entry_point make_input make_expected =
   let aux n =
     let input = make_input n in
     let expected = make_expected n in
     trace (simple_error ("expect_n " ^ (string_of_int n))) @@
-    let result = expect program entry_point input expected in
+    let result = expect ?options program entry_point input expected in
     result
   in
   let%bind _ = bind_map_list aux lst in
   ok ()
 
-let expect_n = expect_n_aux [0 ; 2 ; 42 ; 163 ; -1]
-let expect_n_pos = expect_n_aux [0 ; 2 ; 42 ; 163]
-let expect_n_strict_pos = expect_n_aux [2 ; 42 ; 163]
-let expect_n_pos_small = expect_n_aux [0 ; 2 ; 10]
-let expect_n_strict_pos_small = expect_n_aux [2 ; 10]
+let expect_n ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163 ; -1]
+let expect_n_pos ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163]
+let expect_n_strict_pos ?options = expect_n_aux ?options [2 ; 42 ; 163]
+let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
+let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]
 let expect_n_pos_mid = expect_n_aux [0 ; 2 ; 10 ; 33]
 
 let expect_b program entry_point make_expected =
diff --git a/src/ligo/transpiler/transpiler.ml b/src/ligo/transpiler/transpiler.ml
index c6f6e43e8..5e9d31a02 100644
--- a/src/ligo/transpiler/transpiler.ml
+++ b/src/ligo/transpiler/transpiler.ml
@@ -19,7 +19,9 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("bool", []) -> ok (T_base Base_bool)
   | T_constant ("int", []) -> ok (T_base Base_int)
   | T_constant ("nat", []) -> ok (T_base Base_nat)
+  | T_constant ("tez", []) -> ok (T_base Base_tez)
   | T_constant ("string", []) -> ok (T_base Base_string)
+  | T_constant ("address", []) -> ok (T_base Base_address)
   | T_constant ("unit", []) -> ok (T_base Base_unit)
   | T_constant ("operation", []) -> ok (T_base Base_operation)
   | T_constant ("map", [key;value]) ->
@@ -31,7 +33,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("option", [o]) ->
       let%bind o' = translate_type o in
       ok (T_option o')
-  | T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized constant") (fun () -> name) ())
+  | T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized type constant") (fun () -> name) ())
   | T_sum m ->
       let node = Append_tree.of_list @@ list_of_map m in
       let aux a b : type_value result =
@@ -69,37 +71,43 @@ let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [
     Append_tree.exists_path aux node_tv in
   let lr_path = List.map (fun b -> if b then `Right else `Left) path in
   let%bind (_ , lst) =
-    let aux = fun (ty , acc) cur ->
-      let%bind (a , b) = Mini_c.get_t_pair ty in
+    let aux = fun (ty' , acc) cur ->
+      let%bind (a , b) =
+        let error =
+          let title () = "expected a pair" in
+          let content () = Format.asprintf "Big: %a.\tGot: %a\tFull path: %a\tSmall path: %a"
+              Mini_c.PP.type_ ty
+              Mini_c.PP.type_ ty'
+              PP_helpers.(list_sep bool (const ".")) path
+              PP_helpers.(list_sep lr (const ".")) (List.map snd acc)
+          in
+          error title content
+        in
+        trace_strong error @@
+        Mini_c.get_t_pair ty' in
       match cur with
-      | `Left -> ok (a , (a , `Left) :: acc)
-      | `Right -> ok (b , (b , `Right) :: acc) in
+      | `Left -> ok (a , acc @ [(a , `Left)])
+      | `Right -> ok (b , acc @ [(b , `Right)])
+    in
     bind_fold_list aux (ty , []) lr_path in
   ok lst
 
-let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tym ind ->
+let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * [`Left | `Right]) list result = fun ty tym ind ->
   let tys = kv_list_of_map tym in
   let node_tv = Append_tree.of_list tys in
-  let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result =
-    if i = ind then (
-      ok (ty, [])
-    ) else (
-      simple_fail "bad leaf"
-    ) in
-  let node a b : (type_value * (type_value * [`Left | `Right]) list) result =
-    match%bind bind_lr (a, b) with
-    | `Left (t, acc) ->
-        let%bind (a, _) = Mini_c.get_t_pair t in
-        ok @@ (t, (a, `Left) :: acc)
-    | `Right (t, acc) -> (
-        let%bind (_, b) = Mini_c.get_t_pair t in
-        ok @@ (t, (b, `Right) :: acc)
-      ) in
-  let error_content () =
-    let aux ppf (name, ty) = Format.fprintf ppf "%s -> %a" name PP.type_ ty in
-    Format.asprintf "(%a).%s" (PP.list_sep_d aux) tys ind in
-  trace_strong (fun () -> error (thunk "bad index in record (shouldn't happen here)") error_content ()) @@
-  Append_tree.fold_ne leaf node node_tv
+  let%bind path =
+    let aux (i , _) = i = ind in
+    trace_option (simple_error "no leaf with given index") @@
+    Append_tree.exists_path aux node_tv in
+  let lr_path = List.map (fun b -> if b then `Right else `Left) path in
+  let%bind (_ , lst) =
+    let aux = fun (ty , acc) cur ->
+      let%bind (a , b) = Mini_c.get_t_pair ty in
+      match cur with
+      | `Left -> ok (a , acc @ [(a , `Left)])
+      | `Right -> ok (b , acc @ [(b , `Right)] ) in
+    bind_fold_list aux (ty , []) lr_path in
+  ok lst
 
 let rec translate_block env (b:AST.block) : block result =
   let aux = fun (precs, env) instruction ->
@@ -124,21 +132,30 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
       let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result =
         fun (prev, acc) cur ->
           let%bind ty' = translate_type prev in
-        match cur with
-        | Access_tuple ind ->
-            let%bind ty_lst = AST.Combinators.get_t_tuple prev in
-            let%bind ty'_lst = bind_map_list translate_type ty_lst in
-            let%bind path = tuple_access_to_lr ty' ty'_lst ind in
-            let path' = List.map snd path in
-            ok (List.nth ty_lst ind, path' @ acc)
-        | Access_record prop ->
-            let%bind ty_map = AST.Combinators.get_t_record prev in
-            let%bind ty'_map = bind_map_smap translate_type ty_map in
-            let%bind (_, path) = record_access_to_lr ty' ty'_map prop in
-            let path' = List.map snd path in
-            ok (Map.String.find prop ty_map, path' @ acc)
+          match cur with
+          | Access_tuple ind ->
+              let%bind ty_lst = AST.Combinators.get_t_tuple prev in
+              let%bind ty'_lst = bind_map_list translate_type ty_lst in
+              let%bind path = tuple_access_to_lr ty' ty'_lst ind in
+              let path' = List.map snd path in
+              ok (List.nth ty_lst ind, acc @ path')
+          | Access_record prop ->
+              let%bind ty_map =
+                let error =
+                  let title () = "accessing property on not a record" in
+                  let content () = Format.asprintf "%s on %a in %a"
+                    prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in
+                  error title content
+                in
+                trace error @@
+                AST.Combinators.get_t_record prev in
+              let%bind ty'_map = bind_map_smap translate_type ty_map in
+              let%bind path = record_access_to_lr ty' ty'_map prop in
+              let path' = List.map snd path in
+              ok (Map.String.find prop ty_map, acc @ path')
+          | Access_map _k -> simple_fail "no patch for map yet"
       in
-      let%bind (_, path) = bind_fold_list aux (ty, []) s in
+      let%bind (_, path) = bind_fold_right_list aux (ty, []) s in
       let%bind v' = translate_annotated_expression env v in
       return (S_patch (r.type_name, path, v'))
     )
@@ -172,7 +189,10 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
       let%bind body' = translate_block env' body in
       return (S_while (expr', body'))
   | I_skip -> ok []
-  | I_do _ae -> simple_fail "todo : do"
+  | I_do ae -> (
+      let%bind ae' = translate_annotated_expression env ae in
+      return @@ S_do ae'
+    )
 
 and translate_literal : AST.literal -> value = fun l -> match l with
   | Literal_bool b -> D_bool b
@@ -181,6 +201,7 @@ and translate_literal : AST.literal -> value = fun l -> match l with
   | Literal_tez n -> D_tez n
   | Literal_bytes s -> D_bytes s
   | Literal_string s -> D_string s
+  | Literal_address s -> D_string s
   | Literal_unit -> D_unit
 
 and transpile_small_environment : AST.small_environment -> Environment.Small.t result = fun x ->
@@ -207,7 +228,10 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
     ok @@ Combinators.Expression.make_tpl (expr, tv, env) in
   let f = translate_annotated_expression env in
   match ae.expression with
-  | E_failwith _ae -> simple_fail "todo : failwith"
+  | E_failwith ae -> (
+      let%bind ae' = translate_annotated_expression env ae in
+      return @@ E_constant ("FAILWITH" , [ae'])
+    )
   | E_literal l -> return @@ E_literal (translate_literal l)
   | E_variable name ->
       let%bind tv =
@@ -268,7 +292,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
           | `Right -> "CDR" in
         Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
       let%bind tpl' = translate_annotated_expression env tpl in
-      let expr = List.fold_right' aux tpl' path in
+      let expr = List.fold_left aux tpl' path in
       ok expr
   | E_record m ->
       let node = Append_tree.of_list @@ list_of_map m in
@@ -282,36 +306,17 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
       in
       Append_tree.fold_ne (translate_annotated_expression env) aux node
   | E_record_accessor (record, property) ->
-      let%bind translation = translate_annotated_expression env record in
-      let%bind record_type_map =
-        let error =
-          let title () =
-            Format.asprintf "Accessing field of %a, that has type %a, which isn't a record"
-              AST.PP.annotated_expression record AST.PP.type_value record.type_annotation in
-          let content () = "" in
-          error title content in
-        trace error @@
-        get_t_record record.type_annotation in
-      let node_tv = Append_tree.of_list @@ kv_list_of_map record_type_map in
-      let leaf (key, _) : expression result =
-        if property = key then (
-          ok translation
-        ) else (
-          simple_fail "bad leaf"
-        ) in
-      let node (a:expression result) b : expression result =
-        match%bind bind_lr (a, b) with
-        | `Left expr -> (
-            let%bind (tv, _) = Mini_c.get_t_pair @@ Expression.get_type expr in
-            return ~tv @@ E_constant ("CAR", [expr])
-          )
-        | `Right expr -> (
-            let%bind (_, tv) = Mini_c.get_t_pair @@ Expression.get_type expr in
-            return ~tv @@ E_constant ("CDR", [expr])
-          ) in
-      let%bind expr =
-        trace_strong (simple_error "bad key in record (shouldn't happen here)") @@
-        Append_tree.fold_ne leaf node node_tv in
+      let%bind ty' = translate_type (get_type_annotation record) in
+      let%bind ty_smap = get_t_record (get_type_annotation record) in
+      let%bind ty'_smap = bind_map_smap translate_type ty_smap in
+      let%bind path = record_access_to_lr ty' ty'_smap property in
+      let aux = fun pred (ty, lr) ->
+        let c = match lr with
+          | `Left -> "CAR"
+          | `Right -> "CDR" in
+        Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
+      let%bind record' = translate_annotated_expression env record in
+      let expr = List.fold_left aux record' path in
       ok expr
   | E_constant (name, lst) ->
       let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in (
@@ -615,9 +620,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
   | T_constant ("nat", []) ->
       let%bind n = get_nat v in
       return (E_literal (Literal_nat n))
+  | T_constant ("tez", []) ->
+      let%bind n = get_nat v in
+      return (E_literal (Literal_tez n))
   | T_constant ("string", []) ->
       let%bind n = get_string v in
       return (E_literal (Literal_string n))
+  | T_constant ("address", []) ->
+      let%bind n = get_string v in
+      return (E_literal (Literal_address n))
   | T_constant ("option", [o]) -> (
       match%bind get_option v with
       | None -> ok (e_a_empty_none o)
diff --git a/src/ligo/typer/typer.ml b/src/ligo/typer/typer.ml
index f396b1b0e..d54941bf8 100644
--- a/src/ligo/typer/typer.ml
+++ b/src/ligo/typer/typer.ml
@@ -127,21 +127,18 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
       let%bind ex' = type_annotated_expression e ex in
       match m with
       (* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
-      | I.Match_bool { match_false ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
+      | I.Match_bool { match_false = [] ; match_true = [ I_do { expression = E_failwith fw } ] }
+      | I.Match_bool { match_false = [ I_skip ] ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
           let%bind fw' = type_annotated_expression e fw in
-          let%bind mf' = type_block e match_false in
           let%bind () =
             trace_strong (simple_error "Matching bool on not-a-bool")
             @@ assert_t_bool (get_type_annotation ex') in
-          let mt' = [ O.I_do (
-              make_a_e
-                (E_failwith fw')
-                (t_unit ())
-                e
-            ) ]
+          let assert_ = make_a_e
+              (E_constant ("ASSERT" , [ex' ; fw']))
+              (t_unit ())
+              e
           in
-          let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in
-          return (O.I_matching (ex' , m'))
+          return (O.I_do assert_)
         )
       | _ -> (
           let%bind m' = type_match type_block e ex'.type_annotation m in
@@ -159,15 +156,56 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
           match access with
           | I.Access_record s ->
               let%bind m = O.Combinators.get_t_record ty in
-              trace_option (simple_error "unbound record access in record_patch") @@
-              Map.String.find_opt s m
-          | Access_tuple i ->
+              let%bind ty =
+                trace_option (simple_error "unbound record access in record_patch") @@
+                Map.String.find_opt s m in
+              ok (ty , O.Access_record s)
+          | I.Access_tuple i ->
               let%bind t = O.Combinators.get_t_tuple ty in
-              generic_try (simple_error "unbound tuple access in record_patch") @@
-              (fun () -> List.nth t i)
+              let%bind ty =
+                generic_try (simple_error "unbound tuple access in record_patch") @@
+                (fun () -> List.nth t i) in
+              ok (ty , O.Access_tuple i)
+          | I.Access_map ind ->
+              let%bind (k , v) = O.Combinators.get_t_map ty in
+              let%bind ind' = type_annotated_expression e ind in
+              let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' ,  k) in
+              ok (v , O.Access_map ind')
         in
-        let%bind _assert = bind_fold_list aux ty.type_value (path @ [Access_record s]) in
-        ok @@ O.I_patch (tv, path @ [Access_record s], ae')
+        let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_record s]) in
+        ok @@ O.I_patch (tv, path', ae')
+      in
+      let%bind lst' = bind_map_list aux lst in
+      ok (e, lst')
+  | I_tuple_patch (r, path, lst) ->
+      let aux (s, ae) =
+        let%bind ae' = type_annotated_expression e ae in
+        let%bind ty =
+          trace_option (simple_error "unbound variable in tuple_patch") @@
+          Environment.get_opt r e in
+        let tv = O.{type_name = r ; type_value = ty.type_value} in
+        let aux ty access =
+          match access with
+          | I.Access_record s ->
+              let%bind m = O.Combinators.get_t_record ty in
+              let%bind ty =
+                trace_option (simple_error "unbound record access in tuple_patch") @@
+                Map.String.find_opt s m in
+              ok (ty , O.Access_record s)
+          | I.Access_tuple i ->
+              let%bind t = O.Combinators.get_t_tuple ty in
+              let%bind ty =
+                generic_try (simple_error "unbound tuple access in tuple_patch") @@
+                (fun () -> List.nth t i) in
+              ok (ty , O.Access_tuple i)
+          | I.Access_map ind ->
+              let%bind (k , v) = O.Combinators.get_t_map ty in
+              let%bind ind' = type_annotated_expression e ind in
+              let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' ,  k) in
+              ok (v , O.Access_map ind')
+        in
+        let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_tuple s]) in
+        ok @@ O.I_patch (tv, path', ae')
       in
       let%bind lst' = bind_map_list aux lst in
       ok (e, lst')
@@ -328,6 +366,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
       return (E_literal (Literal_nat n)) (t_nat ())
   | E_literal (Literal_tez n) ->
       return (E_literal (Literal_tez n)) (t_tez ())
+  | E_literal (Literal_address s) ->
+      return (e_address s) (t_address ())
   (* Tuple *)
   | E_tuple lst ->
       let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
@@ -351,6 +391,13 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
               @@ (fun () -> SMap.find property r_tv) in
             return (E_record_accessor (prev , property)) tv
           )
+        | Access_map ae -> (
+            let%bind ae' = type_annotated_expression e ae in
+            let%bind (k , v) = get_t_map prev.type_annotation in
+            let%bind () =
+              Ast_typed.assert_type_value_eq (k , get_type_annotation ae') in
+            return (E_look_up (prev , ae')) v
+          )
       in
       trace (simple_error "accessing") @@
       bind_fold_list aux e' path
@@ -410,18 +457,22 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
               let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
               ok (Some c') in
         let%bind key_type =
-          let%bind opt =
+          let%bind sub =
             bind_fold_list aux None
             @@ List.map get_type_annotation
             @@ List.map fst lst' in
-          trace_option (simple_error "empty map expression") opt
+          let%bind annot = bind_map_option get_t_map_key tv_opt in
+          trace (simple_error "untyped empty map expression") @@
+          O.merge_annotation annot sub
         in
         let%bind value_type =
-          let%bind opt =
+          let%bind sub =
             bind_fold_list aux None
             @@ List.map get_type_annotation
             @@ List.map snd lst' in
-          trace_option (simple_error "empty map expression") opt
+          let%bind annot = bind_map_option get_t_map_value tv_opt in
+          trace (simple_error "untyped empty map expression") @@
+          O.merge_annotation annot sub
         in
         ok (t_map key_type value_type ())
       in
@@ -553,6 +604,7 @@ let untype_literal (l:O.literal) : I.literal result =
   | Literal_int n -> ok (Literal_int n)
   | Literal_string s -> ok (Literal_string s)
   | Literal_bytes b -> ok (Literal_bytes b)
+  | Literal_address s -> ok (Literal_address s)
 
 let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
   let open I in
@@ -643,8 +695,19 @@ and untype_instruction (i:O.instruction) : (I.instruction) result =
         List.rev_uncons_opt p in
       let%bind tl_name = match tl with
         | Access_record n -> ok n
-        | Access_tuple _ -> simple_fail "last element of patch is tuple" in
-      ok @@ I_record_patch (s.type_name, hds, [tl_name, e'])
+        | Access_tuple _ -> simple_fail "last element of patch is tuple"
+        | Access_map _ -> simple_fail "last element of patch is map"
+      in
+      let%bind hds' = bind_map_list untype_access hds in
+      ok @@ I_record_patch (s.type_name, hds', [tl_name, e'])
+
+and untype_access (a:O.access) : I.access result =
+  match a with
+  | Access_record n -> ok @@ I.Access_record n
+  | Access_tuple n -> ok @@ I.Access_tuple n
+  | Access_map n ->
+      let%bind n' = untype_annotated_expression n in
+      ok @@ I.Access_map n'
 
 and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
   let open I in