coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Andrew W. Appel" <appel AT Princeton.EDU>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] VST release 2.12 in Coq Platform 2023.03
- Date: Mon, 18 Sep 2023 15:48:42 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=princeton.edu; dmarc=pass action=none header.from=princeton.edu; dkim=pass header.d=princeton.edu; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=5JsDuWdMymO8tJBfkSv6oyBlCOLtEesTbVwGV13ciCo=; b=kn35gnnkBHFan+5V9G5rZGgLIt5Yrzd+PokXjGAPRKra83WeTz7ebbmK2iaZDXWuOoAb4JeqVsZA03X3d8TUC3hag73hw7wn5ivilv2JsPhCNhiuGKDcj1efFrheQeMe+DdDDv4ZIngzrR8tunCfGtTwywHSLc2wWnzSFcGdiGl/9A7yzMiqK+JbP8VF/5PmRBzsvKqJKWbjBXRHJP11jc/b+O7tApFNTpAY8kxwlBtYUF7b7MHJTWLBIjDsx35xg3xROmtSzewVQumcERw8h7rHuuMz9pim/FGmy2pC/eiiRmA8k/xj9MummQL7uOGcfzoE7MdDJhOk9AOr+Vfs9Q==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=hd5avQV5gc0jM7f34+iGJ4t6J4QKOdcaKwCt1CWzUD0L/WT2y+fXO24gXR7IQPa7dG97y0CJRaq4rN5l1nfG+1Zb3nt6rHbf464YTfF+qE9fvBYIqRqOw32SWM0T7xpWHvwCGYFR1UdqkFTjoc07gN3cUdyRu9JuQdRX6MB7IvlgcbKcVe6gijPaXZ57CT/HHS61Cve9YALtJ3BlnDUSoulU/MKNxhEDuxAKBImxzT+cS/G9/F76LzrVAtVvId5/yx+yXnDU4tajUs6goX6g7X0ujuT8bJDVYicvlkEG77AchIr4xhGo9lk5ZP8rIKfzQ9dgYgJoQgxMqh8f5vTWZQ==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=appel AT Princeton.EDU; spf=Pass smtp.mailfrom=appel AT princeton.edu; spf=Pass smtp.helo=postmaster AT NAM12-BN8-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:xEKniazXGwjfc9R6Gll6t+cPwyrEfRIJ4+MujC+fZmUNrF6WrkVSy WYXXTvUbPbeZDamL4t1aY/l8E9QvcXSn4I3SwBo+1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2Qc3l48sfrZ80s+5aSq4Vv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPs8dZTXFomA7cFwbdJOlFir KQpMg4SO0Xra+KemNpXS8FKr+F6dozBGtNavXttizbEEfwhXJbPBb3Q4sNV1ysxgcYIGuvCY 80eanxkaxGojx9nZg9RUcph2r3z2T+gKFW0q3rNzUYzy2HL1AF1+KD3Mdzed8CNQ4NYklvwS mfupj6nXEhEaY3BodaD2muxqOLPliDrYrI1MrCTyPNggX6hmmNGXXX6UnP++5FVkHWWUNVGb kcQ5yAGtrk37EXtT9/nXhT+rmTsg/IHc99ZEul/4gfdzKPRulyeADJcEWUHb8E6vsgrQzBsz kWOg97iGT1otvuSVG6Z8bCX6zi1PED5MFM/WMPNdiNdi/GLnW35pkunog9LQfXt3O7mUyr92 S6LpyUYjrAex5xDnaai8FyNx3rmqpHVR0Rnrk/aT0C03DNfPYSFXo2P7USEzPBiKI3CcEKNk kJZkOej7ccPL6q3qgqzfMs3EoqE2dO5IRzHoFs2H5Ae5zWnoHGiWoZL4QBBHkRiM+daWDy0S nPvlBJ12b10G1Dzc55yXp+7UPpy/K2xTN7gb+3fTvhQbrdPdgOo+D9kZBOO01DXi0J2wLsbP LGFe/2NFlcfM7xslxCtdtce0Jgq5yEw/nzSTpbF1Caa0aKSSXqWaLUdOn6cR7kdwILdhy7K4 vBNNNCvyRpNYNbhYyLSz5EfHWoKIVc/G5ryjc5dLcyHHSZLB0AjDO3305o6Wok4gZlQqPjEz ku9VmBc1lD7o3/NcieOS3J7bYLQTYRNlm06MQMsLGSX9SAaO6j315gmdrwzYbUD385gx6QtT /A6JuOxMs4WQTHDozkgfZ3xqbJ5TyuShCWMAXuBQCM+dJteVQD26ofaXg/wxhIvUAuzl+UD+ oOF6C2Kb6YHdQpYCOTuVMmO1HK05HgUp/JzVRDHI/5VY0Tdz7JpIC3Q0N4xCdAFFkjB9Augy QyXXBMqhdTMh6QX89D5o7+OgKn0Mul5H2tcR3L665TvPwbk32OT+61ye8fWQiL8DkbaoL6DY 8dRxNHCaMw3pk5A6ddAIuw63JAA6MvKjJ4E6AZdRVHgTUmhU5FkKVm4hfh/jLVHnOJliFHnS 3C024doPJuSM5nYC38XHg0ua9qD2dwymjX/6fcUIl3w1BRo/YioAFljAB2RtBNzdLdFEpsp4 eMEiv4k7waSjhkLMNHfgBtEqEWKDHgLCJs8ur8gXYTEtwsMy3N5W6L6NBPY2p+0Ru93AhEYG QPM3KvmrJZA93XGaEs2RCTs3/ICpJEguyJq7V4lJnawkd/Bm85t4kVbq2gqdDlv8DRGzONBF Wx5PGJlJai13mlJheoSe0uOCg1+FBmi1Uip8GQwlUrdVFiOVEbBCEYfKNS91hkV3EwEdwcK4 YzC7njuVAjbWf3Y3wwwaBZDkOPiR9kgzT/yspmrMOrdFqZrfAe/pLGlYFcJjB7VAckRoknjj ssy9cZSbZzLDwIhk5cZOaK7i4tJEAulIVZcS85P5KkKRGHQWA+j0Ai0dnyeRJl/GOzow2SZV epef85BbkHrnmLG5DUWHrUFLLJIjeYkrohKMK/iIWkd9aCTtHx1uZbX7TLzn3IvX84oq8smN 4fNbHiXJwR8X5ePd7Pl96Go+1ZUYOXooCXa9cXsqqAjMcJGt+thN0YvzrGzonOZdhN9+A6Zt x/CYKmQyPF+zYNrnM3nFaAr68CcN4boTOrRmOysm40mUD8NGZ6mW8ApRp3PJx5XO7AcR9Nx0 7mBrbYbGWvb6a0uXTmxd4apTsF0CAbbYAaTGvrtLX9RkDeFXonBzyZrF6VU73BWuIs12/RLj DdUpCd9mRD5ljudKLBoh/BiLisg
- Ironport-hdrordr: A9a23:jQXlfq75ahBRYLs/nAPXwS+BI+orL9Y04lQ7vn2ZFiY5TiXIra qTdaogviMc0AxhPk3I6urwQZVoIEmsgqKdhLN8AV7MZniDhILFFuBfBOjZskvd8k/Fh4lgPM 5bGsAQZuEYZmIK7voSlTPIdurIt+P3kpxA692/815dCSVRL41w5QZwDQiWVmdsQhNdOJY/HJ 2AouJaujuJYx0sH4yGL0hAe9KGi8zAlZrgbxJDLQUg8hOygTSh76O/OwSE3y0ZTyhEzd4ZgC P4ek3Cl++eWsOAu1PhPlzonttrcRzau5V+7fm3+4Uow/PX+0eVjcpaKv2/VXsO0ZmSAR4R4a LxSlEbTo1OAjrqDxuIiAqo1A/63Dk07Xj+jVeenHv4uMT8ACk3EsxbmOtiA2nkAmcbzaFBOZ hwrhGknosSCQmFkDX25tDOWR0vnk2ooWA6mepWi3BES4MRZLJYsIRapSpuYeM9NTO/7JpiHP hlDcna6voTeVSGb2rBtm0qxNC3RHw8EhqPX0BHsM2I1Dpdmmx/0iIjtbkit2ZF8Ih4R4hP5u zCPKgtnLZSTtUOZaY4H+sFSdvfMB29ffsNChPtHb3KLtB5B5uWke+L3Fwc3pDXRKA1
- Ironport-phdr: A9a23:jRezUBNngUCp8z48mcol6nZMBRdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr1QCZFtSCo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6z9pHJfglFhjmwbbx2I RmrsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KOT4n/m/Klsx+gqFVrw6uqBFk2YHYfISVOeBicq/BY98XQ3dKUMZLVyxGB4Oxd 4UDAvYHPelFtYnyuVUPpga+CgW2Geji1idIhmfo0q0+3egqDAbL0xY4H9IWrnvUqM74Or0IU eC0yqnH0SvMb+9R2Tf78oTGfR4vrv+VUL92bMHexlUhGRnfgVWMtYzqISmV1uIVvmWY4eRuW +yhh3MmpgxvrDWi2MghhpXUi48I113I6zt1zZg2KNO4S0N1btGqHIdMuyyYKYd4TMwvTn1pt Ssm1rALv4OwciYNyJQi3RHfavqHfpCH4hLiSOaRISp4i2l/dL2jgBay9FCsyuL9Vsmo1FZFt DFKnsPNtnAK0RHY98uJSuNl80quxTqDzR3f5v1GLEwui6bWJZwszqQym5cdqUjPAC77lFn4g aKTa0ko5vOn5uXib7r8upOROYp5hw78P6krn8GzHOA1Pw4TVGaB4+u8zqfs/UjhTbVKkPI2l q7ZvYjCK8kHoaC1HhFZ3p8+5hinDDqqydMYkmIZI15ffxKHkpTpNErJIPDlC/ewnk6gkC9xx /DBIr3uHInCLmTCkLfme7Zx8UlcyBcvzdBb4JJUDbIBLOjvVU/2sdzUFh45MwqqzOb7ENhw2 Z8SVXiSDqOFMq7eq0GE6+wtLuWWZoIYti7xK/0/6P7viX85l0Udfa6s3ZYPcn+4BuxmLFudY Xf3mtcBC2YKvgwiQ+P0lF2CVjhTa2ysUK0h+zE3EISmApzbSYC3nLOBxDu7HoFRZm1eF1yAC W3oeJmcW/cQdCKSJddsnSADVbi4UoMuyRWutBLhxLd8NerV+igYtYr529Rv5u3Tkwsy9T1uA MiH3WGNVTI8omRdDTQxxeV0pVF34laFy6lxxfJCX5QH7PRQFww+KJT0zupgCtm0VBiXLfmTT 1PzCPygDSs8UZoOhZcne15wH5/q2hnbxyeuK4cPlrqACYAz9OTx80WndJU18GrPyKR01wpue cBIL2Dz3saXliDWDo/NyQCCkrqyML4b12jL/XuCymyHuAdZVhRxWOPLRyNXfVPY+PL+4E6KV LqyEfI/KAIUwNaaJ69iUsfoi15LWPDlfvnyXjH5gH++UC6B3ajEd4/2YyMY1STZBlIDllUa5 W6LMSAmHCanqG/CCzooGF7yMAv36ecrkHqgVQcvyh2SKU1s073g4hkOmfmVUO8exJoikQJ48 XBeOgb42NjbTd2duwBmYaNQJ8sn50tK3n7YsAo7OYG8K6dlhRgVdAEfU1rG8RJxB80AlMErq Clv1w9uMeeC11gHcTqE3Jf2M7mRK2/o/RnpZbSEklfZmM2b/KsC8pFa4x3qoR2pG0w+8n5mz 8gd0n2S4Y/PBRYTVpS5W1g+9hxzrbXXKicn4Iac2XppOKiy+jjMvrBhTOI90hukV+9FMaWPG RP1FYs3K/XvYO0mll61bw4VafhI/f18NMenev2ana+zabo42mv+0iIdu987jRnfkkg0AvTF1 JsE3fyCiw6OVjOmyUykrtiyg4dPIzcbAmu4zyHgQo9XfKx7O4gRWgLMa4W6wMtzg5n1VjtW7 lmmUhkPwNekfTKKdV371gBM0kJRrHC603jdrXQ8g3Qyo6yT0Tabie36bBcDElZRRW9pgEvrJ 86Zo+1QDwC4KgMukhWi/0PzwaNW8b9+I2fkSkBNZyHqLmtmX8Ncr5K6atVUoNMtuCRTCqGnZ EyCD6T6qF0c2j/iGG1XwHY6cSurs9P3hU4yhGWYJXd15H3XHKM4jR7H/NHYbeZL3zwNSTV/j 3/aCkX0M9Sy/NqSnovOqajiDyT4DsIVK3K0i9zb/CKgrXVnGxi+g+y+lriFWUAh3Cn32sMrH STEoRDgY5X6gqGzMOZpZE5tVxf378t3HJ07k5Nl2MlWgCBFwM/OojxYyjSWU50Tw6/1YXsTS CRextfU5FKgw0h/NjeTwIm/UHyBw8xnbt38Y2UM2yt74doZbcXcpLFCgyZxpUK16AzLZv0o1 D4F0fYqwGYAgucCtRYqyGOQDq1YTiw6dWT80g+F6dyztvAdbX63fLyYzFB/m9usELaE5AxQR TyqH/VqVT815cJ5PlXW1XT14YyxY9jcY+UYsRiMmgvBhexYe9oh0+AHji19NSfhrGUonqQl2 Ad208jw7+3lYy19ubi0CRlCOnjpatMPr3vz2L1GkJ/e3pjzTMk5XGRRGsOuFbXxTXoTrai1a 17ISWVj7C/dQf2GQ2r9oA9nty6dTsrtbinPYiFflZI7GFGcPBAN2VhIGmll2MZ/Tkfzm4Tga BkrvDlJvwyh80IexL4wb0utFTuPwWXgIjYsFsrFJUIPvFgbvhXbbZTFvLA0Q3AQ/4X//laEc jXJPl0RX29VAhfWVwi7Zuv8ooSYlorQTuumcamUaO3X+7UHDqWGmcr0gIA+p27eZILSZzFjF 6NpgEMbBCIgQp2LlWlXEH4Zz3qVPZzc+U30vyRzqorXHO3DYAv0/sPPDrJTNY8q4BWqmeKZM OXWgi9lKDFe35dKxHnSybFZ0kRAwy1pcjCsF/wHu0uvBOrInbRLChcAdy5pHO1hyvtmmyNra YvcgN6z0aNkhPkoDVsDTUbmhsyiec0NJSe6KU/DA0GIcr+BIFipi4n7bLi9RrtZkOhP/0Ho/ 2/DTAm5ZWvFyGKhXgvnKexWiSCHIBFS8JqwdBpgEymrTd7rbAG6LM4ijTAyxu5R5DuCPmodP D5gNkJV++HIq3oA3bMlQDMHsSE2SIvM0zyU5OTZNJsM5P5iAyAu0vlf/Gx/0bxeqidNWP1yn iLW6N9ouVCv1OeVmV8FGFJDrChGgIWTsABsI6Lco9NJQW7J+DoV92SWABkWoN0jB9Hy8fM1q JCHhOfoJTFO/siBt9MbHNTRIdmbPWAJFzPMQWSRJi1VCDmhOCfYmlBXl+yU+juNtJ8mp5Pwm Z0IDLhGSFgyEfBcAUNgVo9nQt8/TnYvlriVi9QN7Hy1oUzKRclUiZvAU+qbHfTlLDvKxakBf RYDxqn0aJgCLoCukVI3cUF0xc6ZfiiYFcAIuCBqaRU45VlA4GQrBHNmwFrrM0us+CNBSabyz 0Rw0k0mJr1wvDb0vwVrfhyT/HR2yA9p3oy75FLZOD/pcPXtB8cPU3Ky7w5pdcqnCwdtMV/rx RAiaGiCH/QJyOI/PWFz1l2GsMMWS6cFFP9KPEdIl6PQO6VNsxwUqz35lxVOvbKXUMI7xgV2K cX+/TUcikpidIBnf6WIffgQlwECiP7W5X34jrhpkl1Zeh5okivaeTZW6hYBbuB0fnPxrOIws VfQkGMbIDpeEKdz6vNyqBFnMrzZnXu5iuxNdhjqZeLHd/vL6S+dz4bNS1c0nCvgcmF957lw2 so/dEzSemwSnuP5//UhE+PncFsQRewCsX/ZcGCJrPnHxo9zM8OlDOf0QOSStaESxEW5AAIuG IdK5cMETMDEOK7wNd3mKrUI1RIrognnOQfcZMk=
- Ironport-sdr: 65087167_e5ACqjb3Q2F20l8w4CmAjzuePFshBWhZNtmabePUsD+rFMv 8GANzjaulrpulmDS53jLZF7tXlpwIgzvgtWxL7w==
I am pleased to announce VST release 2.12, the Verified Software Toolchain for Coq 8.17 (or 8.16) and CompCert 3.12.
VST is best installed via the Coq Platform, and this release is in Coq Platform 2023.03 for Coq 8.17.1.
Not much is new in this release. VST users might enjoy the new entailer!! tactic,
which is like entailer! but does not perform saturate_local. That is, it does not add so many hypotheses above the line that are propositional consequences of spatial conjuncts; those hypotheses turn out to be useful only rarely. Read the
manual for more information.
Also new this year is VSTlib: Library Components for Verified C Programs. This
is not part of the VST package itself, it is a separate package coq-vst-lib available in opam-coq-archive. See the paper for more information.
Bug warning: A bug in Coq 8.17.1's refine tactic causes VST's
unlocalize tactic to fail sometimes. Most VST proofs don't use unlocalize
(which is why the CI didn't catch it!) but if yours does, you might want to use VST 2.11 or VST 2.12 in Coq 8.16.1.
-- Andrew Appel
- [Coq-Club] VST release 2.12 in Coq Platform 2023.03, Andrew W. Appel, 09/18/2023
Archive powered by MHonArc 2.6.19+.