.

certora/confs/SafeWebAuthnSignerProxy.conf

@@ -3,8 +3,6 @@
     "files": [
         "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
         "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
-        //"certora/harnesses/ERC20Like/DummyWeth.sol",
-		//"certora/harnesses/Utilities.sol",
         "modules/passkey/contracts/libraries/P256.sol"
     ],
     "link": [

certora/specs/SafeWebAuthnSignerProxy.spec

@@ -1,50 +1,13 @@
-/* Setup Artifacts
-import "ERC20/erc20cvl.spec";
-import "ERC20/WETHcvl.spec";
-import "ERC721/erc721.spec";
-import "ERC1967/erc1967.spec";
-import "PriceAggregators/chainlink.spec";
-import "PriceAggregators/tellor.spec";
-
-import "spec_utils/problems.spec";
-import "spec_utils/unresolved.spec";
-import "spec_utils/optimizations.spec";
-
-import "spec_utils/generic.spec"; // pick additional rules from here
-
-use builtin rule sanity filtered { f -> f.contract == currentContract }
-
-use builtin rule hasDelegateCalls filtered { f -> f.contract == currentContract }
-use builtin rule msgValueInLoopRule;
-use builtin rule viewReentrancy;
-use rule privilegedOperation filtered { f -> f.contract == currentContract }
-use rule timeoutChecker filtered { f -> f.contract == currentContract }
-use rule simpleFrontRunning filtered { f -> f.contract == currentContract }
-use rule noRevert filtered { f -> f.contract == currentContract }
-use rule alwaysRevert filtered { f -> f.contract == currentContract }
-*/
 using SafeWebAuthnSignerSingleton as SafeWebAuthnSignerSingleton;
 
+persistent ghost uint delegateSuccess;
+
 hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {
     // DELEGATECALL is used in this contract, but it only ever calls into the singleton.
     assert (executingContract != currentContract || addr == SafeWebAuthnSignerSingleton,
         "we should only `delegatecall` into the singleton."
     );
-}
-
-/*
-Property 12. Proxy - Delegate Call Integrity (calls the Singleton)
-Hooking on delegate calls will make sure we'll get a violation if the singleton isn't the contract called.
-Rule verified.
-*/
-rule delegateCallsOnlyToSingleton {
-    env e;
-    method f;
-    calldataarg args;
-
-    f(e, args);
-
-    assert true;
+    delegateSuccess = rc;
 }
 
 /*
@@ -74,3 +37,31 @@ rule configParametersImmutability {
            yBefore == yAfter &&
            verifiersBefore == verifiersAfter;
 }
+
+/*
+Property 12. Proxy - Delegate Call Integrity (calls the Singleton)
+Hooking on delegate calls will make sure we'll get a violation if the singleton isn't the contract called.
+Rule verified.
+*/
+rule delegateCallsOnlyToSingleton {
+    env e;
+    method f;
+    calldataarg args;
+
+    f(e, args);
+
+    assert true;
+}
+
+/*
+Property 13. Proxy - Fallback reverting conditions.
+Fallback reverts iff the delegatecall didn't succeed. Data manipulation does not revert.
+Rule verified.
+*/
+rule fallbackRevertingConditions(method f, calldataarg args) filtered { f -> f.isFallback } {
+    env e;
+
+    f@withrevert(e, args);
+
+    assert lastReverted <=> delegateSuccess == 0;
+}