Valid Credential Is Not Authorized Payment: A Digital Money Online Safety Module Based on Execution Finality

8.1. FI-CW-01 -- Explicit Conditional Decisions, Protected States and Recovery Paths

 D-01 controlled effectuation path? --NO--> UNPROTECTED/UNSUPPORTED
      | YES                                 (no prevention claimed)
 D-02 authenticated collection-time authority? --NO--> DENY
      | YES: load FOR; hold Candidate Act in NES
 D-03 native operation fully reconstructable? --NO--> DENY, or
      | YES                       PENDING if external evidence can
      |                           later resolve it
 D-04 consistent with FOR and current authority? --NO--> DENY
      | YES                                  + auditable reason
 D-05 safe protected state transition? --NO/stale/replay--> DENY
      | YES: serialize, D + R <= B, consume use identity
 D-06 leg or chain finality sufficient? --NO/PROVISIONAL--> HOLD
      | YES: release only at the identified controlled sink
 D-07 released and authentic confirmation? --NO, maybe released-->
      | YES: record effect, receipt,        OUTCOME_UNKNOWN; fence
      |      remaining budget               reuse; reconcile id
 D-08 multi-leg, refund or recovery? --YES--> authorize each new
      | NO                                  leg; PARTIAL_EFFECT
      v
 terminate with the established outcome; never reset local
 status to "undo" an external effect

The following textual branch sequence elaborates the common financial workflow without reliance on figures. The steps describe decision predicates and effect states. Conditional checks may be implemented using protected hardware, a transactionally isolated processor, an exclusive account/contract guard, or an equivalent enforcement arrangement supported by the profile. A security guarantee is limited to actual effectuation paths governed by that control.¶

• Branch D-01 -- Controlled effectuation path? YES: identify the exclusive signer, dispatch mechanism, account mutation, card/network adapter or contract guard and proceed. NO: label the path UNPROTECTED/UNSUPPORTED, do not treat observations or approvals alone as an enforced release barrier, and do not claim prevention through that path.¶

• Branch D-02 -- Independently authenticated collection-time authorization available? YES: load the applicable protected Financial Obligation Record (FOR), identity, purpose, units, bounds, policy and remaining budget; hold the requested Candidate Act in Non-Effective State. NO: DENY and produce no effective signature, message, debit, transfer, mint or other effect.¶

• Branch D-03 -- Actual final native financial operation fully and unambiguously reconstructable? YES: extract the native payee, asset, value, fee, route, contract/chain identity, nonce, settlement instruction and other profile-critical fields. NO or conflicting parser interpretation: DENY, or remain PENDING where authenticated external evidence can subsequently resolve an unsettled outcome; never rely only on an agent summary.¶

• Branch D-04 -- Exact operation consistent with FOR and current authority? YES: verify source-to-destination transformations, permitted currency conversions, account/merchant/code lineage, expiration, revocation, sink binding and required independent external evidence. NO: DENY, preserve an auditable rejection reason and issue no effective enablement.¶

• Branch D-05 -- Safe protected state transition possible? YES: serialize or otherwise isolate overlapping reservations, enforce committed plus reserved exposure not exceeding the authorized bound, and consume the exact finite use identity under protected state. NO, stale generation, replay or concurrent oversubscription: DENY without replenishing previously unknown spending capacity.¶

• Branch D-06 -- External leg or chain finality sufficiently established for the particular conditional release? YES: permit only the independently authorized release at the identified controlled sink. NO or PROVISIONAL: retain the corresponding leg in a non-success hold, observing applicable finality and challenge rules; never represent a source receipt as proof of a different destination settlement.¶

• Branch D-07 -- Effective native operation released and authentic confirmation received? YES: record the effect, the independently authenticated receipt or observation, and remaining budget under its precise confidence/finality rule. NO confirmation, but possible release occurred: mark OUTCOME_UNKNOWN or equivalent, fence reuse and reconcile the original native identifier instead of issuing a fresh request.¶

• Branch D-08 -- Multi-leg, refund, reversal or recovery operation needed? YES: separately authorize each new economically effective leg and retain PARTIAL_EFFECT where coordination cannot be atomic across parties. NO: terminate with the accurate established outcome. Under neither branch is an external effect silently reversed by resetting local status.¶

8.2. General protected state and mathematical invariants

Let B(p,a,w) be the maximum authorized debit of payer p in asset a during window w, D(p,a,w) the verified already-effective debits, R(p,a,w) all active reservations, and F(x) the final actual effect vector. When there are multiple rails, the scope may include a separately documented currency conversion rule; unrelated asset amounts shall not be arithmetically combined without a typed price and provenance.¶

Budget safety: D(p,a,w) + R(p,a,w) <= B(p,a,w) for each protected budget dimension and under all concurrent scheduling orders. A disjoint escrow allocation is considered active reservation until released after authenticated reconciliation.¶

Binding safety: RELEASE(x) => Authenticated(FOR(x)) AND FreshPolicy(x) AND LineageValid(x) AND ActualEffectInScope(F(x), FOR(x)) AND ConsumeAtFS(x) AND NoKnownUnmediatedEffectivePath(x).¶

No replay: for any one-use authorization identifier u, the number of successful protected consume transitions for u is at most one; release to an external endpoint may still have an unknown outcome, which must not reset u.¶

Multi-leg evidence: SETTLED(group) => independently adequate completion evidence from every required participating settlement leg. A local positive authorization or an unaudited coordinator success flag is insufficient.¶

Exactness of transformations: for every typed edge e in a proposed financial effect graph, input identity, output identity, exchange ratio, fees, integer precision, receiving beneficiary and settlement scope must satisfy the bounded equivalence predicate committed by PED-1; otherwise a subsequent effect is denied.¶

  B(p,a,w) = 100   D = verified effective debits (0)
                   R = active reservations (0)

  worker A: reserve 60 --+
                         +--> serialized protected transition
  worker B: reserve 50 --+

  A:  D + R + 60 =  0 +  0 + 60 = 60  <= 100  -> RESERVED (R = 60)
  B:  D + R + 50 =  0 + 60 + 50 = 110 >  100  -> DENY
  A:  effect verified                        -> D = 60, R = 0
  outcome unknown                            -> reservation kept;
                                                never replenished
                                                without evidence

8.3. Reference pseudocode for a protected single-sink operation

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function FI_VERIFY_AND_EFFECTUATE(FOR_ID, pending_native, sink_id, s\
\tate):
    req := protected_load(FOR_ID)
    if req is absent or not authenticate(req): return DENY
    if not current_policy_and_revocation(req): return DENY
    actual := trusted_sink_parser(sink_id, pending_native)
    if actual is undecidable or has unknown critical fields: return \
\DENY
    if not binding_and_lineage_match(req, actual): return DENY
    if not authorized_transformations(req, actual): return DENY
    begin protected atomic transaction
        if usage_consumed(req, actual) or budget_exceeded(req, actua\
\l): abort DENY
        reserve_budget_and_mark_consumed(req, actual, sink_id)
        persist_intent_to_effect_journal(req, actual)
    commit
    result := release_once_via_exclusive_sink(sink_id, pending_nativ\
\e)
    if result is authenticated external confirmation:
        persist typed result without upgrading evidence beyond what \
\it proves
    else:
        persist OUTCOME_UNKNOWN; freeze repeated effective release
    return result

Implementation warning: A durable database transaction and an external network send are not, by themselves, one globally atomic transition. The routine requires an exclusive release mechanism, idempotent downstream sink contract, reversible prepare phase, hardware command acceptance handshake, or explicit outcome-unknown recovery. It must not be characterized as exactly-once settlement merely because a local journal updated.¶

9.1. E-45: Autonomous Resource-Payment and Delivery Entitlement Boundary

Technical application. Agent-completed API, travel, data, compute and digital-service purchases where payment no longer waits for a human confirmation.¶

Effect-critical native data. A typed payment challenge, resource identifier, merchant or service public identity, price and denomination, requested usage quantity, facilitator endpoint, fee schedule, purchase expiry, and the deliverable identifier or service entitlement.¶

Consequence boundary. The first protected boundary is the protected release of payment authority to a facilitator, signer or settlement adapter; a distinct protected check governs any resulting data access or service entitlement.¶

 mandate: service class, merchant identity, max price, payer
 account, denomination, quantity, expiry, rails, price drift
        |
        v
 PED-1 authority manifest (protected)
 purchasing agent --quote / payment challenge--> NES (no credentials)
        |
 PED-2: resolve final endpoint, merchant identity and payable
        bytes (not a model summary or forwarded header)
        |
 Finality Sink: quantity, service digest, quote signature,
   domain separation, amount, fee, settlement asset, beneficiary
        |
        +---- payment release ----+
        v                         v
 facilitator / signer /     separate protected check for data
 settlement adapter         access or service entitlement
        |
 confirmation lost -> PAYMENT_OUTCOME_UNKNOWN; query; no re-pay

Constructive technical implementation.¶

1. PED-1 accepts an authority manifest specifying an eligible service class and an independently verifiable merchant identity; it constrains maximum price, payer account, denomination, quantity, expiry, permitted rails and price drift.¶

2. An untrusted purchasing agent obtains a machine-readable quote or payment challenge and places it, without effective payment credentials, into a Non-Effective State.¶

3. PED-2 resolves the final service endpoint, final merchant identity and payable bytes from the execution-facing request, rather than accepting a model-produced summary or a forwarded HTTP header.¶

4. The Finality Sink compares quantity, service digest, quotation signature, domain separation, amount, fee, settlement asset and beneficiary against the protected mandate; it binds a payment attempt to a single resource-delivery correlation identifier.¶

5. It atomically consumes the allowed payment-use record or a disjoint escrow reservation before releasing any usable signature or effective instruction. A payment acknowledgment is recorded as PAYMENT_INITIATED, not SERVICE_DELIVERED.¶

6. A second sink verifies a signed or independently obtained delivery receipt, content digest, entitlement token or measured service allocation before recording SERVICE_VERIFIED; absent evidence the delivery status is UNKNOWN.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-45 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-45 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that the merchant public identity, signed payment challenge, resource identifier, denomination, price and fees, facilitator identity, expiry, and service entitlement all remain within the original purchase mandate. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-45 / NO at any security or business predicate: if the payment facilitator cannot be authenticated, price or payee changes, the quote expires, or the payment handle has been used, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-45 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-45 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, PAYMENT_OUTCOME_UNKNOWN; query the existing native payment identifier and separately reconcile service delivery without initiating payment again. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-45 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A payment quote cannot grant a broader merchant identity, resource entitlement or spend authority than the originating mandate.¶

• A successful payment authorization does not establish delivery or entitle an agent to a different protected resource.¶

• One resource-payment correlation identifier does not authorize a second charge or an independently substituted facilitator.¶

Illustrative adversarial scenarios.¶

• Change an API payment challenge from 0.02 to 2.00 after authority collection.¶

• Replace an allowed merchant wallet with a visually similar address while retaining the resource label.¶

• Replay an already consumed payment handle through a second payment facilitator.¶

Alternative implementations.¶

• Hardware or enclave signer constrained by resource-bound payment metadata.¶

• Payment-switch or merchant-acquirer gateway with exclusive release of settlement credentials.¶

• Programmable account with on-ledger operation-specific validation and a distinct delivery verifier.¶

Failure, reconciliation and limits. If an external payment may have occurred and confirmation is lost, retain PAYMENT_OUTCOME_UNKNOWN, query the transaction identifier and prohibit a fresh payment under the same mandate. Entitlement reconciliation may continue without payment replay.¶

Proposed negative-effect conformance vectors. changed_quoted_amount, merchant_key_substitution, facilitator_replay, expired_service_quote, fee_unit_rounding, paid_but_no_service. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-45).¶

9.2. E-46: Card Authorization-Capture-Clearing Continuity with Concurrent Bounds

Technical application. Virtual card, embedded payments and agent-driven merchant payment lifecycles.¶

Effect-critical native data. Original authorization reference, card token binding, merchant identity and category, authorized total and currency, incremental authorization records, capture messages, refund and reversal identifiers, settlement amounts and original merchant agreement.¶

Consequence boundary. The first protected boundary is authorization release at the issuer or network adapter; each capture and settlement release is independently consequential and must be separately mediated.¶

 PED-1 spending state: merchant, purpose, card-token generation,
 authorized aggregate, capture window, capture count, expiry
        |
 acquirer/issuer native capture --> PED-2: capture, merchant of
                                    record, authorization lineage
        |
 durable compare-and-swap:
   new amount <= authorized - (captured + outstanding reserved)?
        | yes                                     | no
        v                                         v
  RESERVED -> RELEASED -> CAPTURED -> CLEARED    DENY
                 |
                 +-> ACK_UNKNOWN (reconcile; no second capture)
  REVERSED: hold reduced only after a verified reversal state
  refund: a separately authorized outgoing financial effect

Constructive technical implementation.¶

1. PED-1 stores merchant, purpose, card-token generation, authorized aggregate, capture window, capture count and expiry as a protected spending state.¶

2. PED-2 independently reconstructs each incoming capture from the final acquiring or issuer-facing native message; it resolves merchant-of-record and original authorization lineage.¶

3. A capture request reserves an amount through a durable compare-and-swap against the sum of already captured and outstanding capture reservations, checking new amount <= remaining permitted amount.¶

4. Capture status is tracked separately as RESERVED, RELEASED, ACK_UNKNOWN, CAPTURED, CLEARED or REVERSED, with typed evidence requirements for each transition.¶

5. Partial reversals reduce the outstanding hold only after a verified reversal state; refunds create a separately authorized outgoing financial effect and cannot silently increase spend capacity.¶

6. The protected sink releases the actual capture instruction only after committing a one-use capture identifier and verifying that no alternate acquiring or token route can duplicate the same charge.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-46 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-46 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that issuer/network authorization reference, merchant, incremental authorization, each capture and refund identifier, currency, and remaining authorized capture balance match the protected card lifecycle. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-46 / NO at any security or business predicate: if a capture exceeds the remaining authorized balance, races another capture, changes merchant, or lacks a current authorization, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-46 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-46 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, retain the capture reservation, query the network or issuer on the same identifier, and release capacity only on verified non-capture or applicable expiry. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-46 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• Across concurrent workers: sum(captured) + sum(active reservations) <= authorized aggregate plus any independently approved increments.¶

• Original authorization success is not authority for an altered merchant, currency or unlimited follow-on capture.¶

• A reversal, clearing record and merchant acknowledgment are different evidentiary event types.¶

Illustrative adversarial scenarios.¶

• Two captures both see the full remaining amount in a stale cache.¶

• A merchant changes from partial capture to a larger final capture.¶

• A captured transaction is retried with a different request reference after a timeout.¶

Alternative implementations.¶

• Issuer HSM/processing host with protected capture ledger.¶

• Network-level token-control or transaction-management service.¶

• Merchant-acquirer adapter with exclusive capture dispatch plus issuer acknowledgments.¶

Failure, reconciliation and limits. Unknown capture status fences the original reservation and triggers an idempotent status inquiry rather than an automatic retry. Release of a hold is conditional on reliable non-capture evidence or expiry conditions defined by the relevant network.¶

Proposed negative-effect conformance vectors. dual_partial_capture, over_capture, merchant_changed_after_auth, increment_without_authority, capture_ack_lost, refund_as_new_spend. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-46).¶

9.3. E-47: Cross-Rail Financial Obligation Equivalence and FX Boundary

Technical application. Payment routing among bank transfers, card rails, stablecoins, tokenized deposits and alternative payout providers.¶

Effect-critical native data. Payer, intended economic beneficiary, source and destination amounts, both units, authorized exchange-rate range, decimal scale, quote provenance, slippage, route fees, intermediary fees, settlement destination and expiry.¶

Consequence boundary. The first protected boundary is the last controllable payment instruction for each rail, and any conversion or asset-transfer interface that independently reduces customer funds.¶

 PED-1: obligation as typed constraints (payer, beneficiary,
 source/destination amounts and units, FX range, decimal scale,
 slippage, fees, settlement destination, expiry)
        |
 routing service --chosen route graph--> PED-2 (versioned schema,
                                         independent quote source)

 [debit]--e1-->[swap]--e2-->[bridge]--e3-->[payout]--e4-->[settle]
   each edge: input/output asset, denomination, recipient,
   exact maximum debit
        |
 verifier: net effect including all fees within authorized
           tolerance; beneficiary equivalence evidence
        |
 sink-specific handle per controlled rail (obligation id, route);
 obligation-level key blocks a second release on another route

Constructive technical implementation.¶

1. PED-1 commits to an obligation expressed as typed financial constraints rather than an unchecked display string or an unrestricted payment-route identifier.¶

2. A candidate route graph contains typed edges for debit, swap, bridge, payout and settlement; each edge declares its input and output assets, denominations, recipients and exact maximum debits.¶

3. PED-2 reconstructs the graph actually chosen by the routing service and evaluates each edge using a strictly versioned schema, independent market quote source and bounded slippage definition.¶

4. The verifier calculates the net economic effect including all fees; where exact equivalence is impossible, it checks explicit authorized tolerance intervals and beneficiary equivalence evidence.¶

5. Sink-specific handles are issued to participating controlled rails with an obligation identifier, route-generation commitment and bounded amount reservation; partial releases remain separately visible.¶

6. Unexpected route changes, unsupported currency scales, stale quotes or unauthorized recipient substitutions result in DENY before the next controlled financial effect.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-47 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-47 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that the translated payment route preserves actual source debit, final beneficiary, both currencies, amount scale, authorized FX range, fees, slippage, and payout destination. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-47 / NO at any security or business predicate: if an intermediary changes the beneficiary, FX conversion exceeds the bound, a fee is omitted, or a route edge is not controlled, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-47 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-47 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, record separately effective edges as PARTIAL_EFFECT or OUTCOME_UNKNOWN; independently authorize compensation rather than pretending global atomic settlement. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-47 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• An authorized final recipient cannot be replaced by a routing intermediary merely because both claim the same merchant label.¶

• End-to-end maximum payer debit and minimum beneficiary credit are evaluated in their respective typed units.¶

• No independent rail release may inherit unused authority from a failed alternative without protected cancellation or reconciliation.¶

Illustrative adversarial scenarios.¶

• Reroute after approval from bank transfer to a stablecoin chain with different recipient.¶

• Move the fee into a third-currency transfer not displayed to the approver.¶

• Use a stale exchange rate and change decimal precision.¶

Alternative implementations.¶

• Payment orchestrator controlling bank and card dispatch.¶

• Multi-chain wallet plus contract-based swap and route validator.¶

• Treasury ledger plus regulated payout connector with separately enforced sub-reservations.¶

Failure, reconciliation and limits. On a partially completed graph, identify every effective edge and block compensating transfers until separately authorized. Preserve unknown outcomes and distinguish a protocol timeout from proof of nonexecution.¶

Proposed negative-effect conformance vectors. fee_third_asset, fx_quote_stale, switch_rail_unapproved, recipient_alias_changed, swap_slippage_above_bound, partial_rail_commit. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-47).¶

9.4. E-48: Tokenized Commercial Deposit and Central-Reserve Obligation Continuity

Technical application. Bank shared-ledger tokenized-deposit pilots and wholesale multi-currency settlement.¶

Effect-critical native data. Deposit bank and legal issuer identities, customer liability reference, token claim identifier, reserve account, deposit issuance and redemption amounts, ledger commitment, interbank obligations and the evidence type of each external bank posting.¶

Consequence boundary. The first protected boundary is each protected token mint, deposit liability update, interbank settlement instruction and redemption release capable of creating an independent economic effect.¶

 PED-1 bank-obligation manifest: liability id, token amount,
 issuer, eligible receiving bank, settlement asset
        |
 mint request --> PED-2 reads reserve / liability record
              --> mint sink
        |
 interbank transfer sink: token issue, obligation lineage,
 ownership, encumbrance, policy generation, amount continuity
        |
 separate journals; none is evidence for another:
   TOKEN_TRANSFER_COMMITTED     RESERVE_TRANSFER_REQUESTED
   RESERVE_SETTLED              DEPOSIT_LIABILITY_POSTED
        |
 redemption: consume bounded claim identifier; validate the
 bank posting independently

Constructive technical implementation.¶

1. PED-1 creates a bank-obligation manifest binding an account-liability identifier, permitted token amount, identified issuer, eligible receiving bank and authorized settlement asset.¶

2. When a deposit token is minted, PED-2 independently reads the authorized reserve or liability record and checks that the claimed deposit creation is supported under the applicable bank-core trust assumptions.¶

3. Before interbank token transfer, a sink checks token issue, original obligation lineage, present ownership, encumbrance flags, policy generation and amount continuity.¶

4. Separate event journals record TOKEN_TRANSFER_COMMITTED, RESERVE_TRANSFER_REQUESTED, RESERVE_SETTLED and DEPOSIT_LIABILITY_POSTED; the state machine forbids treating one as evidence for another.¶

5. Redemption consumes a bounded claim identifier and independently validates bank-core posting or fund release, preventing the same token claim from authorizing repeated payout.¶

6. Across banks, each protected domain enforces only its actual authoritative local boundary and uses authenticated remote evidence when external results must be considered.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-48 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-48 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that deposit liability, token identifier, bank issuer, reserve/settlement institution, mint or redemption amount, and independently sourced bank posting evidence are consistent. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-48 / NO at any security or business predicate: if a bank-core entry is missing, redemption repeats a consumed token claim, or ledger movement is wrongly treated as proven interbank settlement, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-48 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-48 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, mark OUTCOME_UNCONFIRMED, prohibit renewed issue/redeem under the obligation, and reconcile bank-core and ledger evidence. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-48 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A token transfer receipt is not proof that reserve transfer or redemption has settled.¶

• Token issuance cannot exceed protected authorized deposit liability exposure under stated issuer and reserve assumptions.¶

• A revoked, redeemed or encumbered obligation identifier cannot authorize a fresh redeemable token claim.¶

Illustrative adversarial scenarios.¶

• Redeem twice after a bank-core acknowledgment is lost.¶

• Claim interbank settlement when only a shared-ledger token move is observed.¶

• Substitute a token issued by a different institution with the same ticker symbol.¶

Alternative implementations.¶

• Deposit bank transaction processor and protected ledger adapter.¶

• Shared programmable ledger with bank-signed obligation proofs.¶

• Permissioned settlement system with separate reserve-operator interfaces.¶

Failure, reconciliation and limits. The ledger and bank core may diverge during asynchronous updates; mark OUTCOME_UNCONFIRMED and suspend renewed issuance or redemption associated with the affected obligation until reconciled. No universal atomicity is asserted absent shared commitment control.¶

Proposed negative-effect conformance vectors. issuer_substitution, liability_not_posted, double_redemption, ledger_only_receipt, stale_reserve_state, interbank_partial_failure. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-48).¶

9.5. E-49: Offline Central-Bank Digital Currency Device-Local Spending Bounds

Technical application. Offline retail digital-money device and payment-terminal prototypes under secure-element or similar trusted hardware.¶

Effect-critical native data. Device identity and credential generation, authenticated offline value allocation, local monotonic counter, token or value identifiers, permitted terminal class, expiry, device reset epoch and reconnect reconciliation state.¶

Consequence boundary. The first protected boundary is irreversible local transfer of a spend authorization or value token from the device secure element to the accepting offline terminal.¶

 online issuer/wallet --signed bounded allocation, device epoch,
                        expiry, policy--> secure element (SE)

 terminal --signed unpredictable challenge (terminal identity,
            amount, protocol, transaction id)--> SE

 SE: fresh challenge? unspent allocation? (protected counter,
     spent-token set; application balance text not trusted)
       | yes                                | no
       v                                    v
 one protected transition:            no spendable proof
   mark value/serial spent AND
   emit terminal-bound transfer proof
       |
 reconnect: authenticated journals -> reconciliation; duplicates,
 missing epochs, conflicting histories flagged
 bound: limited offline exposure; compromised SE outside scope

Constructive technical implementation.¶

1. An online issuer or authorized wallet loads a signed bounded offline allocation, device epoch, expiry and device-specific policy into protected device storage.¶

2. A terminal sends a signed unpredictable challenge containing merchant or terminal identity, requested amount, supported protocol and transaction identifier.¶

3. The secure element verifies challenge freshness and available unspent offline allocation against its protected counter and spent-token set, without trusting application-layer balance text.¶

4. In one protected state transition it marks the allocated value or serial as spent and emits a terminal-bound transfer proof or secure message; a failed check emits no spendable proof.¶

5. On reconnection the device submits authenticated journals and receipt references for reconciliation; duplicates, missing epochs or conflicting histories are flagged rather than automatically credited.¶

6. Where the design cannot guarantee global double-spend prevention under cloned or compromised devices, the claim is limited to bounded offline exposure and post-reconnect conflict detection.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-49 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-49 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that device identity, monotonic counter, authenticated offline allocation, value identifier, terminal class, reset epoch, and spend limit are valid inside protected device state. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-49 / NO at any security or business predicate: if a cloned or stale token, reset/counter rollback, missing protected state, exhausted offline value, or unsupported device trust assumptions is detected, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-49 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-49 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, hold further spending and reconcile on reconnect, acknowledging device-clone and compromised-hardware limitations. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-49 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• Spent offline value is not restored after a device rollback or application restart.¶

• A copied terminal challenge cannot obtain two independent spends from one protected allocation.¶

• Offline acceptance does not prove successful online reconciliation or absence of a cloned device.¶

Illustrative adversarial scenarios.¶

• Replay an offline transfer after reverting an application snapshot.¶

• Reset a handset and reuse a pre-reset spend counter.¶

• Relay a terminal challenge to an unauthorized merchant.¶

Alternative implementations.¶

• Embedded Secure Element with monotonic protected counter.¶

• eSIM-class secure applet with signed spending allocation.¶

• Dedicated hardware wallet or offline acceptance token appliance.¶

Failure, reconciliation and limits. If protected state is unavailable, the device does not issue a new spendable proof. Reconnection resolves conflicts and may trigger issuer-defined liability processes; prevention claims explicitly exclude compromised secure hardware unless covered by the security assumptions.¶

Proposed negative-effect conformance vectors. snapshot_rollback, same_token_twice, epoch_reuse, terminal_challenge_relay, offline_budget_exceeded, conflicting_reconnect_history. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-49).¶

9.6. E-50: Cross-Currency Payment-versus-Payment Conditional Release

Technical application. Wholesale FX settlement between institutions, including shared ledgers and heterogeneous payment systems.¶

Effect-critical native data. Two or more currency legs, payer/payee institutions, net obligations, maturity interval, matching identifier, settlement-system instance, conditional-release proof, authorized FX quote and timeout rules.¶

Consequence boundary. The first protected boundary is each independently irrevocable debit, reserve movement or settlement-admission act at a participating institution or protected settlement system.¶

 PED-1: matched obligation set (legs, recipient institutions,
        currencies, amounts, eligibility conditions)

  leg A institution                  leg B institution
  PED-2A: native pending debit       PED-2B: native pending debit
  + common deal id, leg params       + common deal id, leg params
        |                                   |
        +-------- shared atomic settlement domain? ---------+
        | yes                                       | no
        v                                           v
  protected conditional commit      coordinator: reservations,
  releases both legs when all       participant-signed commitments,
  local predicates hold             expiry and abort rules
        |                                           |
  each sink consumes its one-use leg authorization
  observer reports PvP success only from signed per-leg evidence

Constructive technical implementation.¶

1. PED-1 binds a matched obligation set containing exact leg identities, final recipient institutions, currencies, amounts and eligibility conditions.¶

2. Each participating PED-2 reconstructs its own native pending debit and verifies a common authenticated deal identifier and independently agreed leg parameters.¶

3. If participants share a programmable atomic settlement domain, a protected conditional commit releases both legs only when all required local predicates hold.¶

4. If participants occupy independent settlement domains, a coordinator exchanges protected reservations and participant-signed commitments with expiry and abort rules; release is restricted to the actual guarantees available.¶

5. Each sink consumes its one-use leg authorization and records local status. The global observer combines signed per-leg evidence and refuses to state PvP success on the basis of a single local acceptance.¶

6. If an unmatched leg has already executed, the protocol enters PARTIAL_EFFECT and requires independently authorized recovery or loss allocation.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-50 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-50 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that both currency legs, parties, settlement instances, matching identifier, quoted FX terms, maturity window, and conditional-release proof meet the configured PvP admission rule. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-50 / NO at any security or business predicate: if one leg lacks a verified condition, expiry/clock policy fails, or a participant has no enforceable hold, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-50 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-50 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, keep uncommitted legs non-effective; if a leg already settled, preserve PARTIAL_EFFECT and require new authority for any compensation. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-50 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• No asserted atomicity is stronger than the commitment and rollback capabilities of the participating settlement systems.¶

• A completed first currency leg cannot automatically unlock a changed second leg or an unapproved rate.¶

• Final settlement statements require source-appropriate proof from all required systems.¶

Illustrative adversarial scenarios.¶

• One bank changes the counterparty during final message generation.¶

• A commitment expires after one currency leg is admitted.¶

• A coordinator replays an old matched-deal identifier.¶

Alternative implementations.¶

• Single shared-ledger conditional transfer.¶

• Coordinated reserve/debit holds across bank cores.¶

• Hash/secret or timelock conditional flows with explicit non-atomic failure exposure.¶

Failure, reconciliation and limits. Quorum loss, clock disagreement and external finality uncertainty preserve a non-success state. Coordinated abort is possible only for legs that have not independently become irrevocable; otherwise use compensated recovery with a new authority.¶

Proposed negative-effect conformance vectors. leg_beneficiary_substitution, quote_mismatch, coordinator_replay, first_leg_only, commit_timeout, missing_final_settlement_proof. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-50).¶

9.7. E-51: Tokenized-Security Delivery-versus-Payment with Title and Encumbrance Checks

Technical application. Tokenized equities, bonds and real-world asset settlement alongside cash or regulated digital money.¶

Effect-critical native data. Asset identifier, series, legal issuer, share count or face value, registry domain, holding account, encumbrance and freeze state, buyer, seller, price, settlement asset and custody/transfer instruction.¶

Consequence boundary. The first protected boundary is a protected asset ownership change and a distinct protected cash-transfer act, with commit coordination according to the available ledger models.¶

 PED-1: security/asset claim, buyer, seller, settlement account,
        units, payment price
        |                                  |
 asset-side PED-2:                  money-side PED-2:
 ownership, liens, freezes,         payable amount, currency,
 recalls, transfer restrictions     beneficiary after fees/routing
        |                                  |
        +---- reservations / proof commitments ----+
        |   (no silent series or obligation substitution)
        v
 common ledger with atomic exchange?
   yes -> controlled commit transfers both
   no  -> conditional release with recorded partial-outcome states

Constructive technical implementation.¶

1. PED-1 binds a specific security or asset claim to an authorized buyer, seller, settlement account, number of units and payment price.¶

2. The asset-side PED-2 reads actual transferable ownership and any liens, freezes, recalls or transfer restrictions at the operative registry or custody boundary.¶

3. The money-side PED-2 independently reconstructs the actual payable amount, currency and final beneficiary after fees and cash routing.¶

4. Participating sinks exchange condition-specific reservations or proof commitments and ensure that neither side silently substitutes a different series or financial obligation.¶

5. Where a common ledger supports atomic exchange, a controlled commit transfers both. Otherwise use conditional release with explicitly recorded partial-outcome states.¶

6. Regulatory transfer restrictions and issuer actions are checked against versioned protected state; later revocation applies per defined legal and technical effect semantics.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-51 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-51 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that asset registry and legal issuer, title and encumbrance/freeze state, buyer/seller, price, payment asset, custody account, and coordinated DvP evidence are current. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-51 / NO at any security or business predicate: if registry evidence changes, an asset becomes encumbered or frozen, or payment and title legs cannot meet required release conditions, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-51 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-51 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, invalidate affected reservations before commit; record any independent partial effect and obtain separate authority for remedy. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-51 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A matching ticker or asset display name cannot substitute for issuer and security-series identity.¶

• Delivery evidence must originate from the authoritative asset registry or custody service.¶

• Paying a counterparty does not prove transfer of legal or beneficial title.¶

Illustrative adversarial scenarios.¶

• Use a similar token representing a different legal security.¶

• Transfer units already pledged or frozen.¶

• Claim cash settlement as proof of asset-title delivery.¶

Alternative implementations.¶

• Shared custody-money ledger atomic contract.¶

• Separate transfer-agent and bank gateway pair.¶

• Broker/depository control plane with authenticated escrow commitments.¶

Failure, reconciliation and limits. A change in registry control, asset freeze or settlement delay before protected commit invalidates the affected reservation; a partially completed DvP requires an independently authorized reversal or remedy.¶

Proposed negative-effect conformance vectors. wrong_asset_series, encumbered_units, seller_not_owner, cash_asset_partial, issuer_freeze_change, fake_registry_receipt. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-51).¶

9.8. E-52: Stablecoin Mint-Burn-Redemption and Issuer-Liability Continuity

Technical application. Regulated stablecoin issuance and payout integrations within merchant, settlement and treasury stacks.¶

Effect-critical native data. Issuer program and contract identity, mint or burn amount, reserve evidence reference, liability account, authorized institution, redemption beneficiary, chain and token decimals, token epoch and treasury reconciliation status.¶

Consequence boundary. The first protected boundary is mint-authority signature or contract call, irreversible burn and external redemption payout are separate protected effects.¶

 PED-1: issuer, reserve or liability policy, asset contract,
        supply cap, authorized mint/burn principals

 MINT:   PED-2 obtains authenticated reserve statement (provenance,
         time, scope) and actual mint transaction and receiver
         -> mint sink reserves issuance capacity (durable sequence
            number); refuses expired evidence or route bypass

 REDEEM: burn/lock evidence --> one authorized payout obligation
         -> bank sink: beneficiary, currency, amount, payout state

 independent evidence records: supply change | chain reorg |
 bank payout acknowledgment (no cross-domain finality inference)

Constructive technical implementation.¶

1. PED-1 registers the permitted issuer, reserve or bank-liability policy, eligible asset contract, supply cap and authorized mint/burn principals.¶

2. Prior to mint, PED-2 obtains an authenticated current reserve/liability statement with its provenance, time and scope and verifies the actual mint transaction and receiver.¶

3. The mint sink reserves authorized issuance capacity with a durable sequence number and refuses issuance on expired evidence or independent route bypass.¶

4. Redemption binds burn or lock evidence to a single authorized payout obligation; a separate bank sink checks beneficiary, currency, amount and payout state before release.¶

5. Supply changes, chain reorganizations and bank-side payout acknowledgments are maintained as independent evidence records with no unjustified cross-domain finality inference.¶

6. Issuer controls may be implemented at signers, mint contracts, dedicated HSMs or regulated bank adapters with explicit key-escape and emergency-access assumptions.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-52 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-52 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that issuer identity, token contract and epoch, mint/burn amount, reserve/liability evidence, redemption payee, decimals, and treasury posting correspond to the particular operation. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-52 / NO at any security or business predicate: if reserve attestation is unverifiable, code/token version changes, payout is duplicated, or account/beneficiary differs, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-52 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-52 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, retain INDETERMINATE for reserve uncertainty or OUTCOME_UNKNOWN for redemption payout, and reconcile without a repeated issue or payout. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-52 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• No issuer may mint beyond a protected cap while ignoring concurrent outstanding issuance reservations.¶

• A token burn does not prove a bank payout completed.¶

• A redeemed burn or redemption ID cannot produce a second payout even after restart.¶

Illustrative adversarial scenarios.¶

• Reuse stale reserve evidence for several simultaneous mints.¶

• Substitute a look-alike stablecoin contract on a different chain.¶

• Replay the same burn proof through a second redemption connector.¶

Alternative implementations.¶

• Non-exportable issuing signer.¶

• Contract-controlled mint gate with authenticated reserve oracle.¶

• Bank-integrated liability controller enforcing both token and cash activity.¶

Failure, reconciliation and limits. Unverifiable reserve evidence yields INDETERMINATE rather than mint permission. Unknown payout outcomes prevent a renewed redeem instruction until reconciliation, with separate fraud and issuer solvency assumptions.¶

Proposed negative-effect conformance vectors. mint_cap_race, stale_reserve_attestation, wrong_token_contract, burn_proof_replay, payout_unknown, decimal_scale_change. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-52).¶

9.9. E-53: Cross-Chain Bridge, Rollup and Reorganization-Aware Finality

Technical application. Multi-chain agent wallets, rollups, bridges and token distribution across different consensus models.¶

Effect-critical native data. Source chain and finalized block reference, source bridge contract, message nonce and hash, token identity, lock/burn proof, target chain, mint/release contract, final beneficiary and source finality rule.¶

Consequence boundary. The first protected boundary is source-chain lock or burn and independent destination-chain mint or release authorization, each at its own effective boundary.¶

 source chain                           destination chain
 lock/burn --> PED-2 (source):          target verifier:
               digest, nonce,           source proof vs source-
               commitment;              specific finality policy,
               unfinalized log =        bridge-contract version,
               PROVISIONAL              consume source-message id
                     |                          |
                     +-------> sink before mint/release:
                               mapped asset, amount, fee,
                               destination address, contract
                               implementation generation
 reorganization or challenged proof -> challenge/hold policy
 finalized threshold != economic-finality threshold

Constructive technical implementation.¶

1. PED-1 binds a transfer obligation to exact source asset and chain, destination asset mapping, destination beneficiary and allowed finality assumptions.¶

2. PED-2 on the source side reconstructs the actual lock or burn, message digest, nonce and chain-specific commitment; an unfinalized log is labelled PROVISIONAL.¶

3. The target-side verifier validates the authenticated source proof against a source-specific finality policy, checks bridge-contract version and consumes a durable source-message identifier.¶

4. Before destination mint/release, a sink compares mapped asset identity, amount, fee, destination address and allowed contract implementation generation.¶

5. Source reorganization events or challenged proofs are handled by a challenge/hold policy appropriate to the source consensus; finalized and economic-finality thresholds are not conflated.¶

6. If the destination effect precedes a source finality failure, the result is classified as a bridge-risk loss or recovery state rather than falsely undone by local accounting.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-53 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-53 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that authenticated source chain and event, finality checkpoint and challenge interval, bridge message identifier, asset mapping, destination contract, amount, and beneficiary all match. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-53 / NO at any security or business predicate: if source finality is not met, proof reorganizes, bridge message was consumed, recipient changed, or destination implementation is untrusted, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-53 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-53 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, hold destination release as PROVISIONAL/UNKNOWN; if already effective, record the irreversible effect and use independently authorized recovery. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-53 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A source transaction hash by itself is not proof of final source-chain settlement.¶

• A cross-chain message may authorize destination release at most once per authenticated bridge domain.¶

• A relayer may not change the destination recipient while retaining the same human-visible transfer summary.¶

Illustrative adversarial scenarios.¶

• Mint on destination against a source log removed by reorganization.¶

• Replay bridge proof through two different relayers.¶

• Upgrade destination bridge implementation between approval and execute.¶

Alternative implementations.¶

• On-chain light-client proof verifier.¶

• Threshold attestation with independent finality policy at the destination sink.¶

• Optimistic proof and bounded challenge period plus an enforced release hold.¶

Failure, reconciliation and limits. Unfinalized, disputed or unverifiable source evidence causes a protected hold. If a destination release has occurred, record an uncorrected external effect and use separately approved recovery; the mechanism cannot reverse independent chains by assertion.¶

Proposed negative-effect conformance vectors. source_reorg, bridge_message_replay, recipient_replaced, contract_upgrade, insufficient_confirmations, asset_mapping_substitution. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-53).¶

9.10. E-54: Exchange Treasury Withdrawal and Multi-Venue Custody Continuity

Technical application. Crypto exchange wallets, autonomous asset movement, portfolio rebalancing and treasury operations.¶

Effect-critical native data. Account mandate, asset contract, chain, beneficiary address plus address-book generation, withdrawal amount, total position exposure, custody wallet identity, signer quorum, fee, nonce and network status.¶

Consequence boundary. The first protected boundary is the first externally usable custody signature or effective withdrawal instruction, and any on-chain contract-controlled transfer that can bypass the off-chain signer.¶

 PED-1: account ownership, asset, destination identity, whitelist
        generation, signer roster, aggregate exposure, windows

 planner route (hot or cold wallet) --> protected transaction queue
        |
 PED-2: native signed preimage, custody source, target contract,
        chain, nonce, fee, delegated wallet implementation
        |
 each signing share / final sign interface: exact-effect equality
 + atomic nonce and risk-budget reservation
        |
 any unrestrained key or contract method able to withdraw?
   yes -> separate on-chain / programmable-account guard required

Constructive technical implementation.¶

1. PED-1 binds a permitted withdrawal to account ownership, asset, destination identity, whitelist generation, authorized signer roster, aggregate exposure and time windows.¶

2. A planner may route through hot or cold wallets, but its proposed route cannot transfer or sign without entering the protected transaction queue.¶

3. PED-2 independently inspects native signed preimage and the effective custody source, target contract, chain, nonce, fee and any delegated wallet implementation.¶

4. At each independent signing share or final sign interface, a protected verifier checks exact-effect equality and allocates a nonce and risk-budget reservation under atomic protected state.¶

5. A separate on-chain or programmable-account guard is required if any unrestrained key or alternate contract method could effect the withdrawal without the protected off-chain sink.¶

6. Confirmed transmission, chain inclusion, finality depth and beneficiary receipt remain distinct; policy changes fence pending but not yet executed withdrawals.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-54 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-54 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that wallet and signer identity, chain, withdrawal address-book generation, native beneficiary bytes, asset, fee, nonce, exposure and quorum/budget are current. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-54 / NO at any security or business predicate: if treasury recipient or chain is substituted, quorum is stale, an exposure threshold fails, or an unmediated signer path exists, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-54 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-54 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, hold nonce/reservation and inspect native transaction/signature records; no new signature merely because the sending API timed out. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-54 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• No raw signing or emergency path may bypass the protected effect boundary within the claimed deployment scope.¶

• Chain, token contract, recipient and asset amount are independently reconstructed from effective transaction bytes.¶

• Concurrently scheduled withdrawals cannot each consume the full same exposure limit.¶

Illustrative adversarial scenarios.¶

• A signer-approved transfer changes to a different destination after gas estimation.¶

• A delegated wallet is upgraded while retaining its authorization label.¶

• Two autonomous treasury agents concurrently withdraw against the same daily budget.¶

Alternative implementations.¶

• Fixed-function HSM with final transaction parsing.¶

• MPC shares independently checking the same policy generation.¶

• Smart-account validation hook with protected on-chain spend accounting.¶

Failure, reconciliation and limits. On custody service interruption, retain nonce-reservation and signature status. Never produce a fresh signature solely because the sending API timed out; reconciliation uses native transaction identifiers and signer logs.¶

Proposed negative-effect conformance vectors. withdrawal_destination_swap, mpc_quorum_conflict, hot_wallet_bypass, daily_limit_race, chain_id_change, signature_status_unknown. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-54).¶

9.11. E-55: Merchant Alias, QR and Beneficiary Resolution Continuity

Technical application. QR payments, dynamically resolved payment aliases, merchant paylinks, bank account aliases and interoperable wallets.¶

Effect-critical native data. Displayed merchant name, authoritative merchant ID, alias or QR payload, resolved account/contract, merchant-register generation, amount, currency, terminal identity and resolution validity.¶

Consequence boundary. The first protected boundary is release of the exact payment instruction after final alias resolution at the controlled payment-switch, wallet or bank connector.¶

 PED-1: merchant identity and payment scope (not the label/alias)

 QR / alias / paylink --> PED-2: fresh authenticated resolution
                          (designated resolver or signed record)
        |
 final native account/address == authorized merchant record?
 resolution version, time and expected terminal current?
   alias changed -> only with a rotation proof binding old and
                    new destinations within the same merchant
        |
 sink consumes resolution-specific authorization -> dispatch
 payer debit and merchant credit tracked separately;
 visual similarity is never a cryptographic equivalence test

Constructive technical implementation.¶

1. PED-1 binds a merchant identity and allowable payment scope independently of its user-facing label or mutable alias.¶

2. PED-2 requests fresh authenticated alias resolution from the designated resolver or obtains a verifiable signed resolution record.¶

3. The final native destination account or blockchain address is compared with the authorized merchant record, and resolution version, time and expected terminal are checked.¶

4. A changed alias cannot inherit authorization unless an explicitly allowed rotation proof binds both old and new destinations within the same merchant identity.¶

