contract: added SimplifiedDeflationaryToken contract

contracts/simplified_deflationary_token/Makefile

@@ -0,0 +1,61 @@
+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
+
+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
+
+PYTHON = python
+
+.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 $(SOLCMC_Z3_TABLE) >> $(README)
+	@cat $(SOLCMC_ELD_TABLE) >> $(README)
+	@echo "" >> $(README)
+	@echo "Adding Certora table to README..."
+	@cat $(CERTORA_TABLE) >> $(README)
+
+#---------------------------- CERTORA ----------------------------#
+certora: $(CERTORA_TABLE)
+
+$(CERTORA_TABLE):
+	@cd $(realpath $(CERTORA_DIR)) && make
+
+#---------------------------- SOLCMC -----------------------------#
+solcmc: $(SOLCMC_Z3_TABLE) $(SOLCMC_ELD_TABLE)
+
+$(SOLCMC_Z3_TABLE):
+	@cd $(realpath $(SOLCMC_DIR)) && make solver=z3
+
+$(SOLCMC_ELD_TABLE):
+	@cd $(realpath $(SOLCMC_DIR)) && make solver=eld
+
+#---------------------------- README -----------------------------#
+plain: cleanr $(README)
+
+$(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
+
+cleanr:
+	rm -f $(README)
+
+clean-solcmc:
+	cd $(realpath $(SOLCMC_DIR)) && make clean
+
+clean-certora:
+	cd $(realpath $(CERTORA_DIR)) && make clean

contracts/simplified_deflationary_token/README.md

@@ -0,0 +1,59 @@
+# Simplified Deflationary Token
+
+## Specification
+This contract implements a simplified version of a deflationary token using `uint256`, where each transaction is charged a fixed fee (10% from the amount of tokens sent).
+The contract deployer will get ownership and total token amount and he’ll be excluded from paying transaction fees moreover can decide whether to exclude or include any user from paying them.
+
+## Properties
+- **liquidity**: Senders with a positive amount of tokens can always send the amount minus the fee.
+- **owner-can-exclude-include-from-fee**: Owner can include or exclude everyone in the fee payment.
+- **owner-fee-after-transfer**: To respect the deflationary token property, after every transfer the owner balance must be increased by fees.
+- **ownership-cannot-change**: The initial owner of the contract defined during the constructor call, cannot change.
+- **total-supply-integrity**: After a transfer, the total amount of tokens is always the same.
+- **user-cannot-exclude-include-from-fee**: A generic user cannot include or exclude someone in fees payment.
+- **validate-transfer-diff-o-s-r**: If owner, sender and receiver have distinct addresses, their balances are updated correctly after the transfer of a positive amount of tokens: Owner balance is incremented by the fee, Sender balance is decremented by the amount and Receiver balance is incremented by the amount minus the fee.
+- **validate-transfer-same-o-r**: If only owner and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the amount, Sender balance is decremented by the amount and Receiver balance is the same as the owner balance.
+- **validate-transfer-same-o-s**: If only owner and sender have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is decremented by the amount minus the fee, Sender balance is the same as the owner balance and Receiver balance is incremented by the amount minus the fee.
+- **validate-transfer-same-o-s-r**: If the owner, sender and receiver have the same address, their balances remain unchanged after the transfer of a positive amount of token.
+- **validate-transfer-same-s-r**: If only sender and receiver have the same address, we check that their balances are updated correctly after the transfer of a positive amount of token: Owner balance is incremented by the fee, Sender balance is decremented by the fee and Receiver balance is the same as the sender balance.
+
+## Versions
+- **v1**: the transfer amount and fees are wrongly managed, the fees are not deducted from the sender but at the same time the owner receives the right fee amount (token duplication).
+- **v2**: the deflationary property is not well implemented, when we make a transfer with less than 10 tokens, no fees are charged.
+- **v3**: conforming to specification.
+
+## Ground truth
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | 1                                    | 1                                    | 0                                    | 1                                    | 0                                    | 1                                    | 0                                    | 0                                    | 0                                    | 0                                    | 0                                    |
+| **v2** | 1                                    | 1                                    | 0                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    |
+| **v3** | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    | 1                                    |
+
+
+## Experiments
+### SolCMC
+#### Z3
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN!                                  | ND                                   | TN                                   | TP!                                  | UNK                                  | UNK                                  | UNK                                  | UNK                                  | UNK                                  |
+| **v2** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | UNK                                  | TP!                                  | FN                                   | TP!                                  | UNK                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | ND                                   | UNK                                  | TP!                                  | UNK                                  | TP!                                  | UNK                                  | TP!                                  | UNK                                  |
+
+
+#### Eldarica
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | TN                                   | TN                                   | UNK                                  | UNK                                  | TN                                   |
+| **v2** | TP!                                  | TP!                                  | TN!                                  | ND                                   | UNK                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | ND                                   | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+
+
+
+### Certora
+|        | liquidity                            | owner-can-exclude-include-from-fee   | owner-fee-after-transfer             | ownership-cannot-change              | total-supply-integrity               | user-cannot-exclude-include-from-fee | validate-transfer-diff-o-s-r         | validate-transfer-same-o-r           | validate-transfer-same-o-s           | validate-transfer-same-o-s-r         | validate-transfer-same-s-r           |
+|--------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|--------------------------------------|
+| **v1** | TP!                                  | TP!                                  | TN                                   | TP!                                  | TN                                   | TP!                                  | TN                                   | TN                                   | TN                                   | TN                                   | TN                                   |
+| **v2** | TP!                                  | TP!                                  | TN                                   | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+| **v3** | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  | TP!                                  |
+
+

contracts/simplified_deflationary_token/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)
+

