Contents:

Library ConCert.Examples.BAT.BATFixed

Basic Attention Token contract

This implementation of the Basic Attention Token is a based on https://github.com/brave-intl/basic-attention-token-crowdsale/blob/66c886cc4bfb0493d9e7980f392ca7921ef1e7fc/contracts/BAToken.sol The implementation includes some minor changes that fixes bugs present in the original Solidity implementation.

This file contains contract function definitions. All contract types and utility functions are defined in ConCert.Examples.BAT.BATCommon. Proofs for this contract can be found in ConCert.Examples.BAT.BATFixedCorrect.

The BAT contract is a combination of a EIP20 token contract and a crowdsale contract. This implementation extends the EIP20 contract implemented in ConCert.Examples.EIP20.EIP20Token.

From Coq Require Import List. Import ListNotations.
From Coq Require Import ZArith_base.
From ConCert.Utils Require Import Extras.
From ConCert.Utils Require Import RecordUpdate.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Examples.BAT Require Import BATCommon.
From ConCert.Examples.EIP20 Require EIP20Token.

Contract functions

Section BATFixed.
Context {BaseTypes : ChainBase}.

Open Scope N_scope.

Init

This function only gets called once when contract is deployed. Will set up the initial storage state of the contract.

  Definition init (chain : Chain)
                  (ctx : ContractCallContext)
                  (setup : Setup)
                  : result State Error :=

BAToken should not be deployable if one of the following conditions does not hold on setup

funding period is non-empty
funding period does not start before the slot where the contract is deployed
minimum tokens to fund should not be less than the maximum tokens allowed
the initial supply of tokens should be less than the maximum tokens allowed
token exchange rate must be larger than 0
it must be possible to get over minimum token bound without going over maximum

For the last condition we check that tokenExchangeRate <= tokenCreationCap - tokenCreationMin, however this does exclude a few possible configurations where the contract still works as intended. However, these are not likely to come up in real use cases.

    do _ <- throwIf ((setup.(_fundingEnd) <=? setup.(_fundingStart))%nat
            || (setup.(_fundingStart) <? chain.(current_slot))%nat
            || (setup.(_tokenCreationCap) <? setup.(_tokenCreationMin))
            || (setup.(_tokenCreationCap) <? setup.(_batFund))
            || (setup.(_tokenExchangeRate) =? 0)
            || ((setup.(_tokenCreationCap) - setup.(_tokenCreationMin)) <? setup.(_tokenExchangeRate))
            || address_eqb setup.(_batFundDeposit) ctx.(ctx_contract_address)
            || address_eqb setup.(_fundDeposit) ctx.(ctx_contract_address)) default_error ;
    let token_state := {|
        EIP20Token.balances := FMap.add setup.(_batFundDeposit) setup.(_batFund) FMap.empty;
        EIP20Token.total_supply := setup.(_batFund);
        EIP20Token.allowances := FMap.empty;
      |} in
    Ok {|

EIP20Token initialization:

token_state := token_state;

BAT initialization:

      initSupply := setup.(_batFund);
      isFinalized := false;
      fundDeposit := setup.(_fundDeposit);
      batFundDeposit := setup.(_batFundDeposit);
      fundingStart := setup.(_fundingStart);
      fundingEnd := setup.(_fundingEnd);
      tokenExchangeRate := setup.(_tokenExchangeRate);
      tokenCreationCap := setup.(_tokenCreationCap);
      tokenCreationMin := setup.(_tokenCreationMin);
    |}.

Create Tokens

This entrypoint allows users to fund the crowdsale in return for tokens

  Definition try_create_tokens (sender : Address)
                               (sender_payload : Amount)
                               (current_slot : nat)
                               (state : State)
                               : result State Error :=

Early return if funding is finalized, funding period hasn't started yet, or funding period is over

    do _ <- throwIf (state.(isFinalized)
            || (Nat.ltb current_slot state.(fundingStart))
            || (Nat.ltb state.(fundingEnd) current_slot )
            || (address_eqb sender state.(batFundDeposit))) default_error ;

Here we deviate slightly from the reference implementation. They only check for = 0, but since ConCert's payloads may be negative numbers, we must extend this check to <= 0

do _ <- throwIf (Z.leb sender_payload 0) default_error ;

Note: this conversion from Z to N is safe because by assumption sender_payload > 0

    let tokens := (Z.to_N sender_payload ) * state.(tokenExchangeRate) in
    let checkedSupply := (total_supply state ) + tokens in
    do _ <- throwIf (state.(tokenCreationCap) <? checkedSupply) default_error ;
    let new_token_state : EIP20Token.State := {|
      EIP20Token.total_supply := checkedSupply;
      EIP20Token.balances := FMap.partial_alter (fun balance =>
        Some (with_default 0 balance + tokens)) sender (balances state);
      EIP20Token.allowances := allowances state;
    |} in
    Ok (state <|token_state := new_token_state |>).

