From 3fe7f722d986b1ed4e348614a26822750ea0acd0 Mon Sep 17 00:00:00 2001
From: Shoham Shamir <shoham@certora.com>
Date: Thu, 25 Apr 2024 13:16:50 +0300
Subject: [PATCH] extends and improves tracking sums pattern

---
 docs/user-guide/patterns/index.md |  2 +-
 docs/user-guide/patterns/sums.md  | 32 --------------
 docs/user-guide/patterns/sums.rst | 69 +++++++++++++++++++++++++++++++
 3 files changed, 70 insertions(+), 33 deletions(-)
 delete mode 100644 docs/user-guide/patterns/sums.md
 create mode 100644 docs/user-guide/patterns/sums.rst

diff --git a/docs/user-guide/patterns/index.md b/docs/user-guide/patterns/index.md
index d3da4e71..aa464bf1 100644
--- a/docs/user-guide/patterns/index.md
+++ b/docs/user-guide/patterns/index.md
@@ -5,7 +5,7 @@ Certain patterns often occur in specification files.  This chapter describes
 some of these patterns.
 
 ```{toctree}
-sums.md
+sums.rst
 partial-apply.md
 safe-assum.md
 require-invariants.md
diff --git a/docs/user-guide/patterns/sums.md b/docs/user-guide/patterns/sums.md
deleted file mode 100644
index c573c754..00000000
--- a/docs/user-guide/patterns/sums.md
+++ /dev/null
@@ -1,32 +0,0 @@
-# Tracking Sums
-
-## Enforcing Sum of Two Balances Constraint
-```cvl
-invariant directSumOfTwo(address a, address b)
-    (a != b) => (balanceOf(a) + balanceOf(b) <= to_mathint(totalSupply()));
-```
-
-Ensure that the sum of balances for any two distinct addresses, `a` and `b`, does not exceed 
-the total supply.
-
-## Maintaining Equality Between Sum of Balances and Total Supply
-```cvl
-ghost mathint sumBalances {
-    init_state axiom sumBalances == 0;
-}
-
-hook Sstore balanceOf[KEY address user] uint256 newBalance (uint256 oldBalance)
-{
-    // there is no `+=` operator in CVL
-    sumBalances = sumBalances + newBalance - oldBalance;
-}
-
-invariant totalIsSumBalances()
-    to_mathint(totalSupply()) == sumBalances;
-```
-
-Track the sum of all balances and ensure that it remains equal to the total supply. The 
-`sumBalances` ghost variable is updated with changes in individual balances using a storage 
-hook, ensuring accuracy and consistency in the overall sum.
-
-for more information about the example checkout [this tutorial](https://docs.certora.com/projects/tutorials/en/latest/lesson4_invariants/ghosts/sum_two.html#lesson4-ghost-sum-balances).
diff --git a/docs/user-guide/patterns/sums.rst b/docs/user-guide/patterns/sums.rst
new file mode 100644
index 00000000..f8e5fe9e
--- /dev/null
+++ b/docs/user-guide/patterns/sums.rst
@@ -0,0 +1,69 @@
+.. index::
+   single: sums
+
+Tracking Sums
+=============
+
+This section deals with tracking sums of values. The quintessential example for
+needing to track sums is from ERC-20 contracts, where :solidity:`totalSupply()`
+must be the sum of all balances. This is the example we shall use here,
+namely the :clink:`ERC20</DEFI/ERC20/contracts/ERC20.sol>` contract from the
+:clink:`Examples</>` repository.
+
+
+Trying to verify the sum of two balances
+----------------------------------------
+Often one needs a invariant like :cvl:`sumOfTwo` below:
+
+.. code-block:: cvl
+
+   invariant sumOfTwo(address a, address b)
+       (a != b) => (balanceOf(a) + balanceOf(b) <= to_mathint(totalSupply()));
+
+If we run this invariant, the Prover will find a violations.
+An example of such a violation is summarized in the table below.
+In this example the function called was :cvl:`tranferFrom(c, a, 2)`,
+where :solidity:`c` is an address different from :solidity:`a` and :solidity:`b`.
+
+.. list-table:: Counter example
+   :header-rows: 1
+   :align: center
+
+   * -
+     - Before :cvl:`tranferFrom`
+     - After
+
+   * - :cvl:`balanceOf(a)`
+     - 1
+     - 3
+
+   * - :cvl:`balanceOf(b)`
+     - 2
+     - 2
+
+   * - :cvl:`balanceOf(c)`
+     - 3
+     - 1
+
+   * - :cvl:`totalSupply()`
+     - 3
+     - 3
+
+   * - :cvl:`sumOfTwo(a, b)`
+     - **true** (3 >= 1+2)
+     - **false** (3 < 3+2)
+
+We see that the Prover cannot verify :cvl:`sumOfTwo` invariant without us adding unsound
+assumptions. So instead, we shall prove a stronger property, as explained next.
+
+
+Equality of sum of balances and total supply
+--------------------------------------------
+The preferred solution to tracking sums is using a hook and a ghost, as shown below.
+
+.. cvlinclude:: ../../../Examples/DEFI/ERC20/certora/specs/ERC20Fixed.spec
+   :lines: 98-106, 115-116
+   :caption: :clink:`Total supply is sum of balances</DEFI/ERC20/certora/specs/ERC20Fixed.spec>`
+
+Once this invariant is proved, we can require properties like the one in
+:cvl:`sumOfTwo` above.