Add basic optimisations

[JonasAlaif]

@Aurel300 (do not want to merge, just in case you want to borrow any of the diff). Also this is the program that fails:

use prusti_contracts::*;

pub struct Vector {
    len: usize,
    contents: i32, 
}

impl Vector {
    #[pure]
    #[trusted]
    #[requires(idx < self.len)]
    fn get(self, idx: usize) -> i32 {
        unimplemented!()
    }

    #[trusted]
    #[requires(idx < self.len)]
    #[ensures(result.0 == self.get(idx))]
    #[ensures(result.1 === self)]
    fn impure_get(self, idx: usize) -> (i32, Self) {
        unimplemented!()
    }

    #[trusted]
    #[requires(idx < self.len)]
    #[ensures(self.len == result.len)]
    #[ensures(result.get(idx) == value)]
    #[ensures(forall(|i : usize| (i < self.len && i != idx) ==> result.get(i) == self.get(i)))]
    fn set(self, idx: usize, value: i32) -> Self {
        unimplemented!()
    }
}

struct Bounds {
    max: i32,
    min: i32,
}

struct ClampTransform {
    bounds: Bounds,
}

struct Output {
    vec: FallibleVec,
    transform: ClampTransform,
}

struct ImpureOutput {
    res: FallibleI32,
    transform: ClampTransform,
}

#[requires(data.len >= 1)]
#[requires(idx < data.len)]
#[ensures(result.transform === transform)]
#[ensures(transform.bounds.min <= transform.bounds.max <==>
    matches!(result.vec, FallibleVec::Ok(_)))]
#[ensures(matches!(result.vec, FallibleVec::Ok(_)) ==>
    result.vec.unwrap_vec().len === data.len)]
#[ensures(matches!(result.vec, FallibleVec::Ok(_)) ==>
    forall(|i: usize| (i > idx && i < data.len)  ==>
    result.vec.unwrap_vec().get(i) == data.get(i)))]

#[ensures(matches!(result.vec, FallibleVec::Ok(_)) ==>
    (transform.bounds.min <= transform.bounds.max ==>
        forall(|i: usize| i <= idx ==>
            result.vec.unwrap_vec().get(i) == transform.do_transform(data.get(i)))))]
#[ensures(
    forall(|i: usize|
        (matches!(result.vec, FallibleVec::Ok(_)) && transform.bounds.min <= transform.bounds.max && i <= idx) ==>
        {
            let res_val = result.vec.unwrap_vec().get(i);
            res_val >= transform.bounds.min &&
            res_val <= transform.bounds.max
        }
    ))]


fn apply_row_by_row_rec(
    transform: ClampTransform,
    data: Vector,
    idx: usize,
) -> Output {
    let mut transform = transform;
    let mut data = data;
    if idx >= 1 {
        let rec_output = apply_row_by_row_rec(transform, data, idx - 1);
        match rec_output.vec {
            FallibleVec::Ok(vec) => { 
                data = vec;
                transform = rec_output.transform;
            },
            FallibleVec::Err => return rec_output,
        };
    }

    let (cur, data) = data.impure_get(idx);
    let impure_output = transform.do_transform_impure(cur);
    transform = impure_output.transform;

    if let FallibleI32::Ok(clamped_val) = impure_output.res {
        let data = data.set(idx, clamped_val);
        return Output { vec: FallibleVec::Ok(data), transform: transform };
    }

    Output { vec: FallibleVec::Err, transform: transform }
}

enum FallibleVec {
    Ok(Vector),
    Err,
}

enum FallibleI32 {
    Ok(i32),
    Err,
}

#[trusted]
#[pure]
#[requires(false)]
fn unreachable_i32() -> i32 {
    unreachable!()
}

#[trusted]
#[pure]
#[requires(false)]
fn unreachable_vec() -> Vector {
    unreachable!()
}

impl FallibleI32 {
    #[pure]
    #[requires(matches!(self, FallibleI32::Ok(_)))]
    fn unwrap_i32(self) -> i32 {
        match self {
            FallibleI32::Ok(val) => val,
            FallibleI32::Err => unreachable_i32(),
        }
    }
}

impl FallibleVec {
    #[pure]
    #[requires(matches!(self, FallibleVec::Ok(_)))]
    fn unwrap_vec(self) -> Vector {
        match self {
            FallibleVec::Ok(val) => val,
            FallibleVec::Err => unreachable_vec(),
        }
    }
}

impl ClampTransform {
    #[trusted]
    #[ensures(result.bounds === bounds)]
    fn make_clamp(bounds: Bounds) -> Self {
        Self { bounds }
    }

    #[pure]
    #[requires(self.bounds.min <= self.bounds.max)]
    #[ensures(result >= self.bounds.min && result <= self.bounds.max)]
    #[ensures(data < self.bounds.min ==> result == self.bounds.min)]
    #[ensures(data > self.bounds.max ==> result == self.bounds.max)]
    #[ensures(data >= self.bounds.min && data <= self.bounds.max ==> result == data)]
    fn do_transform(self, data: i32) -> i32 {
        if data < self.bounds.min {
            self.bounds.min
        } else if data > self.bounds.max {
            self.bounds.max
        } else {
            data
        }
    }

    #[trusted]
    #[ensures(self.bounds.min <= self.bounds.max <==> matches!(result.res, FallibleI32::Ok(_)))]
    #[ensures(self.bounds.min <= self.bounds.max ==> result.res.unwrap_i32() === self.do_transform(data))]
    #[ensures(result.transform === self)]
    fn do_transform_impure(self, data: i32) -> ImpureOutput {
        if self.bounds.min > self.bounds.max {
            ImpureOutput { res: FallibleI32::Err, transform: self }
        } else if data < self.bounds.min {
            ImpureOutput { res: FallibleI32::Ok(self.bounds.min), transform: self }
        } else if data > self.bounds.max {
            ImpureOutput { res: FallibleI32::Ok(self.bounds.max), transform: self }
        } else {
            ImpureOutput { res: FallibleI32::Ok(data), transform: self }
        }
    }
}