Remote state reads

src/base/BuiltIns.ml

@@ -370,6 +370,10 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
 
     let eq_elab sc targs ts =
       match (targs, ts) with
+      | [], [ bstyp1; bstyp2 ]
+        when (* Addresses should be compared as ByStr20 *)
+             is_address_type bstyp1 || is_address_type bstyp2 ->
+          elab_tfun_with_args_no_gas sc [ bystrx_typ Type.address_length ]
       | [], [ bstyp1; bstyp2 ]
         when (* We want both types to be ByStr with equal width. *)
              is_bystrx_type bstyp1 && [%equal: BIType.t] bstyp1 bstyp2 ->
@@ -390,7 +394,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
 
     (* RIPEMD-160 is a 160 bit hash, so define a separate type for it. *)
     let ripemd160hash_type =
-      tfun_typ "'A" @@ fun_typ (tvar "'A") (bystrx_typ address_length)
+      tfun_typ "'A" @@ fun_typ (tvar "'A") (bystrx_typ Type.address_length)
 
     (* ByStr -> Option ByStrX *)
     let to_bystrx_type x = fun_typ bystr_typ (option_typ (bystrx_typ x))
@@ -405,6 +409,8 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
     let to_bystr_elab sc targs ts =
       match (targs, ts) with
       | [], [ t ] when is_bystrx_type t -> elab_tfun_with_args_no_gas sc ts
+      | [], [ t ] when is_address_type t ->
+          elab_tfun_with_args_no_gas sc [ bystrx_typ Type.address_length ]
       | _, _ -> fail0 "Failed to elaborate"
 
     let substr_arity = 3
@@ -422,17 +428,21 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
       match (targs, ts) with
       | [], [ PrimType (Bystrx_typ w) ] when w <= int_bit_width_to_int x / 8 ->
           elab_tfun_with_args_no_gas sc ts
+      | [], [ t ]
+        when is_address_type t
+             && Type.address_length <= int_bit_width_to_int x / 8 ->
+          elab_tfun_with_args_no_gas sc [ bystrx_typ Type.address_length ]
       | _, _ -> fail0 "Failed to elaborate"
 
     let bech32_to_bystr20_type =
       fun_typ string_typ
-        (fun_typ string_typ (option_typ (bystrx_typ address_length)))
+        (fun_typ string_typ (option_typ (bystrx_typ Type.address_length)))
 
     let bech32_to_bystr20_arity = 2
 
     let bystr20_to_bech32_type =
       fun_typ string_typ
-        (fun_typ (bystrx_typ address_length) (option_typ string_typ))
+        (fun_typ (bystrx_typ Type.address_length) (option_typ string_typ))
 
     let bystr20_to_bech32_arity = 2
 
@@ -447,6 +457,15 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
       match (targs, ts) with
       | [], [ PrimType (Bystrx_typ w1); PrimType (Bystrx_typ w2) ] ->
           elab_tfun_with_args_no_gas sc (ts @ [ bystrx_typ (w1 + w2) ])
+      | [], [ t1; PrimType (Bystrx_typ w2) ] when is_address_type t1 ->
+          elab_tfun_with_args_no_gas sc
+            (ts @ [ bystrx_typ (Type.address_length + w2) ])
+      | [], [ PrimType (Bystrx_typ w1); t2 ] when is_address_type t2 ->
+          elab_tfun_with_args_no_gas sc
+            (ts @ [ bystrx_typ (w1 + Type.address_length) ])
+      | [], [ t1; t2 ] when is_address_type t1 && is_address_type t2 ->
+          elab_tfun_with_args_no_gas sc
+            (ts @ [ bystrx_typ (Type.address_length + Type.address_length) ])
       | [], [ PrimType Bystr_typ; PrimType Bystr_typ ] ->
           elab_tfun_with_args_no_gas sc (ts @ [ bystr_typ ])
       | _, _ -> fail0 "Failed to elaborate"
@@ -550,7 +569,7 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
         (bystrx_typ Secp256k1Wrapper.uncompressed_pubkey_len)
 
     let schnorr_get_address_type =
-      fun_typ (bystrx_typ pubkey_len) (bystrx_typ address_length)
+      fun_typ (bystrx_typ pubkey_len) (bystrx_typ Type.address_length)
 
     let schnorr_get_address_arity = 1
 
