This adapts changes made in #238 for mem_omega into simp_mem. This adds a ITP style mode into simp_mem, which receives user guidance and attempts to proceed according to user input. It throws errors if the goal state does not match the expected goal state. If the goal state matches, it tries to dischange side conditions automatically. Failing this, it creates new goals for the user to discharge these side conditions. In total, this converts simp_mem into a tactic that's usable for making incremental, interactive progress in simplifying memory non-interference.
Testing:
No semantics changed. Conformance succeeds.
Stacked on top of #238
What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine?
License:
By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
Description:
This adapts changes made in #238 for
mem_omegaintosimp_mem. This adds a ITP style mode intosimp_mem, which receives user guidance and attempts to proceed according to user input. It throws errors if the goal state does not match the expected goal state. If the goal state matches, it tries to dischange side conditions automatically. Failing this, it creates new goals for the user to discharge these side conditions. In total, this convertssimp_meminto a tactic that's usable for making incremental, interactive progress in simplifying memory non-interference.Testing:
No semantics changed. Conformance succeeds.
Stacked on top of #238 What tests have been run? Did
make allsucceed for your changes? Was conformance testing successful on an Aarch64 machine?License:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.