Commit 2f7d7bde authored by Dan Frumin's avatar Dan Frumin

Add the comments.org file

In this file I will keep all the comments regarding different aspects
of formalisation.
parent 2b8c7d91
* 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
** 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment