PaperlayerView exact revision on arXiv

Source-linked AI summary

Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence

Jinwook Kim

arXiv:2608.29134v3cs.CRcs.LO

TL;DR

Security-token standards expose privileged controls without identifying the legal effect a movement executes. This paper mechanizes an Isabelle/HOL semantics for six ERC-8319 effects and reports matching answers to its four research questions through typed semantics, witnesses, conditional refinement, and stratified evidence.

  • Problem

    Existing standards provide privileged controls but do not identify which legally distinct effect a movement executes; that distinction matters because technical correctness does not establish external premises.

    Source: §1 · p. 1

  • Method

    The paper mechanizes an Isabelle/HOL reference semantics for six ERC-8319 effects, modeling typed actions and reversals, outcomes, replay and epoch rules, and receipts.

    Source: §3.1 · p. 3, §4.2 · p. 5, §13 · p. 13

  • Results

    The four research questions receive matching answers through typed semantics and an external-truth boundary, mechanized theorem groups and witnesses, conditional refinement, and stratified evidence.

    Source: §13 · p. 13

  • Takeaways & Limitations

    The work provides a machine-checked domain semantics while keeping candidate-specific verification evidence and open refinement obligations separately scoped.

    Source: §13 · p. 13

    No complete machine-checked theorem connects all Isabelle states and traces to all Solidity/EVM executions, and two runtime-link ledger rows remain successor obligations.

    Source: §11.3 · p. 12

Abstract

from arXiv · show

Security-token standards expose privileged controls without identifying the legal effect executed or the evidence and reversal obligations it carries. We formalize in Isabelle/HOL a reference execution semantics for the six ERC-8319 meanings: FREEZE, SEIZE, CONFISCATE, LIQUIDATE, RESTRICT, and RECOVER. It distinguishes applied, rejected, and operational-failure outcomes and mechanizes action-specific reversals, replay and epoch rules, complete frames, case-local terminality, and final receipts; the session builds without unproved placeholders or additional axioms. An indistinguishability theorem shows that bound kernel inputs cannot establish external facts about title, settlement, or entitlement. Constructive witnesses and direct mutations establish reachability and sensitivity for the declared fault set. For a successor ERC-TRUST Solidity/EVM candidate, we report separately scoped Foundry, Certora, Kontrol/KEVM, mutation, deterministic-build, runtime-identity, and independent-reproduction evidence. All twelve named evidence lanes pass with none pending, while the 74-row obligation ledger remains conditional: 70 rows are closed, two runtime-link rows remain successor obligations, and two are inapplicable. The Native runtime is bound separately from an ERC-3643 interoperability reference that explicitly reports Partial and full=false, not Verified Full. These results do not establish complete Isabelle-to-Solidity-to-EVM refinement, compiler correctness, audit completion, production readiness, deployment verification, or external legal truth. They provide a machine-checked domain semantics and an explicit map of proved, bounded, assumed, and open results.

1 Introduction · 2 Regulatory Execution Problem, System Model, and Non-Goals · 3 ERC-TRUST Overview

The paper gives regulatory actions typed meanings and action-specific execution semantics while distinguishing what the kernel can establish from external legal or factual truth. It presents a bounded ERC-TRUST reference architecture and evidence boundary, not a complete Isabelle-to-EVM refinement or proof of deployment readiness.

1 Introduction

  • Existing token standards provide privileged mechanics, but the same balance movement can represent legally distinct effects with different evidence, reversal, terminality, and receipt obligations.The paper contributes a machine-checked six-action semantics, a theorem suite, executable witnesses and mutation-based falsification, and a scoped ERC-TRUST correspondence case study.Source: §1 · pp. 1–2

2.1 Mechanism, meaning, and assurance · 2.2 System model

  • Mechanisms describe callable transitions, meanings identify regulatory effects and records, and assurance statements specify the model, implementation, tools, and assumptions supporting a claim.The model uses typed commands, persistent state, authorization and policy context, external observations, declared observations, and three outcomes for six actions and declared reversals.Source: §2.1 · p. 2, §2.2 · p. 2

3 ERC-TRUST Overview

  • ERC-TRUST is studied as an execution and conformance layer connecting ERC-8319’s legal-effect vocabulary with ERC-7943’s mechanism-neutral interface.A successful on-chain transition may still rely on unproved external premises such as title, rightful ownership, or whether a sale occurred.Source: §1 · p. 1, §2.1 · p. 2

