Create Dafny environment

[l-monninger]

Summary

We should standardize our Dafny environment. In my opinion, this is best accomplished via nix somehow as not everyone will be using VSCode or Emacs.

Ideally, this issue generates a means of setting up a standardized Dafny environment locally and documentation on how we organize specs and write them in Dafny under the /spec subdirectory.

[l-monninger]

@franck44 I think this might suit you.

[franck44]

@l-monninger How do we plan to use Dafny for this project?

[l-monninger]

@franck44 General verification of smart contract and -core crate logic.

1. Reason about algorithm in Dafny and generate a correct spec.
2. Reimplement with verification in target language with verification or model-checking support, e.g., creusot for rust and foundry invariant testing for Solidity.

Example smart contract method worth verifying: https://github.com/movementlabsxyz/ffs/blob/2bfdf2aefbd9c59aeb6611de346d48c60b4adf8b/protocol/mcr/contracts/src/staking/MovementStaking.sol#L350
Example Rust code worth verifying: https://github.com/movementlabsxyz/ffs/blob/2bfdf2aefbd9c59aeb6611de346d48c60b4adf8b/protocol/mcr/manager/src/manager.rs#L51