diff --git a/modules/passkey/certora/confs/GetConfigurationConf.conf b/modules/passkey/certora/conf/GetConfigurationConf.conf similarity index 91% rename from modules/passkey/certora/confs/GetConfigurationConf.conf rename to modules/passkey/certora/conf/GetConfigurationConf.conf index 20aebd2f..13e8417f 100644 --- a/modules/passkey/certora/confs/GetConfigurationConf.conf +++ b/modules/passkey/certora/conf/GetConfigurationConf.conf @@ -3,7 +3,7 @@ "files": [ "certora/munged/SafeWebAuthnSignerSingleton.sol", "certora/harnesses/GetConfigurationProxyHarness.sol", - "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol" + "contracts/SafeWebAuthnSignerFactory.sol" ], "link": [ "GetConfigurationProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton" diff --git a/modules/passkey/certora/confs/GetSigner.conf b/modules/passkey/certora/conf/GetSigner.conf similarity index 81% rename from modules/passkey/certora/confs/GetSigner.conf rename to modules/passkey/certora/conf/GetSigner.conf index b5e6ef93..6b7129e7 100644 --- a/modules/passkey/certora/confs/GetSigner.conf +++ b/modules/passkey/certora/conf/GetSigner.conf @@ -2,8 +2,8 @@ "assert_autofinder_success": true, "files": [ "certora/harnesses/GetSignerHarness.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" ], "hashing_length_bound": "4694", "link": [ diff --git a/modules/passkey/certora/confs/ProxySimulator.conf b/modules/passkey/certora/conf/ProxySimulator.conf similarity index 80% rename from modules/passkey/certora/confs/ProxySimulator.conf rename to modules/passkey/certora/conf/ProxySimulator.conf index c70bb3af..2f82f8ca 100644 --- a/modules/passkey/certora/confs/ProxySimulator.conf +++ b/modules/passkey/certora/conf/ProxySimulator.conf @@ -2,9 +2,9 @@ "assert_autofinder_success": true, "files": [ "certora/harnesses/ProxySimulator.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol", + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol" ], "hashing_length_bound": "2048", diff --git a/modules/passkey/certora/confs/SafeWebAuthnSignerFactory.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf similarity index 87% rename from modules/passkey/certora/confs/SafeWebAuthnSignerFactory.conf rename to modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf index 33490caf..4c822338 100644 --- a/modules/passkey/certora/confs/SafeWebAuthnSignerFactory.conf +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerFactory.conf @@ -3,8 +3,8 @@ "files": [ "certora/harnesses/FactoryHarnessForSignerConsistency.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" ], "link": [ "FactoryHarnessForSignerConsistency:SINGLETON=SafeWebAuthnSignerSingleton" diff --git a/modules/passkey/certora/confs/SafeWebAuthnSignerProxy.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf similarity index 75% rename from modules/passkey/certora/confs/SafeWebAuthnSignerProxy.conf rename to modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf index 2affd152..c8f57c86 100644 --- a/modules/passkey/certora/confs/SafeWebAuthnSignerProxy.conf +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerProxy.conf @@ -1,9 +1,9 @@ { "assert_autofinder_success": true, "files": [ - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol" + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol" ], "link": [ "SafeWebAuthnSignerProxy:_VERIFIERS=P256", diff --git a/modules/passkey/certora/confs/SafeWebAuthnSignerSingleton.conf b/modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf similarity index 75% rename from modules/passkey/certora/confs/SafeWebAuthnSignerSingleton.conf rename to modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf index 892ba415..078e8d80 100644 --- a/modules/passkey/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/modules/passkey/certora/conf/SafeWebAuthnSignerSingleton.conf @@ -1,9 +1,9 @@ { "assert_autofinder_success": true, "files": [ - "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol", + "contracts/SafeWebAuthnSignerFactory.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol" ], "link": [ diff --git a/modules/passkey/certora/confs/SignerCreationCantOverride.conf b/modules/passkey/certora/conf/SignerCreationCantOverride.conf similarity index 81% rename from modules/passkey/certora/confs/SignerCreationCantOverride.conf rename to modules/passkey/certora/conf/SignerCreationCantOverride.conf index 5ca4866b..afdffaab 100644 --- a/modules/passkey/certora/confs/SignerCreationCantOverride.conf +++ b/modules/passkey/certora/conf/SignerCreationCantOverride.conf @@ -5,9 +5,9 @@ ], "files": [ "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", - "modules/passkey/contracts/libraries/P256.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol", + "contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol" ], "hashing_length_bound": "912", diff --git a/modules/passkey/certora/confs/SingletonIsValidSignatureRevertingConditions.conf b/modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf similarity index 75% rename from modules/passkey/certora/confs/SingletonIsValidSignatureRevertingConditions.conf rename to modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf index 967f03bf..41adb169 100644 --- a/modules/passkey/certora/confs/SingletonIsValidSignatureRevertingConditions.conf +++ b/modules/passkey/certora/conf/SingletonIsValidSignatureRevertingConditions.conf @@ -1,9 +1,9 @@ { "assert_autofinder_success": true, "files": [ - "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/libraries/P256.sol", + "contracts/SafeWebAuthnSignerFactory.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol" ], "loop_iter": "6", diff --git a/modules/passkey/certora/confs/ValidSignatureForSignerIntegrity.conf b/modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf similarity index 84% rename from modules/passkey/certora/confs/ValidSignatureForSignerIntegrity.conf rename to modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf index a1be3ce2..0552db59 100644 --- a/modules/passkey/certora/confs/ValidSignatureForSignerIntegrity.conf +++ b/modules/passkey/certora/conf/ValidSignatureForSignerIntegrity.conf @@ -3,8 +3,8 @@ "files": [ "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol" + "contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerProxy.sol" ], "link": [ "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" diff --git a/modules/passkey/certora/confs/VerifyEQtoIsValidSignatureForSigner.conf b/modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf similarity index 93% rename from modules/passkey/certora/confs/VerifyEQtoIsValidSignatureForSigner.conf rename to modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf index d0700ebb..0192eaa7 100644 --- a/modules/passkey/certora/confs/VerifyEQtoIsValidSignatureForSigner.conf +++ b/modules/passkey/certora/conf/VerifyEQtoIsValidSignatureForSigner.conf @@ -3,7 +3,7 @@ "dynamic_bound": "1", "files": [ "certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol", - "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", + "contracts/SafeWebAuthnSignerSingleton.sol", "certora/munged/SafeWebAuthnSignerProxy.sol", "certora/munged/WebAuthn.sol", "certora/harnesses/WebAuthnHarnessWithMunge.sol" diff --git a/modules/passkey/certora/confs/WebAuthn.conf b/modules/passkey/certora/conf/WebAuthn.conf similarity index 100% rename from modules/passkey/certora/confs/WebAuthn.conf rename to modules/passkey/certora/conf/WebAuthn.conf diff --git a/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol b/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol index d8ae306c..fd584e3a 100644 --- a/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol +++ b/modules/passkey/certora/harnesses/FactoryHarnessForSignerConsistency.sol @@ -2,8 +2,8 @@ pragma solidity >=0.8.0; import {SafeWebAuthnSignerFactory} from "../munged/FactoryForSignerConsistency.sol"; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; contract FactoryHarnessForSignerConsistency is SafeWebAuthnSignerFactory { //Harness diff --git a/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol b/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol index 2f70797f..05c17bc1 100644 --- a/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol +++ b/modules/passkey/certora/harnesses/GetConfigurationProxyHarness.sol @@ -2,7 +2,7 @@ /* solhint-disable no-complex-fallback */ pragma solidity >=0.8.0; -import {P256} from "modules/passkey/contracts/libraries/WebAuthn.sol"; +import {P256} from "../../contracts/libraries/WebAuthn.sol"; /** * @title Safe WebAuthn Signer Proxy diff --git a/modules/passkey/certora/harnesses/GetSignerHarness.sol b/modules/passkey/certora/harnesses/GetSignerHarness.sol index cf156afe..8766656d 100644 --- a/modules/passkey/certora/harnesses/GetSignerHarness.sol +++ b/modules/passkey/certora/harnesses/GetSignerHarness.sol @@ -2,8 +2,8 @@ pragma solidity >=0.8.0; import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; contract GetSignerHarness is SafeWebAuthnSignerFactory { function getSignerHarnessed(uint256 x, uint256 y, P256.Verifiers verifiers) public view returns (uint256 value) { diff --git a/modules/passkey/certora/harnesses/ProxySimulator.sol b/modules/passkey/certora/harnesses/ProxySimulator.sol index dcfe8279..4d5bec7b 100644 --- a/modules/passkey/certora/harnesses/ProxySimulator.sol +++ b/modules/passkey/certora/harnesses/ProxySimulator.sol @@ -2,7 +2,7 @@ /* solhint-disable no-complex-fallback */ pragma solidity >=0.8.0; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; contract ProxySimulator { address internal _proxy; diff --git a/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index 97279978..c7a12e1c 100644 --- a/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/modules/passkey/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -2,8 +2,8 @@ pragma solidity >=0.8.0; import {SafeWebAuthnSignerFactory} from "../munged/SafeWebAuthnSignerFactory.sol"; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { //Harness diff --git a/modules/passkey/certora/harnesses/Utilities.sol b/modules/passkey/certora/harnesses/Utilities.sol index c0404009..1f2b7b30 100644 --- a/modules/passkey/certora/harnesses/Utilities.sol +++ b/modules/passkey/certora/harnesses/Utilities.sol @@ -1,4 +1,4 @@ -import {P256} from "../../modules/passkey/contracts/libraries/WebAuthn.sol"; +import {P256} from "../../contracts/libraries/WebAuthn.sol"; interface IConfigHolder { function getConfiguration() external pure returns (uint256 x, uint256 y, P256.Verifiers verifiers); diff --git a/modules/passkey/certora/harnesses/WebAuthnHarness.sol b/modules/passkey/certora/harnesses/WebAuthnHarness.sol index c4a668e6..2f178713 100644 --- a/modules/passkey/certora/harnesses/WebAuthnHarness.sol +++ b/modules/passkey/certora/harnesses/WebAuthnHarness.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity ^0.8.0; -import {P256, WebAuthn} from "../../modules/passkey/contracts/libraries/WebAuthn.sol"; +import {P256, WebAuthn} from "../../contracts/libraries/WebAuthn.sol"; contract WebAuthnHarness { mapping(bytes32 => mapping(bytes32 => string)) symbolicClientDataJson; diff --git a/modules/passkey/certora/munged/FactoryForSignerConsistency.sol b/modules/passkey/certora/munged/FactoryForSignerConsistency.sol index 5334ef2e..71582890 100644 --- a/modules/passkey/certora/munged/FactoryForSignerConsistency.sol +++ b/modules/passkey/certora/munged/FactoryForSignerConsistency.sol @@ -1,10 +1,10 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity >=0.8.0; -import {ISafeSignerFactory} from "../../modules/passkey/contracts/interfaces/ISafeSignerFactory.sol"; -import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"; -import {SafeWebAuthnSignerSingleton} from "../../modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol"; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; +import {ISafeSignerFactory} from "../../contracts/interfaces/ISafeSignerFactory.sol"; +import {SafeWebAuthnSignerProxy} from "../../contracts/SafeWebAuthnSignerProxy.sol"; +import {SafeWebAuthnSignerSingleton} from "../../contracts/SafeWebAuthnSignerSingleton.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; /** * @title Safe WebAuthn Signer Factory diff --git a/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol b/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol index e10159be..9f6ef9b7 100644 --- a/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol +++ b/modules/passkey/certora/munged/SafeWebAuthnSignerFactory.sol @@ -1,10 +1,10 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity >=0.8.0; -import {ISafeSignerFactory} from "../../modules/passkey/contracts/interfaces/ISafeSignerFactory.sol"; +import {ISafeSignerFactory} from "../../contracts/interfaces/ISafeSignerFactory.sol"; import {SafeWebAuthnSignerProxy} from "./SafeWebAuthnSignerProxy.sol"; import {SafeWebAuthnSignerSingleton} from "./SafeWebAuthnSignerSingleton.sol"; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; /** * @title Safe WebAuthn Signer Factory diff --git a/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol b/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol index 4922d0a4..b37f59a6 100644 --- a/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol +++ b/modules/passkey/certora/munged/SafeWebAuthnSignerSingleton.sol @@ -1,8 +1,8 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity >=0.8.0; -import {SignatureValidator} from "../../modules/passkey/contracts/base/SignatureValidator.sol"; -import {P256, WebAuthn} from "../../modules/passkey/contracts/libraries/WebAuthn.sol"; +import {SignatureValidator} from "../../contracts/base/SignatureValidator.sol"; +import {P256, WebAuthn} from "../../contracts/libraries/WebAuthn.sol"; /** * @title Safe WebAuthn Signer Singleton diff --git a/modules/passkey/certora/munged/WebAuthn.sol b/modules/passkey/certora/munged/WebAuthn.sol index 05fceaab..14daefb6 100644 --- a/modules/passkey/certora/munged/WebAuthn.sol +++ b/modules/passkey/certora/munged/WebAuthn.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity ^0.8.0; -import {P256} from "../../modules/passkey/contracts/libraries/P256.sol"; +import {P256} from "../../contracts/libraries/P256.sol"; /** * @title WebAuthn Signature Verification diff --git a/modules/passkey/certora/requirements.txt b/modules/passkey/certora/requirements.txt index df37fea8..100d68e2 100644 --- a/modules/passkey/certora/requirements.txt +++ b/modules/passkey/certora/requirements.txt @@ -1 +1 @@ -certora-cli==7.10.1 +certora-cli==7.14.2