iotexproject/rs-proximity-gaps

# Reed--Solomon 近距间隙 — 伴生代码仓库 Raullen Chai 和 Xinxin Fan (IoTeX Network) 撰写的两篇论文的手稿、Lean 4 形式化验证以及 Python 验证脚本： 这些论文主要攻克 Reed--Solomon 近距间隙问题中（Johnson 半径 $< \delta < $ 列表解码容量）的开放中间地带——即以太坊路线图上每个基于 FRI 的 STARK 的实际部署领域。 [](https://github.com/iotexproject/rs-proximity-gaps/actions/workflows/ci.yml) ## 代码仓库布局 本代码仓库按论文进行组织：每个论文目录都是独立的。 ``` rs-proximity-gaps/ paper1/ paper.pdf Paper 1 manuscript PROOF_CHAIN.md Step-by-step trace of Paper 1's main theorem lean/ Lean 4 + Mathlib formalization STATUS.md Per-theorem status board (paper label ↔ Lean identifier) FRISoundness/ Named theorems (zero `sorry`, zero project-level axioms) lakefile.toml, lean-toolchain scripts/ Python verification scripts (stdlib only) CAVEATS.md Methodology caveats from a public-facing audit deployment_params.py Deployment parameter table generator proximity_gap_diagram.py Proximity-gap figure ca-bound/ Half- and equal-threshold CA fri-coupling/ FRI even/odd coupling and proximity gap op1-barrier/ Equal-threshold CA equals C(n,w)/|F| op2-obstruction/ M_max >= 2 at FRI parameters list-size/ Moments and pairwise / k-wise independence char2-circle/ Characteristic-2 / circle-FRI extensions cs-construction/ Crites--Stewart construction sweep archive/ Earlier exploratory scripts outputs/ Saved script outputs (mirrors scripts/) paper2/ paper.pdf Paper 2 manuscript scripts/ CAVEATS.md Caveats for the deployment-scale spot checks deployment-l3/ Paper 2 L3 / boundary-lift / GS m=2 list-decode LICENSE Apache 2.0 ``` ## 快速开始 **构建 Lean 形式化验证**（论文 1）： ``` cd paper1/lean lake exe cache get # download Mathlib cache (~5 min) lake build # builds FRISoundness (zero `sorry`) ``` **运行验证脚本**： ``` python3 paper1/scripts/op1-barrier/op1_scaling.py python3 paper2/scripts/deployment-l3/issue419_action_orbit_check.py ``` **重新生成论文 1 的部署参数表或近距间隙图**： ``` python3 paper1/scripts/deployment_params.py [--latex] [--per-round-max] python3 paper1/scripts/proximity_gap_diagram.py ``` 每个脚本的文档字符串详细说明了其计算内容；方法论的注意事项位于每篇论文的 `scripts/CAVEATS.md` 中。保存的输出（预计算部分）与 `paper1/outputs/` 下的脚本布局相对应；可通过重定向 stdout 来刷新，例如： `python3 .../op1_scaling.py > paper1/outputs/op1-barrier/op1_scaling.output.txt`。 CI 工作流（`.github/workflows/ci.yml`）会在每次推送时运行 `lake build` 以及部分 Python 脚本。 ## 引用 ``` @misc{ChaiFan2026FRI, author = {Chai, Raullen and Fan, Xinxin}, title = {{FRI} Soundness Above the {J}ohnson Bound via Threshold Halving}, year = {2026}, howpublished = {Cryptology ePrint Archive, Paper 2026/861}, url = {https://eprint.iacr.org/2026/861}, note = {Companion repository: \url{https://github.com/iotexproject/rs-proximity-gaps}} } @misc{ChaiFan2026ActionOrbit, author = {Chai, Raullen and Fan, Xinxin}, title = {Action-Orbit {FRI} Soundness above {J}ohnson: Universal $K$-Bounds at Ethereum-Deployed {R}eed--{S}olomon Parameters}, year = {2026}, howpublished = {Cryptology ePrint Archive, Paper 2026/858}, url = {https://eprint.iacr.org/2026/858}, note = {Companion repository: \url{https://github.com/iotexproject/rs-proximity-gaps}} } ``` ## 许可证 [Apache License 2.0](LICENSE)。

标签：ePrint论文, FRI, IoTeX, Johnson半径, Lean 4, Python, Reed-Solomon, STARK, 以太坊, 列表解码, 区块链, 密码学, 形式化验证, 手动系统调用, 无后门, 逆向工具, 邻近间隙, 零知识证明