2.3 Threat model

  • The threat model includes malformed commands, replay, stale epochs, policy denials, dependency failures, and false attestations, while requiring fail-closed behavior and unchanged state after rejection or operational failure.It does not assume legitimate authorities, uncompromised keys, truthful oracles, completed settlement, or rightful entitlement.Source: §2.3 · p. 3

2.4 Observation alphabet and non-goals

  • Failure stutter covers persistent kernel and downstream state, committed logs, and return or revert classification, but excludes gas, timing, ordering, side channels, compiler correctness, deployment identity, legal advice, audit completion, and production readiness.The paper explicitly does not establish complete Isabelle-to-Solidity-to-EVM refinement.Source: §1 · p. 2, §2.4 · p. 3

3.1 Actions and reversals

  • Reversals refer to an original action and its recorded prior state; stale, duplicate, or out-of-order attempts are rejected, while applied restorations create terminal records for the restoration attempt.CONFISCATE, LIQUIDATE, and RECOVER have no implicit reversal merely because another transfer can occur.Source: §3.1 · p. 3

3.2 Three outcomes

  • Applied commits the declared transition and canonical receipt, Rejected records completed checks that deny a command, and OperationalFailure marks unavailable or noncanonical assessment dependencies.The contribution is action-specific state, receipt, and audit semantics, not typed status classes in general.Source: §3.2 · p. 3

3.3 Reference architecture

  • The reference architecture centralizes regulatory state and receipts, binds read-only dependencies, and uses same-transaction exact-use tickets for sensitive ERC-7943 calls; its ERC-3643 adapter is Partial with full=false.Verified Full would require fresh atomic deployment, a complete initial-state gate, and same-transaction transfer or Compliance-hook enforcement; avoiding upgradeable patterns limits correspondence and runtime-identity obligations.Source: §3.3 · p. 4

4 Typed Regulatory Execution Semantics

The section formalizes typed regulatory execution with classified outcomes, replay and reversal controls, case-scoped terminality, and an explicit boundary on claims about external legal truth.

4.1 State, commands, and observations

  • Canonical execution totally classifies typed commands as Applied, Rejected, or OperationalFailure; failures stutter the full persistent state, typed entrypoints converge, and the legacy entrypoint fails closed.Applied steps fix regulatory effects, authorization and nonce consumption, and a final receipt.Source: §4.1 · p. 5

4.2 Replay, epochs, and frames

  • Successful actions consume domain-bound identifiers and epoch/nonce authorization; applied actions preserve fields outside declared writes and end with a final receipt, while stale, duplicate, or out-of-order reversals stutter.An applied reversal restores the referenced prior state and records a terminal restoration attempt; authority rotation and policy rebinding invalidate stale authorizations.Source: §4.2 · p. 5

4.3 Case-local terminality

  • Terminality is scoped to the affected case, allowing unrelated cases and assets to proceed after one case becomes terminal.A deliberately conflated global-terminal mutation is distinguished by the current-profile state theorem.Source: §4.3 · p. 5

4.4 External-truth claim boundary

  • Bound kernel inputs cannot distinguish external worlds that disagree on title, sale, debt discharge, or rightful recipient, so the model limits action guarantees without asserting those truths.SEIZE guarantees custody accounting and encumbrance preservation; LIQUIDATE binds disposition to settlement and proceeds commitments; RECOVER binds destination and entitlement commitments with one-time consumption.Source: §4.4 · pp. 5–6

5 Isabelle/HOL Mechanization and ERC-TRUST Instantiation

The section mechanizes a typed regulatory-action model and traces how normative prose becomes proof and implementation obligations, while keeping those evidence links separate. It distinguishes inherited foundation results from new instantiation results and makes the remaining runtime-refinement assumptions explicit.

5 Isabelle/HOL Mechanization and ERC-TRUST Instantiation

  • The mechanized pipeline turns normative sentences into typed definitions, theorems, witness-and-mutation obligations, and implementation obligations, with separate evidence for each edge.Proving the model alone does not discharge the implementation obligation.Source: §5 · p. 6, Figure 3 · p. 6
  • In the compatibility model, strict ERC-7943 frozen-amount increases map to typed FREEZE, while equal or decreasing forward calls are rejected and decreases require authorized UNFREEZE.Forced transfers require typed bindings and fail closed when unbound; the mapping does not expand the claim boundary, and these results do not prove properties of arbitrary third-party deployments.Source: §5 · p. 7

