Sync Degree Enforcement: What Turns a Classification Into a Constraint

TL;DR

• Our earlier work built a hierarchy that classifies how much state synchronization an asset demands, from S₀ to S₃, and left three items open: monotonicity unproved, the S₂/S₃ boundary undecided, and dynamic degree change unresolved. This article closes two of them and partially closes the third.
• The central result is sync degree enforcement pushed to the point where violating the hierarchy stops the code from compiling. A pairing whose asset degree exceeds its path degree cannot be expressed at all inside Rust’s type system. Wrong routing turns from a runtime incident into a build failure.
• That became possible because monotonicity is now proved in both directions. Where system capability dominates what the asset requires, processing preserves the global validity invariant, so over-provisioning is safe. Where capability falls short, a state exists that defeats every preservation guarantee, so under-provisioning is not. Both are mechanized, published on GitHub, and awaiting AFP registration.
• The logical form of the second result decides everything. It is an existential statement, not “this might fail,” which makes wrong routing a structural consequence rather than a probabilistic one. The response changes accordingly: you do not monitor for it, you make the pairing unreachable.
• OSS branches into four processing paths by degree. S₀ writes to the registry and stops, S₁ propagates one way with no locking and no proof, S₂ runs Soft BVC with best-effort mutual rollback, and S₃ runs Full BVC with mutual rollback enforced. Early operation nonetheless runs every asset through S₃ in single mode, because three of the four paths are S₃ minus something and the origin of the subtraction gets validated first.
• The deferred S₂/S₃ boundary is settled on whether mutual rollback is enforced. It is a predicate of its own rather than an intensity parameter, and collapsing the two would break the ordering relation that the monotonicity statement depends on.
• What remains open is dynamic degree change. Static reassignment is closed; the safety of the instant a regulatory action promotes an asset mid-lifecycle is not.

---

1. What Does a Classification Do on Its Own?

In earlier work we defined the sync degree hierarchy [1]. It sorts the strength of state synchronization an asset needs to perform its financial function into four levels, S₀ through S₃, and argues those four form a reduction relation rather than a scoring ladder. That article also left three items on the table. Monotonicity went unproved, the criterion separating S₂ from S₃ stayed undecided, and whether a degree can change across an asset’s lifecycle remained an open question.

Before working through any of them, one question comes first. What does a classification do on its own?

Nothing.

Say the asset metadata records S₂. What happens if the system processes the asset without reading that field? Nothing happens. The asset gets processed, a result comes back, and the record touches none of it. The classification survives as a comment: developers can read it, the system does not.

This is where classification schemes usually end up. The definition lives in a document, the code carries an enum field matching that definition, and the field shows up in logging and dashboards. The classification exists as vocabulary in the design docs and plays no part in the execution path.

So the question this article answers is this one. What else is needed before ignoring the classification actually blocks something?

Call a marking that costs nothing to ignore a label, and a marking that blocks something when violated an enforcement. What the earlier work produced was a label. Turning a label into enforcement decomposes into three conditions, and together they define what sync degree enforcement requires.

First, the paths have to actually diverge. If assets of different degrees run through the same code path, the degree decides nothing by definition. Without branching, a classification is an observation.

Second, choosing wrong has to be harmful. Even with branching, if every path produces the same outcome then a routing error is a performance problem and not a correctness one. Enforcement requires that the wrong path genuinely break something, and that the breakage not be a matter of luck.

Third, the verdict has to land before execution. Catching a bad route while it runs is after-the-fact detection. Enforcement means the bad state was never reachable to begin with.

The hierarchy from the earlier work met none of the three. It had definitions. This article fills the three conditions in order.

2. Four Paths

2.1 What Branching Actually Means

Start with the first condition of sync degree enforcement. Inside OSS, the Sync Degree Router looks up an asset’s degree and delegates the request to one of four handlers. These four are not the same code with different parameters. They are different mechanisms.

