lib

Constants

edgeDeleteAbsent: Int = 4

edgeDeleteActive: Int = 5

edgeInsertAbsent: Int = 0

The seven-admitted-edges row index of each admitted edge. The six tree edges are 0..5 in the order approval-asset-binding fixes (0 insertAbsent … 5 deleteActive), so the edge byte of an approval name is this index; the read is 6 and never appears in an approval, because a read needs none (tree-edge-admission-by-approval).

edgeInsertActive: Int = 1

edgeUpdateActive: Int = 2

edgeUpdateTerminal: Int = 3

edgeWitnessTerminal: Int = 6

kindAbsent: Int = 0

The three token kinds, in the order the state pins their policies.

kindActive: Int = 1

kindTerminal: Int = 2

leafAbsent: ByteArray = #"00"

The Absent leaf byte (#157 three-state-leaf-codec).

leafActive: ByteArray = #"01"

The Active leaf byte.

leafTerminal: ByteArray = #"02"

The Terminal leaf byte.

Functions

quantity(policyId: PolicyId, value: Value, 3rd_arg: TokenId) -> Option<Int>

Helper functions for token handling in the MPF Cage validator.

This module provides utilities for:

  • Token identification and extraction from values
  • Asset name computation from output references
  • Value construction for single tokens

Role in the Cage System

The cage validator needs to identify, extract, and manipulate single NFTs. This module provides the plumbing:

  • assetName: Derives a unique, deterministic asset name from an OutputReference using SHA2-256. This is the foundation of the cage minting policy’s uniqueness guarantee.

  • tokenFromValue: Extracts the single non-ADA token from a value. Used to identify which caged token a UTxO belongs to.

  • quantity: Checks how many of a specific token exist in a value. Used during minting validation to ensure exactly 1 token is minted.

  • valueFromToken: Constructs a value with exactly 1 of a token. Used in tests and when building expected output values.

Design Decisions

TokenId only contains the assetName, not the PolicyId. This is because the policy ID is always the cage script’s own hash, which is available from context. Separating them avoids redundancy and makes it easier to compare tokens across different operations.

Test Hints

  • assetName is deterministic: same OutputReference always produces same asset name
  • assetName is collision-resistant: different OutputReferences produce different asset names (SHA2-256 property)
  • tokenFromValue returns None for ADA-only values
  • tokenFromValue returns None for multi-policy values
  • tokenFromValue returns None for multi-asset-name values under one policy
  • quantity returns None when the policy or asset name is absent Get the quantity of a specific token in a value.

Looks up the given policy ID in the value’s token map, then looks up the asset name within that policy’s token entries.

Returns Some(quantity) if the token exists (quantity may be positive or negative, e.g., in mint fields), None if the policy or asset name is not present.

Usage in Validators

Used in validateMint to verify that exactly 1 token is minted:

quantity(policyId, mint, tokenId) == Some(1)

Test Hints

  • Token present with quantity 1 -> Some(1)
  • Token present with quantity -1 (burn) -> Some(-1)
  • Token not present (wrong policy) -> None
  • Token not present (wrong asset name) -> None
  • Empty value -> None

exactQuantity(
  policyId: PolicyId,
  value: Value,
  3rd_arg: TokenId,
  expected: Int,
) -> Bool

Check that a value’s token map for policyId contains exactly one asset, namely tokenId, at the expected quantity. Other policies in the value are ignored; this is used by the global state policy to avoid minting unrelated assets under the discovery policy id.

tokenFromPolicy(policyId: PolicyId, value: Value) -> Option<TokenId>

Extract the sole asset name under a specific policy id, ignoring other policies. Returns None if that policy has zero or multiple asset names.

assetName(ref: OutputReference) -> Hash<Sha2_256, OutputReference>

Compute a unique asset name from an output reference.

The asset name is the SHA2-256 hash of the transaction ID concatenated with the output index (as 2 big-endian bytes). This ensures uniqueness since an output reference can only be consumed once.

Algorithm

  1. Take the transaction ID (a 32-byte hash)
  2. Encode the output index as 2 bytes in big-endian format
  3. Concatenate: tx_id ++ output_index_bytes
  4. Apply SHA2-256 to the concatenation

Why 2 Bytes for Output Index

Using from_int_big_endian(ref.output_index, 2) encodes the output index as exactly 2 bytes. This supports output indices from 0 to 65535, which is more than sufficient for Cardano transactions (which have far fewer outputs in practice).

Uniqueness Guarantee

Since an OutputReference (tx_id, output_index) can only appear once in the UTXO set, and validateMint requires this OutputReference to be consumed in the minting transaction, the same asset name can never be minted twice. The SHA2-256 hash makes it computationally infeasible to find a different OutputReference that produces the same asset name.

Test Hints

  • Same OutputReference always produces same hash (deterministic)
  • Different tx_id -> different hash
  • Different output_index -> different hash
  • Output index 0 vs 256 -> different hash (tests big-endian encoding)

valueFromToken(policyId: PolicyId, 2nd_arg: TokenId) -> Value

Construct a Value containing exactly 1 of the specified token.

Creates a Cardano Value with a single native token at quantity 1 under the given policy ID and asset name. Does NOT include any ADA – the caller is responsible for adding minimum ADA if needed.

Usage

  • In validateMint: the expected output value is built with this function to compare against the actual minted value.
  • In tests: used to construct expected UTxO values.

Test Hints

  • The resulting value should have exactly one policy (besides ADA)
  • The token quantity should be exactly 1
  • tokenFromValue(valueFromToken(pid, tid)) should return Some(tid)

tokenFromValue(value: Value) -> Option<TokenId>

Extract a single token ID from a value.

This function expects the value to contain exactly one non-ADA policy with exactly one asset name. Returns None if the value doesn’t match this pattern (e.g., contains multiple tokens or no tokens).

This is useful for extracting the caged token from a UTxO that should contain only ADA and a single NFT.

Algorithm (step by step)

  1. Get all policy IDs from the value via policies(value)
  2. Remove the ADA policy (empty string “”) from the list via delete
  3. If exactly one non-ADA policy remains: a. Get its token map via tokens(value, policyId) b. Get all asset name keys from the token map c. If exactly one asset name exists:
    • Look it up in the token map (this always succeeds)
    • Return Some(TokenId { assetName }) d. Otherwise return None
  4. If zero or more than one non-ADA policy, return None

Important: Ignores Quantity

Note that this function does NOT check the token quantity. It returns the TokenId regardless of whether the quantity is 1, 2, or even -1. The caller must verify quantity separately if needed.

Security Consideration

This function is used in extractToken (cage.ak) which is called for both Modify and End operations. If a UTxO somehow contained two different NFTs, this function would return None and the validator would fail – this is the correct behavior.

Test Hints

  • Value with ADA + 1 NFT -> Some(TokenId)
  • Value with only ADA -> None
  • Value with ADA + 2 different policies -> None
  • Value with ADA + 1 policy + 2 asset names -> None
  • Value with 1 NFT (no ADA entry) -> Some(TokenId)
  • Value with ADA + 1 NFT quantity 5 -> Some(TokenId) (quantity ignored)

extractTokenFromInputs(
  what: OutputReference,
  inputs: List<Input>,
) -> Option<(Input, TokenId)>

Find an input by output reference and extract its token.

Searches the input list for the specified output reference and extracts the single token from that input’s value. Returns None if the input is not found or doesn’t contain exactly one token (aside from ADA).

This is a convenience function that combines input lookup with token extraction. It’s used in the Contribute validation path where we need to find the State UTxO and extract its caged token to compare against the request’s requestToken.

Differences from extractToken in cage.ak

This function returns Option (graceful failure), while extractToken in cage.ak uses expect (hard failure). This version is defined in the library for reuse, while the cage.ak version is specialized for the spending validator context where failure should abort the transaction.

Test Hints

  • Input exists and contains exactly one NFT -> Some((input, tokenId))
  • Input exists but has no NFT (ADA only) -> None
  • Input exists but has multiple NFTs -> None
  • Output reference not found in inputs -> None

183 slice b: requests carry an edge index, not value bytes. The leaf

deltaOf(edge: Int) -> List<(Int, Int)>

The token column of seven-admitted-edges, read off the edge and nothing else (#157 mint-matches-edge-deltas): (kind, quantity) pairs the fold sums per key and the mint must then equal exactly. An unknown edge moves nothing.

approvalName(
  edge: Int,
  key: ByteArray,
  owner: ByteArray,
  destination: (ByteArray, ByteArray),
) -> ByteArray

The approval binding (#157 approval-asset-binding): blake2b_256(edge ‖ key ‖ owner ‖ destination), where edge is one byte (the seven-admitted-edges row index), key the registry key, owner the request owner’s credential bytes and destination the request-destination-binding bytes — its address followed by its datum hash, both exactly as the request carries them.

One approval certifies one (edge, key, owner, destination). The cage recomputes this name from the request and refuses a mismatch, so an approval minted for a different owner, edge, key or destination cannot be spent here; reuse by the same owner for the same tuple is the same authority and is harmless. Shared with naming’s mint arm, which computes the identical bytes from its redeemer — one formula, two partitions, so drift makes honest batches refuse loudly.

decodeAddress(bytes: ByteArray) -> Option<Address>

Decode the binary address bytes a request names into the ledger’s own Address (#157 request-destination-binding). Header kinds 6-7 are enterprise addresses (header plus a 28-byte payment hash), kinds 0-3 are base addresses (header, 28-byte payment hash, 28-byte stake hash); everything else — pointer addresses, reward addresses, a wrong length — is refused. Any network nibble is accepted, exactly as naming’s own codec does.

Both credentials are recovered, so a destination binds the stake part too: a folder cannot deliver Alice’s token to her payment credential under its own staking key.

destinationMatches(destination: (ByteArray, Option<Data>), out: Output) -> Bool

Does this output sit at the destination the request named, carrying the inline datum the request carries (#157 request-destination-binding, #419)? Address equality is over the whole address, payment and stake credential alike; the output carries exactly the request’s datum inline, or no datum at all when the request carries none.

Total: an undecodable destination matches nothing, so a request that names nonsense cannot be folded rather than folding anywhere.

datumMatches(expected: Option<Data>, datum: Datum) -> Bool

The datum half of destinationMatches: exactly the carried datum inline, or no datum for none. A datum presented by hash is never it.

destinationDatumHash(datum: Option<Data>) -> ByteArray

The hash an approval binds for the datum a request carries: the BLAKE2b-256 of its serialisation, empty for none — the bytes the request named before it carried the datum, so an approval’s name is unchanged for the same tuple (#419).

approvalDestination(
  destination: (ByteArray, Option<Data>),
) -> (ByteArray, ByteArray)

A request’s destination as approvalName binds it: its address and the hash of the datum it carries.

paysAddress(address: ByteArray, out: Output) -> Bool

Does an output pay this destination address at all, whatever it carries? The refund leg of custody (#157 token-destinations-and-refunds, custody-lovelace-refund) binds the address and the lovelace, never the datum.

183 slice b: `insertRefusal` retires with the `Operation` wire. An

occupiedRefusal() -> Option<String>

The reason an insert on a key the trie already binds is refused (#173 A-006, A-009; interface §2; Lean refusal, which answers key-exists for every occupied key). The primitive refuses BEFORE any mint arithmetic runs, so this is not the keyed-mint witness and must not be confused with it.

Called where mpf.miss(trie, key, proof) answers false on an insert. KNOWN LIMIT, accepted in A-009: mpf.miss answers false both for an occupied key and for a malformed exclusion proof, and the cage cannot tell them apart. Both are REFUSED, so nothing the model refuses is admitted; the trace name is imprecise for the malformed-proof case.

mintRefusal() -> Option<String>

The reason a fold whose claimed mint disagrees with the summed delta of its edges is refused (#173 A-006, Lean L2 fold_batch_claimed_mint_by_kind_key).

One construction site, so a test asserting the reason asserts the value the fold actually traces. The name is the model’s (net-mint-mismatch); it replaces the pre-#173 delta-mismatch at this one site, for every edge, because there is one mint guard.

kindTotal(value: Value, policy: PolicyId) -> Int

The total quantity a value moves under one policy, summed across every asset name — the COARSER accounting the keyed guard refines.

It exists to make the keyed guard’s row non-vacuous: without it, a test asserting that a wrong keyed distribution is refused cannot show that the distribution it used agrees per kind, and a batch that also disagreed per kind would be refused by the coarser rule for a reason that says nothing about keys.

Search Document