Verification failure due to Nat and Int mismatch

[rdivyanshu]

Dafny version

4.2.0

Update: Tested on dafny version 4.4.0, same issue.

Code to produce this issue

lemma seq_thm <T> (j: nat, f: nat --> T)
  requires forall i :: 0 <= i < j ==> f.requires(i)
  ensures forall i :: 0 <= i < j ==> seq(j, f)[i] == f(i)
{}

Command to run and resulting output

dafny /compile\:0 /useBaseNameForFileName /timeLimit\:30 /vcsCores\:4 /showSnippets\:1 test.dfy
test.dfy(4,0): Error: a postcondition could not be proved on this return path
  |
4 | {}
  | ^

test.dfy(3,10): Related location: this is the postcondition that could not be proved
  |
3 |   ensures forall i :: 0 <= i < j ==> seq(j, f)[i] == f(i)
  |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 1 verified, 1 error

What happened?

I was looking at boogie code generated by Dafny in above case. Axiom of Seq#Create

axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int ::
  { Seq#Index(Seq#Create(ty, heap, len, init), i) }
  $IsGoodHeap(heap) && 0 <= i && i < len ==>
  Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i)));

Postcondition generated in boogie

  ensures (forall i#3: int :: 
    { Apply1(Tclass._System.nat(), _module._default.seq_thm$T, $Heap, f#0, $Box(i#3)) } 
      { Seq#Index(Seq#Create(_module._default.seq_thm$T, $Heap, j#0, f#0), i#3) } 
    true
       ==> 
      LitInt(0) <= i#3 && i#3 < j#0
       ==> Seq#Index(Seq#Create(_module._default.seq_thm$T, $Heap, j#0, f#0), i#3)
         == Apply1(Tclass._System.nat(), _module._default.seq_thm$T, $Heap, f#0, $Box(i#3)));

Axiom matches part we have to prove except TTint does n't match Tclass._System.nat().

I modifies code to below and it verifies

lemma seq_thm <T> (j: nat, f: int --> T)
  requires forall i :: 0 <= i < j ==> f.requires(i)
  ensures forall i :: 0 <= i < j ==> seq(j, f)[i] == f(i)
{}

What type of operating system are you experiencing the problem on?

Linux

[rdivyanshu]

It seems like it is duplicate of #4799