Commit Graph

161 Commits

Author SHA1 Message Date
0deaee1217 Added unfinished invariant regarding user token sums and totalSupply 2022-05-10 17:36:19 -07:00
2fc3a5d4b8 implemented independence rule 2022-05-09 17:54:01 -04:00
da0fdc1aa0 harness setup for ERC1155Supply 2022-05-09 17:30:57 -04:00
aafb14461b made the spec run 2022-05-06 14:12:32 -04:00
02de598056 removed sanity 2022-04-11 13:56:34 -07:00
135e21f35d comment cleanup 2022-04-11 13:26:46 -07:00
6662d0556f verify all - rules passing 2022-04-11 12:46:56 -07:00
d1454932b2 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20 2022-04-10 19:55:27 -07:00
cab9b09b7b rough contracts all finished 2022-04-10 19:55:23 -07:00
741e9a8b6d timelock function moved 2022-04-08 20:57:53 +01:00
66c72f2b5d CI preparations 2022-04-08 20:52:38 +01:00
163a76f436 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into certora/erc20 2022-04-08 15:38:32 +01:00
75417fbf9f finilized rules 2022-04-08 15:38:26 +01:00
ec8f03ee96 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20 2022-04-07 15:50:14 -07:00
140df5b7ce everything except Alex fix for totalVotes_sums_accounts 2022-04-07 15:49:37 -07:00
da674eced1 typos and cleaning 2022-04-04 22:34:51 +01:00
479118fcd1 push to report issues 2022-04-04 21:33:31 +01:00
8c86b250bc fixed rule description 2022-04-04 21:19:54 +01:00
a0b58c3071 flashMint finished 2022-04-04 21:16:15 +01:00
fe7d42dedd Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into certora/erc20 2022-04-01 17:58:48 +01:00
44fba3e2eb ERC1155 finished 2022-04-01 17:58:41 +01:00
b2b72e7783 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20 2022-03-31 14:40:36 -07:00
22827223c0 more passing 2022-03-31 14:40:20 -07:00
033f08972f Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into certora/erc20 2022-03-31 21:08:21 +01:00
ec4e77397f AccessControl verification 2022-03-31 21:08:14 +01:00
50cf82823e one more TC cleaning 2022-03-31 21:08:00 +01:00
53b6ed80bb ERC1155 verification (not finished) 2022-03-31 21:07:28 +01:00
92f07bae1b typechecker error and skipped require bug 2022-03-30 17:12:30 -07:00
4c74b2951d Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into
remotes/origin/certora/erc20
2022-03-28 12:07:21 -07:00
3f1ee39910 call trace error 2022-03-28 12:05:33 -07:00
4b9500cf25 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into certora/erc20 2022-03-27 16:06:49 +01:00
a35ad6dfc3 wrapper and timelockController cleaning 2022-03-27 16:04:31 +01:00
140f019155 Merge branch 'certora/erc20' of github.com:Certora/openzeppelin-contracts into remotes/origin/certora/erc20 2022-03-25 12:57:21 -07:00
6895946f41 updated rules 2022-03-25 12:57:16 -07:00
5153c462d5 wrapper counterexample to check 2022-03-23 19:42:14 +00:00
8318470cca flashMint cleaning 2022-03-23 19:12:16 +00:00
faf5820f03 Fix many spelling errors (#3274) 2022-03-22 18:16:20 -03:00
8d9ab176d7 Timelock hash bug, example for Alex 2022-03-21 17:58:21 +00:00
62d60a5890 Timelock, erc20Wrapper and erc20FlashMint verification 2022-03-20 22:36:48 +00:00
7caa9bbb2c TimelockController wating for hash fix 2022-03-11 00:29:03 +00:00
1900c86c99 removed unnecessary harness from the first iteration 2022-03-08 19:58:23 +00:00
61fa061ecf erc20votes pointers workaround and preset 2022-03-08 16:38:11 +00:00
99864fd2da Merge branch 'OpenZeppelin:master' into certora/erc20 2022-03-01 14:23:25 -05:00
915ca181ba Add Certora's Governance verification rules (#2997)
Co-authored-by: Shelly Grossman <shelly@certora.com>
Co-authored-by: Aleksander Kryukov <58052996+RedLikeRosesss@users.noreply.github.com>
Co-authored-by: Michael M <91594326+MichaelMorami@users.noreply.github.com>
Co-authored-by: Aleksander Kryukov <firealexkryukov@gmail.com>
2021-12-27 19:11:59 -03:00
b5980a569c reorganized governance verification in preparation for erc20 verification 2021-12-17 09:22:06 -05:00
7912b1af7d filtered out relay, since it is havocing 2021-12-16 14:58:55 -05:00
3c150953ed harnessing fix 2021-12-03 14:52:53 -05:00
d64869545d did some harnessing 2021-12-02 16:47:18 -05:00
5888bee853 fixed executeOnly rule 2021-12-02 15:16:26 -05:00
ec5d501791 filtered out timeouts 2021-12-02 15:06:29 -05:00