Degree	Path	Mechanism
S₀	State Registration Only	Registry write and nothing else. No synchronization cycle exists.
S₁	Lightweight Observation Path	One-way propagation. No locking, no GKR proof, plain state hash update.
S₂	Soft BVC	Preemptive lock plus GKR proof plus bidirectional commit. Mutual rollback is best-effort.
S₃	Full BVC	Preemptive lock plus GKR proof plus bidirectional atomic commit. Mutual rollback enforced.

Worth noting: S₀ and S₁ never enter the BVC pattern at all. Earlier work defined BVC as the mechanism realizing atomic state binding [2], and on two of these paths that mechanism is absent wholesale. Skipping the preemptive lock for an S₁ asset is not an optimization. There is nothing to lock. For an asset that only demands one-way observation, a lock binding two domains answers a requirement that was never made.

That is what it means for branching to be real. Each path runs a different set of operations, things get omitted, and the omissions follow from the definition of the degree.

Figure 1: Four Processing Paths by Sync Degree

2.2 Why We Start Without Branching

And yet we do not turn branch mode on at the start. In its early phase OSS runs in single mode, processing every asset as S₃ Full BVC. The degree router exists, but it records metadata rather than splitting paths.

That decision needs justifying, since defining a hierarchy and then not processing by it looks contradictory.

Branching pays off only when you are dividing something already validated. S₂ Soft BVC is Full BVC with enforced mutual rollback removed, and the S₁ light path removes locking and proofs on top of that. Three of the four paths are defined by subtraction from S₃. Subtract before the original has been validated and, when something breaks, you cannot tell whether the fault lies in the BVC pattern or in the subtraction.

There is a tradeoff here. Single mode forces the full BVC cycle onto S₀ assets too, which is plainly wasteful: registering one static NFT drags in two-domain locking and GKR proof generation. We pay that cost deliberately in the early phase. What it buys is a failure surface with exactly one pattern to watch.

Which raises the next question on its own. Why do we believe single mode is safe? Processing every asset as S₃ means sending S₀ assets down the S₃ path. On what grounds is that safe?

That is precisely the proposition the earlier work left unproved: monotonicity.

3. That the Wrong Path Is Not Harmless

3.1 Two Directions

On to the second condition, which requires that choosing the wrong path be harmful. It is really two independent questions.

Over-provisioning: system capability exceeds what the asset requires. An S₀ asset sent down the S₃ path. The system imposes a coupling the asset never asked for. Is that safe?

Under-provisioning: system capability falls short of what the asset requires. An S₃ asset sent down the S₁ path. The asset asked for a coupling the system does not supply. Is that dangerous?

Intuition answers immediately. The first is safe, the second is dangerous. Strong guarantees do not break weak requirements; weak guarantees cannot meet strong ones.

Intuition is not grounds, though, and that goes double for the first answer. Saying over-provisioning is safe leans on a general principle, that a strong guarantee does not harm a weak requirement, and whether that principle always holds is not self-evident. The mutual rollback an S₃ system forces onto an S₂ asset is something that asset never requested. How do we know an unrequested rollback does not corrupt the asset’s meaning?

3.2 Hierarchy Monotonicity

That question is now formally closed. The proof of Synchronization-Degree Hierarchy Monotonicity is complete and published on GitHub, and it is currently awaiting AFP registration [3].

Both directions are proved.

The over-provisioning direction. When the system’s capability degree dominates the asset’s required degree, processing preserves the global validity invariant. Under that condition, every required chain holding the asset agrees on its regulatory state afterwards. Layering an unrequested strong guarantee does not corrupt the asset’s meaning. Over-provisioning is safe.

This is the formal ground for single-mode operation. Processing every asset as S₃ over-provisions all of them, and over-provisioning is safe, so single mode is safe. What the previous section called a deliberately paid inefficiency rests on exactly this theorem. What we pay is cost, not correctness.

3.3 The Decisive Direction Is the Other One

The heart of this work is not the over-provisioning side. It is the under-provisioning side.

The earlier work left only monotonicity open: does a higher degree safely handle a lower-degree asset? For a hierarchy to become enforcement, that alone falls short. Knowing over-provisioning is safe tells you there is a direction you can err in; it does not tell you there is a direction you must not. Enforcement comes from the latter.

So the opposite direction was proved alongside it. In an under-provisioned state, a state exists that defeats every preservation guarantee. When an asset’s required degree exceeds the system’s capability degree, one can construct a state where preservation fails.

Read the logical form of that statement carefully. It is an existential proposition. “This might be dangerous” and “a state exists that defeats it” are entirely different claims, and the difference is decisive.

Form of the statement	Meaning	Appropriate response
Under-provisioning may be dangerous	Probabilistic. It breaks when bad conditions coincide.	Monitoring, retries, defensive coding
A state exists that defeats it	Structural. The pairing itself is already the defect.	Make the pairing unreachable

Wrong routing is a structural consequence, not a probabilistic one. Send an S₃ asset down the S₁ path and the placement already carries its own counterexample. This is not a thing that fires only when your luck runs out.

Consider an asset subject to a regulatory freeze that drifts onto the light path, leaving the freeze applied in one domain only. That is not an incident that needs network delay to coincide. It follows directly from the definition of that path placement. A frozen asset trading through the unfrozen channel during that window is regulatory arbitrage, which is why such assets are forced to S₃ in the first place.

The two directions went up on the board side by side, and only one of them got circled twice. The existential quantifier was the whole finding.

With both directions closed, the hierarchy finally acquires an asymmetry. One side is safe and the other is not. That asymmetry is what licenses the third condition, moving the verdict earlier.

Figure 2: The Asymmetry of Over- and Under-Provisioning

3.4 What This Result Depends On

For accuracy, here is what the proof rests on.

This is a model-level result. It is machine-checked in Isabelle/HOL, but what was verified is the abstract model of the degree hierarchy, not the actual Rust implementation of OSS. Refinement between model and implementation is separate work and has not been done. “Proved” is not the same as “the system is safe.”

The result also sits on top of prior verification assets. The hierarchy was not erected independently; it indexes degrees over the cross-domain state preservation functor [4], and the forgetful maps between successive degree functors were proved to form natural transformations closed under composition [3]. So hierarchy monotonicity was a matter of laying a reduction relation over existing verification assets, not an independent verification built from the ground up. The earlier work forecast exactly that, and the forecast held.

4. What Separates S₂ From S₃

4.1 The Deferred Decision

The earlier work explicitly deferred one decision. Does the criterion dividing S₂ from S₃, namely whether mutual rollback is enforced on simultaneous failure, constitute a predicate of its own defining a separate degree, or is it an intensity parameter inside S₂? That article proposed a four-level discrete hierarchy for the time being while leaving room for later work to recast the two as points on a continuum.

We decide now. They are separate degrees.

4.2 Grounds

The grounds span two layers, mechanism and proof.

Mechanism layer. Soft BVC and Full BVC part ways in the structure of the failure path, not in a parameter value. When a domain’s commit fails under Full BVC, every domain rolls back and the locks release. When the same failure hits Soft BVC, the work is enqueued to a retry queue instead of rolling back, and the transient failure of one domain recovers asynchronously. A “value tuning rollback intensity” cannot capture that difference. On failure, an entirely different code path executes.

And that difference changes the kind of guarantee each system offers. Full BVC guarantees intermediate states are unreachable. Soft BVC guarantees no such thing; it offers the weaker eventually consistent, if not exactly simultaneous guarantee instead. This is not a diluted strong guarantee but a different kind of guarantee.

Proof layer. Here the case is decisive. Treat S₂ and S₃ as two intensities within one degree and the case split in the monotonicity proof collapses. Monotonicity holds under the condition “when the capability degree dominates the required degree,” and domination is defined as an ordering relation between degrees. If S₂ and S₃ are two intensities of the same degree, no ordering relation is defined between them, and the sentence “S₃ capability dominates an S₂ requirement” loses formal meaning.

This is a case of formalization feeding back into a design decision. We proposed four levels as a convenience and then confirmed during formalization that the four were a necessity, not a convenience. The “three levels plus an intensity parameter” option the earlier work left open closes on these grounds.

4.3 Why S₂ Has to Exist

One objection is available. Why not drop S₂ entirely and keep only S₁ and S₃? Is a middle strength necessary?

