A Mechanized Functor Tower for Cross-Domain State Preservation

[jay-oraclizer]

This post adds two machine-checked results to a reusable verification basis for cross-domain state. State-preserving maps between synchronization domains are closed under identity and composition, with associative composition, all as mechanized theorems. And coupling breadth forms a stratified tower of functors in which forgetting a coupled chain is a natural transformation. The mechanization is a set of generic Isabelle/HOL locales over arbitrary state machines, so the laws are directly reusable by any domain that discharges the locale obligations: a bridge, a rollup exit, a shared sequencer, a permissioned settlement leg. In the previous topic we mechanized safety and liveness for atomic cross-domain state synchronization (Mechanized Proofs for Atomic Cross-Domain State Synchronization); here we mechanize composition of the preservation maps and stratify them by coupling breadth.

The gap this closes is practical. Deployed systems hold state at many strengths, bridged, mirrored, causally coupled, atomically bound, and today the strength lives in prose rather than in anything a protocol can check. On the product reading, the central theorem pair turns declared strength into a two-sided admission criterion: for valid states, processing at or above an asset’s declared requirement carries the modeled preservation guarantee, and below it an explicit counterexample rules out any general guarantee. Throughout, the line is kept explicit between what is proved, what is design reading, and what is not established.

1. What the previous post established

The earlier post fixed a state machine model of cross-domain assets and proved two things about a bind-verify-commit synchronization cycle: safety, a bidirectional per-asset preservation relation between domains, and liveness, deterministic and starvation-free selection under a Byzantine census assumption and stated fairness assumptions, both at model level in Isabelle/HOL. It also left two markers: direct composition of preservation maps was deferred, and the open questions asked how heterogeneity of synchronization strength should be treated. The first is discharged formally below; the second is sharpened into a breadth-indexed result, with the refinement to operational synchronization strength left explicit. One vocabulary carryover is load-bearing: every transition is indexed by an operation pair, which regulatory action, applied to which asset. Nothing in the earlier post depended on how many domains an asset touches; that is the dimension this post adds.

2. Preservation maps form a category

A preservation map between two state machines is a pair of functions, one on states and one on actions, subject to the preservation obligations proved earlier. Three theorems give these maps the structure of a category:

theorem preservation_id:
  assumes "state_machine states actions transition terminal"
  shows "state_preservation states actions transition terminal
                             states actions transition terminal id id"

Identity maps any well-formed machine to itself; composition is componentwise and associative, mechanized as preservation_compose and preservation_assoc. Jointly they license link-at-a-time reasoning. In a chain of a rollup leg, a base layer, and a permissioned settlement leg, the rollup-to-settlement map comes without a new proof, its obligations inherited from the links, and the grouping of hops is irrelevant to the guarantee. End-to-end claims factor into per-link obligations, so when an end-to-end property fails, at least one link obligation or composition premise has failed; which one is a diagnosis the decomposition organizes but does not perform.

When the earlier post said the entry would acquire functor status once the laws were accompanied by formal proof, this is that proof.

Composition survives heterogeneous verification. An authenticated interface layer exchanges domain states under a Merkle-style commitment scheme, with explicit obligations relating a hash interface, state extraction, a merge operation, and a blinding relation for partial views. Under those obligations, merging two authenticated states yields a valid state that refines both inputs, and a blinded view of a valid state stays valid: a domain that exposes only part of its state, a common enterprise-ledger posture, still composes soundly. Domain independence is checked separately, by discharging the same obligations against a TCP-inspired endpoint lifecycle, vocabulary borrowed from a classic protocol rather than a trace-conformant model of it, entirely outside the regulatory domain.

3. Regulatory state transition dynamics

The operations in that index are not abstract labels. The mechanized instance runs regulatory actions over a five-state, seven-action space with twelve valid transitions out of thirty-five syntactic pairs: some transitions are reversible, one state is terminal (lemma confiscated_terminal), escalation is directional, and escalation_preservation is the heterogeneous-action locale interpretation rather than another theorem. The sparsity is the content: a seizure of something already confiscated is legally meaningless, and the model rejects it at the transition relation instead of leaving it to runtime convention. Preservation therefore says something concrete: the legal effect a transition carries survives the passage between domains, and a frozen asset does not arrive on the other side merely restricted.

