Add support to shadow memory

[celinval]

Requested feature: Add support to shadow memory
Use case: Allow users to extend their code for verification without impacting runtime

Test case:

union Data {
    word: usize,
    byte: u8,
}

impl Data {
    unsafe fn assume_word(&self) -> usize {
        self.word
    }
    unsafe fn assume_byte(&self) -> u8 {
        self.byte
    }
}

struct Memory {
    data: [Data; 1024],
    word: bool,
}

impl Memory {
    unsafe fn read_word(&self, index: usize) -> usize {
        assert!(self.word);
        unsafe { self.data[index].assume_word() }
    }

    unsafe fn read_byte(&self, index: usize) -> u8 {
        assert!(!self.word);
        unsafe { self.data[index].assume_byte() }
    }

    fn new(word: bool) { /* */}
}

#[kani::proof]
fn check_memory() {
    // info
}

Dummy example where users may want to use shadow memory to track how this code is being used. E.g.: Shadow memory could be used to track if the union has been initialized and which type has been used.