[bridge] Formally verify the Native Bridge Move modules

[apenzk]

Feature Request

We are Movement. We distinguish from the rest of Eth ecosystem by supporting Formal Verification through Move. We should embrace this, live this, and formally verify the native bridge (on the Move side)

This particularly holds true if the bridge is simplified.

Is your feature request related to a problem?

The bridge is not formally verified.. yet.

Describe the solution you'd like

Formally verify the Native Move bridge contract.

Describe alternatives you've considered

The alternative is to not live up to our preached standards.

[andygolay]

Indeed, we are Movement.

Yes, formally verifying the native bridge is important. I was going to start on this after fully finishing the modules, to get more hands-on spec experience, but maybe it would be better in the interest of time for @franck44 to do it, once we decide that the modules are feature-complete?

[andyjsbell]

I made a start a while back https://github.com/movementlabsxyz/aptos-core/blob/movement/aptos-move/framework/aptos-framework/sources/atomic_bridge.spec.move

[andygolay]

If you'd like to check it out, I began a spec for native_bridge.move in the latest commit in PR 100 to aptos-core here: movementlabsxyz/aptos-core@3b91758

As long as the spec doesn't block the modules from compiling, I think it's fine to land PR 100 and then fix the spec so it passes formal verification in a separate PR, which we can track in this issue.

I'm a bit stumped on the syntax of the spec for the bridge_transfer_id function. Details here, please feel free to comment if you can help, thank you:
movementlabsxyz/aptos-core#100 (comment)