CellScript 0.13 Direction Update: Actions, State, and Syntax

English
,
1

Hi, community,

Thank you again for the feedback after last week’s early CellScript preview. The comments were genuinely insightful and inspiring.

This post is a current 0.13 direction update focused on the action model, syntax, and state transitions supported by the implementation today.

The Core Model

CellScript 0.13 makes one idea explicit:

A transaction proposes a Cell transformation.
An action verifies whether that transformation is allowed.

An action is not a method call on a contract object. It is not an account update. It is a typed verifier case.

It names:

  1. the input evidence a transaction wants to spend or read;
  2. the output evidence it wants to create;
  3. the proof obligations that make the transformation valid.

The intended shape is:

action fill_offer(before: Offer) -> after: Offer
where
    require after.price == before.price

Read it as:

Spend one Offer input named before.
Validate one Offer output named after.
The proof lives under where.

Signature Direction

0.13 moves transaction direction into the action signature:

action name(inputs...) -> outputs
where
    proof obligations

For example:

action mint(auth: MintAuthority, to: Address, amount: u64)
    -> (next_auth: MintAuthority, token: Token)
where
    require auth.minted + amount <= auth.max_supply

    require next_auth.token_symbol == auth.token_symbol
    require next_auth.max_supply == auth.max_supply
    require next_auth.minted == auth.minted + amount

    create token = Token {
        amount,
        symbol: auth.token_symbol
    } with_lock(to)

The signature describes topology.
The require lines prove continuity.

That separation is deliberate. Auditors should be able to see exactly which fields are preserved and which fields change.

Named Outputs

0.13 prefers named outputs:

action split(token: Token, to_a: Address, to_b: Address)
    -> (left: Token, right: Token)
where
    require token.amount > 1
    consume token

    create left = Token {
        amount: token.amount / 2,
        symbol: token.symbol
    } with_lock(to_a)

    create right = Token {
        amount: token.amount - token.amount / 2,
        symbol: token.symbol
    } with_lock(to_b)

Named outputs avoid positional guessing. The compiler and the reader both know which proposed output is being constrained.

create name = T { ... }

The canonical output constraint form is:

create token = Token {
    amount,
    symbol
} with_lock(owner)

This does not allocate a Cell at runtime. The transaction has already proposed outputs. The verifier checks that the named output has the expected type, data, and lock.

Field shorthand is allowed:

create token = Token {
    amount,
    symbol
} with_lock(owner)

This means:

create token = Token {
    amount: amount,
    symbol: symbol
} with_lock(owner)

No hidden renaming. No invented fields.

where Proof Blocks

Actions use a structured where block:

action transfer_token(token: Token, to: Address) -> next_token: Token
where
    consume token

    create next_token = Token {
        amount: token.amount,
        symbol: token.symbol
    } with_lock(to)

The header says what transaction shape is being checked.
The where block proves why it is valid.

Inside where, use:

require
let
if / else
match
consume / destroy / claim / settle / transfer
create
helper calls

Ordinary helper functions still use braces:

fn min(a: u64, b: u64) -> u64 {
    if a < b { a } else { b }
}

fn is value-level code. It does not bind transaction inputs or outputs.

State Is Data

0.13 does not hide lifecycle state in compiler magic. If a protocol has state, put it in the Cell data:

enum OfferState {
    Created,
    Live,
    Filled,
    Cancelled,
}

resource Offer has store {
    state: OfferState
    seller: Address
    buyer: Address
    price: u64
}

Enum order does not define a lifecycle. This:

enum OfferState {
    Created,
    Live,
    Filled,
    Cancelled,
}

does not imply:

Created -> Live -> Filled -> Cancelled

The transition graph is declared separately.

Flows Declare Legal Edges

Use flow to declare allowed state transitions:

flow Offer.state {
    Created -> Live;
    Live -> Filled;
    Live -> Cancelled;
}

Or bind edges to actions:

flow OfferFlow for Offer.state {
    Created -> Live;
    Live -> Filled by fill_offer;
    Live -> Cancelled by cancel_offer;
}

Rules:

One state field should have one flow.
Keep legal edges in one place.
An action move must match a declared edge.
A by action_name edge must be proved by that action.

This avoids scattering state transitions across unrelated actions.

move Declares The Edge