The market answers. Look at how tokenized assets actually operate and most of them sit in that middle band. Bond coupon payments demand bidirectional reflection, yet a short delay between payment confirmation and on-chain distribution does not immediately destroy the asset’s financial meaning. Daily NAV updates behave the same way. For these, Full BVC’s enforced mutual rollback is an unrequested guarantee: safe, per the previous section, and expensive.

For an asset under regulatory freeze, the same delay is a window for regulatory arbitrage. Time spent with only one domain frozen permits trades through the unfrozen channel, which constitutes a violation of the FATF Travel Rule [7] and of national AML regimes. Here the cost of delay is not linear.

Under the single description “needs bidirectional reflection” sit two sets with fundamentally different cost structures. Fold them into one degree and the hierarchy loses the language to express the difference.

5. Moving the Verdict Before Execution

5.1 The Third Condition

Now the last condition of sync degree enforcement. The degree verdict has to land before execution.

Once you know under-provisioning is structurally dangerous, the next question is when you find out.

The weakest response is logging. Wrong routing happens, then it lands in a log. Observation after the fact. Next comes the runtime check: the router compares asset degree against path degree and rejects on mismatch. This does block something. But it blocks during execution, and since the check is itself code, a path that omits the check never runs it.

The strongest response is the type check. Encode the comparison between asset degree and path degree into the type system and any pairing whose required degree exceeds its capability degree gets rejected by the compiler. A wrong dispatch stops being a runtime incident and becomes a compile failure.

5.2 Why Sync Degree Enforcement Is Possible

Here the result from section 3 comes back around. For a type encoding to be legitimate, the relation being encoded must be true. A type system does not check whether the relation is correct; it enforces it. Encode a false relation and the false thing gets enforced.

The relation we want to encode is this: required ≤ capability is safe, exceeding it is not. Both halves of that relation are proved. With only one half, the encoding is incomplete: knowing over-provisioning is safe without knowing under-provisioning is dangerous leaves you unable to name what the type check should reject.

Closing both directions is what justifies the encoding. The compiler has to know what to admit and what to reject.

5.3 What Gets Encoded

One of our Rust core development principles is to encode invariants into types, because an invariant the type system guarantees carries zero verification burden. That Rust’s type system is built to catch a substantial class of errors at compile time [6] is the premise of that principle.

The sync degree hierarchy becomes a concrete instance of it. Holding degrees in an enum field and comparing at runtime, versus lifting degrees to type parameters and comparing at compile time, handles the same information and guarantees different things.

/// The minimum synchronization strength an asset requires.
/// Lifted to the type level so it is checked at routing time.
pub trait Degree {
    const RANK: u8;
}

pub struct S0;
pub struct S1;
pub struct S2;
pub struct S3;

impl Degree for S0 { const RANK: u8 = 0; }
impl Degree for S1 { const RANK: u8 = 1; }
impl Degree for S2 { const RANK: u8 = 2; }
impl Degree for S3 { const RANK: u8 = 3; }

/// Witness that `Required` is dominated by `Capability`.
/// Only pairings with an impl can dispatch, and that existence is the
/// monotonicity condition.
pub trait Dominates<Required: Degree>: Degree {}

impl Dominates<S0> for S0 {}
impl Dominates<S0> for S1 {}
impl Dominates<S1> for S1 {}
impl Dominates<S0> for S2 {}
impl Dominates<S1> for S2 {}
impl Dominates<S2> for S2 {}
impl Dominates<S0> for S3 {}
impl Dominates<S1> for S3 {}
impl Dominates<S2> for S3 {}
impl Dominates<S3> for S3 {}

Those ten impls carry the reduction relation S₃ ⊇ S₂ ⊇ S₁ ⊇ S₀ onto the type level. The pairings that exist are over-provisioned or exactly matched, and Dominates<S3> for S1 has no impl. Its absence is the whole point of the design. Under-provisioned pairings cannot be expressed inside the type system.

use std::marker::PhantomData;

pub struct Asset<Required: Degree> {
    pub id: AssetId,
    _degree: PhantomData<Required>,
}

pub struct Path<Capability: Degree> {
    _degree: PhantomData<Capability>,
}