5.1 The conditional theorem named end-to-end refinement

  • The theorem named end_to_end_refinement is conditional on an assumed runtime link; constructing that premise from compiler, runtime semantics, and concrete execution remains unproved.Compiler correctness is explicitly recorded as a nonclaim.Source: §5.1 · p. 7

5.2 Foundation and instantiation

  • The development adds a typed six-action execution model and action-specific reversals to RAC’s inherited outcome-sensitive composition results.RAC supplies the five-state, seven-transition reference machine and results on action order, terminal behavior, observable traces, and finite transformation normal forms; these are not recounted as new contributions.Source: §5.2 · pp. 7–8
  • The obligation ledger has 74 rows: 70 closed, two successor-mandatory runtime-link obligations, two inapplicable, and none current-mandatory.The ledger names the abstract conditions consumed by the current implementation map; it does not establish that the Solidity candidate refines every foundation theorem.Source: §5.2 · p. 8
  • The foundation builds on RAC’s separately released session, whose pinned inputs and negative probes distinguish proof-content failures from supply-chain identity failures.The development records file-by-file succession for fourteen foundation inputs after the historical dependency object became unreachable at its public remote.Source: §5.2 · p. 8

6 Concrete Nonvacuity and Direct Falsification · 7 Relationship to the Solidity and EVM Implementation · 8 Layered Implementation Evidence

The paper presents machine-checked model results and layered, bounded implementation evidence while keeping runtime-link and deployment boundaries explicit. Its qualifications do not amount to complete end-to-end refinement, an audit, or production readiness.

6.1 Constructive reachability

  • Isabelle witnesses make applied, authorization-denial, and policy-unavailable outcomes reachable for every action, preventing theorems from passing only on uninhabited premises.Separate witnesses cover all three reversals, ordinary-transfer success and denial, and alternate-overlay compatibility; reachability alone does not establish model adequacy.Source: §6.1 · p. 8

6.2 Direct falsification

  • The abstract campaign’s 15 direct mutations each break their targeted consumer, while concrete positive and negative paths make correspondence claims falsifiable rather than proving the model correct.Mutated conditions include action/receipt identity, epoch invalidation, outcome separation, frame preservation, and case-local terminality; this campaign is narrower than general mutation adequacy.Source: §6.2 · p. 8, §6 · p. 8

7.1 Abstraction relation

  • The retrieve relation is unique and functional under declared well-formedness and pinned-runtime premises, projects specified state fields exactly, and supports modeled concrete outcomes.It depends on bound on-chain state and pinned configuration rather than assumed execution history; this narrows the model-to-code gap but remains below verified compilation.Source: §7.1 · p. 9

7.2 ABI, storage, calls, and traces

  • The correspondence map covers ABI decoding, storage, dependency calls, exact-use tickets, action and reversal effects, rollback, traces, receipts, and bytecode identity.For fixed-width decoding, KEVM establishes conditional runtime reachability and Isabelle proves word bounds, while a hash-bound K/Isabelle correspondence remains in the trusted computing base.Source: §7.2 · p. 9

7.3 Open central obligation

  • Complete refinement remains open until a proof object constructs the runtime-link relation for every accepted execution in the declared profile.Current profile-scoped refinement theorems derive state, failure, and receipt consequences only when hash-bound qualification certificates and abstract-summary premises hold.Source: §7.3 · p. 9

8 Layered Implementation Evidence; 8.5 What the current evidence supports

  • The evidence layers hand off tool-specific results without logically composing them; the current support is scoped to declared model results, bounded checks, selected EVM paths, and reproducible bytecode.Rejected and operational outcomes preserve declared persistent fields in the abstract model, while applied actions write their declared write set and one final receipt; the corresponding implementation evidence is bounded and conditional, not an audit or production-readiness claim.Source: §8 · p. 9, Figure 4 · p. 9, §8.5 · p. 10

8.1 Current profile

  • 12 of 12 evidence lanes pass with none pending, while the 74-row ledger remains conditional: 70 closed, two runtime-link successor obligations, and two inapplicable.The separate package projection reports 7/7 reusable packages, 49/49 Core obligations, 24/24 mandatory Supporting obligations, and 0/6 optional Verified Full obligations; these are not independent whole-runtime proofs and do not imply the missing central theorem.Source: §8.1 · p. 10