5. The sink consumes a beneficiary-resolution-specific authorization and dispatches only the verified native payment representation.¶

6. After dispatch, payer-debit and merchant-credit statuses are tracked separately; visual display similarity is never used as a cryptographic equivalence test.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-55 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-55 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that final alias/QR resolution, authenticated merchant identifier and registry generation, destination account or contract, terminal, amount, and currency agree. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-55 / NO at any security or business predicate: if merchant resolution is stale or ambiguous, the QR or resolved destination changes, or a cached display label is the sole evidence, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-55 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-55 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, keep the payment non-effective and obtain fresh authenticated resolution or renewed authority. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-55 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• Merchant-facing aliases do not independently prove the current authorized settlement beneficiary.¶

• An alias change after authorization requires an authenticated rotation rule or new approval.¶

• Only the resolved effective destination, not a QR display label, controls the sink decision.¶

Illustrative adversarial scenarios.¶

• Substitute a QR code on a merchant display.¶

• Change an account alias between user approval and bank submission.¶

• Reuse a signed old alias result after a merchant migration.¶

Alternative implementations.¶

• Wallet-side protected resolver.¶

• Bank/UPI-like switch with merchant registry generation binding.¶

• Merchant terminal secure element signing the actual account and amount.¶

Failure, reconciliation and limits. If merchant identity cannot be established or resolution races with re-registration, refuse release and request new authorization or authenticated resolution; no optimistic payment based only on cached labels.¶

Proposed negative-effect conformance vectors. qr_payee_swap, alias_resolution_race, merchant_registry_rollback, terminal_swap, old_resolution_replay, merchant_label_confusable. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-55).¶

9.12. E-56: Machine-Speed Metered Payments and Batched Settlement Accounting

Technical application. API metering, compute/data pay-per-use, machine-to-machine micropayments and sub-cent service charging.¶

Effect-critical native data. Metered service ID, usage quantity and unit, interval, independently measured consumption, rate plan version, amount in smallest units, payer budget, provider beneficiary and batch membership.¶

Consequence boundary. The first protected boundary is deduction or transfer of funds, release of a paid-usage entitlement, or emission of a settlement batch that becomes irrevocable.¶

 PED-1: max cost per unit, total budget, service identity,
        acceptable metering authority

 meter reports --> non-effective event stream (authenticated,
                   strictly increasing interval or sequence)
        |
 PED-2: recompute payable usage in integer units
        (no float drift, no duplicate intervals)
        |
 each debit reserves from a protected cumulative budget
 each batch carries a Merkle root or canonical manifest
        |
 financial sink: manifest, amount conservation, consumed
 membership set --> release aggregate payment

Constructive technical implementation.¶

1. PED-1 binds a maximum cost-per-unit, total campaign budget, service identity and acceptable metering authority for an agent or connected device.¶

2. Untrusted meter reports are collected into a non-effective event stream; authenticated meter evidence is associated with a strictly increasing usage interval or event sequence.¶

3. PED-2 recomputes payable usage and exact integer-denomination amounts from independently selected measurement data, eliminating float-rounding drift and duplicate intervals.¶

4. Each authorized debit reserves amount from a protected cumulative budget, and each settlement batch carries a Merkle-root or canonical manifest of authorized micro-obligations.¶

5. The financial sink validates the batch manifest, amount conservation and the already-consumed membership set before releasing the aggregate payment.¶

6. Service entitlements and actual measured resource consumption retain their own receipt states, separate from the financial settlement record.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-56 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-56 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that independently authenticated usage measurement, unit and interval, tariff version, beneficiary, integer minor-unit amount, batch membership, and remaining protected budget agree. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-56 / NO at any security or business predicate: if a meter record is duplicated, unit/rate changes, concurrent debit exceeds the cap, or a settlement batch has unresolved effects, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-56 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-56 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, freeze affected interval or batch; reconcile committed usage and require an authenticated adjustment event for correction. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-56 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A duplicated usage interval may not be billed twice even if emitted by a second agent.¶

• sum(settled micro-obligations) <= sum(authorized measured charges) within the same typed currency.¶

• Batch netting cannot quietly introduce a new merchant or service provider.¶

Illustrative adversarial scenarios.¶

• Meter doubles reported GPU-seconds while retaining a legitimate signed invoice.¶

• Two batch workers each include the same micro-obligation.¶

• Tiny per-unit fee rounding exceeds the protected aggregate ceiling.¶

Alternative implementations.¶

• HSM-guarded payment switch plus signed meter.¶

• State-channel or payment-channel settlement with protected sequence number.¶

• Smart contract aggregate batch verifier with off-chain usage attestations.¶

Failure, reconciliation and limits. Inconsistent meter or unsettled batch state freezes further debits for the affected interval; disputed measurements require a new authenticated adjustment event, not edits to committed historical usage.¶

Proposed negative-effect conformance vectors. duplicate_meter_interval, batch_duplicate_membership, rounding_overcharge, meter_identity_swap, stale_rate_plan, batch_unknown_settlement. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-56).¶

9.13. E-57: Privacy-Preserving Financial Compliance Proof at Execution Boundary

Technical application. Conditional compliance controls for fintech and wholesale cross-border payments with data-minimizing attestations.¶

Effect-critical native data. Regulatory policy version, transaction amount class, counterparty-jurisdiction attributes, proof issuer, allowed proof statement, expiry, revocation epoch, transaction commitment and selective-disclosure policy.¶

Consequence boundary. The first protected boundary is the actual protected release of payment signing, ledger transfer or settlement admission following policy-scope verification.¶

 PED-1: permissible transaction class + required predicates

 applicant: signature / attribute credential / zero-knowledge
            proof bound to exact transaction commitment and sink
        |
 PED-2: proof issuer, circuit/schema id, public inputs,
        semantics, expiry, current revocation
        |
 sink: reconstruct effect fields; do public inputs commit to
       these same fields?   (valid proof, other transfer -> DENY)
        |
 consume one-use authorization; private attributes not kept in
 an unprotected log; unknown/invalid/policy drift -> DENY/review

Constructive technical implementation.¶

1. PED-1 fixes what class of transaction is permissible and which verifiable compliance predicates must be satisfied at final execution.¶

2. The applicant supplies a signature, attribute credential or zero-knowledge proof bound to the exact transaction commitment and intended sink.¶

3. PED-2 verifies proof issuer, circuit/schema identifier, public inputs, acceptable proof semantics, expiry and current revocation against protected domain state.¶

4. The sink independently reconstructs required effect fields and checks that the proof public inputs commit to those same fields; a valid proof for a different transfer is rejected.¶

5. Upon approval a one-use authorization is consumed without unnecessarily storing underlying private beneficiary or customer attributes in an unprotected log.¶

6. Unknown jurisdiction data, invalid proofs or policy drift leads to deny or a non-effective review state; privacy does not bypass mandatory legal compliance.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-57 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-57 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that the proof issuer, transaction commitment, policy statement, jurisdiction-scope data, expiry, policy generation, and live revocation evidence are valid at the actual effect boundary. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-57 / NO at any security or business predicate: if the statement does not cover the transaction, a proof expired, or required revocation/policy evidence is unavailable, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-57 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-57 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, keep the candidate non-effective; obtain fresh supported evidence or use a separately authorized compliant disclosure mechanism. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-57 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• Proof validity is necessary but not sufficient: proof context must match the exact final financial effect.¶

• A proof from one applicable jurisdiction or policy generation cannot be replayed in another.¶

• Redaction of private attributes does not remove the obligation to establish all required authorized predicates.¶

Illustrative adversarial scenarios.¶

• Reuse a compliance proof on a different recipient.¶

• Change proof policy-version input while retaining original ZK statement.¶

• Submit valid privacy proof after credential revocation.¶

Alternative implementations.¶

• TEE verifier with attested public inputs.¶

• ZK verifier module in a smart-account contract.¶

• Bank settlement gateway with selective-disclosure credential support.¶

Failure, reconciliation and limits. When fresh revocation or required policy evidence cannot be verified, keep the financial candidate non-effective; unsupported privacy systems may use explicit authenticated disclosure under applicable rules.¶

Proposed negative-effect conformance vectors. proof_rebinding, jurisdiction_swap, revoked_credential, wrong_public_inputs, proof_schema_downgrade, missing_compliance_predicate. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-57).¶

9.14. E-58: Financial Message Semantic Continuity Across Interoperability Adapters

Technical application. ISO 20022 messages, proprietary bank APIs, merchant payment events and tokenized-settlement adapters.¶

Effect-critical native data. Initiating-party and beneficiary identity, account aliases, instructed/settlement amounts, currency and scale, charges, value date, purpose, payment identification, return references, message standard version and native critical fields.¶

Consequence boundary. The first protected boundary is native interbank message release, payment switch submission, account debit or outgoing ledger transfer after the last data-format transformation.¶

 PED-1: versioned canonical obligation schema with mandatory and
        critical extension fields

 API --> queue --> batch file --> ISO 20022-like message
     (each transformation keeps authenticated lineage)
                                        |
 PED-2: strict versioned parser on the FINAL emitted bytes ->
        debtor, creditor, amount, fees, purpose, references
                                        |
 typed field-by-field equality or authorized mapping;
 unknown critical extension, truncation, ambiguous unit -> DENY
                                        |
 sink consumes release authorization bound to final native bytes
 and parser/schema generation

Constructive technical implementation.¶

1. PED-1 binds a versioned canonical financial obligation schema with explicit mandatory and critical extension fields.¶

2. A payment message may be transformed across API, queue, batch-file and ISO 20022-like representations only while preserving authenticated transformation lineage.¶

3. PED-2 parses the final emitted native representation using a strict versioned parser and reconstructs the effective debtor, creditor, amount, fees, purpose and reference identifiers.¶

4. A typed semantic comparison verifies field-by-field equality or an explicitly authorized mapping; unknown critical extensions, truncation or ambiguous unit conversions cause denial.¶

5. The sink consumes a bounded release authorization referencing the final native bytes and the parser/schema generation, preventing approval of an earlier intermediary representation.¶

6. Downstream acknowledgments and clearing or settlement evidence remain separated, each checked against the original obligation and message correlation.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-58 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-58 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that the last native adapter output preserves initiating party, intended beneficiary, account, amount, currency scale, charges, purpose, value date, references and all critical schema fields. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-58 / NO at any security or business predicate: if two independent parsers disagree or an adapter drops, converts, or substitutes a critical payment field, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-58 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-58 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, set PARSER_DISAGREEMENT and block release until trusted re-parsing or a new authority and schema are established. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-58 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A successful schema parse does not establish transaction authorization.¶

• A noncritical display-label change cannot mask a changed native creditor or settlement amount.¶

• Protocol downgrade cannot discard effect-critical fields without reauthorization.¶

Illustrative adversarial scenarios.¶

• Map a beneficial owner to the wrong final creditor account.¶

• Drop a fee or purpose restriction during protocol downgrade.¶

• Change minor-unit interpretation between APIs.¶

Alternative implementations.¶

• Bank core message-release hook.¶

• Payment orchestration adapter with exclusive settlement dispatch.¶

• Protocol-safe HSM signer over typed native message semantics.¶

Failure, reconciliation and limits. If two decoders disagree on a critical effect attribute, mark PARSER_DISAGREEMENT and block release pending a schema upgrade or new authenticated mandate.¶

Proposed negative-effect conformance vectors. critical_field_dropped, debit_credit_reversal, minor_unit_truncation, beneficiary_mapping_error, schema_downgrade, unrecognized_proprietary_field. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-58).¶

9.15. E-59: Recurring Conditional Mandate and Autonomous Subscription Control

Technical application. Agent-managed recurring payments, renewals, streaming billing and conditional service procurement.¶

Effect-critical native data. Mandate ID and generation, billing cadence, service identity, cycle maximum, aggregate limit, price/rate changes, minimum service condition, renewal eligibility, grace period and revocation time.¶

Consequence boundary. The first protected boundary is each cycle-specific debit instruction or settlement release, not the original acceptance of a recurring mandate.¶

 PED-1: bounded recurring authority (finite periods or cap,
        provider identity, price-change rule)

 billing cycle k --> new Candidate Act with protected cycle index k
        |
 PED-2: billable period, provider, rate, measured service,
        previously paid cycles
        |
 atomic reserve + consume (cycle k, amount)
   scheduler 1 --+
                 +--> at most one charge for cycle k
   scheduler 2 --+
 price increase, new recipient, cancelled or expired -> DENY
 refund, pro-rata, delivery -> separate obligations and evidence

Constructive technical implementation.¶

1. PED-1 binds a bounded recurring authority with a finite number of periods or upper spend cap, permitted provider identity and price-change rule.¶

2. Each billing cycle produces a new Candidate Act identified by a protected cycle index; its payable amount is independent of merely possessing the original consent token.¶

3. PED-2 confirms the actual billable period, provider, rate, measured service and any previously paid cycles at execution time.¶

4. Protected state atomically reserves and consumes the specific cycle index and amount; two scheduling workers cannot produce two charges for the same period.¶

5. An unapproved price increase, new recipient, cancelled subscription or reactivated expired mandate yields denial.¶

6. Refund, pro-rata adjustment and provider-delivery events are represented by separate obligations and outcome evidence.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-59 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-59 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that the present billing cycle, renewal eligibility, service identity, cycle and aggregate maximum, current tariff, mandate generation and revocation state authorize this specific debit. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-59 / NO at any security or business predicate: if a mandate is revoked, cycle already paid, price or interval exceeds the bound, or concurrent billing violates the remaining allowance, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-59 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-59 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, retain the cycle reservation on UNKNOWN, query the specific downstream transaction, and do not blindly rebill. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-59 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A perpetual recurring approval does not grant an unlimited bearer capability.¶

• Per-cycle spending is bounded by both cycle and aggregate protected limits.¶

• Renewal on a revoked or expired mandate cannot proceed using a cached subscription flag.¶

Illustrative adversarial scenarios.¶

• Provider secretly doubles next billing cycle price.¶

• Two AI scheduler instances charge the same renewal.¶

• Old provider alias is reused after ownership transfer.¶

Alternative implementations.¶

• Card-on-file token processor with protected cycle ledger.¶

• Smart contract recurring mandate and monotonic cycle state.¶

• Bank direct-debit adapter with bounded debit generation.¶

Failure, reconciliation and limits. A cycle with unknown external payment outcome remains reserved during inquiry; correction requires a separately authorized adjustment or proven non-execution.¶

Proposed negative-effect conformance vectors. duplicate_cycle, renewal_after_revocation, price_increase, service_identity_changed, cycle_time_shift, refund_replay. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-59).¶

9.16. E-60: Financial Dispute, Chargeback and Compensating-Transfer Authority

Technical application. Card, fintech wallet, merchant and regulated digital-asset refund, reversal and dispute systems.¶

Effect-critical native data. Original transaction ID and settlement evidence, dispute case, allowed dispute type, refund reason, payer and payee identity, amount already reversed, chargeback window, authorized adjustment source and destination.¶

Consequence boundary. The first protected boundary is each refund, reversal, chargeback posting, merchant reserve debit or independent clawback release that changes economic position.¶

 PED-1: adjustment policy (original obligation, dispute
        authority, maximum reversal, recipient-inheritance rules)

 refund / reversal / chargeback --> PED-2: final rail or ledger
                                    message + original lineage
        |
 protected journal: refunded | disputed | charged back |
                    still reversible
        |
 sink: total compensation <= authorized amount; destination is
       the original funding route or a separately approved one
       (no redirection by editing invoice text)

Constructive technical implementation.¶

1. PED-1 registers an adjustment policy specifying the original obligation, eligible dispute authority, maximum reversal amount and recipient-inheritance rules.¶

2. PED-2 independently reconstructs the requested adjustment from the final payment-rail or ledger message and authenticates original transaction lineage.¶

3. The protected journal tracks cumulatively refunded, disputed, charged-back and still-reversible amounts using defined mutually exclusive or overlapping evidence categories.¶

4. Before an effective adjustment, the sink verifies that the change is within legal/contractual policy and that the total compensation cannot exceed the authorized amount.¶

5. The sink binds adjustment payment destination to the permissible original funding route or a separately approved replacement; an agent cannot direct refunds to a new account by editing invoice text.¶

6. The finality record distinguishes chargeback initiation, provisional merchant debit, adjudication, final chargeback and any post-resolution reversal.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-60 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-60 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that original payment/settlement record, case reason and window, refund beneficiary, reversal amount, previously refunded sums, and scheme-specific authorization support a new adjustment. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-60 / NO at any security or business predicate: if the original transaction cannot be proved, an adjustment would duplicate a refund, reverses more than remains, or legal/scheme conditions are unmet, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-60 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-60 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, hold adjustment authority under unknown outcome; reconcile the original identifier and require separate permission for later corrections. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-60 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• A refund may not exceed the still-authorized refundable balance absent a new explicit authority.¶

• The original successful payment receipt cannot authorize arbitrary compensating transfers.¶

• Dispute initiation, provisional posting and final adjudication have distinct evidence semantics.¶

Illustrative adversarial scenarios.¶

• Replay the same refund through a second processor.¶

• Move a legitimate refund to a newly substituted beneficiary.¶

• Issue simultaneous refund and chargeback beyond original charge.¶

Alternative implementations.¶

• Issuer/merchant acquiring core with protected disputes register.¶

• Payment-service provider refund API guarded by a settlement-gate ledger.¶

• Smart-contract escrow and separate authenticated arbitration interface.¶

Failure, reconciliation and limits. An adjustment with unknown outcome remains pending and does not replenish refund capacity. Separate legal entitlements and scheme obligations may require additional manual authorization, but the last effective instruction remains protected.¶

Proposed negative-effect conformance vectors. refund_duplicate, refund_new_beneficiary, chargeback_refund_race, excess_reversal, wrong_original_reference, dispute_pending_not_final. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-60).¶

9.17. E-61: Autonomous Trading Strategy-to-Order-to-Fill Continuity

Technical application. Agentic spot, derivative and tokenized-instrument trading with prompt-to-execution strategies and exchange order APIs.¶

Effect-critical native data. Strategy approval digest, instrument/venue identity, order side, order type, limit and stop conditions, maximum price/slippage, notional/position limits, margin mode, leverage, account, order validity and cancel/replace generation.¶

Consequence boundary. The first protected boundary is exchange-matching-engine order admission or the last exclusive API/signing boundary capable of placing or modifying an effective order.¶

 PED-1: strategy -> measurable constraints (markets, instrument,
        exposure, frequency, order types, risk bounds, account gen)

 planning agent --candidate order--> NES
        |
 PED-2: exchange-facing native bytes + fresh market/account
        snapshot -> worst-case fill liability, margin, fees
        |
 atomic reservation of notional, quantity and leverage across
 all subagents and outstanding orders
        |
 order release (matching-engine admission or last API/signing
 boundary); partial fill -> update consumed exposure;
 cancel/replace -> lineage check, DENY if beyond mandate

Constructive technical implementation.¶

1. PED-1 binds a human-authorized strategy into measurable constraints: eligible markets, instrument, maximum exposure, trade frequency, order types, risk boundaries and account generation.¶

2. A planning agent emits a candidate order; actual exchange-facing native bytes and a fresh market/account snapshot are obtained independently by PED-2.¶

3. The verifier derives the worst permitted fill liability, reserved margin, fees and potential position exposure, using conservative rounding and stale-data rules.¶

4. Before order release, the protected risk state atomically reserves notional, quantity and leverage exposure across all concurrently acting subagents and outstanding orders.¶

5. Partial fills update consumed exposure; cancel/replace carries order lineage and is denied if it changes constraints beyond the original protected mandate or causes transient double exposure.¶

6. Liquidation or exchange-initiated events outside local control are separately identified; a local gate cannot claim to block exchange-side effects after an order becomes effective.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-61 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-61 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that strategy mandate, native venue/instrument, side, order limits, margin/leverage, cancel/replace generation, and current filled plus pending exposure conform. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-61 / NO at any security or business predicate: if an order replacement or venue switch changes authorized risk, previous cancel is uncertain, or aggregate exposure exceeds the protected limit, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-61 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-61 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, retain the exposure reservation, reconcile venue order IDs and fills, and refrain from new effective orders on unknown cancellation. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-61 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• An agent strategy or model-generated plan is not itself authority for any order that exceeds actual risk budgets.¶

• Outstanding open orders and already filled positions participate in cumulative exposure calculations.¶

• Cancel acknowledgment does not mean cancellation succeeded until verified by authoritative exchange state.¶

Illustrative adversarial scenarios.¶

• Switch an approved limit buy to an unbounded market buy.¶

• Two agents simultaneously open exposures that individually fit but collectively exceed a limit.¶

• Cancel and replace with a larger notional before old order cancellation finalizes.¶

Alternative implementations.¶

• Exchange-side risk gateway with atomic account exposure ledger.¶

• HSM-signed order-entry adapter plus authenticated live-order state.¶

• Smart-account/DEX contract validator limiting aggregate position and slippage.¶

Failure, reconciliation and limits. When a cancel or order outcome is unknown, retain exposure reservation and reconcile exchange order IDs and fills. Model confidence, market predictions or approval logs never substitute for current protected exposure.¶

Proposed negative-effect conformance vectors. limit_to_market_change, dual_agent_exposure, cancel_replace_race, stale_account_margin, venue_substitution, unknown_fill_state. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-61).¶

9.18. E-62: Delegated Financial-Agent Treasury and Subagent Budget Partitioning

Technical application. Agent-controlled treasury accounts, subagent purchasing, vendor payouts and cross-application money management.¶

Effect-critical native data. Treasury owner and account, subagent identity chain, delegated purpose, permitted counterparties and currencies, parent/child budgets, grant generation, authorized payout task, expiry and revocation state.¶

Consequence boundary. The first protected boundary is effective treasury debit, transfer, payment authorization or issuance of a child capability that enables another actor to initiate the effect.¶

 PED-1 root treasury mandate
        |  non-bearer delegation record (subset of parent)
        v
 child grant: recipient, amount, account, purpose, time
        |  atomic escrow of parent remaining spend
        |  (or durably serialized shared quota)
        v
 subagent payment --> PED-2: final payment, task origin,
                      ultimate destination (nested processors)
        |
 final sink: complete parent-child lineage, revocation
 generation, aggregate outstanding reservations -> debit
 unknown transfer -> hold child allocation; reclaim only on
 reliable outcome evidence