Two roles stay distinct. The instance verifies the internal consistency of one concrete state machine; the normative requirement that legally distinct actions remain distinguishably represented is a public matter, recorded in a draft Standards Track proposal, ERC-8319, currently in review (discussion). The mechanization does not implement that proposal, and the proposal mandates no particular state machine; it is cited only as the public taxonomy motivating this instance.

obj_step :: "(reg_action × asset_id) ⇒ global_state ⇒ global_state option"

Transitions are indexed by the action and by a stable asset identifier, and by nothing else; the next section leans on that fact.

4. Synchronization degrees as a tower of functors

Not every asset needs the same strength. On the product reading the spectrum runs from single-chain existence through eventual reconciliation and causal consistency to full atomic binding for the strongest class, including anything subject to the regulatory actions above. The mechanization stratifies the structure underneath that spectrum, not the operational meanings themselves; the distinction bounds every claim that follows.

The state space is graded by chain breadth. For each k, a carrier holds the global states whose asset holdings are supported on chains 0..k, anchored at hub chain 0, giving one functor per level:

definition deg_carrier :: "nat ⇒ global_state set" where
  "deg_carrier k = {gs. ∀c aid. asset_exists gs c aid ⟶ c ≤ k}"

definition F :: "nat ⇒ gobj" where
  "F k = ⟨ obj_states = deg_carrier k, obj_step = deg_step k ⟩"

The index formalizes coupling breadth: how many chains an asset’s state spans. Reading its levels as the operational hierarchy, observation, causal execution, atomic binding, rollback semantics, requires a separate refinement from breadth to those semantics, and that refinement is not established here. What is established is the structure the operational hierarchy would sit on.

Between adjacent levels, degree_forget (Suc k) drops the holdings of the topmost chain, and the central theorem is that this map is natural: forgetting commutes with every regulatory transition.

theorem degree_natural_transformation:
  "natural_transformation (F (Suc k)) (F k) (degree_forget (Suc k))"

\eta_{k+1} \circ F_{k+1}(\alpha) = F_k(\alpha) \circ \eta_{k+1}

for every operation α = (reg_action, asset_id), and composites of the η maps are again natural, so projection to any lower level is lawful in one step or many.

A short trace, as a statement about the model: take an asset on chains 0..2 and a freeze indexed to it. Applying the freeze at breadth 2 and then forgetting chain 2 lands in the same state as forgetting first and applying at breadth 1, so projection to a narrower context cannot disagree with the regulatory history that context should have seen. A live exit protocol, with delay, retries, and membership change, is a candidate application of this law and only that; no claim is made that any particular protocol refines the model.

Degrees attach to assets, not to the system. The hierarchy is parametric in an arbitrary assignment asset_degree :: asset_id ⇒ nat, fixed in a context and generalized on export, the formal shape of a position the previous thread converged on: synchronization strength is declared, not discovered. In the product design reading a degree is declared at issuance; the theorems are agnostic about when, cover static reassignment between cycles, and leave change during a live cycle outside the model, where it returns as an open question.

On the product reading, the theorem pair below supports a conservative two-sided admission policy and is the second headline of the post:

theorem over_provisioning_guarantees:
  assumes deg: "asset_degree aid ≤ d" and val: "valid_state gs"
  shows "guarantees_preservation d gs aid"

theorem no_downward_safety:
  assumes "asset_degree aid > system_degree"
  shows "¬ (∀gs. guarantees_preservation system_degree gs aid)"

over_provisioning_guarantees establishes the modeled preservation guarantee for valid states once system capability meets or exceeds the declared requirement; no_downward_safety supplies an explicit counterexample showing why no unconditional guarantee over all states survives under-provisioning. Together they turn the containment

S_3 \supseteq S_2 \supseteq S_1 \supseteq S_0

from a classification into the basis for an enforceable admission rule. Venue-level acceptance and refusal are design consequences of the pair, not the theorem statements themselves; the containment notation belongs to the product reading, while the formal layer contributes the theorems and the breadth index they are stated over.

The boundary between levels is pinned down as well, and one point deserves precision: lamport_hb is defined as strict order on timestamps, so what the theorem certifies is that the model’s timestamp order is a strict partial order. The name is borrowed from happened-before without claiming a message-causality construction:

