From 1a60b061d5bb809c3d7e4ee915c77a00b1eca95d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ernesto=20Garc=C3=ADa?= <ernestognw@gmail.com>
Date: Thu, 16 Mar 2023 13:08:28 -0600
Subject: [PATCH] Add Pausable FV (#4117)

Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
---
 .gitignore                            |  1 +
 certora/harnesses/PausableHarness.sol | 19 ++++++
 certora/specs.json                    |  5 ++
 certora/specs/Pausable.spec           | 96 +++++++++++++++++++++++++++
 4 files changed, 121 insertions(+)
 create mode 100644 certora/harnesses/PausableHarness.sol
 create mode 100644 certora/specs/Pausable.spec

diff --git a/.gitignore b/.gitignore
index 9350b262e..2aac74485 100644
--- a/.gitignore
+++ b/.gitignore
@@ -68,3 +68,4 @@ contracts-exposed
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol
new file mode 100644
index 000000000..37c5d591d
--- /dev/null
+++ b/certora/harnesses/PausableHarness.sol
@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/security/Pausable.sol";
+
+contract PausableHarness is Pausable {
+    function pause() external {
+        _pause();
+    }
+
+    function unpause() external {
+        _unpause();
+    }
+
+    function onlyWhenPaused() external whenPaused {}
+
+    function onlyWhenNotPaused() external whenNotPaused {}
+}
diff --git a/certora/specs.json b/certora/specs.json
index e76db3084..80fbf26af 100644
--- a/certora/specs.json
+++ b/certora/specs.json
@@ -1,4 +1,9 @@
 [
+  {
+    "spec": "Pausable",
+    "contract": "PausableHarness",
+    "files": ["certora/harnesses/PausableHarness.sol"]
+  },
   {
     "spec": "AccessControl",
     "contract": "AccessControlHarness",
diff --git a/certora/specs/Pausable.spec b/certora/specs/Pausable.spec
new file mode 100644
index 000000000..e49293ffc
--- /dev/null
+++ b/certora/specs/Pausable.spec
@@ -0,0 +1,96 @@
+import "helpers.spec"
+
+methods {
+    paused() returns (bool) envfree
+    pause()
+    unpause()
+    onlyWhenPaused()
+    onlyWhenNotPaused()
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _pause pauses the contract                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    pause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+    
+    // liveness
+    assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
+
+    // effect
+    assert success => pausedAfter, "contract must be paused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _unpause unpauses the contract                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule unpause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    unpause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+    
+    // liveness
+    assert success <=> pausedBefore, "works if and only if the contract was paused before";
+
+    // effect
+    assert success => !pausedAfter, "contract must be unpaused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenPaused modifier can only be called if the contract is paused                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenPaused(env e) {
+    require nonpayable(e);
+
+    onlyWhenPaused@withrevert(e);
+    assert !lastReverted <=> paused(), "works if and only if the contract is paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenNotPaused(env e) {
+    require nonpayable(e);
+    
+    onlyWhenNotPaused@withrevert(e);
+    assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only _pause and _unpause can change paused status                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPauseChange(env e) {
+    method f;
+    calldataarg args;
+
+    bool pausedBefore = paused();
+    f(e, args);
+    bool pausedAfter = paused();
+
+    assert pausedBefore != pausedAfter => (
+        (!pausedAfter && f.selector == unpause().selector) ||
+        (pausedAfter && f.selector == pause().selector)
+    ), "contract's paused status can only be changed by _pause() or _unpause()";
+}