1. 21 Jul, 2021 6 commits
• update hoare_let · 355ceff7
Edoardo Putti authored
```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```
• add a section for the double free examples · ebdaed1e
Edoardo Putti authored
• allow for specifying the intermediate value · 8f39a784
Edoardo Putti authored
```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```
• prove context rule for error triples in Iris style · 6810c92c
Edoardo Putti authored
```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.```
• rename hoare_pure to hoare_intro · 18a31ecb
Edoardo Putti authored
```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 Φ?```
2. 28 Jun, 2021 1 commit
3. 27 Jun, 2021 4 commits
• add bind section to examples · 7105730f
Edoardo Putti authored
• add post_bind · 80e7da05
Edoardo Putti authored
• add a hoare context triple that mimics the SL one · 6fc357be
Edoardo Putti authored
```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.```
• update last incorrectness triples signatures · 6c400a19
Edoardo Putti authored
```again these signatures are easier to use when
it comes to eapply```
4. 26 Jun, 2021 1 commit
5. 22 Jun, 2021 2 commits
6. 21 Jun, 2021 6 commits
• add the existential flavour for the iris context rule · b5e01b96
Edoardo Putti authored
```Instead of having a universal quantificator here we have
a existential quantificator which fits better with the current
hoare triples expressing reachability.```
• change name of rule proposed by Robbert · 36ce25a6
Edoardo Putti authored
```this rule works but features a universal quantification which is
not in the spirit of incorrectness logic.```
• prove Robbert's triple for the sequence · 1fb838b9
Edoardo Putti authored
```this rule does not reference the value that gets discarded during
the execution of the sequential program so it's nice to have around.```
• adds the hoare context rule taken from Iris · 0026adfe
Edoardo Putti authored
```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.```
• add both versions of the hoare sequence rule · a28e3f49
Edoardo Putti authored
```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

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.```
7. 08 Jun, 2021 3 commits
• update seq rule with a more general statement · 9735757c
Edoardo Putti authored
```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.```
• add a primitive rule for the wand · 2b457482
Edoardo Putti authored
```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.```
• draft for CoqProject file · 4ee79380
Edoardo Putti authored
8. 31 May, 2021 4 commits
9. 21 May, 2021 2 commits
10. 15 Apr, 2021 1 commit
11. 15 Mar, 2021 3 commits
12. 12 Mar, 2021 3 commits
• add the trivial hoare triple rules · d1ce44c2
Edoardo Putti authored
• refactor proof rules and use them to prove examples · 27638c50
Edoardo Putti authored
```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```
• prove alloc rule · c99f9661
Edoardo Putti authored
13. 08 Mar, 2021 4 commits
• draft for example from paper · d62f3ce7
Edoardo Putti authored
```now that we have the hoare triples for the incorrectness logic
it is time to see if they are any good```
• finish proving hoare rules · e2a29f6a
Edoardo Putti authored
```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.```
• try to use our proof rules · 2196ab89
Edoardo Putti authored
• comment out all the previous examples · c1836288
Edoardo Putti authored
```I am getting some strange errors from Coq and I'm not sure
what is happening. I'll discuss this with Jules```