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)

Function	Description	Complexity
Sqrt	Integer square root (floor of √N)	O(log N)
Power	Exponentiation with overflow protection	O(Exp)
GCD	Greatest common divisor (Euclidean algorithm)	O(log min(A,B))
Max	Maximum of two values	O(1)
Min	Minimum of two values	O(1)

Fixed-Point Math (Spark_Math.Fixed)

Function	Description	Complexity
Sqrt	Square root approximation (within 'Small)	O(log(N/Small))
Max	Maximum of two values	O(1)
Min	Minimum of two values	O(1)

Roadmap

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

Planned Functions

Category	Functions	Status
Basic	Sqrt	✅ Implemented
Exponential	Log, Log(Base), Exp, **	⬚ Planned
Trigonometric	Sin, Cos, Tan, Cot	⬚ Planned
Inverse Trig	Arcsin, Arccos, Arctan, Arccot	⬚ Planned
Hyperbolic	Sinh, Cosh, Tanh, Coth	⬚ Planned
Inverse Hyperbolic	Arcsinh, Arccosh, Arctanh, Arccoth	⬚ Planned

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!

Installation

Using Alire

Add the dependency to your project:

alr with spark_math

Or add it manually to your alire.toml:

[[depends-on]]
spark_math = "^0.1.0"

Manual Installation

Clone the repository and add it to your GPR project path:

git clone https://github.com/heziode/spark_math.git

In your .gpr file:

with "spark_math.gpr";

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

Running GNATprove

cd tests
alr exec -- gnatprove -P spark_math_tests.gpr --mode=gold proof.adb

Verification Status

SPARK defines five proof levels:

Level	Description
Stone	Valid SPARK code
Bronze	Initialization and correct data flow
Silver	Absence of run-time errors (AoRTE)
Gold	Proof of key integrity properties
Platinum	Full functional proof of requirements

Package	Level
Spark_Math.Numerics_Core	🥇 Gold
Spark_Math.Integer	🥇 Gold
Spark_Math.Fixed	🥇 Gold

Project Structure

spark_math/
├── alire.toml                      # Alire package manifest
├── spark_math.gpr                  # Main GPR project file
├── src/
│   ├── spark_math.ads              # Root package
│   ├── spark_math-numerics_core.ads/.adb  # Generic core algorithms
│   ├── spark_math-integer.ads/.adb # Integer math package
│   └── spark_math-fixed.ads        # Fixed-point math package
├── tests/
│   ├── alire.toml                  # Test project manifest
│   ├── spark_math_tests.gpr        # Test GPR project file
│   └── src/
│       ├── test_runner.adb         # AUnit test runner
│       ├── test_integer_math.ads/.adb  # Integer math tests
│       └── test_fixed_math.ads/.adb    # Fixed-point math tests
└── README.md

Running Tests

cd tests
alr run

Why SPARK?

Unlike traditional runtime-checked libraries, Spark_Math provides:

1. Compile-time guarantees: Proofs eliminate entire classes of bugs
2. No runtime overhead: Checks are done at proof time, not runtime
3. Overflow protection: Power function has preconditions preventing overflow
4. Division safety: All divisions are protected against divide-by-zero
5. Formal documentation: Contracts serve as executable specifications

Contributing

Contributions are welcome!

Please, follow the project's Ada style guide defined in STYLE_GUIDE.md.

License

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