Stable identity first. Source edits second.
The Semaprax semantic program graph records typed declarations, effects, contracts, ownership facts, call relationships, and lowering identities under a content-derived revision.
entity Semaprax
status pre-alpha research
snapshot b9f593c
authority github.com/wavect/semaprax| Repository snapshot | b9f593c · 2026-09-16. The reviewed main commit equals the v0.5.0 tag. Its exact-tag CI completed successfully; the separate branch CI was cancelled. Neither is a blanket production or security guarantee. |
|---|---|
| Full product status | 55 Partial · 0 Implemented · 0 Missing |
| Graph and project contract | Feature-selected graph schemas preserve earlier contracts. Project v1 is the baseline; owned-data profiles v8, v9, v10 and v11 have distinct admission and support boundaries. |
| Published pre-release | v0.5.0 · Published 16 September 2026 at 09:43 UTC. Three archives: Linux x86-64, macOS Apple Silicon and Windows x86-64, with SHA256SUMS. The packaged semaprax binary is the full toolchain, not the standalone Cargo CLI. Exact-tag CI. |
| Package and API previews | A published toolchain does not publish its generated Rust/npm packages or promote private APIs. Project v8-v11 support decisions, public generic ownership, broader platforms and native/Wasm Agent-stage execution remain separate. |
Semaprax resolves canonical .spx source into checked HIR, a compiler representation of typed program meaning. Stable identities connect graph queries, candidate changes, execution and evidence. Supported edits must match their source revision; runtime Agent proposals must pass typed decoding and deterministic authorization. Graphs and receipts never grant publication, network or payment authority by themselves.
Readable .spx remains the canonical Git representation. Explicit @id values identify declarations independently of supported display-name changes. The revision binds canonical source and the compiler-owned implicit prelude, not incidental source spans or a graph wire format.
Context v1/v2 applies depth, node and byte budgets; v2 adds directional traversal. Task-oriented context and text, binary and model-text projections add focused exchange with replay checks. Smaller serialized output is not automatically fewer billed model tokens or better answers.
Inspect context, derive a candidate, preview impact, review, replay checks, then explicitly authorize application. The operation families now extend beyond renames to bounded expression replacement, structural changes and specified rebase/merge composition. Each protocol keeps its own revision, identity and operation limits.
Managed workspace generations, candidate evidence, Project revision storage and MCP workflows retain explicit write and publication authority. Validation of multiple files is not an atomic update to arbitrary raw paths, Git or editors. The Rust embedding API supplies capped inputs, cancellation and opaque sessions, not unrestricted host access.
Admitted profiles include records, variants, classes, inheritance, generics, Option/Result, explicit mutation, loops, collections, iterators, function values and bounded closures. Text, bytes and the bundled library support useful small programs. Owning closure captures, general generic constraints and arbitrary feature combinations remain limited.
Owned and borrowed values, cleanup plans, loan facts and selected resource/generic compositions are implemented. v0.5.0 adds direct owned String variant payloads, while generic String substitutions and nested owned-record variant payloads remain restricted. This is not a complete general lifetime system or a Rust compatibility claim.
Initialize, observe, propose, decode, authorize, execute and reduce. The checked reducer selects Continue, Complete, Suspend or Fail, with authorization repeated each turn. Compiled Proposal schemas constrain streaming and typed decoding before effect dispatch. Source Agent stages currently execute in the retained interpreter, not native/Wasm parity.
Explicit host adapters supply credentials, transport and stores. Limits can cover calls, tokens, bytes, deadlines and quoted costs. Durable profiles acknowledge intent before dispatch and refuse uncertain redispatch. Generic host profiles support bounded retry/failover; the bound source-model route does not automatically retry or switch providers. Usage observations are not guaranteed invoices.
Checked HTTPS POST, Rust-host authentication/sessions and checkpointed jobs are separate integration profiles, not a full web framework. Economic Agents explore payment intents, simulation, approval and reconciliation with host-supplied wallets/signing. A model proposal is neither payment authority nor an exactly-once settlement guarantee.
Project v8 carries Bytes and selected Option/Result forms; v9 adds flat owned records, v10 owned UTF-8 and v11 nested owned records. Generated native/Rust and npm/Wasm consumers, private transports and public generic metadata each have separate contracts. Toolchain release, package publication and public support are different decisions.
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)
}Reviewed against the pinned source commit and the v0.5.0 release record. Versioned specifications define admission and authority; older v0.4 release headings in the matrix and roadmap are historical, not the latest release identity. GitHub repository.
Reviewed against the pinned source commit and the v0.5.0 release record. Versioned specifications define admission and authority; older v0.4 release headings in the matrix and roadmap are historical, not the latest release identity.
No. It is a compiler-derived typed program representation, not a generic document index or embedding database. Canonical source and the compiler prelude bind revisions; validated HIR provides the semantic identities and facts.
Not arbitrarily. v0.5.0 contains several bounded edit families, including specified expression replacement, structural changes and composition. Each has its own revision and admission checks; evidence and read-only inspection do not grant arbitrary filesystem, Git or publication authority.