GitLab

as done before for the context rule here I need to move the
intermediate value v to the start of the arguments because it
is not automatically picked up by eapply

kind of silly for me to find it now but the intermediate value
is something I might want to specify without giving out all
the other values

The new rules are a generalisation of the normal hoare
context rule and to prove it we show how to recover
the first context rule from the general.

Both rules admit the existence of values v in the lemma
premises but they describe it differently.

If in the first triple the value was explicit when using
⌜ r = v ⌝ or ⌜ Φ v ⌝ in the triple result for the general
rule we don't need to be explicity immediately.

There is a problem though as now the result assertion for
is Q : val → val → iProp instead of being Q :  val → iProp
and this might confuse people. Where do we get the new v
in the current triple if it does not have it?

You can always introduce a dummy ⌜ Φ v ⌝ in the result assertion
or just ignore v by wrapping in another lamba the original term
λ _ : Q.

this rule mimicks the iIntro rule from Iris. Pure assertions in the
precondition of a correctness triple can be pulled in the proof
context and used when unfolding a program execution but in our logic
it's not the pure assertions in the presumption but the pure assertion
in the result that can be pulled.

This also is a path I've been thinking on recently; an incorrectness
triple {{ ⌜ Φ ⌝ ∗ P }} e {{ Q }} cannot give you the Φ?

In separation logic the hoare triple for the context is as follows

{{ P }} e {{ x, R x }}  forall v, {{ R v }} K[v] {{ x, Q x}}
------------------------------------------------------------
	{{ P }} e {{ x, Q x}}

But this rule makes use of the fact that {{ False }} e {{x, Q x}}
is always valid.

In IL this is not true, the trivial triple is  [ P ] e [x, False ]
which gave me the idea of moving the value v to the result assertion.

This is actually in line with the previous IL triples that I saw where
the distinction on the good/bad values are put in the result
assertion.

Say K ≝ let x = ⬜ in if x ≥ 1 then x else error. Then the traditional
incorrectness triples are written as.

[v ∈ N] K[v] [r, v ≥ 1]
[v ∈ N] K[v] [ERR: v = 0]

So the current hoare_ctxS_iris_forall' rule encodes this pattern
as we can always split the bad values from the good value in the
result assertion.

again these signatures are easier to use when
it comes to eapply

this does not make much of a difference because we are just lifting
the assertion x = v to a generic predicate but should be enough for
a fist step

the hoare rules arguments must be given in order and this
means that the rules are nicer to use if the arguments that
can be inferred automatically are not the first.

This means that we can be specific with the first arguments
or not and the rest will follow along.

Instead of having a universal quantificator here we have
a existential quantificator which fits better with the current
hoare triples expressing reachability.

this rule works but features a universal quantification which is
not in the spirit of incorrectness logic.

this rule does not reference the value that gets discarded during
the execution of the sequential program so it's nice to have around.

This rule is different from the previous hoare context
rule because the quantification of v is at the triple
level instead of the lemma level.

This means that we can still use the predicate P' to make
an assertion on the possible result values of e while at the
same time we are not required to give it out at the lemma level.

Robbert wants me to prove the more general rule for the sequence where
we are allowed to not pick a value to put in the sequence as we will
discard it.

This rule should not be provable with the current hoare_ctxS rule as
we will still have a proof obligation in the form of an existential variable.

the original statement included a part about the intermediate
result of our computation even though we only throw it away.

This lemma is stronger because we can prove the previous one and
works better syntactically.

the interesting part of this is that in the theory behind Iris
the frame rule is recovered through the wand rule and monotonicity.

As I followed the same path this is quite nice to have, at least
to confirm that everything is working as I am expecting.

Signed-off-by: julesjacobs <julesjacobs@gmail.com>

the separating conjunction and the map disjoint specification
give us that separated locations are distinct. Now for this
contrived example we are reasoning about distinct pointers
which means we have to be able to distinguish locations.

the proof rules definitions were ok but to actually use
them effectively and have the eauto or eapply instance the correct
parts for us we have to refactor them so that we can specify the
interesting parts of our goals ourself and have eauto pick up for us

As an example in the context proof rule reordering from

Lemma hoare_ctxS E P P' e Q v

to

Lemma hoare_ctxS E P' P e Q v

makes it possible for us to specify both the context we want
to use and the intermediate heap P' while having eauto fill out
P e Q v for us

now that we have the hoare triples for the incorrectness logic
it is time to see if they are any good

I forgot to add all the error rules so everything was quite useless

Jules also went on to suggest tricks and better formulas for the rules
so I tried to follow advice where possible and not encode the shape of
the iProps in the lemmas.

I am getting some strange errors from Coq and I'm not sure
what is happening. I'll discuss this with Jules