From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x436.google.com (mail-wr1-x436.google.com [IPv6:2a00:1450:4864:20::436]) by sourceware.org (Postfix) with ESMTPS id D0ABD383D825 for ; Thu, 12 May 2022 12:39:58 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org D0ABD383D825 Received: by mail-wr1-x436.google.com with SMTP id d5so7082272wrb.6 for ; Thu, 12 May 2022 05:39:58 -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=45s5ZsPuWRE3EX+AMV0TdAYtfMnQF8thuAlyzxNZQCI=; b=D/4I5BpQL2HV4m3k8LrCPX6ev6Js869LHghiGRj9WG9ab4jDBSwqGRprqqst/we9Eg PlEkMe1SmFIKCpNqcOZC/LR0wWFq12ZV2+o9Ff1291j2uonH9/8Q3cWVW9oyv0/vQ5Of WV+OdOUwlvQ/TIh9d3yGRtD3NxyiW56SKBXFsh1W1c5c6XcoaHjB0IK2B6REq3YPUVxm cv6YW8C0RAezTAUPbmrDjKSdUlbxy/dEN9DUMbpVBANwWfDHzh03wB/5rY+vo5Ug7lVL k+gfOd/6p/9ct2r0jBGGsWXD16k8HETj06OHeKJH8xAkkzAeTx6XGiX+lWxZ9euyvWkb 17Dg== X-Gm-Message-State: AOAM530fUf1ubEsTSR7Qjp2RnLV0jr3ofhtME+4RybO2ZgTt+wDUzGqR CMVyRPCY86Il+b6yvpHqefhZOPuuQe2T0Q== X-Google-Smtp-Source: ABdhPJzdAtVn0Vj8+6SDEVeljWJPsJLsEaHB47S/PHDbJ2/8g7e20UgDiQ7UUjtjf/regIHyFP2O1Q== X-Received: by 2002:a05:6000:2c2:b0:20c:c6e1:e881 with SMTP id o2-20020a05600002c200b0020cc6e1e881mr18119590wry.333.1652359197189; Thu, 12 May 2022 05:39:57 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id bh12-20020a05600c3d0c00b003942a244ed1sm2556078wmb.22.2022.05.12.05.39.56 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 12 May 2022 05:39:56 -0700 (PDT) Date: Thu, 12 May 2022 12:39:56 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Proof of 'Image support for signed integers Message-ID: <20220512123956.GA780522@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="k+w/mQv8wyuph6w0" 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: Thu, 12 May 2022 12:40:00 -0000 --k+w/mQv8wyuph6w0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Prove System.Image_I, similarly to the proof done for System.Image_U. The contracts make the connection between the result of Image_Integer, the available space computed with System.Width_U and the result of 'Value as computed by Value_Integer. I/O units that now depend on non-pure units are also marked not Pure anymore. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-imagef.adb: Adapt to new signature of Image_I, by providing ghost imported subprograms. For now, no contract is used on these subprograms, as System.Image_F is not proved. * libgnat/s-imagef.ads: Add modular type Uns as formal parameter, to use in defining Int_Params for instantiating Image_I. * libgnat/s-imagei.adb: Add contracts and ghost code. * libgnat/s-imagei.ads: Replace Int formal parameter by package Int_Params, which bundles type Int and Uns with ghost subprograms. Add contracts. * libgnat/s-imfi128.ads: Adapt to new formal of Image_F. * libgnat/s-imfi32.ads: Adapt to new formal of Image_F. * libgnat/s-imfi64.ads: Adapt to new formal of Image_F. * libgnat/s-imgint.ads: Adapt to new formals of Image_I. * libgnat/s-imglli.ads: Adapt to new formals of Image_I. * libgnat/s-imgllli.ads: Adapt to new formals of Image_I. * libgnat/s-valint.ads: Adapt to new formals of Value_I. * libgnat/s-vallli.ads: Adapt to new formals of Value_I. * libgnat/s-valllli.ads: Adapt to new formals of Value_I. * libgnat/s-valuei.adb (Prove_Scan_Only_Decimal_Ghost): New ghost lemma. * libgnat/s-valuei.ads: New formal parameters to prove the new lemma. * libgnat/s-valuti.ads (Int_Params): Define a generic package to be used as a trait-like formal parameter in Image_I and other generics that need to instantiate Image_I. * libgnat/s-widthu.ads (Big_10): Qualify the 10 literal. --k+w/mQv8wyuph6w0 Content-Type: application/gzip Content-Disposition: attachment; filename="patch.diff.gz" Content-Transfer-Encoding: base64 H4sICMz/fGIAA3BhdGNoLTAwOS5kaWZmAO1dX3cTObJ/51Po8IJNnBA7IcCEcIZhLnszw0AO CQzw4tOxFafP2N3e7nYCe+6Hv1Wl/92Sup04y84esjsQWqVSSSWVfipJpWl6ccG2t2dpxZJH s8nkUTJNHs3T81mWVI/K7XSRzPjFTjI9Z+fR5Hvb29stHO5tbW21cfn5Z7a9Nxw8Y1vw52if /fzzPXaPXafVJTv9VlZ8sXOMxOPjw/rX2fhDlc4P2arkjY/3tmzaj8lcfgbWy2TyFzBk5/n0 m1vEa5aWQLHFGLQPY6/yrCqSSVUO2OwyLys2yad8wOZ5vmRpdpUUaZJVJUuyKUvKkhdVmmcl pLDqMi3ZKsMGLrhmt+BAzi7yAnIk828l0OTZ/NuAZbn4XKyy7SpdcDa55JO/0mw2AL4MuFzn q/mUnXNW5blmNwGJ5t9YXl3y4jot+Q47w2Lh/zwDbhMOOb6xklcVcAKRuBGSLfN5OvkG7DS3 41mWF3zn3hZ9WRbJbJGwlyrD+ERk6IkvzP45eiEzDyhr8EdkHb/MpuNXq2qtrEoR41dJycu1 sv6DFHcjgd+AnsfHSs9rZT0peP1T56wNeTtnPV2dL4t8ViSL8UcptM7ahxFxD4n+SL5O01nJ foIOlJUVEr1NqlWRzNlPR+w4qx78mU5h5Gyz0SFlwN4BmdLFasGy1eKcFyy/YFM+gTE8Z8Ar hTFQXSYwPJIMO2nBlwUveVZBD4TBAB+B647mdQY98f726D5LJpN8hQMI+z72zzKdZTSa8owz /hVULtgPICWbcHbNWcaBKdCS1Xi8P3jCtg6eDZ7sgtVoHdey/PRCFAbSz3G0zJNixlEAEHQ4 oPIpTX0bPXzYw2Y5Tf/FoVWGffaIDXeD7Jy8Q6j2PSDSsklThoQZv64ZOIbloKIk61/5RQot IWxPqZVbkhnMYQyli+WcL6ClExrVvUVS/MXRGEE5y7yo+vYInxQ8qcAIAKe0Ss7n3AiVVeOT hDiTKr4t6ZuwPqKPpFRCqZlBD6i1MBphoUioG7FALeaidaa8SK+oO1ScGhvSDbMp1ZM6CxTL i4tkwsHmYtE8mSoeKMc0KabUTYK8ri/TySWaXRQIukouudsTxMMdU2Nl8UjiD1k5frcUbfnu CgSZ59cwUH7J8znYbhwfr5N5yfuovoJP8mKqBuQEDBPTWdLSGqjXlzxjZ8WKw2B0x2+2ms8P 65RUQoMUJjBg8BNKiGLs6mwcuisWLj7gv4Rgh7JekIGaa0yjeizMYcvYV3kvVtmEGuPPIlnq hrFE6UNhkD2zGk7KRZMvFTaQffHQZfkOZr7xr8KICKlkzt5pVYiq/cTgV5i7dF1fF/liwM5y SDkWyu+rJCmH1FRXIf6Xf03GZ/lYN5Jont4nKOHVZYJTDpRhVbIr41MwheNfQC3T8VsymTev ok5CdjKT7AVD0w1eTibMTdytt836Ojoux1II1TAouJK5v16jg/ECSLKCgXlS5Fdg7aBpx+3t BBYZ/hz9W1qqq+gkdbMDu81ziGNWCNfGXzf4y/NyTGq6wIanoSY53KAP0jhVCgyoDlJj7ETt m7OEnL0UqrbMqdLccVYHMY0fhCYwySi9oDLacwCVnUMZpXgOSWVnbNpEX8YGlWZhW8Rw2RaV zunpN56cTSrNIGC0agz8VJpJYODVmASoNJeGgfC2Qp1KZ283BJi9narGMDQ8lTxRKs2rNhYD GnapdGZ37IUyO1T9xnhrhYpyzPVpVctsO3XKq7GkFNzviUJ7H4U9Obx37960oxugjC/gy3Y3 QNnuBiiFG+BgcMC24M8n5AWY8Qxw40TWTsFSAl9JBi30/MWhg90wZZFP6bvIQ1bNapZJMoe+ 82t6lU75PUsZvU8D9nnAvqzXOmncSZK2O0nSdidJqp0ko2eD4VO2hX/t71IDIeDd1M/2NvLb 5A96UkgBL6fJDoxX1GW580s6k4NX/C47aCmGHygUFxLr5Yi5dI5dl84/bu7HMf4bze02fhzp vzErqlv5cbr6b76PO+T7eI3+Q50wSuEvocfhInU8mSdq8WxhLJiesD+dy4Uspoq1OKyNxZI4 NateaSmxz4rez8oln8AauuBZAh0RfRNqySc6uuVO2LnRUlGtn325NrCAFIKXdkkWk++wmPRJ 1Cx3QwtMT1l+Vn/HdaevdgHBN7Eg9ZRW5/O3WaH6KtMu7GZXsUERAgxvscb1FOVmv9WS18Pd YaA85mAqCWG+pXm0TKv0iuP0jOILIIqes9dpAY23s4O+OeaKJeV18vfOQDT7i11940DspRfs jB1ZJVToJEQackq/SUpouC02ZBzdhvR9+6yvvf3ukuBXctartUBdgkOFiE8hAWYS9DCrLi2B 5olJkbNBX3dbTxolIQSUNDQj4wqMPVdDgmqgZ1ScmaiCp/S9A5lolOdHwBNaIUpxGmByYhLZ tn8WBNZq2j+Ry9JT6F9G6ScP3s2nfYZ84BdPkq9YaC1KJP0BZUhA7yAdkH2h1lQ8yNjgB09p oQV2V0agN3cW93dq7HlIjKAEepzaHgK8kpyX+XxVcXZF0z98ORtIbz2MpX/xImcAcTI+S5DV DvuTA1wu/tLcaCWB6FeRqH0Bwa/MxR4UfqEdHaibppTbVtYmEEKrhEBSCvYHHeg7ctSqpYTu B6/y7ApWG1hpuRT3JInhKN1G/Qb+gWUL670sZjXUY61mlDWSDe4pYgcmfytDowzU4tgqyKJ1 bEt7QYpTvSj8NNy1IaFdAZinqPThbt/yJhrE21geSvD6JodVOXvDFwtYJOnPTeraJEYZqPt9 wb5DkArbtm5zHK+OMkCf2COYVetDmsT/1Ke0w0CBv6ZX0FSLxUrtuaHnYJ2iP8eLFr99RlMi vsGnz/2YNGfX6YSL+tNKWdjeQ+XPwG96jolLKGWhIuG/LyAD/t77zB6yL/2wJpsq9TZVULfr K5lGot49W0dHVs6wNM16iEaO1WBDGrL2Dj99ZvWxZi3BSEt68v38JUZLCjw0fL+08UXta/r3 LMa7B2IWsOD80odCPsPsAfXEf3+WyOCcz1KN/B2/BFIeYS1r+QykqJN/FvTYNaFClEcVHs5E eTDDZ8zxPkhYqwhggt4Xsd//UFemmes9En4WhGERHiEJtZUlCH1tz/RJkNvUuM1b614K8Pl6 ppz0HIcw09+b9HS2YoSu2OGT/cHes/jhimM1r6YKWdarosDQEbURMxV2FyQO+FZElrGq2ytp VBGLmQJs50xHNMnqoGzkAWMOO5jk+kj4AP73f+zB9gMvWU/QHSEB/tX7CBLs9r20LRBv5EVk 66G7AI8GsGss0Pp9u8XlJOFZikNtCe/2/TLWF2eGHCT4qIeB8dLOsYejb3OJ3cPCegD8XGYX WEU73WYWahspmDh1BBVP9JmmkhY9yi3mHyTWRCHK8fRhZhPEp7y24eAeKRELW22RxSINjbFp VN2ejv1lzbFZFc7oDBIGPAXe/uXw6bDLh900xCsiUphdgNe6/d5Tj5jXZMA+mhxooz2KtD3A p1UC1YDeTKovS1QieYGdnTth14UapSgpDAD2AmAkjSxrI0tYHOgIYJkOyY4f7OEZudHw6WB4 0NGOe9sal+x6jTzsa18BVjO9OJTH3Bhrbj1CS4J2B7YqYaDN1clY2bhjMOVXdqe2lhUn7npC Z3p3cVFyx0WtV6IITNxWUi6SUd/HrT5K4rUId0lZjy0l2xGUZ3cJK7O3c6gmdcpWu5neifrJ E5yoR/vDwXC3q4aNot+eS6cQ+oIMqNvV+hXOevxxnUVIdXZom0gmV3LiuCJtE53PcZ2pK5xf q1ZzQS/5P31aOYUWSCuZw2vuPJlwDJ+xeibpSQ14LUJ8ZO1/imYnIi8L7AsD9mpVSBbK1gRI x/YpvxDNqaxZsBVCGqHptAzPN3o/AsUAYPtBCHLI3h+7DuAOmAzNLTAAiLSL09EzLyAAvprA gzC0PA9Inv2niII/CNy1+wBzPXjmB17enMe1nGsCjoRNFFfoVEXBy2WeTWlHNqcDyRa3jH+t 2EU6W5kNWU97h/aGvnvDhwQLKATh2/sP3oLW4nRMnMiDDb93UU9ShUoQ7q5S4Lt8VUwc/QjV iOO2yXI5T8VBYSR2VatVHlHjhwyoshmfrqekE49H2m46Yfo0NJMrnBgpzc1Rnj26ezKfs99p o9hyUUuH9u/kwRZGF/7hw/01t7edwfneUX/Y5kuJggTshhLOOQgK7csuk5KJTXCe2fwW+TS9 AK1F1dKw1MK8rqcmMwlEjb+noUxOvC4QzU4U/kWT4YKuiTY+gmadti/4XPjIznl1zdUqjcpH ULCSw8pmaDnD6Z5HcRVVhAb+pn7RXVMW3ThlLXunLL592k3pKJ4YTo+ONKQMDit3UdGjZccL lB4GGyFO+elI8BVjRCsY6J4fmRIDa+fAgmM40G0V8AuYEqmQUcyM6FpL0nY78hvaEaodjHmx yEIurPdbXzLBXz2jw2YbW8VZFRyQ4geo3sY6LsZi5Gex1hgpV3OyUKFy8PiXzW/KlwDi8ViY CyLo8FYxW+GVHWXuUkHTM83YF7vKNkPIm2ZT/pWX5nRYwq5h+brE61hZ9xMLxE5tll1zurM1 oatLFbvkBd7akXhRCVp2cYTUnCECd4oGRW87LkZSXnZxiMSdIu0g1d0a8LBYA3e18tKTfwfK wHxU35AItU3D1aSV3daqfxPbbDxc9cV4Jw+SFrtlvBu/jGbYxSdjHZ/wOGQazpIXGrKhu4RM p/GgGO8Jlvg2F+dEsSNM8c4cXXakI6PTfEJDUNyNQzPRPNiNPoCnB4Mh3p9+vDsYruPmweKF kGgJ8sUS9+dpj13f89QQuKS7l/Ikor7iCc1jMzN5d9RnPGVr6TKwQxfDVg6kcVjIjTXaKA2d R4ge15Q72g8fGkfIQH70+P6CY1htvogfuYo/YgbcHVrJlsvlyPrHFhu6niUD/aTjwWZniYZX FI/or4ciqemdqh3d7XVEtT7fa52VqUCaiVMs3gM0237ncp0b1uLIp5UumXU3kA4ZuYNO/iDc bAPmQTbqqG7vOMN7snjLXF3Q6Lva5V/xILfe0GDWWQG7e5o9ayNRxJWNFX9uBJZY0PGy4kBS nkC7l515PFZhT5dxJol+Y3e6mkx2LzGHS9w2Nara7fct6dAY/Am2AApZ5svVHG8ey7NAerMG K6Xv9hbGlSJMa2aZFjQ5hDULjqsPmGKop5m+193IUIXWMCln/YFVSau7b7Pf+hFbUQMq9XXc gG27azYPixBQuQmvmOkK9ckbrT1jndzPkPXq4tdc7LZr1LKEh3WSU3KGxm2jTopbV3dLBY8W /kbbKk3H1Xaz/iavdyaI7B6YshxXZaxNQ51EswI76MyA7SO51sn7DbdCXQqHv+tkIhnU+Ub8 h+GtXU6NutYUS2qNL2pEyXS8HdnW5nx9vlEJU0sHNMtUusEBLg0hW6AZ7tYSCNLSrULVS52G Quf/RuW/C9m7TVFmGCKshxFlhs2Wk9xqCtxqN3IC//ZufQPuHrG7lWNxTC+gCz2ygVvTBxRc XNkinYrtRN0laxokux7oU2rPNbYPiePmCHtfm0p953rP6rW+exxpWD0nXtL/FrA7bu6I/eng 5O4gXOB0jhiPruI68Gs1l2uYyjbJ64Date3Y8To1wG2gdaDeXSwiixhFFreLrJtpZBHryHwG sk4SGj0y2QbufpTd1rQ+3YVPO9oj0ho5NW+VP7ftBNrUdHUnU61XG2EzJglOxFESq1xz3MJ4 d1BR3W9/R+7Gp+1349P2u/GpuRu/Nxg+YVvw1/5jffnbFwpJhLBK5mVO66aJub6QL3kh4jjB RPvPVVpQVsHpjH+txsfvdtShvuN3lLtcTS4FW7ofgZQnGGAom6Ztt6TbbkcLbuaKtH2Dg39d 8gm6vfjXCV+KkpB5kaTQJ703pAU7+5q0u5cbuTRNuxJWnaD9pHAy7hxdEClZeUn3t+W1XP6V T1YoI8gMdaIL30nJrvl8PqCLUMUUVILEGISLhMPYUNP8OpN1xPykF1oE4xVgeZdDuNyDl7hv erH5preabxp+76aXzduvUPtjO27ZISPwOFo4ZIQIDBGMbFNjbQW4Yb3nL/pOGMmmd5UCvgnl nawKrqCUukcoBbLvo6qbjHgPXNG4iQ4HGevCvYUd5iAS6xyUqWwwcu5YB/hpmnrkkXjUEaXg 6AXD4O3CLlcLfUfB179VSGQvWu+512/OnAjI+d7evjNsQ/dMPWehMZ+IQEo+edLQA2paPJcq LvBXMBpKe4Myzazzv5qFbREFIf5Lb0me7FBAxokIWjhbgXwgFZcRHU9NmEN0skFGnuWr2SUa z8t8PrW4DmRFMZfUAeQZ7ojbBEM8hfrk2WBvaO9O+Dcm1glj06lD/bfdWLVMZ+2Qa20d6lxs benLjjDwg0cXbsGuXx8bt70va1e6eX4Yfv5Is1Xp3lQycRtxPa9ut8orGYdu9hseJq5xwUPk H30HT4NX2HFAO0zqu5+6at4bJE7Xca4Uywp5r7I4uaIBLZrTtO/GsCgrdNDeX1bHBeDNCmTM afLGQf+PzkVlY0oJdNMFE2FOS9wOJvhYKU/wsI9LfoS8y2lSiaODyxwguOYntzHmOFDMqVEy 2FNhbuWdZfqCrNIp7qXimQmZlwg0Q5DHnQAELBbWNssZ9HLCuCUYVjpQIDmLbSq0qx2WNBfp cPQ0sqbR6ZFFjaEJr2oMDS1rng2ewqrm2YBumTWjfr8+9CCt2fh1+hX6DTAS4Z2woSx4Jb5b wWT1sgZSDutAqEmtDRqR1yP4LucKJqrYtz1R5oC9LKACmGvHCTUGH+QY78RFyNTCzQ+8qF2A wEyUjIm5kqrSqRvsjaK9QCRHO4EkifUBSXLrLrA38vYA+uzrAHujhv4btFr9SNxN+3sjpS6o mKOtvVFH1SMLkibKKaL2vVFT61iDTko/2I8qXSRHlS5JYkqXJLdW+sG+V+n02af0g/2G0hu0 WulI3E3pB/tKVVAxR1UH+x2VjixImiiniNIP9ptKxxp0UDrAjCqidJUcUbomCStdkygf1oh8 WI+HUR8WzK3knxHfuni0BC/LrfXDo/XDoxXM9x/n0fK/d+L4ubSBOsPOe9h0gglHUcM1lvlo PW+kwOJtrDxFHssr42aJHCcv3/8+/iOfQpeXxzYt0yrHc8lciXUFyLz6S/B7z9hdB6EmI2Od ouqQS1VmzWjUUiM7OB9YfrT1QlNbHU0qbUeQ68bv7Q40K3GWbM34046ctw1Gbcnr8G2JUd0t xrbD0Rdwu1Oo65CI3SJOt4SwDjFfI7J1t0jb0goI7i1ht1uiZNdk1lw3GTzbYXzbSNqGUz2s dhuYE8G0VQzuDqThuNsxZ6U4K98Fl83nsb1FlRzDZYokgssUyXq4zH4spw2dCTb+Tccf6OwH Ogvm+69EZ2/e1LOIrx+6ozNB7EVnwL0LOnuTZ0CLf0RwWpMohNig1O+B2IyAN8NuzQreAMWB MjaK4pCfIPcoCfFc8/ONkZ2WfcPITvPdGLLTHDeF7DTDu0B2mvmdIDsYbXeA7DTXTSM7zfjW yE5zugGya9iKDWG8Bl8b7TUSu+K+NuDXBfl1gX5+7Dfqjv2aJvgHCvyBAr0/P1Cgg/cCMHA9 HBgDgusiwe5wsCMm/N6gcCPI8PbwcOP40AMQHSnd09kOYtwUbLwz3HgHwHHzyPFuoeMdY8c7 Ao93hx43CB83gh/vFES2I8k14eRVMo9t75rkIJi0SEJY0iKhU54UihL+fOo55CldtPWJyUSj iNt5e6NGfoqadGeLRn6j3vk+uTazXbOzoHO+QdfN/nfY3onar+hmhqSB0WsLNn6dF4ukMkbF cHNYxbJp3g6Fesu6NLwpnKx4cv1gMPQd5G3VcVMFNfMSkD+QzS86Tm81ttt+toFsznnMLhm6 zaXhjaCIxYzOVGvvW/meCkXKmuVxXoDqZGtiK1eTHLM1betWi4RszVOyNU+DtgZhaLgfttkO HwYMdWE3a60L47Suc9wUWXZwOXaxLH5IJGnWsyya1eYsy2OyLE/CliWu0fUsi4vlNmZZNNuu lqUtww0tSxegvp5laQO/IcsSRDd0e3RdI9NmZbqYmS52Zj1DsyFLsxlz47c3tzE6t7Y6mzQ7 38XubNTw3JXlWd/03JXtuQPjc2vrsyETtIo8+m2SYwZo1fLot0WC3XN/iOYH/nwcfIZHrmrd 5xs8P/GnlKNZW3yj6n3t1h9J1+JraH8orBba8tZPm1rBJzGAyS/zJPsrdBWMLqpRnJNTvG5T v7UkHgLRz6qIX2XUR0kUirqQ0rs2eMVLXJYyohwZhtbQaF7RozpbYvmloV9rV6b0DS1voXTt ScsvrqMFLtpBC/c0j/pVu9fYcqsFY4HGdRtDlFOTSr91agoJBcNQpQUr8gEGm/itcWHPSBKy 7/KVGVGGq2Yjj+qXH7L0n8L1hH4sLAJj4wwHqPBRNMq/HYn8mOJepFNxb5CaZ0CV8Ed/Fq4+ XaBFT+UOb5Rr5At2jtwYhTkbOYGVRRxgaIb8QoX6W2XpJK2+6ch/AtPogKKJeCj6Zi3YfNwv HNA1ailk/tjbdeZOphiykZgs2MuOfA8fh/O4vZ84PD/yPPsb2M8SjwF7c0VDx4Q7WCfrJUQ2 wetFxZtS6wfB7JeNXcPmNoAg3SYXYU/IU7ODhpsiCNWzpX93qGkUs9Ico00P3r5VhqEDZ9y3 jYLWkNEJ1rY+I9QnqhDKDBXUpUzvM+1Rcscx776o5WjEbwQGnoe/VSYT7jn8PHngIUR1/db2 kIWfTVwDPgYXsKuWqEEWSSt8lKtXERka/hKRF0x8FGWiX07FAQS007hbwSnWM1pIEQa+1NCv xGAgeGyjTKdcn1IoJfrzhBVZFulVUnEr4op+rNi5kP3RPHtkv1RsYow0srePwMa77xKj+LjF Rpy1zJILBvwxiwYr2RMbve+k1yXZCnLdCjPc8vNq1iqAW+6gQh9U8JlbVob4tKjHmKg7qIhC ohupjcvMrVIwzsJmOkOzwHiwhbVK1UnRYP+xSP++Id647Vtb1aqjJAXn8+Q8L8iuoIV7dkAP 1e4+HQz3/A4cd3GsIOtZgSGE8QtawfdCJPyIIT4JufTABm7TbxRHQcARMGtIRFCT/3MlIjZA IdIK6gb3oD0FUq232PWyU639LDykHwAKQD4BkpwFIxFvf7TWAwIIynmyb8Lb2C/LWfUXAF1i 8uS8zOf4IsCV9eqqnC3X2T+SY+yEPiLCoRdBkgmicdOpUJejPXK2jh4/GYxG7cpEwfVzKup5 lQpKPQepd/AAWQlTVApg4X+KIi9EFLCU5jAn7LjFDsYjTH0LPh3g8z2S7Eq904GRgqAcCiW2 IzV+a9+D1onUmRtZyjxJ1PIikf2Oz4M3PJuBkl8csZGXwHr3NfCQsfWKcY3ces9YrnyamYIP pDoLcQtLeqSMPu7ayqf9eVccD/UgRR7kCqsh6HIX47cc+2tSfJPwsimxB4SKNbEZZvZDQxJM iSfQ1ApZxnhJF0sgUsvhgfsokebmPk7kFu950Bh7MPX6RJwZVa8WqgO/bpSwyHtHeE5UgbvQ 06Sd0HAVR8NVOxqu2tFwZZ11fkKTBf61T3DYGvmZeoYFoS8dLp7Q4zGViY62WIHyeFbiYBcU 6vQuNi0g5x17qvozKbBJwfT+4+3LM1LfAAbGgN2/fx9s4f375K0Ac6hes7tveVJhdl1l07kI FkjQmqx2DtLoMJ/KYyVW3B6crnkJJD/Jp9w+8IwIXdpXfEXonCO0R4YphTXKs4l4CA65aVYL DCAHnZPhyeMSu5FcUmC7YV+jM9hsBvYp08LvUHa19pADJxyckZnVBDVsPvUleRca1s5W84Sl fuLWIrzFssTLIRZBKwKzWBTfsdDaoVZ4KJr5J+Cpny7oe2D7WmjxBjWxU2/zRhTzgkdvHbxO iMiy0GYSfCertVH+vU9nxaVeG4kEWrITlA3kbc6JTRUcmwCn3vPh2o9jvh62z0DdZ6JrNBGr 4ExkkoMzkUUSmoksEvLLPMNdZ/rTTEO61SgC+MtiVjM+GApcNWXBM5jG1aJGD/hX+t7NDtgB K4M67CrDidubNxbXn2T08eFu8z3rbjlBkgeY3c1v3E1/JF/TxWph1hT86zLPuLy8M9wVk9OF fFAKueHAcJsHeIzf5DMglg2jXi6nQHf/D3hV2enfqgAA --k+w/mQv8wyuph6w0--