Fix namespace collision and SMACK assert encoding in BoogieToStrata

[PROgram52bc]

Issue #, if available: #1148

Description of changes:

1. Namespace collision (issue 1 in BoogieToStrata: Blockers preventing SMACK-generated Boogie verification #1148): Constants that share a name with a procedure are now prefixed with _const in the Strata output. The rename is applied consistently in declarations and references.

2. Recursive synonym resolution (Fixes issue 2 in BoogieToStrata: Blockers preventing SMACK-generated Boogie verification #1148): DealiasTypeExpr now recurses on its result, resolving synonym chains like ref := i64 := int fully to the base type. Previously it resolved only one level, causing panics on comparison/arithmetic operators applied to multi-level type synonyms.

3. SMACK assert encoding (issue 3 in BoogieToStrata: Blockers preventing SMACK-generated Boogie verification #1148): Procedures named assert_.* now get a requires (arg != 0) precondition emitted. Call elimination generates VCs at each call site, making SMACK assertions verifiable.

4. InferModifies: SMACK-generated Boogie often omits explicit modifies clauses on procedures that mutate globals. Setting InferModifies = true in BoogieToStrata has two effects: (1) it runs ModSetCollector.CollectModifies(program) to populate empty modifies clauses, and (2) through CheckModifies in Boogie's resolution context, it suppresses typechecking of modifies clauses. Without this, ResolveAndTypecheck would reject SMACK programs that omit modifies clauses.

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

[tautschnig]

Thanks for tackling all three #1148 issues in one PR — I ran the three fixes end-to-end on the included reproducers and each of them does what the description claims. The direction looks right, and I especially like that fix (3) follows atomb's suggestion of an opaque procedure with a precondition rather than inlining assert. I have a mix of blocking and non-blocking comments, grouped below:

Blocking

• Test harness gap. VerifyTestFile adds --check when no .expect file exists, which literally emits Skipping verification. without invoking the solver. I re-ran the three new tests: with no .expect, SmackAssert.bpl passes CI even though the whole point of the test is that call $r := assert_.i32(0); should now fail verification. Please add .expect files for all three new tests (SmackAssert.expect crucially must contain a failed line so the harness flips expectedExitCode to 2 and actually catches regressions).

• Fix (2) has no regression test. dealiasTypeExpr now recurses, but there is no .bpl test exercising a multi-level synonym chain (the issue's reproducer TypeSynonymComparison.core.st wasn't carried over). Existing TypeSynonyms{1,2}.bpl only use single-level synonyms. Without a test, this fix has no CI coverage. A 10-line .bpl using type i64 = int; type ref = i64; with <= / + over ref would close this.

• Rename mechanism is not applied consistently. Four of the places that emit variable names still call Name(...) instead of NameOf(decl, ...). This is only triggered when a global gets renamed (i.e. its sanitized name collides with a proc/const/func), but once it does, the output is broken. Reproducer:

  const $a.b: int;   axiom $a.b > 0;
  var   $a_b: int;   // both sanitize to _a_b
  procedure main() returns (r: int)
    modifies $a_b;
  {
    $a_b := 1;
    havoc $a_b;
    r := $a.b + $a_b;
  }

  Produces (inout parameter name and havoc target still use the pre-rename identifier, while the identifier expression uses the renamed one):

  procedure main(inout _a_b : int, out r : int)
  {
    _a_b := 1;
    havoc _a_b;
    r := (_a_b + __var__a_b);   // __var__a_b is undefined
  }
  

  ...and strata verify reports Unknown expr identifier __var__a_b. See the inline comment at VisitCallCmd for the full list of affected sites.

• StartsWith("assert_") is too permissive and triggers on user-written procedures. Reproducer:

  procedure assert_helper(p: int) returns (r: int);
  procedure main() returns (r: int) { call r := assert_helper(0); }

  emits requires (p != 0); on assert_helper even though the user never wrote it. Any Boogie program with a procedure whose name happens to start with assert_ (e.g. assert_helper, assert_invariant, assert_equal) would start failing verification. SMACK's actual pattern is assert_.<type> (literal dot); please tighten to match that specifically.

Non-blocking

• InferModifies = true isn't mentioned in the PR body. It's not just a knob — it runs ModSetCollector (mutating the program) and, via CheckModifies, suppresses modifies-clause typechecking. Please document the motivation and add a .bpl test with a procedure that mutates a global without an explicit modifies clause, so regressions in this new assumption are caught.
• Proof opportunities for dealiasTypeExpr. Since this is partial def, strong termination isn't provable without an acyclicity argument on p.globalContext. Natural lemmas that the rest of the file could rely on: dealiasTypeExpr_idempotent : dealiasTypeExpr p (dealiasTypeExpr p te) = dealiasTypeExpr p te, and a "result is fully unwound" lemma: if dealiasTypeExpr p te is .fvar _ idx #[], then p.globalContext.kindOf! idx is neither .expr _ nor .type [] (.some _). If you don't want to prove these, at least consider a Lean-side #guard test constructing a three-level synonym Program and checking the result is .int.
• Refactoring the rename builder. The ClaimOrRename logic would be more readable as a named static helper that takes the claimed set and the _renames dict as parameters, rather than a closure inside EmitProgramAsStrata. The ordering "procs → impls → consts → funcs → globals" is a deliberate tie-breaker (first-seen wins) — please document it at the _renames field, since it's a semantic choice with implications (e.g. a name collision between a proc and a const always renames the const, never the proc).
• Duplicated spec emission for assert_.*. The new spec { requires ... } block in VisitProcedure duplicates the emission pattern in WriteProcedureHeader. Consider injecting a synthetic Requires into node.Requires just before calling WriteProcedureHeader so the existing code path handles it uniformly.
• IdentifierExpr fallback. identExpr.Decl != null ? NameOf(...) : Name(...): post-Boogie-resolution, Decl should always be non-null. Silently falling back to Name(...) emits the unrenamed name and is wrong in the collision case. Consider asserting non-null instead, or at least add a comment about when Decl can be null and why the fallback is safe.

[PROgram52bc]

Thanks @tautschnig for your detailed comments. I have addressed everything except for the dealiasTypeExpr proof, which could be completed in a separate PR, especially in light of the refactoring that's going to take place.

[MikaelMayer]

🤖🔍 Good progress since the last round. The .expect files have been added for all test cases, ClaimOrRename is now a static helper, and the assert_. pattern (with the dot) correctly avoids false positives like assert_helper. The rename mechanism is well-structured and the test coverage is solid.

One remaining issue below.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.