TL;DR
Property 2 modeling has begun. Priority_Resolution.thy defines three domain-independent locales (priority_system, deadlock_free_locking, fair_leader_system), and DQuencer_Instance.thy instantiates them into the regulatory domain. Five key design decisions shaped the implementation. (1) Using nat × nat × nat × nat tuples for priority keys, directly leveraging Isabelle’s built-in lexicographic order and avoiding manual linorder instance registration. (2) Sign inversion of timestamps and node_id to map “smaller is higher priority” onto nat’s default ordering. (3) Reusing Property 1’s code without modification through oss_message record inheritance. (4) Abstracting BFT consensus not as BLS signature cryptographic security but as the determinism property of consensus output. (5) Radically simplifying locale signatures from the initial design, reducing deadlock_free_locking to a single assumption (timeout > 0) that suffices to prove deadlock freedom. Currently 5 sorry remain in Priority_Resolution.thy and 0 in DQuencer_Instance.thy. The sorry elimination process will be covered in the next post.
From Property 1 to Property 2: What Is Being Extended
After Property 1’s proof was complete, we established the first principle for extension: add new structures on top of the existing model without modifying it. The four generic locales in State_Preservation.thy, along with Regulatory_Instance.thy‘s state transition model, global state, sync function, and valid_state invariant, all remain untouched.
What Property 2 adds is confined to four areas.
First, a priority system. A total order that determines which regulatory action to process first when conflicting actions arrive simultaneously. Property 1 handled concurrent arrivals through preemptive locking for sequential processing, but never defined the criteria for ordering.
Second, a Byzantine node model. Property 1 assumed all nodes honestly follow the protocol. Now we model an environment where up to f < n/3 malicious nodes exist.
Third, timeout-based deadlock freedom. Defense against Byzantine nodes intentionally refusing to release locks.
Fourth, fairness-based starvation freedom. Reducing VRF leader election’s probabilistic guarantee to a deterministic assumption for proof.
All four are defined in new files (Priority_Resolution.thy, DQuencer_Instance.thy), with no modifications to existing files.
Priority_Resolution.thy: Three Generic Locales in Isabelle/HOL
Priority_Resolution.thy is a standalone theory file that imports only Main. It never imports Regulatory_Instance.thy and knows nothing about the regulatory domain. The three locales it defines are reusable abstractions applicable across distributed systems.
locale priority_system: Deterministic Selection
This locale formalizes the problem of selecting the highest-priority element from a finite set. The required structure is minimal: a priority function mapping into a linear order (linorder), and that mapping must be injective.
locale priority_system =
fixes priority :: "'m ⇒ 'k::linorder"
assumes priority_injective:
"⟦ priority m1 = priority m2 ⟧ ⟹ m1 = m2"
The injectivity assumption models tiebreaking. When a real system uses a composite key (authority level, timestamp, severity, node ID), two distinct messages sharing the same priority is structurally excluded.
The key theorem to prove within this locale is highest_priority_exists. Given an injective priority function over a finite non-empty set, the element with maximum priority exists uniquely.
lemma highest_priority_exists:
assumes "finite S" and "S ≠ {}"
shows "∃!m. m ∈ S ∧ (∀m' ∈ S. priority m' ≤ priority m)"
The proof has two steps. First, show the existence of a maximum element in a finite set (connecting to the appropriate lemma in Isabelle’s Finite_Set library), then derive uniqueness from injectivity. The uniqueness direction is already proven: if priority m = priority m2, injectivity gives m2 = m. One sorry remains on the existence direction, corresponding to the connection with Finite_Set‘s Max-related lemmas.
On top of this, the select_highest function is defined.
definition select_highest :: "'m set ⇒ 'm option" where
"select_highest S =
(if S = {} then None
else Some (THE m. m ∈ S ∧ (∀m' ∈ S. priority m' ≤ priority m)))"
THE is Isabelle/HOL’s definite description operator, which selects the uniquely existing element. Since highest_priority_exists proves ∃!, the use of THE is justified. Three theorems, select_highest_deterministic, select_highest_in_set, and select_highest_is_max, are built on this definition and are currently sorry.
Where can this locale apply beyond regulatory systems? DeFi protocol transaction ordering, deterministic winner selection in MEV auctions, task priority resolution in distributed schedulers. Any system requiring deterministic selection based on total order over a finite set can instantiate this locale.
locale deadlock_free_locking: Timeout-Based Deadlock Freedom
This locale formalizes the minimal structure guaranteeing deadlock freedom in a resource locking system.
locale deadlock_free_locking = fixes timeout :: nat assumes timeout_positive: "timeout > 0"
A single assumption: the timeout is positive. On top of this, lock effectiveness is defined as a function of time.
definition lock_effective :: "nat ⇒ nat ⇒ bool" where "lock_effective lock_time current_time ⟷ current_time < lock_time + timeout"
A lock expires once timeout time units pass since the acquisition time (lock_time). Expired locks have no blocking effect regardless of whether the holder explicitly released them.
Two key theorems are proven in this locale. lock_eventually_expires shows that every lock eventually expires, and deadlock_freedom shows that any currently effective lock expires within lock_time + timeout. Both are proven without sorry.
theorem lock_eventually_expires: "∃t'. t' ≥ current_time ∧ ¬ lock_effective lock_time t'" theorem deadlock_freedom: assumes "lock_effective lock_time current_time" shows "∃t'. t' ≤ lock_time + timeout ∧ ¬ lock_effective lock_time t'"
The proofs are constructive, directly presenting lock_time + timeout as the witness. Unfolding lock_effective_def shows that lock_time + timeout < lock_time + timeout is false, so the lock has expired, and auto handles the rest.
One design decision deserves attention here. Oraclizer’s locking structure uses single-resource locks (one lock per asset ID). The classical deadlock condition of “circular wait” is structurally impossible with single-resource locking. The situation where process A holds resource X while waiting for resource Y, and simultaneously process B holds Y while waiting for X, cannot occur when each process holds at most one lock. Timeouts provide additional defense on top of this structural guarantee, handling the case where a Byzantine node intentionally refuses to release its lock.
This locale’s generic applicability extends to distributed database row locks, file system locks, and distributed cache key locks, anywhere the same structure of “finite resources, locks, and timeouts” exists.
locale fair_leader_system: Starvation Freedom under Fair Leadership
This locale formalizes the minimal conditions guaranteeing starvation freedom in a leader-based consensus system.
locale fair_leader_system =
fixes leader_at :: "nat ⇒ 'n"
and is_honest :: "'n ⇒ bool"
and pending :: "nat ⇒ nat"
and fairness_bound :: nat
assumes fairness_bound_positive: "fairness_bound > 0"
and fair_leader:
"∀epoch. ∃e. epoch ≤ e ∧ e < epoch + fairness_bound ∧ is_honest (leader_at e)"
and honest_progress:
"⟦ is_honest (leader_at e); pending e > 0 ⟧ ⟹ pending (Suc e) < pending e"
and non_honest_bounded:
"pending (Suc e) ≤ pending e"
Each of the four assumptions serves a specific role.
fair_leader is the fairness assumption. Starting from any epoch, at least one honest node is elected as leader within fairness_bound epochs. In D-quencer with VRF-based leader election, the probability of a Byzantine leader being elected k consecutive times is \((f/n)^k\), decreasing exponentially. Converting this probabilistic property into a deterministic assumption is what fair_leader does. This corresponds to the “assume” side of the assume-guarantee reasoning described in the previous post.
honest_progress is the crux. When an honest leader is elected and the pending queue is non-empty, the pending queue size strictly decreases in the next epoch. Since strict decrease on natural numbers guarantees reaching 0 within finite time, this forms the basis for the termination proof.
non_honest_bounded is a closed-system assumption. Even during dishonest leader epochs, the pending queue does not grow. This means no new requests arrive during the analysis interval. The limitation of this assumption must be explicitly acknowledged. If new request arrivals are modeled, the pending queue could grow unboundedly, and starvation freedom would require more complex conditions. The current scope is limited to “complete processing of a given finite queue.”
Two key theorems are proven within this locale. starvation_bound shows that if the pending queue is non-empty, at least one request is processed within fairness_bound epochs. This theorem is proven without sorry.
theorem starvation_bound: assumes "pending epoch > 0" shows "∃e. epoch ≤ e ∧ e < epoch + fairness_bound ∧ pending (Suc e) < pending e"
The proof obtains an honest leader epoch e from fair_leader, uses pending_monotone (monotonic non-increase of the pending queue) to show pending e > 0 at that epoch, then applies honest_progress.
eventual_completion shows that all pending requests are eventually processed. Using well-founded induction on the pending queue size (a natural number), repeated application of starvation_bound drives the queue to zero. One sorry remains on this theorem, corresponding to the well-founded induction construction.
theorem eventual_completion: shows "∃e_final. pending e_final = 0"
Figure 1: Priority_Resolution.thy — Three Generic Locales with Assumptions, Theorems, and Proof Status
DQuencer_Instance.thy: Instantiation into the Regulatory Domain
DQuencer_Instance.thy is the junction where two worlds merge.
theory DQuencer_Instance imports Priority_Resolution Regulatory_Instance begin
It imports the three generic locales from Priority_Resolution and the regulatory state transition model, global state, and sync function from Regulatory_Instance. This file serves three roles: (1) defining regulatory domain-specific types and functions, (2) instantiating the generic locales, and (3) combining Properties 1 and 2.
authority_level and action_severity
The regulatory authority hierarchy is formalized. The RCP framework‘s jurisdictional priority model, described in the previous post, is translated into code.
datatype authority_level = Regional | National | International fun authority_rank :: "authority_level ⇒ nat" where "authority_rank Regional = 1" | "authority_rank National = 2" | "authority_rank International = 3"
authority_rank_injective is proven immediately by the cases tactic, since three enumeration values map to distinct nats.
Regulatory action severity is also formalized.
fun action_severity :: "reg_action ⇒ nat" where "action_severity UNRESTRICT = 1" | "action_severity UNFREEZE = 2" | "action_severity RELEASE = 3" | "action_severity RESTRICT = 4" | "action_severity FREEZE = 5" | "action_severity SEIZE = 6" | "action_severity CONFISCATE = 7"
This ordering reflects legal principles. Asset-protective actions (CONFISCATE, SEIZE, FREEZE) have higher priority than asset-releasing actions (UNRESTRICT, UNFREEZE, RELEASE). When concurrent conflicting regulatory orders arrive, the more conservative action prevails, consistent with legal practice.
Priority Key: Lexicographic Order on nat Tuples
A core design decision of Property 2 modeling lies here.
type_synonym priority_key = "nat × nat × nat × nat"
In Isabelle/HOL, nat × nat × nat × nat automatically has a linorder instance. The lexicographic order on product types is defined in the standard library. This decision matters because no separate linorder instance registration is required. Manually registering a linorder instance for a new datatype in Isabelle requires defining less_eq and less, then proving antisym, trans, and total, a non-trivial process. Using nat tuples provides all of this automatically.
One technical issue exists, however. In nat’s default order, “larger value = higher rank,” but for timestamps and node_id, “smaller value = higher priority” is needed. Earlier-issued regulatory orders take precedence, and lower-numbered nodes win tiebreakers.
The solution is sign inversion.
The sign inversion sketch that became max_time – msg_timestamp. Smaller timestamps produce larger priority keys.
definition make_priority_key ::
"nat ⇒ nat ⇒ dq_message ⇒ priority_key"
where
"make_priority_key max_time max_node msg =
(authority_rank (dqm_authority_level msg),
max_time - msg_timestamp msg,
action_severity (msg_action msg),
max_node - dqm_source_node msg)"
In max_time - msg_timestamp msg, max_time is the system-wide upper bound for timestamps. The smaller the timestamp (the earlier it arrived), the larger this value becomes, giving it higher rank in nat’s default order. The same logic applies to max_node.
Preventing nat underflow is essential in this construction. If max_time < msg_timestamp, the subtraction truncates to 0 in nat (floor truncation of nat subtraction). To prevent this, msg_timestamp msg ≤ max_time and dqm_source_node msg ≤ max_node are required as preconditions.
Message Extension through Record Inheritance
Property 1’s oss_message is extended without modification.
record dq_message = oss_message + dqm_authority_level :: authority_level dqm_source_node :: nat
Isabelle’s record inheritance mechanism makes dq_message a subtype of oss_message. All fields defined on oss_message (msg_action, msg_asset_id, msg_authority, msg_timestamp, msg_source, msg_targets) are accessible on dq_message as well.
The practical value of this decision is that Property 1’s sync function only uses oss_message fields, so passing dq_message to sync requires no explicit conversion. The combined_safety_liveness theorem can directly invoke Property 1’s sync and valid_state_preservation.
Byzantine Node Model and dquencer_system Locale
Nodes are dichotomized into Honest and Byzantine.
datatype node_behavior = Honest | Byzantine record node_info = ni_id :: nat ni_behavior :: node_behavior
The dquencer_system locale encapsulates the system-wide BFT assumptions.
locale dquencer_system =
fixes nodes :: "node_info set"
and f_max :: nat
and lock_timeout :: nat
and fairness_bound :: nat
and max_time :: nat
and max_node :: nat
assumes finite_nodes: "finite nodes"
and bft_threshold: "card nodes ≥ 3 * f_max + 1"
and byzantine_bound: "card (byzantine_nodes nodes) ≤ f_max"
and nonempty_nodes: "nodes ≠ {}"
and timeout_positive: "lock_timeout > 0"
and fairness_positive: "fairness_bound > 0"
bft_threshold directly expresses \(n \geq 3f + 1\). From this, honest_majority is derived.
lemma honest_majority: "card (honest_nodes nodes) > 2 * f_max"
The proof combines honest_byzantine_partition (partition), honest_byzantine_disjoint (disjointness), and card_Un_disjoint (cardinality of disjoint union) through arithmetic reasoning. honest_nonempty follows immediately as a corollary: honest nodes exceed \(2f_{\max}\), hence exceed 0, hence the set is non-empty.
BFT Consensus Abstraction
Rather than formalizing BLS signature cryptographic security or the vote counting process, we model only the result property of consensus: under honest majority, the consensus output matches the highest-priority valid message.
definition bft_select ::
"dq_message list ⇒ global_state ⇒ nat ⇒ nat ⇒ dq_message option"
where
"bft_select msgs gs max_t max_n =
(let valid_msgs = filter (valid_dq_message gs) msgs;
prio_msgs = map (λm. (make_priority_key max_t max_n m, m)) valid_msgs;
sorted = sort_key fst prio_msgs
in if sorted = [] then None else Some (snd (last sorted)))"
valid_dq_message verifies that a message represents a valid transition in the current global state. The asset must exist, and the action must return Some from reg_transition given the current state.
The justification for this abstraction follows three steps: (1) with over 2/3 honest nodes, the BFT consensus output reflects honest majority agreement; (2) honest nodes follow the priority protocol, so the consensus result is the highest-priority message; (3) since priority is a total order, the result is deterministic.
Locale Instantiation
The deadlock_free_locking instantiation is the most direct.
context dquencer_system begin interpretation dq_locking: deadlock_free_locking lock_timeout by unfold_locales (rule timeout_positive)
The dquencer_system‘s timeout_positive assumption immediately satisfies deadlock_free_locking‘s sole assumption. After instantiation, dq_locking.deadlock_freedom and dq_locking.lock_eventually_expires become directly usable in the D-quencer context.
The fair_leader_system instantiation is more elaborate. A separate dquencer_liveness locale is defined, adding the leader schedule and pending queue function on top of dquencer_system.
locale dquencer_liveness = dquencer_system +
fixes leader_schedule :: "nat ⇒ node_info"
and pending_count :: "nat ⇒ nat"
assumes fair_leader: "..."
and honest_processes: "..."
and pending_non_increasing: "..."
begin
interpretation dq_fair: fair_leader_system
leader_schedule "λn. ni_behavior n = Honest" pending_count fairness_bound
The abstract is_honest function is concretized as λn. ni_behavior n = Honest, connecting the abstract notion of “honesty” to D-quencer’s node_behavior type.
Int(3) > Nat(2) > Reg(1)
Sign inversion: earlier = higher
CONFISCATE(7) > … > UNRESTRICT(1)
Tiebreaker: lower ID = higher priority
Injectivity from 4-tuple uniqueness
Proof: unfold_locales (rule timeout_positive)
(λn. ni_behavior n = Honest)
pending_count fairness_bound
→ honest_majority > 2 * f_max
→ honest_nonempty
valid_state gs ∧ valid_transition ∧ ¬locked
→ ∃gs’. sync … gs = Some gs’ ∧ valid_state gs’
Figure 2: DQuencer_Instance.thy — Priority Key Construction, Locale Instantiation, and Combined Theorem
Combining Properties 1 and 2
The combined_safety_liveness theorem connects both properties at the end of the file.
theorem combined_safety_liveness:
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 not_locked: "¬ is_locked gs aid"
and fin: "finite (connected_chains gs aid)"
shows "∃gs'. sync source action aid gs = Some gs' ∧ valid_state gs'"
This theorem directly invokes Property 1’s valid_state_preservation. If the preconditions are met (valid state, asset exists, valid transition, not locked, finite connected chains), sync succeeds and the resulting state preserves valid_state.
This theorem itself contains no Byzantine elements. Property 2’s Byzantine-related guarantees (deterministic selection, timeout-based lock release, starvation freedom) ensure that this theorem’s preconditions are actually met in practice. Even if a Byzantine node holds a lock, timeout releases it so the not_locked precondition is eventually satisfied; deterministic priority resolution ensures a valid action is selected; and starvation freedom ensures this process completes within finite time.
This is the formal meaning of “Property 2 satisfies in a Byzantine environment the if-condition that Property 1 defined.”
Current Sorry Status
The following table summarizes the remaining sorry obligations and their expected resolution strategies.
| File | Theorem | Sorry Content | Expected Resolution |
|---|---|---|---|
| Priority_Resolution.thy | highest_priority_exists | Existence direction | Connect to Finite_Set max lemma |
| Priority_Resolution.thy | select_highest_deterministic | THE uniqueness | Follows from highest_priority_exists |
| Priority_Resolution.thy | select_highest_in_set | Set membership | Unfold definition + THE property |
| Priority_Resolution.thy | select_highest_is_max | Maximality | Unfold definition + THE property |
| Priority_Resolution.thy | eventual_completion | Well-founded induction | Induction on nat pending count |
| DQuencer_Instance.thy | (none) | — | — |
Of the 5 sorry, three (select_highest_*) are likely to resolve once highest_priority_exists is solved. eventual_completion requires a separate induction construction.
That DQuencer_Instance.thy has zero sorry is noteworthy. The instantiations and the combined theorem are all built on previously proven lemmas.
Design Decisions in the Modeling Process
Decision 1: nat Tuples vs Custom Datatype
The first fork was whether to use nat × nat × nat × nat for the priority key or define a dedicated datatype priority_key with manual linorder registration.
A dedicated datatype offers stronger type safety. nat × nat × nat × nat accepts any 4-tuple, while a dedicated datatype constrains construction to meaningful values only. However, the cost of linorder instance registration is substantial: defining less_eq and less, proving antisym, trans, and total, then proving that this order coincides with the intended lexicographic order. Property 2’s core contribution is not the order structure itself but the liveness proofs built on top of it, making excessive engineering effort on the order structure inefficient.
The choice of nat tuples was driven by three factors: automatic linorder provision, reduced modeling complexity, and focus on the essential contribution.
Decision 2: BFT Consensus Abstraction Level
Should we formalize BLS signatures? Model the vote counting process? Or assume only the determinism of consensus output?
Formal verification of consensus protocols is a complete research topic on its own. Tendermint’s TLA+ specification and Gasper’s Dafny verification were each independent research projects. Including consensus protocol verification in Property 2’s scope would expand the proof goal from “liveness under Byzantine faults” to “BFT consensus correctness + liveness under Byzantine faults,” significantly reducing feasibility.
The chosen abstraction: express that the consensus output is the highest-priority valid message as a structural property of the model, while leaving the fact that BFT consensus actually achieves this outside the proof scope. The bft_select function is this abstraction’s implementation.
Decision 3: Radical Simplification of Locale Signatures
In the initial design, the three locales’ signatures were far heavier than their final form. priority_system included messages :: "'m set" as a locale fix, making the message set itself a fixed parameter of the locale. deadlock_free_locking had six fixes: resources, is_locked, lock_holder, lock_time, timeout, and current_time.
During the actual .thy writing process, we drastically reduced these signatures. messages was removed from priority_system and converted to a theorem argument S. In deadlock_free_locking, only timeout :: nat remained, with all other parameters moved to definitions and theorem arguments.
The motivation for this change was locale reusability. The more parameters included in locale fixes, the more assumptions must be satisfied during instantiation, narrowing the locale’s scope. The core insight of deadlock_free_locking is that “if the timeout is positive, deadlock cannot occur,” and expressing this requires neither the resource set nor lock holder information. The single assumption timeout > 0 suffices to prove both lock_eventually_expires and deadlock_freedom.
The initial design also included a dquencer_state record (containing epoch, leader, pending queue, and lock timestamps for the complete D-quencer state). In the actual implementation, this was removed and distributed across locale parameters: dquencer_system for system-wide constants and dquencer_liveness for schedule-specific functions. A monolithic state record creates the burden of handling irrelevant fields in every proof step. Distribution means each theorem explicitly uses only the parameters it actually depends on, producing cleaner proof structures.
The planned to_oss_message conversion function from the design document also became unnecessary. Isabelle’s record inheritance makes dq_message a subtype of oss_message, so existing field accessors (msg_action, msg_asset_id, etc.) work directly on dq_message. Automatic subtyping replaced explicit conversion, making both code and proofs more concise.
These simplifications were not planned in advance but discovered during the actual writing of the .thy files. A similar experience occurred in Property 1, where the proving process revealed that separating consistent_state and no_locked_without_reason was more natural than the initial monolithic valid_state. In formal verification, the difference between the design document and the final code is not failure but evidence that the proof tool reveals better structure.
Decision 4: Accepting the Closed-System Assumption
The non_honest_bounded assumption (pending queue non-increase during dishonest leader epochs) presupposes a closed system. In an open system with continual request arrivals, this assumption does not hold, and starvation freedom would require modeling the relationship between arrival rate and throughput.
The reason for accepting this assumption: Property 2’s goal is to show that “a given finite set of regulatory requests is fully processed.” Arrival rate analysis belongs to queueing theory, requiring different methodological tools than formal verification. Recognizing the limitation, recording it explicitly, and providing strong guarantees within the current scope is the honest approach.
Next Steps: Sorry Elimination
Five sorry remain. The next post will document the process of eliminating them. From Property 1’s experience, sorry elimination was not mere debugging but an opportunity to improve the model structure itself. The redesign of fold to λ during the regulatory_homomorphism proof is one example.
We expect similar discoveries in Property 2. Whether the Finite_Set library connection in highest_priority_exists works as expected, and how directly the well-founded induction in eventual_completion can be constructed, can only be determined by attempting the actual proofs. Just as unexpected difficulties arose in Property 1 where they were least anticipated, the same will be true for Property 2.
References
[1]. Lochbihler, A., Schneider, J. (2021). Mechanizing Authenticated Data Structures in Isabelle/HOL. CPP 2021. https://dl.acm.org/doi/10.1145/3437992.3439921
[2]. Nipkow, T., Paulson, L., Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer. https://isabelle.in.tum.de/doc/tutorial.pdf
[3]. Nipkow, T., Klein, G. (2014). Concrete Semantics with Isabelle/HOL. Springer. https://concrete-semantics.org/
Learn More
Defining D-quencer Liveness under Byzantine Faults
Cross-Domain State Preservation: What Was Proven and What It Means