Use singular move, with colons:

action fill_offer(input: Offer) -> output: Offer
    move input.state: Live -> output.state: Filled
where
    require output.price == input.price
    require output.seller == input.seller

Read it as:

input.state must be Live.
output.state must be Filled.
The edge Live -> Filled must exist in the flow.

move belongs before where, not inside it:

action settle(input: Position) -> output: Position
    move input.phase: Open -> output.phase: Settled
where
    require output.owner == input.owner

move declares the claimed state edge.
where proves the constraints.

Source Qualifiers

Not every parameter is a consumed input Cell. 0.13 uses prefix source qualifiers:

action grant_vesting(
    read config: VestingConfig,
    tokens: Token,
    beneficiary: Address
) -> grant: VestingGrant
where
    require tokens.symbol == config.token_symbol
    require tokens.amount > 0

    consume tokens

    create grant = VestingGrant {
        beneficiary,
        total_amount: tokens.amount,
        claimed_amount: 0
    } with_lock(beneficiary)

Common qualifiers:

Syntax Meaning
read config: T Read-only CellDep/reference-backed data
protected cell: T Lock-guarded Cell view
witness sig: T Decoded witness data
lock_args args: T Typed lock script args

Prefer:

read config: VestingConfig

not lower-level source encoding in the action signature.

Lifecycle Verbs

Cell-backed inputs must have a clear fate:

Verb Meaning
consume x Spent as protocol material
destroy x Terminates, if the type has destroy
transfer x to owner Same data, different lock or owner
claim x Redeems a receipt
settle x Finalises an obligation/order/receipt

Example:

resource Token has store, destroy {
    amount: u64
    symbol: [u8; 8]
}

action burn(token: Token)
where
    require token.amount > 0
    destroy token

No output does not silently mean destroy. The action should say what happens.

Small Complete Example

enum OfferState {
    Created,
    Live,
    Filled,
    Cancelled,
}

resource Offer has store {
    state: OfferState
    seller: Address
    buyer: Address
    price: u64
    payment_symbol: [u8; 8]
}

resource Token has store, destroy {
    amount: u64
    symbol: [u8; 8]
}

flow Offer.state {
    Created -> Live;
    Live -> Filled;
    Live -> Cancelled;
}

Publish:

action publish(input: Offer) -> output: Offer
    move input.state: Created -> output.state: Live
where
    require output.seller == input.seller
    require output.buyer == input.buyer
    require output.price == input.price
    require output.payment_symbol == input.payment_symbol

Fill:

action fill(input: Offer, payment: Token, buyer: Address)
    -> (output: Offer, seller_payment: Token)
    move input.state: Live -> output.state: Filled
where
    require payment.amount == input.price
    require payment.symbol == input.payment_symbol

    require output.seller == input.seller
    require output.buyer == buyer
    require output.price == input.price
    require output.payment_symbol == input.payment_symbol

    consume payment

    create seller_payment = Token {
        amount: payment.amount,
        symbol: payment.symbol
    } with_lock(input.seller)

Cancel:

action cancel(input: Offer) -> output: Offer
    move input.state: Live -> output.state: Cancelled
where
    require output.seller == input.seller
    require output.buyer == input.buyer
    require output.price == input.price
    require output.payment_symbol == input.payment_symbol

Style Checklist

For 0.13-style actions:

Put Cell-backed inputs on the left side.
Put proposed output Cells on the right side.
Use named outputs.
Use source qualifiers for read/protected/witness/lock_args data.
Put move before where.
Use move field: From -> field: To.
Use where for proof logic.
Use require for constraints.
Use create for output constraints.
Use lifecycle verbs for consumed inputs.
Declare flow separately.
Keep state visible as data.
Do not use replace/replaces.

The Short Version

Signature is transaction topology.
State is explicit data.
Flow declares legal edges.
Move binds an action to one edge.
Where scopes the proof.
Require states verifier constraints.
Create constrains proposed outputs.

Or even shorter:

The action header says what changes.
The where block proves why it is allowed.

Feedback is very welcome, especially on whether this action surface feels clear enough for real CKB protocol examples and audit review.

3 Likes
2

0.13.1 Patch Preview

Local Ergonomics and Syntax Governance

CellScript 0.13.0 establishes the new action model:

