MSR-to-ProVerif: Pulling out formula negations #631
Conversation
| notsArePulledOut' (Qua _ _ p ) = notsArePulledOut' p | ||
| notsArePulledOut' _ = True | ||
|
|
||
| pullnots' f = if f /= pullStep f then pullnots' (pullStep f) else f |
There was a problem hiding this comment.
@yavivanov: What does this function do?
There was a problem hiding this comment.
The idea is that pullStep and pullnots' work together to pull the negations to the front. So, I'm going to go into both of them.
pullStep pulls the negations in a sub-formula "one sub-formula/level" to the front once (if that's possible). Essentially, it does only one step to the front wherever possible. This is why the cases where we have negations that we can pull to the front are not recursive - they just pull the negation in the sub-formula one level above and don't go deeper. If no negation can somehow be pulled to the front, then the function returns the same formula without any changes.
pullnots' is what pulls the negations to the front recursively. Originally, all should've been done by pullStep, i.e. the recursion should've been there. The problem was that we recurse on the formula top-down (to smaller sub-formulas), but we change the smaller sub-formulas as we pull the negations. Moreover, we cannot go back up to a bigger sub-formula, see what has changed, pull the negations further (from the level of the larger sub-formula[s] to the level of even larger sub-formulas) and then dive in at where we left. Potentially, we might need to go all the way back to the highest level to be able to pull negations or we need to "wait" for the negations three levels down to be pulled to the same level so that we can pull negations at the current one. I didn't manage to get it to consider such cases during the top-down recursion on the formula. Thus, having everything in pullStep meant that some transformations where not "seen". Thus, I made it so that pullStep does only one step to the front and pullnots' makes sure we exhaustively do all steps and each time consider the results of the different steps.
pullnots' checks if we have pulled all negations as much as possible (if f /= pullStep f). In this case, calling pullStep doesn't pull anything - it returns the same formula again, and so does pullnots' (else-branch). If the formula was changed by the pullStep call, then we have pulled some negations in it one level above their respective levels. Thus, we try to pull the resulting negations in the formula one further level above their respective level (then-branch).
| Conn And (Not p) (Not q) -> Not $ p .||. q | ||
| Conn Or (Not p) (Not q) -> Not $ p .&&. q | ||
| Conn Imp p (Not q) -> Not $ p .&&. q | ||
| Conn c p q -> Conn c (pullStep p) (pullStep q) |
There was a problem hiding this comment.
We should exhaustively list the cases here, so if new connectives are added, we do not compute incorrect results. I think this can only be an iff, in which case ... can't we pull the Not out as well, if both sides have it?
There was a problem hiding this comment.
Yes, the Iff case should absolutely be there - I think that I missed it only because I somehow didn't write test formulas with it.
Hi!
As requested by @rkunnema, I have implemented a function that pulls the negations in lemma formulas as much to the front as possible. In the ideal case, the function transforms a given formula into a logically equivalent formula that contains only one negation at the formula's start. So, for a given formula F that has negations, we try to obtain a formula in the form ¬F' having only one negation.
The transformation benefits the MSR-to-ProVerif translation by allowing us to translate/analyze the obtained F' with ProVerif.
If such a transformation is not entirely possible for a given formula, the functionality outputs a translation warning showing how far it has transformed the formula.
Note that the translation uses the transformed formula (no matter how far transformed it is).
The changes are confined to the Export.hs file in the export module and only affect the MSR to ProVerif translation.