* [Ada] Fix proof of runtime unit System.Exp_Mod
@ 2022-09-02 7:53 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:53 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
[-- Attachment #1: Type: text/plain, Size: 267 bytes --]
Regain the proof of System.Exp_Mod after changes in provers and Why3.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-expmod.adb (Lemma_Add_Mod): Add new lemma to factor
out a complex sub-proof.
(Exp_Modular): Add assertion to help proof.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1487 bytes --]
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb
--- a/gcc/ada/libgnat/s-expmod.adb
+++ b/gcc/ada/libgnat/s-expmod.adb
@@ -106,6 +106,13 @@ is
-------------------
procedure Lemma_Add_Mod (X, Y : Big_Natural; B : Big_Positive) is
+
+ procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) with
+ Pre => F /= 0,
+ Post => (Q * F + R) mod F = R mod F;
+
+ procedure Lemma_Euclidean_Mod (Q, F, R : Big_Natural) is null;
+
Left : constant Big_Natural := (X + Y) mod B;
Right : constant Big_Natural := ((X mod B) + (Y mod B)) mod B;
XQuot : constant Big_Natural := X / B;
@@ -119,6 +126,8 @@ is
(Left = ((XQuot + YQuot) * B + X mod B + Y mod B) mod B);
pragma Assert (X mod B + Y mod B = AQuot * B + Right);
pragma Assert (Left = ((XQuot + YQuot + AQuot) * B + Right) mod B);
+ Lemma_Euclidean_Mod (XQuot + YQuot + AQuot, B, Right);
+ pragma Assert (Left = (Right mod B));
pragma Assert (Left = Right);
end if;
end Lemma_Add_Mod;
@@ -259,6 +268,7 @@ is
pragma Assert (Equal_Modulo
((Big (Result) * Big (Factor)) * Big (Factor) ** (Exp - 1),
Big (Left) ** Right));
+ pragma Assert (Big (Factor) >= 0);
Lemma_Mult_Mod (Big (Result) * Big (Factor),
Big (Factor) ** (Exp - 1),
Big (Modulus));
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:53 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:53 [Ada] Fix proof of runtime unit System.Exp_Mod Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).