Formally verified, bias-free entropy conversion engine in Ada/SPARK

[Avila]

Hi everyone,

Quick note: English is my second language, so I am using an AI to help translate this into proper technical English, as Spanish is my native tongue.

I wanted to share a complete architecture designed in Ada/SPARK for high-integrity cryptography. It is a secure, bias-free entropy conversion engine that maps raw random bytes (harvested via Windows ProcessPrng / BcryptGenRandom) into human-readable sequences.

Note on Architecture: The production package declares 14 specialized procedures for different charset variations. Structurally, all 14 procedures are divided into and implement one of the 3 core algorithmic patterns. The Chain_Safe_Token procedure in the .ads section below is provided as an explicit example of how these 14 entry points are specified.

The entire core codebase achieves 100% Proved status under gnatprove. It guarantees zero runtime exceptions, zero buffer overflows, zero division-by-zero, and proven loop termination. This formal math allows the implementation to safely strip runtime checks in production via -gnatp, unlocking performance ranges between 1100 MB/s and 1400 MB/s depending on the targeted character sets.

---

4. Summary of SPARK Analysis Results

Here is the full verification report generated by gnatprove. The engine achieved a flawless 100% Proved status across 925 total verification paths with absolutely zero unproved properties:

---------------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results        Total       Flow   CodePeer                                          Provers   Justified   Unproved
---------------------------------------------------------------------------------------------------------------------------------
Data Dependencies                32         32          .                                                .           .          .
Flow Dependencies                21         21          .                                                .           .          .
Initialization                   20         20          .                                                .           .          .
Non-Aliasing                      .          .          .                                                .           .          .
Run-time Checks                 620          .          .    620 (CVC4 89%, Trivial 7%, Z3 4%, colibri 0%)           .          .
Assertions                      105          .          .                105 (CVC4 97%, Trivial 2%, Z3 1%)           .          .
Functional Contracts            103          .          .               103 (CVC4 89%, Trivial 2%, Z3 10%)           .          .
LSP Verification                  .          .          .                                                .           .          .
Termination                      24          .          .                                        24 (CVC4)           .          .
Concurrency                       .          .          .                                                .           .          .
---------------------------------------------------------------------------------------------------------------------------------
Total                           925    73 (8%)          .                                        852 (92%)           .          .

Max steps used for successful proof: 33855

Questions for Discussion

I would love to gather your feedback on this implementation, especially on two fronts:

1. Type-Driven Design vs Explicit Contracts: Do you consider this strict subtype clamping approach cleaner than writing expansive runtime preconditions for dynamic charsets in SPARK?
2. Timing Resiliency: Since the execution profile variations depend exclusively on the host hardware/kernel entropy rejection rates, do you agree this eliminates standard state-dependent timing vulnerabilities without needing full constant-time logic?

Thanks for reading, and I’m happy to dive deeper into other procedures if you’d like to look at the rest of the engine!

Empirical Performance Testing Strategy

To benchmark and audit the distribution, a verification suite (Gen_test) executes dynamic stress pipelines over billions of iterations. Here is an optimized look at how the high-throughput test harness populates the baseline character array under perfect power-of-2 distributions:

      if Is_Perfect_RNG then

         Start := Ada.Real_Time.Clock;

         Outer_Loop :
         for I in 1 .. Round loop
            pragma Optimize (time);
            
            Success := NTSTATUS'Last;
            ProcessPrng_Public(Buffer => Rnd_Buffer,
                               Status => Success);
            
            if Success /= 1 then

               Success := NTSTATUS'Last;
               BcryptGenRandom_Public(Buffer => Rnd_Buffer,
                                      Status => Success);
               
               if Success /= 0 then
                  return;
               end if;

            end if;

            pragma Loop_Optimize (unroll);
            for Idx in Rnd_Buffer'First .. Rnd_Buffer'Last loop
               B(Rnd_Buffer(Idx)) := B(Rnd_Buffer(Idx)) + 1;
            end loop;
            
         end loop Outer_Loop;

         ---------------------------

         Finish := Ada.Real_Time.Clock;

Architectural Specification (.ads Example)

Here is the structural design, enforcing cryptographic bounds and strict information-flow contracts right into the type system:

