稳定语义身份
作者定义的 @id 与编译器身份会在源代码、HIR、图序列化、诊断和生成符号之间保持一致。包含 NUL 的身份在机器输出前被拒绝。
先稳定身份,再修改源代码。
Semaprax 语义程序图在内容派生的修订版下记录类型化声明、效果、契约、所有权事实、调用关系和编译身份。
entity Semaprax
status 预 Alpha 研究
snapshot c16348f
authority github.com/wavect/semaprax| 仓库快照 | c16348f · 2026-08-29. 文档工作流通过,但总体工作流失败,因此本页不把该 head 标为已验证。 |
|---|---|
| 完整产品状态 | 49 部分 · 0 已实现 · 0 缺失 |
| 语义图与项目契约 | Graph ≤ v24 · Project v1 基线 · Project v8, v9, v10 开发者预览 |
| 提升基线 | 本快照不声称存在精确且已通过的提升提交或工作流运行。 |
| 源代码中的开发者预览 | Owned 数据、record 与 UTF-8 项目配置,以及软件包分析、借用扩展、Project Agent Transport 与 Revision Store 已存在于源代码中,但尚未发布或提升。 |
Semaprax 将人类可读源代码解析为经过验证的 HIR,并按功能选择语义图模式。Graph v22 加入 owned record 与 variant 事实,v23 加入 Shared Loan Plan,v24 加入投影 owned 字节字段借用。Project v1 仍是已提升基线;Project v8-v10 及其软件包路径只是开发者预览,并非受支持的公开 API。
作者定义的 @id 与编译器身份会在源代码、HIR、图序列化、诊断和生成符号之间保持一致。包含 NUL 的身份在机器输出前被拒绝。
Agent Context v1 与 v2 返回受依赖关系约束的图切片,并明确限制节点、字节、深度与遍历方向。
补丁操作以语义身份和精确的图修订版为目标。系统会直接拒绝过期修订版;当前提供的操作类型也有意保持在有限范围内。
Review、Impact、Target 和 Workspace 验证流程会生成确定性产物,并明确说明这些产物无法证明什么。Workspace Operations v1 只允许在严格限制下重命名声明和导入别名,发布前还必须重新生成验证证据。
CleanupPlan 与 Shared Loan Plan 将所有权和借用事实与 lowering 分离。Graph v24 增加投影字节字段借用。这不是完整且兼容 Rust 的借用检查器。
Workspace Operations v1 仍是狭窄的重命名协议,旁边另有变更、替换、结构与发布层。Project v8-v10、Agent Transport v5、Revision Store v1、软件包报告、离线锁与兼容性证据仍未提升。
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
ensures result == left + right
{
left + right
}GitHub 规范是权威来源。本页是带日期的研究摘要。 GitHub 仓库.
不是。它是编译器的类型化版本化程序表示,不是通用文档或向量集合。
还不能。单文件补丁仍受到严格限制。Workspace Operations v1 只允许在现有受控路径中执行通过证据校验的重命名,不能任意访问整个源代码树,也不保证整个 Git 操作具备原子性。