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: Switch to using bv_decide to decide memory goals instead of bv_omega #197

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

feat: Switch to using bv_decide to decide memory goals instead of bv_omega #197

wants to merge 69 commits into from

Commits on Sep 26, 2024

  1. feat: bitvector constant folding simprocs 

    This simproc simplifies expressions by attempting to constant fold using `omega`
to make sure we never see modulos, and moves all arithmetic constants to the left.

The goal is for this to be upstreamed sooner rather than later.
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    878735e View commit details
    Browse the repository at this point in the history

  2. chore: delete bv_omega', reuse bv_omega

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

  3. chore: BitVec.le_def already has bv_toNat tag

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

  4. Apply suggestions from code review 

    Co-authored-by: Alex Keizer <[email protected]>
    @bollu @alexkeizer
    bollu and alexkeizer authored Sep 26, 2024
    Configuration menu
    Copy the full SHA
    50ee21b View commit details
    Browse the repository at this point in the history

  5. chore: reword docstring

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

  6. chore: move files around to have tests in tests/

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

  7. chore: add more docstring

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

  8. chore: cleanup

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

  9. chore: try to get 'simp only [bv_toNat] at *' working

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

  10. chore: directly invoke simp instead of using evalTactic. Next step:… 

    … directly invoke `omega`
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    3eab45f View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'origin/main' into replace-simp-mem-eval… 

    …-tactic
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    d5dbe2b View commit details
    Browse the repository at this point in the history

  12. chore: cleanup

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

  13. chore: inline omega, and don't use so we can return the model back

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

  14. chore: cleanup code around omega

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

  15. chore: don't enable tracing in memory aliasing tests.

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

  16. Merge branch 'address-normalization-simproc' into simp-mem-v2

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

  17. chore: don't call simproc

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

  18. chore: add failed experiment with address normalization timing out

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

  19. chore: nuke all old theory, and rewrite things in terms of bitvectors

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

  20. chore: see that mem_decide_bv works well when we don't have arithmeti… 

    …c on nats

I'm considering switching the `n` in `mem_legal' a n` to a `BitVec 64`, but
it maybe possible to write preprocessing to write the proof state purely
in terms of bitvectors; Let's first get enough to try to push `memcpy`
proof through.
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    7924c21 View commit details
    Browse the repository at this point in the history

  21. chore: fine-tune tactic a bit

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

  22. bv_decide fails mysteriously?? when used as evalTactic?? what is goin… 

    …g on??
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    f2cc13c View commit details
    Browse the repository at this point in the history

  23. I'm going crazy x(

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

  24. chore: indeed bv_decide is confused.

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

  25. chore: hunt down inconsistency.

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

  26. chore: create abstraction to bridge bitvec/nat

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

  27. chore: get memory aliasing file working

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

  28. chore: show how bitvector theory can fail us, and what the remedy is … 

    …in SHA-512 case
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    610147d View commit details
    Browse the repository at this point in the history

  29. chore: rewrite to use bitvectors. 

    This one is particularly interesting, since we see where bitvec
theory limits us: we can't reason about the fact that the length = 80!.
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    92d0290 View commit details
    Browse the repository at this point in the history

  30. chore: make progress on memcpy proof, it's actually... usable? it doe… 

    …sn't hang for 10+ seconds each time
    @bollu
    bollu committed Sep 26, 2024
    Configuration menu
    Copy the full SHA
    4532ae2 View commit details
    Browse the repository at this point in the history

  31. feat: yep yep this is massively more usable

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

  32. chore: add missing assumption

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

  33. chore: kill a 'sorry'

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

Commits on Sep 27, 2024

  1. chore: try to simplify proof state to see what's going wrong

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

  2. chore: use proof 2

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

  3. chore: get memcpy proof through

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

  4. chore: shrink

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

  5. chore: simplify proof of memcpy further

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

  6. chore: move axiom into precondition

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

  7. chore: delete axiom that was used in place of a hypothesis

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

  8. chore: add notes in the other files

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

  9. chore: time bv_decide, 11 seconds

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

  10. chore: fixup simp_mem some more

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

  11. chore: checkpoint

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

  12. chore: be careful with withMainContext

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

  13. chore: checkpoint state

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

  14. chore: give up on calling bv_decide and simp programatically, too muc… 

    …h stuff is messed up
    @bollu
    bollu committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    b2ce27d View commit details
    Browse the repository at this point in the history

  15. chore: document totally bonkers popcount failure

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

  16. chore: update memcpy proof

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

Commits on Sep 28, 2024

  1. chore: start adding linters and related constructs

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

  2. chore: add linting to help spot weird BV expressions

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

  3. chore: show what's needed for popcount

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

  4. chore: get SHA512Prelude working

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

Commits on Sep 30, 2024

  1. chore: bump up toolchain 29/9/2024

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

Commits on Oct 1, 2024

  1. bugfixes in pairing with @shilgoel, @alexkeizer

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

  2. chore: regenerate LRAT proofs

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

  3. chore: add or_self, was somehow lost?

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

  4. chore: fixup paths

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

  5. chore: update SHA512_block_armv8_rules

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

  6. chore: fixup proof

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

  7. chore: update popcount32

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

  8. chre: fixup MemCpyVCG

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

  9. chore: CSE changed

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

  10. Merge branch 'toolchain-bump-29-9-2024' into simp-mem-v2

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

  11. chore: clenup AddLoop

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

  12. chore: Henrik's fix worked

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

  13. chore: merge conflict resolved

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

Commits on Oct 3, 2024

  1. chore: write alternative for read/write_bytes called read/write_bytes… 

    …' that takes bitvec as argument
    @bollu
    bollu committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    421619e View commit details
    Browse the repository at this point in the history

  2. chore: explore changing read_mem_bytes and write_mem_bytes to read_me… 

    …m_bytes' and write_mem_bytes', this is a total disaster.
    @bollu
    bollu committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    e8995e4 View commit details
    Browse the repository at this point in the history