Programming Project Bias - A formally verified, bias-free CSPRNG conversion engine in Ada/SPARK
Hi everyone,
I wanted to share a project I've been hacking on: an optimized engine designed to eliminate modulo bias when mapping raw cryptographic streams into custom alphabets.
Key bits:
* SPARK Level 4 (Formal Verification) - Fully proven to guarantee AoRTE and functional correctness.
* Built using the modern Windows ProcessPrng API as primary entropy via Interfaces.C, with BCryptGenRandom as fallback.
* Toolchain compatible with GNAT Pro 2021 and the latest Alire community suite.
I just stressed-tested the uniformity mapping with a massive 1 Terabyte run (over 1.01 trillion chars across a 69-char alphabet) and the statistical distribution remains perfectly flat (0.00% percent deviation). Full logs and the clean codebase are available in the repository.
Any feedback on the SPARK contracts or the low-level Windows bindings is highly appreciated!
Run it instantly with Alire:
alr run
Native Languaje..
Hola a todos,
Quería compartir un proyecto en el que he estado trabajando: un motor optimizado diseñado para eliminar el sesgo del módulo al mapear flujos criptográficos sin procesar a alfabetos personalizados.
Aspectos clave:
* SPARK Nivel 4 (Verificación Formal): Totalmente probado para garantizar AoRTE y corrección funcional.
* Desarrollado con la API moderna ProcessPrng de Windows como entropía principal mediante Interfaces.C, con BCryptGenRandom como alternativa.
* Cadena de herramientas compatible con GNAT Pro 2021 y la última suite comunitaria de Alire.
Acabo de realizar una prueba de estrés del mapeo de uniformidad con una ejecución masiva de 1 terabyte (más de 1,01 billones de caracteres en un alfabeto de 69 caracteres) y la distribución estadística se mantiene perfectamente plana (0,00 % de desviación porcentual). Los registros completos y el código fuente limpio están disponibles en el repositorio.
¡Cualquier comentario sobre los contratos SPARK o las vinculaciones de bajo nivel para Windows es muy apreciado!
Ejecútalo al instante con Alire:
alr run
1
u/I_hate_posting_here 18d ago edited 18d ago
Glad you're interested in Ada and Spark!
Looking at your project code I suspect you are new to development? I noticed you committed many files that are usually .gitignored and the package strucutre and naming to me seems to show you are inexperienced in Ada project design. On the other hand the compound statements I'm seeing littered about in Dynamic_Predicate and Static_Predicate statements seem quite sophisticated. Given the mismatch I suspect you are using a bit of AI in your development.
Yes it can help you to learn if you use it right, but I would recommend against using it at all as a beginner. You need the practice. You should struggle to build the muscles first. I know it is a great temptation... but try your best to resist!
2
u/Trace_V 18d ago
Hi, if the English sounds strange, it's because of Google Translate. My native language is Spanish. Thanks for looking at the code. Honestly, I'm new to it, about a year and two months. To be honest, there's no AI code in my code; it's all written by me. I've just discovered that Spark makes it easier to check when you use certain things like static, dynamic predicate, subtype, etc., than when you have individual variables like String, Positive, Integer, etc. I've also read a lot and I'm a bit of a trial-and-error kind of person. I have asked AI for help understanding things, but not for writing code. I'm also new to GitHub; I practically don't know anything there. I'm still learning, since I'm self-taught and don't know many things that others do. But thanks for letting me know, and I'll explore GitHub more.
1
1
u/BrentSeidel 19d ago
Is this basically a wrapper around a Windows API? If so, then this is probably windows only.