8.2 Foundry and Certora; 8.3 Kontrol and KEVM; 8.4 Mutation and artifact identity

  • 93 Foundry tests, 4/4 Certora rules, 4/4 Kontrol proofs, 121/121 Solidity mutations, and 23 reproduced vectors with 401 assertions provide scoped—not whole-runtime—evidence.Foundry also reports two fuzz properties with 256 runs each and nine invariants with 256 runs by 500 calls (1,152,000 invariant calls, zero reverts). Runtime qualification kills 18 declared self-mutations; four fixture items are not evaluable, and the deterministic build binds source and compiler settings to bytecode.Source: §8.2 · p. 10, §8.3 · p. 10, §8.4 · p. 10

9 Artifact and Reproducibility · 10 Adversarial Analysis and Standardization Objections

The paper pins its reproducibility claims to a specific candidate artifact and uses adversarial objections to distinguish its typed-action contribution from prior work while making residual proof and operational limits explicit.

9 Artifact and Reproducibility

  • The reviewed artifact is candidate 0.2.0-candidate.1 at public-main commit a1cd93c8288b2a92655a9daf2e96d7f564cda614, with exact tree and source-root hashes recorded.The working label has no tag or release; the repository is github.com/Oraclizer/erc-trust.Source: §9 · pp. 10–11
  • Its repository includes Isabelle, Solidity, Certora, Kontrol/KEVM, mutation, conformance, runtime-binding, and replay artifacts, while checks remain separate because they establish different facts.Appendix G lists the full command set.Source: §9 · p. 11
  • Reproducing every command would regenerate declared results under pinned environments, but would not prove compiler or tool correctness, deployment identity, or external legal truth.Source: §9 · p. 11

10.1 Existing standards already contain typed controls

  • Among 22 strongest-form objections with stable identifiers, the standards response is a common six-effect semantics—not a claim that typed controls were absent—and applied transitions are not legal judgments.The model separates action vocabulary from jurisdiction policy; a new observable effect requires a new action or profile and proof update rather than overloading an existing effect.Source: §10.1 · p. 11, §10 · p. 11

10.2 Execution distinctions may duplicate established patterns

  • The domain-specific execution contribution combines referenced prior state, stale and duplicate rejection, case-local terminality, typed receipts, audit/retry-linked outcomes, and complete persistent-state stutter.The exact-use ticket binds selector, caller, calldata, policy, epochs, and command in one transaction, then deletes immediately; raw sensitive selectors remain closed.Source: §10.2 · p. 11

10.3 The proof may validate only its own model

  • The paper acknowledges that runtime linkage remains open, tool PASS results do not compose, mutation sensitivity covers only the declared fault set, and nonvacuity does not establish model adequacy.Cross-layer positive and negative evidence makes selected disagreements observable, while specification review and counterexamples remain relevant to model adequacy.Source: §10.3 · p. 11

10.4 Operational and governance limits

  • The compiler remains trusted, deployment is not claimed, and verified code cannot establish authority legitimacy or key security; ERC-TRUST has no assigned ERC number or opened submission.An official submission with the intended header is planned only after ERC-8319 is merged; reviewers may overturn dispositions with stronger standards, theorems, traces, or counterexamples.Source: §10.4 · p. 12
  • Two clean builds agree on a 20,043-byte Native runtime, leaving 4,533 bytes; the ERC-3643 adapter is 19,480 bytes with 5,096 bytes left, and the governor is 2,787 bytes.Runtime binding establishes identity, not constructor execution or deployment, and compiler or feature drift must rerun the size gate.Source: §10.4 · p. 12

11 Limitations, Trusted Computing Base, and Nonclaims · 12 Related Work and Contribution Boundaries · 13 Conclusion

The paper contributes a typed reference semantics for ERC-8319 regulatory effects and a bounded evidence account for an ERC-TRUST candidate. It distinguishes mechanized domain claims from unresolved runtime, deployment, and external-truth claims.

11.1 Trusted computing base

  • The trusted computing base includes proof tools, ordinary verification and hashing programs, a word-correspondence record, and human review; not all components are proved correct.Named components include Isabelle and HOL libraries, K/KEVM/Kore and its solver, Solidity, Foundry, Certora, Kontrol harnesses, and replay-related operating-system and filesystem behavior.Source: §11.1 · p. 12

