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

feat: recurrence for BitVec.mul as repeated shifts for bitblasting #6

Closed
wants to merge 64 commits into from
Closed

feat: recurrence for BitVec.mul as repeated shifts for bitblasting #6

wants to merge 64 commits into from

Commits on Jun 3, 2024

  1. chore: start writing recurrences for mul

    @bollu
    bollu committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    247349c View commit details
    Browse the repository at this point in the history

  2. chore: write udiv recursion eqn

    @bollu
    bollu committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    55cfc6d View commit details
    Browse the repository at this point in the history

  3. chore: add mul verified statement from z3

    @bollu
    bollu committed Jun 3, 2024
    Configuration menu
    Copy the full SHA
    2e5ea9f View commit details
    Browse the repository at this point in the history

Commits on Jun 4, 2024

  1. chore: check in WIP

    @bollu
    bollu committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    910ce3b View commit details
    Browse the repository at this point in the history

  2. chore: make progress

    @bollu
    bollu committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    5ae0995 View commit details
    Browse the repository at this point in the history

  3. chore: continue writing theorems

    @bollu
    bollu committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    203b34b View commit details
    Browse the repository at this point in the history

  4. chore: push

    @bollu
    bollu committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    6df5fd5 View commit details
    Browse the repository at this point in the history

  5. chore: finish proof of recurrence

    @bollu
    bollu committed Jun 4, 2024
    Configuration menu
    Copy the full SHA
    bec5b36 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2024

  1. chore: rejigger files, move to bitvec/bitblast

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    e6cba22 View commit details
    Browse the repository at this point in the history

  2. chore: cleaup proofs, move them to the right locations

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    2f0cb91 View commit details
    Browse the repository at this point in the history

  3. chore: drop large z3 comment

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    8632849 View commit details
    Browse the repository at this point in the history

  4. chore: move theorems around to proper location

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    351a7ce View commit details
    Browse the repository at this point in the history

  5. chore: more cleanup

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    75867dd View commit details
    Browse the repository at this point in the history

  6. chore: move twoPow into bitwise

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    bea6a61 View commit details
    Browse the repository at this point in the history

  7. Apply suggestions from code review 

    chore: remove parens around 0, 1

Co-authored-by: Tobias Grosser <[email protected]>
    @bollu @tobiasgrosser
    bollu and tobiasgrosser authored Jun 8, 2024
    Configuration menu
    Copy the full SHA
    33be7e5 View commit details
    Browse the repository at this point in the history

  8. chore: delete more parens around 0#w, 1#w

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    9bc8d7d View commit details
    Browse the repository at this point in the history

  9. chore: drop newline

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    fc67256 View commit details
    Browse the repository at this point in the history

  10. Apply suggestions from code review 

    chore: period to end of docstring.

Co-authored-by: Tobias Grosser <[email protected]>
    @bollu @tobiasgrosser
    bollu and tobiasgrosser authored Jun 8, 2024
    Configuration menu
    Copy the full SHA
    71a6c23 View commit details
    Browse the repository at this point in the history

  11. chore: drop paren

    @bollu
    bollu committed Jun 8, 2024
    Configuration menu
    Copy the full SHA
    c91edf1 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2024

  1. wip: bitblast shifts

    @bollu
    bollu committed Jun 13, 2024
    Configuration menu
    Copy the full SHA
    ecde706 View commit details
    Browse the repository at this point in the history

Commits on Jun 15, 2024

  1. chore: start shift right

    @bollu
    bollu committed Jun 15, 2024
    Configuration menu
    Copy the full SHA
    a61c43e View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2024

  1. chore: update shift left to different widths

    @bollu
    bollu committed Jun 26, 2024
    Configuration menu
    Copy the full SHA
    5cba64a View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2024

  1. chore: more bitblast

    @bollu
    bollu committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    0b4a59f View commit details
    Browse the repository at this point in the history

  2. chore: fixup final theorem

    @bollu
    bollu committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    cbf80f8 View commit details
    Browse the repository at this point in the history

  3. chore: shiftRight recurrence theorem

    @bollu
    bollu committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    b14ba43 View commit details
    Browse the repository at this point in the history

  4. chore: that was logical shift right. Skip arithmetic shift right for now 

    The arithmetic shift right lacks a `BitVec` implementation anyway, so
