From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x32f.google.com (mail-wm1-x32f.google.com [IPv6:2a00:1450:4864:20::32f]) by sourceware.org (Postfix) with ESMTPS id 89CE23815FFA for ; Mon, 30 May 2022 08:32:45 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 89CE23815FFA Received: by mail-wm1-x32f.google.com with SMTP id y24so5888704wmq.5 for ; Mon, 30 May 2022 01:32:45 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=KCi3J+hI0jKoyxBqS+B2ARTFyAJIfMMnAboFu/Hk2Ec=; b=hfvUtLxo5zmzQ+yuZ59GzS5DY3o7Nl5NmPBoZSog7SKY8xBSeNXSPLNkH6iOZ0YvQA 0drikdBqqmlTMnXK6iM4izKwh3qa2ieBMehfSZeq393k0PcLIF/KNzurPVpqJPuqrmoZ W0RPjuM2qVhcLS4xDmWeDcC5d0/Wp+o23FvFMXb8FERZ/hTB4YLLWKpwZ+F9hibrHMRV VE77eCuthBY2LBIpi8lruQ6X62aLKaN55Xdbl8fWI1Xg/7knAxdeOZclB/QFj2hIGT2b 1e0dmJmUXEEzrLDXi+MAc1oLFYxeyYelztiEfop3Ms2DJ1hCCyyfoiBadNdixFLVfRtm 5xrQ== X-Gm-Message-State: AOAM530C5OH+gfFIHVQrnlzKEUx32H9hmfwH5HWkztBWvxHOueZB3N1W 1vYVWmqwDyvGTVfgoKD2Ycu4tukBy5L0Yg== X-Google-Smtp-Source: ABdhPJzeWVo6B3Xl7ijvI0/VjP4C3GhW6JCDnXkiLY1OIIeC0H2zP/ZopFRG3J+TgXJxcOfV7whEeA== X-Received: by 2002:a05:600c:1da5:b0:397:73e3:8c80 with SMTP id p37-20020a05600c1da500b0039773e38c80mr17820540wms.45.1653899564139; Mon, 30 May 2022 01:32:44 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id bd15-20020a05600c1f0f00b0039466988f6csm9705919wmb.31.2022.05.30.01.32.43 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 30 May 2022 01:32:43 -0700 (PDT) Date: Mon, 30 May 2022 08:32:43 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Update proofs of double arithmetic unit after prover changes Message-ID: <20220530083243.GA210728@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="VS++wcV0S1rZb1Fb" Content-Disposition: inline X-Spam-Status: No, score=-7.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 30 May 2022 08:32:46 -0000 --VS++wcV0S1rZb1Fb Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Changes in GNATprove (translation to Why3 and provers) result in proofs being much less automatic, and requiring ghost code to detail intermediate steps. In some cases, it is better to use the new By mechanism to prove assertions in steps, as this avoids polluting the proof context for other proofs. For that reason, add units s-spark.ads and s-spcuop.ads/b to the runtime sources. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * Makefile.rtl: Add new units. * libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers. * libgnat/s-spcuop.adb: New unit for ghost cut operations. * libgnat/s-spcuop.ads: New unit for ghost cut operations. * libgnat/s-spark.ads: New unit. --VS++wcV0S1rZb1Fb Content-Type: application/gzip Content-Disposition: attachment; filename="patch.diff.gz" Content-Transfer-Encoding: base64 H4sICLh/lGIAA3BhdGNoLTAwOS5kaWZmAO09a1PjuLLf8yv6w62zMHECcTLMg8PWCY9hOcsA l2Rql1O3KuXESvAZY2dtB8j++tuS37YkP+Iws7O4aneILbVa/e6WLOvGfA6dzsLwQNtbzGZ7 mq7tfda+krlhkq7jmTDl3m51Oh1Bj1a73Rb1+te/oPNu8EE5gDb95z3gjfOr4fh2fDm5ur4a D0e/XlydT66P/z06gv9rAYDbce8117P/Z8ee/pc8e7vRbXtuGhbntmmkb7fZ7aXmfOXcna3s ZR7G0l3NjfxtT5vdE95t05gmb7daOo+s2Gphad6e29EcQ7dXXU2fJgjFe5whM7dJmtzcJpTs /X1Kdfz/OyR6C5Fr8mpBC54M7x6Gutb9YiGZZl+JPjmxrUfiuIZtHbba7Plo7XrkoTu6Gd7+ 2j1ZeZPrJXE0D1u4h7ByibQBHWWpzb5qCwJTW1+HjYcOgp6c2qupSShP/JEohMlnWyds+r33 qkoJgP/2lX6PCp7h0sb0OjYWk/+Fj+zfC8sjC+L4QM7vbdc7DJvRRw42u9K8laOZ6SZUouiF DINLe4aPF/QJzFfWjKHfaodNwltw4U4+r0xvckpm9sPSdg16N2wFsHPaU+BUxf/6+N8gjeBu 3A4cgghZcGzbJtEiADi/GBQdB44YAPX5eWRYC5PAm8Lfp73EMNyrXQxDLYJRDPO0XxVGHubp IKJZknNctoyQgSjAL8qdiHKww4bfTU25cd41zrjGuZZjWQyN8U6Jf984BEn0MzDCwT/BNwaT kfEnoRwOWsW6aZKHB82lBsW/lo49I/oKodw49iOZnBqPhk4snQkCTie0IR8UdUCNyNu3Su9D 2ohESEEWqdOfLiwUHgT0J9HjxwCapYN3T6wQ7SPwScfwbnU4DX01Tj6CNNXTj6CEmOBvlGWf Xl8sF/+Gnd7u7m4WUrG88CCpHEh5PpeB1C8BiQs5B2lAISUEM6Iu1x7DjohCShXpFhFnYyD9 JoBQkuxyRdNvTScM/wAf57ylQo0L7sReOAdp3EMjNro35t7kksy9DFQFAqPH7apmu+ZoIO/f l/cfxP2VWMZuqP9G/eVb57QaSpSwhgr+YsDOOK+ENVTw0maQwHaq6o7oYrgVq3UJpWa4qY3j Vt1QcMwEw41COkw4mUAeysUHwDEcEV/TCivhWkzuMl3UuEveLIjnuHuY9JDMA7pUccD1vR/Y c/Zz0NENmtPogXcEbeatNNNcwwMSwliaBvbD59N1Ep765g0jVxfdLXWj6j5mIWoP2ur+257S V9NutCjN8K8if50Kr5gknvZUDNFmGIh7muWlQv2PR1k6pfT8Dc8GHmbAo3ETg/cBIEOzvU77 kl6lkMr7ghxmajFmah6zQbOYDXiYyWYfYNbfTcRvU7IwrISBv6RR3KTQpSTHXTra4kGDoesS B9sfr5mW8mxq7Nui0NufU4GzFXf3R0jTwZ/CpcdMCT/UYJqchiFBITO8ksY91nQ++YRutSLO g2+G8yCJc7bfL8aEGr2MlLCfSqTYcaeMsJSJA6TRuDASkNuaDBRhFFDCOBT4xXYFbU6JBIhw Sv1GGyzRHf68KuWQ7cB2ybiYneHPsI/NY7rU1UghZQulu9LYXM2qP3bcVCczU3NSoTvA+Mme PD/74U7SVieQQlMd//ppR4U3bzj6hxf1wNElhpUU/cMgYHjbVwZ9GjC8x7xb3c8m3nwuo/dI YB+Lck/N5StZVH0+sOjuxH54WHmanwkmASp0Qgowrx73xBgkydCQqLmEXR6OZPhZMiLJDVI2 KIk7+h42BYijPhT5o2CE7Lh8bSs0CzK7VK70lUGFMULs9/OzkLbdyLJVwD/uJBLBWL8U4Llr FsuVEcD+5vLHCz7zQigR9ET4WVkG+yHz1BoiGPXOcUGtKkUpPCoJkRyJjUSBRUEseC4jCoOm RWEgEAWJzCXi/cqiMAhZ0M8zryPqWT2aE9VbUHMl9ktQCEEeVyhStCPyFAlZmhiCpilbxZIg WU0DdvaVwEQF/6pKOEQmqpfkU1l7CUd5i1nOTnIyiZw9zzYJS4Hl0KV5uUg1RaMn7EDJwTPc EucrlO5B6UiBoDYkaa0qYdUoaK3KWveVsGAUtO7zMlRfKgzXc4zpKiqLi5lVqiLNVYwS9TIx OG4ZbbfOhBqcQOkyP38Car0J1OWIgIT1ukfz3yIHBCTbAOF+FuENjGcWi9JFYfHsaFtezVoi bGIyCQHx15X4gBjBMo1p6XfkaeiX5o79AC6NWqwFkD9Wmml4a/Tt3hMhFissk+cl2kiiw6Nm rogL9jwPi7ZzjMW917mn9tQ1dAKG3/2rZT9ZzMrqxDUchKMxTtFtF2A/EicPTcaybj2flvid JZuY5+mWhQs8xdJUTkKKxi05TqEA8cYRyE8+HqhIdNivSMwgVijTa6zyWqHvzOJMZevKfgIT 7RpophnIZiD1BltX0TwaBPtmj2w46VdJ+waSxo0AmyG7xORvDCleuS2GJGBB5Z7ximxp9mwW unOzs1TPijup0p2li/WNsTqbVW1jntl58ahZaqISdrLYezOG+plydQY2LvrFPCmFakky53EV U1mtQuWgjMAn4sa6+2NkKnGzTIGlYI8GOhbJkDxk6R5HHhJVcEhv+qiIg8rHIbuRwGfkUNfT FUjelKLiQy0AagRAVur6DlIwyd4ccTfp/hxxN156Vej/srClm8PiqdQsy5WKWTaLWnLUamj6 QiWsTIr8mLWj5go1xJJ77GKxy87rJcK/hEmjG8f4u7YO4w1ekk1gbElY/eBvxVYH+++Vt+/T K8KBsZm6aWPze4yDoMVdtgWvGE7vKfD7SoE7/O/3ewP/Z9r4i/51Z9qx2RLYrJ2C9z6AvVxA dxruZ2T+VKV3M1T+aQdxQOLj+DkloVVpcQfElSOG+Ni0RfAGfHh+BwqPMTok4rhHV3aipxFx 2RIRfRRoQ/JBnz0ILHICVq4iztoqPqwfiuYl4j7+vm8ud+INO0lqGnM6Fuwdwb5vVmIoKabd G4lOPC5w1iVKOe1ifohZUoorQvvK9/N1uCZxdFXYVo1zlENqsFOmT5GKdahuwOaj9cMzji6I 1aF8hqjF6xY5UchfYtGo0zm50JVFV74q+BdgeTnVksTiG6i2AGAlbY18WgDxMP1MTfo7RCSY SLD1ra8e0NdVMc45+KD0si+u5tiWYoiYpFIC5jNI3kxzi3rfm/wI36+qJw4NmW70u78L/C5E rjfEJN0VqnpfKVMgTpyLeSNlz6Yc4pdrqjkBELC1IN+SvT5XwNd8H9HLBL5ic3JJetVLhwVm EcpXNCWFsk2nsEkhOZ6DsJqcUykoFRBBqZgo3EVZS51+RFXixkxQLWyCqqFIIaX/qoarYuAC cqsm7lTVdMnWXrhq39QCTEyxeqsweVR4ErARdjxkRYsw2e7NrVRVpxTPTspCUbzo/tyjICZt J0swNcxoXMj/zs3ouF9Rkavq6gZBBt+M5kgf7eFUeb6RMRX/n0gt0g3U7Ds8MZVyzH9Z1o3V JJu+KdHlvquT78Dl0kt5u6qSy9MWzs6bl2NCaR9V3mdV3ObDgdCEX2vKz33Xfg823GVTl+KF NC8/jNSP+nk6s6l8TxrVdRK5CMdG8DL5/PkC0LxJeTFzQqf0YmabQ7JvUSspJFrljExgnyVH CFWn7/YMMr8cU9tEl6ZBqIaRFvJMBn9dvcr0xKWRbfkbWVW8mR2HxcjX9zfiwk9uMqIi0Iv7 GyHOzfqbnjhv68XLBNnszF8oOGBn6bTVg/2B8i6/ThBxqI5NEmwq4yljuAolfWuTd4xdwUF2 TR5lt83D7LZ5nJ3sQDuahLx0UiE7B6+6y3qZLGLTnf5iIcs2rXxip8Ck8hWWt2ktNh/RRUyX CGzJfuZdaTDmab0tVlqZxjamrlvT1a0pqlRLX3W0hI6Kq3ZH2de82JU5rlKwrFutb0Q72i/N uVhb6q9/1+JYnrjVWZiHUZ2neRhla2rMIJWiWmnpL9o5wHvwonsA8q+OVJJviXDHmwYjIf17 bjb47ncHFLiajKFqbMmtWuIiTEm2t+Iu24UIfxmZqrlMXlJMSq7Ccvlc8Q2EQOZFqyCN7H2E Dbc/8vond0CyfHiw31PU9zQfft/PHTLrX+Ktc1y61d09J5husIFuwzS5sWh4W8FwU7HwNtX8 ZQPe4vxMDfOzjasofxvx2LYn+F5zorp5jZrIa+IucV6TQDVRL8g163B4kxdMYZmgmRrBdgoE 25H4MvKeoeYWs8foaiKNjIE1kE/GwMpvrw7PXjE8dPXgGQ8E5rbDTgjSHaLR84WCc+oJ0pjM DPplKnaYPf2jC58Mhx7aYiXhEc1dw0xziQLsq1YRRNd4oHDoI3o8vga2hcNEx+O7ttP1A5ED 9Z3Se4eByIdeXxnkPhqT25OVeFUz86ZA4pW5/m5xqS5SgyZPqv6bF++yRzWPVlPXM7x0KOx3 DTH6zyp77LISPyjALWf1takL/+F9gUWRn2Ltv7PKxY8DvvaB0ok5c7A5NR4RI5F0KiJyFZx4 KQrSj2TLU+UKUPUXFMun402fRpOYY+ni5AYnJwjdTXlfUt5RyLxAlZJi+flyYkTOrdq2Uu4J y5m4ctu38oA3pbn8PBye5PwgNCo+DicgUeE5YwWPa9JoA5crJVEFj1uJ1OU+0kYv/l4dptXC iOeVA5twIGsPfghnkSnB5CO59Gu0knBFWPisLUd+yjB4q9DS5YeDvtJ/z9/KI7tk9j2LZj8Y W0l8DafPa1hcpGkoJJaLbtWQOIte7ZBYiFaVkDiLTf2QGDKQTmxrplGNnBtWWCEQfdcoGNuf ZUo060XGr86+clRfhmS1ScQlSfXDm0r5kpIF3C0H5VunXt08oI53lpC02sGg30DICs4W+97i rS1EAtnRc0uapefYaunGfA6dDi0q7unkcc9amSZM9xaz2Z6ma3umMV1Ymrfndtyl5nztarrb ssgTzA0E/GDrBHr7+weDQavT6cQAWu12uwAIjUL2lX1o95T+AcYfrbbss5zVLwpPKmGVrgJ4 51fDMZxcf765uDy7ZX9cX51djUd14TWN3wju8L8xnMFn6OJfNzCEW/i1Nrym8YvxXAKBWWPw Sl8ceCf2cs0+BgA7J7ug7quqAp8cQmBkz70nzSHwyV5ZOttvosCFNetuHz8mZ4YLc4qHG+Bx CLC2VzDTLACH6OHOCUIXKWg+u2c7VFON+ZreQZSJE8LziPPghp/eRehf4JxYxNFMuEFbYczg 0pgRyyWgubCkd9x7ogNM16xDRI1OCI+RJUEXRI0Y2NSBR+KwpZC+AnT1YUfzKNIO2Evabhfx XIOpeX7LCJ6/aBJNO56bHn6X4d5eEv+8e5zbk0FtF4GVS+YrUwFsCb9djH+J4F1/GcPw6g5+ G97eDq/Gd4jfE+JnYzvyGHwoAuiqi4Ej4GQczfLWlD6fz25PfsEew+OLy4vxXQgPZ/LpYnx1 NhrBp+tbVKqb4e344uTL5fAWbr7c3lyPzrrFzN2evAxd0MBdkpmBLCXPM8KoHcjAiMzYr3d0 guc3l0keUYGivFxQCiAtAniarrN4CaEtUXQM12Xfv9CJO0O+xFw5PzmB25XF1scujamjOWs4 C4dXYvyiEbs9JS1jWRHLKFyWqlui3x2SwUXxMHW41x4JqteMGI/04x8wQ/MQao5McSw9AS/T TUYl0EzbWjDxxMYo/EvHRm48HCbxcwlhkKg3dtHv3NxdXJ332aDBj+7tl6vxxeczRJ3KgYfY m2uk3sUcLBuTUwohhvfPe89bftzbe3p66i6sVdd2Fui82UzcvZ/LifI2+cEMwRMKio2W2bDY d8Ex5iAmWoHYLrFWHtEeAM0CXGG0cmc7X+GLZTB583D+AbyzZw/nhrfjr2UwgX4iDl2/tenZ sUwWh7qGDgFvjsns3rJNe0G/sxEb/e3Mt9l4qNVearOv2gIVau165KE7Qmv1K5MwGuuyX5PP GNKxDOBm5ZBWm37jnG7FSPY4rBY1zlb2EiO+6WZhYwQlETcO1Ne4sWn8RJFiF07gC96fwDXe OwPq7MZwgb+uYCSB1zR+/OsYbNBh3Ri80tdr3PgaN77Gja9xYwbea9z4Gjf+gHHj1NbXqVCw e7LyJteo0low/1wsSXdWXs/nfiTJSqrzleXbD1qUP8Fe5I8VsWZEgRuHoGkg8BGObdskGpp3 h3grxwp/0zVKvyq7E7aNdiAnIEUbk6KhRnbUQ0m2bGiobIScIUu9gHnDOmsEJREwv/3wGjA3 jd9fM2B+LbTK8XsNmF8D5irwXgPmzej3GjC/Bsw/UMBMMcTwlooHhp5Uo3DaFkqF7bjUaGIg acODZq0YYe+JuWT0REKgxNJXfeJvi0/XPjgDyWbrq5mBsop/o1FAD4R2HDDsXLpdGN+TNXNN tmWuA9tMzQT7iLm/Ncb1IQUvNqBJ9f+aDC19ghFrAINiSz9/bsZWZm6bpv1ER37S1h8pFB/S GybeQzbPY9bRe7IxS/AjaPK8RF1ghkvxeYwAaNA/VOCYxtt/rAxsEPEzaqIExAji9SjuHlK6 rB4SbejkOkha31h24Te2czeAFw+FSs164oxsf0Y285V0mgrKoE8zvwkMuzgXw2dTBCt8JYtx yPd32AQVG+ibXXQPnjZHnqDx1Lsb0YdmKgX0GYrocxzTZ1iCPvFQCfpMkTIpjMMHKLAoVJ6z Il3RUkJxNhitLLA/hhYSkIow5og71JbQGeKExtTjYR6DE9ltKHEMUcHr/N52vXCT07lpT9GX IAI0nWoib6wwUom08f8BzAK4Iz2lAAA= --VS++wcV0S1rZb1Fb--