Coding 2024-06-27
I was focused on other things today, but I'm going to try to devote at least a few minutes to understanding what is up with Dafny.
According to the descriptions of the different batches when I isolated the assertions, the problem with the lemma that isn't brittle because of RNG screw is down to the postcondition.
A little more detail. The commutative property of summation basically says that we can re-index a summation, and get the same result, as long as we obey some "obvious" rules for the re-indexing. In the corresponding lemma, I'm using an ensures clause to assert this equality. Now, intuitively, I think the (relatively) high variance here corresponds to "requiring a lot of work from the verifier", which means I may be missing a step that Dafny is papering over. The current set of assertions is:
- If we remove k from the initial set of values to sum over, the equality still holds.
- Every item in the reduced set of permuted values "came from" a unique value in the reduced set of values.
- The sum of the set of permuted values is equal to the sum of the reduced set of permuted values, plus the value indexed by the permutation of k.
There is a missing step after this that Dafny can, "with effort", fill in for me. My hope is to figure out how to guide it so it can just go.
I'm not getting there tonight, so I'll get to bed and think about it for a while.
Good night.