{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":557786788,"defaultBranch":"main","name":"HOL4P4","ownerLogin":"kth-step","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-10-26T09:53:50.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/48919830?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1715153434.0","currentOid":""},"activityList":{"items":[{"before":"ca712779d5c1ccb33c42dffaeba72b11b63a042e","after":"c2cdabf5e0cdf0afacaf24b28517c0a336f90eb0","ref":"refs/heads/dev_select","pushedAt":"2024-07-03T16:34:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"More lingering changes from the Trindemossen update","shortMessageHtmlLink":"More lingering changes from the Trindemossen update"}},{"before":"baf6fc402592c6a530acbe37050bc4cd582adf27","after":"ca712779d5c1ccb33c42dffaeba72b11b63a042e","ref":"refs/heads/dev_select","pushedAt":"2024-07-03T11:54:53.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Final updates for Trindemossen + fixes to big-step soundness proof","shortMessageHtmlLink":"Final updates for Trindemossen + fixes to big-step soundness proof"}},{"before":"17b48190408383482e4c1f87f80c12a070ab67df","after":"baf6fc402592c6a530acbe37050bc4cd582adf27","ref":"refs/heads/dev_select","pushedAt":"2024-07-01T15:32:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Updated big-step soundness proofs","shortMessageHtmlLink":"Updated big-step soundness proofs"}},{"before":"d1e6a58a53d474f97d467a306db9507131355fee","after":"a6e72a07fcaf60bcab7b7e3da7ae267d5d96ee69","ref":"refs/heads/main","pushedAt":"2024-07-01T12:09:15.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Merge pull request #41 from kth-step/dev_trindemossen\n\nUpdate HOL4 to Trindemossen-1 release","shortMessageHtmlLink":"Merge pull request #41 from kth-step/dev_trindemossen"}},{"before":"a36b8433509c900b3eadbaca13579b6a62ef4410","after":"b24675ccfd077765763db6b533b4642f415fd203","ref":"refs/heads/dev_trindemossen","pushedAt":"2024-06-29T20:31:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"AnoudAlshnakat","name":"Anoud","path":"/AnoudAlshnakat","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/15954354?s=80&v=4"},"commit":{"message":"adjusted the old proofs to the new HOL4 version","shortMessageHtmlLink":"adjusted the old proofs to the new HOL4 version"}},{"before":"a50224469e2431e5809ce35c5a1f492288914c3b","after":"17b48190408383482e4c1f87f80c12a070ab67df","ref":"refs/heads/dev_select","pushedAt":"2024-06-28T23:03:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Simplifying big-step soundness proof","shortMessageHtmlLink":"Simplifying big-step soundness proof"}},{"before":"9857baf3a800cf859b08cb40cc6d4d063dfaabd7","after":"a50224469e2431e5809ce35c5a1f492288914c3b","ref":"refs/heads/dev_select","pushedAt":"2024-06-26T08:20:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Progress of big-step semantics soundness proof","shortMessageHtmlLink":"Progress of big-step semantics soundness proof"}},{"before":"0706f7cae51570dda634fd2ee61dd9a8a96c41bc","after":"9857baf3a800cf859b08cb40cc6d4d063dfaabd7","ref":"refs/heads/dev_select","pushedAt":"2024-06-24T02:22:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Cleanup of symbolic execution libraries, slimming of bespoke compset","shortMessageHtmlLink":"Cleanup of symbolic execution libraries, slimming of bespoke compset"}},{"before":"e54c219fec1c5bf5b595c2fd1521943fa9f1d71e","after":"0706f7cae51570dda634fd2ee61dd9a8a96c41bc","ref":"refs/heads/dev_select","pushedAt":"2024-06-23T14:08:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Changes to composition theorem in symbolic execution, bespoke compsets, clean-up of definitions","shortMessageHtmlLink":"Changes to composition theorem in symbolic execution, bespoke compset…"}},{"before":"75da3368ea4a52cf48736890d0ba0e9e7c9723fb","after":"e54c219fec1c5bf5b595c2fd1521943fa9f1d71e","ref":"refs/heads/dev_select","pushedAt":"2024-06-19T21:29:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Case binop expression","shortMessageHtmlLink":"Case binop expression"}},{"before":"ea942f13a849b96e89ffa063656dd4c87c44dd6f","after":"75da3368ea4a52cf48736890d0ba0e9e7c9723fb","ref":"refs/heads/dev_select","pushedAt":"2024-06-19T13:28:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Fixed a few lemmata","shortMessageHtmlLink":"Fixed a few lemmata"}},{"before":"762ac32e8a747595a9249d515719323691898383","after":"ea942f13a849b96e89ffa063656dd4c87c44dd6f","ref":"refs/heads/dev_select","pushedAt":"2024-06-19T05:30:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Fix for symbolic execution to re-enable usage of big-step semantics with new composition theorem + proofs of lemmata","shortMessageHtmlLink":"Fix for symbolic execution to re-enable usage of big-step semantics w…"}},{"before":"5596b1b42e6e2f6ed4df2f8e8a6d4fec0283dba6","after":"762ac32e8a747595a9249d515719323691898383","ref":"refs/heads/dev_select","pushedAt":"2024-06-17T15:05:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Progress on soundness theorem of big-step semantics","shortMessageHtmlLink":"Progress on soundness theorem of big-step semantics"}},{"before":"511d376e9ee06333506ee1571fa5eab05465a285","after":"5596b1b42e6e2f6ed4df2f8e8a6d4fec0283dba6","ref":"refs/heads/dev_select","pushedAt":"2024-06-17T09:40:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Progress on soundness of big-step semantics","shortMessageHtmlLink":"Progress on soundness of big-step semantics"}},{"before":"914c805f1d55960aa2ea0f6eeee37f55bfa04971","after":"511d376e9ee06333506ee1571fa5eab05465a285","ref":"refs/heads/dev_select","pushedAt":"2024-06-16T22:12:27.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"More lemmata to p4_auxTheory","shortMessageHtmlLink":"More lemmata to p4_auxTheory"}},{"before":"e0ec2a69171020cca8c7a8800f3a6deabd666bb8","after":"914c805f1d55960aa2ea0f6eeee37f55bfa04971","ref":"refs/heads/dev_select","pushedAt":"2024-06-16T01:06:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Progress on big-step semantics soundness proof","shortMessageHtmlLink":"Progress on big-step semantics soundness proof"}},{"before":"2c33afc56c7dac7b824988cdb549ebe3da5ec350","after":"e0ec2a69171020cca8c7a8800f3a6deabd666bb8","ref":"refs/heads/dev_select","pushedAt":"2024-06-13T12:32:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Fixed cheats and typos","shortMessageHtmlLink":"Fixed cheats and typos"}},{"before":"09e1e3278a08ae79bd85a855b598be10a12ce6fd","after":"2c33afc56c7dac7b824988cdb549ebe3da5ec350","ref":"refs/heads/dev_select","pushedAt":"2024-06-13T12:09:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Progress on big-step semantics soundness proof","shortMessageHtmlLink":"Progress on big-step semantics soundness proof"}},{"before":"a4f4cfe309ffe9c5ab5ee35c082884826fd1c2a4","after":"09e1e3278a08ae79bd85a855b598be10a12ce6fd","ref":"refs/heads/dev_select","pushedAt":"2024-06-12T12:56:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Shuffling around usage of some lemmata","shortMessageHtmlLink":"Shuffling around usage of some lemmata"}},{"before":"ec1c8e0c32032021d33a79ae83a2ed58c6b4f2a4","after":"a4f4cfe309ffe9c5ab5ee35c082884826fd1c2a4","ref":"refs/heads/dev_select","pushedAt":"2024-06-12T12:39:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Further progress on big-step semantics soundness proof","shortMessageHtmlLink":"Further progress on big-step semantics soundness proof"}},{"before":"e658d29c606df1b610c56ace03b4e5d6683fb0dc","after":"ec1c8e0c32032021d33a79ae83a2ed58c6b4f2a4","ref":"refs/heads/dev_select","pushedAt":"2024-06-11T14:03:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Soundness proofs of big-step semantics","shortMessageHtmlLink":"Soundness proofs of big-step semantics"}},{"before":"d61451fa56d392cbcc1ab96d386aeb3d2d55c43d","after":"e658d29c606df1b610c56ace03b4e5d6683fb0dc","ref":"refs/heads/dev_select","pushedAt":"2024-06-07T13:46:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Backup before deleting comments and old stuff","shortMessageHtmlLink":"Backup before deleting comments and old stuff"}},{"before":"66a5a83811730a5c465a8dc826d1331804274fb3","after":"d61451fa56d392cbcc1ab96d386aeb3d2d55c43d","ref":"refs/heads/dev_select","pushedAt":"2024-06-06T19:58:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Fixes to symbolic execution, progress on bigstep proofs","shortMessageHtmlLink":"Fixes to symbolic execution, progress on bigstep proofs"}},{"before":"999455fa3ba91f70bab476bebe58863228de3871","after":"66a5a83811730a5c465a8dc826d1331804274fb3","ref":"refs/heads/dev_select","pushedAt":"2024-06-03T09:51:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Fixed cheats in big-step statement semantics soundness proof","shortMessageHtmlLink":"Fixed cheats in big-step statement semantics soundness proof"}},{"before":"cc0afa9969df1fbf4ee8e90afb0706b59fbec89c","after":"999455fa3ba91f70bab476bebe58863228de3871","ref":"refs/heads/dev_select","pushedAt":"2024-06-02T23:45:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Updated big-step statement semantics soundness theorem","shortMessageHtmlLink":"Updated big-step statement semantics soundness theorem"}},{"before":"71b21ec654e28bb7d3fba808dfe8a9294663ea46","after":"cc0afa9969df1fbf4ee8e90afb0706b59fbec89c","ref":"refs/heads/dev_select","pushedAt":"2024-06-02T16:23:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Soundness proof for big-step expression semantics","shortMessageHtmlLink":"Soundness proof for big-step expression semantics"}},{"before":"5dcffbf56903ea5074d1face41d31b2c9bbc7e24","after":"71b21ec654e28bb7d3fba808dfe8a9294663ea46","ref":"refs/heads/dev_select","pushedAt":"2024-05-31T16:09:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Expanding big-step proofs","shortMessageHtmlLink":"Expanding big-step proofs"}},{"before":"8e44d51aa903108b4d3e7315ad1e09beee54158b","after":"5dcffbf56903ea5074d1face41d31b2c9bbc7e24","ref":"refs/heads/dev_select","pushedAt":"2024-05-31T13:11:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Termination proofs and work on soundness proofs for big-step semantics","shortMessageHtmlLink":"Termination proofs and work on soundness proofs for big-step semantics"}},{"before":"67d7c39b1dd27960488b2f06af0f8c8cf1a676f7","after":"8e44d51aa903108b4d3e7315ad1e09beee54158b","ref":"refs/heads/dev_select","pushedAt":"2024-05-21T15:28:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Reverted addition of action names to tbl_map, added map of action names to import tool output","shortMessageHtmlLink":"Reverted addition of action names to tbl_map, added map of action nam…"}},{"before":"07826295d89e2b7352f0ec1fa332914d57c9cd2f","after":"67d7c39b1dd27960488b2f06af0f8c8cf1a676f7","ref":"refs/heads/dev_select","pushedAt":"2024-05-21T07:07:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"didriklundberg","name":"Didrik Lundberg","path":"/didriklundberg","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12450179?s=80&v=4"},"commit":{"message":"Efficient contract unification, more robust postcondition proving","shortMessageHtmlLink":"Efficient contract unification, more robust postcondition proving"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEdhrW1QA","startCursor":null,"endCursor":null}},"title":"Activity · kth-step/HOL4P4"}