Accounting tests

src/base/PrettyPrinters.ml

@@ -93,7 +93,8 @@ and literal_to_json lit =
             ("argtypes", `List argtl);
             ("arguments", `List argl);
           ]
-  | _ -> `Null
+  | Msg m -> `Assoc (List.map m ~f:(fun (s, _t, l') -> (s, literal_to_json l')))
+  | Clo _ | TAbs _ -> `Null
 
 let literal_to_jstring ?(pp = false) lit =
   let j = literal_to_json lit in

src/eval/Eval.ml

@@ -376,7 +376,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 conf s' r in
+              let%bind l = Configuration.remote_load s' r in
               let conf' = Configuration.bind conf (get_id x) l in
               stmt_eval conf' sts
           | _ ->
@@ -947,8 +947,6 @@ let handle_message (tenv, incoming_funds, procedures, stmts, tname) cstate =
   in
   let new_msgs = conf'.emitted in
   let new_events = conf'.events in
-  (* Make sure that we aren't too generous and subract funds *)
-  let%bind cstate'' = post_process_msgs cstate' new_msgs in
 
   (*Return new contract state, messages and events *)
-  pure (cstate'', new_msgs, new_events, conf'.accepted)
+  pure (cstate', new_msgs, new_events, conf'.accepted)

src/eval/EvalUtil.ml

@@ -191,40 +191,19 @@ module Configuration = struct
             ~inst:(EvalName.as_error_string i)
             (ER.get_loc (get_rep k))
 
-  let remote_load st caddr k =
+  let remote_load caddr k =
     let%bind fval =
       fromR
       @@ StateService.external_fetch ~caddr ~fname:k ~keys:[] ~ignoreval:false
     in
     match fval with
-    | 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 ~kind:"Unexpected sender balance or amount literal"
-                ~inst:
-                  (sprintf "sender balance = %s, amount = %s" (pp_literal v)
-                     (pp_literal amount_lit))
-        else pure v
+    | Some v, _ -> pure v
     | _ ->
-        fail1 ~kind:"Error loading field"
-          ~inst:(EvalName.as_error_string (get_id k))
+        fail1 ~kind:"Error loading remote field"
+          ~inst:
+            (Printf.sprintf "%s at address %s"
+               (EvalName.as_error_string (get_id k))
+               (SLiteral.Bystrx.hex_encoding caddr))
           (ER.get_loc (get_rep k))
 
   let remote_field_type caddr k =
@@ -394,37 +373,11 @@ module Configuration = struct
     if st.accepted then (* Do nothing *)
       pure st
     else
-      (* 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 ~kind:"Insufficient sender balance for acceptance"
-              ~inst:
-                ("Incoming vs sender_balance: "
-                ^ Uint128.to_string incoming'
-                ^ " vs "
-                ^ Uint128.to_string sender_balance)
-          else if
-            (* 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. *)
-            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 ~kind:"Incoming balance is negative (somehow)"
-              ~inst:(Uint128.to_string incoming')
-      | _ ->
-          fail0 ~kind:"Unrecognized balance literal at sender"
-            ~inst:(pp_literal sender_balance_l)
+      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 }
 
   (* Finds a procedure proc_name, and returns the procedure and the
      list of procedures in scope for that procedure *)
@@ -460,7 +413,7 @@ module Configuration = struct
                  String.compare s t)
         in
         if tag_found && amount_found && recipient_found && uniq_entries then
-          pure m'
+          pure ()
         else
           fail0
             ~kind:"Message is missing a mandatory field or has duplicate fields"
@@ -471,10 +424,32 @@ module Configuration = struct
 
   let send_messages conf ms =
     let%bind ls' = fromR @@ Datatypes.scilla_list_to_ocaml ms in
-    let%bind ls = mapM ~f:validate_outgoing_message ls' in
+    let%bind () = forallM ~f:validate_outgoing_message ls' in
+    let%bind out_funds =
+      foldM ls' ~init:Uint128.zero ~f:(fun run_total msg_lit ->
+          match msg_lit with
+          | SLiteral.Msg msg ->
+              let%bind amount = fromR @@ MessagePayload.get_amount msg in
+              pure Uint128.(run_total + amount)
+          | _ ->
+              fail0
+                ~kind:
+                  "Literal verified as a message, but is not a message literal"
+                ~inst:(pp_literal msg_lit))
+    in
     let old_emitted = conf.emitted in
-    let emitted = old_emitted @ ls in
-    pure { conf with emitted }
+    let emitted = old_emitted @ ls' in
+    let old_balance = conf.balance in
+    let%bind balance =
+      if Uint128.compare old_balance out_funds < 0 then
+        fail0 ~kind:"Balance too low for outgoing message"
+          ~inst:
+            (sprintf "Current balance: %s. Required balance: %s"
+               (Uint128.to_string old_balance)
+               (Uint128.to_string out_funds))
+      else pure @@ Uint128.(old_balance - out_funds)
+    in
+    pure { conf with emitted; balance }
 
   let validate_event m' =
     let open EvalLiteral in

tests/checker/good/Good.ml

@@ -94,6 +94,8 @@ module Tests = Scilla_test.Util.DiffBasedTests (struct
       "unbox_result5.scilla";
       "simple-dex-remote-reads.scilla";
       "type_casts.scilla";
+      "accounting_tests.scilla";
+      "accounting_tests_support.scilla";
       "timestamp.scilla";
       "codehash.scilla";
       "chainid.scilla";

tests/checker/good/gold/accounting_tests.scilla.gold

@@ -0,0 +1,177 @@
+{
+  "cashflow_tags": {
+    "State variables": [
+      { "field": "support_contract", "tag": "NotMoney" },
+      { "field": "test_string_1", "tag": "NoInfo" },
+      { "field": "test_string_2", "tag": "NoInfo" },
+      { "field": "outgoing_amount", "tag": "Money" },
+      { "field": "max_outgoing_msgs", "tag": "NotMoney" }
+    ],
+    "ADT constructors": []
+  },
+  "contract_info": {
+    "scilla_major_version": "0",
+    "vname": "AccountingTests",
+    "params": [
+      {
+        "vname": "support_contract",
+        "type":
+          "ByStr20 with contract field stored_strings : List (String) end"
+      }
+    ],
+    "fields": [
+      { "vname": "test_string_1", "type": "String", "depth": 0 },
+      { "vname": "test_string_2", "type": "String", "depth": 0 },
+      { "vname": "outgoing_amount", "type": "Uint128", "depth": 0 },
+      { "vname": "max_outgoing_msgs", "type": "Uint128", "depth": 0 }
+    ],
+    "transitions": [
+      { "vname": "Reset", "params": [] },
+      { "vname": "Test_Insufficient_Balance", "params": [] },
+      { "vname": "Test_Send_1", "params": [] },
+      { "vname": "Finalize_Test_Send_1", "params": [] },
+      { "vname": "Test_Send_2", "params": [] },
+      { "vname": "Finalize_Test_Send_2", "params": [] },
+      { "vname": "Test_Send_3", "params": [] },
+      { "vname": "Test_Send_3_Helper", "params": [] },
+      { "vname": "Finalize_Test_Send_3", "params": [] },
+      {
+        "vname": "CheckSenderBalance",
+        "params": [ { "vname": "expected_balance", "type": "Uint128" } ]
+      },
+      {
+        "vname": "CheckRecipientBalance",
+        "params": [ { "vname": "expected_balance", "type": "Uint128" } ]
+      },
+      { "vname": "Test_Send_4", "params": [] },
+      { "vname": "Test_Send_5", "params": [] },
+      { "vname": "Test_Send_6", "params": [] },
+      { "vname": "Test_Send_7", "params": [] },
+      { "vname": "Test_Send_8", "params": [] },
+      { "vname": "Test_Send_9", "params": [] },
+      { "vname": "Test_Send_10", "params": [] },
+      { "vname": "Test_Send_11", "params": [] },
+      { "vname": "Test_Send_12", "params": [] },
+      { "vname": "Test_Send_13", "params": [] },
+      { "vname": "Test_Send_14", "params": [] },
+      { "vname": "Test_Send_15", "params": [] },
+      { "vname": "Test_Send_16", "params": [] },
+      { "vname": "Test_Send_17", "params": [] },
+      { "vname": "Test_Send_18", "params": [] },
+      { "vname": "Test_Send_19", "params": [] }
+    ],
+    "procedures": [
+      { "vname": "AssertReset", "params": [] },
+      {
+        "vname": "Finalize_Test_Send_Helper_2_Msgs",
+        "params": [ { "vname": "test_no", "type": "Uint128" } ]
+      },
+      {
+        "vname": "CheckBalance",
+        "params": [ { "vname": "expected_balance", "type": "Uint128" } ]
+      },
+      {
+        "vname": "CheckSupportBalance",
+        "params": [ { "vname": "expected_balance", "type": "Uint128" } ]
+      }
+    ],
+    "events": [],
+    "ADTs": [
+      {
+        "tname": "Option",
+        "tparams": [ "'A" ],
+        "tmap": [
+          { "cname": "Some", "argtypes": [ "'A" ] },
+          { "cname": "None", "argtypes": [] }
+        ]
+      },
+      {
+        "tname": "Bool",
+        "tparams": [],
+        "tmap": [
+          { "cname": "True", "argtypes": [] },
+          { "cname": "False", "argtypes": [] }
+        ]
+      },
+      {
+        "tname": "Nat",
+        "tparams": [],
+        "tmap": [
+          { "cname": "Zero", "argtypes": [] },
+          { "cname": "Succ", "argtypes": [ "Nat" ] }
+        ]
+      },
+      {
+        "tname": "List",
+        "tparams": [ "'A" ],
+        "tmap": [
+          { "cname": "Cons", "argtypes": [ "'A", "List ('A)" ] },
+          { "cname": "Nil", "argtypes": [] }
+        ]
+      },
+      {
+        "tname": "Pair",
+        "tparams": [ "'A", "'B" ],
+        "tmap": [ { "cname": "Pair", "argtypes": [ "'A", "'B" ] } ]
+      }
+    ]
+  },
+  "warnings": [
+    {
+      "warning_message":
+        "Read only field, consider making it a contract parameter: test_string_2",
+      "start_location": {
+        "file": "contracts/accounting_tests.scilla",
+        "line": 83,
+        "column": 9
+      },
+      "end_location": { "file": "", "line": 0, "column": 0 },
+      "warning_id": 3
+    },
+    {
+      "warning_message":
+        "Read only field, consider making it a contract parameter: test_string_1",
+      "start_location": {
+        "file": "contracts/accounting_tests.scilla",
+        "line": 76,
+        "column": 9
+      },
+      "end_location": { "file": "", "line": 0, "column": 0 },
+      "warning_id": 3
+    },
+    {
+      "warning_message":
+        "Read only field, consider making it a contract parameter: outgoing_amount",
+      "start_location": {
+        "file": "contracts/accounting_tests.scilla",
+        "line": 45,
+        "column": 13
+      },
+      "end_location": { "file": "", "line": 0, "column": 0 },
+      "warning_id": 3
+    },
+    {
+      "warning_message":
+        "Read only field, consider making it a contract parameter: max_outgoing_msgs",
+      "start_location": {
+        "file": "contracts/accounting_tests.scilla",
+        "line": 46,
+        "column": 15
+      },
+      "end_location": { "file": "", "line": 0, "column": 0 },
+      "warning_id": 3
+    },
+    {
+      "warning_message": "Unused load statement to: s1",
+      "start_location": {
+        "file": "contracts/accounting_tests.scilla",
+        "line": 152,
+        "column": 3
+      },
+      "end_location": { "file": "", "line": 0, "column": 0 },
+      "warning_id": 3
+    }
+  ],
+  "gas_remaining": "7916"
+}
+