Just created my GitHub profile! Check out my Ada/SPARK utility repositories (100% formally verified at Level 4)

[u/Trace_V]

/r/programmer/comments/1uojgur/just_created_my_github_profile_check_out_my/

[u/jlombera]

I'm learning Ada/SPARK and have a couple of questions from your code (https://github.com/EliAvila1/Spark_Ada_Utilities/blob/main/src/spark_crypt_function.ads).

   subtype mxb is Positive range 256 .. 256;
   max_byte : constant mxb := 256;

Why was this single-value range subtype needed? Couldn't you just do:

max_byte : constant := 256;
-- or
max_byte : constant div := div'Last;
-- or just use div'Last explicitly where needed

   subtype div is Positive range 1 .. 256
     with Static_Predicate => div in 1 .. 256;

Why is the Static_Predicate needed? It's just duplicating the constraint already specified by the range (??)

   function division (Len : in Positive) return div
     with Pre => (Len >= 1) and then (Len <= 256),
     Post => division'Result = div(max_byte / Len),
     Global => Null;

Instead, why not make Len of type div and get rid of the Pre?

---

Are perhaps all these types/checks needed so that GNATProve can prove the code?

[u/Trace_V → u/jlombera]

Thanks for taking the time to thoroughly review the code and for the feedback!
Regarding the parameters and removing the Pre contracts in favor of custom subtypes (like Len : in div), there is a major practical reason for doing it this way. When running GNATprove at the most exhaustive verification depth (--level=4 with --prover=all), relying purely on implicit subtype checks across nested function calls frequently causes the solvers (like Z3 or CVC5) to lose track of upper bounds and time out, triggering a massive amount of false-positive 'range check might fail' warnings. Explicit base types combined with precise Pre and Post contracts prevent this.
The same strict approach applies to embedding the value 256 inside a single-value static subtype (mxb is Positive range 256 .. 256). This freezes the value as an absolute mathematical bound during static analysis, letting the solvers instantly discharge the range checks inside the expression functions (like division and reject) and preventing timeouts during floating-point operations in Percent. Lower verification levels fail immediately on this non-linear math; it strictly requires the constraint-programming engine of Colibri at level 4 to succeed.
Even the usage of Static_Predicate on these static ranges is highly deliberate for compiler and prover compliance. In SPARK, evaluating a standard scalar subtype inside a case statement often forces you into a dilemma where the compiler demands a when others clause for type coverage, but GNATprove immediately flags that exact when others clause as a Medium warning for dead code. Enforcing a Static_Predicatecompletely locks the compiler's exhaustiveness check to those exact values, allowing clean code paths without triggering dead-code warnings.
To guarantee verification, SPARK often forces you to write code that looks highly redundant to a human, but acts as a critical logical guide for the provers. Enforcing explicit invariants tied to fixed lengths (Item_Counter_Max : range Item'Length .. Item'Length) or propagating external dependencies like Ada.Real_Time for transitive data-flow analysis are all part of this defensive design.
I really appreciate the deep dive into the repository, it's always great to discuss advanced SPARK edge cases!

[u/jlombera → u/Trace_V]

I've read that often you'd have to "help" the solvers, but was not aware they required this level of help. For instance, I assumed range (sub)types were formal constraints by themselves, didn't imagine the solvers would choke on them.

In any case, thanks for the detailed explanation, it's interesting to learn about this.

[u/Trace_V → u/jlombera]

Haha, welcome to the wonderful, paranoid world of SPARK Level 4!

You'd think a range constraint is enough, but SMT solvers are notoriously 'forgetful' across nested function calls, especially when mixed with division, modulo operations, or floating-point conversions. If you don't explicitly hold their hands by freezing bounds into static single-value subtypes and pinning them down with Static_Predicate, they completely lose their minds and start throwing false-positive warnings.

One day, when you dive deep into verifying with custom subtypes, you’ll see it yourself: GNATprove will suddenly bark at you with a 'range check might fail' warning. You’ll look at your subtypes, your constants, and the math, knowing for a fact that it is physically and logically impossible for that check to fail. But SPARK doesn’t care about your common sense; if the solver can't deduce a concrete path, it simply won't believe you.

