架构 · 源码、语义与权限

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

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

稳定身份连接受检查源码、语义查询、证明义务与修改建议。v0.9.0还以共享决策核心连接开发与运行时模型选择，部署权限仍由主机掌握。原生命令、数据和所有权扩展仍需显式选择相应配置。

semaprax://architecturev0.9.0

entity     Semaprax
status     Beta 测试版
snapshot   933196b
authority  github.com/wavect/semaprax

Semaprax 如何工作？

Semaprax 检查可读的 .spx 源码，并将其解析为 HIR，即带有类型信息的编译器表示。源码身份与语义身份将查询、定律义务、候选修改和执行绑定到被检查的程序。编码智能体可以使用这一核心周围的开发工具；运行时智能体则在显式提供的宿主能力下，分别解码提案、授权副作用并归约状态。

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

选择一个阶段，突出显示下方架构中对应的部分。

规范源码与稳定身份

可读的 .spx 仍是 Git 中的规范表示。显式 @id 让声明在受支持的显示名称变更后保留身份。编译器生成的修订绑定源码与选定前导库；图编码展示这些事实，并不替代源码。

受限上下文与紧凑投影

选择声明、方向、深度、节点数与字节上限。任务上下文以及文本、二进制或模型文本投影，都保留对选定事实的确切重放。原生语义上下文代理可以借助 Graft 或 Graphify 导航仓库，但不会将外部索引当作编译器事实。

源码定律与受保护的实现修复

原生 law 声明为契约要求与关系要求提供持久身份。单独选定的 LawSet 固定完整定律清单和严格策略。已安装的 Lean/Z3 适配器可证明已获准的标量、模运算、结构化和列表定律；过期、不受支持、未知和已被反证的结果保持区分。候选修复必须满足受到保护的需求。

带修订检查的语义修改

检查上下文、生成候选修改、预览影响与审阅结果、重放检查，然后授权应用。范围明确的表达式替换、结构化编辑和指定组合，各自保留操作与修订限制。源码定律编辑和实现修复遵循不同的保护规则。

受管理的发布与嵌入

受管理的工作区代次、候选证据和 Project 修订存储，将发布绑定到经过检查的候选版本。Rust 嵌入 API 提供范围明确的输入与不透明会话。仅通过多文件验证，并不会修改任意文件、Git 引用或编辑器缓冲区。

日常语言功能与集合

已获准的配置包括记录、变体、类、继承、带限定参数推断的泛型、Option/Result、循环、迭代器、函数值、字符串和字节。不可变 List<i64> 增加持久化 nil/cons/uncons 操作。一般约束与任意功能组合仍需各自的准入规则。

所有权与回调生命周期

拥有所有权的值、借用视图、清理计划及选定的资源组合均可执行。限定的闭包配置包括拥有所有权的 Bytes 捕获、复制的标量快照、事务式可变标量状态，以及同步借用文本捕获。每种配置分别检查逃逸、移动、回滚和清理规则；更广泛的生命周期关系仍待扩展。

受显式边界契约约束的 Rust API

预先准备的 Rust API 索引选择受支持的导入和确切 Cargo 输入。生成的所有权、借用视图与回调适配器，将经过检查的源码连接到真实的 Regex/Url 和 Serde/迭代器使用方。同线程 Future 桥接使用调用方拥有的执行器。外部假设保持显式；生成的连接代码并不能证明 crate 内部实现。

类型化运行时智能体

初始化、观察、提案、解码、授权、执行与归约。每轮重新授权，归约器选择 Continue、Complete、Suspend 或 Fail。默认在线路径使用解释器；显式启用的库路径接受调用方持有的原生 C11 或 Core Wasm 阶段宿主，其本地一致性证据有明确范围。

预算、持久化恢复与模型调用

显式适配器提供传输、凭据与存储。持久化配置在分发前确认意图，并将未解决的尝试保留为不确定状态。限制与回执区分调用、工作量、字节、token 和成本。通用宿主重试/故障切换与绑定的源码模型路径具有不同契约；后者不会自动切换提供方，也不会重试结果不确定的工作。

可恢复源码与拥有所有权的续体

解释器支持范围明确的顺序及依赖控制流的 yield、选定的拥有所有权的 Bytes 传递，以及经过认证的持久化源码配置。公共拥有所有权的智能体子集具有两轮生命周期和选定的进程重启验证。普通原生/Wasm 生成器仍拒绝包含 yield 的函数；通用调度器和统一续体 ABI 尚未完成。

