fix: proc change inside loops (proc change, proc change circuit)

[strub]

When the changed fragment is inside a while loop, it runs again on
the next iterations, after the loop guard, the rest of the loop body
and its own previous runs. Neither tactic accounted for this:

• proc change circuit only kept the variables read after the
  fragment in each enclosing block, ignoring the loop guard and the
  part of the loop body before the fragment. With
  while (i < 2) { y <- x; x <- a; i <- i + 1; } return y;
  proc change circuit 4.2 + 1 { x <- x; } was accepted.

• both tactics ignored the variables read by the fragment itself: in
  while (i < 2) { t <- t + a; y <- t; i <- i + 1; } return y;
  t <- t + a; y <- t could be changed into y <- t + a (the local
  equivalence only required ={y} at the end, as t is not read
  outside of the fragment).

• proc change kept in the local equivalence the conjuncts of the
  precondition whose variables are not written by the surrounding
  code, but not those written by the fragment. With
  while (i < 2) { x <- x + a; i <- i + 1; }
  under x = 0 /\ a = 1, x <- x + a could be changed into x <- 1.

All three allowed deriving false.

The keep set of proc change circuit is now computed with zpr_pv
(code after the fragment, and the guard and whole body of each
enclosing loop), as proc change already does, and, inside a loop,
both tactics add to the observable variables the ones read by both
fragments; proc change also adds the writes of the fragment to the
writes the frame must be independent from. Soundness: the two
programs are related by "the states agree on the observable
variables" (and the frame holds on the original side). The code after
the fragment only reads observable variables, so preserves this
relation, which in turn implies the precondition of the local
equivalence (the shared reads are observable), whose postcondition
re-establishes it. For the circuit check, which compares both
fragments from the same state, we use that both are deterministic.
The circuit keep set is also restricted to the variables accessed by
the fragments (the others are unchanged), so that a global read by
the loop guard does not make the circuit translation fail.

Origin: proc change circuit: e07ffa0 (2026-06-24, r2026.07).
proc change: the frame was introduced in cc03b30 (2026-03-23,
r2026.05), the restriction of the local postcondition to the
observable variables in 78cf6eb (2026-03-25, r2026.05).

Tests: tests/procchange_loop.ec and
tests/circuits/proc_change_circuit_loop.ec (the fail lines fail
before this change). unit (114 files), stdlib (128) and examples (49)
pass unchanged.