coqdoc for safety.v

theories/safety.v

 From iris.heap_lang Require Export adequacy.
 From tutorial_popl20 Require Export fundamental.
 
+(** * Safety of semantic types and type safety based on that
+
+    We prove that any _closed_ expression that is semantically typed
+    is safe, i.e., it does not crash. Based on this theorem we then
+    prove _type safety_, i.e., any _closed_ syntactically well-typed
+    program does not get stuck. Type safety is a simple consequence of
+    the fundamental theorem of logical relations together with the
+    safety for semantic typing.
+*)
+
+
+(** The following lemma states that given a closed program [e], heap
+    [σ], and _Coq_ predicate [φ : val → Prop], if there is a semantic
+    type [A] such that [A] implies [φ], and [e] is semantically typed
+    at type [A], then we have [adequate NotStuck e σ (λ v σ, φ
+    v)]. The proposition [adequate NotStuck e σ (λ v σ, φ v)] means
+    that [e], starting in heap [σ] does not get stuck, and if [e]
+    reduces to a value [v], we have [φ v]. *)
 Lemma sem_gen_type_safety `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, ∃ A : sem_ty Σ, (∀ v, A v -∗ ⌜φ v⌝) ∧ (∅ ⊨ e : A)) →
   adequate NotStuck e σ (λ v σ, φ v).
@@ -13,6 +31,9 @@ Proof.
   by iIntros; iApply HA.
 Qed.
 
+(** This lemma states that semantically typed closed programs do not
+get stuck. It is a simple consequence of the lemma
+[sem_gen_type_safety] above. *)
 Lemma sem_type_safety `{heapPreG Σ} e σ es σ' e' :
   (∀ `{heapG Σ}, ∃ A, ∅ ⊨ e : A) →
   rtc erased_step ([e], σ) (es, σ') → e' ∈ es →