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

Use itree SpecM monad instead of CompM in Heapster #1778

Merged
merged 93 commits into from
Dec 10, 2022
Merged

Use itree SpecM monad instead of CompM in Heapster #1778

merged 93 commits into from
Dec 10, 2022

Commits on Jul 12, 2022

  1. began defining SpecM in Prelude.sawcore

    @lag47
    lag47 committed Jul 12, 2022
    Configuration menu
    Copy the full SHA
    661c442 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2022

  1. added some SpecM definitions

    @lag47
    lag47 committed Jul 19, 2022
    Configuration menu
    Copy the full SHA
    f852a35 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2022

  1. wrote new interface for SpecM

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

Commits on Jul 29, 2022

  1. fixed haddock syntax errors

    @lag47
    lag47 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    7f1b785 View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2022

  1. further refactored SpecM

    @lag47
    lag47 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    b501146 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2022

  1. partially rewrote saw translation

    Lucas Silver committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    6e783f7 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2022

  1. new draft of multiFixS function signature

    Lucas Silver committed Aug 17, 2022
    Configuration menu
    Copy the full SHA
    92fb1f9 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2022

  1. refactored MultiFixSBodiesS

    @lag47
    lag47 committed Aug 19, 2022
    Configuration menu
    Copy the full SHA
    1e8e7b3 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2022

  1. implementing SAW functions

    @lag47
    lag47 committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    211fac9 View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2022

  1. updated documentation

    @lag47
    lag47 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    bed9ee8 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2022

  1. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Aug 25, 2022
    Configuration menu
    Copy the full SHA
    f0a4895 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2022

  1. updated the SAW core prelude with the new versions of the SpecM opera… 

    …tions
    Eddy Westbrook committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    0e5bd0e View commit details
    Browse the repository at this point in the history

  2. Added VoidEvRetType for defining the evRetType of a Void to the SAW c… 

    …ore prelude
    Eddy Westbrook committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    be309ca View commit details
    Browse the repository at this point in the history

Commits on Aug 31, 2022

  1. renamed CallS to callS

    Eddy Westbrook committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    8b6a93c View commit details
    Browse the repository at this point in the history

  2. added the more general identOpenTerm

    Eddy Westbrook committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    f195a8f View commit details
    Browse the repository at this point in the history

  3. partially finished changing the translation to generate SpecM computa… 

    …tions instead of CompM
    Eddy Westbrook committed Aug 31, 2022
    Configuration menu
    Copy the full SHA
    4ecf85d View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2022

  1. almost done changing the translation to generate SpecM computations i… 

    …nstead of CompM
    Eddy Westbrook committed Sep 1, 2022
    Configuration menu
    Copy the full SHA
    3eea089 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2022

  1. got the new translation to SpecM to compile, yay!

    Eddy Westbrook committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    b5eb9f1 View commit details
    Browse the repository at this point in the history

  2. fixed some small bugs in the SAW core translation

    Eddy Westbrook committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    c434a4c View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2022

  1. changed more of the CompM operations in the translation to use the co… 

    …rresponding SpecM operations instead
    Eddy Westbrook committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    a074cbc View commit details
    Browse the repository at this point in the history

  2. fixed the type of errorS

    Eddy Westbrook committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    3d90681 View commit details
    Browse the repository at this point in the history

  3. added translations for the SpecM operations

    Eddy Westbrook committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    fbbc4c3 View commit details
    Browse the repository at this point in the history

  4. updated sawLet to use sort 1 instead of sort 0

    Eddy Westbrook committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    4e0c3f9 View commit details
    Browse the repository at this point in the history

  5. whoops, updated the SAW translation to use retS instead of returnS

    Eddy Westbrook committed Sep 6, 2022
    Configuration menu
    Copy the full SHA
    0b2d854 View commit details
    Browse the repository at this point in the history

