CellScript 0.15 Release Notes
Release date: 2026-05-26.
Release tag: v0.15.0
GitHub release:
https://github.com/a19q3/CellScript/releases/tag/v0.15.0.
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.
Highlights
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 authorized by the 0.15 kernel effects consume + burn instead
of the legacy has destroy capability. Use a policy-specific form when the
audit needs to distinguish singleton absence, TYPE_ID consumption,
field-identified instance consumption, or amount burn.
IrInstruction::Destroy now carries policy: IrDestructionPolicy through
IR and codegen. Codegen only emits the legacy same-TypeHash absence scan for
singleton/type-id destruction policies; instance and amount policies are
reported as runtime-required instead of being over-constrained as singleton
absence.
Kernel/Protocol Primitive Split
0.15 splits resource capabilities into kernel effects and protocol verbs.
New kernel-effect capabilities in has ... clauses:
resource Token has store, create, consume, replace, burn, relock, retarget_type, read_ref
These are context-sensitive identifiers: they are only treated as capability
keywords inside has ... clauses and remain ordinary identifiers elsewhere
(e.g., action burn(token: Token) compiles normally).
Capability::is_protocol_verb() and Capability::kernel_effects() classify
capabilities for migration tooling. transfer and destroy are protocol
verbs in 0.15; their effects decompose as:
transfer -> consume + create + relock (+ replace if lock changes)
destroy -> consume + burn (or consume + assert_absence)
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.
Internal Metadata Renaming
Public metadata fields that previously used type_hash ambiguously are now
explicit about which CKB hash domain they refer to:
| Old name |
New name |
type_hash-absence |
ckb_type_script_hash-absence |
type_hash-preservation |
ckb_type_script_hash-preservation |
lock_hash-preservation |
ckb_lock_script_hash-preservation |
Protocol Macro Provenance
ProofPlan coverage records include macro provenance for selected
compiler-recognized flows such as transfer, create, claim, settle,
consume, destroy, and pool protocol metadata. This is audit metadata;
it is not a replacement for builder-backed CKB transaction evidence.
Runtime-Obligation Policy Gate
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.
New Syntax Reference
Type Declaration Identity
resource Token has store {
identity(ckb_type_id) // CKB TYPE_ID
amount: u64
}
shared OracleData {
identity(script_args) // Script.args identity
value: u64
}
resource NFT has store {
identity(field(token_id)) // Field-based identity
token_id: [u8; 32]
owner: Address
}
Default is identity none (no tracking); backward compatible.
Identity-Aware Lifecycle Forms
// create_unique — identity-aware cell creation
let token = create_unique<Token>(identity = ckb_type_id) {
amount: 100
} with_lock(recipient)
// create_unique with a field identity
let nft = create_unique<NFT>(identity = field(token_id)) {
token_id,
owner
} with_lock(owner)
// replace_unique - identity-aware replacement (consumes input)
let updated = replace_unique<Token>(identity = ckb_type_id) token {
amount: token.amount - 10
}
let moved = replace_unique<NFT>(identity = field(token_id)) nft {
token_id: nft.token_id,
owner: new_owner
}
Destruction Policy Forms
// Prove no same-TypeHash output exists
destroy_singleton_type(token)
// Prove TYPE_ID identity is consumed (not replaced)
destroy_unique(token, identity = type_id)
// Prove a specific instance is consumed (allow other same-type outputs)
destroy_instance(token, identity_field = id)
// Prove quantity delta (burn)
burn_amount(token, field = amount)
Aggregate Invariant Syntax
invariant conservation {
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)
}
invariant no_duplicate_nft {
trigger: type_group
scope: transaction
reads: outputs<NFT>.token_id
assert_distinct(outputs<NFT>.token_id, scope = transaction)
}
Future Direction: 0.16 Enforced Boundary Architecture
In 0.15, invariants are treated as declared ProofPlan obligations rather than
implicitly executed verifier functions. This is intentional: an invariant is
only sound when its trigger, scope, reads, and CKB script boundary are explicit.
The next step is invariant satisfaction checking. A declared invariant should be
considered production-satisfied only if one of the following holds:
- it has been lowered into executable verifier code;
- it is matched by a checked action obligation with compatible trigger, scope,
type, field, and relation coverage;
- it is rejected by strict or production gates as runtime-required.
Aggregate primitives such as assert_sum, assert_conserved, assert_delta,
assert_distinct, and assert_singleton are the first candidates for
executable lowering, because their fixed-width field restrictions already
provide a bounded ABI and scanner shape.
The 0.16 theme is moving from boundary scaffolding to enforced architecture:
all runtime and stdlib helpers should derive from a shared SyscallSpec,
status-like values should be impossible to treat as domain values, semantic
schema access should require validated field objects, lifecycle effects should
merge through CFG-aware summaries, and ProofPlan claims should cite concrete
IR/codegen/runtime evidence IDs.
Verification
Targeted 0.15 gate:
./scripts/cellscript_gate.sh ci
./scripts/cellscript_gate.sh backend
cargo test --locked -p cellscript proof_plan --lib -- --test-threads=1
cargo test --locked -p cellscript aggregate_invariant --lib -- --test-threads=1
cargo test --locked -p cellscript identity --lib -- --test-threads=1
cargo test --locked -p cellscript --test cli cellc_explain_proof -- --test-threads=1
Full release gate:
./scripts/cellscript_gate.sh release
