From 73601afdbb9416ed1d8b873996db6981359d4043 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Jul 2024 12:25:49 +0200 Subject: [PATCH 01/23] refactor: use address 0 as the head and tail of the list --- src/DoubleLinkedList.sol | 53 ++++++++------------------------- test/TestDoubleLinkedList.t.sol | 2 +- 2 files changed, 13 insertions(+), 42 deletions(-) diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index ef931a3..7a988d4 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -16,8 +16,6 @@ library DoubleLinkedList { struct List { mapping(address => Account) accounts; - address head; - address tail; } /* ERRORS */ @@ -48,14 +46,14 @@ library DoubleLinkedList { /// @param list The list to get the head. /// @return The address of the head. function getHead(List storage list) internal view returns (address) { - return list.head; + return list.accounts[address(0)].next; } /// @notice Returns the address at the tail of the `list`. /// @param list The list to get the tail. /// @return The address of the tail. function getTail(List storage list) internal view returns (address) { - return list.tail; + return list.accounts[address(0)].prev; } /// @notice Returns the next id address from the current `id`. @@ -79,12 +77,11 @@ library DoubleLinkedList { /// @param id The address of the account. function remove(List storage list, address id) internal { Account memory account = list.accounts[id]; + if (id == address(0)) revert AddressIsZero(); if (account.value == 0) revert AccountDoesNotExist(); - if (account.prev != address(0)) list.accounts[account.prev].next = account.next; - else list.head = account.next; - if (account.next != address(0)) list.accounts[account.next].prev = account.prev; - else list.tail = account.prev; + list.accounts[account.prev].next = account.next; + list.accounts[account.next].prev = account.prev; delete list.accounts[id]; } @@ -100,7 +97,7 @@ library DoubleLinkedList { if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); uint256 numberOfIterations; - address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { next = list.accounts[next].next; @@ -109,37 +106,11 @@ library DoubleLinkedList { } } - // Account is not the new tail. - if (numberOfIterations < maxIterations && next != address(0)) { - // Account is the new head. - if (next == list.head) { - list.accounts[id] = Account({prev: address(0), next: next, value: value}); - list.head = id; - list.accounts[next].prev = id; - } - // Account is not the new head. - else { - address prev = list.accounts[next].prev; - list.accounts[id] = Account({prev: prev, next: next, value: value}); - list.accounts[prev].next = id; - list.accounts[next].prev = id; - } - } - // Account is the new tail. - else { - // Account is the new head. - if (list.head == address(0)) { - list.accounts[id] = Account({prev: address(0), next: address(0), value: value}); - list.head = id; - list.tail = id; - } - // Account is not the new head. - else { - address tail = list.tail; - list.accounts[id] = Account({prev: tail, next: address(0), value: value}); - list.accounts[tail].next = id; - list.tail = id; - } - } + if (numberOfIterations == maxIterations) next = address(0); + + address prev = list.accounts[next].prev; + list.accounts[id] = Account(prev, next, value); + list.accounts[prev].next = id; + list.accounts[next].prev = id; } } diff --git a/test/TestDoubleLinkedList.t.sol b/test/TestDoubleLinkedList.t.sol index f746022..9457d8a 100644 --- a/test/TestDoubleLinkedList.t.sol +++ b/test/TestDoubleLinkedList.t.sol @@ -11,7 +11,7 @@ contract TestDoubleLinkedList is Test { address[] public accounts; address public ADDR_ZERO = address(0); - DoubleLinkedList.List public list; + DoubleLinkedList.List internal list; function setUp() public { accounts = new address[](NDS); From e3863d50ff4558748423657f319d7ac855e5466d Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Jul 2024 12:40:44 +0200 Subject: [PATCH 02/23] chore: adapt munging --- certora/applyHarnessFifo.patch | 26 +++++++++++++------------- certora/applyHarnessSimple.patch | 29 +++++++++++++---------------- 2 files changed, 26 insertions(+), 29 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 7a35618..f004fac 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,19 +1,19 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200 -+++ DoubleLinkedList.sol 2023-05-23 16:44:01.777091764 +0200 -@@ -18,6 +18,8 @@ +--- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 ++++ DoubleLinkedList.sol 2024-07-10 12:38:54.711124189 +0200 +@@ -16,6 +16,8 @@ + + struct List { mapping(address => Account) accounts; - address head; - address tail; + address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion. + address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion. } /* ERRORS */ -@@ -101,14 +103,18 @@ +@@ -98,8 +100,10 @@ uint256 numberOfIterations; - address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + list.insertedAfter = address(0); // HARNESS while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { @@ -21,17 +21,17 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol next = list.accounts[next].next; unchecked { ++numberOfIterations; - } +@@ -107,6 +111,7 @@ } + if (numberOfIterations == maxIterations) next = address(0); + list.insertedBefore = next; // HARNESS -+ - // Account is not the new tail. - if (numberOfIterations < maxIterations && next != address(0)) { - // Account is the new head. + + address prev = list.accounts[next].prev; + list.accounts[id] = Account(prev, next, value); diff -ruN MockDLL.sol MockDLL.sol --- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2023-05-23 16:42:32.913885637 +0200 ++++ MockDLL.sol 2024-07-10 12:36:30.235182781 +0200 @@ -0,0 +1,111 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index 9fb9d16..1abeb16 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,16 +1,16 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2023-05-23 16:01:50.888803463 +0200 -+++ DoubleLinkedList.sol 2023-05-23 16:34:10.324900474 +0200 -@@ -18,6 +18,8 @@ +--- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 ++++ DoubleLinkedList.sol 2024-07-10 12:34:45.178218509 +0200 +@@ -16,6 +16,8 @@ + + struct List { mapping(address => Account) accounts; - address head; - address tail; + address insertedBefore; // HARNESS: address of the account before which the account was inserted at last insertion. + address insertedAfter; // HARNESS: address of the account after which the account was inserted at last insertion. } /* ERRORS */ -@@ -93,24 +95,23 @@ +@@ -90,23 +92,20 @@ /// @param list The list to search in. /// @param id The address of the account. /// @param value The value of the account. @@ -22,9 +22,9 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - uint256 numberOfIterations; -- address next = list.head; // If not added at the end of the list `id` will be inserted before `next`. +- address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + list.insertedAfter = address(0); -+ address next = list.head; // `id` will be inserted before `next`. ++ address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + while (next != address(0) && list.accounts[next].value >= value) { @@ -35,17 +35,14 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol - } } +- if (numberOfIterations == maxIterations) next = address(0); + list.insertedBefore = next; -+ - // Account is not the new tail. -- if (numberOfIterations < maxIterations && next != address(0)) { -+ if (next != address(0)) { - // Account is the new head. - if (next == list.head) { - list.accounts[id] = Account({prev: address(0), next: next, value: value}); + + address prev = list.accounts[next].prev; + list.accounts[id] = Account(prev, next, value); diff -ruN MockDLL.sol MockDLL.sol --- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2023-05-23 16:16:00.233326262 +0200 ++++ MockDLL.sol 2024-07-10 12:26:25.130305388 +0200 @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; From 52aa3c530d0e3c0cd3b6e4c55125de2cee8da299 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 10 Jul 2024 19:20:45 +0200 Subject: [PATCH 03/23] fix: simple dll verif, missing linkedToZero --- certora/confs/DllSimple.conf | 2 +- certora/specs/DllSimple.spec | 72 +++++++++++++++++++++--------------- 2 files changed, 43 insertions(+), 31 deletions(-) diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index 1477691..d04826d 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -4,7 +4,7 @@ ], "solc": "solc-0.8.17", "verify": "MockDLL:certora/specs/DllSimple.spec", - "loop_iter": "7", + "loop_iter": "2", "optimistic_loop": true, "rule_sanity": "basic", "server": "production", diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index 07ba5cd..57c08f0 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -20,13 +20,16 @@ definition isInDLL(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = - getPrev(id) != 0 || getNext(id) != 0; + id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); -definition isEmpty(address id) returns bool = - ! isInDLL(id) && ! isLinked(id); +definition isLinkedToZero(address id) returns bool = + isLinked(id) => + (getNext(id) == 0 => getPrev(0) == id) && + (getPrev(id) == 0 => getNext(0) == id); definition isTwoWayLinked(address first, address second) returns bool = - first != 0 && second != 0 => (getNext(first) == second <=> getPrev(second) == first); + (first != 0 => getPrev(second) == first => getNext(first) == second) && + (second != 0 => getNext(first) == second => getPrev(second) == first); definition isHeadWellFormed() returns bool = getPrev(getHead()) == 0 && (getHead() != 0 => isInDLL(getHead())); @@ -41,7 +44,6 @@ definition hasNoNextIsTail(address addr) returns bool = isInDLL(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { - requireInvariant zeroEmpty(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); requireInvariant tipsZero(); @@ -52,50 +54,59 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). -invariant zeroEmpty() - isEmpty(0) +invariant linkedToZero(address addr) + isLinkedToZero(addr) + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant twoWayLinked(0, id); + requireInvariant twoWayLinked(id, 0); + } + } + +invariant headWellFormed() + isHeadWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedIsInDLL(getNext(id)); + requireInvariant linkedToZero(id); + } + } + +rule headWellFormedPreservedInsertSorted(address id, uint256 value) { + address prev; address next; -rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { - address prev; + require isHeadWellFormed(); - require isEmpty(0); + requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant noNextIsTail(prev); insertSorted(id, value); require prev == getInsertedAfter(); + require next == getInsertedBefore(); - assert isEmpty(0); + assert isHeadWellFormed(); } -invariant headWellFormed() - isHeadWellFormed() - { preserved remove(address id) { - requireInvariant zeroEmpty(); - requireInvariant twoWayLinked(getPrev(id), id); - requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getNext(id)); - } - } - invariant tailWellFormed() isTailWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant linkedIsInDLL(getPrev(id)); + requireInvariant linkedToZero(id); } } rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { - address next; address prev; + address prev; address next; require isTailWellFormed(); - requireInvariant zeroEmpty(); + requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -110,7 +121,6 @@ rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { invariant tipsZero() getTail() == 0 <=> getHead() == 0 { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant noNextIsTail(id); requireInvariant noPrevIsHead(id); } @@ -128,7 +138,7 @@ invariant noPrevIsHead(address addr) } rule noPrevIsHeadPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoPrevIsHead(addr); @@ -157,7 +167,7 @@ invariant noNextIsTail(address addr) } rule noNextisTailPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoNextIsTail(addr); @@ -185,7 +195,7 @@ invariant linkedIsInDLL(address addr) } rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require isLinked(addr) => isInDLL(addr); require isLinked(getPrev(next)) => isInDLL(getPrev(next)); @@ -215,16 +225,18 @@ invariant twoWayLinked(address first, address second) } rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { - address first; address second; address next; + address first; address second; address prev; address next; require isTwoWayLinked(first, second); require isTwoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); safeAssumptions(); requireInvariant linkedIsInDLL(id); insertSorted(id, value); + require prev == getInsertedAfter(); require next == getInsertedBefore(); assert isTwoWayLinked(first, second); From 55e0838a642b202160c6bf66a08611b06e21ef24 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 10:54:52 +0200 Subject: [PATCH 04/23] fix: finish DllSimple proof --- certora/confs/DllSimple.conf | 2 +- certora/specs/DllSimple.spec | 92 ++++++++++++++++++++++++++++-------- 2 files changed, 72 insertions(+), 22 deletions(-) diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index d04826d..1477691 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -4,7 +4,7 @@ ], "solc": "solc-0.8.17", "verify": "MockDLL:certora/specs/DllSimple.spec", - "loop_iter": "2", + "loop_iter": "7", "optimistic_loop": true, "rule_sanity": "basic", "server": "production", diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index 57c08f0..972b9ee 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -16,7 +16,7 @@ methods { // DEFINITIONS -definition isInDLL(address id) returns bool = +definition isInDll(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = @@ -32,16 +32,16 @@ definition isTwoWayLinked(address first, address second) returns bool = (second != 0 => getNext(first) == second => getPrev(second) == first); definition isHeadWellFormed() returns bool = - getPrev(getHead()) == 0 && (getHead() != 0 => isInDLL(getHead())); + getPrev(getHead()) == 0 && (getHead() != 0 => isInDll(getHead())); definition isTailWellFormed() returns bool = - getNext(getTail()) == 0 && (getTail() != 0 => isInDLL(getTail())); + getNext(getTail()) == 0 && (getTail() != 0 => isInDll(getTail())); definition hasNoPrevIsHead(address addr) returns bool = - isInDLL(addr) && getPrev(addr) == 0 => addr == getHead(); + isInDll(addr) && getPrev(addr) == 0 => addr == getHead(); definition hasNoNextIsTail(address addr) returns bool = - isInDLL(addr) && getNext(addr) == 0 => addr == getTail(); + isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { requireInvariant headWellFormed(); @@ -56,21 +56,42 @@ function safeAssumptions() { invariant linkedToZero(address addr) isLinkedToZero(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant twoWayLinked(0, id); requireInvariant twoWayLinked(id, 0); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); } } +rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isLinkedToZero(addr); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isLinkedToZero(addr); +} + invariant headWellFormed() isHeadWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getNext(id)); + requireInvariant linkedIsInDll(getNext(id)); requireInvariant linkedToZero(id); } } @@ -97,7 +118,7 @@ invariant tailWellFormed() { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getPrev(id)); + requireInvariant linkedIsInDll(getPrev(id)); requireInvariant linkedToZero(id); } } @@ -184,8 +205,37 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { assert hasNoNextIsTail(addr); } -invariant linkedIsInDLL(address addr) - isLinked(addr) => isInDLL(addr) +invariant inDllIsLinked(address addr) + isInDll(addr) => isLinked(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isInDll(addr) => isLinked(addr); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isInDll(addr) => isLinked(addr); +} + +invariant linkedIsInDll(address addr) + isLinked(addr) => isInDll(addr) filtered { f -> f.selector != sig:insertSorted(address,uint256).selector } { preserved remove(address id) { safeAssumptions(); @@ -197,8 +247,8 @@ invariant linkedIsInDLL(address addr) rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { address addr; address prev; address next; - require isLinked(addr) => isInDLL(addr); - require isLinked(getPrev(next)) => isInDLL(getPrev(next)); + require isLinked(addr) => isInDll(addr); + require isLinked(getPrev(next)) => isInDll(getPrev(next)); safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); @@ -211,7 +261,7 @@ rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); require next == getInsertedBefore(); - assert isLinked(addr) => isInDLL(addr); + assert isLinked(addr) => isInDll(addr); } invariant twoWayLinked(address first, address second) @@ -232,7 +282,7 @@ rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { requireInvariant twoWayLinked(prev, getNext(prev)); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value); @@ -243,14 +293,14 @@ rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { } invariant forwardLinked(address addr) - isInDLL(addr) => isForwardLinkedBetween(getHead(), addr) + isInDll(addr) => isForwardLinkedBetween(getHead(), addr) filtered { f -> f.selector != sig:remove(address).selector && f.selector != sig:insertSorted(address, uint256).selector } rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { address addr; address prev; - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -260,7 +310,7 @@ rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule forwardLinkedPreservedRemove(address id) { @@ -268,7 +318,7 @@ rule forwardLinkedPreservedRemove(address id) { require prev == getPreceding(id); - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant noPrevIsHead(id); @@ -278,7 +328,7 @@ rule forwardLinkedPreservedRemove(address id) { remove(id); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule removeRemoves(address id) { @@ -286,7 +336,7 @@ rule removeRemoves(address id) { remove(id); - assert !isInDLL(id); + assert !isInDll(id); } rule insertSortedInserts(address id, uint256 value) { @@ -294,7 +344,7 @@ rule insertSortedInserts(address id, uint256 value) { insertSorted(id, value); - assert isInDLL(id); + assert isInDll(id); } invariant decrSorted() @@ -310,7 +360,7 @@ invariant decrSorted() // result: isForwardLinkedBetween(getHead(), getTail()) // explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows -// otherwise, from tailWellFormed(), we know that isInDLL(getTail()) so the result follows from forwardLinked(getTail()). +// otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). // result: forall addr. isForwardLinkedBetween(addr, getTail()) // explanation: it can be obtained from the previous result and forwardLinked. From 33465a457b3ff00feec92d6e2f2e3260336960fd Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 11:09:19 +0200 Subject: [PATCH 05/23] fix: derived results --- certora/specs/DllSimple.spec | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index 972b9ee..d0dcdca 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -359,10 +359,10 @@ invariant decrSorted() // DERIVED RESULTS // result: isForwardLinkedBetween(getHead(), getTail()) -// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows -// otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). +// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows. +// Otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). -// result: forall addr. isForwardLinkedBetween(addr, getTail()) +// result: forall addr. isInDll(addr) => isForwardLinkedBetween(addr, getTail()) // explanation: it can be obtained from the previous result and forwardLinked. // Going from head to tail should lead to addr in between (otherwise addr is never reached because there is nothing after the tail). @@ -373,6 +373,5 @@ invariant decrSorted() // explanation: it comes from the fact that every non zero address that is in the DLL is linked to getHead(). // result: there are no cycles that do not contain the 0 address -// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() -// is part of the cycle. This is absurd because we know from headWellFormed() that the previous element of -// getHead() is the 0 address. +// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() is part of the cycle. +// The result follows because we know from headWellFormed() that the previous element of getHead() is the 0 address. From f085b623b8f965d9acbbb2382a3fbf208dee4ec2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 11:13:11 +0200 Subject: [PATCH 06/23] chore: import small modifications from DllSimple --- certora/specs/DllFifo.spec | 73 +++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 37 deletions(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index 6f81c7c..56141bc 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -20,29 +20,29 @@ methods { // DEFINITIONS -definition isInDLL(address id) returns bool = +definition isInDll(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = getPrev(id) != 0 || getNext(id) != 0; definition isEmpty(address id) returns bool = - ! isInDLL(id) && ! isLinked(id); + ! isInDll(id) && ! isLinked(id); definition isTwoWayLinked(address first, address second) returns bool = first != 0 && second != 0 => (getNext(first) == second <=> getPrev(second) == first); definition isHeadWellFormed() returns bool = - getPrev(getHead()) == 0 && (getHead() != 0 => isInDLL(getHead())); + getPrev(getHead()) == 0 && (getHead() != 0 => isInDll(getHead())); definition isTailWellFormed() returns bool = - getNext(getTail()) == 0 && (getTail() != 0 => isInDLL(getTail())); + getNext(getTail()) == 0 && (getTail() != 0 => isInDll(getTail())); definition hasNoPrevIsHead(address addr) returns bool = - isInDLL(addr) && getPrev(addr) == 0 => addr == getHead(); + isInDll(addr) && getPrev(addr) == 0 => addr == getHead(); definition hasNoNextIsTail(address addr) returns bool = - isInDLL(addr) && getNext(addr) == 0 => addr == getTail(); + isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { requireInvariant zeroEmpty(); @@ -82,7 +82,7 @@ invariant headWellFormed() requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getNext(id)); + requireInvariant linkedIsInDll(getNext(id)); } } @@ -93,12 +93,12 @@ invariant tailWellFormed() requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); - requireInvariant linkedIsInDLL(getPrev(id)); + requireInvariant linkedIsInDll(getPrev(id)); } } rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { - address next; address prev; + address prev; address next; require isTailWellFormed(); @@ -135,7 +135,7 @@ invariant noPrevIsHead(address addr) } rule noPrevIsHeadPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoPrevIsHead(addr); @@ -164,7 +164,7 @@ invariant noNextIsTail(address addr) } rule noNextisTailPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; require hasNoNextIsTail(addr); @@ -181,8 +181,8 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { assert hasNoNextIsTail(addr); } -invariant linkedIsInDLL(address addr) - isLinked(addr) => isInDLL(addr) +invariant linkedIsInDll(address addr) + isLinked(addr) => isInDll(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { safeAssumptions(); @@ -192,10 +192,10 @@ invariant linkedIsInDLL(address addr) } rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { - address addr; address next; address prev; + address addr; address prev; address next; - require isLinked(addr) => isInDLL(addr); - require isLinked(getPrev(next)) => isInDLL(getPrev(next)); + require isLinked(addr) => isInDll(addr); + require isLinked(getPrev(next)) => isInDll(getPrev(next)); safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); @@ -208,7 +208,7 @@ rule linkedIsInDllPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); require next == getInsertedBefore(); - assert isLinked(addr) => isInDLL(addr); + assert isLinked(addr) => isInDll(addr); } invariant twoWayLinked(address first, address second) @@ -228,7 +228,7 @@ rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { require isTwoWayLinked(getPrev(next), next); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value, maxIterations()); @@ -238,18 +238,18 @@ rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { } invariant forwardLinked(address addr) - isInDLL(addr) => isForwardLinkedBetween(getHead(), addr) + isInDll(addr) => isForwardLinkedBetween(getHead(), addr) filtered { f -> f.selector != sig:remove(address).selector && f.selector != sig:insertSorted(address, uint256, uint256).selector } rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { address addr; address prev; - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); - require isInDLL(getTail()) => isForwardLinkedBetween(getHead(), getTail()); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(getTail()) => isForwardLinkedBetween(getHead(), getTail()); safeAssumptions(); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); requireInvariant twoWayLinked(prev, getNext(prev)); requireInvariant noNextIsTail(prev); @@ -257,7 +257,7 @@ rule forwardLinkedPreservedInsertSorted(address id, uint256 value) { require prev == getInsertedAfter(); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule forwardLinkedPreservedRemove(address id) { @@ -265,7 +265,7 @@ rule forwardLinkedPreservedRemove(address id) { require prev == getPreceding(id); - require isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + require isInDll(addr) => isForwardLinkedBetween(getHead(), addr); safeAssumptions(); requireInvariant noPrevIsHead(id); @@ -275,7 +275,7 @@ rule forwardLinkedPreservedRemove(address id) { remove(id); - assert isInDLL(addr) => isForwardLinkedBetween(getHead(), addr); + assert isInDll(addr) => isForwardLinkedBetween(getHead(), addr); } rule removeRemoves(address id) { @@ -283,7 +283,7 @@ rule removeRemoves(address id) { remove(id); - assert !isInDLL(id); + assert !isInDll(id); } rule insertSortedInserts(address id, uint256 value) { @@ -291,7 +291,7 @@ rule insertSortedInserts(address id, uint256 value) { insertSorted(id, value, maxIterations()); - assert isInDLL(id); + assert isInDll(id); } rule insertSortedDecreasingOrder(address id, uint256 value) { @@ -301,25 +301,25 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { safeAssumptions(); requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant linkedIsInDLL(id); + requireInvariant linkedIsInDll(id); insertSorted(id, value, maxIter); require prev == getInsertedAfter(); - uint256 positionInDLL = lenUpTo(id); + uint256 positionInDll = lenUpTo(id); - assert positionInDLL > maxIter => greaterThanUpTo(value, 0, maxIter) && id == getTail(); - assert positionInDLL <= maxIter => greaterThanUpTo(value, id, getLength()) && value > getValueOf(getNext(id)); + assert positionInDll > maxIter => greaterThanUpTo(value, 0, maxIter) && id == getTail(); + assert positionInDll <= maxIter => greaterThanUpTo(value, id, getLength()) && value > getValueOf(getNext(id)); } // DERIVED RESULTS // result: isForwardLinkedBetween(getHead(), getTail()) -// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows -// otherwise, from tailWellFormed(), we know that isInDLL(getTail()) so the result follows from forwardLinked(getTail()). +// explanation: if getTail() == 0, then from tipsZero() we know that getHead() == 0 so the result follows. +// Otherwise, from tailWellFormed(), we know that isInDll(getTail()) so the result follows from forwardLinked(getTail()). -// result: forall addr. isForwardLinkedBetween(addr, getTail()) +// result: forall addr. isInDll(addr) => isForwardLinkedBetween(addr, getTail()) // explanation: it can be obtained from the previous result and forwardLinked. // Going from head to tail should lead to addr in between (otherwise addr is never reached because there is nothing after the tail). @@ -330,6 +330,5 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { // explanation: it comes from the fact that every non zero address that is in the DLL is linked to getHead(). // result: there are no cycles that do not contain the 0 address -// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() -// is part of the cycle. This is absurd because we know from headWellFormed() that the previous element of -// getHead() is the 0 address. +// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead()/ is part of the cycle. +// The result follows because we know from headWellFormed() that the previous element of getHead() is the 0 address. From 833e5f7cc0036cf3b67723d1a09fb4dea6f5df11 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 11:16:42 +0200 Subject: [PATCH 07/23] chore: import full verification from DllSimple --- certora/specs/DllFifo.spec | 92 +++++++++++++++++++++++++++++++++++--- 1 file changed, 85 insertions(+), 7 deletions(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index 56141bc..8c373b7 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -24,13 +24,16 @@ definition isInDll(address id) returns bool = getValueOf(id) != 0; definition isLinked(address id) returns bool = - getPrev(id) != 0 || getNext(id) != 0; + id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); -definition isEmpty(address id) returns bool = - ! isInDll(id) && ! isLinked(id); +definition isLinkedToZero(address id) returns bool = + isLinked(id) => + (getNext(id) == 0 => getPrev(0) == id) && + (getPrev(id) == 0 => getNext(0) == id); definition isTwoWayLinked(address first, address second) returns bool = - first != 0 && second != 0 => (getNext(first) == second <=> getPrev(second) == first); + (first != 0 => getPrev(second) == first => getNext(first) == second) && + (second != 0 => getNext(first) == second => getPrev(second) == first); definition isHeadWellFormed() returns bool = getPrev(getHead()) == 0 && (getHead() != 0 => isInDll(getHead())); @@ -56,9 +59,36 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). -invariant zeroEmpty() - isEmpty(0) - filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } +invariant linkedToZero(address addr) + isLinkedToZero(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant twoWayLinked(0, id); + requireInvariant twoWayLinked(id, 0); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isLinkedToZero(addr); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isLinkedToZero(addr); +} rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { address prev; @@ -78,14 +108,32 @@ rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { invariant headWellFormed() isHeadWellFormed() + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant linkedIsInDll(getNext(id)); + requireInvariant linkedToZero(id); } } +rule headWellFormedPreservedInsertSorted(address id, uint256 value) { + address prev; address next; + + require isHeadWellFormed(); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isHeadWellFormed(); +} + invariant tailWellFormed() isTailWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } @@ -94,6 +142,7 @@ invariant tailWellFormed() requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant linkedIsInDll(getPrev(id)); + requireInvariant linkedToZero(id); } } @@ -181,6 +230,35 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { assert hasNoNextIsTail(addr); } +invariant inDllIsLinked(address addr) + isInDll(addr) => isLinked(addr) + filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + { preserved remove(address id) { + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + +rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { + address addr; address prev; address next; + + require isInDll(addr) => isLinked(addr); + + requireInvariant twoWayLinked(getPrev(next), next); + requireInvariant twoWayLinked(prev, getNext(prev)); + requireInvariant linkedToZero(prev); + requireInvariant inDllIsLinked(prev); + + insertSorted(id, value); + + require prev == getInsertedAfter(); + require next == getInsertedBefore(); + + assert isInDll(addr) => isLinked(addr); +} + invariant linkedIsInDll(address addr) isLinked(addr) => isInDll(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } From 48a104c9931cac0f8e225ba6baaeb790cf1e1525 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 11:20:17 +0200 Subject: [PATCH 08/23] fix: remove zeroEmpty --- certora/specs/DllFifo.spec | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index 8c373b7..ae5dc54 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -48,7 +48,6 @@ definition hasNoNextIsTail(address addr) returns bool = isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { - requireInvariant zeroEmpty(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); requireInvariant tipsZero(); @@ -90,27 +89,10 @@ rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { assert isLinkedToZero(addr); } -rule zeroEmptyPreservedInsertSorted(address id, uint256 value) { - address prev; - - require isEmpty(0); - - requireInvariant twoWayLinked(prev, getNext(prev)); - requireInvariant noNextIsTail(prev); - requireInvariant tipsZero(); - - insertSorted(id, value, maxIterations()); - - require prev == getInsertedAfter(); - - assert isEmpty(0); -} - invariant headWellFormed() isHeadWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant linkedIsInDll(getNext(id)); @@ -138,7 +120,6 @@ invariant tailWellFormed() isTailWellFormed() filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); requireInvariant linkedIsInDll(getPrev(id)); @@ -151,7 +132,6 @@ rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { require isTailWellFormed(); - requireInvariant zeroEmpty(); requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); @@ -166,7 +146,6 @@ rule tailWellFormedPreservedInsertSorted(address id, uint256 value) { invariant tipsZero() getTail() == 0 <=> getHead() == 0 { preserved remove(address id) { - requireInvariant zeroEmpty(); requireInvariant noNextIsTail(id); requireInvariant noPrevIsHead(id); } From eb24ad8b8be88156d0787174b96ed9ce2b8917cd Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 11:23:32 +0200 Subject: [PATCH 09/23] fix: insertSorted signature --- certora/specs/DllFifo.spec | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index ae5dc54..42305e8 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -60,7 +60,7 @@ function safeAssumptions() { invariant linkedToZero(address addr) isLinkedToZero(addr) - filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); @@ -81,7 +81,7 @@ rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { requireInvariant linkedToZero(prev); requireInvariant inDllIsLinked(prev); - insertSorted(id, value); + insertSorted(id, value, maxIterations()); require prev == getInsertedAfter(); require next == getInsertedBefore(); @@ -91,7 +91,7 @@ rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { invariant headWellFormed() isHeadWellFormed() - filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); @@ -108,7 +108,7 @@ rule headWellFormedPreservedInsertSorted(address id, uint256 value) { requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); - insertSorted(id, value); + insertSorted(id, value, maxIterations()); require prev == getInsertedAfter(); require next == getInsertedBefore(); @@ -211,7 +211,7 @@ rule noNextisTailPreservedInsertSorted(address id, uint256 value) { invariant inDllIsLinked(address addr) isInDll(addr) => isLinked(addr) - filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } + filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } { preserved remove(address id) { requireInvariant twoWayLinked(getPrev(id), id); requireInvariant twoWayLinked(id, getNext(id)); @@ -230,7 +230,7 @@ rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { requireInvariant linkedToZero(prev); requireInvariant inDllIsLinked(prev); - insertSorted(id, value); + insertSorted(id, value, maxIterations()); require prev == getInsertedAfter(); require next == getInsertedBefore(); From 26ef4135a4118f28f752aec3c3378bfea1b06016 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 12:44:54 +0200 Subject: [PATCH 10/23] feat: emptyEquiv --- certora/specs/DllFifo.spec | 22 ++++++++++++++++++++-- certora/specs/DllSimple.spec | 16 +++++++++++++++- 2 files changed, 35 insertions(+), 3 deletions(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index 42305e8..c8498bd 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -26,6 +26,9 @@ definition isInDll(address id) returns bool = definition isLinked(address id) returns bool = id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); +definition isEmptyEquiv() returns bool = + getNext(0) == 0 <=> getPrev(0) == 0; + definition isLinkedToZero(address id) returns bool = isLinked(id) => (getNext(id) == 0 => getPrev(0) == id) && @@ -48,6 +51,7 @@ definition hasNoNextIsTail(address addr) returns bool = isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { + requireInvariant emptyEquiv(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); requireInvariant tipsZero(); @@ -58,6 +62,17 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). +invariant emptyEquiv() + isEmptyEquiv() + { preserved remove(address id) { + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + invariant linkedToZero(address addr) isLinkedToZero(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256, uint256).selector } @@ -76,6 +91,7 @@ rule linkedToZeroPreservedInsertSorted(address id, uint256 value) { require isLinkedToZero(addr); + safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); requireInvariant linkedToZero(prev); @@ -225,6 +241,7 @@ rule inDllIsLinkedPreservedInsertSorted(address id, uint256 value) { require isInDll(addr) => isLinked(addr); + safeAssumptions(); requireInvariant twoWayLinked(getPrev(next), next); requireInvariant twoWayLinked(prev, getNext(prev)); requireInvariant linkedToZero(prev); @@ -279,16 +296,18 @@ invariant twoWayLinked(address first, address second) } rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { - address first; address second; address next; + address first; address second; address prev; address next; require isTwoWayLinked(first, second); require isTwoWayLinked(getPrev(next), next); + require isTwoWayLinked(prev, getNext(prev)); safeAssumptions(); requireInvariant linkedIsInDll(id); insertSorted(id, value, maxIterations()); + require prev == getInsertedAfter(); require next == getInsertedBefore(); assert isTwoWayLinked(first, second); @@ -365,7 +384,6 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { require prev == getInsertedAfter(); uint256 positionInDll = lenUpTo(id); - assert positionInDll > maxIter => greaterThanUpTo(value, 0, maxIter) && id == getTail(); assert positionInDll <= maxIter => greaterThanUpTo(value, id, getLength()) && value > getValueOf(getNext(id)); } diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index d0dcdca..175aeb0 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -22,6 +22,9 @@ definition isInDll(address id) returns bool = definition isLinked(address id) returns bool = id != 0 && (getPrev(id) != 0 || getNext(id) != 0 || getPrev(0) == id || getNext(0) == id); +definition isEmptyEquiv() returns bool = + getNext(0) == 0 <=> getPrev(0) == 0; + definition isLinkedToZero(address id) returns bool = isLinked(id) => (getNext(id) == 0 => getPrev(0) == id) && @@ -54,6 +57,17 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). +invariant emptyEquiv() + isEmptyEquiv() + { preserved remove(address id) { + safeAssumptions(); + requireInvariant twoWayLinked(getPrev(id), id); + requireInvariant twoWayLinked(id, getNext(id)); + requireInvariant linkedToZero(id); + requireInvariant inDllIsLinked(id); + } + } + invariant linkedToZero(address addr) isLinkedToZero(addr) filtered { f -> f.selector != sig:insertSorted(address, uint256).selector } @@ -279,7 +293,7 @@ rule twoWayLinkedPreservedInsertSorted(address id, uint256 value) { require isTwoWayLinked(first, second); require isTwoWayLinked(getPrev(next), next); - requireInvariant twoWayLinked(prev, getNext(prev)); + require isTwoWayLinked(prev, getNext(prev)); safeAssumptions(); requireInvariant linkedIsInDll(id); From 76a0d1d2494323f24427c89370f21e56277341bf Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:10:38 +0200 Subject: [PATCH 11/23] feat: emptyZero --- certora/specs/DllFifo.spec | 4 ++++ certora/specs/DllSimple.spec | 3 +++ 2 files changed, 7 insertions(+) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index c8498bd..fd1f605 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -51,6 +51,7 @@ definition hasNoNextIsTail(address addr) returns bool = isInDll(addr) && getNext(addr) == 0 => addr == getTail(); function safeAssumptions() { + requireInvariant emptyZero(); requireInvariant emptyEquiv(); requireInvariant headWellFormed(); requireInvariant tailWellFormed(); @@ -62,6 +63,9 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). +invariant emptyZero() + ! isInDll(0); + invariant emptyEquiv() isEmptyEquiv() { preserved remove(address id) { diff --git a/certora/specs/DllSimple.spec b/certora/specs/DllSimple.spec index 175aeb0..c560d07 100644 --- a/certora/specs/DllSimple.spec +++ b/certora/specs/DllSimple.spec @@ -57,6 +57,9 @@ function safeAssumptions() { // or even all of the public functions (in that last case they are still relevant for proving // the property at initial state). +invariant emptyZero() + ! isInDll(0); + invariant emptyEquiv() isEmptyEquiv() { preserved remove(address id) { From dfba522451683c6a7e8155b1ede9b3d1707b708c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:21:27 +0200 Subject: [PATCH 12/23] refactor: remove insertedAfter initialization --- certora/applyHarnessFifo.patch | 11 ++++------- certora/applyHarnessSimple.patch | 11 +++++------ 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index f004fac..d0e4042 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol --- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-10 12:38:54.711124189 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:17:25.523919166 +0200 @@ -16,6 +16,8 @@ struct List { @@ -10,18 +10,15 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol } /* ERRORS */ -@@ -98,8 +100,10 @@ - - uint256 numberOfIterations; +@@ -100,6 +102,7 @@ address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. -+ list.insertedAfter = address(0); // HARNESS while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + list.insertedAfter = next; // HARNESS next = list.accounts[next].next; unchecked { ++numberOfIterations; -@@ -107,6 +111,7 @@ +@@ -107,6 +110,7 @@ } if (numberOfIterations == maxIterations) next = address(0); @@ -31,7 +28,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol list.accounts[id] = Account(prev, next, value); diff -ruN MockDLL.sol MockDLL.sol --- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-10 12:36:30.235182781 +0200 ++++ MockDLL.sol 2024-07-11 10:58:47.037997151 +0200 @@ -0,0 +1,111 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index 1abeb16..fa62a59 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol --- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-10 12:34:45.178218509 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:19:00.201544572 +0200 @@ -16,6 +16,8 @@ struct List { @@ -10,7 +10,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol } /* ERRORS */ -@@ -90,23 +92,20 @@ +@@ -90,23 +92,19 @@ /// @param list The list to search in. /// @param id The address of the account. /// @param value The value of the account. @@ -23,12 +23,11 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol - uint256 numberOfIterations; - address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. -+ list.insertedAfter = address(0); + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + while (next != address(0) && list.accounts[next].value >= value) { -+ list.insertedAfter = next; ++ list.insertedAfter = next; // HARNESS next = list.accounts[next].next; - unchecked { - ++numberOfIterations; @@ -36,13 +35,13 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol } - if (numberOfIterations == maxIterations) next = address(0); -+ list.insertedBefore = next; ++ list.insertedBefore = next; // HARNESS address prev = list.accounts[next].prev; list.accounts[id] = Account(prev, next, value); diff -ruN MockDLL.sol MockDLL.sol --- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-10 12:26:25.130305388 +0200 ++++ MockDLL.sol 2024-07-11 12:42:15.108949766 +0200 @@ -0,0 +1,91 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; From fe1d00f941d206287b4dcd2baa84d7231353b84c Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:31:29 +0200 Subject: [PATCH 13/23] refactor: minimize munging --- certora/applyHarnessFifo.patch | 115 ------------------------------ certora/applyHarnessSimple.patch | 95 ------------------------ certora/confs/DllFifo.conf | 4 +- certora/confs/DllSimple.conf | 4 +- certora/helpers/MockDllFifo.sol | 105 +++++++++++++++++++++++++++ certora/helpers/MockDllSimple.sol | 93 ++++++++++++++++++++++++ 6 files changed, 202 insertions(+), 214 deletions(-) create mode 100644 certora/helpers/MockDllFifo.sol create mode 100644 certora/helpers/MockDllSimple.sol diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index d0e4042..8222e01 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -26,118 +26,3 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol address prev = list.accounts[next].prev; list.accounts[id] = Account(prev, next, value); -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-11 10:58:47.037997151 +0200 -@@ -0,0 +1,111 @@ -+// SPDX-License-Identifier: AGPL-3.0-only -+pragma solidity ^0.8.0; -+ -+import "./DoubleLinkedList.sol"; -+ -+contract MockDLL { -+ using DoubleLinkedList for DoubleLinkedList.List; -+ -+ // VERIFICATION INTERFACE -+ -+ DoubleLinkedList.List public dll; -+ -+ uint256 public maxIterations; -+ -+ uint256 internal dummy_state_variable; -+ -+ function dummy_state_modifying_function() public { -+ // to fix a CVL error when only one function is accessible -+ dummy_state_variable = 1; -+ } -+ -+ function getValueOf(address _id) public view returns (uint256) { -+ return dll.getValueOf(_id); -+ } -+ -+ function getHead() public view returns (address) { -+ return dll.getHead(); -+ } -+ -+ function getTail() public view returns (address) { -+ return dll.getTail(); -+ } -+ -+ function getNext(address _id) public view returns (address) { -+ return dll.getNext(_id); -+ } -+ -+ function getPrev(address _id) public view returns (address) { -+ return dll.getPrev(_id); -+ } -+ -+ function remove(address _id) public { -+ dll.remove(_id); -+ } -+ -+ function insertSorted( -+ address _id, -+ uint256 _value, -+ uint256 _maxIterations -+ ) public { -+ dll.insertSorted(_id, _value, _maxIterations); -+ } -+ -+ // SPECIFICATION HELPERS -+ -+ function getInsertedAfter() public view returns (address) { -+ return dll.insertedAfter; -+ } -+ -+ function getInsertedBefore() public view returns (address) { -+ return dll.insertedBefore; -+ } -+ -+ function getLength() public view returns (uint256) { -+ uint256 len; -+ for (address current = getHead(); current != address(0); current = getNext(current)) len++; -+ return len; -+ } -+ -+ function linkBetween(address _start, address _end) internal view returns (bool, address) { -+ if (_start == _end) return (true, address(0)); -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == _end) return (true, _start); -+ _start = next; -+ } -+ return (false, address(0)); -+ } -+ -+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { -+ (ret, ) = linkBetween(_start, _end); -+ } -+ -+ function getPreceding(address _end) public view returns (address last) { -+ (, last) = linkBetween(getHead(), _end); -+ } -+ -+ function greaterThanUpTo( -+ uint256 _value, -+ address _to, -+ uint256 _maxIter -+ ) public view returns (bool) { -+ address from = getHead(); -+ for (; _maxIter > 0; _maxIter--) { -+ if (from == _to) return true; -+ if (getValueOf(from) < _value) return false; -+ from = getNext(from); -+ } -+ return true; -+ } -+ -+ function lenUpTo(address _to) public view returns (uint256) { -+ uint256 maxIter = getLength(); -+ address from = getHead(); -+ for (; maxIter > 0; maxIter--) { -+ if (from == _to) break; -+ from = getNext(from); -+ } -+ return getLength() - maxIter; -+ } -+} diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index fa62a59..fa8d984 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -39,98 +39,3 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol address prev = list.accounts[next].prev; list.accounts[id] = Account(prev, next, value); -diff -ruN MockDLL.sol MockDLL.sol ---- MockDLL.sol 1970-01-01 01:00:00.000000000 +0100 -+++ MockDLL.sol 2024-07-11 12:42:15.108949766 +0200 -@@ -0,0 +1,91 @@ -+// SPDX-License-Identifier: AGPL-3.0-only -+pragma solidity ^0.8.0; -+ -+import "./DoubleLinkedList.sol"; -+ -+contract MockDLL { -+ using DoubleLinkedList for DoubleLinkedList.List; -+ -+ // VERIFICATION INTERFACE -+ -+ DoubleLinkedList.List public dll; -+ -+ uint256 internal dummy_state_variable; -+ -+ function dummy_state_modifying_function() public { -+ // to fix a CVL error when only one function is accessible -+ dummy_state_variable = 1; -+ } -+ -+ function getValueOf(address _id) public view returns (uint256) { -+ return dll.getValueOf(_id); -+ } -+ -+ function getHead() public view returns (address) { -+ return dll.getHead(); -+ } -+ -+ function getTail() public view returns (address) { -+ return dll.getTail(); -+ } -+ -+ function getNext(address _id) public view returns (address) { -+ return dll.getNext(_id); -+ } -+ -+ function getPrev(address _id) public view returns (address) { -+ return dll.getPrev(_id); -+ } -+ -+ function remove(address _id) public { -+ dll.remove(_id); -+ } -+ -+ function insertSorted(address _id, uint256 _value) public { -+ dll.insertSorted(_id, _value); -+ } -+ -+ // SPECIFICATION HELPERS -+ -+ function getInsertedAfter() public view returns (address) { -+ return dll.insertedAfter; -+ } -+ -+ function getInsertedBefore() public view returns (address) { -+ return dll.insertedBefore; -+ } -+ -+ function getLength() internal view returns (uint256) { -+ uint256 len; -+ for (address current = getHead(); current != address(0); current = getNext(current)) len++; -+ return len; -+ } -+ -+ function linkBetween(address _start, address _end) internal view returns (bool, address) { -+ if (_start == _end) return (true, address(0)); -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == _end) return (true, _start); -+ _start = next; -+ } -+ return (false, address(0)); -+ } -+ -+ function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { -+ (ret, ) = linkBetween(_start, _end); -+ } -+ -+ function getPreceding(address _end) public view returns (address last) { -+ (, last) = linkBetween(getHead(), _end); -+ } -+ -+ function isDecrSortedFrom(address _start) public view returns (bool) { -+ for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { -+ address next = getNext(_start); -+ if (next == address(0)) return true; -+ if (getValueOf(_start) < getValueOf(next)) return false; -+ _start = getNext(_start); -+ } -+ return true; -+ } -+} diff --git a/certora/confs/DllFifo.conf b/certora/confs/DllFifo.conf index 9f343df..1bc933d 100644 --- a/certora/confs/DllFifo.conf +++ b/certora/confs/DllFifo.conf @@ -1,9 +1,9 @@ { "files": [ - "certora/munged-fifo/MockDLL.sol", + "certora/helpers/MockDllFifo.sol", ], "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllFifo.spec", + "verify": "MockDllFifo:certora/specs/DllFifo.spec", "loop_iter": "4", "optimistic_loop": true, "rule_sanity": "basic", diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index 1477691..c099557 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -1,9 +1,9 @@ { "files": [ - "certora/munged-simple/MockDLL.sol", + "certora/helpers/MockDllSimple.sol", ], "solc": "solc-0.8.17", - "verify": "MockDLL:certora/specs/DllSimple.spec", + "verify": "MockDllSimple:certora/specs/DllSimple.spec", "loop_iter": "7", "optimistic_loop": true, "rule_sanity": "basic", diff --git a/certora/helpers/MockDllFifo.sol b/certora/helpers/MockDllFifo.sol new file mode 100644 index 0000000..26cc3b4 --- /dev/null +++ b/certora/helpers/MockDllFifo.sol @@ -0,0 +1,105 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "../munged-fifo/DoubleLinkedList.sol"; + +contract MockDllFifo { + using DoubleLinkedList for DoubleLinkedList.List; + + // VERIFICATION INTERFACE + + DoubleLinkedList.List public dll; + + uint256 public maxIterations; + + uint256 internal dummy_state_variable; + + function dummy_state_modifying_function() public { + // to fix a CVL error when only one function is accessible + dummy_state_variable = 1; + } + + function getValueOf(address _id) public view returns (uint256) { + return dll.getValueOf(_id); + } + + function getHead() public view returns (address) { + return dll.getHead(); + } + + function getTail() public view returns (address) { + return dll.getTail(); + } + + function getNext(address _id) public view returns (address) { + return dll.getNext(_id); + } + + function getPrev(address _id) public view returns (address) { + return dll.getPrev(_id); + } + + function remove(address _id) public { + dll.remove(_id); + } + + function insertSorted(address _id, uint256 _value, uint256 _maxIterations) public { + dll.insertSorted(_id, _value, _maxIterations); + } + + // SPECIFICATION HELPERS + + function getInsertedAfter() public view returns (address) { + return dll.insertedAfter; + } + + function getInsertedBefore() public view returns (address) { + return dll.insertedBefore; + } + + function getLength() public view returns (uint256) { + uint256 len; + for (address current = getHead(); current != address(0); current = getNext(current)) { + len++; + } + return len; + } + + function linkBetween(address _start, address _end) internal view returns (bool, address) { + if (_start == _end) return (true, address(0)); + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == _end) return (true, _start); + _start = next; + } + return (false, address(0)); + } + + function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { + (ret,) = linkBetween(_start, _end); + } + + function getPreceding(address _end) public view returns (address last) { + (, last) = linkBetween(getHead(), _end); + } + + function greaterThanUpTo(uint256 _value, address _to, uint256 _maxIter) public view returns (bool) { + address from = getHead(); + for (; _maxIter > 0; _maxIter--) { + if (from == _to) return true; + if (getValueOf(from) < _value) return false; + from = getNext(from); + } + return true; + } + + function lenUpTo(address _to) public view returns (uint256) { + uint256 maxIter = getLength(); + address from = getHead(); + for (; maxIter > 0; maxIter--) { + if (from == _to) break; + from = getNext(from); + } + return getLength() - maxIter; + } +} diff --git a/certora/helpers/MockDllSimple.sol b/certora/helpers/MockDllSimple.sol new file mode 100644 index 0000000..a835202 --- /dev/null +++ b/certora/helpers/MockDllSimple.sol @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "../munged-simple/DoubleLinkedList.sol"; + +contract MockDllSimple { + using DoubleLinkedList for DoubleLinkedList.List; + + // VERIFICATION INTERFACE + + DoubleLinkedList.List public dll; + + uint256 internal dummy_state_variable; + + function dummy_state_modifying_function() public { + // to fix a CVL error when only one function is accessible + dummy_state_variable = 1; + } + + function getValueOf(address _id) public view returns (uint256) { + return dll.getValueOf(_id); + } + + function getHead() public view returns (address) { + return dll.getHead(); + } + + function getTail() public view returns (address) { + return dll.getTail(); + } + + function getNext(address _id) public view returns (address) { + return dll.getNext(_id); + } + + function getPrev(address _id) public view returns (address) { + return dll.getPrev(_id); + } + + function remove(address _id) public { + dll.remove(_id); + } + + function insertSorted(address _id, uint256 _value) public { + dll.insertSorted(_id, _value); + } + + // SPECIFICATION HELPERS + + function getInsertedAfter() public view returns (address) { + return dll.insertedAfter; + } + + function getInsertedBefore() public view returns (address) { + return dll.insertedBefore; + } + + function getLength() internal view returns (uint256) { + uint256 len; + for (address current = getHead(); current != address(0); current = getNext(current)) { + len++; + } + return len; + } + + function linkBetween(address _start, address _end) internal view returns (bool, address) { + if (_start == _end) return (true, address(0)); + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == _end) return (true, _start); + _start = next; + } + return (false, address(0)); + } + + function isForwardLinkedBetween(address _start, address _end) public view returns (bool ret) { + (ret,) = linkBetween(_start, _end); + } + + function getPreceding(address _end) public view returns (address last) { + (, last) = linkBetween(getHead(), _end); + } + + function isDecrSortedFrom(address _start) public view returns (bool) { + for (uint256 maxIter = getLength(); maxIter > 0; maxIter--) { + address next = getNext(_start); + if (next == address(0)) return true; + if (getValueOf(_start) < getValueOf(next)) return false; + _start = getNext(_start); + } + return true; + } +} From a70980165be2aea0bdbec4eae959467bd9c47816 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:41:27 +0200 Subject: [PATCH 14/23] docs: next is always insertedBefore --- certora/applyHarnessFifo.patch | 6 +++--- certora/applyHarnessSimple.patch | 7 +++---- src/DoubleLinkedList.sol | 2 +- 3 files changed, 7 insertions(+), 8 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 8222e01..4f69001 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:17:25.523919166 +0200 +--- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:40:22.469518264 +0200 @@ -16,6 +16,8 @@ struct List { @@ -11,7 +11,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol /* ERRORS */ @@ -100,6 +102,7 @@ - address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + list.insertedAfter = next; // HARNESS diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index fa8d984..bcbedda 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-10 12:25:51.055549876 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:19:00.201544572 +0200 +--- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 ++++ DoubleLinkedList.sol 2024-07-11 13:40:08.765859975 +0200 @@ -16,6 +16,8 @@ struct List { @@ -22,8 +22,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - uint256 numberOfIterations; -- address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. -+ address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + while (next != address(0) && list.accounts[next].value >= value) { diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index 7a988d4..aae953b 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -97,7 +97,7 @@ library DoubleLinkedList { if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); uint256 numberOfIterations; - address next = list.accounts[address(0)].next; // If not added at the end of the list `id` will be inserted before `next`. + address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { next = list.accounts[next].next; From 7c249ac28ad66c70949720850f0bf35deda060ce Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:45:05 +0200 Subject: [PATCH 15/23] docs: fix natspec of getValueOf --- src/DoubleLinkedList.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index aae953b..867556b 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -34,7 +34,7 @@ library DoubleLinkedList { /* INTERNAL */ - /// @notice Returns the `account` linked to `id`. + /// @notice Returns the value of the account linked to `id`. /// @param list The list to search in. /// @param id The address of the account. /// @return The value of the account. From 2a403e170a1970abbe3dbffaf7aff2cd981fc5bf Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 11 Jul 2024 13:58:01 +0200 Subject: [PATCH 16/23] docs: correct one typo --- certora/specs/DllFifo.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/DllFifo.spec b/certora/specs/DllFifo.spec index fd1f605..f0ce8c3 100644 --- a/certora/specs/DllFifo.spec +++ b/certora/specs/DllFifo.spec @@ -409,5 +409,5 @@ rule insertSortedDecreasingOrder(address id, uint256 value) { // explanation: it comes from the fact that every non zero address that is in the DLL is linked to getHead(). // result: there are no cycles that do not contain the 0 address -// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead()/ is part of the cycle. +// explanation: let N be a node in a cycle. Since there is a link from getHead() to N, it means that getHead() is part of the cycle. // The result follows because we know from headWellFormed() that the previous element of getHead() is the 0 address. From 5cfa1a6eb4712f5f942ef1490588879740f1acc6 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 12 Jul 2024 09:59:02 +0200 Subject: [PATCH 17/23] refactor: simplify loop in insertSorted --- certora/applyHarnessFifo.patch | 15 ++++++--------- certora/applyHarnessSimple.patch | 16 +++++++--------- src/DoubleLinkedList.sol | 8 +++----- 3 files changed, 16 insertions(+), 23 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 4f69001..4fad2fe 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:40:22.469518264 +0200 +--- DoubleLinkedList.sol 2024-07-12 09:49:49.899261374 +0200 ++++ DoubleLinkedList.sol 2024-07-12 09:53:11.964303440 +0200 @@ -16,6 +16,8 @@ struct List { @@ -10,15 +10,12 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol } /* ERRORS */ -@@ -100,6 +102,7 @@ - address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { +@@ -101,10 +103,12 @@ + uint256 numberOfIterations; + for (; numberOfIterations < maxIterations; numberOfIterations++) { + if (next == address(0) || list.accounts[next].value < value) break; + list.insertedAfter = next; // HARNESS next = list.accounts[next].next; - unchecked { - ++numberOfIterations; -@@ -107,6 +110,7 @@ } if (numberOfIterations == maxIterations) next = address(0); diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index bcbedda..24b686d 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-11 13:38:21.976522997 +0200 -+++ DoubleLinkedList.sol 2024-07-11 13:40:08.765859975 +0200 +--- DoubleLinkedList.sol 2024-07-12 09:49:49.899261374 +0200 ++++ DoubleLinkedList.sol 2024-07-12 09:52:16.333105454 +0200 @@ -16,6 +16,8 @@ struct List { @@ -10,7 +10,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol } /* ERRORS */ -@@ -90,23 +92,19 @@ +@@ -90,21 +92,20 @@ /// @param list The list to search in. /// @param id The address of the account. /// @param value The value of the account. @@ -21,16 +21,14 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); -- uint256 numberOfIterations; address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. -- while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { -+ while (next != address(0) && list.accounts[next].value >= value) { +- uint256 numberOfIterations; +- for (; numberOfIterations < maxIterations; numberOfIterations++) { ++ for (;;) { + if (next == address(0) || list.accounts[next].value < value) break; + list.insertedAfter = next; // HARNESS next = list.accounts[next].next; -- unchecked { -- ++numberOfIterations; -- } } - if (numberOfIterations == maxIterations) next = address(0); diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index 867556b..fd305bf 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -96,14 +96,12 @@ library DoubleLinkedList { if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - uint256 numberOfIterations; address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. - while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) { + uint256 numberOfIterations; + for (; numberOfIterations < maxIterations; numberOfIterations++) { + if (next == address(0) || list.accounts[next].value < value) break; next = list.accounts[next].next; - unchecked { - ++numberOfIterations; - } } if (numberOfIterations == maxIterations) next = address(0); From 0043ef2ca8c46cb86db01fe057670a2916371edd Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 14 Aug 2024 10:17:03 +0200 Subject: [PATCH 18/23] refactor: use getters --- certora/applyHarnessFifo.patch | 8 ++++---- certora/applyHarnessSimple.patch | 10 +++++----- src/DoubleLinkedList.sol | 6 +++--- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 4fad2fe..5bb92f1 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-12 09:49:49.899261374 +0200 -+++ DoubleLinkedList.sol 2024-07-12 09:53:11.964303440 +0200 +--- DoubleLinkedList.sol 2024-08-14 10:10:08.974975205 +0200 ++++ DoubleLinkedList.sol 2024-08-14 10:14:10.970436843 +0200 @@ -16,6 +16,8 @@ struct List { @@ -15,11 +15,11 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol for (; numberOfIterations < maxIterations; numberOfIterations++) { if (next == address(0) || list.accounts[next].value < value) break; + list.insertedAfter = next; // HARNESS - next = list.accounts[next].next; + next = getNext(list, next); } if (numberOfIterations == maxIterations) next = address(0); + list.insertedBefore = next; // HARNESS - address prev = list.accounts[next].prev; + address prev = getPrev(list, next); list.accounts[id] = Account(prev, next, value); diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index 24b686d..ebbbe89 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-07-12 09:49:49.899261374 +0200 -+++ DoubleLinkedList.sol 2024-07-12 09:52:16.333105454 +0200 +--- DoubleLinkedList.sol 2024-08-14 10:10:08.974975205 +0200 ++++ DoubleLinkedList.sol 2024-08-14 10:13:25.455164370 +0200 @@ -16,6 +16,8 @@ struct List { @@ -21,18 +21,18 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. + address next = getHead(list); // `id` will be inserted before `next`. - uint256 numberOfIterations; - for (; numberOfIterations < maxIterations; numberOfIterations++) { + for (;;) { if (next == address(0) || list.accounts[next].value < value) break; + list.insertedAfter = next; // HARNESS - next = list.accounts[next].next; + next = getNext(list, next); } - if (numberOfIterations == maxIterations) next = address(0); + list.insertedBefore = next; // HARNESS - address prev = list.accounts[next].prev; + address prev = getPrev(list, next); list.accounts[id] = Account(prev, next, value); diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol index fd305bf..009e94f 100644 --- a/src/DoubleLinkedList.sol +++ b/src/DoubleLinkedList.sol @@ -96,17 +96,17 @@ library DoubleLinkedList { if (id == address(0)) revert AddressIsZero(); if (list.accounts[id].value != 0) revert AccountAlreadyInserted(); - address next = list.accounts[address(0)].next; // `id` will be inserted before `next`. + address next = getHead(list); // `id` will be inserted before `next`. uint256 numberOfIterations; for (; numberOfIterations < maxIterations; numberOfIterations++) { if (next == address(0) || list.accounts[next].value < value) break; - next = list.accounts[next].next; + next = getNext(list, next); } if (numberOfIterations == maxIterations) next = address(0); - address prev = list.accounts[next].prev; + address prev = getPrev(list, next); list.accounts[id] = Account(prev, next, value); list.accounts[prev].next = id; list.accounts[next].prev = id; From df17d59c00cc202859288beee4e11b7a9d639521 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 5 Dec 2024 14:03:52 +0100 Subject: [PATCH 19/23] feat: remove timestamp in patch --- certora/applyHarnessFifo.patch | 4 ++-- certora/applyHarnessSimple.patch | 4 ++-- certora/makefile | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch index 5bb92f1..d76321b 100644 --- a/certora/applyHarnessFifo.patch +++ b/certora/applyHarnessFifo.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-08-14 10:10:08.974975205 +0200 -+++ DoubleLinkedList.sol 2024-08-14 10:14:10.970436843 +0200 +--- DoubleLinkedList.sol ++++ DoubleLinkedList.sol @@ -16,6 +16,8 @@ struct List { diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch index ebbbe89..fd5e6c9 100644 --- a/certora/applyHarnessSimple.patch +++ b/certora/applyHarnessSimple.patch @@ -1,6 +1,6 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol ---- DoubleLinkedList.sol 2024-08-14 10:10:08.974975205 +0200 -+++ DoubleLinkedList.sol 2024-08-14 10:13:25.455164370 +0200 +--- DoubleLinkedList.sol ++++ DoubleLinkedList.sol @@ -16,6 +16,8 @@ struct List { diff --git a/certora/makefile b/certora/makefile index e22c5bd..a946404 100644 --- a/certora/makefile +++ b/certora/makefile @@ -7,7 +7,7 @@ munged-simple: $(wildcard ../src/*.sol) applyHarnessSimple.patch @patch -p0 -d munged-simple < applyHarnessSimple.patch record-simple: - diff -ruN ../src munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' > applyHarnessSimple.patch + diff -ruN ../src munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' | sed 's,\(\-\-\- [^[:space:]]*\).*,\1,' | sed 's,\(+++ [^[:space:]]*\).*,\1,' > applyHarnessSimple.patch munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @rm -rf munged-fifo @@ -15,7 +15,7 @@ munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @patch -p0 -d munged-fifo < applyHarnessFifo.patch record-fifo: - diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' > applyHarnessFifo.patch + diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' | sed 's,\(\-\-\- [^[:space:]]*\).*,\1,' | sed 's,\(+++ [^[:space:]]*\).*,\1,' > applyHarnessFifo.patch clean: rm -rf munged-simple munged-fifo From ac6cfd2488fe9266e00d9496f9c08eae2c916c34 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 5 Dec 2024 14:12:13 +0100 Subject: [PATCH 20/23] refactor: remove now useless workaround --- certora/helpers/MockDllFifo.sol | 7 ------- certora/helpers/MockDllSimple.sol | 7 ------- 2 files changed, 14 deletions(-) diff --git a/certora/helpers/MockDllFifo.sol b/certora/helpers/MockDllFifo.sol index 26cc3b4..de97115 100644 --- a/certora/helpers/MockDllFifo.sol +++ b/certora/helpers/MockDllFifo.sol @@ -12,13 +12,6 @@ contract MockDllFifo { uint256 public maxIterations; - uint256 internal dummy_state_variable; - - function dummy_state_modifying_function() public { - // to fix a CVL error when only one function is accessible - dummy_state_variable = 1; - } - function getValueOf(address _id) public view returns (uint256) { return dll.getValueOf(_id); } diff --git a/certora/helpers/MockDllSimple.sol b/certora/helpers/MockDllSimple.sol index a835202..65950fa 100644 --- a/certora/helpers/MockDllSimple.sol +++ b/certora/helpers/MockDllSimple.sol @@ -10,13 +10,6 @@ contract MockDllSimple { DoubleLinkedList.List public dll; - uint256 internal dummy_state_variable; - - function dummy_state_modifying_function() public { - // to fix a CVL error when only one function is accessible - dummy_state_variable = 1; - } - function getValueOf(address _id) public view returns (uint256) { return dll.getValueOf(_id); } From 47d174452928135585a54ebcf016852de8583ce2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 5 Dec 2024 14:13:22 +0100 Subject: [PATCH 21/23] chore: format .conf files --- certora/confs/DllFifo.conf | 20 ++++++++++---------- certora/confs/DllSimple.conf | 20 ++++++++++---------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/certora/confs/DllFifo.conf b/certora/confs/DllFifo.conf index 1bc933d..3b6d13a 100644 --- a/certora/confs/DllFifo.conf +++ b/certora/confs/DllFifo.conf @@ -1,12 +1,12 @@ { - "files": [ - "certora/helpers/MockDllFifo.sol", - ], - "solc": "solc-0.8.17", - "verify": "MockDllFifo:certora/specs/DllFifo.spec", - "loop_iter": "4", - "optimistic_loop": true, - "rule_sanity": "basic", - "server": "production", - "msg": "FIFO DLL", + "files": [ + "certora/helpers/MockDllFifo.sol" + ], + "solc": "solc-0.8.17", + "verify": "MockDllFifo:certora/specs/DllFifo.spec", + "loop_iter": "4", + "optimistic_loop": true, + "rule_sanity": "basic", + "server": "production", + "msg": "FIFO DLL" } diff --git a/certora/confs/DllSimple.conf b/certora/confs/DllSimple.conf index c099557..dd16af5 100644 --- a/certora/confs/DllSimple.conf +++ b/certora/confs/DllSimple.conf @@ -1,12 +1,12 @@ { - "files": [ - "certora/helpers/MockDllSimple.sol", - ], - "solc": "solc-0.8.17", - "verify": "MockDllSimple:certora/specs/DllSimple.spec", - "loop_iter": "7", - "optimistic_loop": true, - "rule_sanity": "basic", - "server": "production", - "msg": "Simple DLL", + "files": [ + "certora/helpers/MockDllSimple.sol" + ], + "solc": "solc-0.8.17", + "verify": "MockDllSimple:certora/specs/DllSimple.spec", + "loop_iter": "7", + "optimistic_loop": true, + "rule_sanity": "basic", + "server": "production", + "msg": "Simple DLL" } From 52a62ed2d01c0fc3a9c8c2b3e03213ee3a256a44 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 5 Dec 2024 14:14:25 +0100 Subject: [PATCH 22/23] chore: named imports --- certora/helpers/MockDllFifo.sol | 2 +- certora/helpers/MockDllSimple.sol | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/helpers/MockDllFifo.sol b/certora/helpers/MockDllFifo.sol index de97115..2531de0 100644 --- a/certora/helpers/MockDllFifo.sol +++ b/certora/helpers/MockDllFifo.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: AGPL-3.0-only pragma solidity ^0.8.0; -import "../munged-fifo/DoubleLinkedList.sol"; +import {DoubleLinkedList} from "../munged-fifo/DoubleLinkedList.sol"; contract MockDllFifo { using DoubleLinkedList for DoubleLinkedList.List; diff --git a/certora/helpers/MockDllSimple.sol b/certora/helpers/MockDllSimple.sol index 65950fa..376e5d5 100644 --- a/certora/helpers/MockDllSimple.sol +++ b/certora/helpers/MockDllSimple.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: AGPL-3.0-only pragma solidity ^0.8.0; -import "../munged-simple/DoubleLinkedList.sol"; +import {DoubleLinkedList} from "../munged-simple/DoubleLinkedList.sol"; contract MockDllSimple { using DoubleLinkedList for DoubleLinkedList.List; From ed091a1534b720e57a486c146cae6c4c22db6d1e Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 5 Dec 2024 20:28:57 +0100 Subject: [PATCH 23/23] refactor: merge sed filters --- certora/makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/makefile b/certora/makefile index a946404..f3a1e41 100644 --- a/certora/makefile +++ b/certora/makefile @@ -7,7 +7,7 @@ munged-simple: $(wildcard ../src/*.sol) applyHarnessSimple.patch @patch -p0 -d munged-simple < applyHarnessSimple.patch record-simple: - diff -ruN ../src munged-simple | sed 's+\.\./src/++g' | sed 's+munged-simple/++g' | sed 's,\(\-\-\- [^[:space:]]*\).*,\1,' | sed 's,\(+++ [^[:space:]]*\).*,\1,' > applyHarnessSimple.patch + diff -ruN ../src munged-simple | sed 's,\.\./src/\|munged-simple/,,g' | sed 's,\(\(\-\-\-\|+++\) [^[:space:]]*\).*,\1,' > applyHarnessSimple.patch munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @rm -rf munged-fifo @@ -15,9 +15,9 @@ munged-fifo: $(wildcard ../src/*.sol) applyHarnessFifo.patch @patch -p0 -d munged-fifo < applyHarnessFifo.patch record-fifo: - diff -ruN ../src munged-fifo | sed 's+\.\./src/++g' | sed 's+munged-fifo/++g' | sed 's,\(\-\-\- [^[:space:]]*\).*,\1,' | sed 's,\(+++ [^[:space:]]*\).*,\1,' > applyHarnessFifo.patch + diff -ruN ../src munged-fifo | sed 's,\.\./src/\|munged-fifo/,,g' | sed 's,\(\(\-\-\-\|+++\) [^[:space:]]*\).*,\1,' > applyHarnessFifo.patch clean: rm -rf munged-simple munged-fifo -.PHONY: help clean # do not add munged here, as it is useful to protect munged edits +.PHONY: help clean record-simple record-fifo # do not add munged folders here, as it is useful to protect munged edits