theorem boundary_well_defined:
  "(causal_consistent_at aid d ⟷ (2 ≤ asset_degree aid ⟶ 2 ≤ d))
   ∧ (asset_degree aid ≤ d ⟶ causal_consistent_at aid d)
   ∧ (∀t1 t2. lamport_hb t1 t2 ⟶ ¬ lamport_hb t2 t1)
   ∧ (∀t. ¬ lamport_hb t t)
   ∧ (∀t1 t2 t3. lamport_hb t1 t2 ⟶ lamport_hb t2 t3 ⟶ lamport_hb t1 t3)"

5. What the theorems do and do not say

Stating scope is part of the result, and one exchange in the previous thread (post 5) is why this section is more than a footnote. It asked whether a categorical treatment of degrees inherits an individuation requirement: read aggregation over lots as a colimit, and commingled balances erase the very diagram the colimit needs.

The tower is lot-agnostic, but it is not individuation-free. It requires no per-lot provenance: the naturality squares index transitions by (reg_action, asset_id) and by chain breadth, and nothing tracks which units came from where. But they presuppose a stable asset-level identifier with a well-defined degree assignment asset_degree aid. Commingling units of different declared degrees under one identifier is therefore outside the model’s typing boundary, an unrepresented case rather than a refuted one. Two repairs are visible, bucketed identifiers or a conservative aggregate degree, and both are design directions, not consequences of the theorems: the mechanization proves no multi-asset join rule, and a colimit reading is legitimate only once its diagram and index are named and the representation preserves that index. Raw fungible balances erase lot indices, so for them that reading is unavailable.

The costs differ visibly too: bucketed identifiers fracture fungibility until buckets retire, while a single aggregate degree must dominate every unit’s declaration, so one high-degree unit widens the whole balance’s obligations. The typing boundary is where those costs become explicit.

Two further structural assumptions belong in the same place. The naturality results depend on a single-hub topology: chain 0 is not forgotten at any level and admissibility anchors to it, so nothing here speaks to multi-hub or changing topologies. And the action vocabulary is fixed: the squares commute for the given operation index, not across changes of the action set itself.

The division of labor, in one view:

Proved in the mechanization	Design reading	Not established
category structure of preservation maps (identity, composition, associativity); naturality of degree_forget; over_provisioning_guarantees; no_downward_safety; boundary_well_defined; authenticated merge and blinded-view validity, under the stated interface obligations	degree as issuance-time declared, checkable interface metadata; venue-level accept and refuse; exit protocols as applications of the naturality law	refinement from breadth to operational degree semantics; any multi-asset join rule; degree change during a live cycle; multi-hub naturality; conformance of any implementation to the model

The thread’s question then has a precise answer: the categorical statement does not inherit the per-lot requirement, it inherits the asset-level individuation the operation index already carries. The boundary was implicit in the definitions; the exchange forced it to be stated as theorem scope.

6. Why this matters here

Partial synchronization is the normal condition of the rollup ecosystem, and a graded model gives its strength a type. The interface reading, a design reading built on the theorems rather than a theorem itself, is direct: an asset declares its degree, a venue advertises the degree it can process, acceptance at or below that level is backed by over_provisioning_guarantees for inputs satisfying the valid-state premise, and refusal above it is what no_downward_safety conservatively motivates. Moving upward is a conversion protocol, not a relabeling; mismatches stop being silent downgrades and become typed refusals. The authenticated interface results extend the same discipline to counterparties that verify by commitment and expose blinded views, a common pattern where permissioned ledgers meet public chains, provided the interface obligations are discharged. Atomic binding also changes the structure of extraction opportunities around discrete updates, but that question lies outside the present scope.

7. Artifacts

• Mechanization: Cross_Domain_State_Preservation session, Isabelle/HOL, sorry-free build; theories including Functor_Laws.thy, Composition.thy, Hierarchy.thy, External_Instance.thy (repository at commit aafdcf327cce0dbfed4e9123dfe3f46ef786d028).
• Paper: The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL, v3.

8. Open questions

These are directions under active exploration, and community perspectives are the reason for posting them here.

• Aggregate degrees. Where units with distinct declared degrees share one representation, which conservative aggregation rules are sound, and what do they cost in expressiveness and fungibility?
• Dynamic promotion. If an asset’s declared degree changes while a synchronization cycle is in flight, which degree governs that cycle, and where must the transition boundary be placed?
• Beyond a single hub. The present naturality result preserves hub chain 0. What additional structure would recover naturality across multiple hubs or a changing coupling topology?
• Obligation boundaries. Which laws belong in a public specification, which should be discharged by implementation-level conformance or code verification, and which remain design guidance?

