ZSA Guide Zcash Shielded Assets: asset identity, issuance, transfer, and burn 6 Issuance of Custom Assets 8 The transaction carrier

7 The global issuance state

This section constructs the record that every node keeps of the issued Custom Assets: the global issuance state of ZIP 227 and its chaining through blocks and transactions (§7.1); the transition of that state under one transaction, in which burn precedes issuance, together with the order in which the note commitments of a transaction enter the note commitment tree (§7.2); the properties of finalisation and of the recorded balance (§7.3); and the complete verification of an OrchardZSA transaction, with each check paired with the requirement that it serves (§7.4). The rules are those of ZIP 227, which is Draft; one case that they leave undetermined is an open problem (Remark 7.5).

7.1 The issuance state and its chaining

Definition 7.1 (Global issuance state).

Let

\mathsf{MAX\_ISSUE}:=2^{64}-1=18\,446\,744\,073\,709\,551\,615,

the largest value of one Issue Note (Definition 6.1). The global issuance state is a finite partial map

	$\displaystyle\mathsf{issued\_assets}\colon\mathcal{E}^{*}$	$\displaystyle\rightharpoonup\{0,\dots,\mathsf{MAX\_ISSUE}\}\times\{0,1\}\times% \bigl{(}\mathsf{Note}^{\mathsf{Issue}}\cup\{\bot\}\bigr{)},$
	$\displaystyle\mathsf{AssetBase}$	$\displaystyle\mapsto(\mathsf{balance},\mathsf{final},\mathsf{note}_{\mathsf{% ref}}),$

from Asset Bases to triples, with $\mathcal{E}^{*}$ as in §2.3. The components are written

	$\displaystyle\mathsf{issued\_assets}(\mathsf{AssetBase}).\mathsf{balance},% \qquad\mathsf{issued\_assets}(\mathsf{AssetBase}).\mathsf{final},$
	$\displaystyle\mathsf{issued\_assets}(\mathsf{AssetBase}).\mathsf{note}_{% \mathsf{ref}}.$

An Asset Base outside the domain of the map, written $\mathsf{issued\_assets}(\mathsf{AssetBase})=\bot$ , reads as $(0,0,\bot)$ , and a write to a component of such an Asset Base creates its entry from that default. The components mean the following.

1.

The balance is the amount of the Asset in circulation: the amount issued less the amount burnt.
2.

The finalisation bit $\mathsf{final}$ records whether $\mathsf{finalize}=1$ occurred in an earlier issuance of the Asset; it never changes from $1$ to $0$ .
3.

The reference note $\mathsf{note}_{\mathsf{ref}}$ is the Asset’s reference note (Definition 6.10), or $\bot$ .

ZIP 227 types the third component in $\mathsf{Note}^{\mathsf{Issue}}$ while its default reads $\bot$ ; it is typed here in $\mathsf{Note}^{\mathsf{Issue}}\cup\{\bot\}$ . The bound $\mathsf{MAX\_ISSUE}$ applies to the balance, the amount in circulation, and not to cumulative issuance: after burns an unfinalised Asset can be issued again, so the sum of all values issued of one Asset may exceed $\mathsf{MAX\_ISSUE}$ . The phrases “maximum total supply” and “limit the total issuance” of ZIP 227 are looser than its rule (I6) of Construction 7.3, which the volume follows.

Chaining. Every node MUST update the map while processing any transaction that contains a burn set or an Issuance Bundle. A transaction has an input state $\mathsf{issued\_assets}_{\mathsf{IN}}$ and an output state $\mathsf{issued\_assets}_{\mathsf{OUT}}$ :

1.

the input state of the first transaction of the OrchardZSA activation block is the empty map;
2.

the input state of the first transaction of any later block is the final state of the preceding block;
3.

the input state of every later transaction of a block is the output state of the preceding transaction;
4.

the final state of a block is the output state of its last transaction.

