Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add builtins substr and concat for ByStr and to_bystrx to convert to fixed length byte strings #906

Merged
merged 9 commits into from
Nov 13, 2020
Merged

Add builtins substr and concat for ByStr and to_bystrx to convert to fixed length byte strings #906

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
e9b098b
Add substr and concat for ByStr Scilla type
vaivaswatha Nov 10, 2020
f386522
Add builtin to_bystrx
vaivaswatha Nov 13, 2020
bcbc0b2
Merge branch 'master' into polynetwork
vaivaswatha Nov 13, 2020
d050ef0
make fmt
vaivaswatha Nov 13, 2020
c6554af
Update src/base/Syntax.ml
vaivaswatha Nov 13, 2020
b18e7ad
remove unneeded comment
vaivaswatha Nov 13, 2020
082d16c
Update src/base/Syntax.ml
vaivaswatha Nov 13, 2020
58e4c04
Add expected fail tests
vaivaswatha Nov 13, 2020
a9f39e0
One more failing test
vaivaswatha Nov 13, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 35 additions & 2 deletions src/base/BuiltIns.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -822,6 +822,19 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
let ripemd160hash ls _ =
hash_helper ripemd160_hasher "ripemd160hash" address_length ls

(* ByStr -> Option ByStrX *)
let to_bystrx_type x = fun_typ bystr_typ (option_typ (bystrx_typ x))

let to_bystrx_arity = 1

let to_bystrx x ls _ =
match ls with
| [ ByStr bs ] -> (
match Bystrx.of_raw_bytes x (Bystr.to_raw_bytes bs) with
| Some l' -> some_lit (ByStrX l')
| None -> pure @@ none_lit (bystrx_typ x) )
| _ -> builtin_fail "Crypto.to_bystr" ls

(* ByStrX -> ByStr *)
let to_bystr_type = tfun_typ "'A" @@ fun_typ (tvar "'A") bystr_typ

Expand All @@ -837,6 +850,20 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
| [ ByStrX bs ] -> pure @@ ByStr (Bystrx.to_bystr bs)
| _ -> builtin_fail "Crypto.to_bystr" ls

let substr_arity = 3

let substr_type =
fun_typ bystr_typ @@ fun_typ uint32_typ @@ fun_typ uint32_typ bystr_typ

let substr ls _ =
try
match ls with
| [ ByStr x; UintLit (Uint32L s); UintLit (Uint32L e) ] ->
pure
@@ ByStr (Bystr.sub x ~pos:(Uint32.to_int s) ~len:(Uint32.to_int e))
| _ -> builtin_fail "Crypto.substr" ls
with Invalid_argument msg -> builtin_fail ("Crypto.substr: " ^ msg) ls

let to_uint256_type = tfun_typ "'A" @@ fun_typ (tvar "'A") uint256_typ

let to_uint256_arity = 1
Expand Down Expand Up @@ -908,11 +935,14 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
match ts with
| [ PrimType (Bystrx_typ w1); PrimType (Bystrx_typ w2) ] ->
elab_tfun_with_args_no_gas sc (ts @ [ bystrx_typ (w1 + w2) ])
| [ PrimType Bystr_typ; PrimType Bystr_typ ] ->
elab_tfun_with_args_no_gas sc (ts @ [ bystr_typ ])
| _ -> fail0 "Failed to elaborate"

let concat ls _ =
match ls with
| [ ByStrX bs1; ByStrX bs2 ] -> pure @@ ByStrX (Bystrx.concat bs1 bs2)
| [ ByStr bs1; ByStr bs2 ] -> pure @@ ByStr (Bystr.concat bs1 bs2)
| _ -> builtin_fail "Crypto.concat" ls

let[@warning "-32"] ec_gen_key_pair_type =
Expand Down Expand Up @@ -1299,6 +1329,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct

