# 性能测量与资源记录

## 0.8.0：报告复用与定理分页

以正式 0.7.1 为基线，分别测量报告复用（T6）和定理索引（T7），再验证组合结果。T6 返回 create_goal 内部本次真实验证报告，Web 省去取得报告所需的第二次 verify；T7 为空查询保留定理声明下标，每次读取当前状态。非空查询、旧 list 和保存恢复验证保持原义。

interaction 使用 Node 24.15.0、2048 MiB old-space、100,000,000 operations 和 300,000 ms 截止。三库固定输入、每格三个新进程，全部串行；同一 harness 的 SHA256、输入锁和环境均核对一致。操作系统缓存及桌面背景负载未控制，下表为本机三个样本的中位数，不是浏览器页面耗时。

| 库 | 0.7.1 新目标调用链 | 最终组合版本 | 中位数改善 |
| --- | ---: | ---: | ---: |
| hol | 26.032 ms | 19.687 ms | 24.37% |
| nf | 621.498 ms | 409.612 ms | 34.09% |
| set | 19,304.176 ms | 10,976.272 ms | 43.14% |

调用链从 create_goal 请求序列化前开始，到新目标 rules 的响应解析及断言结束；包含报告取得、全页摘要收集和新会话准备，排除原库加载验证、原目标 start、清理、DOM、网络与日志写入。T6 单独的调用链改善为 21.06%、31.75%、37.39%，各组三次样本范围不重叠。

T7 的独立对照采用同一 T6 报告策略，主指标为原库空查询全页收集：

| 库 | 仅 T6 | T6＋最终索引 | 判断 |
| --- | ---: | ---: | --- |
| hol，2 页 | 1.417 ms | 1.620 ms | 增加 0.203 ms，范围重叠，未达到改善目标 |
| nf，60 页 | 34.544 ms | 21.846 ms | 改善 36.76%，范围不重叠 |
| set，481 页 | 1,533.089 ms | 187.126 ms | 改善 87.79%，范围不重叠 |

保留 T7 用于中大库。hol 的变化未触及“同时超过 10% 和 5 ms”的小库回退线，也不作为小库加速依据。最终 set interaction 最大峰值 RSS 为 1,537,588 KiB，较仅 T6 增加 1,204 KiB，未触及原定内存门槛。

### 512 MiB 检查与原始回退

首次组合候选的 verify 模式进程总时长为 17,775.34 ms，对照 12,247.77 ms，增加 45.13%，超出判断线；两侧仍完成 48,097 条证明。该失败保留。随后将索引从动态 push 改为先计数、精确分配、按实际声明位置填充，避免动态容量增长。

最终候选与同轮基线都在原 512 MiB 配置下完成 48,097 / 48,097，进程总时长为 13,193.98 / 11,718.04 ms，增加 12.60%；峰值 RSS 为 721,644 / 717,380 KiB，增加 4,264 KiB。时间与 RSS 均在既定门槛内。这是一对观测；现有记录不能把两轮耗时差异因果归于预分配或 GC。

最终 Windows 引擎 SHA256 为 `619affadba12328548d483ee5cc5669bdd61d78f7139fc6a63aed4d77a75161d`。[逐样本数据](../benchmarks/results/v0.8.0.json)包含四组 interaction 和两对 512 MiB 检查，保留初始候选的回退。完整本地日志位于源码工作区的 `artifacts/proof-diagnostics-large-library/20261104-t5-t7/`；最终统计为 `comparison-preallocated.json` 和 `verify-resource-preallocated.json`。旧候选的 interaction 测量未当作最终版本数据。

## 0.4：真实数据库性能基线与加载内存优化

版本说明：下文保留0.4的历史测量及当时失败。0.5已修复长字符串响应内存膨胀，并完成大库工作台流程；新结果见[LARGE_WORKBENCH.md](LARGE_WORKBENCH.md)。

测量日期：2026-10-26。比较已发布0.3.0与0.4候选的同一MoonBit JS公共dispatcher路径。
三份完整数据库固定于官方`metamath/set.mm`提交`b4c3130f3b8081e1e4a33b47321141359e3380ae`，没有截短文件或改写证明。
来源、Git blob、SHA256和固定交互目标见[输入锁](../benchmarks/databases.lock.json)；
[逐样本公开数据](../benchmarks/results/v0.4.0.json)保留46条成功/失败/诊断记录及阶段内存、计时和构建身份。

