CellScript 0.15.0

Release date: 2026-05-26.

CellScript 0.15 is the scoped-invariant, Covenant ProofPlan, and verifier
soundness hardening release. It closes the known fail-open and
semantic-boundary bugs found during the hardening audit, makes verifier
triggers, scope, coverage, builder assumptions, and enforcement gaps explicit
in source and metadata, and promotes cell identity into a first-class primitive
while resetting the capability vocabulary from protocol verbs to kernel
effects.

The short version: 0.15 adds scoped invariant declarations, aggregate
assertion primitives, Covenant ProofPlan metadata and cellc explain-proof,
first-class cell identity policies, explicit destruction policies, a
kernel/protocol primitive split, expression-local unsigned widening, a
compat/strict migration path, semantic-boundary hardening, and renames internal
type_hash metadata fields.

0.15 is intentionally a hardening release, not the final boundary architecture.
It blocks the known dangerous cases and introduces the scaffolding required for
0.16, where the same boundaries can become fully type-enforced, CFG-aware, and
coverage-linked.

Highlights

Verifier Soundness Hardening

0.15 closes the known high-risk boundary leaks where verifier semantics could
be lowered too early into ordinary low-level values, raw byte spans, raw paths,
or syntax occurrences. The hardening work includes:

• fail-closed paths no longer lowering as ordinary Return(U64(error)) values;
• runtime/helper and syscall status paths checked before exposing DSL values;
• lock predicate success requiring canonical bool == 1;
• Molecule semantic field access gated by containing-layout canonicality;
• branch-local and duplicate lifecycle effects conservatively rejected until
  CFG-aware resource summaries are complete;
• package/dependency paths contained inside their declared capability roots;
• const initializers restricted to compile-time-safe expressions;
• initial SyscallSpec, IR status-boundary, validated schema planning,
  ResourceEffectSummary, and ProofPlan executable-evidence scaffolding.

This is a hardening release. It does not claim full first-class status typing,
full SyscallSpec migration, CFG lifecycle merging, or complete source-to-runtime
ProofPlan evidence linking.

Scoped Invariant Syntax

0.15 adds first-class invariant declarations with explicit trigger, scope,
and reads:

invariant udt_amount_non_increase {
    trigger: type_group
    scope: group
    reads: group_inputs<Token>.amount, group_outputs<Token>.amount

    assert_sum(group_outputs<Token>.amount) <= assert_sum(group_inputs<Token>.amount)
}

Supported triggers: explicit_entry, lock_group, type_group.
Supported scopes: selected_cells, group, transaction.

Invariants are preserved through AST, type checking, IR, module metadata,
formatting, LSP symbols, hover/completions, docs, and scoped CKB entry
compilation.

Aggregate Invariant Primitives

0.15 adds scoped aggregate assertion primitives for common covenant-style
relations:

assert_sum(group_outputs<Token>.amount) <= assert_sum(group_inputs<Token>.amount)
assert_conserved(Token.amount, scope = group)
assert_delta(Token.amount, witness.delta, scope = selected_cells)
assert_distinct(outputs<NFT>.token_id, scope = transaction)
assert_singleton(Config.config_id, scope = group)

Aggregate fields must resolve to fixed-width integer or fixed-byte schema
fields. Dynamic tables, generic collections, and bool fields are rejected.
Non-literal assert_delta arguments must be bound through reads to
witness.* or lock_args.*, so the runtime delta has an auditable source.

Boundary: Aggregate primitives are currently metadata-only for automatic
aggregate verifier-loop lowering. They emit codegen_coverage_status: "gap:metadata-only" and status: "runtime-required" until a later lowering
pass proves them on chain. 0.15 now also cross-references declared aggregate
invariants against checked action obligations; matched obligations are reported
as bounded action coverage, while unmatched declarations remain visible and
gateable.

Covenant ProofPlan Metadata

0.15 adds a ProofPlan stage and cellc explain-proof audit surface.
Runtime, action, function, and lock metadata expose ProofPlan records with:

• invariant name and source span
• trigger, scope, reads, coverage
• input/output relation checks
• group cardinality
• identity/lifecycle policy
• builder assumptions
• diagnostics and codegen coverage status
• matched/unmatched invariant action coverage

cellc explain-proof prints trigger/scope/reads/coverage/on-chain status in
human-readable and JSON output.

ScriptArgs and lock_args provenance is reported under reads.lock_args,
not reads.witness; witness remains reserved for transaction witness data.