A transaction proposes a Cell transformation.
An action verifies whether that transformation is allowed.

0.13.1 does not change this model.

Instead, it proposes two small local syntax improvements:

  1. preserve sugar
  2. anonymous require blocks

Both are meant to reduce repetitive notation without hiding verifier obligations.

Design Principle

0.13.1 follows one rule:

Reduce ceremony, not safety visibility.

A syntax addition should be accepted only if:

its expansion is obvious;
security-relevant fields remain visible;
it does not behave like replace;
audit tooling can expand it back into canonical require statements.

The goal is still the same:

The action header says what changes.
The where block proves why it is allowed.

1. preserve Sugar

A common 0.13 pattern is field preservation:

require output.seller == input.seller
require output.price == input.price
require output.payment_symbol == input.payment_symbol

0.13.1 proposes:

preserve output from input {
    seller
    price
    payment_symbol
}

This desugars exactly to:

require output.seller == input.seller
require output.price == input.price
require output.payment_symbol == input.payment_symbol

The point is readability, not abstraction. The auditor still sees every preserved field at the action site.

Rules

Allowed:

preserve output from input {
    seller
    price
    payment_symbol
}

Not allowed:

preserve output from input

Not allowed:

preserve output from input {
    *
}

Not allowed:

preserve output from input except {
    state
}

CellScript should use whitelist preservation, not blacklist preservation. If a new field is added later, it should not be silently preserved or silently ignored.

For 0.13.1, preserve applies only to resource data fields. It does not preserve Cell metadata such as:

lock
type
capacity

Those should remain explicit or move into standard-library helpers later.

2. Anonymous require Blocks

Long runs of require statements are common:

require payment.amount == input.price
require payment.symbol == input.payment_symbol
require output.buyer == buyer

0.13.1 allows grouping:

require {
    payment.amount == input.price
    payment.symbol == input.payment_symbol
    output.buyer == buyer
}

This desugars into independent atomic requirements:

require payment.amount == input.price
require payment.symbol == input.payment_symbol
require output.buyer == buyer

A require block may contain only pure boolean expressions.

Allowed:

require {
    payment.amount == input.price
    payment.symbol == input.payment_symbol
}

Not allowed:

require {
    let x = payment.amount
    x == input.price
}

Not allowed:

require {
    consume payment
}

Not allowed:

require payment_valid {
    payment.amount == input.price
}

For 0.13.1, require blocks should stay anonymous. Named blocks may look like reusable proof policies, which is exactly the kind of ambiguity CellScript should avoid.

3. Updated 0.13.1 Style Example

action fill(input: Offer, payment: Token, buyer: Address)
    -> (output: Offer, seller_payment: Token)
    move input.state: Live -> output.state: Filled
where
    preserve output from input {
        seller
        price
        payment_symbol
    }

    require {
        payment.amount == input.price
        payment.symbol == input.payment_symbol
        output.buyer == buyer
    }

    consume payment

    create seller_payment = Token {
        amount: payment.amount,
        symbol: payment.symbol
    } with_lock(input.seller)

This keeps the 0.13 action model intact while improving readability.

1 Like
3

0.13.2 Patch: Standard Library Patterns Arrive

CellScript 0.13.2 adds the first stable standard-library audit patterns. This is a small but important step for the language. The goal is not to hide CKB Cell semantics behind magic syntax. The goal is to give common verifier patterns a clear, namespaced spelling while keeping their lowering explicit and auditable.

The new standard-library surface includes lifecycle helpers:

std::lifecycle::transfer(input, output, to) {
    amount
    symbol
}

std::receipt::claim(receipt, output, lock) {
    amount
}

std::lifecycle::settle(input, output, lock) {
    amount
}

It also includes Cell metadata helpers:

std::cell::same_lock(output, input)
std::cell::preserve_lock(output, input)
std::cell::preserve_capacity(output, input)

These helpers are not hidden protocol policy. They lower to explicit verifier obligations such as consuming an input, creating a named output, preserving a whitelisted set of fields, checking lock or capacity continuity, and keeping type continuity visible.

Core syntax stays small:

action
where
move
require
create
consume
read / protected / witness / lock_args

The standard library sits one layer above that: typed, explicit, reusable audit patterns that expand back into the verifier model.

2 Likes