# 兼容性与资源额度

schema 1、旧 dispatch_json 和原生 src/core 接口保持兼容。Engine 彼此隔离，关闭会话与卸载数据库显式执行。旧工作文件通过重新验证和重放恢复。

0.7.1 将证明中的标签与字符错误定位到具体 token 或字符，字段形状、错误码和数学结果保持不变。最终栈错误与声明级交互错误保留原跨度，具体规则见 [API 的诊断约定](API.md#请求与响应)。

## 输入与证明

- 标准 ASCII profile：可打印 ASCII，以及 space、tab、CR、LF、form-feed。BOM、非 ASCII、其他控制字符明确拒绝。
- 支持常量、变量、活动 `$f/$e`、`${/$}` 作用域、`$d`、公理、定理、普通标签证明与压缩证明。
- 必要假设遵守原声明次序；同时代换允许合法空表达式；检查类型、essential hypothesis、不交变量条件、自引用与未来引用。
- include 为源集合内的确定性解析；相对包含文件目录解析路径，同一规范化文件只包含第一次。源文件各自须具有完整语法边界。子源内的诊断使用子源 id 与子源本地字节偏移、行列，不折算到包含它的文件。
- `?` 明确记为 incomplete。解析成功或 list 成功不把未检查 `$p` 变成可信依赖。
- 可重做现有定理，也可在已有 `$p` 的上下文中创建新目标，完整继承活动假设及 `$d`。新目标只编辑已有符号组成的表达式与新标签；不支持自由新增声明或公理。
- 规则检索只返回当前目标可用的活动假设、可见公理和此前已验证定理，支持标签/结论子串与精确类型码筛选；不包含原目标或未来标签。预览只证明一步合法，不能据此判断目标可证或获得进展。
- 暂不提供逆向 tactic、自动证明搜索或通用模型搜索；独立小型AI实验已真实执行固定10题，模型10/10、有限搜索8/10，见[实际结果](AI_RESULTS_2026-10-24.md)；不构成通用搜索或新数学成果声明。
- 普通构造会话完成后可导出自足普通 `.mm`。压缩导出、原证明 replay 转普通证明未交付。

## 官方 C 的已知分歧

固定官方 C 对 79 项为 **72 项符合预期、7 项分歧**。具体分歧如下：

| 用例 | C 的实际行为与上游预期 |
| --- | --- |
| test015、test045 | self include 触发上游 BUG1765，参考工具错误 |
| test022、test041、test043 | C 允许变量在后续作用域使用不同 typecode 的 `$f`；测试预期 invalid |
| test050、test054 | C 拒绝对 hypothesis/local step 的 `Z` 保存；测试预期 valid |

MoonMetamath 与固定 mmreference 在这套材料上符合上游预期。上述分歧须依据规范和最小输入理解，不能以 C 的多数结果代替语义判定。独立 C 接受实际浏览器导出文件，是单独确认的结果。

## 默认资源额度

| schema 字段 | 默认值 |
| --- | --- |
| `max_file_bytes` | 67,108,864（64 MiB） |
| `max_total_bytes` | 134,217,728（128 MiB） |
| `max_include_depth` | 32 |
| `max_tokens` | 10,000,000 |
| `max_operations` | 10,000,000 |
| `max_stack_items` | 100,000 |
| `max_expression_tokens` | 1,000,000 |

这些参数约束每次调用的资源使用。字段取非负整数；溢出与超限不标 valid。Node 源解析宿主另限制最多 1000 个文件，只读允许 root 内文件；CLI Worker 默认 120000 ms 截止及 512 MiB old-generation heap 限制，`--timeout-ms` 可设为 1..300000，超时或 SIGINT 会终止 Worker 并返回退出码 5。Web 只读用户选择的文件集合；普通多文件选择使用文件名，复杂嵌套目录需保持相应逻辑路径。

规则分页默认每页 20 条，上限 100 条，offset 非负，limit 可为 0。工作文件另限 128 MiB、10,000 个成功动作；点击保存时，本机浏览器只保留至多 2 MiB 的上次保存，超出时仍可下载文件但不覆盖本机保存。

网页显示当前阶段与已确认步骤。取消终止活动及恢复 Worker，原内部句柄不能继续使用；可重新加载或在新 Worker 中恢复此前保存的工作。恢复检查源哈希、重新解析验证并重放动作，失败不替换当前工作。完成状态来自重放后的 finish 检查；保存格式仅接受源和动作。`reset` 释放同一 dispatcher 实例所有上下文。

## 环境与历史测量

运行环境为 Node.js 24；源码构建支持 Windows x64、Linux x64，核心测试覆盖 JS 和 wasm-gc。Web 使用 Worker 中的 JavaScript。

完整 set.mm 的既有测量条件见 [性能报告](PERFORMANCE.md) 和 [大库工作台](LARGE_WORKBENCH.md)。本轮修改的验证记录与历史测量分别保留。

所有保留源均检查 ASCII、单文件和总字节额度。解析时 `$d` 派生变量对的累计展开受 max_operations 限制，包含 include；证明执行另行计数。CLI 可用 --max-operations 显式配置。