From a Separate Entry to a Functor Tower: Folding the Composition into Cross-Domain State Preservation

TL;DR

• We retire the separate-entry-plus-relocation skeleton locked in by the prior design article, and move the work into revision 3 of the existing Cross_Domain_State_Preservation entry.
• The point of the move is not to split the composition into a new package but to complete a single cross-domain state preservation functor. Three theorems (identity preservation, composition preservation, associativity) close the category axioms and force “Functor” to be a theorem rather than rhetoric.
• In the same entry, we formalize the sync degree hierarchy as natural transformations between functors. Degree demotion is \(\eta_k: F_{k+1} \Rightarrow F_k\), and the composition of natural transformations makes the whole ladder cohere.
• The name Oraclizer comes from Turing’s oracle machine; the organizing skeleton of the degree hierarchy comes from Turing degrees. But the sync degrees inherit none of the properties of Turing degrees. What transferred is a single skeleton: organizing a hierarchy by a reduction relation.

A Decision That Becomes Prophecy, a Decision That Becomes Record

The prior design article, Designing Compositional State Assurance: Three Locales and One Glue, locked in a design and closed with a single note: if hindsight proved those decisions right, the article would read as prophecy; if wrong, as record. Either way its place would remain, and both prophecy and record serve the integrity of the verification work.

The outcome was both. The three-layer locale design became prophecy. It survived intact. The separate entry and the four-file relocation became record. They were scrapped. We do not edit the body of a published article for stability. Instead, this article corrects what changed.

Two things changed. First, rather than spinning up a new entry to hold the composition, we turned the structure toward completing the existing entry as a functor. Second, we reframed “a composition framework” as the completion of a cross-domain state preservation functor. And one thing was added: we decided to formalize the sync degree hierarchy in the same entry, as natural transformations. Half of this article is about what changed and what survived; the other half is about where the degree-hierarchy idea came from and how it is formalized. The latter is the article’s center of gravity.

From a Separate Entry to Functor Completion

First, a recap of the scrapped decision. The prior design created a new entry, Compositional_State_Assurance, and chose a seven-file layout that relocated the four .thy files of the two completed properties (State_Preservation, Regulatory_Instance, Priority_Resolution, DQuencer_Instance) into it. That article weighed two alternatives: relocating the four files, or importing the existing entry. The import path carried three costs. A change to the existing entry would ripple into the new entry’s build; a verification-time skew could open between the two entries; a reviewer would have to verify both entries together. To avoid these three costs, it chose relocation.

Revision 3 voids the comparison itself. With no two entries, there are no costs between two entries. It is a monotone update that adds three new files (Composition.thy, Functor_Laws.thy, Hierarchy.thy) to the existing Cross_Domain_State_Preservation entry. The four existing files stay exactly where they are, their theorems untouched. The only external import added is ADS_Functor. The three import costs and the “looks like copy-paste” of relocation vanish at once.

Figure 1: From a Separate Entry to Revision 3

But this transition is more than cost avoidance. The prior article saw the composition as a new subject, a new unit of contribution: a package of safety plus liveness plus composition plus Canton integration. Revision 3 sees it differently. The composition is not a new package; it is the completion of the same entry. The grounds were already in the first article of the series. Bridging Safety and Liveness: A Prelude to Compositional Verification called the first completed property a functor pattern. Closing that functor under the category axioms is what the composition actually is. Seen as completing the entry into a functor, the composition is not a new asset to break off but the last piece of an existing one.

Visibility of the academic asset also favors one entry. If the functoriality asset scatters across two entries, its outline as a single cross-domain state preservation functor blurs. One entry completed into a functor over time states the identity more sharply: a cross-domain functor on the same axis as Lochbihler and Marić’s single-domain authenticated-data functor. Scattering cuts visibility; concentration builds it.

From Rhetoric to Theorem: The Cross-Domain State Preservation Functor

In revision 2, currently under review at the Archive of Formal Proofs, we temporarily dropped the word Functor from the entry title. The reason is simple. At that point the code had no functor laws. There were state-preservation morphisms satisfying naturality, but no theorem forcing those morphisms to form a functor: no preservation of identities, no preservation of composition, no associativity. Putting “Functor” in the title without the theorem was over-claiming, and we declined to.

The core of preservation_compose, gluing two naturality squares into the composite morphism’s square, worked out on a meeting-room whiteboard.

Revision 3 closes this gap with three theorems. The objects are state machines (states, actions, transition, terminal), and the morphisms are (state_map, action_map) pairs satisfying naturality. Over this category:

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