Commits on Sep 7, 2022

  1. fixed up references to EnTree specs

    Eddy Westbrook committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    c5d8962 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2022

  1. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Oct 4, 2022
    Configuration menu
    Copy the full SHA
    9a596bb View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2022

  1. changed the SpecM monad to be a sort 0 instead of a sort 1

    Eddy Westbrook committed Oct 5, 2022
    Configuration menu
    Copy the full SHA
    f355421 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2022

  1. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    bebfce2 View commit details
    Browse the repository at this point in the history

  2. removed the old LetRecType1 type, and updated LetRecType to reference… 

    … the version from the SpecM module
    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    48f53a5 View commit details
    Browse the repository at this point in the history

  3. changed some uses of errorM to errorS; added a workaround for issue #… 

    …1748; changed uses of LetRecTypes to use List1 LetRecType, to be consistent with the SpecM module
    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    13d26b9 View commit details
    Browse the repository at this point in the history

  4. replaced uses of LetRecTypes with List1 LetRecType in the SpecM stuff… 

    … to be consistent with the Coq SpecM module
    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    4af67c3 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    354f285 View commit details
    Browse the repository at this point in the history

  6. removed workaround for issue #1748

    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    a991178 View commit details
    Browse the repository at this point in the history

  7. fixed mallocSpec in the linked list example to use a SpecM type

    Eddy Westbrook committed Oct 6, 2022
    Configuration menu
    Copy the full SHA
    9b19195 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2022

  1. changed the translation of functions to always use the empty FunStack

    Eddy Westbrook committed Oct 8, 2022
    Configuration menu
    Copy the full SHA
    6ad6fa5 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2022

  1. whoops, fixed Prelude.EmptyFunStack to the correct Prelude.emptyFunStack

    Eddy Westbrook committed Oct 11, 2022
    Configuration menu
    Copy the full SHA
    fb7e632 View commit details
    Browse the repository at this point in the history

  2. fixed some examples to use SpecM instead of CompM

    Eddy Westbrook committed Oct 11, 2022
    Configuration menu
    Copy the full SHA
    00e56cb View commit details
    Browse the repository at this point in the history

  3. fixed the translations of lowned rules to always use the empty FunStack

    Eddy Westbrook committed Oct 11, 2022
    Configuration menu
    Copy the full SHA
    7ed4c4a View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2022

  1. updated all examples to work with the new SpecM monad

    Eddy Westbrook committed Oct 12, 2022
    Configuration menu
    Copy the full SHA
    49ecbb1 View commit details
    Browse the repository at this point in the history

  2. Changed SpecM to take in a single EvType argument instead of two sepa… 

    …rate arguments specifying the event type
    Eddy Westbrook committed Oct 12, 2022
    Configuration menu
    Copy the full SHA
    e172e9a View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2022

  1. added QuantType instances to SAWCoreScaffolding.v

    Eddy Westbrook committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    4a07629 View commit details
    Browse the repository at this point in the history

  2. moved QuantType instances to a new file, SpecMExtra.v; updated the tr… 

    …anslations of existsS and forallS to use implicit arguments for their QuantType instances
    Eddy Westbrook committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    620c5f8 View commit details
    Browse the repository at this point in the history

  3. updated mbox example to work with the new translation

    Eddy Westbrook committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    bec4e69 View commit details
    Browse the repository at this point in the history

  4. updated examples to use the new VoidEv single argument instead of the… 

    … 2 arguments required before
    Eddy Westbrook committed Oct 13, 2022
    Configuration menu
    Copy the full SHA
    085e608 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2022

  1. updated the Prelude to the new definitions of CallS and MultiFixS

    Eddy Westbrook committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    eafdee7 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2022

  1. Updated to the new version of the CallS and MultiFixS combinators, th… 

    …at take a single "FrameCall" argument to specify function arguments
    Eddy Westbrook committed Oct 21, 2022
    Configuration menu
    Copy the full SHA
    c269957 View commit details
    Browse the repository at this point in the history

