Piggy bank smart contract improvements (#240)

examples/piggybank/PiggyBank.v

@@ -79,17 +79,16 @@ Section PiggyBankImpl.
 
   Definition insert (state : State) (ctx : ContractCallContext) : Result :=
     let amount := ctx.(ctx_amount) in
-    do _ <- throwIf (amount <=? 0) error_amount_not_positive;
+    do _ <- throwIf (amount <? 0) error_amount_not_positive;
     do _ <- throwIf (is_smashed state) error_already_smashed;
     let state := state<| balance ::= Z.add amount |> in
     Ok (state, []).
 
   Definition smash (state : State) (ctx : ContractCallContext) : Result :=
     let owner := state.(owner) in
-    do _ <- throwIf (is_smashed state) error_already_smashed;
     do _ <- throwIf (address_neqb ctx.(ctx_from) owner) error_not_owner;
-    do _ <- throwIf (negb (ctx.(ctx_amount) =? 0)) error_amount_not_zero;
-    let acts := [act_transfer owner state.(balance)] in
+    do _ <- throwIf (is_smashed state) error_already_smashed;
+    let acts := [act_transfer owner (state.(balance) + ctx.(ctx_amount))] in
     let state := state<| balance := 0 |><| piggyState := Smashed |> in
     Ok (state, acts).
 

examples/piggybank/PiggyBankCorrect.v

@@ -22,7 +22,7 @@ Ltac insert_reduce :=
   match goal with
   | H : insert ?state ?ctx = _ |- _ =>
     unfold insert in H;
-    destruct (ctx_amount ctx <=? 0)%Z eqn:Epos in H; try discriminate;
+    destruct (ctx_amount ctx <? 0)%Z eqn:Epos in H; try discriminate;
     destruct (is_smashed state) eqn:Esmash in H; try discriminate
   end.
 
@@ -31,8 +31,7 @@ Ltac smash_reduce :=
   | H : smash ?state ?ctx = _ |- _ =>
     unfold smash in H;
     destruct (is_smashed state) eqn:Esmash in H; try discriminate;
-    destruct (address_neqb ctx.(ctx_from) state.(owner)) eqn:Eowner in H; try discriminate;
-    destruct (negb (ctx_amount ctx =? 0)%Z) eqn:Enonzero in H; try discriminate
+    destruct (address_neqb ctx.(ctx_from) state.(owner)) eqn:Eowner in H; try discriminate
   end.
 
 (** ** Functional properties *)
@@ -61,7 +60,7 @@ Section FunctionalProperties.
     smash prev_state ctx = Ok (next_state, acts) ->
     next_state.(piggyState) = Smashed /\
     next_state.(balance) = 0 /\
-    acts = [act_transfer prev_state.(owner) prev_state.(balance)].
+    acts = [act_transfer prev_state.(owner) (prev_state.(balance) + ctx.(ctx_amount))].
   Proof.
     intros Hsmash.
     smash_reduce.
@@ -77,14 +76,14 @@ Section FunctionalProperties.
     match msg with
       | Some Insert => acts = [] /\ Z.add ctx.(ctx_amount) prev_state.(balance) = next_state.(balance)
       | Some Smash => next_state.(piggyState) = Smashed /\ next_state.(balance) = 0
-                      /\ acts = [act_transfer prev_state.(owner) prev_state.(balance)]
+                      /\ acts = [act_transfer prev_state.(owner) (prev_state.(balance) + ctx.(ctx_amount))]
       | None => False
     end.
   Proof.
     intros Hreceive. unfold PiggyBank.receive in Hreceive.
     destruct msg; try discriminate.
     destruct m;
-    [apply insert_inserts_correct | apply smash_transfers_correctly with ctx];
+    [apply insert_inserts_correct | apply smash_transfers_correctly];
     apply Hreceive.
   Qed.
 End FunctionalProperties.
@@ -178,6 +177,7 @@ Section SafetyProperties.
     rewrite state_smashed. cbn.
     - destruct_match; eauto.
       destruct_match; eauto.
+      destruct_match; eauto.
     - eauto.
   Qed.
 
@@ -193,7 +193,7 @@ Section SafetyProperties.
     intros state_intact Hreceive.
     unfold PiggyBank.receive in Hreceive.
     destruct prev_state; cbn in *; rewrite state_intact in Hreceive.
-    destruct (ctx_amount ctx <=? 0) eqn:E; try discriminate.
+    destruct (ctx_amount ctx <? 0) eqn:E; try discriminate.
     inversion Hreceive; cbn; lia.
   Qed.
 
@@ -214,7 +214,7 @@ Section SafetyProperties.
 
   (** Balance in PiggyBank is correct on the blockchain *)
   Lemma balance_on_chain' :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+    forall (bstate : ChainState) caddr,
     let effective_balance := (env_account_balances bstate caddr - sumZ (fun act => act_body_amount act) (outgoing_acts bstate caddr))%Z in
     reachable bstate ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
@@ -229,40 +229,40 @@ Section SafetyProperties.
     - lia.
     - unfold PiggyBank.receive in receive_some.
       destruct msg; try discriminate. destruct m;
-      [insert_reduce | smash_reduce; apply neq_false_eq in Enonzero];
+      [insert_reduce | smash_reduce];
       inversion receive_some; cbn; lia.
     - unfold PiggyBank.receive in receive_some.
       destruct msg; try discriminate. destruct m;
-      [insert_reduce | smash_reduce; apply neq_false_eq in Enonzero];
+      [insert_reduce | smash_reduce];
       inversion receive_some; destruct head; cbn in *; lia.
     - now erewrite sumZ_permutation in IH by eauto.
     - solve_facts.
   Qed.
 
   Lemma balance_on_chain :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+    forall bstate caddr,
     reachable bstate ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
     outgoing_acts bstate caddr = [] ->
     exists cstate,
       contract_state bstate caddr = Some cstate /\
       env_account_balances bstate caddr = cstate.(balance).
   Proof.
-    intros * trace reach deployed.
+    intros * reach deployed.
     edestruct balance_on_chain' as (cstate & balance); eauto.
     intros Hact. rewrite Hact in balance. cbn in *.
     now exists cstate.
   Qed.
 
   Lemma no_outgoing_actions_when_intact :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+    forall bstate caddr,
     reachable bstate ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
     exists cstate,
       contract_state bstate caddr = Some cstate /\
       (cstate.(piggyState) = Intact -> outgoing_acts bstate caddr = []).
   Proof.
-    intros * trace reach deployed.
+    intros * reach deployed.
     contract_induction; intros; auto.
     - now specialize (IH H).
     - cbn in *. unfold PiggyBank.receive in receive_some.
@@ -294,7 +294,7 @@ Section SafetyProperties.
 
   (** When the PiggyBank is smashed its balance needs to remain zero *)
   Lemma balance_is_zero_when_smashed' :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+    forall (bstate : ChainState) caddr,
     let effective_balance := (env_account_balances bstate caddr - sumZ (fun act => act_body_amount act) (outgoing_acts bstate caddr))%Z in
     reachable bstate ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
@@ -320,7 +320,6 @@ Section SafetyProperties.
         /\ ctx_from ctx <> ctx_contract_address ctx).
         destruct facts as [Hamount [Hqueue _]].
         unfold is_smashed in Esmash. destruct prev_state.(piggyState) eqn:Estate; try discriminate.
-        apply neq_false_eq in Enonzero. rewrite Enonzero in Hamount.
         rewrite Hqueue, <- Hamount; try reflexivity. cbn. lia.
     - now destruct facts.
     - now erewrite sumZ_permutation in IH by eauto.
@@ -379,7 +378,7 @@ Section SafetyProperties.
   Qed.
 
   Lemma balance_is_zero_when_smashed :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+    forall (bstate : ChainState) caddr,
     reachable bstate ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
     outgoing_acts bstate caddr = [] ->
@@ -388,29 +387,142 @@ Section SafetyProperties.
       (cstate.(piggyState) = Smashed ->
       (env_account_balances bstate caddr = 0)%Z).
   Proof.
-    intros * trace reach deployed act.
+    intros * reach deployed act.
     edestruct balance_is_zero_when_smashed' as (cstate & deploy & balance); eauto.
     rewrite act, Z.sub_0_r in balance.
     exists cstate.
     split; eauto.
   Qed.
 
-  Lemma smash_poss :
-    forall bstate caddr (trace : ChainTrace empty_state bstate),
+  Lemma balance_on_pos :
+    forall bstate caddr,
     reachable bstate ->
-    emptyable (chain_state_queue bstate) ->
     env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) ->
+    outgoing_acts bstate caddr = [] ->
     exists cstate,
-      contract_state bstate caddr = Some cstate ->
+      contract_state bstate caddr = Some cstate /\
+      0 <= cstate.(balance).
+  Proof.
+    intros * reach deployed Hact.
+    edestruct balance_on_chain as (cstate & balance); eauto.
+    exists cstate.
+    destruct balance as [H <-].
+    split; auto.
+    apply Z.ge_le.
+    now apply account_balance_nonnegative.
+  Qed.
+
+  Definition serializeState state := (@serialize State _) state.
+
+  Lemma smash_poss : forall bstate (reward : Amount) (caddr creator : Address),
+    address_is_contract creator = false ->
+    (reward >= 0)%Z ->
+    reachable bstate ->
+    emptyable (chain_state_queue bstate) ->
+    (exists cstate,
+      env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) /\
+      env_contract_states bstate caddr = Some (serializeState cstate)) ->
         exists bstate',
           reachable_through bstate bstate' /\
-          env_contracts bstate caddr = Some (PiggyBank.contract : WeakContract) /\
           emptyable (chain_state_queue bstate') /\
           exists cstate',