This nails that the identity morphism is a preservation morphism. In functor terms, \(F(\mathrm{id}) = \mathrm{id}\): applying the preservation structure to an identity returns an identity.

theorem preservation_compose:
  assumes "state_preservation S_a A_a T_a term_a  S_b A_b T_b term_b  f f'"
      and "state_preservation S_b A_b T_b term_b  S_c A_c T_c term_c  g g'"
  shows   "state_preservation S_a A_a T_a term_a  S_c A_c T_c term_c
                              (g ∘ f) (g' ∘ f')"

This nails that the composition of preservation morphisms is again a preservation morphism. \(F(g \circ f) = F(g) \circ F(f)\): preservation follows preservation through composition.

theorem preservation_assoc:
  assumes "state_preservation S_a A_a T_a term_a  S_b A_b T_b term_b  f f'"
      and "state_preservation S_b A_b T_b term_b  S_c A_c T_c term_c  g g'"
      and "state_preservation S_c A_c T_c term_c  S_d A_d T_d term_d  k k'"
  shows   "((k ∘ g) ∘ f = k ∘ (g ∘ f)) ∧ ((k' ∘ g') ∘ f' = k' ∘ (g' ∘ f'))"

This nails associativity of morphism composition, the last piece of the category axioms. Together the three theorems complete a category with identities and associativity, and over it establish that cross-domain synchronization is functorial. “Functor” is now not a decoration in the title but a proposition the code forces. With the laws in place, the entry title is restored to Cross-Domain State Preservation Functor.

There is a reason all three are needed. preservation_compose alone amounts to a single functor-like property. When a reviewer asks “is this a functor, or one theorem that looks like one?”, the answer holds only once identities and associativity are nailed down too. preservation_assoc follows almost directly from associativity of function composition, since state_map and action_map are functions. The cost is low and the standing rises sharply. The core of preservation_compose is to glue two naturality squares into the square of the composite morphism, reusing the pattern from the completed preservation proofs.

Figure 2: Three Laws That Make Cross-Domain Preservation a Functor

This is the cross-domain analogue of the “Merkle functors are closed under composition” that Lochbihler proved for single-domain authenticated data. The difference is the axis. ADS_Functor treats the authenticity of data structures within one domain; we treat the preservation of state transitions across domains. Same functor language, different axis.

As a byproduct of the completion, the already-completed preservation instances automatically become actual morphisms of this functor. Preservation between differing action vocabularies (escalation_preservation), the bidirectional bridge linking on-chain and off-chain (onchain_daml_bridge), and one-directional layer preservation (forward_layer_preservation, backward_layer_preservation) are all instances of state_preservation, so they are non-empty as morphisms of the functor. The risk of a vacuously true functor with no morphisms disappears here.

The Three Layers Were Not Abandoned

One thing must be clear about the transition. This is not an abandonment of the composition design. The three-layer locales locked in by the prior article survived intact. The three locales of Composition.thy are unchanged.

locale guarded_invariant =
  fixes carrier :: "'s set"  and step :: "'s ⇒ 'op ⇒ 's option"
    and ops :: "'op set"  and inv :: "'s ⇒ bool"
    and guard :: "'s ⇒ 'op ⇒ bool"
  assumes step_closed:
            "⟦s ∈ carrier; op ∈ ops; step s op = Some s'⟧ ⟹ s' ∈ carrier"
    and   guarded_preservation:
            "⟦s ∈ carrier; op ∈ ops; inv s; guard s op;
              step s op = Some s'⟧ ⟹ inv s'"

locale eventual_discharger =
  fixes schedule :: "nat ⇒ 'event"  and discharges :: "'event ⇒ bool"
    and window :: nat
  assumes window_positive:   "window > 0"
    and   bounded_occurrence:
            "∀t. ∃t'. t ≤ t' ∧ t' < t + window ∧ discharges (schedule t')"

locale safety_liveness_composition =
  safe: guarded_invariant carrier step ops inv guard +
  live: eventual_discharger schedule discharges window
  for carrier step ops inv guard schedule discharges window +
  fixes realize :: "'event ⇒ 's ⇒ 'op option"
  assumes realize_discharges:
            "⟦s ∈ carrier; discharges ev; realize ev s = Some op⟧
              ⟹ op ∈ ops ∧ guard s op"
    and   realize_progresses:
            "⟦s ∈ carrier; inv s; discharges ev; realize ev s = Some op⟧
              ⟹ ∃s'. step s op = Some s' ∧ inv s'"

