Added more comments to the sum-example

Author: Louis Cheung

cogent/examples/cpp2022-artefact/README.md

@@ -1,6 +1,6 @@
 # ARTEFACT
 ---
-This is an artefact for "Overcoming Restraint: Composing Verification of Foreign Functions with Cogent"
+This is an artefact for "Overcoming Restraint: Composing Verification of Foreign Functions with Cogent" ([published](https://doi.org/10.1145/3497775.3503686))
 
 This formalisation works with [Isabelle2019](https://isabelle.in.tum.de/website-Isabelle2019/index.html),
 [AutoCorres version 1.6.1](https://trustworthy.systems/projects/TS/autocorres/) and
@@ -10,6 +10,9 @@ The work that is being presented are all the files in **loops**, **sum-example**
 
 Note that for MacOS users, some of the make files depend on the GNU version of **sed**, i.e. **gsed** on MacOS.
 
+The top level make file only generates the C code and theory files for the loop and sum example.
+This is just to keep the GitHub build happy.
+
 ## Install Isabelle2019
 
 Follow the instructions for installing.
@@ -27,6 +30,11 @@ Set the environment variable **COGENT_DIR** to be the top level directory of Cog
 
 ## Sum Example
 
+The sum example was the first completed attempt at composing verification of foreign functions and abstract types with Cogent functions and types.
+This is the reason why some of the approaches and proofs have not been optimised,
+the word arrays in this example can only contain primitive numeric types,
+and that the update to C refinement is only for 32-bit word arrays.
+
 ### Important Files
 
 * _Sum.cogent_: Contains the Cogent program for sum and other functions.
@@ -65,6 +73,14 @@ To run the example, go into the **sum-example** folder and use the command:
 
 ## Loops Example
 
+The loops example drew from the lessons learnt from the sum example, and hence is much more polished, reusable,
+and resilient to changes made to the Cogent program.
+Some notable differences are:
+
+* The value typing relation for arrays is defined for all non-heap element types.
+* The update to C refinement proof for the word array operations and generalise loop occurs on a polymorphic monadic Isabelle shallow embeddings.
+This means that it does not need to undergo alpha renaming when used by other Cogent programs.
+
 ### Important Files
 
 * _repeat.cogent_: Cogent declarations for the higher order polymorphic loop.

cogent/examples/cpp2022-artefact/sum-example/WordArray_Abstractions.thy

@@ -163,6 +163,7 @@ locale WordArray = main_pp_inferred begin
       UWA (TPrim (Num t)) _ _ \<Rightarrow> (''WordArray'', [RPrim (Num t)])
     | _ \<Rightarrow> (''Unknown Abstract Type'', [])"
 
+  text "Definition 3.2"
   definition "wa_abs_typing_u \<Xi>' a name \<tau>s sig (r :: ptrtyp set) (w :: ptrtyp set) \<sigma> \<equiv>
     (case a of
       UWA (TPrim (Num t)) len arr \<Rightarrow> name = ''WordArray'' \<and> \<tau>s = [TPrim (Num t)] \<and> sig \<noteq> Unboxed \<and>
@@ -174,12 +175,14 @@ locale WordArray = main_pp_inferred begin
                       unat (size_of_num_type t)  * unat len \<le> unat (max_word :: ptrtyp)
     | _ \<Rightarrow> name = ''Unknown Abstract Type'' \<and> \<tau>s = [] \<and> r = {} \<and> w = {} \<and> sig = Unboxed)"
 
+  text "Definition 3.1"
   definition "wa_abs_typing_v \<Xi>' a name \<tau>s \<equiv>
     (case a of
       VWA (TPrim (Num t)) xs \<Rightarrow> name = ''WordArray'' \<and> \<tau>s = [TPrim (Num t)] \<and> 
       (\<forall>i < length xs. \<exists>x. xs ! i = VPrim x \<and>  lit_type x = Num t)
     | _ \<Rightarrow> name = ''Unknown Abstract Type'' \<and> \<tau>s = [])"
 
+  text "Definition 3.5"
   definition  "wa_abs_upd_val \<Xi>' au av name \<tau>s sig (r :: ptrtyp set) (w :: ptrtyp set) \<sigma> \<equiv>
     wa_abs_typing_u \<Xi>' au name \<tau>s sig r w \<sigma> \<and> wa_abs_typing_v \<Xi>' av name \<tau>s \<and>
     (case au of
@@ -271,6 +274,8 @@ end
 
 section "Sublocale Proof"
 
+text "Discharging the abstract type requirements (Definition 2.12)"
+
 sublocale WordArray \<subseteq> update_sem wa_abs_typing_u wa_abs_repr
   apply (unfold wa_abs_repr_def[abs_def] wa_abs_typing_v_def[abs_def] wa_abs_typing_u_def[abs_def] wa_abs_upd_val_def[abs_def])
   apply (unfold_locales; clarsimp split: atyp.splits type.splits prim_type.splits)

cogent/examples/cpp2022-artefact/sum-example/WordArray_CorresProof_Asm.thy

@@ -6,7 +6,7 @@ theory WordArray_SVCorres
   imports WordArray_Shallow WordArray_VAbsFun
 begin
 
-subsection "Shallow Word Array Value Relation"
+subsection "Shallow Word Array Value Relation (Definition 3.4)"
 text 
   "The shallow embedding of a word array is a list of words. Currently we only support word
    arrays with primitive words as values. In the future, we hope to extend this to elements which
@@ -69,7 +69,7 @@ end
 context WordArray begin
 
 
-section "Shallow to Deep Corresondence Lemmas (@{term scorres}) for Word Array Functions"
+section "Shallow to Deep Corresondence Lemmas (@{term scorres}) for Word Array Functions (Theorem 2.9)"
 
 lemmas valRel_WordArray_simps = valRel_WordArrayUX
 

cogent/examples/cpp2022-artefact/sum-example/WordArray_SVCorres.thy

@@ -9,7 +9,7 @@ fun myslice :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a lis
   where
 "myslice frm to xs = List.take (to - frm) (List.drop frm xs)"
 
-section "Shallow Word Array Function Definitions"
+section "Shallow Word Array Function Definitions (Figure 4)"
 
 overloading
   wordarray_put2' \<equiv> wordarray_put2

cogent/examples/cpp2022-artefact/sum-example/WordArray_Shallow.thy

@@ -5,6 +5,8 @@ theory WordArray_UpdCCorres
   imports WordArray_UAbsFun
 begin
 
+section "Helper definition and lemmas"
+
 context update_sem_init begin
 
 definition
@@ -56,8 +58,9 @@ sublocale WordArray \<subseteq> Generated _ wa_abs_typing_u wa_abs_repr
 
 context WordArray begin
 
-section "Correspondence Lemmas Between Update Semantics and C"
+section "Refinement from  Update Semantics and C (Theorem 2.4)"
 
+(* Theorem 3.6 *)
 lemma upd_C_wordarray_put2_corres_gen:
   "\<And>i \<gamma> v' \<Gamma>' \<sigma> st.
     \<lbrakk>i < length \<gamma>; val_rel (\<gamma> ! i) v'; \<Gamma>' ! i = option.Some (prod.fst (prod.snd (\<Xi> ''wordarray_put2_0'')));

cogent/examples/cpp2022-artefact/sum-example/WordArray_UpdCCorres.thy

@@ -3,6 +3,8 @@ theory WordArray_Update
 
 begin
 
+section "Word array method embeddings (Figure 6a)"
+
 type_synonym ('f, 'a, 'l) ufoldmapdef = "('f, 'a, 'l) uabsfuns \<Rightarrow> ('f, 'a, 'l) store \<Rightarrow>
                                           'l \<Rightarrow> 32 word \<Rightarrow> 32 word \<Rightarrow> 'f expr \<Rightarrow> 
                                           type \<Rightarrow> ('f, 'a, 'l) uval \<Rightarrow> type \<Rightarrow> ('f, 'a, 'l) uval \<Rightarrow>
@@ -113,6 +115,8 @@ definition upd_wa_mapAccumnb
         (\<Xi>', [], [option.Some \<tau>i] \<turnstile> (App (uvalfun_to_exprfun func) (Var 0)) : \<tau>o) \<and> 
         upd_wa_mapAccumnb_bod \<xi>\<^sub>u y1 p frm to (uvalfun_to_exprfun func) u acc v obsv z))"
 
+section "Helper lemmas"
+
 context update_sem begin
 lemma discardable_or_shareable_not_writable:
 assumes "D \<in> k \<or> S \<in> k"
@@ -143,13 +147,13 @@ and     "u  \<inter> r = {} \<Longrightarrow> r \<inter> u' = {}"
            simp: frame_def
            dest: abs_typing_valid)
 
-
 end (* of context *)
 
+section "Type preservation and frame relation theorems (Theorem 2.2)"
 
 context WordArray begin
 
-section wordarray_length
+subsection wordarray_length
 
 lemma upd_wa_length_preservation:
   "\<lbrakk>uval_typing \<Xi>' \<sigma> v (TCon ''WordArray'' [t] (Boxed ReadOnly ptrl)) r w;
@@ -161,7 +165,7 @@ lemma upd_wa_length_preservation:
   apply (clarsimp simp: frame_def intro!: u_t_prim')
   done
 
-section wordarray_get
+subsection wordarray_get
 
 lemma upd_wa_get_preservation:
   "\<lbrakk>uval_typing \<Xi>' \<sigma> v (TRecord [(a, TCon ''WordArray'' [t] (Boxed ReadOnly ptrl), Present),
@@ -188,7 +192,7 @@ lemma upd_wa_get_preservation:
   apply (case_tac ta; clarsimp intro!: u_t_prim')
   done
 
-section wordarray_put2
+subsection wordarray_put2
 
 lemma upd_wa_put2_preservation:
   "\<lbrakk>uval_typing \<Xi>' \<sigma> v (TRecord [(a, TCon ''WordArray'' [t] (Boxed Writable ptrl), Present),
@@ -237,7 +241,7 @@ lemma upd_wa_put2_preservation:
   apply (rule conjI; clarsimp)
   done
 
-section wordarray_fold_no_break
+subsection wordarray_fold_no_break
 
 lemma upd_wa_foldnb_bod_to_geq_len:
   "\<lbrakk> proc_ctx_wellformed \<Xi>';
@@ -736,7 +740,7 @@ lemma upd_wa_foldnb_bod_preservation:
   apply (rule frame_trans; simp)
   done
 
-section wordarray_map_no_break
+subsection wordarray_map_no_break
 
 lemma upd_wa_mapAccumnb_bod_to_geq_len:
   "\<lbrakk> proc_ctx_wellformed \<Xi>';