Michelson: preliminary gas infrastructure

Costs are yet to be tweaked.

This patch is joint work between:
  Milo Davis <davis.mil@husky.neu.edu>
  Benjamin Canou <benjamin@canou.fr>
  Pierre Chambart <pierre.chambart@ocamlpro.com>

lib_embedded_client_alpha/client_proto_programs.ml

@@ -53,9 +53,9 @@ let print_trace_result (cctxt : #Client_commands.logger) ~show_source ~parsed =
         (Format.pp_print_list
            (fun ppf (loc, gas, stack) ->
               Format.fprintf ppf
-                "- @[<v 0>location: %d (remaining gas: %d)@,\
+                "- @[<v 0>location: %d (remaining gas: %a)@,\
                  [ @[<v 0>%a ]@]@]"
-                loc gas
+                loc Gas.pp gas
                 (Format.pp_print_list print_expr)
                 stack))
         trace >>= fun () ->

lib_embedded_client_alpha/client_proto_programs.mli

@@ -28,14 +28,14 @@ val trace :
   input:Michelson_v1_parser.parsed ->
   Client_rpcs.block ->
   #Client_rpcs.ctxt ->
-  (Script.expr * Script.expr * (int * int * Script.expr list) list) tzresult Lwt.t
+  (Script.expr * Script.expr * (int * Gas.t * Script.expr list) list) tzresult Lwt.t
 
 val print_trace_result :
   #Client_commands.logger ->
   show_source:bool ->
   parsed:Michelson_v1_parser.parsed ->
   (Script_repr.expr * Script_repr.expr *
-   (int * int * Script_repr.expr list) list)
+   (int * Gas.t * Script_repr.expr list) list)
     tzresult -> unit tzresult Lwt.t
 
 val print_run_result :

lib_embedded_client_alpha/client_proto_rpcs.ml

@@ -64,7 +64,7 @@ module Constants = struct
   let max_signing_slot cctxt block =
     call_error_service1 cctxt Services.Constants.max_signing_slot block ()
   let instructions_per_transaction cctxt block =
-    call_error_service1 cctxt Services.Constants.instructions_per_transaction block ()
+    call_error_service1 cctxt Services.Constants.max_gas block ()
   let stamp_threshold cctxt block =
     call_error_service1 cctxt Services.Constants.proof_of_work_threshold block ()
 end

lib_embedded_client_alpha/client_proto_rpcs.mli

@@ -163,7 +163,7 @@ module Helpers : sig
     block -> Script.expr ->
     (Script.expr * Script.expr * Tez.t) ->
     (Script.expr * Script.expr *
-     (Script.location * int * Script.expr list) list) tzresult Lwt.t
+     (Script.location * Gas.t * Script.expr list) list) tzresult Lwt.t
   val typecheck_code:
     #Client_rpcs.ctxt ->
     block -> Script.expr -> Script_ir_translator.type_map tzresult Lwt.t

lib_embedded_protocol_alpha/src/TEZOS_PROTOCOL

@@ -46,6 +46,7 @@
         "Tezos_context",
 
         "Script_typed_ir",
+        "Gas",
         "Script_ir_translator",
         "Script_interpreter",
 

lib_embedded_protocol_alpha/src/apply.ml

@@ -133,7 +133,7 @@ let apply_manager_operation_content
             Script_interpreter.execute
               origination_nonce
               source destination ctxt script amount argument
