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

WIP: building decideEventuallyZeroes on top of decideIfZeroes #687

Draft
wants to merge 29 commits into
base: main
Choose a base branch
from
Draft

WIP: building decideEventuallyZeroes on top of decideIfZeroes #687

wants to merge 29 commits into from

Commits on Sep 29, 2024

  1. chore: delete dead code

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

  2. chore: try to add more abstractions

    @bollu
    bollu committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    6dd5e8a View commit details
    Browse the repository at this point in the history

  3. chore: prove eval eq eval'

    @bollu
    bollu committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    f966632 View commit details
    Browse the repository at this point in the history

  4. chore: get main thm through

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

Commits on Sep 30, 2024

  1. WIP: FSM abstractions

    @alexkeizer
    alexkeizer committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    24b76a6 View commit details
    Browse the repository at this point in the history

  2. appendVector'

    @alexkeizer
    alexkeizer committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    888925b View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. tmp

    @luisacicolini
    luisacicolini committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    2311e78 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. WIP: CircuitProd helpers

    @alexkeizer
    alexkeizer committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    283e21a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'fsm-abstractions' of github.com:opencompl/lean-mlir int… 

    …o fsm-abstractions
    @alexkeizer
    alexkeizer committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    5c7c9bd View commit details
    Browse the repository at this point in the history

  3. fix: red squigly 

    Co-authored-by: Siddharth <[email protected]>
    @alexkeizer @bollu
    alexkeizer and bollu committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    01f9647 View commit details
    Browse the repository at this point in the history

  4. WIP: introduce more BitVec abstractions 

    Co-authored-by: Siddharth <[email protected]>
    @alexkeizer @bollu
    alexkeizer and bollu committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a31f8db View commit details
    Browse the repository at this point in the history

  5. refactor: move refactored defs to a New suffixed copy of FiniteStat… 

    …eMachine

Co-authored-by: Siddharth <[email protected]>
    @alexkeizer @bollu
    alexkeizer and bollu committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    8245bea View commit details
    Browse the repository at this point in the history

  6. final final attempt 

    Let's not continue this
    @alexkeizer
    alexkeizer committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    78c3b3d View commit details
    Browse the repository at this point in the history

  7. nuke bitvectors 

    Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Luisa Cicolini <[email protected]>
    @alexkeizer @bollu @luisacicolini
    3 people committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    62e8341 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. cleaned bitwise op section a bit

    @luisacicolini
    luisacicolini committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    7c44731 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2024

  1. name fixes

    @luisacicolini
    luisacicolini committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    6f4d5c3 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2024

  1. pairing with sid: bitwiseAnd, its eval and support stuff

    @luisacicolini
    luisacicolini committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    4846151 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. chore: bring back eval and eval'. 

    This lets us use the low level corecursion definition using eval',
and the theorem `eval_eq_eval'` to go between the higher level
and lower level versions.
    @bollu
    bollu committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    adad959 View commit details
    Browse the repository at this point in the history

  2. chore: prove bitwiseAnd 

    We circumvent the prior proof of high technology with map and evalMap,
instead going for directly defining the FSM for bitwise and.

This method has the distinct advantage of actually being able to be written
with the current broken defs.

This also forces us to add quite a bit of lemmata, which is always nice.
    @bollu
    bollu committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    718c323 View commit details
    Browse the repository at this point in the history

  3. chore: make eval_bitwiseAnd not depend on sorry anymore

    @bollu
    bollu committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    9fa03c7 View commit details
    Browse the repository at this point in the history

  4. feat: faff about with subsingleton, hoping for a cleanup, but none wa… 

    …s achieved
    @bollu
    bollu committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    40d4863 View commit details
    Browse the repository at this point in the history

  5. bitwise operators

    @luisacicolini
    luisacicolini committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    b65b8ef View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2024

  1. chore: document chris proof

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

  2. bitwise fsm cleaned

    @luisacicolini
    luisacicolini committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    27a5816 View commit details
    Browse the repository at this point in the history

  3. bitwise fsm cleaned

    @luisacicolini
    luisacicolini committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    6943aa5 View commit details
    Browse the repository at this point in the history

  4. either enlightnening or nonsense

    @luisacicolini
    luisacicolini committed Oct 8, 2024
    Configuration menu
    Copy the full SHA
    43e64bc View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Sid & Alex pairing

    @alexkeizer
    alexkeizer committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    34dd02e View commit details
    Browse the repository at this point in the history

  2. brain dump

    @alexkeizer
    alexkeizer committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    ec6bc2e View commit details
    Browse the repository at this point in the history

  3. chore: write thoughts on proof needed

    @bollu
    bollu committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    1b9d980 View commit details
    Browse the repository at this point in the history