Add TimSort rewritten code

[Omar0Tarek]

rewriting TimSort implementation code to be ready for verification

[vakaras]

Add /home/data/eth/rust/prusti-dev2/prusti-tests/tests/cargotest.rs:

#[cargo_test]
fn test_timsort() {
    test_local_project("verifying_tim_sort");
}

[fpoli]

Is the temp file there by mistake?

[vakaras]

Please remove this file.

[vakaras]

@Omar0Tarek Please fix the errors so that the CI passes. You should be able to run the test locally as follows:

./x.py build --all; ./x.py test timsort

P. S. You need to run ./x.py setup if you have not done that already.

[Omar0Tarek]

I finished verifying the absence of panics and overflows.

When I run Prusti from the IDE, the verification succeeds, but when I run the CI tests locally, they fail producing the following error.

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__Snap$Slice$i32$ might not hold. There might be insufficient permission to access Slice$i32(_1.val_ref) (@0.0)

error: could not compile `verifying_tim_sort` due to previous error; 62 warnings emitted
', prusti-tests/tests/cargotest.rs:177:18
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[vakaras]

I finished verifying the absence of panics and overflows.

When I run Prusti from the IDE, the verification succeeds, but when I run the CI tests locally, they fail producing the following error.

error: [Prusti internal error] Prusti encountered an unexpected internal error
  |
  = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
  = note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [application.precondition:insufficient.permission; 0] Precondition of function snap$__$TY$__Snap$Slice$i32$ might not hold. There might be insufficient permission to access Slice$i32(_1.val_ref) (@0.0)

error: could not compile `verifying_tim_sort` due to previous error; 62 warnings emitted
', prusti-tests/tests/cargotest.rs:177:18
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I think this is caused by the example being very large and stressing the limits of the verifier. Since the example verifies on CI, it seems to be fine.