cellc check --deny-runtime-obligations rejects runtime-required ProofPlan
gaps, including declared invariants whose coverage is still metadata-only or
whose action coverage is unmatched.

Production and strict gates also reject records that claim checked runtime
coverage without executable evidence. Static or metadata-only details such as
checked-static do not populate executable runtime/codegen evidence.

Lock-group transaction risk diagnostics warn when a lock_group verifier
scans transaction-wide views, because only inputs sharing that lock trigger
the verifier.

Expression-local Unsigned Widening

0.15 defines a deliberately bounded coercion rule for primitive unsigned
integers. CellScript may widen u8 -> u16 -> u32 -> u64 -> u128 only inside
arithmetic and numeric comparison expressions.

This is not a general implicit numeric coercion feature. Assignment, return,
ABI, witness, create layout, struct field initialization, Molecule layout,
and serialization boundaries remain exact-type boundaries. Integer literals may
be context-typed by an expected primitive integer type, but non-literal values
must use an explicit cast at boundaries:

let total: u64 = amount_u64 + fee_u16 // accepted expression-local widening
let stored: u64 = fee_u16             // rejected boundary widening
let stored: u64 = fee_u16 as u64      // accepted explicit boundary cast

Compound assignment is a write boundary: target += rhs is valid only when
rhs is the same width as, or narrower than, target. Generic u128
arithmetic and ordering remain unsupported except for explicitly implemented
u128 delta and equality paths.

Cell Identity and TYPE_ID Lifecycle

0.15 promotes cell identity from a metadata annotation into a first-class
primitive policy:

resource Token has store {
    identity(ckb_type_id)
    amount: u64
}

Supported identity policies:

Policy	Meaning	0.15 executable boundary
identity none	No identity tracking (default, backward compatible)	No identity verifier is emitted
identity ckb_type_id	CKB TYPE_ID: derived from first input + output index	create_unique requires a TYPE_ID output plan and reports global creation uniqueness as runtime-required; replace_unique preserves TypeHash
identity field(path)	Fixed-width field identity within the data payload	create_unique anchors the output field bytes and reports global uniqueness as runtime-required; replace_unique compares input/output field bytes
identity script_args	Identity derived from the executing script args	create_unique anchors the output LockHash and reports global uniqueness as runtime-required; replace_unique preserves LockHash
identity singleton_type	Singleton type identity	create_unique anchors the output TypeHash and reports singleton creation exclusivity as runtime-required; replace_unique preserves TypeHash

Identity-aware lifecycle forms:

// Identity-aware creation
let minted = create_unique<Token>(identity = ckb_type_id) {
    amount: 100
} with_lock(recipient)

// Identity-aware replacement (consumes input, preserves identity)
let updated = replace_unique<Token>(identity = ckb_type_id) old {
    amount: old.amount - 50
}

IrInstruction::CreateUnique and IrInstruction::ReplaceUnique carry
identity metadata through the full compile pipeline. TypeMetadata.identity_policy
exposes the policy in compiled JSON metadata (hidden when none).

replace_unique has the syntax
replace_unique<T>(identity = policy) input_cell { ... }; the input operand is
required because the verifier compares the consumed Cell with the replacement
output. It does not take a with_lock(...) clause.

For create_unique policies, 0.15 emits local runtime anchors for the created
output and records the full global uniqueness proof as runtime-required.
For ckb_type_id, the remaining boundary is the TYPE_ID builder plan. For
field-, script-args-, and singleton-type creation, global uniqueness remains a
builder/indexer responsibility outside the CKB-VM execution scope.

Explicit Destruction Policies

0.15 adds policy-specific destruction forms so the compiler and verifier know
what is being proved:

Form	What it proves
destroy_singleton_type(cell)	No output with the same TypeHash exists
destroy_unique(cell, identity = type_id)	TYPE_ID continuation absence, lowered through the same output TypeHash scan
destroy_instance(cell, identity_field = id)	A field-identified instance destruction intent; full same-field output scan is runtime-required
burn_amount(cell, field = amount)	Quantity-delta burn intent; executable delta proof is runtime-required

Bare destroy cell still compiles as DestructionPolicy::Default. In strict
mode it must be authori...

CellScript 0.14.0

CellScript 0.14 is focused on CKB semantic completeness rather than another syntax cleanup pass. The release exposes more of the concrete CKB transaction surface directly in source, metadata, and validation: bounded Spawn/IPC verifier reuse, structured WitnessArgs access, explicit Source views, ScriptGroup and outputs_data metadata validation, TYPE_ID create-plan metadata, strict script-reference records, CKB-profile since/time/epoch helpers, capacity-floor metadata, and fixed-Hash dynamic Blake2b support. The action model remains the explicit verifier model from 0.13; 0.14 only completes the intentional state-edge spelling cleanup from legacy move to transition.

