Core VCG: goto inside if-then-else causes path multiplication across procedures

[fabiomadge]

Problem

When a procedure contains a goto inside an if branch, the VCG produces multiple EnvWithNext results (one per branch). These multiple results propagate through ProgramEval, causing subsequent procedures to be verified once per path from the previous procedure.

Reproduction

program Core;

procedure first(a : int) returns (r : int)
spec { }
{
  if (a > 0) {
    r := 1;
    goto done;
  }
  r := 0;
  done: { }
};

procedure second(a : int) returns (r : int)
spec { }
{
  assert a > 0;
  r := a;
};

Expected: assert_0 fails once.
Actual: assert_0 fails twice (once per path from first).

Root cause

In StatementEval.lean, processIteBranches has a special case (line ~530) that merges both branches into a single result when neither has a nextLabel. When one branch has a goto (nextLabel := some l), it falls through to the general case (line ~539) which returns Ewns_t ++ Ewns_f — separate paths.

These separate paths propagate up through:

1. evalAuxGo line ~497: List.flatMap continues remaining statements for each path
2. Procedure.eval: returns List (Procedure × Env) with multiple entries
3. ProgramEval line ~77: pEs.flatMap evaluates remaining declarations for each entry

Note: Procedure.evalOne (line ~84) explicitly expects a single result and errors on multiple, suggesting this multiplication is unintended.

Proposed fix

In processIteBranches, when the general case produces multiple results, group them by nextLabel and merge environments within each group using Env.merge:

1. Partition results from each branch into goto paths (nextLabel.isSome) and normal paths
2. Merge normal paths from both branches using Env.merge cond' E_t E_f (same as the existing special case)
3. Merge goto paths targeting the same label using Env.merge
4. Return at most one result per distinct nextLabel

This ensures an ite with gotos produces at most N results (one per distinct target label + one for fall-through), not a product of branch paths.

Impact

This blocks using goto for early return encoding in Laurel-to-Core translation. Currently Laurel uses assume false to model early returns, which is incorrect for execution and requires duplicating postcondition assertions at each return site. The goto approach is cleaner but unusable until this is fixed.