(* All built-in functions *)
let built_in_multidict : builtin -> built_in_record list = function
(* Polymorphic builtins *)
| Builtin_eq -> [String.eq_arity, String.eq_type, elab_id, String.eq;
BNum.eq_arity, BNum.eq_type, elab_id , BNum.eq;
Crypto.eq_arity, Crypto.eq_type, Crypto.eq_elab, Crypto.eq;
Expand All @@ -1308,8 +1339,9 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
Crypto.concat_arity, Crypto.concat_type, Crypto.concat_elab, Crypto.concat]
| Builtin_to_uint256 -> [Crypto.to_uint256_arity, Crypto.to_uint256_type, Crypto.to_uint256_elab, Crypto.to_uint256;
Uint.to_uint_arity, Uint.to_uint_type, Uint.to_uint_elab Bits256, Uint.to_uint256]
(* Strings *)
| Builtin_substr -> [String.substr_arity, String.substr_type, elab_id, String.substr]
| Builtin_substr -> [String.substr_arity, String.substr_type, elab_id, String.substr;
Crypto.substr_arity, Crypto.substr_type, elab_id, Crypto.substr
]
| Builtin_strlen -> [String.strlen_arity, String.strlen_type, elab_id, String.strlen]
| Builtin_to_string -> [String.to_string_arity, String.to_string_type, String.to_string_elab, String.to_string]

Expand All @@ -1323,6 +1355,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
| Builtin_keccak256hash -> [Crypto.hash_arity, Crypto.hash_type,Crypto.hash_elab, Crypto.keccak256hash]
| Builtin_ripemd160hash -> [Crypto.hash_arity, Crypto.ripemd160hash_type,Crypto.hash_elab, Crypto.ripemd160hash]
| Builtin_to_bystr -> [Crypto.to_bystr_arity, Crypto.to_bystr_type, Crypto.to_bystr_elab, Crypto.to_bystr]
| Builtin_to_bystrx i -> [Crypto.to_bystrx_arity, Crypto.to_bystrx_type i, elab_id, Crypto.to_bystrx i]
| Builtin_bech32_to_bystr20 -> [Crypto.bech32_to_bystr20_arity, Crypto.bech32_to_bystr20_type, elab_id, Crypto.bech32_to_bystr20]
| Builtin_bystr20_to_bech32 -> [Crypto.bystr20_to_bech32_arity, Crypto.bystr20_to_bech32_type, elab_id, Crypto.bystr20_to_bech32]
| Builtin_schnorr_verify -> [Crypto.schnorr_verify_arity, Crypto.schnorr_verify_type, elab_id, Crypto.schnorr_verify]
Expand Down
156 changes: 85 additions & 71 deletions src/base/Gas.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -320,6 +320,19 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
match (op, types, args) with
| Builtin_eq, [ PrimType Bystr_typ; PrimType Bystr_typ ], [ a1; _ ] ->
pure @@ GasGasCharge.SizeOf (GI.get_id a1)
| ( Builtin_substr,
[
PrimType Bystr_typ;
PrimType (Uint_typ Bits32);
PrimType (Uint_typ Bits32);
],
[ s; i1; i2 ] ) ->
pure
@@ GasGasCharge.MinOf
( GasGasCharge.SizeOf (GI.get_id s),
GasGasCharge.SumOf
( GasGasCharge.ValueOf (GI.get_id i1),
GasGasCharge.ValueOf (GI.get_id i2) ) )
| Builtin_eq, [ a1; a2 ], _
when is_bystrx_type a1 && is_bystrx_type a2
&& Option.(value_exn (bystrx_width a1) = value_exn (bystrx_width a2))
Expand Down Expand Up @@ -360,6 +373,8 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
GasGasCharge.ProdOf (GasGasCharge.StaticCost 15, x) ))
| Builtin_to_bystr, [ a ], _ when is_bystrx_type a ->
pure (GasGasCharge.StaticCost (Option.value_exn (bystrx_width a)))
| Builtin_to_bystrx i, [ PrimType Bystr_typ ], _ ->
pure (GasGasCharge.StaticCost i)
| Builtin_bech32_to_bystr20, _, [ prefix; addr ]
| Builtin_bystr20_to_bech32, _, [ prefix; addr ] ->
let base = 4 in
Expand All @@ -369,6 +384,11 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
( GasGasCharge.SizeOf (GI.get_id prefix),
GasGasCharge.SizeOf (GI.get_id addr) ),
GasGasCharge.StaticCost base ))
| Builtin_concat, [ PrimType Bystr_typ; PrimType Bystr_typ ], [ s1; s2 ] ->
pure
@@ GasGasCharge.SumOf
( GasGasCharge.SizeOf (GI.get_id s1),
GasGasCharge.SizeOf (GI.get_id s2) )
| Builtin_concat, [ a1; a2 ], _ when is_bystrx_type a1 && is_bystrx_type a2
->
pure
Expand Down Expand Up @@ -460,88 +480,85 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
[@@@ocamlformat "disable"]