impl<Capability: Degree> Path<Capability> {
    /// Dispatch an asset down this path.
    /// Fails to compile unless the `Capability: Dominates<Required>` bound holds.
    pub fn dispatch<Required>(&self, asset: Asset<Required>) -> Result<SyncReceipt, SyncError>
    where
        Required: Degree,
        Capability: Dominates<Required>,
    {
        // Reaching this body is itself evidence that Capability::RANK >= Required::RANK.
        // No runtime branch for degree comparison exists.
        self.execute(asset.id)
    }
}

Over-provisioning passes. Handing an Asset<S0> to a Path<S3>, which is single-mode operation, belongs here. Attempt under-provisioning and this happens.

error[E0277]: the trait bound `S1: Dominates<S3>` is not satisfied
  --> src/main.rs:96:30
   |
96 |     let _ = path_s1.dispatch(asset_s3);
   |                     -------- ^^^^^^^^ unsatisfied trait bound
   |                     |
   |                     required by a bound introduced by this call
   |
help: the trait `Dominates<S3>` is not implemented for `S1`

The compiler refusing to route an S3 asset down the S1 path. Nothing here is a check; the pairing simply cannot be written.

What produces that rejection is not check code. It arises because a bound goes unsatisfied, which means there is no check site available to omit. Nothing goes unexecuted and thereby missed, because there is no check. What exists is a relation, and relations do not execute.

One thing worth flagging: there is no clever technique in this code. Phantom types and trait bounds are ordinary tools in Rust, and anyone can write those ten lines. The hard part was never the encoding but knowing the relation being encoded is true. Formal verification did not enable us to write this code; it gave us grounds to call the code correct. Write the same code without the proof and what you have is enforced guesswork.

Figure 3: From Label to Compile-Time Enforcement

5.4 Where the Entry Structure Splits

Type-level verdicts produce one more consequence. The degree verdict moves to the very front of processing.

An asset’s degree is fixed at tokenization time and recorded as registry metadata [1]. That value does not get looked up after a synchronization request arrives. It determines from the outset what kind of request a transaction touching that asset even is. A transaction handling an S₀ asset and one handling an S₃ asset are not the same request with different parameters. The entry paths themselves differ.

This split does not happen at a billing or settlement stage. It happens in the structure by which requests enter the system. Asked what the degree does inside the system, the answer comes to this. It is read first, and it splits earliest.

6. Boundaries and Limits

Separating what our account of sync degree enforcement claims from what it does not.

The model-implementation gap. Monotonicity and its converse are proved at the model level. That this model corresponds to the actual OSS implementation must be established separately and has not been. The type encoding above is one way to narrow that correspondence, but what the type system enforces is the degree comparison, not the fact that each path actually performs processing worthy of its degree. Whether Path<S3> genuinely enforces mutual rollback is not something the type tells you.

Assumptions of the proof. The formal model of the hierarchy stands on an abstraction treating atomic synchronization as a single step. The partially synchronous networks, message delays, and node failures of real deployment sit outside that abstraction. Narrowing that gap is separate follow-up work.

Timing of branch mode. The transition from single mode to branch mode is conditioned on operational stabilization of the BVC pattern, and measurement decides when that condition is met. What we can present now is the rationale and the ordering, not a schedule.

Correctness of the classification itself. A formally closed hierarchy and a correctly classified asset are different matters. The type system stops an Asset<S3> from reaching the S₁ path, but it cannot stop an asset that should be S₃ from being constructed as an Asset<S1>. Classification correctness lives outside the hierarchy and depends on the attribute evaluation performed at tokenization.

7. Open Questions

Dynamic degree change. Of the three items the earlier work left, only this one is partially resolved. Static reassignment is closed: reassigning an asset’s degree within the system’s capability range carries the over-provisioning guarantee across, and that is proved [3]. But that is static. The safety of the instant an asset is promoted mid-life, say a regulatory action pushing an S₂ asset to S₃, remains unclosed. If a synchronization cycle is in flight at promotion time, whose rules does that cycle follow? The question intersects session boundaries, and later work takes it up.

