Preface
CellScript 0.15 is set for release next week. It makes no attempt to make covenant design sound simple.It does the opposite.
The central feature is ProofPlan. A ProofPlan is compiler-produced audit
metadata for contract obligations. It tells you where a claim came from, when it
is meant to apply, which part of the transaction it reads, whether generated
verifier code covers it today, and which assumptions remain outside that
coverage.
That last distinction matters. ProofPlan is not a formal proof, and 0.15 does
not pretend otherwise. Its value is that it turns hidden assumptions into
visible review material.
In other words, verifier code is what can run on chain. ProofPlan is the
inspection surface that explains what the compiler believes the contract is
trying to protect.
Why 0.15 Exists
Before 0.15, a contract could contain a perfectly reasonable claim that was
still difficult to inspect from the outside. A reviewer might see a token
transfer or an NFT operation and ask: which script boundary is responsible for
this rule? Does the rule cover the current cell, the current script group, or a
wider transaction view? Is the rule actually enforced by generated verifier
code, or is it a design intention that still needs builder evidence?
Those are not academic questions. On CKB, the shape of the transaction matters.
The lock script, type script, selected inputs, group inputs, group outputs,
witnesses, and script arguments all have different meanings. A covenant-style
contract is only reviewable if those meanings are made explicit.
CellScript 0.15 introduces language and metadata for doing exactly that.
The goal is not to bury the reader in compiler terminology. The goal is to make
each contract promise answerable in ordinary language.
The First Idea: A Scoped Invariant
A scoped invariant is a named rule. It says what should remain true, when the
rule is meant to apply, what cells it is about, and which transaction views it
needs to inspect.
Here is the simplest useful shape:
invariant token_amount_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)
}
Read this as a sentence rather than as syntax. The contract is saying: for the
current type-script group, compare the token amounts in the group inputs and
the group outputs, and expect the sums to match.
The three small words near the top do most of the work.
trigger says which verifier boundary this invariant belongs to. In 0.15, an
invariant can be attached to an explicit entry-style path, a lock group, or a
type group.
scope says how wide the claim is. It may cover only selected cells, the
current script group, or a transaction-wide view.
reads says what data the rule depends on. This is not decoration. It is the
review map. If a rule depends on group inputs, group outputs, witness data, or
lock arguments, the reader should not have to infer that from scattered code.
The syntax is intentionally explicit. In a small example it can feel a little
formal. In a real review, that explicitness pays for itself because the
contract’s assumptions are no longer hidden in prose or in scattered helper
calls.
The Five Aggregate Primitives
Many covenant-style rules are about groups of cells rather than one value. A
token supply rule compares totals. An NFT rule checks uniqueness. A singleton
rule says there should only be one live configuration cell of a certain kind.
CellScript 0.15 gives these patterns names:
| Primitive | Plain reading |
|---|---|
assert_sum(view.field) |
Sum this field over a view, then compare it with another sum or value. |
assert_conserved(Type.field, scope = ...) |
This field should be conserved across the stated scope. |
assert_delta(Type.field, value, scope = ...) |
This field may change by a known or explicitly read delta. |
assert_distinct(view.field, scope = ...) |
Values of this field should be distinct. |
assert_singleton(Type.field, scope = ...) |
This field describes singleton-style membership. |
For example:
invariant nft_no_duplicates {
trigger: type_group
scope: transaction
reads: outputs<NFT>.token_id
assert_distinct(outputs<NFT>.token_id, scope = transaction)
}
The meaning is straightforward: the transaction outputs should not contain
duplicate NFT token IDs.
The important 0.15 boundary is just as straightforward. The compiler records
this claim in ProofPlan, but aggregate invariant lowering is not yet a blanket
promise that every such rule is fully turned into executable on-chain loops.
Where the check is metadata-only, ProofPlan says so.
That honesty is the feature.
Reading ProofPlan Output
The command to inspect the audit surface is cellc explain-proof.
cargo run --locked --bin cellc -- explain-proof \
examples/language/v0_15_scoped_invariant.cell \
--target riscv64-elf \
--target-profile ckb
On the current branch, the scoped-invariant example begins with a summary like
this:
Covenant ProofPlan for module `cellscript::language::v0_15_scoped_invariant`
Summary:
records: 16
on_chain_checked: 6
runtime_required: 10
checked_partial: 0
metadata_only_gaps: 10
fail_closed: 0
diagnostic_errors: 0
diagnostic_warnings: 12
macro_provenance_records: 2
invariant_action_matches: 0
invariant_unmatched_action_coverage: 2
The exact numbers will change as the compiler improves. The categories are what
matter.
on_chain_checked means the obligation is represented by executable checks
today. runtime_required means the obligation still needs some combination of
runtime evidence, builder policy, action coverage, or future verifier lowering.
metadata_only_gaps means the compiler has preserved a claim for review, but
is not claiming that it is fully enforced on chain.
This is a more useful output than a vague pass/fail. It tells you what kind of
confidence you have.
Reading One Record Slowly
A single invariant record may look like this:
constraint: token_amount_conservation
origin: invariant:token_amount_conservation
trigger: type_group
scope: group
reads:
- group_inputs<Token>.amount
- group_outputs<Token>.amount
- Source::GroupOutput
- Source::GroupInput
relation_checks:
- assert_sum:group_outputs<Token>.amount==group_inputs<Token>.amount=metadata-only
on_chain_checked: no
codegen_coverage_status: gap:metadata-only
builder_assumption:
- declared(metadata-only invariant not yet lowered to executable verifier code)
warning: declared invariant is metadata-only until executable lowering covers it
The record is saying something quite concrete. It came from the
token_amount_conservation invariant. It belongs to the type-group path. It is
about the current group. It reads token amounts from group inputs and outputs.
The relation is visible. The generated code does not yet fully enforce this
aggregate invariant. Therefore the remaining obligation must be handled by
builder policy, action evidence, review policy, or future compiler work.
There is no need to dress this up. If the output says gap:metadata-only, then
the invariant is visible but not fully proved by generated verifier code. That
is still useful, because an explicit gap is easier to review than an implicit
assumption.
The safe claim is: this invariant is recorded in ProofPlan, and its current
coverage status is visible.
The unsafe claim is: ProofPlan proves the whole invariant on chain.
0.15 is careful not to make the unsafe claim.
Identity Becomes Part of the Contract Surface
ProofPlan is not the only 0.15 change. The release also makes cell identity
easier to state and review.
In many CKB protocols, a cell is not just some data. It is a continuing object:
an NFT, a pool state, a configuration cell, a TYPE_ID-backed asset, or a piece
of state tied to script arguments. If a transaction replaces that cell, the
reviewer needs to know what must remain the same.
0.15 lets the type say that directly:
resource NFT has store, create, replace {
identity(field(token_id))
token_id: [u8; 32]
owner: Address
}
This says that the NFT’s identity is its token_id field. Once that is stated,
lifecycle operations can preserve it deliberately:
action move_nft(nft_before: NFT, new_owner: Address) -> NFT
where
replace_unique<NFT>(identity = field(token_id)) nft_before {
token_id: nft_before.token_id,
owner: new_owner
}
The reader does not have to guess whether the replacement output is meant to be
the same NFT. The identity policy and the lifecycle form say so.
Supported identity policies include CKB TYPE_ID identity, fixed-field identity,
script-args identity, and singleton-type identity. Creation still has an
important boundary: full global uniqueness may require TYPE_ID builder planning
or builder/indexer evidence. In 0.15, ProofPlan records that boundary instead
of hiding it.
Destruction Is More Explicit
Destruction has a similar problem. Saying destroy cell is sometimes too
vague. Are we proving that a singleton has no continuation? Are we consuming a
TYPE_ID-backed object? Are we burning an amount? Are we removing one
field-identified instance?
0.15 introduces more precise forms:
destroy_singleton_type(config)
destroy_unique(asset, identity = type_id)
destroy_instance(nft, identity_field = token_id)
burn_amount(token, field = amount)
These forms are deliberately not collapsed into one word. They describe
different proof intentions. Some can be lowered into executable verifier checks
today. Some are still runtime-required obligations. The important part is that
the intended proof is now visible to the reviewer.
A Practical Review Method
A good ProofPlan review starts before looking at the output. First, translate
the invariant into ordinary language. For example, the expression
assert_conserved(Token.amount, scope = group) means: within this group, token
amount should be conserved.
Then ask which trigger should be responsible for that rule. If the rule is about
type-script state, a type-group trigger may make sense. If it is about a spend
authorisation boundary, a lock-group trigger may be more appropriate. If it is
attached to a selected action path, an explicit entry trigger may be clearer.
Next, look at scope. A selected-cell rule is narrower than a group rule. A group
rule is narrower than a transaction-wide rule. Wider is not automatically
better. Wider claims often need stronger evidence.
After that, read the reads list as if it were an audit receipt. Does the rule
depend on inputs, outputs, group views, witness data, or lock arguments? If the
claim needs data that is not named, the review is incomplete.
Only then run explain-proof and separate covered checks from open obligations.
This distinction is the point of the tool. A record marked as covered can be
treated differently from a record marked as runtime-required or
gap:metadata-only.
For package-level release gates, the stricter command is:
cellc check \
--all-targets \
--target-profile ckb \
--production \
--primitive-strict 0.15 \
--deny-runtime-obligations
That kind of gate should be used with judgement. During development, open
runtime obligations are useful because they show what remains to be designed.
Before a production claim, they need a clear owner and a clear closing path.