Numi2/SuperNeo-NuMetal
GitHub: Numi2/SuperNeo-NuMetal
SuperNeo NuMetal 是 Swift 实现的格点折叠协议研究级原型，专注于在 Apple 平台上的协议验证与基准测试。
Stars: 1 | Forks: 0
# SuperNeo NuMetal
SuperNeo NuMetal 是 SuperNeo 格点折叠协议在
定制约束系统（CCS）上的 Swift 和 Metal 研究级实现，
适用于 Apple 平台。
实现的公开配置文件为 `Goldilocks/Phi81(d=54)`：Goldilocks 域算术、
54 次分圆环、Ajtai 风格格点承诺、折叠协议阶段、
版本化证明信封、可检验测试向量、基准测试工具，
以及假设范围的 Lean 形式化验证跟踪。
本仓库旨在用于协议研究、实现验证、基准测试和可复现性工作。
它不是生产级经过安全审计的密码学库。
## 状态
| 领域 | 当前状态 |
| --- | --- |
| 配置文件 | `Goldilocks/Phi81(d=54)`，`profileID = 1`。 |
| 软件包 | macOS 14+ Swift 软件包，包含库产品 `SuperNeo_NuMetal`、
CLI 可执行文件 `superneo` 以及形式向量辅助工具 `superneo-formal-vectors`。 |
| 证明模式 | 折叠约简、带公共 CE 打开材料的终端证明、
压缩的公共终端信封。 |
| 工作负载 | 捆绑的一热向量和 8 位二进制加法 CCS 工作负载。 |
| 后端 | CPU 参考实现以及选定的 Metal 加速。默认路由避免在小规模形状上使用 Metal，
将 Metal 作为加速路径而非信任预言机。 |
| 保障策略 | 对覆盖的恒定工作量 CPU 路径使用 `.highAssurance`，
对覆盖的 CPU 重校验 Metal 输出使用 `.cpuRedundantMetal`，
以及终端证明接受策略用于应用验证器上下文。 |
| 测试向量 | 折叠、终端和压缩终端工件，带有清单绑定的可信上下文。 |
| 基准测试 | 最新本地 Apple M4 快速切片已固定在 `benchmark-results/` 并汇总如下。 |
| 形式化 | Lean 4 中的条件协议形式化，由 `Docs/FormalStatus.json` 跟踪。 |
## 亮点
- 终端应用接受现在拥有可复用的策略 API。调用方可以
固定可信陈述上下文、在终端验证前拒绝折叠约简，
选择仅终端、仅压缩或两者皆可的终端证明形式，
并设置最大证明字节数。
- Swift/Lean 一致性桥接现在将可执行的 Swift 向量与
Lean 生成的 Ext2 和 CE 证明字节向量在生产门中比较，
并包含用于故障关闭漂移检测的变异测试。
- 基准测试仪器现在将 Metal 命令缓冲区的 GPU 时间与主机
编码、提交和等待时间分离，以便报告能够区分设备工作与
提交开销。
- Lean 形式化轨道拥有一个保守的标记不良事件组合层，
而完整协议定理仍有意地阻塞在机械化概率组合和 Swift 等价证明上。
## 能力
- Goldilocks 基域算术与 2 次扩张算术。
- `Phi_81(X) = X^54 + X^27 + 1` 的 54 次分圆环算术。
- 适用于 SuperNeo 嵌入的保范数域到环见证打包。
- Ajtai 承诺配置文件，`kappa = 18`，分解长度 `14`，
范数界 `2`，以及论文推导的声称配置文件安全级别 `129` 位。
- `PiCCS`、`PiRLC`、`PiDEC`、折叠约简验证、终端 CE
验证、压缩的公共终端信封，以及可选的 CE 打开
证明。
- 确定性序列化用于证明信封、承诺、公共输入、
评估声明、验证密钥材料与测试向量工件。
- 终端证明接受策略 API，用于可信验证器上下文、
可接受的证明种类以及证明字节限制。
- R1CS 到 CCS 辅助工具，用于捆绑的一热向量与二进制加法
工作负载。
- CPU 参考执行以及用于选定域、环、
承诺、变换求值以及融合提交/求值的 Metal 内核。
- 自适应 Metal 路由，在保持小型默认证明在 CPU 上的同时，
保留强制的 Metal 策略以用于大型形状加速、基准覆盖与
内核开发。
- 存在差异的 CPU/Metal 检查，当两条路径都存在时。
- 针对证明信封解析、验证器上下文绑定、重复 JSON 键、
工件模式、工作负载元数据、密钥种子域分离、
Metal 工作区不变量、已检查的分配大小以及高强度
执行策略的加固。
核心配置文件常量记录在 [Docs/Parameters.md](Docs/Parameters.md)。
| 数量 | 值 |
| --- | ---: |
| 基域模数 | `2^64 - 2^32 + 1` |
| 扩张域 | `F_q[u] / (u^2 - 7)` |
| 分圆多项式 | `X^54 + X^27 + 1` |
| 环次数 | `54` |
| Ajtai 行数 | `18` |
| 分解长度 | `14` |
| RLC 挑战系数 | `[-2, -1, 0, 1, 2]` |
| 挑战扩展因子 | `216` |
| 最大新鲜批次数 | `61` |
| 最大先验 CE 声明数 | `14` |
## 范围与信任模型
验证器接受仅在提供的 CCS 形状、公共输入、证明种类、
验证密钥、证明信封上下文与终端关系策略的背景下才有意义。
应用代码必须拥有预期的上下文、密钥分发、
工件来源、重放策略以及面向用户的接受语义。
折叠约简验证公共约简并返回输出
承诺-求值声明。需要终端接受的应用应
验证终端或压缩终端证明，并要求在策略边界处为终端证明种类。
`SuperNeoTerminalProofAcceptancePolicy` 还允许
应用限制接受的终端信封形式，并在昂贵的验证器路径前
拒绝过大的证明字节。
当前边界：
- 无生产级安全审计或独立安全认证，
- 无程序到 CCS 的通用编译器，
- 无持久化层、重放防护系统或面向用户的验证产品，
- 无针对任意应用陈述的完备零知识声明，
- 无完备的常量时间或侧信道证明，
- 无完备的完整协议定理。
简明证明语义记录在
[Docs/WhatThisProves.md](Docs/WhatThisProves.md)，操作威胁模型记录在
[Docs/ThreatModel.md](Docs/ThreatModel.md)。
## 需求
- macOS 14 或更新版本。
- Swift 工具链版本 6.1 或更新，通过 Xcode 或 Xcode 命令行工具。
- 支持 Metal 的 Apple 平台用于 GPU 加速与 Metal 基准行。
CPU 测试与 CPU 证明路径在不使用 Metal 基准行时仍可用。
- 通过 `elan` 使用的 Lean 4，用于可选的形式化工作区。
- SageMath 以及固定版本的上游 lattice-estimator 用于完整估计器复现。
干运行估计器参数推导不需要 SageMath。
根 Swift 软件包无第三方软件包依赖。基准专用依赖隔离在
[Benchmarks/Package.swift](Benchmarks/Package.swift)。
## 仓库布局
| 路径 | 用途 |
| --- | --- |
| [SuperNeo-NuMetal](SuperNeo-NuMetal) | 主 Swift 库实现。 |
| [SuperNeoCLI](SuperNeoCLI) | `superneo` 命令行集成演示。 |
| [SuperNeo-NuMetalTests](SuperNeo-NuMetalTests) | XCTest 覆盖与可用性表面测试。 |
| [TestVectors](TestVectors) | 已检查的公共证明工件、清单与 JSON 模式。 |
| [Benchmarks](Benchmarks) | Swift 基准测试软件包。 |
| [Scripts](Scripts) | 生产门、基准测试、验证与复现脚本。 |
| [Docs](Docs) | 协议、安全、基准、加固与形式化文档。 |
| [Formal]( \
--expected-verifier-key-digest \
--expected-shape-digest \
--expected-statement-digest \
--expected-public-inputs \
--require-terminal \
path/to/artifact.json
```
若不带可信上下文参数，验证器从工件本身读取种子与摘要，
这适用于演示但不适用于策略决策。证明信封将证明字节绑定到
配置文件 ID、证明种类、CCS 形状摘要、语句摘要、验证密钥摘要、
会话域与正文长度。请参考
[Docs/ProofEnvelope.md](Docs/ProofEnvelope.md)。
库集成应优先使用终端接受策略而非手动证明种类调度：
```
let policy = SuperNeoTerminalProofAcceptancePolicy(
publicInput: publicInput,
verifierKeyDigest: key.verifierKeyDigest,
proofKindPolicy: .compressedOnly,
maximumProofByteCount: 4 * 1024 * 1024
)
let result = verifier.verifyTerminalProofEnvelope(
publicInput: publicInput,
proofBytes: proofBytes,
policy: policy
)
```
使用 `.terminalOrCompressed` 当两种完整的终端信封形式均可接受。
使用 `.terminalOnly` 或 `.compressedOnly` 当资源策略、
工件策略或部署兼容性要求某一种形式。
## 测试向量
已检查的向量旨在用于兼容性与跨实现测试：
| 文件 | 工作负载 | 证明种类 |
| --- | --- | --- |
| [TestVectors/one-hot-vector-fold-v1.json](TestVectors/one-hot-vector-fold-v1.json) | 一热向量 | 折叠 |
| [TestVectors/one-hot-vector-terminal-v1.json](TestVectors/one-hot-vector-terminal-v1.json) | 一热向量 | 终端 |
| [TestVectors/one-hot-vector-compressed-terminal-v1.json](TestVectors/one-hot-vector-compressed-terminal-v1.json) | 一热向量 | 压缩终端 |
| [TestVectors/binary-addition-u8-fold-v1.json](TestVectors/binary-addition-u8-fold-v1.json) | 8 位二进制加法 | 折叠 |
| [TestVectors/binary-addition-u8-terminal-v1.json](TestVectors/binary-addition-u8-terminal-v1.json) | 8 位二进制加法 | 终端 |
`TestVectors/manifest.json` 是已检查向量的可信上下文：
哈希、字节数、公共输入、密钥种子、摘要、证明种类要求与严格验证命令。
`TestVectors/artifact.schema.json` 是机器可读的工件模式。
```
swift Scripts/validate-test-vectors.swift
```
请参考 [TestVectors/README.md](TestVectors/README.md) 了解重建规则与模式期望。
## 基准测试
基准结果仅在声明的正确性门后才有意义。
基准运行器在导出结果前验证协议输出，并在存在双路径时对比 CPU/Metal 输出。
当前性能亮点：
- 默认执行使用自动 Metal 路由并保持小型形状在 CPU 上；
使用 `.metalAccelerated` 当调用方希望强制 GPU 工作以用于已知工作负载或基准行。
- 生成的基准报告现在包含 GPU 命令缓冲区的 Metal 运行时间列，
以及 Metal 编码、提交与等待的主机耗时列，以便在报告中区分设备工作与提交开销。
- 最新的 Metal 审计移除了重复的工作区 CSR 上传，
增加了暂存缓冲区重用与内联调度参数，
引入了系数并行的环乘内核，
并为分解尺寸消息添加了窄 Ajtai 小消息内核。
- 行部分稀疏变换求值调度可用于调优但仍为可选，
因为本地小型 A/B 运行比阻塞基线更慢。
最新本地基准快照：
| 字段 | 值 |
| --- | --- |
| 生成时间 | `2026-04-14T03:00:20Z` |
| 源提交 | `31d69f0` |
| 源状态 | dirty |
| 主机 | MacBook Air，苹果 M4，10 个 CPU 核心，24 GB 内存 |
| 工具链 | Swift 6.3，Xcode 26.4 |
| 操作系统 | macOS 26.5 构建 `25F5042g` |
| 配置文件 | `quick` |
| 情况过滤器 | `m256-K2-k1-binary` |
| Metal 设备 | 苹果 M4 |
证明大小针对最新情况：
| 情况 | 约束 | 证明 | 信封 | 求和检查 | PiCCS | PiRLC | PiDEC | 输出声明 |
| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
| `m256-K2-k1-binary` | 256 | 344,616 B | 344,757 B | 880 B | 32,856 B | 12,248 B | 145,280 B | 153,328 B |
来自同一运行的选定计时行：
| 行 | 时间 | 推导速率 |
| --- | ---: | ---: |
| `fold/cpu/m256-K2-k1-binary` | 28 ms | 35.71 folds/s，9,143 constraints/s |
| `fold/metal/m256-K2-k1-binary` | 41 ms | 24.39 folds/s，6,244 constraints/s |
| `fold/prepared/cpu/m256-K2-k1-binary` | 27 ms | 37.04 folds/s，9,481 constraints/s |
| `fold/prepared/metal/m256-K2-k1-binary` | 38 ms | 26.32 folds/s，6,737 constraints/s |
| `stage/sumcheck/m256-K2-k1-binary` | 16 ms | |
| `stage/piCCSClaims/m256-K2-k1-binary` | 4.64 ms | |
| `stage/piRLC/m256-K2-k1-binary` | 2.18 ms | |
| `stage/piDEC/m256-K2-k1-binary` | 2.64 ms | |
| `reduceFold/cpu/m256-K2-k1-binary` | 2.37 ms | |
| `terminalVerify/cpu/m256-K2-k1-binary` | 4.83 ms | |
| `proofEnvelope/roundTrip/m256-K2-k1-binary` | 9.09 ms | |
| `kernel/ajtaiCommit/batch/cpu/m256-K2-k1-binary` | 5.34 ms | 187.23 commitments/s |
| `kernel/ajtaiCommit/batch/metal/m256-K2-k1-binary` | 1.79 ms | 559.60 commitments/s |
| `kernel/transformedEvaluation/cpuSparse/m256-K2-k1-binary` | 83 us | |
| `kernel/transformedEvaluation/metalSparse/m256-K2-k-binary` | 4.13 ms | |
完整生成的报告位于
[benchmark-results/report.md](benchmark-results/report.md)。基准配置文件、
正确性门、基于元数据的基线对比以及硬件级报告策略在
[Docs/Benchmarking.md](Docs/Benchmarking.md) 中有详细说明。
请不要使用这些数字进行跨版本比较。当前固定的 README 图形仅覆盖最新的本地 Apple M4 快速切片。
## 形式化与可复现性
构建 Lean 工作区：
```
cd Formal
lake build
```
验证形式状态清单与回归测试框架：
```
Scripts/validate-formal-status.py
Scripts/test-formal-status-validation.py
```
将可执行的 Swift 形式向量与 Lean 生成的向量进行比较：
```
Scripts/compare-formal-ext2-vectors.py
Scripts/compare-formal-ce-vectors.py
```
生成论文声明复现工件：
```
Scripts/reproduce-superneo-paper.sh quick
```
记录实现的模块 SIS 估计器元组（无需运行 SageMath）：
```
Scripts/reproduce-lattice-estimator.sh --dry-run lattice-estimator-results/superneo-goldilocks-phi81.json
Scripts/validate-lattice-estimator-artifact.py \
--expect-status not_run \
--expect-latest-status absent \
lattice-estimator-results/superneo-goldilocks-phi81.json
```
完整的估计器复现需要 SageMath 以及固定版本的上游
`malb/lattice-estimator` 源码，由脚本配置。
最新上游运行仅用于漂移监控，不应替代固定证据。
请参考 [Docs/FormalVerification.md](Docs/FormalVerification.md)、
[Docs/PaperReproduction.md](Docs/PaperReproduction.md) 以及
[Docs/LatticeEstimatorReproduction.md](Docs/LatticeEstimatorReproduction.md)。
## 文档
核心参考：
- [参数](Docs/Parameters.md)
- [威胁模型](Docs/ThreatModel.md)
- [证明语义](Docs/WhatThisProves.md)
- [证明信封](Docs/ProofEnvelope.md)
- [应用接受策略](Docs/ApplicationAcceptancePolicy-2026-04-14.md)
- [CLI](Docs/CLI.md)
- [基准测试](Docs/Benchmarking.md)
- [GPU 确定性](Docs/GPUDeterminism.md)
- [形式化验证](Docs/FormalVerification.md)
- [论文复现](Docs/PaperReproduction.md)
- [格点估计器复现](Docs/LatticeEstimatorReproduction.md)
- [路线图状态](Docs/RoadmapStatus.md)
最近的实现与加固说明：
- [基准元数据对比，2026-04-14](Docs/BenchmarkMetadataComparison-2026-04-14.md)
- [应用接受策略，2026-04-14](Docs/ApplicationAcceptancePolicy-2026-04-14.md)
- [PiRLC 基准隔离，2026-04-14](Docs/BenchmarkPiRLCIsolation-2026-04-14.md)
- [开启批处理并行阈值，2026-04-14](Docs/BenchmarkOpeningBatchThreshold-2026-04-14.md)
- [关系求值计划，2026-04-14](Docs/BenchmarkRelationEvaluationPlan-2026-04-14.md)
- [求和检查先验声明求值批，2026-04-14](Docs/BenchmarkSumcheckPriorBatch-2026-04-14.md)
- [求和检查公共预计算清理，2026-04-14](Docs/BenchmarkSumcheckPublicPrecompute-2026-04-14.md)
- [变换求值融合，2026-04-14](Docs/BenchmarkTransformedEvaluationFusion-2026-04-14.md)
- [Metal 性能优化，2026-04-14](Docs/MetalPerformanceOptimization-2026-04-14.md)
- [二进制加法终端向量，2026-04-14](Docs/BinaryAdditionTerminalVector-2026-04-14.md)
- [压缩终端向量，2026-04-14](Docs/CompressedTerminalVector-2026-04-14.md)
- [向量清单重复键加固，2026-04-14](Docs/VectorManifestDuplicateKeyHardening-2026-04-14.md)
详细的、带时间戳的工件解析、负载规范、密钥种子域分离、
终端向量、Ajtai 密钥、基准测试通过项与形式化提升记录保存在
[Docs](Docs) 中。
标签：8位二进制加法, Ajtai, Apple平台, CCS, CPU参考实现, d=54, Goldilocks, Lean 4, Metal, Metal加速, NuMetal, Phi81, SuperNeo, Swift, 一键热向量, 公钥打开材料, 冗余CPU校验, 协议研究, 压缩终端信封, 可重现性, 向量化工作负载, 基准工具, 实现验证, 常量工作时间, 形式化向量助手, 形式化验证, 循环环, 折叠协议, 晶格承诺, 晶格折叠, 格密码, 格折叠, 测试向量, 版本化证明信封, 约束系统, 自定义约束系统, 金凤花字段, 高保证策略