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 movements without identifying their legally distinct effects or associated evidence and reversal obligations. The paper formalizes six ERC-8319 meanings in Isabelle/HOL, verifies typed execution properties, and reports separately scoped Solidity/EVM evidence. It establishes a bounded machine-checked semantics and evidence map, while leaving complete cross-layer refinement, deployment, and external legal truth unestablished.

  • Problem

    Security-token standards provide privileged mechanics, but their on-chain observations do not identify which legally distinct effect a privileged movement executed or which evidence and reversal obligations it carries.

  • Method

    The paper formalizes six ERC-8319 regulatory effects and reversals in Isabelle/HOL, then relates the model to one Solidity/EVM candidate through scoped abstraction, conditional refinement, and separately classified evidence.

  • Results

    The paper answers its four research questions with typed semantics, mechanized theorem groups and witnesses, conditional profile-scoped correspondence results, and evidence stratification with artifact-identity discipline.

  • Takeaways & Limitations

    The result provides machine-checked domain semantics and an explicit map of proved, bounded, assumed, and open claims for regulatory token execution.

  • Takeaways & Limitations

    Complete Isabelle-to-Solidity-to-EVM refinement remains open, while deployment verification, production readiness, external legal truth, and several runtime-link obligations are not established.

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

The paper addresses a gap in security-token standards: privileged movements lack typed legal-effect, evidence, and reversal semantics. It separates mechanisms, meanings, and assurance claims while bounding what its model and evidence establish.

  • Research gap: Existing standards provide privileged transfer and control mechanisms, but their on-chain observations do not identify the legally distinct effect a movement executes.The same balance movement may represent custody, confiscation, recovery, or liquidation, with different evidence and reversal obligations.
  • Research questions: The paper asks how to model six ERC-8319 effects, verify their abstract properties, relate them to one Solidity/EVM candidate, and report heterogeneous evidence without implying end-to-end refinement.These questions cover semantics, machine-checked properties, cross-layer correspondence, and evidence discipline.
  • Contributions: The work contributes a machine-checked reference semantics with separate reversals and three-way outcomes, plus theorem suites, constructive witnesses, mutations, and a scoped ERC-TRUST correspondence case study.The case study distinguishes model theorems, abstraction relations, conditional refinement corollaries, Solidity and EVM evidence, artifact identity, and the absent deployment boundary.
  • Evidence discipline: Evidence stratification prevents combinations of tool passes from implying a stronger cross-layer theorem, while artifact-identity rules separate semantic runtime drift from packaging drift.The paper also maintains a stable-identifier objection register for stronger standards, theorems, traces, or counterexamples.
  • Scope: The scope excludes complete Isabelle-to-Solidity-to-EVM refinement and presents the result as a domain-specific semantics and evidence-boundary study.The paper does not introduce generic typed outcomes, replay protection, formal verification, mutation testing, or software provenance.
  • Action model: Reversals refer to original actions and recorded prior state rather than untyped balance operations; stale, duplicate, and out-of-order attempts reject with persistent-state stutter.CONFISCATE, LIQUIDATE, and RECOVER have no implicit reversal merely because another transfer could later occur.

4 Typed Regulatory Execution Semantics

The abstract kernel executes typed commands over state, authorization, and external observations, classifying every step as applied, rejected, or operational failure. Its mechanized theorems constrain state changes, receipts, reversals, case terminality, and external-truth inference.

  • Canonical execution: Canonical execution is a total function from state, command, authorization context, and external observation to state, outcome, and observation.The abstract command domain includes forward actions and reversals, with concrete encoding delegated to the implementation relation.
  • Outcome semantics: Every canonical step receives exactly one of Applied, Rejected, or OperationalFailure, and rejected or operationally failed steps preserve the complete persistent state.The theorem covers full-state stutter within the declared abstract domain, but not gas or timing equality.
  • Frames and receipts: Applied results fix regulatory effects, balance and custody changes, case records, authorization and nonce consumption, observations, and the final canonical receipt.Rejected and operational outcomes preserve state, while the full frame preserves every unrelated field outside the declared write set.
  • Replay, epochs, and frames: Replay protection combines domain-bound command identifiers with authority epochs and nonces, while stale authorizations are invalidated by authority rotation or policy rebinding.Applied actions consume the identifier and nonce; rejected and operational outcomes commit no receipt.
  • Case terminality: Terminality is scoped to the affected case, allowing unrelated cases and assets to proceed after one case becomes terminal.A deliberately global-terminal mutation is distinguished by the current-profile state theorem.
  • External-truth boundary: Two external worlds can disagree about title, sale, debt discharge, and rightful recipients while inducing identical kernel observations, so bound inputs cannot establish those facts.The theorem is a positive limitation: checked commitments cannot be silently upgraded into legal or factual truth claims.

