I’m playing around with a verified utf8 library, so I want to be able to say something like “a single-octet utf8 value resides at a given address if a byte with the high-order bit set to 0 resides there”. What’s the best way to express and prove that constraint on a byte? Ideally this could be done without referring to integer encodings, since really I care about bit sequences and not numbers less than 255, but I’m curious about what’s possible currently.
Also, currently I’m creating a dataview where you can create a proof of a utf8 value at addr l from a proof of one byte with such-and-such constraints at l, or two bytes with such-and-such constraints at l, or three bytes with such-and-such constraints at l. Is this a good way to express this kind of variable-size data structure?
praxi lemma_byte{i:int} (byte(i)): [0 <= i < 255] void
absprop bitseq(int, int, int) // bitseq(i, n, b): bit n of int i is b
propdef hordbit(i:int, b:int) = bitseq(i, 7, b) // the high-order bit of i
is b
I will then state (but not prove) lemmas I need along the way.On Friday, February 20, 2015 at 12:44:03 PM UTC-5, Shea Levy wrote:
Hi all,
I’m playing around with a verified utf8 library, so I want to be able to
say something like “a single-octet utf8 value resides at a given address if
a byte with the high-order bit set to 0 resides there”. What’s the best way
to express and prove that constraint on a byte? Ideally this could be done
without referring to integer encodings, since really I care about bit
sequences and not numbers less than 255, but I’m curious about what’s
possible currently.
Also, currently I’m creating a dataview where you can create a proof of a
utf8 value at addr l from a proof of one byte with such-and-such
constraints at l, or two bytes with such-and-such constraints at l, or
three bytes with such-and-such constraints at l. Is this a good way to
express this kind of variable-size data structure?