Digital Asset System Overview

Module-owned token values and verified calls let you build assets whose shared-boundary behavior is controlled by the defining module.

The point is not only "tokens as data." Sector9 gives asset modules a language boundary: outside code can hold and transfer a value, but only the owner module can inspect or mutate its payload. When that value crosses canisters through an sr9 shared boundary, proof-enabled builds also carry caller proof material, so verified actors can compose with other verified actors instead of treating every remote asset operation as opaque trust.

Concepts

Sector9 combines two ideas:

1. Module-owned token values

   • Assets are token types defined inside a module.
   • Only the defining module can read or mutate the payload.
   • External code can only pass values around or call the module API.
   • Each module may define at most one non-polymorphic token type, with a matching <TokenName>Shared module for shared-boundary conversion.

2. Verified cross-canister calls

   • Any shared method that accepts or returns shareable token values must be marked sr9.
   • In proof-enabled IC/Ref builds, sr9 methods verify caller proofs and reject non-canister or invalid callers before token conversion.
   • In non-proof modes, token boundary rewrites still apply, but proof verification is not injected.

Together, these rules prevent ordinary counterfeiting and double-spend paths under the verified boundary discipline, while keeping token logic customizable. For local accounting patterns such as mint, burn, and transfer, pair this page with Token Systems.

Token vs Opaque

• token is for shareable assets that cross canister boundaries through verified calls. The compiler inserts wire wrappers and module-hash tags at shared boundaries.
• opaque is verification-only. It enforces module ownership in verification, but it does not introduce wire wrappers and is not allowed in shared signatures.

Inside verified module code, both forms are handled as sealed identities outside the owner module. Non-owner modules may store, return, and forward handles, including through records, options, tuples, variants, arrays, BMap, MBMap, BSeq, and proof collections. They may use a handle only by calling an owner API whose handle-capability summary is known; they still cannot inspect, forge, pattern-match, or mutate the owner payload directly.

Actor state may hold live token/opaque handles when those capability rules are satisfied. Upgrade-persistent state should use the same source-level handle types, including inside supported containers. Stable upgrade is not shared-wrapper serialization and must not call toShared/fromShared. For token, stable compatibility includes the defining token module's CHASH; same-shaped tokens from a different token module identity are rejected unless the program performs an explicit migration. For local opaque, stable compatibility follows the ordinary Motoko raw stable type shape; if the owner changes the raw payload shape, migrate explicitly through an owner API such as Mod.upgrade(old).

Opaque payloads may declare anonymous domain invariants inside opaque { ... }. The verifier folds those facts into the owner module's carrier predicate: constructors must establish them, mutators must preserve them, and non-owner modules may rely only on public model/observer facts the owner exposes. Parent opaque invariants can mention child public models such as Wallet.model(wallet), not child private fields.

There is no generated public valid(handle) observer. Generic validity is implicit in possession of the folded handle carrier and is preserved by public owner APIs through their contracts and lowering. Parent modules should mention only domain-specific public facts when they need them, such as Pool.solvent(pool) or Pool.totalLiquidity(pool).

Owner mutators are transaction-shaped. Inside the owner module, a mutator may temporarily break an opaque invariant while updating multiple payload fields, but the verifier marks the owner dirty and closes the carrier before return, await, call boundaries that receive or write the dirty owner, and explicit owner close points. A failed close means the method crossed a stable boundary before repairing the invariant; see test/viper/op4/opaque_owner_two_field_transaction_sat.mo and test/viper/op4/opaque_owner_dirty_call_boundary_unsat.mo.

This matters for multi-actor protocols. If one actor upgrades to a changed token module while the others still run the old module, its stable tokens must not silently become the new identity. The rest of the actors should reject that new identity until they also upgrade or explicitly opt in.

Collection models over handles expose identity only. A Map<K,H>, Seq<H>, BMap<K,H>, or BSeq<H> fact can say which handles are present, but it does not prove that the owner's model(h) stayed unchanged after a possible owner mutation. Exact BMap.entries / MBMap.entries and BSeq conversion snapshots are supported enumeration routes, but they preserve handle identity only. When an invariant needs aggregate payload facts, keep an immutable summary such as Map<K,Nat> or Map<K,Model> and update it through the owner module's public API. Do not treat a collection of handles as a collection of payload snapshots unless a future capability-aware summary API explicitly provides that authority.

Verified Behavior Matrix

The opaque/token handle rules above are pinned by focused regression fixtures:

Behavior	Regression fixtures
Three-plus local modules can pass opaque handles through owner APIs while storing them in records, variants, arrays, BMap, MBMap, and BSeq.XSeq.	test/viper/opaque_apps/dex_sat.mo, test/viper/opaque_apps/fulfillment_sat.mo, test/viper/opaque_apps/marketplace_sat.mo
Map values may be opaque handles, including through imported/aliased core BMap provenance.	test/viper/mutmap/step11_bmap_foreign_handle_value_sat.mo, test/viper/mutmap/step12_bmap_value_helpers_foreign_handle_sat.mo, test/viper/mutmap/step63_core_bmap_alias_descriptor_sat.mo
Exact collection snapshots prove enumeration structure and handle identity, not owner payload stability.	test/viper/op7/bmap_entries_exact_snapshot_sat.mo, test/viper/op7/bmap_entries_handle_identity_not_payload_unsat.mo, test/viper/op7/bseq_toarray_handle_identity_not_payload_unsat.mo, test/viper/op7/mbmap_entries_snapshot_epoch_unsat.mo
Records, options, tuples, variants, arrays, and mixed token/opaque structures can carry handles without exposing owner payloads.	test/viper/mutmap/step49_composed_bmap_option_payload_handle_sat.mo, test/viper/mutmap/step60_composed_payload_bmap_value_handle_sat.mo, test/viper/modown/token_opaque_mixed_maps_sat.mo
BSeq.XSeq<T> is the supported app-facing sequence carrier for handle values; direct iterator-state actor storage remains outside the supported actor-state surface.	test/viper/mutmap/step79_bseq_first_alias_descriptor_sat.mo, test/viper/mutmap/step80_iter_next_value_handle_descriptor_sat.mo, test/viper/mutmap/step82_bseq_iter_next_value_handle_descriptor_sat.mo, test/viper/mutmap/step65_bseq_iterstate_actor_boundary_reject.mo
Descriptor-backed collection APIs fail closed when a handle-carrying operation is not supported for that container. For example, direct BMap.toArray over handle values remains rejected; use BMap.entries / MBMap.entries or BSeq snapshots when a supported exact identity snapshot is needed.	test/viper/mutmap/step94_bmap_toarray_handle_descriptor_reject.mo
Actor-state reachable handles recovered from supported containers cannot stay live across await.	test/viper/mutmap/step48_actor_bseq_value_handle_await_reject.mo, test/viper/mutmap/step64_actor_bseq_toarray_handle_await_reject.mo, test/viper/mutmap/step93_bmap_swap_actor_value_await_reject.mo
Opaque invariants are folded owner carriers and compose through public model/observer facts, including actor and remote-boundary cases.	test/viper/mutmap/step87_opaque_invariant_fact_sat.mo, test/viper/mutmap/step89_opaque_parent_child_invariant_sat.mo, test/viper/mutmap/step90_imported_opaque_invariant_surface_sat.mo, test/viper/mutmap/step91_actor_opaque_invariant_summary_sat.mo, test/viper/mutmap/step92_remote_opaque_invariant_not_exported_unsat.mo
Opaque owner mutators may batch field updates and are rechecked at return, await, and escaping call boundaries.	test/viper/op4/opaque_owner_two_field_transaction_sat.mo, test/viper/op4/opaque_owner_dirty_exit_unsat.mo, test/viper/op4/opaque_owner_dirty_await_boundary_unsat.mo, test/viper/op4/opaque_owner_dirty_call_boundary_unsat.mo
Stable token persistence is CHASH-gated by the token owner, while local opaque stable persistence follows raw Motoko stable shape compatibility.	test/viper/modown/token_stable_storage_sat.mo, test/viper/modown/token_stable_container_storage_sat.mo, test/viper/mutmap/step77_opaque_stable_storage_sat.mo, test/viper/mutmap/step78_imported_opaque_stable_storage_sat.mo

Proof-Enabled Call Flow (High Level)

1. The verifier or deployer gate produces proof material for the canister build.
2. Proof-enabled IC/Ref builds install proof material as hidden init args or through the generated controller-only setters.
3. Verified canisters store the proof and attach it to outbound sr9 calls.
4. sr9 methods reject non-canister callers and invalid proofs before decoding token arguments.
5. Proof payloads bind the caller principal and module hash. Receivers can authenticate the caller principal and read the caller module hash exposed by the runtime hooks. There is not a separate shipped provenance key beyond the current proof and CHASH wiring.

This is the interoperability mechanism that ordinary Motoko does not provide. A typed actor reference tells you the remote call has the right shape; an sr9 proof-enabled boundary adds a check that the caller participates in the Sector9 proof flow. The receiving canister can then connect caller principal, module identity, and token-wire identity to its own contracts. It still has to state those contracts explicitly; proof material does not replace protocol specification.

Module Hash and Token Identity

Each module has a typed-AST hash exposed by Runtime.moduleHash(). It is stable for the compiled module body and changes when the module's typed definition changes. A token module typically includes it in asset identity to prevent cross-module spoofing. The core fungible token library also records the minting module hash, so mint authority and token-definition identity are separate proof facts.

Example identity for a fungible asset:

import Runtime "mo:core/Runtime";

public type Id = (Blob, Text, Principal);

public pure func id(symbol : Text, minter : Principal) : Id {
  (Runtime.moduleHash(), symbol, minter)
};

For the production-shaped version, see core token/Fungible. It exposes helpers such as idOf, balance, transfer, burnAll, and a verified TokenShared conversion module.

Summary

• token types are module-owned values that only the defining module can inspect or mutate.
• opaque types give the same owner-only inspection rule for verification-only handles that do not cross shared boundaries.
• Non-owner modules may route handles through capability-summarized module APIs and supported carriers/collections without gaining payload access.
• Opaque domain invariants live in folded owner carriers and compose through public model/observer facts.
• sr9 shared methods enforce verified cross-canister calls for token-bearing signatures in proof-enabled builds.
• Runtime.moduleHash() lets you bind asset identity to the module that defines it.
• Shared-boundary conversion is defined by the token module's <TokenName>Shared module, not by callers.
• Use shared-boundary rules before exposing token values over canister calls.