[WGlynn]

Agreed on the asset-level split. The operation index carries asset_id, so asset-level individuation is inside the model and per-lot provenance is not required for the naturality squares to commute. My earlier objection was aimed one level too low. It still bites at the boundary you drew in Section 5, commingling of distinct declared degrees under one identifier, because the two repairs you name there are not symmetric under an adversary. Bucketed identifiers I’d already argued for as the conservative form: epoch-bucketed ids, lot equals type, fungibility fractures by epoch and self-heals as epochs retire into the final asset. The cost is bounded and it expires. The aggregate-degree repair does neither. If one high-degree unit must dominate the whole balance’s obligations, then degree is monotone upward under mixing, and the attack surface is whatever issuance leaves open. Where anyone can send units to a balance, a third party mints one maximal-degree unit into a target and widens its obligations for free. Where issuance is permissioned the attack does not vanish, it just changes hands: the set that

can impose the label is every authorized issuer rather than the holder, and one careless or compromised issuer is enough. Either way the holder cannot shed the label short of splitting the representation you were trying to keep whole. Aggregation buys fungibility by opening a griefing surface that scales

with how open issuance is; bucketing keeps the cost on the party that wants the high degree, while aggregation lets someone else impose it. That asymmetry looks like the real content of open question 1. A conservative aggregation rule can be sound in the safety sense you proved and still fail a cost test once degree assignment is adversarially reachable. So the sharper question is whether any aggregate rule survives an adversary who can mint into a commingled balance, or whether soundness under that model forces you back to bucketing, in which case the two repairs are not two design directions but one, and the fungibility fracture stops being a choice and becomes a consequence.

The whole tower also sits against the pattern most cross-chain systems actually ship, burn-and-mint, and burn-and-mint is your degree-1 floor. One live copy, burn on the source, mint on the destination, supply conserved by an accountant, no multi-chain simultaneity to keep consistent. It is the single-chain-existence base of your hierarchy, and a one-way latch per asset in the strict sense: the burn fires once, the mint fires once, and the burned-but-not-minted interval fails to nowhere-spendable. Read that way, everything above degree 1 is the cost of an asset that must be co-present and jointly governed rather than merely moved. Burn-and-mint dissolves the consistency problem by never multi-homing; the tower is what you need precisely when single-homing is not allowed. The commingling question in Section 5 is one face of that cost, and it does not arise at degree 1 because there is only one degree and the burn-proof carries the lot. On dynamic promotion, the same latch fixes the boundary. A degree change mid-cycle is another monotone per-asset event with a firing time, so the conservative rule I gave in the earlier thread carries over: during the interval when domains disagree, the cycle is governed by whichever degree carries the stronger obligation, and the transition commits only once every connected domain reads it as crossed. The ambiguous interval is again a closed set bounded by skew, failing toward the tighter of the two degrees. That is where the transition boundary belongs, at the last domain to cross rather than the first, so no domain ever releases an obligation on the strength of a change another domain has not yet acknowledged. On the single-hub assumption, I read chain 0 as the finality anchor, and that lines up with the one-way latch I described earlier: what crosses the finality boundary is monotone and per-lot, and a single hub is what keeps happened-before a latch rather than a cycle. Multi-hub naturality probably has to answer the individuation question first, since two hubs with independent degree assignments over a shared representation is commingling again, one level up. On the last question, spec versus conformance versus guidance, I’ll name the frame rather than smuggle it in: I’ve been developing this under the name augmented mechanism design, and its one line is augment the proven core, never replace it. It sorts laws into three tiers by what a majority is allowed to move. A physics tier: laws in the machine-checked core because nothing downstream can be trusted to hold them, not an incentive, not a vote, not an operator, so they have to be true by construction and proven, which is what your Isabelle core already is. A constitutional tier: interface obligations the implementation must discharge and conformance-check case by case, binding but local, not global invariants re-proven on every change. A governance tier: design guidance a reasonable deployment could set differently without touching the proven core. The test that sorts a given law is the one your scope section already forced into the open, ask what breaks if a majority wants it broken: a safety property that breaks was never guidance and belongs in the tier no majority can reach, a law where nothing essential breaks was never physics. I’m aware this is the framework happening to answer the question, so take it as a claim to check rather than a pitch: the tower earns its keep by giving that partition a type instead of a convention, and degree-forget naturality is a clean first-tier example, since if forgetting a chain stopped commuting with a regulatory transition no governance could paper over the divergence.

