Piggy bank example (AU-COBRA#227)

Signed-off-by: laurahejn <[email protected]>
Co-authored-by: 4ever2 <[email protected]>

.gitignore

@@ -1,5 +1,6 @@
 .hidden
 *.tmp
+.DS_Store
 
 # dpd-graph outputs
 *.dpd

examples/_CoqProject

@@ -147,6 +147,3 @@ piggybank/PiggyBankCorrect.v
 piggybank/PiggyBankExtractLIGO.v
 piggybank/PiggyBankExtractLiquidity.v
 piggybank/PiggyBankExtractRust.v
-piggybank/PiggyBankPrinters.v
-piggybank/PiggyBankGens.v
-piggybank/PiggyBankTests.v

examples/fa2/FA2Gens.v

@@ -44,7 +44,7 @@ Module FA2Gens (Info : FA2TestsInfo).
     Definition gTransferCallerFromTo (state : FA2Token.State)
                                      (ledger : TokenLedger)
                                      (tokenid : token_id)
-                                     : GOpt (Address * Address * Address) := 
+                                     : GOpt (Address * Address * Address) :=
       let gAccountWithTokens := liftOpt fst (sampleFMapOpt_filter ledger.(balances) (fun p => 0 <? (snd p))) in
       let policy := state.(permission_policy) in
       let gSelfTransfer :=

examples/piggybank/PiggyBank.v

@@ -10,7 +10,7 @@ From ConCert.Execution Require Import Monad.
 From ConCert.Execution Require Import ResultMonad.
 From ConCert.Execution Require Import Serializable.
 From Coq Require Import List. Import ListNotations.
-From Coq Require Import ZArith.
+From Coq Require Import ZArith_base.
 
 
 
@@ -63,6 +63,7 @@ Section PiggyBankErrors.
   Definition error_not_owner : Error := 2.
   Definition error_already_smashed : Error := 3.
   Definition error_amount_not_positive : Error := 4.
+  Definition error_amount_not_zero : Error := 5.
 End PiggyBankErrors.
 
 (** * Implementation *)
@@ -87,8 +88,9 @@ Section PiggyBankImpl.
     let owner := state.(owner) in
     do _ <- throwIf (is_smashed state) error_already_smashed;
     do _ <- throwIf (address_neqb ctx.(ctx_from) owner) error_not_owner;
-    let state := state<| balance := 0 |> in
+    do _ <- throwIf (negb (ctx.(ctx_amount) =? 0)) error_amount_not_zero;
     let acts := [act_transfer owner state.(balance)] in
+    let state := state<| balance := 0 |><| piggyState := Smashed |> in
     Ok (state, acts).
 
   Definition receive (chain : Chain)
@@ -107,11 +109,12 @@ Section PiggyBankImpl.
                   (_ : Setup)
                   : result State Error :=
     Ok {|
-      balance := 0;
+      balance := ctx.(ctx_amount);
       owner := ctx.(ctx_from);
       piggyState := Intact
     |}.
 
   Definition contract : Contract Setup Msg State Error :=
     build_contract init receive.
+
 End PiggyBankImpl.