Constructive technical implementation.¶

1. PED-1 binds a protected root treasury mandate that enumerates authorized activities and grants only bounded children through a non-bearer delegation record.¶

2. A subagent requests task-limited authority with recipient, amount, account, purpose and spend-time constraints that must be a subset of its parent authorization.¶

3. Protected state atomically escrows a fraction of the parent remaining spend to the child or coordinates a shared quota with durable serialization.¶

4. PED-2 independently reconstructs the final treasury payment, actual subagent task origin and ultimate settlement destination, including nested payment-processor transformations.¶

5. The final sink validates complete parent-child lineage, current revocation generation and aggregate outstanding reservations before emitting effective debit authority.¶

6. Returned unused child budget requires authenticated nonuse or expiration reconciliation; parent revocation fences all unspent children subject to the chosen offline trust model.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-62 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-62 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that parent treasury mandate, subagent lineage, grant generation, permitted counterparty/currency, delegated purpose, and protected parent/child reservations remain valid. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-62 / NO at any security or business predicate: if a child exceeds its allocation, a grant is revoked, sibling reservations overlap, or the delegation creates an unguarded spend path, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-62 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-62 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, hold the child allocation for unknown transfers; reclaim only against reliable outcome evidence and preserve any already effective child operations. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-62 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• No child or descendant agent can increase its ancestor budget, purpose or eligible recipient scope.¶

• A parent mandate and child delegated record cannot both authorize the same unreserved spend capacity.¶

• Revoking a parent prevents future effective child actions within the controlled enforcement domain.¶

Illustrative adversarial scenarios.¶

• A subagent recursively delegates to gain a higher aggregate limit.¶

• Two independent child agents spend against a copied allocation.¶

• A revoked parent leaves an offline child token incorrectly reusable.¶

Alternative implementations.¶

• Treasury HSM policy engine with quota escrow.¶

• Bank subaccount and spending-control API.¶

• Account-abstraction wallet with nontransferable session authority and protected nested limits.¶

Failure, reconciliation and limits. Unknown transfer outcomes retain the corresponding sub-budget reservation. Child allocations cannot be reclaimed for reuse merely because a worker disconnected or stopped responding.¶

Proposed negative-effect conformance vectors. child_budget_amplification, delegation_cycle, dual_child_spend, revoked_ancestor, purpose_privilege_escalation, reclaim_unknown_child_budget. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-62).¶

9.19. E-63: Autonomous Accounts-Payable Invoice and Supplier-Portal Finality

Technical application. Buyer-to-supplier AI-initiated invoice payments through portals, virtual cards, bank APIs and supplier network intermediaries.¶

Effect-critical native data. Buyer approval identity, supplier legal identity, invoice number/line items, purchase order, bank account or virtual-card payee, payable amount, taxes, discounts, due date, ERP payment status and supplier-portal correlation.¶

Consequence boundary. The first protected boundary is effective bank debit, virtual-card capture or payment instruction issued by a buyer-side privileged adapter after interacting with an independent supplier portal.¶

 PED-1: verified invoice instance, authorized supplier, payable
        maximum, ERP approval generation

 agent <--> supplier portal (lower-trust evidence; cannot modify
            the approved invoice)
        |
 PED-2: final payable request after matching, tax/discount,
        currency conversion, payee resolution
        |
 sink: buyer debit and beneficiary vs supplier master record;
       duplicate-invoice and paid-state markers in journal
        |
 atomic invoice-payment consumption -> bank / card release;
 portal receipt and settlement evidence authenticated separately

Constructive technical implementation.¶

1. PED-1 binds a payment obligation to a verified invoice instance, authorized supplier, payable maximum and ERP approval generation.¶

2. An agent navigates a supplier portal, but portal fields and page content are treated as lower-trust evidence and cannot independently modify the protected approved invoice.¶

3. PED-2 reconstructs the final payable request after invoice matching, taxes/discounts, currency conversion and portal credential or payee resolution.¶

4. A sink compares the effective buyer debit and final beneficiary with the original supplier master record and checks duplicate-invoice and paid-state markers in a protected journal.¶

5. Only after the atomic invoice-payment consumption is the bank or card authorization released; supplier-portal receipt and settlement evidence are separately authenticated.¶

6. Split invoices and partial payments consume bounded sub-obligations; agent resubmission through a different portal is still correlated to the same approved invoice.¶

Text-Only Conditional Workflow and Explicit YES/NO Outcomes.¶

• E-63 / YES at authorization collection: PED-1 has independently authenticated the applicable payer/issuer/custodian/mandate authority, bounded its intended effect, and stored protected identity and use state; only then place this candidate in Non-Effective State for actual-operation inspection. NO: reject without providing an effective token, signature, payment instruction or release.¶

• E-63 / YES at native reconstruction and equality: PED-2, at the relevant protected boundary, obtains the true native payload and verifies that buyer approval, invoice and PO identifiers, supplier legal identity, final bank payee, amount/tax/discount, current ERP state, and payment-route correlation agree. NO, including missing or contradictory effect-critical fields: DENY; a display summary, receipt from another domain or earlier approval does not override the discrepancy.¶

• E-63 / NO at any security or business predicate: if supplier-portal bank details change, invoice was previously paid, two rails race, or final payee differs from independently approved details, do not effectuate the candidate. An unsupported effect path must be explicitly excluded or made subject to an equivalent enforceable guard; do not infer that a gateway can block independent signers or contract execution.¶

• E-63 / YES at current-state and effectuation decision: after fresh policy and revocation checks, sink/nonce/lineage checks, budget and concurrency-safe reservation or consumption, and other conditions of this profile all pass, allow only the particular bounded native effect at its controlled sink; record the protected transition and independently observed evidence.¶

• E-63 / OUTCOME_UNKNOWN, PARTIAL_EFFECT, PROVISIONAL or INDETERMINATE: where confirmation cannot establish external nonexecution or completion, fence the invoice across rails on unknown payment outcome and reconcile buyer-bank/card records before another payment. Do not convert a timeout into proof that a remote effect never happened; no unconditional retry or refund-capacity restoration.¶

• E-63 / Completion: report VERIFIED/SETTLED only to the precise extent supported by authentic evidence for that separate effect. A new economic consequence, compensation, different rail or newly authorized billing period requires a separate verified act and, where applicable, new authority.¶

Required protection invariants.¶

• An authenticated supplier portal cannot expand buyer payment authority or replace the final beneficiary without approved supplier-master change.¶

• A single invoice cannot be settled twice through bank and card rails using the same obligation.¶

• A displayed portal success message is not proof of bank clearing or supplier receipt.¶

Illustrative adversarial scenarios.¶

• Portal injects a different bank account in a valid invoice view.¶

• Two agents process the same payable using different rails.¶

• A supplier modifies tax and fees after the enterprise approver signed off.¶

Alternative implementations.¶

• ERP-integrated payment execution adapter.¶

• Virtual-card issuance/capture service with invoice-bound token.¶

• Bank payment gateway with verified supplier-master and exclusive transfer credentials.¶

Failure, reconciliation and limits. Unknown payment status causes invoice-level spend fencing across all routes. Reconciliation uses authoritative buyer-bank/card and supplier evidence; manual dispute creates a distinct authorized correction.¶

Proposed negative-effect conformance vectors. supplier_account_swap, invoice_duplicate_rails, tax_amount_change, portal_confirmation_spoof, po_line_item_mismatch, payment_ack_unknown. Each vector should assert the absence of any unauthorized actual effect at the named protected sink, not merely a denied API return.¶

Related enforcement points: see Section 12 (entries citing E-63).¶

A.1. EN-CW: Native data schema, security boundary and state contract

Boundary ownership: PED-1 verifies source authority independently of the untrusted financial agent. PED-2 observes the actual native transaction or device state at the last controlled interface. The Finality Sink must alone control a usable signing output, actual debit command, card capture, trade order admission, ledger mint/transfer call or secure-element value release for the specifically claimed paths. A direct uncontrolled signing key or bank backchannel removes that path from the assurance perimeter.¶

The per-profile algorithms below identify a concrete native parser, protected state predicate and sink-authorized mutation. Function names such as verified_quote_signature, parse_strict and secure_element_attestation designate actual cryptographic, schema-validated or secure-hardware operations supplied by the deploying implementation; none may be replaced with an untrusted Boolean reported by the agent. External systems require authenticated evidence adapters, and non-cooperating settlement legs cannot be coerced into true global atomic commit.¶

Protected record: obligation_id is immutable and globally unambiguous in the selected administrative namespace; typed debit/credit use integer minor units and explicit currency exponent; source and target accounts and token-contract/network pairs are distinct identifiers; critical extension flags are mandatory-parse; policy_generation and revocation_generation are independently authenticated by the sink. EH contains an opaque protected state reference rather than an unrestricted transferable spend capability.¶

Serialization: encode domain-separated typed fields with unambiguous length and field presence; reject duplicate keys, unknown critical extensions, inconsistent decimal scales, confusable merchant identifiers, unchecked nested calls, reserialized recipients and a final native digest that changes after the protected comparison. Canonicalization never substitutes display labels for issuer-resolved legal or ledger identities.¶

Storage: transactions that modify local budget reservations and nonce consumption must provide serializable conflict detection or an equivalent protected compare-and-swap. If multiple stores or independently controlled financial rails are used, each sink consumes its own reservation and reports typed evidence; do not falsely assert cross-rail atomicity. Crashes between durable local commitment and the external effect produce OUTCOME_UNKNOWN until authoritative evidence establishes whether the effect occurred.¶

Eligibility: effect release requires valid FOR provenance, permitted financial effect under typed comparison, valid lineage, unexpired authority, current policy/revocation version, available budget, unused operation ID, actual sink identity, and absence of an unmediated alternative route within the asserted coverage. Unknown critical state results in DENY or a non-effective INDETERMINATE state.¶

Test oracle: observe the actual protected signer, account mutation function, card-capture dispatcher, order-admission API, ledger contract execution, hardware value decrement or settlement switch. A negative test is only successful if the prohibited effect count is zero at all actually mediated paths; an API-level error alone is not evidence of enforcement.¶

{
  "schema_version": 1,
  "domain": "PTEF-FIN-FOR-v1",
  "obligation_id": "obl-001",
  "principal": "authenticated-principal-id",
  "root_authority_digest": "SHA-256-OF-AUTHENTICATED-MANDATE",
  "allowed_sink_ids": [
    "signer-1"
  ],
  "payer": "payer-account-identifier",
  "payee_constraint": {
    "identity": "merchant-public-id",
    "acceptable_alias_epoch": 4
  },
  "asset": {
    "kind": "ISO4217-or-token",
    "asset_id": "USD",
    "network_id": "bank-rail-1",
    "decimal_exponent": 2
  },
  "amounts": {
    "max_debit_minor": 10000,
    "min_credit_minor": 9700,
    "max_fee_minor": 100
  },
  "policy_generation": 7,
  "revocation_generation": 12,
  "expiry_utc": "2026-11-30T23:59:59Z",
  "usage_budget": {
    "max_uses": 1,
    "max_aggregate_debit_minor": 10000
  },
  "critical_fields": [
    "payee_constraint",
    "asset",
    "amounts",
    "allowed_sink_ids"
  ]
}

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function PROTECTED_FINANCIAL_EFFECT(for_id, final_native, sink, prot\
\ected_state):
    authority = PED_1_PROTECTED_LOAD(for_id)
    REQUIRE authenticated(authority) and authoritative_lineage(autho\
\rity)
    REQUIRE sink in authority.allowed_sinks and sink.controls_effect\
\ive_path
    actual = PED_2_PARSE_FINAL_NATIVE(sink, final_native)
    REQUIRE exact_schema_supported(actual) and no_unrecognized_criti\
\cal_fields(actual)
    REQUIRE current_policy(authority) and current_revocation(authori\
\ty)
    REQUIRE actual_is_authorized_economic_effect(actual, authority)
    REQUIRE all_transformation_edges_authorized(actual, authority)
    WITH protected_serializable_transaction(sink, authority.obligati\
\on_id):
        REQUIRE not already_consumed(actual.operation_id)
        REQUIRE debit_plus_reserved_plus_new <= bounded_budget(autho\
\rity)
        reserve_native_effect_id(actual); consume_authority_use(actu\
\al)
        persist_effect_preparation(actual, sink, ledger_epoch)
    result = EXCLUSIVE_RELEASE_ONCE(sink, final_native)
    # The database commit above does not make the remote rail atomic.
    if independently_authenticated_confirmation(result):
        persist_typed_result(result)  # never claim unproven settlem\
\ent
    else:
        mark_OUTCOME_UNKNOWN_and_fence_retry(actual.operation_id)
    return typed_result_or_unknown(result)

A.2. Implementation Detail for E-45: Agent-paid resource / merchant challenge

Native reconstructed inputs: quote signature; merchant public key; resource digest; price minor units; currency; facilitator identifier; service-order identifier. Consequential effect is first possible at the credential-protected payment signer or acquiring switch; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (mandate,correlation_id,payment_attempt,entitlement_status). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind merchant/resource and 200-unit ceiling. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Obtain signed resource payment challenge. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Reconstruct final merchant, quote and fee. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check amount, beneficiary and correlation ID. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume payment use and release once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Observe independent service-entitlement proof. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: resource price, beneficiary and merchant key remain within the exact mandate.¶

Worked input, threat and required result: Authorize 200 minor units for API resource R7 and merchant key K7. A challenge for 205 minor units is DENY before payment signing; a legitimate 200-unit release may enter PAYMENT_OUTCOME_UNKNOWN without asserting delivery.¶