contracts/simplified_deflationary_token/certora/getters.sol

@@ -0,0 +1 @@
+

contracts/simplified_deflationary_token/certora/liquidity.spec

@@ -0,0 +1,40 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+}
+
+function balancesSum(env e, address owner, address receiver) returns mathint {
+    mathint balancesSum;
+    uint ownerBalance = 0;
+    uint receiverBalance = 0;
+
+    if(e.msg.sender != owner) {
+        ownerBalance = balanceOf(owner);
+    }
+    if(e.msg.sender != receiver && owner != receiver) {
+        receiverBalance = balanceOf(receiver);
+    }
+    balancesSum = balanceOf(e.msg.sender) + ownerBalance + receiverBalance;
+    return balancesSum;
+}
+
+rule liquidity {
+    env e;
+    address owner = currentContract.owner;
+    uint amount;
+    address receiver;
+
+    requireInvariant correctTransactionFeePercent();
+    requireInvariant correctTotalSupply();
+    require(balancesSum(e, owner, receiver) <= currentContract.totalSupply);
+    require(e.msg.value == 0);
+    require(amount <= balanceOf(e.msg.sender) && amount > 0);
+
+    bool isMoneyTransferred = transfer@withrevert(e, receiver, amount);
+    assert(!lastReverted);
+}
+
+invariant correctTransactionFeePercent()
+    currentContract.transactionFeePercent == 10;
+
+invariant correctTotalSupply()
+    currentContract.totalSupply == 1000000000000000000000000;

contracts/simplified_deflationary_token/certora/methods.spec

@@ -0,0 +1 @@
+

contracts/simplified_deflationary_token/certora/owner-can-exclude-include-from-fee.spec

@@ -0,0 +1,13 @@
+rule owner_can_exclude_include_from_fee {
+    env e;
+    address owner = currentContract.owner;
+    address account;
+
+    require(owner == e.msg.sender);
+    require(e.msg.value == 0);
+    require(currentContract.isExcludedFromFee[account] == false);
+    excludeFromFee@withrevert(e, account);
+    assert(currentContract.isExcludedFromFee[account] == true);
+    includeInFee@withrevert(e, account);
+    assert(currentContract.isExcludedFromFee[account] == false);
+}

contracts/simplified_deflationary_token/certora/owner-fee-after-transfer.spec

@@ -0,0 +1,19 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+    function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+
+rule owner_fee_after_transfer {
+    env e;
+    address owner = currentContract.owner;
+    address receiver;
+
+    uint256 amount;
+    require(amount > 0);
+    require(currentContract.isExcludedFromFee[e.msg.sender] == false);
+
+    uint256 fee = calculateFee(amount);
+
+    assert(fee > 0);
+}

contracts/simplified_deflationary_token/certora/ownership-cannot-change.spec

@@ -0,0 +1,24 @@
+methods {
+    function balanceOf(address account) external returns (uint256) envfree;
+    function calculateFee(uint256 amount) external returns (uint256) envfree;
+}
+
+hook Sstore SimplifiedDeflationaryToken.owner address hook_owner (address hook_old_owner) {
+    old_owner = hook_old_owner;
+}
+
+ghost address old_owner;
+
+rule ownership_cannot_change {
+    env e;
+    calldataarg args;
+
+    require(old_owner == currentContract.owner);
+
+    transfer@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+    excludeFromFee@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+    includeInFee@withrevert(e, args);
+    assert(old_owner == currentContract.owner);
+}