project_bias

一个使用 Ada 编写、并通过 SPARK 进行形式化验证的高性能、无偏密码学流引擎。 该引擎在将原始熵映射到自定义字符集时，通过丢弃取模偏置值来保证零统计偏差， 直接从原生操作系统内核池中提取安全字节。

验证级别

• SPARK Level 4（形式化验证）： 已完全证明可确保无运行时错误（AoRTE）并符合功能契约。
• 工具链兼容性： 已使用 GNAT/SPARK Pro 2021 以及通过 Alire 提供的最新社区 SPARK 工具链进行验证。

核心架构与熵池

该引擎通过 Interfaces.C 直接与底层操作系统 API 交互，以消除抽象层和延迟：

• ProcessPrng（主要）： 使用现代用户模式操作系统熵提供程序（ProcessPrng）作为原始安全字节的主要来源。
• BCryptGenRandom（回退）： 使用 Windows CNG API（bcrypt.dll）实现稳健的次级回退层。

截断的数学边界

-- 用于强制均匀分布且无取模偏置的公式：
-- Formul = Charset'Length * (256 / Charset'Length) - 1
-- 任何提取的字节 > Formula'result = 将被排除

结构

• src/ProcessPrng_Wrapper.ad[s|b]：主要现代 Windows 内核 PRNG 的绑定。
• src/BcryptGenRandom_Wrapper.ad[s|b]：次级密码学回退绑定。
• src/Chain_Generator.ad[s|b]：编排无偏提取的主状态机。
• src/Math_Functions.ad[s|b]：映射操作的形式化前置/后置条件。

构建与运行

alr run