Polarnova/CryptBoolean

# CryptBoolean：Lean 中的密码学布尔函数 CryptBoolean 是一个基于 Lean 4 和 Mathlib 的密码学布尔函数形式化项目，参考 Claude Carlet 的《密码学与纠错码布尔函数》（*Boolean Functions for Cryptography and Error Correcting Codes*）。它开发了 代数、频谱、编码理论和密码学理论，作为一个可重用的定理库。 该项目使用 [FABL](https://github.com/Polarnova/FABL) 进行布尔傅里叶分析，并提供了 FABL 的归一化系数与 Carlet 的原始 Walsh 变换之间的明确桥梁。 ## 状态 目前经过验证的产出范围涵盖了 Carlet 第 2 章和第 3 章的部分结论。 每个 Blueprint 节点都有完整的数学陈述和经过审查的依赖关系。形式化的 节点与已编译的 Lean 声明相关联；未证明的开源定理仍然可见，且没有占位符关联。 | 章节 | 主题 | 陈述 | 形式化 | 开放 | Lean 声明 | 依赖边 | |---|---|---:|---:|---:|---:|---:| | 2 | 表示与傅里叶/Walsh 变换 | 36 | 35 | 1 | 159 | 45 | | 3 | 布尔函数与 Reed--Muller 编码 | 7 | 6 | 1 | 21 | 19 | | **总计** | | **43** | **41** | **2** | **180** | **64** | 第 2 章的范围包括代数与数值标准型、Walsh 和伪布尔 傅里叶变换、反演与 Plancherel 恒等式、完整的原始泊松公式、 数值标准型整性判据、仿射不变性、限制恢复、 谱支撑界、导数、自相关和有限域表示。第 3 章 定义了 Reed--Muller 码并证明了一般的距离界、维度和基数 公式，以及对偶定理。 目前仍有恰好两处源陈述处于开放状态。Carlet 命题 3 需要一个有限域坐标 桥接，将 ANF 次数与单变量指数的最大二进制权重相对应，并 保证在相关的分圆轨道上不会发生抵消。Carlet 第 3 章命题 12 需要 任意仿射平面标准型、仿射平面指示子的余维数--次数定理， 以及用于最小权重分类的等号情形切片基础设施。 生产库中包含零个 `sorry`、项目自定义的公理、不安全的声明，或 原生证明快捷方式。 ## 使用 CryptBoolean 本仓库固定使用 Lean 和 Mathlib `v4.32.0` 以及最新的稳定版 FABL 发行版，目前为 `v0.5.6`。克隆后，获取并验证预编译的依赖项，然后构建 CryptBoolean： ``` lake exe cache get ./.github/scripts/require_latest_fabl_release.sh lake build CryptBoolean ``` 发布检查会在 Linux x86-64 和 macOS arm64 上下载 FABL 和 ProbabilityApproximation 归档文件； 如果找不到匹配的已验证资产，将会直接报错，而不是去编译其源代码。 一个每小时运行的工作流（也可以通过 FABL 发布调度来触发）会在 FABL 发布更新的稳定版时，提交一个精确版本锁定的升级 pull request。它会更新 Lean 工具链和两个 Lake manifest，在 GitHub Actions 中运行完整的 CryptBoolean 和 Blueprint 构建，并且只会合并状态为成功的依赖项更新。 根模块导入了每个经验证的产出模块： ``` import CryptBoolean ``` 源模块位于 `CryptBoolean/Carlet` 下，遵循 Carlet 的章节结构。表示桥梁位于 `CryptBoolean/Bridge` 下。 ## 书籍与依赖图 Verso Blueprint 在其 Lean 声明旁边展示了面向源码的陈述，并记录了 经过审查的依赖图。陈述块仅包含数学内容；实现和 归一化说明会单独渲染。GitHub Actions 执行完整的发布构建。 要在根库处于最新状态后进行本地预览： ``` cd blueprint-verso lake exe cache get ./scripts/site.sh serve dev ``` 然后打开 [http://localhost:8000/](http://localhost:8000/)。生成的文件位于 `blueprint-verso/_out/` 下。推送到 `main` 分支会运行相同的检查构建，并 通过 GitHub Pages 自动发布书籍，网址为 [polarnova.github.io/CryptBoolean](https://polarnova.github.io/CryptBoolean/)。 `dev` 配置文件保留了用于审查的保真度元数据；公共 CI 使用默认的 `release` 配置文件，并在阅读视图中省略这些标签。 ## 贡献 阅读 [`AGENTS.md`](AGENTS.md) 以了解贡献者契约和验证工作流程。 ## 参考文献与先前工作 - Claude Carlet，《密码学与纠错码布尔函数》（*Boolean Functions for Cryptography and Error Correcting Codes*），2010 年。 - Thomas W. Cusick 和 Pantelimon Stănică，《密码学布尔函数及其应用》（*Cryptographic Boolean Functions and Applications*）， 第二版，2009 年。 - Ryan O'Donnell，《布尔函数分析》（*Analysis of Boolean Functions*），2021 年 5 月版，由 [FABL](https://github.com/Polarnova/FABL) 形式化。 - [Mathlib](https://github.com/leanprover-community/mathlib4)，CryptBoolean 所使用的 数学基础。 - [Verso Blueprint](https://github.com/leanprover/verso-blueprint)，用于面向源码的书籍 和依赖图。

标签：Lean 4, 密码学, 布尔函数, 形式化验证, 手动系统调用, 数学定理库