5 Isabelle/HOL Mechanization and ERC-TRUST Instantiation

The section mechanizes ERC-8319’s six legal effects while keeping foundation transition labels, conditional runtime refinement, and implementation evidence explicitly separate.

  • Figure 3 separates the path from normative prose to typed definitions, theorems, witnesses, mutations, and implementation obligations.Each relation carries its own evidence class, so proving the model does not discharge the implementation obligation.
  • The mechanization keeps six legal-effect kinds separate from seven foundation transition labels, including reversal-only RELEASE and transfer-layer RECOVER and LIQUIDATE.A named theorem prevents conflation between the two inventories.
  • 5.1 The conditional theorem named end-to-end refinement: The theorem named end_to_end_refinement is conditional because its locale assumes the runtime link rather than constructing it from compiler, runtime-semantics, and concrete-execution evidence.Compiler correctness is explicitly recorded as a nonclaim.
  • 5.2 Foundation and instantiation: The development inherits RAC’s outcome-sensitive state-machine results and adds typed six-action execution, action-specific reversals, and separately scoped implementation evidence.It does not recount RAC’s classifications as new contributions.
  • 5.2 Foundation and instantiation: The successor candidate records fourteen successor inputs and a 74-row obligation ledger: 70 closed, two successor-mandatory runtime-link rows, two inapplicable, and no current-mandatory row.These records expose the remaining central link but do not show refinement of every foundation theorem.

6 Concrete Nonvacuity and Direct Falsification

Constructive witnesses make the abstract claims nonvacuous, while direct mutations test whether declared distinctions are load-bearing. The implementation evidence remains separately scoped and does not establish complete cross-layer refinement.

  • Concrete nonvacuity: 18 manifest inputs cover six actions across three outcome scenarios, with computed outcomes, target states, observables, and write sets.Isabelle also supplies reachable witnesses for every action, all reversals, ordinary-transfer paths, and alternate-overlay compatibility paths.
  • Direct falsification: 15 direct abstract mutations each break its targeted consumer theorem, testing distinctions including outcome separation, epoch invalidation, frames, and case-local terminality.This campaign covers only the declared fault set and is narrower than mutation adequacy in general.
  • Correspondence obligations: The correspondence map covers ABI decoding, storage projection, dependency calls, exact-use tickets, action effects, rollback, failure stutter, receipts, and artifact identities.These obligations connect normative claims to implementation checks without making them a single proof.
  • Cross-kernel boundary: The fixed-width decoder combines conditional KEVM reachability, Isabelle word bounds, and a hash-bound K/Isabelle record whose correspondence remains trusted.No single kernel checks the final correspondence.
  • Open boundaries: The current candidate has conditional profile-scoped relations and two open evidence edges: model-to-Solidity correspondence and deployment.Selected EVM seams and bounded rules narrow the gap but remain below verified compilation.
  • Profile status: All twelve named evidence lanes pass, while the obligation ledger reports 70 of 74 rows closed, two successor obligations, and two inapplicable rows.These fractions are qualification status, not progress toward an unconditional theorem; the central cross-layer theorem remains absent.

9 Artifact and Reproducibility

The candidate is tied to explicit artifact coordinates, separate commands, and reproducibility procedures. The evidence record preserves distinctions between artifact regeneration, tool-specific results, and unresolved claims about deployment and correctness.

  • Artifact identity: The reviewed candidate is identified by a repository, commit, tree, source roots, and a minimum replay entry.These coordinates define the exact artifact under review rather than a generic repository state.
  • Reproducibility: The repository contains Isabelle theories, Solidity tests, specifications, mutation scripts, conformance vectors, runtime bindings, and replay scripts.The command set keeps model, tool, build, runtime-binding, and release-identity checks separate because they establish different facts.
  • Reproducibility limits: Reproducing every command would regenerate declared results under pinned environments but would not prove compiler correctness, tool correctness, deployment identity, or external legal truth.Reproduction validates artifact regeneration within the declared setup, not the broader claims excluded by the paper.
  • Scope of novelty: The contribution is a common semantics for six regulatory effects, not the first typed-control mechanism in security-token standards.Existing standards already provide forced transfer, recovery, freezing, request lifecycles, and related controls.
  • Semantic distinctions: Action/reversal separation is combined with prior-state references, stale and duplicate rejection, case-local terminality, and typed receipt identity.The paper distinguishes this domain-specific combination from earlier freeze/unfreeze and pause/unpause mechanisms.
  • Evidence boundaries: Tool PASS results remain in their own evidence classes, and mutation sensitivity covers only the declared fault set.A conditional theorem cannot discharge its runtime-link assumption, and the verified candidate is not thereby a deployment claim.

