coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Mansky, William" <mansky1 AT uic.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Announcing VST 3.0beta
- Date: Tue, 16 Apr 2024 18:10:46 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uic.edu; dmarc=pass action=none header.from=uic.edu; dkim=pass header.d=uic.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=nUYnw4zsbumAh9OWpJDSYdgM60LEe1/K9z/FeZta/oc=; b=FZMCChMYcQO1tFX8o60Mg7RdNf0ZZm5J7jZixVvqbccUrLt7M1RyjZ4eI/0jEBOfrMAkuvRowZ2hGMJ+yDXYtHDu2o6rEteHWoF6jMC1U4ErkdfnAT3rhp5pwRYfyu8kAXzAPKhphjndLj21NEm8J9tFrXHMhL+rXEfW0yAMD+LUKd3+P4GxrxRXZ84GwXadMv3601VEyPjF4I4084CFchXYWmpzi5CqboWpWM/jB2PHp583hgiso0d9cnpMVN7y4wzpKefegD6WuBXIhm6yJwzjGhl1Zm+zHI8qTnOyQyc8yqw0hHM8Zx7iEcmZ5bZ375Agie8j2GF5234YvIvPLw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mhmphCAk8h0WkYy1a+epXtQzCTm/mM/ufsYJ2ehcQBeE652xALT0mLlTSq80N+T1BGUW6vpR0fPwr/REtm1mY6GCRWZAny4Z0mRtZ301nLCutD7HdyKiMWl6OmR1pzzptJfUcUR2R0sn0loJNMX34Q51HO+Jeam30dW2wBTp3yPOYk7CLBzJ7FKetUIVAw7vpLRoWorFdmKGP4dqYhUpNqwvG0B1fAJovOQmCHNdh21mWQxsDlmWd5N7zbThYsoJKo+J9YMY0j1IU3gLpRQo1JF6DY+MzWFEcqa5JiWG8W4aUIdCS9547AqSJRKPqNJTd/4g8jTcySNPZbKmXcbzjg==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mansky1 AT uic.edu; spf=Pass smtp.mailfrom=mansky1 AT uic.edu; spf=Pass smtp.helo=postmaster AT NAM11-BN8-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:kqusiqAPZdN81hVW/0bow5YqxClBgxIJ4kV8jS/XYbTApD501zxSx 2YdUWiAM6uIZ2agctF+aIW29x8O7JTXnNVrOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZzdJ5xYuajhIs/7a9ks11BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xScdFHW3+QzMEs3Ioki/O12KEhk+ uNNfVjhbjjb7w636JSSb7A1w+4FfIzsNo5ZvWx8xzbEC/pgWYrEX6jB+d5f2nE3m9xKGvHdI cEebFKDbjycO1sWYghRUslg2rb17pX8W2UwRFa9oKMx+GvClSRs0bOrPdbIEjCPbZwLxxfC/ jKcpQwVBDkhG93C4gK79kuSi+H2gwX2Y6A4K7ino6sCbFq7nTdJVEJ+uUGAifK+kwu1X89VA 1cF/zIn66k07k2iCNfnNyBUu1aBtx8YHtBWQ+sz7VjUzayOu1fEQG8ZUjRGddoq8tcsQiAn3 UOImNWvAiFztLqSSjSW8bL8QS6O1TY9dDUFTxUYXFY56dj8pLs1hRPmZ/xsD/vg5jHqIg3Yz zePpSk4orwci88Xyqm2lWwrZRr9/vAlqSZlt23qsnKZ0+9vWGKyi2WVBbXz6P9BKMOTSAmHt X1dws+YtrhfUNeKiTCHR/gLEPex/fGZPTbAgFlpWZ486zCq/H3ldodViN2fGKuLGphYEdMKS BaJ0e+02HO1FCbxBUOQS97hY/nGNYC6SbzYugn8N7KimKRZeg6d5z1JbkWNxW3rm0VEufhgY MzBKZv9XCpKWP8PIN+KqwE1gOdDKscWlDu7eHwH50j9jOH2iIO9FelabADeNrBRAF2s+V+Ir IYOXyd19/mveLalOHWImWLiBVULJmI8Hpf4t4RccfSbSjeK60lwY8I9NYgJItQ/94wMzrmg1 ijkBidwlgGk7VWZclriV5yWQOizNXqJhSlmZXBE0JfB8yRLXLtDG49FLMZvJeR/r7YzpRO2J tFcE/i97j10Ymyv01wggVPV9eSOrTzy3VvWbRm2KiMyZYBhTAHv89rpNFmnvioXAyb98YN0r 7S830mJCdAOViZzPvbwMfiP9lKWuWRCueRQW0CTHMJfVn+x+6dXKgvwrMQNHecyFTv5yAC37 T2mWSUjmbGVoqse0sX4uqSfnoL4T8p8BhV7GkfY35aXNA7b3DOq/qpdYtmyJBHcS2LG16Gwb spFz/zHEaMmnXQbl6FeArpU3aYFyN+3nIBjzyNgB2TtU1SnLphCM0u295BDmYMVz4AIpDbsf FyE/+drHImgOeTnIQY3HxUkZOHS7sMksGDewtptKXqr+RIt2qSMVHhTGBy+iCZ9Cr9RG6F9y McDvP8m0SCOuiAIAP2n0B8Nr3+tK0YeWZoJrpsZWY/nqjQ6w2F4PKDzNHXE34GtWf5tbG8RP T6mtIjTje99x23DUUYJO1rj4O5/vakK6Td2lAIsBlLRgdfUpO4F7DsI+xQNcwll5BFm0eVyB 2tVC3NINZi+pzdGuOUTXkSHOR1wOxmCy0mgl3oLjDL4SmerZEzsLUo8G8G0wRgJ1lkFVQRZ8 62SkkThdTO7Jc3e/DU+ZhNmj/rJXNYqzAnzw/q/FZ7ZApNhX2Lvrf6wbHtVqRG9WcIVr2/Er NlM4+xfR/DaNykRgqtjEKic9+0aZy6lLVx4Y8NK3f02D0TDXgqtyB6yJFuUeMgQA9DrrWrhU 9dPIOBLXDSAjBe+lCgRX/MwEuUljcwX68onUZK1AHwNrJ+0jCdj6bDU/QjA3F4bec1ky5sBG 9mAZgC5MzKigFVPkDXwt+hCAG2zZOcEaCDa3OyY9OYoFYoJgNpzcHMdg6eFgHGIDDRJpx6kn hvPR6vz/dxQzY5Bm4jNEKIaIy6WLdj1dvqD8SHtktBoQO7MD/zztFIumgG6BzhVALofYMQot LKvtNWs4ljJkoxrWE/kmr6ANZJz2+OMYMRtPPjKcUZqxRm5ZJe04j8o2XyJFphSodYMuuilX 1SZbeWzR/40WvBc5iRcVA1DISknUoX2cabSiievpNucChUm8FLmLfH20VTLfG1kZiszFJmmM TDNutGq/cF+kIRAIDQmFsNWKcZ0D3G7UJR3auCrkyeTC1eZp2+ru5zgpEIG0i7KAHzVK/TKy 8vJaTamfSvjpZyS6s9StrFzmRglDHxdp+0UVWBF8v5UjwGKNkI3Hd4/A74nVK4NyjfT0avmb g7jdGEhUCXxfQpVeCXGvejMYF2tOfwsCPzYeBoS4EKmWwWnDtihAZxg1BtazVVYRz/B9Nyje PYioiDeHx7ozp9QELNZorTxhOp83frVy04Z4U23wYS4Hx8aBq5Mz3B7WhZEUSvcCczWiUHXP i4PSHtZRF2gA1vEeSq6l6W5xDlC1N8u89kpUctL6PD2ntzCicdmmLj4Mey11aAfZsMXIrJIX WnwW2aG/2GR3DoUpLctvNUqx6RzDJpn2+CkebT7S1R6c76Yswwa0wEqxELjj/3OPCZCElibm zWxi5T7LFrQM1hfgdV61i1Qk6+ckRsw4/XhkQ/04zLKjHTVCjQflweClGrGFH07l0QvU4i0j tvfgIZ9bmB6bAfZmAQ=
- Ironport-hdrordr: A9a23:RBxY3qwhx5RrUBJHuXuGKrPxy+skLtp133Aq2lEZdPULSKGlfp GV9sjziyWetN9IYgBHpTnyAtj4fZq8z+8D3WB1B9uftWbdyQ+Vxe1ZjLcKoAeQbREWlNQtsp uIGpIWYLKfMbEQt7eY3ODMKadE/DDxytHLuQ6x9RdQZDAvT5slwxZyCw6dHEEzbhJBH4AFGJ 2V4dcCjya8eFwMB/7LTkUtbqzmnZnmhZjmaRkJC1oM8w+Vlw6l77b8DlyxwgoeaTVS2r0vmF K12DARp5/T+c1T+CWsm1M73K4m1+cJDeEzSvBkv/JlZwkETDzYJbiJFYfy/Azd69vfkGrC2O O82CvIef4Dok85N1vF2yfFyk3u1i0j5GTlzkLdiXz/odbhTDZ/EMZZg5lFGyGpmXbIkesMoJ 6j5VjpxKZ/HFfFhmDw9tLIXxZlmg69pmcji/caizhaXZEFYLFcoIQD9AcNea1waB7S+cQiCq 1jHcvc7PFZfReTaG3YpHBmxJipUm4oFhmLT0Aesoie0iRQnnp+00wErfZv60so5dY4Ud1J9u 7EOqNnmPVHSdIXd7t0AKMbTc6+GgX2MGPx2aKpUCra/Y08Sg3wQsTMkcgIDcmRCeA18Kc=
- Ironport-phdr: A9a23:vM9gJxNpbq8Wu22MBswl6nY/BRdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6Qr1QCXFtiLo9t/yMPo8InYGlY8qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtMiTanfL9/L hS7oQrRu8QVnIBvNrs/xhzVr3RHfOhb2XlmKVWPkRji+8y+5oRj8yNeu/Ig885PT6D3dLkmQ LJbETorLXk76NXkuhffQwSP4GAcUngNnRpTHwfF9hD6UYzvvSb8q+FwxTOVPczyTbAzRDSi8 6JmQwLmhSsbKzI09nzch8pth6xZvR2hvQRyzY7Kbo+IKPpwcKDTcs8VSmdaRMldSzBND5mgY 4cTEeYMO/tToYnnp1sJqBuzHQegCuT1xT9OnX/23q073/w8Gg7G3QwgG9YOsHXOo9XwOqsZT Oe4zKzSwjXFdPNW2jf85JXTfxA8oPGDQah8ftTMxkkyDg7IiEibpoP5MT2PzOsNr3Sb4PR6V eKpk2Mrth99rzyzy8ksiITHiYYYx03K+Ct3zos4Jdy1RU51b9O4DJddtSKXOot5TM0tQ2xkp Sk0xLIYtJKmfyUHyJQqyhjCYPKJdIiI5wjsVOeXITpgmX1lf7O/iwy18Ui6xe3wTsy00E5Lr iZcidnNuGsN2wbU6sidRftx5l+h2SyI1wDU5OFLOUU0la3GJJE/2LIwk4ccvVzMHi/3hEX2j LKWeV4+9ue07OTnZ63qpoebN49ulgH+M6IumsOlDeQ9LwcDWXWQ9+ek1LD78kD1XK9GguAqn qTbqpzWO8oWq6+jDwJR0osv8wizAja63NkWmHQLMU5JdwmGgoXsIV7CPP71APKxjluyjjhmw vXLMqDhD5jLM3POjrPhfatm605A1gUz181R55NVC74fOP//Rkn8v8HCABAjKQy72ePnBc191 owAXWKPBbeUPrvOvFGP++4jPvCAaZINtjv+MvQl4OXhgmEjlV8aYKmpwYAYaHelHvRgPkqVe 2Lsgs0GEWcWoAUxUPDqiFyFUT5VfXqyWL885i0/CIKhCofDRZqhj6CG3Ce+BpFWZ2ZGBU6QE XrweIiIR+0AZD+OLsJjiDAIS7asRo472RyqtAL2079nIfDV+i0cu5Ljzt915+jLmBE37zN0C d+d02KNTm1phW4IWj4207xlrUNj11iDzLB0g/pDGtNL/fNGTh86NYLAz+x9E93+RxrNfs2VR 1a+XtWmHTYxQ8otzN8JekZxAsmtjhTe3yWxGLIVjLyKBJks8q3GxXTxJsB9y2zH1KY7lVUmT NFPZiWagfs1/A/KQoXNjk+xlqCwdK1a0jSHvDOIynPLt0VFWiZxV7/EVDYRfB2Fg87+4xaIa raoErc2dkN+yMqGK6JPIJW9iFxAX/TyYfzDYmn3lmutU0XbjoiQZZbnLj1OlB7WD1IJxlh7F ReuMAE/An3kuGfCFHl0ElmpZUrw8O54oXf9T0kuzgjMYVcyn6Gt9EszgvqRA+gWwqpCoD0o/ jB9Gk2+zov+FtuL4QdtYfYUessztW9OznmRrAlhJtqlJqFmiEQZdlFytkX11AQuIphBmo4no G55hBFqJ/eg2UhaPyidwYi2OrDTLTzq+wuzbqfNxlzE+PC/3/5Wrd4e+xDktgzvEVc++XJ61 dUTy2Gb+pjBEAsVV9T2T1oz8B954brdZ0HR/qvy0ntheemxuz7GgZcyAfc9jwyndJFZOb+FE wn7F4sbAdKvIaokgQrhaBVMJ+1U+KMuWqHuP/KbxK6mOvphlzO6nCxG5o56yEeF6yt7TKbBw Z8Ex/iS2gbPWS37iR+ttcX+mIYMYj93fCL3zCHiH41AP4VvfI1NBGuzYoW2yth4m5/xSitA7 lfwT1gC2cKvZV+TdwmhhUsJjRtR+yf533rlnFkW23kzo6GS3TLD2bHnfRsDYCtQQXV6yE3rK s6yhswbW06ha04okgGk7AD03fs+xuw3Im/NTENPZyWzIXtlV/76s7OEeM1esbs1sC4RXeihK wPSWvvmrh0W3jm2VW5Xwis4ZmiCp5Ty2RF2lSjOSRQ75GqccsZ2yxDF4dXaTvMExTsKSh5zj jzPD0S9Nd2klTmNv6/Kqfv2F2eoV5kJNDLu0ZvFriywo2tjHRy4mfm33NzhCwkzlyHhhZFmU iDBrRC0ZYeOtezyNOthZUp5XXfh6sE8F41j2oc9n5Af33EGi47doSJByD+sd48Ah+SvMTIEX nYTzsTQ4RT51UErNX+Py4/jFxD/ioNga9S8fmIKy3c45sFOBr2T6e8Mli90r1yk6APJNKQl2 G5Flr10syBc0rxa3Whlhj+QCb0TA0RCaCnllhDSqsu7sL0SfmGkN765yEt5m9mlSrCEuABVH njjKfJAVWd96NtyNFXU3Tj98IbhLZPVZNQItQzNuwrBhK5YJI97xbIawDFqP27wpyhvzuc9l h9/hLmnvYPBJmlwtvHcYFYQJnj+YMUd/SvohKBVk5ON3oyhKZ5mHy0CQJriSf/7WCJXr/nsM ByCVSEtsnrOU6SKBheRsQ01yhCHW4DuLXycI2MViMlvVAXIblIKmxgaBX07hsJrSljslZanK AEhoWlMrl/g9kkQkqQxb0a5CiGH4172D1V8AJmHcEgLtEcbvx+TaYrGqbsvVyBAos/49FDLd jPdP0IQSjhWEk2cWQK5N+H3t4CZqrqWWrLmfamJPeXry6QWVu/Wl8imitI0pm/VZMvTZiIwX bpniwJCRS4rQc2BwmdWEnVFmX6VNJzL/E/kqH8w85nakryjWRqxt9GGU+IAaIw2qR7q2fzRP LbI3HQrbmsBnpIUmy2SweBGjgdL0nNgK2H2Q7pY7XafHuWNwOcSBhofIUufLeNw5rknlklIM M/f0Jbu06Jgy+QyABFDXEDgncegYYoLJXu8PRXJHhTDOLODLDzNi8b5BMH0AaVXl/lRvgast CyzNWbGZ23GvR+5EhelPKdLkT2ROwFYtMelaBFxBGP/TdXgLBqmLNtwij5wyrox4xGCfWIRK jlzdUpRo6bYsXse260gXTYasDw0cKGNgG6B4vPdK4oKvPcjGSlym+9AoTw7x7ZT8CBYVal1l S/V/bsM6xmtluiCzCYiUQIb9m4N3drU+x85Z+OIq8olOz6M5h8G4GSOBg5fotJkDoeqoKVM0 p3Vk6m1Lj5e8tXS9M9aBs7OKcvBPmByVHihUDPSEgYBSiamcG/FgEkI2vSb8GaWv8ESt5nn3 pcCV/UIMT59XuNfEUljENEYdd1vWSg4lLeAkMMSzVyXiUCIAe987tXAXP/UBujzIjGEi7UCf wEP3b7zMYUUMMv8xlBmbV552o/NHgCDOLIF6j0kZQgyrkJX9XF4RWBmwEPpZDSm53oLHOK1l Bo72UNuJP4g/zD27xIrN0LH8WEuxVIpl4yv0lXzOHbhab29VoZMB2/oulgtZ9nlFh1tY1T6n FQ4ZmucAeMLyeMmLScy1UfdoccdRaYaFPUbJkdWnbbOOZBKmRxdsnn1mBUBvLOdT8MkzExzL datty4Sglo/KoJqY/SWfO0QkRBRnvzc5Cbwj7JomVZMKRpVqDHAP3JY3S5Afrg+eXjy97Q1u 1XbwmlNJDBXBaht/qMi91tjab6Jl3uyiucaeE7tb7fNf/vB4zqS0pPRJzF4nkIQyRsf9OAvg 556KhiaCxh0nrDJT0xbZ42fcElUd5QArnGLJHTX6Lyfz84tZNezTriwH73J6fxcx0ugGExB9 2UkyO0kR8Dp+meIaMDtIfgC1Akn4xntKBOdFvNVdRmXkTAB5cai0Jtw2oobLTYYUzwV2cqf+ 7fc4AImnajaND/TSmobVc0JOm9kAKWH
- Ironport-sdr: 661ebf2c_InJjgURNVugXxXtr4LrWy1QFM0HK21+dW8ZagAH1G2pa+Hy aSnhPagSJT9i8dkqipkvfyT/r6MtpzVPQ6mfDXA==
I am pleased to announce the release of VST 3.0beta. VST 3.x is "VST on Iris", a rebuild of VST's core logic in the generic Iris framework. This means that most of msl no longer exists, veric has been rebuilt as a more maintainable and extensible logic, and it is possible to freely use Iris theorems and tactics in VST proofs. The top-level guarantee is exactly the same as in VST 2.x: soundness w.r.t. the operational semantics of CompCert Clight. See also https://doi.org/10.1145/3632848.
Key new features include: 1. Support for Iris typeclasses and Iris Proof Mode (IPM). Predicates can be proved Persistent, Absorbing, etc., and then automatically handled accordingly in IPM. At any entailment, you can use iIntros to enter Iris Proof Mode. For details on Iris Proof Mode, see the Iris documentation (https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md). It is also possible to rewrite with both entailments and equivalences, as an alternative to using derives_trans or sep_apply to modify part of a separation logic assertion. 2. Full support for Iris ghost state (rather than the "Iris-style ghost state" of previous versions). Any Iris resource algebra can be used as ghost state after adding a thin wrapper (see ora/theories/algebra/frac_auth.v and progs64/verif_incr_gen.v). Ghost state can be discarded at any time, while memory resources are still treated linearly. 3. A compatibility mode, available by importing VST.floyd.compat. This hides Iris-related boilerplate and restores the notation and lemmas of VST 2.x, so that existing proofs will largely work as is. There are a few incompatibilities; proofs that use ghost state or external state (e.g., I/O via ITrees) cannot use compat, and proofs that manually manipulate entailment clauses with sepcon_assoc and sepcon_comm may break (but they're more easily proved with IPM anyway). For a full list of known incompatibilities and advice on porting, see PORTING.md (https://github.com/PrincetonUniversity/VST/blob/vst_on_iris/PORTING.md). 4. Installation instructions: Install the coq-vst.3.0beta2 opam package, download the release from https://github.com/PrincetonUniversity/VST/releases, or clone the vst_on_iris branch for the bleeding-edge version. Build with Coq 8.18-8.19, CompCert 3.13.1, and Iris 4.2.0. 5. It is likely that VST 2.x will be supported only until 2025, perhaps up to VST 2.16, in parallel with releases of VST 3.x. Release 2.14 of VST, compatible with Coq 8.17-8.19 and CompCert 3.13.1, was recently released and will soon be available via the Coq Platform 2024 release for Coq 8.19.
We are excited to release VST 3.0 to the world, and would appreciate your feedback, either via issues on GitHub or by emailing mansky1 AT uic.edu.
|
- [Coq-Club] Announcing VST 3.0beta, Mansky, William, 04/16/2024
Archive powered by MHonArc 2.6.19+.