From 4dd1ef998800483f8126718a202ee2fdb175888f Mon Sep 17 00:00:00 2001 From: Fabrice Le Fessant Date: Tue, 23 May 2017 15:04:31 +0200 Subject: [PATCH] Michelson: replace all numbers with only `int` and `nat` --- src/Makefile | 2 +- src/Makefile.files | 2 + .../embedded/alpha/client_proto_programs.ml | 30 +- src/node/updater/environment.ml | 1 + src/proto/alpha/script_int_repr.ml | 252 ++-------- src/proto/alpha/script_int_repr.mli | 165 ++++--- src/proto/alpha/script_interpreter.ml | 264 ++++++----- src/proto/alpha/script_interpreter.mli | 4 - src/proto/alpha/script_ir_translator.ml | 442 +++++++----------- src/proto/alpha/script_repr.mli | 11 + src/proto/alpha/script_typed_ir.ml | 147 +++--- src/proto/environment/z.mli | 76 +++ 12 files changed, 646 insertions(+), 750 deletions(-) create mode 100644 src/proto/environment/z.mli diff --git a/src/Makefile b/src/Makefile index 3a64e1cad..093e5900c 100644 --- a/src/Makefile +++ b/src/Makefile @@ -371,7 +371,7 @@ proto/embedded_proto_%.cmxa: \ CLIENT_PROTO_INCLUDES := \ minutils utils compiler node/updater node/db node/net node/shell client \ - $(shell ocamlfind query lwt ocplib-json-typed sodium) + $(shell ocamlfind query lwt ocplib-json-typed sodium zarith) proto/client_embedded_proto_%.cmxa: \ ${TZCOMPILER} \ diff --git a/src/Makefile.files b/src/Makefile.files index fde10535c..7a7bf9d21 100644 --- a/src/Makefile.files +++ b/src/Makefile.files @@ -12,6 +12,7 @@ $(addprefix proto/environment/, \ buffer.mli \ format.mli \ \ + z.mli \ lwt_sequence.mli lwt.mli lwt_list.mli \ \ mBytes.mli \ @@ -114,6 +115,7 @@ UTILS_LIB_IMPLS := \ UTILS_PACKAGES := \ ${MINUTILS_PACKAGES} \ + zarith \ base64 \ calendar \ ezjsonm \ diff --git a/src/client/embedded/alpha/client_proto_programs.ml b/src/client/embedded/alpha/client_proto_programs.ml index 3ac378ab1..c1f670e76 100644 --- a/src/client/embedded/alpha/client_proto_programs.ml +++ b/src/client/embedded/alpha/client_proto_programs.ml @@ -197,7 +197,6 @@ let collect_error_locations errs = | Invalid_case (loc, _) | Invalid_kind (loc, _, _) | Fail_not_in_tail_position loc - | Undefined_cast (loc, _, _) | Undefined_binop (loc, _, _, _) | Undefined_unop (loc, _, _) | Bad_return (loc, _, _) @@ -208,8 +207,7 @@ let collect_error_locations errs = | Invalid_contract (loc, _) | Comparable_type_expected (loc, _) | Overflow loc - | Reject loc - | Division_by_zero loc) :: rest -> + | Reject loc) :: rest -> collect (loc :: acc) rest | _ :: rest -> collect acc rest in collect [] errs @@ -336,13 +334,6 @@ let report_errors cctxt errs = cctxt.warning "%aThe FAIL instruction must appear in a tail position." print_loc loc - | Undefined_cast (loc, tya, tyb) -> - cctxt.warning - "@[@[%atype cast is undefined from@ %a@]@ \ - @[to@ %a.@]@]" - print_loc loc - print_ty tya - print_ty tyb | Undefined_binop (loc, name, tya, tyb) -> cctxt.warning "@[@[%aoperator %s is undefined between@ %a@]@ \ @@ -404,24 +395,6 @@ let report_errors cctxt errs = print_loc loc >>= fun () -> cctxt.warning "@[@[Type@ %a@]@ is not comparable.@]" print_ty ty - | Bad_sign ty -> - begin match ty with - | Int_t kind -> - let signed = match kind with - | Script_int.Int8 -> true - | Script_int.Int16 -> true - | Script_int.Int32 -> true - | Script_int.Int64 -> true - | Script_int.Uint8 -> false - | Script_int.Uint16 -> false - | Script_int.Uint32 -> false - | Script_int.Uint64 -> false in - if signed then - cctxt.warning "Unsigned integer type expected." - else - cctxt.warning "Signed integer type expected." - | _ -> assert false - end | Inconsistent_types (tya, tyb) -> cctxt.warning "@[@[Type@ %a@]@ \ @@ -429,7 +402,6 @@ let report_errors cctxt errs = print_ty tya print_ty tyb | Reject _ -> cctxt.warning "Script reached FAIL instruction" | Overflow _ -> cctxt.warning "Unexpected arithmetic overflow" - | Division_by_zero _ -> cctxt.warning "Division by zero" | err -> cctxt.warning "%a" Local_environment.Environment.Error_monad.pp_print_error [ err ] in diff --git a/src/node/updater/environment.ml b/src/node/updater/environment.ml index b631f8135..07790ee86 100644 --- a/src/node/updater/environment.ml +++ b/src/node/updater/environment.ml @@ -243,6 +243,7 @@ module Make(Param : sig val name: string end)() = struct module Buffer = Buffer module Format = Format module Hex_encode = Hex_encode + module Z = Z module Lwt_sequence = Lwt_sequence module Lwt = Lwt module Lwt_list = Lwt_list diff --git a/src/proto/alpha/script_int_repr.ml b/src/proto/alpha/script_int_repr.ml index e97e2ae66..b8cceb801 100644 --- a/src/proto/alpha/script_int_repr.ml +++ b/src/proto/alpha/script_int_repr.ml @@ -7,224 +7,60 @@ (* *) (**************************************************************************) -(* sign *) -type signed = Signed -type unsigned = Unsigned +type n = Natural_tag +type z = Integer_tag +type 't num = Z.t -(* length *) -type eight = Eight -type sixteen = Sixteen -type thirtytwo = Thirtytwo -type sixtyfour = Sixtyfour +let compare x y = Z.compare x y -(* int values *) -type ('s, 'l) int_val = Int of repr and repr = int64 +let zero = Z.zero +let zero_n = Z.zero -(* types *) -and ('s, 'l) int_kind = - | Int8 : (signed, eight) int_kind - | Uint8 : (unsigned, eight) int_kind - | Int16 : (signed, sixteen) int_kind - | Uint16 : (unsigned, sixteen) int_kind - | Int32 : (signed, thirtytwo) int_kind - | Uint32 : (unsigned, thirtytwo) int_kind - | Int64 : (signed, sixtyfour) int_kind - | Uint64 : (unsigned, sixtyfour) int_kind +let to_string x = Z.to_string x +let of_string s = try Some (Z.of_string s) with _ -> None -(* homogeneous operator types *) -type ('s, 'l) binop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -> ('s, 'l) int_val -type ('s, 'l) unop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -type ('s, 'l) checked_binop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -> ('s, 'l) int_val option -type ('s, 'l) checked_unop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val option -type ('s, 'l) shift = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, eight) int_val -> ('s, 'l) int_val +let to_int64 x = try Some (Z.to_int64 x) with _ -> None +let of_int64 n = Z.of_int64 n -(* cast operators *) -let cast - : type tos tol. (tos, tol) int_kind -> (_, _) int_val -> (tos, tol) int_val - = fun to_kind (Int v) -> - let (land) = Int64.logand - and (lor) = Int64.logor - and (=) = Compare.Int64.(=) in - match to_kind with - | Int8 when v land 0x80L = 0x80L -> - Int ((v land 0x000000FFL) lor 0xFFFFFFFFFFFFFF00L) - | Int8 -> - Int (v land 0x000000FFL) - | Uint8 -> - Int (v land 0x000000FFL) - | Int16 when v land 0x8000L = 0x8000L -> - Int ((v land 0x0000FFFFL) lor 0xFFFFFFFFFFFF0000L) - | Int16 -> - Int (v land 0x0000FFFFL) - | Uint16 -> - Int (v land 0x0000FFFFL) - | Int32 when v land 0x80000000L = 0x80000000L -> - Int ((v land 0xFFFFFFFFL) lor 0xFFFFFFFF00000000L) - | Int32 -> - Int (v land 0xFFFFFFFFL) - | Uint32 -> - Int (v land 0xFFFFFFFFL) - | Int64 -> Int v - | Uint64 -> Int v +let to_int x = try Some (Z.to_int x) with _ -> None +let of_int n = Z.of_int n -let checked_cast - : type tos tol. (tos, tol) int_kind -> (_, _) int_val -> (tos, tol) int_val option - = fun to_kind (Int v as arg) -> - let Int casted as res = cast to_kind arg in - if Compare.Int64.(casted <> v) then None else Some res +let add x y = Z.add x y +let sub x y = Z.sub x y +let mul x y = Z.mul x y -(* to native int64s *) -let to_int64 _ (Int v) = - v -let of_int64 k v = - cast k (Int v) -let checked_of_int64 k v = - checked_cast k (Int v) +let ediv x y = + try + let (q, r) = Z.ediv_rem x y in + Some (q, r) + with _ -> None -(* arithmetics *) -let add kind (Int va) (Int vb) = - of_int64 kind (Int64.add va vb) -let sub kind (Int va) (Int vb) = - of_int64 kind (Int64.sub va vb) -let mul : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val - = fun kind (Int va) (Int vb) -> let r = Int64.mul va vb in match kind with - | Int8 -> of_int64 Int8 r - | Uint8 -> of_int64 Uint8 r - | Int16 -> of_int64 Int16 r - | Uint16 -> of_int64 Uint16 r - | Int32 -> of_int64 Int32 r - | Uint32 -> of_int64 Uint32 r - | Int64 -> of_int64 Int64 r - | Uint64 -> invalid_arg "Script_int.mul" -let div : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val - = fun kind (Int va) (Int vb) -> let r = Int64.div va vb in match kind with - | Int8 -> of_int64 Int8 r - | Uint8 -> of_int64 Uint8 r - | Int16 -> of_int64 Int16 r - | Uint16 -> of_int64 Uint16 r - | Int32 -> of_int64 Int32 r - | Uint32 -> of_int64 Uint32 r - | Int64 -> of_int64 Int64 r - | Uint64 -> invalid_arg "Script_int.div" -let rem : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val - = fun kind (Int va) (Int vb) -> let r = Int64.rem va vb in match kind with - | Int8 -> of_int64 Int8 r - | Uint8 -> of_int64 Uint8 r - | Int16 -> of_int64 Int16 r - | Uint16 -> of_int64 Uint16 r - | Int32 -> of_int64 Int32 r - | Uint32 -> of_int64 Uint32 r - | Int64 -> of_int64 Int64 r - | Uint64 -> invalid_arg "Script_int.rem" -let neg kind (Int v) = - of_int64 kind (Int64.neg v) -let abs kind (Int v) = - of_int64 kind (Int64.abs v) +let add_n = add +let mul_n = mul +let ediv_n = ediv -(* bitwise logic *) -let logand _ (Int va) (Int vb) = - Int (Int64.logand va vb) -let logor _ (Int va) (Int vb) = - Int (Int64.logor va vb) -let logxor kind (Int va) (Int vb) = - cast kind (Int (Int64.logxor va vb)) -let lognot kind (Int v) = - cast kind (Int (Int64.lognot v)) -let logsl kind (Int va) (Int vb) = - cast kind (Int (Int64.shift_left va (Int64.to_int vb))) -let logsr _ (Int va) (Int vb) = - Int (Int64.shift_right_logical va (Int64.to_int vb)) +let abs x = Z.abs x +let neg x = Z.neg x +let int x = x -(* sign aware comparison *) -let compare - : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (signed, sixtyfour) int_val - = fun kind (Int va) (Int vb) -> - let cmp = match kind with - | Int8 -> Compare.Int64.compare va vb - | Uint8 -> Compare.Uint64.compare va vb - | Int16 -> Compare.Int64.compare va vb - | Uint16 -> Compare.Uint64.compare va vb - | Int32 -> Compare.Int64.compare va vb - | Uint32 -> Compare.Uint64.compare va vb - | Int64 -> Compare.Int64.compare va vb - | Uint64 -> Compare.Uint64.compare va vb in - Int Compare.Int.(if cmp = 0 then 0L else if cmp > 0 then 1L else -1L) +let shift_left x y = + if Compare.Int.(Z.compare y (Z.of_int 256) > 0) then + None + else + let y = Z.to_int y in + Some (Z.shift_left x y) -let equal kind va vb = - Compare.Int64.(to_int64 kind va = to_int64 kind vb) +let shift_right x y = + if Compare.Int.(Z.compare y (Z.of_int 256) > 0) then + None + else + let y = Z.to_int y in + Some (Z.shift_right x y) -(* checked arithmetics *) -let checked_add : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val option - = fun kind (Int va) (Int vb) -> let r = Int64.add va vb in match kind with - | Int8 -> checked_of_int64 Int8 r - | Uint8 -> checked_of_int64 Uint8 r - | Int16 -> checked_of_int64 Int16 r - | Uint16 -> checked_of_int64 Uint16 r - | Int32 -> checked_of_int64 Int32 r - | Uint32 -> checked_of_int64 Uint32 r - | Int64 when Compare.Int.(Compare.Int64.compare r va < 0) -> None - | Int64 -> Some (Int r) - | Uint64 when Compare.Int.(Compare.Uint64.compare r va < 0) -> None - | Uint64 -> Some (Int r) +let shift_left_n = shift_left +let shift_right_n = shift_right -let checked_sub : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val option - = fun kind (Int va) (Int vb) -> let r = Int64.sub va vb in match kind with - | Int8 -> checked_of_int64 Int8 r - | Uint8 -> checked_of_int64 Uint8 r - | Int16 -> checked_of_int64 Int16 r - | Uint16 -> checked_of_int64 Uint16 r - | Int32 -> checked_of_int64 Int32 r - | Uint32 -> checked_of_int64 Uint32 r - | Int64 when Compare.Int64.(vb >= 0L) -> - if Compare.Int.(Compare.Int64.compare r va <= 0) then Some (Int r) else None - | Int64 -> - if Compare.Int.(Compare.Int64.compare r va >= 0) then Some (Int r) else None - | Uint64 when Compare.Int.(Compare.Uint64.compare r va > 0) -> None - | Uint64 -> Some (Int r) - -let checked_neg : type l. (signed, l) int_kind -> (signed, l) int_val -> (signed, l) int_val option - = fun kind (Int v) -> let r = Int64.neg v in match kind with - | Int8 -> checked_of_int64 Int8 r - | Int16 -> checked_of_int64 Int16 r - | Int32 -> checked_of_int64 Int32 r - | Int64 when Compare.Int64.(v = Int64.min_int) -> None - | Int64 -> Some (Int r) - -let checked_abs : type l. (signed, l) int_kind -> (signed, l) int_val -> (signed, l) int_val option - = fun kind (Int v) -> let r = Int64.abs v in match kind with - | Int8 -> checked_of_int64 Int8 r - | Int16 -> checked_of_int64 Int16 r - | Int32 -> checked_of_int64 Int32 r - | Int64 when Compare.Int64.(v = Int64.min_int) -> None - | Int64 -> Some (Int r) - -let checked_mul : type s l. (s, l) int_kind -> (s, l) int_val -> (s, l) int_val -> (s, l) int_val option - = fun kind (Int va) (Int vb) -> let r = Int64.mul va vb in match kind with - | Int8 -> checked_of_int64 Int8 r - | Uint8 -> checked_of_int64 Uint8 r - | Int16 -> checked_of_int64 Int16 r - | Uint16 -> checked_of_int64 Uint16 r - | Int32 -> checked_of_int64 Int32 r - | Uint32 -> checked_of_int64 Uint32 r - | Int64 -> - if Compare.Int64.(vb = 0L || va = 0L) then Some (Int r) - else if Compare.Int64.(r = 0L) then None - else if Compare.Int64.(Int64.div r va = vb) then Some (Int r) - else None - | Uint64 -> invalid_arg "Script_int.checked_mul" - -let string_of_int_kind (type s) (type l) (kind:(s,l) int_kind) = - match kind with - | Int8 -> "int8" - | Uint8 -> "uint8" - | Int16 -> "int16" - | Uint16 -> "uint16" - | Int32 -> "int32" - | Uint32 -> "uint32" - | Int64 -> "int64" - | Uint64 -> "uint64" +let logor x y = Z.logor x y +let logxor x y = Z.logxor x y +let logand x y = Z.logand x y +let lognot x = Z.lognot x diff --git a/src/proto/alpha/script_int_repr.mli b/src/proto/alpha/script_int_repr.mli index 9f338e6d6..581e5730a 100644 --- a/src/proto/alpha/script_int_repr.mli +++ b/src/proto/alpha/script_int_repr.mli @@ -7,78 +7,113 @@ (* *) (**************************************************************************) -(* sign *) -type signed = Signed -type unsigned = Unsigned +(** The types for arbitraty precision integers in Michelson. + The type variable ['t] is always [n] or [z], + [n num] and [z num] are incompatible. -(* length *) -type eight = Eight -type sixteen = Sixteen -type thirtytwo = Thirtytwo -type sixtyfour = Sixtyfour + This is internally a [Z.t]. + This module mostly adds signedness preservation guarantees. *) +type 't num -(* int values *) -type ('s, 'l) int_val = Int of repr and repr +(** Flag for natural numbers. *) +and n = Natural_tag -(* int types *) -type ('s, 'l) int_kind = - | Int8 : (signed, eight) int_kind - | Uint8 : (unsigned, eight) int_kind - | Int16 : (signed, sixteen) int_kind - | Uint16 : (unsigned, sixteen) int_kind - | Int32 : (signed, thirtytwo) int_kind - | Uint32 : (unsigned, thirtytwo) int_kind - | Int64 : (signed, sixtyfour) int_kind - | Uint64 : (unsigned, sixtyfour) int_kind +(** Flag for relative numbers. *) +and z = Integer_tag -(* homogeneous operator types *) -type ('s, 'l) binop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -> ('s, 'l) int_val -type ('s, 'l) unop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -type ('s, 'l) checked_binop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val -> ('s, 'l) int_val option -type ('s, 'l) checked_unop = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, 'l) int_val option -type ('s, 'l) shift = - ('s, 'l) int_kind -> ('s, 'l) int_val -> ('s, eight) int_val -> ('s, 'l) int_val +(** Natural zero. *) +val zero_n : n num -(* cast operators *) -val cast : ('tos, 'tol) int_kind -> ('s, 'l) int_val -> ('tos, 'tol) int_val -val checked_cast : ('tos, 'tol) int_kind -> ('s, 'l) int_val -> ('tos, 'tol) int_val option +(** Relative zero. *) +val zero : z num -(* to native int64s *) -val to_int64 : ('s, 'l) int_kind -> ('s, 'l) int_val -> int64 -val of_int64 : ('s, 'l) int_kind -> int64 -> ('s, 'l) int_val -val checked_of_int64 : ('s, 'l) int_kind -> int64 -> ('s, 'l) int_val option +(** Compare two numbers as if they were *) +val compare : 'a num -> 'a num -> int -(* arithmetics *) -val abs : (signed, 'l) unop -val neg : (signed, 'l) unop -val add : ('s, 'l) binop -val sub : ('s, 'l) binop -val mul : ('s, 'l) binop -val div : ('s, 'l) binop -val rem : ('s, 'l) binop -val checked_abs : (signed, 'l) checked_unop -val checked_neg : (signed, 'l) checked_unop -val checked_add : ('s, 'l) checked_binop -val checked_sub : ('s, 'l) checked_binop -val checked_mul : ('s, 'l) checked_binop +(** Conversion to an OCaml [string] in decimal notation. *) +val to_string : _ num -> string -(* bitwise logic *) -val logand : (unsigned, 'l) binop -val logor : (unsigned, 'l) binop -val logxor : (unsigned, 'l) binop -val lognot : (unsigned, 'l) unop -val logsl : (unsigned, 'l) shift -val logsr : (unsigned, 'l) shift +(** Conversion from an OCaml [string]. + Returns [None] in case of an invalid notation. + Supports [+] and [-] sign modifiers, and [0x], [0o] and [0b] base modifiers. *) +val of_string : string -> z num option -(* sign aware comparison *) -val compare : ('s, 'l) int_kind -> - ('s, 'l) int_val -> ('s, 'l) int_val -> (signed, sixtyfour) int_val -val equal : ('s, 'l) int_kind -> - ('s, 'l) int_val -> ('s, 'l) int_val -> bool +(** Conversion to an OCaml [int64], returns [None] on overflow. *) +val to_int64 : _ num -> int64 option -(* utilities *) -val string_of_int_kind : ('s, 'l) int_kind -> string +(** Conversion from an OCaml [int]. *) +val of_int64 : int64 -> z num + +(** Conversion to an OCaml [int], returns [None] on overflow. *) +val to_int : _ num -> int option + +(** Conversion from an OCaml [int64]. *) +val of_int : int -> z num + +(** Addition between naturals. *) +val add_n : n num -> n num -> n num + +(** Multiplication between naturals. *) +val mul_n : n num -> n num -> n num + +(** Euclidean division between naturals. + [ediv_n n d] returns [None] if divisor is zero, + or [Some (q, r)] where [n = d * q + r] and [[0 <= r < d]] otherwise. *) +val ediv_n: n num -> n num -> (n num * n num) option + +(** Sign agnostic addition. + Use {!add_n} when working with naturals to preserve the sign. *) +val add : _ num -> _ num -> z num + +(** Sign agnostic subtraction. + Use {!sub_n} when working with naturals to preserve the sign. *) +val sub : _ num -> _ num -> z num + +(** Sign agnostic multiplication. + Use {!mul_n} when working with naturals to preserve the sign. *) +val mul : _ num -> _ num -> z num + +(** Sign agnostic euclidean division. + [ediv n d] returns [None] if divisor is zero, + or [Some (q, r)] where [n = d * q + r] and [[0 <= r < |d|]] otherwise. + Use {!ediv_n} when working with naturals to preserve the sign. *) +val ediv: _ num -> _ num -> (z num * n num) option + +(** Compute the absolute value of a relative, turning it into a natural. *) +val abs : z num -> n num + +(** Negates a number. *) +val neg : _ num -> z num + +(** Turns a natural into a relative, not changing its value. *) +val int : n num -> z num + +(** Reverses each bit in the representation of the number. + Also applies to the sign. *) +val lognot : _ num -> z num + + +(** Shifts the natural to the left of a number of bits between 0 and 256. + Returns [None] if the amount is too high. *) +val shift_left_n : n num -> n num -> n num option + +(** Shifts the natural to the right of a number of bits between 0 and 256. + Returns [None] if the amount is too high. *) +val shift_right_n : n num -> n num -> n num option + +(** Shifts the number to the left of a number of bits between 0 and 256. + Returns [None] if the amount is too high. *) +val shift_left : 'a num -> n num -> 'a num option + +(** Shifts the number to the right of a number of bits between 0 and 256. + Returns [None] if the amount is too high. *) +val shift_right : 'a num -> n num -> 'a num option + +(** Applies a boolean or operation to each bit. *) +val logor : n num -> n num -> n num + +(** Applies a boolean and operation to each bit. *) +val logand : n num -> n num -> n num + +(** Applies a boolean xor operation to each bit. *) +val logxor : n num -> n num -> n num diff --git a/src/proto/alpha/script_interpreter.ml b/src/proto/alpha/script_interpreter.ml index 78a7af5d3..e4a3ef4f0 100644 --- a/src/proto/alpha/script_interpreter.ml +++ b/src/proto/alpha/script_interpreter.ml @@ -8,7 +8,6 @@ (**************************************************************************) open Tezos_context -open Script_int open Script open Script_typed_ir open Script_ir_translator @@ -21,7 +20,6 @@ let dummy_storage_fee = Tez.fifty_cents type error += Quota_exceeded type error += Overflow of Script.location type error += Reject of Script.location -type error += Division_by_zero of Script.location type error += Runtime_contract_error : Contract.t * Script.expr * _ ty * _ ty * _ ty -> error let () = @@ -46,14 +44,6 @@ let () = (obj1 (req "location" Script.location_encoding)) (function Overflow loc -> Some loc | _ -> None) (fun loc -> Overflow loc) ; - register_error_kind - `Permanent - ~id:"divisionByZeroRuntimeError" - ~title: "Division by zero (runtime script error)" - ~description: "" - (obj1 (req "location" Script.location_encoding)) - (function Division_by_zero loc -> Some loc | _ -> None) - (fun loc -> Division_by_zero loc) ; register_error_kind `Temporary ~id:"scriptRejectedRuntimeError" @@ -230,20 +220,26 @@ let rec interp | Map_update, Item (k, Item (v, Item (map, rest))) -> logged_return (Item (map_update k v map, rest), qta - 1, ctxt) (* timestamp operations *) - | Add_seconds_to_timestamp kind, Item (n, Item (t, rest)) -> - let n = Script_int.to_int64 kind n in - Lwt.return - (Period.of_seconds n >>? fun p -> - Timestamp.(t +? p) >>? fun res -> - Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res -> - logged_return res - | Add_timestamp_to_seconds kind, Item (t, Item (n, rest)) -> - let n = Script_int.to_int64 kind n in - Lwt.return - (Period.of_seconds n >>? fun p -> - Timestamp.(t +? p) >>? fun res -> - Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res -> - logged_return res + | Add_seconds_to_timestamp, Item (n, Item (t, rest)) -> + begin match Script_int.to_int64 n with + | None -> fail (Overflow loc) + | Some n -> + Lwt.return + (Period.of_seconds n >>? fun p -> + Timestamp.(t +? p) >>? fun res -> + Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res -> + logged_return res + end + | Add_timestamp_to_seconds, Item (t, Item (n, rest)) -> + begin match Script_int.to_int64 n with + | None -> fail (Overflow loc) + | Some n -> + Lwt.return + (Period.of_seconds n >>? fun p -> + Timestamp.(t +? p) >>? fun res -> + Ok (Item (res, rest), qta - 1, ctxt)) >>=? fun res -> + logged_return res + end (* string operations *) | Concat, Item (x, Item (y, rest)) -> logged_return (Item (x ^ y, rest), qta - 1, ctxt) @@ -254,12 +250,22 @@ let rec interp | Sub_tez, Item (x, Item (y, rest)) -> Lwt.return Tez.(x -? y) >>=? fun res -> logged_return (Item (res, rest), qta - 1, ctxt) - | Mul_tez kind, Item (x, Item (y, rest)) -> - Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res -> - logged_return (Item (res, rest), qta - 1, ctxt) - | Mul_tez' kind, Item (y, Item (x, rest)) -> - Lwt.return Tez.(x *? Script_int.to_int64 kind y) >>=? fun res -> - logged_return (Item (res, rest), qta - 1, ctxt) + | Mul_teznat, Item (x, Item (y, rest)) -> + 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) + end + | Mul_nattez, Item (y, Item (x, rest)) -> + 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) + end (* boolean operations *) | Or, Item (x, Item (y, rest)) -> logged_return (Item (x || y, rest), qta - 1, ctxt) @@ -270,63 +276,98 @@ let rec interp | Not, Item (x, rest) -> logged_return (Item (not x, rest), qta - 1, ctxt) (* integer operations *) - | Checked_abs_int kind, Item (x, rest) -> - begin match Script_int.checked_abs kind x with + | Abs_int, Item (x, rest) -> + logged_return (Item (Script_int.abs x, rest), qta - 1, ctxt) + | Int_nat, Item (x, rest) -> + logged_return (Item (Script_int.int x, rest), qta - 1, ctxt) + | Neg_int, Item (x, rest) -> + logged_return (Item (Script_int.neg x, rest), qta - 1, ctxt) + | Neg_nat, Item (x, rest) -> + logged_return (Item (Script_int.neg x, rest), qta - 1, ctxt) + | Add_intint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt) + | Add_intnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt) + | Add_natint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.add x y, rest), qta - 1, ctxt) + | Add_natnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.add_n x y, rest), qta - 1, ctxt) + | Sub_int, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.sub x y, rest), qta - 1, ctxt) + | Mul_intint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt) + | Mul_intnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt) + | Mul_natint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.mul x y, rest), qta - 1, ctxt) + | Mul_natnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.mul_n x y, rest), qta - 1, ctxt) + + | Ediv_teznat, Item (x, Item (y, rest)) -> + let x = Script_int.of_int64 (Tez.to_cents 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_cents q, Tez.of_cents 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) + + | Ediv_tez, Item (x, Item (y, rest)) -> + let x = Script_int.abs (Script_int.of_int64 (Tez.to_cents x)) in + let y = Script_int.abs (Script_int.of_int64 (Tez.to_cents 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_cents r with + | None -> assert false (* Cannot overflow *) + | Some r -> r in + logged_return (Item (Some (q, r), rest), qta -1, ctxt) + end + + | Ediv_intint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt) + | Ediv_intnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt) + | Ediv_natint, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.ediv x y, rest), qta -1, ctxt) + | Ediv_natnat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.ediv_n x y, rest), qta -1, ctxt) + | Lsl_nat, Item (x, Item (y, rest)) -> + begin match Script_int.shift_left_n x y with | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) + | Some r -> logged_return (Item (r, rest), qta - 1, ctxt) end - | Checked_neg_int kind, Item (x, rest) -> - begin match Script_int.checked_neg kind x with + | Lsr_nat, Item (x, Item (y, rest)) -> + begin match Script_int.shift_right_n x y with | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) + | Some r -> logged_return (Item (r, rest), qta - 1, ctxt) end - | Checked_add_int kind, Item (x, Item (y, rest)) -> - begin match Script_int.checked_add kind x y with - | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) - end - | Checked_sub_int kind, Item (x, Item (y, rest)) -> - begin match Script_int.checked_sub kind x y with - | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) - end - | Checked_mul_int kind, Item (x, Item (y, rest)) -> - begin match Script_int.checked_mul kind x y with - | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) - end - | Abs_int kind, Item (x, rest) -> - logged_return (Item (Script_int.abs kind x, rest), qta - 1, ctxt) - | Neg_int kind, Item (x, rest) -> - logged_return (Item (Script_int.neg kind x, rest), qta - 1, ctxt) - | Add_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.add kind x y, rest), qta - 1, ctxt) - | Sub_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.sub kind x y, rest), qta - 1, ctxt) - | Mul_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.mul kind x y, rest), qta - 1, ctxt) - | Div_int kind, Item (x, Item (y, rest)) -> - if Compare.Int64.(Script_int.to_int64 kind y = 0L) then - fail (Division_by_zero loc) - else - logged_return (Item (Script_int.div kind x y, rest), qta - 1, ctxt) - | Mod_int kind, Item (x, Item (y, rest)) -> - if Compare.Int64.(Script_int.to_int64 kind y = 0L) then - fail (Division_by_zero loc) - else - logged_return (Item (Script_int.rem kind x y, rest), qta - 1, ctxt) - | Lsl_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.logsl kind x y, rest), qta - 1, ctxt) - | Lsr_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.logsr kind x y, rest), qta - 1, ctxt) - | Or_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.logor kind x y, rest), qta - 1, ctxt) - | And_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.logand kind x y, rest), qta - 1, ctxt) - | Xor_int kind, Item (x, Item (y, rest)) -> - logged_return (Item (Script_int.logxor kind x y, rest), qta - 1, ctxt) - | Not_int kind, Item (x, rest) -> - logged_return (Item (Script_int.lognot kind x, rest), qta - 1, ctxt) + | Or_nat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.logor x y, rest), qta - 1, ctxt) + | And_nat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.logand x y, rest), qta - 1, ctxt) + | Xor_nat, Item (x, Item (y, rest)) -> + logged_return (Item (Script_int.logxor x y, rest), qta - 1, ctxt) + | Not_int, Item (x, rest) -> + logged_return (Item (Script_int.lognot x, rest), qta - 1, ctxt) + | Not_nat, Item (x, rest) -> + logged_return (Item (Script_int.lognot x, rest), qta - 1, ctxt) (* control *) | Seq (hd, tl), stack -> step origination qta ctxt hd stack >>=? fun (trans, qta, ctxt, origination) -> @@ -355,60 +396,57 @@ let rec interp (* comparison *) | Compare Bool_key, Item (a, Item (b, rest)) -> let cmpres = Compare.Bool.compare a b in - let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in + let cmpres = Script_int.of_int cmpres in logged_return (Item (cmpres, rest), qta - 1, ctxt) | Compare String_key, Item (a, Item (b, rest)) -> let cmpres = Compare.String.compare a b in - let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in + let cmpres = Script_int.of_int cmpres in logged_return (Item (cmpres, rest), qta - 1, ctxt) | Compare Tez_key, Item (a, Item (b, rest)) -> let cmpres = Tez.compare a b in - let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in + let cmpres = Script_int.of_int cmpres in logged_return (Item (cmpres, rest), qta - 1, ctxt) - | Compare (Int_key kind), Item (a, Item (b, rest)) -> - let cmpres = Script_int.compare kind a b in + | 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) + | 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) | Compare Key_key, Item (a, Item (b, rest)) -> let cmpres = Ed25519.Public_key_hash.compare a b in - let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in + let cmpres = Script_int.of_int cmpres in logged_return (Item (cmpres, rest), qta - 1, ctxt) | Compare Timestamp_key, Item (a, Item (b, rest)) -> let cmpres = Timestamp.compare a b in - let cmpres = Script_int.of_int64 Int64 (Int64.of_int cmpres) in + let cmpres = Script_int.of_int cmpres in logged_return (Item (cmpres, rest), qta - 1, ctxt) (* comparators *) | Eq, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres = 0L) in + 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) | Neq, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres <> 0L) in + 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) | Lt, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres < 0L) in - logged_return (Item (cmpres, rest), qta - 1, ctxt) - | Gt, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres > 0L) in + 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) | Le, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres <= 0L) in + 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) + | 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) | Ge, Item (cmpres, rest) -> - let cmpres = Script_int.to_int64 Int64 cmpres in - let cmpres = Compare.Int64.(cmpres >= 0L) in + 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) - (* casts *) - | Checked_int_of_int (_, kt), Item (v, rest) -> - begin match Script_int.checked_cast kt v with - | None -> fail (Overflow loc) - | Some res -> logged_return (Item (res, rest), qta - 1, ctxt) - end - | Int_of_int (_, kt), Item (v, rest) -> - logged_return (Item (Script_int.cast kt v, rest), qta - 1, ctxt) (* protocol *) | Manager, Item ((_, _, contract), rest) -> Contract.get_manager ctxt contract >>=? fun manager -> @@ -506,7 +544,7 @@ let rec interp let hash = Script.hash_expr (unparse_data ty v) in logged_return (Item (hash, rest), qta - 1, ctxt) | Steps_to_quota, rest -> - let steps = Script_int.of_int64 Uint32 (Int64.of_int qta) in + let steps = Script_int.abs (Script_int.of_int qta) in logged_return (Item (steps, rest), qta - 1, ctxt) | Source (ta, tb), rest -> logged_return (Item ((ta, tb, orig), rest), qta - 1, ctxt) diff --git a/src/proto/alpha/script_interpreter.mli b/src/proto/alpha/script_interpreter.mli index 5d8faa92b..96f53370c 100644 --- a/src/proto/alpha/script_interpreter.mli +++ b/src/proto/alpha/script_interpreter.mli @@ -13,15 +13,11 @@ open Script_typed_ir type error += Quota_exceeded type error += Overflow of Script.location type error += Reject of Script.location -type error += Division_by_zero of Script.location type error += Runtime_contract_error : Contract.t * Script.expr * _ ty * _ ty * _ ty -> error val dummy_code_fee : Tez.t val dummy_storage_fee : Tez.t -(* calling convention : - ((amount, arg), globals)) -> (ret, globals) *) - val execute: Contract.origination_nonce -> Contract.t -> Contract.t -> Tezos_context.t -> diff --git a/src/proto/alpha/script_ir_translator.ml b/src/proto/alpha/script_ir_translator.ml index 4277c6b83..3d9bb2602 100644 --- a/src/proto/alpha/script_ir_translator.ml +++ b/src/proto/alpha/script_ir_translator.ml @@ -8,7 +8,6 @@ (**************************************************************************) open Tezos_context -open Script_int open Script open Script_typed_ir @@ -28,7 +27,6 @@ type error += Invalid_kind of Script.location * kind list * kind (* Instruction typing errors *) type error += Fail_not_in_tail_position of Script.location -type error += Undefined_cast : Script.location * _ ty * _ ty -> error type error += Undefined_binop : Script.location * string * _ ty * _ ty -> error type error += Undefined_unop : Script.location * string * _ ty -> error type error += Bad_return : Script.location * _ stack_ty * _ ty -> error @@ -43,7 +41,6 @@ type error += Invalid_constant : Script.location * Script.expr * _ ty -> error type error += Invalid_contract of Script.location * Contract.t type error += Comparable_type_expected : Script.location * _ ty -> error type error += Inconsistent_types : _ ty * _ ty -> error -type error += Bad_sign : _ ty -> error (* Toplevel errors *) type error += Ill_typed_data : string option * Script.expr * _ ty -> error @@ -118,13 +115,18 @@ let compare_comparable | Bool_key -> Compare.Bool.compare x y | Tez_key -> Tez.compare x y | Key_key -> Ed25519.Public_key_hash.compare x y - | Int_key kind -> - let res = - Script_int.to_int64 Script_int.Int64 - (Script_int.compare kind x y) in - if Compare.Int64.(res = 0L) then 0 - else if Compare.Int64.(res > 0L) then 1 + | Int_key -> + let res = (Script_int.compare x y) in + if Compare.Int.(res = 0) then 0 + else if Compare.Int.(res > 0) then 1 else -1 + + | Nat_key -> + let res = (Script_int.compare x y) in + if Compare.Int.(res = 0) then 0 + else if Compare.Int.(res > 0) then 1 + else -1 + | Timestamp_key -> Timestamp.compare x y let empty_set @@ -215,7 +217,8 @@ let map_fold let ty_of_comparable_ty : type a. a comparable_ty -> a ty = function - | Int_key k -> Int_t k + | Int_key -> Int_t + | Nat_key -> Nat_t | String_key -> String_t | Tez_key -> Tez_t | Bool_key -> Bool_t @@ -224,14 +227,8 @@ let ty_of_comparable_ty let unparse_comparable_ty : type a. a comparable_ty -> Script.expr = function - | Int_key Int8 -> Prim (-1, "int8", []) - | Int_key Int16 -> Prim (-1, "int16", []) - | Int_key Int32 -> Prim (-1, "int32", []) - | Int_key Int64 -> Prim (-1, "int64", []) - | Int_key Uint8 -> Prim (-1, "uint8", []) - | Int_key Uint16 -> Prim (-1, "uint16", []) - | Int_key Uint32 -> Prim (-1, "uint32", []) - | Int_key Uint64 -> Prim (-1, "uint64", []) + | Nat_key -> Prim (-1, "nat", []) + | Int_key -> Prim (-1, "int", []) | String_key -> Prim (-1, "string", []) | Tez_key -> Prim (-1, "tez", []) | Bool_key -> Prim (-1, "bool", []) @@ -241,14 +238,8 @@ let unparse_comparable_ty let rec unparse_ty : type a. a ty -> Script.expr = function | Unit_t -> Prim (-1, "unit", []) - | Int_t Int8 -> Prim (-1, "int8", []) - | Int_t Int16 -> Prim (-1, "int16", []) - | Int_t Int32 -> Prim (-1, "int32", []) - | Int_t Int64 -> Prim (-1, "int64", []) - | Int_t Uint8 -> Prim (-1, "uint8", []) - | Int_t Uint16 -> Prim (-1, "uint16", []) - | Int_t Uint32 -> Prim (-1, "uint32", []) - | Int_t Uint64 -> Prim (-1, "uint64", []) + | Nat_t -> Prim (-1, "nat", []) + | Int_t -> Prim (-1, "int", []) | String_t -> Prim (-1, "string", []) | Tez_t -> Prim (-1, "tez", []) | Bool_t -> Prim (-1, "bool", []) @@ -290,8 +281,10 @@ let rec unparse_data = fun ty a -> match ty, a with | Unit_t, () -> Prim (-1, "Unit", []) - | Int_t k, v -> - Int (-1, Int64.to_string (to_int64 k v)) + | Int_t, v -> + Int (-1, Script_int.to_string v) + | Nat_t, v -> + Int (-1, Script_int.to_string v) | String_t, s -> String (-1, s) | Bool_t, true -> @@ -352,53 +345,20 @@ let rec unparse_data (* ---- Equality witnesses --------------------------------------------------*) -type ('ta, 'tb) eq = - | Eq : 'same * 'same -> ('same, 'same) eq +type ('ta, 'tb) eq = Eq : 'same * 'same -> ('same, 'same) eq let eq : type t. t -> t -> (t, t) eq tzresult = fun ta tb -> Ok (Eq (ta, tb)) -let int_kind_eq - : type sa la sb lb. (sa, la) int_kind -> (sb, lb) int_kind -> - ((sa, la) int_kind, (sb, lb) int_kind) eq tzresult - = fun ka kb -> match ka, kb with - | Int8, Int8 -> eq ka kb - | Uint8, Uint8 -> eq ka kb - | Int16, Int16 -> eq ka kb - | Uint16, Uint16 -> eq ka kb - | Int32, Int32 -> eq ka kb - | Uint32, Uint32 -> eq ka kb - | Int64, Int64 -> eq ka kb - | Uint64, Uint64 -> eq ka kb - | _ -> error @@ Inconsistent_types (Int_t ka, Int_t kb) - -let unsigned_int_kind - : type sa la. (sa, la) int_kind -> (sa, unsigned) eq tzresult - = fun kind -> match kind with - | Uint8 -> eq Unsigned Unsigned - | Uint16 -> eq Unsigned Unsigned - | Uint32 -> eq Unsigned Unsigned - | Uint64 -> eq Unsigned Unsigned - | _ -> error @@ Bad_sign (Int_t kind) - -let signed_int_kind - : type sa la. (sa, la) int_kind -> (sa, signed) eq tzresult - = fun kind -> match kind with - | Int8 -> eq Signed Signed - | Int16 -> eq Signed Signed - | Int32 -> eq Signed Signed - | Int64 -> eq Signed Signed - | _ -> error @@ Bad_sign (Int_t kind) - +(* TODO: shall we allow operations to compare nats and ints ? *) let comparable_ty_eq : type ta tb. ta comparable_ty -> tb comparable_ty -> (ta comparable_ty, tb comparable_ty) eq tzresult = fun ta tb -> match ta, tb with - | Int_key ka, Int_key kb -> - int_kind_eq ka kb >>? fun (Eq _) -> - (eq ta tb : (ta comparable_ty, tb comparable_ty) eq tzresult) + | Int_key, Int_key -> eq ta tb + | Nat_key, Nat_key -> eq ta tb | String_key, String_key -> eq ta tb | Tez_key, Tez_key -> eq ta tb | Bool_key, Bool_key -> eq ta tb @@ -411,9 +371,8 @@ let rec ty_eq = fun ta tb -> match ta, tb with | Unit_t, Unit_t -> eq ta tb - | Int_t ka, Int_t kb -> - int_kind_eq ka kb >>? fun (Eq _) -> - (eq ta tb : (ta ty, tb ty) eq tzresult) + | Int_t, Int_t -> eq ta tb + | Nat_t, Nat_t -> eq ta tb | Key_t, Key_t -> eq ta tb | String_t, String_t -> eq ta tb | Signature_t, Signature_t -> eq ta tb @@ -505,24 +464,16 @@ let merge_branches 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_int_kind = Ex_int_kind : ('s, 'l) int_kind -> ex_int_kind let rec parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult = function - | Prim (_, "int8", []) -> ok (Ex_comparable_ty (Int_key Int8)) - | Prim (_, "int16", []) -> ok (Ex_comparable_ty (Int_key Int16)) - | Prim (_, "int32", []) -> ok (Ex_comparable_ty (Int_key Int32)) - | Prim (_, "int64", []) -> ok (Ex_comparable_ty (Int_key Int64)) - | Prim (_, "uint8", []) -> ok (Ex_comparable_ty (Int_key Uint8)) - | Prim (_, "uint16", []) -> ok (Ex_comparable_ty (Int_key Uint16)) - | Prim (_, "uint32", []) -> ok (Ex_comparable_ty (Int_key Uint32)) - | Prim (_, "uint64", []) -> ok (Ex_comparable_ty (Int_key Uint64)) + | Prim (_, "int", []) -> ok (Ex_comparable_ty Int_key) + | Prim (_, "nat", []) -> ok (Ex_comparable_ty Nat_key) | Prim (_, "string", []) -> ok (Ex_comparable_ty String_key) | Prim (_, "tez", []) -> ok (Ex_comparable_ty Tez_key) | Prim (_, "bool", []) -> ok (Ex_comparable_ty Bool_key) | Prim (_, "key", []) -> ok (Ex_comparable_ty Key_key) | Prim (_, "timestamp", []) -> ok (Ex_comparable_ty Timestamp_key) - | Prim (loc, ("int8" | "int16" | "int32" | "int64" - | "uint8" | "uint16" | "uint32" | "uint64" + | Prim (loc, ("int" | "nat" | "string" | "tez" | "bool" | "key" | "timestamp" as prim), l) -> error (Invalid_arity (loc, prim, 0, List.length l)) @@ -533,21 +484,14 @@ let rec parse_comparable_ty : Script.expr -> ex_comparable_ty tzresult = functio error (Comparable_type_expected (loc, ty)) | expr -> error @@ unexpected expr [] Type_namespace - [ "int8" ; "int16" ; "int32" ; "int64" ; - "uint8" ; "uint16" ; "uint32" ; "uint64" ; + [ "int" ; "nat" ; "string" ; "tez" ; "bool" ; "key" ; "timestamp" ] and parse_ty : Script.expr -> ex_ty tzresult = function | Prim (_, "unit", []) -> ok (Ex_ty Unit_t) - | Prim (_, "int8", []) -> ok (Ex_ty (Int_t Int8)) - | Prim (_, "int16", []) -> ok (Ex_ty (Int_t Int16)) - | Prim (_, "int32", []) -> ok (Ex_ty (Int_t Int32)) - | Prim (_, "int64", []) -> ok (Ex_ty (Int_t Int64)) - | Prim (_, "uint8", []) -> ok (Ex_ty (Int_t Uint8)) - | Prim (_, "uint16", []) -> ok (Ex_ty (Int_t Uint16)) - | Prim (_, "uint32", []) -> ok (Ex_ty (Int_t Uint32)) - | Prim (_, "uint64", []) -> ok (Ex_ty (Int_t Uint64)) + | Prim (_, "int", []) -> ok (Ex_ty Int_t) + | Prim (_, "nat", []) -> ok (Ex_ty Nat_t) | Prim (_, "string", []) -> ok (Ex_ty String_t) | Prim (_, "tez", []) -> ok (Ex_ty Tez_t) | Prim (_, "bool", []) -> ok (Ex_ty Bool_t) @@ -586,8 +530,7 @@ and parse_ty : Script.expr -> ex_ty tzresult = function | Prim (loc, ("pair" | "or" | "set" | "map" | "list" | "option" | "lambda" | "unit" | "signature" | "contract" - | "int8" | "int16" | "int32" | "int64" - | "uint8" | "uint16" | "uint32" | "uint64" + | "int" | "nat" | "string" | "tez" | "bool" | "key" | "timestamp" as prim), l) -> error (Invalid_arity (loc, prim, 0, List.length l)) @@ -596,15 +539,15 @@ and parse_ty : Script.expr -> ex_ty tzresult = function [ "pair" ; "or" ; "set" ; "map" ; "list" ; "option" ; "lambda" ; "unit" ; "signature" ; "contract" ; - "int8" ; "int16" ; "int32" ; "int64" ; - "uint8" ; "uint16" ; "uint32" ; "uint64" ; - "string" ; "tez" ; "bool" ; + "int" ; "nat" ; + "string" ; "tez" ; "bool" ; "key" ; "timestamp" ] let comparable_ty_of_ty : type a. int -> a ty -> a comparable_ty tzresult = fun loc ty -> match ty with - | Int_t k -> ok (Int_key k) + | Int_t -> ok Int_key + | Nat_t -> ok Nat_key | String_t -> ok String_key | Tez_t -> ok Tez_key | Bool_t -> ok Bool_key @@ -646,13 +589,22 @@ let rec parse_data | String_t, expr -> traced (fail (Invalid_kind (location expr, [ String_kind ], kind expr))) (* Integers *) - | Int_t k, Int (_, v) -> begin try - match checked_of_int64 k (Int64.of_string v) with - | None -> raise Exit - | Some i -> return i - with _ -> fail (error ()) - end - | Int_t _, expr -> + | Int_t, Int (_, v) -> + begin match Script_int.of_string v with + | None -> fail (error ()) + | Some v -> return v + end + | Nat_t, Int (_, v) -> + begin match Script_int.of_string v with + | None -> fail (error ()) + | Some v -> + if Compare.Int.(Script_int.compare v Script_int.zero >= 0) then + return (Script_int.abs v) + else fail (error ()) + end + | Int_t, expr -> + traced (fail (Invalid_kind (location expr, [ Int_kind ], kind expr))) + | Nat_t, expr -> traced (fail (Invalid_kind (location expr, [ Int_kind ], kind expr))) (* Tez amounts *) | Tez_t, String (_, v) -> begin try @@ -1060,13 +1012,11 @@ and parse_instr return (Failed { descr }) (* timestamp operations *) | Prim (loc, "ADD", []), - Item_t (Timestamp_t, Item_t (Int_t kind, rest)) -> - check_item (unsigned_int_kind kind) loc "ADD" 2 2 >>=? fun (Eq _) -> - return (typed loc (Add_timestamp_to_seconds kind, Item_t (Timestamp_t, rest))) + Item_t (Timestamp_t, Item_t (Nat_t, rest)) -> + return (typed loc (Add_timestamp_to_seconds, Item_t (Timestamp_t, rest))) | Prim (loc, "ADD", []), - Item_t (Int_t kind, Item_t (Timestamp_t, rest)) -> - check_item (unsigned_int_kind kind) loc "ADD" 1 2 >>=? fun (Eq _) -> - return (typed loc (Add_seconds_to_timestamp kind, Item_t (Timestamp_t, rest))) + Item_t (Nat_t, Item_t (Timestamp_t, rest)) -> + return (typed loc (Add_seconds_to_timestamp, Item_t (Timestamp_t, rest))) (* string operations *) | Prim (loc, "CONCAT", []), Item_t (String_t, Item_t (String_t, rest)) -> @@ -1079,13 +1029,11 @@ and parse_instr Item_t (Tez_t, Item_t (Tez_t, rest)) -> return (typed loc (Sub_tez, Item_t (Tez_t, rest))) | Prim (loc, "MUL", []), - Item_t (Tez_t, Item_t (Int_t kind, rest)) -> - check_item (unsigned_int_kind kind) loc "MUL" 2 2 >>=? fun (Eq _) -> - return (typed loc (Mul_tez kind, Item_t (Tez_t, rest))) + Item_t (Tez_t, Item_t (Nat_t, rest)) -> + return (typed loc (Mul_teznat, Item_t (Tez_t, rest))) | Prim (loc, "MUL", []), - Item_t (Int_t kind, Item_t (Tez_t, rest)) -> - check_item (unsigned_int_kind kind) loc "MUL" 1 2 >>=? fun (Eq _) -> - return (typed loc (Mul_tez' kind, Item_t (Tez_t, rest))) + Item_t (Nat_t, Item_t (Tez_t, rest)) -> + return (typed loc (Mul_nattez, Item_t (Tez_t, rest))) (* boolean operations *) | Prim (loc, "OR", []), Item_t (Bool_t, Item_t (Bool_t, rest)) -> @@ -1100,144 +1048,140 @@ and parse_instr Item_t (Bool_t, rest) -> return (typed loc (Not, Item_t (Bool_t, rest))) (* integer operations *) - | Prim (loc, "CHECKED_ABS", []), - Item_t (Int_t k, rest) -> - check_item (signed_int_kind k) loc "CHECKED_ABS" 1 1 >>=? fun (Eq _) -> - return (typed loc (Checked_abs_int k, Item_t (Int_t k, rest))) - | Prim (loc, "CHECKED_NEG", []), - Item_t (Int_t k, rest) -> - check_item (signed_int_kind k) loc "CHECKED_NEG" 1 1 >>=? fun (Eq _) -> - return (typed loc (Checked_neg_int k, Item_t (Int_t k, rest))) - | Prim (loc, "CHECKED_ADD", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "CHECKED_ADD" 1 2 >>=? fun (Eq _) -> - return (typed loc (Checked_add_int kl, Item_t (Int_t kl, rest))) - | Prim (loc, "CHECKED_SUB", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "CHECKED_SUB" 1 2 >>=? fun (Eq _) -> - return (typed loc (Checked_sub_int kl, Item_t (Int_t kl, rest))) - | Prim (loc, "CHECKED_MUL", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "CHECKED_MUL" 1 2 >>=? fun (Eq _) -> - return (typed loc (Checked_mul_int kl, Item_t (Int_t kl, rest))) | Prim (loc, "ABS", []), - Item_t (Int_t k, rest) -> - check_item (signed_int_kind k) loc "ABS" 1 1 >>=? fun (Eq _) -> - return (typed loc (Abs_int k, Item_t (Int_t k, rest))) + Item_t (Int_t, rest) -> + return (typed loc (Abs_int, Item_t (Nat_t, rest))) + | Prim (loc, "INT", []), + Item_t (Nat_t, rest) -> + return (typed loc (Int_nat, Item_t (Int_t, rest))) | Prim (loc, "NEG", []), - Item_t (Int_t k, rest) -> - check_item (signed_int_kind k) loc "NEG" 1 1 >>=? fun (Eq _) -> - return (typed loc (Neg_int k, Item_t (Int_t k, rest))) + Item_t (Int_t, rest) -> + return (typed loc (Neg_int, Item_t (Int_t, rest))) + | Prim (loc, "NEG", []), + Item_t (Nat_t, rest) -> + return (typed loc (Neg_nat, Item_t (Int_t, rest))) | Prim (loc, "ADD", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "ADD" 1 2 >>=? fun (Eq _) -> - return (typed loc (Add_int kl, Item_t (Int_t kl, rest))) + Item_t (Int_t, Item_t (Int_t, rest)) -> + return (typed loc (Add_intint, Item_t (Int_t, rest))) + | Prim (loc, "ADD", []), + Item_t (Int_t, Item_t (Nat_t, rest)) -> + return (typed loc (Add_intnat, Item_t (Int_t, rest))) + | Prim (loc, "ADD", []), + Item_t (Nat_t, Item_t (Int_t, rest)) -> + return (typed loc (Add_natint, Item_t (Int_t, rest))) + | Prim (loc, "ADD", []), + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Add_natnat, Item_t (Nat_t, rest))) | Prim (loc, "SUB", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "SUB" 1 2 >>=? fun (Eq _) -> - return (typed loc (Sub_int kl, Item_t (Int_t kl, rest))) + Item_t (Int_t, Item_t (Int_t, rest)) -> + return (typed loc (Sub_int, Item_t (Int_t, rest))) + | Prim (loc, "SUB", []), + Item_t (Int_t, Item_t (Nat_t, rest)) -> + return (typed loc (Sub_int, Item_t (Int_t, rest))) + | Prim (loc, "SUB", []), + Item_t (Nat_t, Item_t (Int_t, rest)) -> + return (typed loc (Sub_int, Item_t (Int_t, rest))) + | Prim (loc, "SUB", []), + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Sub_int, Item_t (Int_t, rest))) | Prim (loc, "MUL", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "MUL" 1 2 >>=? fun (Eq _) -> - return (typed loc (Mul_int kl, Item_t (Int_t kl, rest))) - | Prim (loc, "DIV", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "DIV" 1 2 >>=? fun (Eq _) -> - return (typed loc (Div_int kl, Item_t (Int_t kl, rest))) - | Prim (loc, "MOD", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "MOD" 1 2 >>=? fun (Eq _) -> - return (typed loc (Mod_int kl, Item_t (Int_t kl, rest))) + Item_t (Int_t, Item_t (Int_t, rest)) -> + return (typed loc (Mul_intint, Item_t (Int_t, rest))) + | Prim (loc, "MUL", []), + Item_t (Int_t, Item_t (Nat_t, rest)) -> + return (typed loc (Mul_intnat, Item_t (Int_t, rest))) + | Prim (loc, "MUL", []), + Item_t (Nat_t, Item_t (Int_t, rest)) -> + return (typed loc (Mul_natint, Item_t (Int_t, rest))) + | Prim (loc, "MUL", []), + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Mul_natnat, Item_t (Nat_t, rest))) + | Prim (loc, "EDIV", []), + Item_t (Tez_t, Item_t (Nat_t, rest)) -> + return (typed loc (Ediv_teznat, + Item_t (Option_t (Pair_t (Tez_t,Tez_t)), rest))) + | Prim (loc, "EDIV", []), + Item_t (Tez_t, Item_t (Tez_t, rest)) -> + return (typed loc (Ediv_tez, + Item_t (Option_t (Pair_t (Nat_t,Tez_t)), rest))) + | Prim (loc, "EDIV", []), + Item_t (Int_t, Item_t (Int_t, rest)) -> + return (typed loc (Ediv_intint, + Item_t (Option_t (Pair_t (Int_t,Nat_t)), rest))) + | Prim (loc, "EDIV", []), + Item_t (Int_t, Item_t (Nat_t, rest)) -> + return (typed loc (Ediv_intnat, + Item_t (Option_t (Pair_t (Int_t,Nat_t)), rest))) + | Prim (loc, "EDIV", []), + Item_t (Nat_t, Item_t (Int_t, rest)) -> + return (typed loc (Ediv_natint, + Item_t (Option_t (Pair_t (Int_t,Nat_t)), rest))) + | Prim (loc, "EDIV", []), + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Ediv_natnat, + Item_t (Option_t (Pair_t (Nat_t,Nat_t)), rest))) | Prim (loc, "LSL", []), - Item_t (Int_t k, Item_t (Int_t Uint8, rest)) -> - check_item (unsigned_int_kind k) loc "LSL" 1 2 >>=? fun (Eq _) -> - return (typed loc (Lsl_int k, Item_t (Int_t k, rest))) + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Lsl_nat, Item_t (Nat_t, rest))) | Prim (loc, "LSR", []), - Item_t (Int_t k, Item_t (Int_t Uint8, rest)) -> - check_item (unsigned_int_kind k) loc "LSR" 1 2 >>=? fun (Eq _) -> - return (typed loc (Lsr_int k, Item_t (Int_t k, rest))) + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Lsr_nat, Item_t (Nat_t, rest))) | Prim (loc, "OR", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (unsigned_int_kind kl) loc "OR" 1 2 >>=? fun (Eq _) -> - check_item (int_kind_eq kl kr) loc "OR" 1 2 >>=? fun (Eq _) -> - return (typed loc (Or_int kl, Item_t (Int_t kl, rest))) + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Or_nat, Item_t (Nat_t, rest))) | Prim (loc, "AND", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (unsigned_int_kind kl) loc "AND" 1 2 >>=? fun (Eq _) -> - check_item (int_kind_eq kl kr) loc "AND" 1 2 >>=? fun (Eq _) -> - return (typed loc (And_int kl, Item_t (Int_t kl, rest))) + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (And_nat, Item_t (Nat_t, rest))) | Prim (loc, "XOR", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (unsigned_int_kind kl) loc "XOR" 1 2 >>=? fun (Eq _) -> - check_item (int_kind_eq kl kr) loc "XOR" 1 2 >>=? fun (Eq _) -> - return (typed loc (Xor_int kl, Item_t (Int_t kl, rest))) + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Xor_nat, Item_t (Nat_t, rest))) | Prim (loc, "NOT", []), - Item_t (Int_t k, rest) -> - check_item (unsigned_int_kind k) loc "NOT" 1 1 >>=? fun (Eq _) -> - return (typed loc (Not_int k, Item_t (Int_t k, rest))) + Item_t (Int_t, rest) -> + return (typed loc (Not_int, Item_t (Int_t, rest))) + | Prim (loc, "NOT", []), + Item_t (Nat_t, rest) -> + return (typed loc (Not_nat, Item_t (Int_t, rest))) (* comparison *) | Prim (loc, "COMPARE", []), - Item_t (Int_t kl, Item_t (Int_t kr, rest)) -> - check_item (int_kind_eq kl kr) loc "COMPARE" 1 2 >>=? fun (Eq _) -> - return (typed loc (Compare (Int_key kl), Item_t (Int_t Int64, rest))) + Item_t (Int_t, Item_t (Int_t, rest)) -> + return (typed loc (Compare Int_key, Item_t (Int_t, rest))) + | Prim (loc, "COMPARE", []), + Item_t (Nat_t, Item_t (Nat_t, rest)) -> + return (typed loc (Compare Nat_key, Item_t (Int_t, rest))) | Prim (loc, "COMPARE", []), Item_t (Bool_t, Item_t (Bool_t, rest)) -> - return (typed loc (Compare Bool_key, Item_t (Int_t Int64, rest))) + return (typed loc (Compare Bool_key, Item_t (Int_t, rest))) | Prim (loc, "COMPARE", []), Item_t (String_t, Item_t (String_t, rest)) -> - return (typed loc (Compare String_key, Item_t (Int_t Int64, rest))) + return (typed loc (Compare String_key, Item_t (Int_t, rest))) | Prim (loc, "COMPARE", []), Item_t (Tez_t, Item_t (Tez_t, rest)) -> - return (typed loc (Compare Tez_key, Item_t (Int_t Int64, rest))) + return (typed loc (Compare Tez_key, Item_t (Int_t, rest))) | Prim (loc, "COMPARE", []), Item_t (Key_t, Item_t (Key_t, rest)) -> - return (typed loc (Compare Key_key, Item_t (Int_t Int64, rest))) + return (typed loc (Compare Key_key, Item_t (Int_t, rest))) | Prim (loc, "COMPARE", []), Item_t (Timestamp_t, Item_t (Timestamp_t, rest)) -> - return (typed loc (Compare Timestamp_key, Item_t (Int_t Int64, rest))) + return (typed loc (Compare Timestamp_key, Item_t (Int_t, rest))) (* comparators *) | Prim (loc, "EQ", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Eq, Item_t (Bool_t, rest))) | Prim (loc, "NEQ", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Neq, Item_t (Bool_t, rest))) | Prim (loc, "LT", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Lt, Item_t (Bool_t, rest))) | Prim (loc, "GT", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Gt, Item_t (Bool_t, rest))) | Prim (loc, "LE", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Le, Item_t (Bool_t, rest))) | Prim (loc, "GE", []), - Item_t (Int_t Int64, rest) -> + Item_t (Int_t, rest) -> return (typed loc (Ge, Item_t (Bool_t, rest))) - (* casts *) - | Prim (loc, "CHECKED_CAST", [ t ]), - stack -> - (Lwt.return (parse_ty t)) >>=? fun (Ex_ty ty) -> begin match ty, stack with - | Int_t kt, - Item_t (Int_t kf, rest) -> - return (typed loc (Checked_int_of_int (kf, kt), - Item_t (Int_t kt, rest))) - | ty, Item_t (ty', _) -> - fail (Undefined_cast (loc, ty', ty)) - | _, Empty_t -> - fail (Bad_stack (loc, "CHECKED_CAST", 1, stack)) - end - | Prim (loc, "CAST", [ t ]), - stack -> - (Lwt.return (parse_ty t)) >>=? fun (Ex_ty ty) -> begin match ty, stack with - | Int_t kt, Item_t (Int_t kf, rest) -> - return (typed loc (Int_of_int (kf, kt), - Item_t (Int_t kt, rest))) - | ty, Item_t (ty', _) -> - fail (Undefined_cast (loc, ty', ty)) - | _, Empty_t -> - fail (Bad_stack (loc, "CAST", 1, stack)) - end (* protocol *) | Prim (loc, "MANAGER", []), Item_t (Contract_t _, rest) -> @@ -1299,7 +1243,7 @@ and parse_instr return (typed loc (H t, Item_t (String_t, rest))) | Prim (loc, "STEPS_TO_QUOTA", []), stack -> - return (typed loc (Steps_to_quota, Item_t (Int_t Uint32, stack))) + return (typed loc (Steps_to_quota, Item_t (Nat_t, stack))) | Prim (loc, "SOURCE", [ ta; tb ]), stack -> (Lwt.return (parse_ty ta)) >>=? fun (Ex_ty ta) -> @@ -1311,9 +1255,8 @@ and parse_instr | "MEM" | "UPDATE" | "MAP" | "REDUCE" | "GET" | "EXEC" | "FAIL" | "CONCAT" | "ADD" | "SUB" - | "MUL" | "DIV" | "MOD" | "OR" | "AND" | "XOR" - | "NOT" | "CHECKED_ABS" | "CHECKED_NEG" - | "CHECKED_ADD" | "CHECKED_SUB" | "CHECKED_MUL" + | "MUL" | "EDIV" | "OR" | "AND" | "XOR" + | "NOT" | "ABS" | "NEG" | "LSL" | "LSR" | "COMPARE" | "EQ" | "NEQ" | "LT" | "GT" | "LE" | "GE" @@ -1324,7 +1267,7 @@ and parse_instr as name), (_ :: _ as l)), _ -> fail (Invalid_arity (loc, name, 0, List.length l)) | Prim (loc, ("NONE" | "LEFT" | "RIGHT" | "NIL" - | "EMPTY_SET" | "DIP" | "CHECKED_CAST" | "CAST" | "LOOP" + | "EMPTY_SET" | "DIP" | "LOOP" as name), ([] | _ :: _ :: _ as l)), _ -> fail (Invalid_arity (loc, name, 1, List.length l)) @@ -1337,11 +1280,9 @@ and parse_instr | _ :: _ :: _ :: _ :: _ as l)), _ -> fail (Invalid_arity (loc, "LAMBDA", 3, List.length l)) (* Stack errors *) - | Prim (loc, ("ADD" | "SUB" | "MUL" | "DIV" | "MOD" + | Prim (loc, ("ADD" | "SUB" | "MUL" | "EDIV" | "AND" | "OR" | "XOR" | "LSL" | "LSR" - | "CONCAT" | "COMPARE" - | "CHECKED_ABS" | "CHECKED_NEG" - | "CHECKED_ADD" | "CHECKED_SUB" | "CHECKED_MUL" as name), []), + | "CONCAT" | "COMPARE" as name), []), Item_t (ta, Item_t (tb, _)) -> fail (Undefined_binop (loc, name, ta, tb)) | Prim (loc, ("NEG" | "ABS" | "NOT" @@ -1363,17 +1304,15 @@ and parse_instr | Prim (loc, ("DROP" | "DUP" | "CAR" | "CDR" | "SOME" | "H" | "DIP" | "IF_NONE" | "LEFT" | "RIGHT" | "IF_LEFT" | "IF" | "LOOP" | "IF_CONS" | "MANAGER" | "DEFAULT_ACCOUNT" - | "NEG" | "ABS" | "NOT" + | "NEG" | "ABS" | "INT" | "NOT" | "EQ" | "NEQ" | "LT" | "GT" | "LE" | "GE" as name), _), stack -> fail (Bad_stack (loc, name, 1, stack)) | Prim (loc, ("SWAP" | "PAIR" | "CONS" | "MAP" | "GET" | "MEM" | "EXEC" | "CHECK_SIGNATURE" | "ADD" | "SUB" | "MUL" - | "DIV" | "MOD" | "AND" | "OR" | "XOR" - | "LSL" | "LSR" | "CONCAT" - | "CHECKED_ABS" | "CHECKED_NEG" | "CHECKED_ADD" - | "CHECKED_SUB" | "CHECKED_MUL" | "COMPARE" as name), _), + | "EDIV" | "AND" | "OR" | "XOR" + | "LSL" | "LSR" | "CONCAT" as name), _), stack -> fail (Bad_stack (loc, name, 2, stack)) (* Generic parsing errors *) @@ -1384,17 +1323,16 @@ and parse_instr "MEM" ; "UPDATE" ; "MAP" ; "REDUCE" ; "GET" ; "EXEC" ; "FAIL" ; "CONCAT" ; "ADD" ; "SUB" ; - "MUL" ; "DIV" ; "MOD" ; "OR" ; "AND" ; "XOR" ; - "NOT" ; "CHECKED_ABS" ; "CHECKED_NEG" ; - "CHECKED_ADD" ; "CHECKED_SUB" ; "CHECKED_MUL" ; - "ABS" ; "NEG" ; "LSL" ; "LSR" ; + "MUL" ; "EDIV" ; "OR" ; "AND" ; "XOR" ; + "NOT" ; + "ABS" ; "INT"; "NEG" ; "LSL" ; "LSR" ; "COMPARE" ; "EQ" ; "NEQ" ; "LT" ; "GT" ; "LE" ; "GE" ; "MANAGER" ; "TRANSFER_TOKENS" ; "CREATE_ACCOUNT" ; "CREATE_CONTRACT" ; "NOW" ; "AMOUNT" ; "BALANCE" ; "DEFAULT_ACCOUNT" ; "CHECK_SIGNATURE" ; "H" ; "STEPS_TO_QUOTA" ; "PUSH" ; "NONE" ; "LEFT" ; "RIGHT" ; "NIL" ; - "EMPTY_SET" ; "DIP" ; "CHECKED_CAST" ; "CAST" ; "LOOP" ; + "EMPTY_SET" ; "DIP" ; "LOOP" ; "IF_NONE" ; "IF_LEFT" ; "IF_CONS" ; "EMPTY_MAP" ; "IF" ; "SOURCE" ; "LAMBDA" ] @@ -1511,7 +1449,8 @@ let type_map descr = = fun acc ty v -> match ty, v with | Unit_t, _ -> acc - | Int_t _, _ -> acc + | Int_t, _ -> acc + | Nat_t, _ -> acc | Signature_t, _ -> acc | String_t, _ -> acc | Tez_t, _ -> acc @@ -1720,21 +1659,6 @@ let () = | _ -> None) (fun (loc, ()) -> Fail_not_in_tail_position loc) ; - register_error_kind - `Permanent - ~id:"undefinedCastTypeError" - ~title: "Undefined cast (typechecking error)" - ~description: - "A CAST operation is performed to or from an unsupported type." - (located (obj2 - (req "wrongInputType" ex_ty_enc) - (req "wrongOutputType" ex_ty_enc))) - (function - | Undefined_cast (loc, tyl, tyr) -> - Some (loc, (Ex_ty tyl, Ex_ty tyr)) - | _ -> None) - (fun (loc, (Ex_ty tyl, Ex_ty tyr)) -> - Undefined_cast (loc, tyl, tyr)) ; register_error_kind `Permanent ~id:"undefinedBinopTypeError" @@ -1912,21 +1836,7 @@ let () = | _ -> None) (fun (Ex_ty tya, Ex_ty tyb) -> Inconsistent_types (tya, tyb)) ; - register_error_kind - `Permanent - ~id:"badSignTypeError" - ~title: "Bad sign (typechecking error)" - ~description: - "A signed (resp. unsigned) integer kind was used in a place \ - where only unsigned (resp. signed) integers can be used, \ - this error is always accompanied \ - with another error that provides more context." - (obj1 (req "wrongIntegerType" ex_ty_enc)) - (function - | Bad_sign ty -> Some (Ex_ty ty) - | _ -> None) - (fun (Ex_ty ty) -> - Bad_sign ty) ; + (* Toplevel errors *) register_error_kind `Permanent diff --git a/src/proto/alpha/script_repr.mli b/src/proto/alpha/script_repr.mli index 43c8f371c..b4626bd88 100644 --- a/src/proto/alpha/script_repr.mli +++ b/src/proto/alpha/script_repr.mli @@ -7,6 +7,17 @@ (* *) (**************************************************************************) +(* A smart contract is some code and some storage. The storage has a + type and an initial value. The code is the code itself, the types of + its arguments, the type of its result, and the type of the storage + it is using. + + All of them are expressed in a simple [expr] type, combining + [Int] (integer constant), [String] (string constant), [Prim] + (a generic primitive for most operations) and [Seq] a sequence + of operations. + *) + type location = int diff --git a/src/proto/alpha/script_typed_ir.ml b/src/proto/alpha/script_typed_ir.ml index cd8813370..7c45b6add 100644 --- a/src/proto/alpha/script_typed_ir.ml +++ b/src/proto/alpha/script_typed_ir.ml @@ -14,7 +14,8 @@ open Script_int (* ---- Auxiliary types -----------------------------------------------------*) type 'ty comparable_ty = - | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty + | Int_key : (z num) comparable_ty + | Nat_key : (n num) comparable_ty | String_key : string comparable_ty | Tez_key : Tez.t comparable_ty | Bool_key : bool comparable_ty @@ -60,7 +61,8 @@ and ('arg, 'ret) typed_contract = and 'ty ty = | Unit_t : unit ty - | Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty + | Int_t : z num ty + | Nat_t : n num ty | Signature_t : signature ty | String_t : string ty | Tez_t : Tez.t ty @@ -162,19 +164,27 @@ and ('bef, 'aft) instr = | Concat : (string * (string * 'rest), string * 'rest) instr (* timestamp operations *) - | Add_seconds_to_timestamp : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr - | Add_timestamp_to_seconds : (unsigned, 'l) int_kind -> - (Timestamp.t * ((unsigned, 'l) int_val * 'rest), Timestamp.t * 'rest) instr + (* TODO: check if we need int instead of nat *) + | Add_seconds_to_timestamp : + (n num * (Timestamp.t * 'rest), Timestamp.t * 'rest) instr + | Add_timestamp_to_seconds : + (Timestamp.t * (n num * 'rest), Timestamp.t * 'rest) instr (* currency operations *) + (* TODO: we can either just have conversions to/from integers and + do all operations on integers, or we need more operations on + Tez. Also Sub_tez should return Tez.t option (if negative) and *) | Add_tez : (Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr | Sub_tez : (Tez.t * (Tez.t * 'rest), Tez.t * 'rest) instr - | Mul_tez : (unsigned, 'l) int_kind -> - (Tez.t * ((unsigned, 'l) int_val * 'rest), Tez.t * 'rest) instr - | Mul_tez' : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * (Tez.t * 'rest), Tez.t * 'rest) instr + | Mul_teznat : + (Tez.t * (n num * 'rest), Tez.t * 'rest) instr + | Mul_nattez : + (n num * (Tez.t * 'rest), Tez.t * 'rest) instr + | Ediv_teznat : + (Tez.t * (n num * 'rest), ((Tez.t, Tez.t) pair) option * 'rest) instr + | Ediv_tez : + (Tez.t * (Tez.t * 'rest), ((n num, Tez.t) pair) option * 'rest) instr (* boolean operations *) | Or : (bool * (bool * 'rest), bool * 'rest) instr @@ -185,42 +195,54 @@ and ('bef, 'aft) instr = | Not : (bool * 'rest, bool * 'rest) instr (* integer operations *) - | Checked_neg_int : (signed, 'l) int_kind -> - ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr - | Checked_abs_int : (signed, 'l) int_kind -> - ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr - | Checked_add_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Checked_sub_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Checked_mul_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Neg_int : (signed, 'l) int_kind -> - ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr - | Abs_int : (signed, 'l) int_kind -> - ((signed, 'l) int_val * 'rest, (signed, 'l) int_val * 'rest) instr - | Add_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Sub_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Mul_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Div_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Mod_int : ('s, 'l) int_kind -> - (('s, 'l) int_val * (('s, 'l) int_val * 'rest), ('s, 'l) int_val * 'rest) instr - | Lsl_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr - | Lsr_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * ((unsigned, eight) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr - | Or_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr - | And_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr - | Xor_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * ((unsigned, 'l) int_val * 'rest), (unsigned, 'l) int_val * 'rest) instr - | Not_int : (unsigned, 'l) int_kind -> - ((unsigned, 'l) int_val * 'rest, (unsigned, 'l) int_val * 'rest) instr + | Neg_nat : + (n num * 'rest, z num * 'rest) instr + | Neg_int : + (z num * 'rest, z num * 'rest) instr + | Abs_int : + (z num * 'rest, n num * 'rest) instr + | Int_nat : + (n num * 'rest, z num * 'rest) instr + | Add_intint : + (z num * (z num * 'rest), z num * 'rest) instr + | Add_intnat : + (z num * (n num * 'rest), z num * 'rest) instr + | Add_natint : + (n num * (z num * 'rest), z num * 'rest) instr + | Add_natnat : + (n num * (n num * 'rest), n num * 'rest) instr + | Sub_int : + ('s num * ('t num * 'rest), z num * 'rest) instr + | Mul_intint : + (z num * (z num * 'rest), z num * 'rest) instr + | Mul_intnat : + (z num * (n num * 'rest), z num * 'rest) instr + | Mul_natint : + (n num * (z num * 'rest), z num * 'rest) instr + | Mul_natnat : + (n num * (n num * 'rest), n num * 'rest) instr + | Ediv_intint : + (z num * (z num * 'rest), ((z num, n num) pair) option * 'rest) instr + | Ediv_intnat : + (z num * (n num * 'rest), ((z num, n num) pair) option * 'rest) instr + | Ediv_natint : + (n num * (z num * 'rest), ((z num, n num) pair) option * 'rest) instr + | Ediv_natnat : + (n num * (n num * 'rest), ((n num, n num) pair) option * 'rest) instr + | Lsl_nat : + (n num * (n num * 'rest), n num * 'rest) instr + | Lsr_nat : + (n num * (n num * 'rest), n num * 'rest) instr + | Or_nat : + (n num * (n num * 'rest), n num * 'rest) instr + | And_nat : + (n num * (n num * 'rest), n num * 'rest) instr + | Xor_nat : + (n num * (n num * 'rest), n num * 'rest) instr + | Not_nat : + (n num * 'rest, z num * 'rest) instr + | Not_int : + (z num * 'rest, z num * 'rest) instr (* control *) | Seq : ('bef, 'trans) descr * ('trans, 'aft) descr -> ('bef, 'aft) instr @@ -235,31 +257,27 @@ and ('bef, 'aft) instr = | Lambda : ('arg, 'ret) lambda -> ('rest, ('arg, 'ret) lambda * 'rest) instr | Fail : - ('bef, 'aft) instr + ('bef, 'aft) instr | Nop : ('rest, 'rest) instr (* comparison *) | Compare : 'a comparable_ty -> - ('a * ('a * 'rest), (signed, sixtyfour) int_val * 'rest) instr + ('a * ('a * 'rest), z num * 'rest) instr (* comparators *) | Eq : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr + (z num * 'rest, bool * 'rest) instr | Neq : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr + (z num * 'rest, bool * 'rest) instr | Lt : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr + (z num * 'rest, bool * 'rest) instr | Gt : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr + (z num * 'rest, bool * 'rest) instr | Le : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr + (z num * 'rest, bool * 'rest) instr | Ge : - ((signed, sixtyfour) int_val * 'rest, bool * 'rest) instr - (* casts *) - | Int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind -> - (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr - | Checked_int_of_int : ('sf, 'lf) int_kind * ('st, 'lt) int_kind -> - (('sf, 'lf) int_val * 'rest, ('st, 'lt) int_val * 'rest) instr - (* protocol *) + (z num * 'rest, bool * 'rest) instr + + (* protocol *) | Manager : (('arg, 'ret) typed_contract * 'rest, public_key_hash * 'rest) instr | Transfer_tokens : 'sto ty -> @@ -267,10 +285,11 @@ and ('bef, 'aft) instr = | Create_account : (public_key_hash * (public_key_hash option * (bool * (Tez.t * 'rest))), (unit, unit) typed_contract * 'rest) instr - | Default_account : (public_key_hash * 'rest, (unit, unit) typed_contract * 'rest) instr + | Default_account : + (public_key_hash * 'rest, (unit, unit) typed_contract * 'rest) instr | Create_contract : 'g ty * 'p ty * 'r ty -> (public_key_hash * (public_key_hash option * (bool * (bool * (Tez.t * - (('p * 'g, 'r * 'g) lambda * ('g * 'rest)))))), + (('p * 'g, 'r * 'g) lambda * ('g * 'rest)))))), ('p, 'r) typed_contract * 'rest) instr | Now : ('rest, Timestamp.t * 'rest) instr @@ -280,8 +299,8 @@ and ('bef, 'aft) instr = (public_key_hash * ((signature * string) * 'rest), bool * 'rest) instr | H : 'a ty -> ('a * 'rest, string * 'rest) instr - | Steps_to_quota : - ('rest, (unsigned, thirtytwo) int_val * 'rest) instr + | Steps_to_quota : (* TODO: check that it always returns a nat *) + ('rest, n num * 'rest) instr | Source : 'p ty * 'r ty -> ('rest, ('p, 'r) typed_contract * 'rest) instr | Amount : diff --git a/src/proto/environment/z.mli b/src/proto/environment/z.mli new file mode 100644 index 000000000..69facbc50 --- /dev/null +++ b/src/proto/environment/z.mli @@ -0,0 +1,76 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2014 - 2016. *) +(* Dynamic Ledger Solutions, Inc. *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +type t +val zero: t +val one: t + +external abs: t -> t = "ml_z_abs" "ml_as_z_abs" +(** Absolute value. *) + +external neg: t -> t = "ml_z_neg" "ml_as_z_neg" +(** Unary negation. *) + +external add: t -> t -> t = "ml_z_add" "ml_as_z_add" +(** Addition. *) + +external sub: t -> t -> t = "ml_z_sub" "ml_as_z_sub" +(** Subtraction. *) + +external mul: t -> t -> t = "ml_z_mul" "ml_as_z_mul" +(** Multiplication. *) + +val ediv_rem: t -> t -> (t * t) +(** Euclidean division and remainder. [ediv_rem a b] returns a pair [(q, r)] + such that [a = b * q + r] and [0 <= r < |b|]. + Raises [Division_by_zero] if [b = 0]. + *) + +external logand: t -> t -> t = "ml_z_logand" "ml_as_z_logand" +(** Bitwise logical and. *) + +external logor: t -> t -> t = "ml_z_logor" "ml_as_z_logor" +(** Bitwise logical or. *) + +external logxor: t -> t -> t = "ml_z_logxor" "ml_as_z_logxor" +(** Bitwise logical exclusive or. *) + +external lognot: t -> t = "ml_z_lognot" "ml_as_z_lognot" +(** Bitwise logical negation. + The identity [lognot a]=[-a-1] always hold. + *) + +external shift_left: t -> int -> t = "ml_z_shift_left" "ml_as_z_shift_left" +(** Shifts to the left. + Equivalent to a multiplication by a power of 2. + The second argument must be non-negative. + *) + +external shift_right: t -> int -> t = "ml_z_shift_right" "ml_as_z_shift_right" +(** Shifts to the right. + This is an arithmetic shift, + equivalent to a division by a power of 2 with rounding towards -oo. + The second argument must be non-negative. + *) + +val to_string: t -> string +val of_string: string -> t + +external to_int64: t -> int64 = "ml_z_to_int64" +(** Converts to a 64-bit integer. May raise [Overflow]. *) +external of_int64: int64 -> t = "ml_z_of_int64" +(** Converts from a 64-bit integer. *) + +external to_int: t -> int = "ml_z_to_int" +(** Converts to a base integer. May raise an [Overflow]. *) +external of_int: int -> t = "ml_z_of_int" [@@ noalloc] +(** Converts from a base integer. *) + +external equal: t -> t -> bool = "ml_z_equal" [@@ noalloc] +external compare: t -> t -> int = "ml_z_compare" [@@ noalloc]