From b6df4daa88cfb12464f4b9158e61eb8b6f0b5f41 Mon Sep 17 00:00:00 2001
From: ChaoticWalrus <93558947+ChaoticWalrus@users.noreply.github.com>
Date: Mon, 24 Jun 2024 07:43:27 -0700
Subject: [PATCH] feat: improve certora coverage (#489)

* feat: add rules for withdrawal delay behavior

* chore: update branch list in Prover GH action file
---
 .github/workflows/certora-prover.yml      |  5 +++-
 certora/specs/core/DelegationManager.spec | 34 +++++++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml
index e255d8e29..f8556b756 100644
--- a/.github/workflows/certora-prover.yml
+++ b/.github/workflows/certora-prover.yml
@@ -7,7 +7,10 @@ on:
       - release-v*
       - formal-verification
       - m2-mainnet
-  pull_request: {}
+      - testnet-holesky
+  pull_request:
+    branches:
+      - dev
   workflow_dispatch: {}
 
 jobs:
diff --git a/certora/specs/core/DelegationManager.spec b/certora/specs/core/DelegationManager.spec
index a575c6716..4e7b8a538 100644
--- a/certora/specs/core/DelegationManager.spec
+++ b/certora/specs/core/DelegationManager.spec
@@ -67,6 +67,9 @@ methods {
     function owner() external returns (address) envfree;
     function strategyManager() external returns (address) envfree;
     function eigenPodManager() external returns (address) envfree;
+    function minWithdrawalDelayBlocks() external returns (uint256) envfree;
+    function calculateWithdrawalRoot(IDelegationManager.Withdrawal) external returns (bytes32) envfree;
+    function pendingWithdrawals(bytes32) external returns (bool) envfree;
 }
 
 /*
@@ -257,6 +260,37 @@ rule sharesBecomeUndelegatedWhenStakerUndelegates(address operator, address stak
     }
 }
 
+rule newWithdrawalsHaveCorrectStartBlock() {
+    IDelegationManager.Withdrawal queuedWithdrawal;
+    bytes32 withdrawalRoot = calculateWithdrawalRoot(queuedWithdrawal);
+    require(!pendingWithdrawals(withdrawalRoot));
+
+    // perform arbitrary function call
+    method f;
+    env e;
+    calldataarg arg;
+
+    assert(
+        !pendingWithdrawals(withdrawalRoot)
+        || (queuedWithdrawal.startBlock == assert_uint32(e.block.number)),
+        "withdrawal start block set incorrectly"
+    );
+}
+
+rule withdrawalDelayIsEnforced() {
+    IDelegationManager.Withdrawal queuedWithdrawal;
+    address[] tokens;
+    uint256 middlewareTimesIndex;
+    bool receiveAsTokens;
+    env e;
+    completeQueuedWithdrawal(e, queuedWithdrawal, tokens, middlewareTimesIndex, receiveAsTokens);
+    bool callReverted = lastReverted;
+    assert(
+        callReverted
+        || (assert_uint256(queuedWithdrawal.startBlock + minWithdrawalDelayBlocks()) >= e.block.number),
+        "withdrawal delay not properly enforced"
+    );
+}
 
 /*
 rule batchEquivalence {