{"push_id":639444043,"size":278,"distinct_size":0,"ref":"refs/heads/master","head":"051ba872b10ac8c47afb71529c2d63c92d4bd948","before":"e4edd634a91155d6ab74045fc000bb8e1d9dea55","commits":[{"sha":"5831d5ca5af53e47787c5681f17de9cd6a4df3a3","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Partial work on proving first conversion","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/5831d5ca5af53e47787c5681f17de9cd6a4df3a3"},{"sha":"0bf358700e22bdcff4227ecc4696a56fd9079f79","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved an invariant about get_var with injective f","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/0bf358700e22bdcff4227ecc4696a56fd9079f79"},{"sha":"9ee8e45267cce9eca2cd336847c7130684cd1cbb","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Extend invariant to get_vars, progress on proving move","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/9ee8e45267cce9eca2cd336847c7130684cd1cbb"},{"sha":"35eef231aaac07b8db2f4d84d446ce8a74ab9e5c","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved properties of toAList and fromAList","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/35eef231aaac07b8db2f4d84d446ce8a74ab9e5c"},{"sha":"bd914cc0ded03ec29c3f1a31eb6c36a54e77cb60","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Some work on Move, work on Call","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/bd914cc0ded03ec29c3f1a31eb6c36a54e77cb60"},{"sha":"23f389aeec236b7a8d6d66ff0af8b8d90b24cb03","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Changes to semantics of wAlloc","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/23f389aeec236b7a8d6d66ff0af8b8d90b24cb03"},{"sha":"a6c19fe718e46b46124dad9424fe78fc7462528a","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"WIP on proving side theorems about the semantics","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/a6c19fe718e46b46124dad9424fe78fc7462528a"},{"sha":"89504b9b970903b9294ca06740b14420d5e22604","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Partial progress proving first lemma for Call","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/89504b9b970903b9294ca06740b14420d5e22604"},{"sha":"210c773de64013123adc6fff7ce7c63a8dff8c33","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Annotated cheats in proof for Call case","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/210c773de64013123adc6fff7ce7c63a8dff8c33"},{"sha":"3495377b313e3db33988f449aec68530c2fa5ac7","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Added a new lemmas script, progress on proving the stack replacement theorem","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/3495377b313e3db33988f449aec68530c2fa5ac7"},{"sha":"9331734c8438e7508194ad9106d4e7118359ebd3","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Rewrite theorem statement, proved Alloc and Raise cases","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/9331734c8438e7508194ad9106d4e7118359ebd3"},{"sha":"537eb4b8697a78c7be5e7e0320af1e6890421b7f","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved case for seq depends on 1 cheated property","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/537eb4b8697a78c7be5e7e0320af1e6890421b7f"},{"sha":"722e1ecca4135e4f3fc192f17d1af016b84b3f17","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved the Call case for the stack swap theorem","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/722e1ecca4135e4f3fc192f17d1af016b84b3f17"},{"sha":"75a39b3bf31172ef81a97577f120bc7950256412","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved theorem, pending 1 cheated lemma","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/75a39b3bf31172ef81a97577f120bc7950256412"},{"sha":"55cec5f148d01a10a73ed38bfd9ba5cad505d5ad","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Updated to the new definition of env_to_list, proved cheat and packaged the lemma","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/55cec5f148d01a10a73ed38bfd9ba5cad505d5ad"},{"sha":"4065c5b85b432de7d23dc015c815951cdf7f79f1","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Revert the sorting algorithm","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/4065c5b85b432de7d23dc015c815951cdf7f79f1"},{"sha":"1cc923d1559619deda4f7fb505a4b5ce43b03162","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Moved fromAList into HOL, rearranged some lemmas","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/1cc923d1559619deda4f7fb505a4b5ce43b03162"},{"sha":"407cc5befee6b59921431a916150745ff4e7d8dd","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Proved Alloc case","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/407cc5befee6b59921431a916150745ff4e7d8dd"},{"sha":"20af08bd4f42895a33a15b9d86089eb64c394a84","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Some progress on linking up the 2nd step of the proof","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/20af08bd4f42895a33a15b9d86089eb64c394a84"},{"sha":"dbeca07b2952cad8e23d8dbe56e8d3a49df90915","author":{"email":"bf0d15eaf1845b5ba1a9324b87d1b62bc58c79bd@gmail.com","name":"Yong Kiam"},"message":"Defined the final correctnss thm, strengthening stack_swap in progress","distinct":false,"url":"https://api.github.com/repos/CakeML/cakeml/commits/dbeca07b2952cad8e23d8dbe56e8d3a49df90915"}]}