diff mbox series

[Ada] Fix proof of runtime unit System.Wid_*

Message ID 20220902075322.GA1121031@poulhies-Precision-5550
State New, archived
Headers
Series [Ada] Fix proof of runtime unit System.Wid_* |

Commit Message

Marc Poulhiès Sept. 2, 2022, 7:53 a.m. UTC 
  Regain the proof of System.Wid_* after changes in provers and Why3.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/s-widthu.adb (Lemma_Euclidean): Lemma to prove the
	relation between the quotient/remainder of a division.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb
--- a/gcc/ada/libgnat/s-widthu.adb
+++ b/gcc/ada/libgnat/s-widthu.adb
@@ -73,6 +73,14 @@  package body System.Width_U is
         Ghost,
         Post => X / Y / Z = X / (Y * Z);
 
+      procedure Lemma_Euclidian (V, Q, F, R : Big_Integer)
+      with
+        Ghost,
+        Pre  => F > 0 and then Q = V / F and then R = V rem F,
+        Post => V = Q * F + R;
+      --  Ghost lemma to prove the relation between the quotient/remainder of
+      --  division by F and the value V.
+
       ----------------------
       -- Lemma_Lower_Mult --
       ----------------------
@@ -104,6 +112,12 @@  package body System.Width_U is
          pragma Assert (X / YZ = XYZ + R / YZ);
       end Lemma_Div_Twice;
 
+      ---------------------
+      -- Lemma_Euclidian --
+      ---------------------
+
+      procedure Lemma_Euclidian (V, Q, F, R : Big_Integer) is null;
+
       --  Local variables
 
       W : Natural;
@@ -152,7 +166,7 @@  package body System.Width_U is
             R : constant Big_Integer := Big (T_Init) rem F with Ghost;
          begin
             pragma Assert (Q < Big_10);
-            pragma Assert (Big (T_Init) = Q * F + R);
+            Lemma_Euclidian (Big (T_Init), Q, F, R);
             Lemma_Lower_Mult (Q, Big (9), F);
             pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
             pragma Assert (Big (T_Init) < Big_10 * F);