@@ -592,7 +611,8 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
 
     let contains_elab sc targs ts =
       match (targs, ts) with
-      | [], [ MapType (kt, vt); u ] when [%equal: BIType.t] kt u ->
+      | [], [ MapType (kt, vt); u ] when type_assignable ~expected:kt ~actual:u
+        ->
           elab_tfun_with_args_no_gas sc [ kt; vt ]
       | _, _ -> fail0 "Failed to elaborate"
 
@@ -607,7 +627,8 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
     let put_elab sc targs ts =
       match (targs, ts) with
       | [], [ MapType (kt, vt); kt'; vt' ]
-        when [%equal: BIType.t] kt kt' && [%equal: BIType.t] vt vt' ->
+        when type_assignable ~expected:kt ~actual:kt'
+             && type_assignable ~expected:vt ~actual:vt' ->
           elab_tfun_with_args_no_gas sc [ kt; vt ]
       | _, _ -> fail0 "Failed to elaborate"
 
@@ -621,7 +642,8 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
 
     let get_elab sc targs ts =
       match (targs, ts) with
-      | [], [ MapType (kt, vt); kt' ] when [%equal: BIType.t] kt kt' ->
+      | [], [ MapType (kt, vt); kt' ]
+        when type_assignable ~expected:kt ~actual:kt' ->
           elab_tfun_with_args_no_gas sc [ kt; vt ]
       | _, _ -> fail0 "Failed to elaborate"
 
@@ -634,7 +656,8 @@ module ScillaBuiltIns (SR : Rep) (ER : Rep) = struct
 
     let remove_elab sc targs ts =
       match (targs, ts) with
-      | [], [ MapType (kt, vt); u ] when [%equal: BIType.t] kt u ->
+      | [], [ MapType (kt, vt); u ] when type_assignable ~expected:kt ~actual:u
+        ->
           elab_tfun_with_args_no_gas sc [ kt; vt ]
       | _, _ -> fail0 "Failed to elaborate"
 

src/base/Cashflow.ml

@@ -187,6 +187,11 @@ struct
       match s with
       | Load (x, y) ->
           CFSyntax.Load (add_noinfo_to_ident x, add_noinfo_to_ident y)
+      | RemoteLoad (x, adr, y) ->
+          CFSyntax.RemoteLoad
+            ( add_noinfo_to_ident x,
+              add_noinfo_to_ident adr,
+              add_noinfo_to_ident y )
       | Store (x, y) ->
           CFSyntax.Store (add_noinfo_to_ident x, add_noinfo_to_ident y)
       | Bind (x, e) -> CFSyntax.Bind (add_noinfo_to_ident x, cf_init_tag_expr e)
@@ -203,6 +208,13 @@ struct
               add_noinfo_to_ident m,
               List.map ~f:add_noinfo_to_ident ks,
               retrieve )
+      | RemoteMapGet (x, adr, m, ks, retrieve) ->
+          CFSyntax.RemoteMapGet
+            ( add_noinfo_to_ident x,
+              add_noinfo_to_ident adr,
+              add_noinfo_to_ident m,
+              List.map ~f:add_noinfo_to_ident ks,
+              retrieve )
       | MatchStmt (x, pss) ->
           CFSyntax.MatchStmt
             ( add_noinfo_to_ident x,
@@ -423,6 +435,7 @@ struct
                           new_map
                       | _ -> targ_tag_map )
                   | PrimType _ | PolyFun (_, _) | Unit -> targ_tag_map
+                  | Address _ -> (* TODO *) targ_tag_map
                 in
                 let tvar_tag_map, _ =
                   List.fold_left arg_typs ~init:(init_targ_to_tag_map, arg_tags)
@@ -505,6 +518,7 @@ struct
     | Unit ->
         (* Ignore *)
         false
+    | Address _ -> (* TODO *) false
 
   let init_ctr_tag_map () =
     let open DataTypeDictionary in
@@ -1608,6 +1622,18 @@ struct
             (not @@ [%equal: ECFR.money_tag] (get_id_tag new_x) (get_id_tag x))
             || not
                @@ [%equal: ECFR.money_tag] (get_id_tag new_f) (get_id_tag f) )