11.2 Model limitations

  • The model abstracts gas, timing, sequencing, denial of service, some reentrancy, and broad dependency behavior; proxy, migration, batch, and broader ERC-3643 profiles need new evidence.It fixes a reference action vocabulary and a current immutable architecture.Source: §11.2 · p. 12

11.3 Implementation limitations

  • No complete machine-checked theorem links all Isabelle states and traces to all Solidity/EVM executions; two runtime-link rows remain successor obligations and six optional Verified Full obligations are unclaimed.The ERC-3643 profile is Partial, lacking a complete imported initial state and same-transaction enforcement for ordinary inbound transfers; the candidate is unaudited and not for production.Source: §11.3 · p. 12

11.4 External and deployment limitations

  • The work proves no external legal facts and binds no live deployment; a future manifest could identify one deployment, but would not establish every deployment or operational safety.Unproved facts include authority legitimacy, policy correctness, identity, settlement, proceeds, title, entitlement, and rightful ownership.Source: §11.4 · p. 12

12.1 Security-token standards / 12.2 Typed legal and business workflows

  • ERC-1400, ERC-3643, ERC-7943, ERC-1450, and ERC-8319 are prior standards; Stipula and Daml [3] already formalize or type legal and business workflows.The claimed contribution is narrower: semantics and evidence boundaries for an Ethereum security-token execution vocabulary, not the first use of types for legal meaning or authorization.Source: §12.1 · p. 12, §12.2 · p. 13

12.3 Smart-contract formal verification / 12.4 Mutation and provenance

  • Prior EVM verification and verified-compilation systems [20] offer stronger cross-layer proof; this work applies regulatory semantics, falsification, and evidence stratification [2].Its distinct contribution also includes an explicit external-truth boundary and artifact identity inspection.Source: §12.3 · p. 13, §12.4 · p. 13

13 Conclusion

  • The artifact mechanizes ERC-8319 action semantics and records separately scoped evidence for one ERC-TRUST candidate, with answers to all four research questions.Its results include typed actions and reversals, three-way outcomes, replay and epoch rules, complete frames, case-local terminality, canonical receipts, witnesses, and direct mutations.Source: §13 · p. 13
  • The conclusion leaves runtime-link construction, a mechanized word correspondence, a Verified Full ERC-3643 profile, and deployment binding among explicit open obligations.It also calls for model-adequacy review and conformance evidence for alternative architectures; reusable elements include typed outcomes with persistent-state stutter, evidence stratification, and a reviewable objection register. Tool passes do not combine into a compiler-to-EVM proof, and no deployment or legal truth is verified.Source: §13 · p. 13

A Theorem Inventory

The inventory maps manuscript results to principal Isabelle declarations, pairing formalized execution, state, and compatibility claims with explicit limits on what those results establish. It distinguishes unconditional results from conditional relations, trusted seams, and scoped reference behavior.

Canonical execution and transaction relation

  • Canonical execution formalizes typed-action convergence, complete success frames, exact core effects, and final receipts, while rejection and operational failure stutter.The transaction relation also covers action and reversal results, with malformed transactions and dependency reverts modeled as abstract stutters.Source: A Theorem Inventory · p. 14

Witnesses and manifest evaluation

  • Constructive witnesses establish action and outcome reachability, while manifest evaluation uses reachable fixtures and keeps six-by-three distinct from five-by-seven.These witnesses do not by themselves establish model adequacy.Source: A Theorem Inventory · p. 14

External-truth boundary

  • The claim-boundary theorem shows that identical core inputs cannot distinguish external legal truth, including title, sale or debt truth, and rightful ownership.This is an epistemic boundary, not a claim about the truth or falsity of any external world.Source: A Theorem Inventory · p. 14

Token compatibility and ERC-3643 onboarding

  • Compatibility theorems model ERC-7943 freeze and forced-transfer mappings and an explicit ERC-3643 subset; onboarding remains Partial, not Verified Full.Onboarding results cover declared-entry and touched-account behavior, including operational stutter on a forced-transfer restriction mismatch; they do not establish manifest completeness or an ordinary-transfer hook theorem.Source: A Theorem Inventory · pp. 14–15

Retrieve relation and state distinctions

  • Current-state results require an exact runtime, project nonce exactly, scope case terminality, and distinguish independent freeze and restriction state from conflated and global-terminal mutants.The inventory also records direct negative adequacy results for the state distinctions.Source: A Theorem Inventory · pp. 14–15