The chaining is that of treestates in the Ironwood Guide’s Definition “Treestate and anchor” (§“Anchors”) (ZIP 227, “Global Issuance State” and “Management of the Global Issuance State”). Class: specified. The OrchardZSA activation block is not assigned, since ZIP 227, “Deployment”, reads “TBD”; this is an open problem, listed in “Open problems” (§10.2).

ZIP 227, “Rationale for Global Issuance State”, gives three reasons, which are rationale of the ZIP. The balance of an issued Custom Asset must never become negative, along the lines of ZIP 209, and no single transaction field carries both the issued and the burnt amounts, so nodes keep a running record of the amount in circulation. The bound $\mathsf{MAX\_ISSUE}$ is a practical limit that lets an issuer issue the complete supply of an Asset in one transaction, indeed in one Issue Note. The finalisation bit lets nodes reject further issuance of a finalised Asset. The properties themselves are proved in “Finalisation” (§7.3).

Remark 7.2 (Issuance state under reorganisation).

By the chaining of Definition 7.1, the final state of a block is a function of the branch from the OrchardZSA activation block to that block. A reorganisation (Ironwood Guide, Definition “Reorganisation”) therefore replaces the state by the one obtained by chaining along the new branch from the last common block, as it replaces the treestates. ZIP 227 states forward chaining only and no rule for reorganisations: the statement here is a consequence of the definition, not a rule of the ZIP. Every result of this section, and Theorem 9.7, holds per branch.

7.2 State transition of a transaction

Construction 7.3 (Transition of the issuance state).

Input. A transaction $T$ that may contain an OrchardZSA bundle (Definition 5.2), with burn set $\mathsf{assetBurn}$ , empty when $T$ has none, and an Issuance Bundle $(\mathsf{issuer},\mathsf{vIssueActions},\mathsf{issueAuthSig})$ (Definition 6.5); and its input state $\mathsf{issued\_assets}_{\mathsf{IN}}$ .

Output. The output state $\mathsf{issued\_assets}_{\mathsf{OUT}}$ , defined only when every requirement below holds; otherwise $T$ is invalid and contributes no state. Every write below is to $\mathsf{issued\_assets}_{\mathsf{OUT}}$ , and every read is of its current value. The labels follow the order of ZIP 227, which numbers none.

For every transaction:

(T1)

The transaction carries at most one Action Group, and that Action Group has no expiry height of its own.
(T2)

$\mathsf{issued\_assets}_{\mathsf{OUT}}:=\mathsf{issued\_assets}_{\mathsf{IN}}$ .
(T3)

The burn set $\mathsf{assetBurn}$ satisfies (B1) to (B3) of Definition 5.1.

(T4)

For every $(\mathsf{AssetBase},v)\in\mathsf{assetBurn}$ , it MUST hold that

\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{balance}% \geq v;

the node then sets, for every pair,

\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{balance}:=% \mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{balance}-v,

before any issuance is processed. By (B3) the pairs have distinct Asset Bases, so checking every pair and then subtracting equals processing the pairs one by one.

If $T$ contains an Issuance Bundle: rules (I1) to (I3) of Definition 6.12 hold, and for each Issuance Action $(\mathsf{assetDescHash},\mathsf{vNotes},\mathsf{flagsIssuance})$ of $\mathsf{vIssueActions}$ , in order, with zero-based position $i_{A}$ in the bundle, let $\mathsf{AssetBase}$ be derived from $\mathsf{issuer}$ and $\mathsf{assetDescHash}$ by Construction 2.10 (Remark 6.14). Then:

(I4)

Every Issue Note description of the action MUST be a valid encoding, and each yields the Issue Note of Definition 6.5 with that $\mathsf{AssetBase}$ . It MUST hold that $\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{final}\neq 1$ , evaluated against the state as updated by the earlier actions of the same bundle.
(I5)

