instrument each entrypoint function that establishes precondition+postconditions

[ksolana]

example:

entry public fun create_and_transfer(to: address, ctx: &mut TxContext) {
        transfer::transfer(create(ctx), to)
}

Preconditions:

We'd need to validate each parameter of create_and_transfer before calling the transfer.

• is the to address valid. A slightly extended idea would be if we want to block the transfer to an address for some reason?

Postconditions

• I found https://docs.stacks.co/id/docs/stacks-academy/post-conditions but still need to refine what we can take from there.

I think these checks will be in addition to what we'll get by enabling MoveVM checks at runtime.

PS:

• Maybe solana-move can also use some compile time check. Specification of entry functions in solana-move #380
• It might be relevant to other functions but i'm not too sure.
• Ehereum has nice article on having pre+post conditions https://ethereum.org/en/developers/docs/smart-contracts/formal-verification/

[nvjle]

I think these checks will be in addition to what we'll get by enabling MoveVM checks at runtime.

Would you elaborate on specifically where you differ from the checks that the MoveVM does (which we would presumably implement in our VM)? It would be useful to simply enumerate what the MoveVM does for parameter/signature verification-- so that we can implement to the degree possible.

In Discord regarding this issue, you mentioned "cross-contract interactions". In the Move Language, it is my understanding that any "interaction"-- which I assume would be a function call (what other kind of external interactions would there be in a Move Language program?)-- are verified in the same way. If you are referring to calling from an existing Solana program into a Move Language program (and vice-versa), I still would assume we'd try to verify parameters/signatures the same way. I think the goal of the new runtime work is to have all programs "interact" the same way, regardless of language.

[nvjle]

It is also worth noting that the Move Language provides a fairly sophisticated "specification" sub-language for expressing all sorts of invariant and condition checks ("pre- and post-conditions") in Move programs. These can be statically analyzed by the move-prover. See some examples here move-prover/tests/sources/functional.

[ksolana]

It would be useful to simply enumerate what the MoveVM does for parameter/signature verification-- so that we can implement to the degree possible.

I think this is the most reasonable path forward as need to do this anyways.