第五章ProofGrid 分布式证明

概述

ProofGrid是 JasperGold 的分布式证明管理系统，可以将证明任务分发到本地机器或服务器集群（Server Farm）上并行执行，大幅缩短证明时间。

ProofGrid 基础概念

Server Farms

ProofGrid 支持 LSF、GRID 等作业调度系统，可以在服务器集群上并行提交证明任务。

Engine Race

ProofGrid 的核心策略：对每个属性同时启动多个引擎，第一个完成的引擎获胜。这避免了手动选择引擎的不确定性。

Nice Licenses

"Nice"许可证是低优先级许可证，当有高级许可证空闲时自动使用，满载时自动放弃，不影响其他用户。

ProofGrid Manager GUI

Proof Threads View

显示每个属性的证明线程列表，包括：

• 正在运行的引擎
• 每个引擎的运行时间和状态
• 线程进度

Engine Graph

实时绘制引擎进展曲线：

• Progress indicators：Property Table 中的进度指示
• Plateaus：曲线平坦表示引擎没有新进展
• Spikes：正尖峰表示引擎取得突破
• Negative Spikes：负尖峰通常表示反例找到或状态空间缩小

Summary View

ProofGrid 运行的总体统计：已证明/失败/运行中的属性数量。

配置指南

Per-Property Time Limit

set_prove_per_property_time_limit 60s

为每个属性设置合理的时间限制，避免单个属性占用过多资源。

Focused Proof

对于端到端的高价值断言，使用 focused proof：

set_proofgrid_focused_prove -property <critical_assertion>

配置命令

# 启用 ProofGrid
set_proofgrid_mode on

# 设置并行任务数
set_proofgrid_max_jobs 16

# 设置服务器类型
set_proofgrid_server_type lsf

# 设置 Nice 许可证
set_proofgrid_nice_licenses on

使用流程

1. 配置 ProofGrid 参数（服务器、任务数、时间限制）
2. 启动证明（prove -all）
3. 在 ProofGrid Manager 中监控进度
4. 观察 Engine Graph，识别 plateau 的属性
5. 对 plateau 的属性调整策略或增加约束

ProofGrid 分布式证明界面

ProofGrid 分布式证明方法论

什么时候需要 ProofGrid

单机证明遇到以下情况时考虑 ProofGrid：

• 属性数量大（几百上千个），单机串行跑太慢
• 单个属性就需要很长时间（小时级）
• 项目回归周期短，需要快速跑完所有证明
• 有多个 CPU 核/服务器可用

ProofGrid 的工作原理

ProofGrid 将证明任务自动分发到多个计算节点并行执行：

1. 主节点切分属性列表，调度到 worker 节点
2. 每个 worker 独立跑一部分属性，使用不同引擎配置
3. 结果回传到主节点汇总
4. 未证明的属性可以重新分发，尝试不同引擎

使用策略

• 先用单机跑第一轮：快速证明大部分简单属性（通常 70-80% 能在几分钟内 proven）
• 剩下的难属性上 ProofGrid：将 remaining 属性并行分发到多节点
• Proof Threads View：实时监控每个节点的进度
• Engine Graph：分析哪个引擎对哪类属性最有效