If $\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{note}_{% \mathsf{ref}}=\bot$ , the first Issue Note of the action MUST be a reference note (Definition 6.10): its value MUST be $0$ , and its recipient $(d,\mathsf{pk_{d}})$ MUST be the default diversified address of the all-zero Orchard spending key. The node then sets $\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{note}_{% \mathsf{ref}}$ to that note.
(I6)

For each Issue Note of the action, at zero-based position $i_{N}$ and of value $v$ : its element $\rho$ MUST equal $\mathsf{DeriveIssuedRho}(\mathsf{nf}_{0,0},i_{A},i_{N})$ (Construction 6.7); it MUST hold that

$\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{balance}+v% \leq\mathsf{MAX\_ISSUE},$

and the node then adds $v$ to that balance; and the node MUST compute the note commitment of the Issue Note by Definition 3.2, whose inputs are qualified in Remark 6.2.
(I7)

If $\mathsf{finalize}=1$ in $\mathsf{flagsIssuance}$ , the node sets $\mathsf{issued\_assets}_{\mathsf{OUT}}(\mathsf{AssetBase}).\mathsf{final}:=1$ .

(ZIP 227, “Specification: Consensus Rule Changes”; ZIP 226, “Additional Consensus Rules for the assetBurn set”.) Class: specified. The encodings that (T1) and (I4) name belong to the carrier: ZIP 227 states (T1) “for every transaction” as $\mathtt{nActionGroupsOrchard}\in\{0,1\}$ and $\mathtt{nAGExpiryHeight}=0$ , fields that exist only in withdrawn ZIP 230, and (I4) by reference to the field encodings of ZIP 230; that carrier is open (Remark 8.1). ZIP 227 writes the balance of (I6) as $\mathsf{issued\_assets}_{\mathsf{OUT}}.\mathsf{balance}$ , without the argument $\mathsf{AssetBase}$ , which is restored here.

Four consequences are read off Construction 7.3. Burns are checked against the balance before issuance, so a transaction cannot burn units that it issues. A burn of an Asset Base without an entry fails (T4), since the default balance is $0$ and (B2) gives $v>0$ . A finalised Asset remains burnable, since no rule of the burn half reads $\mathsf{final}$ . Since (I4) precedes (I7) within an action, one action may issue notes and finalise its Asset.

Definition 7.4 (Insertion order of note commitments).

When a transaction $T$ that passes Construction 7.3 is added to the block chain, the leaves that it appends to the note commitment tree of its treestate are, in this order:

1.

for each Action of the Action Group of $T$ , in order, the extracted commitment $\mathsf{cmx}$ of the note that the Action creates, whatever its value and whether or not the Action is a Split Action;
2.

then, for each Issuance Action of the Issuance Bundle of $T$ , in order, and each of its Issue Notes, in order, the extracted commitment of the note commitment computed by (I6).

The transactions of a block are taken in block order. The definition extends the Ironwood Guide’s Construction “State update” (§“Verification of a transaction”), which appends the commitments of Actions only. The position of every leaf, and hence every authentication path, is a function of the chain under this order, so nodes and wallets agree on positions only under it. Which pool’s tree the order extends is the open problem of Remark 1.7 (ZIP 227, “Addition to the Note Commitment Tree”; protocol specification, §“Note Commitment Trees”). Class: specified.

Remark 7.5 (Empty Issuance Actions).

The rules of ZIP 227 place no requirement on the number of Issue Notes of an Issuance Action, and withdrawn ZIP 230, “Issuance Action Description (IssueAction)”, admits an action without notes so that an issuer can finalise an Asset without issuing more of it. Consider such an action on the Asset Base $\mathsf{AssetBase}$ .

(a)

If $\mathsf{note}_{\mathsf{ref}}\neq\bot$ when the action is processed, an action with $\mathsf{finalize}=0$ changes nothing, and one with $\mathsf{finalize}=1$ sets $\mathsf{final}$ by (I7).
(b)

If $\mathsf{note}_{\mathsf{ref}}=\bot$ , rule (I5) refers to a first Issue Note that does not exist, and the rules do not determine whether the action, finalising or not, is valid. If a finalising one were accepted, it would create the entry $(0,1,\bot)$ : an Asset finalised with no reference note and no issuance.