package Math_Functions with SPARK_Mode => On is
   subtype mxb is Positive range 256 .. 256;
   max_byte : constant mxb := 256;
   subtype Byte_Length is Positive range 1 .. 256;
   subtype Sesgo_Free  is Positive range 128 .. 255;
   subtype Noused      is Positive range 1 .. 128;
   subtype PerRecjt    is Float    range 0.39 .. 50.00;

   function Byte_Division (Div : in Byte_Length) return Byte_Length
     with
       Global => Null,
       Post   => Byte_Division'Result = Byte_Length(max_byte / Div);

   function Unbiased_Secure (Len : Byte_Length) return Sesgo_Free
     with
       Global => Null,
       Post   => Unbiased_Secure'Result = Sesgo_Free(Len * Byte_Division(Div => Len) - 1);

   function Reject (Vod : Sesgo_Free) return Noused
     with
       Global => Null,
       Post   => Reject'Result = Noused(max_byte - Vod);

   function Percent (Trh : in Noused) return PerRecjt
     with
       Global => Null,
       Post   => Percent'Result = PerRecjt(Float'Min(50.00, Float'Max(0.39, (Float(Trh) / Float(max_byte)) * 100.0)));
end Math_Functions;

subtype Safe_Token is String
  with Dynamic_Predicate =>
    (for all Simple in Safe_Token'Range =>
       Safe_Token(Simple) in '0' .. '9' | 'A' .. 'Z' | 'a' .. 'z' | '_' | '-');

-- Example of one of the 14 entry points defined in the package
procedure Chain_Safe_Token (Chain   : in out Safe_Token;
                            Success :    out NTSTATUS;
                            Works   : in out Boolean;
                            Entropy : in out sub_entropy)
  with 
    Global  => (Input => Ada.Real_Time.Clock_Time),
    Depends => (Chain   => Chain,
                Success => Chain,
                Works   =>+ Chain,
                Entropy =>+ Chain,
                null    => Ada.Real_Time.Clock_Time),
    Pre     => (Chain'Length >= 1) and then (Chain'First = 1)
               and then (Chain'Last = Chain'Length) and then (Chain'Length <= 10_000)
               and then (for all Char in Chain'Range => Chain(Char) = '0')
               and then Works = False
               and then (Entropy = 0.0),
    Post    => (if Works then
                  (for all Char in Chain'Range => Chain(Char) in '0' .. '9' | 'A' .. 'Z' | 'a' .. 'z' | '_' | '-')
                else
                  (for all Char in Chain'Range => Chain(Char) = Chain'Old(Char)) and then Entropy = Entropy'Old);

The private logic relies on a static dynamic-sizing map (`Dynamic_Length`) ensuring that the underlying random arrays always carry a massive buffer margin, mathematically guaranteeing that the loops will never run out of entropy tokens.

 ------------------------------
 -- Chain_Alphanumeric_Mixed --
 ------------------------------
   procedure Chain_Alphanumeric_Mixed (Chain   : in out Alphanumeric_Mixed;
                                       Success :    out NTSTATUS;
                                       Works   : in out Boolean;
                                       Entropy : in out sub_entropy)
   is
      Chain_Set  : Constant Alphanumeric_Mixed(1 .. 69) := "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz!@#%_*-";
      New_Length : Constant Positive := Dynamic_Length(Len => Chain'Length);
      Rnd_Buffer : BUFFER_RNG(0 .. BUFFER_RNG_LENGTH(Chain'Length + New_Length) - 1) := (others => 0);
      Rnd_Len    : size_t range Rnd_Buffer'First .. Rnd_Buffer'Length := Rnd_Buffer'First;
      Chain_Len  : Natural range 0 .. Chain'Length := 0;
      Sesgo      : Constant Sesgo_Free := Unbiased_Secure(Len => Chain_Set'Length);
      subtype Unbiased is Interfaces.Unsigned_8 range 0 .. Interfaces.Unsigned_8(Sesgo);
   begin
      Success := NTSTATUS'Last;
      ProcessPrng_Public(Buffer => Rnd_Buffer, Status => Success);
      if Success /= 1 then
         Success := NTSTATUS'Last;
         BcryptGenRandom_Public(Buffer => Rnd_Buffer, Status => Success);
         if Success /= 0 then
            return;
         else
            Works := (Success = 0);
         end if;
      else
         Works := (Success = 1);
      end if;

      while Chain_Len < Chain'Length and then Rnd_Len < Rnd_Buffer'Length loop
         pragma Loop_Variant (Increases => Rnd_Len);
         pragma Loop_Invariant (Chain_Len in 0 .. Chain'Length);
         pragma Loop_Invariant (Rnd_Len in Rnd_Buffer'First .. Rnd_Buffer'Length);
         if Rnd_Buffer (Rnd_Len) in Unbiased then
            Chain_Len := Chain_Len + 1;
            Chain (Chain_Len) := Chain_Set ((Natural (Rnd_Buffer(Rnd_Len)) mod Chain_Set'Length) + 1);
         end if;
         Rnd_Len := Rnd_Len + 1;
      end loop;

      Rnd_Buffer := (others => 0);
      pragma Unreferenced(Rnd_Buffer);
      Calculate_Shannon_Entropy(Item => Chain, Ento => Entropy);
   end Chain_Alphanumeric_Mixed;

 ------------------------
 -- Chain_Only_Numbers --
 ------------------------
   procedure Chain_Only_Numbers (Chain   : in out Only_Numbers;
                                 Success :    out NTSTATUS;
                                 Works   : in out Boolean;
                                 Entropy : in out sub_entropy)
   is
      New_Length : Constant Positive := Dynamic_Length(Len => Chain'Length);
      Rnd_Buffer : BUFFER_RNG(0 .. BUFFER_RNG_LENGTH(Chain'Length + New_Length) - 1) := (others => 0);
      Rnd_Len    : size_t range Rnd_Buffer'First .. Rnd_Buffer'Length := Rnd_Buffer'First;
      Chain_Len  : Natural range 0 .. Chain'Length := 0;
      subtype Unbiased is Interfaces.Unsigned_8 range 0 .. 249;
   begin
      Success := NTSTATUS'Last;
      ProcessPrng_Public(Buffer => Rnd_Buffer, Status => Success);
      if Success /= 1 then
         Success := NTSTATUS'Last;
         BcryptGenRandom_Public(Buffer => Rnd_Buffer, Status => Success);
         if Success /= 0 then
            return;
         else
            Works := (Success = 0);
         end if;
      else
         Works := (Success = 1);
      end if;

      while Chain_Len < Chain'Length and then Rnd_Len < Rnd_Buffer'Length loop
         pragma Loop_Variant (Increases => Rnd_Len);
         pragma Loop_Invariant (Chain_Len in 0 .. Chain'Length);
         pragma Loop_Invariant (Rnd_Len in Rnd_Buffer'First .. Rnd_Buffer'Length);
         if Rnd_Buffer(Rnd_Len) in Unbiased then
            Chain_Len := Chain_Len + 1;
            pragma Assert (Character'Val (Character'Pos('0') + Natural(Rnd_Buffer(Rnd_Len)) mod 10) in '0' .. '9');
            Chain(Chain_Len) := Character'Val (Character'Pos('0') + (Natural (Rnd_Buffer(Rnd_Len)) mod 10));
         end if;
         Rnd_Len := Rnd_Len + 1;
      end loop;

      Rnd_Buffer := (others => 0);
      pragma Unreferenced(Rnd_Buffer);
      Calculate_Shannon_Entropy(Item => Chain, Ento => Entropy);
   end Chain_Only_Numbers;

 -------------------------
 -- Chain_Hex_Uppercase --
 -------------------------
   procedure Chain_Hex_Uppercase (Chain   : in out Hex_Uppercase;
                                  Success :    out NTSTATUS;
                                  Works   : in out Boolean;
                                  Entropy : in out sub_entropy)
   is
      Chain_Set  : Constant Hex_Uppercase(1 .. 16) := "0123456789ABCDEF";
      New_Length : Constant Positive := Dynamic_Length(Len => Chain'Length);
      Rnd_Buffer : BUFFER_RNG(0 .. BUFFER_RNG_LENGTH(Chain'Length + New_Length) - 1) := (others => 0);
      Rnd_Len    : size_t range Rnd_Buffer'First .. Rnd_Buffer'Length := Rnd_Buffer'First;
      Chain_Len  : Natural range 0 .. Chain'Length := 0;
   begin
      Success := NTSTATUS'Last;
      ProcessPrng_Public(Buffer => Rnd_Buffer, Status => Success);
      if Success /= 1 then
         Success := NTSTATUS'Last;
         BcryptGenRandom_Public(Buffer => Rnd_Buffer, Status => Success);
         if Success /= 0 then
            return;
         else
            Works := (Success = 0);
         end if;
      else
         Works := (Success = 1);
      end if;

      while Chain_Len < Chain'Length and then Rnd_Len < Rnd_Buffer'Length loop
         pragma Loop_Variant (Increases => Chain_Len);
         pragma Loop_Variant (Increases => Rnd_Len);
         pragma Loop_Invariant (Chain_Len in 0 .. Chain'Length);
         pragma Loop_Invariant (Rnd_Len in Rnd_Buffer'First .. Rnd_Buffer'Length);
         Chain_Len := Chain_Len + 1;
         Chain (Chain_Len) := Chain_Set ((Natural (Rnd_Buffer(Rnd_Len)) mod Chain_Set'Length) + 1);
         Rnd_Len := Rnd_Len + 1;
      end loop;

      Rnd_Buffer := (others => 0);
      pragma Unreferenced(Rnd_Buffer);
      Calculate_Shannon_Entropy(Item => Chain, Ento => Entropy);
   end Chain_Hex_Uppercase;

Empirical Audit Logs (97+ Billion Characters Stress Test)

To prove that the mathematical constraints translate perfectly into a completely uniform distribution, here is an extraction of the empirical test logs from a massive 97,657,298,301 characters audit run on the Pure Numeric configuration:

==========================================================================================================================================================================================
==                                                               Date : 2026-08-03 | Day : Monday    | Hour : 12:39 PM                                                                  ==
==========================================================================================================================================================================================

Charset                   => 0123456789
Charset Length            => 10

Global Classification     => [ PURE NUMERIC (0-9) ]
Entropy Loss: [ 0.00 % ]  => Charset is Byte-Pure. No duplicates.

--- Character Frequency [ Total Chars  97657298301 ] ---

Character => '0' Appear   => 9765902809 times
Character => '1' Appear   => 9765770362 times
Character => '2' Appear   => 9765699784 times
Character => '3' Appear   => 9765664853 times
Character => '4' Appear   => 9765854612 times
Character => '5' Appear   => 9765775939 times
Character => '6' Appear   => 9765716940 times
Character => '7' Appear   => 9765636036 times
Character => '8' Appear   => 9765613991 times
Character => '9' Appear   => 9765662975 times

-------------------------------------------------------------------------------------------

Max Repeats               => Character '0' with 9765902809 times.
Min Repeats               => Character '8' with 9765613991 times.

Divergence Variance Delta => 288818 units.
Theoretical Ideal Average => 9765730304.00

Real Standard Deviation   => 90084.07
Percet Deviation          => 0.0009 %

Real Time Duration        => 152.038718900
Process MB/s              => 612.56 MB/s

Free Unbiased Range       => 0 .. 249
Unused Bytes              => 6
Reject Percent            => 2.73 %
Free Unbiased Formula     => Charset'Length * (256 / Charset'Length) - 1

Entropy Source            => ProcessPrng (Principal) - BcryptGenRandom (Secondary)
Entropy Default           => ProcessPrng
Entropy Fallback          => BcryptGenRandom

-------------------------------------------------------------------------------------------

Distribution Stability    => 100.00% (Optimal Objective > 99.50%)
Audit Verdict             => [ PERFECT ] -> Uniformity matches military-grade physical noise.

-------------------------------------------------------------------------------------------

[JC001]

This looks like an interesting project. Why are the results strings? Why not sequences of bytes? The latter would seem more generally useful. I have a few comments:

@Avila

harvested via Windows ProcessPrng / BcryptGenRandom

So this is restricted to Windows? That’s a significant limitation that should be made clear.

@Avila

4. Summary of SPARK Analysis Results

Why is your first numbered section number 4?

@Avila

The engine achieved a flawless 100% Proved status across 925 total verification paths with absolutely zero unproved properties

This sounds like marketing hype, unsuitable for this technical forum. “Flawless”, “100% proved”, and “zero unproven” all say the same thing, and this sentence repeats information from the preceding paragraph while adding no new information. The extensive use of bold type and unnecessary hyperbole (flawless, massive) makes one wonder if there is really anything to it.

@Avila

1. Type-Driven Design vs Explicit Contracts: Do you consider this strict subtype clamping approach cleaner than writing expansive runtime preconditions for dynamic charsets in SPARK?

I think it is always better to use subtypes than pre- and postconditions when possible. My understanding is that SPARK often finds them easier to prove, as well.

@Avila

subtype Safe_Token is String
  with Dynamic_Predicate =>
    (for all Simple in Safe_Token'Range =>
       Safe_Token(Simple) in '0' .. '9' | 'A' .. 'Z' | 'a' .. 'z' | '_' | '-');

subtype Safe_Token is String with Dynamic_Predicate =>
   (for all Simple of Safe_Token =>
       Simple in '0' .. '9' | 'A' .. 'Z' | 'a' .. 'z' | '_' | '-');

is simpler and clearer.

@Avila

 ------------------------------
 -- Chain_Alphanumeric_Mixed --
 ------------------------------

A basic style rule is that comments must add value: they must not simply repeat information that is obvious from the code. These box comments simply repeat a subprogram name, so they add no value and should not be used.

I note that there’s no link to obtain the code. Is it available?

[Irvise]

Very interesting project!

I also agree with Jeff, I would prefer subtypes over contracts 100% of the time. They are easier to read, they reduce and model the problem space in a declarative manner and they are equally or even more effective at proof time and at compilation time.

Best regards,
Fer

[Avila]

Hi JC001,

Thanks for taking the time to review my post. I’m really glad to hear that you found the project interesting!

To be completely honest, English is not my first language, so I relied heavily on an AI translation tool for the write-up. It clearly injected that redundant ‘marketing hype’ and hyperbole, which wasn’t my intention at all. I am actually a self-taught developer and I just started learning programming and Ada about a year ago, so I still have a lot to learn regarding technical writing and community standards. I will definitely clean up the text.

Regarding your other points:

• Windows limitation: You are completely correct. For now, it relies on Windows ProcessPrng / BcryptGenRandom. However, I am already planning to update the project architecture to support Linux entropy sources in the very next iteration.
• Strings vs. Bytes: The primary goal of this engine is the conversion and readability stage after raw bytes are generated. If a user only needs raw bytes, they can simply call BcryptGenRandom or ProcessPrng directly without this engine. I chose Strings because this tool specifically focuses on delivering human-readable, bias-free tokens ready for higher-level use cases.
• Box comments: I use those large block comments purely as visual anchors. Since I am still learning, when I am scrolling fast through a dense .adb implementation file, it helps my eyes catch subprogram boundaries instantly without having to slow down to read small text identifiers.
• Subtypes syntax: Thanks for the tip! Your syntax for all Simple of Safe_Token is much cleaner and more idiomatic. I will gladly adopt it for the codebase.
• Section numbering: That was a formatting oversight on my part while compiling the notes. Thanks for catching it.

I am currently setting up my GitHub account and polishing these style issues. I will upload the code very soon so you and the community can review it, and I’ll share the link in this thread as soon as it’s public.

Thanks again for your time, your patience, and your valuable insights!

[Avila]

Hi Fer,

Thank you so much! I’m really glad you find the project interesting.

it’s incredibly encouraging to hear that this approach with subtypes is the right way to go. JC001 actually gave me an even cleaner syntax for that subtype predicate, so I will definitely be using it in the codebase.

I’m setting up my GitHub right now and will share the link here very soon so you can check out the full code. Thanks for the feedback and the support!

[JC001]

@Avila

• it relies on Windows ProcessPrng / BcryptGenRandom

I think I misunderstood. IIUC, “entropy” refers to true randomness. These subprograms provide pseudo-random numbers.

I’m not clear when one would want random, human-readable tokens.

I suspected the tone of the post might be due to your use of an LLM to translate your original. Some are better than others. I find deepl.com is often good.

[Avila]

Thanks for the feedback, JC001! You are totally right about the terminology. To be precise, the engine consumes CSPRNG outputs (`ProcessPrng` / `BCryptGenRandom`) which under the hood leverage the Windows kernel entropy pools, but yes, the direct source in the code is a CSPRNG. As for the use case: human-readable, bias-free tokens are useful for generating high-entropy cryptographic keys, secure recovery phrases, or session identifiers that need to be manually typed or communicated by humans (like backup codes or one-time activation tokens) without losing statistical uniformity due to simple modulo mapping. And good catch on the translation! English is not my native language, so I relied on a translator to structure the post. I appreciate the DeepL recommendation, I’ll definitely check it out.

I HAVE ALREADY CREATED MY NEW GITHUB PROFILE AND POSTED THE CODE

GitHub - EliAvila10/project_bias: High-performance, bias-free cryptographic engine...

[Avila]

GitHub - EliAvila10/project_bias: High-performance, bias-free cryptographic engine...

[Irvise]

Enhorabuena!

Two tips The README.md is in Spanish, that is fully fine by me, but I would recommend to translate it to English so that it could be used by a wider audience. I would also recommend to add a LICENSE file directly to the root of the repo. In the Alire.toml file you indicate that it is Apache-v2, that would be enough, but normally a direct license file would be preferred.

Best regards,
Fer

[Avila]

Thanks for the advice—I really appreciate it. I’ve already made the changes you recommended. Thanks.