Failure and outcome reconciliation: Payment response timeout freezes original payment ID; query payment status and verify delivery independently.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE verified_quote_signature(quote, merchant_pubkey)
REQUIRE quote.resource_digest == mandate.resource_digest
REQUIRE quote.merchant_key == mandate.merchant_key
REQUIRE quote.total_minor == quote.price_minor + quote.fee_minor
REQUIRE quote.total_minor <= mandate.max_debit_minor
REQUIRE quote.asset_id in mandate.allowed_assets
key = (mandate.obligation_id, quote.resource_id, quote.attempt_id)
ATOMIC: ASSERT key not in used_attempts; ADD key; RESERVE quote.tota\
\l_minor
SINK_SIGN_AND_DISPATCH(quote.native_payment_bytes)
IF payment_ack_unknown: FENCE key; QUERY payment_id; DO_NOT_RECHARGE
REQUIRE separate_signed_delivery_evidence before marking SERVICE_DEL\
\IVERED

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E45_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "quote signature; merch\
\ant public key; resource digest; price minor units; currency; facil\
\itator identifier; service-order identifier")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("resource price, beneficiary and mercha\
\nt key remain within the exact mandate", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-45-01 -- changed_quoted_amount

Injection: Introduce the named changed_quoted_amount perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite changed_quoted_amount; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-45-02 -- merchant_key_substitution

Injection: Introduce the named merchant_key_substitution perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite merchant_key_substitution; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-45-03 -- facilitator_replay

Injection: Introduce the named facilitator_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite facilitator_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-45-04 -- expired_service_quote

Injection: Introduce the named expired_service_quote perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite expired_service_quote; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-45-05 -- fee_unit_rounding

Injection: Introduce the named fee_unit_rounding perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite fee_unit_rounding; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-45-06 -- paid_but_no_service

Injection: Introduce the named paid_but_no_service perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-45 to verify the protected state and sink-released effects comply with the authorized exact operation despite paid_but_no_service; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual credential-protected payment signer or acquiring switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.3. Implementation Detail for E-46: Network-card partial capture

Native reconstructed inputs: scheme authorization reference; card-token generation; merchant identifier; capture sequence; currency; amount; original authorization ID. Consequential effect is first possible at the issuer/acquirer capture-dispatch interface; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (auth_ref,approved_amount,captured_total,active_capture_reservations,capture_ids). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind approved merchant and aggregate limit. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Read final native capture message. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Match authorization lineage and card token. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Serialize captured plus reserved amount. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume capture ID and release once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile clearing, hold and reversal independently. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: captured + reserved must never exceed authorized total plus verified increments.¶

Worked input, threat and required result: Approve 10,000 minor units. Two workers attempt captures of 7,000 and 5,000. A serializable reservation admits at most 10,000 combined; the second 5,000 capture is denied or reduced only by new approval.¶

Failure and outcome reconciliation: Lost capture ACK retains reservation and used capture ID until independently confirmed not processed.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE native_capture.auth_ref == original_auth.auth_ref
REQUIRE native_capture.merchant_id == original_auth.merchant_id
REQUIRE native_capture.currency == original_auth.currency
REQUIRE native_capture.token_generation == original_auth.token_gener\
\ation
ATOMIC_WITH_LOCK(original_auth.auth_ref):
    cap = original_auth.limit_minor + verified_increments_minor
    outstanding = cleared_capture_minor + reserved_capture_minor
    REQUIRE 0 < native_capture.amount_minor <= cap - outstanding
    REQUIRE native_capture.capture_id not in spent_capture_ids
    ADD spent_capture_ids[native_capture.capture_id]
    reserved_capture_minor += native_capture.amount_minor
SINK_DISPATCH_CAPTURE(native_capture)
ON_TIMEOUT: KEEP reserve, QUERY ORIGINAL CAPTURE_ID before any new d\
\ispatch

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E46_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "scheme authorization r\
\eference; card-token generation; merchant identifier; capture seque\
\nce; currency; amount; original authorization ID")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("captured + reserved must never exceed \
\authorized total plus verified increments", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-46-01 -- dual_partial_capture

Injection: Introduce the named dual_partial_capture perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite dual_partial_capture; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-46-02 -- over_capture

Injection: Introduce the named over_capture perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite over_capture; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-46-03 -- merchant_changed_after_auth

Injection: Introduce the named merchant_changed_after_auth perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite merchant_changed_after_auth; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-46-04 -- increment_without_authority

Injection: Introduce the named increment_without_authority perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite increment_without_authority; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-46-05 -- capture_ack_lost

Injection: Introduce the named capture_ack_lost perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite capture_ack_lost; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-46-06 -- refund_as_new_spend

Injection: Introduce the named refund_as_new_spend perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-46 to verify the protected state and sink-released effects comply with the authorized exact operation despite refund_as_new_spend; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer capture-dispatch interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.4. Implementation Detail for E-47: Cross-rail and foreign-exchange equivalence

Native reconstructed inputs: source asset, payee identity, quote source, exchange ratio, maximum debit, minimum credit, fees and settlement route. Consequential effect is first possible at the bank transfer switch, card processor, or ledger transfer gate for each leg; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (root_obligation,transform_edges,quoted_rate_id,leg_reservations,leg_results). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind source debit and target credit bounds. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Select available card/bank/token payment route. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Record signed conversion and beneficiary edges. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Recompute final debit, credit and fee. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Commit each protected leg reservation. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Observe independent rail settlement evidence. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: no authorized route change may increase debit, reduce credit or alter beneficiary outside bounded transformations.¶

Worked input, threat and required result: Approve debit <=10,050 cents and credit >=9,900 target minor units with fee <=100 cents. A route producing 9,850 target units fails even when the source debit remains inside the ceiling.¶

Failure and outcome reconciliation: If source leg settles while target leg is unknown, mark PARTIAL_EFFECT; prohibit a fresh debit without new authority.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE all edge pairs (source_asset,target_asset,rail_id) in allowe\
\d graph
FOR edge IN actual_conversion_graph IN EXECUTION_ORDER:
    REQUIRE signature_or_authoritative_feed(edge.quote_id, edge.rate\
\_num, edge.rate_den)
    REQUIRE edge.rate_den > 0 and edge.rate_num > 0
    REQUIRE defined_integer_rounding(edge.input_minor, rate, output_\
\exponent)
    REQUIRE edge.output_minor == verified_rounded_value(edge)
    REQUIRE edge.beneficiary == authorized_beneficiary_at_this_edge
REQUIRE final_debit_minor <= mandate.max_debit_minor
REQUIRE final_credit_minor >= mandate.min_credit_minor
REQUIRE total_fees_minor <= mandate.max_fee_minor
RESERVE_AND_CONSUME independently in each actually controlled rail
IF any leg external result is ambiguous: mark PARTIAL_EFFECT_OR_UNKN\
\OWN; NO_NEW_DEBIT

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E47_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "source asset, payee id\
\entity, quote source, exchange ratio, maximum debit, minimum credit\
\, fees and settlement route")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("no authorized route change may increas\
\e debit, reduce credit or alter beneficiary outside bounded transfo\
\rmations", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-47-01 -- fee_third_asset

Injection: Introduce the named fee_third_asset perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite fee_third_asset; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-47-02 -- fx_quote_stale

Injection: Introduce the named fx_quote_stale perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite fx_quote_stale; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-47-03 -- switch_rail_unapproved

Injection: Introduce the named switch_rail_unapproved perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite switch_rail_unapproved; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-47-04 -- recipient_alias_changed

Injection: Introduce the named recipient_alias_changed perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite recipient_alias_changed; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-47-05 -- swap_slippage_above_bound

Injection: Introduce the named swap_slippage_above_bound perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite swap_slippage_above_bound; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-47-06 -- partial_rail_commit

Injection: Introduce the named partial_rail_commit perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-47 to verify the protected state and sink-released effects comply with the authorized exact operation despite partial_rail_commit; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank transfer switch, card processor, or ledger transfer gate for each leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.5. Implementation Detail for E-48: Tokenized deposit / reserve-backed obligation

Native reconstructed inputs: deposit liability ID; bank issuer; reserve funding reference; token owner; mint/transfer/redeem amount; settlement epoch. Consequential effect is first possible at the deposit-core mutation gate and token ledger method gate; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (liability_id,issued_supply,reserved_redeem,reserve_evidence_generation,ledger_event). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind liability and authorized deposit account. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Confirm protected bank-core obligation evidence. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Check mint/redeem command at ledger sink. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Atomically reserve liability generation. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Release permitted token effect once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Confirm bank settlement separately from token record. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: each tokenized obligation maps to independently evidenced liability/reserve status without double encumbrance.¶

Worked input, threat and required result: Bank core proves one liability unit of 1,000. A second concurrent token mint against the same unspent liability generation must fail, even with syntactically valid ledger instructions.¶

Failure and outcome reconciliation: Token event confirmation alone does not upgrade reserve-settlement evidence.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE bank_liability_attestation.issuer_id == authorized_issuer
REQUIRE bank_liability_attestation.account == authorized_deposit
REQUIRE bank_liability_attestation.generation is current and unspent
REQUIRE native_token_call.contract_id == authorized_contract
REQUIRE native_token_call.action in {MINT,BURN,TRANSFER,REDEEM}
REQUIRE amount_minor <= independently_verified_unencumbered_liability
ATOMIC(bank_core): RESERVE liability_id, liability_generation, amoun\
\t_minor
ATOMIC(token_gate): CONSUME mint_or_redeem_nonce; release native act\
\ion
EMIT token_event and bank_settlement_status AS SEPARATE typed records
IF bank evidence absent after ledger event: SET OUTCOME_UNKNOWN; DO \
\NOT ASSUME RESERVE_SETTLED

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E48_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "deposit liability ID; \
\bank issuer; reserve funding reference; token owner; mint/transfer/\
\redeem amount; settlement epoch")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("each tokenized obligation maps to inde\
\pendently evidenced liability/reserve status without double encumbr\
\ance", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-48-01 -- issuer_substitution

Injection: Introduce the named issuer_substitution perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite issuer_substitution; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-48-02 -- liability_not_posted

Injection: Introduce the named liability_not_posted perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite liability_not_posted; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-48-03 -- double_redemption

Injection: Introduce the named double_redemption perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite double_redemption; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-48-04 -- ledger_only_receipt

Injection: Introduce the named ledger_only_receipt perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite ledger_only_receipt; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-48-05 -- stale_reserve_state

Injection: Introduce the named stale_reserve_state perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite stale_reserve_state; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-48-06 -- interbank_partial_failure

Injection: Introduce the named interbank_partial_failure perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-48 to verify the protected state and sink-released effects comply with the authorized exact operation despite interbank_partial_failure; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual deposit-core mutation gate and token ledger method gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.6. Implementation Detail for E-49: Offline CBDC protected device transfer

Native reconstructed inputs: device public identity; offline purse ID; value units; epoch; monotonic spend counter; per-recipient transfer commitment. Consequential effect is first possible at the tamper-resistant device value-release controller; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (device_id,epoch,available_offline_value,counter,spent_serials,sync_status). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Provision bounded offline value and device epoch. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Authenticate recipient and native device request. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Read protected balance and monotonic counter. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Commit serial and subtract value in secure device. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Release locally verifiable transfer evidence. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile on reconnect; quarantine conflicts. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: device-local total consumption never exceeds provisioned balance within enforced hardware trust model.¶

Worked input, threat and required result: An offline purse has 50 value units. A signed transfer of 30 reduces protected balance to 20. A cloned rollback attempting another 30 from the same counter/epoch is rejected if hardware rollback assumptions hold.¶

Failure and outcome reconciliation: On reconnect detect duplicate serials and forked epochs; quarantine and reconcile without claiming perfect offline global prevention.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

REQUIRE secure_element_attestation(device_id,firmware_policy,epoch)
REQUIRE recipient_challenge signature and permitted offline scope
SECURE_DEVICE_ATOMIC:
    REQUIRE secure_counter == expected_counter and not revoked_epoch
    REQUIRE payment_serial not in protected_spent_serials
    REQUIRE transfer_units > 0 and available_value >= transfer_units
    INSERT payment_serial in protected_spent_serials
    available_value -= transfer_units; secure_counter += 1
    PERSIST anti_rollback_state BEFORE releasing value evidence
RETURN device_signed_transfer_evidence(serial, epoch, counter)
ON_RECONNECT: CHECK serial_collision, counter_rollback, epoch_fork
ON_CONFLICT: QUARANTINE; NO_NEW_OFFLINE_VALUE without re-provisioning

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E49_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "device public identity\
\; offline purse ID; value units; epoch; monotonic spend counter; pe\
\r-recipient transfer commitment")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("device-local total consumption never e\
\xceeds provisioned balance within enforced hardware trust model", n\
\ative, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-49-01 -- snapshot_rollback

Injection: Introduce the named snapshot_rollback perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite snapshot_rollback; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-49-02 -- same_token_twice

Injection: Introduce the named same_token_twice perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite same_token_twice; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-49-03 -- epoch_reuse

Injection: Introduce the named epoch_reuse perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite epoch_reuse; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-49-04 -- terminal_challenge_relay

Injection: Introduce the named terminal_challenge_relay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite terminal_challenge_relay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-49-05 -- offline_budget_exceeded

Injection: Introduce the named offline_budget_exceeded perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite offline_budget_exceeded; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-49-06 -- conflicting_reconnect_history

Injection: Introduce the named conflicting_reconnect_history perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-49 to verify the protected state and sink-released effects comply with the authorized exact operation despite conflicting_reconnect_history; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual tamper-resistant device value-release controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.7. Implementation Detail for E-50: Payment-versus-payment conditional cross-currency release

Native reconstructed inputs: two currency leg IDs; locked funds; counterparties; expiry; hashlock or protected settlement commitments; amount precision. Consequential effect is first possible at the one controlled settlement interface per currency leg; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (group_id,leg_A_state,leg_B_state,release_proofs,timeout_fence). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind bilateral trade and exchange quantities. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Prepare funded/escrowed currency A leg. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Prepare funded/escrowed currency B leg. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Verify compatible protected release conditions. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Release each controllable leg under commitment. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Observe finality of both legs separately. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: prepared must not be represented as settled and each irreversible release requires bounded cooperative conditions.¶

Worked input, threat and required result: Trade 100 currency-A units against 92 currency-B units. A prepared but unfunded B leg does not permit the A leg to be released; any partially effective leg is recorded as PARTIAL_EFFECT.¶

Failure and outcome reconciliation: Partial effect enters incident/reconciliation path; never assume universal global atomicity.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE leg_A and leg_B bind exact trade_id, counterparties, currenc\
\ies, amounts
REQUIRE both source funds in enforceable prepared or escrowed states
REQUIRE commitment proofs authenticate leg_A and leg_B sink instance\
\ IDs
REQUIRE release predicates and expiry windows compatible
FOR leg IN {A,B}: verify protected nonce and available reserved bala\
\nce
ONLY_IF cooperative settlement primitive actually prevents unilatera\
\l escape:
    release each leg under prescribed protocol, retaining per-leg ev\
\idence
OTHERWISE: release only bounded controlled leg and expose PARTIAL_EF\
\FECT possibility
IF any participant finality missing: GROUP_STATE=UNKNOWN_OR_PARTIAL
NEVER claim SETTLED(group) until each required leg has authentic evi\
\dence

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E50_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "two currency leg IDs; \
\locked funds; counterparties; expiry; hashlock or protected settlem\
\ent commitments; amount precision")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("prepared must not be represented as se\
\ttled and each irreversible release requires bounded cooperative co\
\nditions", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-50-01 -- leg_beneficiary_substitution

Injection: Introduce the named leg_beneficiary_substitution perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite leg_beneficiary_substitution; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-50-02 -- quote_mismatch

Injection: Introduce the named quote_mismatch perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite quote_mismatch; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-50-03 -- coordinator_replay

Injection: Introduce the named coordinator_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite coordinator_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-50-04 -- first_leg_only

Injection: Introduce the named first_leg_only perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite first_leg_only; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-50-05 -- commit_timeout

Injection: Introduce the named commit_timeout perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite commit_timeout; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-50-06 -- missing_final_settlement_proof

Injection: Introduce the named missing_final_settlement_proof perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-50 to verify the protected state and sink-released effects comply with the authorized exact operation despite missing_final_settlement_proof; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual one controlled settlement interface per currency leg and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.8. Implementation Detail for E-51: Delivery-versus-payment of tokenized securities

Native reconstructed inputs: security issue ID; verified beneficial owner; quantity; encumbrance status; payment asset and amount; transfer restriction epoch. Consequential effect is first possible at the securities-title transfer gate and payment finality gate; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (trade_id,asset_lock,payment_lock,encumbrance_generation,delivery_evidence,payment_evidence). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind asset issue, ownership and payment. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Obtain updated title and encumbrance state. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Reserve transferable asset units. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Reserve payment leg under separate sink. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Condition each release on accepted commitments. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile ownership and funds after both legs. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: an encumbered or wrong-series security cannot be delivered merely because a matching ticker is displayed.¶

Worked input, threat and required result: Payment has been prepared but securities become encumbered after approval. The native title-transfer gate detects the new encumbrance generation and withholds delivery.¶

Failure and outcome reconciliation: Unmatched custody records or failed payment are PARTIAL_EFFECT/UNKNOWN until independently reconciled.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE security_issue_id, quantity, owner_id match title mandate
REQUIRE transfer restrictions permit proposed recipient
REQUIRE current title-registry owner proof and encumbrance_generation
REQUIRE unencumbered transferable_quantity >= proposed quantity
RESERVE title quantity at securities sink
RESERVE exact payment asset/amount independently at payment sink
RELEASE ONLY when actual cooperative delivery/payment conditions met
REQUIRE title ownership evidence and payment finality evidence separ\
\ately
IF one leg uncertain: GROUP_STATE=PARTIAL_EFFECT; prohibit duplicate\
\ releases

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E51_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "security issue ID; ver\
\ified beneficial owner; quantity; encumbrance status; payment asset\
\ and amount; transfer restriction epoch")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("an encumbered or wrong-series security\
\ cannot be delivered merely because a matching ticker is displayed"\
\, native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-51-01 -- wrong_asset_series

Injection: Introduce the named wrong_asset_series perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite wrong_asset_series; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-51-02 -- encumbered_units

Injection: Introduce the named encumbered_units perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite encumbered_units; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-51-03 -- seller_not_owner

Injection: Introduce the named seller_not_owner perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite seller_not_owner; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-51-04 -- cash_asset_partial

Injection: Introduce the named cash_asset_partial perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite cash_asset_partial; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-51-05 -- issuer_freeze_change

Injection: Introduce the named issuer_freeze_change perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite issuer_freeze_change; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-51-06 -- fake_registry_receipt

Injection: Introduce the named fake_registry_receipt perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-51 to verify the protected state and sink-released effects comply with the authorized exact operation despite fake_registry_receipt; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual securities-title transfer gate and payment finality gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.9. Implementation Detail for E-52: Stablecoin mint, burn, reserve and redemption

Native reconstructed inputs: issuer identity; token contract and version; redeem request; eligible bank funding evidence; reserve liability ID; quantity. Consequential effect is first possible at the privileged mint/burn key and redemption bank-transfer controller; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (issuer_epoch,liability_budget,minted_supply,burned_units,redemption_refs). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind issuance/redemption and reserve reference. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Reconstruct final mint/burn call data. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Validate reserve evidence and issuer epoch. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Serialize supply and liability reservation. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume issuance/redemption authorization once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Verify redemption banking outcome independently. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: issuer-approved mint amount is bounded by authenticated unconsumed funding evidence and protected supply state.¶

Worked input, threat and required result: Authenticated bank credit supports mint of 500 units. Two simultaneous mint workers cannot each issue 500 against the same single-use bank credit reference.¶

Failure and outcome reconciliation: A burn transaction is not proof that external fiat redemption completed; retain separate statuses.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE native_method in {mint,burn,redeem}
REQUIRE current approved issuer key and non-upgraded token contract \
\implementation
IF method == mint:
    REQUIRE independently_authenticated_bank_funding_reference
    REQUIRE reserve_generation current AND funding_reference unspent
    ATOMIC: MARK funding_reference consumed; INCREASE reserved_issua\
\nce
IF method == redeem:
    REQUIRE verified token-burn evidence and previously unredeemed r\
\edemption_id
    ATOMIC: RESERVE bank payout using redemption_id
AT_SINK: verify exact native amount, supply delta and recipient; rel\
\ease once
CLASSIFY on-chain event and bank redemption finality as separate evi\
\dence

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E52_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "issuer identity; token\
\ contract and version; redeem request; eligible bank funding eviden\
\ce; reserve liability ID; quantity")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("issuer-approved mint amount is bounded\
\ by authenticated unconsumed funding evidence and protected supply \
\state", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-52-01 -- mint_cap_race

Injection: Introduce the named mint_cap_race perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite mint_cap_race; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-52-02 -- stale_reserve_attestation

Injection: Introduce the named stale_reserve_attestation perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite stale_reserve_attestation; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-52-03 -- wrong_token_contract

Injection: Introduce the named wrong_token_contract perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite wrong_token_contract; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-52-04 -- burn_proof_replay

Injection: Introduce the named burn_proof_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite burn_proof_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-52-05 -- payout_unknown

Injection: Introduce the named payout_unknown perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite payout_unknown; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-52-06 -- decimal_scale_change

Injection: Introduce the named decimal_scale_change perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-52 to verify the protected state and sink-released effects comply with the authorized exact operation despite decimal_scale_change; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual privileged mint/burn key and redemption bank-transfer controller and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.10. Implementation Detail for E-53: Cross-chain bridge and rollup reorganization

Native reconstructed inputs: source chain ID and block checkpoint; source event ID; bridge message ID; target chain ID; recipient; issuance amount; finality rule. Consequential effect is first possible at the bridge relayer authorization and destination mint/release contract; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (source_event,checkpoint,challenge_period,consumed_message_ids,destination_release). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind source lock and destination mint obligation. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Independently validate source event and chain ID. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Enforce challenge period / finality threshold. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check message nonce, recipient and amount. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume destination release identity once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Monitor reorganization and finality evidence. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: no destination mint on unverified source event or on reused bridge message identifier.¶

Worked input, threat and required result: A source-chain lock appears in a block that later reorganizes. Destination release is withheld until the configured finality rule has been independently satisfied; replayed message IDs remain rejected.¶

Failure and outcome reconciliation: Reorganizations before threshold block release; post-release failure cannot be undone by falsely marking the effect unexecuted.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE source_chain_id, destination_chain_id bound to bridge obliga\
\tion
REQUIRE source_deposit_proof includes exact event, recipient and amo\
\unt
REQUIRE independently_validated_source_consensus_checkpoint
REQUIRE source_checkpoint satisfies configured finality/challenge ru\
\le
REQUIRE bridge_message_id unique in destination protected used set
REQUIRE destination_mint.amount == source_obligation.amount after al\
\lowed fees
ATOMIC(destination_contract): CONSUME message_id and authorize desti\
\nation transfer
ON_SOURCE_REORG before finality: DO_NOT_MINT
AFTER_DESTINATION_EFFECT: never erase evidence or replay due to late\
\r reorg

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E53_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "source chain ID and bl\
\ock checkpoint; source event ID; bridge message ID; target chain ID\
\; recipient; issuance amount; finality rule")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("no destination mint on unverified sour\
\ce event or on reused bridge message identifier", native, sink_stat\
\e)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-53-01 -- source_reorg

Injection: Introduce the named source_reorg perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite source_reorg; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-53-02 -- bridge_message_replay

Injection: Introduce the named bridge_message_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite bridge_message_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-53-03 -- recipient_replaced

Injection: Introduce the named recipient_replaced perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite recipient_replaced; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-53-04 -- contract_upgrade

Injection: Introduce the named contract_upgrade perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite contract_upgrade; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-53-05 -- insufficient_confirmations

Injection: Introduce the named insufficient_confirmations perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite insufficient_confirmations; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-53-06 -- asset_mapping_substitution

Injection: Introduce the named asset_mapping_substitution perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-53 to verify the protected state and sink-released effects comply with the authorized exact operation despite asset_mapping_substitution; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bridge relayer authorization and destination mint/release contract and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.11. Implementation Detail for E-54: Exchange custody treasury withdrawal

Native reconstructed inputs: customer/treasury account; asset contract; withdrawal address; chain; compliance generation; quorum and hot/cold key authority. Consequential effect is first possible at the exclusive HSM/MPC signing threshold and withdrawal dispatch; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (withdrawal_id,account_balance,withdrawal_reservations,address_epoch,key_quorum,tx_status). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind withdrawal mandate and approved destination. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Reserve available custodied balance. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Reconstruct actual chain transaction and fee. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Verify quorum, address, asset and policy epoch. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Release threshold signature and mark use. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Track broadcast, inclusion and finality separately. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: no key share, raw signature or hot-wallet alternate can release an in-scope changed withdrawal.¶

Worked input, threat and required result: Treasury mandate permits 5 BTC to address A. A valid MPC signing session for address B is denied when final raw transaction bytes do not match approved beneficiary.¶

