interpreter: measure-based termination for small-step configurations

[theebayuser]

Summary

States the well-founded termination argument for small-step configurations
once, as reusable lemmas, and demonstrates it on an existing example.

TerminatesWith.of_termination_and_partial splits total correctness into a
termination half and a partial-correctness half. The Iris route supplies the
second (adequacy lands in PartiallyMeets); the first is a separate
well-founded argument. This adds that argument in symbolic form:

• reachesNormal_of_wf / reachesNormal_of_measure — a measure that strictly
  decreases along Step forces a finite trace to a configuration with no
  successor. Deliberately says only that a normal form is reached;
  classifying it as .done rather than .trapped or stuck is left to the
  caller's invariant, because Config.Safe gives error-freedom, not progress.
• terminatesWith_of_iteration / terminatesWith_of_loop — the form a loop
  proof actually takes. Requiring the measure to decrease on every step is
  too strong: the instructions inside one iteration do not decrease a trip
  count, only the back edge does. These index configurations by loop state
  instead, and allow the postcondition to be weakened on the way out.
• totalCorrectness_of_measure_of_partial — composition with the Iris side.
• Config.Normal, normal_unique — supporting definitions;
  done_normal/trapped_normal delegate to the existing done_terminal /
  trapped_terminal.

Why

The seam is already in use, and its termination halves are written by hand each
time. SwapElementsOpt3.opt3_func0_terminates unrolls a straight-line program
step by step, which is fine and unaffected by this PR. The other five sites all
re-derive the same strong induction over a decreasing measure:
NumIntegerOpt3.mod3_gcd_smallStep_termination, and the SimpleLoop, Gcd,
Factorial and EvenOddRec examples.

Examples/MeasureLoopDemo.lean shows the difference concretely: it proves
SimpleLoop's exact specification, about the same simpleLoopConfig, by
supplying the two branches and applying terminatesWith_of_loop. The
per-iteration trace lemmas are unchanged — those are the real semantic content
and no lemma removes them. What disappears is the induction skeleton.

I have left the existing proofs alone rather than rewrite them in this PR. If
porting any of them would be useful, I am happy to do that as a follow-up.

Validation

• interpreter: lake build Interpreter runner clean; just runner-smoke passes.
• codelib: lake build --wfail clean.
• programs/lean: lake build Project --wfail clean.
• No sorry/admit/axiom; every new theorem's axiom footprint is
  [propext, Classical.choice, Quot.sound].
• MeasureLoopDemo is imported from Examples/Basic.lean, so CI compiles it.