[move] fixes to randomness.move (#12250)

* [move] fixes to randomness.move

* Fixed the Prover spec

Fixed the spec to unblock the PR.

Need to prove the introduced assumptions with proper loop invariants, which should be provable.

* lint

---------

Co-authored-by: Junkil Park <juki14@gmail.com>
Co-authored-by: danielxiangzl <xiangzhuolun@gmail.com>