Remy Willems

While this issue only shows a tiny example, I saw cases where the leakiness of an opaque function increased proof resource count to >1M RU. It seems like there's no...

Lowering severity since this is by design so it's a lack of documentation.

Currently opaque is implemented by adding an additional `reveal: bool` parameter to opaque functions, and only defining the body when `true` is passed for this parameter. The trigger for the...

Thanks for the reply! > I wonder if it would be more flexible to calculate and check this per module, so it's independent of the .doo bundling. That way you...

> Note there's also a similar issue when you add translation to the dependency graph Good point! I'm thinking of also adding a checksum of the input used to translation...

It's not a bug, but rather a missing defense in depth feature, that could prevent an actual bug from causing invalid execution of a valid program and instead causing rejection...

@MikaelMayer could you be more verbose in your problem description? It's not clear to me what the issue is.

> I'm just surprised because I expected that, given a random seed, the iterations' result would be the same. Me too. This shouldn't happen, even if you do not specify...

It seems like Dafny is telling you that you don't have sufficient reads clauses to invoke `fields`. What makes you think that you do? I don't see the reads clause...

I see, sorry I only now understand your intent, and now I also understand why it's surprising your program didn't verify to begin with. What's the reads clause of a...