* Rules that didn't make it
** A binding rule for the semantic judgment that /nearly/ works.
A rule that we would like to have
#+BEGIN_SRC 
WP e {{ v, {E,E;Γ} ⊧ K[v] ≤ e₂ : τ }}
-----------------------------------------
{E,E;Γ} ⊧ K[e₁] ≤ e₂ : τ
#+END_SRC
However, this rule is too weak. Consider a derivation where =e₁= is
atomic and we want to open an invariant to symbolically execute it.
#+BEGIN_SRC 
|={E1,E2}=> WP e {{ v, |={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }}
---------------------------------------------------------------- wp-atomic
WP e {{ v, {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ }}_E1
-----------------------------------------
{E1,E1;Γ} ⊧ K[e₁] ≤ e₂ : τ
#+END_SRC
After employing such reasoning we can open up an invariant, and
symbolically execute =e₁=. But then we are left with
#+BEGIN_SRC 
|={E2,E1}=> {E1,E1;Γ} ⊧ K[v] ≤ e₂ : τ
#+END_SRC
which means that we have to close the invariant *now*. However, it
might be the case that we need to symbolically execute =e₂= in order
to restore the invariant before closing it.
* Assorted
** Logically atomic rules for the relatoinal interpretation
<2017-07-10 ma>
Consider the following rule for the left hand side for some function `inc`:
#+BEGIN_SRC 
x ↦ᵢ n+1 ⊢ {E,E;Γ} ⊧ K[()] ≤ t : τ
----------------------------------------
x ↦ᵢ n ⊢ {E,E;Γ} ⊧ K[inc #x ()] ≤ t : τ
#+END_SRC
For a definition of =inc= in F_mu_ref_conc we can prove this rule
using basic inductive rules for the left hand side. However, we may
encounter the same issue as with Hoare triples: this rule is unusable
in situations when `x ↦ n` is in the invariant. The program =inc= is
not actually atomic, so we cannot open the invariant around it.
However, it is /logically/ atomic, i.e. it behaves "as if" it is physically
atomic.

We may want to write the aforementioned rule in a different style:
#+BEGIN_SRC 
  Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ  :
    □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
       ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
        (∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗ 
            {E2,E1;Γ} ⊨ fill K (Lit Unit) ≤log≤ t : τ))
    -∗ ({E1,E1;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ).
#+END_SRC
To use this rule, we need to provide, possibly under an invariant (by
  opening invariants in E1)
- a way of obtaining =x ↦ᵢ n= and a "frame" =R(n)=;
- a way of "reversing" the rule in case of failure;
- a way of "finishing up" the rule in case of success;
where the two last points do not have to be provided simultaneously.
*** Some references on logical atomicity
- Triples for logical atomicity have originally been introduced in the following paper:

  TaDA: A Logic for Time and Data Abstraction
  Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner
  ECOOP'2014

  http://www.doc.ic.ac.uk/~pmd09/research/publications/2014/ecoop/tada-a-logic-for-time-and-data-abstraction

- In the original Iris 1.0 paper, it has been shown how atomic triples can be encoded in Iris (using view shifts, and higher-order quantification).

- Zhen Zhang, a former intern of Derek Dreyer, has made some progress at formalizing logical atomicity in Coq. His results can be found here:

  https://gitlab.mpi-sws.org/FP/iris-atomic

  He improved the definition of the logical atomic triple somewhat.
  The relevant files to look at are: atomic.v, the definition of
  logical atomic triples, atomic_incr.v, a proof for a simple atomic
  incrementer, and treiber.v for Treiber stack.

** Why do we need the expressions to be closed everywhere?
<2017-07-10 ma>

(For many lemmas in [[file:F_mu_ref_conc/relational_properties.v]]
This is not a very serious restriction, as the "real" programs are always closed,
and you shouldn't attempt symbolic execution of open expressions.

For =wp_lift_pure_det_head_step_no_fork= you have to prove that your
expression is not a value -- this is no longer true if you have open
expressions. If you have =x=, then closing it up by an env
substitution will yield a value.
** Why do we have a single =bin_log_related_cas_l=?
=bin_log_related_cas_l= is a rule in [[file:F_mu_ref_conc/relational_properties.v]]

We already have =bin_log_related_cas_suc_l= and
=bin_log_related_cas_fail_l=. However, those rules are not sufficient
for our purposes, as we might not know whether the CAS succeeds
/before/ we open the invariant.

Example: proof of =bin_log_FG_increment_logatomic= in counter.v
** subst_p_rec with binders
#+BEGIN_SRC 
  Lemma subst_p_rec (x f : binder) e1 e2 e `{Closed ∅ e2} :
    subst_p (<[x:=e2]>{[f:=(Rec f x e1)]}) e =
    subst' f (Rec f x e1) (subst' x e2 e).
#+END_SRC
We need a version of this lemma with x and f binders
in order to prove the compatibility lemma for lambdas

#+BEGIN_SRC 
□ (<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ) ⊨ e ≤log≤ e' : τ2) -∗
Γ ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2.
#+END_SRC

To show tht (rec f x e, rec f x e') are related, we use the definition
of the arrow type, so we have some values (v, v') related at τ1. Then
we would like to use the hypothesis by inserting (v, v') in the
environment substitution. But then we have =subst_p (<[x:=(v,v')]>
...) e=. You would like to convert that to =subst' x ..= so that one
can actually use the hypothesis.

* Comments on the design
** Common setting for different symbolic execution tactics
There are multiple layers of tactics for symbolic execution in the code.
*** Layers of tactics
We have symbolic execution rules (either as lemmas or as tactics and tactic lemmas) for
- WP calculus
- Symbolic execution in the ghost threadpool
- Symbolic execution in the relational interpretation
*** Tactics and tactic lemmas
Here we make a distinction between an actual /tactic/ and a /tacic lemma/.
A /tactic lemma/ is a lemma in Coq that is a Coq proposition that is saying more than a certain ~iProp~ holds.
Hence, the tacic lemma is typechecked. A /tactic/ is an actual piece of Ltac code that makes it more convenient to apply the aforementioned lemma.
For instance, this is a tactic lemma for symbolically executing a ~Load~ in the ghost threadpool.
#+BEGIN_SRC coq
Lemma tac_tp_load `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l v Q q :
  nclose specN ⊆ E1 →
  envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
  envs_lookup_delete i2 Δ1 = Some (false, j ⤇ e, Δ2)%I →
  e = fill K' (Load (Loc l)) →
  envs_lookup i3 Δ2 = Some (false, l ↦ₛ{q} v)%I →
  envs_simple_replace i3 false 
    (Esnoc (Esnoc Enil i2 (j ⤇ fill K' (of_val v))) i3 (l ↦ₛ{q} v)%I) Δ2 = Some Δ3 →
  (Δ3 ⊢ |={E1,E2}=> Q) →
  (Δ1 ⊢ |={E1,E2}=> Q).
#+END_SRC
It takes care of managing the context in a typesafe way.
Then this lemma is actually applied with the help of the following tactic
#+BEGIN_SRC coq
Tactic Notation "tp_load" constr(j) :=
  iStartProof;
  eapply (tac_tp_load j);
    [solve_ndisj || fail "tp_load: cannot prove 'nclose specN ⊆ ?'"
    |iAssumptionCore || fail "tp_load: cannot find spec_ctx" (* spec_ctx *)
    |iAssumptionCore || fail "tp_load: cannot find '" j " ⤇ ?'" 
    |tp_bind_helper
    |iAssumptionCore || fail "tp_load: cannot find '? ↦ₛ ?'"
    |env_cbv; reflexivity || fail "tp_load: this should not happen"
    |(* new goal *)].
#+END_SRC
The tactic itself provides error messages as well as some means of discharging the assumptions for the tactic lemma.
Since the tactic lemma is being ~eapply~ed, it is always important to think about the order we put the assumptions in the lemma.
At the moment we apply the lemma Coq's unification mechanism instantiates ~Δ1~, ~E1~, ~E2~, and ~Q~.
We need to make sure that by discharging the assumptions in the correct order we can instantiate ~Δ3~ to something meaningful.
For instance, the fourth assumption says something about the shape of the expression that is executed in thread ~j~; however, this expression is not known until we lookup it up in the context.
Hence, the fourth assumption should come *after* the third one.
Likewise, the fifth assumption says that there is a resource ~l ↦ₛ v~ in context ~Δ2~, but we only know the location ~l~ once we decompose the expression ~e~ into an evaluation context and a load expression.
Thus, this assumption should come after ~e = fill K'(Load (Loc l))~.
*** Pure reductions
Since ultimately all the levels of the symbolic executions operate on the same language we can share some machinery between the levels.
One observation is that the easiest (as well as the most numerous) tactics to write are those that preform symbolic execution of pure reductions.
To that extent we would like to have one generic "pure symbolic reduction" tactic/tactic lemma per level.
This is achieved by writing "open ended" tactic lemmas that are parameterized  over a typeclass of pure reductions.
The typeclass ~PureExec φ e1 e2~ says that there is a pure (and deterministic) reduction from ~e1~ to ~e2~ in the language under some (pure) assumption φ.
Using this typeclass and typeclass resolution we can write tactic lemmas that are easy to apply:
#+BEGIN_SRC
Lemma tac_rel_pure_r `{logrelG Σ} K e1 ℶ E1 E2 Δ Γ e e2 eres ϕ t τ :
  e = fill K e1 →
  PureExec ϕ e1 e2 →
  ϕ →
  nclose specN ⊆ E1 →
  eres = fill K e2 →
  (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ (fill K e2) : τ) →
  (ℶ ⊢ {E1,E2;Δ;Γ} t ≤log≤ e : τ).
#+END_SRC
When ~tac_rel_pure~ is applied, it tries to solve the first goal ~e = fill K e1~ by decomposing expression ~e~ in all the possible ways
and trying to unify it with ~e1~. After that it searches for an appropriate ~PureExec~ instance.
The whole process is implemented in the following tactic
#+BEGIN_SRC
Tactic Notation "rel_pure_r" open_constr(ef) :=
  iStartProof;
  rel_reshape_cont_r ltac:(fun K e' =>
      unify e' ef;
      simple eapply (tac_rel_pure_r K e');
      [tac_bind_helper             (* e = fill K e1 *)
      |apply _                     (* PureExec ϕ e1 e2 *)
      |try (exact I || reflexivity || tac_rel_done)  (* φ *)
      |solve_ndisj                 (* ↑specN ⊆ E1 *)
      |simpl; reflexivity          (* eres = fill K e2 *)
      |simpl_subst/=               (* new goal *)])
  || fail "rel_pure_r: cannot find the reduct".
#+END_SRC
Ignoring the "fail" part, we can see from the outline what is going on in the tactic:
- It tries to reshape the expression on the right hand side in the relational interpretation, until the tactic succeeds.
- It only proceeds with the specific decomposition if ~e = K[e']~ and ~e'~ unifies with ~ef~.
- After that, it applies the tactic lemma and tries to discharge the proof obligations in order
- Sometimes, the dependency ~φ~ in ~PureExec φ e1 e2~ can be discharged trivially by ~reflexivity~ or ~tac_rel_done~.
- We simplify the substitutions in the new goal, in case we do a beta-reduction