Commits on Nov 3, 2022

  1. added SpecM versions of mapBVVecM and appendCastBVVecM, and updated t… 

    …he translation to use these
    Eddy Westbrook committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    c81daf7 View commit details
    Browse the repository at this point in the history

  2. whoops, forgot to change appendCastBVVecM in one spot in the translation

    Eddy Westbrook committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    da763a5 View commit details
    Browse the repository at this point in the history

  3. whoops, forgot to change mapBVVecM to mapBVVecS

    Eddy Westbrook committed Nov 3, 2022
    Configuration menu
    Copy the full SHA
    54c7e58 View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2022

  1. first try at entree is_elem_spec_ref

    @m-yac
    m-yac committed Nov 8, 2022
    Configuration menu
    Copy the full SHA
    d973782 View commit details
    Browse the repository at this point in the history

Commits on Nov 9, 2022

  1. update mbox_proofs header with entrees

    @m-yac
    m-yac committed Nov 9, 2022
    Configuration menu
    Copy the full SHA
    ea28b0b View commit details
    Browse the repository at this point in the history

Commits on Nov 11, 2022

  1. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Nov 11, 2022
    Configuration menu
    Copy the full SHA
    83f4ddc View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2022

  1. get mbox_free_chain_spec_ref working

    @m-yac
    m-yac committed Nov 16, 2022
    Configuration menu
    Copy the full SHA
    91954fc View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2022

  1. prove mbox_concat/mbox_concat_chains_spec_ref

    @m-yac
    m-yac committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    409b1bb View commit details
    Browse the repository at this point in the history

  2. add alternate mbox_concat_chains_spec_ref

    @m-yac
    m-yac committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    5cd47ad View commit details
    Browse the repository at this point in the history

  3. add mbox_detach_spec_ref

    @m-yac
    m-yac committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    366c077 View commit details
    Browse the repository at this point in the history

  4. add mbox_drop_spec_ref

    @m-yac
    m-yac committed Nov 17, 2022
    Configuration menu
    Copy the full SHA
    d540e52 View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2022

  1. fixed up mbox proofs to work with updated entree-specs automation

    Eddy Westbrook committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    9c609ab View commit details
    Browse the repository at this point in the history

  2. Revert "fixed up mbox proofs to work with updated entree-specs automa… 

    …tion"

This reverts commit 9c609ab.
    @m-yac
    m-yac committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    a361a65 View commit details
    Browse the repository at this point in the history

  3. Proofs for mbox_len

    @RyanGlScott
    RyanGlScott committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    3e6e12b View commit details
    Browse the repository at this point in the history

  4. Merge branch 'heapster-itree' of https://github.com/GaloisInc/saw-script 

     into heapster-itree
    @m-yac
    m-yac committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    80f8565 View commit details
    Browse the repository at this point in the history

  5. update proofs with latest automation

    @m-yac
    m-yac committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    41e5a5b View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into heapster-itree

    Eddy Westbrook committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    bf26c67 View commit details
    Browse the repository at this point in the history

  7. add maybe automation, start on mbox_randomize

    @m-yac
    m-yac committed Nov 18, 2022
    Configuration menu
    Copy the full SHA
    aec2ac4 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2022

  1. Make mbox_len_spec_ref* proofs work with latest entree-specs

    @RyanGlScott
    RyanGlScott committed Nov 22, 2022
    Configuration menu
    Copy the full SHA
    63b3a79 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2022

  1. mbox_copy_spec_ref

    @RyanGlScott
    RyanGlScott committed Nov 23, 2022
    Configuration menu
    Copy the full SHA
    0e1e995 View commit details
    Browse the repository at this point in the history

  2. Another way to prove mbox_copy, beginnings of mbox_copy_chain

    @RyanGlScott
    RyanGlScott committed Nov 23, 2022
    Configuration menu
    Copy the full SHA
    183e923 View commit details
    Browse the repository at this point in the history

