anodized 0.4.0

use anodized::spec;

// Test simple identifier capturing with auto-generated alias
#[spec(
    captures: count,
    ensures: old_count <= *output,
)]
fn increment_counter(count: u32) -> u32 {
    count + 1
}

// Struct for testing
struct Container {
    value: i32,
    counter: u32,
    items: Vec<String>,
    capacity: usize,
}

impl Container {
    fn new() -> Self {
        Container {
            value: 0,
            counter: 0,
            items: Vec::new(),
            capacity: 10,
        }
    }

    fn is_valid(&self) -> bool {
        self.counter < 100
    }

    #[spec(
        captures: self.value as initial_value,
        ensures: self.value == initial_value + amount,
    )]
    fn add_to_value(&mut self, amount: i32) {
        self.value += amount;
    }

    #[spec(
        captures: self.items.clone() as original_items,
        ensures: self.items.len() == original_items.len() || self.items.len() == original_items.len() + 1,
    )]
    fn maybe_push(&mut self, item: String, should_push: bool) {
        if should_push {
            self.items.push(item);
        }
    }

    #[spec(
        captures: [
            self.items.len() as original_len,
            self.capacity as original_cap,
        ],
        ensures: [
            self.items.len() == original_len + 1,
            self.capacity >= original_cap,
        ],
    )]
    fn push_item(&mut self, item: String) {
        if self.items.len() == self.capacity {
            self.capacity *= 2;
        }
        self.items.push(item);
    }

    #[spec(
        requires: self.is_valid(),
        captures: self.counter as old_counter,
        ensures: self.counter == old_counter + 1,
    )]
    fn increment_if_valid(&mut self) {
        self.counter += 1;
    }
}

#[test]
fn simple_capture_with_auto_alias() {
    assert_eq!(increment_counter(5), 6);
    assert_eq!(increment_counter(0), 1);
}

#[test]
fn capture_with_explicit_alias() {
    let mut container = Container::new();
    container.value = 10;
    container.add_to_value(5);
    assert_eq!(container.value, 15);
}

#[test]
fn multiple_captures() {
    let mut container = Container::new();

    // Add items up to capacity
    for i in 0..10 {
        container.push_item(format!("item_{}", i));
    }
    assert_eq!(container.items.len(), 10);
    assert_eq!(container.capacity, 10);

    // This should trigger capacity doubling
    container.push_item("item_10".to_string());
    assert_eq!(container.items.len(), 11);
    assert_eq!(container.capacity, 20);
}

#[test]
fn captures_with_preconditions() {
    let mut container = Container::new();
    container.counter = 50;

    container.increment_if_valid();
    assert_eq!(container.counter, 51);
}

#[cfg(feature = "runtime-check-and-panic")]
#[test]
#[should_panic(expected = "Postcondition failed")]
fn capture_postcondition_failure() {
    #[spec(
        captures: *value as old_value,
        ensures: *value == old_value + 10,
    )]
    fn bad_increment(value: &mut i32) {
        // Wrong! Should add 10
        *value += 5
    }

    let mut val = 5;
    bad_increment(&mut val);
}

#[cfg(feature = "runtime-check-and-panic")]
#[test]
#[should_panic(expected = "Precondition failed")]
fn precondition_runs_before_captures() {
    struct TestStruct {
        counter: u32,
    }

    impl TestStruct {
        #[spec(
            requires: self.counter < 100,
            captures: self.counter as old_counter,
            ensures: self.counter == old_counter + 1,
        )]
        fn increment(&mut self) {
            self.counter += 1;
        }
    }

    let mut test = TestStruct { counter: 100 };
    // Should panic on precondition, not reach captures
    test.increment();
}

#[test]
fn explicit_clone_for_non_copy_types() {
    let mut container = Container::new();
    container.items.push("first".to_string());
    container.items.push("second".to_string());

    // Should not push
    container.maybe_push("third".to_string(), false);
    assert_eq!(container.items.len(), 2);

    // Should push
    container.maybe_push("third".to_string(), true);
    assert_eq!(container.items.len(), 3);
}

#[derive(Debug, Clone, Copy)]
struct Point {
    x: i32,
    y: i32,
}

#[spec(
    captures: arr as [first, second, third],
    ensures: [
        first == arr[0],
        second == arr[1],
        third == arr[2],
    ],
)]
fn match_array(arr: [i32; 3]) {
    println!("Array elements: {}, {}, {}", arr[0], arr[1], arr[2]);
}

#[spec(
    captures: tuple as (a, b, c),
    ensures: [
        a + b + c == tuple.0 + tuple.1 + tuple.2,
    ],
)]
fn match_tuple(tuple: (i32, i32, i32)) {
    let (a, b, c) = tuple;
    println!("Sum: {}, Product: {}", a + b + c, a * b * c);
}

#[spec(
    captures: point as Point { x, y },
    ensures: [
        x == point.x,
        y == point.y,
    ],
)]
fn match_struct(point: Point) {
    println!("Point: ({}, {})", point.x, point.y);
}

#[spec(
    captures: [a, b, c] as slice,
    ensures: [
        slice[0] == a,
        slice[1] == b,
        slice[2] == c,
    ],
)]
fn capture_as_array(a: i32, b: i32, c: i32) {
    println!("Captured as array: {:?}", [a, b, c]);
}

#[test]
fn match_array_success() {
    let numbers = [1, 2, 3];
    match_array(numbers);
}

#[test]
fn match_tuple_success() {
    let coords = (3, 4, 5);
    match_tuple(coords);
}

#[test]
fn match_struct_success() {
    let point = Point { x: 5, y: -3 };
    match_struct(point);
}

#[test]
fn capture_as_array_success() {
    capture_as_array(10, 20, 30);
}