Zilliqa · jjcnn · Mar 8, 2021 · Mar 8, 2021
diff --git a/src/base/ScillaParser.mly b/src/base/ScillaParser.mly
@@ -352,22 +352,14 @@ type_term :
 
 stmt:
 | l = ID; FETCH; r = sid   { (Load (to_loc_id l (toLoc $startpos(l)), ParserIdentifier.mk_id r (toLoc $startpos(r))), toLoc $startpos) }
-| l = ID; REMOTEFETCH; adr = ID; PERIOD; r = sid
-    { (RemoteLoad (to_loc_id l (toLoc $startpos(l)),
-                   to_loc_id adr (toLoc $startpos(adr)),
-                   ParserIdentifier.mk_id r (toLoc $startpos(r))),
-       toLoc $startpos) }
+| r = remote_fetch_stmt { r }
 | l = ID; ASSIGN; r = sid { (Store ( to_loc_id l (toLoc $startpos(l)), ParserIdentifier.mk_id r (toLoc $startpos(r))), toLoc $startpos) }
 | l = ID; EQ; r = exp    { (Bind ( to_loc_id l (toLoc $startpos(l)), r), toLoc $startpos) }
 | l = ID; FETCH; AND; c = CID { (ReadFromBC ( to_loc_id l (toLoc $startpos(l)), c), toLoc $startpos) }
 | l = ID; FETCH; r = ID; keys = nonempty_list(map_access)
   { MapGet( to_loc_id l (toLoc $startpos(l)), to_loc_id r (toLoc $startpos(r)), keys, true), toLoc $startpos }
-| l = ID; REMOTEFETCH; adr = ID; PERIOD; r = ID; keys = nonempty_list(map_access)
-  { RemoteMapGet(to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r)), keys, true), toLoc $startpos }
 | l = ID; FETCH; EXISTS; r = ID; keys = nonempty_list(map_access)
   { MapGet( to_loc_id l (toLoc $startpos(l)), to_loc_id r (toLoc $startpos(r)), keys, false), toLoc $startpos }
-| l = ID; REMOTEFETCH; EXISTS; adr = ID; PERIOD; r = ID; keys = nonempty_list(map_access)
-  { RemoteMapGet(to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r)), keys, false), toLoc $startpos }
 | l = ID; keys = nonempty_list(map_access); ASSIGN; r = sid
   { MapUpdate( to_loc_id l (toLoc $startpos(l)), keys, Some (ParserIdentifier.mk_id r (toLoc $startpos(r)))), toLoc $startpos }
 | DELETE; l = ID; keys = nonempty_list(map_access)
@@ -386,6 +378,17 @@ stmt:
   FORALL; l = sident; p = component_id
   { Iterate (l, p), toLoc $startpos }
 
+remote_fetch_stmt:
+| l = ID; REMOTEFETCH; adr = ID; PERIOD; r = sident
+  { RemoteLoad (to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), r), toLoc $startpos }
+| (* Reading _sender._balance or _origin._balance *)
+  l = ID; REMOTEFETCH; adr = SPID; PERIOD; r = SPID
+  { RemoteLoad (to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r))), toLoc $startpos }
+| l = ID; REMOTEFETCH; adr = ID; PERIOD; r = ID; keys = nonempty_list(map_access)
+  { RemoteMapGet(to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r)), keys, true), toLoc $startpos }
+| l = ID; REMOTEFETCH; EXISTS; adr = ID; PERIOD; r = ID; keys = nonempty_list(map_access)
+  { RemoteMapGet(to_loc_id l (toLoc $startpos(l)), to_loc_id adr (toLoc $startpos(adr)), to_loc_id r (toLoc $startpos(r)), keys, false), toLoc $startpos }
+
 stmt_pm_clause:
 | BAR ; p = pattern ; ARROW ;
   ss = separated_list(SEMICOLON, stmt) { p, ss }

diff --git a/src/eval/Eval.ml b/src/eval/Eval.ml
@@ -348,7 +348,7 @@ let rec stmt_eval conf stmts =
           let%bind a = fromR @@ Configuration.lookup conf adr in
           match a with
           | ByStrX s' when Bystrx.width s' = Type.address_length ->
