Skip to main content

3. Resource Logic & The "Token" Type System

1. Introduction: Assets in a Non-Linear Language​

Most modern smart contract languages struggle with the "Asset Paradox": how can you represent a digital asset as a piece of data while ensuring it cannot be copied (double-spent) or accidentally deleted (loss of funds)?

  • Solidity solves this by keeping assets as entries in a global ledger (a mapping(address => uint256)). The "token" never actually moves; only a number changes.
  • Move solves this via Linear Types. A Resource in Move has no "copy" or "drop" ability, meaning the type system itself guarantees the asset is always accounted for.

Sector9 takes a unique third path. It keeps a developer-friendly asynchronous actor model in a Motoko-derived language, but overlays a Deductive Resource Logic using the token and opaque keywords. The current implementation combines module-level ownership, compiler-enforced shared-boundary rewrites, and source-level handle-capability summaries consumed by the Viper/MVIR pipeline.

2. Module-Owned Token Values​

The foundational concept in Sector9 is that the module owns the type.

module {
  public type Token = token { ticker : Text; var amount : Nat };
  // ...
}

When a type is declared as a token, the Sector9 verifier enforces a strict access control policy:

  1. Opaque to Outsiders: Only the code inside the defining module can read or mutate the fields (e.g., t.amount). External canisters or even other modules in the same canister can only pass the token value around or call the module's public API.
  2. Verification-Only Restriction: The opaque keyword is a sibling to token. It provides the same module-level isolation but is restricted to the verification lane; opaque types cannot be shared across canisters, whereas token types can.

By restricting access to a single module, Sector9 creates a Trust Anchor. If the module's internal logic is proved to be conservation-preserving (e.g., from.amount -= n; to.amount += n), then callers can rely on that module's public contracts rather than inspecting token internals directly.

3. The "Verified Call" Flow (sr9 methods)​

To move assets across canisters safely, Sector9 introduces the sr9 marker for shared methods.

Identity and Provenance​

Every token is implicitly tagged with the CHASH (Content Hash) of its defining module. In the verifier model, this identity distinguishes the module that owns the token representation.

id = (module_hash, symbol, minter)

Token-carrying shared methods must use the sr9 verified-call lane. In the current implementation, token transport is tied to compiler-managed shared-boundary rewrites and CHASH-derived owner labels for the token module. Stable token persistence uses the same defining-module CHASH as an upgrade compatibility identity; same-shaped tokens from a different token module identity are rejected unless the program performs an explicit migration. Broader build-provenance identities are a design direction, not a separate shipped provenance key.

4. Shared Boundary Rewrites​

The most technically complex part of the resource logic is how tokens cross the "Wire" (the asynchronous boundary between canisters). This is handled by Shared Boundary Rewrites in the compiler.

NameShared and toShared/fromShared​

Every token module must provide a NameShared submodule. This module acts as the "Custom Serializer" for the asset:

  • A private, non-polymorphic, shareable Shared wire type.
  • A private non-async fromShared(wire_data) helper that rehydrates a token from its wire representation.
  • A private non-async toShared(token_instance) helper that converts a live token into its wire representation.

The wrapper module is intentionally narrow: it is a public module used by the compiler boundary rewrite, but its conversion helpers stay private and verified.

For token-bearing sr9 shared boundaries, the compiler rewrites the shared signature through that wire representation:

  1. Outbound token values: toShared is inserted where a live token value is exported to the wire.
  2. Inbound token values: fromShared is inserted where a wire value is rehydrated into the owner module's token representation.

Stable upgrade persistence is not a shared boundary. It keeps source-level token handles under the same defining-module CHASH and does not call toShared or fromShared. Local opaque handles follow ordinary Motoko raw stable type shape compatibility and explicit owner migrations when the payload shape changes.

The Anti-Double-Spend "Burn"​

To prevent double-spending, Sector9 relies on a "Consume-on-Return" pattern. In the toShared function, the developer is expected to "burn" the local value:

private func toShared(t : Token) : Shared {
  let amt = t.amount;
  t.amount := 0; // BURN: prevent keeping a copy of the value
  { ticker = t.ticker; amount = amt }
}

