assume { f(x); } puts HA_app_ok in antecedent position, handing the prover trap-freedom for free

[0xGeorgii]

A bare call statement inside an assume block emits its HA_app_ok atom into the antecedent of the obligation's Himpl, rather than into the consequent.

Per core/wasm-to-v/ROCQ_CONTRACT.md a realization claim is a trap-freedom claim: downstream HA_app_ok f ts denotes val_fun V f vs <> None, which interp_realized turns into fun_computes, defined through sem_mx, a total-correctness judgment whose conclusion demands the body reduce to a value stack and never to a trap.

In antecedent position that claim is therefore assumed, not proved: the prover is handed "this call terminates and does not trap" as a free hypothesis. In consequent position it is an obligation. Every case covered on main today puts it in the consequent.

The shape is reachable and emits without complaint. It was found while auditing the dead feat/wasm-verifier-e2e branch, whose nested_quant.inf is the only source in either tree that produces it; compiled on current main it emits an Himpl whose antecedent conjoins HA_has_type with HA_app_ok.

Two readings, and the choice is a language-semantics call rather than a bug report:

1. Intended - an assume filters execution paths, so assuming the call is realizable is exactly what the author asked for. Then it should be pinned with a corpus fixture and one sentence in the contract.
2. Unintended - a bare non-assert call inside an assume should be rejected with a new P0xx, because silently weakening an obligation is worse than refusing the construct.

Important caveat for whoever takes this: the coqc gate cannot catch a polarity error. Himpl elaborates HA_app_ok identically in either position, so a corpus entry pins the shape, not the soundness.