Fix @extern functions being mistakenly verified

[Copilot]

• Investigate the issue - @extern functions are verified in some cases
• Identify the root cause - DropVCs flag not added to Choose expressions in OpaqueChooseInjector
• Implement fix: Add DropVCs flag to ValDef in OpaqueChooseInjector.scala
• Revert incorrect fix in VerificationComponent.scala
• Run code review
• Run CodeQL check

Summary

Fixed an issue where @extern functions were being mistakenly verified. The root cause was that OpaqueChooseInjector creates Choose expressions for extern/opaque functions but didn't add the DropVCs flag to the ValDef. When ChooseEncoder processes these Choose expressions, it generates assertion VCs unless DropVCs is present (see lines 79-86 in ChooseEncoder.scala).

Changes

• Modified OpaqueChooseInjector.scala to add DropVCs flag to the ValDef when creating Choose expressions, consistent with how ChooseInjector.scala handles similar cases (line 40).
• Reverted incorrect fix in VerificationComponent.scala

Original prompt

---

This section details on the original issue you should resolve

<issue_title>@extern functions are mistakenly verified in some cases</issue_title>
<issue_description>This verified, as I would expect with @extern:

import stainless.annotation.{extern,pure}
import stainless.lang.StaticChecks.*
object Test:
  @pure @extern
  def f(a: Int, b1: Int, b2: Int): Unit = {
    require(0 <= a && a <= 0x1000 && 0 <= b1 && b1 <= b2)
    ()
  }.ensuring(_ => 0 <= a * b1 && 0 <= a * b1 && a * b1 <= a * b2)

but this did not, where I just add one more conjunct to the assumptions:

import stainless.annotation.{extern,pure}
import stainless.lang.StaticChecks.*
class Test:
  @pure @extern
  def f(a: Int, b1: Int, b2: Int): Unit = {
    require(0 <= a && a <= 0x1000 && 0 <= b1 && b1 <= b2 && b2 <= 0x1000)
    ()
  }.ensuring(_ => 0 <= a * b1 && 0 <= a * b1 && a * b1 <= a * b2)

I'm using just --strict-arithmetic=false as a flag.

It looks like in some cases f is not removed from functions to verify, even though it's marked as extern. This defeats the purpose of extern annotation.

[Warning ]  - Result for 'postcondition' VC for f @5:7:
[Warning ] 0 > a || a > 4096 || 0 > b1 || b1 > b2 || b2 > 4096 || {
[Warning ]   val (_$1: Unit) @extern = choose$0(a, b1, b2)
[Warning ]   0 <= a * b1 && a * b1 <= a * b2
[Warning ] }
```</issue_description>

<agent_instructions>Can you identify parts of code that may be responsible for this issue and propose possible changes? If needed, to build the software, you can use command `sbt universal:stage`. To invoke the resulting tool on an input file test.scala , you can run `frontends/dotty/target/universal/stage/bin/stainless-dotty --timeout=10 test.scala` and see if you can reproduce the issue.</agent_instructions>

## Comments on the Issue (you are @copilot in this section)

<comments>
</comments>

• Fixes @extern functions are mistakenly verified in some cases #1689

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

[CLAassistant]

Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you all sign our Contributor License Agreement before we can accept your contribution.
1 out of 2 committers have signed the CLA.

✅ samuelchassot
❌ Copilot
_{You have signed the CLA already but the status is still pending? Let us recheck it.}

[vkuncak]

@copilot This is not the solution I would expect at this stage. I would expect that we should not need to check explicitly for the extern annotation, as the bug would otherwise always manifest. Yet the bug happens only for certain number of conjuncts in require. I would instead expect that trees.DropVCs is not always inserted where it should be. Feel free to post comments here first before updating the PR.

[Copilot]

@copilot This is not the solution I would expect at this stage. I would expect that we should not need to check explicitly for the extern annotation, as the bug would otherwise always manifest. Yet th...

You're right. The proper fix is in OpaqueChooseInjector.scala - when creating Choose expressions for extern/opaque functions, the DropVCs flag needs to be added to the ValDef. This is consistent with how ChooseInjector.scala handles similar cases (line 40). Without this flag, ChooseEncoder generates assertion VCs (see line 79-86 in ChooseEncoder.scala).

Fixed in fc53f03 - reverted the VerificationComponent.scala change and added DropVCs to the ValDef in OpaqueChooseInjector.