4 ms·

This is pretty cool! I do have a nitpick I think is important. An empty byte array getting converted to zero seems like a bad edge case that should probably pr

This is pretty cool! I do have a nitpick I think is important. An empty byte array getting converted to zero seems like a bad edge case that should probably produce some kind of error invariant. This isn't a minor concern if the intent is to use this in serious applications that require this degree of formalism. The two proofs are easy to break: `ToBytes(FromBytes([])) != []`. It's an obvious example of the issue: FromBytes handles inputs ToBytes can't generate therefore they are not true inverses of each other. It's a simple case but it was quick to find in this simple example, and it hints at dangerous oversights that could lead to severe bugs in more complex scenarios, like in cryptography. It's critical to account for such edge cases.

occamrazor 3y ago
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!
abbeyj 3y ago
I was coming to say almost the exact opposite. `ToBytes(0)` should be equal to the empty array. This seems like the more natural representation, at least to me. 1. The implementation of `FromBytes` works properly only if the base case returns 0 for the empty array. So you already have, for free, `FromBytes([]) == 0`. You might as well use it. 2. `LemmaFromToBytes` currently requires the somewhat awkward and complicated `requires |bytes| > 0 && (|bytes| == 1 || bytes[0] != 0)`. We need to restrict this to only allowing non-empty arrays. And then we need to restrict it to not allowing leading zeros on arrays, except if the array is of length 1 and then we do allow a leading zero. If we represent 0 as `[]` instead of `[0]` then this all simplifies down to something like `requires |bytes| == 0 || bytes[0] != 0`. We allow arrays of any size and we never allow leading zeros on any array, which is easier to express. 3. Currently `ToBytes` has an `if-else` at the end and requires repeating the code `[byte]` in both branches. That's obviously not a lot of repetition but wouldn't it be nice to eliminate that? If we change the beginning to `if v == 0 then []` then we can replace the `if-else` at the end with just `ToBytes(w) + [byte]`. And we can get rid of the `ensures |r| > 0`. Then the structure of `ToBytes` and `FromBytes` more closely mirror each other, with the base cases being "the same".

occamrazor 3y ago

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!

abbeyj 3y ago

I was coming to say almost the exact opposite. `ToBytes(0)` should be equal to the empty array. This seems like the more natural representation, at least to me. 1. The implementation of `FromBytes` works properly only if the base case returns 0 for the empty array. So you already have, for free, `FromBytes([]) == 0`. You might as well use it. 2. `LemmaFromToBytes` currently requires the somewhat awkward and complicated `requires |bytes| > 0 && (|bytes| == 1 || bytes[0] != 0)`. We need to restrict this to only allowing non-empty arrays. And then we need to restrict it to not allowing leading zeros on arrays, except if the array is of length 1 and then we do allow a leading zero. If we represent 0 as `[]` instead of `[0]` then this all simplifies down to something like `requires |bytes| == 0 || bytes[0] != 0`. We allow arrays of any size and we never allow leading zeros on any array, which is easier to express. 3. Currently `ToBytes` has an `if-else` at the end and requires repeating the code `[byte]` in both branches. That's obviously not a lot of repetition but wouldn't it be nice to eliminate that? If we change the beginning to `if v == 0 then []` then we can replace the `if-else` at the end with just `ToBytes(w) + [byte]`. And we can get rid of the `ensures |r| > 0`. Then the structure of `ToBytes` and `FromBytes` more closely mirror each other, with the base cases being "the same".