Skip to content

This commit moves logical step higher than weakest precondition. This

Thomas Somersrequested to merge
full-physical-step into master

allows the logical step to be used in Iris projects that do not use the standard weakest precondition.

  • Moved logical_step.v from program_logic to base_logic
  • Move weakest precondition rules for logical step to weakestpre.v
  • Added ElimModal instances for logical step w.r.t. physical step, logical step and weakest precondition
  • Remove the 'wp_use_step_strong' lemma as it is the same as 'wp_step_update_strong'

These changes were applied to use logical_step in Perennial

Merge request reports