-              let%bind l = Configuration.remote_load s' r in
+              let%bind l = Configuration.remote_load conf s' r in
               let conf' = Configuration.bind conf (get_id x) l in
               stmt_eval conf' sts
           | _ -> fail0 "Expected remote load address to be ByStr20 value" )

diff --git a/src/eval/EvalUtil.ml b/src/eval/EvalUtil.ml
@@ -167,6 +167,15 @@ module Configuration = struct
 
   let store i l = fromR @@ StateService.update ~fname:i ~keys:[] ~value:l
 
+  let lookup st k = Env.lookup st.env k
+
+  (* Helper function for remote fetches *)
+  let lookup_sender_addr st =
+    let%bind sender = fromR @@ lookup st (mk_loc_id (label_name_of_string MessagePayload.sender_label)) in
+    match sender with
+    | EvalLiteral.ByStrX bs -> pure bs
+    | _ -> fail0 (sprintf "Incorrect type of _sender in environment: %s" (pp_literal sender))
+
   let load st k =
     let i = get_id k in
     if [%equal: EvalName.t] i balance_label then
@@ -183,13 +192,30 @@ module Configuration = struct
                (EvalName.as_error_string i))
             (ER.get_loc (get_rep k))
 
-  let remote_load caddr k =
+  let remote_load st caddr k =
     let%bind fval =
       fromR
       @@ StateService.external_fetch ~caddr ~fname:k ~keys:[] ~ignoreval:false
     in
     match fval with
