Skip to content

Commit

Permalink
Updated comment
Browse files Browse the repository at this point in the history
  • Loading branch information
remedcu committed Jul 16, 2024
1 parent ef7b231 commit 636e169
Showing 1 changed file with 10 additions and 28 deletions.
38 changes: 10 additions & 28 deletions modules/4337/certora/harnesses/Account.sol
Original file line number Diff line number Diff line change
Expand Up @@ -55,40 +55,22 @@ contract Account is Safe {
}

/*
Actual Signature:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000e7 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012b 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 efbeef" // length of bytes + data of bytes of signature 3
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef
This function is used to calculate the hash of the signatures in a standard way. This will result in signatures having possible excess data to result in the same hash
as the same signatures without the excess data. This is required for formal verification.
With Excess Data Type 1:
Actual Signature:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000e7 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012b 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 efbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 3 + excess data
"0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeefdeadbeefdeadbeefdeadbeef
0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000041000000000000000000000000000000000000000000000000000000000000000004deadbeef
With Excess Data Type 2:
With Excess Data:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000eb 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012f 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 efbeef" // length of bytes + data of bytes of signature 3
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000eb000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012f000000000000000000000000000000000000000000000000000000000000000004deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef
"0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000004 deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data
All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7
Both will have the same canonical hash: 0xc860b1a81652620308a8138a17ef5105d9b18e6e766516ffd3de9897260d1320
*/
function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) {
uint256 dynamicOffset = safeThreshold * 0x41;
Expand Down

0 comments on commit 636e169

Please sign in to comment.