Implement and check optimizations

[enjhnsn2]

After the baseline verified runtime is completed, we will implement some optimizations and show that these optimizations preserve our safety properties. I will list out some potential optimizations as I think of them.

1. For system calls that use a mutable buffer (i.e., write), let the os copy data directly into the sandbox.
2. Use mmap instead of vector initialization to set up sandbox memory (faster startup).

[enjhnsn2]

3. Prove that sandbox memory and runtime memory are non-overlapping so we can use Rust's extra-fast copy optimization copy_nonoverlapping (memcpy) instead of copy (memmove)