modify proto-alpha

This commit is contained in:
Galfour 2019-03-13 11:56:49 +00:00
parent 4b4c450b9a
commit b197c30299
10 changed files with 920 additions and 808 deletions

View File

@ -65,6 +65,13 @@ module Script_timestamp = struct
Raw_context.current_timestamp ctxt
|> Timestamp.to_seconds
|> of_int64
let set_now ctxt timestamp =
timestamp
|> to_zint
|> Z.to_int64
|> Time.of_seconds
|> (Raw_context.set_current_timestamp ctxt)
end
module Script = struct
include Michelson_v1_primitives

View File

@ -178,6 +178,7 @@ module Script_timestamp : sig
val add_delta: t -> z num -> t
val sub_delta: t -> z num -> t
val now: context -> t
val set_now: context -> t -> context
val to_zint: t -> Z.t
val of_zint: Z.t -> t
end
@ -248,6 +249,7 @@ module Script : sig
| I_NEQ
| I_NIL
| I_NONE
| I_NOP
| I_NOT
| I_NOW
| I_OR

View File

@ -93,6 +93,7 @@ type prim =
| I_NEQ
| I_NIL
| I_NONE
| I_NOP
| I_NOT
| I_NOW
| I_OR
@ -226,6 +227,7 @@ let string_of_prim = function
| I_NEQ -> "NEQ"
| I_NIL -> "NIL"
| I_NONE -> "NONE"
| I_NOP -> "NOP"
| I_NOT -> "NOT"
| I_NOW -> "NOW"
| I_OR -> "OR"
@ -340,6 +342,7 @@ let prim_of_string = function
| "NEQ" -> ok I_NEQ
| "NIL" -> ok I_NIL
| "NONE" -> ok I_NONE
| "NOP" -> ok I_NOP
| "NOT" -> ok I_NOT
| "NOW" -> ok I_NOW
| "OR" -> ok I_OR

View File

@ -91,6 +91,7 @@ type prim =
| I_NEQ
| I_NIL
| I_NONE
| I_NOP
| I_NOT
| I_NOW
| I_OR

View File

@ -51,6 +51,7 @@ type root_context = t
let current_level ctxt = ctxt.level
let current_timestamp ctxt = ctxt.timestamp
let set_current_timestamp ctxt timestamp = { ctxt with timestamp }
let current_fitness ctxt = ctxt.fitness
let first_level ctxt = ctxt.first_level
let constants ctxt = ctxt.constants

View File

@ -80,6 +80,7 @@ val recover: context -> Context.t
val current_level: context -> Level_repr.t
val current_timestamp: context -> Time.t
val set_current_timestamp: context -> Time.t -> context
val current_fitness: context -> Int64.t
val set_current_fitness: context -> Int64.t -> t

View File