Class: case (b) is an open problem, listed in “Open problems” (§10.2); a rule that fixes the validity of such an action closes it.

An issuance state is reachable if it is the input or the output state of a transaction in a sequence of transactions, chained from the empty map as in Definition 7.1, each of which has an output state under Construction 7.3. A valid chain in the results of this section is such a sequence; an invalid transaction contributes no state. Every chain accepted by Construction 7.10 is a valid chain in this sense, since that procedure includes the transition.

Lemma 7.6 (First-issuance detection).

Assume that no valid chain contains an Issuance Action without Issue Notes on an Asset Base whose $\mathsf{note}_{\mathsf{ref}}$ is $\bot$ when the action is processed, which is case (b) of Remark 7.5. Then in every reachable issuance state $S$ , and for every $\mathsf{AssetBase}$ , the Asset Base is in the domain of $S$ if and only if $S(\mathsf{AssetBase}).\mathsf{note}_{\mathsf{ref}}\neq\bot$ . Hence conditioning (I5) on the absence of an entry is equivalent to conditioning it on $\mathsf{note}_{\mathsf{ref}}=\bot$ . Status (Definition 1.3): proved here for the specified rules; conditional on the hypothesis, which concerns the open case of Remark 7.5.

Proof.

Induction over the transactions of a valid chain, the invariant being checked after every write of Construction 7.3. It holds for the empty map. Rule (T2) copies a state. Rule (T4) writes only Asset Bases with $\mathsf{balance}\geq v>0$ , by (B2), hence Asset Bases already in the domain, and leaves $\mathsf{note}_{\mathsf{ref}}$ unchanged. Rule (I4) only reads. For an action on an Asset Base outside the domain, $\mathsf{note}_{\mathsf{ref}}=\bot$ and the action has at least one Issue Note by the hypothesis, so (I5) sets $\mathsf{note}_{\mathsf{ref}}$ to that note before (I6) and (I7) write: the entry is created together with its reference note. For an action on an Asset Base in the domain, $\mathsf{note}_{\mathsf{ref}}\neq\bot$ by the invariant, and (I5) does not apply. No rule writes $\bot$ to $\mathsf{note}_{\mathsf{ref}}$ or removes an entry. Both the burn step and the hypothesis are needed: without the hypothesis, a finalising action of case (b), if accepted, creates the entry $(0,1,\bot)$ by (I7). □

Lemma 7.7 (Keys of the issuance state).

In every reachable issuance state, every Asset Base in the domain equals $\mathsf{ZSAValueBase}(\mathsf{AssetDigest})$ for the Asset Identifier $(\mathsf{issuer},\mathsf{assetDescHash})$ of some accepted Issuance Action (Construction 2.10), and is therefore the value of $\mathsf{GroupHash}$ at an input under z.cash:OrchardZSA (Table 3). For every transaction of a valid chain, the Asset Base of every pair of its burn set is in the domain of its input state, and is therefore of the same form. Status (Definition 1.3): proved here for the specified rules; unconditional, case (b) of Remark 7.5 included. The lemma discharges, in Theorem 9.5, the premise of Proposition 5.6 on the bases of burn pairs, which (B1) alone does not discharge.

Proof.

Induction over the transactions of a valid chain. The initial map is empty. Rules (I4) to (I7) write only the entry at the Asset Base that Construction 7.3 derives from $\mathsf{issuer}$ and $\mathsf{assetDescHash}$ by Construction 2.10, whether or not the action has Issue Notes, and so does (I7) in case (b) of Remark 7.5 if such an action is accepted. Rule (T4) writes only an Asset Base in the domain: an Asset Base outside it reads $\mathsf{balance}=0$ , and (B2) requires $v>0$ , so the check of (T4) fails. The same argument gives the second claim, since (T4) reads the input state, copied by (T2), before any issuance of the transaction. □