连接编译器的开发工具

完整工具链的 harness 协调显式任务、编译器反馈、提供方描述、按项目锁定与信任、模型路由、技能和桥接。官方 Ponytail/Caveman 技能包、Graft/Graphify 适配器与 RTK 模型视图服务于选定工作流。具有权威性的命令结果与供模型阅读的紧凑输出保持分离。

经检查的开发重载

持续保留的解释器会话检查候选修改、规划兼容性，并在调用之间激活修改。轮询监视声明的 Project 输入；无效修改不会影响当前修订的可用性。VS Code 控件展示当前、待激活和未提交状态。源码智能体日志迁移属于完整工具链中的独立路径。

应用与经济智能体配置

参考服务将经过检查的会话、任务与作业决策，同快照宿主、显式 HTTP/TLS 以及选定的 JSON 事件或 OTLP 遥测组合起来。已通过的 Linux/Podman 流程仍有明确范围；SQL 适配器会被拒绝。经济智能体保留由宿主负责的钱包、批准、签名和对账边界。

生成的包与本地注册表信任

拥有所有权数据的 Project 配置，以及一个由编译器生成的私有泛型 Wasm 端点，都具备生成使用方的验证证据。公共泛型接口仍不受支持，也未发布。本地签名注册表元数据、持有的代次与锁定读取，本身不提供托管包注册表或网络获取权限。

证明与发布来源

精确标签的Lean作业检查有限形式化内核和证明义务导出。发布作业另行证明五份归档、验证汇总签名，并在发布前执行各原生安装流程。这些证据不能证明整门语言正确、归档已公证或跨主机可复现。

一个决策核心，两个领域

硬性筛选先检查保密要求、工具、模态、上下文与预算，再向建议型路由器提供候选。开发阶段与运行时部署共享引擎，但证据键独立。规则路由不调用路由模型；注明日期的支持记录中，没有学习型适配器通过实测或资格门槛。

持久回合与选择边界

只有已结算并接受的回合才能开启新路由。交接最多携带16 KiB状态、已接受输出的摘要与结果引用，不复制对话。委派从父预算预留额度并继承截止时间。工具或专家选择须依据当前授权和参数模式重新授权；状态不明时停止核对。

原生命令配置与有界数据

Project v26/v28源码命令仅支持原生执行。v28允许每个String最大1 MiB及stdout/stderr合计1 MiB暂存输出，支持有界追加；读取文件和能力限制保持原有范围。std.data.json.scan验证完整UTF-8 JSON并显式选择重复键策略，std.pattern提供有界ASCII字节模式匹配。这些扩展不会自动放宽其他解释器、Wasm或公共API配置。

编译器指导与保留证据的优化

内置诊断主题提供精确导入、效果声明、所有权修复及支持语法。清单格式化使用显式fmt –manifest模式。标签中的优化保留身份、HIR回放、借用记账与资源上限；各自凭据和待验证门槛保持可见，不等同于已测得整项目加速。

源代码投影保持可读

module examples.meaning;

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

@id("app.main")
fn main() -> i64
    ensures result == 42
{
    add(19, 23)
}

// STATUS

审计快照中的仓库状态

仓库快照	`933196b` · 2026-10-15. v0.9.0 标签指向固定的源码提交。该标签的确切 CI 已成功完成，但不构成全面的生产可用性或安全保证。
完整产品状态	55 部分 · 0 已实现 · 0 缺失
语义图与项目契约	规范源码、稳定 ID 和经过检查的编译器表示，将定律、语义查询、修改与执行连接起来。按功能选择的图模式和 Project 模式，各自保留独立的准入、兼容性和宿主权限契约。
已发布的 Beta 版本	`v0.9.0` · 2026年10月11日15:07 UTC发布，精确标签发布流水线的91项作业全部通过。五个平台归档和两个安装脚本附带SHA256SUMS、五份归档证明及经过独立验证的汇总签名来源记录。发布前必须通过各平台的原生安装流程。归档未经公证，也不承诺可复现构建；离线验证不能确认当前撤销状态。确切标签 CI.
包与 API 预览	此版本包含可用的语言、定律、开发工具和宿主集成配置。生成的 Rust/npm 包、公共泛型 ABI 及更广泛的平台支持，仍须分别决定其发布与支持范围。