SPARK-Ada Using GNATProve to Assume a Postcondition of a GCC Intrinsic Function

Question

I would like to create a function in SPARK_Mode that utilizes the GNAT GCC intrinsic function "__builtin_ctzll".

with Interfaces; use Interfaces;
package GCC_Intrinsic with
   SPARK_Mode
is

   function DividesLL (A, B : Unsigned_64) return Boolean is (B mod A = 0) with
      Ghost,
      Pre => A /= 0;

   function CTZLL (X : Unsigned_64) return Natural with
      Pre  => X /= 0,
      Post => CTZLL'Result in 0 .. Unsigned_64'Size - 1
      and then DividesLL (Unsigned_64 (2)**CTZLL'Result, X)
      and then
      (for all Y in CTZLL'Result + 1 .. Unsigned_64'Size - 1 =>
         not DividesLL (Unsigned_64 (2)**Y, X));
   
   pragma Import (Intrinsic, CTZLL, "__builtin_ctzll");

end GCC_Intrinsic;

I would like to assume the postcondition to be true since it is the definition of the number of trailing zeros which is implied by the documentation. However, I am unsure how to accomplish this, having read much documentation and having tried to use "pragma Assume". I am relatively new to Ada/SPARK and am using GNAT Community 2020. Can someone please help me solve this issue so that gnatprove is able to prove the postcondition of CTZLL?

Answer 1

When I formulate the postcondition (contract) of __builtin_ctzll using Shift_Right, I'm able proof (using GNAT CE 2020 and proof level 1) that test.adb is free of run-time errors if it would be run.

Note: Related documentation: SPARK user's manual, section 7.4.5: Writing Contracts on Imported Subprograms.

intrinsic.ads

pragma Assertion_Policy (Check);

with Interfaces; use Interfaces;

package Intrinsic with SPARK_Mode is

   --  Count Trailing Zeros (long long unsigned).
   
   function CTZLL (X : Unsigned_64) return Natural with
     Pre  => X /= 0,       
     Post => CTZLL'Result in 0 .. Unsigned_64'Size - 1 and
             (for all I in 0 .. CTZLL'Result - 1 =>
                (Shift_Right (X, I) and 2#1#) = 2#0#) and 
             (Shift_Right (X, CTZLL'Result) and 2#1#) = 2#1#;

   --  You could also use aspects (Import, Convention, External_Name).
   pragma Import (Intrinsic, CTZLL, "__builtin_ctzll");
   
end Intrinsic;

test.adb

pragma Assertion_Policy (Check);

with Interfaces; use Interfaces;
with Intrinsic;  use Intrinsic;

procedure Test with SPARK_Mode is
begin
   
   --  Absence of Run-Time Errors (AoRTE) for this program can be proven:
   --  Assert_Failure will not be raised at runtime.
   
   pragma Assert (CTZLL ( 1) = 0);
   pragma Assert (CTZLL ( 2) = 1);
   pragma Assert (CTZLL ( 3) = 0);
   pragma Assert (CTZLL ( 4) = 2);
   pragma Assert (CTZLL ( 5) = 0);
   pragma Assert (CTZLL ( 6) = 1);
   pragma Assert (CTZLL ( 7) = 0);
   pragma Assert (CTZLL ( 8) = 3);
   pragma Assert (CTZLL ( 9) = 0);
   pragma Assert (CTZLL (10) = 1);
      
   pragma Assert (CTZLL (2 ** 63    ) = 63);
   pragma Assert (CTZLL (2 ** 64 - 1) =  0);
   
end Test;

output (of gnatprove)

$ gnatprove -P default.gpr -j0 -u test.adb --level=1 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
test.adb:12:19: info: precondition proved
test.adb:12:19: info: assertion proved
[...]
test.adb:24:19: info: precondition proved
test.adb:24:19: info: assertion proved

---

For those not familiar with __builtin_ctzll: returns the number of trailing 0-bits in x, starting at the least significant bit position. If x is 0, the result is undefined. See also here. Example:

main.adb

with Ada.Text_IO;         use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
with Interfaces;          use Interfaces;
with Intrinsic;           use Intrinsic;

procedure Main is
begin
   for K in 1 .. 10 loop
      Put (K, Width => 3);
      Put (K, Width => 9, Base => 2);
      Put (CTZLL (Unsigned_64 (K)), Width => 4);
      New_Line;
   end loop;
end Main;

output (of Main)

$ ./obj/main
  1     2#1#   0
  2    2#10#   1
  3    2#11#   0
  4   2#100#   2
  5   2#101#   0
  6   2#110#   1
  7   2#111#   0
  8  2#1000#   3
  9  2#1001#   0
 10  2#1010#   1