7.3 Finalisation

Every Issuance Action carries the Boolean $\mathsf{finalize}$ in $\mathsf{flagsIssuance}$ (Definition 6.5). An Asset is finalised in a reachable issuance state $S$ when $S(\mathsf{AssetBase}).\mathsf{final}=1$ for its Asset Base. Setting $\mathsf{finalize}$ finalises the Asset by (I7), and every later Issuance Action for its Asset Base, with or without Issue Notes, fails (I4). Only (I7) writes $\mathsf{final}$ , and it writes $1$ , so $\mathsf{final}$ never returns from $1$ to $0$ , as Definition 7.1 states. Finalisation is the only mechanism of the issuance life cycle that ZIP 227 specifies (ZIP 227, “Requirements”, “Issuance Action” and “Specification: Consensus Rule Changes”). Class: specified.

Proposition 7.8 (Finalised supply never grows).

If $S(\mathsf{AssetBase}).\mathsf{final}=1$ in a reachable issuance state $S$ of a valid chain, then in every later reachable state $S^{\prime}$ of the same chain $S^{\prime}(\mathsf{AssetBase}).\mathsf{final}=1$ and $S^{\prime}(\mathsf{AssetBase}).\mathsf{balance}\leq S(\mathsf{AssetBase}).% \mathsf{balance}$ , and the balance is non-increasing from $S$ on. The Asset can still be burnt. This is a property of the map; its relation to the notes in the tree is Theorem 9.7. Status (Definition 1.3): proved here for the specified rules; unconditional.

Proof.

Induction over the later transactions. Only (I7) writes $\mathsf{final}$ , and it writes $1$ . Rule (I4) rejects every later Issuance Action for $\mathsf{AssetBase}$ , with or without Issue Notes, since it reads $\mathsf{final}=1$ , so (I6) never runs for that Asset Base again. The only other rule that writes $\mathsf{balance}$ is (T4), which subtracts. No rule of the burn half reads $\mathsf{final}$ , so a burn of the Asset is accepted whenever (T3) and (T4) hold. □

Proposition 7.9 (The recorded balance).

In every reachable issuance state $S$ of a valid chain and for every Asset Base $B$ ,

S(B).\mathsf{balance}=\sum v_{\mathsf{iss}}-\sum v_{\mathsf{burn}}\in\{0,\dots% ,\mathsf{MAX\_ISSUE}\},

the first sum over the values of the Issue Notes of Asset Base $B$ of the accepted Issuance Actions up to $S$ , the second over the values of the pairs $(B,v_{\mathsf{burn}})$ of the burn sets of the accepted transactions up to $S$ . The balance increases only under (I6) and decreases only under (T4), so burn is the only mechanism that lowers it, and a burn of an Asset Base that has never been issued is rejected. The bound is on circulation, not on cumulative issuance (Definition 7.1). This is a property of the map; its equality with the value of the notes created and not consumed is Theorem 9.7. Status (Definition 1.3): proved here for the specified rules; unconditional.

Proof.

Induction over the transactions, the claim being checked after every write. For the empty map both sides are $0$ . Rule (T2) copies a state. Rule (T4) subtracts $v$ after checking $\mathsf{balance}\geq v$ , which keeps the identity and $\mathsf{balance}\geq 0$ ; an Asset Base without an entry reads $0$ , and (B2) gives $v>0$ , so a burn of a never-issued Asset Base fails. Rule (I6) adds $v$ after checking that the sum is at most $\mathsf{MAX\_ISSUE}$ , which keeps the identity and the upper bound; the reference note of (I5) has value $0$ and enters both sides as $0$ . No other rule writes $\mathsf{balance}$ , and a rejected transaction contributes no state. □

Figure 2 draws the transitions of one entry of the map.

