make `WeakestPrecondition.cmd` complete wrt `Semantics.exec`#361

Merged

samuelgruetter merged 15 commits intomasterfrom wp_is_exec_1

Aug 11, 2023

+1,085-632

Commits on Jul 26, 2023

Commits on Jul 28, 2023

instead of unfold1_cmd_goal, eapply lemma_corresponding_to_command
samuelgruetter
committed

Commits on Jul 29, 2023

wip "env everywhere" approach
samuelgruetter
committed

Commits on Jul 31, 2023

make WeakestPrecondition.cmd complete wrt exec
samuelgruetter
committed

Commits on Aug 1, 2023

hardcode env implementation in bedrock2.Semantics,
samuelgruetter
committed

Commits on Aug 2, 2023

Commits on Aug 3, 2023

bedrock2.Semantics is now metrics-free, and metrics are in MetricSemantics
samuelgruetter
committed

Commits on Aug 4, 2023

refinement lemmas for induction over command syntax
samuelgruetter
committed

Commits on Aug 6, 2023

Commits on Aug 11, 2023