A Mechanized Functor Tower for Cross-Domain State Preservation

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? 1 post - 1 participant Read full topic