lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } > This might not seem like much, but it repre

lemma LemmaFromToBytes(v: nat) ensures FromBytes(ToBytes(v)) == v { // Dafny does all the work! } > This might not seem like much, but it represents something you cannot easily do in other languages. This lemma asks Dafny to check that, for any possible nat value v, it always holds that FromBytes(ToBytes(v)) == v. Again, Dafny checks this at compile time — no testing required! --- How long does it take, do we rely on caching compilation results here? Is it iterating through all values?