Formal status of the boundary predicate. The S₁/S₂ boundary predicate the earlier work defined, causal consistency, was confirmed to be single-valued inside the formal model, satisfied under over-provisioning, and derivable as a strict ordering corresponding to Lamport‘s happened-before relation [5][3]. That tells us the boundary is well defined. It does not tell us the boundary was drawn in the right place. Well-definedness and the soundness of the choice are questions at different layers.

Constructive meaning of the under-provisioning counterexample. That a state defeating under-provisioning exists is proved. How readily that state is reached in real deployment is a separate matter, since an existence proof says nothing about degree of reachability. Whether this counterexample is an extreme construction or a common configuration is for measurement to answer, and whichever way it lands, the case for type-level blocking does not change. What changes is our perception of the size of the risk.

The floor of the light path. That the S₁ path skips locking and proofs invites the question of what we guarantee on it. The earlier work argued existing data oracles are trapped at S₁ by their structural type. So what separates our S₁ path from theirs? Ours is an S₁ that a system capable of reaching S₃ descended to by choice; theirs is an S₁ that is the ceiling. Whether S₁-as-capability and S₁-as-limit are observationally distinguishable is an interesting question we have not answered.

---

Conclusion

The earlier work built the hierarchy. This one asked what that hierarchy actually blocks inside the system, and answered with three conditions.

The paths genuinely diverge, choosing wrong is not harmless, and the verdict lands before execution. OSS branches into four processing paths by degree, but starts in single mode until the BVC pattern that the subtractions derive from has been validated. Single mode is safe because over-provisioning safety is proved.

The center of gravity sits on the other side. In an under-provisioned state, a state exists that defeats every preservation guarantee. The existential form matters. Wrong routing is not an accident awaiting a coincidence of bad conditions but a consequence following from the placement’s definition.

Because both directions are closed, the degree comparison can descend into the type system, since the compiler knows both what to admit and what to reject. A wrong dispatch is not detected at runtime; it becomes inexpressible at compile time. At that point, classification stops being a label and becomes sync degree enforcement.

The S₂/S₃ boundary the earlier work deferred is settled on whether mutual rollback is enforced. What we proposed as a convenience turned out, under formalization, to be a necessity. Merge the two and the ordering relation collapses; without the ordering relation, monotonicity cannot even be stated.

What remains, remains honestly. There is no model-implementation correspondence yet, dynamic promotion is closed only as far as static reassignment, and the correctness of the classification itself lives outside the hierarchy. The hierarchy blocks the wrong path. It does not block the wrong classification.

Even so, the hierarchy is no longer vocabulary inside a document. Violate it and something actually blocks.

Learn More

• Oraclizer Docs: State Synchronization
• Oraclizer Docs: OIP v0.5 State Management

References

• [1] Oraclizer Research. (2026). Sync Degree Hierarchy: Classifying What Assets Demand from State Synchronization. https://research.oraclizer.io/sync-degree-hierarchy-state-oracles/
• [2] Oraclizer Research. (2026). Atomic State Binding: Formalizing Causal Consistency in Bidirectional Synchronization. https://research.oraclizer.io/atomic-state-binding-oracle-synchronization/
• [3] Oraclizer. (2026). Formal Verification: Cross-Domain State Preservation. GitHub Repository. https://github.com/Oraclizer/formal-verification
• [4] Kim, J. (2026). The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL. arXiv:2604.03844. https://arxiv.org/abs/2604.03844
• [5] Lamport, L. (1978). Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM, 21(7), 558-565. https://amturing.acm.org/p558-lamport.pdf
• [6] Jung, R., Jourdan, J.-H., Krebbers, R., & Dreyer, D. (2021). Safe Systems Programming in Rust: The Promise and the Challenge. Communications of the ACM, 64(4), 144-152. https://dl.acm.org/doi/10.1145/3418295
• [7] Financial Action Task Force (FATF). (2021). Updated Guidance for a Risk-Based Approach for Virtual Assets and Virtual Asset Service Providers. https://www.fatf-gafi.org/en/publications/Fatfrecommendations/Guidance-rba-virtual-assets-2021.html