Add builtins substr and concat for ByStr and to_bystrx to convert to …

…fixed length byte strings (#906)

* Add substr and concat for ByStr Scilla type

* Add builtin to_bystrx

* make fmt

* Update src/base/Syntax.ml

Co-authored-by: Anton Trunov <anton@zilliqa.com>

* remove unneeded comment

* Update src/base/Syntax.ml

Co-authored-by: Anton Trunov <anton@zilliqa.com>

* Add expected fail tests

* One more failing test

Co-authored-by: Anton Trunov <anton@zilliqa.com>

src/base/BuiltIns.ml

@@ -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
 
@@ -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
@@ -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 =
@@ -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;
@@ -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]
 
@@ -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]

src/base/Gas.ml

@@ -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))
@@ -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
@@ -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
@@ -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 *)
@@ -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

src/base/Literal.ml

@@ -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
 
@@ -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
 
@@ -278,6 +282,8 @@ module MkLiteral (T : ScillaType) = struct
 
     let equal = String.equal
 
+    let sub = String.sub
+
     let concat = ( ^ )
   end
 

src/base/Syntax.ml

@@ -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
@@ -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"
@@ -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                   *)

tests/eval/good/builtin-eq-bystr.scilexp

@@ -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