Skip to content

Commit

Permalink
Update SafeWebAuthnSignerFactory.spec
Browse files Browse the repository at this point in the history
  • Loading branch information
liav-certora committed Jun 9, 2024
1 parent c81f4a6 commit d208c5a
Showing 1 changed file with 0 additions and 20 deletions.
20 changes: 0 additions & 20 deletions certora/specs/SafeWebAuthnSignerFactory.spec
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,6 @@ rule deterministicSigner()

ghost mathint numOfCreation;
ghost mapping(address => uint) address_map;
ghost address createdAddress;
ghost bool validValue;

hook EXTCODESIZE(address addr) uint v {
Expand All @@ -115,7 +114,6 @@ hook EXTCODESIZE(address addr) uint v {
hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v {
numOfCreation = numOfCreation + 1;
address_map[v] = length;
createdAddress = v;
}

rule SignerCreationCantOverride()
Expand Down Expand Up @@ -225,21 +223,3 @@ rule getSignerRevertingConditions {

assert lastReverted <=> triedTransferringEth;
}

rule createSignerRevertingConditions {
env e;
uint256 x;
uint256 y;
P256.Verifiers verifiers;

address signer = getSigner(e, x, y, verifiers);
bool signerHasNoCode = hasNoCode(signer);

bool triedTransferringEth = e.msg.value != 0;

createSigner@withrevert(e, x, y, verifiers);

bool notCreatedSigner = signerHasNoCode && (createdAddress != signer);

assert lastReverted <=> (triedTransferringEth || notCreatedSigner);
}

0 comments on commit d208c5a

Please sign in to comment.