From 2f7d7bde830e0dfdefca13212891c35a8f7bb1f8 Mon Sep 17 00:00:00 2001
From: Dan Frumin
Date: Tue, 4 Jul 2017 14:35:51 +0200
Subject: [PATCH] Add the comments.org file
In this file I will keep all the comments regarding different aspects
of formalisation.
---
comments.org | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 56 insertions(+)
create mode 100644 comments.org
diff --git a/comments.org b/comments.org
new file mode 100644
index 0000000..8983079
--- /dev/null
+++ b/comments.org
@@ -0,0 +1,56 @@
+* 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.
+
--
GitLab