Commits on Nov 24, 2022

  1. update proofs with latest ex and shelve automation

    @m-yac
    m-yac committed Nov 24, 2022
    Configuration menu
    Copy the full SHA
    031d9a4 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2022

  1. Simplify mbox_copy_spec_ref__alt slightly, some progress on mbox_copy… 

    …_chain_spec_ref
    @RyanGlScott
    RyanGlScott committed Nov 27, 2022
    Configuration menu
    Copy the full SHA
    c1f05e6 View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2022

  1. update mbox auto with change to 999 RelGoal hint

    @m-yac
    m-yac committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    03fb5d0 View commit details
    Browse the repository at this point in the history

  2. don't greedily destruct Mboxes for now

    @m-yac
    m-yac committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    7c40584 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2022

  1. More progress on mbox_copy_chain and mbox_split_at

    @RyanGlScott
    RyanGlScott committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    f73203a View commit details
    Browse the repository at this point in the history

  2. add timing commands

    @m-yac
    m-yac committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    faaa363 View commit details
    Browse the repository at this point in the history

  3. update proofs with less cbns change

    @m-yac
    m-yac committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    64b1355 View commit details
    Browse the repository at this point in the history

  4. add sawLet automation

    @m-yac
    m-yac committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    269f3e5 View commit details
    Browse the repository at this point in the history

  5. mbox_split_at_spec_ref is proven!

    @RyanGlScott
    RyanGlScott committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    aba8237 View commit details
    Browse the repository at this point in the history

  6. More progress on mbox_copy_chain

    @RyanGlScott
    RyanGlScott committed Nov 29, 2022
    Configuration menu
    Copy the full SHA
    4759cd2 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2022

  1. use eithers instead of either, update proofs

    @m-yac
    m-yac committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    ab0e39c View commit details
    Browse the repository at this point in the history

  2. added heapster_set_event_type command, along with the io example to u… 

    …se it
    Eddy Westbrook committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    26f44ac View commit details
    Browse the repository at this point in the history

  3. Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into… 

    … heapster-itree
    Eddy Westbrook committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    0e9eed5 View commit details
    Browse the repository at this point in the history

  4. Complete proof of mbox_copy_chain

    @RyanGlScott
    RyanGlScott committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    290db7e View commit details
    Browse the repository at this point in the history

  5. mbox_detach_from_end proofs

    @RyanGlScott
    RyanGlScott committed Nov 30, 2022
    Configuration menu
    Copy the full SHA
    e4a40b3 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2022

  1. prove mbox_randomize_spec_ref

    @m-yac
    m-yac committed Dec 1, 2022
    Configuration menu
    Copy the full SHA
    fac87aa View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2022

  1. small tweaks to the hello world example

    Eddy Westbrook committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    ac18311 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into… 

    … heapster-itree
    Eddy Westbrook committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    1a077f4 View commit details
    Browse the repository at this point in the history

Commits on Dec 8, 2022

  1. translateCurryLocalPermImpl: Don't force the use of an EmptyFunStack 

    This caused typechecking errors in practice in some downstream code.
    @RyanGlScott
    RyanGlScott committed Dec 8, 2022
    Configuration menu
    Copy the full SHA
    c862d47 View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2022

  1. clean up + update mbox_proofs, linked_list_proofs

    @m-yac
    m-yac committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    c2385cc View commit details
    Browse the repository at this point in the history

  2. get make passing (rust typechecking fails)

    @m-yac
    m-yac committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    2f1d08b View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into heapster-itree

    @m-yac
    m-yac committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    bbac0b2 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into heapster-itree

    @RyanGlScott
    RyanGlScott committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    eabdf2d View commit details
    Browse the repository at this point in the history

  5. Install entree-specs as a Coq dependency 

    This updates the CI to build a particular `entree-specs` commit before building
the Coq support libraries. This also updates the instructions in the
`saw-core-coq` `README` accordingly.

Note that this requires limiting the Coq support window to 8.15 for now, as
`entree-specs` requires 8.15 as the minimum. In particular, `entree-specs`
does not yet support 8.16 (see GaloisInc/entree-specs#1), so we now require
Coq 8.15 exactly.
    @RyanGlScott
    RyanGlScott committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    d2d9f01 View commit details
    Browse the repository at this point in the history

  6. update proofs with latest changes to saw-core-coq

    @m-yac
    m-yac committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    b91d94e View commit details
    Browse the repository at this point in the history

  7. incorperate Haddock suggestions from @RyanGlScott

    @m-yac
    m-yac committed Dec 9, 2022
    Configuration menu
    Copy the full SHA
    52eca30 View commit details
    Browse the repository at this point in the history