Refund

This entrypoint can be called if crowdsale is not successfully funded. Users calling this entrypoint will have their tokens removed and get their money refunded.

  Definition try_refund (sender : Address)
                        (current_slot : nat)
                        (state : State)
                        : result (State * list ActionBody) Error :=

Early return if funding is finalized, or funding period is NOT over, or if total supply exceeds or is equal to the minimum fund tokens.

    do _ <- throwIf (state.(isFinalized)
            || (Nat.leb current_slot state.(fundingEnd))
            || (state.(tokenCreationMin) <=? (total_supply state ))) default_error ;

Don't allow the batFundDeposit account to refund

    do _ <- throwIf (address_eqb sender state.(batFundDeposit)) default_error ;
    do sender_bats <- result_of_option (FMap.find sender (balances state)) default_error ;
    do _ <- throwIf (sender_bats =? 0) default_error ;
    let new_total_supply := (total_supply) state - sender_bats in

Convert tokens back to the currency of the blockchain, to be sent back to the sender address

    let amount_to_send := Z.of_N (sender_bats / state.(tokenExchangeRate)) in
    let new_token_state : EIP20Token.State := {|
      EIP20Token.total_supply := new_total_supply;
      EIP20Token.balances := FMap.add sender 0 (balances state);
      EIP20Token.allowances := allowances state;
    |} in
    let new_state := state <|token_state := new_token_state |> in
    let send_act := act_transfer sender amount_to_send in
      Ok (new_state , [send_act ]).

Finalize

This entrypoint will end the crowdsale and pay out the money to the owner. Can only be called if funding was successful.

  Definition try_finalize (sender : Address)
                          (current_slot : nat)
                          (contract_balance : Amount)
                          (state : State)
                          : result (State * list ActionBody) Error :=

Early return if funding is finalized, or if sender is NOT the fund deposit address, or if the total token supply is less than the minimum required amount, or if it is too early to end funding and the total token supply has not reached the cap. Note: the last requirement makes it possible to end a funding early if the cap has been reached.

    do _ <- throwIf (state.(isFinalized) ||
                    (address_neqb sender state.(fundDeposit)) ||
                    ((total_supply state ) <? state.(tokenCreationMin))) default_error ;
    do _ <- throwIf ((Nat.leb current_slot state.(fundingEnd)) &&
                      negb ((total_supply state ) =? state.(tokenCreationCap)))
                      default_error ;

Send the currency of the contract back to the fund

    let send_act := act_transfer state.(fundDeposit) contract_balance in
    let new_state := state <|isFinalized := true |> in
    Ok (new_state , [send_act ]).

Receive

This is the main entrypoint function. All contract calls will be handled by this function

  Open Scope Z_scope.
  Definition receive_bat (chain : Chain)
                         (ctx : ContractCallContext)
                         (state : State)
                         (maybe_msg : option Msg)
                         : result (State * list ActionBody) Error :=
    let sender := ctx.(ctx_from) in
    let sender_payload := ctx.(ctx_amount) in
    let slot := chain.(current_slot) in
    let contract_balance := ctx.(ctx_contract_balance) in
    match maybe_msg with
    | Some create_tokens =>
        without_actions (try_create_tokens sender sender_payload slot state)
    | Some refund =>
        not_payable ctx (try_refund sender slot state) default_error
    | Some finalize =>
        not_payable ctx (try_finalize sender slot contract_balance state) default_error
    | _ => Err default_error
    end.
  Close Scope Z_scope.

Composes EIP20Token.receive and receive_bat by first executing EIP20Token.receive (if the message is an EIP20 message), and otherwise executes receive_bat

  Definition receive (chain : Chain)
                     (ctx : ContractCallContext)
                     (state : State)
                     (maybe_msg : option Msg)
                     : result (State * list ActionBody) Error :=
    match maybe_msg with
    | Some (tokenMsg msg) =>
        do _ <- throwIf (negb (isFinalized state)) default_error ;
        do res <- EIP20Token.receive chain ctx state.(token_state) (Some msg) ;
        let new_state := state <|token_state := fst res |> in
            Ok (new_state , snd res )
    | _ => receive_bat chain ctx state maybe_msg
    end.

  Definition contract : Contract Setup Msg State Error :=
    build_contract init receive.

End BATFixed.