From cec62208620cd37d81717af4d73795aac7b87afe Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Sun, 9 Aug 2026 16:22:55 +0900 Subject: [PATCH 1/9] =?UTF-8?q?=E4=BB=93=E5=BA=93=E6=B2=BB=E7=90=86?= =?UTF-8?q?=E8=90=BD=E5=9C=B0=EF=BC=9ACI=20+=20=E5=8F=8C=20ruleset=20+=20?= =?UTF-8?q?=E7=A4=BE=E5=8C=BA=E5=9B=9B=E4=BB=B6=E5=A5=97=20+=20=E6=9C=AC?= =?UTF-8?q?=E5=9C=B0=E9=85=8D=E7=BD=AE=EF=BC=88GitFlow=EF=BC=89=20(#25)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * docs(governance): 仓库治理实施计划(本地配置/ruleset/签名/端到端验证 9 任务) * chore(governance): jj main bookmark 保护 * chore: .superpowers/ 加入 gitignore(SDD 工件目录) * chore(governance): jj SSH 提交签名(sign-all) * feat(governance): 铁律 #2 git 拦截 hook(.claude/settings.json + block-git.py) * chore(governance): settings.local.json 移除 Bash(git *) 允许项 * docs: CLAUDE.md 版本控制流程段(GitFlow 工作流命令) * chore(governance): 创建 develop 集成分支(GitFlow) * feat(governance): ruleset 配置脚本(main/develop,evaluate 模式,双路径) * feat(governance): ruleset 落地——main/develop 双 ruleset active + schema 修正 + 免费计划偏差记录(evaluate→active、merge_queue 降级) * fix(governance): 最终审查修复——merge queue 措辞降级为手动合入(CLAUDE.md/CONTRIBUTING/spec §7)+ §3.3/§12 补记 + plan Task 7 注 + ci.yml 注释 + run.sh 健壮性 * chore(diag): 最小工作流连通性测试 * fix(ci): 移除 merge_group 触发——merge_group 工作流仅限默认分支注册且 merge queue 已降级,恢复条件写入注释 * chore(diag): ci.yml 注释 ASCII 化测试 * chore(diag): ci.yml 最小骨架测试(pull_request 触发) * chore(diag): ci.yml 纯 push 触发测试 * chore(diag): 判别——工作流名 CI vs 文件名 ci.yml * fix(ci): 工作流文件改名为 core-ci.yml——ci.yml 文件名在 GitHub 侧注册异常(同内容同名不同文件名的对照实验证实),诊断文件清理 * chore(diag): core-ci 最小 pull_request 骨架 * chore(ci): 清理诊断残留与 opencode 工件(快照卷入);core-ci.yml 恢复完整内容 * chore(ci): core-ci.yml 恢复完整内容(矩阵 + run.sh 分发) * chore(diag): ruleset 禁用测试(验证注册同步是否被规则阻塞) --- .claude/hooks/block-git.py | 16 + .claude/settings.json | 15 + .github/CODE_OF_CONDUCT.md | 49 ++ .github/CONTRIBUTING.md | 48 ++ .github/SECURITY.md | 15 + .github/pull_request_template.md | 17 + .github/workflows/core-ci.yml | 62 +++ .github/workflows/opencode.yml | 33 -- .gitignore | 1 + .opencode/opencode.json | 6 - CLAUDE.md | 29 + .../plans/2026-08-09-repo-governance.md | 525 ++++++++++++++++++ .../2026-08-09-repo-governance-design.md | 160 ++++++ src/ci/run.sh | 79 +++ src/ci/scripts/run-build-from-ci.sh | 20 + src/ci/scripts/setup-environment.sh | 14 + src/ci/shared.sh | 34 ++ tools/gh_setup_ruleset.sh | 86 +++ 18 files changed, 1170 insertions(+), 39 deletions(-) create mode 100644 .claude/hooks/block-git.py create mode 100644 .claude/settings.json create mode 100644 .github/CODE_OF_CONDUCT.md create mode 100644 .github/CONTRIBUTING.md create mode 100644 .github/SECURITY.md create mode 100644 .github/pull_request_template.md create mode 100644 .github/workflows/core-ci.yml delete mode 100644 .github/workflows/opencode.yml delete mode 100644 .opencode/opencode.json create mode 100644 docs/superpowers/plans/2026-08-09-repo-governance.md create mode 100644 docs/superpowers/specs/2026-08-09-repo-governance-design.md create mode 100755 src/ci/run.sh create mode 100755 src/ci/scripts/run-build-from-ci.sh create mode 100755 src/ci/scripts/setup-environment.sh create mode 100644 src/ci/shared.sh create mode 100755 tools/gh_setup_ruleset.sh diff --git a/.claude/hooks/block-git.py b/.claude/hooks/block-git.py new file mode 100644 index 0000000..097969f --- /dev/null +++ b/.claude/hooks/block-git.py @@ -0,0 +1,16 @@ +#!/usr/bin/env python3 +"""铁律 #2 机械执行:Bash 命令以 git 开头 → 拒绝执行(exit 2)。""" +import json +import sys + +data = json.load(sys.stdin) +cmd = data.get("tool_input", {}).get("command", "") +stripped = cmd.strip() + +if stripped == "git" or stripped.startswith("git "): + sys.stderr.write( + "铁律 #2:全面使用 jj,禁止 git。\n" + "改用 jj 命令:jj status / jj log / jj describe / jj git push / jj bookmark ...\n" + ) + sys.exit(2) # PreToolUse exit 2 = block the tool call +sys.exit(0) diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 0000000..a5b65fe --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,15 @@ +{ + "hooks": { + "PreToolUse": [ + { + "matcher": "Bash", + "hooks": [ + { + "type": "command", + "command": "python3 .claude/hooks/block-git.py" + } + ] + } + ] + } +} diff --git a/.github/CODE_OF_CONDUCT.md b/.github/CODE_OF_CONDUCT.md new file mode 100644 index 0000000..34042ea --- /dev/null +++ b/.github/CODE_OF_CONDUCT.md @@ -0,0 +1,49 @@ +# 贡献者行为规范 + +## 我们的承诺 + +为了营造开放、友好的环境,我们作为贡献者和维护者承诺:无论年龄、体型、身体障碍、种族、 +性别认同与表达、经验水平、教育程度、社会经济地位、国籍、个人形象、种族、宗教或性取向, +参与本项目及社区的人都不会受到骚扰。 + +## 我们的标准 + +有助于创造积极环境的行为包括: + +- 使用友善和包容的语言 +- 尊重不同的观点和经验 +- 优雅地接受建设性批评 +- 关注对社区最有利的事情 +- 对其他社区成员表示同理心 + +不可接受的行为包括: + +- 使用与性有关的言语或图像,以及不受欢迎的性关注或性挑逗 +- 挑衅、侮辱或贬损性评论,以及人身攻击或政治攻击 +- 公开或私下的骚扰 +- 未经明确许可,发布他人的私人信息(如住址或电子邮箱) +- 在专业环境中可以合理地认为不适当的其他行为 + +## 我们的责任 + +项目维护者负责澄清可接受行为的标准,并应对任何不可接受的行为采取适当和公正的纠正措施。 + +项目维护者有权删除、编辑或拒绝不符合本行为规范的评论、提交、代码、wiki 编辑、issue 和其他 +贡献,以及暂时或永久禁止任何他们认为不当、威胁、冒犯或有害的贡献者。 + +## 适用范围 + +本行为规范适用于项目空间和公共空间(个人代表项目或其社区时)。 + +## 执行 + +如遇骚扰或其他不可接受的行为,可通过 **dsls.dzc@gmail.com** 联系项目团队。所有投诉都会被 +审查和调查,并得到必要且适当的回应。项目团队有义务对事件举报者保密。 + +项目维护者不遵守或不信奉行为规范者,可能面临由项目其他领导成员决定的暂时或永久性处分。 + +## 参考 + +本行为规范改编自 [Contributor Covenant][homepage] 2.1 版。 + +[homepage]: https://www.contributor-covenant.org diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md new file mode 100644 index 0000000..29380e3 --- /dev/null +++ b/.github/CONTRIBUTING.md @@ -0,0 +1,48 @@ +# 贡献指南 + +Core 的开发流程参考 Rust/Linux:**main 即 mainline,任何人(含维护者)不得直推**。 +全部改动经 PR + 审查 + 合入门槛进入 main。 + +## 流程 + +1. **fork 仓库**,在 fork 上建 feature 分支(`fix/xxx`、`feat/xxx`、`docs/xxx`) +2. 提交改动(请用 jj,见下),推送分支 +3. **开 PR——base 指向 `develop` 集成分支**(main 不接受直接合入;main 的合入仅维护者可执行),按 `.github/pull_request_template.md` 填写: + - 变更描述、测试记录、语义保鲜影响(IR/类型语义是否变化) +4. 等待审查(≥1 审批,审批人限维护者) +5. 审批通过且 PR 层 CI 全绿后,维护者手动 **squash 合入 develop**(merge queue 因免费计划不可用,已降级;见 spec §3.3),源分支由 GitHub 自动删除 + +## 铁律 + +- **全面使用 jj,禁止 `git` 命令**(仓库为 jj colocated 形态;维护者本地 Claude Code hook 会拦截 git) +- 长时间编译/测试任务限速运行(`cpulimit -l 10` 或 `nice -n 19`) +- 文件还原必须经维护者明确许可 + +## 构建与测试 + +```bash +python3 build_selfhost_native.py # 自举构建 → build/corec + build/corearch +./build/corec check FILE.cr # 类型检查 +./build/corec run 'fn main()->int{return 42;}' # 解释器执行 + +python3 tests/bootstrap/test_pipeline.py # Python bootstrap 管线测试 +python3 tests/selfhost/test_compile.py # 自举编译器测试 +# tests/suite/*.cr 为集成测试:./build/corec build FILE.cr -o OUT --static && ./OUT +``` + +CI 与本地跑同一套命令(`src/ci/run.sh`,按 `CI_JOB_NAME` 分发)。 + +## 编码约定 + +- 全部数组为动态字节缓冲(`string` + grow 函数),无 `MAX_*` 上限 +- 扁平 AST / 扁平 IR(每节点为 `{kind, a, b, c, ...}` 结构) +- 每个目录的 `_import.cr` 集中管理共享导入 +- 关键字唯一真源:`src/compiler/lexer.cr` +- 文档(`docs/`)更新与实现同步;伪代码文档(`docs/pseudocode/`)由源码生成,改源码后须重跑 `tools/pseudocode_check.py` + +## 审查标准 + +- 不绕过问题(root cause 直修) +- 语义保鲜:IR 全程保留类型/语义信息 +- 惰性/数据流优化不改变程序输出 +- 测试随变更更新 diff --git a/.github/SECURITY.md b/.github/SECURITY.md new file mode 100644 index 0000000..9ec0175 --- /dev/null +++ b/.github/SECURITY.md @@ -0,0 +1,15 @@ +# 安全策略 + +## 报告漏洞 + +请通过 GitHub 的 **私有漏洞报告**(仓库页 → Security → Report a vulnerability)提交, +不要公开披露。 + +## 响应 + +维护者会在收到报告后尽快响应。修复后通过正常 PR 流程合入,按需发布安全说明。 + +## 范围 + +编译器本身(`src/compiler/`)、运行时(`src/runtime/`)、生成代码的正确性。 +生成代码/编译器的安全问题按严重程度处理。 diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md new file mode 100644 index 0000000..267e836 --- /dev/null +++ b/.github/pull_request_template.md @@ -0,0 +1,17 @@ +## 变更描述 + + + +## 测试 + + + +- [ ] 本地测试通过 + +## 语义保鲜影响 + + + +## 已知限制 / 后续 + + diff --git a/.github/workflows/core-ci.yml b/.github/workflows/core-ci.yml new file mode 100644 index 0000000..15f6175 --- /dev/null +++ b/.github/workflows/core-ci.yml @@ -0,0 +1,62 @@ +# Core 主 CI——结构与 rust-lang/rust 的 ci.yml 同构(模板源 ~/rust),按 Core 裁剪。 +# 触发分层(merge_group 暂缺:merge_queue 因免费计划降级不可用,且 merge_group 事件 +# 的工作流只能在默认分支注册——待计划升级后恢复 merge_group + suite/full-bootstrap): +# - pull_request(PR 快速层):check / bootstrap-tests / selfhost-tests +# - (恢复时)merge_group(完整层):suite / full-bootstrap +# PR 层 job 在合并时也需通过(Rust 语义:PR CI jobs 自动注册为 auto jobs)。 +# job 命令定义在 src/ci/run.sh(case CI_JOB_NAME 分发),本地用 run.sh 可复现。 + +name: CI +on: + pull_request: + branches: + - "**" + +permissions: + contents: read + +defaults: + run: + shell: bash + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + job: + name: ${{ matrix.name }} + runs-on: ubuntu-latest + timeout-minutes: 120 + # run_type: pr = PR 快速层;full = 完整层(仅 merge_group 触发——当前休眠)。 + if: ${{ matrix.run_type == 'pr' || github.event_name == 'merge_group' }} + env: + CI_JOB_NAME: ${{ matrix.name }} + strategy: + fail-fast: false + matrix: + include: + - name: check + run_type: pr + - name: bootstrap-tests + run_type: pr + - name: selfhost-tests + run_type: pr + - name: suite + run_type: full + - name: full-bootstrap + run_type: full + # opt-regress(O0/O1 自举回归)留位,按 TODO 逐步点亮: + # - name: opt-regress + # run_type: full + steps: + - name: checkout the source code + uses: actions/checkout@v5 + with: + fetch-depth: 2 + + - name: add extra environment variables + run: src/ci/scripts/setup-environment.sh + + - name: run the build + run: src/ci/scripts/run-build-from-ci.sh diff --git a/.github/workflows/opencode.yml b/.github/workflows/opencode.yml deleted file mode 100644 index 2bede61..0000000 --- a/.github/workflows/opencode.yml +++ /dev/null @@ -1,33 +0,0 @@ -name: opencode - -on: - issue_comment: - types: [created] - pull_request_review_comment: - types: [created] - -jobs: - opencode: - if: | - contains(github.event.comment.body, ' /oc') || - startsWith(github.event.comment.body, '/oc') || - contains(github.event.comment.body, ' /opencode') || - startsWith(github.event.comment.body, '/opencode') - runs-on: ubuntu-latest - permissions: - id-token: write - contents: read - pull-requests: read - issues: read - steps: - - name: Checkout repository - uses: actions/checkout@v6 - with: - persist-credentials: false - - - name: Run opencode - uses: anomalyco/opencode/github@latest - env: - DEEPSEEK_API_KEY: ${{ secrets.DEEPSEEK_API_KEY }} - with: - model: deepseek/deepseek-v4-flash \ No newline at end of file diff --git a/.gitignore b/.gitignore index 6c52d3d..3d05b4c 100644 --- a/.gitignore +++ b/.gitignore @@ -30,3 +30,4 @@ a.out *.ccr *.cir a.out +.superpowers/ diff --git a/.opencode/opencode.json b/.opencode/opencode.json deleted file mode 100644 index a5c196e..0000000 --- a/.opencode/opencode.json +++ /dev/null @@ -1,6 +0,0 @@ -{ - "$schema": "https://opencode.ai/config.json", - "plugin": [ - "openslimedit@latest" - ] -} \ No newline at end of file diff --git a/CLAUDE.md b/CLAUDE.md index 7de3e99..8fafdd9 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -23,6 +23,35 @@ There are two compilers: - **Python bootstrap** (`bootstrap/corec/`) — the initial compiler, written in Python, used to build the self-hosted compiler - **Self-hosted compiler** (`src/compiler/`) — the Core compiler written in Core itself, built by the Python bootstrap +## 版本控制流程(GitFlow) + +- 全面使用 `jj`(铁律 #2,hook 机械拦截 git)。分支模型:feature → develop → main +- **main = 正式版线**:仅维护者 DslsDZC 可合入(ruleset:update 规则 + 无管理员绕过) +- **develop = 集成分支**:日常 PR 目标(ruleset:PR 通道 + 审批 + merge queue + CI 门槛) +- 日常开发(feature → develop): + +```bash +jj bookmark create feature/xxx # 每个改动独立分支(base = develop) +# ...开发提交(SSH 自动签名)... +jj git push -b feature/xxx +gh pr create --base develop --fill # PR 指向 develop("不能指向 main") +# → 审查(审批+CI 绿)→ **手动 squash 合入 develop**(merge queue 因免费计划降级,见 spec §3.3) +jj git fetch && jj bookmark move develop -r develop@origin +``` + +- 发布(develop → main,仅维护者): + +```bash +jj git push -b develop +gh pr create --base main --fill # required reviewers = 你 → 你批准 → 手动 squash 合入 +``` + +- 合入 main 后(发布线): + +```bash +jj git fetch && jj bookmark move main -r main@origin +``` + ## Build & Test Commands ```bash diff --git a/docs/superpowers/plans/2026-08-09-repo-governance.md b/docs/superpowers/plans/2026-08-09-repo-governance.md new file mode 100644 index 0000000..f7d833e --- /dev/null +++ b/docs/superpowers/plans/2026-08-09-repo-governance.md @@ -0,0 +1,525 @@ +# 仓库治理落地 Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** 将已批准的仓库治理设计(spec `docs/superpowers/specs/2026-08-09-repo-governance-design.md`)落地:本地 jj 保护/签名/hook、develop 集成分支、GitHub 双 ruleset、签名密钥注册、端到端验证。 + +**Architecture:** GitFlow(feature → develop → main,main 仅维护者合入)。GitHub 侧用 ruleset(main/develop 两个)+ merge queue;本地侧用 jj 配置(bookmark protect、SSH 签名)+ Claude Code PreToolUse hook(铁律 #2 机械执行)。CI 已实现(上阶段完成),本计划将其 job 名接入 ruleset 状态检查。 + +**Tech Stack:** jj 0.44(colocated)、Claude Code hooks、gh CLI / GitHub Rulesets REST API、GitHub Web UI、GitFlow 分支模型。 + +## Global Constraints + +- **版本控制:全面 jj,禁止 git**(CLAUDE.md 铁律 #2;Task 3 落地 hook 后机械拦截。本计划内所有"提交"步骤一律 `jj describe`/`jj git push`,写 `git` 命令即违规) +- **编译限速**(铁律 #6):本计划无长时间编译任务;若验证步骤意外触发构建,加 `cpulimit -l 10` 或 `nice -n 19` +- **ruleset 目标(spec §3.1 M1-M7 / §3.2 D1-D11)**:main 仅维护者可更新(update 规则 + bypass_actors 不含 Admin)、禁强推、禁删、PR 门槛(≥1 审批 + 对话解决 + stale 作废)、签名提交、无管理员绕过、protected tags `release/*`;develop:PR 唯一通道、审批限维护者、merge queue(SQUASH)、CI 状态检查(CI / check、CI / bootstrap-tests、CI / selfhost-tests)、squash only + 自动删分支、核心路径保护(src/compiler/**、src/arch/**) +- **过渡**:两个 ruleset 先 `enforcement: evaluate`,验证无干扰后转 `active` +- **签名**:`signing.backend=ssh`、`signing.key=~/.ssh/id_ed25519.pub`、`signing.sign-all=true`;GitHub 侧公钥须注册为 **Signing key**(Task 8) +- **PR 一律 base=develop**(CONTRIBUTING 已写入);develop→main 合入仅 DslsDZC +- **已知风险(不阻塞本计划)**:CI full-bootstrap job 撞 corec2 自举阻塞项(TODO),点亮属后续项 + +--- + +### Task 1: jj bookmark protect(本地防手滑) + +**Files:** 无(jj repo 配置) + +**Interfaces:** +- Produces: `bookmarks.main.protect = true`(repo 级配置)——Task 9 验证依赖 + +- [ ] **Step 1: 设置保护** + +```bash +jj config set --repo bookmarks.main.protect true +``` + +- [ ] **Step 2: 验证配置生效** + +```bash +jj config get bookmarks.main.protect +``` +Expected: `true` + +- [ ] **Step 3: 验证行为(rebase 不能挪动 main)** + +```bash +# main 已被保护:对 main 做 rewrite 操作会被拒绝 +jj rebase -r 'main' -A main 2>&1 || echo "REJECTED as expected" +``` +Expected: 命令报错(protected bookmark 不能隐式移动)或 `REJECTED as expected`。若意外成功则回退(`jj undo`)并检查 `bookmarks.main.protect` 值。 + +- [ ] **Step 4: 提交(jj)** + +```bash +jj describe -m "chore(governance): jj main bookmark 保护" +``` + +### Task 2: jj SSH 提交签名 + +**Files:** 无(jj user 配置) + +**Interfaces:** +- Produces: `signing.backend=ssh`、`signing.key=~/.ssh/id_ed25519.pub`、`signing.sign-all=true`——Task 3 的提交即首个签名提交(在 Task 3 Step 4 验证签名) + +- [ ] **Step 1: 配置签名** + +```bash +jj config set --user signing.backend ssh +jj config set --user signing.key /home/DslsDZC/.ssh/id_ed25519.pub +jj config set --user signing.sign-all true +``` + +- [ ] **Step 2: 验证配置** + +```bash +jj config get signing.backend # Expected: ssh +jj config get signing.key # Expected: /home/DslsDZC/.ssh/id_ed25519.pub +jj config get signing.sign-all # Expected: true +``` + +- [ ] **Step 3: 确认公钥存在** + +```bash +ls -la /home/DslsDZC/.ssh/id_ed25519.pub # Expected: 文件存在 +``` + +- [ ] **Step 4: 提交(jj)** + +```bash +jj describe -m "chore(governance): jj SSH 提交签名(sign-all)" +``` + +### Task 3: git 硬拦截 hook(铁律 #2 机械执行) + +**Files:** +- Create: `.claude/hooks/block-git.py` +- Create: `.claude/settings.json` + +**Interfaces:** +- Produces: `.claude/settings.json` 的 PreToolUse hook——Task 4 依赖(settings.local.json 清理后权限模型一致);Task 9 验证 + +- [ ] **Step 1: 写 hook 脚本** + +Create `.claude/hooks/block-git.py`: + +```python +#!/usr/bin/env python3 +"""铁律 #2 机械执行:Bash 命令以 git 开头 → 拒绝执行(exit 2)。""" +import json +import sys + +data = json.load(sys.stdin) +cmd = data.get("tool_input", {}).get("command", "") +stripped = cmd.strip() + +if stripped == "git" or stripped.startswith("git "): + sys.stderr.write( + "铁律 #2:全面使用 jj,禁止 git。\n" + "改用 jj 命令:jj status / jj log / jj describe / jj git push / jj bookmark ...\n" + ) + sys.exit(2) # PreToolUse exit 2 = block the tool call +sys.exit(0) +``` + +- [ ] **Step 2: 写 settings.json(提交入库)** + +Create `.claude/settings.json`: + +```json +{ + "hooks": { + "PreToolUse": [ + { + "matcher": "Bash", + "hooks": [ + { + "type": "command", + "command": "python3 .claude/hooks/block-git.py" + } + ] + } + ] + } +} +``` + +- [ ] **Step 3: 验证 hook 脚本逻辑(直接喂 JSON)** + +```bash +# git 命令 → 应被拒绝(exit 2) +echo '{"tool_input": {"command": "git status"}}' | python3 .claude/hooks/block-git.py; echo "exit=$?" +# jj 命令 → 应放行(exit 0) +echo '{"tool_input": {"command": "jj status"}}' | python3 .claude/hooks/block-git.py; echo "exit=$?" +``` +Expected: 第一次 `exit=2` 且 stderr 有铁律提示;第二次 `exit=0`。 + +- [ ] **Step 4: 验证签名生效(本提交是 sign-all 后的首个提交)** + +```bash +jj describe -m "feat(governance): 铁律 #2 git 拦截 hook(.claude/settings.json)" +jj log -r @ --no-graph -T 'signature.format()' +``` +Expected: describe 成功后,签名模板输出非空(SSH 签名信息)。若为空,检查 Task 2 配置与 `jj sign --help`。 + +- [ ] **Step 5: 验证 hook 在会话内拦截** + +在 Claude Code 会话中执行 `git status`(作为测试): +Expected: 工具调用被 PreToolUse hook 阻断,反馈显示"铁律 #2:全面使用 jj,禁止 git"。 + +### Task 4: settings.local.json 清理(移除 git 允许项) + +**Files:** +- Modify: `.claude/settings.local.json`(移除 `"Bash(git *)",` 一行) + +**Interfaces:** +- Consumes: Task 3 的 hook(拦截已生效) +- Produces: 权限模型与 hook 一致——Task 9 验证 + +- [ ] **Step 1: 移除允许项** + +编辑 `.claude/settings.local.json`,删除 permissions.allow 数组中的这一行: + +```json + "Bash(git *)", +``` + +- [ ] **Step 2: 验证无残留** + +```bash +grep -n 'Bash(git' .claude/settings.local.json; echo "exit=$?" +``` +Expected: 无输出(grep 找不到),exit=1。 + +- [ ] **Step 3: 验证 JSON 仍合法** + +```bash +python3 -c "import json; json.load(open('.claude/settings.local.json')); print('JSON OK')" +``` +Expected: `JSON OK` + +- [ ] **Step 4: 提交(jj)** + +```bash +jj describe -m "chore(governance): settings.local.json 移除 Bash(git *) 允许项" +``` + +### Task 5: CLAUDE.md 版本控制流程段 + +**Files:** +- Modify: `CLAUDE.md`(在"Build & Test Commands"之前插入新段) + +**Interfaces:** +- Produces: CLAUDE.md 的"版本控制流程"段——Task 9 核对文档与机制一致 + +- [ ] **Step 1: 插入流程段** + +在 `CLAUDE.md` 的 `## Build & Test Commands` 之前插入: + +```markdown +## 版本控制流程(GitFlow) + +- 全面使用 `jj`(铁律 #2,hook 机械拦截 git)。分支模型:feature → develop → main +- **main = 正式版线**:仅维护者 DslsDZC 可合入(ruleset:update 规则 + 无管理员绕过) +- **develop = 集成分支**:日常 PR 目标(ruleset:PR 通道 + 审批 + merge queue + CI 门槛) +- 日常开发(feature → develop): + +```bash +jj bookmark create feature/xxx # 每个改动独立分支(base = develop) +# ...开发提交(SSH 自动签名)... +jj git push -b feature/xxx +gh pr create --base develop --fill # PR 指向 develop("不能指向 main") +# → 审查 → merge queue → squash 合入 develop → 自动删源分支 +jj git fetch && jj bookmark move develop -r develop@origin +``` + +- 发布(develop → main,仅维护者): + +```bash +jj git push -b develop +gh pr create --base main --fill # required reviewers = 你 → 你批准 → queue 合入 +``` + +- 合入 main 后(发布线): + +```bash +jj git fetch && jj bookmark move main -r main@origin +``` +``` + +- [ ] **Step 2: 验证插入** + +```bash +grep -n "版本控制流程\|develop = 集成分支" CLAUDE.md +``` +Expected: 两行都在,位置在 Build & Test Commands 之前。 + +- [ ] **Step 3: 提交(jj)** + +```bash +jj describe -m "docs: CLAUDE.md 版本控制流程段(GitFlow 工作流命令)" +``` + +### Task 6: 创建并推送 develop 集成分支 + +**Files:** 无(分支操作) + +**Interfaces:** +- Produces: `develop` bookmark(本地 + origin@)——Task 7 的 develop ruleset 目标、Task 9 验证 + +- [ ] **Step 1: 本地创建 develop(从远端 main 派生)** + +```bash +jj bookmark create develop -r 'main@origin' +``` + +- [ ] **Step 2: 推送 develop 到 origin** + +```bash +jj git push -b develop +``` +Expected: `bookmark: develop [add to ]` + +- [ ] **Step 3: 验证** + +```bash +jj bookmark list develop +jj log -r develop@origin --no-graph -T 'commit_id.short()' +``` +Expected: develop@origin 存在,指向与 main 相同的提交。 + +- [ ] **Step 4: 提交说明(jj)** + +```bash +jj describe -m "chore(governance): 创建 develop 集成分支(GitFlow)" +``` + +### Task 7: GitHub ruleset 配置(main + develop) + +**Files:** +- Create: `tools/gh_setup_ruleset.sh`(内含两个 ruleset 的 JSON 载荷) + +**Interfaces:** +- Consumes: Task 6 的 develop 分支(ruleset 目标存在);CI job 名(.github/workflows/ci.yml:`CI / check`、`CI / bootstrap-tests`、`CI / selfhost-tests`) +- Produces: 两个 ruleset(evaluate 模式)——Task 9 验证 + +- [ ] **Step 1: 写配置脚本** + +Create `tools/gh_setup_ruleset.sh`: + +(2026-08-09 落地后注:内嵌脚本为初版——最终以 tools/gh_setup_ruleset.sh 为准:active 替代 evaluate、merge_queue 已移除、字段名修正,偏差详见 spec §3.3) + +```bash +#!/bin/bash +# 仓库治理 ruleset 配置脚本(spec §3 清单落地,路径 A) +# 用法:gh auth refresh 后运行本脚本;或按脚本内 JSON 在网页版手动配置(路径 B) +# API 事实:restrict-pushes = update 规则 + bypass_actors(不含 Admin 角色=关闭管理员绕过); +# required_reviewers 为 pull_request 规则的 beta 参数(Team 型)——个人用户用 +# bypass_actors 空集 + 权限模型(仅 DslsDZC 有写权限)实现。 +set -euo pipefail +REPO="dslsdzc/core" + +main_ruleset() { +cat <<'JSON' +{ + "name": "main-only-maintainer", + "target": "branch", + "enforcement": "evaluate", + "conditions": {"ref_name": {"include": ["refs/heads/main"], "exclude": []}}, + "bypass_actors": [], + "rules": [ + {"type": "update", "parameters": {"update_allows_fetch_and_merge": false}}, + {"type": "pull_request", "parameters": { + "required_approving_review_count": 1, + "dismiss_stale_reviews_on_push": true, + "require_last_push_approval": false, + "required_review_thread_resolution": true + }}, + {"type": "required_signatures"}, + {"type": "non_fast_forward"}, + {"type": "deletion"} + ] +} +JSON +} + +develop_ruleset() { +cat <<'JSON' +{ + "name": "develop-integration", + "target": "branch", + "enforcement": "evaluate", + "conditions": {"ref_name": {"include": ["refs/heads/develop"], "exclude": []}}, + "bypass_actors": [], + "rules": [ + {"type": "pull_request", "parameters": { + "required_approving_review_count": 1, + "dismiss_stale_reviews_on_push": true, + "require_last_push_approval": false, + "required_review_thread_resolution": true + }}, + {"type": "required_status_checks", "parameters": { + "checks": [ + {"context": "CI / check"}, + {"context": "CI / bootstrap-tests"}, + {"context": "CI / selfhost-tests"} + ], + "strict_required_status_checks_policy": true + }}, + {"type": "merge_queue", "parameters": { + "check_response_timeout_minutes": 60, + "grouping_strategy": "ALLGREEN", + "max_entries_to_build": 5, + "max_entries_to_merge": 2, + "merge_method": "SQUASH", + "min_entries_to_merge": 1, + "min_entries_to_merge_wait_minutes": 1 + }}, + {"type": "non_fast_forward"}, + {"type": "deletion"} + ] +} +JSON +} + +main_ruleset > /tmp/main_ruleset.json +develop_ruleset > /tmp/develop_ruleset.json +echo "== main ruleset payload ==" +cat /tmp/main_ruleset.json +echo "== develop ruleset payload ==" +cat /tmp/develop_ruleset.json + +if command -v gh >/dev/null && gh auth status >/dev/null 2>&1; then + gh api -X POST "repos/${REPO}/rulesets" --input /tmp/main_ruleset.json + gh api -X POST "repos/${REPO}/rulesets" --input /tmp/develop_ruleset.json + echo "== 已创建 rulesets ==" + gh api "repos/${REPO}/rulesets" --jq '.[] | {name, enforcement}' +else + echo "gh 不可用:请按上方 JSON 在网页版 Settings → Rules → Rulesets 手动创建(路径 B)" +fi +``` + +- [ ] **Step 2: 验证脚本语法** + +```bash +bash -n tools/gh_setup_ruleset.sh && echo "syntax OK" +``` +Expected: `syntax OK` + +- [ ] **Step 3: 验证 JSON 载荷合法** + +```bash +bash tools/gh_setup_ruleset.sh 2>&1 | grep -A5 "payload" ; python3 -c "import json; [json.load(open(p)) for p in ['/tmp/main_ruleset.json','/tmp/develop_ruleset.json']]; print('JSON OK')" +``` +Expected: `JSON OK`(gh 不可用时会打印路径 B 提示——正常,此环境 gh 故障) + +- [ ] **Step 4: 提交(jj)** + +```bash +jj describe -m "feat(governance): ruleset 配置脚本(main/develop,evaluate 模式,双路径)" +``` + +- [ ] **Step 5: 落地(二选一,gh 恢复后走 A,否则走 B)** + +路径 A(gh 恢复后): +```bash +gh auth refresh -h github.com +bash tools/gh_setup_ruleset.sh +``` +Expected: 创建成功,`gh api repos/dslsdzc/core/rulesets --jq '.[] | {name, enforcement}'` 显示两个 ruleset(evaluate)。 + +路径 B(gh 故障期,网页版)——按 spec §3.1/§3.2 清单 + 本脚本 JSON 在 Settings → Rules → Rulesets 创建: +1. New ruleset → 名称 `main-only-maintainer` → Target: `main`(默认分支) +2. Enforcement: **Evaluate**(先试运行) +3. Rules: Block force pushes / Restrict deletions / Require a pull request before merging(1 approval、Dismiss stale approvals、Require conversation resolution) +4. Require signed commits;Rules 列表确认 **Restrict pushes** 生效且 **Repository admin 不在 bypass 列表**("Enforce for admins") +5. 保存;重复创建 `develop-integration`(Target: develop): + - Require a pull request before merging(1 approval、stale 作废、对话解决) + - Require status checks:勾选 CI / check、CI / bootstrap-tests、CI / selfhost-tests(若 PR CI 尚未跑过则稍后回填) + - Require merge queue(squash merge、60min 超时) + - Block force pushes / Restrict deletions +6. 核对第 3.3 节机制限制(无"禁止 PR 指向 main"开关——规则兜底已由审批限制实现) + +- [ ] **Step 6: 验证 ruleset 已存在** + +```bash +gh api "repos/dslsdzc/core/rulesets" --jq '.[] | {name, enforcement, target}' 2>&1 || echo "gh 不可用——网页版确认两个 ruleset 存在" +``` +Expected: `main-only-maintainer`(evaluate)+ `develop-integration`(evaluate)或网页版可见。 + +- [ ] **Step 7: 观察 evaluate 期告警(至少一个 PR 周期)** + +对照 spec §8:evaluate 模式下 GitHub 会报告"本可拦截的事件"——确认无意外误报后转 active(网页版 Edit → Enforcement: Active)。转 active 前完成 Task 8(签名密钥),否则未签名提交会被真实拦截。 + +### Task 8: GitHub SSH 签名密钥注册(网页版,用户执行) + +**Files:** 无(GitHub 设置) + +**Interfaces:** +- Consumes: Task 2 的 `~/.ssh/id_ed25519.pub` +- Produces: 签名校验通过的前提——Task 9 验证 + +- [ ] **Step 1: 网页版注册 Signing key** + +操作路径(gh 故障期,必须手动): +1. GitHub → Settings → **SSH and GPG keys** +2. **New SSH key** → Key type: **Signing Key**(不是 Authentication) +3. Title: `core-signing`;Key 内容:`cat /home/DslsDZC/.ssh/id_ed25519.pub` 的输出(全粘贴) +4. Add SSH key + +- [ ] **Step 2: 验证签名可被 GitHub 识别** + +推送一个已签名提交(如 Task 3-7 的任一提交)到 feature 分支后,在 PR 页或 Commits 页查看提交: +Expected: 显示 **Verified** 徽标。若显示 "Unverified",检查 Key type 是否误选为 Authentication Key,重新注册。 + +### Task 9: 端到端验证(spec §8 清单执行) + +**Files:** 无(验证) + +**Interfaces:** +- Consumes: Task 1-8 全部产物 + +- [ ] **Step 1: 本地安全网验证** + +```bash +jj config get bookmarks.main.protect # true +jj config get signing.sign-all # true +# hook 拦截(喂 JSON 模拟) +echo '{"tool_input": {"command": "git log"}}' | python3 .claude/hooks/block-git.py; echo "exit=$?" # exit=2 +grep -c 'Bash(git' .claude/settings.local.json # 0 +grep -n "版本控制流程" CLAUDE.md # 存在 +jj log -r @ --no-graph -T 'signature.format()' # 非空(最新提交已签名) +``` + +- [ ] **Step 2: 分支与 ruleset 验证** + +```bash +jj bookmark list develop # develop@origin 存在 +jj log -r main@origin --no-graph -T 'commit_id.short()' && jj log -r develop@origin --no-graph -T 'commit_id.short()' # develop 与 main 同点 +``` +网页版核对(ruleset active 后): +- [ ] 直推 main 被拒(403)——仅 DslsDZC 且绕过关闭 +- [ ] 指向 main 的 PR(非你创建)无法被批准合入 +- [ ] develop→main 合并只有你执行成功 +- [ ] RhineIris fork PR:base=develop,你审批后合入 develop +- [ ] PR 层 CI 绿(CI / check、CI / bootstrap-tests、CI / selfhost-tests) +- [ ] merge queue:审批过 + CI 绿 → 自动 squash 合入 develop → 源分支自动删除 + +- [ ] **Step 3: 首个治理 PR** + +本 feature 分支 `feature/repo-governance` 即首个 PR: +1. 网页版 https://github.com/dslsdzc/core/pull/new/feature/repo-governance → base 选 **develop**(若 develop 尚未建则先建) +2. 按 PR 模板填写(变更描述/测试/语义保鲜影响) +3. 合并:你批准 → merge queue → squash 合入 develop +4. 之后按 §7 工作流执行一次完整的 feature → develop 流程,再执行一次 develop → main + +- [ ] **Step 4: 收尾核对 spec §12 状态清单** + +全部 ⬜ 项变为 ✅(本地配置、develop、ruleset、签名密钥、首个 PR)。剩余 ⬜(CI 完整层点亮、opt-regress)属后续项,在 spec §11 跟踪。 + +--- + +## Self-Review 记录 + +- **Spec 覆盖**:§3.1 M1-M7 → Task 7(main ruleset:update 规则= M1、非强推= M2、deletion= M3、pull_request 门槛= M4、required_signatures= M5、bypass_actors 空集= M6、protected tags 在网页版规则项= M7——M7 为 tag ruleset,脚本未含,已列入网页版 Step 5 核对);§3.2 D1-D11 → Task 7(pull_request= D1/D3/D4/D5、required_status_checks= D6/D10、merge_queue= D8、squash+删分支= D9、D2= non_fast_forward、D7 文件路径限制为 ruleset 扩展规则(file_path_restriction),脚本未含——列入网页版核对项;D11= bypass_actors 空集);§4 双路径 → Task 7 Step 5;§6 本地配置 → Task 1/2/3/4/5;§7 工作流 → Task 5/9;§8 验证清单 → Task 9;§9 四件套已随 spec 首 PR 提交(非本计划任务);§10 发布规范 → 后续(非本计划)。 +- **占位符扫描**:无 TBD/TODO;网页版核对项均给出精确勾选内容与 JSON 对照。 +- **类型一致性**:CI job 名(CI / check 等)与 .github/workflows/ci.yml 的 job name 一致;signing 配置项名与 jj 0.44 实测一致(`config set --user/--repo`、`config get ` 已实测)。 diff --git a/docs/superpowers/specs/2026-08-09-repo-governance-design.md b/docs/superpowers/specs/2026-08-09-repo-governance-design.md new file mode 100644 index 0000000..591bfee --- /dev/null +++ b/docs/superpowers/specs/2026-08-09-repo-governance-design.md @@ -0,0 +1,160 @@ +# 仓库治理与分支保护设计 + +日期:2026-08-09 +状态:设计已批准(brainstorming 会话,分节确认);CI 部分已实现,其余待落地 + +## 1. 概述 + +Core 的愿景是成为严肃系统语言(语义保鲜、内核路线、形式验证)——开发流程按**最终形态**立规,执行按**现状规模**宽松。治理模型参考 Rust/Linux:main 即 mainline,**任何人(含维护者)不得直推**,全部改动经 PR + 审查 + 合入门槛进入 main。 + +| 事实 | 值 | +|---|---| +| 维护者(唯一写权限) | DslsDZC(你) | +| 贡献者 | RhineIris——fork + PR 模式,无写权限,feature 分支在其 fork 上 | +| 仓库形态 | jj colocated(.git 存在,git 命令物理可用) | +| 合并历史 | 直推 main 为主,偶发 PR 合并 | + +## 2. 治理模型 + +- **GitFlow 标准**:`main` = 正式版线(仅正式版内容,对应 semver 发布);`develop` = 集成分支(日常 PR 目标);feature → develop 走 PR(审查 + CI + merge queue);**develop → main 的合入只有维护者(DslsDZC)能做**(GitFlow 的发布负责人语义) +- **非对称**:唯一实际审查 = 你对 RhineIris PR 的单向把关;你的改动走 PR 但自批兜底 +- **愿景结构 + 现状执行**:规则按最终形态全立(将来贡献者增多规则自动生效);执行上互审约定优先、自批兜底(GitHub 无原生"非作者审批"开关,工具层面拦不住作者自批——此为已知限制,流程约定补充) +- **机制限制(如实记录)**:GitHub 无原生"禁止以 main 为 base 创建 PR"开关——"PR 不能指向 main"由 **main 规则组合强制**(restrict pushes 仅 DslsDZC + required reviewers 仅 DslsDZC:指向 main 的 PR 无维护者批准无法合入)+ CONTRIBUTING 约定(PR 一律指向 develop)实现 +- **铁律机械执行**:CLAUDE.md 第 2 条(禁止 git、全面 jj)用 hook 硬拦截 + +## 3. GitHub 侧:ruleset 最终清单(main / develop 两个 ruleset) + +### 3.1 main ruleset(目标:main)——只有维护者能触碰 + +| # | 规则 | 配置 | +|---|---|---| +| M1 | 推送限定 | Restrict pushes:**仅 DslsDZC**——物理上只有维护者能向 main 推送/合入(develop→main 合并只能由你执行) | +| M2 | 禁强推 | Block force pushes | +| M3 | 禁删分支 | Block deletions | +| M4 | 合入门槛 | Require a pull request before merging + **required reviewers 仅 DslsDZC** + ≥1 approval——任何指向 main 的 PR(含 RhineIris、未来协作者)**无维护者批准无法合入** | +| M5 | 强制签名提交 | Require signed commits(SSH 签名;GitHub 合并产生的 squash 提交自带 GitHub 签名,自动通过) | +| M6 | 管理员无绕过 | 规则对仓库管理员同样生效(关闭 admin bypass——否则 M1 形同虚设) | +| M7 | Protected tags | `release/*` 标签禁强推、禁删除 | + +### 3.2 develop ruleset(目标:develop 集成分支)——日常开发入口 + +| # | 规则 | 配置 | +|---|---|---| +| D1 | 禁直推 | Require a pull request before merging(PR 是唯一合入通道) | +| D2 | 禁强推 | Block force pushes | +| D3 | 强制审批 | Require 1 approval + required reviewers 仅 DslsDZC(合入 develop 亦须维护者批准,队列自动执行合并) | +| D4 | 过时审批作废 | Dismiss stale pull request approvals when new commits are pushed | +| D5 | 对话必须解决 | Require conversation resolution before merging | +| D6 | 合并前必须更新分支 | Require branches to be up to date(merge queue 下由队列保证,双保险) | +| D7 | 文件路径限制 | 核心路径 `src/compiler/**`、`src/arch/**` 变更需审批(防御性双保险) | +| D8 | merge queue | Require merge queue(bors 对应物);入口 = 审批过 + PR 层 CI 绿 | +| D9 | 合并策略 | Allow squash merges only + 自动删除已合并源分支 | +| D10 | 状态检查 | PR 层 CI job 名(check / bootstrap-tests / selfhost-tests)——CI 已实现(见第 5 节),配置时直接填入 | +| D11 | 管理员无绕过 | 规则对仓库管理员同样生效 | + +### 3.3 机制限制与过渡 + +- **GitHub 无原生"禁止以 main 为 base 创建 PR"开关**:M4(required reviewers 仅 DslsDZC)使指向 main 的 PR 无法被非你合入——"PR 不能指向 main"以规则兜底 + CONTRIBUTING 约定(PR 一律指向 develop)实现 +- **落地过渡**:两个 ruleset 先以 **evaluate(试运行)模式**启用,观察确认无干扰后转 active +- **2026-08-09 落地偏差(免费计划限制,已实测)**: + - `enforcement: evaluate` 仅 Enterprise 可用——免费计划已直接以 **active** 创建(无试运行期,规则即刻生效) + - `merge_queue` 规则被 API 拒绝("Invalid rule 'merge_queue'" 空原因)——**降级为手动合入**:审批 + CI 状态检查门槛保留(D1/D3/D8 的自动化串行部分由人工点击合入替代) + - pull_request 参数 schema 实测:5 个必填布尔(含 `require_code_owner_review`)、`allowed_merge_methods: ["squash"]` 强制 squash-only + - `required_status_checks` 参数数组字段名是 `required_status_checks`(非 `checks`) + - M7(release/* 标签保护)与 D7(文件路径限制)未落地:脚本与已建 ruleset 均未含(免费计划可用但暂缓),列入后续项 + +## 4. GitHub 侧:落地方式 + +- **路径 A(gh 恢复后)**:`tools/gh_setup_ruleset.sh`——`gh api` 按上述清单创建 ruleset(脚本内嵌规则 JSON) +- **路径 B(现在可用)**:网页版 Settings → Rules → Rulesets,按第 3 节清单逐项配置 +- **前置**:SSH 签名密钥(`~/.ssh/id_ed25519.pub`)在 GitHub Settings → SSH keys 注册为 **Signing key**(仅注册为认证 key 则签名校验失败) + +## 5. CI(已实现,2026-08-09) + +照 rust-lang/rust 模板(`~/rust`)重写,已本地验证: + +``` +.github/workflows/ci.yml ← 矩阵 job + 双层触发 +src/ci/run.sh ← job 分发器(本地复现入口) +src/ci/shared.sh ← helper +src/ci/scripts/run-build-from-ci.sh ← GHA 入口 +src/ci/scripts/setup-environment.sh ← 环境转储 +``` + +- 双层触发:`pull_request`(PR 快速层:check / bootstrap-tests / selfhost-tests)+ `merge_group`(完整层:suite / full-bootstrap)——PR 层 job 在 merge 下也运行(Rust 的 PR-jobs-auto-register 语义) +- 砍掉:citool(静态矩阵内联)、全部 install-*.sh(Core 零工具链依赖)、docker/、artifacts +- 已知风险(如实标记):`full-bootstrap` 撞 corec2 tokenizer 死循环(TODO 自举阻塞项)+ 预存 bug 1(1GiB bump heap 峰值)——完整层按 TODO 逐个点亮;`opt-regress`(O0/O1 回归)留位 +- 本地验证:`CI_JOB_NAME=bootstrap-tests src/ci/run.sh` 端到端通过 + +## 6. 本地配置 + +| 项 | 命令/文件 | 效果 | +|---|---|---| +| jj bookmark 保护 | `jj config set --repository bookmarks.main.protect true` | main 不被 rebase/rewrite 意外挪动 | +| jj 提交签名 | `jj config set --user signing.backend ssh`、`signing.key ~/.ssh/id_ed25519.pub`、`signing.sign-all true` | 全部新提交 SSH 签名(满足规则 M5(强制签名提交)) | +| git 硬拦截 hook | `.claude/settings.json`(提交入库):PreToolUse 检测 Bash 命令以 `git` 开头 → 输出报错 + 非零退出 → 命令被拒绝 | 铁律 #2 机械执行 | +| settings.local.json 清理 | 移除 `Bash(git *)` 允许项 | 权限模型与 hook 一致 | +| CLAUDE.md | 新增"版本控制流程"段(下述命令序列) | 文档与机制一致 | + +## 7. 新工作流(你) + +``` +日常开发(feature → develop): +jj bookmark create feature/xxx # feature 分支(base = develop) +...开发提交(自动签名)... +jj git push -b feature/xxx +gh pr create --base develop --fill # PR 指向 develop("不能指向 main") +→ 审查(互审优先/自批兜底)→ 手动合入(审批过 + PR CI 绿) +→ squash 合入 develop + 自动删源分支 +jj git fetch && jj bookmark move develop -r develop@origin # 本地 develop 对齐 + +develop → main(只有你能): +jj git push -b develop # 你有写权限 +gh pr create --base main --fill # develop→main PR(required reviewers = 你) +→ 你批准 → 手动 squash 合入 main +``` + +## 8. 验证清单(合入后端到端) + +- [ ] 直推 main 被拒(403);推 feature 分支成功 +- [ ] 指向 main 的 PR(非你创建)无法被批准合入——required reviewers 仅 DslsDZC +- [ ] develop→main 合并只有你执行成功 +- [ ] 你的 feature PR:自批 → queue → squash 合入 develop → 源分支自动删除 +- [ ] RhineIris fork PR:base=develop,完整流程,你审批后合入 develop +- [ ] 未签名提交的 PR 被拒(签名规则生效);`jj log --no-graph -T 'signature'` 可见签名 +- [ ] 管理员账号直推 main 同样被拒(绕过已关闭) +- [ ] `git` 命令被 hook 硬拦截;`jj` 一切正常 +- [ ] jj main protect 生效(rebase 移不动 main) +- [ ] PR 层 CI 绿;完整层 job 状态如实标记 + +## 9. 社区协作基础设施(2026-08-09 补充) + +| 文件 | 内容 | +|---|---| +| `.github/pull_request_template.md` | PR 模板:变更描述 / 测试 / 语义保鲜影响 / 已知限制 | +| `.github/CONTRIBUTING.md` | 贡献指南:fork→PR→审查→queue 流程、铁律(禁 git)、构建测试命令、编码约定、审查标准 | +| `.github/SECURITY.md` | 漏洞报告路径(GitHub 私有漏洞报告)与响应承诺 | +| `.github/CODE_OF_CONDUCT.md` | 贡献者行为规范(Contributor Covenant 2.1 中文版,执行联系人 dsls.dzc@gmail.com) | + +## 10. 发布规范 + +- 版本号:**semver**(`MAJOR.MINOR.PATCH`) +- 标签:`release/vMAJOR.MINOR.PATCH`(对应 protected tags 规则 `release/*`) +- 发布流程:维护者从 main 打 tag → 标签保护防止强推/删除 +- changelog:按需维护(后续项) + +## 11. 后续项(明确延期) + +- Issue 模板(bug/特性请求)、标签体系——贡献者规模上来后补 +- Dependabot——**不做**(仓库零外部依赖) +- CI 优化:actions/cache 缓存 `build/corec`(多 job 共享构建产物);`full-bootstrap` 点亮(依赖自举阻塞项修复);`opt-regress`(O0/O1 回归)启用 +- 部署环境门禁(required deployment)——无发布流水线前不做 + +## 12. 当前状态 + +- ✅ CI 骨架:已实现(2026-08-09),本地验证通过,随首个 PR 上线 +- ✅ 社区四件套:PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写(2026-08-09),随本 spec 首 PR 上线 +- ⬜ 本地配置:jj protect / jj 签名 / hook / settings 清理 / CLAUDE.md——零网络依赖,待落地 +- ⬜ 创建 `develop` 集成分支(从 main 派生,作为日常 PR 目标) +- ✅ GitHub ruleset:**main-only-maintainer**(id 20601201)+ **develop-integration**(id 20601189)已创建并 active(2026-08-09);gh TLS 间歇性故障期间以重试创建成功;squash-only(allowed_merge_methods=['squash'])已应用于双 ruleset;delete_branch_on_merge=True 已设 +- ⬜ spec 提交与 PR 流程本身(本条 spec 将作为首个 PR 提交) diff --git a/src/ci/run.sh b/src/ci/run.sh new file mode 100755 index 0000000..e364228 --- /dev/null +++ b/src/ci/run.sh @@ -0,0 +1,79 @@ +#!/usr/bin/env bash + +# Core CI job 分发器——按 $CI_JOB_NAME 执行对应 job 的命令集。 +# 本地复现:CI_JOB_NAME=check src/ci/run.sh +# 注意:本地长时间编译请遵守 CLAUDE.md 铁律 6(cpulimit/nice 限速)。 +# +# 模板来源:rust-lang/rust src/ci/run.sh(configure/make 部分替换为 Core 构建命令)。 + +CI_JOB_NAME="${CI_JOB_NAME:-}" +set -euo pipefail +IFS=$'\n\t' + +if [ -n "$CI_JOB_NAME" ]; then + echo "[CI_JOB_NAME=$CI_JOB_NAME]" +fi + +ci_dir="$(cd "$(dirname "$0")" && pwd)" +source "$ci_dir/shared.sh" + +# 自举构建:Python bootstrap → 原生 corec/corearch +build_selfhost() { + python3 build_selfhost_native.py +} + +# src/compiler 全量语法检查(check 不触发 ELF 后端) +check_compiler_sources() { + for f in src/compiler/*.cr; do + echo "check $f" + ./build/corec check "$f" + done +} + +# 集成套件:每个 .cr 编译成 ELF 并运行,main 返回 0 为通过 +run_suite() { + for f in tests/suite/*.cr; do + echo "suite: $f" + ./build/corec build "$f" -o /tmp/core_suite_bin --static + /tmp/core_suite_bin + done +} + +case "$CI_JOB_NAME" in + check) + build_selfhost + check_compiler_sources + ;; + + bootstrap-tests) + python3 tests/bootstrap/test_pipeline.py + python3 tests/bootstrap/test_borrow.py + python3 tests/bootstrap/test_generics.py + ;; + + selfhost-tests) + python3 tests/selfhost/test_compile.py + python3 tests/selfhost/test_impl.py + python3 tests/selfhost/test_borrow.py + ;; + + suite) + build_selfhost + run_suite + ;; + + full-bootstrap) + # 三阶段自举验证(corec → corec2 → corec3)按 TODO 逐步点亮。 + # stage-2:用自举产物编译编译器自身(main.cr 经 imports 拉全编译器)。 + # 已知风险:corec2 tokenizer 死循环(TODO 自举阻塞项)+ 预存 bug 1 + # (1GiB bump heap 峰值)——CI 上可能失败/超时/OOM,点亮前如实标记。 + build_selfhost + ./build/corec build src/compiler/main.cr -o /tmp/corec2 --static + /tmp/corec2 --help + ;; + + *) + echo "error: unknown CI_JOB_NAME: $CI_JOB_NAME" >&2 + exit 1 + ;; +esac diff --git a/src/ci/scripts/run-build-from-ci.sh b/src/ci/scripts/run-build-from-ci.sh new file mode 100755 index 0000000..cad956f --- /dev/null +++ b/src/ci/scripts/run-build-from-ci.sh @@ -0,0 +1,20 @@ +#!/bin/bash +# Start the CI build. You shouldn't run this locally: call src/ci/run.sh instead. +# 模板来源:rust-lang/rust src/ci/scripts/run-build-from-ci.sh,按 Core 精简。 + +set -euo pipefail +IFS=$'\n\t' + +source "$(cd "$(dirname "$0")" && pwd)/../shared.sh" + +export CI="true" +export SRC=. + +echo "::group::CPU and Memory information" +if [ -f /proc/cpuinfo ]; then + grep -c processor /proc/cpuinfo | xargs echo "ncpus:" + grep MemTotal /proc/meminfo +fi +echo "::endgroup::" + +src/ci/run.sh diff --git a/src/ci/scripts/setup-environment.sh b/src/ci/scripts/setup-environment.sh new file mode 100755 index 0000000..b264d12 --- /dev/null +++ b/src/ci/scripts/setup-environment.sh @@ -0,0 +1,14 @@ +#!/bin/bash +# Dump the environment so job logs are self-describing (mirrors the intent of +# rust-lang/rust's setup-environment.sh, minus the EXTRA_VARIABLES plumbing — +# Core jobs don't need per-job env vars yet). +set -euo pipefail +IFS=$'\n\t' + +echo "::group::Environment" +echo "CI_JOB_NAME=${CI_JOB_NAME:-}" +echo "CI=${CI:-}" +echo "GITHUB_EVENT_NAME=${GITHUB_EVENT_NAME:-}" +echo "uname: $(uname -a)" +echo "python3: $(python3 --version 2>&1 || echo missing)" +echo "::endgroup::" diff --git a/src/ci/shared.sh b/src/ci/shared.sh new file mode 100644 index 0000000..c1c99de --- /dev/null +++ b/src/ci/shared.sh @@ -0,0 +1,34 @@ +#!/bin/false +# shellcheck shell=bash + +# This file is intended to be sourced with `. shared.sh` or +# `source shared.sh`, hence the invalid shebang and not being +# marked as an executable file in git. +# +# 模板来源:rust-lang/rust src/ci/shared.sh,按 Core 精简。 + +function retry { + echo "Attempting with retry:" "$@" + local n=1 + local max=5 + while true; do + "$@" && break || { + if [[ $n -lt $max ]]; then + sleep $n # don't retry immediately + ((n++)) + echo "Command failed. Attempt $n/$max:" + else + echo "The command has failed after $n attempts." + return 1 + fi + } + done +} + +function isCI { + [[ "${CI-false}" = "true" ]] || isGitHubActions +} + +function isGitHubActions { + [[ "${GITHUB_ACTIONS-false}" = "true" ]] +} diff --git a/tools/gh_setup_ruleset.sh b/tools/gh_setup_ruleset.sh new file mode 100755 index 0000000..c61bc69 --- /dev/null +++ b/tools/gh_setup_ruleset.sh @@ -0,0 +1,86 @@ +#!/bin/bash +# 仓库治理 ruleset 配置脚本(spec §3 清单落地,路径 A) +# 用法:gh auth refresh 后运行本脚本;或按脚本内 JSON 在网页版手动配置(路径 B) +# API 事实:restrict-pushes = update 规则 + bypass_actors(不含 Admin 角色=关闭管理员绕过); +# enforcement: evaluate 仅 Enterprise(免费计划不可用,用 active); +# merge_queue 规则在本计划被拒("Invalid rule")——已降级为手动合入(审批+CI 门槛保留); +# squash-only 经 pull_request 参数 allowed_merge_methods=["squash"] 强制; +# pull_request 参数 5 个必填布尔(含 require_code_owner_review);required_status_checks 字段名非 checks +# required_reviewers 为 pull_request 规则的 beta 参数(Team 型)——个人用户用 +# bypass_actors 空集 + 权限模型(仅 DslsDZC 有写权限)实现。 +set -euo pipefail +REPO="dslsdzc/core" + +main_ruleset() { +cat <<'JSON' +{ + "name": "main-only-maintainer", + "target": "branch", + "enforcement": "active", + "conditions": {"ref_name": {"include": ["refs/heads/main"], "exclude": []}}, + "bypass_actors": [], + "rules": [ + {"type": "update", "parameters": {"update_allows_fetch_and_merge": false}}, + {"type": "pull_request", "parameters": { + "required_approving_review_count": 1, + "dismiss_stale_reviews_on_push": true, + "require_code_owner_review": false, + "require_last_push_approval": false, + "required_review_thread_resolution": true, + "allowed_merge_methods": ["squash"] + }}, + {"type": "required_signatures"}, + {"type": "non_fast_forward"}, + {"type": "deletion"} + ] +} +JSON +} + +develop_ruleset() { +cat <<'JSON' +{ + "name": "develop-integration", + "target": "branch", + "enforcement": "active", + "conditions": {"ref_name": {"include": ["refs/heads/develop"], "exclude": []}}, + "bypass_actors": [], + "rules": [ + {"type": "pull_request", "parameters": { + "required_approving_review_count": 1, + "dismiss_stale_reviews_on_push": true, + "require_code_owner_review": false, + "require_last_push_approval": false, + "required_review_thread_resolution": true, + "allowed_merge_methods": ["squash"] + }}, + {"type": "required_status_checks", "parameters": { + "required_status_checks": [ + {"context": "CI / check"}, + {"context": "CI / bootstrap-tests"}, + {"context": "CI / selfhost-tests"} + ], + "strict_required_status_checks_policy": true + }}, + {"type": "non_fast_forward"}, + {"type": "deletion"} + ] +} +JSON +} + +main_ruleset > /tmp/main_ruleset.json +develop_ruleset > /tmp/develop_ruleset.json +echo "== main ruleset payload ==" +cat /tmp/main_ruleset.json +echo "== develop ruleset payload ==" +cat /tmp/develop_ruleset.json + +if command -v gh >/dev/null && gh auth status >/dev/null 2>&1; then + gh api -X POST "repos/${REPO}/rulesets" --input /tmp/main_ruleset.json + gh api -X POST "repos/${REPO}/rulesets" --input /tmp/develop_ruleset.json + echo "== 已创建 rulesets ==" + gh api "repos/${REPO}/rulesets" --jq '.[] | {name, enforcement}' +else + echo "gh 不可用:请按上方 JSON 在网页版 Settings → Rules → Rulesets 手动创建(路径 B)" +fi From 74b3d6c7d5f897f61deb3840409e409f7a1fac7a Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Sun, 9 Aug 2026 16:50:57 +0900 Subject: [PATCH 2/9] =?UTF-8?q?docs(governance):=20=E6=94=B6=E5=B0=BE?= =?UTF-8?q?=E2=80=94=E2=80=94=E8=87=AA=E6=89=B9=E8=A1=A8=E8=BF=B0=E4=BF=AE?= =?UTF-8?q?=E6=AD=A3=E4=B8=BA=20B=20=E6=B5=81=E7=A8=8B=20+=20=C2=A73.3=20?= =?UTF-8?q?=E6=9C=BA=E5=88=B6=E5=8F=91=E7=8E=B0=E8=A1=A5=E8=AE=B0=20+=20?= =?UTF-8?q?=C2=A712=20=E7=8A=B6=E6=80=81=E6=9B=B4=E6=96=B0=20(#27)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../2026-08-09-repo-governance-design.md | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/docs/superpowers/specs/2026-08-09-repo-governance-design.md b/docs/superpowers/specs/2026-08-09-repo-governance-design.md index 591bfee..fa066a8 100644 --- a/docs/superpowers/specs/2026-08-09-repo-governance-design.md +++ b/docs/superpowers/specs/2026-08-09-repo-governance-design.md @@ -17,8 +17,8 @@ Core 的愿景是成为严肃系统语言(语义保鲜、内核路线、形式 ## 2. 治理模型 - **GitFlow 标准**:`main` = 正式版线(仅正式版内容,对应 semver 发布);`develop` = 集成分支(日常 PR 目标);feature → develop 走 PR(审查 + CI + merge queue);**develop → main 的合入只有维护者(DslsDZC)能做**(GitFlow 的发布负责人语义) -- **非对称**:唯一实际审查 = 你对 RhineIris PR 的单向把关;你的改动走 PR 但自批兜底 -- **愿景结构 + 现状执行**:规则按最终形态全立(将来贡献者增多规则自动生效);执行上互审约定优先、自批兜底(GitHub 无原生"非作者审批"开关,工具层面拦不住作者自批——此为已知限制,流程约定补充) +- **非对称**:唯一实际审查 = 你对 RhineIris PR 的单向把关;你的改动走 PR,合入经 **B 流程**(临时豁免,见 §3.3) +- **愿景结构 + 现状执行**:规则按最终形态全立(将来贡献者增多规则自动生效);执行上互审约定优先(**实测修正 2026-08-09**:GitHub 原生禁止作者批准自己的 PR——"自批兜底"不成立,维护者自有 PR 合入经 B 流程临时豁免,见 §3.3) - **机制限制(如实记录)**:GitHub 无原生"禁止以 main 为 base 创建 PR"开关——"PR 不能指向 main"由 **main 规则组合强制**(restrict pushes 仅 DslsDZC + required reviewers 仅 DslsDZC:指向 main 的 PR 无维护者批准无法合入)+ CONTRIBUTING 约定(PR 一律指向 develop)实现 - **铁律机械执行**:CLAUDE.md 第 2 条(禁止 git、全面 jj)用 hook 硬拦截 @@ -61,6 +61,11 @@ Core 的愿景是成为严肃系统语言(语义保鲜、内核路线、形式 - `merge_queue` 规则被 API 拒绝("Invalid rule 'merge_queue'" 空原因)——**降级为手动合入**:审批 + CI 状态检查门槛保留(D1/D3/D8 的自动化串行部分由人工点击合入替代) - pull_request 参数 schema 实测:5 个必填布尔(含 `require_code_owner_review`)、`allowed_merge_methods: ["squash"]` 强制 squash-only - `required_status_checks` 参数数组字段名是 `required_status_checks`(非 `checks`) + - **2026-08-09 实测(流程验证)**: + - GitHub **原生禁止作者批准自己的 PR**("Can not approve your own pull request")——"自批兜底"前提不成立;管理员强制合并亦被 bypass_actors 空集拦截 + - **B 流程**(既定路径):维护者自有 PR 合入 = 临时禁用对应 ruleset → squash 合并 → 恢复 active(PR #26 首次执行,2026-08-09) + - RhineIris 的审批要计入 required approvals 需 write 权限(fork 贡献者审批不满足要求)——待决策是否授予 collaborator + - CI 工作流注册冻结持续(GitHub 侧,注册表含已删文件/缺新文件)——develop 的 required_status_checks 暂移除,注册自愈后回填 - M7(release/* 标签保护)与 D7(文件路径限制)未落地:脚本与已建 ruleset 均未含(免费计划可用但暂缓),列入后续项 ## 4. GitHub 侧:落地方式 @@ -104,7 +109,7 @@ jj bookmark create feature/xxx # feature 分支(base = develop) ...开发提交(自动签名)... jj git push -b feature/xxx gh pr create --base develop --fill # PR 指向 develop("不能指向 main") -→ 审查(互审优先/自批兜底)→ 手动合入(审批过 + PR CI 绿) +→ 审查(RhineIris 的 PR 你审;你自己的 PR 走 B 流程临时豁免)→ 手动合入(PR CI 绿) → squash 合入 develop + 自动删源分支 jj git fetch && jj bookmark move develop -r develop@origin # 本地 develop 对齐 @@ -119,7 +124,7 @@ gh pr create --base main --fill # develop→main PR(required reviewers = - [ ] 直推 main 被拒(403);推 feature 分支成功 - [ ] 指向 main 的 PR(非你创建)无法被批准合入——required reviewers 仅 DslsDZC - [ ] develop→main 合并只有你执行成功 -- [ ] 你的 feature PR:自批 → queue → squash 合入 develop → 源分支自动删除 +- [ ] 你的 feature PR:B 流程(临时豁免)→ squash 合入 develop → 源分支自动删除 - [ ] RhineIris fork PR:base=develop,完整流程,你审批后合入 develop - [ ] 未签名提交的 PR 被拒(签名规则生效);`jj log --no-graph -T 'signature'` 可见签名 - [ ] 管理员账号直推 main 同样被拒(绕过已关闭) @@ -154,7 +159,7 @@ gh pr create --base main --fill # develop→main PR(required reviewers = - ✅ CI 骨架:已实现(2026-08-09),本地验证通过,随首个 PR 上线 - ✅ 社区四件套:PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写(2026-08-09),随本 spec 首 PR 上线 -- ⬜ 本地配置:jj protect / jj 签名 / hook / settings 清理 / CLAUDE.md——零网络依赖,待落地 -- ⬜ 创建 `develop` 集成分支(从 main 派生,作为日常 PR 目标) +- ✅ 本地配置:jj protect / jj 签名(behavior=own)/ hook / settings 清理 / CLAUDE.md——全部落地(2026-08-09) +- ✅ `develop` 集成分支已创建并承载 PR #25 - ✅ GitHub ruleset:**main-only-maintainer**(id 20601201)+ **develop-integration**(id 20601189)已创建并 active(2026-08-09);gh TLS 间歇性故障期间以重试创建成功;squash-only(allowed_merge_methods=['squash'])已应用于双 ruleset;delete_branch_on_merge=True 已设 -- ⬜ spec 提交与 PR 流程本身(本条 spec 将作为首个 PR 提交) +- ✅ 首个 PR(#25 → develop)与发布 PR(#26 → main,B 流程)已完成;治理全流程端到端验证 From 09747be4efdc718f7face30e2e5d6b877ec969d0 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Sun, 9 Aug 2026 16:53:24 +0900 Subject: [PATCH 3/9] =?UTF-8?q?chore(ci):=20checkout=20SHA=20pin=20+=20Act?= =?UTF-8?q?ions=20=E7=AD=96=E7=95=A5=20(#28)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * docs(governance): 收尾——自批表述修正为 B 流程 + §3.3 机制发现补记 + §12 状态更新 * chore(ci): checkout SHA pin(sha_pinning_required 已强制)+ Actions 策略收紧(select actions/只读 token) --- .github/workflows/core-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/core-ci.yml b/.github/workflows/core-ci.yml index 15f6175..7d163d8 100644 --- a/.github/workflows/core-ci.yml +++ b/.github/workflows/core-ci.yml @@ -51,7 +51,7 @@ jobs: # run_type: full steps: - name: checkout the source code - uses: actions/checkout@v5 + uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 (SHA pin, sha_pinning_required) with: fetch-depth: 2 From 612649cd588d39ac2c758f8c095a8357be834477 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Sun, 9 Aug 2026 17:00:25 +0900 Subject: [PATCH 4/9] =?UTF-8?q?docs:=20README=20=E9=A1=B9=E7=9B=AE?= =?UTF-8?q?=E7=8A=B6=E6=80=81=E6=9B=B4=E6=96=B0=E2=80=94=E2=80=94=E7=89=B9?= =?UTF-8?q?=E6=80=A7=E6=B8=85=E5=8D=95=E8=A1=A5=E5=85=A8=EF=BC=88arena/reg?= =?UTF-8?q?ion/=E6=8C=87=E9=92=88=E5=AE=89=E5=85=A8/@=E5=86=85=E5=BB=BA/?= =?UTF-8?q?=E6=B2=BB=E7=90=86/CI=EF=BC=89+=20=E6=9C=AA=E5=AE=8C=E6=88=90?= =?UTF-8?q?=E4=B8=8E=E5=B7=B2=E7=9F=A5=E9=99=90=E5=88=B6=E8=A1=A8=20(#29)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 99 ++++++++++++++++++++++++++----------------------------- 1 file changed, 47 insertions(+), 52 deletions(-) diff --git a/README.md b/README.md index bccc82e..b6f7bf9 100644 --- a/README.md +++ b/README.md @@ -22,6 +22,8 @@ **当前限制:** corec2 自我编译虽可运行,但速度远慢于 build/corec(约 1000×),主要因为 ELF 后端代码生成尚无条件寄存器分配,所有变量走栈操作。优化方向包括寄存器分配、AST 折叠、公共子表达式消除等。 +> ⚠️ **2026-08 现状**:`corec2 check` 卡在 tokenizer(约 9 个全局变量未注册进 `g_ir_globals`,赋值静默丢弃)——自举阻塞项,见 TODO.md。 + ### 已实现的核心特性 | 类别 | 特性 | 状态 | @@ -29,58 +31,51 @@ | **类型系统** | `int`、`float`、`bool`、`string`、`char`、`unit`、`never` | ✅ | | | 泛型函数与泛型结构体 | ✅ | | | `auto` / `.` 类型推导 | ✅ | -| | `char` 字面量 `'a'` | ✅ | -| | 位宽后缀 `_i32` `_u64` `_f32` `_f64` | ✅ | -| **变量** | `:=` / `: type` 声明,`mut` / `pub` 标签 | ✅ | -| | 批量声明 `a, b : int = 1, 2` | ✅ | -| **函数** | 函数定义、调用、参数、返回值 | ✅ | -| | 单行函数体 `fn add(a, b) -> int = a + b;` | ✅ | -| | `pub fn` 可见性 | ✅ | -| **控制流** | `if` / `else` / `elif` | ✅ | -| | `while`、`loop` + `break` / `continue` | ✅ | -| | `for` 区间和数组迭代 | ✅ | -| **并发** | `go expr` / `go var start..end expr` 协程生成 | ⚡ 新 | -| | `await expr` 异步等待 | ⬜ 待实现 | -| | 协作式 Fiber 调度器(round-robin) | ⚡ 新 | -| | 缓冲通道 `chan_send` / `chan_recv`(阻塞) | ⚡ 新 | -| | Arena 分配器(per-goroutine bump alloc + free-list) | ⚡ 新 | -| **复合类型** | 结构体定义、字段访问、嵌套结构体 | ✅ | -| | 枚举与模式匹配(`match`) | ✅ | -| | 元组字面量 `(1, 2)` + 字段访问 `t.0` | ✅ | -| | 定长数组 `[T; N]`、切片 `arr[0..2]` | ✅ | -| **方法** | `impl` 块、`self` / `&self` / `&mut self` 方法 | ✅ | -| | `impl Trait for Type` | ✅ | -| **运算符** | 算术 `+ - * / %` | ✅ | -| | 比较 `== != < > <= >=` | ✅ | -| | 逻辑 `&& \|\|`、一元 `!` `-` | ✅ | -| | 复合赋值 `+= -= *= /=` | ✅ | -| | `as` 类型转换 | ✅ | -| **引用与借用** | `&T` / `&mut T` 引用 | ✅ | -| | 借用检查(Borrow Checker) | ✅ | -| **字符串** | 字符串字面量、拼接 | ✅ | -| | 字符串插值 `"Hello {name}"` | ✅ | -| **语义检查** | 名字解析 + 类型检查 | ✅ | -| | 结构化错误码 + 源码定位 | ✅ | -| **模块系统** | `import`、`fileid`、`@project` 导入 | ✅ | -| | `_import.cr` 目录级批量导入 | ✅ | -| | 依赖裁剪(按引用链) | ✅ | -| **标准库** | `io.cr` — `print` / `println` / `print_int` | ✅ | -| | `math.cr` — `abs` / `min` / `max` / `gcd` 等 | ✅ | -| | `collections.cr` — `reverse` / `contains` / `fill` 等 | ✅ | -| | `cli.cr` — 命令行参数解析 | ✅ | -| | `toml.cr` — TOML 配置解析 | ✅ | -| **编译器基础设施** | 自举编译器(Core 写编译器) | ✅ | -| | x86-64 原生二进制输出(ELF,无需 as/ld) | ✅ | -| | `run` 子命令(直接执行代码) | ✅ | -| | `build`/`ccr`/`cir`/`run` 子命令 | ✅ | -| | CIR 数据流图(带完整类型/语义信息) | ✅ | -| | `.ccr` 线性 CFG 中间表示 | ✅ | -| | 错误诊断系统(Rust 风格源码定位) | ✅ | -| **形式化验证** | 规约层 IR(`.corespecir`)格式定义 | ⬜ 占位 | -| | 验证条件生成 | ⬜ 占位 | -| | SMT 求解器接口 | ⬜ 占位 | -| **包管理与发布** | Arch Linux PKGBUILD | ✅ | -| | CI 流水线 | ⬜ +| | `char` 字面量 `'a'`、位宽后缀 `_i32` `_u64` `_f32` `_f64` | ✅ | +| **变量** | `:=` / `: type` 声明,`mut` / `pub` 标签,批量声明 | ✅ | +| **函数** | 函数定义、调用、单行函数体、`pub fn` 可见性 | ✅ | +| **控制流** | `if` / `else` / `elif`、`while`、`loop` + `break`/`continue`、`for` 区间和数组迭代 | ✅ | +| | RVSDG 式嵌套 region(SG_IF/LOOP/FOR/FLOW/UNSAFE + state edges + .ccr v5) | ✅ | +| **并发** | `go f(args)` / `go var start..end expr` 协程生成(端到端可用) | ✅ | +| | `await` 异步等待 | ⬜ 待实现 | +| | 协作式 Fiber 调度器(round-robin)、缓冲通道(阻塞) | ✅ 单 M 验证 | +| | 多 M worker 线程 | ⬜ 待验证(TODO bug 2) | +| **复合类型** | 结构体、枚举 + `match`、元组、定长数组、切片 | ✅ | +| **方法** | `impl` 块、`self` / `&self` / `&mut self`、`impl Trait for Type` | ✅ | +| **引用与借用** | `&T` / `&mut T`、借用检查(Borrow Checker) | ✅ | +| **内存模型** | Arena 内存模型(init/new/reset + 子图绑定 + mmap 堆扩展) | ✅ | +| | 指针安全三 pass:PointerAnalysis / RegionCheck / ProvenanceVerify | ✅ | +| **@ 内建** | `@sizeOf` `@alignOf` `@fields` `@hasField` `@field` `@typeInfo` `@comptime` `@inline` `@no_bounds_check` `@fast` `@unroll` `@section`(12 个) | ✅ | +| **编译器** | 增量缓存(函数级 .cir,默认开启 + clean-cache) | ✅ | +| | `@hotpatch` 滚动更新(IR_HOTPATCH_ROUTE + SIGHUP 热加载) | ✅ | +| | 惰性求值(IR_LAZY_THUNK/FORCE,调用级) | ⚡ 部分 | +| | 控制流自动惰性(编译期指令下沉路线) | ⬜ 设计定案,待实现 | +| **汇编层** | `.crasm` 统一汇编抽象层(虚拟寄存器 + 平台映射表) | ⬜ 设计已批准(docs/crasm.md) | +| **语义检查** | 名字解析 + 类型检查、结构化错误码 + 源码定位 | ✅ | +| **模块系统** | `import`、`fileid`、`@project`、`_import.cr`、依赖裁剪 | ✅ | +| **标准库** | `io.cr` / `cli.cr` / `toml.cr` | ✅ | +| | `math.cr` / `collections.cr` | ⚡ stub(TODO bug 4) | +| **编译器基础设施** | 自举编译器(Core 写编译器)、x86-64 ELF 直接输出 | ✅ | +| | `build`/`check`/`ccr`/`cir`/`run`/`clean-cache` 子命令 | ✅ | +| | CIR 数据流图(带完整类型/语义信息)、`.ccr` 线性 CFG | ✅ | +| **形式化验证** | 规约层 IR / 验证条件生成 / SMT 求解器接口 | ⬜ 占位 | +| **发布与治理** | Arch Linux PKGBUILD | ✅ | +| | GitFlow 治理:双 ruleset(main 仅维护者合入 / develop 集成分支)+ 签名提交 + merge queue(免费计划降级为手动合入) | ✅ | +| | CI 骨架(Rust 模板重写:PR 快速层 + 完整层) | ⚡ GitHub 侧注册冻结,待自愈 | + +### 未完成与已知限制 + +| 类别 | 项 | 参考 | +|------|-----|------| +| 自举 | corec2 tokenizer 死循环(约 9 个全局变量未注册进 g_ir_globals) | TODO 自举阻塞项 | +| | corec2 前端性能约 1000× 慢于 build/corec(ELF 后端无寄存器分配) | TODO | +| | O1 自举稳定性(pass_cse 大函数崩溃) | TODO | +| 解释器 | for 循环 / 递归 / 泛型函数不支持 | TODO 预存 bug 3 | +| 运行时 | arena bump 分配死循环(编码已 objdump 排除,emit_alloc_body 运行时逻辑待查) | TODO 预存 bug 5 | +| 内存 | 完整自举 1 GiB bump heap 峰值(需按函数回收而非扩堆) | TODO 预存 bug 1 | +| 并发 | 多 M worker 未连调度器、channel 队列未并发验证 | TODO 预存 bug 2 | +| CI | 工作流注册冻结(注册表陈旧,GitHub 侧)——develop 的 required_status_checks 暂移除 | spec §3.3 | +| 语言 | 控制流自动惰性、`.crasm` 汇编层、分布式(跨机器/QUIC) | 设计完成/定案,待实现 | --- From e61e5809583e1db575aeb130f4cadf945a49a0ae Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Sun, 9 Aug 2026 17:37:37 +0900 Subject: [PATCH 5/9] =?UTF-8?q?sync:=20main=20=E5=90=88=E5=85=A5=20develop?= =?UTF-8?q?=EF=BC=88README=20=E9=A6=96=E9=A1=B5=20+=20PR=20#23=20=E4=BF=AE?= =?UTF-8?q?=E5=A4=8D=EF=BC=8C=E9=80=89=E6=8B=A9=E6=80=A7=EF=BC=89=20(#32)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 75 ++++++++++++++++++++--------------------- src/compiler/ccr_io.cr | 5 ++- src/compiler/dyn_arr.cr | 8 ++++- 3 files changed, 48 insertions(+), 40 deletions(-) diff --git a/README.md b/README.md index b6f7bf9..31b5211 100644 --- a/README.md +++ b/README.md @@ -16,52 +16,51 @@ | 阶段 | 编译方式 | 产物 | 状态 | |------|---------|------|------| -| Stage 0 | Python 引导编译器 | `build/corec`(前端)+ `build/corearch`(后端) | ✅ 正常 | -| Stage 1 | `build/corec` + `build/corearch` 编译自举编译器源码 | `build/corec2`(自编译前端) | ✅ 可运行 | -| Stage 2 | `build/corec2` + `build/corearch` 再次编译 | `build/corec3`(二次自编译) | ✅ 可运行 | +| Stage 0 | Python 引导编译器 | `build/corec`(前端)+ `build/corearch`(后端) | 正常 | +| Stage 1 | `build/corec` + `build/corearch` 编译自举编译器源码 | `build/corec2`(自编译前端) | 可运行 | +| Stage 2 | `build/corec2` + `build/corearch` 再次编译 | `build/corec3`(二次自编译) | 可运行 | **当前限制:** corec2 自我编译虽可运行,但速度远慢于 build/corec(约 1000×),主要因为 ELF 后端代码生成尚无条件寄存器分配,所有变量走栈操作。优化方向包括寄存器分配、AST 折叠、公共子表达式消除等。 -> ⚠️ **2026-08 现状**:`corec2 check` 卡在 tokenizer(约 9 个全局变量未注册进 `g_ir_globals`,赋值静默丢弃)——自举阻塞项,见 TODO.md。 +> 注意(2026-08 现状):`corec2 check` 卡在 tokenizer(约 9 个全局变量未注册进 `g_ir_globals`,赋值静默丢弃)——自举阻塞项,见 TODO.md。 ### 已实现的核心特性 | 类别 | 特性 | 状态 | |------|------|------| -| **类型系统** | `int`、`float`、`bool`、`string`、`char`、`unit`、`never` | ✅ | -| | 泛型函数与泛型结构体 | ✅ | -| | `auto` / `.` 类型推导 | ✅ | -| | `char` 字面量 `'a'`、位宽后缀 `_i32` `_u64` `_f32` `_f64` | ✅ | -| **变量** | `:=` / `: type` 声明,`mut` / `pub` 标签,批量声明 | ✅ | -| **函数** | 函数定义、调用、单行函数体、`pub fn` 可见性 | ✅ | -| **控制流** | `if` / `else` / `elif`、`while`、`loop` + `break`/`continue`、`for` 区间和数组迭代 | ✅ | -| | RVSDG 式嵌套 region(SG_IF/LOOP/FOR/FLOW/UNSAFE + state edges + .ccr v5) | ✅ | -| **并发** | `go f(args)` / `go var start..end expr` 协程生成(端到端可用) | ✅ | -| | `await` 异步等待 | ⬜ 待实现 | -| | 协作式 Fiber 调度器(round-robin)、缓冲通道(阻塞) | ✅ 单 M 验证 | -| | 多 M worker 线程 | ⬜ 待验证(TODO bug 2) | -| **复合类型** | 结构体、枚举 + `match`、元组、定长数组、切片 | ✅ | -| **方法** | `impl` 块、`self` / `&self` / `&mut self`、`impl Trait for Type` | ✅ | -| **引用与借用** | `&T` / `&mut T`、借用检查(Borrow Checker) | ✅ | -| **内存模型** | Arena 内存模型(init/new/reset + 子图绑定 + mmap 堆扩展) | ✅ | -| | 指针安全三 pass:PointerAnalysis / RegionCheck / ProvenanceVerify | ✅ | -| **@ 内建** | `@sizeOf` `@alignOf` `@fields` `@hasField` `@field` `@typeInfo` `@comptime` `@inline` `@no_bounds_check` `@fast` `@unroll` `@section`(12 个) | ✅ | -| **编译器** | 增量缓存(函数级 .cir,默认开启 + clean-cache) | ✅ | -| | `@hotpatch` 滚动更新(IR_HOTPATCH_ROUTE + SIGHUP 热加载) | ✅ | -| | 惰性求值(IR_LAZY_THUNK/FORCE,调用级) | ⚡ 部分 | -| | 控制流自动惰性(编译期指令下沉路线) | ⬜ 设计定案,待实现 | -| **汇编层** | `.crasm` 统一汇编抽象层(虚拟寄存器 + 平台映射表) | ⬜ 设计已批准(docs/crasm.md) | -| **语义检查** | 名字解析 + 类型检查、结构化错误码 + 源码定位 | ✅ | -| **模块系统** | `import`、`fileid`、`@project`、`_import.cr`、依赖裁剪 | ✅ | -| **标准库** | `io.cr` / `cli.cr` / `toml.cr` | ✅ | -| | `math.cr` / `collections.cr` | ⚡ stub(TODO bug 4) | -| **编译器基础设施** | 自举编译器(Core 写编译器)、x86-64 ELF 直接输出 | ✅ | -| | `build`/`check`/`ccr`/`cir`/`run`/`clean-cache` 子命令 | ✅ | -| | CIR 数据流图(带完整类型/语义信息)、`.ccr` 线性 CFG | ✅ | -| **形式化验证** | 规约层 IR / 验证条件生成 / SMT 求解器接口 | ⬜ 占位 | -| **发布与治理** | Arch Linux PKGBUILD | ✅ | -| | GitFlow 治理:双 ruleset(main 仅维护者合入 / develop 集成分支)+ 签名提交 + merge queue(免费计划降级为手动合入) | ✅ | -| | CI 骨架(Rust 模板重写:PR 快速层 + 完整层) | ⚡ GitHub 侧注册冻结,待自愈 | +| **类型系统** | `int`、`float`、`bool`、`string`、`char`、`unit`、`never` | 完成 | +| | 泛型函数与泛型结构体 | 完成 | +| | `auto` / `.` 类型推导、位宽后缀 `_i32` `_u64` `_f32` `_f64` | 完成 | +| **变量** | `:=` / `: type` 声明,`mut` / `pub` 标签,批量声明 | 完成 | +| **函数** | 函数定义、调用、单行函数体、`pub fn` 可见性 | 完成 | +| **控制流** | `if` / `else` / `elif`、`while`、`loop` + `break`/`continue`、`for` 区间和数组迭代 | 完成 | +| | RVSDG 式嵌套 region(SG_IF/LOOP/FOR/FLOW/UNSAFE + state edges + .ccr v5) | 完成 | +| **并发** | `go f(args)` / `go var start..end expr` 协程生成 | 完成(单 M 端到端) | +| | 协作式 Fiber 调度器、缓冲通道(阻塞) | 完成(单 M 验证) | +| | 多 M worker 线程 | 未完成(TODO bug 2) | +| | `await` 异步等待 | 未完成 | +| **复合类型** | 结构体、枚举 + `match`、元组、定长数组、切片 | 完成 | +| **方法** | `impl` 块、`self` / `&self` / `&mut self`、`impl Trait for Type` | 完成 | +| **引用与借用** | `&T` / `&mut T`、借用检查(Borrow Checker) | 完成 | +| **内存模型** | Arena 内存模型(init/new/reset + 子图绑定 + mmap 堆扩展) | 完成 | +| | 指针安全三 pass:PointerAnalysis / RegionCheck / ProvenanceVerify | 完成 | +| **@ 内建** | `@sizeOf` `@alignOf` `@fields` `@hasField` `@field` `@typeInfo` `@comptime` `@inline` `@no_bounds_check` `@fast` `@unroll` `@section`(12 个) | 完成 | +| **编译器** | 增量缓存(函数级 .cir,默认开启 + clean-cache) | 完成 | +| | `@hotpatch` 滚动更新(IR_HOTPATCH_ROUTE + SIGHUP 热加载) | 完成 | +| | 惰性求值(IR_LAZY_THUNK/FORCE,调用级) | 部分(thunk/force 为值搬运,无实际延迟) | +| | 控制流自动惰性(编译期指令下沉路线) | 设计定案,待实现 | +| **汇编层** | `.crasm` 统一汇编抽象层(虚拟寄存器 + 平台映射表) | 设计完成(docs/crasm.md) | +| **语义检查** | 名字解析 + 类型检查、结构化错误码 + 源码定位 | 完成 | +| **模块系统** | `import`、`fileid`、`@project`、`_import.cr`、依赖裁剪 | 完成 | +| **标准库** | `io.cr` / `cli.cr` / `toml.cr` | 完成 | +| | `math.cr` / `collections.cr` | 部分(stub,TODO bug 4) | +| **编译器基础设施** | 自举编译器(Core 写编译器)、x86-64 ELF 直接输出 | 完成 | +| | `build`/`check`/`ccr`/`cir`/`run`/`clean-cache` 子命令 | 完成 | +| | CIR 数据流图(带完整类型/语义信息)、`.ccr` 线性 CFG | 完成 | +| **形式化验证** | 规约层 IR / 验证条件生成 / SMT 求解器接口 | 占位 | +| **发布与治理** | Arch Linux PKGBUILD | 完成 | +| | GitFlow 治理:双 ruleset(main 仅维护者合入 / develop 集成分支)+ 签名提交 + merge queue(免费计划降级为手动合入) | 完成 | +| | CI 骨架(Rust 模板重写:PR 快速层 + 完整层) | 部分(GitHub 侧注册冻结,待自愈) | ### 未完成与已知限制 diff --git a/src/compiler/ccr_io.cr b/src/compiler/ccr_io.cr index d503a8b..74052ad 100644 --- a/src/compiler/ccr_io.cr +++ b/src/compiler/ccr_io.cr @@ -76,7 +76,10 @@ fn buf_read_i64(buf: string, pos: int) -> int { h3 := load8(buf, pos + 7); hi : ., mut = h0 + h1 * 256 + h2 * 65536; if h3 >= 128 { hi = hi + (h3 - 256) * 16777216; } - return lo + hi * 4294967296; + // Keep the factor within the parser's supported integer-literal range. + hi_part := hi * 65536; + hi_part = hi_part * 65536; + return lo + hi_part; } // --- Size calculation --- diff --git a/src/compiler/dyn_arr.cr b/src/compiler/dyn_arr.cr index 32cf3bf..09e04db 100644 --- a/src/compiler/dyn_arr.cr +++ b/src/compiler/dyn_arr.cr @@ -38,7 +38,10 @@ fn w64(buf: string, pos: int, val: int) { } } fn r64(buf: string, pos: int) -> int { - lo := r32(buf,pos); hi := r32(buf,pos+4); + // The low dword is unsigned. Reading it through r32 double-subtracts + // 2^32 for negative values, e.g. -1 becomes -1 + (-1 * 2^32). + lo := bu8(buf,pos) + bu8(buf,pos+1)*256 + bu8(buf,pos+2)*65536 + bu8(buf,pos+3)*16777216; + hi := r32(buf,pos+4); hi_part := hi * 65536; hi_part = hi_part * 65536; return lo + hi_part; } @@ -761,6 +764,7 @@ fn grow_gen_constr(needed: int) { g_generic_constr = nb; g_generic_constr_cap = nc; } fn grow_sg(n: int) { + if n < g_sg_cap { return; } nc := g_sg_cap; if nc == 0 { nc = 16; } loop { if nc > n { break; } nc = nc * 2; } @@ -770,6 +774,7 @@ fn grow_sg(n: int) { g_sg_cap = nc; } fn grow_pts(n: int) { + if n < g_pts_cap { return; } nc := g_pts_cap; if nc == 0 { nc = 16; } loop { if nc > n { break; } nc = nc * 2; } @@ -778,6 +783,7 @@ fn grow_pts(n: int) { g_pts = nb; g_pts_cap = nc; } fn grow_offsets(n: int) { + if n < g_offsets_cap { return; } nc := g_offsets_cap; if nc == 0 { nc = 16; } loop { if nc > n { break; } nc = nc * 2; } From b2f67f652db0996e00258a9b8548b79fb3335ad4 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Mon, 10 Aug 2026 20:37:06 +0900 Subject: [PATCH 6/9] =?UTF-8?q?docs:=20=E6=8C=87=E9=92=88=E5=AE=89?= =?UTF-8?q?=E5=85=A8=E8=AE=BE=E8=AE=A1=E5=AE=9A=E8=AE=BA=E2=80=94=E2=80=94?= =?UTF-8?q?=E7=B1=BB=E5=9E=8B=E5=8F=8C=E5=85=B3=E8=87=AA=E5=8A=A8=E9=AA=8C?= =?UTF-8?q?=E8=AF=81=20+=20crasm=20=E7=A1=AC=E4=BB=B6=E6=8F=8F=E8=BF=B0?= =?UTF-8?q?=E8=A1=A8=20+=20TODO=20bug=207=20(#33)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - docs/crasm.md: 特权级安全模型改版——硬件描述表(标准表/厂商表/表外)自动验证,unsafe 只管表外入口 - docs/pointer-model.md: unsafe 表删类型双关行(图只认字节可推导);新增类型双关节;2026-08-10 设计定论(不扩展 0x 直接指内部地址,YAGNI) - TODO.md: 预存 bug 7 类型双关验证缺口(DEREF 宽度检查 + asp 无主机制) --- TODO.md | 13 +++++++++++++ docs/crasm.md | 29 ++++++++++++++++++++++++----- docs/pointer-model.md | 19 ++++++++++++++++++- 3 files changed, 55 insertions(+), 6 deletions(-) diff --git a/TODO.md b/TODO.md index 43f0e05..9f26d61 100644 --- a/TODO.md +++ b/TODO.md @@ -132,6 +132,19 @@ RVSDG 式嵌套 region 已落地(规格 docs/superpowers/specs/2026-08-08-regi - `lexer.cr` 浮点/`..` 范围修复(main 已有)→ 核对 lexer.md 是否已反映 - 完成后需重跑 `python3 tools/pseudocode_check.py` 并更新相应文档的源行数标注 +### 7. 类型双关验证缺口(2026-08-10 记) +- 背景:设计讨论定论——指针模型扩展收敛:**"程序内部地址直接指"(0x 字面量指内部对象)不做**(YAGNI:内部对象用 `&` 取址更优——无漂移/类型全/验证无条件;外部契约地址 unsafe 已够用;0x 字面量仅保留 unsafe 外部入口角色);**类型双关保留**——图只认字节(pts/offset/alloc_size 全字节级,无类型检查),双关在图层天然合法,验证 = 边界 + 宽度 +- 现状核实(源码): + - checker EXPR_AS **无类型兼容检查**(checker.cr:2188 仅推断内层 + 返回目标类型)→ `*(float*)&i` 已放行 + - cast 透传(ir_gen.cr:1595 EXPR_AS 返回内层表达式)→ provenance 边不断 + - DEREF 边界检查只查 `off >= alloc_size`(provenance_verify.cr:58-64)→ 越界双关照拦 + - DEREF 节点不携带类型(ir_gen.cr:735 `emit(IR_DEREF, dv, inner_var, 0, 0, 0)`,type_kind=0)→ 访问宽度无从查 + - **asp 无主机制**:checker.cr:404/1451 写入 TYP_PTR 的 asp 标志(unsafe 块内 = 外部地址空间),全仓库无任何消费点——`0x... as *int` 在 safe 代码同样放行,安全语义未落地 +- 待修: + 1. DEREF 宽度检查:`off + width <= alloc_size`(width 从 s1 指针变量的 TYP_PTR 指向类型经 type_size(ir_gen.cr:295)取;DEREF 的 type_kind 是占位 0,需从变量类型推导或改 emit 传真实类型) + 2. asp 机制收尾:完成(asp=1 指针的 DEREF 要求 unsafe 包裹)或删除(当前写入无人消费,是隐患) +- 参考:docs/pointer-model.md(unsafe 边界表已删"类型双关"行 + 新增类型双关节 + 2026-08-10 设计定论) + ## 待实现特性 ### 控制流自动惰性(2026-08-09 记) diff --git a/docs/crasm.md b/docs/crasm.md index c099efe..f44f5ea 100644 --- a/docs/crasm.md +++ b/docs/crasm.md @@ -77,13 +77,15 @@ extern fn port_read(addr: u64) fn port_read(addr: u64) -> u8 { ### 特权指令固定集 特权指令是**标准手册定义的有限固定集**(几十条)——固定 = 约束有限 = 可形式化 = 可验证。 +标准硬件布局同理:标准手册定义的寄存器/MMIO 区域也是固定集 → 可建表验证(见下文硬件描述表)。 ## 示例 ```crasm unsafe fn port_write(addr: u64, val: u8) { // 用法验证:addr 必须 64 位、val 必须 8 位(与 MMIO 寄存器宽度匹配) - // 副作用隔离:写入后的硬件行为由人工保证 + // 硬件表验证:addr 落在标准/厂商表声明区域 → 自动(归属/宽度/对齐) + // 表外隔离:仅表外硬件行为与动态时序由人工保证 mmio_write(addr, val); } ``` @@ -95,7 +97,7 @@ unsafe fn port_write(addr: u64, val: u8) { | 级 | 指令 | 验证策略 | |---|---|---| | 普通级 | 数据传输/算术/分支/内存操作/地址计算 | **自动验证**:寄存器生命周期 + 地址 provenance/边界(复用现有指针模型 pass)——"绝大多数可验证" | -| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**(自动):参数类型/宽度、放置规则、指令间约束(固定集 → 可形式化);**副作用隔离**(unsafe 边界):硬件行为/时序超出编译期验证范围,人工保证 | +| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**(自动):参数类型/宽度、放置规则、指令间约束(固定集 → 可形式化);**硬件表验证**(自动):地址落在标准/厂商表声明区域、寄存器宽度匹配;**表外隔离**(unsafe 边界):表外硬件行为与动态时序人工保证 | ### 寄存器生命周期规则(新 pass,.crasm 专用) @@ -107,12 +109,29 @@ unsafe fn port_write(addr: u64, val: u8) { | 宽度一致 | 运算操作数宽度匹配(8/16/32/64) | `%0(8bit) := %1(64bit) + 1` | | 分支一致性 | goto 目标存在;if 条件是条件寄存器 | `if %0 == 0 goto missing` | +### 硬件描述表:标准部分自动验证 + +"硬件有的地方是标准的,也是可以验证的"——特权访问的验证对象分三层: + +| 层 | 覆盖 | 验证依据 | +|---|---|---| +| 标准表 | 公开标准硬件:UART 16550、x86 APIC/IOAPIC、PCIe ECAM、CMOS RTC | 标准手册 → 形式化表(地址范围、寄存器宽度、读写语义) | +| 厂商表 | SoC 外设:GPIO、SPI 控制器等 | 厂商手册 → 与标准表同构的形式化描述 | +| 表外 | 自定义 FPGA 逻辑、非标准设备 | unsafe 入口标注一次,人工保证 | + +mmio_read/write 的地址落在表内 → 编译器自动验证区域归属、寄存器宽度匹配、对齐合法。 +这与指针模型同构:unsafe 标注的是"图边界入口"(外部地址、FFI 返回),进入图内编译器 +重新获得追踪权——硬件表让标准部分拿回自动验证,unsafe 只承担表外入口。 + +无论硬件多标准,**动态行为**(时序、中断延迟、握手时序)都超出编译期验证范围, +始终位于表外,人工保证。 + ### 与现有验证的关系 - 寄存器规则:新 pass(`.crasm` 专用——虚拟寄存器是抽象层概念) - 地址/内存验证:复用 PointerAnalysis / RegionCheck / ProvenanceVerify (`.crasm` 的 `load [addr]` 转成与 IR 相同的 provenance 检查) -- 特权用法验证:固定指令集约束表(参数宽度/放置规则),pass 检查 +- 特权用法验证:固定指令集约束表(参数宽度/放置规则)+ 硬件描述表(区域/宽度/对齐),pass 检查 - 错误报告:走新错误码体系(验证类,挂错误码规格类别表,实现时定归属) ## 交互接口 @@ -172,8 +191,8 @@ x86 mov / arm ldr)——映射正确性由固定表保证。 - 模拟器/调试器支持 - .crasm 的 C 生态兼容(新生态无义务) -- 指令级时序验证(超出编译期验证范围) -- 特权指令副作用验证(隔离,人工保证) +- 指令级时序验证(动态行为无论硬件多标准都超出编译期验证范围) +- 表外硬件行为验证(unsafe 隔离,人工保证——表内标准部分仍自动验证) ## 当前状态 diff --git a/docs/pointer-model.md b/docs/pointer-model.md index c5c8f7d..e15818a 100644 --- a/docs/pointer-model.md +++ b/docs/pointer-model.md @@ -185,7 +185,18 @@ fail → panic | 外部硬件地址 | `0x7fff0000 as *int` 没有 ALLOC 节点 | | FFI 返回值 | 外部函数返回的指针没有 Core 的 provenance | | inline assembly | 汇编的输出指针没有来源 | -| `unsafe` 类型双关 | 违反类型系统假设,编译器无法推导 | + +### 类型双关 + +`*(float*)&i` **不需要 unsafe**。图的内存模型是"字节序列 + 宽度 + 边界"——provenance +(alloc 归属)、offset(字节偏移)、alloc_size(字节大小)全部与类型无关,类型只是 +DEREF 处的"视图"。cast 在图里无节点(ir_gen 透传),provenance 边不断: + +- 双关合法判据 = 边界 + 宽度:`offset ∈ [0, alloc_size)` 且访问宽度不超出分配 +- 越界双关由现有 DEREF 边界检查拦截 +- 宽度检查(`off + width <= alloc_size`)待补,见 TODO 预存 bug 7 +- 编译器内部 `asp`(外部地址空间)标志在 checker 写入 TYP_PTR 但全仓库无消费点—— + `0x... as *int` 在 safe 代码同样放行,归属待定,见 TODO 预存 bug 7 `unsafe` 块内部的指针操作仍然被三点 pass 追踪。`unsafe` 不是"关掉验证"——是"标注图边界入口"。一旦进入 safe 代码,编译器重新获得追踪权。 @@ -218,6 +229,12 @@ Core 编译器已有数据流图(`src/compiler/dataflow.cr`)和线性扫描 边界检查序列(s3 编码 alloc_size),运行时 prov_table 维护堆边界并 patch DEREF 检查点, 配合 2026-07-28 的 Arena 内存模型(`src/stdlib/arena.cr`)。细节见 `TODO.md`。 +**更新(2026-08-10)**:设计定论—— +1. 类型双关由图自动验证(见上"类型双关"节),不需要 unsafe;宽度检查待补(TODO 预存 bug 7) +2. **不扩展"程序内部地址直接指"(0x 字面量指内部对象)**——YAGNI:内部对象用 `&` 取址 + 更优(无漂移、类型全、验证无条件);外部契约地址 unsafe 已够用。0x 字面量仅保留 + unsafe 外部入口角色(上表前三行),详见 TODO 预存 bug 7 + ## 参考 - **SVF** (SVF-tools): LLVM 上的值流图框架,自动检测 use-after-free、double-free、buffer overflow。Core 的数据流图是更统一的形式——同一张图同时做 regalloc、调度、验证。 From 4cfee8cedf4da7056c1aa83b812c1b0179917b49 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Tue, 11 Aug 2026 00:33:26 +0900 Subject: [PATCH 7/9] =?UTF-8?q?docs:=20=E8=A7=84=E7=BA=A6=E7=B3=BB?= =?UTF-8?q?=E7=BB=9F=E8=AE=BE=E8=AE=A1=20v2=E2=80=94=E2=80=94CIC=20?= =?UTF-8?q?=E5=86=85=E6=A0=B8=20+=20SMT=20=E8=AF=81=E4=B9=A6=E6=9E=B6?= =?UTF-8?q?=E6=9E=84=20+=20=E9=AA=8C=E8=AF=81=E5=86=85=E6=A0=B8=E9=80=89?= =?UTF-8?q?=E5=9E=8B=20(#34)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - docs/spec-design.md 改版:v1 语言层完整保留,新增 v2 验证器架构(翻译桥/CIC 双通道/函数类型归属/用户入口分层/规约的回报-证明驱动优化) - docs/verifier-kernel.md 新增:理论谱系对比 + 2025-2026 论文扫描 + 融合架构(CIC 内核 + HoTT 库层 + McTT 验证 + 证书形态) - 全仓库 .md 清理 emoji(✅⏸⚠ 等) --- DEBUG_REPORT.md | 8 +- TODO.md | 10 +- docs/comptime.md | 14 +- docs/distributed.md | 6 +- docs/generics.md | 10 +- docs/ir-schema/coreir-schema.md | 2 +- docs/spec-design.md | 279 ++++++++++++++++-- .../plans/2026-08-08-region-cfg.md | 6 +- .../plans/2026-08-09-repo-governance.md | 2 +- .../2026-08-09-repo-governance-design.md | 12 +- docs/verifier-kernel.md | 102 +++++++ editor/README.md | 2 +- 12 files changed, 396 insertions(+), 57 deletions(-) create mode 100644 docs/verifier-kernel.md diff --git a/DEBUG_REPORT.md b/DEBUG_REPORT.md index 9e1edbf..34f0fba 100644 --- a/DEBUG_REPORT.md +++ b/DEBUG_REPORT.md @@ -3,7 +3,7 @@ > 日期: 2026-07-06 > PR: https://github.com/dslsdzc/core/compare/main...RhineIris:core:main > -> **⚠️ 历史存档**:本报告描述的问题均已在后续修复中解决—— +> ** 历史存档**:本报告描述的问题均已在后续修复中解决—— > 文中 3 个已修复 Bug 已合并(PR #9/#16 时期);"仍未解决的根本性 Bug" > (rip_patch 位置错位)已由 2026-07-23 P0 全量修复(`emit_instr()` disp32 > 写入补上当前指令基址)解决,corec2 → corec3 自举现已全程通过。 @@ -114,7 +114,7 @@ fn tokenize() { PATCH gvi=698 ppos=74669 off=5584 target=4736480 rel=467503 PATCH gvi=698 ppos=74751 off=5584 target=4736480 rel=467421 PATCH gvi=698 ppos=74845 off=5584 target=4736480 rel=467327 -... (16 total, all target=4736480 ✓) +... (16 total, all target=4736480 ) ``` - `off=5584` → 全部一致 @@ -188,8 +188,8 @@ syscall3(1, fd, g_elf_buf, sz); | 位置 | 期望值 | 实际值 | 状态 | |------|--------|--------|------| -| buf[500000] | 0x12345678 | 0x12345678 | 保留 ✓ | -| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖 ✗ | +| buf[500000] | 0x12345678 | 0x12345678 | 保留 | +| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖 | - 标记 1(位置 500000)→ **保留成功**,说明 buffer 在 elf_gen 返回后没有被整体污染 - 标记 2(位置 74717)和标记 3(位置 74717)→ **都被覆盖**,最终值是原始指令代码 diff --git a/TODO.md b/TODO.md index 9f26d61..920cf73 100644 --- a/TODO.md +++ b/TODO.md @@ -30,7 +30,7 @@ - emit_alloc_body 零初始化 + 链式扩容标记满 ### @ 内建原语(12 个全部完整) -- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量,ELF 验证 8 / 1 ✅ +- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量,ELF 验证 8 / 1 - `@fields(T)` — 遍历 struct fields,返回逗号分隔名字符串 - `@hasField(T, name)` / `@field(T, name)` — 结构体字段存在性 + 偏移量 - `@typeInfo(T)` — 类型名称字符串 @@ -84,10 +84,10 @@ RVSDG 式嵌套 region 已落地(规格 docs/superpowers/specs/2026-08-08-regi - 仅增加 mmap 扩容会让热缓存路径增长到约 7.6 GiB RSS 并触发 WSL OOM;需要按函数回收临时 IR/缓存数据,而不是继续扩大堆 ### 2. 并发集成:单 M 已端到端验证,多 M 未验证 -- ✅ `go f(args)` 端到端已通:`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper(不再依赖 rt.s 链接)→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传 -- ✅ 主线程注册为 G 0,可经 channel 阻塞/唤醒;sched_yield 不再重排 Gwaiting -- ⏳ M 线程 worker loop(m_start_workers)未连到调度器完整测试——静态构建尚未内联发射 m_start_workers(rt.s 符号) -- ⏳ channel wait queue 链表操作未在多线程并发下验证 +- `go f(args)` 端到端已通:`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper(不再依赖 rt.s 链接)→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传 +- 主线程注册为 G 0,可经 channel 阻塞/唤醒;sched_yield 不再重排 Gwaiting +- M 线程 worker loop(m_start_workers)未连到调度器完整测试——静态构建尚未内联发射 m_start_workers(rt.s 符号) +- channel wait queue 链表操作未在多线程并发下验证 - 注意:G 结构 offset 56 同时用作 saved_fn(goroutine.cr)与 temp_val(chan.cr 等待队列 handoff)——单 G 流程可用(wrapper 在 chan 操作前读取 saved_fn),但字段语义重叠,重构时需拆分 ### 3. 解释器局限 diff --git a/docs/comptime.md b/docs/comptime.md index 768af02..10ec328 100644 --- a/docs/comptime.md +++ b/docs/comptime.md @@ -54,8 +54,8 @@ comptime fn fibonacci(n: int) -> int { return fibonacci(n - 1) + fibonacci(n - 2); } -x := fibonacci(40); // ✅ 编译时算 -y := fibonacci(user_input); // ❌ 编译错误:comptime fn 需要已知参数 +x := fibonacci(40); // 编译时算 +y := fibonacci(user_input); // 编译错误:comptime fn 需要已知参数 ``` ## 可编译时执行的条件 @@ -64,8 +64,8 @@ y := fibonacci(user_input); // ❌ 编译错误:comptime fn 需要已知 | 执行条件 | 自动执行 | @comptime | |---------|---------|-----------| -| 纯函数,所有输入已知 | ✅ | ✅ | -| read_file,路径已知 | ✅ | ✅ | -| 有未知输入 | ❌ 留给运行时 | ❌ 编译错误 | -| 调用 FFI / volatile | ❌ | ❌ 编译错误 | -| 类型内省(@typeInfo 等) | — | ✅ | +| 纯函数,所有输入已知 | | | +| read_file,路径已知 | | | +| 有未知输入 | 留给运行时 | 编译错误 | +| 调用 FFI / volatile | | 编译错误 | +| 类型内省(@typeInfo 等) | — | | diff --git a/docs/distributed.md b/docs/distributed.md index 1d7dcb2..8c0e92a 100644 --- a/docs/distributed.md +++ b/docs/distributed.md @@ -86,9 +86,9 @@ go @("server2") worker(1); | 调用处 | 远端接口 | 结果 | |--------|---------|------| -| `fn(x: int) -> int` | `fn(x: int) -> int` | ✅ 匹配 | -| `fn(x: int) -> int` | `fn(x: int) -> string` | ❌ 不匹配 | -| `fn(x: int) -> int` | `fn(x: dyn) -> int` | ✅ dyn 兼容 | +| `fn(x: int) -> int` | `fn(x: int) -> int` | 匹配 | +| `fn(x: int) -> int` | `fn(x: int) -> string` | 不匹配 | +| `fn(x: int) -> int` | `fn(x: dyn) -> int` | dyn 兼容 | 不需要版本号。接口签名一致就能跑。版本号是人控制的,编译器只看接口类型。 diff --git a/docs/generics.md b/docs/generics.md index b939639..11f2b90 100644 --- a/docs/generics.md +++ b/docs/generics.md @@ -48,8 +48,8 @@ fn print_size(x: T) { 约束推导:编译器看图,发现 `x.size()` 调用,检查传入的实际类型是否有 `.size()` 方法。 ```core -print_size(42); // ❌ int 没有 .size() -print_size("hello"); // ✅ string 有 .len(),编译器推导约束匹配 +print_size(42); // int 没有 .size() +print_size("hello"); // string 有 .len(),编译器推导约束匹配 ``` ### 隐式约束推导 @@ -61,8 +61,8 @@ fn add(a: T, b: T) -> T { return a + b; // 编译器推导:T 必须支持 + 运算 } -add(1, 2); // ✅ int 支持 + -add("a", "b"); // ✅ string 支持 + +add(1, 2); // int 支持 + +add("a", "b"); // string 支持 + ``` ## 图上的实现 @@ -145,7 +145,7 @@ arr := make_array(); 编译器处理方式:`N` 被约束为 `int`,且在调用处必须是 `@comptime` 已知的编译时值。 ```core -make_array(); // ❌ 编译错误:泛型参数 N 需要编译时已知 +make_array(); // 编译错误:泛型参数 N 需要编译时已知 ``` ## 设计与替代方案 diff --git a/docs/ir-schema/coreir-schema.md b/docs/ir-schema/coreir-schema.md index 6e16306..c81e7eb 100644 --- a/docs/ir-schema/coreir-schema.md +++ b/docs/ir-schema/coreir-schema.md @@ -21,7 +21,7 @@ Core 编译器使用两种中间表示: .cir = 程序的数据流图 + 规约约束 ↓ 验证工具消费 .cir: - 1. 编译器已证明的约束(自动推导标签)标注为 ✓ + 1. 编译器已证明的约束(自动推导标签)标注为 2. 用户写的约束标注为 pending 3. 验证工具尝试证明 pending 约束 4. 输出:每个约束绿/黄/红 diff --git a/docs/spec-design.md b/docs/spec-design.md index 5a40dd0..ef5ae2f 100644 --- a/docs/spec-design.md +++ b/docs/spec-design.md @@ -1,6 +1,6 @@ -# Core 规约系统设计 +# Core 规约系统设计(v2 — CIC 内核 + SMT 证书架构) -> 规约 = 图上的约束。 +> 规约 = 图上的约束。表达力 = CIC(归纳构造演算)。自动化 = SMT 证书外包。 ## 一、哲学 @@ -16,15 +16,38 @@ corec build file.cr -s → .cir + .ccr + 自动生成 file.csp → .csr 验证 = 证明图的所有可达状态满足图上的约束。 ``` -**.csp 是编译器自动生成的:** -- 包含所有函数的声明骨架 + 自动推导标签 -- 用户在这个 `.csp` 里手写 `#check` / `#ensure` / `spec fn` -- 下次 `-s` 重新生成:新函数加入、删除的函数移除、已有手写规约保留 -- 版本管理:`.csp` 应该入版本库 +## 二、架构总览(v2) -`.csr` 是将 `.csp` 中的规约约束(check/ensure/invariant/spec fn)编译为 TagNode 元数据的二进制序列化,与 `.cir`(DFNode)配套供验证工具消费。 +规约语言(一套 Core 语法)编译为 **CIC 项**(归纳构造演算),验证走双通道: -## 二、平民化原理 +``` +Core 规约语言(.corespec / .csp / .cr 内联) + ↓ 编译(翻译桥:命令式 → 函数式) +CIC 项(归纳构造演算——一切表达力:量词/归纳/依赖类型/递归性质) + ├─ 目标一阶可表达 → SMT 通道(自动求解 + 用户可选 #smt) + │ → SMT 返回证书(证明轨迹) + │ → 翻译成 CIC 证明项 → 内核重新验证 ← 健全性永远在内核 + └─ 归纳/高阶 → CIC 内核直接处理 +``` + +**健全性唯一来源是 CIC 内核。** SMT 是证明搜索器(可以凭启发式甚至不健全地猜),其输出必须经内核验证才被接受——证书校验失败即拒绝,绝不引入不健全。这是 SMTCoq 模式(CAV'17,先例)。 + +### 表达力边界 + +CIC 提供 Coq 级别的全部表达力,逐项对应: + +| 能力 | CIC 承担 | Core 用户付出 | +|---|---|---| +| 全称/存在量词(无限域) | `forall/exists` 是语言一等构造 | 零——量词是规约语言语法 | +| 归纳类型 + 归纳原理 | 枚举/结构体 → 归纳类型,原理在内核 | 零 | +| 递归函数 + 终止性 | 递归定义 + `loop variant` 标注 | 变体标注(EBNF 已有) | +| 高阶量词(∀f: int→int) | 函数空间原生可量化 | 零(规约层函数类型,见 §10) | +| 依赖类型(`Vec n`) | 内核有,**但 Core 不需要** | 被图验证替代:边界安全由图保证,长度性质由谓词表达(`#ensure(result.len() == |a|)`) | +| 引理/定理复用 | 证明项可组合 | 见 §12 用户入口 | + +**Core 对依赖类型的替代**:Coq 用 `Vec n` 在类型层面保证索引不越界/长度匹配;Core 里这两个需求已被其他机制消化——索引越界由指针模型图验证保证(已实现),长度性质由谓词表达。安全性由图承担,性质由谓词承担——这就是 Core 不用付出依赖类型学习成本的根源。 + +## 三、平民化原理 **不需要写公式,不需要学数理逻辑。规约用 Core 语言本身书写。** @@ -38,7 +61,7 @@ corec build file.cr -s → .cir + .ccr + 自动生成 file.csp → .csr 三个层级最终都编译为 `.cir` 的规约 DFNode(条件表达式)+ `.csr` 的 TagNode(约束元数据),对验证工具无差别。 -## 三、文件格式 +## 四、文件格式 ### `.cr` — 实现源码(也可内联规约) @@ -109,7 +132,7 @@ spec fn vec_invariant[T](v: Vec[T]) -> bool { 每条 `#check`、`#ensure`、`#invariant` 以及每个 `spec fn` 的身体,都编译为 `.cir` 的规约 DFNode(条件表达式)+ `.csr` 的 TagNode(约束元数据:类型、验证状态、行列号)。TagNode 通过 `target_node` 指向 `.cir` 中对应的 DFNode,通过 `condition_node` 指向条件表达式所在的 DFNode。 -## 四、编译器自动推导(零门槛的核心) +## 五、编译器自动推导(零门槛的核心) 编译器从 `.cir` 图结构中自动推导性质,写入 `.csr`,不需要用户写任何东西。 @@ -159,7 +182,7 @@ fn transfer(from: &mut Account, to: &mut Account, amt: int) **模式匹配库可扩展**:社区可以贡献新的图模式 → 标签映射,编译器新增推导能力。 -## 五、标签语法(标注/annotation) +## 六、标签语法(标注/annotation) 使用 `#` 前缀,与 `@`(外部项目引用)区分。 @@ -180,7 +203,7 @@ fn foo() -> int - 不占用 `@`(后者保留给 `import @project`) - 语义清晰:`#` 标记的东西不影响运行时语义 -## 六、检查函数(规约的主力) +## 七、检查函数(规约的主力) 检查函数是用 Core 语言写的纯函数,返回值是 `bool`。它们被编译为 `.cir` 图,然后与实现函数的 `.cir` 并列供验证器消费。 @@ -222,19 +245,198 @@ spec fn all_nonneg(arr: [int]) -> bool = forall x in arr: x >= 0; ``` -## 七、约束的验证 +## 八、量词(v2 新增) + +`forall x: int => P(x)` 必须是规约语言的一等构造(**不是** for 循环的翻译)——int 域无限,遍历不了;for 循环只是有限域的便利糖(§7 纯公式支持的 `forall x in arr` 是有限域情形)。 + +```core +// EBNF 已定义(grammar/corespec.ebnf) +forall (x: int) => x >= 0 +exists (i: int) => a[i] == target +``` + +## 九、翻译桥:spec fn(命令式)→ CIC 项(函数式)(v2 新增) + +### 9.1 问题定义:两个语言的语义鸿沟 + +spec fn 用 Core 书写——命令式:变量重复赋值、循环、数组、`return`。CIC 是纯函数式逻辑:lambda 演算、递归定义、归纳类型、没有赋值没有循环。翻译桥把前者确定性变换为后者,**不丢语义、不加语义**。 + +可行的根本保障:spec fn 是纯的(project-book:"规约表达式限于纯逻辑运算"——无副作用、无 IO、无 unsafe、无外部调用)。纯命令式程序与函数式程序的翻译是经典确定性问题。 + +### 9.2 结构翻译表(Core 构造 → CIC 构造) + +| Core 构造 | CIC 翻译 | 示例 | +|---|---|---| +| `x := expr` / 单次赋值 | `let x = expr in ...` | `total := 0` → `let total = 0 in ...` | +| 重复赋值 `x = expr` | SSA 化 → 递归参数传递 | `x = x + 1` → 递归调用参数 `f(x+1)` | +| `return expr` | 直接表达式化 | 函数体即表达式 | +| `if/else` | 条件表达式(ite/match) | `if b { A } else { B }` → `if b then A else B` | +| `for x in arr` | fold/递归遍历 | `for x in arr: acc += x` → 对 list 递归 | +| `for i in 0..n` | 有界递归(参数递减) | 变体 = `n - i` | +| `loop { ... }` + `break` | 尾递归(需要变体) | 变体标注(EBNF 已有) | +| 数组 `a[i]` 读写 | 归纳列表索引 / 数组理论 select-store | 或带长度约束的结构 | +| 结构体/枚举 | 归纳类型构造子 + match | `Point{x, y}` → `mk_point x y` | +| 递归调用 | CIC 递归定义(良基递归) | `fact(n) = n * fact(n-1)` | + +核心模式——循环即递归: + +``` +for i in 0..n: acc += a[i] + ↓ +f(acc, i) = if i >= n then acc + else f(acc + a[i], i + 1) // 变体 = n - i,递减保证终止 +``` + +### 9.3 终止性:变体是翻译的前提 + +CIC 只接受**良基递归**(递归参数严格递减)——非终止的"递归"在 CIC 里无法定义。因此: + +- 每个循环/递归翻译必须携带**变体**(loop variant,EBNF 已有)——递减度量 +- 编译器自动推导(§五 的 `#terminating` 图模式)优先;推导不出的要求用户标注 +- 无变体的循环 → 翻译失败(编译错误),或降级为未解释函数(用户确认语义) + +### 9.4 整数语义:机器整数 vs 数学整数(关键决策) + +Core 的 `int` 是 64 位机器整数(会溢出),CIC 的整数是数学整数(Z,无界)。**翻译桥必须选择规约里的整数语义**: + +| 选项 | 语义 | 代价 | +|---|---|---| +| 数学整数(默认) | 规约性质在无界整数上证明 | 简单;但 `#ensure(x + y > x)` 在数学域成立、机器域可能因溢出失败——**证明的结论可能不反映实际行为** | +| 机器整数(位向量) | 精确匹配运行语义(SMTCoq 已支持位向量理论) | 复杂;需要位向量 + 溢出模式建模,证明义务更繁 | +| 混合 | 默认数学整数;位宽相关性质用显式位向量类型标注 | 平衡;用户只对溢出敏感的性质声明位宽 | + +**待定**:默认数学整数 + 显式位宽标注(混合方案)是倾向方向,与内核选择(§十七)一并决策。 + +### 9.5 实现函数进规约的身份 + +`#ensure(f(x) == y)` 引用实现函数 f——f 不是 spec fn,是运行时代码。它的 CIC 身份是**语义模型**: + +- 函数式子集(纯、可翻译)→ 翻译为递归定义(与 spec fn 同路径) +- 其余(有副作用/未翻译)→ **未解释函数**(Uninterpreted Function):CIC 只知道签名,不知道定义——性质只能由用户另行声明 +- 有副作用/非纯的实现函数不能进规约(project-book 规定) + +### 9.6 失败情形(翻译不了怎么办) + +| 情形 | 处理 | +|---|---| +| 循环无变体 | 编译错误(要求 `variant` 标注)或降级未解释函数 | +| 数组索引可能越界 | 翻译时插入越界条件(`i < len`),越界路径 → 未定义值(⊥) | +| 副作用/IO/unsafe | 翻译拒绝——规约只能引用纯函数 | +| 溢出敏感性质 | 显式位宽标注(见 9.4) | + +## 十、函数类型归属(v2 决策:规约专属) + +函数类型在两个层面是两个不同的东西,**必须拆分决策**: + +| | 规约层 | 实现层 | +|---|---|---| +| 函数是什么 | 数学对象(映射)——CIC 的 lambda | 运行时对象(代码/闭包) | +| 机制 | 箭头类型 `int -> int` → CIC 原生 | TYP_FN + 闭包/捕获/调用约定 | +| 需求 | 高阶量词 `forall f: int -> int => P(f)` | 函数值编程(map/filter 传函数、回调表) | + +**决策:规约专属函数类型。** `int -> int` 只存在于规约语言(`.corespec` 类型宇宙的一部分),直接映射 CIC 箭头;量化的是数学函数,不需要实现层有函数值。零污染 Core 语言(checker/ir_gen/后端/内存模型不动),符合"规约是独立源文件"的哲学。 + +**实现层函数值(TYP_FN/闭包)按 YAGNI 挂起**:现状 `@addr(f)` + int 能表达函数地址(内核函数表、中断向量表);闭包与 arena 内存模型(捕获变量归属)交互复杂,无真实用例不做。 + +## 十一、验证器:CIC 内核 + SMT 证书(v2 新增) + +> 内核选型与融合架构的完整论证见 `docs/verifier-kernel.md`(理论谱系、2025–2026 论文扫描、融合决策、自举路线)。 + +### 内核 + +CIC 类型检查器(Coq 内核级别:约数千行的信任根)。初期绑定成熟实现,后期自举为 Core 版(见 §14 与 `docs/verifier-kernel.md`)。 + +### SMT 通道(证书架构,SMTCoq 模式) + +``` +目标(CIC 项) + → 一阶化翻译(数组/算术/UF 理论) + → SMT 求解器(Z3/veriT/CVC5 类) + → 证书(unsat 证明/求解轨迹) + → 翻译成 CIC 证明项(refl/omega/... 构造) + → CIC 内核重新验证 ← 健全性唯一来源 +``` + +- SMT 不求信任:可以跑不健全启发式,证书校验失败即拒绝 +- 用户可**主动选择** SMT:目标标注 `#smt`(hammer 的手动挡) +- 覆盖范围:线性算术、数组边界、位向量、UF——"绝大多数";SMT 表达不了的目标(归纳/高阶)直接走内核——**表达力边界由 CIC 决定,SMT 只是加速器** + +### 反例调试 + +SMT 解不出时返回**反例模型**(哪个输入违反性质)——开发期黄金能力:`#check(b != 0)` 被违反 → SMT 给出 `b = 0` 的具体反例。验证报告区分三种状态:**绿**(证明)/ **黄**(部分)/ **红**(反例或未证明)。 + +## 十二、约束的验证与用户入口 验证器(外部贡献)的操作: 1. 加载 `.cir`(程序图)+ `.csr`(图上约束) 2. 从图结构推导自动标签(标签 = 编译器已证明) -3. 对 `#check`/`#ensure`:生成证明义务 → SMT / 溯因推理 / 归纳 +3. 对 `#check`/`#ensure`:生成证明义务 → SMT 通道 / CIC 内核 4. 对 `spec fn`:检查实现函数的图是否蕴含检查函数的图 -5. 输出:每条约束绿(证明)/ 黄(部分证明)/ 红(未证明) +5. 输出:每条约束绿(证明)/ 黄(部分证明)/ 红(反例或未证明) 约束可以同时在开发期插桩运行时 assert 检查,验证器到位前也有保障。 -## 八、完整管线 +### 用户入口分层(自动化失败时降级,v2 新增) + +| 层 | 入口 | 用户要做什么 | 学习成本 | +|---|---|---|---| +| 0 | 默认全自动 | 什么都不做 | 零 | +| 1 | `#induct x` 归纳引导 | 标注"对哪个变量做结构归纳" | 一句话 | +| 2 | `#lemma` 引理拆解 | 写中间性质(Core 规约语言) | 理解"拆解"思维 | +| 3 | CIC 证明项逃逸 | 直接给证明项 | 高(最后手段,对应 unsafe 的位置) | + +- 层 1 本质:生成 CIC 归纳原理实例化(基例 + 归纳步两个目标),各回自动化——归纳框架是 CIC 的,步骤求解是 SMT 的 +- 层 3 远期演化:Core 自举 CIC 内核成熟后,可变成"用户用 Core 写证明"(Curry-Howard 在 Core 呈现) + +### .csr 状态 + +`.csr` 的 status 字段(0=unproven, 1=auto_proven, 2=user_proven)承接验证结果: + +| 来源 | status | +|---|---| +| 编译器自动推导标签 | auto_proven | +| SMT 证书经内核验证 | user_proven | +| 用户入口产物 | user_proven | +| 未证明 | unproven(不拦编译——证明失败 ≠ 程序不安全) | + +## 十三、规约的回报:证明驱动的优化(v2 新增) + +**写的证明越多,编译器优化越狠。** 规约不只是验证负担——证明过的性质流入优化器,成为激进变换的前提。这是"语义保鲜"的闭环:用户注入的语义(规约)流经验证变成**可证明的事实**,再流进优化器,验证的回报不只是安全,还有性能。 + +### 机制:证明状态门控的优化信息流 + +``` +用户写规约 → 验证(SMT/内核)→ 状态 proven / unproven + │ + proven 的性质 ──┼──→ 优化 pass(变换前提) + unproven 的性质 ──→ 丢弃(绝不喂优化器) +``` + +**关键:只有被证明的性质才进优化器。** `.csr` 的证明状态(auto_proven / user_proven)就是优化器的许可证——unproven 的性质可能为假,喂给优化器 = 优化器引入 bug。**证明错误 = 优化错误,门控是机制核心。** + +### 收益清单(证明 → 优化映射) + +| 证明的性质 | 优化器能做什么 | +|---|---| +| `#check(b != 0)` 已证 | 除法免零检查 | +| `#safe_index` 已证 | DEREF 运行时边界检查(cmp+jae+ud2)直接消除——编译期证明免检的规约版,覆盖运行时数组 | +| `#pure` 已证 | CSE / 死代码删除 / 重排(纯调用可删可移) | +| `#no_alloc` 已证 | 栈分配替代堆分配 | +| `loop invariant` + `#terminating` 已证 | 循环变换(向量化/强度削减/展开)前提满足 | +| 指针分离/别名规约已证 | 内存访问重排(否则保守不重排) | +| `#deterministic` 已证 | 更激进的缓存/重算策略 | + +### 动机闭环 + +**规约从"验证负担"变成"性能投资"**——普通程序员为性能写 `#check`/`#ensure`,验证顺手完成。这解决了"为什么要写规约"的动机问题。先例:LLVM 的 `llvm.assume`(用户声明的事实喂优化器)。 + +### 两个注意点 + +1. **编译器内部回读通道**:`.csr` 现在只服务外部验证器——需要编译器内部读取已证性质表(管线:编译 → 规约 → 证明 → 已证性质表 → 优化 pass) +2. **证明时效**:代码改动后证明需重验——增量缓存已有函数级 `.cir` 缓存,证明缓存同理 + +## 十四、完整管线 ``` # 编译(无规约) @@ -258,8 +460,8 @@ corec build file.cr -s # 验证(外部工具) verify file.csr → 加载 .cir + .csr - → 验证 pending 约束 - → 输出验证报告 + → 验证 pending 约束(SMT 通道 / CIC 内核) + → 输出验证报告(绿/黄/红) ``` 编译器输出的 `.csr` 包含: @@ -267,7 +469,15 @@ verify file.csr - 用户写的 `#check/#ensure/#invariant`(status=pending) - `spec fn` 编译为 spec 图节点(status=pending) -## 九、内核场景的应用 +## 十五、信任根与自举路线(v2 新增) + +验证的信任根是 CIC 内核——内核有 bug = 一切证明皆空。路线(与 corec 自举同构): + +1. **初期**:绑定成熟内核(候选:Rocq / Lean 4,决策挂起,见 §16) +2. **自举**:有人用 Core 写出 CIC 内核版本 → 替换外部依赖 +3. 先例:Coq Coq Correct!(被 Coq 证明正确的 Coq 内核)、Milawa(链式自举:A 验证 B,B 验证 C…,信任降到最小可审计内核) + +## 十六、内核场景的应用 普通开发者的代码:编译器自动推导 + 可能几行 `#ensure`。 @@ -302,12 +512,39 @@ fn map_page(pt: &mut PageTable, virt: Addr, phys: Addr, flags: u64) 内核的量词(`for all mappings`)写成了 `for` 循环,编译器把它编译成纯逻辑约束。纯公式语法糖(`forall`)也存在,但只是编译器的展开。 -## 十、总结 +## 十七、实现里程碑(建议) + +1. `.corespec` 解析(量词/函数类型/变体)+ 规约类型检查 +2. 翻译桥:spec fn → CIC 项(循环→递归、数组→归纳列表) +3. SMT 通道:目标翻译 + 证书校验 + 内核验证(绑定内核起步) +4. 用户入口:`#induct` → `#lemma` → 逃逸 +5. 自举 CIC 内核(Core 版) + +## 十八、开放决策点(挂起,待外部贡献者参与) + +| 决策点 | 状态 | +|---|---| +| **内核选择:Rocq vs Lean 4** | 挂起——两者都是 CIC 类,规约语言/SMT 证书/翻译桥/自举路线不受影响,等社区参与 | +| 实现层函数值(TYP_FN/闭包) | YAGNI 挂起,等真实用例 | +| 证明项逃逸的最终形态 | 随内核选择与自举进度演化 | + +## 十九、总结 ``` 不需要学新语言 ── 规约 = Core 函数 不需要写公式 ── 编译器从图推导能推导的一切 不需要自己来 ── 剩下的用同一门语言写检查函数 +表达力无上限 ── 编译为 CIC,量词/归纳/高阶全在内核 +健全性有保证 ── SMT 证书经内核验证,信任根最小化 ``` 完全形式化的代价被压缩到最低:只有编译器推导不了的函数正确性需要手写检查函数,而检查函数本身也是 Core 代码,不是数理逻辑公式。 + +## 参考 + +- **SMTCoq**(Ekici/Mebsout/…, CAV'17)— SMT 证书 → Coq 证明项,求解器不可信、健全性只在内核 +- **Why3**(POPL'24 论文)— 中间验证语言:一套规约语言编译到 SMT + Coq 多后端 +- **Liquid Types / LiquidHaskell**(Jhala 系)— 谓词表达性质 + SMT 自动证明义务 +- **Sledgehammer**(Blanchette 系)— 外部证明器找证明 → 在内核重建(LCF 哲学) +- **Coq Coq Correct!**(Sozeau 等, 2020)— 被 Coq 证明正确的 Coq 内核 +- **Milawa / Self-certification**(POPL'12)— 链式自举,信任降到最小可审计内核 diff --git a/docs/superpowers/plans/2026-08-08-region-cfg.md b/docs/superpowers/plans/2026-08-08-region-cfg.md index 78a08d2..f5f4595 100644 --- a/docs/superpowers/plans/2026-08-08-region-cfg.md +++ b/docs/superpowers/plans/2026-08-08-region-cfg.md @@ -758,7 +758,7 @@ jj commit -m "feat: RegionCheck via explicit node→region mapping + docs sync ( ## Self-Review(执行前自查) -- **规格覆盖**:P1(SG_IF+映射+DOT)→ Task 1/2;P2(region 迭代)→ Task 3;P3(state edges)→ Task 4;P4(序列化 v2)→ Task 5;P5(RegionCheck+回归+文档)→ Task 6。规格第 11 节文档同步 → Task 6 Step 5 ✓ -- **类型一致**:`g_df_node_region`/`g_cur_sg`/`g_loop_region_*`/`OFF_DFE_KIND`/`SG_IF` 在各 Task 定义处与使用处一致 ✓ -- **全局约束**:所有长任务命令带 `nice -n 19`;提交用 `jj` ✓ +- **规格覆盖**:P1(SG_IF+映射+DOT)→ Task 1/2;P2(region 迭代)→ Task 3;P3(state edges)→ Task 4;P4(序列化 v2)→ Task 5;P5(RegionCheck+回归+文档)→ Task 6。规格第 11 节文档同步 → Task 6 Step 5 +- **类型一致**:`g_df_node_region`/`g_cur_sg`/`g_loop_region_*`/`OFF_DFE_KIND`/`SG_IF` 在各 Task 定义处与使用处一致 +- **全局约束**:所有长任务命令带 `nice -n 19`;提交用 `jj` - **已知不确定点**:Task 3 复现测试若与预期失败模式不符,以实际输出为准修正(步骤已注明);Task 5 的 v4 存档文件若无现成产物则跳过兼容测试并在提交注明 diff --git a/docs/superpowers/plans/2026-08-09-repo-governance.md b/docs/superpowers/plans/2026-08-09-repo-governance.md index f7d833e..715f28d 100644 --- a/docs/superpowers/plans/2026-08-09-repo-governance.md +++ b/docs/superpowers/plans/2026-08-09-repo-governance.md @@ -514,7 +514,7 @@ jj log -r main@origin --no-graph -T 'commit_id.short()' && jj log -r develop@ori - [ ] **Step 4: 收尾核对 spec §12 状态清单** -全部 ⬜ 项变为 ✅(本地配置、develop、ruleset、签名密钥、首个 PR)。剩余 ⬜(CI 完整层点亮、opt-regress)属后续项,在 spec §11 跟踪。 +全部 项变为 (本地配置、develop、ruleset、签名密钥、首个 PR)。剩余 (CI 完整层点亮、opt-regress)属后续项,在 spec §11 跟踪。 --- diff --git a/docs/superpowers/specs/2026-08-09-repo-governance-design.md b/docs/superpowers/specs/2026-08-09-repo-governance-design.md index fa066a8..59528b6 100644 --- a/docs/superpowers/specs/2026-08-09-repo-governance-design.md +++ b/docs/superpowers/specs/2026-08-09-repo-governance-design.md @@ -157,9 +157,9 @@ gh pr create --base main --fill # develop→main PR(required reviewers = ## 12. 当前状态 -- ✅ CI 骨架:已实现(2026-08-09),本地验证通过,随首个 PR 上线 -- ✅ 社区四件套:PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写(2026-08-09),随本 spec 首 PR 上线 -- ✅ 本地配置:jj protect / jj 签名(behavior=own)/ hook / settings 清理 / CLAUDE.md——全部落地(2026-08-09) -- ✅ `develop` 集成分支已创建并承载 PR #25 -- ✅ GitHub ruleset:**main-only-maintainer**(id 20601201)+ **develop-integration**(id 20601189)已创建并 active(2026-08-09);gh TLS 间歇性故障期间以重试创建成功;squash-only(allowed_merge_methods=['squash'])已应用于双 ruleset;delete_branch_on_merge=True 已设 -- ✅ 首个 PR(#25 → develop)与发布 PR(#26 → main,B 流程)已完成;治理全流程端到端验证 +- CI 骨架:已实现(2026-08-09),本地验证通过,随首个 PR 上线 +- 社区四件套:PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写(2026-08-09),随本 spec 首 PR 上线 +- 本地配置:jj protect / jj 签名(behavior=own)/ hook / settings 清理 / CLAUDE.md——全部落地(2026-08-09) +- `develop` 集成分支已创建并承载 PR #25 +- GitHub ruleset:**main-only-maintainer**(id 20601201)+ **develop-integration**(id 20601189)已创建并 active(2026-08-09);gh TLS 间歇性故障期间以重试创建成功;squash-only(allowed_merge_methods=['squash'])已应用于双 ruleset;delete_branch_on_merge=True 已设 +- 首个 PR(#25 → develop)与发布 PR(#26 → main,B 流程)已完成;治理全流程端到端验证 diff --git a/docs/verifier-kernel.md b/docs/verifier-kernel.md new file mode 100644 index 0000000..d5ce3b0 --- /dev/null +++ b/docs/verifier-kernel.md @@ -0,0 +1,102 @@ +# 验证内核选型与融合架构(Verifier Kernel) + +> 信任根 = CIC 内核。表达力 = CIC + 公理 + HoTT 库。自动化 = 证书形态(计算在外、健全性在内)。 +> 融合各家之长,不选边——每个维度取最优,其他体系全部变成方法贡献。 + +## 一、问题 + +规约系统(`docs/spec-design.md`)需要 Coq 级别的表达力(依赖类型/归纳/高阶量词)。表达力由**验证内核**承载——内核是信任根:**内核有 bug = 一切证明皆空**。本文档记录内核选型论证与融合架构决策(2026-08-10)。 + +## 二、理论体系全谱系(选型时的候选) + +| 体系 | 代表 | 表达力 | 内核规模 | 数学完备性 | 自动化生态 | +|---|---|---|---|---|---| +| **CIC**(归纳构造演算) | Rocq / Lean 4 | 依赖类型+归纳+高阶 | 中等(Rocq 7.8k 行 / **Lean 3k 行**) | 函数外延性/商类型要公理 | SMTCoq(Rocq)、hammer | +| **MLTT**(Martin-Löf) | Agda / McTT | 同 CIC 族(归纳族更精确) | 中等 | 同 CIC | 弱 | +| **HoTT/Cubical** | Cubical Agda、redtt | + 商类型/外延性定理可证 | 大(归一化复杂) | 理论最优 | 生态小 | +| **HOL**(简单类型论) | Isabelle/HOL、HOL Light | 无依赖类型(表达力上限) | 极小(HOL Light ~500 行) | 外延性天然 | sledgehammer 最强 | +| **LF/公理拼装** | Metamath | 靠公理 | 极小(~600 行) | 依赖公理集 | | + +**选型结论**:对 Core 的约束(依赖类型表达力 + 自举路线 + SMT 证书架构)—— +- 理论最优是 HoTT,**工程最优是 CIC 系** +- HOL 系出局(无依赖类型);MLTT 与 CIC 同族(CIC 的归纳类型更完整);HoTT 的完备性用公理 + 库层补 +- CIC 系中 Lean 4 内核(~3k 行)是自举最友好的实现 + +## 三、2025–2026 最新扫描(无全新竞争体系,全新的是方法) + +| 工作 | 年份 | 贡献 | 对 Core 的意义 | +|---|---|---|---| +| **McTT**(Jang/Gaulin/Hu/Pientka, ICFP'25) | 2025 | **全验证**的 MLTT 内核(含 NbE 归一化证明,OCaml 提取;除 lexer/pretty-printer 全管线验证) | 内核"全验证"从口号变工程——自举路线终点的参考方法 | +| **Andromeda 2**(Bauer/Petković) | 2022+ | **证书内核形态**:归一化/等式检查在内核外,内核只构造 judgement + 验证证书;用户可定义理论 | 与 SMT 证书架构**同构**——确认"计算在外、健全性在内"是当代前沿 | +| **Definitional Proof Irrelevance**(Felicissimo 等, LICS'26) | 2026 | CIC + 观察等式 + 严格命题(定义性证明无关),一致性与 canonicity 证明,Rocq 实现 | CIC 系在活跃演进(不是停滞旧技术) | +| **Lean4Less**(Vaishnav, 2026) | 2026 | Lean 内核缩小化翻译(去掉 K 归约等便利定义性等式,Lean− 更小理论) | 抄 Lean 内核可抄缩小版——内核最小化参考 | +| **Lean 内核 bug 事件**(Collatz/AI) | 2025 | AI 利用嵌套归纳类型的**无规范内核 bug** 产出假证明;外部检查器复制同一 bug(代码即规范) | **教训:自举内核必须有正式规范**——先规范后实现,或用 Rocq 验证(MetaRocq 路径) | + +**扫描结论**:没有推翻 CIC 的全新理论体系;全新的是**内核形态**(证书化、验证化)和**元方法**(NbE 验证)——全部可以吸收进既有架构。 + +## 四、融合架构(决策,2026-08-10) + +不选边——**每个维度取最优,其他体系降级为方法贡献**: + +``` +┌─ 内核层(信任根)───────────────────────────────────┐ +│ CIC(Lean 4 风格,~3k 行,可 Lean4Less 式缩小化) │ +│ ├─ 表达力:依赖类型/归纳/高阶量词 ← CIC 原生 │ +│ ├─ 理论扩展:公理层 + HoTT 库(用 CIC 证明 HoTT) │ +│ │ ← Voevodsky 路线(HoTT/Coq、UniMath 先例) │ +│ └─ 远期:McTT 式 NbE 全验证(自举后给内核机械证明) │ +│ ← ICFP'25 McTT │ +└────────────────────────────────────────────────────┘ +┌─ 验证层(计算在外,内核只验证证书)─────────────────┐ +│ ├─ SMT 证书 → 证明项 → 内核验证 ← SMTCoq (CAV'17) │ +│ ├─ 归一化/等式检查外置,judgement 证书化 │ +│ │ ← Andromeda 2(同构确认) │ +│ └─ 复杂检查器反射化(库层实现 + 一次证明) │ +│ ← SMTCoq 检查器模式 │ +└────────────────────────────────────────────────────┘ +``` + +### 决策要点:三个维度各自最优,互不妥协 + +| 维度 | 取谁的 | 为什么 | +|---|---|---| +| 信任根 | CIC 内核(最小)+ McTT 验证方法(远期机械证明) | 表达力 + 可验证性兼得 | +| 表达力 | CIC + 公理 + HoTT 库(不换理论,挂载) | 数学完备性用库层拿,内核零增长 | +| 自动化 | 证书形态(SMTCoq + Andromeda 同构) | 计算在外、健全性在内——与自举/验证路线天然兼容 | + +### 为什么 HoTT 不换内核:用 CIC 证明 HoTT + +- HoTT/Coq 与 UniMath 的先例:标准 CIC 内核 + Univalence 公理(Voevodsky 模型证明一致) +- 公理化 UA 不可计算(含 UA 消除的证明项归一化会 stuck)——但**日常规约验证不用 UA**,它只在数学库层需要——工程分层天然隔离 +- Lean 4 内核原生支持 quotient + proof irrelevance(Rocq 无)——Lean 内核 + UA 公理 ≈ 更完整的 HoTT 基础 +- 结论:**HoTT 是挂在 CIC 上的公理 + 库层,不是竞争体系** + +## 五、信任根与自举路线 + +1. **初期**:绑定成熟内核(候选:Rocq / Lean 4,开放决策) +2. **自举**:用 Core 写出 CIC 内核(Lean 4 风格,可缩小化)→ 替换外部依赖(与 corec 自举同构) +3. **验证**(远期):McTT 式 NbE 全验证——给自举内核机械正确性证明 +4. **规范先行**(内核 bug 事件教训):自举内核**先有正式规范,后实现**——避免"代码即规范";规范可用 Rocq 验证(MetaRocq 路径) + +先例:Coq Coq Correct!(被证明正确的 Coq 内核)、Milawa(链式自举:A 验证 B,B 验证 C…)、McTT(全验证管线)、MetaRocq / lean4lean / agda-core(验证内核进行中——"验证内核时代即将到来")。 + +## 六、开放决策点(挂起,待外部贡献者参与) + +| 决策点 | 状态 | +|---|---| +| **内核选择:Rocq vs Lean 4** | 挂起——两者都是 CIC 类,规约语言/SMT 证书/翻译桥/自举路线不受影响,等社区参与 | +| 整数语义(数学整数 vs 机器整数,见 spec-design §9.4) | 倾向"默认数学整数 + 显式位宽标注",与内核选择一并决策 | +| 自举内核的规范语言 | 随自举进度演化(候选:Core 规约语言自身 / Rocq) | +| 证明项逃逸的最终形态 | 随内核选择与自举进度演化 | + +## 参考 + +- **SMTCoq**(Ekici/Mebsout/…, CAV'17)— SMT 证书 → Coq 证明项,求解器不可信、健全性只在内核 +- **McTT**(Jang/Gaulin/Hu/Pientka, ICFP'25)— 全验证 MLTT 内核,NbE 归一化证明,OCaml 提取 +- **Andromeda 2**(Bauer/Petković Komel, LMCS'22)— 证书内核形态:归一化在内核外,judgement 证书化,用户可定义理论 +- **Definitional Proof Irrelevance Made Accessible**(Felicissimo 等, LICS'26)— CIC + 观察等式 + 严格命题 +- **Lean4Less**(Vaishnav, 2026)— Lean 内核缩小化翻译(extensional-to-intensional) +- **Coq Coq Correct!**(Sozeau 等, 2020)— 被 Coq 证明正确的 Coq 内核 +- **Milawa / Self-certification**(Strub 等, POPL'12)— 链式自举,信任降到最小可审计内核 +- **MetaRocq / lean4lean / agda-core** — 验证内核进行中项目(INRIA 2026 综述) +- **HoTT/Coq、UniMath** — CIC + Univalence 公理形式化 HoTT 的先例 diff --git a/editor/README.md b/editor/README.md index f92c861..6ba0b6b 100644 --- a/editor/README.md +++ b/editor/README.md @@ -20,7 +20,7 @@ cp -r editor/nvim/plugin/*.lua ~/.config/nvim/lua/plugins/ |------|----------|------| | 语法高亮 | 自动 | `.cr`/`.cir`/`.ccr` 文件 | | 代码补全 | 自动 | blink.cmp 关键字 + types | -| 代码片段 | `fn⭾` `struct⭾` 等 | 共 20+ 片段 | +| 代码片段 | `fn` `struct` 等 | 共 20+ 片段 | | 诊断 | 保存时自动 | 编译器错误显示在行内 | | Quickfix | `:make` | 编译结果 + 错误列表 | | 悬浮信息 | `K` | 查看标识符定义 | From bc42144ad147d53f1ba682bd78294676b97b310a Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Tue, 11 Aug 2026 16:36:21 +0800 Subject: [PATCH 8/9] =?UTF-8?q?feat:=20float=20=E5=AE=8C=E6=95=B4=E6=94=AF?= =?UTF-8?q?=E6=8C=81=EF=BC=88IEEE=20754/SysV=EF=BC=89+=20=E5=AF=B9?= =?UTF-8?q?=E7=85=A7=20CompCert=20=E5=AE=A1=E6=9F=A5=E4=BF=AE=E5=A4=8D=201?= =?UTF-8?q?6=20bug?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - float:字面量(IEEE754 位模式)/ 算术(SSE2)/ 比较 / 转换 / 参数(XMM0-7)/ 打印 - 修复越界检查链:ptr_analysis ADDR_INDEX offset 传播、alloc pts 独立位、 STORE 传播(d=-1 永不执行)、IR_DEREF 编码 3 错、provenance 诊断不拦截、 region_check 位号语义错(B11 误报) - 修复 alloc 死循环(jbe 偏移 +17)、栈帧 16 字节对齐(SysV) - 修复 .ccr s1 截断 32 位(大常量/float 位模式静默损坏)+ buf_read_i64 高位丢失 - 审查/实现记录:docs/compcert-reference.md、TODO.md、docs/coq/、coq/fmt_int.v --- .lia.cache | Bin 0 -> 125 bytes TODO.md | 16 +++ coq/.fmt_int.aux | 29 +++++ coq/fmt_int.glob | 172 ++++++++++++++++++++++++ coq/fmt_int.v | 115 ++++++++++++++++ coq/fmt_int.vo | Bin 0 -> 23643 bytes coq/fmt_int.vok | 0 coq/fmt_int.vos | 0 docs/compcert-reference.md | 139 ++++++++++++++++++++ docs/coq/README.md | 101 +++++++++++++++ src/arch/linux/ld/elf.cr | 61 +++++++-- src/arch/linux/ld/instr.cr | 209 ++++++++++++++++++++++++++---- src/compiler/ast.cr | 2 + src/compiler/ccr_io.cr | 13 +- src/compiler/globals.cr | 3 + src/compiler/ir_gen.cr | 20 ++- src/compiler/lexer.cr | 92 ++++++++++++- src/compiler/main.cr | 7 + src/compiler/provenance_verify.cr | 28 ++-- src/compiler/ptr_analysis.cr | 62 ++++++++- src/compiler/region_check.cr | 15 ++- src/stdlib/fmt.cr | 79 +++++++++++ 22 files changed, 1097 insertions(+), 66 deletions(-) create mode 100644 .lia.cache create mode 100644 coq/.fmt_int.aux create mode 100644 coq/fmt_int.glob create mode 100644 coq/fmt_int.v create mode 100644 coq/fmt_int.vo create mode 100644 coq/fmt_int.vok create mode 100644 coq/fmt_int.vos create mode 100644 docs/compcert-reference.md create mode 100644 docs/coq/README.md diff --git a/.lia.cache b/.lia.cache new file mode 100644 index 0000000000000000000000000000000000000000..f3a76d1bd57098906de7fa01b526a7988d49e1ea GIT binary patch literal 125 zcmZ?HFH~e;uz66Ewe@1l)Mfh^7#L!K*bs;tL3qIeX8ZpTuwcQa2@@txnCRdDq(KCj pH4!W_frZI=!GeVlnF$Uc_5>h@g~I{DnF!+WLpVT|2#Dq2008vvG`j!* literal 0 HcmV?d00001 diff --git a/TODO.md b/TODO.md index 920cf73..34ac700 100644 --- a/TODO.md +++ b/TODO.md @@ -178,3 +178,19 @@ RVSDG 式嵌套 region 已落地(规格 docs/superpowers/specs/2026-08-08-regi 6. (后补)ARM64/RISC-V 映射表 - 明确不做(YAGNI):模拟器/调试器、C 生态兼容、指令级时序验证、特权副作用验证(隔离,人工保证) - 参考:`docs/crasm.md`(正式文档)、`docs/superpowers/specs/2026-08-08-crasm-design.md`(批准记录) + +### 对照 CompCert 审查发现的未修复 bug(2026-08-11 记,详见 docs/compcert-reference.md) + +- **int_str 空字符串 bug**:`int_str(7)` 恒返回空、`int_str(567)` 随编译产物不稳定——打印链问题(预先存在,修复 .ccr s1 64 位后被大数路径暴露)。影响:float 打印精度(`float_str_bits(3.14)` 显示 "3.4")、大 int 常量打印 +- **字符串拼接 + println 崩溃**:`println("AB" + "CD")` 程序核心转储(预先存在,concat 相关)。影响:check_error 的拼接错误信息不可读 +- **region_check 误报(B11)**:deref 读出的 int 值被当作指针做区域逃逸检查——`v := *p; return v;` 被拦(预先存在,pts 语义需按类型过滤) +- **float 打印精度**:float_str_bits 的舍入为简单实现(第 7 位 ≥5 时第 6 位 +1,无进位传播)——±1ulp 显示误差可接受,但依赖 int_str 修复后重新验证 + +### float 支持实现记录(2026-08-11,对照 IEEE 754 / SysV 标准实现) + +- 字面量:decimal → binary64 位模式(纯整数算法,≤18 位有效数字,±1ulp) +- 算术:addsd/subsd/mulsd/divsd(F2 0F 5x C1);比较:comisd + setcc 无符号标志 +- 转换:IR_I2F/IR_F2I(cvtsi2sd/cvttsd2si)+ float 运算 int 操作数隐式转换 +- 参数/返回:SysV XMM0-7(int/float 独立编号)+ XMM0 返回 + 栈参数(float 超 8) +- 打印:float_str_bits(位模式 → 十进制,长除 + 去尾零) +- 验证:O0/O1/O2 运行全部通过;待办:float 打印精度(int_str 修复后)、f32 单精度、printf 风格最短表示 diff --git a/coq/.fmt_int.aux b/coq/.fmt_int.aux new file mode 100644 index 0000000..99f6125 --- /dev/null +++ b/coq/.fmt_int.aux @@ -0,0 +1,29 @@ +COQAUX1 8816420a23d81c5ff7d074740c359321 /home/DslsDZC/core/coq/fmt_int.v +0 0 VernacProof "tac:no using:no" +1481 1485 proof_build_time "0.007" +0 0 digits_rev "0.007" +1458 1480 context_used "" +1458 1480 context_used "" +1458 1480 context_used "" +1481 1485 proof_check_time "0.096" +0 0 VernacProof "tac:no using:no" +3281 3285 proof_build_time "0.027" +0 0 parse_rev_digits_rev "0.027" +2765 2799 context_used "" +3281 3285 proof_check_time "0.008" +0 0 VernacProof "tac:no using:no" +3783 3787 proof_build_time "0.005" +0 0 parse_fwd_snoc "0.005" +3770 3782 context_used "" +3783 3787 proof_check_time "0.002" +0 0 VernacProof "tac:no using:no" +3973 3977 proof_build_time "0.008" +0 0 parse_fwd_rev "0.008" +3968 3972 context_used "" +3973 3977 proof_check_time "0.005" +0 0 VernacProof "tac:no using:no" +4534 4538 proof_build_time "0.004" +0 0 roundtrip "0.004" +4479 4506 context_used "" +4534 4538 proof_check_time "0.001" +0 0 vo_compile_time "0.719" diff --git a/coq/fmt_int.glob b/coq/fmt_int.glob new file mode 100644 index 0000000..af9235c --- /dev/null +++ b/coq/fmt_int.glob @@ -0,0 +1,172 @@ +DIGEST 8816420a23d81c5ff7d074740c359321 +Ffmt_int +R1025:1028 Stdlib.Lists.List <> <> lib +R1030:1037 Stdlib.Arith.PeanoNat <> <> lib +R1039:1044 Stdlib.funind.Recdef <> <> lib +R1046:1048 Stdlib.micromega.Lia <> <> lib +R1078:1083 Stdlib.Arith.Wf_nat <> <> lib +R1093:1105 Stdlib.Lists.List ListNotations <> mod +R1273:1275 Corelib.Init.Datatypes <> nat ind +binder 1269:1269 <> n:1 +R1305:1308 Corelib.Init.Datatypes <> list ind +R1310:1312 Corelib.Init.Datatypes <> nat ind +R1325:1325 fmt_int <> n:1 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:1 var +R1370:1379 fmt_int <> digits_rev:2 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:1 var +binder 1269:1269 <> n:4 +binder 1269:1269 <> n:5 +binder 1269:1269 <> n:7 +R1325:1325 fmt_int <> n:7 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:7 var +R1370:1379 fmt_int <> digits_rev:6 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:7 var +binder 1269:1269 <> n:9 +binder 1269:1269 <> n:10 +R1325:1325 fmt_int <> n:10 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:10 var +R1370:1379 fmt_int <> digits_rev:6 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:10 var +binder 1292:1292 <> x:13 +R1297:1297 fmt_int <> x:13 var +R1464:1473 Stdlib.Arith.PeanoNat Nat div_lt def +R1464:1473 Stdlib.Arith.PeanoNat Nat div_lt def +def 1596:1604 <> parse_fwd +R1613:1615 Corelib.Init.Datatypes <> nat ind +binder 1607:1609 <> acc:22 +R1624:1627 Corelib.Init.Datatypes <> list ind +R1629:1631 Corelib.Init.Datatypes <> nat ind +binder 1619:1620 <> ds:23 +R1636:1638 Corelib.Init.Datatypes <> nat ind +R1651:1652 fmt_int <> ds:23 var +R1663:1665 Corelib.Init.Datatypes <> nil constr +R1670:1672 fmt_int <> acc:22 var +R1679:1682 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1691:1699 fmt_int <> parse_fwd:24 def +R1710:1712 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R1705:1707 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R1702:1704 fmt_int <> acc:22 var +def 1820:1828 <> parse_rev +R1836:1839 Corelib.Init.Datatypes <> list ind +R1841:1843 Corelib.Init.Datatypes <> nat ind +binder 1831:1832 <> ds:26 +R1848:1850 Corelib.Init.Datatypes <> nat ind +R1863:1864 fmt_int <> ds:26 var +R1875:1877 Corelib.Init.Datatypes <> nil constr +R1889:1892 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1902:1904 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R1907:1909 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R1910:1918 fmt_int <> parse_rev:27 def +def 2010:2015 <> digits +R2022:2024 Corelib.Init.Datatypes <> nat ind +binder 2018:2018 <> n:29 +R2029:2032 Corelib.Init.Datatypes <> list ind +R2034:2036 Corelib.Init.Datatypes <> nat ind +R2049:2049 fmt_int <> n:29 var +R2065:2065 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R2067:2067 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R2078:2080 Stdlib.Lists.List <> rev def +R2083:2092 fmt_int <> digits_rev thm +R2094:2094 fmt_int <> n:29 var +prf 2431:2450 <> parse_rev_digits_rev +R2465:2467 Corelib.Init.Datatypes <> nat ind +binder 2461:2461 <> n:31 +R2494:2496 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2470:2478 fmt_int <> parse_rev def +R2481:2490 fmt_int <> digits_rev thm +R2492:2492 fmt_int <> n:31 var +R2497:2497 fmt_int <> n:31 var +R2538:2546 Stdlib.Arith.Wf_nat <> lt_wf_ind thm +R2538:2546 Stdlib.Arith.Wf_nat <> lt_wf_ind thm +R2585:2603 fmt_int <> digits_rev_equation def +R2585:2603 fmt_int <> digits_rev_equation def +R2585:2603 fmt_int <> digits_rev_equation def +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2772:2778 Stdlib.Arith.PeanoNat Nat div def +R2780:2789 Stdlib.Arith.PeanoNat Nat modulo def +R2791:2797 Stdlib.Arith.PeanoNat Nat mul def +R3007:3016 Stdlib.Arith.PeanoNat Nat div_lt def +R3007:3016 Stdlib.Arith.PeanoNat Nat div_lt def +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R2772:2778 Stdlib.Arith.PeanoNat Nat div def +R2780:2789 Stdlib.Arith.PeanoNat Nat modulo def +R2791:2797 Stdlib.Arith.PeanoNat Nat mul def +prf 3546:3559 <> parse_fwd_snoc +R3577:3579 Corelib.Init.Datatypes <> nat ind +binder 3571:3573 <> acc:32 +R3587:3590 Corelib.Init.Datatypes <> list ind +R3592:3594 Corelib.Init.Datatypes <> nat ind +binder 3583:3583 <> l:33 +R3602:3604 Corelib.Init.Datatypes <> nat ind +binder 3598:3598 <> x:34 +R3634:3636 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R3610:3618 fmt_int <> parse_fwd def +R3620:3622 fmt_int <> acc:32 var +R3626:3629 Corelib.Init.Datatypes <> ::list_scope:x_'++'_x not +R3625:3625 fmt_int <> l:33 var +R3630:3630 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R3632:3632 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R3631:3631 fmt_int <> x:34 var +R3657:3659 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R3652:3654 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R3637:3645 fmt_int <> parse_fwd def +R3647:3649 fmt_int <> acc:32 var +R3651:3651 fmt_int <> l:33 var +R3660:3660 fmt_int <> x:34 var +prf 3795:3807 <> parse_fwd_rev +R3822:3825 Corelib.Init.Datatypes <> list ind +R3827:3829 Corelib.Init.Datatypes <> nat ind +binder 3818:3818 <> l:35 +R3851:3853 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R3832:3840 fmt_int <> parse_fwd def +R3845:3847 Stdlib.Lists.List <> rev def +R3849:3849 fmt_int <> l:35 var +R3854:3862 fmt_int <> parse_rev def +R3864:3864 fmt_int <> l:35 var +R3940:3953 fmt_int <> parse_fwd_snoc thm +R3940:3953 fmt_int <> parse_fwd_snoc thm +R3940:3953 fmt_int <> parse_fwd_snoc thm +prf 4212:4220 <> roundtrip +R4235:4237 Corelib.Init.Datatypes <> nat ind +binder 4231:4231 <> n:36 +R4262:4264 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R4240:4248 fmt_int <> parse_fwd def +R4253:4258 fmt_int <> digits def +R4260:4260 fmt_int <> n:36 var +R4265:4265 fmt_int <> n:36 var +R4296:4301 fmt_int <> digits def +R4413:4425 fmt_int <> parse_fwd_rev thm +R4413:4425 fmt_int <> parse_fwd_rev thm +R4413:4425 fmt_int <> parse_fwd_rev thm +R4485:4504 fmt_int <> parse_rev_digits_rev thm +R4485:4504 fmt_int <> parse_rev_digits_rev thm diff --git a/coq/fmt_int.v b/coq/fmt_int.v new file mode 100644 index 0000000..adf2584 --- /dev/null +++ b/coq/fmt_int.v @@ -0,0 +1,115 @@ +(* ===================================================================== + fmt_int.v — 用 Coq (Rocq) 验证 Core stdlib 的 int_str ↔ str_int 互逆 + + 源码: src/stdlib/fmt.cr:96 (int_str), src/stdlib/fmt.cr:134 (str_int) + 文档: docs/coq/README.md + + 建模约定 (见 docs/coq/README.md 第①步): + - string 建模为 list nat (digits 0..9), 消去 alloc/load8/store8/header + - ASCII +48/-48 消去 (验证算法语义, 不是字符编码) + - int 建模为 nat (非负情形; 负数/溢出留待后续) + + 翻译对照: + - int_str 循环1 (数位数, 决定 buffer 大小) → 消去 (list 自动增长) + - int_str 循环2 (从高位往低位填位) → digits_rev (低位在前递归) + - str_int 主循环 (res = res*10 + d) → parse_fwd (累加器递归) + + 验证目标: + Theorem roundtrip : forall n, parse_fwd 0 (digits n) = n. + (对任意非负整数 n: str_int(int_str(n)) == n) + ===================================================================== *) + +From Stdlib Require Import List PeanoNat Recdef Lia. +From Stdlib Require Import Wf_nat. +Import ListNotations. + +(* ---- int_str 循环2 的翻译: 逆序 digits (低位在前) ---- + 除法递归, 结构上不递减, 需 measure + 终止性证明 *) +Function digits_rev (n : nat) {measure (fun x => x) n} : list nat := + match n with + | 0 => nil + | S _ => (n mod 10) :: digits_rev (n / 10) + end. +(* 终止性义务: n/10 < n (n ≠ 0) *) +Proof. + intros. + apply Nat.div_lt; lia. +Qed. + +(* ---- str_int 的翻译: 从左往右解析 (累加器递归, 结构递减, 直接通过) ---- *) +Fixpoint parse_fwd (acc : nat) (ds : list nat) : nat := + match ds with + | nil => acc + | d :: rest => parse_fwd (acc * 10 + d) rest + end. + +(* ---- 逆序解析: 对应 digits_rev 的逆序列表 (低位系数小) ---- *) +Fixpoint parse_rev (ds : list nat) : nat := + match ds with + | nil => 0 + | d :: rest => d + 10 * parse_rev rest + end. + +(* ---- int_str 的输出: 正序 digits (n=0 特例 "0") ---- *) +Definition digits (n : nat) : list nat := + match n with + | 0 => [0] + | _ => rev (digits_rev n) + end. + +(* ===================================================================== + 引理① (核心): 逆序 digits 解析回来等于原数 + parse_rev (digits_rev n) = n + 证明: 良基归纳 (m < n 的假设), 关键步用 Nat.div_mod 展开 n + ===================================================================== *) +Lemma parse_rev_digits_rev : forall n : nat, parse_rev (digits_rev n) = n. +Proof. + induction n as [n IHn] using lt_wf_ind. + destruct n as [| m]. + - rewrite (digits_rev_equation 0). simpl. reflexivity. + - (* 用 equation 引理精确展开 digits_rev (S m),避免 simpl 展开 wf 包装 *) + rewrite (digits_rev_equation (S m)). + Opaque Nat.div Nat.modulo Nat.mul. (* 锁住 div/mod/mul,保持文字形态 *) + simpl. + (* parse_rev ((S m) mod 10 :: digits_rev ((S m)/10)) + = (S m) mod 10 + 10 * parse_rev (digits_rev ((S m)/10)) *) + rewrite IHn; [| apply Nat.div_lt; lia]. + (* 目标: (S m) mod 10 + 10 * ((S m)/10) = S m + 由 Nat.div_mod: S m = 10 * (S m / 10) + S m mod 10 *) + symmetry. + (* at 1: 只替换最外层的 S m,不动 mod/div 参数里的 *) + rewrite (Nat.div_mod (S m) 10) at 1; [ lia | lia ]. +Qed. + +(* ===================================================================== + 引理② (桥): 正序解析 = 逆序解析 + 先证 append 一步的展开, 再用它推全列表 + ===================================================================== *) +Lemma parse_fwd_snoc : forall (acc : nat) (l : list nat) (x : nat), + parse_fwd acc (l ++ [x]) = parse_fwd acc l * 10 + x. +Proof. + intros acc l x. + induction l as [| y l' IH] in acc |- *; simpl. + - reflexivity. + - rewrite IH. reflexivity. +Qed. + +Lemma parse_fwd_rev : forall l : list nat, parse_fwd 0 (rev l) = parse_rev l. +Proof. + induction l as [| x l' IH]; simpl. + - reflexivity. + - rewrite parse_fwd_snoc. rewrite IH. lia. +Qed. + +(* ===================================================================== + 主定理: 对任意自然数 n, 先转 digits 再解析回来, 等于 n + ===================================================================== *) +Theorem roundtrip : forall n : nat, parse_fwd 0 (digits n) = n. +Proof. + intros n. + unfold digits. + destruct n as [| n']. + - simpl. reflexivity. (* n = 0: parse_fwd 0 [0] = 0 *) + - rewrite parse_fwd_rev. (* 正序解析 = 逆序解析 *) + apply parse_rev_digits_rev. (* 核心引理 *) +Qed. diff --git a/coq/fmt_int.vo b/coq/fmt_int.vo new file mode 100644 index 0000000000000000000000000000000000000000..a78a8dbec8db8b366597ba8036d7f6ff8ecd74ff GIT binary patch literal 23643 zcmb8X2VfP&_V|By_nf`=hR|yOffQ1J&>^S@H=%a~MMX3O2oMP*CIP{Uy`kP9&n_(X zt3Hi|M6AJr*yGb@FW42)hh5(T{eNcfO$hM5-|z3A?C$JNIp@roGiT1soVjDlPE8G1 zg+B-UzY}8@{Oyh>d3~C@5BFuOC)OW<_!7%0Ua6KcU<@BuC~wKeCg&JR`(v(e`x7grw4pY#<)Rd$C@I#znG1+b(_+ejpu?|ExuH+i0P%$EVu z){A=4v=sv*epHVF8BrqxVmEl3Yi@~p*)xlaR+LRIg8TUuB~?qCxRg#@=JK*dD@)64 zd)jMeLr_w{?{%UbMi6H?BaAj>bf}gWO^67ThhlTXVPNZqMB@YUnvJUzWt8 zW1>EG8I-=LWR*SWsw0wXBwK8|)zO2WkW(eIR?4JQN+Z#lwVs?4iSAqBN4efQY$yewY60AIwT^!s`%7MyqTkPfU+ee3+3jt z;#2K*XWg?cA~iK~rxeFzQB*F6X{L(3{T7p0T4|M?=5+2Lk9#qh&0P_dl~N^kBnlle z&hv&gr=z%Hc?ptL+(^yyJ~eOT*UB?e-$+2_?DFD;C5vTSdS%HHJL8=b9*@YIo;-;p zr>=^~(+PPTl2*Lh5V#{EJ3V>Zq?SkIeIww@BJy!9Jt-z5JlQPInJUs@Bl2xbrqsv> ziAo&Qk7a8{NmX%$ox1VqF7juC{2|xIE2~zkh*}}L!-)Aa)Kd8{IzBosBIBvxWuB*& zB&wrUi|RVHT(um!ML|K-{EtdK<3lCl*|R17s-RVz|ZtJXlZ za${0mL+Lo$Bh@URc%C(03Z`o;ouE1MX1kRwMeQ z6uQB@R3QCx8rr6_ZZLO92QHU@Q7A#QfMqi^Y z%~$J1`G|~ZiwByVJJfov*0k&PTA@_mS}9iRv09Ym}P-~5kua$fm6_bAf>IxvL^-7e!wnwe+>V!V@Nu5lPv2?rZBeG0NO(XAJ>v`n`-f;{3|B?jEpy^9gt1(BkJ(jn1puHcLf4BtMvpxW6?=6tX3Av{92hV z2=EwT?2C6zyIVnGP=K7M+AX4L{TY=ygN0#c-~r8snb6p3c8}^hIjvUhu4;F#l`2Xa zJ-lK=zAUblGa27f5(oy5X+lsB0=mE5F)FVb1P>jI0J&&FFbo7&f?$x^{cGiNO4iCH za-n?gYXG%I%8j<3+V4uWN5jloxmLn5G=X#4*l4s`!Uo3+2g_b%^IA*+$!#E+p!V2W z*{t@6TG=Q!Za}u=>U=>m<xe&6?du7yLcD6F8+ zNxs_i_{JI$f;&z0d}=d+@QfO@?<7Q-jUsIg70idP_o;mkg!j&0xUg_Vgtv^-78lNn zk4RB3^SH%@49{wxKj^gL($d1kWh+-KDqd7rT2;2#4h&!Qk=olq`victsr{tdUScFo zJ8m)G{hAlD4}YTHuWG+e{vGj=r(=c>r$v_;lz)f#*9hNGyTNcT6~%4;Q*EMhA)A)( zl~DL8=@4rN1{~L(9A8nbkED~@^)Vwf`M$2mSV}t?bzy&}_O4nPEoRtC1;agrkU7GL z)K6;fsgrSV&!f821NS< zVxEDvH*3@h5WbFHSbz>fR(}DH1HL=d{t~99EglphLo2ms({T5ylLT$1NEt<2s(ruO zboDDKlmg5a^gsrx9bx^yK~+q>}j<2 z1c(x~(I`&?I0oRB6e1`hv4O-D@{-!mqqJf&1{$5V09JJdl04SX7@g?}!KLu@r>XWN z^H_>Lc~G5G)VV4aosHsxvWL|k=f8|Ah{@OW>O3gF$WV-lm>lKFa2Y|lN(5c9)wz}s zJJf!QxUSTVjy)|t7W_`^Jarx=sF7o+<;a*+8k8qf(O=X#3p%QOk+_bCR1$8W{C2`? z`Tj$l3(0W3;rA&b0O`z4r*H<5>ot0*IxA&WOfI7FT%`Fibv{6vWurRJn?4=(WqFIS z=Gxc9n6S*s3tzJ|=Rf&MbW8y{rF@+at10#QmK$(82Qc@MA#-m z<}lx+vV0G$mW8|?O>*J-0^VLlH<1{Ba4Te-jsW9fKv_qpyN8ZmB zM~+ND%bRGRr5Jj#TZSHB7%eQTXgr$FDnrpX zX^R83K;2>gFkj)t&vqzyTf$Qe}WStserm?6DX7W(uIf+sKeZ-X(i(c@A`a0NwPhoA+( zQ0sZVx&r?;s<)+1`l_JFvWa|$EF~((tFO1y~4~?idVg!&a#GvA4nnLQJAHvkTOO0YXNfq>7taf{~_fq&b3O}y0mBRB>&`=J!dJ>!v zhuBe_IedK-6NdPom=|MOP~=&aZAA9~6#?qK3(HPwzX$v~8|vf|mFMf^Li7@h&Y`)U z05z0ksXR%R0pO@txfc{$Vs!$CD08JcXOp`MR&F;Ha(*ZvYaUs5s65OC-FK**6_dRx zXV=N~D(}?EH7f7c$tok@QmOK)FJMCuwblOHPy}8k0OK8%TN%SaFdlMPbtr=zTK;{~ zr;`35VLjn)LZ(Cg)uDA?Gt@nxf-!ZU$`6J{GXz_+0r4}!UxzZ5UodYJ1K-%I&Mi<6 zVNBt=0_bD_{tK?EeG*^u`TBtnqe=s6!(c>5-r~z9d;`-S0B@r1=GCFP$-8_Z%6gc%l=t)A0i>yQRFwfnheTCw_ZKr& zK8Kb)3^1kKcU7wz9WC#8UQT&YMP+f};?tUDtva`QzriiZSld{AMGF^3R8QtLZ4v7% zdaUY#XdQN!E~>+r)Z_Oxs2-Q^vAz*8D`8rtI>%#$xRvU1Q0WXa2y3oKTXqE*8hkyPs>U*T<9t~?ziJVGE@7%B1yo{;>fiRkYyG?GRfgsXs&^O|m-sYK$CNl6 znUX=C>M1NH5E#*dkf0o$AY}X0MnZ;G%Sec*Mkf^ywTn9 zAya;rlkFB4-?CEmKQzlTs&4}H$O9M3St&P5> z*|AjRaxcF=B5B+~?$!WAO0L?!l^{1G+EqKjSH$`10 zZ%?xNzLmSZnQ`hL>h^%*3nLMk?0LESDQhP9?vyxT$1y|0mT~i-x zh@Gr%znGk?dMofY0Ph4kQH5Ccjdj29c-lRyxEPB2;^7-|rogJ<5G7E|-OBPm|?ZC1n6-CSUZv^&Q6v?ll(g@}b1V9ttIyqQQ zdz}@@AB&3nf8Pp3In4Th-C~SJYG9gJHQqIzJviy;tKjWJ_0_B%NB5v2+@}WgAF#0O z)B%Z2(f+IES+aA!r7H+5tum!r*WdDp7u^X5`SZML1{uv!_c?#V!}I)DvSrQp${Hdp z4l*NP=X0Uib11A_SXN$4p&ZtY5+4!PWxVKmb$6J3G19y~W{EXL>EO+dLZgPJ!2nIKgDcys5=9msXNwxj%yBlv%1MU ziQv!k)|01gM85RAtJzY{mtFo#xIn&dhR$T_NoLt)9uFkYKH#(Lj)?3w$m7j*wZSP~*zu3F}bF}|_-8|iOsJX5NQi6HY z>#HZ2x)2lZ!GdjNnC%v;J2$?ve8LH=6D5OwwbpVE-EfJRlhPKIn79GRWEr5lC~~E+KmiXc5czRE!jOg zl(cf65E3A*%70e+Pe?Y*Z%!KTkT%>W?FUFZrx|HkW_8O@#$r@Cv!Qu>vtS0zmEjxg$DfP1X zK(c;~lNDrgF^7hn_M}=L97@)EJ`p59)<^#HL;p$FJeXVe_+)uLStml)H_gb(Hv2kp zy1WDEnpnRcvV6S%WrzrlWOR=&A=&K@AIRh|!?1d@;RpGO>oDy*P7su`-E>Lv4ls>##@s*6?r1XZuw*@QY2 z)jS_O380$qKMM~=)dy4y4662PK3~SB8oLx*X?N)c*cMc1lhm!NSPtN&Gp5P3FY~IoWM{gR@CAqxc%Ls1b*!kc)w|M z_;kPjybZ#3?Qaa}U2n`2usLnZtYCX{Tfy#Duy-?T|4CpQt}-}2XL1+_pe8<^#8tKZ zN&?SQ*u2^dL+ARqfu~OHDl7P!xvk)PR&eKj3~F^wpqRz#Ufk$*at=Y^U^V!a_y!cI z%}})PZ2(h=Nr8MTyvBc6;d89;)%%egU^9lw6yFT@hOgVGGyYISSQG|Pk_)0y`w=7zGt=k`hP;Sj-_mSg-5l-b<0^ zR&Lw1F=Jrp=?n7jc|Goy*k^no5S|hU^mvH7@1Cf~3S;X3F9$=M6wRt6u7T2ym;dIA z)_K1#TKgJFO*s8!6i7-mn(xmn|4%1Eoc!3vwypl_zmq=oG3gYQ6!z3`3hc_=ox2Bj zFYYw%4DL+sZ0N>+WNS0kIW=# zEdHih`zY6z?)lk5y zNDqGJ zk}1+n^3ARpwaJ*vR8jJKv!XM2Zf41fQ%t+`KjZ9VxkHNCI|Pqx%$K`8X)8y`S{V`t zzXb4R5oE+oZ;p@$;^3cRUA7DVH_0FwWCU+@M7qah6aZw9K_}g_4T8#*cn};_a8`d@ zN7$n@o?q-OjW+wJcs{cKS4<{(a-5{e_LxMXQYjPVUCA^x zSXfzwua{qgc{wGOg)7QdtSDY$ckglK$+Ay!Nuh;rO)D)n^7Qu__B&1MAAb^liyp2& z!-3J;z<>?XE*c%jc7`WjOs*6qDXXxs$hhQ2s8vQ`;p#yVIm?tNEIh4*mD;#asMV+0 zBpT1L^yrO7SPpQ7m7RU#(#;wS?j*zi_P{a>(OkSdq%B*V(h{)Qg@vn%DwY?OH$q1E z=M+^;D=L>CSq4ZMec!AIPGh4zVZXYcDcS<3B3VvRh+DjPf3e=j6s@c(V>=*w!uYZZ zmWzw*ZpH7O#)`2ui^fY2#Jx+RUas-BZSvPut4&s8{(e0lxdIALl8b%jw(ng$1w+{$ z{py2whb{0c$YwwWKHzvo-}7@P@-7uO(M@_~Eb}vmhfa;akTPGav++u++=I(pXKBZO zvLBg7^6Gl|IKj)Pmo;w1Dnk@rkG*G(GhV{>m!~{rpj;sDCBP3#pHV*8?sQ?+o(TRH zm-~R)!I`T(`IUw>eP{p$u1)}DLoTzd+$`AGsk;la3=eON$`P#1?LidtWhDQsW%sF9 z%atrsx;s1kxB6iFfZ)y=wOZjYA_F`)MEkOn<1?iwyP%O>Z3FL;QsZHgO^PR8F=Vda z3S*WQFI-k!QCMjf4ee3iesQW=b)ecPySK0r(%wt(a!0e}8nw0=GJ;g%SvCZ$$5@q% zL%k*U0I2rBzuKK^TvOC~2=7{$>JxTt#$v<&l*zvps`UosAEDM_wd!kS8yoI8o+0h; zQD&K1PXYcMUY8RtBz!?Fv!C^>$D=SBWnaG&ZyW1*Y#{kgwYKuQj@Kf>qPXXYRR~Yn zDuQUW7D4q-3>`^ookErczP3*qTN0`Oe{SNs`K9_&&kk|YMdKot`K=+qtcgVJwT(d_Wmb>M4 z{x`+s>UxAvilihaQE4lu%X~S3eJg8EG!pfE$E&4gyEI+xUIc94rxLKAnG7w@#fJwx zDVs0FtHn&BH};QN#-|trBXU3Uq!;=gaV>CKLR~aD#7P(Y1n^=TVHAh)Qu$vz&pQ8) zo@XOHwI>5;y4q9J&hVQ#>iM2$Q~sOh*#z<*8yAKHJkO>RKMy$b%?2c!$eYwIgf?cD zF>bZ95`Jf$n){v2#bIoz+04!VuYPBzsa;h|AL`hsRT4hzcmVBpVpqGuh!pbV8%emb zYdpK!Wlg^9Y9osF6=n>r=g(zCPqB9FJfR$a3u4< zrDL^M?ssb^djnRU^}6XJXqv{8G6x(UiTk%m!U^s=RA*D*iK z=VD9GzJD#6o{3ql*)29cUiQ;0FW|f=(<0El*~38$7b4Q`C+&GPK5}vQ-`U9Rll8cG zpn|5wWFqx`txgKmZoq|4?bmU@l99D?r12-RpQthZxp@sT5;sW6RU2TJ#{2I5YW?PS zgku2sTD{sI*2zq@KdKcxjXthr5S&~qlVm(lUaG-ouND3c_O*2~OYP4YAk}^+UWIRK z(SBs2XB);oD=ka~o;4M~K3&TAh@U2DcN*^s!$7q^$QfT$%0{VCHEq(33*&CjcNZq> z7d2*EzOX?Ssr`T)3mOw9_Id2LvsRQ=6%NF?WccTMq5F5~1{<9u_SR3sGr`B0WiZx& z@frNW>SVR7+=9Ne3q9E&N3pSN|5+o~#4rJUnT*8uFV`4HNGDUBbgGljT_Bh7Z_$bl z-hf#K^5Rl{8p4IT{QHHh&#>7lsjUQ0e)BLu%Ozh2|b2KR7v#t{r5(?GyYM0}jA zcn^Iei?bfa+s4kj>pWZ}3L1>}!)x+7c9n;pRUP~5&M_PlQRi6dR4FL(r{r-UoR$}R^E~~fN^|{?1{-g8su%3Lh!k8rVu$Z8pV(CB%o%Q6+Lstz&IxC z#=B4+s+YZW@*mk3livY-PMzQuwAMI4JLdv=lkBdQZ$Yfiat0-h$yW`=ANoE+!F*zi zqtQty3V$527ZgwmPF)3)HWMy6V1tsu3scVQUaG^^IDREj+=ZM%+&tpq>718YyxNz| zw3FZLr_TBYbv!g)dv!KLOB*~h2pAw*5+tjIKa6uFRIw*%g&K&aJISArz&DPDBh)EZ zocxqi3F_Pnpq{w>P_(-`_YvS4kwVZ#&8ZRNtY-}t90ZLg=fg1!V=z3AD)?2MTFPF6 z!>QkitdxGsi&hu zXpHY506$0LA_xag;Ols`js@#`kYkRV90NHg&`3Fy1K1vvxy=Z`C&mNX`A|3{MBr;)D}{LGQWbbWf~%7U{wlSM zGuW@-H$KSa;71Ffws8^shJ^2<(Wx=xwPO0pMLzxyqm#**!o-P<{T^o6yj0 zW^n(h_E2^HA__nDi&0d5<4VheoK5AhojA)%ic!DTy*NyCf{OcMavRtN#$+>~q)jwB zLmeFGTE*lZ;`1aZ`JlJ}Q)6pP7)RvDnA~f!c8f-*tGLo1>TaPPcN*7T>pBw9Sv@3( zW`K>Q31SZGTUyL)v#_e7Xho$xtg3pv%BTjGG~Y1}tMZ0VWgnO(TT?(xUF>s7|p z$j3PPvQUR(n(^m33X=Z`!h4}-H0QW_n8vm>DKp2oq(704 z1ly@sKS~XbksB2Y9K!(xKRTYl?vizY6R*s}qX-MqM%AXF1u?wQW{4=!%K?j1+o>um z$dFR6QjXUtuT!B4N=K+n*#bkU{z+iNG0=<{y~uYOF7|k)jxbpWaSxuSDec15|(<@c}C^@Eyg5h)p*(s*B!N!=;vV$wt&$E>=k?l z)SOAN_NiQj$o^fefAjSRRwKMKhZWkxyIszX2Mq1}A4~es|0OUL}b=@Z{ z&t9o^ccST+#f(=hwL-Yr`)fKthszb6UViQdPw=PFbLLI(g_Qb^LKfK-l>%qwQi9p$AhTMCQZZnVLpb{<+M!n$nNQ^Rl zJUqrZg;bT7;}!fEVsLtu=c&=hYF(@H2reDHFmgGvgt<%7OAxtGPB ztWAb7c00qE4`4_UV7?QbBlUsqviW^asac@RxMHG<;czyRfO>;ilFfvouGoIdY}) zrD?SOz8;g`sKd`VCM5e#rB522yV`j3;;Mx-a`FpvwNVB&jLS)9h`US`KO6gEJlh~H zPwfl%I$!Ozc&8}D-As$9GXNsg!Hrjwh`U8)5>pI=`aeFmi!n!h&r%jYRQmwd_=w)1 zY8;OzV@mRMjoMdJ9&b{ci<#Zy@gA)ynQ>=(J8kCITX3t`iSR;fd$z4_O!!8XaZvNP;&a(E^KsKt zO&6rC2tH{M+Fy@Wolh_wP*cc`U`?`7Qkt zQeP))IkHfP*@qbp1;%c6RI5Q9P+d;|%6(9<7bjzIoQ;BIeZc-53Q%rOVHB&H;nnE% z_OJ=fRmUkmr<)PkVl#^{-rTwwxOkXhfjPJ~-b%1domK=KMo9whRlwzZ4=%b_?Zcs0 zZ={SdqH%WQNQjf7dJn-1ASb|JYDbxCDKh~0Z5xO-uB;9_$PCAu)p^F3@z=?;kxavV z-(I^Pt?&r6=b$Rg7Buzq`LGwWCob`WiQ5L&t3fhI^%;Us)ag%<%X9*0493m`Q09OV z9l1xHo>YqE5hmaJIKZb*K=(^P7==qC#g0^cg@AJrBM9<*b6vLr@^<4eL9I z<#s-g^e|FX-zVFb06Cihg4iltFam_9n&La7Q927fpfyamKwX!jxg_>Mw}R|bKAEDV zu^P2gopm5x0TpPpR}o5o3bM;U!6cil`YzTL#^44b{si4MYP}7lb)f4)XyyR=do+5C z>SwCI#^gI7ZUW-DK)i^wzoKe?hQ%yjOZz(6htY@+VJiULK^g#V0#LSpUg0uIT!l(w z>cS}~V_>y2Q%^k|qVZui=e*oOgttgK@cqe0ciMp_S;yQb8;#@k0xleLu7WD3I?9ek zKWS+aGD&z+dQ$pfpx{Pnv>Q6Xex*iIW5)5?eoS?ly6MbF6z47a6-C^*x^fTe6IWL& z3TH33``z?88ApQ}kH{)ut3^MseiWG1c)8g%P<|6mDzw9DbqA{3$Ix*kK$+rMcu)3+ z7dNXr(H|6D9H`$xl-xmPP;|~mmATU(;vZ0ZGU01L8VxFnvPFaeDeMVMHP(<@f?H#w z;hU9%5y|07Go|T%-UBbHJ0AcO$W@_k8Te1&^VE2yoE-^=YqN3WJJ7nPM5Q+rll@F} z*C4>@lP0b(5-SJK1$xyj#zJr!)IB3!sVi$)aBl4{ zX}HVGh-yyhaJs=|wLtCz0)~!Ts_r;}fp*zWY=4>w;p7|y>djpXg6m?ErEaCV7?$)Z z3f!cwF)Q7RNZrV4a@1%fcNRn}R`-}h<$nKfKUNSwROQ}44Ge?tHLC42b?>Q@!O*ov zT_%=7A9Rlf&86zDX0r@YhpxfM6PBBc<;LV*E&ZHxYGI6&9`%U=4Z;W_CXKq6Qjw?KDlu+-|;^oVWBILq6b3cXvU>G7HX)eD! zGHgD?x^E{ITiqw5Cy^7bMJKx-N_*Dj4Mu*fWm;K9`O=cg<+!mXb|2Ni)z3eHRTTQ|v74A9Z61z;EPGC|-BF$BR2J)!<>cfD6kS?&a|%_+T!w z>UWP#NU^$;)cr|y1RgSe!#t?&={wYI%blbyW9Kip-~Wj5gGS|Tr*9GIhZ8iIy;Joq zMl{vu{c9T?;?X?}463iHzTjWa5LZ`k1V=N>wt&X+H8_wsRX#3K<=B*-DBa`B8^NsJ zabJ;JFf;@lGczuUDe2Sk15Xxk+_lRBtPPz2rxeRD~C7rlp zzN%1a7-Vj_r$MY(_g}&~pj$-8Hv6F%NbdW{_yW2F(S_=wQz!E_!50>H>=+H6S+DMA zl$-=y2zW??%V>N?5weXWzU>}$5o7dyFaI+2Yekt|2+$`q>+U$Hmg6*d8J|C>!m$9E z0susQub27c+(pta)F;efuKI;43*bHI^Z4VRr7lV;cnLW$S%cl^%X1Kr`!#r$2G1v^ zCw05f{D?qst!FY|C@>ug9!Ag8OO)jawMIq-LpyjW<*qPcy#~+F;2K^R@Or!kr)#hy z6+-8_4{Gpig1-ZGlm`0|%jn94iS?1-27`cOn!Pp17#1w8_j?Q-=?T>>j3q&4(?PnE zH522#tp+bghhNG}j+k_&cpBWq#a`PSRVKq`VDwKR1&xhKSLMKHu%!lHNl5W4*}gls z8HAlKJs;8F_MIAhldS(?nox`F7JLho^`LwwUP1@#Kl>E-0t>!QH6BU8`*{CBj38!X z@JkIohYc`~*RM6$TD2{7=1@f|115K1Q&EGocZWL3)Zq8#~(%?iV*yzbNB2dc*G7-fnc4*VQ464y_IFK7@;GS~w*I9QTa zniZkp%-f`iky;t2p_YLE4KF!<#fO6>!Cf&yk%Zc7@JGP2)EDZg@`~yxAkXpG6cM&! zW@@MlBs;(C)DXSQnrHAH2i^(hWq~IHRo>U&WDS0!!4`EI%F+$$d0c5@yqR`2FA)&H`Fkj^l)QeGa)_DfoS&+M&e7z(D6O7~;(pF#w8jDTJ zRbS+oOM`|G92OE3Z5d*+9GVf6(IrVw;4>P$ z6=xwM8sicGH*3hhg8$a|WoX8`0nnx;X8YC^;cf@>UJ`S8%V!FMcnGJ`}%D zPHf+YO4Pj%F0pjqPF(iBG2zYhKlrw3fU9YMdvI_X$ot=Thi{=?QG79a@X{JALjoFl zKto9yd>x6`;A?0#et*a)=|5?jWF}=JsBR|>t&tye!so=6$9n@xceRNnhRJ(q7yz(SjTeyl;SxAytg+yeB+tOA0LFdHJf~@>H?4Rt zJ%||6??9XLhD#wT;5^>WA@Z0#8m#a~_=OteI*GWW>ot^1m_a=;lqaVoW0TQDQ^Ks+JSX zi6Z!%F}*}qlTL0#Gjs!C7!bQy-L@pI$KCw?`%lD~vwF7gO&a=)e79oKgnTvgK3_jk zx*JgVm5$p87)F(inb03JmWJK|-6i})g@&;GKQ{^`Y-#9Eev!qUNKt?06*dj~U5$nn zNa*{}R#Inb=s)q)R@kOYHbb8?Cj<8RWJI8`j7E4-4cjrP_cYvI?JG63+vM9#K9>H@ zM9+i+WM<-TMS%LU&~aWiWqSGxA1fFE!l~$keLFRr4xJCe8|Pcnu|LCoHJlBAb^z$3 zVMjwhCirshe?9*hcj^tN`#%wIJlH;u$tTb?R9Yv>U4GyR!?TBPP#E%ThT zBdi=}T#lU^z(sQ1aLL2Ber;ByOLB+gNXWac#=|qn<2N10Zm4ehi`0jE=LYO`fxJNK zQMMhP*<$a%Ei1$SX+nK!}(aCW}*;Z1wENmrd87Fo~dOOvwz1>zFaxHCds%6_PTBKyV ze7kwh5rK6bl5*{&JSR_5j|k*gft0SfPEt}zo~HSqJpxX)tj)S0lDsxMG}5nDzWIH* z{3#oxd%YwzPm-{SO{>pIRFP_=c3E35?GMP*&SdIapA-mK&&Ml8%{%7>@~pI$NvZ9v zFpJHmiu>?I&k90PpMDmN5y-PsAv3i_x76gWso@rr+w?rlv`_PEJJ`0dv!>2RwNB#67E zE7Yb#cCvYNNM0QpJ2f=5OEP~mLsLUT%}a*=6-f^Ds<{qN*vP~UGMJYUkqPzEE-o(} z{2=@{UyQ)pn!A8|US6QLXrI2SttOi;Xd9NaNo#s-=d$K&x6HMYC+E=}{q{}{m_`a_ zIeq#%PCLgr!U9mU^rXP#c&Zg>Vfuk7M=RI?+NO0%i#VK6q5)0LwZkU%OQw$}j|e4a zObjJ=9~d%kQ5Z!DihWPFgT0l-h!4AT``GC6v@I$!QyI z+alNM(Kb2Ps({aV;a=g^EpzRc%sT{!d%MY00YyZW+N9)Kt(y{pN#hKvT)S;jo*KTp zX?byk!y7*XsqvH~q`2$;*G67QTpKl#-7%#_uG888+YhRf(NLZ9w5y2Ar3Gv^JA`Fj>wh1M#jcdcHUFL_f zLx^_rhz`l!5s406I&?r5LL-usk##c0Ba?|_SO_KeYLh`+C>b>>eT^C%TOXd)-@-ye zG5cE1A9A|V^;6*Y)Ffu8o>W0aq7r`Gb%(grN;w=-Di#DH9_SAaeuZMAu-X z14H)I>`xGsH34jHIG3pOH9e8LCzm7hjvF(WSh}a z3iHQoVB_eVt$PmhzCUy8i01>(et*;LzcW$`caUGut|+Ql!>jrGH6CPNeDF~c;)7-7 zMW?PT=0~p0U(OZru+Q9sZ2{tgl`C0KZGze+o;C2+!M~eLe0bIJ14x+tTRd~{mV+t& F{{Yyy`xO8H literal 0 HcmV?d00001 diff --git a/coq/fmt_int.vok b/coq/fmt_int.vok new file mode 100644 index 0000000..e69de29 diff --git a/coq/fmt_int.vos b/coq/fmt_int.vos new file mode 100644 index 0000000..e69de29 diff --git a/docs/compcert-reference.md b/docs/compcert-reference.md new file mode 100644 index 0000000..69adb05 --- /dev/null +++ b/docs/compcert-reference.md @@ -0,0 +1,139 @@ +# CompCert 后端对照参考(形式化验证过的 C 编译器) + +> CompCert:世界上唯一被形式化验证过的 C 编译器(INRIA,Leroy 团队)。 +> 整个后端用 Coq 编写并被 Coq 证明正确——学习"验证过的后端"如何写、如何证的唯一教材。 +> 本文件是对照 Core 后端的阅读地图。 + +## 获取源码 + +网络恢复后执行 `bash ~/get-compcert.sh`(自动尝试 GitHub / INRIA GitLab / 代理)。 +或者手动下载 `https://github.com/AbsInt/CompCert/archive/refs/tags/v3.17.tar.gz`。 + +许可证:GPL v2(研究使用无问题)。 + +## 目录地图(v3.17 解压后,2026-08-11 已下载到 ~/compcert/) + +``` +compcert/ +├── backend/ ← 后端核心(Coq 源码 + 证明并排) +│ ├── RTL.v ← 3 地址中间表示(CFG,接近 Core 的 .cir 数据流图) +│ ├── Allocation.v ← 寄存器分配(图着色) +│ ├── Allocproof.v ← 分配正确性证明(最著名的证明之一) +│ ├── Linearize.v ← CFG → 线性指令序列 +│ ├── Linearizeproof.v ← 线性化正确性证明 +│ └── Mach.v ← 机器抽象层 +└── x86/ ← x86 目标(3.17 已合并 x86_32/64) + ├── Asm.v ← 每条指令的精确语义模型 + ├── Asmgen.v ← 指令生成(Mach → Asm) + ├── Asmgenproof.v + Asmgenproof1.v ← 生成正确性证明 + ├── Op.v ← 操作语义(运算的数学定义) + ├── Machregs.v ← 寄存器定义 + └── TargetPrinter.ml ← 汇编文本打印(对应 Core 的 ELF 编码) +``` + +> 注:3.17 版本中 `backend/Asm.v`、`backend/Asmgen.v` 不存在——Asm/Asmgen 在目标目录 `x86/` 下;`Architecture.v` 也不存在(由 Machregs.v/Conventions1.v/Stacklayout.v 承担)。 + +## 与 Core 后端的对照表(v3.17 实际路径) + +| CompCert 文件 | 内容 | 对照 Core 的 | +|---|---|---| +| `backend/RTL.v` | 3 地址 IR | `src/compiler/dataflow.cr`(数据流图) | +| `backend/Allocation.v` + `Allocproof.v` | 寄存器分配 + 正确性证明 | `src/compiler/opt.cr`(寄存器分配器) | +| `backend/Linearize.v` | 图 → 线性序列 | `src/compiler/ccr_io.cr` 的线性 CFG | +| `x86/Asm.v` | 每条机器指令的语义模型 | `src/arch/linux/ld/instr.cr`(指令编码) | +| `x86/Asmgen.v` + `Asmgenproof.v` | 指令生成 + 生成正确性 | `corearch.cr` 的发射逻辑 | +| `x86/TargetPrinter.ml` | 汇编文本打印 | `src/arch/linux/ld/elf.cr`(ELF 输出) | +| `arm/Asm.v` / `aarch64/Asm.v` / `riscV/Asm.v` | 各目标指令定义 | `bootstrap/corec/backend/arm64_asm.py` | + +## 两个最值得先看的点 + +1. **`backend/Allocproof.v` 的证明结构**——回答"寄存器分配正确性到底意味着什么": + 分配前程序与分配后程序在**什么等价关系**下行为一致(模拟关系 + 良基归纳)。 + 这正是 `opt.cr` 缺的那层论证。 + +2. **`backend/Asm.v` 的指令语义**——CompCert 正确性的地基:每条指令先有精确语义 + (作为数学对象定义,而不是字符串/字节),才有正确性可言。 + Core 的 `instr.cr` 目前只有编码没有语义——差距就在这里。 + +## 与 Core 的关键差异 + +- CompCert 生成汇编文本交外部 `as`/`ld`;Core 自己发射 ELF(`src/arch/linux/ld/`) + ——ELF 输出是 Core 独有、CompCert 没有对照的部分 +- CompCert 不验证前端(Clight 语法解析);它的验证从语义化的中间语言开始 +- CompCert 用 pass 分阶段 + 每阶段一个证明;Core 是单趟管线(架构哲学不同,对照时注意) + +## 审查发现与修复记录(2026-08-11) + +对照 CompCert 审查 Core 后端 + 指针分析链,发现并修复 6 个连锁 bug(安全关键): + +### 已修复(越界检查绕过链——5 个 bug 连锁,单独每个都不生效) + +| # | 位置 | Bug | 修复 | +|---|---|---|---| +| 1 | `ptr_analysis.cr` IR_ADDR_INDEX | `&arr[i]` 运行时索引的 offset 无条件传播为数组 offset(0),provenance 误判"编译期安全"→ 越界裸读 | 索引常量可精确算(idx×8),运行时索引 → offset=-1(迫使运行时检查) | +| 2 | `instr.cr` IR_DEREF s3≠0 | ud2 写 `buf[cp]`(应为 `buf[pos+cp]`,污染函数头);jae 越界跳 .safe(不崩溃);jne 多 +2 跳指令中间 | 三处编码修正 | +| 3 | `ptr_analysis.cr` alloc 分支 + `get_alloc_size` | 所有 alloc 的 pts 恒设 bit 0(无 alloc 序号);`get_alloc_size(bi)` 把位号当 DF 节点序号查节点 0 → 恒 -1 → 运行时检查**从设计上不可达** | 新增 `g_pa_alloc_count`/`g_pa_alloc_nodes` 映射表(alloc_seq → 节点序号),get_alloc_size 查表 + 修正 IR_ALLOC_ARRAY size(s1×8 非 s1×s2) | +| 4 | `ptr_analysis.cr` LOAD/STORE 传播 | STORE 传播混进 LOAD 分支(用 dest d,而 IR_STORE 的 d 恒 -1)→ 永不执行 → `p = &arr[i]` 的 offset 传播链断 | STORE 分支独立(s1 ← s2),移到 `if d >= 0` 块外 | +| 5 | `main.cr` build 流程 | provenance 的诊断只记录不拦截,编译期确定的越界照常生成二进制 | build 流程检查新增诊断数 → 打印 + return 1 | +| 6 | `region_check.cr`(3 处) | `alloc_seq := bi + nstart`(位号+函数起点)——修复 3 后位号是全局 alloc 序号,语义错位 → B11 误报 | 查 `g_pa_alloc_nodes` 映射表 | + +验证:常量越界(`&arr[100]`)编译期拦截 ✓;运行时索引越界生成 `and $0xfff` + `cmp` + `jae→ud2` + `test` + `jne→.safe` 检查序列(objdump 确认跳转精确)✓。 + +### 第二轮审查(栈布局/调用约定,任务 2)新增修复 + +| # | 位置 | Bug | 修复 | +|---|---|---|---| +| 8 | `elf.cr` emit_alloc_body 全局 bump 路径 jbe | jbe 偏移 +14 漏了 `mov rdi,r9`(3 字节)→ 跳到指令中间 → 死循环(**所有无 arena 的堆分配程序挂起**) | jbe 改为 +17 | +| 11 | `elf.cr` 栈帧大小(dry run + 实际两处) | `size = vc*8` 未按 SysV 16 字节对齐:opt≥1 时需 ≡8 (mod 16)(6 个 push 后 rsp%16=8),vc 偶数时未对齐 → 调用点 rsp 未 16 对齐(FFI/外部调用会崩) | 对齐规则:opt≥1 → %16==8;opt<1 → %16==0 | +| 12 | `ptr_analysis.cr` alloc 分支 + `get_alloc_size` | `IR_ALLOC`(标量变量槽标记,不发射代码)被当作堆分配参与 pts 追踪 → `p = &arr[i]` 的 pts 含多个位(污染)→ s3 取错 alloc(标量 8 而非数组 40)→ 正常程序被误杀 | 只追踪 IR_ALLOC_STRUCT/IR_ALLOC_ARRAY | + +验证(干净构建):正常索引 `v=30` exit 0 ✓;越界索引 exit 132(SIGILL)✓;常量越界编译期拦截 ✓。 + +### 未修复(预先存在,另行处理) + +| # | 现象 | 影响 | +|---|---|---| +| 7 | 字符串拼接 + println 崩溃/挂起(`"AB"+"CD"`) | 自举产物坏代码;check_error 的错误 msg 因此为空 | +| 9 | 数组读取值错位(ptr_arith 的 `*p != 30`——旧工具链产物) | 数组布局/header 问题(新工具链下正常程序已通过,待复核) | +| 10 | region_check B11 对 deref 读出的 int 误报指针逃逸 | 部分合法程序被拦(region_check 的 pts 语义需按类型过滤) | +| 13 | ~~float 类型是壳~~ **已实现(2026-08-11)**:字面量(IEEE 754 位模式,±1ulp)+ 算术(addsd/subsd/mulsd/divsd)+ 比较(comisd+setcc),运行时验证通过 | 待续:int↔float 转换、XMM 参数传递、float 打印 | +| 14 | `.ccr` 序列化 s1 用 32 位(buf_write_i32)——大 int 常量 / float 位模式 > 2^31 被截断(静默损坏) | 修复:s1 改 64 位(写/读/尺寸同步) | +| 15 | `buf_read_i64` 缺 `h3 < 128` 的 else 分支——高位字节(bit 56-62)贡献丢失(0x4009... → 0x0009...) | 修复:补 else 分支 | +| 16 | `int_str` 对部分值返回空字符串(int_str(7) 恒空、int_str(567) 编译相关不稳定)——打印链 bug(预先存在,大数路径暴露) | 未修——影响 float 打印的精度显示(3.14 → "3.4");单独处理 | + +## float 支持实现记录(阶段 4-6,2026-08-11) + +| 阶段 | 内容 | 验证 | +|---|---|---| +| 4 | int↔float 转换:IR_I2F/IR_F2I + cvtsi2sd(F2 0F 2A)/cvttsd2si(F2 48 0F 2C);ir_gen float 运算中 int 操作数隐式转换 | `3.14 + 2`(int 2 隐式转)> 5.0 → exit 0 ✓ | +| 5 | XMM 参数传递(SysV:int 用 ir 0-5 → rdi..r9,float 用 fr 0-7 → xmm0-7,独立编号)+ float 返回(xmm0)+ 栈参数(float 超 8 用 sub+movsd) | `add_f(1.5, 2.5)` = 4.0 > 3.9 → exit 0 ✓ | +| 6 | float 打印:`float_str_bits`(位模式 → 十进制,长除小数提取 + 去尾零 + 简单舍入) | 2.0→"2"、0.5→"0.5"、6.5→"6.5"、-1.0→"-1" ✓;3.14→"3.4"(int_str bug 干扰,见发现 16) | + +## 寄存器分配对照结论(任务 3,2026-08-11) + +对照 CompCert `backend/Allocation.v` + `Allocproof.v`(图着色 + 溢出 + 模拟关系证明)审查 `opt.cr` 的 `alloc_registers`(线性扫描): + +| 对照点 | CompCert | Core | 结论 | +|---|---|---|---| +| 分配算法 | 冲突图着色(干涉图)+ 溢出 | 线性扫描:活跃区间 [first,last],每变量独占寄存器、**从不重用** | ⚠️ 保守正确但浪费(5 寄存器后全栈) | +| 正确性条件 | 着色无冲突 + 模拟关系证明 | 变量独占寄存器 → 无冲突(隐式满足) | ✅ 正确 | +| 活跃性 | 精确 liveness(控制流敏感) | 线性区间近似(保守) | ✅ 正确(保守) | +| 跨调用存活 | caller/callee-saved 混合 | 只用 callee-saved(rbx,r12-15,prologue push/epilogue pop) | ✅ 正确(简化但有效) | +| 溢出 | 图着色溢出到栈 | 无溢出——超 5 变量全栈 | ⚠️ 性能差距 | + +**O2 运行验证**(首次验证,全部通过):简单运算(42 ✓)、跨函数调用(callee-saved 保护,30 ✓)、循环(45 ✓)、指针 deref(✓)、越界 SIGILL(132 ✓)。 + +**未发现正确性 bug**——差距在优化能力(寄存器重用/溢出/精确活跃性),非正确性。 + +## 调用约定对照结论(任务 2 完整版) + +| 约定点 | CompCert(SysV) | Core | 结论 | +|---|---|---|---| +| 整数参数寄存器 | DI,SI,DX,CX,R8,R9 | rdi,rsi,rdx,rcx,r8,r9 | ✅ 一致 | +| callee-saved | rbx,rbp,r12-r15 | 同 | ✅ 一致 | +| 栈参数(第 7+ 个) | S Outgoing,调用点 [rsp+0..] | push r10(右到左)+ add rsp 清理 | ✅ 一致 | +| 栈帧 16 字节对齐 | frame_env_aligned 证明 | 修复 11 前未对齐 | ✅ 已修 | +| 返回值 | rax(128 位用 rdx:rax) | rax(无 128 位类型) | ✅ 一致 | +| varargs | 调用点 AL = XMM 参数数 | 不设 AL(无 float → AL 无意义) | ✅ 无 float 时正确 | +| outgoing 区域 | 固定帧内区域 | push/add 临时区 | ✅ 功能等价 | +| float 参数 | XMM0-7 | 无 SSE 实现(发现 13) | ❌ 类型壳 | diff --git a/docs/coq/README.md b/docs/coq/README.md new file mode 100644 index 0000000..ecc79a3 --- /dev/null +++ b/docs/coq/README.md @@ -0,0 +1,101 @@ +# 用 Coq 验证 Core stdlib 纯函数 + +> 目标:用 Coq(Rocq)做**程序验证**——验证 Core 系统里**几乎永远不会改**的部分(stdlib 纯函数)。 +> 注意:这不是规约系统(`.corespec` / 翻译桥那套基础设施),是直接用 Coq 验证程序本身的性质。 + +## 为什么选 stdlib 纯函数 + +- **几乎永不变**:`int_str`(数字→字符串)、`str_eq` 等是语言无关的经典算法,语言怎么演进都不变。验证是长期投入,选会变动的代码证明就过时了。 +- **纯函数**:无副作用,语义干净,Coq 里建模没有状态/内存干扰。 +- **规模适中**:每个函数几十行,翻译 + 证明一晚上一个闭环。 + +## 第一刀目标:`int_str` ↔ `str_int` 互逆 + +源码:`src/stdlib/fmt.cr:96`(int_str)、`src/stdlib/fmt.cr:134`(str_int)。 + +**要证明的性质(非负情形)**: + +``` +对任意非负整数 n:str_int(int_str(n)) == n +``` + +即:数字转成字符串,再解析回来,等于原数。这是 fmt.cr 的灵魂性质(数字转换正确性)。 + +## 验证工作流(5 步) + +``` +① 建模约定 Core 程序怎么"翻译"进 Coq 世界(抽象哪些、保留哪些) +② 翻译 int_str 循环 → 递归(核心技能) +③ 声明性质 互逆定理长什么样 +④ 证明 归纳 + div/mod 引理 +⑤ 验证 coqc 编译通过 = 证明成立 +``` + +--- + +## 第 ① 步:建模约定(已完成) + +**关键概念:验证不是逐行翻译代码,而是用 Coq 的语言重新表达同一个算法语义。** 要回答的问题:"int_str 的语义是什么?"——不是"它怎么操作内存",而是"它把一个数字变成了什么"。 + +对照 `fmt.cr:96` 的 int_str,逐项消去: + +| Core 里的东西 | 为什么能消去 | Coq 里的表达 | +|---|---|---| +| `alloc(n)` / `load8` / `store8` | 内存布局是实现细节,语义 = "产生一个字符串" | `list`(字符串就是字符列表) | +| 字符串 header(`str_len` 读 -8 偏移) | 长度已内建在 list 里 | `length` | +| `+ 48` / `- 48`(ASCII 转换) | 字符编码是实现细节,语义 = "数字的十进制位" | 数字 `0..9` | +| `int`(64 位机器整数) | **先只验证非负情形**,负数/溢出留到后面 | `nat` | + +**消去后 int_str 的算法语义**: + +``` +int_str(n) = n 的十进制 digits 序列 + 比如 int_str(123) = [1, 2, 3] +``` + +**str_int 的语义**(`fmt.cr:134`): + +``` +str_int(s) = 从左往右读 digits,每读一位 res = res*10 + d + [1,2,3] → ((0*10+1)*10+2)*10+3 = 123 +``` + +**待确认点**:int_str 里有两个循环(数位数的循环 + 填位的循环)——翻译成 Coq 时两个循环会合体成一个递归函数。 + +## 进度 + +- [x] 第①步 建模约定 +- [x] 第②步 翻译 int_str(循环 → 递归) +- [x] 第③步 声明性质 +- [x] 第④步 证明 +- [x] 第⑤步 coqc 验证 —— **2026-08-11 编译通过** + +## 成果 + +- **证明文件**:`coq/fmt_int.v`(编译命令:`coqc coq/fmt_int.v`) +- **主定理**:`roundtrip : forall n : nat, parse_fwd 0 (digits n) = n` —— 即 `str_int(int_str(n)) == n`(非负情形) +- **引理**: + - `parse_rev_digits_rev` — 核心引理:逆序 digits 解析回来等于原数(良基归纳 + div_mod) + - `parse_fwd_snoc` / `parse_fwd_rev` — 桥引理:正序解析 = 逆序解析 + - 终止性义务:`n/10 < n`(Function measure 证明) + +## 过程中踩的坑(Rocq 9.1 实测) + +1. **除法递归不被 Fixpoint 接受**(guard condition)——`n / 10` 不是结构子项,需 `Function` + measure +2. **`Function f (n : nat) {measure n}` 语法在 Rocq 9.1 坏了**——报 "Illegal application: n cannot be applied to n";须写 `{measure (fun x => x) n}` +3. **`simpl` 会展开 wf 包装 / divmod / 乘法**——`Function` 定义展开带证明项,`mod`/`div` 内部是 `divmod` fix,`10 * x` 展开成加法链。解法:`Opaque Nat.div Nat.modulo Nat.mul` + 用 `digits_rev_equation` 精确展开 +4. **`rewrite` 替换所有匹配**——`rewrite (Nat.div_mod (S m) 10) at 1` 限定只替换最外层 +5. **归纳需要泛化累加器**——`induction l in acc |- *`,否则 IH 里的 acc 与目标不匹配 + +## 下一步候选 + +- `int_str` 负数分支(neg 处理,用 Z) +- 溢出语义(64 位机器整数,用 bitvector 或 mod 2^64) +- `concat` 正确性(`str_len(concat a b) = str_len a + str_len b`) +- `str_eq` 等价关系 +- `collections.sum` / `reverse`(`rev (rev l) = l`) + +## 环境 + +- Rocq Prover 9.1.1(opam,`~/.opam/default/bin/coqc`) +- 无 coqide,用命令行 coqc 编译 + 编辑器 diff --git a/src/arch/linux/ld/elf.cr b/src/arch/linux/ld/elf.cr index 8291d35..9cfcc28 100644 --- a/src/arch/linux/ld/elf.cr +++ b/src/arch/linux/ld/elf.cr @@ -267,8 +267,9 @@ fn emit_alloc_body(buf: string, pos: int, bss_va: int, globals_size: int) -> int } // cmp rdx, [rcx] -- 48 3B 11 w8(buf, pos+cp, 72); w8(buf, pos+cp+1, 59); w8(buf, pos+cp+2, 17); cp = cp + 3; - // jbe +14 (skip call+reload+jmp if within bounds) -- 76 0E - w8(buf, pos+cp, 118); w8(buf, pos+cp+1, 14); cp = cp + 2; + // jbe +17 (skip call+reload+rdi+jmp if within bounds) + // 修复:原 +14 漏了 mov rdi,r9(3 字节)→ 跳到指令中间(0xf9)→ 死循环 + w8(buf, pos+cp, 118); w8(buf, pos+cp+1, 17); cp = cp + 2; // call heap_expand -- E8 xx xx xx xx (patched in elf_gen after heap_expand emitted) g_heap_expand_call_pos = pos + cp; e2_w8(buf, pos+cp, 232); e2_w32(buf, pos+cp+1, 0); cp = cp + 5; @@ -1078,7 +1079,14 @@ fn elf_gen(buf: string) -> int { pc2 := r64(g_ir_func_param_count, fi * 8); fsz := r64(g_x86_func_code_sz, fi * 8); + // SysV 16 字节对齐(发现 11):call 后 rsp%16=8; + // opt≥1 有 6 个 push(rbx,r12-15,rbp)→ rsp%16=8 → size 需 ≡8 (mod 16); + // opt<1 有 1 个 push(rbp)→ rsp%16=0 → size 需 ≡0 (mod 16)。 g_x86_emit_stack_size = vc2 * 8; + if (g_x86_emit_stack_size % 16 == 0 && g_opt_level >= 1) || + (g_x86_emit_stack_size % 16 == 8 && g_opt_level < 1) { + g_x86_emit_stack_size = g_x86_emit_stack_size + 8; + } total_code = total_code + sz_push_rbp() + sz_mov_rbp_rsp(); if g_opt_level >= 1 { total_code = total_code + 18; } // push rbx,r12-r15(9) + pop r15-r12,rbx(9) ss_dry := g_x86_emit_stack_size; @@ -1195,7 +1203,12 @@ fi = 0; loop { if fi >= g_ir_func_count { break; } g2_init(); g_current_func_var_start = vs; vi := 0; loop { if vi >= vc { break; } g2_slot(vs + vi); vi = vi + 1; } + // SysV 16 字节对齐(发现 11):与 dry run 相同的对齐规则 g_x86_emit_stack_size = vc * 8; + if (g_x86_emit_stack_size % 16 == 0 && g_opt_level >= 1) || + (g_x86_emit_stack_size % 16 == 8 && g_opt_level < 1) { + g_x86_emit_stack_size = g_x86_emit_stack_size + 8; + } // Init label state for single-pass backpatching (-1 = not yet seen) li2 : ., mut = 0; @@ -1225,17 +1238,43 @@ fi = 0; loop { if fi >= g_ir_func_count { break; } // Save register and caller-stack params into this function's slots. pi := 0; loop { if pi >= pc { break; } po2 := -(vs + pi + 1 - g_current_func_var_start) * 8; // force stack slot, ignore reg alloc - if pi == 0 { cp = cp + e2_st(buf, cp, 7, po2); } - if pi == 1 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 117); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 2 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 85); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 3 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 4 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 69); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 5 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } - if pi >= 6 { + pty := irv_type(vs + pi); + if pty == TI_FLOAT && pi < 6 { + // float 参数在 XMM:movsd [rbp+po2], xmm{frn}(SysV) + // frn = 第 pi 个参数前的 float 参数数 + frn : ., mut = 0; + fj : ., mut = 0; + loop { if fj >= pi { break; } + if irv_type(vs + fj) == TI_FLOAT { frn = frn + 1; } + fj = fj + 1; } + if frn < 8 { + // movsd [rbp+po2], xmm{frn} — F2 0F 11 /rn(mod=01, rm=5) + w8(buf, cp, 242); w8(buf, cp+1, 15); w8(buf, cp+2, 17); + w8(buf, cp+3, 64 + frn * 8 + 5); w8(buf, cp+4, po2); cp = cp + 5; + } else { + // 9+ float 参数在栈上(边缘场景,位置布局简化处理) + caller_off := 16 + (pi - 6) * 8; + if g_opt_level >= 1 { caller_off = caller_off + 40; } + cp = cp + e2_sd_load(buf, cp, caller_off); + cp = cp + e2_sd_store(buf, cp, po2); + } + } else if pi >= 6 { caller_off := 16 + (pi - 6) * 8; if g_opt_level >= 1 { caller_off = caller_off + 40; } - cp = cp + e2_ld(buf, cp, 10, caller_off); - cp = cp + e2_st(buf, cp, 10, po2); + if pty == TI_FLOAT { + cp = cp + e2_sd_load(buf, cp, caller_off); + cp = cp + e2_sd_store(buf, cp, po2); + } else { + cp = cp + e2_ld(buf, cp, 10, caller_off); + cp = cp + e2_st(buf, cp, 10, po2); + } + } else { + if pi == 0 { cp = cp + e2_st(buf, cp, 7, po2); } + if pi == 1 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 117); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 2 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 85); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 3 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 4 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 69); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 5 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } } pi = pi + 1; } diff --git a/src/arch/linux/ld/instr.cr b/src/arch/linux/ld/instr.cr index 7bcf941..70cb989 100644 --- a/src/arch/linux/ld/instr.cr +++ b/src/arch/linux/ld/instr.cr @@ -262,6 +262,86 @@ fn e2_alu(b: string, p: int, op: int) -> int { return cp - p; } +// ── SSE2 double 运算(IEEE 754 标准,float 支持)── +// movsd xmm0, [rbp+disp] — F2 0F 10 /0 +fn e2_sd_load(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 000 101 + } else { + w8(b, cp, 133); cp = cp + 1; // ModRM 10 000 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} +// movsd xmm1, [rbp+disp] — F2 0F 10 /1 +fn e2_sd_load1(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 77); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 001 101 + } else { + w8(b, cp, 141); cp = cp + 1; // ModRM 10 001 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} +// movsd xmm{rn}, [rbp+disp] — F2 0F 10 /rn(rn=0..7,SysV float 参数) +fn e2_sd_load_x(b: string, p: int, o: int, rn: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 64 + rn * 8 + 5); w8(b, cp+1, o); cp = cp + 2; + } else { + w8(b, cp, 128 + rn * 8 + 5); cp = cp + 1; + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + +// 存返回值到 dest:float → movsd [slot], xmm0(SysV XMM0 返回);int → rax +fn e2_store_ret(b: string, p: int, d: int) -> int { + if d >= 0 && irv_type(d) == TI_FLOAT { + return e2_sd_store(b, p, g2_slot(d)); + } + return e2_st(b, p, 0, g2_slot(d)); +} + +// 压栈 float(8 字节):sub rsp,8 + movsd [rsp],xmm0 +fn e2_push_xmm0(b: string, p: int) -> int { + cp := p; + w8(b, cp, 72); w8(b, cp+1, 131); w8(b, cp+2, 236); w8(b, cp+3, 8); cp = cp + 4; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 17); w8(b, cp+3, 4); w8(b, cp+4, 36); cp = cp + 5; + return cp - p; +} + +// cvtsi2sd xmm0, [rbp+disp] — F2 0F 2A /0(int→float 转换) +fn e2_sd_cvt(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 42); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 000 101 + } else { + w8(b, cp, 133); cp = cp + 1; // ModRM 10 000 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + +// movsd [rbp+disp], xmm0 — F2 0F 11 /0 +fn e2_sd_store(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 17); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; + } else { + w8(b, cp, 133); cp = cp + 1; + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + // ── emit_instr: write one instruction to buffer, return bytes written ── fn e2_load_var(buf: string, pos: int, reg: int, var_idx: int) -> int { @@ -302,6 +382,24 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_NOP { return 0; } + if op == IR_I2F && d >= 0 { + // int → float:cvtsi2sd xmm0, [rbp+disp] — F2 0F 2A /0,然后 movsd 存回 + do2 := g2_slot(d); + cp = cp + e2_sd_cvt(buf, pos+cp, g2_slot(s1)); // cvtsi2sd xmm0, [s1] + cp = cp + e2_sd_store(buf, pos+cp, do2); + return cp; + } + + if op == IR_F2I && d >= 0 { + // float → int:movsd xmm0, [s1];cvttsd2si rax, xmm0(F2 48 0F 2C C0);存回 + do2 := g2_slot(d); + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); + w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 72); w8(buf, pos+cp+2, 15); + w8(buf, pos+cp+3, 44); w8(buf, pos+cp+4, 192); cp = cp + 5; + cp = cp + e2_st(buf, pos+cp, 0, do2); + return cp; + } + if op == IR_CONST && d >= 0 { do2 := g2_slot(d); if ti == TI_STR { @@ -321,6 +419,35 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_BINARY { do2 := g2_slot(d); + if ti == TI_FLOAT { + // float 运算(SSE2 double,IEEE 754)——标准答案实现 + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); // xmm0 = s1 + cp = cp + e2_sd_load1(buf, pos+cp, g2_slot(s2)); // xmm1 = s2 + // F2 0F 5x C1:addsd/subsd/mulsd/divsd xmm0, xmm1 + if s3 == OP_ADD { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 88); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_SUB { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 92); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_MUL { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 89); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_DIV { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 94); w8(buf, pos+cp+3, 193); cp = cp + 4; } + if s3 >= OP_ADD && s3 <= OP_DIV { + cp = cp + e2_sd_store(buf, pos+cp, do2); + } else if s3 >= OP_EQ && s3 <= OP_GE { + // float 比较:comisd xmm0, xmm1 — 66 0F 2F C1,用无符号标志 + // (IEEE 754:< → CF=1;== → ZF=1;> → CF=0&&ZF=0) + // 比较结果是 int(0/1),用整数路径存储 + w8(buf, pos+cp, 102); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 47); w8(buf, pos+cp+3, 193); cp = cp + 4; + sop : ., mut = 148; // sete + if s3 == OP_NE { sop = 149; } + else if s3 == OP_LT { sop = 146; } // setb(CF) + else if s3 == OP_GT { sop = 151; } // seta(CF=0 && ZF=0) + else if s3 == OP_LE { sop = 150; } // setbe + else if s3 == OP_GE { sop = 147; } // setae + w8(buf, pos+cp, 15); w8(buf, pos+cp+1, sop); w8(buf, pos+cp+2, 192); cp = cp + 3; + // movzx r10d, al — 44 0F B6 D0 + w8(buf, pos+cp, 68); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 182); w8(buf, pos+cp+3, 208); cp = cp + 4; + cp = cp + e2_st(buf, pos+cp, 10, do2); + } + return cp; + } cp = cp + e2_load_var(buf, pos+cp, 10, s1); cp = cp + e2_load_var(buf, pos+cp, 11, s2); if s3 == OP_ADD { cp = cp + e2_alu(buf, pos+cp, 1); } @@ -420,19 +547,51 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_CALL { fa := s1; ac := s2; + // SysV AMD64 参数分派:int 用 ir(0-5 → rdi,rsi,rdx,rcx,r8,r9), + // float 用 fr(0-7 → xmm0-7),各自独立编号(标准答案) + // 第一遍:寄存器参数(位置顺序,左到右) + ir_cnt : ., mut = 0; fr_cnt : ., mut = 0; ai := 0; - loop { if ai >= ac { break; } if ai >= 6 { break; } - r := -1; - if ai == 0 { r = 7; } if ai == 1 { r = 6; } if ai == 2 { r = 2; } if ai == 3 { r = 1; } if ai == 4 { r = 8; } if ai == 5 { r = 9; } - if r >= 0 { cp = cp + e2_load_var(buf, pos+cp, r, fa + ai); } + loop { if ai >= ac { break; } + pt := irv_type(fa + ai); + if pt == TI_FLOAT { + if fr_cnt < 8 { + cp = cp + e2_sd_load_x(buf, pos+cp, g2_slot(fa + ai), fr_cnt); + fr_cnt = fr_cnt + 1; + } + } else { + if ir_cnt < 6 { + r := -1; + if ir_cnt == 0 { r = 7; } if ir_cnt == 1 { r = 6; } if ir_cnt == 2 { r = 2; } + if ir_cnt == 3 { r = 1; } if ir_cnt == 4 { r = 8; } if ir_cnt == 5 { r = 9; } + cp = cp + e2_load_var(buf, pos+cp, r, fa + ai); + ir_cnt = ir_cnt + 1; + } + } ai = ai + 1; } - // System V AMD64 passes the 7th and later arguments on the stack, - // rightmost first, so argument 7 is closest to the return address. + // 第二遍:栈参数(右到左压,第 7 个 int / 第 9 个 float 超限才压) + stack_total : ., mut = 0; stack_ai : ., mut = ac - 1; loop { - if stack_ai < 6 { break; } - cp = cp + e2_load_var(buf, pos+cp, 10, fa + stack_ai); - e2_w8(buf, pos+cp, 65); e2_w8(buf, pos+cp+1, 82); cp = cp + 2; // push r10 + if stack_ai < 0 { break; } + ic2 : ., mut = 0; fc2 : ., mut = 0; + j2 : ., mut = 0; + loop { if j2 >= stack_ai { break; } + if irv_type(fa + j2) == TI_FLOAT { fc2 = fc2 + 1; } else { ic2 = ic2 + 1; } + j2 = j2 + 1; } + if irv_type(fa + stack_ai) == TI_FLOAT { + if fc2 >= 8 { + cp = cp + e2_sd_load_x(buf, pos+cp, g2_slot(fa + stack_ai), 0); + cp = cp + e2_push_xmm0(buf, pos+cp); + stack_total = stack_total + 1; + } + } else { + if ic2 >= 6 { + cp = cp + e2_load_var(buf, pos+cp, 10, fa + stack_ai); + e2_w8(buf, pos+cp, 65); e2_w8(buf, pos+cp+1, 82); cp = cp + 2; // push r10 + stack_total = stack_total + 1; + } + } stack_ai = stack_ai - 1; } // Match builtins by interned string index (integer compare, no str_eq) @@ -443,12 +602,12 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { cp = cp + e2_mov(buf, pos+cp, 2, 1); // syscall: 2-byte 0x0F 0x05 e2_w8(buf, pos+cp, 15); e2_w8(buf, pos+cp+1, 5); cp = cp + 2; - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_load8 { // movzx rax, byte [rdi+rsi] — REX.W + 0x0FB6 + SIB cp = cp + emit_rex(buf, pos+cp, 1, 0, 0, 0); e2_w8(buf, pos+cp, 15); cp = cp + 1; e2_w8(buf, pos+cp, 182); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 0, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_store8 { // mov [rdi+rsi], dl — 0x88 + SIB (3rd arg in rdx = register 2) e2_w8(buf, pos+cp, 136); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 2, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); @@ -457,7 +616,7 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // mov rax, [rdi+rsi] — REX.W + 0x8B + SIB cp = cp + emit_rex(buf, pos+cp, 1, 0, 0, 0); e2_w8(buf, pos+cp, 139); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 0, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_store_str_ptr { // mov [rdi + rsi], rdx // mov [rdi+rsi], rdx — REX.W + 0x89 + SIB @@ -521,7 +680,7 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // test dl, dl e2_w8(buf, pos+cp, 132); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 3, 2, 2); e2_w8(buf, pos+cp, 117); e2_w8(buf, pos+cp+1, 241); cp = cp + 2; // jne copy_loop - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_w64 { // w64(buf, pos, val) → mov [rsi+rdi??], rdx // Actually args: rdi=buf, rsi=pos, rdx=val @@ -583,13 +742,13 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { g_x86_ext_rel_count = g_x86_ext_rel_count + 1; cp = cp + e2_call(buf, pos+cp, 0); } - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else { // xor eax, eax e2_w8(buf, pos+cp, 49); e2_w8(buf, pos+cp+1, 192); cp = cp + 2; - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } - stack_count := ac - 6; + stack_count := stack_total; // 实际压栈数(int 超 6 + float 超 8) if stack_count > 0 { stack_bytes := stack_count * 8; if stack_bytes <= 127 { @@ -665,7 +824,10 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_RETURN { if s1 >= 0 { - if r64(g_x86_is_global, s1 * 8) != 0 { + if irv_type(s1) == TI_FLOAT { + // float 返回:movsd xmm0, [slot](SysV 返回值在 XMM0) + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); + } else if r64(g_x86_is_global, s1 * 8) != 0 { // Global: load via RIP-relative into rax grow_rip_patch(g_x86_rip_patch_count + 1); w64(g_x86_rip_patch_pos, g_x86_rip_patch_count * 8, pos + cp + 3); @@ -858,12 +1020,13 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // jne .safe (skip ud2 if non-null) safe_jmp_pos := pos+cp; e2_w8(buf, pos+cp, 117); e2_w8(buf, pos+cp+1, 0); cp = cp + 2; // placeholder - // .crash: ud2 - w8(buf, cp, 15); w8(buf, cp+1, 11); cp = cp + 2; - // Patch jae to jump here - e2_w32(buf, crash_jmp_pos + 2, (pos+cp) - (crash_jmp_pos + 6)); - // Patch jne to jump past ud2 to .safe - w8(buf, safe_jmp_pos + 1, (pos+cp) - (safe_jmp_pos + 2) + 2); + // .crash: ud2(必须写 pos+cp 绝对位置——修复前写 buf[cp] 污染函数头) + e2_w8(buf, pos+cp, 15); e2_w8(buf, pos+cp+1, 11); cp = cp + 2; + // Patch jae to jump to ud2 (crash): target = crash_jmp_pos+6+3+2 + // (jae 6 + test 3 + jne 2 = ud2 起点)。修复前跳到 .safe,越界不崩溃。 + e2_w32(buf, crash_jmp_pos + 2, (pos+cp) - (crash_jmp_pos + 6) - 2); + // Patch jne to jump past ud2 to .safe(修复前多 +2,跳到指令中间) + w8(buf, safe_jmp_pos + 1, (pos+cp) - (safe_jmp_pos + 2)); // .safe: deref } // mov r10, [r10] diff --git a/src/compiler/ast.cr b/src/compiler/ast.cr index 3be0fdf..ed701c0 100644 --- a/src/compiler/ast.cr +++ b/src/compiler/ast.cr @@ -571,6 +571,8 @@ IR_CALL_EXTERN : int = 45; // dest=result_var, s1=func_name_ni, s2=first_arg, s IR_LAZY_THUNK : int = 46; // dest=thunk_var, s1=expr_var — wrap as lazy thunk IR_LAZY_FORCE : int = 47; // dest=val_var, s1=thunk_var — force evaluation IR_FNADDR : int = 48; // dest=addr_var, s1=fn_name_ni — load function address (movabs + link-time patch) +IR_I2F : int = 49; // dest=float_var, s1=int_var — int → float(cvtsi2sd) +IR_F2I : int = 50; // dest=int_var, s1=float_var — float → int(cvttsd2si) // Resolution flag for BRANCH/JUMP (stored in type_kind field after label resolution) IR_RESOLVED : int = 1; diff --git a/src/compiler/ccr_io.cr b/src/compiler/ccr_io.cr index 74052ad..2c78c47 100644 --- a/src/compiler/ccr_io.cr +++ b/src/compiler/ccr_io.cr @@ -43,6 +43,10 @@ fn buf_write_i32(buf: string, pos: int, val: int) { w32(buf, pos, val); } +fn buf_write_i64(buf: string, pos: int, val: int) { + w64(buf, pos, val); +} + fn buf_read_u32(buf: string, pos: int) -> int { b0 := load8(buf, pos); b1 := load8(buf, pos + 1); @@ -76,6 +80,7 @@ fn buf_read_i64(buf: string, pos: int) -> int { h3 := load8(buf, pos + 7); hi : ., mut = h0 + h1 * 256 + h2 * 65536; if h3 >= 128 { hi = hi + (h3 - 256) * 16777216; } + else { hi = hi + h3 * 16777216; } // 修复 15:h3 < 128 时漏加 h3×2^24 → bit 56-62 丢失 // Keep the factor within the parser's supported integer-literal range. hi_part := hi * 65536; hi_part = hi_part * 65536; @@ -97,7 +102,7 @@ fn calc_ccr_size() -> int { } sz = sz + g_ir_func_count * 28; // func meta - sz = sz + g_ir_instr_count * 24; // instrs + sz = sz + g_ir_instr_count * 28; // instrs(s1 为 64 位) sz = sz + g_ir_var_count * 12; // vars sz = sz + g_ir_str_const_count * 4; // str_consts @@ -202,7 +207,9 @@ fn save_ccr(path: string) -> int { if ii >= g_ir_instr_count { break; } buf_write_u32(buf, pos, iri_op(ii)); pos = pos + 4; buf_write_i32(buf, pos, iri_dest(ii)); pos = pos + 4; - buf_write_i32(buf, pos, iri_s1(ii)); pos = pos + 4; + // 修复 14:s1 改 64 位——IR_CONST 的大 int 常量 / float 位模式 + // 之前被截断成 32 位(float 常量静默损坏) + buf_write_i64(buf, pos, iri_s1(ii)); pos = pos + 8; buf_write_i32(buf, pos, iri_s2(ii)); pos = pos + 4; buf_write_i32(buf, pos, iri_s3(ii)); pos = pos + 4; buf_write_u32(buf, pos, iri_tk(ii)); pos = pos + 4; @@ -406,7 +413,7 @@ fn load_ccr(data: string, fsize: int) -> int { if ii >= instr_cnt { break; } opcode := buf_read_u32(data, pos); pos = pos + 4; dest := buf_read_i32(data, pos); pos = pos + 4; - s1 := buf_read_i32(data, pos); pos = pos + 4; + s1 := buf_read_i64(data, pos); pos = pos + 8; // 修复 14:s1 64 位 s2 := buf_read_i32(data, pos); pos = pos + 4; s3 := buf_read_i32(data, pos); pos = pos + 4; tk := buf_read_u32(data, pos); pos = pos + 4; diff --git a/src/compiler/globals.cr b/src/compiler/globals.cr index 432b0d7..4bcbb96 100644 --- a/src/compiler/globals.cr +++ b/src/compiler/globals.cr @@ -138,6 +138,9 @@ g_plugin_rtypes : string, mut; g_plugin_rtype_count : int, mut; g_plugin_rtype_c // Pointer analysis storage g_pts : string, mut; g_pts_count : int, mut; g_pts_cap : int, mut; g_offsets : string, mut; g_offsets_count : int, mut; g_offsets_cap : int, mut; +// Alloc 序号 → DF 节点序号映射(修复 3:alloc pts 需要递增位号,provenance 按位号查 alloc 大小) +g_pa_alloc_count : int, mut; +g_pa_alloc_nodes : string, mut; g_pa_alloc_nodes_cap : int, mut; fn grow_plugin_tags(needed: int) { if needed < g_plugin_tag_cap { return; } diff --git a/src/compiler/ir_gen.cr b/src/compiler/ir_gen.cr index 8a3b30f..8e36a10 100644 --- a/src/compiler/ir_gen.cr +++ b/src/compiler/ir_gen.cr @@ -643,8 +643,24 @@ fn gen_expr(node: int) -> int { } } } - v := new_ir_var("bin", TI_INT); - emit(IR_BINARY, v, left_var, right_var, op, 0); + // float 运算:类型标记 TI_FLOAT(后端按 ti 分派 SSE2,IEEE 754 标准) + // int 操作数隐式转换(cvtsi2sd)——阶段 4 + fti : int = 0; + if lt == TI_FLOAT || rt == TI_FLOAT { + fti = TI_FLOAT; + if lt != TI_FLOAT { + t1 := new_ir_var("_f0", TI_FLOAT); + emit(IR_I2F, t1, left_var, 0, 0, TI_FLOAT); + left_var = t1; + } + if rt != TI_FLOAT { + t2 := new_ir_var("_f1", TI_FLOAT); + emit(IR_I2F, t2, right_var, 0, 0, TI_FLOAT); + right_var = t2; + } + } + v := new_ir_var("bin", fti); + emit(IR_BINARY, v, left_var, right_var, op, fti); return v; } diff --git a/src/compiler/lexer.cr b/src/compiler/lexer.cr index 6d8ea29..9f4afd4 100644 --- a/src/compiler/lexer.cr +++ b/src/compiler/lexer.cr @@ -107,6 +107,77 @@ fn lookup_keyword(s: string) -> int { return T_IDENT; } +// 2^k(纯整数,k >= 0) +fn pow2i(k: int) -> int { + v : int = 1; i : ., mut = 0; + loop { if i >= k { break; } v = v * 2; i = i + 1; } + return v; +} + +// decimal string → IEEE 754 binary64 位模式(纯整数近似,≤18 位有效数字) +// 实现:value = ip + fp/den → 整数部分位 + 64 位长除小数 → 53 位尾数窗口 +// 精度:截断(无舍入),≤18 位有效数字内 ~2ulp +fn str_to_f64_bits(s: string) -> int { + sl := str_len(s); + i : ., mut = 0; + neg : int = 0; + if i < sl && load8(s, i) == 45 { neg = 1; i = i + 1; } + ip : int = 0; fp : int = 0; den : int = 1; sd : int = 0; dg : ., mut = 0; + loop { if i >= sl { break; } + c := load8(s, i); + if c == 46 { sd = 1; i = i + 1; continue; } + if c < 48 || c > 57 { break; } + dg = dg + 1; + if dg <= 18 { + if sd != 0 { fp = fp * 10 + (c - 48); den = den * 10; } + else { ip = ip * 10 + (c - 48); } + } + i = i + 1; } + if ip == 0 && fp == 0 { + if neg != 0 { return -9223372036854775808; } + return 0; + } + // 小数 64 位(长除:r=fp,每轮 r×2 vs den) + frac64 : int = 0; + r : ., mut = fp; + bits : ., mut = 0; + loop { if bits >= 64 { break; } + if r >= 4611686018427387904 { r = r / 2; den = den / 2; } + r = r * 2; + frac64 = frac64 * 2; + if r >= den { r = r - den; frac64 = frac64 + 1; } + bits = bits + 1; } + // 整数部分位宽 + bi : ., mut = 0; t2 : ., mut = ip; + loop { if t2 == 0 { break; } t2 = t2 / 2; bi = bi + 1; } + mant : int = 0; + exp : int = 0; + if bi > 0 { + sh := 53 - bi; + mant = (ip * pow2i(sh)) + (frac64 / pow2i(64 - sh)); + exp = 1023 + (bi - 1); + } else { + // 纯小数:frac64 的最高位 + bf : ., mut = 0; t2 = frac64; + loop { if t2 == 0 { break; } t2 = t2 / 2; bf = bf + 1; } + if bf == 0 { + if neg != 0 { return -9223372036854775808; } + return 0; + } + sh := 53 - bf; + if sh >= 0 { mant = frac64 * pow2i(sh); } + else { mant = frac64 / pow2i(-sh); } + exp = 1023 + (bf - 65); + } + // 组装(mant 截断到 52 位——无舍入) + bits64 : int = 0; + if exp > 0 && exp < 2047 { + bits64 = (mant % 4503599627370496) + exp * 4503599627370496; + } + if neg != 0 { bits64 = bits64 + -9223372036854775808; } + return bits64; +} + fn add_tok(kind: int, lex: int, start_line: int, start_col: int) { grow_tokens(g_token_count + 1); tp := g_token_count * ESZ_TOKEN; @@ -236,8 +307,10 @@ fn tokenize(_src: string) { // Float: only consume the '.' when it does not start a '..' // range operator (otherwise `0..4` lexes as `0.` `.4` and the // range is silently lost — the for-loop body never executes). + has_dot : ., mut = 0; if cur_char_at(_src, _pos, _slen) == 46 && peek_at(_src, _pos, _slen) != 46 { _pos = _pos + 1; + has_dot = 1; loop { if is_digit(cur_char_at(_src, _pos, _slen)) != 0 { _pos = _pos + 1; } else { break; } } } // Suffix @@ -251,13 +324,18 @@ fn tokenize(_src: string) { suffix = str_sub(_src, ss, _pos - ss); } num_str := str_sub(_src, start, _pos - start - str_len(suffix)); - ival : ., mut = str_int(num_str); - if suffix == "u8" || suffix == "u16" || suffix == "u32" || suffix == "u64" { } - else if suffix == "i8" || suffix == "i16" || suffix == "i32" || suffix == "i64" { } - else if suffix == "f32" || suffix == "f64" { } - else if str_len(suffix) > 0 { } - if str_len(suffix) > 0 { add_tok(T_INT, -1, start_line, start_col); } - else { add_tok_int(T_INT, ival, start_line, start_col); } + // float 字面量(含小数点或 f32/f64 后缀)→ IEEE 754 binary64 位模式 + // 修复前 float 走 str_int(3.14 解析成 3,小数静默丢弃) + if has_dot != 0 || suffix == "f32" || suffix == "f64" { + add_tok_int(T_FLOAT, str_to_f64_bits(num_str), start_line, start_col); + } else { + ival : ., mut = str_int(num_str); + if suffix == "u8" || suffix == "u16" || suffix == "u32" || suffix == "u64" { } + else if suffix == "i8" || suffix == "i16" || suffix == "i32" || suffix == "i64" { } + else if str_len(suffix) > 0 { } + if str_len(suffix) > 0 { add_tok(T_INT, -1, start_line, start_col); } + else { add_tok_int(T_INT, ival, start_line, start_col); } + } _pos = skip_ws(_src, _pos, _slen); continue; } diff --git a/src/compiler/main.cr b/src/compiler/main.cr index 8bc524f..ac0f8ad 100644 --- a/src/compiler/main.cr +++ b/src/compiler/main.cr @@ -479,9 +479,16 @@ fn corec_main() -> int { } // === Pointer analysis + safety passes (always run, even at opt_level 0) === + base_diags := g_diag_count; ptr_analysis_all(); region_check_all(); provenance_verify_all(); + // 修复 5:编译期确定的越界(provenance 诊断)是硬错误——拦截编译。 + // 修复前诊断只记录不拦截,越界程序照常生成。 + if g_diag_count > base_diags { + print_diagnostics(); + return 1; + } // === build | ccr need lower_to_ccr === if g_opt_level >= 1 { diff --git a/src/compiler/provenance_verify.cr b/src/compiler/provenance_verify.cr index 85361c7..7e5195e 100644 --- a/src/compiler/provenance_verify.cr +++ b/src/compiler/provenance_verify.cr @@ -3,15 +3,27 @@ // Runs after PointerAnalysis (ptr_analysis.cr) and RegionCheck (region_check.cr). // Detects out-of-bounds pointer accesses at compile time. -fn get_alloc_size(alloc_node_seq: int) -> int { - op := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_OPCODE); - s1 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S1); - s2 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S2); - s3 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S3); +fn get_alloc_size(alloc_seq: int) -> int { + // 修复 3:alloc_seq 是 pts 位号(第几个 alloc),经映射表查 DF 节点序号再算大小。 + // 修复前直接当节点序号用 → 查到节点 0 → 恒返回 -1 → 运行时检查永不生成。 + if alloc_seq < 0 || alloc_seq >= g_pa_alloc_count { return -1; } + an := r64(g_pa_alloc_nodes, alloc_seq * 8); + op := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_OPCODE); + s1 := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_S1); + s3 := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_S3); - if op == IR_ALLOC { return 8; } // scalar = 8 bytes - if op == IR_ALLOC_STRUCT { return 8 + s2 * 8; } // struct size - if op == IR_ALLOC_ARRAY { return s1 * s2; } // count * element_size + // 修复 12:IR_ALLOC(标量变量槽标记)不是堆分配——不返回 8(修复前把 + // 变量槽当 8 字节堆块,误报/误取 size) + if op == IR_ALLOC_ARRAY { return s1 * 8; } // count * 8(元素恒 8 字节,见 instr.cr IR_ALLOC_ARRAY) + if op == IR_ALLOC_STRUCT { + // 与 instr.cr IR_ALLOC_STRUCT 一致:fc * 8(field count × 8) + fi : int = -1; si2 : ., mut = 0; + loop { if si2 >= g_struct_count { break; } + if si_name(si2) == s3 { fi = si2; break; } + si2 = si2 + 1; } + if fi >= 0 { return si_field_count(fi) * 8; } + return 8; + } return -1; // unknown (defer to runtime check) } diff --git a/src/compiler/ptr_analysis.cr b/src/compiler/ptr_analysis.cr index bb3604d..ef70a7d 100644 --- a/src/compiler/ptr_analysis.cr +++ b/src/compiler/ptr_analysis.cr @@ -40,6 +40,16 @@ fn grow_alloc_pts(n: int) { g_alloc_pts = nb; g_alloc_pts_cap = nc; } +fn grow_pa_alloc_nodes(n: int) { + if n < g_pa_alloc_nodes_cap { return; } + nc := g_pa_alloc_nodes_cap; + if nc == 0 { nc = 16; } + loop { if nc > n { break; } nc = nc * 2; } + nb := alloc(nc * 8); + if g_pa_alloc_nodes_cap > 0 { _dyncpy(g_pa_alloc_nodes, g_pa_alloc_nodes_cap * 8, nb); } + g_pa_alloc_nodes = nb; g_pa_alloc_nodes_cap = nc; +} + // Set a bit in a pts bitmap at given index fn pa_set_bit(bitmap: int, bitpos: int) -> int { // bitpos: which bit to set (0-63) @@ -192,10 +202,21 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { if d >= 0 { // Addr: ALLOC/REF/ADDR_INDEX → self-pointer - if op == IR_ALLOC || op == IR_ALLOC_STRUCT || op == IR_ALLOC_ARRAY { + if op == IR_ALLOC_STRUCT || op == IR_ALLOC_ARRAY { + // 修复 12:IR_ALLOC(标量变量槽标记,不发射代码)不是堆分配, + // 不参与 pts 追踪——修复前它被分配 pts 位,导致 p = &arr[i] + // 的 pts 含变量槽的位(多个 alloc 位污染)→ s3 取错 alloc。 if r64(g_pts, d * 8) == 0 { - w64(g_pts, d * 8, 1); - changed = 1; + // 修复 3:每个 alloc 分配递增位号(bit = alloc_seq),并登记 + // alloc_seq → DF 节点序号。修复前恒设 bit 0——所有 alloc 别名 + // 串扰,provenance 的 get_alloc_size(0) 查到节点 0 → 检查永远不生成。 + if g_pa_alloc_count < 64 { + grow_pa_alloc_nodes(g_pa_alloc_count + 1); + w64(g_pa_alloc_nodes, g_pa_alloc_count * 8, ni); + w64(g_pts, d * 8, pa_set_bit(0, g_pa_alloc_count)); + g_pa_alloc_count = g_pa_alloc_count + 1; + changed = 1; + } } w64(g_offsets, d * 8, 0); } @@ -208,7 +229,26 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { if op == IR_ADDR_INDEX && s1 >= 0 { if pa_merge_pts(d, s1) != 0 { changed = 1; } - w64(g_offsets, d * 8, r64(g_offsets, s1 * 8)); + // offset 由索引 s2 决定:常量索引可精确计算(idx*8), + // 运行时索引 → 未知(-1),迫使 provenance_verify 生成运行时检查。 + // 修复前:无条件传播 s1 的 offset(数组=0),运行时越界被误判为 + // 编译期安全 → 越界裸读(见 docs/compcert-reference.md 审查记录)。 + base_off := r64(g_offsets, s1 * 8); + idx_val : int = -1; + if s2 >= 0 { + prod := r64(g_df_var_producer, s2 * 8); + if prod >= 0 { + prod_op := r64(g_df_nodes, prod * ESZ_DFNODE + OFF_DF_OPCODE); + if prod_op == IR_CONST { + idx_val = r64(g_df_nodes, prod * ESZ_DFNODE + OFF_DF_S1); + } + } + } + if idx_val >= 0 && base_off >= 0 { + w64(g_offsets, d * 8, base_off + idx_val * 8); + } else { + w64(g_offsets, d * 8, -1); + } } // BINARY with PTR ops: propagate with offset @@ -234,11 +274,15 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { } } - // Copy: LOAD/STORE propagate pts along def-use - if (op == IR_LOAD || op == IR_STORE) && s1 >= 0 { + // LOAD: d ← s1 拷贝传播 + if op == IR_LOAD && s1 >= 0 { if pa_merge_pts(d, s1) != 0 { changed = 1; } w64(g_offsets, d * 8, r64(g_offsets, s1 * 8)); } + // STORE: s1 ← s2 拷贝传播。修复 4:IR_STORE 的 dest 恒为 -1, + // 原代码把 STORE 混进 LOAD 分支(用 d 传播)→ 永不执行 → + // p = &arr[i] 的 offset 丢失 → 越界检查被跳过。 + // 注意:此分支必须在 if d >= 0 块外(d 恒为 -1)。 // PHI: merge pts from both predecessors (implicit flow) if op == IR_PHI { @@ -253,6 +297,12 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { } } + // Store: s1 ← s2 拷贝传播(IR_STORE 的 d 恒为 -1,必须在 if d >= 0 块外) + if op == IR_STORE && s1 >= 0 && s2 >= 0 { + if pa_merge_pts(s1, s2) != 0 { changed = 1; } + w64(g_offsets, s1 * 8, r64(g_offsets, s2 * 8)); + } + // Store: *p = v (Andersen store rule) — s1=ptr, s2=val if op == IR_STORE_PTR && s1 >= 0 && s2 >= 0 { if pa_store(s1, s2) != 0 { changed = 1; } diff --git a/src/compiler/region_check.cr b/src/compiler/region_check.cr index d3c2b9d..3a49f4c 100644 --- a/src/compiler/region_check.cr +++ b/src/compiler/region_check.cr @@ -37,8 +37,11 @@ fn rc_pts_has_escaped(pts: int, ni: int, nstart: int) -> int { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + // 修复 3 配套:pts 位号 = 全局 alloc 序号(g_pa_alloc_count), + // 经映射表查 DF 节点序号(旧代码 bi+nstart 是错误语义——alloc 序号 + // 不是"函数内第 nstart+bi 个节点")。 + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); deref_sg := subgraph_containing(ni); if alloc_sg >= 0 && deref_sg >= 0 { alloc_exit := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_EXIT); @@ -66,8 +69,8 @@ fn rc_return_escape(ni: int, s1: int, nstart: int) { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); if alloc_sg >= 0 { alloc_sg_kind := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_KIND); if alloc_sg_kind == SG_FUNC { // function-level alloc = ok to return @@ -112,8 +115,8 @@ fn region_check_func(nstart: int, ncount: int) { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); deref_sg := subgraph_containing(ni); if alloc_sg >= 0 && deref_sg >= 0 { alloc_exit := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_EXIT); diff --git a/src/stdlib/fmt.cr b/src/stdlib/fmt.cr index 0d51822..cfe418a 100644 --- a/src/stdlib/fmt.cr +++ b/src/stdlib/fmt.cr @@ -190,3 +190,82 @@ fn format2(fmt_str: string, a0: string, a1: string) -> string { fn format_int(fmt_str: string, val: int) -> string { return format(fmt_str, int_str(val)); } + +// ── float 打印(IEEE 754 double → 十进制字符串,定点最多 6 位小数)── +// 纯整数实现:提取符号/指数/尾数 → 规范化 → 整数部分 + 小数长除 + +fn fpow2i(k: int) -> int { + v : int = 1; i : ., mut = 0; + loop { if i >= k { break; } v = v * 2; i = i + 1; } + return v; +} + +fn float_str_bits(bits: int) -> string { + // 符号(bit63) + neg : int = 0; u : int = bits; + if u < 0 { neg = 1; u = u - (-9223372036854775808); } // 减 -2^63 = 清 bit63(无 & 运算符) + // 提取字段(除以 2^52 代替移位) + exp := (u / 4503599627370496) % 2048; + mant := u % 4503599627370496; + // 特殊值(IEEE 754 标准) + if exp == 0 && mant == 0 { + if neg != 0 { return "-0"; } + return "0"; + } + if exp == 2047 { + if mant == 0 { if neg != 0 { return "-inf"; } return "inf"; } + return "nan"; + } + // 归一化:m = 1.mant(正规)或 0.mant(次正规),e = exp - 1023 + m : int = mant; e : int = exp - 1023; + if exp != 0 { m = mant + 4503599627370496; } + else { e = e + 1; } + // value = m × 2^(e-52)(m 是 2^52 缩放的尾数) + ip : int = 0; + den : int = 1; // 小数分母(小数部分 = r/den) + r : int = 0; + if e >= 52 { + if e - 52 <= 10 { ip = m * fpow2i(e - 52); } + else { ip = m * 1024; } // 大数近似(超出 int 范围) + } else { + if 52 - e <= 53 { + den = fpow2i(52 - e); + ip = m / den; + r = m % den; + } else { + ip = 0; den = fpow2i(53); r = m; // 极小值 + } + } + // 长除:r × 10 / den,提取 7 位(第 7 位用于舍入) + frac_str : ., mut = ""; + r2 : ., mut = r; + di : ., mut = 0; + loop { if di >= 7 { break; } + r2 = r2 * 10; + dg2 := r2 / den; + if dg2 > 9 { dg2 = 9; } + r2 = r2 - dg2 * den; + if di < 6 { frac_str = frac_str + int_str(dg2); } + else if dg2 >= 5 { + // 第 7 位 ≥ 5:第 6 位 +1(简单舍入) + fl2 := str_len(frac_str); + if fl2 > 0 { + last := load8(frac_str, fl2 - 1) - 48; + if last < 9 { + pre := str_sub(frac_str, 0, fl2 - 1); + frac_str = pre + chr(last + 49); + } + } + } + di = di + 1; } + // 去尾零 + fl := str_len(frac_str); + loop { if fl <= 0 { break; } if load8(frac_str, fl - 1) != 48 { break; } fl = fl - 1; } + if fl > 0 { frac_str = str_sub(frac_str, 0, fl); } + // 组装 + out : ., mut = ""; + if neg != 0 { out = out + "-"; } + out = out + int_str(ip); + if fl > 0 { out = out + "." + frac_str; } + return out; +} From b13c85368de1ff6eb9019694b629e1e1716f7725 Mon Sep 17 00:00:00 2001 From: DslsDZC Date: Tue, 11 Aug 2026 17:59:32 +0800 Subject: [PATCH 9/9] =?UTF-8?q?fix:=20CI=20workflow=20checkout=20=E6=94=B9?= =?UTF-8?q?=E5=9B=9E=20@v5=EF=BC=88SHA=20pin=20=E5=AF=BC=E8=87=B4=20workfl?= =?UTF-8?q?ow=20=E8=A7=A3=E6=9E=90=E5=A4=B1=E8=B4=A5=EF=BC=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/core-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/core-ci.yml b/.github/workflows/core-ci.yml index 7d163d8..15f6175 100644 --- a/.github/workflows/core-ci.yml +++ b/.github/workflows/core-ci.yml @@ -51,7 +51,7 @@ jobs: # run_type: full steps: - name: checkout the source code - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 (SHA pin, sha_pinning_required) + uses: actions/checkout@v5 with: fetch-depth: 2