11 Limitations, Trusted Computing Base, and Nonclaims

The paper deliberately limits its claims to a domain semantics and bounded evidence record. It leaves central refinement, deployment, legal truth, broader architectures, and several trust assumptions outside what is machine-checked.

  • Trusted computing base: The trusted computing base includes Isabelle, K/KEVM/Kore, Solidity, Foundry, Certora, Kontrol, scripts, extractors, filesystem behavior, and human mapping review.The listed components include both proof kernels and ordinary programs whose correctness is not uniformly established.
  • Model scope: The model abstracts gas, timing, mempool and sequencing, denial of service, broader reentrancy, and the full range of third-party dependency behavior.Proxy, migration, arbitrary batch profiles, and broader ERC-3643 topologies require new conformance and evidence.
  • Cross-layer refinement: No complete machine-checked theorem connects all Isabelle states and traces to all Solidity/EVM executions.Two runtime-link ledger rows remain open, and six optional Verified Full obligations remain unclaimed.
  • Interoperability and readiness: The ERC-3643 profile is Partial, and the candidate is unaudited and not for production.The profile does not establish a complete imported initial state or same-transaction enforcement for ordinary inbound transfers.
  • External-truth nonclaims: No theorem proves authority legitimacy, policy correctness, identity, settlement, proceeds, title, entitlement, or rightful ownership.No deployed chain, address, constructor argument, role assignment, or live dependency is bound in this version.
  • Positioning: The paper’s distinct value is regulatory-action domain theory, an external-truth boundary, witness-and-mutation falsification, and evidence stratification rather than stronger cross-layer proof.The closest cited systems provide EVM reasoning, executable semantics, deep Solidity embedding, or verified compilation.

A Theorem Inventory

The theorem inventory organizes machine-checked results across canonical execution, regulatory cases, retrieval, compatibility, runtime bridging, and obligation closure, while recording explicit boundaries and conditional premises.

  • Canonical execution: Canonical execution separates applied success, rejection, and operational failure, with rejection and operational failure preserving persistent state.Successful execution also has complete frames, exact core effects, and a final canonical receipt.
  • Regulatory cases: The semantic model includes constructive witnesses for retrieval, liquidation, recovery, and other regulatory cases, but witnesses alone do not establish model adequacy.The executable manifest evaluates reachable fixtures rather than copied constants.
  • Boundaries and obligations: The inventory records external-truth nonclaims, partial ERC-3643 compatibility, conditional runtime-link composition, and generated obligation-ledger boundaries.The compatibility model does not prove arbitrary concrete deployments, and heterogeneous composition remains conditional until certification.
  • Retrieval and composition: The current-state abstraction is functional, requires the exact runtime, rejects runtime substitution, and projects case terminality and other state components exactly.Reusable summaries consume package premises rather than constituting a new EVM semantics.
  • State distinctions: Case terminality is scoped to the affected case, distinguishing global-terminal mutations and allowing unrelated cases and assets to proceed.The current-profile theories also distinguish freeze and restriction overlays.

B Assumption and Nonclaim Ledger

The assumption and nonclaim ledger separates semantic and evidence obligations from claims the paper explicitly does not make, including runtime, deployment, and adequacy boundaries.

  • Obligation ledger: Table 6 records each semantic obligation, its abstract and concrete anchors, existing evidence, and any remaining open obligation.The open-obligation column serves as the working map for contributors.
  • Falsification campaigns: The declared fault families cover identity, epochs, outcomes, frames, terminality, reversals, freeze acceptance, tickets, custody, receipts, runtime drift, packaging, and hashes.Each mutation must identify a consumer; unconsumed mutations do not earn evidence credit.
  • Evidence scope: The paper separates independent specification reproduction from the other evidence classes and does not treat mutation campaigns as general mutation adequacy.The abstract campaign at the pinned candidate comprises 15 direct mutations, each detected by its targeted consumer.

F Claim-to-Source Map

