1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
+++
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
|
