Σ-GLYPH

Deterministic compute by content. The same term with the same budget and the same content yields the same receipt — on any machine, across conforming implementations. A long computation can be cut into budgeted segments, resumed from checkpoints by anyone, and verified by replay.

A content-addressed SKI evaluation core with a bit-exact determinism guarantee, and a resumable kernel on top of it. Integer-only, total, budgeted. Book I 1.0.0 · sigma-resume 1.0.0 (release v1.0.0).

Receipt = eval(term_hash, atp, content_environment) // deterministic · integer-only · total

This repository keeps two documents: Book I (the compute core) and sigma-resume (segments, checkpoints, receipts). Everything else it once carried was retired on 2026-10-31 (the retirement record).

Don't trust this page — re-run it

Every behavioural rule of Book I is a machine-readable conformance vector, generated by the reference oracle (never hand-written). Clone and run — no third-party packages, just Python 3:

# Book I — the compute core
$ python3 impl/sigma_glyph.py
ALL PASS
$ python3 tests/spec_conformance/run_reference.py
CONFORMANCE: ALL PASS (148/148)

# sigma-resume — segments, checkpoints, replay
$ python3 tests/resume_test.py
SIGMA-RESUME: 46 PASS, 0 FAIL, 3 UNRUN (an UNRUN is not a pass)

The three UNRUN cases name what the reference deliberately leaves to a host or another layer: atomic on-disk publication, a memo cache, and signed attestation (Warrant's layer). An UNRUN is reported with its reason and never counted as a pass.

Compute one thing

eval is total: every term with every budget resolves to exactly one canonical outcome — a normal form, ATP Exhausted, or Unresolved Reference. A non-terminating term is not an error — it is a priced, canonical outcome. (A concrete implementation may additionally hit a local limit and raise a non-canonical resource fault; those are never part of the canonical result.) Work and peak materialised size are bounded by the budget (size − 1 ≤ spent, a proved invariant — see below).

# I K  ->  K, then Omega = (S I I)(S I I) with a budget of 1000
result: bc0c2fe26e44e2ae spent: 4
Omega: ATP Exhausted spent: 975

Resume one thing

The same computation, run as six segments of 5 ATP each, reaches the result one segment of 1000 ATP reaches, and the chain of checkpoints verifies by replay:

# S K K (S K K (K I))  ->  K I
6 segments: NORMAL_FORM 65cd957fee7ec9fb
one run:    NORMAL_FORM 65cd957fee7ec9fb
verify: ['NORMAL_FORM', 'PAUSED']

Both runnable snippets are in QUICKSTART.md; the release gate executes the first against the installed package and the checkout and requires identical bytes.

Deeper checks (cross-implementation & proofs)

# a second, dependency-free Book I evaluator (its own SHA-256, no crates)
$ (cd impl-rs && cargo build --release) && \
    ./impl-rs/target/release/book1 conformance tests/spec_conformance/vectors.json
RUST-CONFORMANCE: ALL PASS (49/49)

# the Lean evaluator against the oracle (needs a Lean toolchain; CI runs it)
$ python3 proofs/eval_bridge_check.py
EVAL-BRIDGE: ALL AGREE (33/33)

Every MUST is a claim

The normative sentences of Book I and sigma-resume are 88 claim records in .warrant/, and the check runs both ways: every MUST, SHALL and REQUIRED in either document must lie in some claim's sentence, and every claim's sentence must still be in its document. Each claim quotes its sentence verbatim and either names the test cases that witness it and the mutants — deliberate breakages of the implementation, the suite or its schema — that those cases must catch, or says why it is unbacked (12) or only informative (5, such as the RFC 2119 boilerplate). 71 are backed. A claims checker accepts a backed claim only after replaying its witnesses and its 70-mutant harness at one commit, and CI re-executes every new acceptance.

$ warrant claims check
claims: 88 live of spec/book-1-truth.md, spec/sigma-resume.md; 0 problem(s)

warrant is warrant-graph, pinned in .github/warrant-requirements.txt. Reviews are records in the same store: a pull request's head is accepted by the reviewer the repository's profile names, or challenged with findings it signs.

What it is / what it is not

It is

A total, deterministic evaluator whose result's identity is the SHA-256 of its canonical bytes.
A cross-implementation contract: agreement is defined by shared vectors, not by one binary.
A priced machine — compute and memory both paid from one budget.
A resumable one: a checkpoint is a value anyone can continue from their own root.

It is not

A blockchain, a token, or a consensus network.
A general VM or a language runtime — the core is SKI, deliberately tiny.
Fast. It trades speed for an exact, portable identity of computation.

Why not WASM / Nix / IPFS / zkVM / just Python?

The fair skeptic's question. Honest answers, each about what Σ-GLYPH builds in:

vs WASM	WASM executes portably, but its core format gives a computation no content-derived identity — two toolchains, two byte streams, no shared name for "the same result." Σ-GLYPH's identity is the hash of canonical bytes.
vs Nix	Nix reproduces builds by hashing inputs. It pins an environment, not the semantics of a total, priced evaluation. Different layer — Σ-GLYPH is what runs, not how it was assembled.
vs IPFS	The IPFS protocol content-addresses data and does not compute. Σ-GLYPH content-addresses computation — terms and their results — with a totalization guarantee the storage layer makes no claim about.
vs zkVM	A zkVM proves a computation satisfied its relation without re-running it — powerful, and heavy. Σ-GLYPH targets the case where you can re-run: verification by deterministic re-execution. Complementary, not competing.
vs just Python	The Python impl is only the oracle. The guarantee is the spec + vectors, replayed byte-exact by an independent Book I evaluator (a dependency-free Rust one in this repo). "Just Python" gives one binary's behaviour; this gives a contract between strangers.

Machine-checked, and where the trust actually sits

Determinism and totality of the Lean evaluator are definitional (well-founded step, fuel-indexed total eval; no partial/unsafe). The memory bound size − 1 ≤ spent is a theorem on the concrete evaluator (evalHash_size_bound), compared with the Python oracle on 33 Book I vectors.
sigma-resume is mechanized over the same evaluator: a run split into segments with credit carried over equals one run (adv_split, §2), two budgets that spend the same reach the same state (adv_spent_det, §4), and an accepted cycle witness means no budget ever reaches a normal form (cycle_proven_no_normal_form, §5). The Lean cycle checker agrees with verify_cycle on 12 223 generated cases.
Two Book I evaluators — the Python oracle and this repo's dependency-free Rust (its own SHA-256, no external crates) — agree on every Book I vector and on generated terms. Both come from one author/model lineage; agreement is conformance evidence, not independent custody.
TCB honesty: SHA-256 is a total Lean function, but the genesis pins H(I)/H(K)/H(S) and two more byte-level pins are discharged with native_decide — so those checks trust the Lean compiler, not only the kernel. The evaluator theorems are kernel-checked. The full breakdown is in proofs/README.

Scope & non-goals

Vector agreement is evidence of conformance at the tested points; the Lean theorems cover all inputs only for the properties they state (totality, determinism, the size bound). Σ-GLYPH makes no cryptographic claim beyond SHA-256's, and none about sandboxing, side channels, or adversarial resource isolation of a host. It is a definition of what computes to what, not a secure execution environment. The assumptions are in SECURITY-ASSUMPTIONS.md.