The claim-to-source map pairs each headline claim with an evidence class, required qualifier, and forbidden expansion, preserving the boundary between formal semantics and external truth.

  • Semantic claims: Six regulatory actions and three reversals have distinct typed identities and effects in the abstract model.This claim is bounded to the declared Isabelle/HOL semantic domain.
  • Outcome claims: Applied, Rejected, and OperationalFailure are distinct outcomes, with the latter two preserving declared persistent state.The claim concerns the persistent abstract state and declared observation alphabet.
  • Nonclaims: The claim map forbids expanding the formal results into legal validity or correct real-world classification.External-truth nonclaims concern title, settlement, entitlement, and related legal facts.
  • Evidence ceilings: The evidence scope excludes gas, timing, mempool behavior, and every environmental observation.These exclusions define the ceiling of the persistent-state semantics rather than a claim about external execution conditions.

G Verification Commands

The verification commands are intentionally separated by evidence layer, covering replay, Isabelle closure, Solidity and Foundry checks, Certora, Kontrol/KEVM, and artifact identity.

  • Execution model: Every layer runs locally except Certora, which requires a Certora account.Each command establishes only facts for its own layer.
  • Replay: Full current-profile replay uses the release replay script and current-profile verifier.These commands are provided as the executable entry point for replay verification.
  • Isabelle and mutations: Isabelle closure and model-level negative mutations run through separate PowerShell scripts.The commands cover model verification and negative mutation detection.
  • Solidity and Foundry: Solidity build and Foundry testing use forge build --sizes and forge test.The build command also reports runtime sizes.
  • Identity and runtime evidence: Artifact identity checks cover deterministic builds, release identity, runtime binding, and runtime-binding replay verification.Kontrol/KEVM proofs are invoked by matching names listed in the evidence results file.

H Full Objection-Disposition Table

Table 10 records objections, dispositions, and residual limits across standards, semantics, evidence, deployment, and external-truth claims. The paper separates bounded results from unresolved correspondence, deployment, compiler, and legal-truth boundaries.

  • Scope and contribution: The paper distinguishes existing token-control mechanisms from its contribution: typed regulatory semantics, theorem structure, and evidence-boundary analysis.Existing standards already provide related controls and lifecycles; the paper presents its contribution as a bounded domain-specific semantics and evidence study.
  • Interoperability and release boundaries: The ERC-3643 interoperability descriptor remains Partial and full=false, while Native runtime identity and build margins are treated as separate bounded obligations.The adapter does not establish complete initial-state inventory or ordinary-transfer hook coverage; compiler or feature drift can consume reported margins.
  • Residual limits: The paper does not claim complete Isabelle-to-Solidity-to-EVM refinement, compiler correctness, deployment verification, production readiness, or external legal truth.The declared observation alphabet excludes ambient execution observations, and legal legitimacy, governance quality, custody, and lawful instruction remain outside the theorem.
  • Evidence discipline: The evidence regime forbids upward inference from combined tool passes, keeps tool implementations and configurations in the trusted base, and reports bounded counterexample evidence.Multiple tools are assigned separate projections; their pass counts do not compose into a soundness theorem.
  • State properties: Terminality is case-scoped, and the current-profile state theorems distinguish a global-terminal mutant that could block unrelated assets.The paper explicitly treats global terminality as a negative distinction rather than the intended behavior.

I Terminology

The terminology defines the paper’s operational vocabulary for cases, projections, evidence, runtime links, and artifact identity. These terms mark which claims are conditional, hash-bound, partial, or still open.

  • State and case concepts: A case identifies one regulatory proceeding, and terminality is declared per case rather than for the whole token.This terminology supports the paper’s case-local terminality property.
  • Authorization terminology: An exact-use ticket is a one-time authorization bound to caller, calldata, policy, epochs, and command identity, then created and consumed within one transaction.The executable manifest evaluates action-by-outcome scenarios from kernel semantics rather than treating them as written constants.
  • Artifact identity: Packaging drift changes wrapping or metadata without changing the semantic payload, whereas semantic drift changes the payload itself.The distinction supports separate tracking of artifact identity and semantic runtime changes.
  • Evidence terminology: A qualification certificate records that evidence was produced against artifacts with exactly the recorded hashes; qualification is not third-party certification, audit, or regulatory approval.Hash binding therefore identifies the artifact scope of a published pass criterion.
  • Cross-layer relations: A retrieve relation maps concrete storage states to abstract model states, while the runtime link is the assumed relation from accepted runtime execution to the abstract transaction relation.Constructing the runtime link is identified as the open central obligation.
  • Interoperability terminology: The ERC-3643 Partial reference checks touched accounts and restriction observations but leaves manifest completeness and ordinary-transfer hook coverage unproved.Its descriptor is explicitly PARTIAL/full=false.
Loading 2608.29134v3…