{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":67644937,"defaultBranch":"master","name":"helix","ownerLogin":"vzaliva","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2016-09-07T21:28:27.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/86581?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1697117017.0","currentOid":""},"activityList":{"items":[{"before":"f139ec18aeedb014d90e4082e25f21ee12cd088a","after":"2f5aac79cc1e1636df00b0a3584b562a5ab651ea","ref":"refs/heads/master","pushedAt":"2024-06-13T23:57:22.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vzaliva","name":"Vadim Zaliva","path":"/vzaliva","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/86581?s=80&v=4"},"commit":{"message":"brush up, added \"People\" section","shortMessageHtmlLink":"brush up, added \"People\" section"}},{"before":"5d0a71df99722d2011c36156f12b04875df7e1cb","after":"f139ec18aeedb014d90e4082e25f21ee12cd088a","ref":"refs/heads/master","pushedAt":"2023-10-13T11:17:40.000Z","pushType":"push","commitsCount":232,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Merge branch 'llvmgen'","shortMessageHtmlLink":"Merge branch 'llvmgen'"}},{"before":"a196bc45dce880c2e32d7a1666a5a309e9c8fe67","after":"a3be5624c1667e4a2a54b79578e7064061a54180","ref":"refs/heads/llvmgen","pushedAt":"2023-10-13T11:10:38.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Merge pull request #27 from vzaliva/vellvm-decoupling\n\nDecouple vellvm-specific development from HELIX","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1940470350\" data-permission-text=\"Title is private\" data-url=\"https://github.com/vzaliva/helix/issues/27\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/vzaliva/helix/pull/27/hovercard\" href=\"https://github.com/vzaliva/helix/pull/27\">#27</a> from vzaliva/vellvm-decoupling"}},{"before":"7b64f61ebeee614f95fb76cf0f00130726867fca","after":"1eb9065c1b53320cdcbf76bab1cc309c62e9181d","ref":"refs/heads/vellvm-decoupling","pushedAt":"2023-10-12T20:40:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Revert \"[temporarily] Transition to vellvm fork\"\n\nThis reverts commit 173329095aa8d020c84e63247204fe97dfbdcaa8.\n\nvellvm/vellvm#351 is merged","shortMessageHtmlLink":"Revert \"[temporarily] Transition to vellvm fork\""}},{"before":"a44a4786164ae475e0b8bf37ac0d953785d84575","after":"7b64f61ebeee614f95fb76cf0f00130726867fca","ref":"refs/heads/vellvm-decoupling","pushedAt":"2023-10-12T17:16:57.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Fix for wrong sed script application","shortMessageHtmlLink":"Fix for wrong sed script application"}},{"before":null,"after":"a44a4786164ae475e0b8bf37ac0d953785d84575","ref":"refs/heads/vellvm-decoupling","pushedAt":"2023-10-12T13:23:37.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Move `Vellvm_Utils` to main vellvm repo\n\nUnder src/coq/Utils/Misc.v","shortMessageHtmlLink":"Move <code>Vellvm_Utils</code> to main vellvm repo"}},{"before":"36c59c8bd671dd940ecc90734c730e507deddda5","after":"a196bc45dce880c2e32d7a1666a5a309e9c8fe67","ref":"refs/heads/llvmgen","pushedAt":"2023-10-04T01:00:12.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"YaZko","name":"Yannick Zakowski","path":"/YaZko","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1241556?s=80&v=4"},"commit":{"message":"Merge branch 'llvmgen' of github.com:vzaliva/helix into llvmgen","shortMessageHtmlLink":"Merge branch 'llvmgen' of github.com:vzaliva/helix into llvmgen"}},{"before":"cdabb1a3f7946fd60bbb45f679db65231f1332e8","after":"36c59c8bd671dd940ecc90734c730e507deddda5","ref":"refs/heads/llvmgen","pushedAt":"2023-09-15T09:40:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Update drone pipeline: use zoickx/drone-helper","shortMessageHtmlLink":"Update drone pipeline: use zoickx/drone-helper"}},{"before":"0209079d4d11b42aef1f617486775b47022c9954","after":"cdabb1a3f7946fd60bbb45f679db65231f1332e8","ref":"refs/heads/llvmgen","pushedAt":"2023-09-11T19:17:00.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"Prove: `string_of_mem_block_keys_equiv_eq_proper`\n\nThis completes the proof of `interp_Mem_denoteDSHOperator_equiv_proper`","shortMessageHtmlLink":"Prove: <code>string_of_mem_block_keys_equiv_eq_proper</code>"}},{"before":"6b4b944ef16363c8784daa56c2a61edaacbad3f7","after":"0209079d4d11b42aef1f617486775b47022c9954","ref":"refs/heads/llvmgen","pushedAt":"2023-09-11T16:46:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"Prove: interp_Mem proper (generalised over memblocks) on all singular operator denotations *\n\n* assuming `string_of_mem_block_keys_equiv_eq_proper`","shortMessageHtmlLink":"Prove: interp_Mem proper (generalised over memblocks) on all singular…"}},{"before":"56257cb5a6322957514cefd60f319917c9af5de7","after":"6b4b944ef16363c8784daa56c2a61edaacbad3f7","ref":"refs/heads/llvmgen","pushedAt":"2023-09-11T12:06:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"Prove: interp_Mem proper for `denoteDSHOperator` *\n\n* assuming more generic instances for operators (generalised over memblocks)","shortMessageHtmlLink":"Prove: interp_Mem proper for <code>denoteDSHOperator</code> *"}},{"before":"22aba04f81d20deaeef9d9597613bfa0f1d62311","after":"56257cb5a6322957514cefd60f319917c9af5de7","ref":"refs/heads/llvmgen","pushedAt":"2023-09-11T07:56:33.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Remove unused [and unprovable] admits","shortMessageHtmlLink":"Remove unused [and unprovable] admits"}},{"before":"1877ff62783f4eb83b0debebf776184d54282435","after":"22aba04f81d20deaeef9d9597613bfa0f1d62311","ref":"refs/heads/llvmgen","pushedAt":"2023-09-08T14:36:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"wip on `interp_Mem_equiv_proper` lemmas","shortMessageHtmlLink":"wip on <code>interp_Mem_equiv_proper</code> lemmas"}},{"before":"1dd4d37f3d780232142b6b50404ded97b489e37b","after":"1877ff62783f4eb83b0debebf776184d54282435","ref":"refs/heads/llvmgen","pushedAt":"2023-09-08T12:50:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"wip on `interp_Mem_equiv_proper` lemmas","shortMessageHtmlLink":"wip on <code>interp_Mem_equiv_proper</code> lemmas"}},{"before":"dfb267fddcae4b54d913428b0537f162ac514c30","after":"1dd4d37f3d780232142b6b50404ded97b489e37b","ref":"refs/heads/llvmgen","pushedAt":"2023-09-07T19:22:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"replace `interp_Mem_equiv_proper` with specialized lemmas\n\nIt turnes out that `interp_Mem_equiv_proper` does not hold in general.\nThere are ITrees which do not preserve equivalence relation on memory.\nA possible solution is to replace this lemma with lemmas specialized\nfor particular ITrees on which it was used and for which we can prove\nthat they preserve the equivalence relation on memory.","shortMessageHtmlLink":"replace <code>interp_Mem_equiv_proper</code> with specialized lemmas"}},{"before":"9e1f09d25abb3038dbc52cc6cb64fef6e148ed50","after":"dfb267fddcae4b54d913428b0537f162ac514c30","ref":"refs/heads/llvmgen","pushedAt":"2023-09-06T15:27:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"`interp_Mem_equiv_proper` proved to be false","shortMessageHtmlLink":"<code>interp_Mem_equiv_proper</code> proved to be false"}},{"before":"0a476b31b05ed31e2c9f9c84787c631243313d43","after":"9e1f09d25abb3038dbc52cc6cb64fef6e148ed50","ref":"refs/heads/llvmgen","pushedAt":"2023-09-04T12:27:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"prove other admits in `interp_Mem_equiv_proper`","shortMessageHtmlLink":"prove other admits in <code>interp_Mem_equiv_proper</code>"}},{"before":"b39477d8db6f5bdaa96be19310a93036010ba5f7","after":"0a476b31b05ed31e2c9f9c84787c631243313d43","ref":"refs/heads/llvmgen","pushedAt":"2023-09-01T16:41:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Bonk `interp_mem_interp_helix_ret`","shortMessageHtmlLink":"Bonk <code>interp_mem_interp_helix_ret</code>"}},{"before":"124d2fe005eb79974ff1b4e6a8a9761f07f91b30","after":"b39477d8db6f5bdaa96be19310a93036010ba5f7","ref":"refs/heads/llvmgen","pushedAt":"2023-09-01T11:37:15.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"attempt to fix a proof of interp_Mem_equiv_proper","shortMessageHtmlLink":"attempt to fix a proof of interp_Mem_equiv_proper"}},{"before":"49eb9e8463c3143ca7683132810eee12a0684c9a","after":"124d2fe005eb79974ff1b4e6a8a9761f07f91b30","ref":"refs/heads/llvmgen","pushedAt":"2023-08-28T16:59:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Fix memory setoid rewriting issues","shortMessageHtmlLink":"Fix memory setoid rewriting issues"}},{"before":"f6db73c116d1d5d773ef48027ad9e61e10d5d95f","after":"49eb9e8463c3143ca7683132810eee12a0684c9a","ref":"refs/heads/llvmgen","pushedAt":"2023-08-25T16:14:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Finalize get_array_cell admits","shortMessageHtmlLink":"Finalize get_array_cell admits"}},{"before":"d38c44b7ea6d225957267fc7f2aaeb339e59e275","after":"f6db73c116d1d5d773ef48027ad9e61e10d5d95f","ref":"refs/heads/llvmgen","pushedAt":"2023-08-25T15:46:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Try a generic lemma about get_array_cell for single-element-arrays","shortMessageHtmlLink":"Try a generic lemma about get_array_cell for single-element-arrays"}},{"before":"b04f72815c1ccd168b50f1c14d1aa662720fa14c","after":"d38c44b7ea6d225957267fc7f2aaeb339e59e275","ref":"refs/heads/llvmgen","pushedAt":"2023-08-25T15:10:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Postcondition almost done","shortMessageHtmlLink":"Postcondition almost done"}},{"before":"29b449bebd86aed0b77116ffb3fe3db8ffcf75fb","after":"b04f72815c1ccd168b50f1c14d1aa662720fa14c","ref":"refs/heads/llvmgen","pushedAt":"2023-08-24T15:05:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YaZko","name":"Yannick Zakowski","path":"/YaZko","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1241556?s=80&v=4"},"commit":{"message":"Turn around the whole proof to properly instantiate the existentials","shortMessageHtmlLink":"Turn around the whole proof to properly instantiate the existentials"}},{"before":"6f7ab4b11479d7ff08a8a218da9e574de025a952","after":"29b449bebd86aed0b77116ffb3fe3db8ffcf75fb","ref":"refs/heads/llvmgen","pushedAt":"2023-08-22T16:29:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YaZko","name":"Yannick Zakowski","path":"/YaZko","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1241556?s=80&v=4"},"commit":{"message":"wip","shortMessageHtmlLink":"wip"}},{"before":"50792ed3bde70e78930f1df7f6513405262e6430","after":"6f7ab4b11479d7ff08a8a218da9e574de025a952","ref":"refs/heads/llvmgen","pushedAt":"2023-08-22T15:19:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YaZko","name":"Yannick Zakowski","path":"/YaZko","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1241556?s=80&v=4"},"commit":{"message":"And a inch more: second free_frame","shortMessageHtmlLink":"And a inch more: second free_frame"}},{"before":"19a4ceb9d30199e85b1ecfff653ec732cdde4c6a","after":"50792ed3bde70e78930f1df7f6513405262e6430","ref":"refs/heads/llvmgen","pushedAt":"2023-08-22T15:05:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"YaZko","name":"Yannick Zakowski","path":"/YaZko","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1241556?s=80&v=4"},"commit":{"message":"pushing things a bit further down the pipe","shortMessageHtmlLink":"pushing things a bit further down the pipe"}},{"before":"0cfc0e94e3242fc4a971114e3e774cd62189a4f7","after":"19a4ceb9d30199e85b1ecfff653ec732cdde4c6a","ref":"refs/heads/llvmgen","pushedAt":"2023-08-16T12:58:48.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Admits cleanup: remove dangling, prove small, organize others","shortMessageHtmlLink":"Admits cleanup: remove dangling, prove small, organize others"}},{"before":"4a0688c4067a9862a603e6941ad3ea455fdf1e03","after":"0cfc0e94e3242fc4a971114e3e774cd62189a4f7","ref":"refs/heads/llvmgen","pushedAt":"2023-08-15T20:35:17.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"zoickx","name":"Ilia Zaichuk","path":"/zoickx","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/20614336?s=80&v=4"},"commit":{"message":"Add global env preservation to genIR_post","shortMessageHtmlLink":"Add global env preservation to genIR_post"}},{"before":null,"after":"1ba23f4616e1670e265064ca15a9e8a10c3a0510","ref":"refs/heads/llvm_genv_admit","pushedAt":"2023-08-14T13:50:28.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"olympichek","name":"Valerii Huhnin","path":"/olympichek","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33845529?s=80&v=4"},"commit":{"message":"ad-hoc add statement about global output var to the invariant","shortMessageHtmlLink":"ad-hoc add statement about global output var to the invariant"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wNi0xM1QyMzo1NzoyMi4wMDAwMDBazwAAAARk8RNc","endCursor":"Y3Vyc29yOnYyOpK7MjAyMy0wOC0xNFQxMzo1MDoyOC4wMDAwMDBazwAAAANqVz94"}},"title":"Activity · vzaliva/helix"}