Testing Process

[aa-luna]

RustyRelic Repo
Looking for best practice on testing? We were thinking of creating a separate cargo program and run new_unchecked?
Also checking in to see if our logic is on the right track. Took the feedback and used pointers within both the requires and ensures block.

• For our requires block we created a pointer for n and then slicing to make sure it is not 0

#[rustc_allow_const_fn_unstable(const_refs_to_cell)]
   #[requires({
       let size = core::mem::size_of::<T>();
       let ptr = &n as *const T as *const u8;
       let slice = unsafe { core::slice::from_raw_parts(ptr, size) };
       !slice.iter().all(|&byte| byte == 0)
   })]

• For our ensures block we are creating two pointers, one for result and one for n and making sure neither are 0.

#[ensures(|result: &Self|{
        let size = core::mem::size_of::<T>();
        let n_ptr: *const T = &n;
        let result_inner: T = result.get();
        let result_ptr: *const T = &result_inner;
        let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) };
        let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) };
    
        n_slice == result_slice
    })]

OUTPUT:

SUMMARY:
 ** 0 of 1772 failed (2 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.57577264s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

[celinval]

Hi @aa-luna, unfortunately the only way to check contracts today is through Kani harnesses.

We have this issue to enable it: model-checking/kani#3326. If this is something that you think would be helpful to you, please let us know so we can prioritize the issue.