diff options
author | Claire Dross <dross@adacore.com> | 2022-07-12 11:34:31 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2022-09-02 09:34:06 +0200 |
commit | e973ea0151a1551947fcdcadaeb9406789324b06 (patch) | |
tree | 6ecc4ac659c302648e363988a210fed016cab833 /gcc | |
parent | bf52ee6a4f86cbd60770fc22ad5abce0f437762a (diff) | |
download | gcc-e973ea0151a1551947fcdcadaeb9406789324b06.zip gcc-e973ea0151a1551947fcdcadaeb9406789324b06.tar.gz gcc-e973ea0151a1551947fcdcadaeb9406789324b06.tar.bz2 |
[Ada] Fix proof of runtime unit System.Exp_Mod
Regain the proof of System.Exp_Mod after changes in provers and Why3.
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.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/s-expmod.adb | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/gcc/ada/libgnat/s-expmod.adb b/gcc/ada/libgnat/s-expmod.adb index 527338d..f1fdf71 100644 --- 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)); |