{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":596388676,"defaultBranch":"main","name":"WrappedEther.dfy","ownerLogin":"Consensys","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-02-02T04:15:31.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/10818037?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715902707.0","currentOid":""},"activityList":{"items":[{"before":"13743566395683ada6bc3d20229c9c667f31ba60","after":"69552a4c87ab752fdc90474b86f4ddf3236acab5","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-06-04T07:35:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"booleanfunction","name":"Joanne Fuller","path":"/booleanfunction","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43776922?s=80&v=4"},"commit":{"message":"fix block_0_0x0a59 in main (by splitting)","shortMessageHtmlLink":"fix block_0_0x0a59 in main (by splitting)"}},{"before":"3b207ffabb2898b6da8b999028c312fdbaf8eaa1","after":"13743566395683ada6bc3d20229c9c667f31ba60","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-06-04T06:55:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"booleanfunction","name":"Joanne Fuller","path":"/booleanfunction","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43776922?s=80&v=4"},"commit":{"message":"fix block_0_0x0a0b in main (split into 2 blocks)","shortMessageHtmlLink":"fix block_0_0x0a0b in main (split into 2 blocks)"}},{"before":"62f3cc1359772fc2e4d8836dfbf06b3b091ca175","after":"3b207ffabb2898b6da8b999028c312fdbaf8eaa1","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-06-04T06:00:54.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"booleanfunction","name":"Joanne Fuller","path":"/booleanfunction","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43776922?s=80&v=4"},"commit":{"message":"fix block_0_0x0a93 in main","shortMessageHtmlLink":"fix block_0_0x0a93 in main"}},{"before":"e6af59e6dff99a78a563da78779fa0cc2ab0028a","after":"62f3cc1359772fc2e4d8836dfbf06b3b091ca175","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-06-04T03:41:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"booleanfunction","name":"Joanne Fuller","path":"/booleanfunction","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/43776922?s=80&v=4"},"commit":{"message":"fix block_0_0x0407 in allowance","shortMessageHtmlLink":"fix block_0_0x0407 in allowance"}},{"before":"7617730d9e6eaf34efe324d807a21db0b54bc00b","after":"e6af59e6dff99a78a563da78779fa0cc2ab0028a","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-28T01:46:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Fixes for `allowance` and `approve`\n\nTwo example fixes for these modules.","shortMessageHtmlLink":"Fixes for <code>allowance</code> and <code>approve</code>"}},{"before":"181a02b7c0970c325d08e9d341d148c20aca10f6","after":"7617730d9e6eaf34efe324d807a21db0b54bc00b","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-28T01:40:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Update proof to use `evm-dafny` submodule\n\nPreviously, the proof was using a version of the `evm-dafny` which was\nexternal to this repository.  Now, its using the version given as a\nsubmodule.","shortMessageHtmlLink":"Update proof to use <code>evm-dafny</code> submodule"}},{"before":"bcbf955dd5c0e35012ece734e91343c4a553e397","after":"181a02b7c0970c325d08e9d341d148c20aca10f6","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-27T00:57:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Reset proof\n\nThis regenerates the proof using the latest version of `DevmProofGen`.\nThis includes some fixes, though of course we have now lost all our\nchanges :)","shortMessageHtmlLink":"Reset proof"}},{"before":"4aea1f5fcda078c100ea8fe846d239249c562bc4","after":"bcbf955dd5c0e35012ece734e91343c4a553e397","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-21T06:25:12.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Update `run.sh`\n\nThis just makes it a little easier to switch between different versions\nof Z3 and/or Dafny.","shortMessageHtmlLink":"Update <code>run.sh</code>"}},{"before":"99e4fd9524c6ff6c633c66b310d34d620105410a","after":"4aea1f5fcda078c100ea8fe846d239249c562bc4","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-19T21:10:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Updated proof\n\nThis updates the proof to include full stack information within internal\ncomments; also, to apply the automatic mask conversion for `And`\nbytecodes.","shortMessageHtmlLink":"Updated proof"}},{"before":"5fe526c9dbd5e9e2c26096fe47eebb3544034a4c","after":"99e4fd9524c6ff6c633c66b310d34d620105410a","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-16T23:52:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Initial proof update\n\nThis is really an experimental update to the proof.  I'm not planning to\nwork off of this, but rather to figure out what else is needed to make\nprogress.","shortMessageHtmlLink":"Initial proof update"}},{"before":null,"after":"5fe526c9dbd5e9e2c26096fe47eebb3544034a4c","ref":"refs/heads/23-update-proof-to-check-for-underflow-overflow","pushedAt":"2024-05-16T23:38:27.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Merge pull request #22 from Consensys/18-sum\n\nFixes #18","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2094962693\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/22\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/pull/22/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/pull/22\">#22</a> from Consensys/18-sum"}},{"before":"7feaab4884898b617e450ca59818c2867177c2fa","after":null,"ref":"refs/heads/18-sum","pushedAt":"2024-01-22T23:30:36.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"}},{"before":"b3dbb6fe93375edb406ff454799a633bf2978dfd","after":"5fe526c9dbd5e9e2c26096fe47eebb3544034a4c","ref":"refs/heads/main","pushedAt":"2024-01-22T23:30:33.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Merge pull request #22 from Consensys/18-sum\n\nFixes #18","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2094962693\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/22\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/pull/22/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/pull/22\">#22</a> from Consensys/18-sum"}},{"before":"b899729d3b4c309fc978f930c7d5dbea0c64b4d0","after":"b3dbb6fe93375edb406ff454799a633bf2978dfd","ref":"refs/heads/main","pushedAt":"2024-01-22T23:30:16.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Everything verifies except `util`\n\nAt this stage, everything is now verifying except three methods in\n`util`.  At least two of these are known to be hard.","shortMessageHtmlLink":"Everything verifies except <code>util</code>"}},{"before":null,"after":"7feaab4884898b617e450ca59818c2867177c2fa","ref":"refs/heads/18-sum","pushedAt":"2024-01-22T23:28:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Fixes #18\n\nThis fixes an issue with verifying `WrappedEtherModel` under Dafny\n    v4.4.0.  The key problem is that you cannot use non-deterministic\nchoice with a `function`.","shortMessageHtmlLink":"<span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #18.\">Fixes</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1900529300\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/18\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/issues/18/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/issues/18\">#18</a>"}},{"before":"15ad313468ecad2cd62f7bf7ec9fb30d0c8b55b1","after":null,"ref":"refs/heads/18-the-value-of-a-let-such-that-expression-must-be-uniquely-determined","pushedAt":"2024-01-22T23:24:49.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"}},{"before":"b3dbb6fe93375edb406ff454799a633bf2978dfd","after":"b899729d3b4c309fc978f930c7d5dbea0c64b4d0","ref":"refs/heads/main","pushedAt":"2024-01-22T23:24:39.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Merge pull request #21 from Consensys/18-the-value-of-a-let-such-that-expression-must-be-uniquely-determined\n\nFix #18","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2094956420\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/21\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/pull/21/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/pull/21\">#21</a> from Consensys/18-the-value-of-a-let-such-that…"}},{"before":"b3dbb6fe93375edb406ff454799a633bf2978dfd","after":"15ad313468ecad2cd62f7bf7ec9fb30d0c8b55b1","ref":"refs/heads/18-the-value-of-a-let-such-that-expression-must-be-uniquely-determined","pushedAt":"2024-01-22T23:24:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Fix #18\n\nThis fixes an issue with verifying `WrappedEtherModel` under Dafny\nv4.4.0.  The key problem is that you cannot use non-deterministic choice\nwithin a `function`.","shortMessageHtmlLink":"<span class=\"issue-keyword tooltipped tooltipped-se\" aria-label=\"This commit closes issue #18.\">Fix</span> <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1900529300\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/18\" data-hovercard-type=\"issue\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/issues/18/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/issues/18\">#18</a>"}},{"before":null,"after":"b3dbb6fe93375edb406ff454799a633bf2978dfd","ref":"refs/heads/18-the-value-of-a-let-such-that-expression-must-be-uniquely-determined","pushedAt":"2024-01-22T23:20:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Everything verifies except `util`\n\nAt this stage, everything is now verifying except three methods in\n`util`.  At least two of these are known to be hard.","shortMessageHtmlLink":"Everything verifies except <code>util</code>"}},{"before":"4aac02467dc0dc25052f2ad611885228f9812c4f","after":"b3dbb6fe93375edb406ff454799a633bf2978dfd","ref":"refs/heads/main","pushedAt":"2023-12-11T08:15:31.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Everything verifies except `util`\n\nAt this stage, everything is now verifying except three methods in\n`util`.  At least two of these are known to be hard.","shortMessageHtmlLink":"Everything verifies except <code>util</code>"}},{"before":"52587d5dcf59fa9599df35208b3cc35ba5768c62","after":"4aac02467dc0dc25052f2ad611885228f9812c4f","ref":"refs/heads/main","pushedAt":"2023-12-11T07:04:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Termination of `symbol` complete\n\nThis completes proof of the `symbol` public function.","shortMessageHtmlLink":"Termination of <code>symbol</code> complete"}},{"before":"b87069646fa1291029c4b993aa5470f621bb7af2","after":"52587d5dcf59fa9599df35208b3cc35ba5768c62","ref":"refs/heads/main","pushedAt":"2023-12-11T00:08:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Working through termination of symbol\n\nThis is almost complete ... (he says)","shortMessageHtmlLink":"Working through termination of symbol"}},{"before":"0294bb2c61b3382e08e7a8251f397c7039f04a54","after":"b87069646fa1291029c4b993aa5470f621bb7af2","ref":"refs/heads/main","pushedAt":"2023-12-05T23:05:50.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Working on termination in `symbol`\n\nCurrently, need to properly initialise loop counters in block `0x0310`.\nIn particular, the upper bound comes from ... where exactly?","shortMessageHtmlLink":"Working on termination in <code>symbol</code>"}},{"before":"9190e489e406e102f83c49ef96856eadb2921253","after":"0294bb2c61b3382e08e7a8251f397c7039f04a54","ref":"refs/heads/main","pushedAt":"2023-12-05T04:30:03.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Tweaking run script\n\nThis tweaks the run script to help consider different options.  At this\nstage, there are still two outstanding which cannot be made to verify.","shortMessageHtmlLink":"Tweaking run script"}},{"before":"261fb0d97b55b803808b7b552c59c26729118543","after":"9190e489e406e102f83c49ef96856eadb2921253","ref":"refs/heads/main","pushedAt":"2023-12-04T07:52:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Making progress on util","shortMessageHtmlLink":"Making progress on util"}},{"before":"d2037080459befb984df4cc56d237679aa98004f","after":"261fb0d97b55b803808b7b552c59c26729118543","ref":"refs/heads/main","pushedAt":"2023-12-04T04:33:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"`name()` now verifies","shortMessageHtmlLink":"<code>name()</code> now verifies"}},{"before":"2c2f59681882bccb4b53df4409b15a52c9e525ee","after":"d2037080459befb984df4cc56d237679aa98004f","ref":"refs/heads/main","pushedAt":"2023-11-28T16:34:27.000Z","pushType":"pr_merge","commitsCount":10,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Merge pull request #20 from Consensys/19-recreate-proof\n\n19 recreate proof","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2014841904\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Consensys/WrappedEther.dfy/issues/20\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Consensys/WrappedEther.dfy/pull/20/hovercard\" href=\"https://github.com/Consensys/WrappedEther.dfy/pull/20\">#20</a> from Consensys/19-recreate-proof"}},{"before":"443c5f1484f8a6749f02ffd078a3406873c58bc6","after":"d7eb54f28636fecef0ce56d6697e274b323eac63","ref":"refs/heads/19-recreate-proof","pushedAt":"2023-11-28T16:31:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Tidying up new proof\n\nThis tidies up the new proof which was regenerated using the\nDafnyProofGenerator.  The proof still does not go through.  However, a\nlot of it does :)","shortMessageHtmlLink":"Tidying up new proof"}},{"before":"044011801543c17cad76d8e31539dbcdfeda4b1e","after":"443c5f1484f8a6749f02ffd078a3406873c58bc6","ref":"refs/heads/19-recreate-proof","pushedAt":"2023-11-03T08:17:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"More things are passing ... slowly.\n\nIt looks like:\n\n(1) Generally, having mid-way asserts is good\n\n(2) split here can be useful.","shortMessageHtmlLink":"More things are passing ... slowly."}},{"before":"3c561d82a9ebb3f493efda1a2bdd4f57e048dccf","after":"044011801543c17cad76d8e31539dbcdfeda4b1e","ref":"refs/heads/19-recreate-proof","pushedAt":"2023-11-03T07:03:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"DavePearce","name":"David Pearce","path":"/DavePearce","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/484459?s=80&v=4"},"commit":{"message":"Various improvements\n\nHave got stuck working through the util file.  Am attempting to tweak\nthe DafnyEVM to reduce overhead.  In particular, for the `MStore`\nbytecode which appears to cause problems.","shortMessageHtmlLink":"Various improvements"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEW7l2PgA","startCursor":null,"endCursor":null}},"title":"Activity · Consensys/WrappedEther.dfy"}