[move] Implement Boogie native function for address module

[c0wjay]

trafficstars

Summary

This PR implements calls of native function of the address module in the prover. This enables specifications to functions containing calls of native functions of the address module. Also this PR adds prover specs to the object module, and test spec code of address module.

Motivation

• Previous code in sui-natives.bpl is just a skeleton, so this PR implements boogie side of native functions in address module.

module 0x0::address_spec {
    use sui::address;

    public fun from_bytes(bytes: vector<u8>): address {
        address::from_bytes(bytes)
    }

	spec from_bytes {
	    aborts_if len(bytes) != 20;
	}
}

• Running prover through sui move prove -- --verify-only from_bytes command on above specification returns "error: function does not abort under this condition".

module 0x0::address_spec {
    use sui::address;

    public fun from_bytes(bytes: vector<u8>): address {
        address::from_bytes(bytes)
    }

	spec from_bytes {
	    ensures result == address::from_bytes(bytes);
	}
}

• Running prover through sui move prove -- --verify-only from_bytes command on above specification returns "Error: use of undeclared function: $2_address_$from_bytes".

Key Changes

• aborts_if len(bytes) != 20; specification pass the prover, and other false aborts_if conditions will return errors.
• Implements native function calls of address module (eg. address::from_bytes()) in spec block.
• Prover fails when post-conditions at specification are false and passes when post-conditions are true.

I'm a noob sui contributor, so I would appreciate it if you could point out any mistakes.

[vercel[bot]]

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

Name	Status	Preview	Comments	Updated
frenemies	❌ Failed (Inspect)			Jan 26, 2023 at 2:10AM (UTC)

2 Ignored Deployments

Name	Status	Preview	Comments	Updated
explorer-storybook	⬜️ Ignored (Inspect)			Jan 26, 2023 at 2:10AM (UTC)
wallet-adapter	⬜️ Ignored (Inspect)			Jan 26, 2023 at 2:10AM (UTC)

[c0wjay]

Do you have any feedback on this PR @awelc, @emmazzz ? If you don't mind, I'm thinking of working on other native functions.

[awelc]

@c0wjay, sorry for the delay on this... I will look at this shortly but currently both @emmazzz and I are a bit swamped...

[c0wjay]

@c0wjay, sorry for the delay on this... I will look at this shortly but currently both @emmazzz and I are a bit swamped...

You can give me feedback at your convenience :)

[awelc]

Started to look at this but also added @meng-xu-cs and @emmazzz as reviewers.

[FaliKurve]

Goood