[jay-oraclizer]

Thanks for taking the time to work through all four questions. The minting example makes the first question more concrete.

Section 5 described the aggregate direction as an expressiveness cost: one high-degree unit widens the whole balance’s obligations. Your example turns this into a non-imposition condition. Under open issuance, a third party can impose that widening; under permissioned issuance, the same power moves to the issuers.

Any aggregate rule would therefore need to prevent an inbound action from enlarging another holder’s obligations without consent or opted-in admission control. Bucketing satisfies that condition by construction. Whether a non-bucketed rule can also satisfy it remains formally open. In the design, however, identifier-level separation is already the intended boundary: degree is declared for an asset identifier, not recomputed from whatever enters a balance. The commingling example reinforces the reason for preserving that boundary rather than exposing a missing product mechanism.

On burn-and-mint, single-live-copy and coupling breadth are different axes. The tower does not type simultaneous copy count, so burn-and-mint cannot be identified with degree 1 without an additional refinement. Operationally, the handoff itself belongs at the strong end: the burn and mint legs must be coupled, or the burned-but-not-minted interval remains a liveness gap. The pattern prevents steady-state co-presence, but concentrates consistency obligations into the handoff, burn finality, mint authorization, and replay resistance.

The formal model fixes degree for a cycle and covers reassignment between cycles. Mid-cycle promotion is outside the present model. Letting the stronger obligation govern during disagreement is a conservative candidate, but committing at the last acknowledgment still requires a failure model. An unavailable or Byzantine domain may leave safety intact while making liveness indeterminate. A single transition authority simplifies the topology, but does not by itself prove the cutover safe.

The naturality result preserves a single chain 0 anchor for admissibility, while multi-hub coherence remains open. Individuation captures the need for coherent degree assignments, but multiple anchors would still require an inter-hub coherence condition even when those assignments agree. Reading chain 0 as a finality anchor adds an operational meaning that the proof does not assign.

There may also be a correspondence between the two classifications, with one distinction. Our table classifies epistemic status, while your tiers classify authority over rules. The majority test could be examined as a candidate sorting rule for the obligation-boundaries question, with degree-forget naturality as a test case. Before that correspondence can be claimed, it needs a separate mapping and proof.

The minting example gives the aggregate question a concrete condition to test. The remaining issues require separate operational refinements before they become claims of the model.

[WGlynn]

You’re right that the identifier boundary already does the work I was worried about. If degree is pinned to the asset identifier and no issuance path can mint a higher-degree unit into an existing identifier’s balance, then the monotone-upward widening I raised has nowhere to enter: a third party can create high-degree units, but cannot impose them on someone else’s holdings. My objection was aimed at a model that computes degree over the commingled balance, and yours doesn’t, so it is answered. The residual worth stating precisely is that the boundary holds exactly as long as identifier assignment is itself outside the reach of the parties who benefit from
widening. That is not a gap in the proof, it is a constraint the deployment has to honor, and it is the first place I would aim the conformance tier.

On whether the epistemic classification corresponds to the authority tiering, I don’t think they are the same object, and the way they come apart is, in my experience, the single most reliable predictor of where cross-domain value leaves. Degree measures how much coupling exists. The authority tier measures how hard that coupling is to break. Those are orthogonal. Nothing in the construction forces a high-degree asset to be protected at a high tier, and empirically the assets that died were precisely the ones whose coupling breadth had outrun the authority securing it. Wrapped claims spread across many chains, epistemic degree high, while the peg that made them redeemable sat behind a movable committee, authority tier low. Wormhole was a guardian-set signature check that got bypassed. Multichain was an MPC key set that was effectively one operator. Ronin was a
validator majority small enough to capture. In every case the coupling was real and the thing holding it was governance-tier, and the distance between those two numbers is where the money went.

That reframes your open question in a way I think is good news for the tower. The correspondence is not automatic, so I would not try to prove it holds. I would make it a proof obligation. The invariant every dead bridge
violated is that raising coupling breadth must raise the tier that secures it: you should not be able to add a coupled live copy without moving the peg’s protection into a tier no ordinary majority can reach. Ifdegree-forget naturality were required to commute with tier assignment, so that forgetting a chain cannot silently drop the authority guarding the coupling you just removed, the tower would encode exactly the invariant that
Wormhole, Multichain, and Ronin each broke by hand. Your Isabelle core is the right home for it, because it is the one place the obligation can be true by construction rather than by an operator remembering to hold it. That is the physics-tier example I would most want to see mechanized, more than degree-forget on its own.

