Armael
commented
3 years ago A somewhat related idea: instead of using the (many) specialized rules for each instruction, we could have a proofmode-specific big specification for each instruction. It would not be the same as the "general" specification we have currently, but instead reformulated to be applied in an automation-friendly way. I'm thinking of simply having a lot of disjunctions (which are not proof-friendly and which the current general specs try to avoid) which would then be resolved by automation on concrete scenarios.
The advantage would be:
- simplify the proofmode tactic, by moving some of the ltac code that is currently used to select instruction rules to the shape of the "big spec"+associated automation;
- maybe have slightly more control / flexible automation in choosing the lemma? (unclear)
- technically, it means that we do not need the many specialized rules anymore (but it practice, we might still want to have them for "manual" debugging of the iInstr tactic)
(I'm not completely clear on how this idea interacts with the one described in the previous post.)
The current backtracking behavior on some instructions (load/store in particular) leads to confusing error messages in case of failure. (if the tactic tries rule1 || rule2, and we wanted to apply rule1 but it fails, it will try rule2, fail as well, and print a useless error message related to rule2.)
A related problem is with the jmp instruction; currently the proofmode decides on the rule depending on whether the content of the condition register is syntactically zero, which can be confusing (e.g. if it contains
(z-z), one needs to take care of rewriting that to zero before applying the tactic)One idea would be to regroup rules in different classes / lemma bases, where each lemma base should contain lemmas that can apply non-ambiguously wrt other lemmas in the base. Then, have a syntax for specifying a (set of) lemma base(s) in iInstr/iGo.
Also: it would be useful to be able to directly specify a lemma name...