Spark_Math

A formally verified mathematical library written in SPARK/Ada, providing common mathematical functions for both integer and fixed-point types with compile-time proof of correctness.

Features

Integer Math (Spark_Math.Integer)

Fixed-Point Math (Spark_Math.Fixed)

Roadmap

The goal is to provide SPARK-verified equivalents of Ada.Numerics.Generic_Elementary_Functions for fixed-point and integer types.

Planned Functions

Implementation Notes

Unlike floating-point implementations, fixed-point math requires:

• CORDIC algorithms for trigonometric functions (no FPU dependency)
• Polynomial approximations with bounded error analysis
• Range reduction techniques proven correct in SPARK
• Cycle parameter support for degree/radian flexibility

Contributions for any of these functions are welcome!

Usage

Integer Math Example

with Spark_Math.Integer;

procedure Example is
   --  Instantiate for your integer type
   package My_Math is new Spark_Math.Integer (Integer);
   
   Result : Integer;
begin
   --  Square root (floor)
   Result := My_Math.Sqrt (17);      --  Returns 4
   
   --  Exponentiation
   Result := My_Math.Power (2, 10);  --  Returns 1024
   
   --  Greatest common divisor
   Result := My_Math.GCD (48, 18);   --  Returns 6
   
   --  Max and Min
   Result := My_Math.Max (5, 3);     --  Returns 5
   Result := My_Math.Min (5, 3);     --  Returns 3
end Example;

Fixed-Point Math Example

with Spark_Math.Fixed;

procedure Example is
   --  Define your fixed-point type
   type Voltage is delta 0.001 range 0.0 .. 100.0;
   
   --  Instantiate for your type
   package Voltage_Math is new Spark_Math.Fixed (Voltage);
   
   Result : Voltage;
begin
   --  Square root (approximation within 'Small)
   Result := Voltage_Math.Sqrt (4.0);   --  Returns ~= 2.0
   Result := Voltage_Math.Sqrt (2.0);   --  Returns ~= 1.414
   
   --  Max and Min
   Result := Voltage_Math.Max (3.5, 2.1);  --  Returns 3.5
   Result := Voltage_Math.Min (3.5, 2.1);  --  Returns 2.1
end Example;

SPARK Verification

This library is designed for formal verification with SPARK. All functions include:

• Preconditions (Pre): Specify valid input constraints
• Postconditions (Post): Guarantee output properties
• Loop invariants: Enable proof of loop correctness
• No runtime exceptions: All potential issues are caught at proof time

Verification Status

SPARK defines five proof levels:

Contributing

Contributions are welcome!

License

This project is licensed under the Apache-2.0 WITH LLVM-exception license. See LICENSE for details.