{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":342954381,"defaultBranch":"main","name":"verified-betrfs","ownerLogin":"vmware-labs","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-02-27T20:42:35.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/62306860?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715303940.0","currentOid":""},"activityList":{"items":[{"before":"1e58d0120108d0436de8b3e8bcdcd3b2d80201dd","after":"3fd85ac258e79781353ce77159fcd2efc0c21019","ref":"refs/heads/jonh/marshalled-accessors","pushedAt":"2024-05-24T01:31:31.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"completed resize","shortMessageHtmlLink":"completed resize"}},{"before":"a4910d4caf3471efb415469d5fecbdd6becdf17e","after":"1e58d0120108d0436de8b3e8bcdcd3b2d80201dd","ref":"refs/heads/jonh/marshalled-accessors","pushedAt":"2024-05-24T00:27:59.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"tidying","shortMessageHtmlLink":"tidying"}},{"before":"bdf148b5e680b7bbd7dfa29cd8d1481ff5ecd86f","after":"a4910d4caf3471efb415469d5fecbdd6becdf17e","ref":"refs/heads/jonh/marshalled-accessors","pushedAt":"2024-05-23T20:02:15.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"progress on resizable marshall","shortMessageHtmlLink":"progress on resizable marshall"}},{"before":"006f395cbbd47bf8892670f79397d9a394a7885c","after":"a895709b6853333f3035f5bf73f32db049c9b539","ref":"refs/heads/linked-branch-refinement","pushedAt":"2024-05-10T23:43:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"i decreases fixed","shortMessageHtmlLink":"i decreases fixed"}},{"before":"6e600afd5c10c649ae9a6ae9c1d487d8d9ccc3ab","after":"22da669fea9de8346b39e51c7d7f72a76be6df9b","ref":"refs/heads/main","pushedAt":"2024-05-10T22:25:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jialin-li","name":"Jialin Li","path":"/jialin-li","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9298547?s=80&v=4"},"commit":{"message":"asyncdisk without checksum requirements","shortMessageHtmlLink":"asyncdisk without checksum requirements"}},{"before":"a33c02a80d0f9cbc16e178c2e12f71e63495f2f4","after":"006f395cbbd47bf8892670f79397d9a394a7885c","ref":"refs/heads/linked-branch-refinement","pushedAt":"2024-05-10T01:19:21.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tenzinhl","name":null,"path":"/tenzinhl","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/70078689?s=80&v=4"},"commit":{"message":"Begin LinkedBranch refinement","shortMessageHtmlLink":"Begin LinkedBranch refinement"}},{"before":null,"after":"a33c02a80d0f9cbc16e178c2e12f71e63495f2f4","ref":"refs/heads/linked-branch-refinement","pushedAt":"2024-05-10T01:19:00.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tenzinhl","name":null,"path":"/tenzinhl","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/70078689?s=80&v=4"},"commit":{"message":"Begin LinkedBranch refinement","shortMessageHtmlLink":"Begin LinkedBranch refinement"}},{"before":"b9c4ba0ed78f71e142e0ade168962ce3ebb14d79","after":"bdf148b5e680b7bbd7dfa29cd8d1481ff5ecd86f","ref":"refs/heads/jonh/marshalled-accessors","pushedAt":"2024-05-07T00:18:07.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"tidy exec_marshall","shortMessageHtmlLink":"tidy exec_marshall"}},{"before":"4359a786764020dd2befbfc0cd97c115cb3cf170","after":"b9c4ba0ed78f71e142e0ade168962ce3ebb14d79","ref":"refs/heads/jonh/marshalled-accessors","pushedAt":"2024-05-06T22:33:50.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"learned one dang fact; before cleanup","shortMessageHtmlLink":"learned one dang fact; before cleanup"}},{"before":"1fc70e3d57a61727fecde7a9b790696210864a02","after":"6e600afd5c10c649ae9a6ae9c1d487d8d9ccc3ab","ref":"refs/heads/main","pushedAt":"2024-05-04T00:33:58.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"PivotBranchRefinement_v verified!!","shortMessageHtmlLink":"PivotBranchRefinement_v verified!!"}},{"before":"b018c55733ad64c8df98c52535237fea96c2d9c0","after":"6e600afd5c10c649ae9a6ae9c1d487d8d9ccc3ab","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-05-04T00:30:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"PivotBranchRefinement_v verified!!","shortMessageHtmlLink":"PivotBranchRefinement_v verified!!"}},{"before":"f0695e54861011be57654f28a9a10e82aa7b77bc","after":"b018c55733ad64c8df98c52535237fea96c2d9c0","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-05-02T22:51:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_split_index_interpretation1 proven!","shortMessageHtmlLink":"lemma_split_index_interpretation1 proven!"}},{"before":"1fc70e3d57a61727fecde7a9b790696210864a02","after":"f0695e54861011be57654f28a9a10e82aa7b77bc","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-05-02T22:33:10.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"Refactor lemma_route_ensures & lemma_route_auto triggers, add Key::largest_lte_subrange, change insert_leaf to use route","shortMessageHtmlLink":"Refactor lemma_route_ensures & lemma_route_auto triggers, add Key::la…"}},{"before":"07760f17afb061bb899e9f38f0821946958a43f3","after":"1fc70e3d57a61727fecde7a9b790696210864a02","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-05-01T22:42:09.000Z","pushType":"push","commitsCount":13,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/main' into pivot-branch-refinement","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/main' into pivot-branch-refinement"}},{"before":"ca93b0e8c847dc075c7b81c50134668bd9265753","after":"1fc70e3d57a61727fecde7a9b790696210864a02","ref":"refs/heads/main","pushedAt":"2024-05-01T22:41:59.000Z","pushType":"push","commitsCount":45,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/main' into pivot-branch-refinement","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/main' into pivot-branch-refinement"}},{"before":"ea2f7850cd2f9e50b5ec2d8f428ff20bb9a58963","after":"ca93b0e8c847dc075c7b81c50134668bd9265753","ref":"refs/heads/main","pushedAt":"2024-04-30T15:20:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"fixed trigger for broken proof in LinkedJournalRefinement","shortMessageHtmlLink":"fixed trigger for broken proof in LinkedJournalRefinement"}},{"before":"d13ee563391daf84ff03db9a6b1986b4c072b0b3","after":"ea2f7850cd2f9e50b5ec2d8f428ff20bb9a58963","ref":"refs/heads/main","pushedAt":"2024-04-29T14:58:05.000Z","pushType":"push","commitsCount":9,"pusher":{"login":"jonhnet","name":"Jon Howell","path":"/jonhnet","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1816420?s=80&v=4"},"commit":{"message":"Repair UnifiedCrashAwareJournal to refine to new stack","shortMessageHtmlLink":"Repair UnifiedCrashAwareJournal to refine to new stack"}},{"before":"c42a23b2ed6adc8b4ca281ab9544526209921869","after":"07760f17afb061bb899e9f38f0821946958a43f3","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-26T23:54:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_split_leaf_all_keys proved","shortMessageHtmlLink":"lemma_split_leaf_all_keys proved"}},{"before":"ff0cb5eaafea655f8524d697ec87a918a55dc1dc","after":"c42a23b2ed6adc8b4ca281ab9544526209921869","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-26T22:36:34.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_split_leaf_interpretation proven, add Key::strictly_sorted_implies_unique","shortMessageHtmlLink":"lemma_split_leaf_interpretation proven, add Key::strictly_sorted_impl…"}},{"before":"3d355ea61a89fee121e54468f64fb74d1960d489","after":"ff0cb5eaafea655f8524d697ec87a918a55dc1dc","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-24T23:23:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"change PivotBranch_v wf triggers to fix rlimit exceeded, lemma_split_node_preserves_wf proved","shortMessageHtmlLink":"change PivotBranch_v wf triggers to fix rlimit exceeded, lemma_split_…"}},{"before":"4e41af8eeba74a4ee387c690fa33e323a87853d9","after":"3d355ea61a89fee121e54468f64fb74d1960d489","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-24T22:50:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_sub_index_preserves_wf proven","shortMessageHtmlLink":"lemma_sub_index_preserves_wf proven"}},{"before":"cc360f0aeee0cfb0be03a198cbd010aab09db250","after":"4e41af8eeba74a4ee387c690fa33e323a87853d9","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-23T23:29:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_split_index_interpretation update","shortMessageHtmlLink":"lemma_split_index_interpretation update"}},{"before":"41c5b392347ac97d8d61cdc27bac502473c55b1d","after":"cc360f0aeee0cfb0be03a198cbd010aab09db250","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-23T23:14:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_split_index_interpretation proved","shortMessageHtmlLink":"lemma_split_index_interpretation proved"}},{"before":"8f5df6cfaaa6d1925d4a0af32624bdc20952e298","after":"41c5b392347ac97d8d61cdc27bac502473c55b1d","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-23T22:59:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"grow_refines proved!","shortMessageHtmlLink":"grow_refines proved!"}},{"before":"77d3a985991d661da94c70316fac1f9d3fd04885","after":"d13ee563391daf84ff03db9a6b1986b4c072b0b3","ref":"refs/heads/main","pushedAt":"2024-04-23T19:08:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"jialin-li","name":"Jialin Li","path":"/jialin-li","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9298547?s=80&v=4"},"commit":{"message":"disk model draft","shortMessageHtmlLink":"disk model draft"}},{"before":"e3970e0ec8578a3a918bc436c9d7a10830f6026c","after":"8f5df6cfaaa6d1925d4a0af32624bdc20952e298","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-18T20:42:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_grow_preserves_wf proved!","shortMessageHtmlLink":"lemma_grow_preserves_wf proved!"}},{"before":"6a83a8eebba69e8cf16da69080a0dffd1c2ddd3d","after":"e3970e0ec8578a3a918bc436c9d7a10830f6026c","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-10T21:54:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"factor out lemma_split_child_of_index_interpretation","shortMessageHtmlLink":"factor out lemma_split_child_of_index_interpretation"}},{"before":"b1d5925daa18dd87b189d661178348fc1e10af8e","after":"6a83a8eebba69e8cf16da69080a0dffd1c2ddd3d","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-06T00:20:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_insert_leaf_is_correct proved","shortMessageHtmlLink":"lemma_insert_leaf_is_correct proved"}},{"before":"c4427f9a4770fe7700569a4bbb861f13577db1d2","after":"b1d5925daa18dd87b189d661178348fc1e10af8e","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-04T22:01:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"lemma_interpretation proved","shortMessageHtmlLink":"lemma_interpretation proved"}},{"before":"093404ba7c4a74915253bba2221c02b1e549bd4f","after":"c4427f9a4770fe7700569a4bbb861f13577db1d2","ref":"refs/heads/pivot-branch-refinement","pushedAt":"2024-04-04T21:02:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"x9du","name":null,"path":"/x9du","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/33583761?s=80&v=4"},"commit":{"message":"split_refines proved!","shortMessageHtmlLink":"split_refines proved!"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEUpPMdwA","startCursor":null,"endCursor":null}},"title":"Activity · vmware-labs/verified-betrfs"}