-    | Some v, _ -> pure v
+    | Some v, _ ->
+        (* _sender._balance is a special case if funds have been accepted. _amount must be deducted. *)
+        let%bind sender_addr = lookup_sender_addr st in
+        if st.accepted &&
+           EvalLiteral.Bystrx.equal sender_addr caddr &&
+           EvalName.equal (get_id k) balance_label
+        then
+          let%bind amount_lit = fromR @@ lookup st (mk_loc_id (label_name_of_string MessagePayload.amount_label)) in
+          match v, amount_lit with
+          | UintLit (Uint128L sender_balance), UintLit (Uint128L amount)
+            when Uint128.compare sender_balance amount >= 0 -> 
+              pure @@ EvalLiteral.UintLit (Uint128L (Uint128.(sender_balance - amount)))
+          | _ ->
+              fail0
+              @@ sprintf "Unexpected sender balance or amount literal: sender balance = %s, amount = %s"
+                (pp_literal v) (pp_literal amount_lit)
+        else 
+          pure v
     | _ ->
         fail1
           (Printf.sprintf "Error loading field %s"
@@ -286,24 +312,38 @@ module Configuration = struct
         in
         pure { st with env = kvs @ filtered_env }
 
-  let lookup st k = Env.lookup st.env k
-
   let bc_lookup st k = BlockchainState.lookup st.blockchain_state k
 
   let accept_incoming st =
-    let incoming' = st.incoming_funds in
-    (* Although unsigned integer is used, and this check isn't
-     * necessary, we have it just in case, somehow a malformed
-     * Uint128 literal manages to reach here. *)
-    if Uint128.compare incoming' Uint128.zero >= 0 then
-      let balance = Uint128.add st.balance incoming' in
-      let accepted = true in
-      let incoming_funds = Uint128.zero in
-      pure @@ { st with balance; accepted; incoming_funds }
+    if st.accepted then
+      (* Do nothing *)
+      pure st
     else
-      fail0
-      @@ sprintf "Incoming balance is negative (somehow):%s."
-           (Uint128.to_string incoming')
+      (* Check that sender balance is sufficient *)
+      let%bind sender_addr = lookup_sender_addr st in
+      let%bind sender_balance_l = remote_load st sender_addr (mk_loc_id balance_label) in
+      let incoming' = st.incoming_funds in
+      match sender_balance_l with
+      | UintLit (Uint128L sender_balance) ->
+          if Uint128.compare incoming' sender_balance >= 0 then
+            fail0 "Insufficient sender balance for acceptance."
+        else
+          (* Although unsigned integer is used, and this check isn't
+           * necessary, we have it just in case, somehow a malformed
+           * Uint128 literal manages to reach here. *)
+        if Uint128.compare incoming' Uint128.zero >= 0 then
+          let balance = Uint128.add st.balance incoming' in
+          let accepted = true in
+          let incoming_funds = Uint128.zero in
+          pure @@ { st with balance; accepted; incoming_funds }
+        else
+          fail0
+          @@ sprintf "Incoming balance is negative (somehow):%s."
+            (Uint128.to_string incoming')
+      | _ ->
+          fail0
+          @@ sprintf "Unrecognized balance literal at sender: %s"
+            (pp_literal sender_balance_l)
 
   (* Finds a procedure proc_name, and returns the procedure and the
      list of procedures in scope for that procedure *)

diff --git a/tests/base/parser/bad/gold/cmodule-field-id-colon-cid-eq-hexlit-with.scilla.gold b/tests/base/parser/bad/gold/cmodule-field-id-colon-cid-eq-hexlit-with.scilla.gold
@@ -1,7 +1,7 @@
 {
   "errors": [
     {
-      "error_message": "Syntax error, state number 314",
+      "error_message": "Syntax error, state number 318",
       "start_location": {
         "file":
           "base/parser/bad/cmodule-field-id-colon-cid-eq-hexlit-with.scilla",

diff --git a/tests/checker/good/gold/remote_state_reads.scilla.gold b/tests/checker/good/gold/remote_state_reads.scilla.gold
@@ -29,7 +29,10 @@
       { "field": "remote_reads_test_res_3_10", "tag": "NotMoney" },
       { "field": "remote_reads_test_res_3_11", "tag": "(Option NoInfo)" },
       { "field": "remote_reads_test_res_3_12", "tag": "NotMoney" },
-      { "field": "remote_reads_test_res_3_13", "tag": "(Option NoInfo)" }
+      { "field": "remote_reads_test_res_3_13", "tag": "(Option NoInfo)" },
+      { "field": "sender_balance_pre", "tag": "NoInfo" },
+      { "field": "sender_balance_mid", "tag": "NoInfo" },
+      { "field": "sender_balance_post", "tag": "NoInfo" }
     ],
     "ADT constructors": []
   },
@@ -136,7 +139,10 @@
         "vname": "remote_reads_test_res_3_13",
         "type": "Option (Bool)",
         "depth": 0
-      }
+      },
+      { "vname": "sender_balance_pre", "type": "Uint128", "depth": 0 },
+      { "vname": "sender_balance_mid", "type": "Uint128", "depth": 0 },
+      { "vname": "sender_balance_post", "type": "Uint128", "depth": 0 }
     ],
     "transitions": [
       {
@@ -178,7 +184,8 @@
       },
       { "vname": "OutgoingMsgTest", "params": [] },
       { "vname": "ExceptionTest", "params": [] },
-      { "vname": "AssignTest", "params": [] }
+      { "vname": "AssignTest", "params": [] },
+      { "vname": "SenderBalanceTest", "params": [] }
     ],
     "procedures": [],
     "events": [
@@ -244,9 +251,17 @@
   "warnings": [
     {
       "warning_message":
-        "No transition in contract RRContract contains an accept statement\n",
-      "start_location": { "file": "", "line": 0, "column": 0 },
-      "end_location": { "file": "", "line": 0, "column": 0 },
+        "transition SenderBalanceTest has a potential code path with duplicate accept statements:\n  Accept at contracts/remote_state_reads.scilla:177:3\n  Accept at contracts/remote_state_reads.scilla:181:3\n",
+      "start_location": {
+        "file": "contracts/remote_state_reads.scilla",
+        "line": 177,
+        "column": 3
+      },
+      "end_location": {
+        "file": "contracts/remote_state_reads.scilla",
+        "line": 181,
+        "column": 9
+      },
       "warning_id": 1
     }
   ],

diff --git a/tests/contracts/remote_state_reads.scilla b/tests/contracts/remote_state_reads.scilla
@@ -49,6 +49,9 @@ field remote_reads_test_res_3_11 : Option (Map (ByStr20 with end) Bool) = None {
 field remote_reads_test_res_3_12 : Bool = False (* exists signatures[key1][key2] of remote3 *)
 field remote_reads_test_res_3_13 : Option Bool = None {Bool} (* signatures[key1][key2] of remote3 *)
 
+field sender_balance_pre : Uint128 = Uint128 0
+field sender_balance_mid : Uint128 = Uint128 0
+field sender_balance_post : Uint128 = Uint128 0
 
 transition RemoteReadsTest(
   (* Any address in use - _balance is defined, but not _this_address *)
@@ -164,4 +167,18 @@ transition AssignTest()
   k1 = Uint128 1;
   k2 = Uint128 42;
   assign_test_10[k1][k2] := x
-end
+end
+
+(* Check that sender balance is deducted on acceptance *)
+transition SenderBalanceTest()
+  pre <-- _sender._balance;
+  sender_balance_pre := pre;
+  (* First accept should cause sender balance to decrease *)
+  accept;
+  mid <-- _sender._balance;
+  sender_balance_mid := mid;
+  (* Second accept should make no difference *)
+  accept;
+  post <-- _sender._balance;
+  sender_balance_post := post
+end
diff --git a/tests/runner/Testcontracts.ml b/tests/runner/Testcontracts.ml
@@ -375,7 +375,7 @@ let contract_tests env =
                 "remote_state_reads"
                 >: build_contract_init_test env succ_code "remote_state_reads" "init" ~is_library:false ~ipc_mode:true;
                 "remote_state_reads"
-                >::: build_contract_tests env "remote_state_reads" succ_code 1 8
+                >::: build_contract_tests env "remote_state_reads" succ_code 1 9
                        [];
                 "remote_state_reads"
                 >: build_contract_init_test env succ_code "remote_state_reads" "init_assignable_map_types" ~is_library:false ~ipc_mode:true;
@@ -430,7 +430,7 @@ let contract_tests env =
                 "remote_state_reads"
                   >: build_contract_init_test env fail_code "remote_state_reads" "init_wrong_map_type" ~is_library:false ~ipc_mode:true;
                 "remote_state_reads"
-                >::: build_contract_tests env "remote_state_reads" fail_code 101 126
+                >::: build_contract_tests env "remote_state_reads" fail_code 101 127
                        [];
               ];
          "misc_tests" >::: build_misc_tests env;

diff --git a/tests/runner/auction/state_1.json b/tests/runner/auction/state_1.json
@@ -19,5 +19,17 @@
     "vname": "pendingReturns",
     "type": "Map (ByStr20) (Uint128)",
     "value": []
+  },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678ab",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "242" }
+            ]
+        }
+    ]
   }
