[prover] WP anchors a normal-return postcondition on an aborting path

[wrwg]

[Claude Agent] Filed while preparing the specification-inference benchmark round.

Unaided WP inference emits an unprovable ensures whose antecedent is exactly a
condition the same inference emits as an aborts_if beside it, carrying the
abort code's constructor as though it returned a value on the normal path:

ensures [inferred = sathard]
    current_shares >= shares && current_shares == 0
        ==> ensures_of<error::invalid_argument>(4, result_of<error::invalid_argument>(4));
aborts_if [inferred] current_shares == 0;          // the same condition

It is a normal-return postcondition for a path that never returns normally, so
it is vacuous and cannot be discharged. It is reported as sathard, which reads
as solver difficulty rather than as a modelling slip — and none of the affected
functions has a loop.

It reaches the caller through math64::mul_div, whose abort constructs its code
by calling error::invalid_argument. The prover inlines that, and the abort path
picks up an anchor for the call.

Reproducing

Three targets in aptos-move/flow/evaluation/spec-inference/corpus-v3:
VS-shares-002, LP-price-021, TS-trial-019. Build the package
(corpus-v3/build.py) and run move-flow experiment infer --write-inferred-specs
on any of them.

VS-redeem-004 also carries sathard clauses but is not an instance: those
carry result_of over sibling calls, which is genuine composition difficulty.

A candidate fix, and why it was not taken

In spec_inference.rs, the call transfer adds a behavioral anchor for a callee
whose result is discarded. Guarding that on state.is_normal_return — the same
guard used ~30 lines above in the same function — removes the clause from all
three targets, leaves VS-redeem-004 untouched, and leaves the 44 inference
baselines unchanged.

It was not taken, for two reasons found while testing it:

• No minimal reproduction. Five cases — direct abort, same-module and
  cross-module inline callees, an opaque callee, and a faithful copy of
  math64::mul_div — all produce the correct specification without the guard.
  So the account above describes the symptom, not a demonstrated cause.
• The guard is far broader than the symptom. Instrumented, it suppresses 154
  anchor additions on one function, of which exactly one survived into the
  output. The other 153 were already discarded downstream, so it is probably
  harmless — but "probably" is not a standard for prover code underwriting a
  measurement.

Wanted: the actual trigger, a narrower fix, and a regression test. Note the
prover's inference suite loads only move-stdlib, so a test exercising
math64::mul_div needs a home where aptos-stdlib is available, or a local copy
of the function.