Summaries and heterogeneous composition

  • Reusable summaries relate package premises to abstract-state commits, failure restoration, and receipt agreement; end-to-end refinement remains conditional on a runtime link.The composition result does not establish compiler correctness, and heterogeneous composition remains conditional until certification.Source: A Theorem Inventory · p. 14

Decoder guards, runtime bridge, and obligation ledger

  • Decoder-guard and generated-bridge theorems cover fixed-width guards, route exhaustiveness, typed selectors, and declared artifact identities, but do not construct the runtime-link relation.The obligation ledger names evidence anchors and leaves the runtime link conditional; cross-kernel correspondence remains a trusted seam.Source: A Theorem Inventory · p. 15

Row-corollary results

  • Row-corollary results distinguish action and reversal omissions, with freeze-success refinement conditional on named package receipts and the product inhabitant.The current-profile row consequences depend on those stated premises.Source: A Theorem Inventory · p. 15

B Assumption and Nonclaim Ledger … E Falsification Inventory

These sections identify principal assumptions and nonclaims, map semantic obligations to candidate anchors and remaining open work, distinguish evidence by its ceiling, and define counted falsification campaigns.

B Assumption and Nonclaim Ledger

  • Table 5 is designated as the principal assumptions and nonclaims ledger.Source: Table 5 · p. 15

C Model-to-Code Correspondence Map

D Tool-Evidence Matrix

E Falsification Inventory

  • Declared falsification families span identity, epochs, outcomes, frames, terminality, reversals, FREEZE acceptance, tickets, custody, receipts, runtime and packaging drift, and expected-hash overwrite.Each mutation must identify its consumer; unconsumed mutations earn no evidence credit, and campaign counts are recounted at the merged public commit before release.Source: E Falsification Inventory · p. 17, Table 8 · p. 17

F Claim-to-Source Map

This section maps headline claims to their evidence classes, required qualifiers, and forbidden expansions. It distinguishes the abstract model’s supported claims from legal and environmental claims it does not establish.

F Claim-to-Source Map

  • Table 9 maps each headline claim to its evidence class, qualifier, and forbidden expansion, including the absence of end-to-end proof, compiler correctness, audit, production readiness, deployment verification, and external legal-truth proof.Source: F Claim-to-Source Map · p. 17, Table 9 · p. 18
  • Six regulatory actions and three reversals have distinct typed identities and effects within the declared Isabelle/HOL semantic domain, not as proof of legal validity or correct real-world classification.Source: F Claim-to-Source Map · p. 17
  • Applied, Rejected, and OperationalFailure are distinct outcomes; Rejected and OperationalFailure preserve persistent state within the declared observation alphabet, not every environmental observation.Source: F Claim-to-Source Map · p. 17

G Verification Commands

The section provides separate commands for replay, Isabelle, Solidity/Foundry, Certora, Kontrol/KEVM, and artifact-identity checks. Commands run from the repository root at the stated commit; all layers run locally except Certora, which requires an account.

G Verification Commands

  • Commands are run from the artifact repository root at the commit stated in section 9, and each establishes only its own layer’s facts.On Linux or macOS, install PowerShell 7 and replace powershell -File with pwsh -File.Source: G Verification Commands · p. 18
  • The full current-profile replay and verifier use scripts/replay-current-profile-release.ps1 and scripts/verify-current-profile-release-v3.mjs.The section also lists deterministic-build, release-identity, and runtime-binding checks as artifact-identity commands.Source: G Verification Commands · pp. 18–19
  • Isabelle model closure and model-level negative mutations are run with the two model-verification scripts.The commands are formal/isabelle/ERC_TRUST/evidence/model-verification/run-trust-closure.ps1 and run-negative-mutations.ps1.Source: G Verification Commands · p. 18
  • Solidity build-size reporting and Foundry tests are run with forge build --sizes and forge test.Source: G Verification Commands · p. 18
  • Current ERC-3643 Partial Certora rules run with certoraRun implementation/certora/ERC3643Partial.conf and require a Certora account.Source: G Verification Commands · pp. 18–19
  • Kontrol/KEVM proofs use four names from evidence/kontrol-results-v3.json; repository scripts and configuration files are the executable source of truth.The command is kontrol prove --foundry-project-root . --schedule CANCUN --match-test <proof-name>.Source: G Verification Commands · p. 19

H Full Objection-Disposition Table