The domain-independence principle (that priority, leader, epoch, Byzantine, blockchain do not appear in this file) holds, as does the design in which the two glue definitions (state_join, state_refines) lift ADS_Functor‘s merge and blinding to the state level. Both glue definitions were already fixed and stated in the prior design article.

Two things changed. First, the ADS_Functor composition and glue that the prior article meant to place in a separate Merkle_Composition.thy are merged into Functor_Laws.thy, alongside the functor laws. What functor composition needs is merkle_interface and state extraction, and liveness composition is handled separately on the Composition.thy side, so lowering the coupling reduces the risk of type collisions. Second, the degree-hierarchy file Hierarchy.thy is newly stacked on top.

So the transition did not discard the composition design; it changed the entry structure and stacked a functor layer and a degree layer on top. The two jobs set in the first article of the series, lifting conditional safety to unconditional convergence and internalizing the external honest_progress assumption as a system-internal property, are still carried by this composition. The shape of the final theorem the composition aims to close is unchanged as well.

theorem oraclizer_guarded_bounded_convergence:
  assumes "card nodes ≥ 3 * f_max + 1"
    and   "card (byzantine_nodes nodes) ≤ f_max"
    and   "fair_authorities schedule window"
    and   "finite_domain gs₀"          (* valid_state gs₀ is not assumed *)
  shows "∃t ≤ convergence_bound gs₀. ∃gs_t.
           evolves_to gs₀ t gs_t ∧ valid_state gs_t"

That the statement has no valid_state gs₀ is the decisive difference from the combined_safety_liveness theorem of the two completed properties (which carries valid_state as a premise). Where the earlier result was conditional safety, revision 3 aims at unconditional convergence. This article is the place to correct that composition’s entry structure and functor framing, not to reopen the composition itself.

The Origin of a Name and the Lineage of Degrees

Now to the center of gravity: the third piece added in revision 3, the sync degree hierarchy. Behind the decision to formalize it lies a single line of intellectual lineage. Setting that lineage down honestly is the purpose of this section.

The Name Oraclizer

Start with the name. Oraclizer comes from Turing’s oracle machine.

In May 1938, at Princeton and under Alonzo Church, Turing completed his PhD thesis Systems of Logic Based on Ordinals, published the next year in the Proceedings of the London Mathematical Society. Ordinal logic, a route around Gödel incompleteness, was the thesis’s main subject, but one concept introduced almost in passing became a tool of later computability theory: the oracle machine, the o-machine. It attaches a black box called an oracle to an ordinary Turing machine; the oracle answers membership in some set, and that set may be one no machine can decide. Turing did not go further into the oracle’s nature, fixing it in a single phrase. It “cannot be a machine.” It is a device that supplies, from outside the machine, answers the machine cannot compute on its own.

It is no accident that the blockchain oracle inherits this name. A blockchain is a closed, deterministic system, and a chain cannot know on its own the off-chain truth that lies outside it. The device that injects that answer from outside is the blockchain oracle. In answering, from outside, what the machine cannot answer on its own, the two oracles sit in structurally the same place.

But this lineage is one of name and idea, not formal identity. Turing’s oracle answers a problem no machine can solve (unsolvability). The external truth a blockchain oracle answers is computable elsewhere. The two are not the same object. What we connect is the bloodline of one idea: bringing an answer from outside the machine.

Take one more step. A conventional data oracle, a price feed and the like, is a degenerate form of this idea. It reports observations one-directionally from one domain toward another; it cannot bind the states of two domains. As we set out in the earlier classification study Sync Degree Hierarchy: Classifying What Assets Demand from State Synchronization, such a structure is by definition capped at one-directional observation. A fuller oracle, then, one that makes a chain and its off-chain move as a single causal unit, must bind the states of two domains bidirectionally and atomically. The name Oraclizer comes precisely from being an oracle state machine that executes this fuller oracle. The intent in the name is a machine that performs the function of a true oracle, not a feed that carries data.

The Clue for a Degree Hierarchy: Turing Degrees

The oracle machine left more than a name. It gave rise to a hierarchy, and that hierarchy became the design clue for the sync degree hierarchy.

The relation that arises naturally from the oracle machine is Turing reducibility (\(\leq_T\)). A set A is Turing reducible to a set B when A is decidable by a machine that uses B as an oracle. The relation first appears in the relative computability of section 4 of Turing’s thesis. If there is an oracle answering B, then A is solvable too: A is no harder than B.

