I stumbled on an interesting (to me) GNATprove (FSF 16.1.0, possibly other versions) behavior last week. Since it took me some time to figure out what was going on and how to puzzle around it, I thought it might be worth sharing.
Basically, sometimes it seems that making an assertion involving a specific but somewhat arbitrary number (as long as it’s…checks notes…not a certain number) can help gnatprove with proof obligations regarding all such numbers.
Has anyone else encountered this situation and/or used this trick/strategy to nudge gnatprove?
potato.ads
with Ada.Unchecked_Conversion;
with Interfaces; use Interfaces;
package Potato is
-- Fiddling with bijections between `Unsigned_64` values and length-64 bit
-- vectors.
--
-- `Ada.Unchecked_Conversion` does the trick, but we can also implement and
-- verify conversions that are done using bit shifts/masks. Along the way,
-- we stumble on an unexpected (at least to me) way to nudge `gnatprove`
-- in the right direction.
-- Ceremonial types for `Unsigned_64` and length-64 bit vectors.
type UInt1 is mod 2 with Size => 1;
subtype UInt64 is Unsigned_64;
type Idx_64 is range 0 .. 63;
type BV_64 is array (Idx_64) of UInt1 with Component_Size => 1, Size => 64;
-- `Unchecked_Conversion`s for `UInt64` <=> `BV_64`.
function Convert is new Ada.Unchecked_Conversion (
Source => UInt64,
Target => BV_64
);
function Convert is new Ada.Unchecked_Conversion (
Source => BV_64,
Target => UInt64
);
-- The `Unchecked_Conversion`s form a bijection.
procedure Lemma_Round_Trip_1 (X : UInt64)
with
Post => (X = Convert (Convert (X)));
procedure Lemma_Round_Trip_2 (V : BV_64)
with
Post => (V = Convert (Convert (V)));
-- Define conversions using bit shifting/masking:
function Convert_2 (X : UInt64) return BV_64 is
([for I in Idx_64 => UInt1 (Shift_Right (X, Natural (I)) and 1)]);
function Convert_2 (V : BV_64; I : Idx_64 := 0) return UInt64 is
(
declare
S : constant UInt64 := Shift_Left (UInt64 (V (I)), Natural (I));
begin
(if I = Idx_64'Last then
S
else
S + Convert_2 (V, I + 1))
)
with
Subprogram_Variant => (Increases => I);
-- These `Convert_2` functions also form a bijection.
--
-- Take a peek at the body of `Lemma_Round_Trip_3` for something a wee bit
-- interesting...
procedure Lemma_Round_Trip_3 (X : UInt64)
with
Post => X = Convert_2 (Convert_2 (X));
procedure Lemma_Round_Trip_4 (V : BV_64)
with
Post => V = Convert_2 (Convert_2 (V));
-- This is just `Lemma_Round_Trip_3`, but re-packaged with a universal
-- quantifier in its postcondition. Like `Lemma_Round_Trip_3`, it also needs
-- a little nudge.
procedure Lemma_Round_Trip_3_For_All
with
Post => (for all X in UInt64 => X = Convert_2 (Convert_2 (X)));
end Potato;
potato.adb
package body Potato is
procedure Lemma_Round_Trip_1 (X : UInt64) is null;
procedure Lemma_Round_Trip_2 (V : BV_64) is null;
procedure Lemma_Round_Trip_3 (X : UInt64) is
begin
-- This is interesting/weird/funny/odd:
--
-- It seems that we have to assert one of these guys to make
-- a happy `gnatprove`. You can pick your favorite `UInt64` to use in
-- a single assertion (...as long as you don't pick `0`):
--
-- pragma Assert (1 = Convert_2 (Convert_2 (1)));
-- ...etc...
-- pragma Assert (42 = Convert_2 (Convert_2 (42)));
-- ...etc...
-- pragma Assert (UInt64'Last = Convert_2 (Convert_2 (UInt64'Last)));
-- 42 is a good one - let's drop it in.
pragma Assert (42 = Convert_2 (Convert_2 (42)));
-- Interestingly, the following assertion won't help:
-- pragma Assert (0 = Convert_2 (Convert_2 (0)));
end Lemma_Round_Trip_3;
procedure Lemma_Round_Trip_4 (V : BV_64) is null;
procedure Lemma_Round_Trip_3_For_All is
begin
-- See `Lemma_Round_Trip_3` above for an explanation.
pragma Assert (42 = Convert_2 (Convert_2 (42)));
-- The following loop is optional/superfluous (leave it in if you like).
-- But an appropriate assertion above is necessary, it seems.
--
-- for X in UInt64 loop
-- pragma Loop_Invariant (
-- for all Y in UInt64'First .. X =>
-- Y = Convert_2 (Convert_2 (Y))
-- );
-- end loop;
end Lemma_Round_Trip_3_For_All;
end Potato;