Table 10 catalogs 22 objections in their strongest plausible form, with initial dispositions subject to change after public review. Its responses distinguish the paper’s bounded claims from unresolved limits.

H Full Objection-Disposition Table

  • The table assigns stable identifiers to 22 objections, notes that dispositions are provisional, and says public review may add identifiers without renumbering existing ones.The manuscript also states that ERC-8319 is pending and that TRUST has no assigned number or opened pull request.Source: H Full Objection-Disposition Table · pp. 19–20
  • Novelty objections cite existing standards for recovery, freezing, request lifecycles, neutral mechanics, reversals, typed failures, nonce-bound authorization, and one-time use.The paper separates its domain semantics, theorem and falsification structure, external-truth boundary, evidence taxonomy, and open correspondence obligations from TRUST-specific advocacy.Source: H Full Objection-Disposition Table · pp. 19, 21
  • Typed execution cannot establish legal truth: scope, epoch, cancellation, and receipts constrain execution, but legitimacy, lawful instruction, beneficial title, and external title adjudication remain outside the theorem.SEIZE custody and prior-holder fields do not restore legal ownership.Source: H Full Objection-Disposition Table · pp. 19–20
  • The ERC-3643 descriptor remains Partial: it checks declared imports, touched-account state, restriction observations, and sealed governance, while Verified Full requires a fresh hook-enabled deployment and complete initial-state gate.The descriptor does not claim a complete initial-state inventory or ordinary-transfer hook; owner, Agent, batch, transfer, or compliance paths may bypass an adapter.Source: H Full Objection-Disposition Table · p. 20
  • The Isabelle-to-Solidity/EVM correspondence remains assumed, tool PASS counts cannot be combined into soundness, and tool implementations and configurations remain in the trusted computing base.The paper reports tool-specific projections and bounded counterexample evidence with exact runs and calls; full compiler-to-runtime simulation remains open.Source: H Full Objection-Disposition Table · p. 20
  • Fuzz and invariant counts do not establish generality: unexplored inputs remain, mutation sensitivity covers only declared fault operators and consumer claims, and the fault model is incomplete.Abstract witnesses are paired with concrete positive and negative paths and selected EVM seams, but mutation kills do not establish proof adequacy.Source: H Full Objection-Disposition Table · p. 20
  • Model adequacy depends on specification review and external counterexamples; revert stutter omits gas, timing, mempool, and other ambient observations beyond declared state, logs, and return/revert class.Compiler correctness is an explicit nonclaim, and this version makes no deployment claim; a future manifest must bind chain, address, runtime, constructor, roles, and dependencies.Source: H Full Objection-Disposition Table · p. 20
  • Terminality is case-scoped in the current-profile state theorems, which distinguish a global-terminal mutant that could block unrelated assets after one case closes.Product changes must rerun this negative.Source: H Full Objection-Disposition Table · p. 20

I Terminology

The terminology defines case-local regulatory state and the boundary between the kernel’s abstract model and external facts. It also distinguishes hash-bound evidence qualification from open runtime links and the explicitly partial ERC-3643 reference.

I Terminology

  • Terminality applies to an individual regulatory case, such as a seizure or liquidation, never to the token as a whole.Source: I Terminology · p. 21
  • The core observation projects kernel state and entries while excluding external-world fields; the Native path is distinct from the optional ERC-3643 adapter profile.The kernel is the immutable core that evaluates typed commands and owns regulatory state and receipts.Source: I Terminology · p. 21
  • A qualification certificate records exact artifact hashes, but qualification is a repository-defined pass criterion—not third-party certification, audit, or regulatory approval.Evidence packages group verification results through hash-bound certificates; obligation rows carry their own evidence and qualification certificates.Source: I Terminology · p. 21
  • The retrieve relation maps concrete storage to abstract model state, while the runtime link remains an assumed relation and the open central obligation.Source: I Terminology · p. 21
  • The ERC-3643 interoperability reference checks declared imports and touched accounts but leaves manifest completeness and ordinary-transfer hook coverage unproved; its descriptor is PARTIAL/full=false.Source: I Terminology · p. 21
  • A seam is a narrow, high-risk compiled-EVM boundary verified in isolation, while a witness demonstrates that a scenario’s premise is satisfiable.The author discloses co-authorship of proposed ERC-8319 and leadership of ERC-TRUST development at Oraclizer Labs.Source: I Terminology · pp. 21–22
Loading 2608.29134v3…