{"push_id":1090657045,"size":121,"distinct_size":1,"ref":"refs/heads/coq8.5","head":"009806324840a4c357bf3be8c52669ffa15d54da","before":"e59c08b99fff50a8b185b5a653690831a0d752f4","commits":[{"sha":"3fcc358c23078d5fd06f0edf73c77c0067a34d54","author":{"email":"2cbe48de27626291d4789a0d88f861eebc2cb61c@princeton.edu","name":"Lennart Beringer"},"message":"Polishing, and preparing for DRBG","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/3fcc358c23078d5fd06f0edf73c77c0067a34d54"},{"sha":"e8ee587317b9cb34df5377448f39e0d65e061748","author":{"email":"2cbe48de27626291d4789a0d88f861eebc2cb61c@princeton.edu","name":"Lennart Beringer"},"message":"Merge branch 'master' of https://github.com/PrincetonUniversity/VST\nMerge during commit","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/e8ee587317b9cb34df5377448f39e0d65e061748"},{"sha":"1c3dc68a39594c83620b2b5188ad179972fe6afb","author":{"email":"2cbe48de27626291d4789a0d88f861eebc2cb61c@princeton.edu","name":"Lennart Beringer"},"message":"Added spec for one-shot-hmac (with crypto-guarantee) in protocol_spec_hmac. Proof polishing elsewhere","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/1c3dc68a39594c83620b2b5188ad179972fe6afb"},{"sha":"9ad2e486c51dc27c8361811155f85399f16b3884","author":{"email":"9964fcf15cf03644571918538e83618148b6cc34@princeton.edu","name":"Andrew W. Appel"},"message":"Filled two holes in res_predicates.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/9ad2e486c51dc27c8361811155f85399f16b3884"},{"sha":"2e122138f802e4c1874b51ab99af7e18eda7309b","author":{"email":"9964fcf15cf03644571918538e83618148b6cc34@princeton.edu","name":"Andrew W. Appel"},"message":"Merge branch 'master' of github.com:PrincetonUniversity/VST","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/2e122138f802e4c1874b51ab99af7e18eda7309b"},{"sha":"6fcda4a70deafbe124c54560f6ad6cfc90912667","author":{"email":"9964fcf15cf03644571918538e83618148b6cc34@princeton.edu","name":"Andrew W. Appel"},"message":"Filled all the holes in veric/initialize.v.\n\nAs a consequence, had to change juicy mem alloc_cohere,\nto say that the permissions of m_phi are a SUBSET of the permissions of m_dry,\ninstead of exactly equal.  The difference is only at an\nextern global function (Gfun) that is NOT present in the\nuser's \"G\" (funspec list).  In such a case, m_phi will\nhave (NO Share.bot), where the memory will have Nonempty.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/6fcda4a70deafbe124c54560f6ad6cfc90912667"},{"sha":"0ba7c28765ce08019d1c2c129db8a4a0d18e39f2","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Move aggregate type from VST-reflect repository into examples folder.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/0ba7c28765ce08019d1c2c129db8a4a0d18e39f2"},{"sha":"b880ec0a7193b94da8a1d721c88a9fc7c76feed5","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"More progress in soundness proof in aggregate type demo.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/b880ec0a7193b94da8a1d721c88a9fc7c76feed5"},{"sha":"6f8ccbf7036dca97643df8b9ac18b604ebed916f","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Finish proofs in aggregate type demos.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/6f8ccbf7036dca97643df8b9ac18b604ebed916f"},{"sha":"3bfa21eba42d0aec66e4bec86882fb4e8681c55e","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Some renaming and cleaning up.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/3bfa21eba42d0aec66e4bec86882fb4e8681c55e"},{"sha":"d09fdcfe51e776ffdaca3871240e8d82edc58690","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Remove a unused admitted lemma data_at_data_at_rec. Clean up some local facts lemma.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/d09fdcfe51e776ffdaca3871240e8d82edc58690"},{"sha":"48e3021fae9f269a819c831838b10bfe2ea11ab3","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Clean up the admit for alignof Tlong.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/48e3021fae9f269a819c831838b10bfe2ea11ab3"},{"sha":"694d00391b2d34947b76a65ea975f954693cdcf3","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Remove field_compatible_array_member. Its proof contained admits and it is used only once. Affected proofs are fixed.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/694d00391b2d34947b76a65ea975f954693cdcf3"},{"sha":"82da84db640ab6f24557e52822e62b81855d6ab0","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Fill the hole in field_at.v about share_join_data_at.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/82da84db640ab6f24557e52822e62b81855d6ab0"},{"sha":"493844de50908ab69538f084587e7dcc85bc95f2","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Fix a small bug caused by last com commit.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/493844de50908ab69538f084587e7dcc85bc95f2"},{"sha":"d923bc66c73728bdf657c91369d1ff2531d2dab0","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Fill the hole in nonreadable_memory_block_data_at in field_at. Now all holes in field_at has been filled.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/d923bc66c73728bdf657c91369d1ff2531d2dab0"},{"sha":"2fb47f09dd08ee975e1409c25cd4d11a0d2fb52d","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Fill all holes in nested_pred_lemmas and fix related proofs. Now array_at_data_at needs lo <= hi. Related files in sha and progs are all fixed. But other proofs in hmac and tweec can be affected.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/2fb47f09dd08ee975e1409c25cd4d11a0d2fb52d"},{"sha":"ff412021ff73fa68930f6830d4e9423edb0e497f","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Some modification in demo.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/ff412021ff73fa68930f6830d4e9423edb0e497f"},{"sha":"8a7cf17e1e4285d5311c962fe8169d406b8dba7c","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Finish readme in aggregate_type demo. Other small modifications.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/8a7cf17e1e4285d5311c962fe8169d406b8dba7c"},{"sha":"b86ab89dca1180615cab4dbe1c47c61f7ce7c637","author":{"email":"913446ef8b4114bf9d2c4883d245fa7bbca12257@gmail.com","name":"Qinxiang"},"message":"Small modifications.","distinct":false,"url":"https://api.github.com/repos/PrincetonUniversity/VST/commits/b86ab89dca1180615cab4dbe1c47c61f7ce7c637"}]}