Refer to caption — Figure 2: Transitions of one entry of the global issuance state of Definition 7.1. Solid edges are accepted transitions, labelled with the rules of Construction 7.3 that take them. The first issuance, by (I5) and (I6), creates the entry together with its reference note, as in Lemma 7.6; one action may also issue and finalise at once. The unfinalised entry grows under (I6), up to $\mathsf{MAX\_ISSUE}$ , and shrinks under (T4), down to $0$ ; the finalised entry only shrinks under (T4), again down to $0$ , and every Issuance Action on it is rejected by (I4), as in Proposition 7.8. A burn of an absent entry is rejected by (T4). The dashed edge to $(0,1,\bot)$ is case (b) of Remark 7.5, an open problem.

7.4 Verification of an OrchardZSA transaction

The following procedure has the form of the Ironwood Guide’s Construction “Verification” (§“Verification of a transaction”). Each check is tagged with the requirements of Definition 1.8 that it serves and with the conditions of Definition 4.6 that it completes, and with its class in the sense of Definition 1.2: “specified” for the rule, followed by “carrier designed but unspecified” when its encoding exists only in withdrawn text, or “carrier open” when no design without conflict exists (Remark 8.1).

Construction 7.10 (Verification procedure for OrchardZSA).

Given the note commitment tree and the nullifier set of the pool that carries OrchardZSA notes (Remark 1.7), and the issuance state $\mathsf{issued\_assets}_{\mathsf{IN}}$ , a transaction $T$ is accepted, as far as its OrchardZSA bundle and its Issuance Bundle are concerned, if and only if the following checks pass.

Per Action.

(1)

Proof. The aggregate proof of the Action Group verifies for the relation $\mathcal{R}_{\mathsf{ActionZSA}}$ of Definition 4.6, under the OrchardZSA verifying key of Assumption 4.9, at the primary input

(\mathit{rt},\mathsf{cv}^{\mathsf{net}},\mathsf{nf},\mathsf{rk},\mathsf{cmx},% \mathsf{enableSpends},\mathsf{enableOutputs},\mathsf{enableZSA})

of each Action. [Z1, Z2, Z3 and Z5, through A1^′ to A5^′ and C1 to C3; statement specified, circuit and verifying key designed but unspecified.]

(2)

Spend authorisation. Each Action’s spend-authorisation signature is valid under its $\mathsf{rk}$ on $\mathsf{SigHash}$ (Ironwood Guide, §“Randomised validating keys”; unchanged by ZIP 226). [Requirement R5 of the Ironwood Guide’s Definition “Requirements R1 to R5”, with A6 and A7; specified, signed message designed but unspecified.]

Per Action Group and OrchardZSA bundle.

(3)

Flags. The values $\mathsf{enableSpends}$ , $\mathsf{enableOutputs}$ and $\mathsf{enableZSA}$ are read from the Action Group into every primary input of step (1) (Definition 4.13). [Z2, through C2; flags specified, the bit of $\mathsf{enableZSA}$ open.]
(4)

Anchor. The anchor $\mathit{rt}$ of the Action Group is the root of the carrying pool’s note commitment tree in the final treestate of an earlier block of the chain (Ironwood Guide, §“Anchors”). [Z2, through A3^′; specified, the pool open.]
(5)

Nullifiers. The nullifiers of $T$ , real and split, are pairwise distinct and absent from the carrying pool’s nullifier set (Ironwood Guide, §“Nullifier sets”). [Z3, through A5^′; specified.]
(6)

Burn set. The burn set satisfies (B1) to (B3) of Definition 5.1; this is (T3). [Z1 and Z3; specified, carrier designed but unspecified.]
(7)

Balance. The binding signature is valid on $\mathsf{SigHash}$ under the key $\mathsf{bvk}$ of Definition 5.4, computed from the Actions’ net value commitments, the balancing value and the burn set; the balancing value enters the transparent transaction value pool as in the Ironwood Guide’s Definition “Balancing value”. [Z1 and Z2, through A4^′; specified, carrier designed but unspecified; the fee terms are classified in Remark 8.4.]

Per transaction.

(8)