-              (Constants.instructions_per_transaction ctxt)
+              (Gas.of_int (Constants.max_gas ctxt))
             >>= function
             | Ok (storage_res, _res, _steps, ctxt, origination_nonce) ->
                 (* TODO: pay for the steps and the storage diff:

lib_embedded_protocol_alpha/src/constants_repr.ml

@@ -47,7 +47,7 @@ type constants = {
   slot_durations: Period_repr.t list ;
   first_free_baking_slot: int ;
   max_signing_slot: int ;
-  instructions_per_transaction: int ;
+  max_gas: int ;
   proof_of_work_threshold: int64 ;
   bootstrap_keys: Ed25519.Public_key.t list ;
   dictator_pubkey: Ed25519.Public_key.t ;
@@ -71,7 +71,7 @@ let default = {
     List.map Period_repr.of_seconds_exn [ 60L ] ;
   first_free_baking_slot = 16 ;
   max_signing_slot = 15 ;
-  instructions_per_transaction = 16 * 1024 ;
+  max_gas = 40_000 ;
   proof_of_work_threshold =
     Int64.(lognot (sub (shift_left 1L 56) 1L)) ;
   bootstrap_keys =
@@ -128,9 +128,9 @@ let constants_encoding =
        and max_signing_slot =
          opt Compare.Int.(=)
            default.max_signing_slot c.max_signing_slot
-       and instructions_per_transaction =
+       and max_gas =
          opt Compare.Int.(=)
-           default.instructions_per_transaction c.instructions_per_transaction
+           default.max_gas c.max_gas
        and proof_of_work_threshold =
          opt Compare.Int64.(=)
            default.proof_of_work_threshold c.proof_of_work_threshold
@@ -159,7 +159,7 @@ let constants_encoding =
            slot_durations,
            first_free_baking_slot,
            max_signing_slot,
-           instructions_per_transaction,
+           max_gas,
            proof_of_work_threshold,
            bootstrap_keys,
            dictator_pubkey),
@@ -173,7 +173,7 @@ let constants_encoding =
              slot_durations,
              first_free_baking_slot,
              max_signing_slot,
-             instructions_per_transaction,
+             max_gas,
              proof_of_work_threshold,
              bootstrap_keys,
              dictator_pubkey),
@@ -195,8 +195,8 @@ let constants_encoding =
           unopt default.first_free_baking_slot first_free_baking_slot ;
         max_signing_slot =
           unopt default.max_signing_slot max_signing_slot ;
-        instructions_per_transaction =
-          unopt default.instructions_per_transaction instructions_per_transaction ;
+        max_gas =
+          unopt default.max_gas max_gas ;
         proof_of_work_threshold =
           unopt default.proof_of_work_threshold proof_of_work_threshold ;
         bootstrap_keys =

lib_embedded_protocol_alpha/src/gas.ml

@@ -0,0 +1,290 @@
+(**************************************************************************)
+(*                                                                        *)
+(*    Copyright (c) 2014 - 2016.                                          *)
+(*    Dynamic Ledger Solutions, Inc. <contact@tezos.com>                  *)
+(*                                                                        *)
+(*    All rights reserved. No warranty, explicit or implicit, provided.   *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Tezos_context
+
+(* FIXME: this really is a preliminary estimation of costs,
+   everything in this file needs to be tweaked and proofread. *)
+
+type t = { remaining : int } [@@unboxed]
+
+type cost =
+  { allocations : int ;
+    steps : int }
+
+let encoding =
+  let open Data_encoding in
+  conv
+    (fun { remaining } ->
+       (remaining))
+    (fun (remaining) ->
+       { remaining })
+    int31
+
+let pp ppf { remaining } =
+  Format.pp_print_int ppf remaining
+
+let of_int remaining = { remaining }
+
+let encoding_cost =
+  let open Data_encoding in
+  conv
+    (fun { allocations ; steps } ->
+       (allocations, steps))
+    (fun (allocations, steps) ->
+       { allocations ; steps })
+    (obj2
+       (req "allocations" int31)
+       (req "steps" int31))
+
+let pp_cost ppf { allocations ; steps } =
+  Format.fprintf ppf
+    "(steps: %d, allocs: %d)"
+    steps allocations
+
+type error += Quota_exceeded
+
+let bytes_per_word = 8
+
+let bits_per_word = 8 * bytes_per_word
+
+let words_of_bits n =
+  n / bits_per_word
+
+let check gas =
+  if Compare.Int.(gas.remaining <= 0)
+  then fail Quota_exceeded
+  else return ()
+
+let word_cost = 2
+let step_cost = 1
+
+let consume t cost =
+  { remaining =
+      t.remaining
+      - word_cost * cost.allocations
+      - step_cost * cost.steps }
+
+(* Cost for heap allocating n words of data. *)
+let alloc_cost n =
+  { allocations = n + 1 ;
+    steps = 0 }
+
+(* Cost for one computation step. *)
+let step_cost n =
+  { allocations = 0 ;
+    steps = n }
+
+let free =
+  { allocations = 0 ;
+    steps = 0 }
+
+let ( + ) x y =
+  { allocations = x.allocations + y.allocations ;
+    steps = x.steps + y.steps }
+
+let ( * ) x y =
+  { allocations = x * y.allocations ;
+    steps = x * y.steps }
+
+let max = Compare.Int.max
+
+module Cost_of = struct
+  let cycle = step_cost 1
+  let nop = free
+
+  let stack_op = step_cost 1
+
+  let bool_binop _ _ = step_cost 1
+  let bool_unop _ = step_cost 1
+
+  let pair = alloc_cost 2
+  let pair_access = step_cost 1
+
+  let cons = alloc_cost 2
+
+  let variant_no_data = alloc_cost 1
+
+  let branch = step_cost 2
+
+  let concat s1 s2 =
+    let (+) = Pervasives.(+) in
+    alloc_cost ((String.length s1 + String.length s2) / bytes_per_word)
+
+  (* Cost per cycle of a loop, fold, etc *)
+  let loop_cycle = step_cost 2
+
+  let list_size = step_cost 1
+
+  let log2 =
+    let (+) = Pervasives.(+) in
+    let rec help acc = function
+      | 0 -> acc
+      | n -> help (acc + 1) (n / 2)
+    in help 1
+
+  let module_cost = alloc_cost 10
+
+  let map_access : type key value. (key, value) Script_typed_ir.map -> int
+    = fun (module Box) ->
+      log2 (snd Box.boxed)
+
+  let map_to_list : type key value. (key, value) Script_typed_ir.map -> cost
+    = fun (module Box) ->
+      let size = snd Box.boxed in
+      2 * (alloc_cost @@ Pervasives.(size * 2))
+
+  let map_mem _key map = step_cost (map_access map)
+
+  let map_get = map_mem
+
+  let map_update _ _ map =
+    map_access map * alloc_cost 3
+
+  let map_size = step_cost 2
+
+  let set_access : type elt. elt -> elt Script_typed_ir.set -> int
+    = fun _key (module Box) ->
+      log2 @@ Box.size
+
+  let set_mem key set = step_cost (set_access key set)
+
+  let set_update key _value set =
+    set_access key set * alloc_cost 3
+
+  (* for LEFT, RIGHT, SOME *)
+  let wrap = alloc_cost 1
+
+  let mul n1 n2 =
+    let words =
+      let ( * ) = Pervasives.( * ) in
+      words_of_bits
+        ((Z.numbits (Script_int.to_zint n1))
+         * (Z.numbits (Script_int.to_zint  n2))) in
+    step_cost words + alloc_cost words
+
+  let div n1 n2 =
+    mul n1 n2 + alloc_cost 2
+
+  let add_sub_z n1 n2 =
+    let words = words_of_bits
+        (max (Z.numbits n1) (Z.numbits n2)) in
+    step_cost (words_of_bits words) + alloc_cost words
+
+  let add n1 n2 =
+    add_sub_z (Script_int.to_zint n1) (Script_int.to_zint n2)
+
+  let sub = add
+
+  let abs n =
+    alloc_cost (words_of_bits @@ Z.numbits @@ Script_int.to_zint n)
+
+  let neg = abs
+  let int _ = step_cost 1
+
+  let add_timestamp t n =
+    add_sub_z (Script_timestamp.to_zint t) (Script_int.to_zint n)
+
+  let sub_timestamp t n =
+    add_sub_z (Script_timestamp.to_zint t) (Script_int.to_zint n)
+
+  let diff_timestamps t1 t2 =
+    add_sub_z (Script_timestamp.to_zint t1) (Script_timestamp.to_zint t2)
+
+  let empty_set = module_cost
+
+  let set_size = step_cost 2
+
+  let set_to_list : type item. item Script_typed_ir.set -> cost
+    = fun (module Box) ->
+      alloc_cost @@ Pervasives.(Box.size * 2)
+
+  let empty_map = module_cost
+
+  let int64_op = step_cost 1 + alloc_cost 1
+
+  let z_to_int64 = step_cost 2 + alloc_cost 1
+
+  let int64_to_z = step_cost 2 + alloc_cost 1
+
+  let bitwise_binop n1 n2 =
+    let words = words_of_bits (max (Z.numbits (Script_int.to_zint n1)) (Z.numbits (Script_int.to_zint n2))) in
+    step_cost words + alloc_cost words
+
+  let logor = bitwise_binop
+  let logand = bitwise_binop
+  let logxor = bitwise_binop
+  let lognot n =
+    let words = words_of_bits @@ Z.numbits @@ Script_int.to_zint n in
+    step_cost words + alloc_cost words
+
+  let unopt ~default = function
+    | None -> default
+    | Some x -> x
+
+  let shift_left x y =
+    (alloc_cost @@ words_of_bits @@
+     let (+) = Pervasives.(+) in
+     Z.numbits (Script_int.to_zint x) +
+     (unopt (Script_int.to_int y) ~default:2147483647))
+
+  let shift_right x y =
+    (alloc_cost @@ words_of_bits @@
+     max 1 @@
+     let (-) = Pervasives.(-) in
+     Z.numbits (Script_int.to_zint x) -
+     unopt (Script_int.to_int y) ~default:2147483647)
+
+
+  let exec = step_cost 1
+
+  let push = step_cost 1
+
+  let compare_res = step_cost 1
+
+  (* TODO: protocol operations *)
+  let manager = step_cost 3
+  let transfer = step_cost 50
+  let create_account = step_cost 20
+  let create_contract = step_cost 70
+  let default_account = step_cost 10
+  let balance = step_cost 5
+  let now = step_cost 3
+  let check_signature = step_cost 3
+  let hash_key = step_cost 3
+  (* TODO: This needs to be a function of the data being hashed *)
+  let hash _data = step_cost 3
+  let steps_to_quota = step_cost 1
+  let get_steps_to_quota gas = Script_int.abs @@ Script_int.of_int gas.remaining
+  let source = step_cost 3
+  let amount = step_cost 1
+  let compare_bool _ _ = step_cost 1
+  let compare_string s1 s2 =
+    step_cost (max (String.length s1) (String.length s2) / 8) + step_cost 1
+  let compare_tez _ _ = step_cost 1
+  let compare_zint n1 n2 = step_cost (max (Z.numbits n1) (Z.numbits n2) / 8) + step_cost 1
+  let compare_int n1 n2 = compare_zint (Script_int.to_zint n1) (Script_int.to_zint n2)
+  let compare_nat = compare_int
+  let compare_key_hash _ _ = alloc_cost (36 / bytes_per_word)
+  let compare_timestamp t1 t2 = compare_zint (Script_timestamp.to_zint t1) (Script_timestamp.to_zint t2)
+
+end
+
+let () =
+  let open Data_encoding in
+  register_error_kind
+    `Permanent
+    ~id:"quotaExceededRuntimeError"
+    ~title: "Quota exceeded (runtime script error)"
+    ~description:
+      "A script or one of its callee took too much \
+       time or storage space"
+    empty
+    (function Quota_exceeded -> Some () | _ -> None)
+    (fun () -> Quota_exceeded) ;

lib_embedded_protocol_alpha/src/gas.mli

@@ -0,0 +1,103 @@
+(**************************************************************************)
+(*                                                                        *)
+(*    Copyright (c) 2014 - 2016.                                          *)
+(*    Dynamic Ledger Solutions, Inc. <contact@tezos.com>                  *)
+(*                                                                        *)
+(*    All rights reserved. No warranty, explicit or implicit, provided.   *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Tezos_context
+
+type t
+type cost
+
+val consume : t -> cost -> t
+
+val encoding : t Data_encoding.encoding
+val pp : Format.formatter -> t -> unit
+
+val encoding_cost : cost Data_encoding.encoding
+val pp_cost : Format.formatter -> cost -> unit
+
+val check : t -> unit tzresult Lwt.t
+type error += Quota_exceeded
+
+val of_int : int -> t
+
+module Cost_of : sig
+  val cycle : cost
+  val loop_cycle : cost
+  val list_size : cost
+  val nop : cost
+  val stack_op : cost
+  val bool_binop : 'a -> 'b -> cost
+  val bool_unop : 'a -> cost
+  val pair : cost
+  val pair_access : cost
+  val cons : cost
+  val variant_no_data : cost
+  val branch : cost
+  val concat : string -> string -> cost
+  val map_mem :
+    'a -> ('b, 'c) Script_typed_ir.map -> cost
+  val map_to_list :
+    ('b, 'c) Script_typed_ir.map -> cost
+  val map_get :
+    'a -> ('b, 'c) Script_typed_ir.map -> cost
+  val map_update :
+    'a -> 'b -> ('c, 'd) Script_typed_ir.map -> cost
+  val map_size : cost
+  val set_to_list : 'a Script_typed_ir.set -> cost
+  val set_update : 'a -> 'b -> 'a Script_typed_ir.set -> cost
+  val set_mem : 'a -> 'a Script_typed_ir.set -> cost
+  val mul : 'a Script_int.num -> 'b Script_int.num -> cost
+  val div : 'a Script_int.num -> 'b Script_int.num -> cost
+  val add : 'a Script_int.num -> 'b Script_int.num -> cost
+  val sub : 'a Script_int.num -> 'b Script_int.num -> cost
+  val abs : 'a Script_int.num -> cost
+  val neg : 'a Script_int.num -> cost
+  val int : 'a -> cost
+  val add_timestamp : Script_timestamp.t -> 'a Script_int.num -> cost
+  val sub_timestamp : Script_timestamp.t -> 'a Script_int.num -> cost
+  val diff_timestamps : Script_timestamp.t -> Script_timestamp.t -> cost
+  val empty_set : cost
+  val set_size : cost
+  val empty_map : cost
+  val int64_op : cost
+  val z_to_int64 : cost
+  val int64_to_z : cost
+  val bitwise_binop : 'a Script_int.num -> 'b Script_int.num -> cost
+  val logor : 'a Script_int.num -> 'b Script_int.num -> cost
+  val logand : 'a Script_int.num -> 'b Script_int.num -> cost
+  val logxor : 'a Script_int.num -> 'b Script_int.num -> cost
+  val lognot : 'a Script_int.num -> cost
+  val shift_left : 'a Script_int.num -> 'b Script_int.num -> cost
+  val shift_right : 'a Script_int.num -> 'b Script_int.num -> cost
+  val exec : cost
+  val push : cost
+  val compare_res : cost
+  val manager : cost
+  val transfer : cost
+  val create_account : cost
+  val create_contract : cost
+  val default_account : cost
+  val balance : cost
+  val now : cost
+  val check_signature : cost
+  val hash_key : cost
+  val hash : 'a -> cost
+  val get_steps_to_quota : t -> Script_int.n Script_int.num
+  val steps_to_quota : cost
+  val source : cost
+  val amount : cost
+  val wrap : cost
+  val compare_bool : 'a -> 'b -> cost
+  val compare_string : string -> string -> cost
+  val compare_tez : 'a -> 'b -> cost
+  val compare_int : 'a Script_int.num -> 'b Script_int.num -> cost
+  val compare_nat : 'a Script_int.num -> 'b Script_int.num -> cost
+  val compare_key_hash : 'a -> 'b -> cost
+  val compare_timestamp : Script_timestamp.t -> Script_timestamp.t -> cost
+end
+

lib_embedded_protocol_alpha/src/script_interpreter.ml

@@ -17,23 +17,12 @@ let dummy_storage_fee = Tez.fifty_cents
 
 (* ---- Run-time errors -----------------------------------------------------*)
 
-type error += Quota_exceeded
 type error += Reject of Script.location
 type error += Overflow of Script.location
 type error += Runtime_contract_error : Contract.t * Script.expr -> error
 
 let () =
   let open Data_encoding in
-  register_error_kind
-    `Permanent
-    ~id:"quotaExceededRuntimeError"
-    ~title: "Quota exceeded (runtime script error)"
-    ~description:
-      "A script or one of its callee took too much \
-       time or storage space"
-    empty
-    (function Quota_exceeded -> Some () | _ -> None)
-    (fun () -> Quota_exceeded) ;
   register_error_kind
     `Temporary
     ~id:"scriptRejectedRuntimeError"
@@ -55,9 +44,9 @@ let () =
           Some (contract, expr)
       | _ -> None)
     (fun (contract, expr) ->
-       Runtime_contract_error (contract, expr));
+       Runtime_contract_error (contract, expr))
 
-  (* ---- interpreter ---------------------------------------------------------*)
+(* ---- interpreter ---------------------------------------------------------*)
 
 type 'tys stack =
   | Item : 'ty * 'rest stack -> ('ty * 'rest) stack
@@ -70,418 +59,554 @@ let rec unparse_stack
     | Item (v, rest), Item_t (ty, rest_ty, _) ->
         Micheline.strip_locations (unparse_data ty v) :: unparse_stack (rest, rest_ty)
 
-let check_qta qta =
-  if Compare.Int.(qta <= 0)
-  then fail Quota_exceeded
-  else return ()
+(* f should fail if it does not receive sufficient gas *)
+let rec fold_left_gas ?(cycle_cost = Gas.Cost_of.loop_cycle) gas f acc l =
+  let gas = Gas.consume gas cycle_cost in
+  Gas.check gas >>=? fun () ->
+  match l with
+  | [] -> return (acc, gas)
+  | hd :: tl -> f gas hd acc >>=? fun (acc, gas) ->
+      fold_left_gas gas f acc tl
+
+(* f should fail if it does not receive sufficient gas *)
+let rec fold_right_gas ?(cycle_cost = Gas.Cost_of.loop_cycle) gas f base l =
+  let gas = Gas.consume gas cycle_cost in
+  Gas.check gas >>=? fun () ->
+  match l with
+  | [] -> return (base, gas)
+  | hd :: tl ->
+      fold_right_gas gas f base tl >>=? fun (acc, gas) ->
+      f gas hd acc
 
 let rec interp
   : type p r.
-    ?log: (Script.location * int * Script.expr list) list ref ->
-    Contract.origination_nonce -> int -> Contract.t -> Contract.t -> Tez.t ->
+    ?log: (Script.location * Gas.t * Script.expr list) list ref ->
+    Contract.origination_nonce -> Gas.t -> Contract.t -> Contract.t -> Tez.t ->
     context -> (p, r) lambda -> p ->
-    (r * int * context * Contract.origination_nonce) tzresult Lwt.t
-  = fun ?log origination qta orig source amount ctxt (Lam (code, _)) arg ->
+    (r * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t
+  = fun ?log origination gas orig source amount ctxt (Lam (code, _)) arg ->
     let rec step
       : type b a.
-        Contract.origination_nonce -> int -> context -> (b, a) descr -> b stack ->
-        (a stack * int * context * Contract.origination_nonce) tzresult Lwt.t =
-      fun origination qta ctxt ({ instr ; loc } as descr) stack ->
-        check_qta qta >>=? fun () ->
-        let logged_return ?(origination = origination) (ret, qta, ctxt) =
-          match log with
-          | None -> return (ret, qta, ctxt, origination)
-          | Some log ->
-              log := (descr.loc, qta, unparse_stack (ret, descr.aft)) :: !log ;
-              return (ret, qta, ctxt, origination) in
+        Contract.origination_nonce -> Gas.t -> context -> (b, a) descr -> b stack ->
+        (a stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+      fun origination gas ctxt ({ instr ; loc } as descr) stack ->
+        let gas = Gas.consume gas Gas.Cost_of.cycle in
+        Gas.check gas >>=? fun () ->
+        let logged_return : type a b.
+          (b, a) descr ->
+          ?origination:Contract.origination_nonce ->
+          a stack * Gas.t * context ->
+          (a stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+          fun descr ?(origination = origination) (ret, gas, ctxt) ->
+            match log with
+            | None -> return (ret, gas, ctxt, origination)
+            | Some log ->
+                log := (descr.loc, gas, unparse_stack (ret, descr.aft)) :: !log ;
+                return (ret, gas, ctxt, origination) in
+        let gas_check_terop : type ret arg1 arg2 arg3 rest.
+          ?gas:Gas.t ->
+          ?origination:Contract.origination_nonce ->
+          (_ * (_ * (_ * rest)), ret * rest) descr ->
+          ((arg1 -> arg2 -> arg3 -> ret) * arg1 * arg2 * arg3) ->
+          (arg1 -> arg2 -> arg3 -> Gas.cost) ->
+          rest stack ->
+          ((ret * rest) stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+          fun ?(gas=gas) ?(origination = origination) descr (op, x1, x2, x3) cost_func rest ->
+            let gas = Gas.consume gas (cost_func x1 x2 x3) in
+            Gas.check gas >>=? fun () ->
+            logged_return descr ~origination (Item (op x1 x2 x3, rest), gas, ctxt) in
+        let gas_check_binop : type ret arg1 arg2 rest.
+          ?gas:Gas.t ->
+          ?origination:Contract.origination_nonce ->
+          (_ * (_ * rest), ret * rest) descr ->
+          ((arg1 -> arg2 -> ret) * arg1 * arg2) ->
+          (arg1 -> arg2 -> Gas.cost) ->
+          rest stack ->
+          context ->
+          ((ret * rest) stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+          fun ?(gas=gas) ?(origination = origination) descr (op, x1, x2) cost_func rest ctxt ->
+            let gas = Gas.consume gas (cost_func x1 x2) in
+            Gas.check gas >>=? fun () ->
+            logged_return descr ~origination (Item (op x1 x2, rest), gas, ctxt) in
+        let gas_check_unop : type ret arg rest.
+          ?gas:Gas.t ->
+          ?origination:Contract.origination_nonce ->
+          (_ * rest, ret * rest) descr ->
+          ((arg -> ret) * arg) ->
+          (arg -> Gas.cost) ->
+          rest stack ->
+          context ->
+          ((ret * rest) stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+          fun ?(gas=gas) ?(origination = origination) descr (op, arg) cost_func rest ctxt ->
+            let gas = Gas.consume gas (cost_func arg) in
+            Gas.check gas >>=? fun () ->
+            logged_return descr ~origination (Item (op arg, rest), gas, ctxt) in
+        let gas_compare :
+          type t rest.
+          (t * (t * rest), Script_int.z Script_int.num * rest) descr ->
+          (t -> t -> int) ->
+          (t -> t -> Gas.cost) ->
+          t -> t ->
+          rest stack ->
+          ((Script_int.z Script_int.num * rest) stack
+           * Gas.t
+           * context
+           * Contract.origination_nonce) tzresult Lwt.t =
+          fun descr op cost x1 x2 rest ->
+            let gas = Gas.consume gas (cost x1 x2) in
+            Gas.check gas >>=? fun () ->
+            logged_return descr (Item (Script_int.of_int @@ op x1 x2, rest), gas, ctxt) in
+        let logged_return : ?origination:Contract.origination_nonce ->
+          a stack * Gas.t * context ->
+          (a stack * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t =
+          logged_return descr in
         match instr, stack with
         (* stack ops *)
         | Drop, Item (_, rest) ->
-            logged_return (rest, qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.stack_op in
+            Gas.check gas >>=? fun () ->
+            logged_return (rest, gas, ctxt)
         | Dup, Item (v, rest) ->
-            logged_return (Item (v, Item (v, rest)), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.stack_op in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (v, Item (v, rest)), gas, ctxt)
         | Swap, Item (vi, Item (vo, rest)) ->
-            logged_return (Item (vo, Item (vi, rest)), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.stack_op in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (vo, Item (vi, rest)), gas, ctxt)
         | Const v, rest ->
-            logged_return (Item (v, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.push in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (v, rest), gas, ctxt)
         (* options *)
         | Cons_some, Item (v, rest) ->
-            logged_return (Item (Some v, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.wrap in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (Some v, rest), gas, ctxt)
         | Cons_none _, rest ->
-            logged_return (Item (None, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.variant_no_data in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (None, rest), gas, ctxt)
         | If_none (bt, _), Item (None, rest) ->
-            step origination qta ctxt bt rest
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bt rest
         | If_none (_, bf), Item (Some v, rest) ->
-            step origination qta ctxt bf (Item (v, rest))
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bf (Item (v, rest))
         (* pairs *)
         | Cons_pair, Item (a, Item (b, rest)) ->
-            logged_return (Item ((a, b), rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.pair in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item ((a, b), rest), gas, ctxt)
         | Car, Item ((a, _), rest) ->
-            logged_return (Item (a, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.pair_access in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (a, rest), gas, ctxt)
         | Cdr, Item ((_, b), rest) ->
-            logged_return (Item (b, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.pair_access in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (b, rest), gas, ctxt)
         (* unions *)
         | Left, Item (v, rest) ->
-            logged_return (Item (L v, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.wrap in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (L v, rest), gas, ctxt)
         | Right, Item (v, rest) ->
-            logged_return (Item (R v, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.wrap in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (R v, rest), gas, ctxt)
         | If_left (bt, _), Item (L v, rest) ->
-            step origination qta ctxt bt (Item (v, rest))
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bt (Item (v, rest))
         | If_left (_, bf), Item (R v, rest) ->
-            step origination qta ctxt bf (Item (v, rest))
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bf (Item (v, rest))
         (* lists *)
         | Cons_list, Item (hd, Item (tl, rest)) ->
-            logged_return (Item (hd :: tl, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.cons in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (hd :: tl, rest), gas, ctxt)
         | Nil, rest ->
-            logged_return (Item ([], rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.variant_no_data in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item ([], rest), gas, ctxt)
         | If_cons (_, bf), Item ([], rest) ->
-            step origination qta ctxt bf rest
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bf rest
         | If_cons (bt, _), Item (hd :: tl, rest) ->
-            step origination qta ctxt bt (Item (hd, Item (tl, rest)))
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bt (Item (hd, Item (tl, rest)))
         | List_map, Item (lam, Item (l, rest)) ->
-            fold_right_s (fun arg (tail, qta, ctxt, origination) ->
-                interp ?log origination qta orig source amount ctxt lam arg
-                >>=? fun (ret, qta, ctxt, origination) ->
-                return (ret :: tail, qta, ctxt, origination))
-              l ([], qta, ctxt, origination) >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+            fold_right_gas gas (fun gas arg (tail, ctxt, origination) ->
+                interp ?log origination gas orig source amount ctxt lam arg
+                >>=? fun (ret, gas, ctxt, origination) ->
+                return ((ret :: tail, ctxt, origination), gas))
+              ([], ctxt, origination) l >>=? fun ((res, ctxt, origination), gas) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | List_map_body body, Item (l, rest) ->
-            let rec help rest qta = function
-              | [] -> logged_return ~origination (Item ([], rest), qta, ctxt)
+            let rec help rest gas l =
+              let gas = Gas.consume gas Gas.Cost_of.loop_cycle in
+              Gas.check gas >>=? fun () ->
+              match l with
+              | [] -> logged_return ~origination (Item ([], rest), gas, ctxt)
               | hd :: tl ->
-                  step origination qta ctxt body (Item (hd, rest))
-                  >>=? fun (Item (hd, rest), qta, _, _) ->
-                  help rest qta tl
-                  >>=? fun (Item (tl, rest), qta, ctxt, origination) ->
-                  logged_return ~origination (Item (hd :: tl, rest), qta, ctxt)
-            in help rest qta l >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (res, qta - 1, ctxt)
+                  step origination gas ctxt body (Item (hd, rest))
+                  >>=? fun (Item (hd, rest), gas, _, _) ->
+                  help rest gas tl
+                  >>=? fun (Item (tl, rest), gas, ctxt, origination) ->
+                  logged_return ~origination (Item (hd :: tl, rest), gas, ctxt)
+            in help rest gas l >>=? fun (res, gas, ctxt, origination) ->
+            logged_return ~origination (res, gas, ctxt)
         | List_reduce, Item (lam, Item (l, Item (init, rest))) ->
-            fold_left_s
-              (fun (partial, qta, ctxt, origination) arg ->
-                 interp ?log origination qta orig source amount ctxt lam (arg, partial)
-                 >>=? fun (partial, qta, ctxt, origination) ->
-                 return (partial, qta, ctxt, origination))
-              (init, qta, ctxt, origination) l >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (partial, ctxt, origination) ->
+                 interp ?log origination gas orig source amount ctxt lam (arg, partial)
+                 >>=? fun (partial, gas, ctxt, origination) ->
+                 return ((partial, ctxt, origination), gas))
+              (init, ctxt, origination) l >>=? fun ((res, ctxt, origination), gas) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | List_size, Item (list, rest) ->
-            let len = List.length list in
-            let len = Script_int.(abs (of_int len)) in
-            logged_return (Item (len, rest), qta - 1, ctxt)
+            fold_left_gas ~cycle_cost:Gas.Cost_of.list_size gas
+              (fun gas _ len ->
+                 return (len + 1, gas))
+              0
+              list >>=? fun (len, gas) ->
+            logged_return (Item (Script_int.(abs (of_int len)), rest), gas, ctxt)
         | List_iter body, Item (l, init_stack) ->
-            fold_left_s
-              (fun (stack, qta, ctxt, origination) arg ->
-                 step origination qta ctxt body (Item (arg, stack))
-                 >>=? fun (stack, qta, ctxt, origination) ->
-                 return (stack, qta, ctxt, origination))
-              (init_stack, qta, ctxt, origination) l >>=? fun (stack, qta, ctxt, origination) ->
-            logged_return ~origination (stack, qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (stack, ctxt, origination) ->
+                 step origination gas ctxt body (Item (arg, stack))
+                 >>=? fun (stack, gas, ctxt, origination) ->
+                 return ((stack, ctxt, origination), gas))
+              (init_stack, ctxt, origination) l >>=? fun ((stack, ctxt, origination), gas) ->
+            logged_return ~origination (stack, gas, ctxt)
         (* sets *)
         | Empty_set t, rest ->
-            logged_return (Item (empty_set t, rest), qta - 1, ctxt)
+            logged_return (Item (empty_set t, rest), Gas.consume gas Gas.Cost_of.empty_set, ctxt)
         | Set_map t, Item (lam, Item (set, rest)) ->
+            let gas = Gas.consume gas (Gas.Cost_of.set_to_list set) in
+            Gas.check gas >>=? fun () ->
             let items =
               List.rev (set_fold (fun e acc -> e :: acc) set []) in
             fold_left_s
-              (fun (res, qta, ctxt, origination) arg ->
-                 interp ?log origination qta orig source amount ctxt lam arg >>=?
-                 fun (ret, qta, ctxt, origination) ->
-                 return (set_update ret true res, qta, ctxt, origination))
-              (empty_set t, qta, ctxt, origination) items >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+              (fun (res, gas, ctxt, origination) arg ->
+                 interp ?log origination gas orig source amount ctxt lam arg >>=?
+                 fun (ret, gas, ctxt, origination) ->
+                 return (set_update ret true res, gas, ctxt, origination))
+              (empty_set t, gas, ctxt, origination) items >>=? fun (res, gas, ctxt, origination) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | Set_reduce, Item (lam, Item (set, Item (init, rest))) ->
+            let gas = Gas.consume gas (Gas.Cost_of.set_to_list set) in
+            Gas.check gas >>=? fun () ->
             let items =
               List.rev (set_fold (fun e acc -> e :: acc) set []) in
-            fold_left_s
-              (fun (partial, qta, ctxt, origination) arg ->
-                 interp ?log origination qta orig source amount ctxt lam (arg, partial)
-                 >>=? fun (partial, qta, ctxt, origination) ->
-                 return (partial, qta, ctxt, origination))
-              (init, qta, ctxt, origination) items >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (partial, ctxt, origination) ->
+                 interp ?log origination gas orig source amount ctxt lam (arg, partial)
+                 >>=? fun (partial, gas, ctxt, origination) ->
+                 return ((partial, ctxt, origination), gas))
+              (init, ctxt, origination) items >>=? fun ((res, ctxt, origination), gas) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | Set_iter body, Item (set, init_stack) ->
-            fold_left_s
-              (fun (stack, qta, ctxt, origination) arg ->
-                 step origination qta ctxt body (Item (arg, stack))
-                 >>=? fun (stack, qta, ctxt, origination) ->
-                 return (stack, qta, ctxt, origination))
-              (init_stack, qta, ctxt, origination)
-              (set_fold (fun e acc -> e :: acc) set []) >>=? fun (stack, qta, ctxt, origination) ->
-            logged_return ~origination (stack, qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (stack, ctxt, origination) ->
+                 step origination gas ctxt body (Item (arg, stack))
+                 >>=? fun (stack, gas, ctxt, origination) ->
+                 return ((stack, ctxt, origination), gas))
+              (init_stack, ctxt, origination)
+              (set_fold (fun e acc -> e :: acc) set []) >>=? fun ((stack, ctxt, origination), gas) ->
+            logged_return ~origination (stack, gas, ctxt)
         | Set_mem, Item (v, Item (set, rest)) ->
-            logged_return (Item (set_mem v set, rest), qta - 1, ctxt)
+            gas_check_binop descr (set_mem, v, set) Gas.Cost_of.set_mem rest ctxt
         | Set_update, Item (v, Item (presence, Item (set, rest))) ->
-            logged_return (Item (set_update v presence set, rest), qta - 1, ctxt)
+            gas_check_terop descr (set_update, v, presence, set) Gas.Cost_of.set_update rest
         | Set_size, Item (set, rest) ->
-            logged_return (Item (set_size set, rest), qta - 1, ctxt)
+            gas_check_unop descr (set_size, set) (fun _ -> Gas.Cost_of.set_size) rest ctxt
         (* maps *)
         | Empty_map (t, _), rest ->
-            logged_return (Item (empty_map t, rest), qta - 1, ctxt)
+            logged_return (Item (empty_map t, rest), Gas.consume gas Gas.Cost_of.empty_map, ctxt)
         | Map_map, Item (lam, Item (map, rest)) ->
+            let gas = Gas.consume gas (Gas.Cost_of.map_to_list map) in
+            Gas.check gas >>=? fun () ->
             let items =
               List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
-            fold_left_s
-              (fun (acc, qta, ctxt, origination) (k, v) ->
-                 interp ?log origination qta orig source amount ctxt lam (k, v)
-                 >>=? fun (ret, qta, ctxt, origination) ->
-                 return (map_update k (Some ret) acc, qta, ctxt, origination))
-              (empty_map (map_key_ty map), qta, ctxt, origination) items >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+            fold_left_gas gas
+              (fun gas (k, v) (acc, ctxt, origination) ->
+                 interp ?log origination gas orig source amount ctxt lam (k, v)
+                 >>=? fun (ret, gas, ctxt, origination) ->
+                 return ((map_update k (Some ret) acc, ctxt, origination), gas))
+              (empty_map (map_key_ty map), ctxt, origination) items >>=? fun ((res, ctxt, origination), gas) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | Map_reduce, Item (lam, Item (map, Item (init, rest))) ->
+            let gas = Gas.consume gas (Gas.Cost_of.map_to_list map) in
+            Gas.check gas >>=? fun () ->
             let items =
               List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
-            fold_left_s
-              (fun (partial, qta, ctxt, origination) arg ->
-                 interp ?log origination qta orig source amount ctxt lam (arg, partial)
-                 >>=? fun (partial, qta, ctxt, origination) ->
-                 return (partial, qta, ctxt, origination))
-              (init, qta, ctxt, origination) items >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (partial, ctxt, origination) ->
+                 interp ?log origination gas orig source amount ctxt lam (arg, partial)
+                 >>=? fun (partial, gas, ctxt, origination) ->
+                 return ((partial, ctxt, origination), gas))
+              (init, ctxt, origination) items >>=? fun ((res, ctxt, origination), gas) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | Map_iter body, Item (map, init_stack) ->
+            let gas = Gas.consume gas (Gas.Cost_of.map_to_list map) in
+            Gas.check gas >>=? fun () ->
             let items =
               List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in
-            fold_left_s
-              (fun (stack, qta, ctxt, origination) arg ->
-                 step origination qta ctxt body (Item (arg, stack))
-                 >>=? fun (stack, qta, ctxt, origination) ->
-                 return (stack, qta, ctxt, origination))
-              (init_stack, qta, ctxt, origination) items >>=? fun (stack, qta, ctxt, origination) ->
-            logged_return ~origination (stack, qta, ctxt)
+            fold_left_gas gas
+              (fun gas arg (stack, ctxt, origination) ->
+                 step origination gas ctxt body (Item (arg, stack))
+                 >>=? fun (stack, gas, ctxt, origination) ->
+                 return ((stack, ctxt, origination), gas))
+              (init_stack, ctxt, origination) items >>=? fun ((stack, ctxt, origination), gas) ->
+            logged_return ~origination (stack, gas, ctxt)
         | Map_mem, Item (v, Item (map, rest)) ->
-            logged_return (Item (map_mem v map, rest), qta - 1, ctxt)
+            gas_check_binop descr (map_mem, v, map) Gas.Cost_of.map_mem rest ctxt
         | Map_get, Item (v, Item (map, rest)) ->
-            logged_return (Item (map_get v map, rest), qta - 1, ctxt)
+            gas_check_binop descr (map_get, v, map) Gas.Cost_of.map_get rest ctxt
         | Map_update, Item (k, Item (v, Item (map, rest))) ->
-            logged_return (Item (map_update k v map, rest), qta - 1, ctxt)
+            gas_check_terop descr (map_update, k, v, map) Gas.Cost_of.map_update rest
         | Map_size, Item (map, rest) ->
-            logged_return (Item (map_size map, rest), qta - 1, ctxt)
+            gas_check_unop descr (map_size, map) (fun _ -> Gas.Cost_of.map_size) rest ctxt
         (* timestamp operations *)
         | Add_seconds_to_timestamp, Item (n, Item (t, rest)) ->
-            logged_return (Item (Script_timestamp.add_delta t n, rest), qta - 1, ctxt)
+            gas_check_binop descr
+              (Script_timestamp.add_delta, t, n)
+              Gas.Cost_of.add_timestamp rest ctxt
         | Add_timestamp_to_seconds, Item (t, Item (n, rest)) ->
-            logged_return (Item (Script_timestamp.add_delta t n, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_timestamp.add_delta, t, n)
+              Gas.Cost_of.add_timestamp rest ctxt
         | Sub_timestamp_seconds, Item (t, Item (s, rest)) ->
-            logged_return (Item (Script_timestamp.sub_delta t s, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_timestamp.sub_delta, t, s)
+              Gas.Cost_of.sub_timestamp rest ctxt
         | Diff_timestamps, Item (t1, Item (t2, rest)) ->
-            logged_return (Item (Script_timestamp.diff t1 t2, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_timestamp.diff, t1, t2)
+              Gas.Cost_of.diff_timestamps rest ctxt
         (* string operations *)
         | Concat, Item (x, Item (y, rest)) ->
-            logged_return (Item (x ^ y, rest), qta - 1, ctxt)
+            gas_check_binop descr ((^), x, y) Gas.Cost_of.concat rest ctxt
         (* currency operations *)
         | Add_tez, Item (x, Item (y, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_op in
+            Gas.check gas >>=? fun () ->
             Lwt.return Tez.(x +? y) >>=? fun res ->
-            logged_return (Item (res, rest), qta - 1, ctxt)
+            logged_return (Item (res, rest), gas, ctxt)
         | Sub_tez, Item (x, Item (y, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_op in
+            Gas.check gas >>=? fun () ->
             Lwt.return Tez.(x -? y) >>=? fun res ->
-            logged_return (Item (res, rest), qta - 1, ctxt)
+            logged_return (Item (res, rest), gas, ctxt)
         | Mul_teznat, Item (x, Item (y, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_op in
+            let gas = Gas.consume gas Gas.Cost_of.z_to_int64 in
+            Gas.check gas >>=? fun () ->
             begin
               match Script_int.to_int64 y with
               | None -> fail (Overflow loc)
               | Some y ->
                   Lwt.return Tez.(x *? y) >>=? fun res ->
-                  logged_return (Item (res, rest), qta - 1, ctxt)
+                  logged_return (Item (res, rest), gas, ctxt)
             end
         | Mul_nattez, Item (y, Item (x, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_op in
+            let gas = Gas.consume gas Gas.Cost_of.z_to_int64 in
+            Gas.check gas >>=? fun () ->
             begin
               match Script_int.to_int64 y with
               | None -> fail (Overflow loc)
               | Some y ->
                   Lwt.return Tez.(x *? y) >>=? fun res ->
-                  logged_return (Item (res, rest), qta - 1, ctxt)
+                  logged_return (Item (res, rest), gas, ctxt)
             end
         (* boolean operations *)
         | Or, Item (x, Item (y, rest)) ->
-            logged_return (Item (x || y, rest), qta - 1, ctxt)
+            gas_check_binop descr ((||), x, y) Gas.Cost_of.bool_binop rest ctxt
         | And, Item (x, Item (y, rest)) ->
-            logged_return (Item (x && y, rest), qta - 1, ctxt)
+            gas_check_binop descr ((&&), x, y) Gas.Cost_of.bool_binop rest ctxt
         | Xor, Item (x, Item (y, rest)) ->
-            logged_return (Item (not x && y || x && not y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Compare.Bool.(<>), x, y) Gas.Cost_of.bool_binop rest ctxt
         | Not, Item (x, rest) ->
-            logged_return (Item (not x, rest), qta - 1, ctxt)
+            gas_check_unop descr (not, x) Gas.Cost_of.bool_unop rest ctxt
         (* integer operations *)
         | Abs_int, Item (x, rest) ->
-            logged_return (Item (Script_int.abs x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.abs, x) Gas.Cost_of.abs rest ctxt
         | Int_nat, Item (x, rest) ->
-            logged_return (Item (Script_int.int x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.int, x) Gas.Cost_of.int rest ctxt
         | Neg_int, Item (x, rest) ->
-            logged_return (Item (Script_int.neg x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.neg, x) Gas.Cost_of.neg rest ctxt
         | Neg_nat, Item (x, rest) ->
-            logged_return (Item (Script_int.neg x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.neg, x) Gas.Cost_of.neg rest ctxt
         | Add_intint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.add, x, y) Gas.Cost_of.add rest ctxt
         | Add_intnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.add, x, y) Gas.Cost_of.add rest ctxt
         | Add_natint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.add, x, y) Gas.Cost_of.add rest ctxt
         | Add_natnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.add_n x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.add_n, x, y) Gas.Cost_of.add rest ctxt
         | Sub_int, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.sub x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.sub, x, y) Gas.Cost_of.sub rest ctxt
         | Mul_intint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.mul, x, y) Gas.Cost_of.mul rest ctxt
         | Mul_intnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.mul, x, y) Gas.Cost_of.mul rest ctxt
         | Mul_natint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.mul, x, y) Gas.Cost_of.mul rest ctxt
         | Mul_natnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.mul_n x y, rest), qta - 1, ctxt)
-
+            gas_check_binop descr (Script_int.mul_n, x, y) Gas.Cost_of.mul rest ctxt
         | Ediv_teznat, Item (x, Item (y, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_to_z in
+            Gas.check gas >>=? fun () ->
             let x = Script_int.of_int64 (Tez.to_mutez x) in
-            let result =
-              match Script_int.ediv x y with
-              | None -> None
-              | Some (q, r) ->
-                  match Script_int.to_int64 q,
-                        Script_int.to_int64 r with
-                  | Some q, Some r ->
-                      begin
-                        match Tez.of_mutez q, Tez.of_mutez r with
-                        | Some q, Some r -> Some (q,r)
-                        (* Cannot overflow *)
-                        | _ -> assert false
-                      end
-                  (* Cannot overflow *)
-                  | _ -> assert false
-            in
-            logged_return (Item (result, rest), qta -1, ctxt)
-
+            gas_check_binop ~gas descr
+              ((fun x y ->
+                  match Script_int.ediv x y with
+                  | None -> None
+                  | Some (q, r) ->
+                      match Script_int.to_int64 q,
+                            Script_int.to_int64 r with
+                      | Some q, Some r ->
+                          begin
+                            match Tez.of_mutez q, Tez.of_mutez r with
+                            | Some q, Some r -> Some (q,r)
+                            (* Cannot overflow *)
+                            | _ -> assert false
+                          end
+                      (* Cannot overflow *)
+                      | _ -> assert false),
+               x, y)
+              Gas.Cost_of.div
+              rest
+              ctxt
         | Ediv_tez, Item (x, Item (y, rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.int64_to_z in
+            let gas = Gas.consume gas Gas.Cost_of.int64_to_z in
             let x = Script_int.abs (Script_int.of_int64 (Tez.to_mutez x)) in
             let y = Script_int.abs (Script_int.of_int64 (Tez.to_mutez y)) in
-            begin match Script_int.ediv_n x y with
-              | None ->
-                  logged_return (Item (None, rest), qta -1, ctxt)
-              | Some (q, r) ->
-                  let r =
-                    match Script_int.to_int64 r with
-                    | None -> assert false (* Cannot overflow *)
-                    | Some r ->
-                        match Tez.of_mutez r with
-                        | None -> assert false (* Cannot overflow *)
-                        | Some r -> r in
-                  logged_return (Item (Some (q, r), rest), qta -1, ctxt)
-            end
-
+            gas_check_binop ~gas descr
+              ((fun x y -> match Script_int.ediv_n x y with
+                  | None -> None
+                  | Some (q, r) ->
+                      match Script_int.to_int64 r with
+                      | None -> assert false (* Cannot overflow *)
+                      | Some r ->
+                          match Tez.of_mutez r with
+                          | None -> assert false (* Cannot overflow *)
+                          | Some r -> Some (q, r)),
+               x, y)
+              Gas.Cost_of.div
+              rest
+              ctxt
         | Ediv_intint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt)
+            gas_check_binop descr (Script_int.ediv, x, y) Gas.Cost_of.div rest ctxt
         | Ediv_intnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt)
+            gas_check_binop descr (Script_int.ediv, x, y) Gas.Cost_of.div rest ctxt
         | Ediv_natint, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt)
+            gas_check_binop descr (Script_int.ediv, x, y) Gas.Cost_of.div rest ctxt
         | Ediv_natnat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.ediv_n x y, rest), qta -1, ctxt)
+            gas_check_binop descr (Script_int.ediv_n, x, y) Gas.Cost_of.div rest ctxt
         | Lsl_nat, Item (x, Item (y, rest)) ->
-            begin match Script_int.shift_left_n x y with
+            let gas = Gas.consume gas (Gas.Cost_of.shift_left x y) in
+            Gas.check gas >>=? fun () -> begin
+              match Script_int.shift_left_n x y with
               | None -> fail (Overflow loc)
-              | Some r -> logged_return (Item (r, rest), qta - 1, ctxt)
+              | Some x -> logged_return (Item (x, rest), gas, ctxt)
             end
         | Lsr_nat, Item (x, Item (y, rest)) ->
-            begin match Script_int.shift_right_n x y with
+            let gas = Gas.consume gas (Gas.Cost_of.shift_right x y) in
+            Gas.check gas >>=? fun () -> begin
+              match Script_int.shift_right_n x y with
               | None -> fail (Overflow loc)
-              | Some r -> logged_return (Item (r, rest), qta - 1, ctxt)
+              | Some r -> logged_return (Item (r, rest), gas, ctxt)
             end
         | Or_nat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.logor x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.logor, x, y) Gas.Cost_of.logor rest ctxt
         | And_nat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.logand x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.logand, x, y) Gas.Cost_of.logand rest ctxt
         | Xor_nat, Item (x, Item (y, rest)) ->
-            logged_return (Item (Script_int.logxor x y, rest), qta - 1, ctxt)
+            gas_check_binop descr (Script_int.logxor, x, y) Gas.Cost_of.logxor rest ctxt
         | Not_int, Item (x, rest) ->
-            logged_return (Item (Script_int.lognot x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.lognot, x) Gas.Cost_of.lognot rest ctxt
         | Not_nat, Item (x, rest) ->
-            logged_return (Item (Script_int.lognot x, rest), qta - 1, ctxt)
+            gas_check_unop descr (Script_int.lognot, x) Gas.Cost_of.lognot rest ctxt
         (* control *)
         | Seq (hd, tl), stack ->
-            step origination qta ctxt hd stack >>=? fun (trans, qta, ctxt, origination) ->
-            step origination qta ctxt tl trans
+            step origination gas ctxt hd stack >>=? fun (trans, gas, ctxt, origination) ->
+            step origination gas ctxt tl trans
         | If (bt, _), Item (true, rest) ->
-            step origination qta ctxt bt rest
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bt rest
         | If (_, bf), Item (false, rest) ->
-            step origination qta ctxt bf rest
+            step origination (Gas.consume gas Gas.Cost_of.branch) ctxt bf rest
         | Loop body, Item (true, rest) ->
-            step origination qta ctxt body rest >>=? fun (trans, qta, ctxt, origination) ->
-            step origination (qta - 1) ctxt descr trans
+            step origination (Gas.consume gas Gas.Cost_of.loop_cycle) ctxt body rest >>=? fun (trans, gas, ctxt, origination) ->
+            step origination (Gas.consume gas Gas.Cost_of.loop_cycle) ctxt descr trans
         | Loop _, Item (false, rest) ->
-            logged_return (rest, qta, ctxt)
+            logged_return (rest, gas, ctxt)
         | Loop_left body, Item (L v, rest) ->
-            step origination qta ctxt body (Item (v, rest)) >>=? fun (trans, qta, ctxt, origination) ->
-            step origination (qta - 1) ctxt descr trans
+            step origination (Gas.consume gas Gas.Cost_of.loop_cycle) ctxt body (Item (v, rest)) >>=? fun (trans, gas, ctxt, origination) ->
+            step origination (Gas.consume gas Gas.Cost_of.loop_cycle) ctxt descr trans
         | Loop_left _, Item (R v, rest) ->
-            logged_return (Item (v, rest), qta, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.loop_cycle in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (v, rest), gas, ctxt)
         | Dip b, Item (ign, rest) ->
-            step origination qta ctxt b rest >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (ign, res), qta, ctxt)
+            step origination (Gas.consume gas Gas.Cost_of.stack_op) ctxt b rest >>=? fun (res, gas, ctxt, origination) ->
+            logged_return ~origination (Item (ign, res), gas, ctxt)
         | Exec, Item (arg, Item (lam, rest)) ->
-            interp ?log origination qta orig source amount ctxt lam arg >>=? fun (res, qta, ctxt, origination) ->
-            logged_return ~origination (Item (res, rest), qta - 1, ctxt)
+            interp ?log origination (Gas.consume gas Gas.Cost_of.exec) orig source amount ctxt lam arg >>=? fun (res, gas, ctxt, origination) ->
+            logged_return ~origination (Item (res, rest), gas, ctxt)
         | Lambda lam, rest ->
-            logged_return ~origination (Item (lam, rest), qta - 1, ctxt)
+            logged_return ~origination (Item (lam, rest), Gas.consume gas Gas.Cost_of.push, ctxt)
         | Fail, _ ->
             fail (Reject loc)
         | Nop, stack ->
-            logged_return (stack, qta, ctxt)
+            logged_return (stack, gas, ctxt)
         (* comparison *)
         | Compare Bool_key, Item (a, Item (b, rest)) ->
-            let cmpres = Compare.Bool.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Compare.Bool.compare Gas.Cost_of.compare_bool a b rest
         | Compare String_key, Item (a, Item (b, rest)) ->
-            let cmpres = Compare.String.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Compare.String.compare Gas.Cost_of.compare_string a b rest
         | Compare Tez_key, Item (a, Item (b, rest)) ->
-            let cmpres = Tez.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Tez.compare Gas.Cost_of.compare_tez a b rest
         | Compare Int_key, Item (a, Item (b, rest)) ->
-            let cmpres = Script_int.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Script_int.compare Gas.Cost_of.compare_int a b rest
         | Compare Nat_key, Item (a, Item (b, rest)) ->
-            let cmpres = Script_int.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Script_int.compare Gas.Cost_of.compare_nat a b rest
         | Compare Key_hash_key, Item (a, Item (b, rest)) ->
-            let cmpres = Ed25519.Public_key_hash.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Ed25519.Public_key_hash.compare
+              Gas.Cost_of.compare_key_hash a b rest
         | Compare Timestamp_key, Item (a, Item (b, rest)) ->
-            let cmpres = Script_timestamp.compare a b in
-            let cmpres = Script_int.of_int cmpres in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            gas_compare descr Script_timestamp.compare Gas.Cost_of.compare_timestamp a b rest
         (* comparators *)
         | Eq, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres = 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         | Neq, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres <> 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         | Lt, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres < 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         | Le, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres <= 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         | Gt, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres > 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         | Ge, Item (cmpres, rest) ->
             let cmpres = Script_int.compare cmpres Script_int.zero in
             let cmpres = Compare.Int.(cmpres >= 0) in
-            logged_return (Item (cmpres, rest), qta - 1, ctxt)
+            logged_return (Item (cmpres, rest), Gas.consume gas Gas.Cost_of.compare_res, ctxt)
         (* protocol *)
         | Manager, Item ((_, _, contract), rest) ->
+            let gas = Gas.consume gas Gas.Cost_of.manager in
+            Gas.check gas >>=? fun () ->
             Contract.get_manager ctxt contract >>=? fun manager ->
-            logged_return (Item (manager, rest), qta - 1, ctxt)
+            logged_return (Item (manager, rest), gas, ctxt)
         | Transfer_tokens storage_type,
           Item (p, Item (amount, Item ((tp, Unit_t, destination), Item (sto, Empty)))) -> begin
+            let gas = Gas.consume gas Gas.Cost_of.transfer in
+            Gas.check gas >>=? fun () ->
             Contract.spend_from_script ctxt source amount >>=? fun ctxt ->
             Contract.credit ctxt destination amount >>=? fun ctxt ->
             Contract.get_script ctxt destination >>=? fun destination_script ->
@@ -492,25 +617,27 @@ let rec interp
                   (* we see non scripted contracts as (unit, unit) contract *)
                   Lwt.return (ty_eq tp Unit_t |>
                               record_trace (Invalid_contract (loc, destination))) >>=? fun (Eq _) ->
-                  return (ctxt, qta, origination)
+                  return (ctxt, gas, origination)
               | Some script ->
                   let p = unparse_data tp p in
-                  execute origination source destination ctxt script amount p qta
-                  >>=? fun (csto, ret, qta, ctxt, origination) ->
+                  execute origination source destination ctxt script amount p gas
+                  >>=? fun (csto, ret, gas, ctxt, origination) ->
                   Contract.update_script_storage_and_fees ctxt destination dummy_storage_fee csto >>=? fun ctxt ->
                   trace
                     (Invalid_contract (loc, destination))
                     (parse_data ctxt Unit_t ret) >>=? fun () ->
-                  return (ctxt, qta, origination)
-            end >>=? fun (ctxt, qta, origination) ->
+                  return (ctxt, gas, origination)
+            end >>=? fun (ctxt, gas, origination) ->
             Contract.get_script ctxt source >>=? (function
                 | None -> assert false
                 | Some { storage } ->
                     parse_data ctxt storage_type (Micheline.root storage) >>=? fun sto ->
-                    logged_return ~origination (Item ((), Item (sto, Empty)), qta - 1, ctxt))
+                    logged_return ~origination (Item ((), Item (sto, Empty)), gas, ctxt))
           end
         | Transfer_tokens storage_type,
           Item (p, Item (amount, Item ((tp, tr, destination), Item (sto, Empty)))) -> begin
+            let gas = Gas.consume gas Gas.Cost_of.transfer in
+            Gas.check gas >>=? fun () ->
             Contract.spend_from_script ctxt source amount >>=? fun ctxt ->
             Contract.credit ctxt destination amount >>=? fun ctxt ->
             Contract.get_script ctxt destination >>=? function
@@ -519,8 +646,8 @@ let rec interp
                 let sto = Micheline.strip_locations (unparse_data storage_type sto) in
                 Contract.update_script_storage_and_fees ctxt source dummy_storage_fee sto >>=? fun ctxt ->
                 let p = unparse_data tp p in
-                execute origination source destination ctxt script amount p qta
-                >>=? fun (sto, ret, qta, ctxt, origination) ->
+                execute origination source destination ctxt script amount p gas
+                >>=? fun (sto, ret, gas, ctxt, origination) ->
                 Contract.update_script_storage_and_fees ctxt destination dummy_storage_fee sto >>=? fun ctxt ->
                 trace
                   (Invalid_contract (loc, destination))
@@ -529,20 +656,24 @@ let rec interp
                     | None -> assert false
                     | Some { storage } ->
                         parse_data ctxt storage_type (Micheline.root storage) >>=? fun sto ->
-                        logged_return ~origination (Item (v, Item (sto, Empty)), qta - 1, ctxt))
+                        logged_return ~origination (Item (v, Item (sto, Empty)), gas, ctxt))
           end
         | Create_account,
           Item (manager, Item (delegate, Item (delegatable, Item (credit, rest)))) ->
+            let gas = Gas.consume gas Gas.Cost_of.create_account in
+            Gas.check gas >>=? fun () ->
             Contract.spend_from_script ctxt source credit >>=? fun ctxt ->
             Lwt.return Tez.(credit -? Constants.origination_burn) >>=? fun balance ->
             Contract.originate ctxt
               origination
               ~manager ~delegate ~balance
               ?script:None ~spendable:true ~delegatable >>=? fun (ctxt, contract, origination) ->
-            logged_return ~origination (Item ((Unit_t, Unit_t, contract), rest), qta - 1, ctxt)
+            logged_return ~origination (Item ((Unit_t, Unit_t, contract), rest), gas, ctxt)
         | Default_account, Item (key, rest) ->
+            let gas = Gas.consume gas Gas.Cost_of.default_account in
+            Gas.check gas >>=? fun () ->
             let contract = Contract.default_contract key in
-            logged_return (Item ((Unit_t, Unit_t, contract), rest), qta - 1, ctxt)
+            logged_return (Item ((Unit_t, Unit_t, contract), rest), gas, ctxt)
         | Create_contract (g, p, r),
           Item (manager, Item
                   (delegate, Item
@@ -551,6 +682,8 @@ let rec interp
                            (credit, Item
                               (Lam (_, code), Item
                                  (init, rest))))))) ->
+            let gas = Gas.consume gas Gas.Cost_of.create_contract in
+            Gas.check gas >>=? fun () ->
             let code =
               Micheline.strip_locations
                 (Seq (0, [ Prim (0, K_parameter, [ unparse_ty None p ], None) ;
@@ -566,60 +699,72 @@ let rec interp
               ~script:({ code ; storage }, (dummy_code_fee, dummy_storage_fee))
               ~spendable ~delegatable
             >>=? fun (ctxt, contract, origination) ->
-            logged_return ~origination (Item ((p, r, contract), rest), qta - 1, ctxt)
+            logged_return ~origination (Item ((p, r, contract), rest), gas, ctxt)
         | Balance, rest ->
+            let gas = Gas.consume gas Gas.Cost_of.balance in
+            Gas.check gas >>=? fun () ->
             Contract.get_balance ctxt source >>=? fun balance ->
-            logged_return (Item (balance, rest), qta - 1, ctxt)
+            logged_return (Item (balance, rest), gas, ctxt)
         | Now, rest ->
+            let gas = Gas.consume gas Gas.Cost_of.now in
+            Gas.check gas >>=? fun () ->
             let now = Script_timestamp.now ctxt in
-            logged_return (Item (now, rest), qta - 1, ctxt)
+            logged_return (Item (now, rest), gas, ctxt)
         | Check_signature, Item (key, Item ((signature, message), rest)) ->
+            let gas = Gas.consume gas Gas.Cost_of.check_signature in
+            Gas.check gas >>=? fun () ->
             let message = MBytes.of_string message in
             let res = Ed25519.Signature.check key signature message in
-            logged_return (Item (res, rest), qta - 1, ctxt)
+            logged_return (Item (res, rest), gas, ctxt)
         | Hash_key, Item (key, rest) ->
-            logged_return (Item (Ed25519.Public_key.hash key, rest), qta -1, ctxt)
+            logged_return (Item (Ed25519.Public_key.hash key, rest), Gas.consume gas Gas.Cost_of.hash_key, ctxt)
         | H ty, Item (v, rest) ->
+            let gas = Gas.consume gas (Gas.Cost_of.hash v) in
+            Gas.check gas >>=? fun () ->
             let hash = Script.hash_expr (Micheline.strip_locations (unparse_data ty v)) in
-            logged_return (Item (hash, rest), qta - 1, ctxt)
+            logged_return (Item (hash, rest), gas, ctxt)
         | Steps_to_quota, rest ->
-            let steps = Script_int.abs (Script_int.of_int qta) in
-            logged_return (Item (steps, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.steps_to_quota in
+            logged_return (Item (Gas.Cost_of.get_steps_to_quota gas, rest), gas, ctxt)
         | Source (ta, tb), rest ->
-            logged_return (Item ((ta, tb, orig), rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.source in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item ((ta, tb, orig), rest), gas, ctxt)
         | Amount, rest ->
-            logged_return (Item (amount, rest), qta - 1, ctxt)
+            let gas = Gas.consume gas Gas.Cost_of.amount in
+            Gas.check gas >>=? fun () ->
+            logged_return (Item (amount, rest), gas, ctxt)
     in
     let stack = (Item (arg, Empty)) in
     begin match log with
       | None -> ()
       | Some log ->
-          log := (code.loc, qta, unparse_stack (stack, code.bef)) :: !log
+          log := (code.loc, gas, unparse_stack (stack, code.bef)) :: !log
     end ;
-    step origination qta ctxt code stack >>=? fun (Item (ret, Empty), qta, ctxt, origination) ->
-    return (ret, qta, ctxt, origination)
+    step origination gas ctxt code stack >>=? fun (Item (ret, Empty), gas, ctxt, origination) ->
+    return (ret, gas, ctxt, origination)
 
 (* ---- contract handling ---------------------------------------------------*)
 
-and execute ?log origination orig source ctxt script amount arg qta =
+and execute ?log origination orig source ctxt script amount arg gas =
   parse_script ctxt script
   >>=? fun (Ex_script { code; arg_type; ret_type; storage; storage_type }) ->
   parse_data ctxt arg_type arg >>=? fun arg ->
   trace
     (Runtime_contract_error (source, script.code))
-    (interp ?log origination qta orig source amount ctxt code (arg, storage))
-  >>=? fun ((ret, storage), qta, ctxt, origination) ->
+    (interp ?log origination gas orig source amount ctxt code (arg, storage))
+  >>=? fun ((ret, storage), gas, ctxt, origination) ->
   return (Micheline.strip_locations (unparse_data storage_type storage),
           unparse_data ret_type ret,
-          qta, ctxt, origination)
+          gas, ctxt, origination)
 
-let trace origination orig source ctxt script amount arg qta =
+let trace origination orig source ctxt script amount arg gas =
   let log = ref [] in
-  execute ~log origination orig source ctxt script amount (Micheline.root arg) qta
-  >>=? fun (sto, res, qta, ctxt, origination) ->
-  return ((sto, Micheline.strip_locations res, qta, ctxt, origination), List.rev !log)
+  execute ~log origination orig source ctxt script amount (Micheline.root arg) gas
+  >>=? fun (sto, res, gas, ctxt, origination) ->
+  return ((sto, Micheline.strip_locations res, gas, ctxt, origination), List.rev !log)
 
-let execute origination orig source ctxt script amount arg qta =
-  execute origination orig source ctxt script amount (Micheline.root arg) qta
-  >>=? fun (sto, res, qta, ctxt, origination) ->
-  return (sto, Micheline.strip_locations res, qta, ctxt, origination)
+let execute origination orig source ctxt script amount arg gas =
+  execute origination orig source ctxt script amount (Micheline.root arg) gas
+  >>=? fun (sto, res, gas, ctxt, origination) ->
+  return (sto, Micheline.strip_locations res, gas, ctxt, origination)

lib_embedded_protocol_alpha/src/script_interpreter.mli

@@ -9,7 +9,6 @@
 
 open Tezos_context
 
-type error += Quota_exceeded
 type error += Overflow of Script.location
 type error += Reject of Script.location
 type error += Runtime_contract_error : Contract.t * Script.expr -> error
@@ -21,13 +20,13 @@ val execute:
   Contract.origination_nonce ->
   Contract.t -> Contract.t -> Tezos_context.t ->
   Script.t -> Tez.t ->
-  Script.expr -> int ->
-  (Script.expr * Script.expr * int * context * Contract.origination_nonce) tzresult Lwt.t
+  Script.expr -> Gas.t ->
+  (Script.expr * Script.expr * Gas.t * context * Contract.origination_nonce) tzresult Lwt.t
 
 val trace:
   Contract.origination_nonce ->
   Contract.t -> Contract.t -> Tezos_context.t ->
   Script.t -> Tez.t ->
-  Script.expr -> int ->
-  ((Script.expr * Script.expr * int * context * Contract.origination_nonce) *
-   (Script.location * int * Script.expr list) list) tzresult Lwt.t
+  Script.expr -> Gas.t ->
+  ((Script.expr * Script.expr * Gas.t * context * Contract.origination_nonce) *
+   (Script.location * Gas.t * Script.expr list) list) tzresult Lwt.t

lib_embedded_protocol_alpha/src/script_ir_translator.ml

@@ -418,6 +418,7 @@ let empty_set
       type elt = a
       module OPS = OPS
       let boxed = OPS.empty
+      let size = 0
     end)
 
 let set_update
@@ -427,10 +428,14 @@ let set_update
       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
+        if b
+        then Box.OPS.add v Box.boxed
+        else Box.OPS.remove v Box.boxed
+      let size =
+        let mem = Box.OPS.mem v Box.boxed in
+        if mem
+        then if b then Box.size else Box.size - 1
+        else if b then Box.size + 1 else Box.size
     end)
 
 let set_mem
@@ -446,7 +451,7 @@ let set_fold
 let set_size
   : type elt. elt set -> Script_int.n Script_int.num =
   fun (module Box) ->
-    Script_int.(abs (of_int (Box.OPS.cardinal Box.boxed)))
+    Script_int.(abs (of_int Box.size))
 
 let map_key_ty
   : type a b. (a, b) map -> a comparable_ty
@@ -464,13 +469,13 @@ let empty_map
       type value = b
       let key_ty = ty
       module OPS = OPS
-      let boxed = OPS.empty
+      let boxed = (OPS.empty, 0)
     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
+    try Some (Box.OPS.find k (fst Box.boxed)) with Not_found -> None
 
 let map_update
   : type a b. a -> b option -> (a, b) map -> (a, b) map
@@ -481,25 +486,27 @@ let map_update
       let key_ty = Box.key_ty
       module OPS = Box.OPS
       let boxed =
+        let (map, size) = Box.boxed in
+        let contains = Box.OPS.mem k map in
         match v with
-        | Some v -> Box.OPS.add k v Box.boxed
-        | None -> Box.OPS.remove k Box.boxed
+        | Some v -> (Box.OPS.add k v map, size + if contains then 0 else 1)
+        | None -> (Box.OPS.remove k map, size - if contains then 1 else 0)
     end)
 
 let map_mem
   : type key value. key -> (key, value) map -> bool
   = fun k (module Box) ->
-    Box.OPS.mem k Box.boxed
+    Box.OPS.mem k (fst 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
+    Box.OPS.fold f (fst Box.boxed)
 
 let map_size
   : type key value. (key, value) map -> Script_int.n Script_int.num =
   fun (module Box) ->
-    Script_int.(abs (of_int (Box.OPS.cardinal Box.boxed)))
+    Script_int.(abs (of_int (snd Box.boxed)))
 
 (* ---- Unparsing (Typed IR -> Untyped epressions) --------------------------*)
 

lib_embedded_protocol_alpha/src/script_timestamp_repr.ml

@@ -43,3 +43,5 @@ let sub_delta t delta = Z.sub t (Script_int_repr.to_zint delta)
 
 let add_delta t delta =
   Z.add t (Script_int_repr.to_zint delta)
+
+let to_zint x = x

lib_embedded_protocol_alpha/src/script_timestamp_repr.mli

@@ -28,3 +28,5 @@ val diff : t -> t -> z num
 val add_delta : t -> z num -> t
 
 val sub_delta : t -> z num -> t
+
+val to_zint : t -> Z.t

lib_embedded_protocol_alpha/src/script_typed_ir.ml

@@ -26,6 +26,7 @@ module type Boxed_set = sig
   type elt
   module OPS : Set.S with type elt = elt
   val boxed : OPS.t
+  val size : int
 end
 
 type 'elt set = (module Boxed_set with type elt = 'elt)
@@ -35,7 +36,7 @@ module type Boxed_map = sig
   type value
   val key_ty : key comparable_ty
   module OPS : Map.S with type key = key
-  val boxed : value OPS.t
+  val boxed : value OPS.t * int
 end
 
 type ('key, 'value) map = (module Boxed_map with type key = 'key and type value = 'value)

lib_embedded_protocol_alpha/src/services.ml

@@ -138,7 +138,7 @@ module Constants = struct
       ~error: Data_encoding.empty
       RPC_path.(custom_root / "constants" / "max_signing_slot")
 
-  let instructions_per_transaction custom_root =
+  let max_gas custom_root =
     RPC_service.post_service
       ~description: "Instructions per transaction"
       ~query: RPC_query.empty
@@ -146,7 +146,7 @@ module Constants = struct
       ~output: (wrap_tzerror @@
                 describe ~title: "instructions per transaction" int31)
       ~error: Data_encoding.empty
-      RPC_path.(custom_root / "constants" / "instructions_per_transaction")
+      RPC_path.(custom_root / "constants" / "max_gas")
 
   let proof_of_work_threshold custom_root =
     RPC_service.post_service
@@ -479,7 +479,7 @@ module Helpers = struct
                      (req "trace"
                         (list @@ obj3
                            (req "location" Script.location_encoding)
-                           (req "gas" int31)
+                           (req "gas" Gas.encoding)
                            (req "stack" (list (Script.expr_encoding)))))))
       ~error: Data_encoding.empty
       RPC_path.(custom_root / "helpers" / "trace_code")

lib_embedded_protocol_alpha/src/services_registration.ml

@@ -123,13 +123,12 @@ let max_signing_slot ctxt () =
 
 let () = register0 Services.Constants.max_signing_slot max_signing_slot
 
-let instructions_per_transaction ctxt () =
-  return @@ Constants.instructions_per_transaction ctxt
+let max_gas ctxt () =
+  return @@ Constants.max_gas ctxt
 
 let () =
   register0
-    Services.Constants.instructions_per_transaction
-    instructions_per_transaction
+    Services.Constants.max_gas max_gas
 
 let proof_of_work_threshold ctxt () =
   return @@ Constants.proof_of_work_threshold ctxt
@@ -280,36 +279,36 @@ let () =
       | None ->
           Contract.default_contract
             (List.hd (Bootstrap.accounts ctxt)).Bootstrap.public_key_hash in
-    let qta =
-      Constants.instructions_per_transaction ctxt in
+    let max_gas =
+      Constants.max_gas ctxt in
     let origination_nonce =
       match origination_nonce with
       | Some origination_nonce -> origination_nonce
       | None ->
           Contract.initial_origination_nonce
             (Operation_hash.hash_string [ "FAKE " ; "FAKE" ; "FAKE" ]) in
-    (script, storage, input, amount, contract, qta, origination_nonce) in
+    (script, storage, input, amount, contract, max_gas, origination_nonce) in
   register1 Services.Helpers.run_code
     (fun ctxt () parameters ->
-       let (code, storage, input, amount, contract, qta, origination_nonce) =
+       let (code, storage, input, amount, contract, gas, origination_nonce) =
          run_parameters ctxt parameters in
        Script_interpreter.execute
          origination_nonce
          contract (* transaction initiator *)
          contract (* script owner *)
          ctxt { storage ; code } amount input
-         qta >>=? fun (sto, ret, _qta, _ctxt, _) ->
+         (Gas.of_int gas) >>=? fun (sto, ret, _gas, _ctxt, _) ->
        Error_monad.return (sto, ret)) ;
   register1 Services.Helpers.trace_code
     (fun ctxt () parameters ->
-       let (code, storage, input, amount, contract, qta, origination_nonce) =
+       let (code, storage, input, amount, contract, gas, origination_nonce) =
          run_parameters ctxt parameters in
        Script_interpreter.trace
          origination_nonce
          contract (* transaction initiator *)
          contract (* script owner *)
          ctxt { storage ; code } amount input
-         qta >>=? fun ((sto, ret, _qta, _ctxt, _), trace) ->
+         (Gas.of_int gas) >>=? fun ((sto, ret, _gas, _ctxt, _), trace) ->
        Error_monad.return (sto, ret, trace))
 
 let () =

lib_embedded_protocol_alpha/src/tezos_context.ml

@@ -76,9 +76,9 @@ module Constants = struct
   let max_signing_slot c =
     let constants = Raw_context.constants c in
     constants.max_signing_slot
-  let instructions_per_transaction c =
+  let max_gas c =
     let constants = Raw_context.constants c in
-    constants.instructions_per_transaction
+    constants.max_gas
   let proof_of_work_threshold c =
     let constants = Raw_context.constants c in
     constants.proof_of_work_threshold

lib_embedded_protocol_alpha/src/tezos_context.mli

@@ -121,6 +121,7 @@ module Script_timestamp : sig
   val add_delta : t -> z num -> t
   val sub_delta : t -> z num -> t
   val now : context -> t
+  val to_zint : t -> Z.t
 end
 
 module Script : sig
@@ -275,7 +276,7 @@ module Constants : sig
   val slot_durations: context -> Period.t list
   val first_free_baking_slot: context -> int
   val max_signing_slot: context -> int
-  val instructions_per_transaction: context -> int
+  val max_gas: context -> int
   val proof_of_work_threshold: context -> int64
   val dictator_pubkey: context -> Ed25519.Public_key.t
   val max_number_of_operations: context -> int list

lib_protocol_environment_sigs/v1/z.mli

@@ -78,3 +78,10 @@ external of_int: int -> t = "ml_z_of_int" [@@ noalloc]
 
 external equal: t -> t -> bool = "ml_z_equal" [@@ noalloc]
 external compare: t -> t -> int = "ml_z_compare" [@@ noalloc]
+
+external numbits: t -> int = "ml_z_numbits" [@@ noalloc]
+(** Returns the number of significant bits in the given number.
+    If [x] is zero, [numbits x] returns 0.  Otherwise,
+    [numbits x] returns a positive integer [n] such that
+    [2^{n-1} <= |x| < 2^n].  Note that [numbits] is defined
+    for negative arguments, and that [numbits (-x) = numbits x]. *)

test/test_contracts.sh

@@ -215,7 +215,7 @@ assert_output $CONTRACT_PATH/exec_concat.tz Unit '""' '"_abc"'
 assert_output $CONTRACT_PATH/exec_concat.tz Unit '"test"' '"test_abc"'
 
 # Get current steps to quota
-assert_output $CONTRACT_PATH/steps_to_quota.tz Unit Unit 16382
+assert_output $CONTRACT_PATH/steps_to_quota.tz Unit Unit 39991
 
 # Get the current balance of the contract
 assert_output $CONTRACT_PATH/balance.tz Unit Unit '"4,000,000"'