we move on to div/rem.
    @bollu
    bollu committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    2e6ff6f View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2024

  1. feat: characterize div and mod via arithmetic

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    af5b90d View commit details
    Browse the repository at this point in the history

  2. chore: cleanup hypotheses

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    f967caf View commit details
    Browse the repository at this point in the history

  3. chore: prove another equivalence given an lt hypothesis

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    b9f78b5 View commit details
    Browse the repository at this point in the history

  4. chore: prove necessary equivalence with sufficiently weak hypothesis … 

    …to embark on divrem quest
    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    904a01b View commit details
    Browse the repository at this point in the history

  5. chore: write theorem statement for DivRem recurrence

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    36711b0 View commit details
    Browse the repository at this point in the history

  6. chore: cleanup theorem statement to be cripser

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    f267fe3 View commit details
    Browse the repository at this point in the history

  7. chore: write proof sketch of why the div, rem sorries are true. Now f… 

    …ill them up!
    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    0ed0d44 View commit details
    Browse the repository at this point in the history

  8. chore: I believe the proof, now I need to encode it

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    0e23bbd View commit details
    Browse the repository at this point in the history

  9. chore: see that we have an overflow, can't write it this way.

    @bollu
    bollu committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    211fe3e View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2024

  1. chore: write udiv proof, need to prove the other branch of the proof … 

    …as well
    @bollu
    bollu committed Jun 29, 2024
    Configuration menu
    Copy the full SHA
    5b3bbc1 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2024

  1. chore: stash

    @bollu
    bollu committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    949c9b6 View commit details
    Browse the repository at this point in the history

  2. chore: comment out broken impl

    @bollu
    bollu committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    5c10b83 View commit details
    Browse the repository at this point in the history

  3. chore: start implement sshiftRight' and arith shift right recurrence.

    @bollu
    bollu committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    5beb72b View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2024

  1. chore: stash sshiftRight that hargonix wants next

    @bollu
    bollu committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    9720ab5 View commit details
    Browse the repository at this point in the history

  2. chore: add division invariant

    @bollu
    bollu committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    cc6817d View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2024

  1. chore: add div invariant

    @bollu
    bollu committed Jul 3, 2024
    Configuration menu
    Copy the full SHA
    89f6087 View commit details
    Browse the repository at this point in the history

  2. chore: add one impl of div_invariant

    @bollu
    bollu committed Jul 3, 2024
    Configuration menu
    Copy the full SHA
    44127be View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2024

  1. chore: add new division invariant that should be easier to prove

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    a2c3576 View commit details
    Browse the repository at this point in the history

  2. chore: prove remiander property, still a sorry left

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    56ea083 View commit details
    Browse the repository at this point in the history

  3. chore: add new invariant code. This is more subtle than I thought for… 

    … the second time
    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    9ca69d4 View commit details
    Browse the repository at this point in the history

  4. chore: stash

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    89ce200 View commit details
    Browse the repository at this point in the history

  5. chore: one half of base case

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    53fbd3a View commit details
    Browse the repository at this point in the history

  6. chore: second half of base case, half done

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    ac92331 View commit details
    Browse the repository at this point in the history

  7. chore: base case done

    @bollu
    bollu committed Jul 4, 2024
    Configuration menu
    Copy the full SHA
    80dedc2 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2024

  1. chore: show how to derive final theorem from recurrence

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    c9b1227 View commit details
    Browse the repository at this point in the history

  2. chore: delete dead code

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    0b6e2e8 View commit details
    Browse the repository at this point in the history

  3. feat: I now understand why the remainder is wr and dividend is wn, th… 

    …is is actually important for the proof
    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    8ad944a View commit details
    Browse the repository at this point in the history

  4. chore: lay everything out as a large structure with all preconditions

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    f1559cd View commit details
    Browse the repository at this point in the history

  5. chore: more progress, first settle on using Bool.toNat everywhere

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    809263c View commit details
    Browse the repository at this point in the history

  6. wrap up one branch of proof, now have second branch left

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    25fa2b4 View commit details
    Browse the repository at this point in the history

  7. feat: finish then branch, now do else branch

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    f9f8b09 View commit details
    Browse the repository at this point in the history

  8. chore: finish another sorry on the else branch

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    e15e05c View commit details
    Browse the repository at this point in the history

  9. feat: finish udiv/urem bitblast

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    faea676 View commit details
    Browse the repository at this point in the history

  10. chore: throw away incorrect implementations

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    ccf7628 View commit details
    Browse the repository at this point in the history

  11. chore: establish correctness of non-dependent statement

    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    935d35f View commit details
    Browse the repository at this point in the history

  12. chore: write _zero and _succ theorems for @hargoniX to be able to bit… 

    …blast
    @bollu
    bollu committed Jul 5, 2024
    Configuration menu
    Copy the full SHA
    c83cf03 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. chore: delete new file

    @bollu
    bollu committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    a20b14d View commit details
    Browse the repository at this point in the history

  2. chore: added sshiftRight as well

    @bollu
    bollu committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    09016e7 View commit details
    Browse the repository at this point in the history