+++
title = "PTrue preservation for γ-functions"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5e1"]
forwardlinks = ["3a8g5e"]
zettelid = "3a8g5e1a"
+++

When using γ-functions, one needs to prove that for a join-point, the
`PTrue` property is preserved accross the semantics. For the η-function
when there is no join-point, this was quite straightforward as no
previous nodes had to be examined, there was only one. However, when
proving the γ-function, there are multiple predecessors. Even though we
have the `pred_correct` property, which has been validated by the SAT
solver ([\#3a8g5e]), there is no guarantee that each of the predecessors
will be evaluated to a `Some` value. Therefore, when we do the global
`or` of all the predecessors, and say that this implies the correctness
of the predicate at this point, we cannot be sure that we are evaluating
that predicate to a value.

Furthermore, it is actually most likely that we will not evaluate that
predicate to a value, because there are various conditions and variables
that remain undefined at that point. This means that various conditions
will evaluate to a `None` value.

There are three different possible solutions to this:

1.  Evaluate each predecessor with the original `eval_predicate`
    function, but then or them together lazily using a slightly
    different evaluation function. This evaluation function will take
    into account the fact that some predicates will be able to return
    `None`. The main problem with this is that this doesn't make it easy
    to guarantee that the current predicate will return a `Some` value
    with the same state. Instead, the current predicate would probably
    also have to be evaluated lazily.
2.  Evaluate the whole predicate lazily, and only care about the truth
    value of correctness at the output. This is definitely a better
    solution than the previous, even though it probably requires more
    changes. One main problem with this solution is that it may not be
    possible to prove the required correctness proof using the SAT
    solver.
3.  Finally, another solution would be to keep track of the evaluation
    of each of the conditions, and therefore show that each condition is
    evaluating to a `Some` value. Then, proving that when we encounter a
    predicate that we must have traversed it previously, and due to the
    fact that SSA guarantees that if the definition of a point dominates
    the current point, then it's value is the value is known to be the
    same as at the definition point, one can show that the condition at
    the current point will also evaluate to a `Some` value. This is
    probably the most realistic, but quite a difficult solution with a
    lot of work involved to get it to work.

  [\#3a8g5e]: /zettel/3a8g5e