first draft of a fallback spec, with some TODOs including resolving s…

…anity on the invariant fallbackHanlderNeverSelf, adding the static Dummy to the spec, and strengthening from satisfy to assert

certora/conf/v1.5/fallback.conf

@@ -0,0 +1,37 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/harnesses/ExtensibleFallbackHandlerHarness.sol",
+        "certora/mocks/DummyHandler.sol",
+        "certora/mocks/DummyStaticHandler.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Fallback.spec",
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+
+    "java_args": [
+        " -ea -Dlevel.setup.helpers=info"
+    ],
+    "process": "emv",
+    "prover_args": [
+        " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on",
+        "-enableSolidityBasedInlining true"
+    ]
+}

certora/harnesses/ExtensibleFallbackHandlerHarness.sol

@@ -0,0 +1,15 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+import "../munged/handler/ExtensibleFallbackHandler.sol";
+import {ISafe} from "../munged/interfaces/ISafe.sol";
+
+contract ExtensibleFallbackHandlerHarness is ExtensibleFallbackHandler {
+
+    function getSafeMethod(ISafe safe, bytes4 selector) public view returns (bytes32) {
+        return safeMethods[safe][selector];
+    }
+
+    function getContextAndHandler() external view returns (ISafe safe, address sender, bool isStatic, address handler) {
+        _getContextAndHandler();
+    }
+
+}

certora/harnesses/SafeHarness.sol

@@ -1,6 +1,7 @@
 // SPDX-License-Identifier: LGPL-3.0-only
 import "../munged/Safe.sol";
 import {SafeMath} from "../munged/external/SafeMath.sol";
+import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol";
 
 contract SafeHarness is Safe {
     constructor(
@@ -65,6 +66,19 @@ contract SafeHarness is Safe {
         return getOwners().length;
     }
 
+    function getFallbackHandler() public view returns (address) {
+        address handler;
+        assembly{
+            handler := sload(FALLBACK_HANDLER_STORAGE_SLOT)
+        }
+        return handler ;
+    }
+
+    // TODO deprecate this with CVL2
+    function addressToBytes32(address addr) public pure returns (bytes32) {
+        return bytes32(uint256(uint160(addr)));
+    }
+
     function getTransactionHashPublic(
         address to,
         uint256 value,

certora/mocks/DummyHandler.sol

@@ -0,0 +1,20 @@
+// a dummy handler contract 
+import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol";
+
+contract DummyHandler is IFallbackMethod {
+    constructor(){
+        methodCalled = false ;
+    }
+
+    bool public methodCalled ;
+    function resetMethodCalled() public {
+        methodCalled = false; 
+    }
+
+    // the DUMMY method
+    function handle(ISafe safe, address sender, uint256 value, bytes calldata data) external override returns (bytes memory result) {
+        methodCalled = true ;
+
+        return "Hello, world!"; // TODO
+    }
+}

certora/specs/v1.5/Fallback.spec

@@ -0,0 +1,80 @@
+/* A specification for the exstensible fallback handler */
+
+using ExtensibleFallbackHandlerHarness as fallbackHandler;
+using DummyHandler as dummyHandler;
+using DummyStaticHandler as dummyStaticHandler;
+using SafeHarness as safe;
+
+// ---- Methods block ----------------------------------------------------------
+methods {
+
+    function getFallbackHandler() external returns (address) envfree;
+    function addressToBytes32(address) external returns (bytes32) envfree;
+
+    function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true);
+}
+
+// ---- Functions and ghosts ---------------------------------------------------
+
+
+
+// ---- Invariants -------------------------------------------------------------
+
+
+
+// ---- Rules ------------------------------------------------------------------
+
+/// @dev fallback handler gets set by setFallbackHandler
+/// @status Done: https://prover.certora.com/output/39601/ab995049df0b454b888f3cd6a27331d5?anonymousKey=1a710fa917c8c60a9a420e026d6570d91e1e923b
+rule setFallbackIntegrity(address handler) {
+    env e;
+
+    setFallbackHandler(e,handler);
+    address this_handler = getFallbackHandler();
+
+    assert (this_handler == handler);
+}
+
+/// @dev invariant: the address in fallback handler slot is never self
+/// @status Done (?)s: https://prover.certora.com/output/39601/103eb341ceef481c830e0ba04eb06766?anonymousKey=61cb4fd6726ab3d0fad887f6393865263eecf3f0
+invariant fallbackHanlderNeverSelf()
+    getFallbackHandler() != safe ;
+
+
+/// @dev set safe method integrity: sets/modifies/removes handler  
+/// @status Done: https://prover.certora.com/output/39601/09912f9691e04917b4c0277e30ad8e38?anonymousKey=61db5fd06c13a287939455e3a531ff841442ee2e
+rule setSafeMethodIntegrity(bytes4 selector, address newMethod_addr) {
+    env e; 
+
+    bytes32 newMethod = addressToBytes32(newMethod_addr);
+
+    fallbackHandler.setSafeMethod(e,selector,newMethod);
+    bytes32 this_method = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
+
+    assert (newMethod == this_method);
+}
+
+
+/// @dev a handler, once set via setSafeMethod, is possible to call
+/// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518
+rule hanlderCallableIfSet(bytes4 selector,method f) filtered { f -> f.isFallback } {
+    env e;
+
+    // the fallback handler is in the scene
+    require (getFallbackHandler() == fallbackHandler);
+
+    // the dummy (sub) handler is a valid handler for this safe
+    bytes32 dummy_bytes = addressToBytes32(dummyHandler); // TODO to_bytes32 from CVL2
+    //  bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call
+    fallbackHandler.setSafeMethod(e,selector,dummy_bytes); // we've set the dummy as a handler
+
+    // reset the check to see if dummy handler has been called
+    dummyHandler.resetMethodCalled(e);
+
+    // call the fallback method of the Safe contract
+    calldataarg args ;
+    f(e,args);
+
+    // there is an execution path that calls the connected dummy handler
+    satisfy (dummyHandler.methodCalled(e));
+}