Marcus (agent-cos)
6c6daaf90f
- New generator: compiler/src/generators/z3.ts (1,034 lines) - Translates SpeckDL state → Z3 sort declarations - Translates invariants → Z3 define-fun returning Bool - Translates actions → Z3 transition predicates (enabled + step) - BMC unrolling with --verify-depth=N (default: 10) - CLI: --target=z3 or --target=all - ToggleSwitch and TigerBeetleLedger generate valid SMT-LIB2 - KafkaKRaft spec generates valid SMT-LIB2 structure - Complex forall/set expressions emit 'true' as placeholders (to be improved) - All 41 existing tests still pass This unblocks M1.2 (KRaft verification), M3.2 (Show HN), and M4.3 (OAuth verification).
120 lines
2.5 KiB
Text
120 lines
2.5 KiB
Text
; SpeckDL: KafkaKRaft — Z3 Verification
|
|
; Generated by speckl-compile Z3 backend
|
|
; Bounded model checking depth: 10
|
|
|
|
(set-logic ALL)
|
|
(set-option :produce-models true)
|
|
(declare-sort State 0)
|
|
(declare-sort Option(NodeId) 0)
|
|
(declare-sort LogEntry 0)
|
|
(declare-sort NodeId 0)
|
|
|
|
; --- State Variables ---
|
|
(declare-const currentTerm Int)
|
|
(declare-const state State)
|
|
(declare-const votedFor Option(NodeId))
|
|
(declare-const log (Array Int LogEntry))
|
|
(declare-const commitIndex Int)
|
|
(declare-const nextIndex (Array NodeId Int))
|
|
(declare-const matchIndex (Array NodeId Int))
|
|
(declare-const votesGranted (Array NodeId Bool))
|
|
|
|
; --- Invariants ---
|
|
(define-fun ElectionSafety () Bool
|
|
(and
|
|
true
|
|
)
|
|
)
|
|
(define-fun LeaderCompleteness () Bool
|
|
(and
|
|
true
|
|
)
|
|
)
|
|
(define-fun LogMatching () Bool
|
|
(and
|
|
true
|
|
)
|
|
)
|
|
(define-fun LeaderAppendOnly () Bool
|
|
(and
|
|
true
|
|
)
|
|
)
|
|
(define-fun TermMonotonicity () Bool
|
|
(and
|
|
currentTerm' >= currentTerm
|
|
)
|
|
)
|
|
(define-fun CommitSafety () Bool
|
|
(and
|
|
true
|
|
)
|
|
)
|
|
|
|
; --- Action Transition Predicates ---
|
|
(define-fun RequestVoteEnabled () Bool
|
|
(and
|
|
state = Candidate
|
|
currentTerm >= lastLogTerm
|
|
)
|
|
)
|
|
(define-fun RequestVoteStep () Bool
|
|
(and
|
|
(= votesGranted_post (store votesGranted candidate true))
|
|
)
|
|
)
|
|
(define-fun HandleRequestVoteRequestEnabled () Bool
|
|
(and
|
|
currentTerm >= candidateTerm
|
|
)
|
|
)
|
|
(define-fun HandleRequestVoteRequestStep () Bool
|
|
(and
|
|
(= votedFor_post Some(candidate))
|
|
)
|
|
)
|
|
(define-fun BecomeLeaderEnabled () Bool
|
|
(and
|
|
state = Candidate
|
|
votesGranted.size() >= 3
|
|
)
|
|
)
|
|
(define-fun BecomeLeaderStep () Bool
|
|
(and
|
|
(= state_post Leader)
|
|
(= commitIndex_post length(log))
|
|
)
|
|
)
|
|
(define-fun AppendEntriesEnabled () Bool
|
|
(and
|
|
state = Leader
|
|
)
|
|
)
|
|
(define-fun AppendEntriesStep () Bool
|
|
(and
|
|
(= log_post append(log, newEntry))
|
|
)
|
|
)
|
|
; Next transition relation: RequestVote | HandleRequestVoteRequest | BecomeLeader | AppendEntries
|
|
(define-fun Next () Bool
|
|
(or
|
|
(and (RequestVoteEnabled) (RequestVoteStep))
|
|
(and (HandleRequestVoteRequestEnabled) (HandleRequestVoteRequestStep))
|
|
(and (BecomeLeaderEnabled) (BecomeLeaderStep))
|
|
(and (AppendEntriesEnabled) (AppendEntriesStep))
|
|
; Stuttering step
|
|
(and
|
|
(= currentTerm_post currentTerm)
|
|
(= state_post state)
|
|
(= votedFor_post votedFor)
|
|
(= log_post log)
|
|
(= commitIndex_post commitIndex)
|
|
(= nextIndex_post nextIndex)
|
|
(= matchIndex_post matchIndex)
|
|
(= votesGranted_post votesGranted)
|
|
)
|
|
)
|
|
)
|
|
|
|
(check-sat)
|
|
(get-model)
|