On burn-and-mint not fitting degree-1, I think you are right that it doesn’t, and the reason is that the copy count dips below one. Burn-and-mint is not a single persistent live copy, it is a transition through a vacancy where the asset exists nowhere, degree zero for the length of the burn window. That is why single-live-copy and coupling breadth split the way you drew them: coupling breadth is zero because there is nothing to keep jointly consistent, but the live-copy count is not a steady one, it is one then zero then one. The model wants a floor state below degree-1 for the interval when the burn has fired and the mint has not. And the three obligations you consolidated, finality, authorization, and replay resistance, are exactly the physics-tier guards on that vacancy: finality closes the burn so it cannot reorg back into existence, authorization gates the single permitted mint, replay resistance stops the vacancy from being exited twice. Every real burn-and-mint system spends essentially its whole design budget on that one interval, which is a decent sign it is the load-bearing state and worth a name in the model rather than being smoothed into degree-1.

On dynamic promotion, the failure model I would start from is the one production canonical-messaging systems already run rather than a single transition authority: a bonded validator set with slashing, where the Byzantine safety-liveness tradeoff is not resolved but priced, the bond set above the maximum value extractable from a safety violation. Combined with the conservative latch from the earlier thread, the cycle governed by the stronger-obligation degree and committed only at the last domain to cross, you get a transition rule that fails toward safety and never releases an obligation on the strength of a change some domain has not yet acknowledged. I am building a version of this as canonical burn-and-mint messaging over a bonded validator network with threshold signatures, so I am glad to be a concrete conformance target once the operational refinement is in. The correspondence obligation above is the piece I would most want your machine to check.

[jay-oraclizer]

That is exactly the boundary I meant, and the residual you added is the part worth keeping: identifier assignment, and any later widening operation, has to stay outside the control of the parties that benefit from the widening. It is a deployment constraint rather than a missing theorem, and it is the right first target for conformance.

I agree with the central distinction between coupling breadth and authority strength, and the cases make the point well. Breadth cannot stand in for protection. I would sort the three into different assurance layers, though. Ronin is principally about the authority configuration that was declared, Multichain about divergence between nominal distribution and operational custody, Wormhole about implementation enforcement. No single invariant over declared tier values covers all three, but your own three tiers do: the first is physics-shaped, the second is exactly the conformance tier, the third is implementation verification. I read them as witnesses for the partition rather than for one obligation.

One precision on the proposed formalization. degree_forget moves in the shrinking direction: in the current theory every deg_step transition preserves asset existence pointwise (broadcast_le_exists), while degree_forget removes one domain from the support. If breadth is B and authority strength is A, an admission condition like A >= f(B) isn’t stressed by forgetting while A stays fixed. The dangerous operations are the opposite ones: adding a live copy, lowering a threshold, rotating keys or validators, or changing the authority that can perform those updates. Those are issuance, deployment, or governance transitions outside the current tower, so I think the correspondence obligation belongs at that boundary first. Naturality may still earn its place once the tier assignment and its transition map are defined. Without them the present form is under-specified.

The vacancy observation is useful too, though I would not classify it below degree 1. Degree measures coupling breadth; vacancy measures copy presence over the burn-and-mint lifecycle. The empty state is representable in the present carriers, but the regulatory step relation can neither enter nor leave it on purpose: deg_step is disabled when the hub state is absent, and process_at_degree is the identity there. degree_forget can erase a non-hub chain’s holdings, and it can yield empty support when that chain held the only copy, but it is a projection between degree carriers rather than a lifecycle transition. What the model lacks is an explicit pair of existence-changing operations that enter and exit vacancy deliberately, with finality, authorization, and replay protection as their enabling conditions.

A bonded validator set with slashing is a concrete candidate failure model for the authority axis, not a complete one. The maximum extractable value may be dynamic, and a slashed bond can compensate economic loss without restoring a legal effect. The conservative latch, cutover atomicity, key custody, and implementation conformance stay separate obligations.

On the conformance offer, the most useful thing I can say is that you may not need me for the first step. The locales are generic and public. They are stated over arbitrary state machines, so if you instantiate them for your domains and discharge the obligations, the existing theorems transfer with nothing new from my side. That is probably the fastest way to find out whether the tower says anything useful about your system, and it does not wait on me.

