Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
liav-certora committed Jun 13, 2024
1 parent 08594cc commit ed1bf4d
Show file tree
Hide file tree
Showing 5 changed files with 0 additions and 154 deletions.
29 changes: 0 additions & 29 deletions certora/confs/ProxySimulator.conf

This file was deleted.

7 changes: 0 additions & 7 deletions certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol
Original file line number Diff line number Diff line change
Expand Up @@ -29,11 +29,4 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory {
require(success);
magicValue = abi.decode(result, (bytes4));
}

// /**
// munge to pass the SignerCreationCantOverride rule.
// */
// function _hasNoCode(address account) internal view override returns (bool result) {
// return account.code.length > 0;
// }
}
24 changes: 0 additions & 24 deletions certora/helpers/ProxySimulator.sol

This file was deleted.

56 changes: 0 additions & 56 deletions certora/specs/ProxySimulator.spec

This file was deleted.

38 changes: 0 additions & 38 deletions certora/specs/SafeWebAuthnSignerSingleton.spec
Original file line number Diff line number Diff line change
Expand Up @@ -84,44 +84,6 @@ rule verifyIsValidSignatureAreEqual(env e){
(magicValue_hashed == to_bytes4(0) && magicValue_message == to_bytes4(0));
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
Once signer passed isValidSignature it will never fail on it after any call
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule verifyIsValidSignatureWillContinueToSucceed(){
env e;
env e1;
env e2;
env e3;
require e1.msg.value == 0 && e2.msg.value == 0 && e3.msg.value == 0;

method f;
calldataarg args;

bytes32 message;
WebAuthn.Signature sigStruct;
bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct);

bytes32 message3;
WebAuthn.Signature sigStruct3;
bytes signature3 = WebAuthnHarness.encodeSignature(e, sigStruct3);

bytes4 firstVerified = isValidSignature@withrevert(e1, message, signature);
bool firstReverted = lastReverted;

f(e, args);
// isValidSignature(e3, message3, signature3);

bytes4 secondVerify = isValidSignature@withrevert(e2, message, signature);
bool secondRevert = lastReverted;

assert firstReverted == secondRevert;
assert (!firstReverted && !secondRevert) => (firstVerified == secondVerify);
satisfy true;
}

rule isValidSignatureRevertingConditions {
env e;
bytes32 message;
Expand Down

0 comments on commit ed1bf4d

Please sign in to comment.