Issuance authorisation. If $T$ contains an Issuance Bundle, rules (I1) to (I3) of Definition 6.12 hold. [Z4; specified, signed message designed but unspecified.]
(9)

Issuance state. The output state $\mathsf{issued\_assets}_{\mathsf{OUT}}$ of Construction 7.3 is defined: rules (T1), (T2) and (T4), and (I4) to (I7) for every Issuance Action. [(T1): carrier open; (T4): Z2 and Z3; (I4): Z2, Z3 and Z4; (I5) to (I7): Z3; specified.]

State update, on accepting the block that contains $T$ .

(10)

The leaves of Definition 7.4 are appended to the carrying pool’s note commitment tree. [Z2 and Z3; specified, the pool open.]
(11)

Every nullifier of $T$ , real and split, enters the carrying pool’s nullifier set. [Z3; specified.]
(12)

The issuance state becomes $\mathsf{issued\_assets}_{\mathsf{OUT}}$ , chained as in Definition 7.1; the ZEC chain value pool balance of the carrying pool decreases by the balancing value, as in the Ironwood Guide’s Construction “State update”. [Z3; specified.]

The remaining checks of the Ironwood Guide’s Construction “Verification”, on the transaction’s other components and on its expiry, apply unchanged; the parsing of the OrchardZSA components depends on the carrier, which is open (Remark 8.1) (ZIP 226, “Circuit Statement”, “Additional Consensus Rules for the assetBurn set” and “Value Balance Verification”; ZIP 227, “Specification: Consensus Rule Changes” and “Addition to the Note Commitment Tree”; protocol specification, §“Transactions and Treestates”, §“Nullifier Sets” and §“Note Commitment Trees”). Class: every rule specified; the classes of the carrier, the circuit, the signed message and the pool are as tagged.

The division of the checks follows the Ironwood Guide’s Remark “Division of the checks”. Under Assumption 4.9 the proof of step (1) yields, for each Action, a witness of Definition 4.6. Whether $\mathit{rt}$ is a root that the chain recorded, whether a nullifier is new, and whether a burn or an issuance is admitted by the issuance state are facts about the chain’s history, which no proof over one Action’s data attests; the verifier checks them against its state, in steps (4), (5) and (9). Issuance is checked entirely outside the proof, from public data (Remark 6.6). Table 6 maps each requirement to the conditions of the statement, the issuance and state rules, the checks outside the proof and the result that discharges it, the last as in Table 2.

Requirement	Conditions	Issuance and state rules	Checks	Result
Z1, per-Asset conservation	A1^′, A2^′, A4^′, C1	none	(6), (7)	Theorem 9.5, “No counterfeiting across Assets”
Z2, no counterfeiting across Assets	A1^′, A2^′, A3^′, A4^′, C1, C2, C3	(I4), the derived base; (T4) with Lemma 7.7; Definition 7.4	(3), (4), (7), (10)	Theorem 9.5, “No counterfeiting across Assets”
Z3, supply integrity	A4^′, value $0$ of Split Inputs; A5^′, split nullifier	(T4), (I4) to (I7)	(5), (6), (9) to (12)	Theorem 9.7, “Supply integrity”; Proposition 7.8, “Finalised supply never grows”
Z4, issuance authority	none	(I1) to (I3); (I4), the base derived from $\mathsf{issuer}$	(8); (5), through $\mathsf{nf}_{0,0}$	Theorem 9.8, “Issuance authority”
Z5, hiding of the Asset type	the statement as a whole under Assumption 4.10; A4^′, A5^′	none, issuance being public (Remark 6.6)	none beyond the published burn set	Theorem 9.11, “Privacy of the Asset type”

Table 6: Checks against the requirements they serve. For each requirement of Definition 1.8: the conditions of the OrchardZSA Action statement (Definition 4.6), the rules of Construction 7.3 and Definition 6.12, the numbered checks of Construction 7.10 outside the proof, and the result of “Security” that discharges it.