┌──────────────────────────────────────────────────────┐
│  Layer 3: 完整正确性证明 (Kani/Verus/Creusot)         │
│           数学证明代码等价于数学模型                    │
│           适用：500行以内的核心算法                     │
│           成本：极高，需要专业训练                      │
├──────────────────────────────────────────────────────┤
│  Layer 2: 类型系统编码不变量 (Session Types/Typenum)  │
│           通过类型让非法状态不可表示                    │
│           适用：状态机、协议状态转换                    │
│           成本：中等，编译器代你检查                    │
├──────────────────────────────────────────────────────┤
│  Layer 1: Prusti/Smir 后置条件验证                    │
│           为函数编写前后置条件，自动验证                │
│           适用：关键不变量检查                          │
│           成本：较低，类似写断言但更强                  │
└──────────────────────────────────────────────────────┘

struct Node<S> { /* ... */ }
struct Follower;
struct Candidate;
struct Leader;

impl Node<Follower> {
    fn election_timeout(self) -> Node<Candidate> { /* ... */ }
}

use std::marker::PhantomData;

/// Raft 协议状态，用类型标记
trait RaftState {}
struct Follower { term: u64 }
struct Candidate { term: u64, votes_granted: u32 }
struct Leader { term: u64, next_index: Vec<u64> }

impl RaftState for Follower {}
impl RaftState for Candidate {}
impl RaftState for Leader {}

/// 消息类型，携带会话令牌
struct RaftMessage<S: RaftState> {
    term: u64,
    payload: RaftPayload,
    _marker: PhantomData<S>,
}

enum RaftPayload {
    RequestVote { last_log_index: u64, last_log_term: u64 },
    RequestVoteResponse { vote_granted: bool },
    AppendEntries { entries: Vec<LogEntry>, leader_commit: u64 },
    AppendEntriesResponse { success: bool, match_index: u64 },
}

/// 节点状态机：状态转换只能在合法路径上发生
struct RaftNode<S: RaftState> {
    state: S,
    log: Vec<LogEntry>,
    commit_index: u64,
}

/// Follower → Candidate：选举超时
impl RaftNode<Follower> {
    fn on_election_timeout(self) -> RaftNode<Candidate> {
        let new_term = self.state.term + 1;
        RaftNode {
            state: Candidate {
                term: new_term,
                votes_granted: 1, // 给自己投票
            },
            log: self.log,
            commit_index: self.commit_index,
        }
    }

    /// Follower 处理 AppendEntries：只有更高任期才接受
    fn handle_append_entries(self, msg: RaftMessage<Leader>) 
        -> Result<(RaftNode<Follower>, RaftMessage<Leader>), (RaftNode<Follower>, ImportError)> 
    {
        if msg.term < self.state.term {
            // 这是编译期可拒绝的错误：低任期 Leader 消息
            Err(self.send_reject(msg))
        } else {
            Ok(self.do_append(msg))
        }
    }
}

/// Candidate → Leader：获得多数票
impl RaftNode<Candidate> {
    fn on_vote_granted(mut self, quorum: u32) -> Result<RaftNode<Leader>, Self> {
        self.state.votes_granted += 1;
        if self.state.votes_granted >= quorum {
            Ok(RaftNode {
                state: Leader {
                    term: self.state.term,
                    next_index: vec![self.log.len() as u64; 3],
                },
                log: self.log,
                commit_index: self.commit_index,
            })
        } else {
            Ok(self) // 仍然是 Candidate, 等待更多选票
        }
    }
}

use typenum::*;

/// 集群大小在类型中编码
trait ClusterSize {
    type N: Unsigned;
    type Quorum: Unsigned; // N/2 + 1
}

/// 3节点集群
struct ThreeNodes;
impl ClusterSize for ThreeNodes {
    type N = U3;
    type Quorum = U2; // ceil(3/2) = 2
}

/// 多数票验证：编译期保证
fn grant_quorum<Q: Unsigned, N: Unsigned>(_n: PhantomData<N>, votes: u32) -> bool 
where
    Q: IsEqual<op!((N / U2) + U1)>,
{
    votes >= Q::U32
}

// 验证通过：2 >= 3/2+1 = 2
let result = grant_quorum::<U2, U3>(PhantomData, 2);
assert!(result);

use prusti_contracts::*;

#[ensures(result.index == old(log.len() as u64))]
#[ensures(result.term == term)]
#[ensures(
    old(log).iter().enumerate().all(|(i, e)| 
        log[i].index == e.index && log[i].term == e.term
    )
)]
#[ensures(log.len() == old(log.len()) + 1)]
fn append_entry(log: &mut Vec<LogEntry>, entry: LogEntry, term: u64) -> &LogEntry {
    let new_entry = LogEntry { index: log.len() as u64, term, command: entry.command };
    log.push(new_entry);
    log.last().unwrap()
}

#[ensures(
    result.iter().enumerate().all(|(i, e)| 
        i == 0 || result[i-1].index < e.index
    )
)]
fn verify_log_monotonic(log: &[LogEntry]) -> &[LogEntry] {
    log
}

// Layer 3 (Kani)：核心选主逻辑的无 panic 证明
#[cfg(kani)]
mod verification {
    use kani::any;

    #[kani::proof]
    fn proof_log_append_safe() {
        let mut log = Vec::<LogEntry>::new();
        for i in 0..10 {
            log.push(LogEntry { index: i, term: any(), command: any() });
        }
        // Kani 验证：不会 panic、不会越界、不会溢出
        verify_log_monotonic(&log);
    }
}

// Layer 2 (Session Types)：协议状态转换的正确性
mod protocol {
    use super::state_machine::RaftNode;
    pub use super::sessions::*;
}

// Layer 1 (Prusti)：关键函数的合约保证
#[cfg(feature = "verified")]
mod storage {
    use prusti_contracts::*;
    // 经过验证的持久化存储实现
}