From 09688ae579d32e821b4c80c1f3edbd6ce6975b94 Mon Sep 17 00:00:00 2001 From: tosofia Date: Sun, 16 Mar 2025 12:17:33 +0100 Subject: [PATCH 1/4] Updated contract deposit_erc20 --- contracts/deposit_erc20/Makefile | 127 +++++++++++++---- contracts/deposit_erc20/README.md | 51 +++++++ contracts/deposit_erc20/certora/Makefile | 85 ------------ .../certora/always-depletable.spec | 18 +++ .../certora/conf/always-depletable.conf | 7 + .../certora/conf/deposit-deposit-revert.conf | 7 + .../certora/conf/no-deposit-twice.conf | 7 + .../certora/conf/wd-contract-bal.conf | 7 + .../certora/conf/wd-leq-init-bal.conf | 7 + .../certora/conf/wd-not-revert.conf | 7 + .../certora/conf/wd-sender-rcv.conf | 7 + .../certora/deposit-deposit-revert.spec | 15 ++ contracts/deposit_erc20/certora/getters.sol | 15 -- .../deposit_erc20/certora/helper/erc20.spec | 20 +++ contracts/deposit_erc20/certora/methods.spec | 7 - .../certora/no-deposit-twice.spec | 18 ++- .../certora/wd-contract-bal.spec | 13 +- .../certora/wd-leq-init-bal.spec | 10 +- .../deposit_erc20/certora/wd-not-revert.spec | 17 +++ .../deposit_erc20/certora/wd-sender-rcv.spec | 17 +++ contracts/deposit_erc20/ground-truth.csv | 7 +- contracts/deposit_erc20/skeleton.json | 8 +- .../DepositERC20_no-deposit-twice_v1.sol | 58 ++++++++ .../DepositERC20_wd-contract-bal_v1.sol | 63 +++++++++ .../DepositERC20_wd-leq-init-bal_v1.sol | 57 ++++++++ contracts/deposit_erc20/solcmc/Makefile | 67 --------- .../deposit_erc20/solcmc/no-deposit-twice.sol | 4 - .../deposit_erc20/solcmc/wd-contract-bal.sol | 9 -- .../deposit_erc20/solcmc/wd-leq-init-bal.sol | 3 - .../versions/DepositERC20_v1.sol | 21 ++- .../versions/DepositERC20_v2.sol | 40 ------ .../deposit_erc20/versions/lib/ERC20v1.sol | 118 ++++++++++++++++ .../deposit_erc20/versions/lib/ERC20v2.sol | 130 ++++++++++++++++++ .../deposit_erc20/versions/lib/IERC20.sol | 78 +++++++++++ 34 files changed, 844 insertions(+), 281 deletions(-) create mode 100644 contracts/deposit_erc20/README.md delete mode 100644 contracts/deposit_erc20/certora/Makefile create mode 100644 contracts/deposit_erc20/certora/always-depletable.spec create mode 100644 contracts/deposit_erc20/certora/conf/always-depletable.conf create mode 100644 contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf create mode 100644 contracts/deposit_erc20/certora/conf/no-deposit-twice.conf create mode 100644 contracts/deposit_erc20/certora/conf/wd-contract-bal.conf create mode 100644 contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf create mode 100644 contracts/deposit_erc20/certora/conf/wd-not-revert.conf create mode 100644 contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf create mode 100644 contracts/deposit_erc20/certora/deposit-deposit-revert.spec delete mode 100644 contracts/deposit_erc20/certora/getters.sol create mode 100644 contracts/deposit_erc20/certora/helper/erc20.spec delete mode 100644 contracts/deposit_erc20/certora/methods.spec create mode 100644 contracts/deposit_erc20/certora/wd-not-revert.spec create mode 100644 contracts/deposit_erc20/certora/wd-sender-rcv.spec create mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol create mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol create mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol delete mode 100644 contracts/deposit_erc20/solcmc/Makefile delete mode 100644 contracts/deposit_erc20/solcmc/no-deposit-twice.sol delete mode 100644 contracts/deposit_erc20/solcmc/wd-contract-bal.sol delete mode 100644 contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol delete mode 100644 contracts/deposit_erc20/versions/DepositERC20_v2.sol create mode 100644 contracts/deposit_erc20/versions/lib/ERC20v1.sol create mode 100644 contracts/deposit_erc20/versions/lib/ERC20v2.sol create mode 100644 contracts/deposit_erc20/versions/lib/IERC20.sol diff --git a/contracts/deposit_erc20/Makefile b/contracts/deposit_erc20/Makefile index 38e75235..3b5d630a 100644 --- a/contracts/deposit_erc20/Makefile +++ b/contracts/deposit_erc20/Makefile @@ -1,26 +1,47 @@ -SOLCMC_DIR = ./solcmc -SOLCMC_BUILD_DIR = $(SOLCMC_DIR)/build -SOLCMC_Z3_TABLE = $(SOLCMC_BUILD_DIR)/z3/table.md -SOLCMC_ELD_TABLE = $(SOLCMC_BUILD_DIR)/eld/table.md +MAKEFLAGS = --no-print-directory -CERTORA_DIR = ./certora -CERTORA_BUILD_DIR = $(CERTORA_DIR)/build -CERTORA_TABLE = $(CERTORA_BUILD_DIR)/table.md +# CHANGE THIS PATHS +# Original contract path +CONTRACT = ./versions/DepositERC20_v1.sol +# Contract with solcmc instrumentation path +SOLCMC_CONTRACT = ./solcmc +# Certora specifications path +CERTORA_SPEC = ./certora -VERSIONS_DIR = ./versions SKELETON = ./skeleton.json GROUND_TRUTH = ./ground-truth.csv -README = README.md +README = ./README.md +BUILD_DIR = ./build -PYTHON = python +# SOLCMC params +to = 10m +Z3_DIR = $(BUILD_DIR)/z3 +Z3_OUT = $(Z3_DIR)/out.csv +Z3_CM = $(Z3_DIR)/cm.csv +Z3_TABLE = $(Z3_DIR)/table.md +Z3_LOGS = $(Z3_DIR)/logs +ELD_DIR = $(BUILD_DIR)/eld +ELD_OUT = $(ELD_DIR)/out.csv +ELD_CM = $(ELD_DIR)/cm.csv +ELD_TABLE = $(ELD_DIR)/table.md +ELD_LOGS = $(ELD_DIR)/logs -.PHONY: all certora solcmc plain clean cleanr clean-solcmc clean-certora +# Certora params +CERTORA_DIR = $(BUILD_DIR)/certora +CERTORA_OUT = $(CERTORA_DIR)/out.csv +CERTORA_CM = $(CERTORA_DIR)/cm.csv +CERTORA_TABLE = $(CERTORA_DIR)/table.md +CERTORA_LOGS = $(CERTORA_DIR)/logs + +PYTHON = python3 + +.PHONY: all certora solcmc plain clean cleanr all: plain solcmc certora @echo "Adding Solcmc table to README..." @echo "### SolCMC" >> $(README) - @cat $(SOLCMC_Z3_TABLE) >> $(README) - @cat $(SOLCMC_ELD_TABLE) >> $(README) + @cat $(Z3_TABLE) >> $(README) + @cat $(ELD_TABLE) >> $(README) @echo "" >> $(README) @echo "Adding Certora table to README..." @cat $(CERTORA_TABLE) >> $(README) @@ -28,34 +49,84 @@ all: plain solcmc certora #---------------------------- CERTORA ----------------------------# certora: $(CERTORA_TABLE) -$(CERTORA_TABLE): - @cd $(realpath $(CERTORA_DIR)) && make +$(CERTORA_TABLE): $(CERTORA_CM) + @echo "Generating Certora results table ($(CERTORA_TABLE))..." + @echo "### Certora" > $(CERTORA_TABLE) + @$(PYTHON) ../../scripts/mdtable_gen.py --input $(CERTORA_CM) >> $(CERTORA_TABLE) + +$(CERTORA_CM): $(GROUND_TRUTH) $(CERTORA_OUT) + @echo "Generating Certora confusion matrix ($(CERTORA_CM))..." + @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(CERTORA_OUT) > $(CERTORA_CM) + +$(CERTORA_OUT): setup + @echo "Running Certora experiments..." + @$(PYTHON) ../../scripts/run_certora.py --contracts $(CONTRACT) --specs $(CERTORA_SPEC) --output $(CERTORA_DIR) #---------------------------- SOLCMC -----------------------------# -solcmc: $(SOLCMC_Z3_TABLE) $(SOLCMC_ELD_TABLE) +solcmc: $(Z3_TABLE) $(ELD_TABLE) + +# Solcmc with Z3 +# Make markdown table +$(Z3_TABLE): $(Z3_CM) + @echo "Generating SolCMC results table ($(Z3_TABLE))..." + echo "#### Z3" > $(Z3_TABLE) + @$(PYTHON) ../../scripts/mdtable_gen.py --input $(Z3_CM) >> $(Z3_TABLE) + +# Build confusion matrix with ground truths +$(Z3_CM): $(GROUND_TRUTH) $(Z3_OUT) + @echo "Generating Solcmc confusion matrix ($(Z3_CM))..." + @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(Z3_OUT) > $(Z3_CM) + +# Run experiments +$(Z3_OUT): setup + @echo "Running SolCMC ($(solver)) experiments..." + @$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(Z3_DIR) --timeout $(to) --solver z3 -$(SOLCMC_Z3_TABLE): - @cd $(realpath $(SOLCMC_DIR)) && make solver=z3 +# Solcmc with eldarica +# Make markdown table +$(ELD_TABLE): $(ELD_CM) + @echo "Generating SolCMC results table ($(ELD_TABLE))..." + echo "#### ELD" > $(ELD_TABLE) + @$(PYTHON) ../../scripts/mdtable_gen.py --input $(ELD_CM) >> $(ELD_TABLE) -$(SOLCMC_ELD_TABLE): - @cd $(realpath $(SOLCMC_DIR)) && make solver=eld +# Build confusion matrix with ground truths +$(ELD_CM): $(GROUND_TRUTH) $(ELD_OUT) + @echo "Generating Solcmc confusion matrix ($(ELD_CM))..." + @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(ELD_OUT) > $(ELD_CM) + +# Run experiments +$(ELD_OUT): setup + @echo "Running SolCMC ($(solver)) experiments..." + @$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(ELD_DIR) --timeout $(to) --solver eld + +#---------------------------- SETUP ------------------------------# +setup: $(Z3_LOGS) $(ELD_LOGS) $(CERTORA_LOGS) + +# Create build logs/ dirs, and build/ dirs with them +$(Z3_LOGS): + @mkdir -p $@ + +$(ELD_LOGS): + @mkdir -p $@ + +$(CERTORA_LOGS): + @mkdir -p $@ #---------------------------- README -----------------------------# plain: cleanr $(README) +# Create plain README, without experiments results $(README): $(VERSIONS_DIR) $(SKELETON) $(GROUND_TRUTH) @echo "Generating plain README..." @$(PYTHON) ../../scripts/readme_gen.py -d . > $(README) @echo "## Experiments" >> $(README) #---------------------------- CLEAN ------------------------------# -clean: cleanr clean-solcmc clean-certora +clean: cleanr + @echo "Removing $(BUILD_DIR)..." + @rm -rf $(BUILD_DIR) +# Remove README.md cleanr: - rm -f $(README) - -clean-solcmc: - cd $(realpath $(SOLCMC_DIR)) && make clean - -clean-certora: - cd $(realpath $(CERTORA_DIR)) && make clean + @echo "Removing README..." + @rm -f $(README) diff --git a/contracts/deposit_erc20/README.md b/contracts/deposit_erc20/README.md new file mode 100644 index 00000000..7325d314 --- /dev/null +++ b/contracts/deposit_erc20/README.md @@ -0,0 +1,51 @@ +# Deposit (ERC20) + +## Specification +This contract implements the same functionality of the [Deposit contract](../deposit_eth), but operates on ERC20 tokens instead of ETH. + +The `constructor` takes the token address as a parameter. + +The `deposit` function allows the sender to deposit an arbitrary number of token units into the contract; it can be called only once. Before calling `deposit`, the depositor must approve that the amount they want to deposit can be spent by the contract: if so, the entire allowance is transferred to the contract. + +The function `withdraw(amount)` can be called by anyone to transfer `amount` token units to the transaction sender. + +## Properties +- **always-depletable**: anyone at any time can fire a transaction to receive the full balance of the contract. +- **deposit-deposit-revert**: if `deposit` is called after `deposit` the second call aborts. +- **no-deposit-twice**: `deposit` can only be called once. +- **wd-contract-bal**: the contract token balance is decreased by `amount` after a successful `withdraw(amount)`. +- **wd-leq-init-bal**: the overall withdrawn amount does not exceed the initial deposit. +- **wd-not-revert**: a transaction `withdraw(amount)` is not reverted whenever the `amount` does not exceed the contract balance. +- **wd-sender-rcv**: after a successful `withdraw(amount)`, the balance of the transaction sender is increased by `amount`. + +## Versions +- **v1**: conformant to specification. + +## Ground truth +| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | +|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| +| **v1** | 1 | 1 | 1 | 1 | 0[^1] | 1 | 1 | + +[^1]: This property should not hold for ERC20 tokens, since one can easily increase the contract balance without the contract being able to notice or prevent it. Since this is also possible with ETH (via coinbase or `selfdestruct` transactions), the behavior is comparable for the purposes of these tests. + +## Experiments +### SolCMC +#### Z3 +| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | +|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| +| **v1** | ND | ND | ERR | FN! | TN! | ND | ND | + + +#### ELD +| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | +|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| +| **v1** | ND | ND | TP! | FN! | TN! | ND | ND | + + + +### Certora +| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | +|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| +| **v1** | TP! | TP! | TP! | TP! | TN | TP! | TP! | + + diff --git a/contracts/deposit_erc20/certora/Makefile b/contracts/deposit_erc20/certora/Makefile deleted file mode 100644 index 60f1b037..00000000 --- a/contracts/deposit_erc20/certora/Makefile +++ /dev/null @@ -1,85 +0,0 @@ -# Params -contract = "" -specs = "" - -# Input Files -VERSIONS_DIR = ../versions/ -PROPERTIES_DIR = . -GROUND_TRUTH = ../ground-truth.csv -SPEC_FILES = $(wildcard $(PROPERTIES_DIR)/*.spec) -GETTER_FILE = getters.sol -METHODS_FILE = methods.spec -VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol) - -# Output Files -BUILD_DIR = build -OUTPUT_DIR = $(BUILD_DIR) -CONTRACTS_DIR = $(OUTPUT_DIR)/contracts -LOGS_DIR = $(OUTPUT_DIR)/logs -SPEC_DIR = $(OUTPUT_DIR)/specs -LIB_DIR = $(CONTRACTS_DIR)/lib -OUT = $(OUTPUT_DIR)/out.csv -CM = $(OUTPUT_DIR)/cm.csv -TABLE = $(OUTPUT_DIR)/table.md - -PYTHON = python - -.PHONY: run one setup contracts specs getters directories clean-specs clean - -#---------------------------- RUN --------------------------------# -run: $(TABLE) - -$(TABLE): $(CM) - @echo "Generating Certora results table ($(TABLE))..." - @echo "### Certora" > $(TABLE) - @$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE) - -$(CM): $(GROUND_TRUTH) $(OUT) - @echo "Generating Certora confusion matrix ($(CM))..." - @$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM) - -$(OUT): setup $(VERSIONS_FILES) $(SPEC_FILES) $(GETTER_FILE) - @echo "Running Certora experiments..." - @$(PYTHON) ../../../scripts/run_certora.py --contracts $(CONTRACTS_DIR) --specs $(SPEC_DIR) --output $(OUTPUT_DIR) - -one: clean-specs contracts specs directories - @$(PYTHON) ../../../scripts/run_certora.py --contracts $(contract) --specs $(specs) - -#---------------------------- SETUP ------------------------------# -setup: contracts specs getters directories - -contracts: $(CONTRACTS_DIR) getters - @$(PYTHON) ../../../scripts/inject_getters.py --contracts $(VERSIONS_DIR) --getters $(GETTER_FILE) --output $(CONTRACTS_DIR) - -specs: $(SPEC_DIR) - @for file in $(SPEC_FILES); do \ - if [ "$$file" != $(PROPERTIES_DIR)/"methods.spec" ]; then \ - echo "Processing $$file"; \ - cat $(METHODS_FILE) $$file >> $(SPEC_DIR)/$$file; \ - fi \ - done; - -getters: - @if ! [ -e $(GETTER_FILE) ]; then touch $(GETTER_FILE); fi; - -directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR) $(SPEC_DIR) - -$(CONTRACTS_DIR): - @mkdir -p $@ - -$(SPEC_DIR): - @mkdir -p $@ - -$(LOGS_DIR): - @mkdir -p $@ - -$(LIB_DIR): - @cp -r ../../../lib/ $@ - -#---------------------------- CLEAN ------------------------------# -clean-specs: - rm -rf $(SPEC_DIR) - -clean: - rm -rf $(BUILD_DIR) - diff --git a/contracts/deposit_erc20/certora/always-depletable.spec b/contracts/deposit_erc20/certora/always-depletable.spec new file mode 100644 index 00000000..1c24c4d7 --- /dev/null +++ b/contracts/deposit_erc20/certora/always-depletable.spec @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: GPL-3.0-only +import "helper/erc20.spec"; + +rule always_depletable { + env e; + + require(e.msg.sender != 0); + require(e.msg.sender != currentContract); + require(e.msg.value == 0); + + uint amount = getAddressBalance(e, currentContract); + require(max_uint >= amount + getAddressBalance(e, e.msg.sender)); + require(currentContract.sent + amount <= max_uint); + withdraw@withrevert(e, amount); + + assert !lastReverted; + assert (getAddressBalance(e, currentContract) == 0); +} diff --git a/contracts/deposit_erc20/certora/conf/always-depletable.conf b/contracts/deposit_erc20/certora/conf/always-depletable.conf new file mode 100644 index 00000000..725f04a4 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/always-depletable.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/always-depletable.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf b/contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf new file mode 100644 index 00000000..6ebefe55 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/deposit-deposit-revert.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/no-deposit-twice.conf b/contracts/deposit_erc20/certora/conf/no-deposit-twice.conf new file mode 100644 index 00000000..caa42b95 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/no-deposit-twice.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/no-deposit-twice.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/wd-contract-bal.conf b/contracts/deposit_erc20/certora/conf/wd-contract-bal.conf new file mode 100644 index 00000000..f980a16b --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/wd-contract-bal.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/wd-contract-bal.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf b/contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf new file mode 100644 index 00000000..5f3ef5a1 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/wd-leq-init-bal.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/wd-not-revert.conf b/contracts/deposit_erc20/certora/conf/wd-not-revert.conf new file mode 100644 index 00000000..302bef33 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/wd-not-revert.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/wd-not-revert.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf b/contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf new file mode 100644 index 00000000..f7fe65e9 --- /dev/null +++ b/contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "versions/lib/ERC20v1.sol:ERC20", + "versions/DepositERC20_v1.sol:TokenTransfer" + ], + "verify": "TokenTransfer:certora/wd-sender-rcv.spec" +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/deposit-deposit-revert.spec b/contracts/deposit_erc20/certora/deposit-deposit-revert.spec new file mode 100644 index 00000000..f7381f85 --- /dev/null +++ b/contracts/deposit_erc20/certora/deposit-deposit-revert.spec @@ -0,0 +1,15 @@ +import "helper/erc20.spec"; + +rule deposit_deposit_revert { + env e1; + env e2; + + method f; + calldataarg args; + + deposit(e1); + f(e2, args); + + assert f.selector != sig:deposit().selector; +} + diff --git a/contracts/deposit_erc20/certora/getters.sol b/contracts/deposit_erc20/certora/getters.sol deleted file mode 100644 index 4dfe9d7a..00000000 --- a/contracts/deposit_erc20/certora/getters.sol +++ /dev/null @@ -1,15 +0,0 @@ -function getBalance() public view returns (uint) { - return token.balanceOf(address(this)); -} - -function getAddressBalance(address addr) public view returns (uint) { - return token.balanceOf(addr); -} - -function getSent() public view returns (uint) { - return sent; -} - -function getInitialDeposit() public view returns (uint) { - return initial_deposit; -} diff --git a/contracts/deposit_erc20/certora/helper/erc20.spec b/contracts/deposit_erc20/certora/helper/erc20.spec new file mode 100644 index 00000000..48ba7180 --- /dev/null +++ b/contracts/deposit_erc20/certora/helper/erc20.spec @@ -0,0 +1,20 @@ +/*** + * This spec file adds `DISPATCHER` summaries for the methods in the ERC20 + * specification. It is useful for writing specifications that work with + * arbitrary ERC20 contracts; if using it, you should add a variety of ERC20 + * implementations to the scene. + * + * See [Using DISPATCHER for ERC20 contracts][guide] in the user guide for more + * information. + * + * [guide]: https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html#using-dispatcher-for-erc20-contracts + */ + +methods { + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/methods.spec b/contracts/deposit_erc20/certora/methods.spec deleted file mode 100644 index 23496455..00000000 --- a/contracts/deposit_erc20/certora/methods.spec +++ /dev/null @@ -1,7 +0,0 @@ -methods { - function withdraw(uint) external; - function getBalance() external returns (uint) envfree; - function getAddressBalance(address) external returns (uint) envfree; - function getInitialDeposit() external returns (uint) envfree; - function getSent() external returns (uint) envfree; -} \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/no-deposit-twice.spec b/contracts/deposit_erc20/certora/no-deposit-twice.spec index 01322b86..9f8a2767 100644 --- a/contracts/deposit_erc20/certora/no-deposit-twice.spec +++ b/contracts/deposit_erc20/certora/no-deposit-twice.spec @@ -1,13 +1,11 @@ -rule no_deposit_twice { - env e1; - env e2; - - method f; - calldataarg args; +persistent ghost bool multiple_deposit { + init_state axiom multiple_deposit == false; +} - deposit(e1); - f(e2, args); - - assert f.selector != sig:deposit().selector; +hook Sstore ever_deposited bool value (bool old_value) { + if(old_value && value) + multiple_deposit = true; } +invariant no_deposit_twice() + !multiple_deposit; \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/wd-contract-bal.spec b/contracts/deposit_erc20/certora/wd-contract-bal.spec index 82234866..a732f61e 100644 --- a/contracts/deposit_erc20/certora/wd-contract-bal.spec +++ b/contracts/deposit_erc20/certora/wd-contract-bal.spec @@ -1,15 +1,20 @@ // SPDX-License-Identifier: GPL-3.0-only +import "./helper/erc20.spec"; rule wd_contract_bal { env e; uint amount; mathint mi_amount = amount; - - mathint before = getBalance(); + mathint before = getBalance(e); require before >= mi_amount; withdraw(e, amount); - mathint after = getBalance(); - assert before == after + mi_amount; + mathint after = getBalance(e); + if(e.msg.sender == currentContract) { + assert before == after; + } + else { + assert before == after + mi_amount; + } } diff --git a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec index 68ca22fc..cd80cc65 100644 --- a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec +++ b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec @@ -1,4 +1,10 @@ -// SPDX-License-Identifier: GPL-3.0-only - +import "helper/erc20.spec"; +methods { + function withdraw(uint) external; + function getBalance() external returns (uint) envfree; + function getAddressBalance(address) external returns (uint) envfree; + function getInitialDeposit() external returns (uint) envfree; + function getSent() external returns (uint) envfree; +} invariant wd_leq_init_bal() getSent() <= getInitialDeposit(); diff --git a/contracts/deposit_erc20/certora/wd-not-revert.spec b/contracts/deposit_erc20/certora/wd-not-revert.spec new file mode 100644 index 00000000..379ef5cc --- /dev/null +++ b/contracts/deposit_erc20/certora/wd-not-revert.spec @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: GPL-3.0-only +import "helper/erc20.spec"; + +rule wd_not_revert { + env e; + uint amount; + + uint before = getAddressBalance(e, currentContract); + require(e.msg.sender != 0); + require(e.msg.value == 0); + require(max_uint >= amount + getAddressBalance(e, e.msg.sender)); + require(currentContract.sent + amount + before <= max_uint); + require(amount <= before); + + withdraw@withrevert(e, amount); + assert !lastReverted; +} diff --git a/contracts/deposit_erc20/certora/wd-sender-rcv.spec b/contracts/deposit_erc20/certora/wd-sender-rcv.spec new file mode 100644 index 00000000..791aede5 --- /dev/null +++ b/contracts/deposit_erc20/certora/wd-sender-rcv.spec @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: GPL-3.0-only +import "helper/erc20.spec"; + +rule wd_sender_rcv { + env e; + uint amount; + address sender = e.msg.sender; + + mathint before = getAddressBalance(e, sender); + withdraw(e, amount); + mathint after = getAddressBalance(e, sender); + + if(e.msg.sender != currentContract) + assert after == before + amount; + else + assert after == before; +} diff --git a/contracts/deposit_erc20/ground-truth.csv b/contracts/deposit_erc20/ground-truth.csv index 0c7e695a..9ba73c97 100644 --- a/contracts/deposit_erc20/ground-truth.csv +++ b/contracts/deposit_erc20/ground-truth.csv @@ -1,7 +1,8 @@ property,version,truth,footnote-md +always-depletable,v1,1, +deposit-deposit-revert,v1,1, no-deposit-twice,v1,1, -no-deposit-twice,v2,1, wd-leq-init-bal,v1,0,"This property should not hold for ERC20 tokens, since one can easily increase the contract balance without the contract being able to notice or prevent it. Since this is also possible with ETH (via coinbase or `selfdestruct` transactions), the behavior is comparable for the purposes of these tests." -wd-leq-init-bal,v2,0, wd-contract-bal,v1,1, -wd-contract-bal,v2,1, \ No newline at end of file +wd-not-revert,v1,1 +wd-sender-rcv,v1,1 \ No newline at end of file diff --git a/contracts/deposit_erc20/skeleton.json b/contracts/deposit_erc20/skeleton.json index 44730c30..9816c696 100644 --- a/contracts/deposit_erc20/skeleton.json +++ b/contracts/deposit_erc20/skeleton.json @@ -2,8 +2,12 @@ "name": "Deposit (ERC20)", "specification": "file:spec.md", "properties": { + "always-depletable": "anyone at any time can fire a transaction to receive the full balance of the contract.", + "deposit-deposit-revert": "if `deposit` is called after `deposit` the second call aborts.", "no-deposit-twice": "`deposit` can only be called once.", "wd-leq-init-bal": "the overall withdrawn amount does not exceed the initial deposit.", - "wd-contract-bal": "the contract token balance is decreased by `amount` after a successful `withdraw(amount)`." - } + "wd-contract-bal": "the contract token balance is decreased by `amount` after a successful `withdraw(amount)`.", + "wd-not-revert": "a transaction `withdraw(amount)` is not reverted whenever the `amount` does not exceed the contract balance.", + "wd-sender-rcv": "after a successful `withdraw(amount)`, the balance of the transaction sender is increased by `amount`." + } } diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol new file mode 100644 index 00000000..6e8b6b40 --- /dev/null +++ b/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol @@ -0,0 +1,58 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity >= 0.8.2; + +import "../versions/lib/ERC20v1.sol"; + +/// @custom:version conformant to specification. +contract TokenTransfer { + ERC20 token; + bool ever_deposited; + + uint private sent; + uint initial_deposit; + + // ghost variables + uint _count_deposit; + + constructor(ERC20 token_) { + token = token_; + } + + function deposit() public { + require(!ever_deposited); + + ever_deposited = true; + uint allowance = token.allowance(msg.sender, address(this)); + token.transferFrom(msg.sender, address(this), allowance); + + initial_deposit = token.totalSupply(); + + _count_deposit += 1; + } + + function withdraw(uint amount) public { + sent += amount; + token.transfer(msg.sender, amount); + } + + function getBalance() public view returns (uint) { + return token.balanceOf(address(this)); + } + + function getAddressBalance(address addr) public view returns (uint) { + return token.balanceOf(addr); + } + + function getSent() public view returns (uint) { + return sent; + } + + function getInitialDeposit() public view returns (uint) { + return initial_deposit; + } + + // p1 + function invariant() public view { + assert(_count_deposit <= 1); + } +} diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol new file mode 100644 index 00000000..bf7185d1 --- /dev/null +++ b/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity >= 0.8.2; + +import "../versions/lib/ERC20v1.sol"; + +/// @custom:version conformant to specification. +contract TokenTransfer { + ERC20 token; + bool ever_deposited; + + uint private sent; + uint initial_deposit; + + // ghost variables + uint _count_deposit; + + constructor(ERC20 token_) { + token = token_; + } + + function deposit() public { + require(!ever_deposited); + + ever_deposited = true; + uint allowance = token.allowance(msg.sender, address(this)); + token.transferFrom(msg.sender, address(this), allowance); + + initial_deposit = token.totalSupply(); + + _count_deposit += 1; + } + + function withdraw(uint amount) public { + sent += amount; + token.transfer(msg.sender, amount); + } + + function getBalance() public view returns (uint) { + return token.balanceOf(address(this)); + } + + function getAddressBalance(address addr) public view returns (uint) { + return token.balanceOf(addr); + } + + function getSent() public view returns (uint) { + return sent; + } + + function getInitialDeposit() public view returns (uint) { + return initial_deposit; + } + + function invariant(uint amount) public { + uint old_balance = token.balanceOf(address(this)); + + withdraw(amount); + + uint new_balance = token.balanceOf(address(this)); + + assert(new_balance == old_balance - amount); + } +} \ No newline at end of file diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol new file mode 100644 index 00000000..2725b6f9 --- /dev/null +++ b/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity >= 0.8.2; + +import "../versions/lib/ERC20v1.sol"; + +/// @custom:version conformant to specification. +contract TokenTransfer { + ERC20 token; + bool ever_deposited; + + uint private sent; + uint initial_deposit; + + // ghost variables + uint _count_deposit; + + constructor(ERC20 token_) { + token = token_; + } + + function deposit() public { + require(!ever_deposited); + + ever_deposited = true; + uint allowance = token.allowance(msg.sender, address(this)); + token.transferFrom(msg.sender, address(this), allowance); + + initial_deposit = token.totalSupply(); + + _count_deposit += 1; + } + + function withdraw(uint amount) public { + sent += amount; + token.transfer(msg.sender, amount); + } + + function getBalance() public view returns (uint) { + return token.balanceOf(address(this)); + } + + function getAddressBalance(address addr) public view returns (uint) { + return token.balanceOf(addr); + } + + function getSent() public view returns (uint) { + return sent; + } + + function getInitialDeposit() public view returns (uint) { + return initial_deposit; + } + + function invariant() public view { + assert(sent <= initial_deposit); + } +} \ No newline at end of file diff --git a/contracts/deposit_erc20/solcmc/Makefile b/contracts/deposit_erc20/solcmc/Makefile deleted file mode 100644 index 1cca6c11..00000000 --- a/contracts/deposit_erc20/solcmc/Makefile +++ /dev/null @@ -1,67 +0,0 @@ -# Params -solver = z3 -to = 10m -contract = "" - -# Input files -VERSIONS_DIR = ../versions/ -PROPERTIES_DIR = . -GROUND_TRUTH = ../ground-truth.csv -PROPERTIES_FILES = $(wildcard $(PROPERTIES_DIR)/*.sol) -VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol) - -# Output files -BUILD_DIR = build -OUTPUT_DIR = $(BUILD_DIR)/$(solver) -CONTRACTS_DIR = $(BUILD_DIR)/contracts -LOGS_DIR = $(OUTPUT_DIR)/logs -LIB_DIR = $(CONTRACTS_DIR)/lib -OUT = $(OUTPUT_DIR)/out.csv -CM = $(OUTPUT_DIR)/cm.csv -TABLE = $(OUTPUT_DIR)/table.md - -PYTHON = python - -.PHONY: run one setup contracts directories clean - -#---------------------------- RUN --------------------------------# -run: $(TABLE) - -$(TABLE): $(CM) - @echo "Generating SolCMC results table ($(TABLE))..." - @if [ $(solver) = "z3" ]; then echo "#### Z3" > $(TABLE); \ - elif [ $(solver) = "eld" ]; then echo "#### Eldarica" > $(TABLE); fi - @$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE) - -$(CM): $(GROUND_TRUTH) $(OUT) - @echo "Generating Solcmc confusion matrix ($(CM))..." - @$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM) - -$(OUT): setup $(PROPERTIES_FILES) $(VERSIONS_FILES) - @echo "Running SolCMC ($(solver)) experiments..." - @$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(CONTRACTS_DIR) --output $(OUTPUT_DIR) --timeout $(to) --solver $(solver) - -one: setup - @$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(contract) --timeout $(to) - -#---------------------------- SETUP ------------------------------# -setup: contracts directories - -contracts: $(VERSIONS_FILES) $(PROPERTIES_FILES) $(CONTRACTS_DIR) - @echo "Building contracts..." - @$(PYTHON) ../../../scripts/builder.py --versions $(VERSIONS_DIR) --properties $(PROPERTIES_DIR) --output $(CONTRACTS_DIR) - -directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR) - -$(CONTRACTS_DIR): - @mkdir -p $@ - -$(LOGS_DIR): - @mkdir -p $@ - -$(LIB_DIR): - @cp -r ../../../lib/ $@ - -#---------------------------- CLEAN ------------------------------# -clean: - rm -rf $(BUILD_DIR) diff --git a/contracts/deposit_erc20/solcmc/no-deposit-twice.sol b/contracts/deposit_erc20/solcmc/no-deposit-twice.sol deleted file mode 100644 index 75b7a90b..00000000 --- a/contracts/deposit_erc20/solcmc/no-deposit-twice.sol +++ /dev/null @@ -1,4 +0,0 @@ - // p1 - function invariant() public view { - assert(_count_deposit <= 1); - } diff --git a/contracts/deposit_erc20/solcmc/wd-contract-bal.sol b/contracts/deposit_erc20/solcmc/wd-contract-bal.sol deleted file mode 100644 index 1a16ee30..00000000 --- a/contracts/deposit_erc20/solcmc/wd-contract-bal.sol +++ /dev/null @@ -1,9 +0,0 @@ -function invariant(uint amount) public { - uint old_balance = token.balanceOf(address(this)); - - withdraw(amount); - - uint new_balance = token.balanceOf(address(this)); - - assert(new_balance == old_balance - amount); -} diff --git a/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol b/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol deleted file mode 100644 index cb84a4ec..00000000 --- a/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol +++ /dev/null @@ -1,3 +0,0 @@ -function invariant() public view { - assert(sent <= initial_deposit); -} diff --git a/contracts/deposit_erc20/versions/DepositERC20_v1.sol b/contracts/deposit_erc20/versions/DepositERC20_v1.sol index e748c98d..80682d5f 100644 --- a/contracts/deposit_erc20/versions/DepositERC20_v1.sol +++ b/contracts/deposit_erc20/versions/DepositERC20_v1.sol @@ -27,11 +27,28 @@ contract TokenTransfer { initial_deposit = token.totalSupply(); - _count_deposit += 1; + _count_deposit += 1; } function withdraw(uint amount) public { sent += amount; token.transfer(msg.sender, amount); } -} + + function getBalance() public view returns (uint) { + return token.balanceOf(address(this)); + } + + function getAddressBalance(address addr) public view returns (uint) { + return token.balanceOf(addr); + } + + function getSent() public view returns (uint) { + return sent; + } + + function getInitialDeposit() public view returns (uint) { + return initial_deposit; + } + +} \ No newline at end of file diff --git a/contracts/deposit_erc20/versions/DepositERC20_v2.sol b/contracts/deposit_erc20/versions/DepositERC20_v2.sol deleted file mode 100644 index f3cb563a..00000000 --- a/contracts/deposit_erc20/versions/DepositERC20_v2.sol +++ /dev/null @@ -1,40 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity >= 0.8.2; - -import "./lib/IERC20.sol"; -import "./lib/SafeERC20.sol"; - -/// @custom:version safe IERC20 interactions by using [SafeERC20.sol](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/v4.8.3/contracts/token/ERC20/utils/SafeERC20.sol) (OpenZeppelin) -contract TokenTransfer { - using SafeERC20 for IERC20; - - IERC20 token; - bool ever_deposited; - - uint private sent; - uint initial_deposit; - - // ghost variables - uint _count_deposit; - - constructor(IERC20 token_) { - token = token_; - } - - function deposit() public { - require(!ever_deposited); - - ever_deposited = true; - uint allowance = token.allowance(msg.sender, address(this)); - token.safeTransferFrom(msg.sender, address(this), allowance); - - initial_deposit = token.totalSupply(); - - _count_deposit += 1; - } - - function withdraw(uint amount) public { - sent += amount; - token.safeTransfer(msg.sender, amount); - } -} diff --git a/contracts/deposit_erc20/versions/lib/ERC20v1.sol b/contracts/deposit_erc20/versions/lib/ERC20v1.sol new file mode 100644 index 00000000..db15e7a2 --- /dev/null +++ b/contracts/deposit_erc20/versions/lib/ERC20v1.sol @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: MIT +pragma solidity >= 0.8.2; + +import "./IERC20.sol"; + +/** + * @dev Implementation of the {IERC20} interface. + * + */ +contract ERC20 is IERC20 { + mapping(address => uint256) private _balances; + uint256 private _totalSupply; + + constructor(uint256 amount) { + _totalSupply += amount; + _balances[msg.sender] += amount; + } + + function totalSupply() public view returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view returns (uint256) { + return _balances[account]; + } + + /** + * Requirements: + * - `to` cannot be the zero address. + * - the caller must have a balance of at least `amount`. + */ + function transfer(address to, uint256 amount) public returns (bool) { + _transfer(msg.sender, to, amount); + return true; + } + + function allowance(address owner, address spender) public view returns (uint256) { + require (owner != address(0)); + require (spender != address(0)); + return _balances[owner]; + } + + /** + * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on + * `transferFrom`. This is semantically equivalent to an infinite approval. + * + * Requirements: + * - `spender` cannot be the zero address. + */ + function approve(address spender, uint256 amount) public view returns (bool) { + _approve(msg.sender, spender, amount); + return true; + } + + /** + * @dev See {IERC20-transferFrom}. + * + * + * NOTE: Does not update the allowance if the current allowance + * is the maximum `uint256`. + * + * Requirements: + * + * - `from` and `to` cannot be the zero address. + * - `from` must have a balance of at least `amount`. + * - the caller must have allowance for ``from``'s tokens of at least + * `amount`. + */ + function transferFrom(address from, address to, uint256 amount) public returns (bool) { + _spendAllowance(from, msg.sender, amount); + _transfer(from, to, amount); + return true; + } + + function _transfer(address from, address to, uint256 amount) internal { + require (from != address(0)); + require (to != address(0)); + + uint256 fromBalance = _balances[from]; + require (fromBalance >= amount); + // unchecked { + // Overflow not possible: amount <= fromBalance <= totalSupply. + _balances[from] = fromBalance - amount; + // Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256. + _balances[to] += amount; + // } + } + + /** + * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens. + * + * This internal function is equivalent to `approve`, and can be used to + * e.g. set automatic allowances for certain subsystems, etc. + * + * Requirements: + * + * - `owner` cannot be the zero address. + * - `spender` cannot be the zero address. + */ + function _approve(address owner, address spender, uint256 amount) internal pure { + require (owner != address(0)); + require (spender != address(0)); + require (amount >= 0); + } + + /** + * @dev Updates `owner` s allowance for `spender` based on spent `amount`. + * + * Does not update the allowance amount in case of infinite allowance. + * Revert if not enough allowance is available. + * + */ + function _spendAllowance(address owner, address spender, uint256 amount) internal view { + uint256 currentAllowance = allowance(owner, spender); + require (currentAllowance >= amount); + _approve(owner, spender, currentAllowance); + } +} diff --git a/contracts/deposit_erc20/versions/lib/ERC20v2.sol b/contracts/deposit_erc20/versions/lib/ERC20v2.sol new file mode 100644 index 00000000..a8a5c839 --- /dev/null +++ b/contracts/deposit_erc20/versions/lib/ERC20v2.sol @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: MIT +pragma solidity >= 0.8.2; + +import "./IERC20.sol"; + +/** + * @dev Implementation of the {IERC20} interface with bugged transfer. + * + */ +contract ERC20v2 is IERC20 { + mapping(address => uint256) private _balances; + mapping(address => mapping(address => bool)) private _allowances; + uint256 private _totalSupply; + + constructor(uint256 amount) { + _totalSupply += amount; + _balances[msg.sender] += amount; + } + + function totalSupply() public view returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view returns (uint256) { + return _balances[account]; + } + + /** + * Requirements: + * - `to` cannot be the zero address. + * - the caller must have a balance of at least `amount`. + */ + function transfer(address to, uint256 amount) public returns (bool) { + _transfer(msg.sender, to, amount); + return true; + } + + function allowance(address owner, address spender) public view returns (uint256) { + if (_allowances[owner][spender]) { + return type(uint256).max; + } + else { + return 0; + } + } + + /** + * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on + * `transferFrom`. This is semantically equivalent to an infinite approval. + * + * Requirements: + * - `spender` cannot be the zero address. + */ + function approve(address spender, uint256 amount) public returns (bool) { + _approve(msg.sender, spender, amount); + return true; + } + + /** + * @dev See {IERC20-transferFrom}. + * + * + * NOTE: Does not update the allowance if the current allowance + * is the maximum `uint256`. + * + * Requirements: + * + * - `from` and `to` cannot be the zero address. + * - `from` must have a balance of at least `amount`. + * - the caller must have allowance for ``from``'s tokens of at least + * `amount`. + */ + function transferFrom(address from, address to, uint256 amount) public returns (bool) { + _spendAllowance(from, msg.sender, amount); + _transfer(from, to, amount); + return true; + } + + function _transfer(address from, address to, uint256 amount) internal { + require (from != address(0)); + require (to != address(0)); + + uint256 fromBalance = _balances[from]; + require (fromBalance >= amount); + // unchecked { + // Overflow not possible: amount <= fromBalance <= totalSupply. + _balances[from] = fromBalance - amount; + // Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256. + _balances[to] += amount - 1; + // } + } + + /** + * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens. + * + * This internal function is equivalent to `approve`, and can be used to + * e.g. set automatic allowances for certain subsystems, etc. + * + * Requirements: + * + * - `owner` cannot be the zero address. + * - `spender` cannot be the zero address. + */ + function _approve(address owner, address spender, uint256 amount) internal { + require (owner != address(0)); + require (spender != address(0)); + require (amount == type(uint256).max); + if (amount > 0) { + _allowances[owner][spender] = true; + } + else { + _allowances[owner][spender] = false; + } + } + + /** + * @dev Updates `owner` s allowance for `spender` based on spent `amount`. + * + * Does not update the allowance amount in case of infinite allowance. + * Revert if not enough allowance is available. + * + */ + function _spendAllowance(address owner, address spender, uint256 amount) internal { + uint256 currentAllowance = allowance(owner, spender); + require (currentAllowance >= amount); + // unchecked { + _approve(owner, spender, currentAllowance - amount); + // } + } +} diff --git a/contracts/deposit_erc20/versions/lib/IERC20.sol b/contracts/deposit_erc20/versions/lib/IERC20.sol new file mode 100644 index 00000000..66c4e4d8 --- /dev/null +++ b/contracts/deposit_erc20/versions/lib/IERC20.sol @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.0; + +/** + * @dev Interface of the ERC20 standard as defined in the EIP. + */ +interface IERC20 { + /** + * @dev Emitted when `value` tokens are moved from one account (`from`) to + * another (`to`). + * + * Note that `value` may be zero. + */ + event Transfer(address indexed from, address indexed to, uint256 value); + + /** + * @dev Emitted when the allowance of a `spender` for an `owner` is set by + * a call to {approve}. `value` is the new allowance. + */ + event Approval(address indexed owner, address indexed spender, uint256 value); + + /** + * @dev Returns the amount of tokens in existence. + */ + function totalSupply() external view returns (uint256); + + /** + * @dev Returns the amount of tokens owned by `account`. + */ + function balanceOf(address account) external view returns (uint256); + + /** + * @dev Moves `amount` tokens from the caller's account to `to`. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transfer(address to, uint256 amount) external returns (bool); + + /** + * @dev Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) external view returns (uint256); + + /** + * @dev Sets `amount` as the allowance of `spender` over the caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + function approve(address spender, uint256 amount) external returns (bool); + + /** + * @dev Moves `amount` tokens from `from` to `to` using the + * allowance mechanism. `amount` is then deducted from the caller's + * allowance. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transferFrom(address from, address to, uint256 amount) external returns (bool); +} From f655aed23b6c7f40e0dcde61f7f69484404b2a66 Mon Sep 17 00:00:00 2001 From: TistaMilani Date: Wed, 26 Mar 2025 09:34:18 +0000 Subject: [PATCH 2/4] Renamed conf file according to the new script convention --- ...ays-depletable.conf => DepositERC20_always-depletable_v1.conf} | 0 ...it-revert.conf => DepositERC20_deposit-deposit-revert_v1.conf} | 0 ...o-deposit-twice.conf => DepositERC20_no-deposit-twice_v1.conf} | 0 ...{wd-contract-bal.conf => DepositERC20_wd-contract-bal_v1.conf} | 0 ...{wd-leq-init-bal.conf => DepositERC20_wd-leq-init-bal_v1.conf} | 0 .../{wd-not-revert.conf => DepositERC20_wd-not-revert_v1.conf} | 0 .../{wd-sender-rcv.conf => DepositERC20_wd-sender-rcv_v1.conf} | 0 7 files changed, 0 insertions(+), 0 deletions(-) rename contracts/deposit_erc20/certora/conf/{always-depletable.conf => DepositERC20_always-depletable_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{deposit-deposit-revert.conf => DepositERC20_deposit-deposit-revert_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{no-deposit-twice.conf => DepositERC20_no-deposit-twice_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{wd-contract-bal.conf => DepositERC20_wd-contract-bal_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{wd-leq-init-bal.conf => DepositERC20_wd-leq-init-bal_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{wd-not-revert.conf => DepositERC20_wd-not-revert_v1.conf} (100%) rename contracts/deposit_erc20/certora/conf/{wd-sender-rcv.conf => DepositERC20_wd-sender-rcv_v1.conf} (100%) diff --git a/contracts/deposit_erc20/certora/conf/always-depletable.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/always-depletable.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/deposit-deposit-revert.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/no-deposit-twice.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/no-deposit-twice.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/wd-contract-bal.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/wd-contract-bal.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/wd-leq-init-bal.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/wd-not-revert.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/wd-not-revert.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf diff --git a/contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf similarity index 100% rename from contracts/deposit_erc20/certora/conf/wd-sender-rcv.conf rename to contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf From 1bc246aeecc158aae46e87be1c551405e9d65c24 Mon Sep 17 00:00:00 2001 From: TistaMilani Date: Thu, 15 May 2025 14:52:07 +0200 Subject: [PATCH 3/4] Add hardhat PoC for wd-leq-init-bal property. --- .../deposit_erc20/hardhat/DepositERC20.sol | 54 ++++++++ contracts/deposit_erc20/hardhat/ERC20v1.sol | 118 ++++++++++++++++++ contracts/deposit_erc20/hardhat/IERC20.sol | 78 ++++++++++++ contracts/deposit_erc20/hardhat/test.js | 29 +++++ 4 files changed, 279 insertions(+) create mode 100644 contracts/deposit_erc20/hardhat/DepositERC20.sol create mode 100644 contracts/deposit_erc20/hardhat/ERC20v1.sol create mode 100644 contracts/deposit_erc20/hardhat/IERC20.sol create mode 100644 contracts/deposit_erc20/hardhat/test.js diff --git a/contracts/deposit_erc20/hardhat/DepositERC20.sol b/contracts/deposit_erc20/hardhat/DepositERC20.sol new file mode 100644 index 00000000..2a5865be --- /dev/null +++ b/contracts/deposit_erc20/hardhat/DepositERC20.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity >= 0.8.2; + +import "./ERC20v1.sol"; + +/// @custom:version conformant to specification. +contract TokenTransfer { + ERC20 token; + bool ever_deposited; + + uint private sent; + uint initial_deposit; + + // ghost variables + uint _count_deposit; + + constructor(ERC20 token_) { + token = token_; + } + + function deposit() public { + require(!ever_deposited); + + ever_deposited = true; + uint allowance = token.allowance(msg.sender, address(this)); + token.transferFrom(msg.sender, address(this), allowance); + + initial_deposit = token.totalSupply(); + + _count_deposit += 1; + } + + function withdraw(uint amount) public { + sent += amount; + token.transfer(msg.sender, amount); + } + + function getBalance() public view returns (uint) { + return token.balanceOf(address(this)); + } + + function getAddressBalance(address addr) public view returns (uint) { + return token.balanceOf(addr); + } + + function getSent() public view returns (uint) { + return sent; + } + + function getInitialDeposit() public view returns (uint) { + return initial_deposit; + } + +} diff --git a/contracts/deposit_erc20/hardhat/ERC20v1.sol b/contracts/deposit_erc20/hardhat/ERC20v1.sol new file mode 100644 index 00000000..db15e7a2 --- /dev/null +++ b/contracts/deposit_erc20/hardhat/ERC20v1.sol @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: MIT +pragma solidity >= 0.8.2; + +import "./IERC20.sol"; + +/** + * @dev Implementation of the {IERC20} interface. + * + */ +contract ERC20 is IERC20 { + mapping(address => uint256) private _balances; + uint256 private _totalSupply; + + constructor(uint256 amount) { + _totalSupply += amount; + _balances[msg.sender] += amount; + } + + function totalSupply() public view returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view returns (uint256) { + return _balances[account]; + } + + /** + * Requirements: + * - `to` cannot be the zero address. + * - the caller must have a balance of at least `amount`. + */ + function transfer(address to, uint256 amount) public returns (bool) { + _transfer(msg.sender, to, amount); + return true; + } + + function allowance(address owner, address spender) public view returns (uint256) { + require (owner != address(0)); + require (spender != address(0)); + return _balances[owner]; + } + + /** + * NOTE: If `amount` is the maximum `uint256`, the allowance is not updated on + * `transferFrom`. This is semantically equivalent to an infinite approval. + * + * Requirements: + * - `spender` cannot be the zero address. + */ + function approve(address spender, uint256 amount) public view returns (bool) { + _approve(msg.sender, spender, amount); + return true; + } + + /** + * @dev See {IERC20-transferFrom}. + * + * + * NOTE: Does not update the allowance if the current allowance + * is the maximum `uint256`. + * + * Requirements: + * + * - `from` and `to` cannot be the zero address. + * - `from` must have a balance of at least `amount`. + * - the caller must have allowance for ``from``'s tokens of at least + * `amount`. + */ + function transferFrom(address from, address to, uint256 amount) public returns (bool) { + _spendAllowance(from, msg.sender, amount); + _transfer(from, to, amount); + return true; + } + + function _transfer(address from, address to, uint256 amount) internal { + require (from != address(0)); + require (to != address(0)); + + uint256 fromBalance = _balances[from]; + require (fromBalance >= amount); + // unchecked { + // Overflow not possible: amount <= fromBalance <= totalSupply. + _balances[from] = fromBalance - amount; + // Overflow not possible: balance + amount is at most totalSupply, which we know fits into a uint256. + _balances[to] += amount; + // } + } + + /** + * @dev Sets `amount` as the allowance of `spender` over the `owner` s tokens. + * + * This internal function is equivalent to `approve`, and can be used to + * e.g. set automatic allowances for certain subsystems, etc. + * + * Requirements: + * + * - `owner` cannot be the zero address. + * - `spender` cannot be the zero address. + */ + function _approve(address owner, address spender, uint256 amount) internal pure { + require (owner != address(0)); + require (spender != address(0)); + require (amount >= 0); + } + + /** + * @dev Updates `owner` s allowance for `spender` based on spent `amount`. + * + * Does not update the allowance amount in case of infinite allowance. + * Revert if not enough allowance is available. + * + */ + function _spendAllowance(address owner, address spender, uint256 amount) internal view { + uint256 currentAllowance = allowance(owner, spender); + require (currentAllowance >= amount); + _approve(owner, spender, currentAllowance); + } +} diff --git a/contracts/deposit_erc20/hardhat/IERC20.sol b/contracts/deposit_erc20/hardhat/IERC20.sol new file mode 100644 index 00000000..66c4e4d8 --- /dev/null +++ b/contracts/deposit_erc20/hardhat/IERC20.sol @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.6.0) (token/ERC20/IERC20.sol) + +pragma solidity ^0.8.0; + +/** + * @dev Interface of the ERC20 standard as defined in the EIP. + */ +interface IERC20 { + /** + * @dev Emitted when `value` tokens are moved from one account (`from`) to + * another (`to`). + * + * Note that `value` may be zero. + */ + event Transfer(address indexed from, address indexed to, uint256 value); + + /** + * @dev Emitted when the allowance of a `spender` for an `owner` is set by + * a call to {approve}. `value` is the new allowance. + */ + event Approval(address indexed owner, address indexed spender, uint256 value); + + /** + * @dev Returns the amount of tokens in existence. + */ + function totalSupply() external view returns (uint256); + + /** + * @dev Returns the amount of tokens owned by `account`. + */ + function balanceOf(address account) external view returns (uint256); + + /** + * @dev Moves `amount` tokens from the caller's account to `to`. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transfer(address to, uint256 amount) external returns (bool); + + /** + * @dev Returns the remaining number of tokens that `spender` will be + * allowed to spend on behalf of `owner` through {transferFrom}. This is + * zero by default. + * + * This value changes when {approve} or {transferFrom} are called. + */ + function allowance(address owner, address spender) external view returns (uint256); + + /** + * @dev Sets `amount` as the allowance of `spender` over the caller's tokens. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * IMPORTANT: Beware that changing an allowance with this method brings the risk + * that someone may use both the old and the new allowance by unfortunate + * transaction ordering. One possible solution to mitigate this race + * condition is to first reduce the spender's allowance to 0 and set the + * desired value afterwards: + * https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + * + * Emits an {Approval} event. + */ + function approve(address spender, uint256 amount) external returns (bool); + + /** + * @dev Moves `amount` tokens from `from` to `to` using the + * allowance mechanism. `amount` is then deducted from the caller's + * allowance. + * + * Returns a boolean value indicating whether the operation succeeded. + * + * Emits a {Transfer} event. + */ + function transferFrom(address from, address to, uint256 amount) external returns (bool); +} diff --git a/contracts/deposit_erc20/hardhat/test.js b/contracts/deposit_erc20/hardhat/test.js new file mode 100644 index 00000000..f0c7dddf --- /dev/null +++ b/contracts/deposit_erc20/hardhat/test.js @@ -0,0 +1,29 @@ +const { + loadFixture, + } = require("@nomicfoundation/hardhat-toolbox/network-helpers"); + const { expect } = require("chai"); + + describe("DepositERC20_v1", function() { + async function deployContractv1() { + const [receiver] = await ethers.getSigners(); + + const ERC20Factory = await ethers.getContractFactory("ERC20"); + const ERC20 = await ERC20Factory.deploy(100); + const DepositERC20Factory = await ethers.getContractFactory("TokenTransfer"); + const DepositERC20 = await DepositERC20Factory.deploy(ERC20.getAddress()); + + return { DepositERC20, ERC20, receiver }; + } + it("wd-leq-init-bal: the overall withdrawn amount exceed the initial deposit", async function(){ + const { DepositERC20, ERC20, receiver } = await loadFixture(deployContractv1); + await DepositERC20.deposit(); + + await DepositERC20.connect(receiver).withdraw(100); + await ERC20.connect(receiver).transfer(DepositERC20, 100); + await DepositERC20.connect(receiver).withdraw(100); + + expect(await DepositERC20.getSent()).to.be.equal(200); + + + }) + }) From 6f17cd096e19e52b4d1e5922928d91ca301261ad Mon Sep 17 00:00:00 2001 From: TistaMilani Date: Mon, 9 Jun 2025 16:08:19 +0000 Subject: [PATCH 4/4] Added empty getters and methods files, updated Makefile and solcmc dir according to the actual standard. --- contracts/deposit_erc20/Makefile | 127 ++++-------------- contracts/deposit_erc20/README.md | 51 ------- contracts/deposit_erc20/certora/Makefile | 85 ++++++++++++ .../certora/always-depletable.spec | 7 +- .../DepositERC20_always-depletable_v1.conf | 5 +- ...epositERC20_deposit-deposit-revert_v1.conf | 5 +- .../DepositERC20_no-deposit-twice_v1.conf | 5 +- .../conf/DepositERC20_wd-contract-bal_v1.conf | 5 +- .../conf/DepositERC20_wd-leq-init-bal_v1.conf | 5 +- .../conf/DepositERC20_wd-not-revert_v1.conf | 5 +- .../conf/DepositERC20_wd-sender-rcv_v1.conf | 5 +- contracts/deposit_erc20/certora/getters.sol | 1 + contracts/deposit_erc20/certora/methods.spec | 1 + .../certora/wd-contract-bal.spec | 4 +- .../certora/wd-leq-init-bal.spec | 10 +- .../deposit_erc20/certora/wd-not-revert.spec | 6 +- .../deposit_erc20/certora/wd-sender-rcv.spec | 4 +- .../DepositERC20_no-deposit-twice_v1.sol | 58 -------- .../DepositERC20_wd-contract-bal_v1.sol | 63 --------- .../DepositERC20_wd-leq-init-bal_v1.sol | 57 -------- contracts/deposit_erc20/solcmc/Makefile | 68 ++++++++++ .../deposit_erc20/solcmc/no-deposit-twice.sol | 4 + .../deposit_erc20/solcmc/wd-contract-bal.sol | 9 ++ .../deposit_erc20/solcmc/wd-leq-init-bal.sol | 3 + .../versions/DepositERC20_v1.sol | 16 --- 25 files changed, 241 insertions(+), 368 deletions(-) delete mode 100644 contracts/deposit_erc20/README.md create mode 100644 contracts/deposit_erc20/certora/Makefile create mode 100644 contracts/deposit_erc20/certora/getters.sol create mode 100644 contracts/deposit_erc20/certora/methods.spec delete mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol delete mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol delete mode 100644 contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol create mode 100644 contracts/deposit_erc20/solcmc/Makefile create mode 100644 contracts/deposit_erc20/solcmc/no-deposit-twice.sol create mode 100644 contracts/deposit_erc20/solcmc/wd-contract-bal.sol create mode 100644 contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol diff --git a/contracts/deposit_erc20/Makefile b/contracts/deposit_erc20/Makefile index 3b5d630a..38e75235 100644 --- a/contracts/deposit_erc20/Makefile +++ b/contracts/deposit_erc20/Makefile @@ -1,47 +1,26 @@ -MAKEFLAGS = --no-print-directory +SOLCMC_DIR = ./solcmc +SOLCMC_BUILD_DIR = $(SOLCMC_DIR)/build +SOLCMC_Z3_TABLE = $(SOLCMC_BUILD_DIR)/z3/table.md +SOLCMC_ELD_TABLE = $(SOLCMC_BUILD_DIR)/eld/table.md -# CHANGE THIS PATHS -# Original contract path -CONTRACT = ./versions/DepositERC20_v1.sol -# Contract with solcmc instrumentation path -SOLCMC_CONTRACT = ./solcmc -# Certora specifications path -CERTORA_SPEC = ./certora +CERTORA_DIR = ./certora +CERTORA_BUILD_DIR = $(CERTORA_DIR)/build +CERTORA_TABLE = $(CERTORA_BUILD_DIR)/table.md +VERSIONS_DIR = ./versions SKELETON = ./skeleton.json GROUND_TRUTH = ./ground-truth.csv -README = ./README.md -BUILD_DIR = ./build +README = README.md -# SOLCMC params -to = 10m -Z3_DIR = $(BUILD_DIR)/z3 -Z3_OUT = $(Z3_DIR)/out.csv -Z3_CM = $(Z3_DIR)/cm.csv -Z3_TABLE = $(Z3_DIR)/table.md -Z3_LOGS = $(Z3_DIR)/logs -ELD_DIR = $(BUILD_DIR)/eld -ELD_OUT = $(ELD_DIR)/out.csv -ELD_CM = $(ELD_DIR)/cm.csv -ELD_TABLE = $(ELD_DIR)/table.md -ELD_LOGS = $(ELD_DIR)/logs +PYTHON = python -# Certora params -CERTORA_DIR = $(BUILD_DIR)/certora -CERTORA_OUT = $(CERTORA_DIR)/out.csv -CERTORA_CM = $(CERTORA_DIR)/cm.csv -CERTORA_TABLE = $(CERTORA_DIR)/table.md -CERTORA_LOGS = $(CERTORA_DIR)/logs - -PYTHON = python3 - -.PHONY: all certora solcmc plain clean cleanr +.PHONY: all certora solcmc plain clean cleanr clean-solcmc clean-certora all: plain solcmc certora @echo "Adding Solcmc table to README..." @echo "### SolCMC" >> $(README) - @cat $(Z3_TABLE) >> $(README) - @cat $(ELD_TABLE) >> $(README) + @cat $(SOLCMC_Z3_TABLE) >> $(README) + @cat $(SOLCMC_ELD_TABLE) >> $(README) @echo "" >> $(README) @echo "Adding Certora table to README..." @cat $(CERTORA_TABLE) >> $(README) @@ -49,84 +28,34 @@ all: plain solcmc certora #---------------------------- CERTORA ----------------------------# certora: $(CERTORA_TABLE) -$(CERTORA_TABLE): $(CERTORA_CM) - @echo "Generating Certora results table ($(CERTORA_TABLE))..." - @echo "### Certora" > $(CERTORA_TABLE) - @$(PYTHON) ../../scripts/mdtable_gen.py --input $(CERTORA_CM) >> $(CERTORA_TABLE) - -$(CERTORA_CM): $(GROUND_TRUTH) $(CERTORA_OUT) - @echo "Generating Certora confusion matrix ($(CERTORA_CM))..." - @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(CERTORA_OUT) > $(CERTORA_CM) - -$(CERTORA_OUT): setup - @echo "Running Certora experiments..." - @$(PYTHON) ../../scripts/run_certora.py --contracts $(CONTRACT) --specs $(CERTORA_SPEC) --output $(CERTORA_DIR) +$(CERTORA_TABLE): + @cd $(realpath $(CERTORA_DIR)) && make #---------------------------- SOLCMC -----------------------------# -solcmc: $(Z3_TABLE) $(ELD_TABLE) - -# Solcmc with Z3 -# Make markdown table -$(Z3_TABLE): $(Z3_CM) - @echo "Generating SolCMC results table ($(Z3_TABLE))..." - echo "#### Z3" > $(Z3_TABLE) - @$(PYTHON) ../../scripts/mdtable_gen.py --input $(Z3_CM) >> $(Z3_TABLE) - -# Build confusion matrix with ground truths -$(Z3_CM): $(GROUND_TRUTH) $(Z3_OUT) - @echo "Generating Solcmc confusion matrix ($(Z3_CM))..." - @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(Z3_OUT) > $(Z3_CM) - -# Run experiments -$(Z3_OUT): setup - @echo "Running SolCMC ($(solver)) experiments..." - @$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(Z3_DIR) --timeout $(to) --solver z3 +solcmc: $(SOLCMC_Z3_TABLE) $(SOLCMC_ELD_TABLE) -# Solcmc with eldarica -# Make markdown table -$(ELD_TABLE): $(ELD_CM) - @echo "Generating SolCMC results table ($(ELD_TABLE))..." - echo "#### ELD" > $(ELD_TABLE) - @$(PYTHON) ../../scripts/mdtable_gen.py --input $(ELD_CM) >> $(ELD_TABLE) +$(SOLCMC_Z3_TABLE): + @cd $(realpath $(SOLCMC_DIR)) && make solver=z3 -# Build confusion matrix with ground truths -$(ELD_CM): $(GROUND_TRUTH) $(ELD_OUT) - @echo "Generating Solcmc confusion matrix ($(ELD_CM))..." - @$(PYTHON) ../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(ELD_OUT) > $(ELD_CM) - -# Run experiments -$(ELD_OUT): setup - @echo "Running SolCMC ($(solver)) experiments..." - @$(PYTHON) ../../scripts/run_solcmc.py --contracts $(SOLCMC_CONTRACT) --output $(ELD_DIR) --timeout $(to) --solver eld - -#---------------------------- SETUP ------------------------------# -setup: $(Z3_LOGS) $(ELD_LOGS) $(CERTORA_LOGS) - -# Create build logs/ dirs, and build/ dirs with them -$(Z3_LOGS): - @mkdir -p $@ - -$(ELD_LOGS): - @mkdir -p $@ - -$(CERTORA_LOGS): - @mkdir -p $@ +$(SOLCMC_ELD_TABLE): + @cd $(realpath $(SOLCMC_DIR)) && make solver=eld #---------------------------- README -----------------------------# plain: cleanr $(README) -# Create plain README, without experiments results $(README): $(VERSIONS_DIR) $(SKELETON) $(GROUND_TRUTH) @echo "Generating plain README..." @$(PYTHON) ../../scripts/readme_gen.py -d . > $(README) @echo "## Experiments" >> $(README) #---------------------------- CLEAN ------------------------------# -clean: cleanr - @echo "Removing $(BUILD_DIR)..." - @rm -rf $(BUILD_DIR) +clean: cleanr clean-solcmc clean-certora -# Remove README.md cleanr: - @echo "Removing README..." - @rm -f $(README) + rm -f $(README) + +clean-solcmc: + cd $(realpath $(SOLCMC_DIR)) && make clean + +clean-certora: + cd $(realpath $(CERTORA_DIR)) && make clean diff --git a/contracts/deposit_erc20/README.md b/contracts/deposit_erc20/README.md deleted file mode 100644 index 7325d314..00000000 --- a/contracts/deposit_erc20/README.md +++ /dev/null @@ -1,51 +0,0 @@ -# Deposit (ERC20) - -## Specification -This contract implements the same functionality of the [Deposit contract](../deposit_eth), but operates on ERC20 tokens instead of ETH. - -The `constructor` takes the token address as a parameter. - -The `deposit` function allows the sender to deposit an arbitrary number of token units into the contract; it can be called only once. Before calling `deposit`, the depositor must approve that the amount they want to deposit can be spent by the contract: if so, the entire allowance is transferred to the contract. - -The function `withdraw(amount)` can be called by anyone to transfer `amount` token units to the transaction sender. - -## Properties -- **always-depletable**: anyone at any time can fire a transaction to receive the full balance of the contract. -- **deposit-deposit-revert**: if `deposit` is called after `deposit` the second call aborts. -- **no-deposit-twice**: `deposit` can only be called once. -- **wd-contract-bal**: the contract token balance is decreased by `amount` after a successful `withdraw(amount)`. -- **wd-leq-init-bal**: the overall withdrawn amount does not exceed the initial deposit. -- **wd-not-revert**: a transaction `withdraw(amount)` is not reverted whenever the `amount` does not exceed the contract balance. -- **wd-sender-rcv**: after a successful `withdraw(amount)`, the balance of the transaction sender is increased by `amount`. - -## Versions -- **v1**: conformant to specification. - -## Ground truth -| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | -|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| -| **v1** | 1 | 1 | 1 | 1 | 0[^1] | 1 | 1 | - -[^1]: This property should not hold for ERC20 tokens, since one can easily increase the contract balance without the contract being able to notice or prevent it. Since this is also possible with ETH (via coinbase or `selfdestruct` transactions), the behavior is comparable for the purposes of these tests. - -## Experiments -### SolCMC -#### Z3 -| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | -|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| -| **v1** | ND | ND | ERR | FN! | TN! | ND | ND | - - -#### ELD -| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | -|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| -| **v1** | ND | ND | TP! | FN! | TN! | ND | ND | - - - -### Certora -| | always-depletable | deposit-deposit-revert | no-deposit-twice | wd-contract-bal | wd-leq-init-bal | wd-not-revert | wd-sender-rcv | -|--------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------|------------------------| -| **v1** | TP! | TP! | TP! | TP! | TN | TP! | TP! | - - diff --git a/contracts/deposit_erc20/certora/Makefile b/contracts/deposit_erc20/certora/Makefile new file mode 100644 index 00000000..60f1b037 --- /dev/null +++ b/contracts/deposit_erc20/certora/Makefile @@ -0,0 +1,85 @@ +# Params +contract = "" +specs = "" + +# Input Files +VERSIONS_DIR = ../versions/ +PROPERTIES_DIR = . +GROUND_TRUTH = ../ground-truth.csv +SPEC_FILES = $(wildcard $(PROPERTIES_DIR)/*.spec) +GETTER_FILE = getters.sol +METHODS_FILE = methods.spec +VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol) + +# Output Files +BUILD_DIR = build +OUTPUT_DIR = $(BUILD_DIR) +CONTRACTS_DIR = $(OUTPUT_DIR)/contracts +LOGS_DIR = $(OUTPUT_DIR)/logs +SPEC_DIR = $(OUTPUT_DIR)/specs +LIB_DIR = $(CONTRACTS_DIR)/lib +OUT = $(OUTPUT_DIR)/out.csv +CM = $(OUTPUT_DIR)/cm.csv +TABLE = $(OUTPUT_DIR)/table.md + +PYTHON = python + +.PHONY: run one setup contracts specs getters directories clean-specs clean + +#---------------------------- RUN --------------------------------# +run: $(TABLE) + +$(TABLE): $(CM) + @echo "Generating Certora results table ($(TABLE))..." + @echo "### Certora" > $(TABLE) + @$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE) + +$(CM): $(GROUND_TRUTH) $(OUT) + @echo "Generating Certora confusion matrix ($(CM))..." + @$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM) + +$(OUT): setup $(VERSIONS_FILES) $(SPEC_FILES) $(GETTER_FILE) + @echo "Running Certora experiments..." + @$(PYTHON) ../../../scripts/run_certora.py --contracts $(CONTRACTS_DIR) --specs $(SPEC_DIR) --output $(OUTPUT_DIR) + +one: clean-specs contracts specs directories + @$(PYTHON) ../../../scripts/run_certora.py --contracts $(contract) --specs $(specs) + +#---------------------------- SETUP ------------------------------# +setup: contracts specs getters directories + +contracts: $(CONTRACTS_DIR) getters + @$(PYTHON) ../../../scripts/inject_getters.py --contracts $(VERSIONS_DIR) --getters $(GETTER_FILE) --output $(CONTRACTS_DIR) + +specs: $(SPEC_DIR) + @for file in $(SPEC_FILES); do \ + if [ "$$file" != $(PROPERTIES_DIR)/"methods.spec" ]; then \ + echo "Processing $$file"; \ + cat $(METHODS_FILE) $$file >> $(SPEC_DIR)/$$file; \ + fi \ + done; + +getters: + @if ! [ -e $(GETTER_FILE) ]; then touch $(GETTER_FILE); fi; + +directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR) $(SPEC_DIR) + +$(CONTRACTS_DIR): + @mkdir -p $@ + +$(SPEC_DIR): + @mkdir -p $@ + +$(LOGS_DIR): + @mkdir -p $@ + +$(LIB_DIR): + @cp -r ../../../lib/ $@ + +#---------------------------- CLEAN ------------------------------# +clean-specs: + rm -rf $(SPEC_DIR) + +clean: + rm -rf $(BUILD_DIR) + diff --git a/contracts/deposit_erc20/certora/always-depletable.spec b/contracts/deposit_erc20/certora/always-depletable.spec index 1c24c4d7..3edb4d4f 100644 --- a/contracts/deposit_erc20/certora/always-depletable.spec +++ b/contracts/deposit_erc20/certora/always-depletable.spec @@ -8,11 +8,12 @@ rule always_depletable { require(e.msg.sender != currentContract); require(e.msg.value == 0); - uint amount = getAddressBalance(e, currentContract); - require(max_uint >= amount + getAddressBalance(e, e.msg.sender)); + uint amount = currentContract.token.balanceOf(e, currentContract); + require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender)); require(currentContract.sent + amount <= max_uint); + withdraw@withrevert(e, amount); assert !lastReverted; - assert (getAddressBalance(e, currentContract) == 0); + assert (currentContract.token.balanceOf(e, currentContract) == 0); } diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf index 725f04a4..4b10cb5f 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_always-depletable_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/always-depletable.spec" + "verify": "TokenTransfer:certora/always-depletable.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf index 6ebefe55..d41922de 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_deposit-deposit-revert_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/deposit-deposit-revert.spec" + "verify": "TokenTransfer:certora/deposit-deposit-revert.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf index caa42b95..9751a2cf 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_no-deposit-twice_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/no-deposit-twice.spec" + "verify": "TokenTransfer:certora/no-deposit-twice.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf index f980a16b..da8059d6 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-contract-bal_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/wd-contract-bal.spec" + "verify": "TokenTransfer:certora/wd-contract-bal.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf index 5f3ef5a1..351be50a 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-leq-init-bal_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/wd-leq-init-bal.spec" + "verify": "TokenTransfer:certora/wd-leq-init-bal.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf index 302bef33..c0448798 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-not-revert_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/wd-not-revert.spec" + "verify": "TokenTransfer:certora/wd-not-revert.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf index f7fe65e9..e0e36cdc 100644 --- a/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf +++ b/contracts/deposit_erc20/certora/conf/DepositERC20_wd-sender-rcv_v1.conf @@ -3,5 +3,8 @@ "versions/lib/ERC20v1.sol:ERC20", "versions/DepositERC20_v1.sol:TokenTransfer" ], - "verify": "TokenTransfer:certora/wd-sender-rcv.spec" + "verify": "TokenTransfer:certora/wd-sender-rcv.spec", + "link": [ + "TokenTransfer:token=ERC20" + ] } \ No newline at end of file diff --git a/contracts/deposit_erc20/certora/getters.sol b/contracts/deposit_erc20/certora/getters.sol new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/contracts/deposit_erc20/certora/getters.sol @@ -0,0 +1 @@ + diff --git a/contracts/deposit_erc20/certora/methods.spec b/contracts/deposit_erc20/certora/methods.spec new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/contracts/deposit_erc20/certora/methods.spec @@ -0,0 +1 @@ + diff --git a/contracts/deposit_erc20/certora/wd-contract-bal.spec b/contracts/deposit_erc20/certora/wd-contract-bal.spec index a732f61e..d2010276 100644 --- a/contracts/deposit_erc20/certora/wd-contract-bal.spec +++ b/contracts/deposit_erc20/certora/wd-contract-bal.spec @@ -5,12 +5,12 @@ rule wd_contract_bal { env e; uint amount; mathint mi_amount = amount; - mathint before = getBalance(e); + mathint before = currentContract.token.balanceOf(e, currentContract); require before >= mi_amount; withdraw(e, amount); - mathint after = getBalance(e); + mathint after = currentContract.token.balanceOf(e, currentContract); if(e.msg.sender == currentContract) { assert before == after; } diff --git a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec index cd80cc65..7a1921e9 100644 --- a/contracts/deposit_erc20/certora/wd-leq-init-bal.spec +++ b/contracts/deposit_erc20/certora/wd-leq-init-bal.spec @@ -1,10 +1,4 @@ import "helper/erc20.spec"; -methods { - function withdraw(uint) external; - function getBalance() external returns (uint) envfree; - function getAddressBalance(address) external returns (uint) envfree; - function getInitialDeposit() external returns (uint) envfree; - function getSent() external returns (uint) envfree; -} + invariant wd_leq_init_bal() - getSent() <= getInitialDeposit(); + currentContract.sent <= currentContract.initial_deposit; diff --git a/contracts/deposit_erc20/certora/wd-not-revert.spec b/contracts/deposit_erc20/certora/wd-not-revert.spec index 379ef5cc..fcbe3663 100644 --- a/contracts/deposit_erc20/certora/wd-not-revert.spec +++ b/contracts/deposit_erc20/certora/wd-not-revert.spec @@ -4,14 +4,16 @@ import "helper/erc20.spec"; rule wd_not_revert { env e; uint amount; + uint before = currentContract.token.balanceOf(e, currentContract); - uint before = getAddressBalance(e, currentContract); require(e.msg.sender != 0); require(e.msg.value == 0); - require(max_uint >= amount + getAddressBalance(e, e.msg.sender)); + + require(max_uint >= amount + currentContract.token.balanceOf(e, e.msg.sender)); require(currentContract.sent + amount + before <= max_uint); require(amount <= before); withdraw@withrevert(e, amount); + assert !lastReverted; } diff --git a/contracts/deposit_erc20/certora/wd-sender-rcv.spec b/contracts/deposit_erc20/certora/wd-sender-rcv.spec index 791aede5..096d28d3 100644 --- a/contracts/deposit_erc20/certora/wd-sender-rcv.spec +++ b/contracts/deposit_erc20/certora/wd-sender-rcv.spec @@ -6,9 +6,9 @@ rule wd_sender_rcv { uint amount; address sender = e.msg.sender; - mathint before = getAddressBalance(e, sender); + mathint before = currentContract.token.balanceOf(e, sender); withdraw(e, amount); - mathint after = getAddressBalance(e, sender); + mathint after = currentContract.token.balanceOf(e, sender); if(e.msg.sender != currentContract) assert after == before + amount; diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol deleted file mode 100644 index 6e8b6b40..00000000 --- a/contracts/deposit_erc20/solcmc/DepositERC20_no-deposit-twice_v1.sol +++ /dev/null @@ -1,58 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity >= 0.8.2; - -import "../versions/lib/ERC20v1.sol"; - -/// @custom:version conformant to specification. -contract TokenTransfer { - ERC20 token; - bool ever_deposited; - - uint private sent; - uint initial_deposit; - - // ghost variables - uint _count_deposit; - - constructor(ERC20 token_) { - token = token_; - } - - function deposit() public { - require(!ever_deposited); - - ever_deposited = true; - uint allowance = token.allowance(msg.sender, address(this)); - token.transferFrom(msg.sender, address(this), allowance); - - initial_deposit = token.totalSupply(); - - _count_deposit += 1; - } - - function withdraw(uint amount) public { - sent += amount; - token.transfer(msg.sender, amount); - } - - function getBalance() public view returns (uint) { - return token.balanceOf(address(this)); - } - - function getAddressBalance(address addr) public view returns (uint) { - return token.balanceOf(addr); - } - - function getSent() public view returns (uint) { - return sent; - } - - function getInitialDeposit() public view returns (uint) { - return initial_deposit; - } - - // p1 - function invariant() public view { - assert(_count_deposit <= 1); - } -} diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol deleted file mode 100644 index bf7185d1..00000000 --- a/contracts/deposit_erc20/solcmc/DepositERC20_wd-contract-bal_v1.sol +++ /dev/null @@ -1,63 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity >= 0.8.2; - -import "../versions/lib/ERC20v1.sol"; - -/// @custom:version conformant to specification. -contract TokenTransfer { - ERC20 token; - bool ever_deposited; - - uint private sent; - uint initial_deposit; - - // ghost variables - uint _count_deposit; - - constructor(ERC20 token_) { - token = token_; - } - - function deposit() public { - require(!ever_deposited); - - ever_deposited = true; - uint allowance = token.allowance(msg.sender, address(this)); - token.transferFrom(msg.sender, address(this), allowance); - - initial_deposit = token.totalSupply(); - - _count_deposit += 1; - } - - function withdraw(uint amount) public { - sent += amount; - token.transfer(msg.sender, amount); - } - - function getBalance() public view returns (uint) { - return token.balanceOf(address(this)); - } - - function getAddressBalance(address addr) public view returns (uint) { - return token.balanceOf(addr); - } - - function getSent() public view returns (uint) { - return sent; - } - - function getInitialDeposit() public view returns (uint) { - return initial_deposit; - } - - function invariant(uint amount) public { - uint old_balance = token.balanceOf(address(this)); - - withdraw(amount); - - uint new_balance = token.balanceOf(address(this)); - - assert(new_balance == old_balance - amount); - } -} \ No newline at end of file diff --git a/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol b/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol deleted file mode 100644 index 2725b6f9..00000000 --- a/contracts/deposit_erc20/solcmc/DepositERC20_wd-leq-init-bal_v1.sol +++ /dev/null @@ -1,57 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity >= 0.8.2; - -import "../versions/lib/ERC20v1.sol"; - -/// @custom:version conformant to specification. -contract TokenTransfer { - ERC20 token; - bool ever_deposited; - - uint private sent; - uint initial_deposit; - - // ghost variables - uint _count_deposit; - - constructor(ERC20 token_) { - token = token_; - } - - function deposit() public { - require(!ever_deposited); - - ever_deposited = true; - uint allowance = token.allowance(msg.sender, address(this)); - token.transferFrom(msg.sender, address(this), allowance); - - initial_deposit = token.totalSupply(); - - _count_deposit += 1; - } - - function withdraw(uint amount) public { - sent += amount; - token.transfer(msg.sender, amount); - } - - function getBalance() public view returns (uint) { - return token.balanceOf(address(this)); - } - - function getAddressBalance(address addr) public view returns (uint) { - return token.balanceOf(addr); - } - - function getSent() public view returns (uint) { - return sent; - } - - function getInitialDeposit() public view returns (uint) { - return initial_deposit; - } - - function invariant() public view { - assert(sent <= initial_deposit); - } -} \ No newline at end of file diff --git a/contracts/deposit_erc20/solcmc/Makefile b/contracts/deposit_erc20/solcmc/Makefile new file mode 100644 index 00000000..6ed4dd8f --- /dev/null +++ b/contracts/deposit_erc20/solcmc/Makefile @@ -0,0 +1,68 @@ +# Params +solver = z3 +to = 10m +contract = "" + +# Input files +VERSIONS_DIR = ../versions/ +PROPERTIES_DIR = . +GROUND_TRUTH = ../ground-truth.csv +PROPERTIES_FILES = $(wildcard $(PROPERTIES_DIR)/*.sol) +VERSIONS_FILES = $(wildcard $(VERSIONS_DIR)/*.sol) + +# Output files +BUILD_DIR = build +OUTPUT_DIR = $(BUILD_DIR)/$(solver) +CONTRACTS_DIR = $(BUILD_DIR)/contracts +LOGS_DIR = $(OUTPUT_DIR)/logs +LIB_DIR = $(CONTRACTS_DIR)/lib +OUT = $(OUTPUT_DIR)/out.csv +CM = $(OUTPUT_DIR)/cm.csv +TABLE = $(OUTPUT_DIR)/table.md + +PYTHON = python + +.PHONY: run one setup contracts directories clean + +#---------------------------- RUN --------------------------------# +run: $(TABLE) + +$(TABLE): $(CM) + @echo "Generating SolCMC results table ($(TABLE))..." + @if [ $(solver) = "z3" ]; then echo "#### Z3" > $(TABLE); \ + elif [ $(solver) = "eld" ]; then echo "#### Eldarica" > $(TABLE); fi + @$(PYTHON) ../../../scripts/mdtable_gen.py --input $(CM) >> $(TABLE) + +$(CM): $(GROUND_TRUTH) $(OUT) + @echo "Generating Solcmc confusion matrix ($(CM))..." + @$(PYTHON) ../../../scripts/cm_gen.py --ground-truth $(GROUND_TRUTH) --results $(OUT) > $(CM) + +$(OUT): setup $(PROPERTIES_FILES) $(VERSIONS_FILES) + @echo "Running SolCMC ($(solver)) experiments..." + @$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(CONTRACTS_DIR)/ --output $(OUTPUT_DIR) --timeout $(to) --solver $(solver) + +one: setup + @$(PYTHON) ../../../scripts/run_solcmc.py --contracts $(contract) --timeout $(to) + +#---------------------------- SETUP ------------------------------# +setup: contracts directories + +contracts: $(VERSIONS_FILES) $(PROPERTIES_FILES) $(CONTRACTS_DIR) + @echo "Building contracts..." + @$(PYTHON) ../../../scripts/builder.py --versions $(VERSIONS_DIR) --properties $(PROPERTIES_DIR) --output $(CONTRACTS_DIR) + +directories: $(CONTRACTS_DIR) $(LOGS_DIR) $(LIB_DIR) + +$(CONTRACTS_DIR): + @mkdir -p $@ + +$(LOGS_DIR): + @mkdir -p $@ + +$(LIB_DIR): + @cp -r ../../../lib/ $@ + +#---------------------------- CLEAN ------------------------------# +clean: + @echo "Deleting \"solcmc/build/\"..." + @rm -rf $(BUILD_DIR) diff --git a/contracts/deposit_erc20/solcmc/no-deposit-twice.sol b/contracts/deposit_erc20/solcmc/no-deposit-twice.sol new file mode 100644 index 00000000..1e569b44 --- /dev/null +++ b/contracts/deposit_erc20/solcmc/no-deposit-twice.sol @@ -0,0 +1,4 @@ +function invariant() public view { + assert(_count_deposit <= 1); +} + diff --git a/contracts/deposit_erc20/solcmc/wd-contract-bal.sol b/contracts/deposit_erc20/solcmc/wd-contract-bal.sol new file mode 100644 index 00000000..0772bf6a --- /dev/null +++ b/contracts/deposit_erc20/solcmc/wd-contract-bal.sol @@ -0,0 +1,9 @@ +function invariant(uint amount) public { + uint old_balance = token.balanceOf(address(this)); + + withdraw(amount); + + uint new_balance = token.balanceOf(address(this)); + + assert(new_balance == old_balance - amount); +} \ No newline at end of file diff --git a/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol b/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol new file mode 100644 index 00000000..cb84a4ec --- /dev/null +++ b/contracts/deposit_erc20/solcmc/wd-leq-init-bal.sol @@ -0,0 +1,3 @@ +function invariant() public view { + assert(sent <= initial_deposit); +} diff --git a/contracts/deposit_erc20/versions/DepositERC20_v1.sol b/contracts/deposit_erc20/versions/DepositERC20_v1.sol index 80682d5f..23c78374 100644 --- a/contracts/deposit_erc20/versions/DepositERC20_v1.sol +++ b/contracts/deposit_erc20/versions/DepositERC20_v1.sol @@ -34,21 +34,5 @@ contract TokenTransfer { sent += amount; token.transfer(msg.sender, amount); } - - function getBalance() public view returns (uint) { - return token.balanceOf(address(this)); - } - - function getAddressBalance(address addr) public view returns (uint) { - return token.balanceOf(addr); - } - - function getSent() public view returns (uint) { - return sent; - } - - function getInitialDeposit() public view returns (uint) { - return initial_deposit; - } } \ No newline at end of file