use domain::message::Message;

#[kani::proof]
fn message_survives_pending_storage_roundtrip() {
    let w0: usize = kani::any();
    let w1: usize = kani::any();
    let w2: usize = kani::any();
    let w3: usize = kani::any();

    let original = Message::from_words([w0, w1, w2, w3]);

    let mut pending: [Option<Message>; 4] = [const { None }; 4];
    let idx: usize = kani::any();
    kani::assume(idx < 4);

    pending[idx] = Some(original);

    let retrieved = pending[idx].take();
    assert!(retrieved.is_some());

    let msg = retrieved.unwrap();
    assert!(msg.word(0) == w0);
    assert!(msg.word(1) == w1);
    assert!(msg.word(2) == w2);
    assert!(msg.word(3) == w3);
}

#[kani::proof]
fn message_storage_does_not_cross_slots() {
    let w_a: usize = kani::any();
    let w_b: usize = kani::any();
    kani::assume(w_a != w_b);

    let msg_a = Message::from_words([w_a, 0, 0, 0]);
    let msg_b = Message::from_words([w_b, 0, 0, 0]);

    let mut pending: [Option<Message>; 4] = [const { None }; 4];
    pending[0] = Some(msg_a);
    pending[1] = Some(msg_b);

    let retrieved_a = pending[0].take().unwrap();
    let retrieved_b = pending[1].take().unwrap();

    assert!(retrieved_a.word(0) == w_a);
    assert!(retrieved_b.word(0) == w_b);
}