Higher-order functions problem

[MikaelMayer]

Discussed in #3405

^{Originally posted by Nangos January 26, 2023}
Hi All,

I recently met a problem when verifying with higher-order functions. It boils down to the following minimal example:

var f: int -> int;
assert seq(1, x => f(x))[0] == f(0);  // No problem
assert seq(1, f)[0] == f(0);  // Error: assertion might not hold

In the general case (especially when writing class methods), one would have to write x reads f.reads(x) requires f.requires(x) => f(x) in the place of f. This will be quite a boilerplate.

After some random attempts, I found an acceptable workaround:

// Seems like a mere identity function. What's going on here?
function magic<S, T>(f: S ~> T): (S ~> T) {
  x reads f.reads(x) requires f.requires(x) => f(x)
}

assert seq(1, magic(f))[0] == f(0);  // No problem now

I am still curious about what exactly is happening under the hood and whether there are more elegant ways to deal with this. Any suggestion is welcome.