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

Verifying gcm_init_v8 -- a proof strategy #247

Open
wants to merge 25 commits into
base: main
Choose a base branch
from
Open

Verifying gcm_init_v8 -- a proof strategy #247

wants to merge 25 commits into from

Commits on Nov 20, 2024

  1. More gcm_init_v8

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    e37d50f View commit details
    Browse the repository at this point in the history

  2. Add an important lemma

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    4410723 View commit details
    Browse the repository at this point in the history

  3. Add another lemma for gcm_init_H_asm

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    4a9ca4d View commit details
    Browse the repository at this point in the history

  4. Identified a set of lemmas for simplifying the goal

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    3b01254 View commit details
    Browse the repository at this point in the history

  5. Need to look into RME to prove gcm_polyval_asm_gcm_polyval_equiv

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    2ffd8d7 View commit details
    Browse the repository at this point in the history

  6. Prove a couple more lemmas

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    557856a View commit details
    Browse the repository at this point in the history

  7. Renaming and simplifying theorems

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    5b14ee2 View commit details
    Browse the repository at this point in the history

  8. Some more experiments

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    64483b7 View commit details
    Browse the repository at this point in the history

  9. Incremental proof for gcm_init_v8

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    8950f38 View commit details
    Browse the repository at this point in the history

  10. Bug in h_s36_non_effects

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    9f74fc1 View commit details
    Browse the repository at this point in the history

  11. Proving sorry'ed lemmas

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    6b0c220 View commit details
    Browse the repository at this point in the history

  12. Proving h_H3, h_H4, h_H5

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    3a68c55 View commit details
    Browse the repository at this point in the history

  13. Proving h_H6, h_H7, h_H8

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    c5c3d40 View commit details
    Browse the repository at this point in the history

  14. Proving h_H9, h_H10 and h_H11 and finish the rest of the proof

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    e855c82 View commit details
    Browse the repository at this point in the history

  15. Fix an import issue

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    eb0e911 View commit details
    Browse the repository at this point in the history

  16. Clean up comments and proved some sorry'ed lemmas

    @pennyannn
    pennyannn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    263b643 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2024

  1. Proving h_v16_s106

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    4fd2eb9 View commit details
    Browse the repository at this point in the history

  2. Proving h_v17_s107

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    03e57d9 View commit details
    Browse the repository at this point in the history

  3. Proving h_v16_s73 and h_v18_s75

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    71d054d View commit details
    Browse the repository at this point in the history

  4. Proving h_v16_s144

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    da3b434 View commit details
    Browse the repository at this point in the history

  5. Proving h_v17_s145

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    b708c6c View commit details
    Browse the repository at this point in the history

  6. Proving all intermediate lemmas in the theorem

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    0e35e57 View commit details
    Browse the repository at this point in the history

  7. Clarify bv lemmas and cleanup

    @pennyannn
    pennyannn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    df846b7 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2024

  1. Add an example for problem with bv_decide

    @pennyannn
    pennyannn committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    a54bfd0 View commit details
    Browse the repository at this point in the history

  2. Exposing the bv_decide problem

    @pennyannn
    pennyannn committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    e7e3cf6 View commit details
    Browse the repository at this point in the history