From a9e0ee16315d6930b8075aa8da9eb3da02c169a7 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 13 Feb 2024 14:35:35 +0100 Subject: [PATCH] docs: broken link in README --- certora/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/README.md b/certora/README.md index 396019f..af6bfbe 100644 --- a/certora/README.md +++ b/certora/README.md @@ -19,7 +19,7 @@ The certificate is assumed to contain the submitted root to verify, a total amou Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants: -- it is checked in [MerkleTrees.spec](specs/MerkleTrees.spec) that those functions lead to creating well-formed trees. +- it is checked in [MerkleTree.spec](specs/MerkleTree.spec) that those functions lead to creating well-formed trees. Well-formed trees also verify that the value of their internal node is the sum of the rewards it contains. - it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.