[Bridge] [Framework] Expand specification of the atomic bridge

[franck44]

Problem

In MIP-39, there is a formal model (timed automata in UPPAAL) of the bridge components (contracts and relayer). This model can be used to prove some quantitative properties of the bridge under some assumptions.

The model uses an abstract semantics of the contracts, approximating the changes on the "states" on the two chains.
The model also relies on correctly modelling revert/abort conditions.

Warning

For the verification results to be meaningful, we should make sure that the model is valid i.e. that we have properly captured the behaviours of the contracts (and relayer).

For the relayer (Rust) and the L1 contracts (Solidity) we can test the contracts to be more confident that are properly modelled in our formal model.

Important

For the L2 contract (Move) side, we can formally verify the assumptions made in the model with the Move Prover.

Proposed work

The atomic_bridge.move code has a companion specification atomic_bridge.spec.move.

Warning

Currently the specification does not cover all of the modules in package.

For instance the following modules have not been verified:

• ethereum
• atomic_bridge_initiator
• atomic_bridge_counterparty

The proposal is to write some specification for these modules including:

• conditions under which a function call aborts,
• some post-conditions (ensures) on the status of the bridge transfers.

These properties (once proved) can be matched against the assumptions and encoding in the UPPAAL models.