-]
+]
diff --git a/tests/runner/auction/state_2.json b/tests/runner/auction/state_2.json
@@ -19,5 +19,17 @@
       "vname": "pendingReturns",
       "type": "Map (ByStr20) (Uint128)",
       "value": []
-    }
+    },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678ab",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "242" }
+            ]
+        }
+    ]
+  }
 ]
diff --git a/tests/runner/auction/state_3.json b/tests/runner/auction/state_3.json
@@ -21,5 +21,17 @@
       "vname": "ended",
       "type": "Bool",
       "value": { "constructor": "False", "argtypes": [], "arguments": [] }
-    }
+    },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678cd",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "242" }
+            ]
+        }
+    ]
+  }
 ]
diff --git a/tests/runner/auction/state_4.json b/tests/runner/auction/state_4.json
@@ -21,5 +21,17 @@
       "vname": "ended",
       "type": "Bool",
       "value": { "constructor": "False", "argtypes": [], "arguments": [] }
-    }
+    },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678cd",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "542" }
+            ]
+        }
+    ]
+  }
 ]
diff --git a/tests/runner/auction/state_5.json b/tests/runner/auction/state_5.json
@@ -19,5 +19,17 @@
     "vname": "pendingReturns",
     "type": "Map (ByStr20) (Uint128)",
     "value": []
+  },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678cd",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "642" }
+            ]
+        }
+    ]
   }
-]
+]
diff --git a/tests/runner/cfinvoke/state_1.json b/tests/runner/cfinvoke/state_1.json
@@ -3,5 +3,17 @@
         "vname": "_balance",
         "type": "Uint128",
         "value": "0"
-    }
+    },
+  {
+    "vname": "_external",
+    "type": "Unit",
+    "value": [
+        {
+            "address": "0x12345678901234567890123456789012345678ab",
+            "state": [
+                { "vname": "_balance", "type": "Uint128", "value": "242" }
+            ]
+        }
+    ]
+  }
 ]