The compiler does not invent this burn automatically. If the developer omits it, the module must still satisfy its own conversion contracts and any surrounding conservation invariants; a well-specified token module should make the double-representation case fail verification. The proof obligation is resource conservation: the represented asset in local state plus in-flight wire values must stay balanced.

5. Formal Modeling of Tokens in Viper​

The verifier no longer treats opaque/token behavior as a set of recursive checks scattered through type lowering. Source typing records an opaque/token capability descriptor: owner, kind (opaque or token), payload shape, shareability, model surface, and nested carrier/container paths. The Viper side derives policy from opaque_capability_ctx and stores summaries in the translation registries (type_ctx, names*) so MVIR passes can consume the same facts after source types have been lowered to solver-friendly shapes.

Owned vs Foreign Handles​

Inside the defining module, the payload is available and ordinary contracts can talk about fields or owner-provided model functions. Outside the owner module, the handle identity is still a usable value, but the payload is sealed: non-owner code can pass, store, compare, and return the handle, but it cannot inspect, forge, project, pattern-match, or mutate the payload directly. Opaque validity is implicit in the folded owner carrier. The system does not generate a public generic valid(handle) observer; modules expose domain-specific public observers/models when callers need facts about the handle.

Carrier and Container Summaries​

Handles can appear inside ordinary carriers and supported collections: records, options, tuples, variants, arrays, BMap, MBMap, BSeq, and proof collections such as Map, Seq, Set, and Multiset. Those shapes are not accepted by simple name allowlists. They are accepted when the source capability summary says the shape carries handle identity and downstream passes know how to track the relevant alias, effect, await, and payload locations.

For collection models, identity is separate from payload ownership. Equality of a Map<K,H>, Seq<H>, BMap<K,H>, or BSeq<H> model proves that the same handles are present; it does not prove that Owner.model(h) stayed unchanged after an owner-module mutator could have run. Exact BMap.entries / MBMap.entries and BSeq conversion snapshots are enumeration facts over collection structure and handle identity, not authority over the owner payload.

Shared Boundary Soundness​

If a token reaches a shared actor boundary, the sr9 token wrapper rules still apply. Local-only opaque handles cannot be sent through actor/shared/Candid signatures. Shareable token values cross through their NameShared conversion module, with toShared/fromShared applied structurally at the token leaves.

6. Comparison & Evaluation​

vs. Move Linear Types​

  • Move: Linearity is enforced by the type system. You cannot compile code that duplicates a resource. This is "Hard Linearity."
  • Sector9: Token conservation is enforced by the verifier. You can write code that duplicates a token value, but the relevant token-boundary or conservation proof should fail.
  • Trade-off: Sector9 allows for more complex, non-linear intermediate states (e.g., during a complex calculation), as long as the state is "balanced" before the function returns or hits an await. This is more flexible than Move's rigid type system but requires a more powerful (and slower) toolchain.

vs. Solidity Ledger Model​

  • Solidity: The ledger is central. To check a balance, you query the ledger.
  • Sector9: The asset is First-Class. The token value is the balance. You don't query a central ledger; you hold the asset in your own actor state. This enables "True Custody" where users actually own their digital property in their own canisters.

vs. Erlang/Pony Capability Model​

Sector9's tokens are similar to Capabilities in Pony.

  • Pony: Uses capabilities to control access to memory.
  • Sector9: Uses nominal tokens to control access to Economic Value.

7. Conclusion​

Sector9's Resource Logic is a hybrid approach. By combining module-level ownership, CHASH-backed token identity, and verified boundary rewrites, it gives token modules a verifier-enforced consume-on-return discipline in a non-linear language. Correct asset conservation still depends on the token module's contracts and proofs.

Strengths:

  1. Customizable Logic: Unlike hardcoded tokens, Sector9 tokens have fully programmable internal state.
  2. Nestability: Assets can contain other assets, enabling complex derivatives.
  3. Static Checks: Resource-conservation violations at verified boundaries can be caught at check/verification time instead of relying only on runtime detection.

Weaknesses:

  1. Boilerplate: The NameShared submodule and toShared/fromShared logic add significant boilerplate for developers.
  2. Trust in the Module: Security still depends on the correctness of the token's defining module. If the transfer function has a bug, the "linearity" of the token doesn't help. (However, the module itself is usually small and easily verified).