(* built-in op costs are propotional to size of data they operate on. *)
let builtin_records : builtin_record list = [
(* Strings *)
(Builtin_eq, [string_typ;string_typ], string_coster);
(Builtin_concat, [string_typ;string_typ], string_coster);
(Builtin_substr, [string_typ; tvar "'A"; tvar "'A"], string_coster);
(Builtin_strlen, [string_typ], string_coster);
(Builtin_to_string, [tvar "'A"], string_coster);
let builtin_records_find = function
(* Polymorhpic *)
| Builtin_eq -> [
([string_typ;string_typ], string_coster);
([bnum_typ;bnum_typ], bnum_coster);
([tvar "'A"; tvar "'A"], crypto_coster);
([tvar "'A"; tvar "'A"], int_coster)
];
| Builtin_substr -> [
([string_typ; tvar "'A"; tvar "'A"], string_coster);
([bystr_typ; uint32_typ; uint32_typ], crypto_coster)
];
| Builtin_concat -> [
([string_typ;string_typ], string_coster);
([tvar "'A"; tvar "'A"], crypto_coster)
];
| Builtin_to_uint256 -> [
([tvar "'A"], crypto_coster); ([tvar "'A"], int_conversion_coster 256)
];

(* Strings *)
| Builtin_strlen -> [([string_typ], string_coster)];
| Builtin_to_string -> [([tvar "'A"], string_coster)];

(* Block numbers *)
(Builtin_eq, [bnum_typ;bnum_typ], bnum_coster);
(Builtin_blt, [bnum_typ;bnum_typ], bnum_coster);
(Builtin_badd, [bnum_typ;tvar "'A"], bnum_coster);
(Builtin_bsub, [bnum_typ;bnum_typ], bnum_coster);
| Builtin_blt -> [([bnum_typ;bnum_typ], bnum_coster)];
| Builtin_badd -> [([bnum_typ;tvar "'A"], bnum_coster)];
| Builtin_bsub -> [([bnum_typ;bnum_typ], bnum_coster)];

(* Crypto *)
(Builtin_eq, [tvar "'A"; tvar "'A"], crypto_coster);
(Builtin_to_bystr, [tvar "'A"], crypto_coster);
(Builtin_bech32_to_bystr20, [string_typ;string_typ], crypto_coster);
(Builtin_bystr20_to_bech32, [string_typ;bystrx_typ address_length], crypto_coster);
(Builtin_to_uint256, [tvar "'A"], crypto_coster);
(Builtin_sha256hash, [tvar "'A"], crypto_coster);
(Builtin_keccak256hash, [tvar "'A"], crypto_coster);
(Builtin_ripemd160hash, [tvar "'A"], crypto_coster);
(Builtin_schnorr_verify, [bystrx_typ pubkey_len; bystr_typ; bystrx_typ signature_len], crypto_coster);
(Builtin_ecdsa_verify, [bystrx_typ Secp256k1Wrapper.pubkey_len; bystr_typ; bystrx_typ Secp256k1Wrapper.signature_len], crypto_coster);
(Builtin_concat, [tvar "'A"; tvar "'A"], crypto_coster);
(Builtin_schnorr_get_address, [bystrx_typ pubkey_len], crypto_coster);
(Builtin_alt_bn128_G1_add, [g1point_type; g1point_type], crypto_coster);
(Builtin_alt_bn128_G1_mul, [g1point_type; scalar_type], crypto_coster);
(Builtin_alt_bn128_pairing_product, [g1g2pair_list_type], crypto_coster);
| Builtin_to_bystr -> [([tvar "'A"], crypto_coster)];
| Builtin_to_bystrx _ -> [([tvar "'A"], crypto_coster)];
| Builtin_bech32_to_bystr20 -> [([string_typ;string_typ], crypto_coster)];
| Builtin_bystr20_to_bech32 -> [([string_typ;bystrx_typ address_length], crypto_coster)];
| Builtin_sha256hash -> [([tvar "'A"], crypto_coster)];
| Builtin_keccak256hash -> [([tvar "'A"], crypto_coster)];
| Builtin_ripemd160hash -> [([tvar "'A"], crypto_coster)];
| Builtin_schnorr_verify -> [([bystrx_typ pubkey_len; bystr_typ; bystrx_typ signature_len], crypto_coster)];
| Builtin_ecdsa_verify -> [([bystrx_typ Secp256k1Wrapper.pubkey_len; bystr_typ; bystrx_typ Secp256k1Wrapper.signature_len], crypto_coster)];
| Builtin_schnorr_get_address -> [([bystrx_typ pubkey_len], crypto_coster)];
| Builtin_alt_bn128_G1_add -> [([g1point_type; g1point_type], crypto_coster)];
| Builtin_alt_bn128_G1_mul -> [([g1point_type; scalar_type], crypto_coster)];
| Builtin_alt_bn128_pairing_product -> [([g1g2pair_list_type], crypto_coster)];

(* Maps *)
(Builtin_contains, [tvar "'A"; tvar "'A"], map_coster);
(Builtin_put, [tvar "'A"; tvar "'A"; tvar "'A"], map_coster);
(Builtin_get, [tvar "'A"; tvar "'A"], map_coster);
(Builtin_remove, [tvar "'A"; tvar "'A"], map_coster);
(Builtin_to_list, [tvar "'A"], map_coster);
(Builtin_size, [tvar "'A"], map_coster);
| Builtin_contains -> [([tvar "'A"; tvar "'A"], map_coster)];
| Builtin_put -> [([tvar "'A"; tvar "'A"; tvar "'A"], map_coster)];
| Builtin_get -> [([tvar "'A"; tvar "'A"], map_coster)];
| Builtin_remove -> [([tvar "'A"; tvar "'A"], map_coster)];
| Builtin_to_list -> [([tvar "'A"], map_coster)];
| Builtin_size -> [([tvar "'A"], map_coster)];

(* Integers *)
(Builtin_eq, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_lt, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_add, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_sub, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_mul, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_div, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_rem, [tvar "'A"; tvar "'A"], int_coster);
(Builtin_pow, [tvar "'A"; uint32_typ], int_coster);
(Builtin_isqrt, [tvar "'A"], int_coster);
| Builtin_lt -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_add -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_sub -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_mul -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_div -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_rem -> [([tvar "'A"; tvar "'A"], int_coster)];
| Builtin_pow -> [([tvar "'A"; uint32_typ], int_coster)];
| Builtin_isqrt -> [([tvar "'A"], int_coster)];

(Builtin_to_int32, [tvar "'A"], int_conversion_coster 32);
(Builtin_to_int64, [tvar "'A"], int_conversion_coster 64);
(Builtin_to_int128, [tvar "'A"], int_conversion_coster 128);
(Builtin_to_int256, [tvar "'A"], int_conversion_coster 256);
(Builtin_to_uint32, [tvar "'A"], int_conversion_coster 32);
(Builtin_to_uint64, [tvar "'A"], int_conversion_coster 64);
(Builtin_to_uint128, [tvar "'A"], int_conversion_coster 128);
(Builtin_to_uint256, [tvar "'A"], int_conversion_coster 256);
| Builtin_to_int32 -> [([tvar "'A"], int_conversion_coster 32)];
| Builtin_to_int64 -> [([tvar "'A"], int_conversion_coster 64)];
| Builtin_to_int128 -> [([tvar "'A"], int_conversion_coster 128)];
| Builtin_to_int256 -> [([tvar "'A"], int_conversion_coster 256)];
| Builtin_to_uint32 -> [([tvar "'A"], int_conversion_coster 32)];
| Builtin_to_uint64 -> [([tvar "'A"], int_conversion_coster 64)];
| Builtin_to_uint128 -> [([tvar "'A"], int_conversion_coster 128)];

(Builtin_to_nat, [uint32_typ], to_nat_coster);
]
| Builtin_to_nat -> [([uint32_typ], to_nat_coster)];

