Calculus Token with Proof

中文版

This repository contains the formal correctness proofs of the Ethereum Token contract calculus. All are composed in the interactive proof assistant Coq.

Contract information

• Token name: Calculus Token
• Token symbol: CAL
• Contract address: 0xf67a0910a341800b7446554102344c43883d9c78
• Project website: Calculus

What are proved?

The contract is proved to have following properties, which formally define the correctness of this contract.

1. Property_totalSupply_equal_to_sum_balances the total supply always equals the sum of all balances.

2. Property_totalSupply_fixed_transfer the total supply is never changed by transfer().

3. Property_totalSupply_fixed_after_initialization the total supply is never changed after the contract deployment.

4. Property_totalSupply_fixed_delegate_transfer the total supply is never changed by transferFrom().

5. Property_from_to_balances_change transfer() always transfers the specified amount tokens from the caller account to the specified receiver's account.

6. Property_pause_only_by_owner only the token owner can pause the contract.

7. Property_unpause_only_by_owner only the token owner can unpause the contract.

8. Property_restricted_owner_for_transfer the token owner cannot transfer tokens in arbitrary accounts by transfer().

9. Property_restricted_owner_for_transferFrom the token owner cannot transfer tokens in arbitrary accounts by transferFrom().

Proof structure

The proof is composed of following components. A comprehensive introduction of the proving process and structure can be found at tokenlibs-with-proofs: Proving Process

• Model.v defines the contract model, which abstracts the storage, the events, the message calls, and the external environment of this contract.

• Spec.v defines the contract specification, which formally describes the expected behavior of each public function of this contract.

• DSL.v expresses the Solidity implementation of this contract in Coq and proves the implementation of each public function does implement the specification in Spec.v.

• Prop.v formally defines high-level correctness and security properties of this contract and proves the contract specification does guarantee the correctness.

Quick check the proof

The proof is accomplished in the interactive proof assistant Coq 8.7.0, which can generate explicit proof objects. The proof objects can be checked by a small proof checker provided by Coq in a way independently of the proving process. The proof checker can be installed along with Coq by following the official instructions.

After Coq is installed, the proof checked can be called by the following command.

cd proof; make

Why the formal proof?

The formal proof has the following benefits over the existing test and security audit.

• By defining in the unambiguous mathematical language, the formal proof can precisely define the scope of correctness and security.

• By strict mathematical proving, the formal proof can fully cover every case and code path of the smart contract w.r.t. the given definitions of formal specification and high-level properties.