dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Base64 Encoding Library #3

Open JunyoungLim opened 5 years ago

JunyoungLim commented 5 years ago

This PR introduces the Base64 Library, which has the following key function methods:

function method Decode(s: seq<char>): (b: Result<seq<uint8>>)

which takes a string, and returns a sequence of unsigned bytes when the string is of Base64 encoding, or a failure otherwise,

and

function method Encode(b: seq<uint8>): (s: seq<char>)
    ensures Decode(s) == Success(b)

which takes a sequence of unsigned bytes and returns an encoded string with the Base64 scheme, and guarantees that the Decode function will be able to successfully decode the output of the Encode function.

samuelgruetter commented 5 years ago

ping @RustanLeino, could you please review this?

RustanLeino commented 5 years ago

This slipped through the cracks for me, I'm afraid. It looks good. My only comment is that we now use 2 spaces for the indent instead of 4.