search

movementlabsxyz / movement

The Movement Network is a Move-based L2 on Ethereum.
Apache License 2.0
82 stars 65 forks source link

[bridge] Formally verify the Native Bridge Move modules #870

Open apenzk opened 2 days ago

apenzk commented 2 days ago

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 commented 2 days ago

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 commented 2 days ago

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 commented 1 day ago

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: https://github.com/movementlabsxyz/aptos-core/pull/100/commits/3b917589af0ccba849a40f3d9815778c21eceb08

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: https://github.com/movementlabsxyz/aptos-core/pull/100#issuecomment-2489770158