On mechanizing the correspondence obligation itself, I am going to leave that one where it is for now. I think it is a good idea, and you are right that it is the shape of the invariant those three failures broke. But the part that gives it content is the failure model, and that is closer to your work than mine. It also sits outside the line I am working on, which is regulatory state synchronization rather than the security tiering of the domains underneath. If a public specification appears later I would be glad to read it and say where the present theorems reach and where they stop, which is a statement about the model rather than a verdict on your system. If you do instantiate the locales, I would be curious which obligation gives you the most trouble.

[WGlynn]

Your no-op reframe of vacancy is the part I keep returning to, and I will hold your Section 5 standard: everything of mine below is labeled built, designed, or open.

I can offer candidate operational semantics rather than agreement in prose. The accounting layer of the canonical burn-and-mint in the public VibeSwap repo (contracts/messaging/SupplyAccountant.sol) implements the lifecycle you specified, and your three conditions map one for one, each with its own status. Replay is duplicate-nonce rejection in both directions, discharged, but only in a per-chain projection I will scope below. Authorization is an onlyHub writer gate specified as a bonded threshold-signed validator set but bottoming out today in an owner-settable hub address pointing at an unimplemented orchestrator, so it is open. Finality is an explicit pending state that confirmOutboundBurn moves into the conservation ledger or reverseOutboundBurn returns, and its trigger is a hub attestation the chain cannot verify, so the finality assumption did not disappear, it moved into the trigger, and it is open.

That last point forces one refinement on your framing. Because finality arrives after the burn, vacancy entry is provisional, so the honest model is three-state, pending then confirmed or reversed, not a binary enter and exit, and the ledger has to carry the pending mass explicitly rather than net it away, checkable on-chain via checkInvariant. I should be precise about checkable: the reverting check exists in the contract, but its intended caller is core batch settlement, and that wiring does not exist yet, so enforcement as distinct from inspection is open, not built.

The scope of that invariant is the strongest objection to my own offer, and I would rather file it than have you find it in your first hour of instantiation. What the contract holds is the per-chain projection of your vacancy pair. Global conservation, one burn implies at most one mint anywhere, is a property of the indexed family of these ledgers plus a hub-honesty assumption the family cannot express: a hub that mints one burn attestation on two destination chains keeps every per-chain invariant green, because each destination’s consumed-nonce set is independent and no cross-destination check exists at this layer. So cross-destination replay of a single burn is not expressible here, let alone discharged, a third undischarged obligation living in the same unbuilt hub as authorization and finality. The contract’s header concedes it: the global invariant is the aggregate of the per-chain ones, v0.1 leaves cross-chain reconciliation to off-chain monitors, and the designed-not-built closure is a committed invariant beacon that would let any chain prove its accounting consistent with a global root.

Status, precisely: built and tested at the accounting layer, interface-only at the hub in front of it, so none of it is deployed, and by your own sorting of Wormhole the implementation tier is exactly where an unverified orchestrator fails. I will take your invitation literally, instantiate the locales against this model, try to discharge the preservation obligations, and report where they fail, with those three gaps as the first candidates. The failure report is worth more than any success claim I could make.

The refusal discipline I can witness with merged code from the other system I work on, whose node carries an amendment gate (node/src/amendment.rs, public) that does at the governance boundary what your model does at the vacancy boundary: physics-layer change is refused by named fiat rather than a faked proof, the existence-changing operations are typed so the gate can name them and then refused as constitutionally pending because the rules that would secure them are not in code yet, and only the permissive direction of a parameter change is flagged while the restrictive direction is safe by construction. I will not call that an isomorphism with your over-provisioning versus no-downward-safety pair, since nothing on my side is mechanized against your tower and recognizing the same word is not deriving the same object, and the honest cut is sharper still: both gates were built by the same team for different substrates, so their shared one-way-safe shape is evidence the asymmetry survives a substrate change, not evidence of independent convergence. The refusal gate is built and tested; the safe operations it refuses are designed, not built.

