Unexpcted type checking error

[d-xo]

Attempting to check equivalence between this spec: https://github.com/d-xo/verified-contracts/blob/4e9dea9a360448ffa6cb1e81e1f031edadefc78b/spec/utils/auth.act and this implementation: https://github.com/d-xo/verified-contracts/blob/4e9dea9a360448ffa6cb1e81e1f031edadefc78b/src/utils/auth.sol gives the following error:

Cannot find a valid type for expression EUTEntry (EMapping (AlexPn 440 26 14) (EVar (AlexPn 435 26 9) "wards") [EUTEntry (EVar (AlexPn 441 26 15) "usr")]):
26 | returns wards[usr]

Afaict this should be well typed, and I'm not sure whats going on here

[zoep]

This is not a bug. The last return expression has to be annotated with either pre or post, so that the timings can typecheck.