how to give a bound when traverse infinite map (imap) in Dafny?

Question

here is an example:

type temporal = imap<int, bool>
type Behavior<S> = imap<int, S>
    
function stepmap(f:imap<int, bool>):temporal
  ensures  forall i:int :: i in f ==> sat(i, stepmap(f)) == f[i]
{
  f
}

predicate sat(s:int, t:temporal)
{
  s in t && t[s]
}

function{:opaque} and(x:temporal, y:temporal):temporal
  ensures  forall i:int {:trigger sat(i, and(x, y))} :: sat(i, and(x, y)) == (sat(i, x) && sat(i, y))
{
  stepmap(imap i :: sat(i, x) && sat(i, y))
}

function{:opaque} or(x:temporal, y:temporal):temporal
  ensures  forall i:int {:trigger sat(i, or(x, y))} :: sat(i, or(x, y)) == (sat(i, x) || sat(i, y))
{
  stepmap(imap i :: sat(i, x) || sat(i, y))
}

the function 'and' and 'or' want to construct a new imap by traversing the element in x and y.

this code works with Dafny versions that are less than 4.0, but for new Dafny version, it show an error "imap comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'i'".

So, how to give a bound when traversing an infinite map?

Answer 1

The issue is related to the change in syntax that occurred in Dafny 4.0. The details don't matter so much, but basically you can resolve this in Dafny 4.0+ by using the ghost qualifier:

ghost function{:opaque} and(x:temporal, y:temporal):temporal
ensures ... {
   ...
}

And likewise for or. Note that by marking them as ghost functions you cannot generate executable code for them. However, that might not matter in your setting.