Add loop_invariant and harness for array reverse#430

thanhnguyen-aws wants to merge 8 commits intomodel-checking:mainmodel-checking/verify-rust-std:mainfrom

thanhnguyen-aws:reverseinvariantthanhnguyen-aws/verify-rust-std:reverseinvariantCopy head branch name to clipboard