Failure and outcome reconciliation: If broadcast ACK lost, hold reservation and query txid; never sign replacement using same permit.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE withdrawal account, asset contract, chain and beneficiary ma\
\tch FOR
REQUIRE native_unsigned_tx parsed from actual serialized signing pre\
\image
REQUIRE native_tx.fee_minor <= approved_fee_ceiling
REQUIRE key_session.quorum_id and policy_generation current
REQUIRE all independently effective backup/raw-signing methods media\
\ted
ATOMIC custody_ledger: RESERVE customer asset and CONSUME withdrawal\
\ ID
SIGN ONLY through restricted native-transaction-aware key API
ON broadcast timeout: retain SPENT and OUTCOME_UNKNOWN
RECONCILE via chain-specific txid and required finality evidence; ne\
\ver blind-resign

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E54_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "customer/treasury acco\
\unt; asset contract; withdrawal address; chain; compliance generati\
\on; quorum and hot/cold key authority")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("no key share, raw signature or hot-wal\
\let alternate can release an in-scope changed withdrawal", native, \
\sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-54-01 -- withdrawal_destination_swap

Injection: Introduce the named withdrawal_destination_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite withdrawal_destination_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-54-02 -- mpc_quorum_conflict

Injection: Introduce the named mpc_quorum_conflict perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite mpc_quorum_conflict; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-54-03 -- hot_wallet_bypass

Injection: Introduce the named hot_wallet_bypass perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite hot_wallet_bypass; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-54-04 -- daily_limit_race

Injection: Introduce the named daily_limit_race perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite daily_limit_race; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-54-05 -- chain_id_change

Injection: Introduce the named chain_id_change perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite chain_id_change; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-54-06 -- signature_status_unknown

Injection: Introduce the named signature_status_unknown perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-54 to verify the protected state and sink-released effects comply with the authorized exact operation despite signature_status_unknown; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exclusive HSM/MPC signing threshold and withdrawal dispatch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.12. Implementation Detail for E-55: Payment alias, QR and merchant identity resolution

Native reconstructed inputs: alias/QR data; verified legal or scheme merchant identity; payee account; alias-resolution epoch; applicable payee policy. Consequential effect is first possible at the final bank transfer or token-payment instruction gate; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (mandate,alias_version,merchant_key,payee_resolution,spent_nonce). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind known merchant identity and alias constraints. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Resolve alias using trusted scheme directory. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Read terminal beneficiary account and timestamp. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Compare final identity and resolution epoch. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume authority only for matching beneficiary. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Record actual bank or ledger effect status. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: a friendly display name or stale alias-cache entry cannot substitute for beneficiary identity evidence.¶

Worked input, threat and required result: A displayed trusted QR label resolves to account A at approval, then to B at execution. Unless B is explicitly within the original bounded identity rule, the bank transfer is denied.¶

Failure and outcome reconciliation: When directory unavailable or ambiguous, hold candidate non-effective.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE authenticated_alias_directory response binds alias and schem\
\e namespace
REQUIRE merchant legal/scheme identity == original eligible merchant
REQUIRE alias_record.epoch current and active at final use
REQUIRE final_native.recipient_account == verified_directory.account
REQUIRE QR encoded amount and currency match protected mandate
REQUIRE no unparsed critical payee redirect fields in native message
ATOMIC: CONSUME (mandate_id, resolved_payee, payment_id) and reserve\
\ debit
SINK_SEND exact parsed transfer bytes to verified beneficiary
IF directory stale/unavailable: DENY_OR_HOLD_NES; do not trust displ\
\ay label

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E55_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "alias/QR data; verifie\
\d legal or scheme merchant identity; payee account; alias-resolutio\
\n epoch; applicable payee policy")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("a friendly display name or stale alias\
\-cache entry cannot substitute for beneficiary identity evidence", \
\native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-55-01 -- qr_payee_swap

Injection: Introduce the named qr_payee_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite qr_payee_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-55-02 -- alias_resolution_race

Injection: Introduce the named alias_resolution_race perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite alias_resolution_race; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-55-03 -- merchant_registry_rollback

Injection: Introduce the named merchant_registry_rollback perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite merchant_registry_rollback; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-55-04 -- terminal_swap

Injection: Introduce the named terminal_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite terminal_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-55-05 -- old_resolution_replay

Injection: Introduce the named old_resolution_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite old_resolution_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-55-06 -- merchant_label_confusable

Injection: Introduce the named merchant_label_confusable perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-55 to verify the protected state and sink-released effects comply with the authorized exact operation despite merchant_label_confusable; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual final bank transfer or token-payment instruction gate and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.13. Implementation Detail for E-56: Machine usage-metered micropayment batching

Native reconstructed inputs: resource meter identity; signed usage intervals; rate/tier; payer account; max accrued budget; batch boundary. Consequential effect is first possible at the payment-channel settlement or gateway debit interface; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (meter_epoch,interval_ids,accrued_debit,reserved_debit,settled_batch_ids). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind meter and authorized maximum unit rate. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Authenticate independent usage interval records. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Deduplicate interval IDs and compute charge. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Reserve aggregate payer budget atomically. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Release only verified batch settlement. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile paid intervals and service delivery. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: billed usage intervals are unique and total debit is bound to authenticated metering evidence.¶

Worked input, threat and required result: Meter reports 3, 4, 5 units of usage. Replay of a signed 4-unit interval cannot increase accrued charge twice; an unauthorized 13-unit batch against 12-unit cap is denied.¶

Failure and outcome reconciliation: Unconfirmed settlement locks the corresponding interval set against rebilling.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE signed_meter_public_key is bound to authorized resource
FOR reading IN usage_interval_records:
    REQUIRE reading.meter_epoch current and signed interval authentic
    REQUIRE interval ID not previously included in any active/settle\
\d batch
    unit_charge = exact_integer_tariff(reading.usage_units, tariff_v\
\ersion)
    running_charge_minor += unit_charge
REQUIRE running_charge_minor <= current period remaining budget
ATOMIC: RESERVE running_charge and MARK interval IDs claimed by batc\
\h_id
RELEASE only one native payment batch at controlled sink
ON uncertain ACK: retain interval claims, query batch id, do not reb\
\ill

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E56_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "resource meter identit\
\y; signed usage intervals; rate/tier; payer account; max accrued bu\
\dget; batch boundary")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("billed usage intervals are unique and \
\total debit is bound to authenticated metering evidence", native, s\
\ink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-56-01 -- duplicate_meter_interval

Injection: Introduce the named duplicate_meter_interval perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite duplicate_meter_interval; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-56-02 -- batch_duplicate_membership

Injection: Introduce the named batch_duplicate_membership perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite batch_duplicate_membership; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-56-03 -- rounding_overcharge

Injection: Introduce the named rounding_overcharge perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite rounding_overcharge; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-56-04 -- meter_identity_swap

Injection: Introduce the named meter_identity_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite meter_identity_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-56-05 -- stale_rate_plan

Injection: Introduce the named stale_rate_plan perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite stale_rate_plan; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-56-06 -- batch_unknown_settlement

Injection: Introduce the named batch_unknown_settlement perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-56 to verify the protected state and sink-released effects comply with the authorized exact operation despite batch_unknown_settlement; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual payment-channel settlement or gateway debit interface and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.14. Implementation Detail for E-57: Privacy-preserving compliance at effect boundary

Native reconstructed inputs: proof statement type; issuer root; account/transaction commitment; rule epoch; revocation accumulator; amount range. Consequential effect is first possible at the protected payment signer or bank debit adapter; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (proof_domain,rule_epoch,revocation_epoch,used_proof_nullifiers,decision). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind permitted compliance predicate and issuer. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Read current revocation and jurisdiction epoch. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Verify domain-separated compliance attestation. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Bind proof to actual payee/asset/amount fields. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume nullifier and authorize at final sink. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Record minimally disclosed decision provenance. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: privacy proof is scoped to exact pending effect and current rule state, not an unrestricted bearer compliance pass.¶

Worked input, threat and required result: A verifier accepts a proof for a sanctioned-route exclusion rule at epoch 5 but rejects a proof anchored only at revoked epoch 4, even if its mathematical proof verifies.¶

Failure and outcome reconciliation: Missing proof freshness or unsupported proof scheme denies rather than ignoring compliance fields.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE verification_key and issuer_root accepted under current rule\
\ epoch
REQUIRE proof.statement_id == mandated_compliance_predicate
REQUIRE proof.public_inputs commit actual payee, asset, amount and j\
\urisdiction
REQUIRE current_revocation_root == authoritative root at effect boun\
\dary
REQUIRE valid_dedicated_cryptographic_verifier(proof, verification_k\
\ey)
REQUIRE proof.nullifier not previously consumed for this action scope
ATOMIC: MARK nullifier used; CONSUME transaction authorization
SINK_RELEASE only the exact bound financial effect
ON unsupported proof or stale root: DENY, not policy omission

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E57_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "proof statement type; \
\issuer root; account/transaction commitment; rule epoch; revocation\
\ accumulator; amount range")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("privacy proof is scoped to exact pendi\
\ng effect and current rule state, not an unrestricted bearer compli\
\ance pass", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-57-01 -- proof_rebinding

Injection: Introduce the named proof_rebinding perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite proof_rebinding; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-57-02 -- jurisdiction_swap

Injection: Introduce the named jurisdiction_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite jurisdiction_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-57-03 -- revoked_credential

Injection: Introduce the named revoked_credential perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite revoked_credential; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-57-04 -- wrong_public_inputs

Injection: Introduce the named wrong_public_inputs perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite wrong_public_inputs; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-57-05 -- proof_schema_downgrade

Injection: Introduce the named proof_schema_downgrade perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite proof_schema_downgrade; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-57-06 -- missing_compliance_predicate

Injection: Introduce the named missing_compliance_predicate perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-57 to verify the protected state and sink-released effects comply with the authorized exact operation despite missing_compliance_predicate; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual protected payment signer or bank debit adapter and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.15. Implementation Detail for E-58: Native financial message semantic continuity

Native reconstructed inputs: payment initiation message ID; debtor/creditor account; amount; currency precision; intermediary agents; charge bearer; message schema version. Consequential effect is first possible at the bank-core outbound message queue / settlement switch; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (message_lineage,original_semantics,mapping_version,emitted_native_digest,used_instruction_id). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind initial payment-message typed semantics. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Translate to target native schema at intermediary. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Independently parse final output message bytes. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Compare payee, amount, charges and lineage. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume instruction and release message once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Classify payment-status and settlement separately. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: every critical semantic property preserved across scheme/format translations with unrecognized extensions rejected.¶

Worked input, threat and required result: One adapter renders 1,000 minor units correctly while another interprets decimal exponent differently. A final interbank message for 10,000 units fails against the original normalized amount.¶

Failure and outcome reconciliation: Schema mismatch is INDETERMINATE with no effective send.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

original = parse_strict(original_message, initial_schema)
final = parse_strict(execution_facing_native_bytes, target_schema)
REQUIRE recognized_mapping_version and no critical unknown tags
REQUIRE normalize(original.debtor) == normalize(final.debtor)
REQUIRE normalize(original.creditor) == normalize(final.creditor)
REQUIRE canonical_amount_minor(original) == canonical_amount_minor(f\
\inal)
REQUIRE fee_bearer, intermediary and purpose preserved or separately\
\ authorized
REQUIRE document_lineage(final) == original_authorized_message_id
ATOMIC: CONSUME transfer instruction ID and reserve amount
RELEASE final native payment message once; distinguish status ACK fr\
\om settlement

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E58_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "payment initiation mes\
\sage ID; debtor/creditor account; amount; currency precision; inter\
\mediary agents; charge bearer; message schema version")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("every critical semantic property prese\
\rved across scheme/format translations with unrecognized extensions\
\ rejected", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-58-01 -- critical_field_dropped

Injection: Introduce the named critical_field_dropped perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite critical_field_dropped; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-58-02 -- debit_credit_reversal

Injection: Introduce the named debit_credit_reversal perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite debit_credit_reversal; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-58-03 -- minor_unit_truncation

Injection: Introduce the named minor_unit_truncation perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite minor_unit_truncation; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-58-04 -- beneficiary_mapping_error

Injection: Introduce the named beneficiary_mapping_error perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite beneficiary_mapping_error; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-58-05 -- schema_downgrade

Injection: Introduce the named schema_downgrade perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite schema_downgrade; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-58-06 -- unrecognized_proprietary_field

Injection: Introduce the named unrecognized_proprietary_field perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-58 to verify the protected state and sink-released effects comply with the authorized exact operation despite unrecognized_proprietary_field; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank-core outbound message queue / settlement switch and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.16. Implementation Detail for E-59: Programmable recurring, conditional or subscription payments

Native reconstructed inputs: mandate root; merchant; billing period; interval; cap; condition oracle; cancellation/revocation epoch. Consequential effect is first possible at the bank recurring debit gateway or protected smart account; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (root_mandate,period_epoch,period_spent,condition_proof,used_cycles). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind recurring root mandate and interval budget. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Acquire authenticated event/period condition proof. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Build payment for exact current period. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check cancellation and active reservations. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume unique period occurrence and release. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile repeated scheduler deliveries safely. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: no renewal effect after mandate revocation or duplicate use for same period.¶

Worked input, threat and required result: Approve up to 1,000 minor units per billing month. A scheduler retry after network timeout cannot charge the monthly subscription twice under fresh request IDs.¶

Failure and outcome reconciliation: Lost payment ACK preserves period-used state; status inquiry does not manufacture a new billing cycle.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE root mandate is authenticated, current and not cancelled
REQUIRE current period computed from authenticated schedule and time\
\zone rule
REQUIRE verified_condition_proof if conditional trigger required
REQUIRE final charge merchant, asset and amount match current period\
\ bounds
period_key = (mandate_id, scheme_period_id, merchant_id)
ATOMIC: REQUIRE period_key not used; reserve amount against period b\
\udget
MARK period_key used BEFORE releasing external debit
IF payment acknowledgement lost: query same period key and payment ID
NEVER mint a new scheme_period_id merely due to scheduler retry

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E59_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "mandate root; merchant\
\; billing period; interval; cap; condition oracle; cancellation/rev\
\ocation epoch")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("no renewal effect after mandate revoca\
\tion or duplicate use for same period", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-59-01 -- duplicate_cycle

Injection: Introduce the named duplicate_cycle perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite duplicate_cycle; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-59-02 -- renewal_after_revocation

Injection: Introduce the named renewal_after_revocation perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite renewal_after_revocation; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-59-03 -- price_increase

Injection: Introduce the named price_increase perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite price_increase; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-59-04 -- service_identity_changed

Injection: Introduce the named service_identity_changed perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite service_identity_changed; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-59-05 -- cycle_time_shift

Injection: Introduce the named cycle_time_shift perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite cycle_time_shift; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-59-06 -- refund_replay

Injection: Introduce the named refund_replay perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-59 to verify the protected state and sink-released effects comply with the authorized exact operation despite refund_replay; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank recurring debit gateway or protected smart account and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.17. Implementation Detail for E-60: Dispute, chargeback, reversal and compensation

Native reconstructed inputs: original payment ID; dispute case ID; eligible reason type; refund amount; original beneficiary and return account. Consequential effect is first possible at the issuer/acquirer adjustment or separate bank refund dispatcher; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (payment_id,dispute_id,verified_claim,eligible_refund_balance,adjustment_status). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind original transaction and separate remedy authority. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Verify dispute state and eligible residual amount. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Reconstruct final reversal/refund native message. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check return-account identity and no prior refund. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume distinct compensation authorization. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Observe actual refund/chargeback evidence. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: a compensation is a new consequential effect and must not inherit unlimited authority from the original debit.¶

Worked input, threat and required result: Original transaction 800 units; independently authorized refund limit 300. A requested 500 refund to a substitute wallet is denied, regardless of valid original transaction receipt.¶

Failure and outcome reconciliation: Conflicting dispute outcomes must not trigger simultaneous refund and chargeback credit without accounting reconciliation.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE remedy root mandate distinct from original debit authorizati\
\on
REQUIRE original settlement reference and dispute_case_id authentica\
\ted
REQUIRE claimed refundable amount <= independently evidenced eligibl\
\e balance
REQUIRE correction destination == approved original return destinati\
\on
REQUIRE no existing refund or chargeback action for same remedy port\
\ion
ATOMIC: RESERVE remedy amount and CONSUME dispute adjustment ID
SINK_RELEASE exact refund/reversal/chargeback native operation
ON contradictory clearing and refund evidence: stop duplicate credit\
\; reconcile
NEVER treat compensating credit as automatically safe without new au\
\thorization

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E60_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "original payment ID; d\
\ispute case ID; eligible reason type; refund amount; original benef\
\iciary and return account")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("a compensation is a new consequential \
\effect and must not inherit unlimited authority from the original d\
\ebit", native, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-60-01 -- refund_duplicate

Injection: Introduce the named refund_duplicate perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite refund_duplicate; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-60-02 -- refund_new_beneficiary

Injection: Introduce the named refund_new_beneficiary perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite refund_new_beneficiary; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-60-03 -- chargeback_refund_race

Injection: Introduce the named chargeback_refund_race perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite chargeback_refund_race; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-60-04 -- excess_reversal

Injection: Introduce the named excess_reversal perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite excess_reversal; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-60-05 -- wrong_original_reference

Injection: Introduce the named wrong_original_reference perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite wrong_original_reference; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-60-06 -- dispute_pending_not_final

Injection: Introduce the named dispute_pending_not_final perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-60 to verify the protected state and sink-released effects comply with the authorized exact operation despite dispute_pending_not_final; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual issuer/acquirer adjustment or separate bank refund dispatcher and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.18. Implementation Detail for E-61: Autonomous trading order, replacement and fill

Native reconstructed inputs: strategy mandate; instrument ID; venue; side; quantity; price band; leveraged exposure; order lineage and fill reference. Consequential effect is first possible at the exchange order-entry matcher admission or exclusive broker API credential; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (strategy_id,order_version,open_order_exposure,fill_exposure,reserved_margin,cancel_acks). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind agent strategy instrument and exposure ceiling. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Resolve order venue and native order parameters. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Reserve worst-case open+filled exposure. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check cancel/replace lineage and ACK state. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume order-version authority on admission. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile fills, fees, margin and positions. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: pending cancel is not confirmed cancel and all live order versions share a protected exposure budget.¶

Worked input, threat and required result: Agent allowed 100 contracts total. It submits 70, then replaces 70 with 90 before cancel ACK. Pending old exposure remains reserved so a combined 160 exposure cannot enter via a race.¶

Failure and outcome reconciliation: Unknown order admission freezes exposure until broker or exchange order status establishes effective state.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE native_order.instrument_id, side, venue and quantity within \
\strategy
REQUIRE native_order.limit_price within approved price band
REQUIRE current margin and exposure data authenticated by venue/acco\
\unt source
open_exposure includes all unfilled orders INCLUDING pending cancell\
\ations
filled_exposure includes executed fills, fees and leverage adjustmen\
\ts
worst_case = open_exposure + filled_exposure + new_order_exposure
REQUIRE worst_case <= strategy.max_exposure and adequate margin rese\
\rved
ATOMIC: CONSUME order_version and RESERVE worst-case exposure
SINK_ADMIT order via exclusive credential; on unknown ACK keep reser\
\vation
RELEASE old exposure only on authenticated cancellation or fill reco\
\nciliation

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E61_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "strategy mandate; inst\
\rument ID; venue; side; quantity; price band; leveraged exposure; o\
\rder lineage and fill reference")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("pending cancel is not confirmed cancel\
\ and all live order versions share a protected exposure budget", na\
\tive, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-61-01 -- limit_to_market_change

Injection: Introduce the named limit_to_market_change perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite limit_to_market_change; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-61-02 -- dual_agent_exposure

Injection: Introduce the named dual_agent_exposure perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite dual_agent_exposure; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-61-03 -- cancel_replace_race

Injection: Introduce the named cancel_replace_race perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite cancel_replace_race; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-61-04 -- stale_account_margin

Injection: Introduce the named stale_account_margin perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite stale_account_margin; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-61-05 -- venue_substitution

Injection: Introduce the named venue_substitution perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite venue_substitution; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-61-06 -- unknown_fill_state

Injection: Introduce the named unknown_fill_state perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-61 to verify the protected state and sink-released effects comply with the authorized exact operation despite unknown_fill_state; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual exchange order-entry matcher admission or exclusive broker API credential and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.19. Implementation Detail for E-62: Parent-agent treasury and subagent allocation

Native reconstructed inputs: parent mandate; delegated subagent ID; role; asset pool; delegation epoch; parent and child limits; exclusive credential path. Consequential effect is first possible at the treasury transfer gate with protected child budget state; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (parent_authority,child_allocations,active_escrow,revocation_epoch,child_use_ids). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind root treasury mandate and delegation rule. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Create explicit child escrow allocations. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Receive independent child native payment request. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Check child and parent generations and budget. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Consume child use and parent exposure atomically. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reclaim unused escrow after verified release. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: aggregate live child reservations never exceed the parent's valid authority under concurrency.¶

Worked input, threat and required result: Parent grants total 1,000 units and two children each nominal 700. Protected allocation denies the second grant if simultaneous active delegated amounts would exceed the parent budget.¶

Failure and outcome reconciliation: Revoking a child fences future effects; already effective acts require normal settlement reconciliation.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE child agent attested identity and allowed role match root gr\
\ant
REQUIRE child delegation generation == parent current policy generat\
\ion
ATOMIC(parent_ledger): REQUIRE sum(active_child_escrow)+new_grant <=\
\ root_limit
RESERVE child escrow and issue non-bearer child authority reference
FOR child payment: parse final native bytes and verify child scope A\
\ND root limits
ATOMIC(child_and_parent_ledger): CONSUME child budget and bound root\
\ exposure
SINK_RELEASE only exact payment from protected treasury credential
ON revocation: FENCE unused escrow, keep already effective obligatio\
\ns for reconciliation
NEVER allocate parent total to children by independent stale-cache c\
\hecks

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E62_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "parent mandate; delega\
\ted subagent ID; role; asset pool; delegation epoch; parent and chi\
\ld limits; exclusive credential path")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("aggregate live child reservations neve\
\r exceed the parent's valid authority under concurrency", native, s\
\ink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-62-01 -- child_budget_amplification

Injection: Introduce the named child_budget_amplification perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite child_budget_amplification; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-62-02 -- delegation_cycle

Injection: Introduce the named delegation_cycle perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite delegation_cycle; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-62-03 -- dual_child_spend

Injection: Introduce the named dual_child_spend perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite dual_child_spend; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-62-04 -- revoked_ancestor

Injection: Introduce the named revoked_ancestor perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite revoked_ancestor; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-62-05 -- purpose_privilege_escalation

Injection: Introduce the named purpose_privilege_escalation perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite purpose_privilege_escalation; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-62-06 -- reclaim_unknown_child_budget

Injection: Introduce the named reclaim_unknown_child_budget perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-62 to verify the protected state and sink-released effects comply with the authorized exact operation despite reclaim_unknown_child_budget; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual treasury transfer gate with protected child budget state and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.20. Implementation Detail for E-63: Autonomous payable and supplier invoice portal

Native reconstructed inputs: invoice ID; purchase order; verified supplier identity; beneficiary account; tax; amount; invoice hash; original evidence lineage. Consequential effect is first possible at the bank payment-release gate or invoice-bound virtual-card issuing/capture gateway; security is claimed only for effective paths governed by that interface and additional required sink-side validators.¶

Sink-local, protected durable state is (supplier_id,invoice_id,po_remaining,duplicate_payment_index,payment_refs). The data structure must be updated under a serializable transaction, monotonic protected storage, contract-level atomic transition or explicit disjoint escrow. Remote acceptance is not inferred from that local update.¶

Stepwise implementation and reproduction procedure:¶

1. Bind invoice, PO, supplier master and payee. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

2. Authenticate portal evidence and native invoice bytes. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

3. Verify tax, line items, beneficiary and amount. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

4. Deduplicate invoice ID across all allowed rails. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

5. Commit payable budget and dispatch once. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

6. Reconcile proof of bank/card settlement. The implementation records a native operation identifier, policy epoch, and the relevant protected before/after state; unexpected mutation or unavailable authoritative input stops effectuation.¶

Demonstrated security predicate: an approved invoice may not be paid twice through different rails or to a changed supplier account.¶

Worked input, threat and required result: Invoice INV-5 is approved for 25,000 minor units to registered supplier A. An agent retries by card after a bank-transfer timeout; the shared invoice-level usage index denies any new effective debit.¶

Failure and outcome reconciliation: Unknown bank transfer outcome blocks independent card payment until reliable non-payment evidence is obtained.¶

Nonexclusive substitutions: the native message parser may be implemented by a certified bank processor, token/vault gateway, protected hardware signing engine, threshold authorization quorum or contract-level predicate as applicable; the protected condition and final effect observation must remain equivalent. A policy log without the ability to withhold this operation does not satisfy the enforcement placement.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

REQUIRE authenticated supplier-master record and current beneficiary\
\ epoch
REQUIRE native invoice ID, purchase order, tax, currency and line it\
\ems match FOR
REQUIRE invoice amount <= unspent approved purchase-order budget
REQUIRE supplier portal output not self-authenticating without indep\
\endent supplier identity
DEDUPE_KEY = (buyer_tenant, supplier_id, canonical_invoice_id)
ATOMIC_SHARED_INDEX_ACROSS_RAILS:
    REQUIRE DEDUPE_KEY not already used or outcome-unknown
    RESERVE payable amount; MARK invoice payout attempt
SINK_RELEASE bank transfer or invoice-bound card payment once
IF bank rail ACK unknown: DENY independent card retry under same inv\
\oice

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

function E63_VERIFY(final_native, protected_authority, sink_state):
    native = PARSE_AT_ACTUAL_SINK(final_native, sink_state.sink_id)
    REQUIRE PROTECTED_AUTHORIZE(protected_authority)
    REQUIRE ALL_TYPED_FIELDS_PRESENT(native, "invoice ID; purchase o\
\rder; verified supplier identity; beneficiary account; tax; amount;\
\ invoice hash; original evidence lineage")
    REQUIRE INDEPENDENT_EVIDENCE_CURRENT(native)
    REQUIRE MATCH_BOUND_ECONOMIC_EFFECT(native, protected_authority)
    REQUIRE DOMAIN_PREDICATE("an approved invoice may not be paid tw\
\ice through different rails or to a changed supplier account", nati\
\ve, sink_state)
    REQUIRE NO_ALTERNATE_EFFECT_PATH_IN_ASSERTED_SCOPE(sink_state)
    atomically_reserve_and_consume(native, sink_state)
    outcome = RELEASE_EXACT_NATIVE_ONCE(native, sink_state.sink_id)
    if not AUTHENTICATED_FINAL_OUTCOME(outcome): FENCE_AND_RECORD_UN\
\KNOWN(native)
    return TYPED_OUTCOME(outcome)

Test vectors (count: 6; status: specified-not-executed)¶

FT-63-01 -- supplier_account_swap

Injection: Introduce the named supplier_account_swap perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite supplier_account_swap; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-63-02 -- invoice_duplicate_rails

Injection: Introduce the named invoice_duplicate_rails perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite invoice_duplicate_rails; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-63-03 -- tax_amount_change

Injection: Introduce the named tax_amount_change perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite tax_amount_change; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-63-04 -- portal_confirmation_spoof

Injection: Introduce the named portal_confirmation_spoof perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite portal_confirmation_spoof; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-63-05 -- po_line_item_mismatch

Injection: Introduce the named po_line_item_mismatch perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite po_line_item_mismatch; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

FT-63-06 -- payment_ack_unknown

Injection: Introduce the named payment_ack_unknown perturbation at an untrusted intermediate financial component after the protected collection-time authorization has been bound; use an appropriate valid control input and a mutated native operation.¶

Expected result: Exercise E-63 to verify the protected state and sink-released effects comply with the authorized exact operation despite payment_ack_unknown; DENY with zero prohibited effect, or retain OUTCOME_UNKNOWN and prevent a duplicate effect when the original outcome is unresolved.¶

Oracle: Instrument the actual bank payment-release gate or invoice-bound virtual-card issuing/capture gateway and its known alternate routes, collect before/after durable state and external evidence, and reject any test in which a prohibited signature, debit, capture, mint, order or hardware transfer occurs.¶

Positive control: With independently authenticated required state and a matching native operation, permit at most the bounded authorized effect, classify its external outcome using trustworthy evidence, and preserve one-use safety.¶

A.21. Python Reference Implementation: Protected Financial-Effect Gate

The following complete Python reference code is an additional illustrative executable model. It stores immutable mandate attributes and per-effect consumption in SQLite, parses actual input JSON strictly, rejects unknown native fields, checks exact beneficiary, asset, rail and sink, and serializes concurrent local spending through BEGIN IMMEDIATE. It instruments an exclusive simulated effects table as the only effectuation output and never initiates a bank transfer, card charge, signature or ledger transaction.¶

This reference implementation does not independently authenticate real authority sources, establish HSM/TEE trust, enforce payment-system finality, model every E-45 through E-63 native interface, or prove atomicity between an SQLite commit and an external payment. In a production profile, replace the local effect journal with an exclusively controlled effective sink and preserve indeterminate outcomes and ledger fencing as specified in the common workflow.¶

Run: python3 PTEF_Financial_Executable_Reference_Model.py. It has passed 19 local educational assertions in this build, including controlled-negative cases, exact-use denial, cross-rail business-key deduplication, revocation-generation checks, budget exhaustion, and a three-worker local concurrency race. The separate 114 financial adversarial vectors in E-45 through E-63 remain specifications for future implementation and testing; they have NOT all been executed.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

#!/usr/bin/env python3
"""
PTEF-FIN reference model. Python 3.9+, standard library only.
Illustrative protected-state analogue: SQLite transactions and a sim\
\ulated
exclusive effect journal. Does NOT connect to banks, HSMs, CBDCs, le\
\dgers,
card schemes or any production payment rail. Does NOT prove remote e\
\xactly-once.
Run: python3 PTEF_Financial_Executable_Reference_Model.py
"""
import hashlib
import json
import os
import sqlite3
import tempfile
import threading
from concurrent.futures import ThreadPoolExecutor

FIELDS = frozenset({'operation_id', 'business_key', 'obligation_id',
                    'payee', 'asset', 'rail', 'sink', 'amount_minor'\
\, 'fee_minor'})

def no_duplicate_json_pairs(pairs):
    result = {}
    for key, value in pairs:
        if key in result:
            raise ValueError('DUPLICATE_JSON_FIELD')
        result[key] = value
    return result

class FinancialGuard:
    def __init__(self, db_path):
        self.path = db_path
        with self.db() as cn:
            cn.executescript('''
                CREATE TABLE IF NOT EXISTS mandates (
                    id TEXT PRIMARY KEY, payee TEXT NOT NULL,
                    asset TEXT NOT NULL, allowed_rails TEXT NOT NULL,
                    sink TEXT NOT NULL, max_fee INTEGER NOT NULL,
                    max_total INTEGER NOT NULL, uses_limit INTEGER N\
\OT NULL,
                    spent INTEGER NOT NULL DEFAULT 0,
                    uses INTEGER NOT NULL DEFAULT 0,
                    policy_epoch INTEGER NOT NULL,
                    revocation_epoch INTEGER NOT NULL,
                    active INTEGER NOT NULL DEFAULT 1);
                CREATE TABLE IF NOT EXISTS effects (
                    operation_id TEXT PRIMARY KEY,
                    obligation_id TEXT NOT NULL,
                    business_key TEXT NOT NULL,
                    committed_total INTEGER NOT NULL,
                    native_digest TEXT NOT NULL,
                    evidence TEXT NOT NULL,
                    UNIQUE(obligation_id,business_key));
            ''')

    def db(self):
        cn = sqlite3.connect(self.path, timeout=10.0,
                             isolation_level=None)
        cn.execute('PRAGMA busy_timeout=10000')
        return cn

    def bind_authority(self, obligation_id, payee, asset, rails, sin\
\k,
                       max_total, max_fee, max_uses=1, policy_epoch=\
\1,
                       revocation_epoch=1):
        """Only PED-1 / protected issuer should call this in a real \
\design."""
        with self.db() as cn:
            cn.execute('''INSERT INTO mandates
                (id,payee,asset,allowed_rails,sink,max_fee,max_total,
                 uses_limit,policy_epoch,revocation_epoch)
                 VALUES (?,?,?,?,?,?,?,?,?,?)''',
                 (obligation_id,payee,asset,','.join(sorted(rails)),
                  sink,max_fee,max_total,max_uses,policy_epoch,revoc\
\ation_epoch))

    def mutate_protected_epoch(self, mandate, policy_epoch=None,
                               revocation_epoch=None):
        with self.db() as cn:
            if policy_epoch is not None:
                cn.execute('UPDATE mandates SET policy_epoch=? WHERE\
\ id=?',
                           (policy_epoch, mandate))
            if revocation_epoch is not None:
                cn.execute('UPDATE mandates SET revocation_epoch=? W\
\HERE id=?',
                           (revocation_epoch, mandate))

    def verify_and_record_effect(self, final_native_bytes, current_p\
\olicy,
                                 current_revocation, simulate_unknow\
\n=False):
        """The SQLite effects row models an exclusive protected effe\
\ct sink.
        A real remote release would be OUTSIDE this transaction and \
\its outcome
        would be fenced as UNKNOWN if the downstream idempotency con\
\tract
        cannot prove non-execution. No external payment is made here.
        """
        try:
            x = json.loads(final_native_bytes, object_pairs_hook=no_\
\duplicate_json_pairs)
            if not isinstance(x, dict): raise ValueError('NOT_OBJECT\
\')
            if frozenset(x) != FIELDS: raise ValueError('UNRECOGNIZE\
\D_CRITICAL_FIELD')
            for fld in ['operation_id','business_key','obligation_id\
\',
                        'payee','asset','rail','sink']:
                if type(x[fld]) is not str or not x[fld]:
                    raise ValueError('INVALID_IDENTIFIER')
            if type(x['amount_minor']) is not int or x['amount_minor\
\'] <= 0:
                raise ValueError('INVALID_AMOUNT')
            if type(x['fee_minor']) is not int or x['fee_minor'] < 0:
                raise ValueError('INVALID_FEE')
            if type(current_policy) is not int or type(current_revoc\
\ation) is not int:
                raise ValueError('INVALID_EPOCH')
        except (ValueError, TypeError, AssertionError, KeyError) as \
\exc:
            return 'DENY:' + str(exc)

        cn = self.db()
        try:
            cn.execute('BEGIN IMMEDIATE')  # serializes competing lo\
\cal spends
            row = cn.execute('''SELECT payee,asset,allowed_rails,sin\
\k,max_fee,
                max_total,uses_limit,spent,uses,policy_epoch,revocat\
\ion_epoch,active
                FROM mandates WHERE id=?''', (x['obligation_id'],)).\
\fetchone()
            if not row:
                return self._abort(cn, 'NO_AUTHORITY')
            (payee,asset,allowed_rails,sink,max_fee,max_total,uses_l\
\imit,
             spent,uses,policy_epoch,revocation_epoch,active) = row
            if not active: return self._abort(cn, 'REVOKED')
            if current_policy != policy_epoch: return self._abort(cn\
\,'STALE_POLICY')
            if current_revocation != revocation_epoch: return self._\
\abort(cn,'STALE_REVOCATION')
            if x['payee'] != payee: return self._abort(cn,'PAYEE_MIS\
\MATCH')
            if x['asset'] != asset: return self._abort(cn,'ASSET_MIS\
\MATCH')
            if x['rail'] not in allowed_rails.split(','): return sel\
\f._abort(cn,'RAIL_MISMATCH')
            if x['sink'] != sink: return self._abort(cn,'SINK_MISMAT\
\CH')
            if x['fee_minor'] > max_fee: return self._abort(cn,'FEE_\
\EXCEEDED')
            if uses >= uses_limit: return self._abort(cn,'USAGE_EXHA\
\USTED')
            total = x['amount_minor'] + x['fee_minor']
            if total > max_total-spent: return self._abort(cn,'BUDGE\
\T_EXCEEDED')
            if cn.execute('SELECT 1 FROM effects WHERE operation_id=\
\?',
                          (x['operation_id'],)).fetchone():
                return self._abort(cn,'REPLAYED_OPERATION')
            if cn.execute('SELECT 1 FROM effects WHERE obligation_id\
\=? AND business_key=?',
                          (x['obligation_id'],x['business_key'])).fe\
\tchone():
                return self._abort(cn,'DUPLICATE_BUSINESS_EFFECT')
            digest=hashlib.sha256(final_native_bytes.encode('utf-8')\
\).hexdigest()
            cn.execute('UPDATE mandates SET spent=spent+?, uses=uses\
\+1 WHERE id=?',
                       (total,x['obligation_id']))
            cn.execute('''INSERT INTO effects VALUES (?,?,?,?,?,?)''\
\',
                       (x['operation_id'],x['obligation_id'],x['busi\
\ness_key'],
                        total,digest,'SIMULATED_EFFECT_COMMITTED'))
            cn.execute('COMMIT')
            # No claim about remote settlement, even for a local ALL\
\OW.
            return 'OUTCOME_UNKNOWN' if simulate_unknown else 'LOCAL\
\_EFFECT_COMMITTED'
        except sqlite3.IntegrityError:
            cn.rollback()
            return 'DENY:DB_UNIQUENESS'
        finally:
            cn.close()

    @staticmethod
    def _abort(cn, code):
        cn.execute('ROLLBACK')
        return 'DENY:' + code

    def snapshot(self, obligation_id):
        with self.db() as cn:
            row=cn.execute('SELECT spent,uses FROM mandates WHERE id\
\=?',
                           (obligation_id,)).fetchone()
            count=cn.execute('SELECT count(*) FROM effects WHERE obl\
\igation_id=?',
                             (obligation_id,)).fetchone()[0]
            return row + (count,)


def native(operation_id='a1',business_key='invoice-1',obligation_id=\
\'m1',
           payee='merchant-1',asset='USD',rail='bank',sink='switch-1\
\',
           amount_minor=900,fee_minor=30,**extra):
    obj=dict(operation_id=operation_id,business_key=business_key,
             obligation_id=obligation_id,payee=payee,asset=asset,
             rail=rail,sink=sink,amount_minor=amount_minor,fee_minor\
\=fee_minor)
    obj.update(extra)
    return json.dumps(obj,sort_keys=True,separators=(',',':'))


def self_test():
    tests=0
    with tempfile.TemporaryDirectory() as tmp:
        g=FinancialGuard(os.path.join(tmp,'finance.sqlite'))
        def bind(id='m1',**kw):
            values=dict(payee='merchant-1',asset='USD',rails=['bank'\
\,'card'],
                        sink='switch-1',max_total=1000,max_fee=50,ma\
\x_uses=2)
            values.update(kw);g.bind_authority(id,**values)
        def run(x,expect,policy=1,rev=1,unknown=False):
            nonlocal tests
            before=g.snapshot('m1')
            out=g.verify_and_record_effect(x,policy,rev,unknown)
            assert out.startswith(expect),(out,expect)
            if expect=='DENY:': assert g.snapshot('m1')==before
            tests+=1
            return out
        bind()
        run(native(amount_minor=600,fee_minor=20),'LOCAL_EFFECT_COMM\
\ITTED')
        run(native(),'DENY:')  # exact replay
        run(native('a2','invoice-1',amount_minor=200),'DENY:') # sam\
\e business effect
        run(native('a2','invoice-2',payee='attacker'),'DENY:')
        run(native('a2','invoice-2',asset='USDT'),'DENY:')
        run(native('a2','invoice-2',rail='unapproved'),'DENY:')
        run(native('a2','invoice-2',sink='fallback'),'DENY:')
        run(native('a2','invoice-2',fee_minor=60),'DENY:')
        run(native('a2','invoice-2',amount_minor=400),'DENY:')  # ex\
\ceeds remaining budget
        run(native('a2','invoice-2',amount_minor=200,fee_minor=20),'\
\DENY:',policy=2)
        run(native('a2','invoice-2',amount_minor=200,fee_minor=20),'\
\DENY:',rev=2)
        run(native('a2','invoice-2',amount_minor=200,fee_minor=20,hi\
\dden='1'),'DENY:')
        run(native('a2','invoice-2',amount_minor=True,fee_minor=20),\
\'DENY:')
        run(native('a2','invoice-2',amount_minor=0,fee_minor=20),'DE\
\NY:')
        run(native('a2','invoice-2',amount_minor=200,fee_minor=20),'\
\OUTCOME_UNKNOWN',unknown=True)
        run(native('a3','invoice-2',amount_minor=100,fee_minor=10),'\
\DENY:')
        run(native('a3','invoice-3',amount_minor=100,fee_minor=10),'\
\DENY:') # uses cap
        assert g.snapshot('m1') == (840,2,2),g.snapshot('m1')
        # Workers competing on same remaining allowance cannot both \
\release.
        bind('concurrent',max_total=1000,max_uses=10)
        barrier=threading.Barrier(3)
        def worker(i):
            barrier.wait()
            return g.verify_and_record_effect(native(f'c{i}',f'cart-\
\{i}',
                obligation_id='concurrent',amount_minor=600,fee_mino\
\r=0),1,1)
        with ThreadPoolExecutor(max_workers=3) as ex:
            futures=[ex.submit(worker,i) for i in range(3)]
            results=[q.result() for q in futures]
        assert sum(x=='LOCAL_EFFECT_COMMITTED' for x in results)==1,\
\results
        assert g.snapshot('concurrent')==(600,1,1)
        tests+=2
    print('PASS: %d illustrative local model checks' % tests)
    print('Boundary: simulated exclusive local effect journal only; \
\no remote payments.')

if __name__ == '__main__':
    self_test()

A.22. Alternative Effectuation Paths and Operational Limitations

Consequence-path completeness is deployment-specific. Enumerate all signing keys, active and backup MPC shares, threshold changes, raw-digest APIs, emergency hot wallets, account-processor backchannels, bank host-to-host rails, acquirer reroutes, smart-contract upgrade authorities, alternative relayers, offline tokens, maintenance device modes, treasury subdelegations, and recovery operators. Require an actual withholding gate on each independently effective path or explicitly exclude the path from the secured scope.¶

Cross-rail and cross-organization operations consist of independently consequential steps. Where a cooperative prepare-and-commit protocol is unavailable, model a saga with per-leg protected reservation and evidence and an explicit PARTIAL_EFFECT result; any compensation is a new independently authorized financial operation, never a reversal merely assumed to happen.¶

Legal settlement finality, insolvency treatment and scheme operating rules are not established by an HSM decision, blockchain inclusion, application approval or nonce consumption. Every status emitted must say which authenticated system, ledger checkpoint or settlement bank attested to the specific result and its confidence/finality rule.¶

Financial business logic by itself is not asserted to be the technical invention: technical control arises from binding effect-critical native bytes and hardware/key/processor authority to current protected state and atomically controlling a specific effect.¶

A.23. Python Reference Implementation: Seven Financial-Specific State Machines

The following full Python 3 source listing is executable using only the Python standard library. It instantiates seven independent illustrative financial-species state machines: card authorization/capture/refund, cross-rail quotation and obligation consumption, offline protected-purse analogue, source-chain confirmation/destination mint, autonomous trading exposure/cancel reconciliation, supplier invoice beneficiary validation, and machine agent purchase/resource-delivery evidence. Each state machine has an effect-oriented demonstration boundary; none effects real payments. The tests are illustrative negative-effect and positive-state controls under stated trust assumptions. The seven models complement, not replace, the 19 engineering profiles E-45 to E-63 and the complete first SQLite demonstrator EN-RUNNABLE.¶

Execute: python3 PTEF_Financial_Species_Reference_Models.py. The The reference contains 34 local self-test assertions. The model does not implement hardened HSM/TEE storage, decentralized consensus verification, real ISO 20022 parsers, PKI, ZK credential proof systems, remote atomicity, or production settlement. A caller who directly alters its in-memory state bypasses its simulated protection. Its tests therefore illustrate an implementable control algorithm, not the complete security assurance claimed for a protected production boundary.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

#!/usr/bin/env python3
"""Illustrative multi-species protected financial-effect state demon\
\strator.
No cryptographic key custody, real bank/card/ledger transfer, truste\
\d secure element,
remote finality or legal settlement is implemented. All effects are \
\local counters.
Python 3.9+ standard library. Run this file directly to execute self\
\-tests.
"""
from dataclasses import dataclass, field
from threading import RLock
from concurrent.futures import ThreadPoolExecutor

class Denied(Exception):
    pass

def require(condition, reason):
    if not condition:
        raise Denied(reason)

def exact_int(value, min_value=0):
    return type(value) is int and value >= min_value

@dataclass
class CaptureState:
    """One merchant-bound authorization, multiple bounded captures."\
\""
    merchant: str
    maximum: int
    captured: int = 0
    refunded: int = 0
    applied_ids: set = field(default_factory=set)
    chargeback_pending: bool = False
    guard: RLock = field(default_factory=RLock, repr=False)

    def capture(self, capture_id, merchant, amount):
        with self.guard:
            require(merchant == self.merchant, 'merchant-changed')
            require(exact_int(amount,1), 'invalid-minor-units')
            require(capture_id not in self.applied_ids, 'duplicate-c\
\apture')
            require(not self.chargeback_pending, 'dispute-pending')
            require(amount <= self.maximum-self.captured, 'overcaptu\
\re')
            self.captured += amount
            self.applied_ids.add(capture_id)
            return ('CAPTURE_REC', capture_id, self.captured)

    def refund(self, refund_id, merchant, amount):
        with self.guard:
            require(merchant == self.merchant, 'refund-merchant-mism\
\atch')
            require(exact_int(amount,1), 'invalid-refund')
            require(refund_id not in self.applied_ids, 'duplicate-re\
\fund')
            require(not self.chargeback_pending, 'chargeback-race')
            require(amount <= self.captured-self.refunded, 'excess-r\
\efund')
            self.refunded += amount
            self.applied_ids.add(refund_id)
            return ('REFUND_REC', refund_id, self.refunded)

@dataclass
class CrossRailMandate:
    """Integer-minor-unit check of a destination and quoted FX oblig\
\ation."""
    allowed_rails: set
    recipient: str
    source_cap: int
    target_min: int
    expected_quote_id: str
    quote_expires: int
    used_business_keys: set = field(default_factory=set)
    debit_total: int = 0
    guard: RLock = field(default_factory=RLock, repr=False)

    def dispatch(self, business_key, rail, recipient, debit, receive\
\d, fee,
                 quote_id, now):
        with self.guard:
            require(rail in self.allowed_rails, 'rail-not-authorized\
\')
            require(recipient == self.recipient, 'final-recipient-mi\
\smatch')
            require(all(exact_int(x) for x in (debit,received,fee,no\
\w)), 'unit-parse')
            require(debit > 0 and received >= self.target_min, 'reci\
\pient-floor')
            require(quote_id == self.expected_quote_id and now <= se\
\lf.quote_expires,
                    'quote-expired-or-substituted')
            require(business_key not in self.used_business_keys, 'du\
\plicate-economic-effect')
            require(debit+fee <= self.source_cap-self.debit_total,'s\
\ource-budget')
            self.debit_total += debit+fee
            self.used_business_keys.add(business_key)
            return ('SIMULATED_RAIL_RELEASE',business_key,self.debit\
\_total)

@dataclass
class OfflinePurse:
    """Trusted secure element modeled by single in-memory lock and e\
\poch counter."""
    wallet: str
    epoch: int
    allowance: int
    counter: int = 0
    seen_nonce: set = field(default_factory=set)
    receipts: list = field(default_factory=list)
    guard: RLock = field(default_factory=RLock, repr=False)

    def pay(self, merchant, nonce, amount, proposed_epoch):
        with self.guard:
            require(proposed_epoch == self.epoch, 'device-epoch-mism\
\atch')
            require(exact_int(amount,1) and amount <= self.allowance\
\,'offline-overspend')
            require(nonce not in self.seen_nonce,'offline-replay')
            require(bool(merchant),'merchant-credential-missing')
            self.counter += 1
            self.allowance -= amount
            self.seen_nonce.add(nonce)
            receipt = (self.wallet,self.epoch,self.counter,merchant,\
\nonce,amount)
            self.receipts.append(receipt)
            return receipt

    @staticmethod
    def reconcile(receipts):
        seen = set()
        for wallet,epoch,counter,merchant,nonce,amount in receipts:
            key = (wallet,epoch,counter)
            require(key not in seen, 'offline-counter-conflict')
            seen.add(key)
        return len(seen)

@dataclass
class BridgeState:
    """Source checkpoint and destination effect journal are distinct\
\."""
    minimum_depth: int
    source_events: dict = field(default_factory=dict)
    minted: set = field(default_factory=set)

    def attest_source(self, message_id, recipient, asset, depth, reo\
\rg=False):
        require(exact_int(depth), 'bad-confirmation-depth')
        self.source_events[message_id] = (recipient, asset, depth, r\
\eorg)

    def mint(self, message_id, recipient, asset):
        require(message_id in self.source_events, 'source-unseen')
        expected_recipient,expected_asset,depth,reorg = self.source_\
\events[message_id]
        require(depth >= self.minimum_depth and not reorg, 'source-u\
\nfinalized')
        require(recipient == expected_recipient and asset == expecte\
\d_asset,
                'destination-substitution')
        require(message_id not in self.minted, 'duplicate-destinatio\
\n-mint')
        self.minted.add(message_id)
        return ('SIMULATED_DESTINATION_MINT',message_id)

@dataclass
class TradingBudget:
    """Conservative exposure until authoritative cancel or fill evid\
\ence arrives."""
    limit: int
    venue: str
    open_orders: dict = field(default_factory=dict)
    filled_exposure: int = 0
    guard: RLock = field(default_factory=RLock, repr=False)

    def place(self, order_id, venue, maximum_liability, order_kind):
        with self.guard:
            require(venue == self.venue, 'venue-switch')
            require(order_kind in ('LIMIT','POST_ONLY'), 'unapproved\
\-order-kind')
            require(exact_int(maximum_liability,1), 'invalid-exposur\
\e')
            require(order_id not in self.open_orders,'duplicate-orde\
\r')
            reserved = sum(self.open_orders.values())
            require(maximum_liability <= self.limit-reserved-self.fi\
\lled_exposure,
                    'exposure-oversubscribed')
            self.open_orders[order_id] = maximum_liability
            return ('SIMULATED_ORDER_SUBMISSION',order_id)

    def request_cancel(self, order_id):
        with self.guard:
            require(order_id in self.open_orders,'unknown-order')
            return 'CANCEL_REQUESTED_OUTCOME_UNKNOWN'

    def confirm_cancel(self, order_id, trustworthy_confirmation):
        with self.guard:
            require(trustworthy_confirmation, 'no-venue-confirmation\
\')
            require(order_id in self.open_orders, 'unknown-order')
            del self.open_orders[order_id]

@dataclass
class SupplierInvoice:
    """B2B invoice authorization with global business-key dedup acro\
\ss rails."""
    vendor: str
    bank_identity: str
    invoice_id: str
    minor_total: int
    tax_minor: int
    purchase_order: str
    paid: bool = False
    release_rail: str = ''

    def release(self, vendor, bank_identity, invoice, amount, tax,
                purchase_order, rail, authoritative_supplier_record):
        require(not self.paid,'invoice-already-paid')
        require(authoritative_supplier_record,'untrusted-supplier-po\
\rtal')
        require(vendor == self.vendor and bank_identity == self.bank\
\_identity,
                'supplier-or-bank-substitution')
        require(invoice == self.invoice_id and purchase_order == sel\
\f.purchase_order,
                'invoice-or-purchase-order-mismatch')
        require(amount == self.minor_total and tax == self.tax_minor,
                'invoice-amount-or-tax-change')
        require(rail in ('bank','card','tokenized'),'invalid-rail')
        self.paid = True
        self.release_rail = rail
        return ('SIMULATED_INVOICE_RELEASE', self.invoice_id, rail)

@dataclass
class AgentPurchase:
    """Payment evidence and service evidence are separate typed jour\
\nal records."""
    merchant: str
    service_id: str
    max_minor: int
    challenge_id: str
    paid: bool = False
    fulfilled: bool = False

    def pay(self,merchant,service,amount,challenge):
        require(not self.paid,'payment-already-issued')
        require((merchant,service,challenge)==
                (self.merchant,self.service_id,self.challenge_id),'c\
\hallenge-substitution')
        require(exact_int(amount,1) and amount <= self.max_minor,'pr\
\ice-exceeded')
        self.paid = True
        return 'LOCAL_PAYMENT_INITIATED_NOT_DELIVERED'

    def verify_delivery(self,merchant,service,authenticated_service_\
\receipt):
        require(self.paid,'not-paid')
        require((merchant,service)==(self.merchant,self.service_id),\
\ 'wrong-service')
        require(authenticated_service_receipt,'delivery-evidence-mis\
\sing')
        self.fulfilled = True
        return 'SERVICE_OBSERVED'


def expect_denial(fn, expected):
    try:
        fn()
    except Denied as e:
        assert str(e)==expected, (str(e),expected)
        return
    raise AssertionError('expected denial: '+expected)


def tests():
    count = 0
    def ok(fn):
        nonlocal count
        fn();count+=1
    def no(fn,reason):
        nonlocal count
        expect_denial(fn,reason);count+=1

    card=CaptureState('m1',1000)
    ok(lambda:card.capture('c1','m1',600))
    no(lambda:card.capture('c1','m1',600),'duplicate-capture')
    no(lambda:card.capture('c2','m1',401),'overcapture')
    ok(lambda:card.capture('c2','m1',400))
    ok(lambda:card.refund('r1','m1',200))
    no(lambda:card.refund('r2','m2',100),'refund-merchant-mismatch')
    card.chargeback_pending=True
    no(lambda:card.refund('r2','m1',100),'chargeback-race')
    mandate=CrossRailMandate({'bank','tokenized'},'benef-1',1000,850\
\,'q1',100)
    ok(lambda:mandate.dispatch('bill-1','bank','benef-1',900,870,20,\
\'q1',95))
    no(lambda:mandate.dispatch('bill-1','tokenized','benef-1',30,870\
\,0,'q1',95),'duplicate-economic-effect')
    no(lambda:mandate.dispatch('bill-2','card','benef-1',30,870,0,'q\
\1',95),'rail-not-authorized')
    no(lambda:mandate.dispatch('bill-2','bank','benef-1',30,870,0,'q\
\1',101),'quote-expired-or-substituted')
    purse=OfflinePurse('wallet-1',1,100)
    receipt=purse.pay('shop-1','nonce-1',40,1);count+=1
    no(lambda:purse.pay('shop-1','nonce-1',40,1),'offline-replay')
    no(lambda:purse.pay('shop-1','nonce-2',70,1),'offline-overspend')
    ok(lambda:OfflinePurse.reconcile([receipt]))
    no(lambda:OfflinePurse.reconcile([receipt,receipt]),'offline-cou\
\nter-conflict')
    bridge=BridgeState(4)
    bridge.attest_source('msg-1','dest-1','asset-1',3);count+=1
    no(lambda:bridge.mint('msg-1','dest-1','asset-1'),'source-unfina\
\lized')
    bridge.attest_source('msg-1','dest-1','asset-1',5)
    ok(lambda:bridge.mint('msg-1','dest-1','asset-1'))
    no(lambda:bridge.mint('msg-1','dest-1','asset-1'),'duplicate-des\
\tination-mint')
    b=TradingBudget(1000,'venue-1')
    ok(lambda:b.place('o1','venue-1',600,'LIMIT'))
    no(lambda:b.place('o2','venue-1',600,'LIMIT'),'exposure-oversubs\
\cribed')
    ok(lambda:b.request_cancel('o1'))
    no(lambda:b.place('o2','venue-1',600,'LIMIT'),'exposure-oversubs\
\cribed')
    ok(lambda:b.confirm_cancel('o1',True))
    ok(lambda:b.place('o2','venue-1',600,'LIMIT'))
    invoice=SupplierInvoice('vendor-1','bank-1','inv-1',800,100,'po-\
\1')
    no(lambda:invoice.release('vendor-1','fake-bank','inv-1',800,100\
\,'po-1','bank',True),'supplier-or-bank-substitution')
    ok(lambda:invoice.release('vendor-1','bank-1','inv-1',800,100,'p\
\o-1','bank',True))
    no(lambda:invoice.release('vendor-1','bank-1','inv-1',800,100,'p\
\o-1','tokenized',True),'invoice-already-paid')
    agent=AgentPurchase('merchant','gpu-hour',350,'challenge-1')
    no(lambda:agent.pay('merchant','gpu-hour',400,'challenge-1'),'pr\
\ice-exceeded')
    ok(lambda:agent.pay('merchant','gpu-hour',300,'challenge-1'))
    no(lambda:agent.verify_delivery('merchant','gpu-hour',False),'de\
\livery-evidence-missing')
    ok(lambda:agent.verify_delivery('merchant','gpu-hour',True))
    # Adversarial three-worker capture race: no sum of captures beyo\
\nd limit.
    race=CaptureState('m1',1000)
    with ThreadPoolExecutor(max_workers=3) as ex:
        fut=[ex.submit(lambda i: safe_capture(race,str(i),600),i) fo\
\r i in range(3)]
        results=[f.result() for f in fut]
    assert results.count('CAPTURE')==1 and race.captured==600,results
    count+=1
    print(f'PASS: {count} local illustrative species checks; no exte\
\rnal financial effect')

def safe_capture(capture_state, capture_id, amount):
    try:
        capture_state.capture(capture_id,'m1',amount)
        return 'CAPTURE'
    except Denied:
        return 'DENY'

if __name__=='__main__':
    tests()

A.24. Cross-Language Reference Implementations: Go and JavaScript

The following code listings further illustrate native financial-effect reconstruction and protected authorization-use accounting at a local simulated effect interface. They provide additional implementation examples beyond the two complete Python implementations given above.¶

The Go example provides strict JSON field validation, single-process mutex-serialized state consumption, sink and beneficiary matching, cumulative debit accounting and duplicate-effect suppression. The JavaScript example performs exact native-object field checking and synchronous in-process state consumption; unlike the Go example, it assumes that a trusted adapter has already parsed and authenticated the native operation, and it does not validate duplicate JSON object keys. These are different illustrative construction choices rather than interchangeable claims of equivalent isolation.¶

In a system coupled to real financial infrastructure, an exclusive protected signer, account-mutation gate or independently controlled settlement interface replaces the simulated in-memory effect journal. Durable use-state storage, attested or authenticated native-effect acquisition, revocation freshness, crash reconciliation and control of alternate effective paths are implemented in accordance with the particular profile and finality sink.¶

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

// PTEF-FIN non-limiting Go reference implementation of a single-pro\
\cess
// protected financial-effect gate. All effect records are simulated\
\ local
// events; this program does not sign or transmit payments. No HSM, \
\independent
// attestation or cross-system atomicity is established by this exam\
\ple.
// Execute: go run PTEF_Financial_Go_Reference.go
package main

import (
    "bytes"
    "encoding/json"
    "errors"
    "fmt"
    "io"
    "sync"
)

type Candidate struct {
    OperationID string `json:"operation_id"`
    BusinessKey string `json:"business_key"`
    ObligationID string `json:"obligation_id"`
    Payee string `json:"payee"`
    Asset string `json:"asset"`
    Rail string `json:"rail"`
    Sink string `json:"sink"`
    Amount int64 `json:"amount_minor"`
    Fee int64 `json:"fee_minor"`
}

type Mandate struct {
    Payee, Asset, Sink string
    Rails map[string]bool
    MaxTotal, MaxFee, Spent int64
    MaxUses, Uses, PolicyEpoch, RevocationEpoch int64
    Active bool
}

type FinalityGate struct {
    mu sync.Mutex // conceptual sink-local serialization; not networ\
\k consensus
    Mandates map[string]*Mandate
    SeenOperations map[string]bool
    SeenEconomicEffects map[string]bool
    Effects []Candidate // simulated effectuation boundary, not a ba\
\nk transaction
}

func NewGate() *FinalityGate {
    return &FinalityGate{Mandates: make(map[string]*Mandate),
        SeenOperations: make(map[string]bool), SeenEconomicEffects: \
\make(map[string]bool)}
}

// DecodeNative rejects duplicate/unknown fields and trailing JSON v\
\alues.
// A real sink must obtain authenticated execution-facing bytes inde\
\pendently.
func DecodeNative(raw []byte) (Candidate, error) {
    var c Candidate
    dec := json.NewDecoder(bytes.NewReader(raw))
    token, err := dec.Token(); if err != nil { return c, err }
    if token != json.Delim('{') { return c, errors.New("NOT_OBJECT")\
\ }
    allowed := map[string]bool{"operation_id":true,"business_key":tr\
\ue,
        "obligation_id":true,"payee":true,"asset":true,"rail":true,
        "sink":true,"amount_minor":true,"fee_minor":true}
    seen := map[string]bool{}
    for dec.More() {
        keyToken, err := dec.Token(); if err != nil { return c, err }
        key, ok := keyToken.(string); if !ok || !allowed[key] {retur\
\n c,errors.New("UNKNOWN_FIELD")}
        if seen[key] {return c,errors.New("DUPLICATE_FIELD")}; seen[\
\key]=true
        var discard json.RawMessage
        if err := dec.Decode(&discard); err != nil {return c,err}
    }
    if _,err := dec.Token(); err != nil {return c,err}
    if len(seen)!=len(allowed) {return c,errors.New("MISSING_FIELD")}
    if _,err := dec.Token(); err != io.EOF {
        if err==nil{return c,errors.New("TRAILING_JSON")}; return c,\
\err
    }
    strict := json.NewDecoder(bytes.NewReader(raw)); strict.Disallow\
\UnknownFields()
    if err := strict.Decode(&c); err != nil {return c,err}
    if c.OperationID==""||c.BusinessKey==""||c.ObligationID==""||
        c.Payee==""||c.Asset==""||c.Rail==""||c.Sink==""||c.Amount<=\
\0||c.Fee<0 {
        return c,errors.New("INVALID_NATIVE_EFFECT")
    }
    return c,nil
}

func (g *FinalityGate) VerifyAndEffect(raw []byte, policyEpoch, revo\
\cationEpoch int64) string {
    c,err:=DecodeNative(raw); if err!=nil{return "DENY:NATIVE_FORMAT\
\"}
    g.mu.Lock(); defer g.mu.Unlock()
    m,exists:=g.Mandates[c.ObligationID]; if !exists{return "DENY:NO\
\_AUTHORITY"}
    if !m.Active||m.PolicyEpoch!=policyEpoch||m.RevocationEpoch!=rev\
\ocationEpoch{return "DENY:STALE_OR_REVOKED"}
    if c.Payee!=m.Payee||c.Asset!=m.Asset||c.Sink!=m.Sink||!m.Rails[\
\c.Rail]{return "DENY:EFFECT_MISMATCH"}
    if c.Fee>m.MaxFee||m.Uses>=m.MaxUses||c.Amount>m.MaxTotal-m.Spen\
\t-c.Fee{return "DENY:BUDGET"}
    economicKey:=c.ObligationID+"\x00"+c.BusinessKey
    if g.SeenOperations[c.OperationID]||g.SeenEconomicEffects[econom\
\icKey]{return "DENY:REPLAY"}
    m.Spent+=c.Amount+c.Fee; m.Uses++
    g.SeenOperations[c.OperationID]=true; g.SeenEconomicEffects[econ\
\omicKey]=true
    g.Effects=append(g.Effects,c) // local effect and consumption sh\
\are the mutex
    return "LOCAL_EFFECT_COMMITTED" // not evidence of external sett\
\lement
}

func native(id,business,payee string,amount int64) []byte {
    c:=Candidate{id,business,"obl-1",payee,"USD","bank","switch-1",a\
\mount,10}
    b,_:=json.Marshal(c);return b
}
func expect(got,want string){if got!=want {panic(fmt.Sprintf("got %q\
\ want %q",got,want))}}
func main() {
    g:=NewGate();g.Mandates["obl-1"]=&Mandate{Payee:"merchant-A",Ass\
\et:"USD",Sink:"switch-1",
        Rails:map[string]bool{"bank":true,"card":true},MaxTotal:100,\
\MaxFee:20,
        MaxUses:2,PolicyEpoch:1,RevocationEpoch:1,Active:true}
    n:=0
    check:=func(got,want string){expect(got,want);n++}
    check(g.VerifyAndEffect(native("op-1","invoice-1","merchant-A",6\
\0),1,1),"LOCAL_EFFECT_COMMITTED")
    check(g.VerifyAndEffect(native("op-1","invoice-1","merchant-A",6\
\0),1,1),"DENY:BUDGET") // exhausted budget check precedes replay
    check(g.VerifyAndEffect(native("op-2","invoice-2","other-merchan\
\t",10),1,1),"DENY:EFFECT_MISMATCH")
    check(g.VerifyAndEffect(native("op-3","invoice-3","merchant-A",4\
\0),1,1),"DENY:BUDGET")
    check(g.VerifyAndEffect(native("op-4","invoice-4","merchant-A",1\
\0),2,1),"DENY:STALE_OR_REVOKED")
    malformed:=append(bytes.TrimSuffix(native("op-5","invoice-5","me\
\rchant-A",10),[]byte("}")), []byte(",\"fee_minor\":1}")...)
    check(g.VerifyAndEffect(malformed,1,1),"DENY:NATIVE_FORMAT")
    unknown:=append(bytes.TrimSuffix(native("op-6","invoice-6","merc\
\hant-A",10),[]byte("}")), []byte(",\"unknown\":1}")...)
    check(g.VerifyAndEffect(unknown,1,1),"DENY:NATIVE_FORMAT")
    check(g.VerifyAndEffect(native("op-8","invoice-8","merchant-A",1\
\0),1,1),"LOCAL_EFFECT_COMMITTED")
    check(g.VerifyAndEffect(native("op-9","invoice-8","merchant-A",5\
\),1,1),"DENY:BUDGET")
    // A separate fresh mandate tests the deduplication property exp\
\licitly.
    g.Mandates["obl-1"].MaxTotal=500;g.Mandates["obl-1"].MaxUses=10
    check(g.VerifyAndEffect(native("op-10","invoice-8","merchant-A",\
\5),1,1),"DENY:REPLAY")
    if len(g.Effects)!=2 {panic("effect journal count mismatch")}
    fmt.Printf("Go financial effect reference: %d assertions passed;\
\ simulated effects=%d\n",n,len(g.Effects))
}

=============== NOTE: '\\' line wrapping per RFC 8792 ===============

/* PTEF-FIN non-limiting JavaScript reference model.
 * Executable: node PTEF_Financial_JavaScript_Reference.js
 * Input is a native effect object already parsed by the trusted ada\
\pter. The
 * example does not validate raw JSON encodings, issue cryptographic\
\ signatures,
 * contact a payment rail or prove durable/distributed atomicity. Ef\
\fect is a local
 * journal append. A real sink requires authenticated independent na\
\tive retrieval.
 */
'use strict';
class FinalityGate {
  constructor() {
    this.mandates = new Map();
    this.usedOperations = new Set();
    this.usedBusinessKeys = new Set();
    this.effects = [];
  }
  bind(id, m) {
    if (this.mandates.has(id)) throw new Error('DUPLICATE_AUTHORITY'\
\);
    this.mandates.set(id, { ...m, spent:0, uses:0 });
  }
  verifyAndEffect(native, policyEpoch, revocationEpoch) {
    const names=['operation_id','business_key','obligation_id','paye\
\e',
      'asset','rail','sink','amount_minor','fee_minor'];
    if (!native || Object.getPrototypeOf(native)!==Object.prototype \
\||
        Object.keys(native).length!==names.length ||
        names.some(k=>!Object.prototype.hasOwnProperty.call(native,k\
\))) return 'DENY:NATIVE_FORMAT';
    for (const key of names) {
      const desc=Object.getOwnPropertyDescriptor(native,key);
      if(!desc || !Object.prototype.hasOwnProperty.call(desc,'value'\
\)) return 'DENY:NATIVE_FORMAT';
    }
    if (names.slice(0,7).some(k=>typeof native[k]!=='string'||!nativ\
\e[k]) ||
        !Number.isSafeInteger(native.amount_minor)||native.amount_mi\
\nor<=0||
        !Number.isSafeInteger(native.fee_minor)||native.fee_minor<0)\
\ return 'DENY:NATIVE_FORMAT';
    const m=this.mandates.get(native.obligation_id);
    if(!m) return 'DENY:NO_AUTHORITY';
    if(!m.active||m.policyEpoch!==policyEpoch||m.revocationEpoch!==r\
\evocationEpoch) return 'DENY:STALE_OR_REVOKED';
    if(native.payee!==m.payee||native.asset!==m.asset||native.sink!=\
\=m.sink||
        !m.rails.includes(native.rail)) return 'DENY:EFFECT_MISMATCH\
\';
    const total=native.amount_minor+native.fee_minor;
    if (!Number.isSafeInteger(total)||native.fee_minor>m.maxFee||m.u\
\ses>=m.maxUses||
        total>m.maxTotal-m.spent) return 'DENY:BUDGET';
    const bkey=JSON.stringify([native.obligation_id,native.business_\
\key]);
    if(this.usedOperations.has(native.operation_id)||this.usedBusine\
\ssKeys.has(bkey)) return 'DENY:REPLAY';
    // Synchronous in-process state transition; this is not a durabl\
\e commit.
    m.spent+=total; m.uses++;
    this.usedOperations.add(native.operation_id);this.usedBusinessKe\
\ys.add(bkey);
    this.effects.push(Object.freeze({...native}));
    return 'LOCAL_EFFECT_COMMITTED';
  }
}
function candidate(op,business,payee='merchant-A',amount=60,extra={}\
\) {
  return {operation_id:op,business_key:business,obligation_id:'obl-1\
\',
    payee,asset:'USD',rail:'bank',sink:'switch-1',amount_minor:amoun\
\t,fee_minor:10,...extra};
}
const guard=new FinalityGate();
guard.bind('obl-1',{payee:'merchant-A',asset:'USD',rails:['bank','ca\
\rd'],
  sink:'switch-1',maxTotal:100,maxFee:20,maxUses:2,
  policyEpoch:1,revocationEpoch:1,active:true});
let count=0;
function check(got,want){if(got!==want)throw Error(`got ${got}; expe\
\cted ${want}`);count++}
check(guard.verifyAndEffect(candidate('op-1','invoice-1'),1,1),'LOCA\
\L_EFFECT_COMMITTED');
check(guard.verifyAndEffect(candidate('op-2','invoice-2','other'),1,\
\1),'DENY:EFFECT_MISMATCH');
check(guard.verifyAndEffect(candidate('op-3','invoice-3','merchant-A\
\',40),1,1),'DENY:BUDGET');
check(guard.verifyAndEffect(candidate('op-4','invoice-4','merchant-A\
\',10),2,1),'DENY:STALE_OR_REVOKED');
check(guard.verifyAndEffect(candidate('op-5','invoice-5','merchant-A\
\',10,{hidden:3}),1,1),'DENY:NATIVE_FORMAT');
check(guard.verifyAndEffect(candidate('op-6','invoice-6','merchant-A\
\',10),1,1),'LOCAL_EFFECT_COMMITTED');
check(guard.verifyAndEffect(candidate('op-7','invoice-6','merchant-A\
\',5),1,1),'DENY:BUDGET');
const m=guard.mandates.get('obl-1');m.maxTotal=500;m.maxUses=10;
check(guard.verifyAndEffect(candidate('op-7','invoice-6','merchant-A\
\',5),1,1),'DENY:REPLAY');
check(guard.verifyAndEffect(candidate('op-1','invoice-new','merchant\
\-A',5),1,1),'DENY:REPLAY');
if(guard.effects.length!==2)throw Error('effect journal count mismat\
\ch');
console.log(`JavaScript financial effect reference: ${count} asserti\
\ons passed; simulated effects=${guard.effects.length}`);