[@@@ocamlformat "enable"]

let builtin_hashtbl =
let open Caml in
let ht : (builtin, builtin_record list) Hashtbl.t = Hashtbl.create 64 in
List.iter
(fun row ->
let opname, _, _ = row in
match Hashtbl.find_opt ht opname with
| Some p -> Hashtbl.add ht opname (row :: p)
| None -> Hashtbl.add ht opname [ row ])
builtin_records;
ht

let builtin_cost (op, _) arg_types arg_ids =
let matcher (name, types, fcoster) =
let matcher (types, fcoster) =
(* The names and type list lengths must match and *)
if
[%equal: Syntax.builtin] name op
&& List.length types = List.length arg_types
List.length types = List.length arg_types
&& List.for_all2_exn
~f:(fun t1 t2 ->
(* the types should match *)
Expand All @@ -556,11 +573,8 @@ module ScillaGas (SR : Rep) (ER : Rep) = struct
let msg =
sprintf "Unable to determine gas cost for \"%s\"" (pp_builtin op)
in
let dict =
match Caml.Hashtbl.find_opt builtin_hashtbl op with
| Some rows -> rows
| None -> []
let%bind _, cost =
tryM (builtin_records_find op) ~f:matcher ~msg:(fun () -> mk_error0 msg)
in
let%bind _, cost = tryM dict ~f:matcher ~msg:(fun () -> mk_error0 msg) in
pure cost
end
6 changes: 6 additions & 0 deletions src/base/Literal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,8 @@ module type ScillaLiteral = sig

val equal : t -> t -> bool

val sub : t -> pos:int -> len:int -> t

val concat : t -> t -> t
end

Expand Down Expand Up @@ -252,6 +254,8 @@ module MkLiteral (T : ScillaType) = struct

val equal : t -> t -> bool

val sub : t -> pos:int -> len:int -> t

val concat : t -> t -> t
end

Expand All @@ -278,6 +282,8 @@ module MkLiteral (T : ScillaType) = struct

let equal = String.equal

let sub = String.sub

let concat = ( ^ )
end

Expand Down
9 changes: 8 additions & 1 deletion src/base/Syntax.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ type builtin =
| Builtin_keccak256hash
| Builtin_ripemd160hash
| Builtin_to_bystr
| Builtin_to_bystrx of int
| Builtin_bech32_to_bystr20
| Builtin_bystr20_to_bech32
| Builtin_schnorr_verify
Expand Down Expand Up @@ -102,6 +103,7 @@ let pp_builtin b =
| Builtin_keccak256hash -> "keccak256hash"
| Builtin_ripemd160hash -> "ripemd160hash"
| Builtin_to_bystr -> "to_bystr"
| Builtin_to_bystrx i -> "to_bystr" ^ Int.to_string i
| Builtin_bech32_to_bystr20 -> "bech32_to_bystr20"
| Builtin_bystr20_to_bech32 -> "bystr20_to_bech32"
| Builtin_schnorr_verify -> "schnorr_verify"
Expand Down Expand Up @@ -178,7 +180,12 @@ let parse_builtin s loc =
| "to_uint64" -> Builtin_to_uint64
| "to_uint128" -> Builtin_to_uint128
| "to_nat" -> Builtin_to_nat
| _ -> raise (SyntaxError (sprintf "\"%s\" is not a builtin" s, loc))
| _ -> (
try
let size = String.chop_prefix_exn s ~prefix:"to_bystr" in
Builtin_to_bystrx (Int.of_string size)
with Invalid_argument _ | Failure _ ->
raise @@ SyntaxError (sprintf "\"%s\" is not a builtin" s, loc) )

(*******************************************************)
(* Types of components *)
Expand Down
23 changes: 22 additions & 1 deletion tests/eval/good/builtin-eq-bystr.scilexp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,25 @@ let cc = builtin to_bystr c in
let r1 = builtin eq aa bb in
let r11 = negb r1 in
let r2 = builtin eq aa cc in
andb r11 r2
let res1 = andb r11 r2 in

let ab = builtin concat a b in
let ab2 = 0x0f0fbfbf in

let zero = Uint32 0 in
let one = Uint32 1 in
let two = Uint32 2 in

let a = builtin to_bystr a in
let a1 = builtin substr a zero one in
let a2 = builtin substr a one one in
let aa1 = builtin substr a zero two in
let aa2 = builtin concat a1 a2 in
let res2 = builtin eq aa1 aa2 in
let res3 = builtin eq aa1 a in
let res4 = andb res2 res3 in

let res5 = builtin eq ab ab2 in
let res6 = andb res4 res5 in

res6
Loading