[Iris-Club] pre-wp's definition: s, s1, and s2

[Ralf Jung]

Hi Jeehoon,

> I think I almost understand `pre-wp` ;-)  But I still cannot understand
> the use of step-index: may I ask what is the intuition behind requiring
> `m+1 \in ...` for the value case?  I think I understand why you required
> `m in ...` in the reduction case, since there is actually a step.  But
> for the value case, I am not sure why it is necessary to demand `m+1 \in
> ...`.  Why `m \in ...` is not enough?

Notice that we are using "m+1" on *both* sides of the implication in the
value case.  So, crucially, the step-index is not decreased if the
program is a value.  Decreasing it is not possible because values don't
actually take steps.  (More precisely speaking, if we were to decrease
that step-index, the BIND rule would fail.)

Another way to explain the "m+1" is the following: For all values v (and
masks E), we have the equivalence

  WP v @ E \Phi <-> |=>_E \Phi(v)

In other words, "weakest-pre of a value is a view shift". The
definitions look slightly different because for WP, we want to use the
same variable m as the step-index for the value- and stepping case, so
we quantify over a "0 <= m < n" and think of "m+1" as the current
step-index.  For primitive view shifts, we quantify over "0 < k <= n",
and k is the current step-index.  These two quantifications are entirely
equivalent.

I hope this helps, let me know if you have further questions.

Kind regards,
Ralf