[move] Updated Boogie native function skeletons

[awelc]

trafficstars

I am trying to get the Move prover to run on Sui's framework code again and this PR is one step towards it - it updates native function skeletons defined in Boogie (adds missing ones and removes ones that no longer reflect existing native functions). We are still blocked on https://github.com/move-language/move/issues/653 and https://github.com/move-language/move/issues/660 on the core Move side before we can run the prover but it still seems worthwhile to make this update since the code changes are ready.

[vercel[bot]]

The latest updates on your projects. Learn more about Vercel for Git ↗︎

Name	Status	Preview	Updated
explorer	✅ Ready (Inspect)	Visit Preview	Nov 9, 2022 at 2:49AM (UTC)

[c0wjay]

Hi, I'm very interested in this work - integrating move prover into sui. Is there anything I can do to help you?

[awelc]

Hi, I'm very interested in this work - integrating move prover into sui. Is there anything I can do to help you?

First of, we love the enthusiasm! Our current plan is first get the prover working on the Sui Move codebase without any Sui-specific features supported (at this point we are seeing some problems in the borrow analyzer and the bytecode translator that need to be take can care of before this happens). This would allow us to start writing specs for functions that do not use any Sui-specific features (such as object transfers), for example those that deal with modifying objects passed by mutable references.

We could use help in fleshing these out, but also in thinking on what kinds of properties about your favorite functions you would like to prove, and to sketch the specs for these functions even if the necessary features are not supported yet.

[c0wjay]

First of, we love the enthusiasm! Our current plan is first get the prover working on the Sui Move codebase without any Sui-specific features supported (at this point we are seeing some problems in the borrow analyzer and the bytecode translator that need to be take can care of before this happens). This would allow us to start writing specs for functions that do not use any Sui-specific features (such as object transfers), for example those that deal with modifying objects passed by mutable references.

We could use help in fleshing these out, but also in thinking on what kinds of properties about your favorite functions you would like to prove, and to sketch the specs for these functions even if the necessary features are not supported yet.

I am interested in both the move prover and the test_scenario module in sui, so I was reading the move prover code and boogie by myself. However, it was my first time contributing a code to Sui, so I didn't know how to start. I'm very interested in everything you've said - such as "get the prover working on the Sui Move codebase" or "implement specification of sui native functions", so I'd appreciate it if you could share the work freely if you need help.