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

Wp is exec #362

Draft
wants to merge 8 commits into
base: master
Choose a base branch
from
Draft

Wp is exec #362

wants to merge 8 commits into from

Commits on Aug 1, 2023

  1. define a WP.cmd' in terms of exec, might soon replace WP.cmd 

    and rules for cmd' whose premises are copied from WP.cmd.
This one is "fs everywhere" (ie list of functions everywhere).
The wp_call rule requires a NoDup, which would be cumbersome to
carry around.
    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    7a43f3a View commit details
    Browse the repository at this point in the history

  2. dead simple call based on map.get

    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    4b3e917 View commit details
    Browse the repository at this point in the history

  3. convert from "fs everywhere" to "env everywhere"

    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    b98be1f View commit details
    Browse the repository at this point in the history

  4. instead of unfold1_cmd_goal, eapply lemma_corresponding_to_command 

    In an "env everywhere" setting, where program_logic_goal_for!
adds a (map.get fs fname = Some fimpl) hypothesis.
Surprise mit-plv#1: There's no case in straightline that handles if-then-else
Surprise mit-plv#2: unfold1_... tactics are not the only place that depend
on conversion: There also exists a letexists in SPI that turns a
(WP (cmd.cond e _ _) ...) into an (exists v, eval e v /\ ...), and
probably more elsewhere.
    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    867c49b View commit details
    Browse the repository at this point in the history

  5. wip "env everywhere" approach

    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    36882d9 View commit details
    Browse the repository at this point in the history

  6. make the new cmd opaque to hnf and repeat split

    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    36780ed View commit details
    Browse the repository at this point in the history

  7. trying to pretend the new cmd is unfoldable by 

    sneaking an `apply_rules_until_propositional` call into
`letexists`, `eexists`, `esplit`, and inserting `unfold1_cmd_goal`
where still needed.
Gave up on memmove because it seems too hard to simulate a `cbn`
that happens under exists and ands by applying wp rules under
these exists and ands.
    @samuelgruetter @andres-erbsen
    samuelgruetter authored and andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    978d785 View commit details
    Browse the repository at this point in the history

  8. port more examples from wp to exec

    @andres-erbsen
    andres-erbsen committed Aug 1, 2023
    Configuration menu
    Copy the full SHA
    b46e864 View commit details
    Browse the repository at this point in the history