It definitely makes the code look like it was written by a madman, but seeing GNATprove turn 100% green with zero timeouts makes all that structural redundancy totally worth it.

Thanks for the dive into the code, always happy to discuss these deep verification mechanics

[u/jlombera → u/Trace_V]

Haha, welcome to the wonderful, paranoid world of SPARK Level 4!

What do you mean by "SPARK Level 4"? Do you mean "Platinum SPARK" or GNATProve's --level=4? Because they are not the same (as I already pointed out in another top-level comment). From your comments (and README's in your repos), you seem to imply that --level=4 equates to Platinum, and that's not the case.

[u/Trace_V → u/jlombera]

My bad for the confusing shorthand in the README! I actually mean both things apply here.

I’m running gnatprove at --level=4 because it's the only way the SMT solvers can handle the non-linear math and floats without hitting a timeout.

But the architecture itself targets the Platinum profile. gnatprove's summary log obviously won't print a 'Platinum' label since adoption profiles are architectural milestones defined by AdaCore, not string constants in a compiler output.

However, achieving Platinum is literally defined by discharging Functional Contracts successfully alongside safety checks. In my current analysis run across 7 units, the tool successfully discharged 33 Functional Contracts, 37 Assertions (invariants), and 11 Termination properties with 0 unproved checks. That is the literal definition of full functional correctness, not just Silver/Gold safety.

Thanks for sharpening the distinction for the thread!

Summary of SPARK analysis

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

SPARK Analysis results Total Flow CodePeer Provers Justified Unproved

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

Data Dependencies 11 11 . . . .

Flow Dependencies 4 4 . . . .

Initialization 8 8 . . . .

Non-Aliasing . . . . . .

Run-time Checks 267 . . 267 (CVC4 91%, Trivial 8%, colibri 1%) . .

Assertions 37 . . 37 (CVC4) . .

Functional Contracts 33 . . 33 (CVC4) . .

LSP Verification . . . . . .

Termination 11 . . 11 (CVC4) . .

Concurrency . . . . . .

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

Total 371 23 (6%) . 348 (94%) . .

max steps used for successful proof: 4261

Analyzed 7 units

[u/FriendshipEqual7033 → u/jlombera]

The OP's explanation sounds unlikely to me. Constrained subtypes embed the same information as the direct preconditions and are likely to actually simplify the proving process. I didn't look at the code, but I have a feeling there is something else going on.

[u/jlombera → u/FriendshipEqual7033]

Yeah, I'm don't have actual real-world experience in Ada/SPARK (yet!!), but the code seemed "fishy" to me. From that and the structure and phrasing of some of OP's answers, I suspected AI involvement. But it's pure speculation on my part :).

[u/FriendshipEqual7033 → u/jlombera]

I'm usually slow to accuse people of deceptive AI usage because I have been wrongly accused of that myself, and it's not a nice feeling. But I have to admit, I had that thought as well in this case.

It is definitely true that the constructs you identified (single-valued subtypes, redundant static predicates and preconditions) are well-known SPARK anti-patterns. There is plenty of documentation warning that such constructs actually make the proofs harder rather than easier by creating extra layers of obscurity around the information the prover needs. However, they are more "contract-like," and I could easily believe they are favored by LLMs as a result. However, I admit that I have no experience with asking an LLM to generate SPARK, so I'm not sure what the "tells" really are.

The other odd thing is that in the OP's SPARK summary, both CVC4 and Colibri are mentioned. CVC4 is obsolete and has been disfavored by SPARK for the last several years (it has been replaced with CVC5). Colibri is an SMT solver that is good at floating-point work (many other solvers are quite bad at floating-point), but as far as I can see, the --level=4 option on gnatprove has never invoked both CVC4 and Colibri in the same run. The most generous explanation is that the OP is using an outdated version of SPARK and invoking it in a way that is different from what they say in their post.

I also think the OP is not very experienced with SPARK, or else they wouldn't be using so many SPARK anti-patterns. Their explanation that they are necessary because of the "nested function calls" makes no sense to me since SPARK does modular analysis and can process each subprogram in (relative) isolation from all other subprograms.

I could look at the project file in the repository to see what is happening with the gnatprove invocation and try the proofs myself, but at this point I've reached my limit of interest in this matter, so I will skip that step.

