[WIP] Fix VCG path multiplication with goto in if-then-else

[olivier-aws]

Issue #419

🤖 Note: This PR was created with assistance from an AI agent.

Summary

This PR fixes a critical bug where procedures containing goto (exit) statements inside if-then-else branches caused verification condition (VC) path multiplication. When multiple paths converged to the same exit label, each path was treated independently through ProgramEval, duplicating proof obligations for subsequent procedures.

Changes

1. Block-level path merging (fix(StatementEval): Merge block handler results)

• Added mergeByExitLabel in the block handler to merge environments that converge to the same exit label
• Prevents path multiplication by ensuring at most one result per distinct exit label

2. Fixed path merging logic (fix(StatementEval): Address review feedback)

• Fixed Env.merge argument order in mergeByExitLabel (true-branch = E1, false-branch = E2)
• Fixed condition extraction to inspect path condition structure instead of blindly using newest entry
• Fixed repeated merge corruption by replacing foldl-based merge with exact 2-path matching
• Moved merge logic into processIteBranches for same-label exits

3. Test coverage

• Added ExitItePathMerge.lean with tests for:
  • Merged variable value correctness
  • Three paths converging to same exit label via nested ite

Files Changed

• Strata/Languages/Core/StatementEval.lean (+59/-12)
• StrataTest/Languages/Core/Examples/ExitItePathMerge.lean (+210 new)

Status

🚧 Work in Progress - Testing and review in progress
Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[shigoel]

Thanks, @olivier-aws! I know this is WIP, but I wonder whether merging by labels is the right thing to do especially since we don't (yet) enforce the uniqueness of labels.

[olivier-aws]

Thanks, @olivier-aws! I know this is WIP, but I wonder whether merging by labels is the right thing to do especially since we don't (yet) enforce the uniqueness of labels.

We should enforce uniqueness of labels within a block at least. In that case, I believe that the proposed solution is safe. Do you think we should add a check about uniqueness of labels with a block and reject Core programs that fail this check?

Answer from kiro-cli:

The key insight is that the label-based merging is safe even without enforced label uniqueness because:

Why It's Safe

1. Sibling paths only: mergeByExitLabel only merges paths that result from evaluating the same block's statements. All paths in the input are siblings (started from the same entry point).

2. No cross-block merging: The function never merges paths from different blocks. Each block evaluation is independent.

3. Same-label convergence is meaningful: If two sibling paths converge to the same exit label, they represent different execution paths through the same code that should be merged - regardless of whether other
   blocks elsewhere use the same label name.

Example

Even with duplicate labels across different blocks, the merging is safe:

lean
procedure foo() {
outer: { if (x > 0) { exit outer; } exit outer; }
// Paths merged here (both from foo's outer block)
}

procedure bar() {
outer: { if (y > 0) { exit outer; } exit outer; }
// Paths merged here (both from bar's outer block)
// Never merged with foo's paths!
}

The concern about label uniqueness would only apply if we were merging paths from different blocks, which we never do.

[olivier-aws]

Closing due to git merge issues. Will open a new one

[shigoel]

We should enforce uniqueness of labels within a block at least. In that case, I believe that the proposed solution is safe. Do you think we should add a check about uniqueness of labels with a block and reject Core programs that fail this check?

I think we should, yes -- that's entirely reasonable to me.