### 输入、环境与计时范围

| 输入 | 完整字节数 | 证明数 | 用途 |
|---|---:|---:|---|
| hol.mm | 96,899 | 151 | 小型真实库 |
| nf.mm | 2,985,101 | 5,976 | 中型真实库 |
| set.mm | 51,737,997 | 48,097 | 大型完整库 |

三份原文件均由固定官方C检查器独立验证有效。数学判定仍由产品原生MoonBit核心完成；C只作开发对照。

环境为Windows x64、Intel Core i9-14900HX、32逻辑CPU、约47.7GiB内存、Node24.15.0；
compiler `v0.10.14+7d59c7ec9`、moon `0.1.20260920`保持不变。
每个样本使用新Node进程，样本顺序执行；操作系统文件缓存和桌面背景负载未受控。
这里的“冷进程”不等于冷磁盘缓存。小、中库的完成单元各3次；大库完整验证的2GiB旧版组由先前1次完整诊断与随后同预算2次组成，全部保留，没有删除较慢样本。

读盘、内容校验、JSON序列化、dispatcher调用、响应解析与进程启动分别记录。
下表的load/verify只计同步dispatcher调用，包含其内部JSON处理，**不是纯数学内核时间**。
峰值RSS是Node进程至工作负载结束时的高水位，包含输入、宿主和运行时；不是核心专属内存，也不是V8 old-space额度。
完整子进程截止为120秒，失败单元第一次失败后即停止重复。

### 同预算验证比较

时间为3次完成样本的中位数，括号为最小–最大，单位ms；内存为峰值RSS中位数，单位MiB。

| 输入与相同配置 | 0.3 load | 0.4 load | 0.3 verify | 0.4 verify | 0.3 RSS | 0.4 RSS |
|---|---:|---:|---:|---:|---:|---:|
| hol，512MiB old-space／默认核心预算 | 22.08 (21.70–24.02) | 24.43 (23.23–24.52) | 15.71 (15.39–16.12) | 15.96 (15.26–15.97) | 66.07 | 59.89 |
| nf，512MiB old-space／默认核心预算 | 262.25 (240.76–265.82) | 211.46 (208.63–212.78) | 257.36 (252.13–300.10) | 235.78 (235.38–239.25) | 304.62 | 148.55 |
| set，2048MiB old-space／明确100m操作预算 | 4545.24 (4442.54–7204.46) | 3452.27 (3377.32–3857.61) | 6580.73 (6475.07–12653.20) | 6762.60 (6398.30–11064.78) | 1908.80 | 749.70 |

这组样本中，nf峰值RSS约降低51%，set在相同2GiB配置下约降低61%。
set加载中位数约降低24%；验证阶段没有可靠的加速结论。
小库加载中位数增加约2.4ms，不能宣称所有场景都更快。
三次样本只支持描述性比较，不构成统计显著性或跨硬件性能保证。

### 默认额度与完整set的区别

生产默认`max_operations=10,000,000`保持不变。完整set超过这个预算。

| 配置 | 0.3实际结果 | 0.4实际结果 |
|---|---|---|
| 512MiB old-space，默认核心预算 | load阶段OOM，未进入验证 | load完成；验证44,552/48,097后明确resource_limit，余3,545未检查 |
| 2048MiB old-space，默认预算（旧版单次诊断） | 同样在44,552后达到操作上限 | 不为这条诊断重复增加样本 |
| 512MiB old-space，明确100m操作预算 | 旧版load已在同一加载条件失败，不追加相同失败重试 | 3/3完整验证48,097；load中位数4126.09ms，verify7072.35ms，RSS692.02MiB |

100m是基准运行时显式传入的`limits.max_operations=100000000`，并非修改产品默认值。
512MiB old-space不等于512MiB总进程内存，所以RSS可以超过它。
OOM样本的未完成阶段耗时与最终峰值均为未知；记录的最近内存采样只标为已观察下界。
本项目没有将提高额度后的完成率与低额度失败混算成速度提升。

### CLI整合补充检查

真实CLI路径还包含宿主include收集。整合时发现它原先会为全部token建立数组；改为顺序扫描后，V8的legacy RegExp last-input缓存仍保留整份注释剥离文本。在同一512MiB Worker中的单变量对照确认，释放这项引用后才能继续完成加载。