+      | RemoteLoad (x, adr, f) ->
+          (* TODO - see Load case for inspiration *)
+          (* x is no longer in scope, so remove from local_env *)
+          let new_local_env =
+            AssocDictionary.remove (CFIdentifier.as_string x) local_env
+          in
+          ( RemoteLoad (x, adr, f),
+            param_env,
+            field_env,
+            new_local_env,
+            ctr_tag_map,
+            false )
       | Store (f, x) ->
           let new_f, new_x, new_param_env, new_field_env, new_local_env =
             cf_update_tag_for_field_assignment f x param_env field_env local_env
@@ -1734,6 +1760,18 @@ struct
             (not @@ [%equal: ECFR.money_tag] (get_id_tag x) new_x_tag)
             || (not @@ [%equal: ECFR.money_tag] (get_id_tag m) m_tag)
             || (not @@ [%equal: _] new_ks ks) )
+      | RemoteMapGet (x, adr, m, ks, fetch) ->
+          (* TODO - see MapGet case for inspiration *)
+          (* x is no longer in scope, so remove from local_env *)
+          let new_local_env =
+            AssocDictionary.remove (CFIdentifier.as_string x) local_env
+          in
+          ( RemoteMapGet (x, adr, m, ks, fetch),
+            param_env,
+            field_env,
+            new_local_env,
+            ctr_tag_map,
+            false )
       | MatchStmt (x, clauses) ->
           let ( res_clauses,
                 new_param_env,

src/base/ContractUtil.ml

@@ -17,6 +17,7 @@
 *)
 
 open Core_kernel
+open Type
 open Literal
 open Syntax
 open MonadUtil
@@ -43,11 +44,11 @@ module MessagePayload = struct
 
   let sender_label = "_sender"
 
-  let sender_type = CUType.bystrx_typ address_length
+  let sender_type = CUType.address_typ None
 
   let origin_label = "_origin"
 
-  let origin_type = CUType.bystrx_typ address_length
+  let origin_type = CUType.address_typ None
 
   let recipient_label = "_recipient"
 
@@ -123,6 +124,10 @@ let blocknum_type = CUType.bnum_typ
 
 let label_name_of_string str = CUName.parse_simple_name str
 
+let nonce_label = label_name_of_string "_nonce"
+
+let nonce_type = CUType.uint64_typ
+
 let balance_label = label_name_of_string "_balance"
 
 let balance_type = CUType.uint128_typ
@@ -146,7 +151,7 @@ module ScillaContractUtil (SR : Rep) (ER : Rep) = struct
   let balance_field =
     (CUIdentifier.mk_id balance_label ER.uint128_rep, balance_type)
 
-  let append_implict_contract_params tparams =
+  let append_implicit_contract_params tparams =
     let open CUType in
     let creation_block =
       (CUIdentifier.mk_id creation_block_label ER.bnum_rep, bnum_typ)
@@ -166,7 +171,7 @@ module ScillaContractUtil (SR : Rep) (ER : Rep) = struct
     List.filter args ~f:(fun a ->
         not (List.mem nonevalargs (fst a) ~equal:[%equal: CUName.t]))
 
