Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Base64 Encoding Library #3

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

JunyoungLim
Copy link

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
Copy link
Contributor

ping @RustanLeino, could you please review this?

@RustanLeino
Copy link
Collaborator

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.

davidcok pushed a commit that referenced this pull request Feb 14, 2023
davidcok pushed a commit that referenced this pull request Mar 3, 2023
davidcok added a commit that referenced this pull request Apr 17, 2023
* Working on reusable tests

* Debugging

* Debugging #2

* Debugging #3

* Debugging #4

* Debugging #4

* Debugging #5

* Debugging #6

* Debugging #7

* Debugging #8

* Debugging #9

* Debugging #10

* Debugging #11

* Debugging #12

* Debugging #13

* Debugging #14

* Debugging #14

* Debugging

* Debugging

* Debugging

* Debugging

* OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed

* OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed

* Fixing the concurrency check

* Old edits

* Edits to examples

* Touchups to examples and library

* Math relations and examples

* Some docstring documentation

* Some docstring documentation

* typo

* Formatting

* Removing semicolon

* Adjusting for Dafny 3

* Attempt to fix proof in ld dafny versions

* Fixing up docstrings

* Fixed examples

* Fixed formatting

* Fixed formatting

* Formatting

* Formatting

---------

Co-authored-by: davidcok <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants