Lagging riscv-coq version #1
Comments
|
I'd suggest the following protocol: Whenever someone wants a new feature from a dependency, that person updates the hash in |
|
ok |
andres-erbsen
pushed a commit
that referenced
this issue
Apr 24, 2019
samuelgruetter
added a commit
that referenced
this issue
Jul 28, 2023
In an "env everywhere" setting, where program_logic_goal_for! adds a (map.get fs fname = Some fimpl) hypothesis. Surprise #1: There's no case in straightline that handles if-then-else Surprise #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.
andres-erbsen
pushed a commit
to andres-erbsen/bedrock2
that referenced
this issue
Aug 1, 2023
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
added a commit
that referenced
this issue
Aug 11, 2023
* 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. * dead simple `call` based on `map.get` * convert from "fs everywhere" to "env everywhere" * 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 #1: There's no case in straightline that handles if-then-else Surprise #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. * wip "env everywhere" approach * make WeakestPrecondition.cmd complete wrt exec by leaving the structurally recursive cases of cmd_body unchanged, and defining the two non-structurally recursive cases (loop and call) directly in terms of exec. This seems to be the only approach that does not break proofs in bedrock2Examples too badly. * hardcode env implementation in bedrock2.Semantics, and update compiler, LiveVerif, end2end * add back program/Proper_program because it's used by rupicola * cp Semantics.v MetricSemantics.v * bedrock2.Semantics is now metrics-free, and metrics are in MetricSemantics * refinement lemmas for induction over command syntax * delete WP.v (opaque Module), only LAN9250 needed fixing * LiveVerif: wp_cmd is exec instead of WeakestPrecondition.cmd * env doesn't really need to be an Instance, it seems * fix argument order in refinement
samuelgruetter
pushed a commit
that referenced
this issue
Aug 16, 2024
fix MetricWeakestPrecondition and ...Properties
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Please bump
riscv-coqto latest commit. Is there a general plan for timely propagation of updates?The text was updated successfully, but these errors were encountered: