cpp mini example for demo

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "DEFI/CPP_mini/lib/forge-std"]
+	path = DEFI/CPP_mini/lib/forge-std
+	url = [email protected]:foundry-rs/forge-std.git

DEFI/CPP_mini/README.md

@@ -0,0 +1,42 @@
+## Mini Constant Product Pool
+
+The following system is based on a simplified version of the Trident bug that was found by the Certora Prover.
+You can find a brief explanation about the original system and bug here:
+https://medium.com/certora/exploiting-an-invariant-break-how-we-found-a-pool-draining-bug-in-sushiswaps-trident-585bd98a4d4f 
+
+
+In constant-product pools, liquidity providers (LPs) deposit two types of underlying tokens (Token0 and Token1) in exchange for LP tokens. 
+They can later burn LP tokens to reclaim a proportional amount of Token0 and Token1.
+Trident users can swap one underlying token for the other by transferring some tokens of one type to the pool and receiving some number of the other token.
+To determine the exchange rate, the pool returns enough tokens to ensure that
+(reserves0 ⋅ reserves1)ᵖʳᵉ =(reserves0 ⋅ reserves1)ᵖᵒˢᵗ
+where reserves0 and reserves1 are the amount of token0 and token1 the system holds. 
+
+On first liquidity deposit, the system transfers 1000 LP tokens to address 0 to ensure the pool cannot be emptied.  
+
+An important property is that if there are liquidity providers (totalSupply >0) than there must be assets in both tokens. 
+This property is written in CVL and in foundry as invariant. 
+### Fuzz test
+
+To run the fuzz test from the CPP_mini folder:
+```
+forge coverage --report lcov --report-file fuzz --match-contract CPPMini
+genhtml fuzz -o fuzzcov
+open fuzzcov/index.html
+```
+Coverage is very good - 96.3%, however the bug is missed.
+
+The bug is demonstrated in a manual crafted test `test_manual()` and shows how it can cause a complete drain of the protocol.
+
+
+### Formal verification 
+To run the verification:
+```certoraRun certora/conf/runBroken.conf```
+
+As seen in the report, the property is violated: https://prover.certora.com/output/40726/4ba34bd0d7d54c279c7cb261d1616fef/?anonymousKey=626461dda2213599b57007646d3198b21c249908
+
+
+Once the bug is fixed the property is verified:
+```certoraRun certora/conf/runFixed.conf```
+
+https://prover.certora.com/output/40726/a90ecf39cd7a44d59b30ff8a6172e8ff/?anonymousKey=cac7192076ce98c8465b939d2ac2001385a484ff

DEFI/CPP_mini/certora/conf/runBroken.conf

@@ -0,0 +1,16 @@
+{
+  // files that are part of the scene (everything the Certora Prover can reason about)
+  "files": [
+    "src/ConstantProductPoolMini.sol:ConstantProductPool",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol"
+  ],
+  // the main contract under test and the spec file 
+  "verify": "ConstantProductPool:certora/spec/CPPMini.spec",
+  // After unrolling loops, assume the loop halt conditions hold: https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops 
+  "optimistic_loop": true,
+  // msg to recognize this run (presented in your list of jobs under prover.certora.com)
+  "msg": "ConstantProductPool with bugs",
+  // Check the rule is non-vacuous
+  "rule_sanity": "basic"
+}

DEFI/CPP_mini/certora/conf/runFixed.conf

@@ -0,0 +1,16 @@
+{
+  // files that are part of the scene (everything the Certora Prover can reason about)
+  "files": [
+    "src/ConstantProductPoolMiniFixed.sol:ConstantProductPool",
+    "certora/helpers/DummyERC20A.sol",
+    "certora/helpers/DummyERC20B.sol"
+  ],
+  // the main contract under test and the spec file 
+  "verify": "ConstantProductPool:certora/spec/CPPMini.spec",
+  // After unrolling loops, assume the loop halt conditions hold: https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops 
+  "optimistic_loop": true,
+  // msg to recognize this run (presented in your list of jobs under prover.certora.com)
+  "msg": "ConstantProductPool Fixed",
+  // Check the rule is non-vacuous
+  "rule_sanity": "basic"
+}

DEFI/CPP_mini/certora/helpers/DummyERC20A.sol

@@ -0,0 +1,14 @@
+// Represents a symbolic/dummy ERC20 token
+
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+import "../../src/ERC20.sol";
+
+contract DummyERC20A is ERC20 {
+
+    string public name = "ERC20A";
+    function mint(address account, uint256 amount) external  {
+        _mint(account,amount);
+    }
+}

DEFI/CPP_mini/certora/helpers/DummyERC20B.sol

