fix: unlisted exceptions are unconstrained; no swap across raising calls

[strub]

A hoare postcondition names exceptions (| e x => Q) and may have a
default branch (| _ => Q). An exception covered by neither had no
consistent meaning:

• wp refused a raise of it ("missing postcondition for
  exception");
• conseq / call failed with an anomaly (Failure "no default exception") when the premise named an exception the goal did not,
  and ignored the default branch of the goal when the premise had none;
• the abstract procedure rule (proc I) proves
  hoare [A.f : I ==> I] for every instance of A, including ones that
  raise: it treats such exceptions as unconstrained.

Such an exception is now unconstrained, as if _ => true: wp gives
true, and conseq / call read a missing default as true (a
default branch of the goal must then hold on its own). wp also no
longer applies the default branch, which binds nothing, to the
arguments of the exception.

swap refused blocks containing a raise, but not calls to
procedures that raise (#1129): moving y <- 1 in front of a call that
raises changes the state the exceptional postcondition sees. Raising is
only observable when the goal constrains exceptions (a hoare goal with
a branch other than true); otherwise it is as good as not
terminating, which swapping independent blocks preserves. swap now
also refuses, on such goals, blocks that may raise: a call to a
procedure whose body may raise, to an abstract procedure (assumed to
possibly raise), or an abstract instruction. fission / fusion had
the same gap (a FIXME) and get the same check. Blocks that cannot
raise, e.g. two assignments next to a raise, are still swapped.

This supersedes #1137, which refused every swap on a hoare goal with
exceptional postconditions, and allowed swapping a raise otherwise.

Fixes #1129.

Origin: exceptions were introduced in bba1f1b (r2026.03); the raise
check of swap in 6dbd99d (#926).

Test: tests/exception/exception_default.ec (#1129, abstract and
nested calls, fission, wp and conseq with missing defaults; the
previous build fails on it). unit (120 files), stdlib (128) and
examples (49) pass.