fix(phl): swap with a code path must rebuild the enclosing program

[Yiping106283]

Summary

Since f0827a1, swap accepts a range prefixed by a code path (1.:[1 .. 1]: then-branch of instruction 1; 1?:: else-branch; loop bodies). After swapping inside the addressed block it installed that inner block as the whole program of the goal: the enclosing if/while and every sibling branch disappeared, so false hoare/phoare/equiv judgments became provable (auto, by sim), including lemma bad : false via byphoare. This PR makes the path work as intended: the swap is performed inside the addressed block and the enclosing program is rebuilt.

Fixes #1122.

Root cause

src/phl/ecPhlSwap.ml, LowInternal.swap_stmt. f0827a1 ("Extend code-position handling with gap/range semantics") changed swap_kind.interval to a codegap_range, which carries a path, and made swap_stmt follow it with normalize_cgap_range. That function returns the sub-statement reached by the path; the swap was performed on it and stmt (hd @ s2 @ s1 @ tl) of that sub-statement was returned, which t_swap_r installed with hl_set_stmt as the full program. The normalised path was discarded and nothing zipped the context back, whereas proc change/proc rewrite (src/phl/ecPhlRewrite.ml) open a zipper with EcMatching.Zipper.zipper_and_split_of_cgap_range and rebuild the program with Zipper.zip, and outline goes through Zipper.map_range (routing that dates from 3808ca8 / 8debf27).

Fix

swap_stmt now opens a zipper at the addressed block with EcMatching.Zipper.zipper_and_split_of_cgap_range (as proc change and proc rewrite do), resolves the offset and performs the swap on the block rebuilt from z_head/z_tail, and returns EcMatching.Zipper.zip of the zipper with the swapped block as its tail. check_swap (raise / read-write independence) still runs on the two swapped fragments of the inner block. For a top-level range (empty path) the zipper is ZTop, so the behaviour there is unchanged.

zipper_and_split_of_cgap_range normalised start and fin separately and never checked start <= fin; a reversed range such as [3 .. 1] then split into an empty middle fragment and was silently accepted (proc change [3 .. 1] : { } and proc rewrite [3 .. 1] /= were no-ops on main, and swap would have inherited that). It now goes through Position.normalize_cgap1_range, which raises InvalidCPos on a reversed range, exactly as the old normalize_cgap_range path of swap did. proc change (t_change_stmt) and outline did not catch InvalidCPos from the primitive (an out-of-range position was already reported as an anomaly on main); they now report "invalid code position" / "Outline: invalid code position".

doc/tactics/swap.rst now says that a code position may carry a code path (branch, loop body, match arm).

Impact

• swap, swap{i} with a path now yield the original program with the two fragments exchanged inside the addressed branch/loop body/match arm, in all program logics.
• Top-level swap and interleave (which builds an empty path) are unaffected.
• No change to the independence checks; they were already run on the inner fragments.
• A reversed range is rejected again by swap ("invalid range"), and is now also rejected by proc change, proc rewrite, outline and module updates (M with { proc f [[3 .. 1] ~ ...] }) with "invalid code position" (all callers of zipper_and_split_of_cgap_range); on main they silently did nothing to the program. An empty range ([2 .. 1], i.e. the gap before 2 = the gap after 1) is still accepted, as before.
• proc change/outline with an out-of-range position now give "invalid code position" instead of an anomaly: InvalidCPos.
• A swap path into an instruction that is not an if/while/match (e.g. swap 1.:[1 .. 1] 1 on an assignment) now gives "invalid range" instead of an anomaly (Assertion failed src/ecMatching.ml:374) on main.

Test

• tests/swap-codepath-context.ec (regression test, fail (...)/abort idiom): after swap 1.:[1 .. 1] 1, 1?:, a while-body path and swap{1} in an equiv, the bogus goals can no longer be closed by auto/by sim; reversed ranges [3 .. 1] are rejected at top level and behind a 1.:/1?: path. Fails on unpatched main at the first fail ("this command is expected to fail"), passes with the fix.
• tests/swap-codepath.ec (positive): legitimate swaps of two independent assignments inside a then-branch, an else-branch, a while body, in a phoare goal and with swap{1} in equiv goals; the resulting goal is the whole program (closed by auto with a pre/post that only the untouched branch satisfies, and by sim against the pre-swapped program). Fails on unpatched main, passes with the fix.
• Issue MRE (lemma fake, lemma bad : false, and the else/while/equiv variants) is rejected with the fix.
• tests/procchange.ec, tests/procrewrite.ec, tests/procrewrite-block.ec, tests/procrewrite-simpl.ec, tests/outline.ec pass individually on the patched binary (none uses a reversed range).
• dune build --profile=ci clean; make unit 107/107. make stdlib and make examples were run: the only failures are theories/crypto/assumptions/DHIES.ec:987 (prover timeout under load; passes standalone on both the patched and the unpatched binary) and examples/ChaChaPoly/chacha_poly.ec:2525 (identical on unpatched main).