From 913794b1cb71cc7bba9850f8ed42c294d542fff4 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 18 Jan 2023 08:40:40 +0000 Subject: ada: Simplify dramatically ghost code for proof of System.Arith_Double Using Inline_For_Proof annotation on key expression functions makes it possible to remove hundreds of lines of ghost code that were previously needed to guide provers. gcc/ada/ * libgnat/s-aridou.adb (Big3, Is_Mult_Decomposition) (Is_Scaled_Mult_Decomposition): Add annotation for inlining. (Double_Divide, Scaled_Divide): Simplify and remove ghost code. (Prove_Multiplication): Add calls to lemmas to make proof go through. * libgnat/s-aridou.ads (Big, In_Double_Int_Range): Add annotation for inlining. --- gcc/ada/libgnat/s-aridou.adb | 428 +++++-------------------------------------- gcc/ada/libgnat/s-aridou.ads | 12 +- 2 files changed, 56 insertions(+), 384 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 15f8764..dbf0f42 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -139,7 +139,9 @@ is (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1)) + Big_2xxSingle * Big (Double_Uns (X2)) + Big (Double_Uns (X3))) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); -- X1&X2&X3 as a big integer function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean @@ -1063,17 +1065,10 @@ is T1 := Ylo * Zlo; - pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo)) - + Big (Double_Uns'(Ylo * Zhi))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Yhi * Zlo)), Big (Double_Uns'(Ylo * Zhi))); - pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (Mult = Big_2xxSingle * Big (T2) - + Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))); Lemma_Mult_Distribution (Big_2xxSingle, Big (T2), Big (Double_Uns (Hi (T1)))); @@ -1081,17 +1076,11 @@ is T2 := T2 + Hi (T1); - pragma Assert - (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (Hi (T2))), Big (Double_Uns (Lo (T2)))); Lemma_Double_Big_2xxSingle; - pragma Assert - (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big (Double_Uns (Lo (T1)))); if Hi (T2) /= 0 then R := X; @@ -1947,7 +1936,9 @@ is + Big_2xxSingle * Big_2xxSingle * D2 + Big_2xxSingle * D3 + D4) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function Is_Scaled_Mult_Decomposition (D1, D2, D3, D4 : Big_Integer) @@ -1960,7 +1951,8 @@ is + D4) with Ghost, - Pre => Scale < Double_Size; + Annotate => (GNATprove, Inline_For_Proof), + Pre => Scale < Double_Size; -- Local lemmas @@ -2239,17 +2231,8 @@ is pragma Assert (Big_D3 = Big_T2); pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2); Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3); - pragma Assert (Big_D4 = Big_T3); pragma Assert - (By (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3), - By (Big_2xxSingle * Big_2xxSingle * Big_D12 = - Big_2xxSingle * Big_2xxSingle * Big_T1, - Big_D12 = Big_T1) - and then - By (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2, - Big_D3 = Big_T2) - and then - Big_D4 = Big_T3)); + (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Hi_Lo (T3, Hi (T3), Lo (T3)); @@ -2265,60 +2248,6 @@ is Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (Lo (T2))), Big (Double_Uns (Hi (T3)))); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (Big (Double_Uns (Hi (T1))), - Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))), - Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))), - Big (Double_Uns (Lo (T3)))), - -- Start from stating equality between the expanded values of - -- the right-hand side in the known and desired assertions over - -- Is_Scaled_Mult_Decomposition. - By (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))) - + Big_2xxSingle * - (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3)))) - + Big (Double_Uns (Lo (T3))) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * 0 - + Big_2xxSingle * Big_2xxSingle * Big_T1 - + Big_2xxSingle * Big_T2 - + Big_T3, - -- Now list all known equalities that contribute - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))) - + Big_2xxSingle * - (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3)))) - + Big (Double_Uns (Lo (T3))) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big (Double_Uns (Lo (T3))) - and then - By (Big_2xxSingle * Big_2xxSingle * Big (T1) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big_2xxSingle * Big (T1) - = Big_2xxSingle * Big_2xxSingle - * (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1))))) - and then - By (Big_2xxSingle * Big (T2) - = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))), - Big_2xxSingle * Big (T2) - = Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big (Double_Uns (Lo (T2))))) - and then - Big (T3) = Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big (Double_Uns (Lo (T3)))))); Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle, Big (Double_Uns (Lo (T1))), Big (Double_Uns (Hi (T2)))); @@ -2328,24 +2257,6 @@ is Double_Uns (Lo (T2)) + Double_Uns (Hi (T3))); Lemma_Add_Commutation (Double_Uns (Lo (T1)), Hi (T2)); Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T3)); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (Big (Double_Uns (Hi (T1))), - Big (Double_Uns (Lo (T1) or Hi (T2))), - Big (Double_Uns (Lo (T2) or Hi (T3))), - Big (Double_Uns (Lo (T3)))), - By (Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1) or Hi (T2))) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))), - Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1)) + Double_Uns (Hi (T2))) = - Big_2xxSingle * Big_2xxSingle - * (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))) - and then - Big_2xxSingle * Big (Double_Uns (Lo (T2) or Hi (T3))) = - Big_2xxSingle * Big (Double_Uns (Lo (T2))) - + Big_2xxSingle * Big (Double_Uns (Hi (T3))))); end Prove_Dividend_Scaling; -------------------------- @@ -2360,13 +2271,30 @@ is Lemma_Hi_Lo (T3, Hi (T3), S2); Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Lo (Zu)), T1); Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Hi (Zu)), T2); - pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = - Big_2xxSingle * Big (T2) + Big (T1)); + Lemma_Mult_Distribution (Big (Double_Uns (Q)), + Big_2xxSingle * Big (Double_Uns (Hi (Zu))), + Big (Double_Uns (Lo (Zu)))); + Lemma_Substitution + (Big (Double_Uns (Q)) * Big (Zu), + Big (Double_Uns (Q)), + Big (Zu), + Big_2xxSingle * Big (Double_Uns (Hi (Zu))) + + Big (Double_Uns (Lo (Zu))), + Big_0); pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) - + Big_2xxSingle * Big (Double_Uns (S2)) + + Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big_2xxSingle * Big (Double_Uns (Hi (T1))) + Big (Double_Uns (S3))); + Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T1)); + pragma Assert + (By (Big (Double_Uns (Q)) * Big (Zu) = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) + + Big_2xxSingle * Big (T3) + + Big (Double_Uns (S3)), + Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big_2xxSingle * Big (Double_Uns (Hi (T1))) + = Big_2xxSingle * Big (T3))); pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1)); Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2)); pragma Assert @@ -2375,20 +2303,6 @@ is Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle, Big (Double_Uns (Hi (T3))), Big (Double_Uns (Hi (T2)))); - pragma Assert - (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) - = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))); - pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) - + Big_2xxSingle * Big (Double_Uns (S2)) - + Big (Double_Uns (S3))); - pragma Assert - (By (Big (Double_Uns (Q)) * Big (Zu) = Big3 (S1, S2, S3), - Big3 (S1, S2, S3) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) - + Big_2xxSingle * Big (Double_Uns (S2)) - + Big (Double_Uns (S3)))); end Prove_Multiplication; ------------------------------------- @@ -2596,58 +2510,25 @@ is Lemma_Abs_Commutation (X); Lemma_Abs_Commutation (Y); Lemma_Mult_Decomposition (Mult, Xu, Yu, Xhi, Xlo, Yhi, Ylo); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)), - D4 => Big (Double_Uns'(Xlo * Ylo)))); T1 := Xlo * Ylo; D (4) := Lo (T1); D (3) := Hi (T1); Lemma_Hi_Lo (T1, D (3), D (4)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)) - + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); if Yhi /= 0 then T1 := Xlo * Yhi; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T1))) - + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); T2 := D (3) + Lo (T1); Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (T2), - D4 => Big (Double_Uns (D (4))))); Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (D (3))), Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Hi (T2))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T2))), - D4 => Big (Double_Uns (D (4))))); D (3) := Lo (T2); D (2) := Hi (T1) + Hi (T2); @@ -2657,30 +2538,11 @@ is pragma Assert (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (D (2)))); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))), - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); if Xhi /= 0 then T1 := Xhi * Ylo; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))) - + Big (Double_Uns (Hi (T1))), - D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - (By (Big_2xxSingle * Big (T1) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big (T1) = - Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))))))); T2 := D (3) + Lo (T1); @@ -2699,75 +2561,18 @@ is T3 := D (2) + Hi (T1); Lemma_Add_Commutation (Double_Uns (D (2)), Hi (T1)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (T3) - + Big (Double_Uns (Hi (T2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Add_Commutation (T3, Hi (T2)); T3 := T3 + Hi (T2); T2 := Double_Uns'(Xhi * Yhi); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (T2) + Big (T3), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))), - D2 => Big (Double_Uns (Lo (T2))) + Big (T3), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - By (Big_2xxSingle * Big_2xxSingle * Big (T2) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T2))), - Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big (Double_Uns (Lo (T2)))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T2)))))); T1 := T3 + Lo (T2); D (2) := Lo (T1); Lemma_Add_Commutation (T3, Lo (T2)); - pragma Assert - (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))), - D2 => Big (T1), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - By (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))), - D (2) = Lo (T1)) - and then - By (Big_2xxSingle * Big_2xxSingle * Big (T1) = - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))), - Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (Lo (T1)))))); D (1) := Hi (T2) + Hi (T1); @@ -2777,72 +2582,31 @@ is pragma Assert (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1)))); - - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (D (1))) - = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * - (Big (Double_Uns (Hi (T2)) + Double_Uns (Hi (T1)))))); else D (1) := 0; - - pragma Assert - (By (Is_Mult_Decomposition - (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Yhi)) = 0 - and then Big (Double_Uns'(Xhi * Ylo)) = 0 - and then Big (Double_Uns (D (1))) = 0)); end if; - pragma Assert - (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), - D2 => Big (Double_Uns (D (2))), - D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4))))); else - pragma Assert - (By (Is_Mult_Decomposition - (D1 => 0, - D2 => 0, - D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Yhi)) = 0 - and then Big (Double_Uns'(Xlo * Yhi)) = 0)); - if Xhi /= 0 then T1 := Xhi * Ylo; Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (Hi (T1))), D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo)) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big (Double_Uns (Lo (T1))))); + D4 => Big (Double_Uns (D (4))))); T2 := D (3) + Lo (T1); Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3)); pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (Hi (T1))), D3 => Big (T2), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big (T2) = - Big_2xxSingle * - (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3)))))); + D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); D (3) := Lo (T2); @@ -2855,31 +2619,20 @@ is (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (D (2)))); pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (D (2))), D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - and then - Big_2xxSingle * Big (T2) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))) - and then - Big (Double_Uns (Lo (T2))) = Big (Double_Uns (D (3))))); + D4 => Big (Double_Uns (D (4))))); else D (2) := 0; pragma Assert - (By (Is_Mult_Decomposition + (Is_Mult_Decomposition (D1 => 0, D2 => Big (Double_Uns (D (2))), D3 => Big (Double_Uns (D (3))), - D4 => Big (Double_Uns (D (4)))), - Big (Double_Uns'(Xhi * Ylo)) = 0 - and then Big (Double_Uns (D (2))) = 0)); + D4 => Big (Double_Uns (D (4))))); end if; D (1) := 0; @@ -2918,14 +2671,6 @@ is if Zhi = 0 then if D (1) /= 0 or else D (2) >= Zlo then if D (1) > 0 then - pragma Assert - (By (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (1))), - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) >= 0 - and then - Big_2xxSingle * Big (Double_Uns (D (3))) >= 0 - and then - Big (Double_Uns (D (4))) >= 0)); Lemma_Double_Big_2xxSingle; Lemma_Mult_Positive (Big_2xxDouble, Big_2xxSingle); Lemma_Ge_Mult (Big (Double_Uns (D (1))), @@ -2967,13 +2712,7 @@ is Lemma_Hi_Lo (D (1) & D (2), D (1), D (2)); Lemma_Ge_Commutation (D (1) & D (2), Zu); pragma Assert - (By (Mult >= Big_2xxSingle * Big_2xxSingle * Big (D (1) & D (2)), - By (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))), - Big_2xxSingle * Big (Double_Uns (D (3))) >= 0 - and then - Big (Double_Uns (D (4))) >= 0))); + (Mult >= Big_2xxSingle * Big_2xxSingle * Big (D (1) & D (2))); Prove_Overflow; Raise_Error; @@ -2990,16 +2729,7 @@ is Lemma_Hi_Lo (D (1) & D (2), D (1), D (2)); Lemma_Lt_Commutation (D (1) & D (2), Zu); pragma Assert - (By (Mult < Big_2xxDouble * Big (Zu), - By (Mult < Big_2xxSingle * Big_2xxSingle * (Big (Zu) - 1) - + Big_2xxSingle * Big_2xxSingle, - Big_2xxSingle * Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - <= Big_2xxSingle * Big_2xxSingle * (Big (Zu) - 1) - and then - Big_2xxSingle * Big (Double_Uns (D (3))) + Big (Double_Uns (D (4))) - < Big_2xxSingle * Big_2xxSingle))); + (Mult < Big_2xxDouble * Big (Zu)); Shift := Single_Size; Mask := Single_Uns'Last; @@ -3198,13 +2928,7 @@ is Big_2xxSingle * Big (Double_Uns (D (3))) + Big (Double_Uns (D (4)))); pragma Assert - (By (Big (D (1) & D (2)) < Big (Zu), - By (Big (D (1) & D (2)) * Big_2xxDouble < Big (Zu) * Big_2xxDouble, - By (Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))) >= 0, - By (Big_2xxSingle * Big (Double_Uns (D (3))) >= 0, - Big (Double_Uns (D (3))) >= 0 and then Big_2xxSingle >= 0) - and then Big (Double_Uns (D (4))) >= 0)))); + (Big (D (1) & D (2)) < Big (Zu)); -- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2) @@ -3219,11 +2943,6 @@ is Big_2xxSingle * Big3 (X1, X2, X3) + Big (Double_Uns (X4)) = Big3 (X2, X3, X4); - procedure Prove_Mult_Big_2xxSingle_Twice (X : Big_Integer) - with - Ghost, - Post => Big_2xxSingle * Big_2xxSingle * X = Big_2xxDouble * X; - --------------------------- -- Prove_First_Iteration -- --------------------------- @@ -3231,12 +2950,10 @@ is procedure Prove_First_Iteration (X1, X2, X3, X4 : Single_Uns) is null; - procedure Prove_Mult_Big_2xxSingle_Twice (X : Big_Integer) is null; - -- Local ghost variables Qd1 : Single_Uns := 0 with Ghost; - D234 : Big_Integer := 0 with Ghost; + D234 : Big_Integer with Ghost; D123 : constant Big_Integer := Big3 (D (1), D (2), D (3)) with Ghost; D4 : constant Big_Integer := Big (Double_Uns (D (4))) @@ -3399,26 +3116,9 @@ is Lemma_Mult_Non_Negative (Big_2xxSingle, Big (Double_Uns (D (J + 1)))); pragma Assert - (By (Big3 (D (J), D (J + 1), D (J + 2)) >= + (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (J))), - By (Big3 (D (J), D (J + 1), D (J + 2)) - - Big_2xxSingle * Big_2xxSingle - * Big (Double_Uns (D (J))) - = Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2))), - Big3 (D (J), D (J + 1), D (J + 2)) = - Big_2xxSingle - * Big_2xxSingle * Big (Double_Uns (D (J))) - + Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2)))) - and then - By (Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2))) >= 0, - Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0 - and then - Big (Double_Uns (D (J + 2))) >= 0 - ))); + * Big (Double_Uns (D (J)))); Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1)); Lemma_Ge_Mult (Big (Double_Uns (D (J))), Big (Double_Uns'(1)), @@ -3426,13 +3126,8 @@ is Big (Double_Uns'(1)) * Big_2xxDouble); pragma Assert (Big_2xxDouble * Big (Double_Uns'(1)) = Big_2xxDouble); - Prove_Mult_Big_2xxSingle_Twice (Big (Double_Uns (D (J)))); pragma Assert - (By (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxDouble, - By (Big (Double_Uns (D (J))) * - (Big_2xxSingle * Big_2xxSingle) >= Big_2xxDouble, - Big (Double_Uns (D (J))) * Big_2xxDouble - >= Big_2xxDouble))); + (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxDouble); pragma Assert (False); end if; @@ -3452,34 +3147,11 @@ is else pragma Assert (Qd1 = Qd (1)); pragma Assert - (By (Mult * Big_2xx (Scale) = - Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) - + Big3 (S1, S2, S3) - + Big3 (D (2), D (3), D (4)), - Big3 (D (2), D (3), D (4)) = D234 - Big3 (S1, S2, S3))); - pragma Assert - (By (Mult * Big_2xx (Scale) = + (Mult * Big_2xx (Scale) = Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + Big (Double_Uns (Qd (2))) * Big (Zu) + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))), - Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) - = Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) - and then - Big3 (S1, S2, S3) = Big (Double_Uns (Qd (2))) * Big (Zu) - and then - By (Big3 (D (2), D (3), D (4)) - = Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))), - Big3 (D (2), D (3), D (4)) - = Big_2xxSingle * Big_2xxSingle * - Big (Double_Uns (D (2))) - + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))) - and then - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - = 0) - )); + + Big (Double_Uns (D (4)))); end if; end loop; end; @@ -3631,12 +3303,6 @@ is Lemma_Add_Commutation (Double_Uns (X1), Y1); Lemma_Add_Commutation (Double_Uns (X2), Y2); Lemma_Add_Commutation (Double_Uns (X3), Y3); - pragma Assert (Double_Uns (Single_Uns'(X1 + Y1)) - = Double_Uns (X1) + Double_Uns (Y1)); - pragma Assert (Double_Uns (Single_Uns'(X2 + Y2)) - = Double_Uns (X2) + Double_Uns (Y2)); - pragma Assert (Double_Uns (Single_Uns'(X3 + Y3)) - = Double_Uns (X3) + Double_Uns (Y3)); end Lemma_Add3_No_Carry; --------------------- diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads index 58aa775..b22f0db 100644 --- a/gcc/ada/libgnat/s-aridou.ads +++ b/gcc/ada/libgnat/s-aridou.ads @@ -77,18 +77,24 @@ is function Big (Arg : Double_Int) return Big_Integer is (Signed_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); package Unsigned_Conversion is new BI_Ghost.Unsigned_Conversions (Int => Double_Uns); function Big (Arg : Double_Uns) return Big_Integer is (Unsigned_Conversion.To_Big_Integer (Arg)) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function In_Double_Int_Range (Arg : Big_Integer) return Boolean is (BI_Ghost.In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last))) - with Ghost; + with + Ghost, + Annotate => (GNATprove, Inline_For_Proof); function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int with -- cgit v1.1