What stands on top of this reduction relation is the hierarchy of degrees of unsolvability, commonly called Turing degrees. Sets that reduce to each other are grouped into one degree, and the degrees are partially ordered by \(\leq_T\). This structure is due not to Turing’s thesis but to Emil Post (1944), and was developed into an upper semi-lattice by Kleene and Post (1954). The name “Turing degrees” honors Turing because the reduction relation organizing the hierarchy is his.

What transferred is one skeleton. The idea that when you build a hierarchy of strengths, you organize it by a reduction relation rather than a numeric ladder: \(x \leq y\) means “y subsumes x, y can simulate x,” and the hierarchy is induced from that relation. This is exactly the clue we reached for when trying to classify the synchronization strength an asset demands. The one-directional containment, where a system of higher degree safely absorbs the demands of a lower degree but not the reverse, is precisely the shape of a hierarchy organized by reduction. It was the moment a mathematical skeleton matched the intuition.

A margin note beside a 1939 reduction relation, tying Turing reducibility to the sync degree chain S₃ ⊇ S₂ ⊇ S₁ ⊇ S₀ and to the demotion natural transformation.

An Honest Difference

Here a point must be made plainly. Sync degrees are not Turing degrees. Only the skeleton transferred; the properties are entirely different.

Turing degrees are infinite, uncountable, and form an upper semi-lattice. What they measure is unsolvability, and a higher degree is harder to compute. They contain a jump operator, are partly dense, and have no greatest element. Sync degrees are a total chain of four finite steps (S₀, S₁, S₂, S₃). What they measure is synchronization capability and requirement, and a higher degree means stronger state coupling. The reduction relation S₃ ⊇ S₂ ⊇ S₁ ⊇ S₀ expresses the asymmetry that over-provisioning is safe and under-provisioning carries no guarantee.

Even the meaning of the order differs. Turing’s \(\leq_T\) is “is reducible to,” a comparison of computational difficulty. The sync degrees’ ⊇ is “capability subsumes requirement,” a containment between system capability and asset requirement. So when we say we took this from Turing, it points honestly to one thing. The skeleton that a reduction relation organizes a hierarchy of strengths, that one thing. Lattice structure, uncountability, the jump, density: none are inherited. Blur this difference and inspiration becomes overstatement.

A Functor Tower and Natural Transformations

How, then, is a sync degree formalized? Not by mimicking the recursion-theoretic structure of Turing degrees (that would be the wrong object), but in the language of category theory. For each degree we place a preservation functor \(F_k\) restricted to the state-coupling strength that degree demands (\(F_3\) the strongest, \(F_0\) the weakest), and connect them by natural transformations.

The core is to formalize demotion as a natural transformation. Dropping a higher-degree state view to a lower degree is discarding information, and this aligns with the direction of state_refines, which lifts ADS_Functor‘s blinding to the state level. Demotion is blinding, the hiding of information.

definition degree_forget :: "nat ⇒ global_state ⇒ global_state"
  (* degree demotion: forget a higher-degree state view down to a lower degree *)

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

degree_natural_transformation nails that \(\eta_k: F_{k+1} \Rightarrow F_k\) is a natural transformation between functors: that demotion is compatible with the naturality of preservation, that transitioning then demoting equals demoting then transitioning (the naturality square commutes).

theorem nt_compose:
  "natural_transformation (F (Suc (Suc k))) (F k)
       (degree_forget (Suc k) ∘ degree_forget (Suc (Suc k)))"

nt_compose nails that the composition of natural transformations is again a natural transformation. This is decisive. By this theorem the whole \(S_3 \Rightarrow S_2 \Rightarrow S_1 \Rightarrow S_0\) ladder becomes not a bag of point-to-point forgetful maps but a single structurally coherent hierarchy.

The monotonicity of the hierarchy splits into two theorems.

theorem hierarchy_monotonicity:
  assumes "asset_degree aid ≤ system_degree"  and "valid_state gs"
  shows   "valid_state (process_at_degree system_degree gs aid)"

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

hierarchy_monotonicity says formally that when an asset’s degree is at most the system’s degree, processing does not break preservation (over-provisioning is safe); no_downward_safety says that when an asset’s degree exceeds the system’s, there is no guarantee. This is why the degree hierarchy is an enforcement, not a classification label. The boundary between S₁ and S₂ is causal consistency grounded in Lamport’s happened-before, and boundary_well_defined nails that this boundary is well defined over (asset, system) pairs.