On the correspondence you set aside as under-specified, a candidate definition rather than the aspiration restated. Let the tier of an authority be its cost-to-corrupt, composed from quantities a validator registry already carries (bond floor, signing threshold, unbonding delay, slash exposure), and let the transition map be the parameter-change operations that move them. Then the invariant those three failures broke becomes a checkable conformance obligation, never a physics theorem: a new coupled live copy must come with a monotone non-decrease in cost-to-corrupt. The typing needs one repair, since deg counts copies while tier is economic: a mediating monotone map r from degrees to tiers, r(d) the minimum cost-to-corrupt to support d copies, so the transformation is r∘deg => tier with components r(deg(A)) <= tier(A). Upgrading monotonicity to naturality then costs only those components plus functoriality of tier, after which the squares commute for free because a poset codomain is thin. That leaves a decision on your side I cannot make: whether r lives inside your tier assignment or is a new object with its own obligations, and if your codomain is not thin then I have guessed wrong and would rather you name its morphisms than keep assuming a poset. Multichain does not live in this model at all: the registry-visible quantities were fine while custody lied, so it is a soundness failure of the abstraction functor from declared state to operational custody, an instance of your axiomatic-base residue, which means the conformance check is sound only relative to a custody assumption it cannot witness from inside. The only discipline I know for that base is to keep it named, minimal, and versioned, applied to ourselves first: our base today carries an owner key on the bond floor and upgrade path, and by the Multichain argument custody fidelity as a second explicit entry until something like proof-of-custody discharges it out of model.

One question before I start, because it sits in your judgment not mine. A pending burn is neither vacancy nor a live holding: it has left the source balance but not entered the conservation ledger, and it can still return. Would you model pending as a distinct holding inside the carrier, so a burn in flight still counts toward the degree bound, or as a refinement below the tower that the coarse model quotients away, with the three-state lifecycle appearing only in the conformance proof that the implementation refines your binary enter and exit? The two choices seem to put the finality condition on opposite sides of your proven versus design boundary, and I would rather learn which before I find it the hard way inside Isabelle.

[jay-oraclizer]

You applied the built/designed/open distinction to your own system without being prompted, then surfaced the strongest objection to your own offer yourself. That is the discipline this problem needs, and it saved this thread a round. Honestly, it also raised the bar for how I should reply. So let me answer in kind, including corrections to my last post.

You’re right about the three-state post-burn lifecycle, and my binary vacancy language in the last reply was too coarse. Including the pre-burn position, the concrete path when source finality arrives after the burn is Live -> Pending -> Confirmed | Reversed. The conservative abstraction is: Live -> Pending stutters at the holding level; Pending -> Confirmed performs the abstract handoff; Pending -> Reversed restores the concrete source position while the abstract holding never left the source. So the burned-but-unminted interval is not an unowned abstract hole. It is a concrete refinement obligation: pending mass must remain accounted for and unavailable, and only valid terminal evidence may resolve it.

The two-destination case is the one I kept coming back to. If two destinations keep independent consumed-nonce sets, the same source burn can be accepted as first-seen by both while both local accounting checks stay green. The missing statement is global: one source burn event may be consumed by at most one destination across the whole destination family. Independent per-chain replay checks alone do not imply that theorem. It is related to the multi-hub coherence gap I left open earlier, but it is not the same statement. Any adequate instantiation has to reject that execution; otherwise, the local accounting layer has not refined a global invariant.

One correction I owe you concerns direct reuse. The polymorphic state_preservation locale and its category laws are a plausible framework once the relevant transition obligations are discharged. The tower layer is not polymorphic in the same way: F k, deg_carrier, and the naturality square are built over the regulatory global_state. An instantiation of your lifecycle would therefore need its own concrete carrier and an abstraction map into the existing holding model. Whether the tower can then be reused unchanged, partly reused, or must be rebuilt is something the instantiation itself has to settle, not something I should promise in advance. This does not refute the current theorems. It identifies refinement obligations that the current tower does not state.

I’m still not treating r(degree) <= tier as a theorem. Until tier is derived from an explicit failure model, including quorum, upgrade authority, verifier bypass, finality, and key rotation, the inequality is an admission-policy placeholder. Your bonded-validator model may become evidence for such a definition, but it is not one yet. The amendment-gate analogy is useful at the structural level, and keeping it short of an isomorphism is exactly right.

So my corrected position is narrower than the one I gave before: the abstract preservation framework may still be useful, direct tower reuse has not been established, and the two-destination execution remains the decisive test of any claimed global accounting refinement. When you have that failure report, I’d genuinely like to read it. Where the refinement fails will tell you something about the accounting layer and me something about where the tower’s actual boundary lies.