最终宿主按相同三token规则顺序收集include，并在成功扫描后释放该缓存；没有改变允许目录、源字节、递归顺序或预算。12MiB合成文件的64MiB子进程负控验证了旧数组OOM和旧缓存残留；这些是回归测试，不计入46条真实数据库性能样本。

最终实际CLI验证完整set已加载254,647条声明，并在默认10m预算处报告44,552/48,097、3,545未检查，退出码5。它没有再以Worker内存异常提前终止，也没有被标为完整验证成功。完整验证的显式100m配置仍通过本报告的库级benchmark入口复现。

### 固定交互工作负载

目标在计时前固定为各库最后一个定理：hol `axun`、nf `conventions`、set `young2d`。
每次运行查询5次、预览固定活动假设5次、应用1步、检查状态、重放撤回5次、撤回到0，
最后在同一上下文创建原目标的新标签。它测量部分证明操作，**没有完成新证明**。

下面为相同512MiB/default配置的3样本中位数，单位ms；query/preview/rewind均为整个5次批次：

| 库与版本 | query×5 | preview×5 | rewind×5 | create_goal | 进程峰值RSS MiB |
|---|---:|---:|---:|---:|---:|
| hol 0.3 | 5.71 | 0.91 | 0.76 | 21.86 | 78.08 |
| hol 0.4 | 5.82 | 0.84 | 0.54 | 20.29 | 68.52 |
| nf 0.3 | 38.22 | 1.42 | 0.70 | 454.61 | 368.88 |
| nf 0.4 | 36.37 | 1.27 | 0.69 | 409.90 | 247.37 |

**完整set的交互边界仍未解决。** 0.4在512MiB/100m配置下完成验证、查询、预览和撤回后，于create_goal阶段OOM。
在明确2048MiB/100m诊断配置中，0.3在create_goal内部OOM；0.4的create_goal dispatcher调用完成，
但宿主JSON响应解析随后OOM。因此两者的完整大库工作台流程都没有在该配置下完成，不能将0.4的局部调用结果标为成功。
大库新目标仍重建和验证完整声明前缀，并返回包含源文本的响应；本轮没有为此引入增量验证、共享验证缓存或改变返回接口。

### 根据测量选择的改动

1. 首次512MiB基线直接在load内存失败。去掉词法分析的整份字符数组，并对未变化的活动变量、假设与不交变量上下文复用私有不可变快照；真实push/pop时分别失效。第一轮nf已有内存改善，但set仍加载OOM，保留该中间结果。
2. 同一候选的独立scanner诊断显示，返回全文件约510万token的数组时进程峰值已约705MiB。解析器改用共享私有cursor按声明消费token，避免同时持有全文件token数组和完整数据库。
3. 为保持错误兼容，解析前仍完成ASCII、词法与token预算预检，父文件完整token计数仍在include前累计。公开`scan_source`继续返回数组；没有更改必要假设顺序、作用域、代换、可信前缀或统一证明执行器。

新实现会重扫词法流，单个特别长的声明仍需要它自己的token缓冲。它降低的是全文件token驻留及重复上下文分配，不能称为常量内存解析器。
在已取得大库验证容量改善且兼容测试通过后，本轮停止性能调优，没有为尚未定位的CPU成本增加索引或第二套执行器。

### 复现、证据与限制

命令及参数见[benchmark入口](../benchmarks/README.md)。旧版可从正式0.3.0 Node24 ZIP取出`dist/moonmetamath-core.mjs`，
其SHA256为`7fd5669dad5d0e5bfdf61c5bc5fd5226a4acfe83a574ed8361b56fb911b81c9a`；本次已核对冻结基线与正式归档字节相同。
0.4受测产物SHA256为`51d84d614043e8fe3ec61c4f30adc391aff9f3948189be062fd6d4f02ad262a9`。
每次比较必须保持数据库、工作负载、核心预算、堆额度、Node和工具链一致。

初始harness随后加入证明数、引擎摘要校验和harness身份记录，均在dispatch计时区间之外。
独立测量审查还发现旧`process_wall_ms`包含父进程证据整理，已用250ms延迟负控修复；
原始行不改写，旧process wall排除在本文和公开比较数据之外。dispatch计时程序未因此改变，版本摘要保留在数据中。

完整测试、独立审查及正式发布验收见[PROGRESS](../PROGRESS.md)。这些性能数字来自本机Windows JS路径；
双后端语义检查及跨平台CI不等于已经测量Linux、wasm-gc、浏览器上传完整set或其他机器的性能。