[move prover] add unchecked subtraction

[xudon9]

Motivation

Just like we can ignore addition overflow, it is more convenient to ignore subtraction underflow in some cases.

Have you read the Contributing Guidelines on pull requests?

Yes.

Test Plan

(Share your test plan here. If you changed code, please provide us with clear instructions for verifying that your changes work.)

[wrwg]

Can you please explain closer why you want to do this? It is problematic to just change the semantics of the underlying Move program.

If you want to prevent propagating an abort condition to the caller you can also do:

spec some_fun {
   pragma opaque; // Only use the spec at caller side, not the function implementation
   aborts_if [concrete] <condition under which this implementation aborts>;
   aborts_if [abstract] true; // on caller side assume this never aborts
}

There should be some examples of this in the Diem framework specs, e.g. here:

move/language/documentation/examples/diem-framework/move-packages/DPN/sources/DiemConfig.move

Line 355 in 8958b40

/// The following schema describes aborts conditions which we do not want to be propagated to the verification

[wrwg]

Closing as we aren't moving forward with this. Feel free to reopen if this is the wrong call.