TL;DR
The core theorem regulatory_homomorphism has been proven without sorry: after synchronization, every connected chain reflects the same regulatory state. This is, to our knowledge, the first machine-checked proof of cross-domain state preservation for regulatory compliance. Three obstacles shaped the proof: a Finite_Set.fold definition that blocked progress until replaced with a direct lambda, four failed attempts at existential quantification in Isabelle, and 11 auxiliary lemmas that had to be built as infrastructure before the 7-step proof could proceed.
In the previous article, we documented the process of converting the semi-formal specification into Isabelle/HOL code. The 4-tier locale hierarchy, the atomic sync decision, the abstraction choices for the global state model. The model was complete, but the theorem was not proven. At the end of regulatory_homomorphism‘s statement sat sorry.
This article documents the process of replacing that sorry with an actual proof, the journey of converting cross-domain state preservation from a mathematical claim into mathematical certainty.
The First Wall: Finite_Set.fold
Before attempting the core theorem’s proof, we first needed to establish the properties of update_all_chains. This function propagates a given asset’s regulatory state to all connected chains. As the core operation within sync, precisely characterizing its behavior is a prerequisite for every subsequent proof.
The original definition used Finite_Set.fold.
definition update_all_chains ::
"global_state ⇒ asset_id ⇒ reg_state ⇒ chain_id set ⇒ global_state"
where
"update_all_chains gs aid new_st targets =
(Finite_Set.fold
(λcid gs'. update_chain_reg_state gs' cid aid new_st)
gs targets)"
fold applies a function sequentially over the elements of a finite set. Conceptually identical to list fold, but since sets have no ordering, Isabelle requires proof that the result does not depend on application order. Specifically, we must satisfy the comp_fun_commute instance: showing f x ∘ f y = f y ∘ f x for all element pairs.
Is this possible? Yes. Updates to each chain modify the same asset_id field on different chain_ids, so they are genuinely commutative. The problem was that convincing Isabelle of this commutativity constituted an unnecessarily complex detour. Proving comp_fun_commute requires fully unfolding the definition of update_chain_reg_state, showing equivalence of two function compositions, and handling record update independence through additional lemmas. This entire path is technical overhead unrelated to the essence of the core proof.
The Insight: All at Once, Not One by One
If updates to each chain are independent, there is no reason to model sequential application. A direct definition that updates all chains simultaneously is possible.
definition update_all_chains ::
"global_state ⇒ asset_id ⇒ reg_state ⇒ chain_id set ⇒ global_state"
where
"update_all_chains gs aid new_st targets =
gs⟨ gs_chains := (λcid.
if cid ∈ targets then
(λaid'. if aid' = aid then
(case gs_chains gs cid aid of
None ⇒ None
| Some ast ⇒ Some (ast⟨ as_reg_state := new_st ⟩))
else gs_chains gs cid aid')
else gs_chains gs cid) ⟩"
In this definition, gs_chains is constructed directly as a lambda function. For chains in the targets set, the asset’s reg_state is replaced with new_st; for chains outside the set, the original state is retained. With fold gone, the comp_fun_commute obligation vanishes.
The significance of this change extends beyond the technical. fold models “updating one chain at a time, sequentially.” The direct lambda models “updating all chains simultaneously.” Since OSS’s design intent is atomic synchronization, the latter is also a semantically more accurate model. Proof difficulty exposed a modeling imprecision; revising the model made the proof easier while simultaneously improving semantic accuracy. This is one of the core values of formal verification as a process.
After switching to the direct definition, auxiliary lemmas characterizing update_all_chains became straightforward, handled by unfolding update_all_chains_def and simple automation.
lemma update_all_chains_in_targets:
assumes "cid ∈ targets"
and "gs_chains gs cid aid = Some ast"
shows "gs_chains (update_all_chains gs aid new_st targets) cid aid =
Some (ast⟨ as_reg_state := new_st ⟩)"
unfolding update_all_chains_def using assms by auto
Under the fold definition, proving this single lemma would have required comp_fun_commute plus finite set induction. Under the direct definition: unfold and auto.
Figure 1: update_all_chains Definition Redesign — fold vs Direct Lambda
Four Failed Attempts: The Existential Quantifier Trap
Separate from the fundamental model restructuring, the proof process included a case where understanding Isabelle’s reasoning mechanics took time. The non_terminal_has_action lemma states a simple proposition: “for every non-CONFISCATED state, at least one valid transition exists.”
lemma non_terminal_has_action: assumes "s ≠ CONFISCATED" shows "∃a. reg_transition s a ≠ None"
Intuitively obvious. From ACTIVE, FREEZE works. From FROZEN, UNFREEZE works. From SEIZED, RELEASE works. From RESTRICTED, UNRESTRICT works. But conveying this intuition to Isabelle required four attempts.
Attempt 1: by (cases s) auto. auto cannot handle the existential quantifier ∃a. Proving an existential requires providing a concrete witness, and auto cannot decide which a to choose.
Attempt 2: After explicitly constructing a witness in the ACTIVE case, using ACTIVE by auto. While case ACTIVE sets s = ACTIVE as an assumption, the goal ∃a. reg_transition s a ≠ None still uses s as a free variable, and auto fails to complete the substitution.
Attempt 3: then have + exI rule combination. Tried to substitute FREEZE into the existential via exI[of _ FREEZE], but rule application and simplification ordering did not align.
Attempt 4 (success):
case ACTIVE show ?thesis apply (rule exI[where x=FREEZE]) using ACTIVE by simp
apply (rule exI[where x=FREEZE]) first transforms the goal to reg_transition s FREEZE ≠ None. At this point the existential quantifier is gone; what remains is a concrete inequality. Then using ACTIVE by simp substitutes s = ACTIVE and automatically closes reg_transition ACTIVE FREEZE = Some FROZEN ≠ None.
The key lesson: Isabelle cannot simultaneously perform existential instantiation and case assumption substitution. The two steps must be separated. First apply to remove the quantifier, then using ... by simp to apply the case assumption. This stems from the difference in how Isabelle’s proof engine handles backward reasoning (rule application) versus forward reasoning (assumption utilization) [3, Ch. 5].
The same pattern applied to the remaining four cases (FROZEN, SEIZED, CONFISCATED, RESTRICTED). The CONFISCATED case is dispatched by contradiction with the assumption s ≠ CONFISCATED.
Proof Infrastructure: 11 Auxiliary Lemmas
Before proving the core theorem regulatory_homomorphism, we needed to independently establish what each step of the sync function preserves and what it changes. Since sync’s structure is lock acquisition → state update → lock release, lemmas are needed for each phase.
A total of 11 auxiliary lemmas were added, falling into three groups.
update_all_chains properties (6): update_all_chains_in_targets guarantees that assets on chains within the target set are updated. update_all_chains_in_targets_none ensures None is preserved for chains where the asset does not exist. update_all_chains_outside_targets confirms chains outside the target set are unchanged. update_all_chains_other_asset ensures other assets are unaffected. update_all_chains_locks preserves lock state. update_all_chains_reg_state establishes that the reg_state of chains in the target set changes to new_st. This last lemma is the critical waypoint.
release_lock preservation (2): release_lock_chains and release_lock_reg_state prove that lock release does not alter chain data. Without this guarantee, the state established in Step 5 would not persist through Step 6.
acquire_lock preservation (3): acquire_lock_chains, acquire_lock_reg_state, and acquire_lock_asset_exists prove that lock acquisition does not change chain data, regulatory state, or asset existence. Without this, state information from before lock acquisition could not be validly referenced afterward.
The common pattern across these lemmas is non-interference proof: “this operation does not modify the quantity of interest.” Each is individually trivial, yet failing to establish even one prevents the core theorem’s proof from proceeding. The difference between “trivial” and “unnecessary” becomes visible here.
The 7-Step Proof
With the auxiliary lemma infrastructure in place, the proof of regulatory_homomorphism begins. First, the theorem statement.
theorem regulatory_homomorphism:
assumes valid: "valid_state gs"
and exists: "asset_exists gs source aid"
and current: "get_reg_state gs source aid = Some s"
and trans: "reg_transition s action = Some s'"
and synced: "sync source action aid gs = Some gs'"
and connected: "c ∈ connected_chains gs aid"
and fin: "finite (connected_chains gs aid)"
shows "get_reg_state gs' c aid = Some s'"
In natural language: given a valid global state, if a valid regulatory action is applied to an asset on the source chain and synchronization succeeds, the regulatory state on every chain where that asset exists equals the new state.
The proof unfolds along sync’s definition. sync = lock → validate → update → unlock, and the proof mirrors this structure exactly.
proof -
(* Step 1: Unfold sync to extract intermediate states *)
from synced current trans
obtain gs_locked where
lock: "acquire_lock gs aid = Some gs_locked"
and gs'_def: "gs' = release_lock
(update_all_chains gs_locked aid s' (connected_chains gs aid)) aid"
unfolding sync_def
by (auto split: option.splits simp: Let_def)
Step 1 unfolds the sync definition to extract the intermediate state gs_locked. Since sync returned Some gs', every internal case branch must have succeeded, so acquire_lock must have returned Some gs_locked. Isabelle’s option.splits automates this reasoning.
(* Step 2: acquire_lock preserves chain data *)
have locked_chains: "gs_chains gs_locked = gs_chains gs"
using acquire_lock_chains[OF lock] by simp
(* Step 3: c is in connected_chains, so the asset exists on c *)
from connected have "asset_exists gs c aid"
unfolding connected_chains_def by simp
then obtain ast_c where ast_c: "gs_chains gs c aid = Some ast_c"
unfolding asset_exists_def get_asset_state_def by auto
(* Step 4: Therefore asset also exists in gs_locked on chain c *)
have ast_locked: "gs_chains gs_locked c aid = Some ast_c"
using ast_c locked_chains by simp
Steps 2-4 form a chain of preservation reasoning. Lock acquisition does not change chain data (Step 2), so if the asset existed in the original state (Step 3), the same asset exists in the locked state (Step 4).
(* Step 5: update_all_chains sets chain c's state to s' *)
have updated: "gs_chains
(update_all_chains gs_locked aid s' (connected_chains gs aid)) c aid =
Some (ast_c⟨ as_reg_state := s' ⟩)"
using update_all_chains_in_targets[OF connected ast_locked] by simp
Step 5 is the heart of the proof. Since c belongs to connected_chains gs aid and the asset exists in gs_locked, the update_all_chains_in_targets lemma guarantees the asset’s reg_state is replaced with s'. This is the direct benefit of the fold-to-lambda transition. Under the fold definition, this single line of reasoning would have required comp_fun_commute plus finite set induction.
(* Step 6: release_lock does not change chain data *)
have "gs_chains gs' c aid = Some (ast_c⟨ as_reg_state := s' ⟩)"
using updated unfolding gs'_def release_lock_chains by simp
(* Step 7: Unfold get_reg_state to conclude *)
then show ?thesis
unfolding get_reg_state_def get_asset_state_def by simp
qed
Steps 6-7 close the proof. Lock release preserves chain data (Step 6), and unfolding get_reg_state yields Some s' (Step 7).
It is worth noting that the proof’s 7 steps precisely mirror sync’s 3 phases (lock → update → unlock). Step 1 decomposes sync. Steps 2-4 establish lock non-interference. Step 5 confirms the update effect. Steps 6-7 derive the final state after unlock. The proof’s structure mirrors the system’s structure. This is not coincidence but a characteristic of a well-designed model.
sync definition, extract intermediate gs_lockedacquire_lock preserves chain datac ∈ connected_chains implies asset exists on chain cgs_locked (from Steps 2+3)update_all_chains sets chain c’s state to s'release_lock does not change chain dataget_reg_state to conclude Some s'sync, extract gs_lockedacquire_lock preserves chainsupdate_all_chains sets state to s’release_lock preserves chainsget_reg_state → Some s'Figure 2: regulatory_homomorphism — 7-Step Proof Structure
Cross-Domain State Preservation: Core Proof Complete
The sorry on regulatory_homomorphism has been removed. What this theorem states is precisely the definition of Property 1:
Regulatory_Instance.thy, line 726. No goal (successful proof).
If a valid regulatory state transition occurs on chain A, after synchronization chain B also reflects the same regulatory state.
Formally:
$$\text{sync succeeds} \wedge c \in \text{connected\_chains} \Rightarrow \text{get\_reg\_state}\ gs’\ c\ \text{aid} = \text{Some}\ s’$$
Isabelle/HOL’s kernel has verified this proposition. Without sorry or oops.
Nature of the Remaining Tasks
The core theorem is complete, but two follow-up tasks remain. These are not Property 1 itself, but work that extends the practical applicability of Property 1.
valid_state preservation: “Is the system still valid after sync?” The regulatory_homomorphism theorem requires valid state as a precondition. If sync does not preserve valid state, the theorem applies to only a single synchronization. valid_state_preservation strengthens this theorem into an inductive invariant, guaranteeing that valid state is maintained after arbitrarily many synchronizations. An auxiliary theorem that secures repeatability.
multi_domain instantiation: Connecting the regulatory instance to State_Preservation.thy’s generic multi_domain_preservation locale. Not needed for the core proof, but necessary for demonstrating the structural link between generic theory and concrete instance at AFP submission.
Both tasks will be completed during AFP submission preparation. They do not affect the validity of the core theorem.
The Interplay of Model and Proof
The most striking aspect of this proof process was the mutual dependence between model definitions and proof tractability.
The fold definition blocked the proof. Replacing it with a direct definition made the proof possible. Simultaneously, the direct definition captured OSS’s atomic synchronization semantics more accurately. Proof difficulty exposed a modeling problem; improving the model made the proof easier while also improving semantic accuracy.
This phenomenon is the core value that emerges when formal verification is used not as a “post-implementation validation tool” but as a “design tool.” Had we not attempted the proof, we would not have discovered the issue with the fold definition, and would have encountered the same problem at implementation with far greater cost.
The four failures on non_terminal_has_action fit the same pattern. Proof attempts forced understanding of Isabelle’s reasoning engine, and that understanding saved time on every subsequent existential-quantification proof.
The design of the 11 auxiliary lemmas is likewise. Before attempting the proof, we could not know which non-interference properties would be needed. Each proof step generated the demand “this value must be preserved at this point,” and satisfying that demand required adding an auxiliary lemma. The proof deepening understanding of the model was a pattern that repeated throughout.
Conclusion
Property 1 is done. regulatory_homomorphism carries no sorry, no oops. Isabelle/HOL’s small trusted kernel, the same kernel behind seL4’s verified microkernel, has checked every step.
We should be clear about what this is and what it is not. It is a proof that the synchronization logic preserves regulatory state across domains, within the model’s stated assumptions: atomic sync, honest nodes, finite chains. It is not a proof that the implementation is correct; the gap between model and code remains open, documented, and is the subject of future refinement work. But within those assumptions, the guarantee is absolute. Not probabilistic, not “we tested 10,000 cases.” Absolute.
One aspect worth noting: the proof rests on State_Preservation.thy, a generic locale that is not specific to regulation. Regulatory state was the first instantiation, but the locale itself describes cross-domain state preservation for any finite-state, deterministic-transition domain. The verified theorem is, in effect, a reusable certificate of state homomorphism: a machine-checked guarantee that a certain class of synchronization protocols preserves structure across domains. What this means for the broader state synchronization field, and for AFP submission, is something we will explore more fully in the next article.
In an earlier research article we argued that RWA infrastructure must move beyond post-hoc audits and runtime checks toward mathematically provable compliance. We called it Pattern 3. When you make that kind of claim publicly, you take on an obligation to demonstrate it yourself. This proof is the first installment on that obligation. The .thy files will be publicly available; anyone with an Isabelle installation can rebuild the proof from source and verify every step independently.
Three lessons from the process: definitions determine proofs (fold → direct definition), tool limitations become learning (existential quantification, four failures), and proof infrastructure matters as much as the proof itself (11 auxiliary lemmas).
Two tasks remain. Strengthening the core theorem into an inductive invariant via valid_state_preservation, and completing the structural link to the generic theory via multi_domain_preservation locale instantiation. Both are planned for AFP submission preparation, and neither affects the core guarantee of cross-domain state preservation. The next article will document that process.
One open question remains. The current model defines sync as an atomic function. In practice, this atomicity will be realized through the preemptive locking mechanism. Can the gap between the model’s atomic sync and the implementation’s non-atomic locking protocol be formally bridged? This is the most meaningful extension direction remaining within Property 1’s scope, connecting to an eventual consistency proof under a partially synchronous network model.
References
[1] Lochbihler, A. & Marić, O. (2020). “Authenticated Data Structures As Functors in Isabelle/HOL.” In: FMBC 2020. OASIcs vol. 84, 6:1-6:15. https://doi.org/10.4230/OASIcs.FMBC.2020.6
[2] Nipkow, T. & Klein, G. (2014). Concrete Semantics: With Isabelle/HOL. Springer. http://concrete-semantics.org/
[3] Nipkow, T., Paulson, L.C. & Wenzel, M.T. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS vol. 2283, Springer. https://isabelle.in.tum.de/doc/tutorial.pdf
[4] Ballarin, C. (2014). “Locales: A Module System for Mathematical Theories.” Journal of Automated Reasoning 52(2), 123-153. https://doi.org/10.1007/s10817-013-9284-7
[5] Wenzel, M. (2007). “Isabelle/Isar — A Generic Framework for Human-Readable Proof Documents.” In: From Insight to Proof — Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric vol. 10(23). https://www21.in.tum.de/~wenzelm/papers/isar-framework.pdf
Learn More
Read more on Oraclizer Research:
Formalizing Cross-Domain State Preservation in Isabelle/HOL — Transition from semi-formal specification to formal model, 4-tier locale hierarchy design
Defining Cross-Domain State Preservation: What Are We Proving? — Semi-formal specification of Property 1, state space design, and threat model definition
Why We’re Starting Formal Verification: Applying Our Own Standard — Pattern 3 self-application motivation and verification target introduction
