3 ms·

TFA makes exactly this point. The lemma that Dafny proves is true, the reversed one is not and Dafny can provide the counterexample (the empty list).

• TrueDuality 3y ago
  I didn't notice that it is kind of called out in the post... It's the very last line and left as an exercise to the reader to infer which is almost worse since I would call this a flaw in the implementation of the functions and is being shown off as a sterling example of the capabilities of the language. The conversion between `[]` and `0` is the flaw that is hard to reason about here and propagates through any code that interacts with it in a way that violates a programmers expectations.
  • fluoridation 3y ago
    It's not that uncommon to have de/serialization functions where g(f(x)) == x for all x, but f(g(x)) != x for some x. Usually people just need to be able to correctly deserialize any valid serialized string, and preferably detect when a serialized string is invalid. Being able to deserialize some arbitrary string that doesn't represent any valid value but which can somehow still be reserialized into the same arbitrary string is a rather unusual requirement.
  • jtsiskin 3y ago
    It’s not just [] - it’s any amount of leading 0s. But this is exactly the point - if you forgot about proving `ToBytes(FromBytes(bs)) == bs`, forgot about this edge case, and later tried to prove a function that implicitly relied on that fact - Dafny would let you know!