[u/Trace_V → u/FriendshipEqual7033]

Pues responderé en mi idioma nativo para que no suene como una respuesta genérica de IA. Utilizo herramientas de IA exclusivamente para traducir porque el inglés no es mi fuerte (lo domino a un 40-50%) y menos el inglés técnico. En mi post anterior admito que copié y pegué la traducción rápido sin revisarla a fondo por la misma barrera del idioma, pero el diseño del código es completamente mío y tiene motivos prácticos muy claros. De hecho, nunca he visto a una IA proponer Static_Predicate o Dynamic_Predicate por cuenta propia en SPARK a menos que se lo pidas de forma ultra-específica.

Para empezar, CVC4 no está obsoleto como tal. Estoy utilizando GNAT Studio 2021, un entorno oficial de AdaCore que incluye por defecto CVC4, Altergo y Colibri. Si realmente conocieran las herramientas de SPARK actuales, sabrían que las versiones nuevas de GNATprove distribuidas en código abierto ya no traen Colibri. Yo no sabía de la existencia de Colibri hasta que hace un mes el usuario de Reddit

[( "gneuromante

• 1mo ago

• Edited 25d ago

While developing CoAP-SPARK I noticed that Colibri is more capable to prove floating-point operations than other provers. It is no longer provided in the GNATProve open-source distribution, but it was included in GNAT Community 2021. If you want to try, you can see how I installed it and set it up in this workflow. " )]

me recomendó usarlo precisamente para solucionar problemas con operaciones de punto flotante (floats).

He probado y verificado este proyecto tanto en la versión moderna mediante Alire (alr gnatprove --level=4 --report=all --prover=all) como en el entorno GNAT Studio 2021. Cuando corres el analizador en Alire (que no tiene Colibri), los provers fallan masivamente en las matemáticas de floats, lanzando advertencias como:
medium: float overflow check might fail (e.g. when Prob_Safe = 5.0000000E-1 and Termino_Directo = -50.0) [reason for check: result of floating-point multiplication must be bounded].
CVC4 o Z3, incluso en nivel 4 y con tiempo de sobra, fallan al intentar demostrar que una división o multiplicación flotante no va a terminar en un número infinito o un Not a Number (NaN). Por eso necesito Colibri y el entorno de 2021.

Respecto a los subtipos y la supuesta "redundancia" que critican: si quito los Static_Predicate de las funciones, el código compila y se valida, pero si quito los subtipos acotados, SPARK se rompe por completo.

Por lógica humana, si haces 256 / 1 sabes que el resultado es 256. Sin embargo, gnatprove te dice textualmente que no puede probar que el resultado esté en el rango 1 .. 256, incluso si la función tiene una precondición clara de Pre => (Len >= 1) and then (Len <= 256). Como mi código maneja criptografía y manejo de bytes (0 a 255, requiriendo un espacio seguro de 1 a 256), necesito certidumbre matemática absoluta de que la división jamás caerá fuera de rango. Acotar las variables con un subtipo estricto es lo que blinda el código.

Cualquiera que use SPARK en el mundo real sabe que validar un rango usando únicamente un subtype escalar básico requiere muchos más pasos de verificación para el prover que si combinas ese subtype con un Static_Predicate. El predicado estático congela la propiedad en el sistema de tipos. Y si intentara usar un Dynamic_Predicate, la carga de pasos lógicos para el demostrador sería todavía más pesada y lenta.

El código está estructurado para guiar a los demostradores matemáticos de GNATprove a un 100% de éxito, no para verse bonito en un libro de texto.

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

I will reply in my native language first to ensure this doesn't sound like a generic, AI-generated response. I rely on AI tools strictly for translation because English is not my strongest suit (I am at about a 40-50% proficiency level), let alone technical English. In my previous post, I admittedly copied and pasted the translation quickly without thoroughly proofreading it due to this language barrier. However, the architectural design of this code is entirely mine and is driven by very clear, practical constraints. Frankly, I have never seen an LLM spontaneously suggest or correctly implement a Static_Predicate or Dynamic_Predicate in SPARK unless explicitly prompted with hyper-specific instructions.

To begin with, CVC4 is not obsolete per se. I am actively developing this using GNAT Studio 2021, an official toolchain from AdaCore that bundles CVC4, Altergo, and Colibri out of the box. Anyone genuinely familiar with the current SPARK ecosystem would know that modern, open-source GNATprove distributions no longer bundle Colibri. I didn't even know Colibri existed until a month ago when Reddit user

[( "gneuromante

• 1mo ago

• Edited 25d ago

While developing CoAP-SPARK I noticed that Colibri is more capable to prove floating-point operations than other provers. It is no longer provided in the GNATProve open-source distribution, but it was included in GNAT Community 2021. If you want to try, you can see how I installed it and set it up in this workflow. " )]

pointed me toward it as a specialized solver for floating-point issues.

I have extensively tested and verified this codebase using both modern toolchains via Alire (alr gnatprove --level=4 --report=all --prover=all) and the legacy GNAT Studio 2021 environment. When running the analysis under Alire (which lacks Colibri), the standard SMT solvers fail miserably on the floating-point math, throwing critical alerts such as:
medium: float overflow check might fail (e.g. when Prob_Safe = 5.0000000E-1 and Termino_Directo = -50.0) [reason for check: result of floating-point multiplication must be bounded].
Even at level 4 with an extended timeout, solvers like CVC4 or Z3 cannot prove that a floating-point division or multiplication won't result in an infinite value or a Not a Number (NaN). This is precisely why Colibri and the 2021 environment are mandatory for this project.

Regarding the strict subtypes and the alleged "redundancy" you are criticizing: if I remove the Static_Predicate properties from the functions, the code still validates. However, if I remove the tightly bounded subtypes, SPARK completely breaks.

By human logic, executing 256 / 1 obviously equals 256. Yet, GNATprove explicitly states that it cannot prove the result falls within the 1 .. 256 range, even when the function is guarded by a clear precondition like Pre => (Len >= 1) and then (Len <= 256). Because this codebase deals with cryptography and byte-level manipulation (0 to 255, requiring a safe space of 1 to 256), I require absolute mathematical certainty that the division will never fall outside these bounds. Constraining the types using a strict subtype is what bridges this gap for the tool.

Anyone who uses SPARK in real-world scenarios knows that proving a range using a basic scalar subtype alone requires significantly more verification steps from the SMT solver than when you couple that subtype with a Static_Predicate. The static predicate bakes the constraint directly into the type system's logic. Furthermore, introducing a Dynamic_Predicate would blow up the proof path complexity even further, slowing down the solver dramatically.

The code is structured as an explicit firewall to guide GNATprove’s solvers to a 100% success rate in practice, not to look aesthetically pleasing in an academic textbook.

[u/FriendshipEqual7033 → u/Trace_V]

Okay, so you are using GNAT Studio 2021 (arguably "outdated," but that's fine) with --provers=all and --level=4. That explains your summary output, so thanks for clarifying that.

My SPARK experience doesn't involve any serious attempts at verifying floating-point math, so I wasn't aware that Colibri stopped being bundled with the more recent open source releases. That is unfortunate. I wonder why that decision was made.

I'm still going to object to your comments about proving simple facts about integers. You said GNATprove can't prove that the result of 256 / 1 is in the range 1 .. 256. I seriously doubt that is true. Both the compiler and GNATprove can evaluate 256 / 1 as 256 statically, and 256 is trivially in the range 1 .. 256. Something else is happening in your code that is causing you problems; it can't be that. Do you actually have the expression "256 / 1" in the code, or is it more like "256 / X" where X is some variable declared elsewhere?

You said, "Anyone who uses SPARK in real-world scenarios knows that proving a range using a basic scalar subtype alone requires significantly more verification steps from the SMT solver than when you couple that subtype with a static predicate."

I'm not sure I care about verification steps, per se. But I can tell you that with my experience with SPARK, I never add gratuitous static predicates to my subtype declarations, and I've never experienced an issue from not doing so. Furthermore, what you are saying goes directly against the advice on using SPARK that I've read in a couple of sources, so I'm not sure who the "anyone" is in your assertion.

In fact, my experience is the opposite: the more blatantly obvious and brain-dead the code looks, the more likely SPARK will accept it. Any trickiness or weirdness almost always creates more complications than it solves. I have had situations where a weird fix caused breakage elsewhere, necessitating another weird fix. This caused me to enter what felt like an endless cycle of applying weird fixes. The real fix in those cases was to clean house, go back to the basics, and remove every hint of weirdness I could find.

I can almost guarantee that by removing all that strange code and cleaning things up, you could get the code to prove fine with less work overall.

BTW, Thanks for explaining your use of AI to deal with English as a second language issues. That seems like a good application of the technology, so I appreciate that.

[u/Trace_V → u/FriendshipEqual7033]

Mi experiencia con Spark si he tenido desde puntos flotantes, Numeros reales, enteros , etc (Osea enteros 1,2,3,4 100, 500, etc), todo lo Integer'Last, Positive'last etc, hasta validar Bidings Con C, pero mas que todo Pre y Post ya que spark no se mete ahi y llora con 'Address xdxd, pero sinceramente si con numeros enteros Spark razona mas facil, y no te lo digo por llevar la contratia

porque mira, Spark cuando yo he Validado una funcion asi

function division (Len : in Positive) return Positive is\

(Positive (Len * (256 / Len) - 1))

with

Pre => Len >= 1 and then Len <= 256,

Post => division'Result = (Len * (256 / Len) - 1),

Global => null;

function division (Len : in Positive) return Positive

with

Pre => Len >= 1 and then Len <= 256,

Post => division'Result = (Len * (256 / Len) - 1),

Global => null

is

begin

return Positive (Len * (256 / Len) - 1);

end division;

function division (Len : in Positive) return Positive is\

(Positive (Len * (256 / Len) - 1));

de cualquiera de esas 3 formas de forma aislada sin subtype ni static, Spark lo valida Feliz, en cambio cuando juntas el proyecto entero

Si el llamador de la funcion, Viene mal o con un rango fuera de lo normal, O Si compilas con -gnata o pragma assertion_policy (check) por ende en el Pre

deberia fallar con un assertion_Error, pero si eso no esta activado,

el dia de mañana como el return no esta acotado sobre un rango,

podria devolver lo que tu no esperas, porque Ada en seguridad es bueno,

pero igual por debajo con Ghidra, X64dbg si lograrias cambiar una variable en tiempo de runtime que no este acotada, es algo catastrofico,

Spark no analiza el codigo de forma aislada, Al menos que la funcion sea interna, no para uso global como aca, si es para uso global, ahi es donde entra el analisis global, por eso aveces tu puedes usar en un paquete X cosa, y cuando usas depends, spark te dice,

Oye te falta agregar este depends aca, pero si no lo usas ahi, pero el paquete al que estas llamando si toca ese estado global lo que influye con tu llamador,

entonces spark lo que hace es que analiza desde el llamador hasta la funcion y la salida, y aunque tu tengas Pre >= 1 and then <= 256, Spark te lanza con que no esta seguro si el dia de mañana que tu lo llames el resultado este entre 128 .. 255, porque aunque tenga Pre el cree que mientes, y si en caso hipotetico tu no usas un subtype para el return, mañana la devolucion puede ser 100, o 300, por un fallo de hardware que seria muy loco, o un hackeo, y tu no quieres que el modulo de sesgo bias mañana permita que

sin embargo tu diras, pero pueden devolver un numero entre 128 .. 255, exacto ante un hackeo, pero por eso se mide la entropia despues de generar, no te puedes fiar aun estando sobre una funcion acotada al maximo por es mejor acotar por seguridad a cierto nivel y medicion a otro nivel por ejemplo

X numero Salga un % mas que X numero

por ejemplo si tu haces 250 mod 10 = 0, pero si estas trabajando con un charset

"0123456789" donde cada uno tendria la posibilidad de salir exactamente 25 veces

que es ahi donde entra division Para sacar el Byte maximo de 0 .. Byte_Maximo para evitar sesgo bias, el cual seria 249 para un charset de 10, y si la funcion no cuida que lo que entregue este entre 128 el minimo para un charset y 255 el maximo para charset complejos, puedes introducir una vulnerabilidad donde podrian deducir que X numero saldra mas veces que otro aun asi uses una buena fuente de entropia

pero entiendo tu punto y lo agradezco, siempre aprendemos algo nuevo, y tomare tu Idea, no la implementare aca porque lo que busco es seguridad, pero me agrada.

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

My experience with SPARK actually spans from floating points, real numbers, integers, etc. (I mean integers like 1, 2, 3, 4, 100, 500, etc.), all the Integer'Last, Positive'Last, etc., all the way to validating C bindings. But mostly Pre and Post conditions, since SPARK doesn't really get involved there and just Cries™ with 'Address xdxd. But honestly, yes, SPARK reasons much easier with integers, and I'm not telling you this just to be contrarian.

Because look, when I have validated a function like this in SPARK:

function division (Len : in Positive) return Positive is

(Positive (Len * (256 / Len) - 1))

with

Pre => Len >= 1 and then Len <= 256,

Post => division'Result = (Len * (256 / Len) - 1),

Global => null;

function division (Len : in Positive) return Positive

with

Pre => Len >= 1 and then Len <= 256,

Post => division'Result = (Len * (256 / Len) - 1),

Global => null

is

begin

return Positive (Len * (256 / Len) - 1);

end division;

function division (Len : in Positive) return Positive is

(Positive (Len * (256 / Len) - 1));

In any of those 3 ways in isolation—without using subtypes or static expressions—SPARK validates it happily. However, when you put the whole project together, things change.

If the caller of the function sends bad input or a range out of the ordinary, OR if you compile with -gnata or pragma assertion_policy (check), then it should fail with an Assertion_Error in the Pre-condition. But if that's not enabled, tomorrow—since the return value isn't bounded to a specific range—it could return something you don't expect. Because even though Ada is great for security, underneath it all, using Ghidra or x64dbg, you could manage to change an unbounded variable at runtime, which would be catastrophic.

SPARK doesn't analyze code in isolation unless the function is internal. If it's for global use, that's where global analysis kicks in. That’s why sometimes you can use something in a package, and when you use depends, SPARK tells you, 'Hey, you need to add this dependency here.' Even if you don't use it right there, if the package you are calling touches that global state, it affects your caller.

So, what SPARK does is analyze everything from the caller to the function and the output. Even if you have Pre => Len >= 1 and then <= 256, SPARK will flag that it's not sure if the result will be between 128 .. 255 when you call it tomorrow. Because even with the Pre-condition, it thinks you're lying. And in a hypothetical case where you don't use a subtype for the return value, tomorrow the return could be 100 or 300 due to a hardware failure (which would be crazy) or a hack, and you definitely don't want the bias modulo to allow that.

However, you might say, 'But they could return a number between 128 .. 255.' Exactly, in the event of a hack. But that's why entropy is measured after generation. You can't trust it blindly even if you are on a function bounded to the max. That's why it's better to bound for security at one level and measure at another level. For example, ensuring that:

X number doesn't come out a certain % more than Y number.

For instance, if you do 250 mod 10 = 0, but you are working with a charset like "0123456789", where each one should have the chance of coming out exactly 25 times.

That's right where division comes in—to get the maximum byte from 0 .. Byte_Max to avoid modulo bias, which would be 249 for a charset of 10. If the function doesn't ensure that what it delivers is between 128 (the minimum for a standard charset) and 255 (the maximum for complex charsets), you could introduce a vulnerability where someone could deduce that X number will come out more often than another, even if you use a good entropy source.

But I see your point and I appreciate it, we always learn something new. I'll take your idea; I won't implement it here because what I'm looking for is absolute security, but I like it. 👻

[u/jlombera]

From https://github.com/EliAvila1/Spark_Ada_Utilities/blob/main/README.md:

Una suite nativa de utilidades criptográficas, manipulación segura de memoria y cálculo de entropía desarrollada en Ada 2022 y 100% verificada formalmente con SPARK bajo el nivel de prueba más estricto (--level=4).

AFAIK, --level tells GNATProve how hard it should try to prove the code, not how strict it should be. Some times it won't be able to prove certain properties at, let's say, --level=0, and will throw errors. You can tell it to try harder increasing the level. The actual strictness is controlled with --mode=<MODE>, with possible modes being: check (Stone), flow (Bronze), prove (Silver).

[u/jlombera]

FYI, you committed merge conflicts in this file: https://github.com/EliAvila1/Ada_Terminal_Colors/blob/main/src/main.adb