-  let append_implict_comp_params cparams =
+  let append_implicit_comp_params cparams =
     let sender =
       ( CUIdentifier.mk_id
           (label_name_of_string MessagePayload.sender_label)

src/base/Disambiguate.ml

@@ -159,7 +159,7 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
     pure @@ PostDisSyntax.SIdentifier.mk_id dis_name (get_rep id)
 
   (* Local definition that does not need an address qualifier:
-     Local variables, fields, and procedure, transition and contract parameters,
+     Local variables, fields (local and remote), and procedure, transition and contract parameters,
      as well as non-type, non-constructor and non-variable names. *)
   let name_def_as_simple_global id =
     let open LocalName in
@@ -205,7 +205,17 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
           let%bind dis_t = recurse t in
           pure @@ PostDisType.PolyFun (tvar, dis_t)
       | Unit -> pure @@ PostDisType.Unit
+      | Address None -> pure @@ PostDisType.Address None
+      | Address (Some fts) ->
+          let%bind dis_fts =
+            mapM fts ~f:(fun (id, t) ->
+                let%bind dis_id = name_def_as_simple_global id in
+                let%bind dis_t = recurse t in
+                pure @@ (dis_id, dis_t))
+          in
+          pure @@ PostDisType.Address (Some dis_fts)
     in
+
     recurse t
 
   (**************************************************************)
@@ -514,6 +524,20 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
               remove_local_id_from_dict var_dict_acc (as_string x)
             in
             pure @@ (PostDisSyntax.Load (dis_x, dis_f), new_var_dict)
+        | RemoteLoad (x, adr, f) ->
+            let%bind dis_x = name_def_as_simple_global x in
+            (* adr may be defined anywhere, so must be disambiguated *)
+            let%bind dis_adr =
+              disambiguate_identifier_helper var_dict_acc (SR.get_loc rep) adr
+            in
+            (* f must be a field *)
+            let%bind dis_f = name_def_as_simple_global f in
+            (* x is now in scope as a local, so remove from var dictionary *)
+            let new_var_dict =
+              remove_local_id_from_dict var_dict_acc (as_string x)
+            in
+            pure
+            @@ (PostDisSyntax.RemoteLoad (dis_x, dis_adr, dis_f), new_var_dict)
         | Store (f, x) ->
             (* f must be a locally defined field *)
             let%bind dis_f = name_def_as_simple_global f in
@@ -561,6 +585,27 @@ module ScillaDisambiguation (SR : Rep) (ER : Rep) = struct
             in
             pure
             @@ (PostDisSyntax.MapGet (dis_x, dis_m, dis_ks, fetch), new_var_dict)
+        | RemoteMapGet (x, adr, m, ks, fetch) ->
+            let%bind dis_x = name_def_as_simple_global x in
+            (* adr may be defined anywhere, so must be disambiguated *)
+            let%bind dis_adr =
+              disambiguate_identifier_helper var_dict_acc (SR.get_loc rep) adr
+            in
+            (* m must be a field *)
+            let%bind dis_m = name_def_as_simple_global m in
+            let%bind dis_ks =
+              mapM ks
+                ~f:
+                  (disambiguate_identifier_helper var_dict_acc (SR.get_loc rep))
+            in
+            (* x is now in scope as a local, so remove from var dictionary *)
+            let new_var_dict =
+              remove_local_id_from_dict var_dict_acc (as_string x)
+            in
+            pure
+            @@ ( PostDisSyntax.RemoteMapGet
+                   (dis_x, dis_adr, dis_m, dis_ks, fetch),
+                 new_var_dict )
         | MatchStmt (x, pss) ->
             let%bind dis_x =
               disambiguate_identifier_helper var_dict_acc (SR.get_loc rep) x

src/base/EventInfo.ml

@@ -71,12 +71,27 @@ struct
               ~f:(fun (fname, pl) ->
                 let%bind t =
                   match pl with
-                  | MLit l -> literal_type l ~lc:bloc
+                  | MLit l ->
+                      let%bind t, dyn_checks = literal_type l ~lc:bloc in
+                      if not @@ List.is_empty dyn_checks then
+                        fail1
+                          (Printf.sprintf
+                             "Event type %s requires dynamic typecheck, which \
+                              shouldn't happen\n"
+                             eventname)
+                          bloc
+                      else pure t
                   | MVar v ->
                       let t' = ER.get_type (get_rep v) in
                       pure t'.tp
                 in
-                pure (fname, t))
+                let output_t =
+                  (* Output addresses as ByStr20 *)
+                  match t with
+                  | Address _ -> bystrx_typ Type.address_length
+                  | _ -> t
+                in
+                pure (fname, output_t))
               filtered_m
           in
           (* If we already have an entry for "eventname" in "acc",
@@ -94,9 +109,9 @@ struct
               let matcher m_types tlist =
                 List.length m_types = List.length tlist
                 && (* Check that each entry in tlist is equal to the same entry in m_types. *)
-                List.for_all tlist ~f:(fun (n1, t1) ->
-                    List.exists m_types ~f:(fun (n2, t2) ->
-                        String.(n1 = n2) && [%equal: EIType.t] t2 t1))
+                List.for_all tlist ~f:(fun (n1, actual) ->
+                    List.exists m_types ~f:(fun (n2, expected) ->
+                        String.(n1 = n2) && type_assignable ~expected ~actual))
               in
               if not @@ matcher m_types tlist then
                 fail1