sscoble/speckl
1
0
Fork 0
Code Issues 2 Pull requests Projects Releases Packages Wiki Activity Actions
speckl/out/TigerBeetleLedger.smt2
Scott Scoble 8b520284cb TS generator: fix #12 (5 expression patterns) + #11 (opaque record types) 
#12: All 5 untranslated SpeckDL patterns now emit valid JS:
  - notIn → !.has(), old() → drop, union → Set spread,
    set diff → filter, append() → [...X, Y], length() → .length
  - ==/!= operator replacement fixed (word-boundary regression)
  - Postcondition object comparisons get @ts-expect-error TS2839

#11: Generator auto-detects opaque identifier types used in state
  variables and action params, emits 'type X = any' before class.
  - State properties use ! (non-null assertion) for strict mode

TigerBeetleLedger → tsc --noEmit = 0 errors. 37/37 tests pass.
2026-05-11 10:16:15 -07:00

3143 lines
98 KiB
Text
Raw Blame History

; SpeckDL: TigerBeetleLedger — Z3 Verification
; Generated by speckl-compile Z3 backend
; Bounded model checking depth: 10
(set-logic ALL)
(set-option :produce-models true)
(declare-fun speckl_len_Int ( (Array Int Int) ) Int)
(declare-sort Account 0)
(declare-sort Transfer 0)
(declare-sort Replica 0)
(declare-sort LogEntry 0)
; --- State Variables ---
(declare-const accounts (Array Int Account))
(declare-const transfers (Array Int Transfer))
(declare-const pending (Array Int Bool))
(declare-const replicaState (Array Int Replica))
(declare-const log (Array Int LogEntry))
(declare-const commitIndex Int)
(declare-const leader Int)
; --- Invariants ---
(define-fun AccountBalanceInvariant () Bool
(and
(forall ((a Account)) (- (= a_balance a_credits_posted) a_debits_posted))
(forall ((a Account)) (>= a_debits_pending 0) (>= a_credits_pending 0))
)
)
(define-fun TransferStateConsistency () Bool
(and
(forall ((t Transfer)) t_pending ((=> true true)))
(forall ((t Transfer)) t_posted ((=> true true)))
(forall ((t Transfer)) t_voided ((=> true true)))
)
)
(define-fun NoOverdraft () Bool
(and
(forall ((a Account)) (or (>= a_balance 0) a_flags.allows_overdraft))
)
)
; --- Action Transition Predicates ---
(define-fun CreateTransferEnabled () Bool
(and
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts t_from).(>= balance t_amount) (select accounts t_from).flags_allows_overdraft)
)
)
(define-fun CommitTransferEnabled () Bool
(and
(select pending id)
(select transfers_keys id)
(select transfers id).(= pending true)
)
)
(define-fun VoidTransferEnabled () Bool
(and
(select pending id)
(select transfers_keys id)
(select transfers id).(= pending true)
)
)
(define-fun PostTransferEnabled () Bool
(and
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts t_from).(>= balance t_amount) (select accounts t_from).flags_allows_overdraft)
)
)
(define-fun BecomeLeaderEnabled () Bool
(and
(select replicaState_keys replica)
(select replicaState replica).(= role "candidate")
(< (select replicaState replica).currentTerm term)
)
)
(define-fun AppendEntryEnabled () Bool
(and
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex)
)
)
; Next transition relation: CreateTransfer | CommitTransfer | VoidTransfer | PostTransfer | BecomeLeader | AppendEntry
(define-fun Next () Bool
(or
(and (CreateTransferEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
(and (CommitTransferEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
(and (VoidTransferEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
(and (PostTransferEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
(and (BecomeLeaderEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
(and (AppendEntryEnabled)
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
; Stuttering step
(and
(= accounts_post accounts)
(= transfers_post transfers)
(= pending_post pending)
(= replicaState_post replicaState)
(= log_post log)
(= commitIndex_post commitIndex)
(= leader_post leader)
)
)
)
; --- Bounded Model Checking ---
; Verification: Always(AccountBalanceInvariant)
; BMC depth: 10
; Declare state copies for 10 steps
(declare-const accounts_0 (Array Int Account))
(declare-const accounts_1 (Array Int Account))
(declare-const accounts_2 (Array Int Account))
(declare-const accounts_3 (Array Int Account))
(declare-const accounts_4 (Array Int Account))
(declare-const accounts_5 (Array Int Account))
(declare-const accounts_6 (Array Int Account))
(declare-const accounts_7 (Array Int Account))
(declare-const accounts_8 (Array Int Account))
(declare-const accounts_9 (Array Int Account))
(declare-const accounts_10 (Array Int Account))
(declare-const transfers_0 (Array Int Transfer))
(declare-const transfers_1 (Array Int Transfer))
(declare-const transfers_2 (Array Int Transfer))
(declare-const transfers_3 (Array Int Transfer))
(declare-const transfers_4 (Array Int Transfer))
(declare-const transfers_5 (Array Int Transfer))
(declare-const transfers_6 (Array Int Transfer))
(declare-const transfers_7 (Array Int Transfer))
(declare-const transfers_8 (Array Int Transfer))
(declare-const transfers_9 (Array Int Transfer))
(declare-const transfers_10 (Array Int Transfer))
(declare-const pending_0 (Array Int Bool))
(declare-const pending_1 (Array Int Bool))
(declare-const pending_2 (Array Int Bool))
(declare-const pending_3 (Array Int Bool))
(declare-const pending_4 (Array Int Bool))
(declare-const pending_5 (Array Int Bool))
(declare-const pending_6 (Array Int Bool))
(declare-const pending_7 (Array Int Bool))
(declare-const pending_8 (Array Int Bool))
(declare-const pending_9 (Array Int Bool))
(declare-const pending_10 (Array Int Bool))
(declare-const replicaState_0 (Array Int Replica))
(declare-const replicaState_1 (Array Int Replica))
(declare-const replicaState_2 (Array Int Replica))
(declare-const replicaState_3 (Array Int Replica))
(declare-const replicaState_4 (Array Int Replica))
(declare-const replicaState_5 (Array Int Replica))
(declare-const replicaState_6 (Array Int Replica))
(declare-const replicaState_7 (Array Int Replica))
(declare-const replicaState_8 (Array Int Replica))
(declare-const replicaState_9 (Array Int Replica))
(declare-const replicaState_10 (Array Int Replica))
(declare-const log_0 (Array Int LogEntry))
(declare-const log_1 (Array Int LogEntry))
(declare-const log_2 (Array Int LogEntry))
(declare-const log_3 (Array Int LogEntry))
(declare-const log_4 (Array Int LogEntry))
(declare-const log_5 (Array Int LogEntry))
(declare-const log_6 (Array Int LogEntry))
(declare-const log_7 (Array Int LogEntry))
(declare-const log_8 (Array Int LogEntry))
(declare-const log_9 (Array Int LogEntry))
(declare-const log_10 (Array Int LogEntry))
(declare-const commitIndex_0 Int)
(declare-const commitIndex_1 Int)
(declare-const commitIndex_2 Int)
(declare-const commitIndex_3 Int)
(declare-const commitIndex_4 Int)
(declare-const commitIndex_5 Int)
(declare-const commitIndex_6 Int)
(declare-const commitIndex_7 Int)
(declare-const commitIndex_8 Int)
(declare-const commitIndex_9 Int)
(declare-const commitIndex_10 Int)
(declare-const leader_0 Int)
(declare-const leader_1 Int)
(declare-const leader_2 Int)
(declare-const leader_3 Int)
(declare-const leader_4 Int)
(declare-const leader_5 Int)
(declare-const leader_6 Int)
(declare-const leader_7 Int)
(declare-const leader_8 Int)
(declare-const leader_9 Int)
(declare-const leader_10 Int)
; Initial state constraints
(assert
(and
(>= commitIndex_0 0)
(>= leader_0 0)
)
)
; Transition constraints
(assert ; Step 0 → 1
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: CommitTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: VoidTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_0 replica).(= role "candidate")
(< (select replicaState_0 replica).currentTerm term)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_0)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
; Stuttering
(and
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
)
)
(assert ; Step 1 → 2
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: CommitTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: VoidTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_1 replica).(= role "candidate")
(< (select replicaState_1 replica).currentTerm term)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_1)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
; Stuttering
(and
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
)
)
(assert ; Step 2 → 3
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: CommitTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: VoidTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_2 replica).(= role "candidate")
(< (select replicaState_2 replica).currentTerm term)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_2)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
; Stuttering
(and
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
)
)
(assert ; Step 3 → 4
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: CommitTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: VoidTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_3 replica).(= role "candidate")
(< (select replicaState_3 replica).currentTerm term)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_3)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
; Stuttering
(and
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
)
)
(assert ; Step 4 → 5
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: CommitTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: VoidTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_4 replica).(= role "candidate")
(< (select replicaState_4 replica).currentTerm term)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_4)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
; Stuttering
(and
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
)
)
(assert ; Step 5 → 6
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: CommitTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: VoidTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_5 replica).(= role "candidate")
(< (select replicaState_5 replica).currentTerm term)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_5)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
; Stuttering
(and
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
)
)
(assert ; Step 6 → 7
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: CommitTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: VoidTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_6 replica).(= role "candidate")
(< (select replicaState_6 replica).currentTerm term)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_6)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
; Stuttering
(and
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
)
)
(assert ; Step 7 → 8
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: CommitTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: VoidTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_7 replica).(= role "candidate")
(< (select replicaState_7 replica).currentTerm term)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_7)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
; Stuttering
(and
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
)
)
(assert ; Step 8 → 9
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: CommitTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: VoidTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_8 replica).(= role "candidate")
(< (select replicaState_8 replica).currentTerm term)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_8)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
; Stuttering
(and
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
)
)
(assert ; Step 9 → 10
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: CommitTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: VoidTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_9 replica).(= role "candidate")
(< (select replicaState_9 replica).currentTerm term)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_9)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
; Stuttering
(and
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
)
)
; Property assertion: not(invariant at some step)
; Warning: invariant "unnamed" not found in spec
(check-sat)
(get-model)
; Verification: Always(NoOverdraft)
; BMC depth: 10
; Declare state copies for 10 steps
(declare-const accounts_0 (Array Int Account))
(declare-const accounts_1 (Array Int Account))
(declare-const accounts_2 (Array Int Account))
(declare-const accounts_3 (Array Int Account))
(declare-const accounts_4 (Array Int Account))
(declare-const accounts_5 (Array Int Account))
(declare-const accounts_6 (Array Int Account))
(declare-const accounts_7 (Array Int Account))
(declare-const accounts_8 (Array Int Account))
(declare-const accounts_9 (Array Int Account))
(declare-const accounts_10 (Array Int Account))
(declare-const transfers_0 (Array Int Transfer))
(declare-const transfers_1 (Array Int Transfer))
(declare-const transfers_2 (Array Int Transfer))
(declare-const transfers_3 (Array Int Transfer))
(declare-const transfers_4 (Array Int Transfer))
(declare-const transfers_5 (Array Int Transfer))
(declare-const transfers_6 (Array Int Transfer))
(declare-const transfers_7 (Array Int Transfer))
(declare-const transfers_8 (Array Int Transfer))
(declare-const transfers_9 (Array Int Transfer))
(declare-const transfers_10 (Array Int Transfer))
(declare-const pending_0 (Array Int Bool))
(declare-const pending_1 (Array Int Bool))
(declare-const pending_2 (Array Int Bool))
(declare-const pending_3 (Array Int Bool))
(declare-const pending_4 (Array Int Bool))
(declare-const pending_5 (Array Int Bool))
(declare-const pending_6 (Array Int Bool))
(declare-const pending_7 (Array Int Bool))
(declare-const pending_8 (Array Int Bool))
(declare-const pending_9 (Array Int Bool))
(declare-const pending_10 (Array Int Bool))
(declare-const replicaState_0 (Array Int Replica))
(declare-const replicaState_1 (Array Int Replica))
(declare-const replicaState_2 (Array Int Replica))
(declare-const replicaState_3 (Array Int Replica))
(declare-const replicaState_4 (Array Int Replica))
(declare-const replicaState_5 (Array Int Replica))
(declare-const replicaState_6 (Array Int Replica))
(declare-const replicaState_7 (Array Int Replica))
(declare-const replicaState_8 (Array Int Replica))
(declare-const replicaState_9 (Array Int Replica))
(declare-const replicaState_10 (Array Int Replica))
(declare-const log_0 (Array Int LogEntry))
(declare-const log_1 (Array Int LogEntry))
(declare-const log_2 (Array Int LogEntry))
(declare-const log_3 (Array Int LogEntry))
(declare-const log_4 (Array Int LogEntry))
(declare-const log_5 (Array Int LogEntry))
(declare-const log_6 (Array Int LogEntry))
(declare-const log_7 (Array Int LogEntry))
(declare-const log_8 (Array Int LogEntry))
(declare-const log_9 (Array Int LogEntry))
(declare-const log_10 (Array Int LogEntry))
(declare-const commitIndex_0 Int)
(declare-const commitIndex_1 Int)
(declare-const commitIndex_2 Int)
(declare-const commitIndex_3 Int)
(declare-const commitIndex_4 Int)
(declare-const commitIndex_5 Int)
(declare-const commitIndex_6 Int)
(declare-const commitIndex_7 Int)
(declare-const commitIndex_8 Int)
(declare-const commitIndex_9 Int)
(declare-const commitIndex_10 Int)
(declare-const leader_0 Int)
(declare-const leader_1 Int)
(declare-const leader_2 Int)
(declare-const leader_3 Int)
(declare-const leader_4 Int)
(declare-const leader_5 Int)
(declare-const leader_6 Int)
(declare-const leader_7 Int)
(declare-const leader_8 Int)
(declare-const leader_9 Int)
(declare-const leader_10 Int)
; Initial state constraints
(assert
(and
(>= commitIndex_0 0)
(>= leader_0 0)
)
)
; Transition constraints
(assert ; Step 0 → 1
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: CommitTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: VoidTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_0 replica).(= role "candidate")
(< (select replicaState_0 replica).currentTerm term)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_0)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
; Stuttering
(and
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
)
)
(assert ; Step 1 → 2
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: CommitTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: VoidTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_1 replica).(= role "candidate")
(< (select replicaState_1 replica).currentTerm term)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_1)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
; Stuttering
(and
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
)
)
(assert ; Step 2 → 3
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: CommitTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: VoidTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_2 replica).(= role "candidate")
(< (select replicaState_2 replica).currentTerm term)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_2)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
; Stuttering
(and
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
)
)
(assert ; Step 3 → 4
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: CommitTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: VoidTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_3 replica).(= role "candidate")
(< (select replicaState_3 replica).currentTerm term)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_3)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
; Stuttering
(and
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
)
)
(assert ; Step 4 → 5
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: CommitTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: VoidTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_4 replica).(= role "candidate")
(< (select replicaState_4 replica).currentTerm term)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_4)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
; Stuttering
(and
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
)
)
(assert ; Step 5 → 6
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: CommitTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: VoidTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_5 replica).(= role "candidate")
(< (select replicaState_5 replica).currentTerm term)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_5)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
; Stuttering
(and
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
)
)
(assert ; Step 6 → 7
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: CommitTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: VoidTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_6 replica).(= role "candidate")
(< (select replicaState_6 replica).currentTerm term)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_6)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
; Stuttering
(and
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
)
)
(assert ; Step 7 → 8
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: CommitTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: VoidTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_7 replica).(= role "candidate")
(< (select replicaState_7 replica).currentTerm term)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_7)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
; Stuttering
(and
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
)
)
(assert ; Step 8 → 9
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: CommitTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: VoidTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_8 replica).(= role "candidate")
(< (select replicaState_8 replica).currentTerm term)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_8)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
; Stuttering
(and
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
)
)
(assert ; Step 9 → 10
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: CommitTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: VoidTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_9 replica).(= role "candidate")
(< (select replicaState_9 replica).currentTerm term)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_9)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
; Stuttering
(and
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
)
)
; Property assertion: not(invariant at some step)
; Warning: invariant "unnamed" not found in spec
(check-sat)
(get-model)
; Verification: Eventually(TransferStateConsistency)
; BMC depth: 10
; Declare state copies for 10 steps
(declare-const accounts_0 (Array Int Account))
(declare-const accounts_1 (Array Int Account))
(declare-const accounts_2 (Array Int Account))
(declare-const accounts_3 (Array Int Account))
(declare-const accounts_4 (Array Int Account))
(declare-const accounts_5 (Array Int Account))
(declare-const accounts_6 (Array Int Account))
(declare-const accounts_7 (Array Int Account))
(declare-const accounts_8 (Array Int Account))
(declare-const accounts_9 (Array Int Account))
(declare-const accounts_10 (Array Int Account))
(declare-const transfers_0 (Array Int Transfer))
(declare-const transfers_1 (Array Int Transfer))
(declare-const transfers_2 (Array Int Transfer))
(declare-const transfers_3 (Array Int Transfer))
(declare-const transfers_4 (Array Int Transfer))
(declare-const transfers_5 (Array Int Transfer))
(declare-const transfers_6 (Array Int Transfer))
(declare-const transfers_7 (Array Int Transfer))
(declare-const transfers_8 (Array Int Transfer))
(declare-const transfers_9 (Array Int Transfer))
(declare-const transfers_10 (Array Int Transfer))
(declare-const pending_0 (Array Int Bool))
(declare-const pending_1 (Array Int Bool))
(declare-const pending_2 (Array Int Bool))
(declare-const pending_3 (Array Int Bool))
(declare-const pending_4 (Array Int Bool))
(declare-const pending_5 (Array Int Bool))
(declare-const pending_6 (Array Int Bool))
(declare-const pending_7 (Array Int Bool))
(declare-const pending_8 (Array Int Bool))
(declare-const pending_9 (Array Int Bool))
(declare-const pending_10 (Array Int Bool))
(declare-const replicaState_0 (Array Int Replica))
(declare-const replicaState_1 (Array Int Replica))
(declare-const replicaState_2 (Array Int Replica))
(declare-const replicaState_3 (Array Int Replica))
(declare-const replicaState_4 (Array Int Replica))
(declare-const replicaState_5 (Array Int Replica))
(declare-const replicaState_6 (Array Int Replica))
(declare-const replicaState_7 (Array Int Replica))
(declare-const replicaState_8 (Array Int Replica))
(declare-const replicaState_9 (Array Int Replica))
(declare-const replicaState_10 (Array Int Replica))
(declare-const log_0 (Array Int LogEntry))
(declare-const log_1 (Array Int LogEntry))
(declare-const log_2 (Array Int LogEntry))
(declare-const log_3 (Array Int LogEntry))
(declare-const log_4 (Array Int LogEntry))
(declare-const log_5 (Array Int LogEntry))
(declare-const log_6 (Array Int LogEntry))
(declare-const log_7 (Array Int LogEntry))
(declare-const log_8 (Array Int LogEntry))
(declare-const log_9 (Array Int LogEntry))
(declare-const log_10 (Array Int LogEntry))
(declare-const commitIndex_0 Int)
(declare-const commitIndex_1 Int)
(declare-const commitIndex_2 Int)
(declare-const commitIndex_3 Int)
(declare-const commitIndex_4 Int)
(declare-const commitIndex_5 Int)
(declare-const commitIndex_6 Int)
(declare-const commitIndex_7 Int)
(declare-const commitIndex_8 Int)
(declare-const commitIndex_9 Int)
(declare-const commitIndex_10 Int)
(declare-const leader_0 Int)
(declare-const leader_1 Int)
(declare-const leader_2 Int)
(declare-const leader_3 Int)
(declare-const leader_4 Int)
(declare-const leader_5 Int)
(declare-const leader_6 Int)
(declare-const leader_7 Int)
(declare-const leader_8 Int)
(declare-const leader_9 Int)
(declare-const leader_10 Int)
; Initial state constraints
(assert
(and
(>= commitIndex_0 0)
(>= leader_0 0)
)
)
; Transition constraints
(assert ; Step 0 → 1
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: CommitTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: VoidTransfer
(select pending_0 id)
(select transfers_keys id)
(select transfers_0 id).(= pending_0 true)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_0 t_from).(>= balance t_amount) (select accounts_0 t_from).flags_allows_overdraft)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_0 replica).(= role "candidate")
(< (select replicaState_0 replica).currentTerm term)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_0)
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
; Stuttering
(and
(= accounts_1 accounts_0)
(= transfers_1 transfers_0)
(= pending_1 pending_0)
(= replicaState_1 replicaState_0)
(= log_1 log_0)
(= commitIndex_1 commitIndex_0)
(= leader_1 leader_0)
)
)
)
(assert ; Step 1 → 2
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: CommitTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: VoidTransfer
(select pending_1 id)
(select transfers_keys id)
(select transfers_1 id).(= pending_1 true)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_1 t_from).(>= balance t_amount) (select accounts_1 t_from).flags_allows_overdraft)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_1 replica).(= role "candidate")
(< (select replicaState_1 replica).currentTerm term)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_1)
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
; Stuttering
(and
(= accounts_2 accounts_1)
(= transfers_2 transfers_1)
(= pending_2 pending_1)
(= replicaState_2 replicaState_1)
(= log_2 log_1)
(= commitIndex_2 commitIndex_1)
(= leader_2 leader_1)
)
)
)
(assert ; Step 2 → 3
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: CommitTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: VoidTransfer
(select pending_2 id)
(select transfers_keys id)
(select transfers_2 id).(= pending_2 true)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_2 t_from).(>= balance t_amount) (select accounts_2 t_from).flags_allows_overdraft)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_2 replica).(= role "candidate")
(< (select replicaState_2 replica).currentTerm term)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_2)
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
; Stuttering
(and
(= accounts_3 accounts_2)
(= transfers_3 transfers_2)
(= pending_3 pending_2)
(= replicaState_3 replicaState_2)
(= log_3 log_2)
(= commitIndex_3 commitIndex_2)
(= leader_3 leader_2)
)
)
)
(assert ; Step 3 → 4
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: CommitTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: VoidTransfer
(select pending_3 id)
(select transfers_keys id)
(select transfers_3 id).(= pending_3 true)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_3 t_from).(>= balance t_amount) (select accounts_3 t_from).flags_allows_overdraft)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_3 replica).(= role "candidate")
(< (select replicaState_3 replica).currentTerm term)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_3)
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
; Stuttering
(and
(= accounts_4 accounts_3)
(= transfers_4 transfers_3)
(= pending_4 pending_3)
(= replicaState_4 replicaState_3)
(= log_4 log_3)
(= commitIndex_4 commitIndex_3)
(= leader_4 leader_3)
)
)
)
(assert ; Step 4 → 5
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: CommitTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: VoidTransfer
(select pending_4 id)
(select transfers_keys id)
(select transfers_4 id).(= pending_4 true)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_4 t_from).(>= balance t_amount) (select accounts_4 t_from).flags_allows_overdraft)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_4 replica).(= role "candidate")
(< (select replicaState_4 replica).currentTerm term)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_4)
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
; Stuttering
(and
(= accounts_5 accounts_4)
(= transfers_5 transfers_4)
(= pending_5 pending_4)
(= replicaState_5 replicaState_4)
(= log_5 log_4)
(= commitIndex_5 commitIndex_4)
(= leader_5 leader_4)
)
)
)
(assert ; Step 5 → 6
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: CommitTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: VoidTransfer
(select pending_5 id)
(select transfers_keys id)
(select transfers_5 id).(= pending_5 true)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_5 t_from).(>= balance t_amount) (select accounts_5 t_from).flags_allows_overdraft)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_5 replica).(= role "candidate")
(< (select replicaState_5 replica).currentTerm term)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_5)
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
; Stuttering
(and
(= accounts_6 accounts_5)
(= transfers_6 transfers_5)
(= pending_6 pending_5)
(= replicaState_6 replicaState_5)
(= log_6 log_5)
(= commitIndex_6 commitIndex_5)
(= leader_6 leader_5)
)
)
)
(assert ; Step 6 → 7
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: CommitTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: VoidTransfer
(select pending_6 id)
(select transfers_keys id)
(select transfers_6 id).(= pending_6 true)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_6 t_from).(>= balance t_amount) (select accounts_6 t_from).flags_allows_overdraft)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_6 replica).(= role "candidate")
(< (select replicaState_6 replica).currentTerm term)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_6)
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
; Stuttering
(and
(= accounts_7 accounts_6)
(= transfers_7 transfers_6)
(= pending_7 pending_6)
(= replicaState_7 replicaState_6)
(= log_7 log_6)
(= commitIndex_7 commitIndex_6)
(= leader_7 leader_6)
)
)
)
(assert ; Step 7 → 8
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: CommitTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: VoidTransfer
(select pending_7 id)
(select transfers_keys id)
(select transfers_7 id).(= pending_7 true)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_7 t_from).(>= balance t_amount) (select accounts_7 t_from).flags_allows_overdraft)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_7 replica).(= role "candidate")
(< (select replicaState_7 replica).currentTerm term)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_7)
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
; Stuttering
(and
(= accounts_8 accounts_7)
(= transfers_8 transfers_7)
(= pending_8 pending_7)
(= replicaState_8 replicaState_7)
(= log_8 log_7)
(= commitIndex_8 commitIndex_7)
(= leader_8 leader_7)
)
)
)
(assert ; Step 8 → 9
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: CommitTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: VoidTransfer
(select pending_8 id)
(select transfers_keys id)
(select transfers_8 id).(= pending_8 true)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_8 t_from).(>= balance t_amount) (select accounts_8 t_from).flags_allows_overdraft)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_8 replica).(= role "candidate")
(< (select replicaState_8 replica).currentTerm term)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_8)
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
; Stuttering
(and
(= accounts_9 accounts_8)
(= transfers_9 transfers_8)
(= pending_9 pending_8)
(= replicaState_9 replicaState_8)
(= log_9 log_8)
(= commitIndex_9 commitIndex_8)
(= leader_9 leader_8)
)
)
)
(assert ; Step 9 → 10
(or
(and ; Action: CreateTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: CommitTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: VoidTransfer
(select pending_9 id)
(select transfers_keys id)
(select transfers_9 id).(= pending_9 true)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: PostTransfer
t_id notIn transfers_keys
(select accounts_keys t_from)
(select accounts_keys t_to)
t_from distinct t_to
(or (select accounts_9 t_from).(>= balance t_amount) (select accounts_9 t_from).flags_allows_overdraft)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: BecomeLeader
(select replicaState_keys replica)
(select replicaState_9 replica).(= role "candidate")
(< (select replicaState_9 replica).currentTerm term)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
(and ; Action: AppendEntry
(+ entry_index = (speckl_len_Int log) 1)
(>= term commitIndex_9)
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
; Stuttering
(and
(= accounts_10 accounts_9)
(= transfers_10 transfers_9)
(= pending_10 pending_9)
(= replicaState_10 replicaState_9)
(= log_10 log_9)
(= commitIndex_10 commitIndex_9)
(= leader_10 leader_9)
)
)
)
; Property assertion: not(invariant at some step)
(assert
(and
(not (unnamed_0))
(not (unnamed_1))
(not (unnamed_2))
(not (unnamed_3))
(not (unnamed_4))
(not (unnamed_5))
(not (unnamed_6))
(not (unnamed_7))
(not (unnamed_8))
(not (unnamed_9))
(not (unnamed_10))
)
)
(echo "Checking: Eventually(unnamed)")
(check-sat)
(get-model)
Reference in a new issue View git blame Copy permalink