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

测量日期：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或其他机器的性能。