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.

Sign up for GitHub

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

Jump to bottom

prove memory safety for chacha20 implementation #72

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
Draft

prove memory safety for chacha20 implementation #72

wants to merge 12 commits into from

Commits on Jul 21, 2022

  1. Fix probable typo introduced in bcd4bcf

    @JasonGross
    JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    e875433 View commit details
    Browse the repository at this point in the history

  2. Create non-inlined chacha20_block

    @JasonGross
    JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    cbd45e7 View commit details
    Browse the repository at this point in the history

  3. pull out which byte/word instances to use in straightline 

    when doing certain types of loads
    @jmgrosen @JasonGross
    jmgrosen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    9cdaae2 View commit details
    Browse the repository at this point in the history

  4. chacha20 memory safety proof wip

    @jmgrosen @JasonGross
    jmgrosen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    58860a3 View commit details
    Browse the repository at this point in the history

  5. expose some slowness

    @andres-erbsen @JasonGross
    andres-erbsen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    da5f6bd View commit details
    Browse the repository at this point in the history

  6. cbv for map lookup seems rather difficult 

    @jmgrosen @samuelgruetter
    @andres-erbsen @JasonGross
    andres-erbsen authored and JasonGross committed Jul 21, 2022
    2 Configuration menu
    Copy the full SHA
    c1b6559 View commit details
    Browse the repository at this point in the history

  7. step through chacha20 loop body

    @andres-erbsen @JasonGross
    andres-erbsen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    c92fdff View commit details
    Browse the repository at this point in the history

  8. get to Qed on basic chacha20 proof

    @jmgrosen @JasonGross
    jmgrosen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    7460694 View commit details
    Browse the repository at this point in the history

  9. a more useful postcondition on chacha20 spec

    @jmgrosen @JasonGross
    jmgrosen authored and JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    0f95bf6 View commit details
    Browse the repository at this point in the history

  10. Fix after rebase

    @JasonGross
    JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    71a6777 View commit details
    Browse the repository at this point in the history

  11. Add back ring instance

    @JasonGross
    JasonGross committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    1771f63 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2022

  1. Improve perf of straightline_cleanup

    @JasonGross
    JasonGross committed Jul 22, 2022
    Configuration menu
    Copy the full SHA
    ba6b597 View commit details
    Browse the repository at this point in the history