Commit Graph

225 Commits

Author SHA1 Message Date
b2ec06aaf2 test matrix 2022-09-20 16:11:32 +02:00
0fa6aad5e5 Update certora harness 2022-09-20 15:12:26 +02:00
e9f53ebc02 run prettier --write 2022-09-09 13:33:55 +02:00
d98d9c03f3 Merge remote-tracking branch 'Certora/master' into formal-verification 2022-09-09 13:19:12 +02:00
24fc709533 Set up codespell (#3643) 2022-08-23 12:43:03 -03:00
2627753bfe votes solvency passing again 2022-08-12 00:32:35 -07:00
4820ed4ea8 missing erc20votes harnessing 2022-08-11 21:27:17 -07:00
4a3b0bb875 filters for skipped functions 2022-08-11 21:11:01 -07:00
3e6045155e reorganized scripts 2022-08-11 20:40:13 -07:00
1701b0c7fd fix erc1155supply vacuity, change CI solc version to 8.4 2022-06-15 17:05:12 -07:00
962a5023e6 remove commented code, fix some old scripts 2022-06-14 16:52:57 -07:00
65ab8e9ac4 Changed rule transfersHaveSameLengthInputArrays (passing) to use _ instead of holder 2022-06-07 17:51:27 -07:00
9bbc7b7eb3 Moved three transfer rules from 1155Supply spec to base 1155 spec 2022-06-07 17:32:45 -07:00
e4492aed8a Cleaned up code for rule transfersHaveSameLengthInputArrays (passing) 2022-06-07 17:26:22 -07:00
ca034ab3df Deleted unused method from GovPreventLateQuorum 2022-06-07 17:20:50 -07:00
75a3602ba6 Modified rule transfersHaveSameLengthInputArrays (passing) to limit array size 2022-06-07 17:16:45 -07:00
7946806fb3 Commented out sanity rules for the purposes of CI 2022-06-06 17:34:11 -07:00
84b371f92c Added rule transfersHaveSameLengthInputArrays (partially passing) 2022-06-06 13:54:53 -07:00
ee2f0ecb68 Improved multiple token transfer batch transfer equivalence rule 2022-06-06 13:02:41 -07:00
6a4fc6acb8 set up CI for round3 scripts 2022-06-06 12:57:50 -07:00
1aa8141b14 removed a assert failure message from an invariant in Initializable spec 2022-06-06 12:56:19 -07:00
866042d6fc Added two transfer batch transfer equivalence rules 2022-06-06 12:53:13 -07:00
234b843c36 commented out failing rules and added solc version to ERC1155 2022-06-06 15:44:07 -04:00
371818f792 Removed reference to _burn and _mint 2022-06-06 12:26:41 -07:00
3ccaf4f6d1 Updated and cleaned up rule descriptions 2022-06-06 11:50:05 -07:00
ffa3daa5d9 Modified verification scripts and Supply spec syntax 2022-06-06 11:42:42 -07:00
990fd18c21 make ERC1155Harness, set up script, and undo munging for ERC1155 2022-06-06 11:26:58 -07:00
5a7cc50974 Modified burnable verification script to follow script naming convention 2022-06-06 11:25:48 -07:00
e3341255b2 Added rule skeletons for equivalence rules 2022-06-06 11:24:50 -07:00
69d9ebfcdf Added modified scripts to run previous ERC1155 spec 2022-06-06 11:24:50 -07:00
5516589b88 final initializable spec modulo extra natspec style comments 2022-06-03 16:45:27 -07:00
6363deaedd Changed rule onlyHolderOrApprovedCanReduceBalance to include filtered block 2022-06-03 16:12:12 -07:00
b10a2b8cd3 Added burn and burnBatch to filtered block of unexpectedBalanceChange 2022-06-03 13:56:46 -07:00
bdb49654c5 Deleted redundant rule burnBatchAmountProportionalToBalanceReduction 2022-06-03 12:27:08 -07:00
bab9528dc1 Added rule comments re burn method rules holding for burnBatch method 2022-06-03 12:24:03 -07:00
93928e3e19 Added rule burnBatchOnEmptyArraysChangesNothing (passing) 2022-06-03 12:13:10 -07:00
f3f26e3ff3 Modified verification scripts to include --send_only flag 2022-06-02 14:25:08 -07:00
3eb67081f3 Added TODO show equivalence between batch and non-batch methods 2022-06-02 14:15:20 -07:00
d02c2ccab3 Added comments throughout regarding reasoning 2022-06-02 14:08:29 -07:00
27fa53bba9 added init_state axiom for sum of balances 2022-06-02 14:37:40 -04:00
b90d195c6c Added rule re burnBatch (not implemented) 2022-06-02 11:30:58 -07:00
a6863a059c Changed invariant total_supply_is_sum_of_balances (partially passing) 2022-06-02 11:30:58 -07:00
669a22e0ff remove duplicate initalize script 2022-06-01 17:39:39 -07:00
cab8e489b2 initializable final draft, ready for review 2022-06-01 17:38:28 -07:00
0119a187c1 Added rule multipleTokenBurnBurnBatchEquivalence (passing) 2022-06-01 10:34:03 -07:00
15e847c835 Added invariant balanceOfZeroAddressIsZero (partially passing) 2022-05-31 18:34:22 -07:00
8e283704c3 Modified 1155 Burnable scripts 2022-05-31 16:29:46 -07:00
38495a5026 Added rule singleTokenBurnBurnBatchEquivalence (passing) 2022-05-31 16:02:23 -07:00
f74e316422 Added rule sequentialBurnsEquivalentToSingleBurnOfSum (passing) 2022-05-31 15:12:48 -07:00
2a73da9f67 Added rule burnBatchAmountProportionalToBalanceReduction (unimplemented) 2022-05-31 14:13:44 -07:00