@@ -0,0 +1,13 @@
+// Represents a symbolic/dummy ERC20 token
+
+// SPDX-License-Identifier: agpl-3.0
+pragma solidity ^0.8.0;
+
+import "../../src/ERC20.sol";
+
+contract DummyERC20B is ERC20 {
+    string public name = "ERC20B";
+    function mint(address account, uint256 amount) external  {
+        _mint(account,amount);
+    } 
+}

DEFI/CPP_mini/certora/spec/CPPMini.spec

@@ -0,0 +1,108 @@
+/***
+This example demonstrate a critical bug found with the Certora Prover 
+***/
+
+// reference from the spec to additional contracts used in the verification 
+using DummyERC20A as _token0;
+using DummyERC20B as _token1;
+using ConstantProductPool as _pool;
+
+
+/*
+    Declaration of methods that are used in the rules. `envfree` indicates that
+    the method is not dependent on the environment (`msg.value`, `msg.sender`).
+    Methods that are not declared here are assumed to be dependent on the
+    environment.
+*/
+
+methods{
+    function token0() external returns (address) envfree;
+    function token1() external returns (address) envfree;
+    function allowance(address,address) external returns (uint256) envfree;
+    function totalSupply() external returns (uint256)  envfree;
+
+    function DummyERC20A.balanceOf(address) external returns (uint256)  envfree; 
+    function DummyERC20B.balanceOf(address) external returns (uint256)  envfree; 
+    function DummyERC20A.allowance(address,address) external returns (uint256)  envfree; 
+    function DummyERC20B.allowance(address,address) external returns (uint256)  envfree; 
+    //external calls to be resolved by dispatcher - taking into account all available implementations 
+    function _.transfer(address recipient, uint256 amount) external => DISPATCHER(true);
+    function _.balanceOf(address) external => DISPATCHER(true);
+    // mathematical summary
+    function Math.sqrt(uint256 y) internal returns (uint256) => floorSqrt(y);
+
+}
+
+
+// A precise summarization of sqrt
+ghost floorSqrt(uint256) returns uint256 {    
+                // sqrt(x)^2 <= x
+    axiom forall uint256 x. floorSqrt(x)*floorSqrt(x) <= to_mathint(x) && 
+                // sqrt(x+1)^2 > x 
+                (floorSqrt(x) + 1)*(floorSqrt(x) + 1) > to_mathint(x);
+}
+
+// a cvl function for precondition assumptions 
+function setup(env e){
+    address zero_address = 0;
+    uint256 MINIMUM_LIQUIDITY = 1000;
+    require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY;
+    require currentContract._balances[zero_address] + currentContract._balances[e.msg.sender] <= totalSupply();
+    require _token0 == token0();
+    require _token1 == token1();
+    require e.msg.sender != currentContract;
+}
+
+invariant allowanceOfPoolAlwaysZero(address a)
+    _token0.allowance(_pool, a) == 0 && _token1.allowance(_pool, a) == 0
+    {
+        preserved with (env e){
+         setup(e);
+        }
+    }
+
+
+/*
+Property: For both token0 and token1 the balance of the system is at least as much as the reserves.
+
+This property is implemented as an invariant. 
+Invariants are defined as a specification of a condition that should always be true once an operation is concluded.
+In addition, the invariant also checks that it holds immediately after the constructor of the code runs.
+
+*/
+
+invariant balanceGreaterThanReserve()
+    (currentContract.reserve0 <= _token0.balanceOf(currentContract))&&
+    (currentContract.reserve1 <= _token1.balanceOf(currentContract))
+    {
+        preserved with (env e){
+         setup(e);
+         requireInvariant allowanceOfPoolAlwaysZero(e.msg.sender);
+        }
+
+
+    }
+
+
+/*
+Property: Integrity of totalSupply with respect to the amount of reserves. 
+
+This is a high level property of the system - the ability to pay back liquidity providers.
+If there are any LP tokens (the totalSupply is greater than 0), then neither reserves0 nor reserves1 should ever be zero (otherwise the pool could not produce the underlying tokens).
+
+This invariant catches the original bug in Trident where the amount to receive is computed as a function of the balances and not the reserves.
+
+Formula:
+    (totalSupply() == 0 <=> getReserve0() == 0 <=> getReserve1() == 0)
+*/
+
+invariant integrityOfTotalSupply()
+
+    (totalSupply() == 0 <=> currentContract.reserve0 == 0) &&
+    (totalSupply() == 0 <=> currentContract.reserve1 == 0)
+    {
+        preserved with (env e){
+            requireInvariant balanceGreaterThanReserve();
+            setup(e);
+        }
+    }

DEFI/CPP_mini/foundry.toml

@@ -0,0 +1,8 @@
+[profile.default]
+src = "src"
+out = "out"
+libs = ["lib"]
+[fuzz]
+runs = 10000
+
+# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options