Figure 3: Two Reduction Hierarchies, One Shared Skeleton

The difference from ADS_Functor sharpens here. ADS_Functor proved that functors are closed under composition (over products, sums, function spaces). But it does not treat a hierarchy of functors and the natural transformations between them. That territory is what degree_natural_transformation and nt_compose open. It is the point where the work moves past being on the same axis as ADS to being territory ADS did not enter.

And here the two threads meet. The functor completion and the degree hierarchy stand on the same categorical skeleton. Close a functor under the category axioms, then stack those functors by degree and join them with natural transformations. The idea of a reduction hierarchy taken from Turing degrees is realized formally as natural transformations between functors. The inspiration came from recursion theory, but the rigorous object is one of category theory. That the functor completion and the degree stratification enter the same entry is not coincidence but structural necessity.

What It Does Not Promise

The soundness of a design also shows in being clear about what it does not promise. Revision 3 does not prove the following.

The abstraction that treats synchronization as atomic (atomic sync) is left in place. An intermediate state propagated to only one domain is outside the model. This assumption is released incrementally in subsequent properties of our verification program, through preemptive-lock correctness and cross-chain finality. The causal-consistency boundary of the degree hierarchy shares the same atomic abstraction, so that release weakens the atomic assumption on both the functor laws and the degree hierarchy together. Partially synchronous network models, dynamic domain topologies, and starvation freedom in an open system are not treated. A formal refinement between model and Rust implementation is also not an output of this stage.

Our stance on the gap between model and implementation rests on three defenses: the independent value of model-level verification (the Heard-Of model tradition), the FORMAL_MODEL_MAPPING.md published with the GitHub repository, and the incremental assumption release of subsequent properties. And the most important distinction, stated again. Proving functor laws and nailing natural transformations closes theorems inside the model; it is not the same as a guarantee that the system is safe. What we close is a model, and how that model corresponds to the implementation is separate, incremental work.

Closing

The prior design article, locking in its decisions, said hindsight would decide whether it read as prophecy or as record. The outcome was both. The three layers survived as prophecy; the separate entry and the four-file relocation were scrapped as record. What changed is the entry structure and the framing, not the skeleton of the composition. The composition resettled not as a new package but as the completion of a cross-domain state preservation functor, and three theorems, nailing identities and associativity, turned “Functor” from rhetoric into theorem.

What this article added is the record of a lineage. The name Oraclizer comes from Turing’s oracle machine; the organizing skeleton of the degree hierarchy comes from Turing degrees. But sync degrees inherit none of the properties of Turing degrees. What we formalized is not recursion-theoretic degrees but a tower of functors joined by natural transformations. Stating precisely that inspiration and formalization come from different mathematics is the only way not to overstate the inspiration.

One question remains. The skeleton of a hierarchy organized by reduction crossed from Turing’s computational difficulty to our synchronization strength. Where else can this skeleton cross? For distributed systems whose coupling strength differs by steps, say publish-subscribe coupling strength or replication consistency levels, can the same form, joining degrees by natural transformations, apply unchanged? Whether the functor laws close without sorry, where the naturality squares stalled and how they were discharged: that record belongs to a separate article. This article sits apart from that proof record; its work here is to correct the design and set down the lineage.

References

1. Turing, A. M. (1939). Systems of Logic Based on Ordinals. Proceedings of the London Mathematical Society, s2-45(1), 161-228. Link
2. Post, E. L. (1944). Recursively enumerable sets of positive integers and their decision problems. Bulletin of the American Mathematical Society, 50(5), 284-316. Link
3. Kleene, S. C., & Post, E. L. (1954). The Upper Semi-Lattice of Degrees of Recursive Unsolvability. Annals of Mathematics, 59(3), 379-407. Link
4. Mac Lane, S. (1998). Categories for the Working Mathematician (2nd ed.). Graduate Texts in Mathematics, vol. 5. Springer. Link
5. Lochbihler, A., & Marić, O. (2020). Authenticated Data Structures as Functors in Isabelle/HOL. FMBC 2020, OASIcs vol. 84. Archive of Formal Proofs entry: ADS_Functor.
6. Abadi, M., & Lamport, L. (1995). Conjoining Specifications. ACM Transactions on Programming Languages and Systems, 17(3), 507-534. Link
7. Kim, J. (2026). Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL. arXiv:2604.03844. Link