tla-rs 0.1.0

#![allow(unused_imports)]
#![allow(unused_attributes)]
#![verus::trusted]
use builtin::*;
use builtin_macros::*;
use vstd::map::*;
use vstd::modes::*;
use vstd::multiset::*;
use vstd::pervasive::*;
use vstd::seq::*;

use crate::implementation::common::marshalling::Marshalable;

mod common;
mod implementation;
mod protocol;
mod services;
mod verus_extra;

use crate::common::native::io_s::EndPoint;
use crate::common::native::io_s::NetcReceiveResult;
use crate::services::RSL::main_i::*;

verus! {
    #[verifier(external)]
    #[verus::line_count::ignore]
    pub unsafe fn unflatten_args (
        num_args: i32,
        arg_lengths: *const i32,
        _total_arg_length: i32,
        flattened_args: *const u8
    ) -> Vec<Vec<u8>>
    {
        let mut offset: isize = 0;
        let mut args: Vec<Vec<u8>> = Vec::new();
        for i in 0..num_args as isize {
            let arg_length = *arg_lengths.offset(i as isize);
            let arg_array: &[u8] = std::slice::from_raw_parts(flattened_args.offset(offset), arg_length as usize);
            let arg_vec: std::vec::Vec<u8> = arg_array.to_vec();
            let mut arg: Vec<u8> = Vec::new();
            arg = arg_vec;
            args.push(arg);
            offset += arg_length as isize;
        }
        args
    }

    // This routine is exported to the C# main executable containing the I/O
    // framework. This lets the I/O framework allocate Rust buffers that it can fill
    // and return to us.
    //
    // For instance, suppose the I/O framework is about to receive a packet, and has
    // learned that packet's length. It will call `allocate_buffer`, and we'll
    // return to it two things: `buffer_ptr`, a pointer to a region of memory with
    // length `length`, and `box_vec_ptr`, a pointer that it will return to us when
    // we ask to receive a message.

    #[verifier(external)]
    #[no_mangle]
    #[verus::line_count::ignore]
    pub unsafe extern "C" fn allocate_buffer(
        length: u64,
        box_vec_ptr: *mut *mut std::vec::Vec<u8>,
        buffer_ptr: *mut *mut u8
    )
    {
        // Allocate a std::vec::Vec<u8> with the given length.
        let mut v: std::vec::Vec<u8> = std::vec::Vec::<u8>::with_capacity(length as usize);
        v.set_len(length as usize);

        // Box the vector.
        let mut b: Box<std::vec::Vec<u8>> = Box::<std::vec::Vec<u8>>::new(v);

        // Return the raw pointer to the vector's buffer as `*buffer_ptr`.
        *buffer_ptr = (*b).as_mut_ptr();

        // Return the raw pointer to the Box as `*box_vec_ptr`.
        *box_vec_ptr = Box::<std::vec::Vec<u8>>::into_raw(b);
    }

    // This routine is exported to the C# main executable containing the I/O
    // framework. This lets the I/O framework deallocate a Rust buffers that
    // it allocated with `allocate_buffer` that it was planning to return to
    // us but has now decided it doesn't want to return to us. For instance,
    // if the I/O framework allocated it to store an incoming packet, but
    // detected that the connection closed, it needs to free the buffer.

    #[verifier(external)]
    #[verus::line_count::ignore]
    #[no_mangle]
    pub unsafe extern "C" fn free_buffer(
        box_vec_ptr: *mut std::vec::Vec<u8>
    )
    {
        // Convert back from a raw pointer to a Box so that when the Box
        // goes out of scope at the end of this function, it will be
        // freed.
        let _box_vec: Box<std::vec::Vec<u8>> = Box::<std::vec::Vec<u8>>::from_raw(box_vec_ptr);
    }

    #[verifier(external)]
    #[verus::line_count::ignore]
    #[no_mangle]
    pub unsafe extern "C" fn rsl_main_wrapper(
        num_args: i32,
        arg_lengths: *const i32,
        total_arg_length: i32,
        flattened_args: *const u8,
        get_my_end_point_func: extern "C" fn(*mut *mut std::vec::Vec<u8>),
        get_time_func: extern "C" fn() -> u64,
        receive_func: extern "C" fn(i32, *mut bool, *mut bool, *mut *mut std::vec::Vec<u8>, *mut *mut std::vec::Vec<u8>),
        send_func: extern "C" fn(u64, *const u8, u64, *const u8) -> bool
    ) -> i32 {
        let args: Vec<Vec<u8>> = unflatten_args(num_args, arg_lengths, total_arg_length, flattened_args);

        let mut my_end_point_vec_ptr = std::mem::MaybeUninit::<*mut std::vec::Vec<u8>>::uninit();
        get_my_end_point_func(my_end_point_vec_ptr.as_mut_ptr());
        let my_end_point_ptr: *mut std::vec::Vec<u8> = my_end_point_vec_ptr.assume_init();
        let my_end_point_box: Box<std::vec::Vec<u8>> = Box::<std::vec::Vec<u8>>::from_raw(my_end_point_ptr);
        let my_end_point_vec: std::vec::Vec<u8> = *my_end_point_box;
        let mut my_end_point: Vec<u8> = Vec::new();
        my_end_point = my_end_point_vec;

        let mut nc = crate::common::native::io_s::NetClient::new(EndPoint{id: my_end_point}, get_time_func, receive_func, send_func);
        match paxos_main(nc, args) {
            Ok(_) => 0,
            Err(_) => 1,
        }
    }

    pub proof fn my_proof(x: bool) {
        
        // assert!(x==true);
        assert(1 + 1 == 2);
        
    }

    #[verifier(external_body)]
    pub fn main() {

        let x = vec![true as u8];
        let mut y: Vec<u8> = vec![];
        x.serialize(&mut y);
        let mut res = false;
        if let Some(z) = bool::deserialize(&y, 0){
            res = true;
        };
        let z = vec![false as u8];
        println!("test");
        assert!(x == z);

        proof {
            my_proof(true);
        }

        // let s: Seq<i32> = seq![1, 2, 3];
    }

}