Verification errors resulting from global constants defined in terms of mutable global state

[marcoeilers]

If we have stateless global constants that are defined in terms of something stateful, Nagini generates Viper functions whose verification fails because of insufficient permissions. Additionally, because this is not expected, the attempt to generate an error message leads to a stack trace in this case.

Example:

from nagini_contracts.contracts import *
from typing import List, Tuple

a = [1,2]
b = a[1]

leads to the generation of

function b(): Ref
  ensures issubtype(typeof(result), int())
  ensures result == list___getitem__(a(), __prim__int___box__(1)) 
{
  list___getitem__(a(), __prim__int___box__(1))
}

which doesn't verify.