The validation story is also stricter. The current release has passed the full CKB release gate with builder-backed production actions, local CKB stateful scenarios, valid and invalid lock-spend coverage, measured cycles, transaction size, occupied capacity, syntax-combination fuzzing, VS Code extension dry-run packaging, and the new 0.14 scope audit. The boundary is deliberately conservative: Spawn/IPC is bounded verifier reuse, not full protocol composability; ScriptGroup, outputs_data, and TYPE_ID are metadata/tamper validated in 0.14, while full accepted/rejected CKB transaction fixture matrices remain a later compatibility-suite track.

CellScript 0.13.2

Key Updates

• Stack-backed Vec<T> helpers with fixed-width elements and local runtime support.

• Canonical action/update syntax:

  • action f(input: T) -> output: T
  • where proof block
  • Explicit move for state transitions

• Lock-boundary data sources: protected, witness, lock_args

• Stdlib & metadata patterns enforce explicit verifier obligations.

• Full stateful scenario coverage: 7 end-to-end scenarios + 43 production actions.

Not Included (Future Work)

• Hidden signer authority or default sighash
• Full generic maps
• Cell-backed collection ownership
• Declarative capacity/since policies

Compatibility

• Canonical actions follow signature-direction outputs.
• State transitions use move before.state: A -> after.state: B.
• Persistent outputs named explicitly: create output = T { ... }.
• Tooling: VS Code extension 0.13.2, metadata schema 30.

Collections & Vec<T>

• Stack-backed helpers: Vec<u64>, Vec<Address>, Vec<Hash>.
• Full runtime lowering: push, pop, insert, remove, first, last, reverse, etc.
• Does not support full generic HashMap<K,V> or cell-backed Vec<Cell<T>>.
• Option<T> reserved for future use.

Surface Syntax & Examples

• Module/import style: module cellscript::token
• Persistent declarations use capability lists.
• Action outputs are deterministic and named.
• move + where for state transitions and proofs.
• require condition for verifier guards.
• Flow declarations explicitly describe state graphs.
• Clean examples separated from profiled acceptance tests.

Verification & Release Gate

• ./scripts/cellscript_ckb_release_gate.sh full runs:

  • Rust formatting, checks, tests, clippy
  • VS Code extension dry-run
  • Syntax-combination audits + stateful business-flow coverage

Stateful CKB Evidence

• 7 end-to-end scenarios: token, NFT sale, timelock, launch, AMM, vesting, multisig.
• 46 committed steps + 20 action-branch scenarios.
• Covers all 43 production actions with dry-run, committed tx, cycles, size, capacity checks.

Stdlib & CLI

• Lifecycle helpers: transfer, claim, settle.
• CLI (cellc) commands: build, new, explain, explain-generics.
• Typed Vec<T> helpers report element width, capacity, and helper usage.

Backend & ELF

• Internal ELF assembler restricted to allowed mnemonics.
• Stack-frame load/store, large immediates, and u128 ops materialized explicitly.
• State storage remains explicit cell data; create uses declared state names.
• Preserved-field verification strictly fail-closed.

Important Boundaries

• Address is not a signer proof.
• witness Address is not sighash authorization.
• Full GNU/RISC-V instruction support is not included.
• No implicit signer defaults or Cell-backed ownership in 0.13.

CellScript 0.12.0

CellScript 0.12 moves the project from a prototype DSL toward a production-gated compiler and local tooling release for the current CKB bundled suite.

Highlights:

• CKB bundled suite closed for current scope: all seven examples strict-admitted, deployed, and action-covered in production acceptance.
• Full bundled coverage: 43/43 source actions, 15/15 locks, builder-backed local CKB transactions, measured cycles, tx size, and occupied-capacity evidence.
• Production-facing metadata and constraints now expose runtime errors, ABI shape, CKB hash/DepGroup policy, capacity requirements, and artifact verification.
• Local package workflow covers init/build/check/fmt/doc, path dependencies, lockfile checks, and artifact validation.
• VS Code extension is included with the CellScript LSP, not just syntax highlighting.
• Wiki and docs were refreshed for 0.12.

Boundary: this production claim applies to the bundled 0.12 suite and its recorded evidence. External contracts still require metadata review, builder evidence, CKB acceptance reports, and security review.