架构 · 按功能选择的语义图模式最高到 V24

让智能体直接查询程序模型,无需从文本重新推断语义。

先稳定身份,再修改源代码。

Semaprax 语义程序图在内容派生的修订版下记录类型化声明、效果、契约、所有权事实、调用关系和编译身份。

semaprax://architecturev0.2
entity     Semaprax
status     预 Alpha 研究
snapshot   c16348f
authority  github.com/wavect/semaprax
// STATUS

审计快照中的仓库状态

仓库快照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 如何工作?

Semaprax 将人类可读源代码解析为经过验证的 HIR,并按功能选择语义图模式。Graph v22 加入 owned record 与 variant 事实,v23 加入 Shared Loan Plan,v24 加入投影 owned 字节字段借用。Project v1 仍是已提升基线;Project v8-v10 及其软件包路径只是开发者预览,并非受支持的公开 API。

// 01

先稳定身份,再修改源代码。

稳定语义身份

作者定义的 @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、软件包报告、离线锁与兼容性证据仍未提升。

// 02

源代码投影保持可读

module examples.meaning;

@id("math.add")
fn add(left: i64, right: i64) -> i64
    requires left >= 0
    ensures result == left + right
{
    left + right
}

GitHub 规范是权威来源。本页是带日期的研究摘要。 GitHub 仓库.

// FAQ

不夸大的问答

语义图是知识图谱或 RAG 系统吗?

不是。它是编译器的类型化版本化程序表示,不是通用文档或向量集合。

智能体能通过语义补丁编辑任意程序吗?

还不能。单文件补丁仍受到严格限制。Workspace Operations v1 只允许在现有受控路径中执行通过证据校验的重命名,不能任意访问整个源代码树,也不保证整个 Git 操作具备原子性。

Wavect 研究项目: Wavect GmbH. 由 Wavect 创建的开源系统研究项目。