+++
title = "Designing a proof with validation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3m2", "3a8g5g", "3a8g5e1a", "3a8g5d", "2e1c6a"]
forwardlinks = ["3a8g5f", "3a8g5e1"]
zettelid = "3a8g5e"
+++

Because of the trickiness of the proof, it would therefore be good to
integrate some validation into the algorithm, however, it's not quite
clear where to do this check. One possibility, which might allow for
quite a few optimisations to not make it too inefficient, is to prove
the following invariant on the semantics:

$$ \forall d\ s,\ t\ R_{d \rightarrow p_c} \Downarrow s \Longleftrightarrow t\\left( \bigcup_{i \in \text{preds}(p_c)} R_{d \rightarrow i} \cdot c_i \right)\Downarrow s. $$

However, this can be simplified even further by actually only verifying
the predicates that were generated from the path expressions instead,
giving the following invariant:

$$ \forall d\ s,\ P_{d \rightarrow p_c} \Downarrow s \Longleftrightarrow \left(\bigvee_{i \in \text{preds}(p_c)} P_{d \rightarrow i} \land c_i \right)\Downarrow s. $$

This property allows us to properly prove the correctness of the
predicates, because on can use this property to prove that if one of the
predecessors evaluates to true (which we can assume for the induction),
then due to the predicate being equivalent to the ors of all the
predecessors, it means that the current predicate must also be correct.