-            contract_state bstate' caddr = Some cstate' /\
+            env_contracts bstate' caddr = Some (PiggyBank.contract : WeakContract) /\
+            env_contract_states bstate' caddr = Some (serializeState cstate') /\
             (env_account_balances bstate' caddr = 0)%Z.
   Proof.
-    (* TODO *)
+    intros * Hcreator Hreward bstate_reachable bstate_queue H.
+    empty_queue H; destruct H as (cstate & contract_deployed & contract_state);
+      (* Prove that H is preserved after transfers, discarding invalid actions, calling other contracts and deploying contracts *)
+      only 3: destruct (address_eqdec caddr to_addr);
+      try (now eexists; rewrite_environment_equiv; repeat split; eauto;
+          cbn; destruct_address_eq; try easy).
+    - (* Prove that H is preserved after calls to the contract *)
+      subst.
+      rewrite contract_deployed in deployed.
+      inversion deployed. subst.
+      rewrite contract_state in deployed_state.
+      inversion deployed_state. subst.
+      clear deployed_state deployed.
+      apply wc_receive_strong in receive_some as
+        (prev_state' & msg' & new_state' & serialize_prev_state & _ & serialize_new_state & receive_some).
+      setoid_rewrite deserialize_serialize in serialize_prev_state.
+      inversion serialize_prev_state. subst.
+      exists new_state'.
+      rewrite_environment_equiv; cbn; repeat split; eauto;
+      cbn; destruct_address_eq; try easy.
+    - update_all.
+      (* Check if piggybank is already smashed *)
+      destruct (is_smashed cstate) eqn:smashed.
+      + (* Case: smashed *)
+        (* In this case the balance should already be zero *)
+        edestruct balance_is_zero_when_smashed as (cstate' & deploy & balance); eauto.
+        * unfold outgoing_acts.
+          now rewrite queue.
+        * cbn in deploy.
+          rewrite contract_state in deploy.
+          unfold serializeState in deploy.
+          rewrite deserialize_serialize in deploy.
+          inversion deploy. subst. clear deploy.
+          unfold is_smashed in smashed.
+          destruct_match in smashed; try discriminate.
+          exists bstate0.
+          split; auto.
+          split; try now rewrite queue.
+          exists cstate'.
+          split; auto.
+      + (* Case: intact *)
+        (* In this case we can smash the piggybank *)
+        add_block [(build_act (owner cstate) (owner cstate) (act_call caddr 0 ((@serialize Msg _) Smash)))] 1%nat; eauto.
+        admit.
+        apply list.Forall_singleton, address_eq_refl.
+        update_all.
+        evaluate_action contract; try easy.
+        * (* Prove that there is enough balance to evaluate action *)
+          now apply account_balance_nonnegative.
+        * (* Prove that receive action returns Some *)
+          cbn; unfold address_neqb.
+          rewrite address_eq_refl; cbn.
+          rewrite smashed; cbn.
+          eauto.
+        * cbn in *.
+          clear contract_state smashed.
+          update_all.
+          edestruct balance_on_chain' as (cstate' & deploy & balance); eauto.
+          cbn in deploy.
+          rewrite deployed_state in deploy.
+          unfold serializeState in deploy.
+          rewrite deserialize_serialize in deploy.
+          inversion deploy. subst. clear deploy.
+          cbn in balance.
+          unfold outgoing_acts in balance.
+          rewrite queue in balance.
+          cbn in balance.
+          rewrite address_eq_refl in balance.
+          cbn in balance.
+          specialize account_balance_nonnegative as H.
+          apply H with (addr := caddr) in reach as balance_pos; clear H.
+          rewrite !Z.add_0_r in balance.
+          apply Zminus_eq in balance.
+
+          (* Finally we need to evaluate the new transfer action that finalize produced *)
+          evaluate_transfer; try easy.
+          -- lia.
+          -- lia.
+          -- admit.
+          -- update (env_account_balances bstate caddr = 0) in balance.
+              { rewrite_environment_equiv. cbn. rewrite address_eq_refl.
+                destruct_address_eq.
+                admit.
+                lia.
+              }
+              clear balance_pos.
+              update_all. 
+              exists bstate.
+              split; auto.
+              split; try now rewrite queue0.
+              eexists.
+              split; auto.
+              split; eauto.
   Admitted.
 
 End SafetyProperties.