@ -159,20 +159,25 @@ let unparse_stack ctxt (stack, stack_ty) =
module Interp_costs = Michelson_v1_gas.Cost_of
let rec interp
: type p r.
type ex_descr_stack = Ex_descr_stack : (('a, 'b) descr * 'a stack) -> ex_descr_stack
let rec step
: type b a.
(?log: execution_trace ref ->
context ->
source: Contract.t -> payer:Contract.t -> self: Contract.t -> Tez.t ->
(p, r) lambda -> p ->
(r * context) tzresult Lwt.t)
= fun ?log ctxt ~source ~payer ~self amount (Lam (code, _)) arg ->
let rec step
: type b a.
context -> (b, a) descr -> b stack ->
(a stack * context) tzresult Lwt.t =
fun ctxt ({ instr ; loc ; _ } as descr) stack ->
source: Contract.t ->
self: Contract.t ->
payer: Contract.t ->
?visitor: (ex_descr_stack -> unit) ->
Tez.t ->
(b, a) descr -> b stack ->
(a stack * context) tzresult Lwt.t) =
fun ?log ctxt ~source ~self ~payer ?visitor amount ({ instr ; loc ; _ } as descr) stack ->
Lwt.return (Gas.consume ctxt Interp_costs.cycle) >>=? fun ctxt ->
(match visitor with
| Some visitor -> visitor @@ Ex_descr_stack(descr, stack)
| None -> ()) ;
let step_same ctxt = step ?log ctxt ~source ~self ~payer ?visitor amount in
let logged_return : type a b.
(b, a) descr ->
a stack * context ->
@ -255,10 +260,10 @@ let rec interp
logged_return (Item (None, rest), ctxt)
| If_none (bt, _), Item (None, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bt rest
step_same ctxt bt rest
| If_none (_, bf), Item (Some v, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bf (Item (v, rest))
step_same ctxt bf (Item (v, rest))
(* pairs *)
| Cons_pair, Item (a, Item (b, rest)) ->
Lwt.return (Gas.consume ctxt Interp_costs.pair) >>=? fun ctxt ->
@ -278,10 +283,10 @@ let rec interp
logged_return (Item (R v, rest), ctxt)
| If_left (bt, _), Item (L v, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bt (Item (v, rest))
step_same ctxt bt (Item (v, rest))
| If_left (_, bf), Item (R v, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bf (Item (v, rest))
step_same ctxt bf (Item (v, rest))
(* lists *)
| Cons_list, Item (hd, Item (tl, rest)) ->
Lwt.return (Gas.consume ctxt Interp_costs.cons) >>=? fun ctxt ->
@ -291,17 +296,17 @@ let rec interp
logged_return (Item ([], rest), ctxt)
| If_cons (_, bf), Item ([], rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bf rest
step_same ctxt bf rest
| If_cons (bt, _), Item (hd :: tl, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bt (Item (hd, Item (tl, rest)))
step_same ctxt bt (Item (hd, Item (tl, rest)))
| List_map body, Item (l, rest) ->
let rec loop rest ctxt l acc =
Lwt.return (Gas.consume ctxt Interp_costs.loop_cycle) >>=? fun ctxt ->
match l with
| [] -> return (Item (List.rev acc, rest), ctxt)
| hd :: tl ->
step ctxt body (Item (hd, rest))
step_same ctxt body (Item (hd, rest))
>>=? fun (Item (hd, rest), ctxt) ->
loop rest ctxt tl (hd :: acc)
in loop rest ctxt l [] >>=? fun (res, ctxt) ->
@ -321,7 +326,7 @@ let rec interp
match l with
| [] -> return (stack, ctxt)
| hd :: tl ->
step ctxt body (Item (hd, stack))
step_same ctxt body (Item (hd, stack))
>>=? fun (stack, ctxt) ->
loop ctxt tl stack
in loop ctxt l init >>=? fun (res, ctxt) ->
@ -338,7 +343,7 @@ let rec interp
match l with
| [] -> return (stack, ctxt)
| hd :: tl ->
step ctxt body (Item (hd, stack))
step_same ctxt body (Item (hd, stack))
>>=? fun (stack, ctxt) ->
loop ctxt tl stack
in loop ctxt l init >>=? fun (res, ctxt) ->
@ -361,7 +366,7 @@ let rec interp
match l with
| [] -> return (acc, ctxt)
| (k, _) as hd :: tl ->
step ctxt body (Item (hd, rest))
step_same ctxt body (Item (hd, rest))
>>=? fun (Item (hd, rest), ctxt) ->
loop rest ctxt tl (map_update k (Some hd) acc)
in loop rest ctxt l (empty_map (map_key_ty map)) >>=? fun (res, ctxt) ->
@ -374,7 +379,7 @@ let rec interp
match l with
| [] -> return (stack, ctxt)
| hd :: tl ->
step ctxt body (Item (hd, stack))
step_same ctxt body (Item (hd, stack))
>>=? fun (stack, ctxt) ->
loop ctxt tl stack
in loop ctxt l init >>=? fun (res, ctxt) ->
@ -603,30 +608,30 @@ let rec interp
consume_gas_unop descr (Script_int.lognot, x) Interp_costs.lognot rest ctxt
(* control *)
| Seq (hd, tl), stack ->
step ctxt hd stack >>=? fun (trans, ctxt) ->
step ctxt tl trans
step_same ctxt hd stack >>=? fun (trans, ctxt) ->
step_same ctxt tl trans
| If (bt, _), Item (true, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bt rest
step_same ctxt bt rest
| If (_, bf), Item (false, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.branch) >>=? fun ctxt ->
step ctxt bf rest
step_same ctxt bf rest
| Loop body, Item (true, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.loop_cycle) >>=? fun ctxt ->
step ctxt body rest >>=? fun (trans, ctxt) ->
step ctxt descr trans
step_same ctxt body rest >>=? fun (trans, ctxt) ->
step_same ctxt descr trans
| Loop _, Item (false, rest) ->
logged_return (rest, ctxt)
| Loop_left body, Item (L v, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.loop_cycle) >>=? fun ctxt ->
step ctxt body (Item (v, rest)) >>=? fun (trans, ctxt) ->
step ctxt descr trans
step_same ctxt body (Item (v, rest)) >>=? fun (trans, ctxt) ->
step_same ctxt descr trans
| Loop_left _, Item (R v, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.loop_cycle) >>=? fun ctxt ->
logged_return (Item (v, rest), ctxt)
| Dip b, Item (ign, rest) ->
Lwt.return (Gas.consume ctxt Interp_costs.stack_op) >>=? fun ctxt ->
step ctxt b rest >>=? fun (res, ctxt) ->
step_same ctxt b rest >>=? fun (res, ctxt) ->
logged_return (Item (ign, res), ctxt)
| Exec, Item (arg, Item (lam, rest)) ->
Lwt.return (Gas.consume ctxt Interp_costs.exec) >>=? fun ctxt ->
@ -827,7 +832,16 @@ let rec interp
logged_return (Item ((t,self), rest), ctxt)
| Amount, rest ->
Lwt.return (Gas.consume ctxt Interp_costs.amount) >>=? fun ctxt ->
logged_return (Item (amount, rest), ctxt) in
logged_return (Item (amount, rest), ctxt)
and interp
: type p r.
(?log: execution_trace ref ->
context ->
source: Contract.t -> payer:Contract.t -> self: Contract.t -> Tez.t ->
(p, r) lambda -> p ->
(r * context) tzresult Lwt.t)
= fun ?log ctxt ~source ~payer ~self amount (Lam (code, _)) arg ->
let stack = (Item (arg, Empty)) in
begin match log with
| None -> return_unit
@ -837,7 +851,7 @@ let rec interp
log := (code.loc, Gas.level ctxt, stack) :: !log ;
return_unit
end >>=? fun () ->
step ctxt code stack >>=? fun (Item (ret, Empty), ctxt) ->
step ctxt ~source ~payer ~self amount code stack >>=? fun (Item (ret, Empty), ctxt) ->
return (ret, ctxt)
(* ---- contract handling ---------------------------------------------------*)

View File

@ -61,3 +61,27 @@ val trace:
parameter: Script.expr ->
amount: Tez.t ->
(execution_result * execution_trace) tzresult Lwt.t
val interp:
(?log: execution_trace ref ->
context ->
source: Contract.t -> payer:Contract.t -> self: Contract.t -> Tez.t ->
('p, 'r) Script_typed_ir.lambda -> 'p ->
('r * context) tzresult Lwt.t)
type 'tys stack =
| Item : 'ty * 'rest stack -> ('ty * 'rest) stack
| Empty : Script_typed_ir.end_of_stack stack
type ex_descr_stack = Ex_descr_stack : (('a, 'b) Script_typed_ir.descr * 'a stack) -> ex_descr_stack
val step:
?log:execution_trace ref ->
context ->
source:Contract.t ->
self:Contract.t ->
payer:Contract.t ->
?visitor: (ex_descr_stack -> unit) ->
Tez.t -> ('b, 'a) Script_typed_ir.descr
-> 'b stack
-> ('a stack * context) tzresult Lwt.t

View File

@ -36,6 +36,7 @@ module Unparse_costs = Michelson_v1_gas.Cost_of.Unparse
type ex_comparable_ty = Ex_comparable_ty : 'a comparable_ty -> ex_comparable_ty
type ex_ty = Ex_ty : 'a ty -> ex_ty
type ex_stack_ty = Ex_stack_ty : 'a stack_ty -> ex_stack_ty
type ex_typed_value = Ex_typed_value : ('a Script_typed_ir.ty * 'a) -> ex_typed_value
type tc_context =
| Lambda : tc_context
@ -322,6 +323,7 @@ let namespace = function
| I_NIL
| I_NONE
| I_NOT
| I_NOP
| I_NOW
| I_OR
| I_PAIR
@ -2968,8 +2970,13 @@ let typecheck_data
(* ---- Unparsing (Typed IR -> Untyped expressions) --------------------------*)
let rec unparse_data
: type a. context -> unparsing_mode -> a ty -> a -> (Script.node * context) tzresult Lwt.t
= fun ctxt mode ty a ->
: type a. context -> ?mapper:(ex_typed_value -> Script.node option tzresult Lwt.t) ->
unparsing_mode -> a ty -> a -> (Script.node * context) tzresult Lwt.t
= fun ctxt ?(mapper = fun _ -> return None) mode ty a ->
mapper (Ex_typed_value (ty, a)) >>=? function
| Some s -> return (s, ctxt)
| None -> (
let unparse_same ctxt ty a = unparse_data ctxt ~mapper mode ty a in
Lwt.return (Gas.consume ctxt Unparse_costs.cycle) >>=? fun ctxt ->
match ty, a with
| Unit_t _, () ->
@ -3060,20 +3067,20 @@ let rec unparse_data
return (Bytes (-1, bytes), ctxt)
| Pair_t ((tl, _, _), (tr, _, _), _), (l, r) ->
Lwt.return (Gas.consume ctxt Unparse_costs.pair) >>=? fun ctxt ->
unparse_data ctxt mode tl l >>=? fun (l, ctxt) ->
unparse_data ctxt mode tr r >>=? fun (r, ctxt) ->
unparse_same ctxt tl l >>=? fun (l, ctxt) ->
unparse_same ctxt tr r >>=? fun (r, ctxt) ->
return (Prim (-1, D_Pair, [ l; r ], []), ctxt)
| Union_t ((tl, _), _, _), L l ->
Lwt.return (Gas.consume ctxt Unparse_costs.union) >>=? fun ctxt ->
unparse_data ctxt mode tl l >>=? fun (l, ctxt) ->
unparse_same ctxt tl l >>=? fun (l, ctxt) ->
return (Prim (-1, D_Left, [ l ], []), ctxt)
| Union_t (_, (tr, _), _), R r ->
Lwt.return (Gas.consume ctxt Unparse_costs.union) >>=? fun ctxt ->
unparse_data ctxt mode tr r >>=? fun (r, ctxt) ->
unparse_same ctxt tr r >>=? fun (r, ctxt) ->
return (Prim (-1, D_Right, [ r ], []), ctxt)
| Option_t ((t, _), _, _), Some v ->
Lwt.return (Gas.consume ctxt Unparse_costs.some) >>=? fun ctxt ->
unparse_data ctxt mode t v >>=? fun (v, ctxt) ->
unparse_same ctxt t v >>=? fun (v, ctxt) ->
return (Prim (-1, D_Some, [ v ], []), ctxt)
| Option_t _, None ->
Lwt.return (Gas.consume ctxt Unparse_costs.none) >>=? fun ctxt ->
@ -3082,7 +3089,7 @@ let rec unparse_data
fold_left_s
(fun (l, ctxt) element ->
Lwt.return (Gas.consume ctxt Unparse_costs.list_element) >>=? fun ctxt ->
unparse_data ctxt mode t element >>=? fun (unparsed, ctxt) ->
unparse_same ctxt t element >>=? fun (unparsed, ctxt) ->
return (unparsed :: l, ctxt))
([], ctxt)
items >>=? fun (items, ctxt) ->
@ -3092,7 +3099,7 @@ let rec unparse_data
fold_left_s
(fun (l, ctxt) item ->
Lwt.return (Gas.consume ctxt Unparse_costs.set_element) >>=? fun ctxt ->
unparse_data ctxt mode t item >>=? fun (item, ctxt) ->
unparse_same ctxt t item >>=? fun (item, ctxt) ->
return (item :: l, ctxt))
([], ctxt)
(set_fold (fun e acc -> e :: acc) set []) >>=? fun (items, ctxt) ->
@ -3102,16 +3109,34 @@ let rec unparse_data
fold_left_s
(fun (l, ctxt) (k, v) ->
Lwt.return (Gas.consume ctxt Unparse_costs.map_element) >>=? fun ctxt ->
unparse_data ctxt mode kt k >>=? fun (key, ctxt) ->
unparse_data ctxt mode vt v >>=? fun (value, ctxt) ->
unparse_same ctxt kt k >>=? fun (key, ctxt) ->
unparse_same ctxt vt v >>=? fun (value, ctxt) ->
return (Prim (-1, D_Elt, [ key ; value ], []) :: l, ctxt))
([], ctxt)
(map_fold (fun k v acc -> (k, v) :: acc) map []) >>=? fun (items, ctxt) ->
return (Micheline.Seq (-1, items), ctxt)
| Big_map_t (_kt, _kv, _), _map ->
| Big_map_t (kt, vt, _), map ->
if false then (
let kt = ty_of_comparable_ty kt in
fold_left_s
(fun (l, ctxt) (k, v) ->
Lwt.return (Gas.consume ctxt Unparse_costs.map_element) >>=? fun ctxt ->
match v with
| None -> return (l, ctxt)
| Some v -> (
unparse_same ctxt kt k >>=? fun (key, ctxt) ->
unparse_same ctxt vt v >>=? fun (value, ctxt) ->
return (Prim (-1, D_Elt, [ key ; value ], []) :: l, ctxt))
)
([], ctxt)
(map_fold (fun k v acc -> (k, v) :: acc) map.diff []) >>=? fun (items, ctxt) ->
return (Micheline.Seq (-1, String (-1, "...") :: items), ctxt)
) else (
return (Micheline.Seq (-1, []), ctxt)
)
| Lambda_t _, Lam (_, original_code) ->
unparse_code ctxt mode (root original_code)
)
(* Gas accounting may not be perfect in this function, as it is only called by RPCs. *)
and unparse_code ctxt mode = function

View File

@ -32,12 +32,15 @@ type ex_comparable_ty = Ex_comparable_ty : 'a Script_typed_ir.comparable_ty -> e
type ex_ty = Ex_ty : 'a Script_typed_ir.ty -> ex_ty
type ex_stack_ty = Ex_stack_ty : 'a Script_typed_ir.stack_ty -> ex_stack_ty
type ex_script = Ex_script : ('a, 'b) Script_typed_ir.script -> ex_script
type ex_typed_value = Ex_typed_value : ('a Script_typed_ir.ty * 'a) -> ex_typed_value
type unparsing_mode = Optimized | Readable
type type_logger =
int -> (Script.expr * Script.annot) list -> (Script.expr * Script.annot) list -> unit
val ty_of_comparable_ty : 'a Script_typed_ir.comparable_ty -> 'a Script_typed_ir.ty
(* ---- Sets and Maps -------------------------------------------------------*)
val empty_set : 'a Script_typed_ir.comparable_ty -> 'a Script_typed_ir.set
@ -77,12 +80,19 @@ val ty_eq :
'ta Script_typed_ir.ty -> 'tb Script_typed_ir.ty ->
(('ta Script_typed_ir.ty, 'tb Script_typed_ir.ty) eq * context) tzresult
val stack_ty_eq :
context -> int ->
'ta Script_typed_ir.stack_ty -> 'tb Script_typed_ir.stack_ty ->
(('ta Script_typed_ir.stack_ty, 'tb Script_typed_ir.stack_ty) eq * context) tzresult
val parse_data :
?type_logger: type_logger ->
context ->
'a Script_typed_ir.ty -> Script.node -> ('a * context) tzresult Lwt.t
val unparse_data :
context -> unparsing_mode -> 'a Script_typed_ir.ty -> 'a ->
context -> ?mapper:(ex_typed_value -> Script.node option tzresult Lwt.t)
-> unparsing_mode -> 'a Script_typed_ir.ty -> 'a ->
(Script.node * context) tzresult Lwt.t
val parse_ty :
@ -94,6 +104,30 @@ val parse_ty :
val unparse_ty :
context -> 'a Script_typed_ir.ty -> (Script.node * context) tzresult Lwt.t
val parse_storage_ty :
context ->
Script.node -> (ex_ty * context) tzresult
type tc_context =
| Lambda : tc_context
| Dip : 'a Script_typed_ir.stack_ty * tc_context -> tc_context
| Toplevel : { storage_type : 'sto Script_typed_ir.ty ; param_type : 'param Script_typed_ir.ty } -> tc_context
type 'bef judgement =
| Typed : ('bef, 'aft) Script_typed_ir.descr -> 'bef judgement
| Failed : { descr : 'aft. 'aft Script_typed_ir.stack_ty -> ('bef, 'aft) Script_typed_ir.descr } -> 'bef judgement
val parse_instr :
?type_logger: type_logger ->
tc_context -> context ->
Script.node -> 'bef Script_typed_ir.stack_ty -> ('bef judgement * context) tzresult Lwt.t
val parse_returning :
?type_logger: type_logger ->
tc_context -> context ->
'arg Script_typed_ir.ty * Script_typed_ir.var_annot option -> 'ret Script_typed_ir.ty -> Script.node ->
(('arg, 'ret) Script_typed_ir.lambda * context) tzresult Lwt.t
val parse_toplevel :
Script.expr -> (Script.node * Script.node * Script.node) tzresult