规范源码与稳定身份
可读 .spx 仍是 Git 中的规范表示。显式 @id 在受支持的显示名称修改后继续标识同一声明。修订绑定规范源码和编译器隐式 prelude,而非偶然的源码位置或图传输格式。
先稳定身份,再修改源代码。
Semaprax 语义程序图在内容派生的修订版下记录类型化声明、效果、契约、所有权事实、调用关系和编译身份。
entity Semaprax
status 预 Alpha 研究
snapshot b9f593c
authority github.com/wavect/semaprax| 仓库快照 | b9f593c · 2026-09-16. 审阅时 main 提交与 v0.5.0 标签一致。该标签的 CI 已成功完成;独立分支 CI 被取消。这不构成全面的生产可用性或安全保证。 |
|---|---|
| 完整产品状态 | 55 部分 · 0 已实现 · 0 缺失 |
| 语义图与项目契约 | 图模式按功能选择并保留旧版契约。Project v1 为基础;所有权数据配置 v8、v9、v10 和 v11 各自具有独立的准入与支持边界。 |
| 已发布的预发布版 | v0.5.0 · 发布于 2026 年 9 月 16 日 09:43 UTC。提供 Linux x86-64、macOS Apple Silicon 和 Windows x86-64 三种压缩包及 SHA256SUMS。包内 semaprax 是完整工具链,并非独立的 Cargo CLI。 确切标签 CI. |
| 包与 API 预览 | 发布工具链并不等于发布其生成的 Rust/npm 包,也不会自动开放私有 API。Project v8-v11 支持决定、公共泛型所有权、更广的平台支持及原生/Wasm Agent 阶段执行仍是独立事项。 |
Semaprax 将规范 .spx 源码解析为经过检查的 HIR,即表示类型化程序语义的编译器结构。稳定身份连接图查询、候选修改、执行和证据。受支持的修改必须匹配源码修订;运行时 Agent 提案必须通过类型化解码和确定性授权。图与回执本身绝不授予发布、联网或支付权限。
可读 .spx 仍是 Git 中的规范表示。显式 @id 在受支持的显示名称修改后继续标识同一声明。修订绑定规范源码和编译器隐式 prelude,而非偶然的源码位置或图传输格式。
Context v1/v2 限制深度、节点和字节预算;v2 增加定向遍历。任务上下文与 text、binary、model-text 投影支持经过重放检查的聚焦交换。更小的序列化输出不自动意味着更少的计费 token 或更好的回答。
检查上下文、派生候选、预览影响、审阅、重放检查,然后显式授权应用。操作家族已超出重命名,包含有边界的表达式替换、结构修改及指定的 rebase/merge 组合。各协议保留独立的修订、身份与操作限制。
受管工作区代、候选证据、Project 修订存储与 MCP 工作流保留显式写入和发布权限。多文件验证不等于任意原始路径、Git 或编辑器的原子更新。Rust 嵌入 API 提供输入上限、取消与不透明会话,并非无限制宿主访问。
获准配置涵盖记录、变体、类、继承、泛型、Option/Result、显式可变性、循环、集合、迭代器、函数值和有边界的闭包。文本、字节及内置库支持实用小程序。拥有捕获值的闭包、通用泛型约束和任意功能组合仍有限制。
已实现拥有与借用值、清理计划、借用事实和选定的资源/泛型组合。v0.5.0 增加直接拥有 String 的变体载荷,但泛型 String 替换及嵌套拥有记录的变体载荷仍受限。这不是完整的通用生命周期系统,也不表示兼容 Rust。
初始化、观察、提案、解码、授权、执行与归约。经检查的 reducer 选择 Continue、Complete、Suspend 或 Fail,每轮重新授权。编译得到的 Proposal 模式在副作用分派前约束流式解析与类型化解码。源码 Agent 阶段目前运行在保留的解释器中,不具备原生/Wasm 对等执行。
显式宿主适配器提供凭据、传输和存储。限制可涵盖调用、token、字节、截止时间和报价成本。持久配置先确认意图再分派,并拒绝不确定的重复派发。通用宿主配置支持有界重试/故障转移;绑定源码模型路线不会自动重试或切换服务商。观测用量不等于保证账单正确。
经检查的 HTTPS POST、Rust 宿主认证/会话及带检查点的任务属于独立集成配置,并非完整 Web 框架。经济智能体探索支付意图、模拟、审批和对账,钱包与签名由宿主提供。模型提案既不是支付权限,也不保证恰好一次结算。
Project v8 承载 Bytes 及选定 Option/Result 形式;v9 增加平面拥有记录,v10 增加拥有 UTF-8,v11 增加嵌套拥有记录。生成的 native/Rust、npm/Wasm 消费端、私有传输与公共泛型元数据各有契约。工具链发布、包发布与公共支持是不同决定。
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)
}本页依据固定提交和 v0.5.0 发布记录审阅。版本化规范定义准入范围与权限;矩阵和路线图中保留的 v0.4 发布标题属于历史记录,不代表最新版本。 GitHub 仓库.
本页依据固定提交和 v0.5.0 发布记录审阅。版本化规范定义准入范围与权限;矩阵和路线图中保留的 v0.4 发布标题属于历史记录,不代表最新版本。
不是。它是编译器派生的类型化程序表示,不是通用文档索引或向量数据库。规范源码和编译器 prelude 绑定修订;已验证 HIR 提供语义身份与事实。
不能任意修改。v0.5.0 包含多类有界修改,包括指定表达式替换、结构修改和组合。每类都有自身修订及准入检查;证据和只读检查不授予任意文件系统、Git 或发布权限。