randomness #10: randomness API update from randomnet (#12335)

* [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>

* fix specs

---------

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