Skip to content

Commit

Permalink
[move] fixes to randomness.move (#12250)
Browse files Browse the repository at this point in the history 
* [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 <[email protected]>
Co-authored-by: danielxiangzl <[email protected]>
  • Loading branch information
@alinush @junkil-park
@danielxiangzl @zjma
3 people authored and zjma committed Mar 1, 2024
1 parent 4a507f1 commit 5596b9b
Show file tree
Hide file tree
Showing 3 changed files with 480 additions and 47 deletions.
Loading

0 comments on commit 5596b9b

Please sign in to comment.