Require amounts to be nonnegative in semantics

theories/Blockchain.v

@@ -476,6 +476,7 @@ Inductive ActionEvaluation :
              {new_env : Environment}
              (from to : Address)
              (amount : Amount),
+        amount >= 0 ->
         amount <= account_balance pre from ->
         address_is_contract to = false ->
         act = build_act from (act_transfer to amount) ->
@@ -492,6 +493,7 @@ Inductive ActionEvaluation :
              (wc : WeakContract)
              (setup : SerializedValue)
              (state : SerializedValue),
+      amount >= 0 ->
       amount <= account_balance pre from ->
       address_is_contract to = true ->
       env_contracts pre to = None ->
@@ -517,6 +519,7 @@ Inductive ActionEvaluation :
              (prev_state : SerializedValue)
              (new_state : SerializedValue)
              (resp_acts : list ActionBody),
+      amount >= 0 ->
       amount <= account_balance pre from ->
       env_contracts pre to = Some wc ->
       env_contract_states pre to = Some prev_state ->
@@ -543,23 +546,23 @@ Context {pre : Environment} {act : Action}
 
 Definition eval_from : Address :=
   match eval with
-  | eval_transfer from _ _ _ _ _ _
-  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _
-  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
+  | eval_transfer from _ _ _ _ _ _ _
+  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _ _
+  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
   end.
 
 Definition eval_to : Address :=
   match eval with
-  | eval_transfer _ to _ _ _ _ _
-  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _
-  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ => to
+  | eval_transfer _ to _ _ _ _ _ _
+  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _ _
+  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ _ => to
   end.
 
 Definition eval_amount : Amount :=
   match eval with
-  | eval_transfer _ _ amount _ _ _ _
-  | eval_deploy _ _ amount _ _ _ _ _ _ _ _ _
-  | eval_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ => amount
+  | eval_transfer _ _ amount _ _ _ _ _
+  | eval_deploy _ _ amount _ _ _ _ _ _ _ _ _ _
+  | eval_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ _ => amount
   end.
 End Accessors.
 
@@ -744,11 +747,11 @@ Definition eval_tx {pre : Environment} {act : Action}
                    {post : Environment} {new_acts : list Action}
                    (step : ActionEvaluation pre act post new_acts) : Tx :=
   match step with
-  | eval_transfer from to amount _ _ _ _ =>
+  | eval_transfer from to amount _ _ _ _ _ =>
     build_tx from to amount tx_empty
-  | eval_deploy from to amount wc setup _ _ _ _ _ _ _ =>
+  | eval_deploy from to amount wc setup _ _ _ _ _ _ _ _ =>
     build_tx from to amount (tx_deploy wc setup)
-  | eval_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ =>
+  | eval_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ _ =>
     build_tx from to amount (tx_call msg)
   end.
 

theories/LocalBlockchain.v

@@ -94,6 +94,7 @@ Section ExecuteActions.
              (amount : Amount)
              (msg : option SerializedValue)
              (lc : LocalChain) : option (list Action * LocalChain) :=
+    do if amount <? 0 then None else Some tt;
     do if amount >? account_balance lc from then None else Some tt;
     match FMap.find to lc.(lc_contracts) with
     | None =>
@@ -119,6 +120,7 @@ Section ExecuteActions.
              (setup : SerializedValue)
              (lc : LocalChain)
     : option (list Action * LocalChain) :=
+    do if amount <? 0 then None else Some tt;
     do if amount >? account_balance lc from then None else Some tt;
     do contract_addr <- get_new_contract_addr lc;
     do match FMap.find contract_addr (lc_contracts lc) with
@@ -226,6 +228,15 @@ Section ExecuteActions.
     auto.
   Qed.
 
+  Lemma ltb_ge x y :
+    x <? y = false ->
+    x >= y.
+  Proof.
+    intros H.
+    apply Z.ltb_ge in H.
+    lia.
+  Qed.
+
   Lemma send_or_call_step from to amount msg act lc_before new_acts lc_after :
     send_or_call from to amount msg lc_before = Some (new_acts, lc_after) ->
     act = build_act from (match msg with
@@ -236,6 +247,8 @@ Section ExecuteActions.
   Proof.
     intros sent act_eq.
     unfold send_or_call in sent.
+    destruct (Z.ltb amount 0) eqn:amount_nonnegative;
+      [cbn in *; congruence|].
     destruct (Z.gtb amount (account_balance lc_before from)) eqn:balance_enough;
       [cbn in *; congruence|].
     destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
@@ -248,7 +261,7 @@ Section ExecuteActions.
       match goal with
       | [p: SerializedValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
       end.
-      Hint Resolve gtb_le : core.
+      Hint Resolve gtb_le ltb_ge : core.
       apply (eval_call from to amount wc msg prev_state new_state resp_acts);
         try solve [cbn in *; auto; congruence].
       + rewrite <- receive.
@@ -286,6 +299,8 @@ Section ExecuteActions.
   Proof.
     intros dep act_eq.
     unfold deploy_contract in dep.
+    destruct (Z.ltb amount 0) eqn:amount_nonnegative;
+      [cbn in *; congruence|].
     destruct (Z.gtb amount (account_balance lc_before from)) eqn:balance_enough;
       [cbn in *; congruence|].
     destruct (get_new_contract_addr lc_before) as [contract_addr|] eqn:new_contract_addr;