`swap`'s raise check (#926) does not look inside called procedures

[Yiping106283]

The fix for #926 (6dbd99d) makes swap refuse blocks that syntactically contain raise, but the check does not look inside called procedures. A call to a procedure that raises is treated as an ordinary independent statement, so an assignment can be moved in front of it and the state observed by the exceptional postcondition changes: the judgment absurd_hoare below is false (M.f always raises exn1 from M.y = 0). This is not a soundness issue as far as we can tell: no rule bridges exceptional postconditions to Pr (every rule relating them to phoare/Pr is gated on an empty exception map, and there is no catch construct), so we found no derivation of false on current main. It is a gap in the #926 fix that would become one as soon as such a bridge is added.

MRE:

require import AllCore.

exception exn1.

module M = {
  var y : int
  proc g() : unit = { raise exn1; }
  proc f() : unit = { g(); y <- 1; }
}.

(* honest: f raises exn1 before `y <- 1`, so M.y = 0 when exn1 escapes *)
lemma honest : hoare [M.f : M.y = 0 ==> false | exn1 => M.y = 0].
proof. proc. inline M.g. wp. skip => />. qed.

(* BOGUS: `swap 1 1` moves `y <- 1` in front of the raising call; the
   syntactic raise check (check_swap) does not look inside callees. *)
lemma fake : hoare [M.f : M.y = 0 ==> false | exn1 => M.y = 1].
proof. proc. swap 1 1. inline M.g. wp. skip => />. qed.

(* f always raises exn1 from M.y = 0, yet the exceptional post `false` is accepted *)
lemma absurd_hoare : hoare [M.f : M.y = 0 ==> false | exn1 => false].
proof.
conseq honest fake.
+ by move=> />.
+ by move=> &hr _ y; split=> // [#] -> //.
qed.

Root cause: src/phl/ecPhlSwap.ml, LowInternal.check_swap (l. 21-37): is_contains_raise uses EcModules.i_iter, which treats Scall (and Sabstract) as leaves; the read/write independence check (PV.interdep) then accepts the swap because g writes nothing. A conservative fix is to also refuse swapping blocks that contain Scall/Sabstract when the goal has a non-empty exceptional postcondition (or when the callee transitively contains raise, treating abstract procedures as possibly raising).