name = "spark_math"
description = "Formally verified mathematical library in SPARK"
version = "0.1.0"

authors = ["Heziode"]
maintainers = ["Heziode <heziode@protonmail.com>"]
maintainers-logins = ["heziode"]
licenses = "Apache-2.0 WITH LLVM-exception"
website = ""
tags = ["spark", "verification", "math", "sqrt", "fixed-point"]

long-description = """
# Spark_Math

[![License](https://img.shields.io/badge/license-Apache--2.0%20WITH%20LLVM--exception-blue.svg)](LICENSE)
[![SPARK](https://img.shields.io/badge/SPARK-Gold-gold.svg)](https://www.adacore.com/about-spark)

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 sqrt 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!

## Usage

### Integer Math Example

```ada
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

```ada
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:

| 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 |

## Contributing

Contributions are welcome!

## License

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

"""
[origin]
commit = "8939f758a129b2dc44094de32e373f2243b9c6f7"
url = "git+https://github.com/adarium-labs/spark_math.git"