From 71e21504120aeaafa08b6f1018a086b4f19b0c89 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Tue, 28 May 2024 13:22:23 -0400
Subject: [PATCH 01/29] Add README with how to build coq lemmas

---
 src/example-archive/coq-lemmas/README.md | 67 ++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 src/example-archive/coq-lemmas/README.md

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
new file mode 100644
index 00000000..d5169dfe
--- /dev/null
+++ b/src/example-archive/coq-lemmas/README.md
@@ -0,0 +1,67 @@
+## Examples
+
+CN examples using lemmas that can be extracted to Coq. The examples are split into:
+
+- Trivial
+- Lists
+- Recursive
+- Advanced
+
+## Generating Coq Lemmas 
+
+To generate Coq lemma for a given `example-file.c` run
+
+```
+cn --lemmata=build/theories/ExportedLemmas.v example-file.c
+```
+
+File `build/theories/ExportedLemmas.v` should be generated with the
+right definitions. Each lemma is exported as a new definition and then
+added as a parameter in the module named `Lemma_Spec`. It should look
+something like this
+
+```
+
+Module Defs (P : Parameters).
+
+  Import Types P.
+  Open Scope Z.
+
+
+  Definition my_lemma_type : Prop :=
+    Is_true true.
+
+End Defs.
+
+
+Module Type Lemma_Spec (P : Parameters).
+
+  Module D := Defs(P).
+  Import D.
+
+  Parameter my_lemma : my_lemma_type.
+
+End Lemma_Spec.
+```
+
+## Prooving the Coq Lemmas
+
+To prove the lemmas, instantiate a new module with type `Lemma_Spec` containing each of parameters as lemmas and their proofs. For the example above, the proofs look like this
+
+```
+
+Module MyP: Parameters.
+End MyP.
+
+Module Proofs : Lemma_Spec MyP.
+  Module D := Defs(MyP).
+  Import D.
+
+  Lemma  just_arith2 : my_lemma_type.
+  Proof.
+    solve [hnf; trivial].
+  Qed.
+
+End Proofs.
+  
+```

From f67c2c08f7310a3038437e4d2f92b8106f1bd977 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Tue, 28 May 2024 13:23:46 -0400
Subject: [PATCH 02/29] Add examples

---
 .../coq-lemmas/inprogress/trivial-002.c       | 10 ++++++++++
 .../coq-lemmas/inprogress/trivial-003.c       | 10 ++++++++++
 .../coq-lemmas/inprogress/trivial-004.c       | 10 ++++++++++
 .../coq-lemmas/inprogress/trivial-005.c       | 10 ++++++++++
 .../coq-lemmas/inprogress/trivial-006.c       | 10 ++++++++++
 .../coq-lemmas/inprogress/trivial-007.c       | 19 +++++++++++++++++++
 .../coq-lemmas/inprogress/trivial-008.c       | 11 +++++++++++
 .../coq-lemmas/working/trivial-001.c          | 10 ++++++++++
 8 files changed, 90 insertions(+)
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-002.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-003.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-004.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-005.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-006.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-007.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-008.c
 create mode 100644 src/example-archive/coq-lemmas/working/trivial-001.c

diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-002.c b/src/example-archive/coq-lemmas/inprogress/trivial-002.c
new file mode 100644
index 00000000..0d2cc978
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-002.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_impossible_in_coq (u32 x)
+  requires true;
+  ensures x <= 4294967295u32; 
+@*/
+
+void nothing() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-003.c b/src/example-archive/coq-lemmas/inprogress/trivial-003.c
new file mode 100644
index 00000000..4716d24d
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-003.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_ineq (u32 x, u32 y)
+  requires x > 0u32; y > 0u32;
+  ensures x > 0u32; y > 0u32;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-004.c b/src/example-archive/coq-lemmas/inprogress/trivial-004.c
new file mode 100644
index 00000000..51c47e76
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-004.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_impossible_in_Coq (u32 x)
+  requires true;
+  ensures (x + 1u32) - 1u32  == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-005.c b/src/example-archive/coq-lemmas/inprogress/trivial-005.c
new file mode 100644
index 00000000..13ce2e09
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-005.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_and (u32 x)
+  requires true;
+  ensures x & x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-006.c b/src/example-archive/coq-lemmas/inprogress/trivial-006.c
new file mode 100644
index 00000000..d07ffbc2
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-006.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_or (u32 x)
+  requires true;
+  ensures x | x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-007.c b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
new file mode 100644
index 00000000..d2f8cea1
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
@@ -0,0 +1,19 @@
+#include <stdbool.h>
+/*@
+  predicate (bool) MyCondition (u32 x){
+    if (x > 4294967295u32){
+      return false;
+    } else {
+      return true; 
+    }
+  } 
+  
+  lemma lem_bit_wise_or (u32 x)
+  requires MyCondition(x) == true;
+  ensures true;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-008.c b/src/example-archive/coq-lemmas/inprogress/trivial-008.c
new file mode 100644
index 00000000..423311ff
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-008.c
@@ -0,0 +1,11 @@
+#include <stdbool.h>
+/*@
+  lemma my_lemma ()
+  requires true;
+  ensures true;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/working/trivial-001.c b/src/example-archive/coq-lemmas/working/trivial-001.c
new file mode 100644
index 00000000..529f1dbe
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/trivial-001.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_trivial ()
+  requires true;
+  ensures true; 
+@*/
+
+void lemma_1() 
+{
+  ; 
+}

From 269f916c9d080cf5817172b771109e6d72fce9f3 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Tue, 28 May 2024 13:25:14 -0400
Subject: [PATCH 03/29] Add build files

---
 src/example-archive/coq-lemmas/build/Makefile |  8 ++++
 .../coq-lemmas/build/_CoqProject              |  7 +++
 .../coq-lemmas/build/theories/CN_Lib.v        | 29 +++++++++++++
 .../build/theories/ExportedLemmas.v           | 43 +++++++++++++++++++
 .../coq-lemmas/build/theories/Gen_Spec.v      | 43 +++++++++++++++++++
 5 files changed, 130 insertions(+)
 create mode 100644 src/example-archive/coq-lemmas/build/Makefile
 create mode 100644 src/example-archive/coq-lemmas/build/_CoqProject
 create mode 100644 src/example-archive/coq-lemmas/build/theories/CN_Lib.v
 create mode 100644 src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
 create mode 100644 src/example-archive/coq-lemmas/build/theories/Gen_Spec.v

diff --git a/src/example-archive/coq-lemmas/build/Makefile b/src/example-archive/coq-lemmas/build/Makefile
new file mode 100644
index 00000000..819ea988
--- /dev/null
+++ b/src/example-archive/coq-lemmas/build/Makefile
@@ -0,0 +1,8 @@
+
+
+
+all:
+	coq_makefile -f _CoqProject -o Makefile.coq
+	cn ../../SantiagosExamples/trivial-lemma.c --lemmata theories/Gen_Spec.v
+	make -f Makefile.coq
+
diff --git a/src/example-archive/coq-lemmas/build/_CoqProject b/src/example-archive/coq-lemmas/build/_CoqProject
new file mode 100644
index 00000000..917968e6
--- /dev/null
+++ b/src/example-archive/coq-lemmas/build/_CoqProject
@@ -0,0 +1,7 @@
+
+-Q theories CN_Lemmas
+
+theories/CN_Lib.v
+theories/ExportedLemmas.v
+
+
diff --git a/src/example-archive/coq-lemmas/build/theories/CN_Lib.v b/src/example-archive/coq-lemmas/build/theories/CN_Lib.v
new file mode 100644
index 00000000..e17d738a
--- /dev/null
+++ b/src/example-archive/coq-lemmas/build/theories/CN_Lib.v
@@ -0,0 +1,29 @@
+Require List.
+Require Import ZArith Bool.
+Require Import Lia.
+Require NArith.
+
+Definition wrapI (minInt : Z) (maxInt : Z) x :=
+  let delta := ((maxInt - minInt) + 1)%Z in
+  let r := Z.modulo x delta in
+  (if (r <=? maxInt) then r else r - delta)%Z.
+
+Lemma wrapI_idem:
+  forall (minInt maxInt x : Z),
+  (minInt <= x <= maxInt)%Z ->
+  (minInt <= 0 < maxInt)%Z ->
+  wrapI minInt maxInt x = x.
+Proof.
+  Open Scope Z.
+  intros.
+  unfold wrapI.
+  pose (delta := ((maxInt - minInt) + 1)).
+  destruct (0 <=? x) eqn: x_neg.
+  - rewrite Z.mod_small by lia.
+    rewrite Zle_imp_le_bool by lia.
+    reflexivity.
+  - rewrite (Znumtheory.Zdivide_mod_minus _ _ (x + delta)).
+    + destruct (x + delta <=? maxInt) eqn: leb; lia.
+    + lia.
+    + exists (-1); lia.
+Qed.
diff --git a/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v b/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
new file mode 100644
index 00000000..ffe0f0be
--- /dev/null
+++ b/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
@@ -0,0 +1,43 @@
+(* build/theories/ExportedLemmas.v: generated lemma specifications from CN *)
+
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+
+
+Module Types.
+
+  (* no type definitions required *)
+
+End Types.
+
+
+Module Type Parameters.
+  Import Types.
+
+  (* no parameters required *)
+
+End Parameters.
+
+
+Module Defs (P : Parameters).
+
+  Import Types P.
+  Open Scope Z.
+
+
+  Definition my_lemma_type : Prop :=
+    Is_true true.
+
+End Defs.
+
+
+Module Type Lemma_Spec (P : Parameters).
+
+  Module D := Defs(P).
+  Import D.
+
+  Parameter my_lemma : my_lemma_type.
+
+End Lemma_Spec.
+
+
diff --git a/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v b/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v
new file mode 100644
index 00000000..7254a094
--- /dev/null
+++ b/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v
@@ -0,0 +1,43 @@
+(* theories/Gen_Spec.v: generated lemma specifications from CN *)
+
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+
+
+Module Types.
+
+  (* no type definitions required *)
+
+End Types.
+
+
+Module Type Parameters.
+  Import Types.
+
+  (* no parameters required *)
+
+End Parameters.
+
+
+Module Defs (P : Parameters).
+
+  Import Types P.
+  Open Scope Z.
+
+
+  Definition lem_trivial_type : Prop :=
+    Is_true true.
+
+End Defs.
+
+
+Module Type Lemma_Spec (P : Parameters).
+
+  Module D := Defs(P).
+  Import D.
+
+  Parameter lem_trivial : lem_trivial_type.
+
+End Lemma_Spec.
+
+

From c1f94ef883e19be2f9cb2c3125764ed4601549ac Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Mon, 10 Jun 2024 13:41:49 -0400
Subject: [PATCH 04/29] Add and reorder examples

---
 src/example-archive/coq-lemmas/README.md      |  2 +-
 .../error-cerberus}/trivial-005.c             |  0
 .../error-cerberus}/trivial-006.c             |  0
 .../coq-lemmas/inprogress/recursive-001.c     | 85 +++++++++++++++++++
 .../coq-lemmas/inprogress/trivial-002.c       |  2 +-
 .../coq-lemmas/inprogress/trivial-003.c       | 10 ---
 .../coq-lemmas/inprogress/trivial-004.c       | 10 ---
 .../coq-lemmas/inprogress/trivial-007.c       |  5 +-
 8 files changed, 88 insertions(+), 26 deletions(-)
 rename src/example-archive/coq-lemmas/{inprogress => broken/error-cerberus}/trivial-005.c (100%)
 rename src/example-archive/coq-lemmas/{inprogress => broken/error-cerberus}/trivial-006.c (100%)
 create mode 100644 src/example-archive/coq-lemmas/inprogress/recursive-001.c
 delete mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-003.c
 delete mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-004.c

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index d5169dfe..535457ad 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -3,8 +3,8 @@
 CN examples using lemmas that can be extracted to Coq. The examples are split into:
 
 - Trivial
-- Lists
 - Recursive
+- Lists
 - Advanced
 
 ## Generating Coq Lemmas 
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-005.c b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c
similarity index 100%
rename from src/example-archive/coq-lemmas/inprogress/trivial-005.c
rename to src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-006.c b/src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c
similarity index 100%
rename from src/example-archive/coq-lemmas/inprogress/trivial-006.c
rename to src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c
diff --git a/src/example-archive/coq-lemmas/inprogress/recursive-001.c b/src/example-archive/coq-lemmas/inprogress/recursive-001.c
new file mode 100644
index 00000000..5f31a1f6
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/recursive-001.c
@@ -0,0 +1,85 @@
+#include <stdbool.h>
+/*@
+
+datatype a_list {
+  LsNil {},
+  LsCons {u32 i, a_list t}
+}
+
+@*/
+
+/* The predicates relating A/B trees to their C encoding. */
+
+enum {
+  NUM_NODES = 16,
+  LEN_LIMIT = (1 << 16),
+};
+
+struct node;
+
+typedef struct node * tree;
+
+struct node {
+  int v;
+  tree nodes[NUM_NODES];
+};
+
+/*@
+
+
+  
+datatype tree_arc {
+  Arc_End {},
+  Arc_Step {i32 i, datatype tree_arc tail}
+}
+
+datatype tree_node_option {
+  Node_None {},
+  Node {i32 v}
+}
+
+function (map<datatype tree_arc, datatype tree_node_option>) empty ()
+function (map<datatype tree_arc, datatype tree_node_option>) construct
+    (i32 v, map<i32, map<datatype tree_arc, datatype tree_node_option> > ts)
+
+function (map<i32, map<datatype tree_arc, datatype tree_node_option> >) default_ns ()
+
+predicate {map<datatype tree_arc, datatype tree_node_option> t,
+        i32 v, map<i32, map<datatype tree_arc, datatype tree_node_option> > ns}
+  Tree (pointer p)
+{
+  if (is_null(p)) {
+    return {t: (empty ()), v: 0i32, ns: default_ns ()};
+  }
+  else {
+    take V = Owned<int>(member_shift<node>(p,v));
+    let nodes_ptr = member_shift<node>(p,nodes);
+    take Ns = each (i32 i; (0i32 <= i) && (i < (num_nodes ())))
+      {Indirect_Tree(array_shift<tree>(nodes_ptr, i))};
+    let t = construct (V, Ns);
+    return {t: t, v: V, ns: Ns};
+  }
+}
+@*/
+
+
+/*
+
+  match ls {
+    LsNil {} =>
+      take value = Owned<struct a_node>(p);
+      assert (value[0] == 0);
+      assert (is_null(p+1));
+      return 0;
+    LsCons {u32 i, a_list tl} =>
+      take value = Owned<struct a_node>(p);
+      assert(value[0] == i);
+      assert (is_array(p+1, tl))
+      return i;
+      }
+  
+ */
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-002.c b/src/example-archive/coq-lemmas/inprogress/trivial-002.c
index 0d2cc978..bb6d2466 100644
--- a/src/example-archive/coq-lemmas/inprogress/trivial-002.c
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-002.c
@@ -1,7 +1,7 @@
 /*@
   lemma lem_impossible_in_coq (u32 x)
   requires true;
-  ensures x <= 4294967295u32; 
+  ensures x <= 2147483647u32; 
 @*/
 
 void nothing() 
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-003.c b/src/example-archive/coq-lemmas/inprogress/trivial-003.c
deleted file mode 100644
index 4716d24d..00000000
--- a/src/example-archive/coq-lemmas/inprogress/trivial-003.c
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-  lemma lem_ineq (u32 x, u32 y)
-  requires x > 0u32; y > 0u32;
-  ensures x > 0u32; y > 0u32;
-@*/
-
-void trivial() 
-{
-  ; 
-}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-004.c b/src/example-archive/coq-lemmas/inprogress/trivial-004.c
deleted file mode 100644
index 51c47e76..00000000
--- a/src/example-archive/coq-lemmas/inprogress/trivial-004.c
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-  lemma lem_impossible_in_Coq (u32 x)
-  requires true;
-  ensures (x + 1u32) - 1u32  == x;
-@*/
-
-void trivial() 
-{
-  ; 
-}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-007.c b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
index d2f8cea1..1752d92a 100644
--- a/src/example-archive/coq-lemmas/inprogress/trivial-007.c
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-007.c
@@ -7,10 +7,7 @@
       return true; 
     }
   } 
-  
-  lemma lem_bit_wise_or (u32 x)
-  requires MyCondition(x) == true;
-  ensures true;
+
 @*/
 
 void trivial() 

From 9d10f7ef2943a8672133b718d8415446f649fecc Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Mon, 10 Jun 2024 17:07:10 -0400
Subject: [PATCH 05/29] Add examples and ignore automatically generated files

---
 src/example-archive/coq-lemmas/.gitignore            |  7 +++++++
 src/example-archive/coq-lemmas/working/trivial-002.c | 10 ++++++++++
 src/example-archive/coq-lemmas/working/trivial-003.c | 10 ++++++++++
 src/example-archive/coq-lemmas/working/trivial-004.c | 10 ++++++++++
 4 files changed, 37 insertions(+)
 create mode 100644 src/example-archive/coq-lemmas/.gitignore
 create mode 100644 src/example-archive/coq-lemmas/working/trivial-002.c
 create mode 100644 src/example-archive/coq-lemmas/working/trivial-003.c
 create mode 100644 src/example-archive/coq-lemmas/working/trivial-004.c

diff --git a/src/example-archive/coq-lemmas/.gitignore b/src/example-archive/coq-lemmas/.gitignore
new file mode 100644
index 00000000..f1dd468a
--- /dev/null
+++ b/src/example-archive/coq-lemmas/.gitignore
@@ -0,0 +1,7 @@
+build/**/*.vo
+build/**/*.vos
+build/**/*.vok
+build/**/*.glob
+build/**/*.aux
+Makefile.coq
+Makefile.coq.conf
diff --git a/src/example-archive/coq-lemmas/working/trivial-002.c b/src/example-archive/coq-lemmas/working/trivial-002.c
new file mode 100644
index 00000000..0d2cc978
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/trivial-002.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_impossible_in_coq (u32 x)
+  requires true;
+  ensures x <= 4294967295u32; 
+@*/
+
+void nothing() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/working/trivial-003.c b/src/example-archive/coq-lemmas/working/trivial-003.c
new file mode 100644
index 00000000..4716d24d
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/trivial-003.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_ineq (u32 x, u32 y)
+  requires x > 0u32; y > 0u32;
+  ensures x > 0u32; y > 0u32;
+@*/
+
+void trivial() 
+{
+  ; 
+}
diff --git a/src/example-archive/coq-lemmas/working/trivial-004.c b/src/example-archive/coq-lemmas/working/trivial-004.c
new file mode 100644
index 00000000..51c47e76
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/trivial-004.c
@@ -0,0 +1,10 @@
+/*@
+  lemma lem_impossible_in_Coq (u32 x)
+  requires true;
+  ensures (x + 1u32) - 1u32  == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}

From e7268c4265be8ea606e7400ac18a7c5e5b1b3d01 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Mon, 10 Jun 2024 17:15:24 -0400
Subject: [PATCH 06/29] Ignore more automatic coq files

---
 src/example-archive/coq-lemmas/.gitignore | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/example-archive/coq-lemmas/.gitignore b/src/example-archive/coq-lemmas/.gitignore
index f1dd468a..5820fc02 100644
--- a/src/example-archive/coq-lemmas/.gitignore
+++ b/src/example-archive/coq-lemmas/.gitignore
@@ -5,3 +5,5 @@ build/**/*.glob
 build/**/*.aux
 Makefile.coq
 Makefile.coq.conf
+.Makefile.coq.d
+/build/.lia.cache
\ No newline at end of file

From 425b0682bf8bf0060fe8dba81d7d06e8c7ea5277 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 19 Jun 2024 14:30:16 -0400
Subject: [PATCH 07/29] adding examples

---
 .../build/theories/ExportedLemmas.v           | 37 --------
 .../coq-lemmas/inprogress/recursive-001.c     | 85 -------------------
 .../coq-lemmas/inprogress/trivial-002.c       | 10 ---
 .../coq-lemmas/inprogress/trivial-009.c       |  8 ++
 .../coq-lemmas/working/recursive-001.c        | 40 +++++++++
 .../coq-lemmas/working/recursive-002.c        | 56 ++++++++++++
 6 files changed, 104 insertions(+), 132 deletions(-)
 delete mode 100644 src/example-archive/coq-lemmas/inprogress/recursive-001.c
 delete mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-002.c
 create mode 100644 src/example-archive/coq-lemmas/inprogress/trivial-009.c
 create mode 100644 src/example-archive/coq-lemmas/working/recursive-001.c
 create mode 100644 src/example-archive/coq-lemmas/working/recursive-002.c

diff --git a/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v b/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
index ffe0f0be..e8fec956 100644
--- a/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
+++ b/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
@@ -4,40 +4,3 @@ Require Import ZArith Bool.
 Require CN_Lemmas.CN_Lib.
 
 
-Module Types.
-
-  (* no type definitions required *)
-
-End Types.
-
-
-Module Type Parameters.
-  Import Types.
-
-  (* no parameters required *)
-
-End Parameters.
-
-
-Module Defs (P : Parameters).
-
-  Import Types P.
-  Open Scope Z.
-
-
-  Definition my_lemma_type : Prop :=
-    Is_true true.
-
-End Defs.
-
-
-Module Type Lemma_Spec (P : Parameters).
-
-  Module D := Defs(P).
-  Import D.
-
-  Parameter my_lemma : my_lemma_type.
-
-End Lemma_Spec.
-
-
diff --git a/src/example-archive/coq-lemmas/inprogress/recursive-001.c b/src/example-archive/coq-lemmas/inprogress/recursive-001.c
deleted file mode 100644
index 5f31a1f6..00000000
--- a/src/example-archive/coq-lemmas/inprogress/recursive-001.c
+++ /dev/null
@@ -1,85 +0,0 @@
-#include <stdbool.h>
-/*@
-
-datatype a_list {
-  LsNil {},
-  LsCons {u32 i, a_list t}
-}
-
-@*/
-
-/* The predicates relating A/B trees to their C encoding. */
-
-enum {
-  NUM_NODES = 16,
-  LEN_LIMIT = (1 << 16),
-};
-
-struct node;
-
-typedef struct node * tree;
-
-struct node {
-  int v;
-  tree nodes[NUM_NODES];
-};
-
-/*@
-
-
-  
-datatype tree_arc {
-  Arc_End {},
-  Arc_Step {i32 i, datatype tree_arc tail}
-}
-
-datatype tree_node_option {
-  Node_None {},
-  Node {i32 v}
-}
-
-function (map<datatype tree_arc, datatype tree_node_option>) empty ()
-function (map<datatype tree_arc, datatype tree_node_option>) construct
-    (i32 v, map<i32, map<datatype tree_arc, datatype tree_node_option> > ts)
-
-function (map<i32, map<datatype tree_arc, datatype tree_node_option> >) default_ns ()
-
-predicate {map<datatype tree_arc, datatype tree_node_option> t,
-        i32 v, map<i32, map<datatype tree_arc, datatype tree_node_option> > ns}
-  Tree (pointer p)
-{
-  if (is_null(p)) {
-    return {t: (empty ()), v: 0i32, ns: default_ns ()};
-  }
-  else {
-    take V = Owned<int>(member_shift<node>(p,v));
-    let nodes_ptr = member_shift<node>(p,nodes);
-    take Ns = each (i32 i; (0i32 <= i) && (i < (num_nodes ())))
-      {Indirect_Tree(array_shift<tree>(nodes_ptr, i))};
-    let t = construct (V, Ns);
-    return {t: t, v: V, ns: Ns};
-  }
-}
-@*/
-
-
-/*
-
-  match ls {
-    LsNil {} =>
-      take value = Owned<struct a_node>(p);
-      assert (value[0] == 0);
-      assert (is_null(p+1));
-      return 0;
-    LsCons {u32 i, a_list tl} =>
-      take value = Owned<struct a_node>(p);
-      assert(value[0] == i);
-      assert (is_array(p+1, tl))
-      return i;
-      }
-  
- */
-void trivial() 
-{
-  ; 
-}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-002.c b/src/example-archive/coq-lemmas/inprogress/trivial-002.c
deleted file mode 100644
index bb6d2466..00000000
--- a/src/example-archive/coq-lemmas/inprogress/trivial-002.c
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-  lemma lem_impossible_in_coq (u32 x)
-  requires true;
-  ensures x <= 2147483647u32; 
-@*/
-
-void nothing() 
-{
-  ; 
-}
diff --git a/src/example-archive/coq-lemmas/inprogress/trivial-009.c b/src/example-archive/coq-lemmas/inprogress/trivial-009.c
new file mode 100644
index 00000000..0583285e
--- /dev/null
+++ b/src/example-archive/coq-lemmas/inprogress/trivial-009.c
@@ -0,0 +1,8 @@
+/*@ function [rec] (u32) my_spec(u32 n) { 42u32 } @*/
+
+unsigned int factorial(unsigned int n)
+/*@ ensures return == my_spec(n); @*/
+{
+  /*@ unfold my_spec(n); @*/
+  return 42;
+}
diff --git a/src/example-archive/coq-lemmas/working/recursive-001.c b/src/example-archive/coq-lemmas/working/recursive-001.c
new file mode 100644
index 00000000..b45f7289
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/recursive-001.c
@@ -0,0 +1,40 @@
+/*@
+function [rec] (u32) fact_spec(u32 n)
+{
+  if (n <= 0u32) { 1u32 }
+  else { n * fact_spec(n - 1u32) }
+}
+@*/
+
+
+/*@
+lemma spec_lemma (u32 n)
+  requires true;
+  ensures fact_spec(n) == n * fact_spec(n-1u32);
+@*/
+
+// Function to calculate the factorial of a number
+unsigned int factorial(unsigned int n)
+/*@ requires 0u32 <= n; n <= 4294967294u32;  @*/
+/*@ requires fact_spec(n) < 4294967295u32; @*/
+/*@ ensures return == fact_spec(n); @*/
+{
+    if (n <= 0) {
+      /*@ unfold fact_spec(n); @*/
+      return 1; // Return 1
+    }
+
+    unsigned result = 1;
+    /*@ unfold fact_spec(1u32-1u32); @*/
+    for (unsigned int i = 1; i <= n; i++)
+      /*@ inv {n}unchanged; @*/
+      /*@ inv 0u32 < n; i <= n+1u32; @*/
+      /*@ inv 0u32 < i; @*/
+      /*@ inv result == fact_spec(i-1u32); @*/
+      {
+        result *= i;
+	/*@ apply spec_lemma((i+1u32)-1u32); @*/
+      }
+
+    return result;
+}
diff --git a/src/example-archive/coq-lemmas/working/recursive-002.c b/src/example-archive/coq-lemmas/working/recursive-002.c
new file mode 100644
index 00000000..d245d459
--- /dev/null
+++ b/src/example-archive/coq-lemmas/working/recursive-002.c
@@ -0,0 +1,56 @@
+// Fails to export becasue of recursive definition
+
+/*@
+function [rec] (u32) fib_spec(u32 n)
+{
+  if (n <= 0u32) {
+    1u32
+  } else {
+    if (n == 1u32) {
+      1u32
+    } else {
+      fib_spec(n - 1u32) + fib_spec(n - 2u32)
+    }
+  }
+}
+@*/
+
+
+/*@
+lemma fib_lemma (u32 n)
+  requires true;
+  ensures fib_spec(n) == fib_spec(n - 1u32) + fib_spec(n - 2u32);
+@*/
+
+// Function to calculate the factorial of a number
+unsigned int fibonacci(unsigned int n)
+/*@ requires 0u32 <= n; n <= 4294967294u32;  @*/
+/*@ requires fib_spec(n) < 4294967295u32; @*/
+/*@ ensures return == fib_spec(n); @*/
+{
+    if (n <= 1) {
+      /*@ unfold fib_spec(n); @*/
+      return 1; // Return 1
+    }
+
+    unsigned previous = 1;
+    unsigned tmp = 1;
+    unsigned result = 1;
+    
+    /*@ unfold fib_spec(1u32-1u32); @*/
+    /*@ unfold fib_spec(1u32); @*/
+    for (unsigned int i = 1; i < n; i++)
+      /*@ inv {n}unchanged; @*/
+      /*@ inv 0u32 < n; i <= n; @*/
+      /*@ inv 0u32 < i; @*/
+      /*@ inv previous == fib_spec(i-1u32); @*/
+      /*@ inv result == fib_spec(i); @*/
+      {
+	tmp = previous;
+	previous = result;
+	result = tmp + previous;
+	/*@ apply fib_lemma(i+1u32); @*/
+      }
+
+    return result;
+}

From 15544d9dfe18da85857a5ffd934ba27e4cdb5774 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Mon, 24 Jun 2024 13:18:27 -0400
Subject: [PATCH 08/29] Clarity

---
 src/example-archive/coq-lemmas/README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 535457ad..a01de3c5 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -4,8 +4,8 @@ CN examples using lemmas that can be extracted to Coq. The examples are split in
 
 - Trivial
 - Recursive
-- Lists
-- Advanced
+- Lists (WIP)
+- Advanced (WIP)
 
 ## Generating Coq Lemmas 
 

From 24e43cec28ad4f498553d6c0cabe0de5fe7fa2ed Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Tue, 9 Jul 2024 10:49:16 -0400
Subject: [PATCH 09/29] Typos

---
 src/example-archive/coq-lemmas/README.md | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index a01de3c5..d6a39163 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -1,6 +1,7 @@
 ## Examples
 
-CN examples using lemmas that can be extracted to Coq. The examples are split into:
+CN examples using lemmas that can be extracted to Coq. The examples
+are split into:
 
 - Trivial
 - Recursive
@@ -44,9 +45,11 @@ Module Type Lemma_Spec (P : Parameters).
 End Lemma_Spec.
 ```
 
-## Prooving the Coq Lemmas
+## Proving the Coq Lemmas
 
-To prove the lemmas, instantiate a new module with type `Lemma_Spec` containing each of parameters as lemmas and their proofs. For the example above, the proofs look like this
+To prove the lemmas, instantiate a new module with type `Lemma_Spec`
+containing each of parameters as lemmas and their proofs. For the
+example above, the proofs look like this
 
 ```
 

From 8b18f3da22c6f774f1ab26f0667fccf7bbffcfa4 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Tue, 9 Jul 2024 10:50:27 -0400
Subject: [PATCH 10/29] Clarify examples

---
 src/example-archive/coq-lemmas/README.md | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index d6a39163..6bd82f61 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -4,9 +4,7 @@ CN examples using lemmas that can be extracted to Coq. The examples
 are split into:
 
 - Trivial
-- Recursive
-- Lists (WIP)
-- Advanced (WIP)
+- Recursive (Not yet handled by the export)
 
 ## Generating Coq Lemmas 
 

From e42511cdfadf37f5c9ce7154ac385724b9f18974 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 13:15:05 -0400
Subject: [PATCH 11/29] Add new script for checking coq extraction

---
 .../coq-lemmas/coq-build/_CoqProject          |   4 +++
 .../coq-lemmas/coq-build/theories/.CN_Lib.aux |   7 +++++
 .../coq-build/theories/.ExportedLemmas.aux    |   2 ++
 .../coq-lemmas/coq-build/theories/.lia.cache  | Bin 0 -> 1312 bytes
 .../coq-lemmas/coq-build/theories/CN_Lib.v    |  29 ++++++++++++++++++
 .../broken-export}/recursive-001.c            |   0
 .../broken-export}/recursive-002.c            |   0
 .../{ => coq}/working/trivial-001.c           |   0
 .../{ => coq}/working/trivial-002.c           |   0
 .../{ => coq}/working/trivial-003.c           |   0
 .../{ => coq}/working/trivial-004.c           |   0
 11 files changed, 42 insertions(+)
 create mode 100644 src/example-archive/coq-lemmas/coq-build/_CoqProject
 create mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
 create mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
 create mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.lia.cache
 create mode 100644 src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v
 rename src/example-archive/coq-lemmas/{working => coq/broken-export}/recursive-001.c (100%)
 rename src/example-archive/coq-lemmas/{working => coq/broken-export}/recursive-002.c (100%)
 rename src/example-archive/coq-lemmas/{ => coq}/working/trivial-001.c (100%)
 rename src/example-archive/coq-lemmas/{ => coq}/working/trivial-002.c (100%)
 rename src/example-archive/coq-lemmas/{ => coq}/working/trivial-003.c (100%)
 rename src/example-archive/coq-lemmas/{ => coq}/working/trivial-004.c (100%)

diff --git a/src/example-archive/coq-lemmas/coq-build/_CoqProject b/src/example-archive/coq-lemmas/coq-build/_CoqProject
new file mode 100644
index 00000000..065c4ea8
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq-build/_CoqProject
@@ -0,0 +1,4 @@
+-Q theories CN_Lemmas
+
+theories/CN_Lib.v
+theories/ExportedLemmas.v
\ No newline at end of file
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux b/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
new file mode 100644
index 00000000..540ba548
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
@@ -0,0 +1,7 @@
+COQAUX1 633e54b5a22b850599c444b8737dbf06 /Users/Santiago/Projects/cn-tutorial/src/example-archive/coq-lemmas/working/trivial-001-build/theories/CN_Lib.v
+0 0 VernacProof "tac:no using:no"
+748 752 proof_build_time "0.009"
+0 0 wrapI_idem "0.009"
+399 412 context_used ""
+748 752 proof_check_time "0.003"
+0 0 vo_compile_time "0.191"
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux b/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
new file mode 100644
index 00000000..a9c2953c
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
@@ -0,0 +1,2 @@
+COQAUX1 3900f32800d8cfc6593331bb6ddc51b3 /Users/Santiago/Projects/cn-tutorial/src/example-archive/coq-lemmas/working/trivial-001-build/theories/ExportedLemmas.v
+0 0 vo_compile_time "0.168"
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.lia.cache b/src/example-archive/coq-lemmas/coq-build/theories/.lia.cache
new file mode 100644
index 0000000000000000000000000000000000000000..c936905014c614dd5ec5054ef868ae50e0441f2c
GIT binary patch
literal 1312
zcmb`G&nrbi6vszzQWk`bof50}SaW;IyxvMFJ1MLzgd}@QOJ(jtZ=>9o*s0h311M!-
zX<<)USy?KD?>Tek{&KUqrq0~?dFJyy=iK)G!Gu!t&wID`$494EH%h4!*fQ*qEQ)%q
zR&C+iwJ3_MH72$pbr@mLrp09Lrn=vB-6=~8G}gm%xEp46us&|mGgEGh{gHcPqs!2u
z8GH;LnLPXm1TzNSwo-jVWJOH>dWy%-5^*`9CB%_(M7*2Ri8(8pNy%A1cRDbh`~tU_
zUIZi`QZlx?)D$H>DA|IF0kSeB`9N1xq8n+(yprisC3Al%fk<dGMhBfw(QyqOo6t}r
zE7QRN!X202q;e>j`OIWXgyrf{pBhRO{74#UBspfkiE}+Db;ob&S-FLMs;OLNaAN)I
z?m<MHL&OH`ovbKAs^7m-{006)h*U1Bv5{w%N}@l38r4w!X=hQe&w#rIdn5ae%~3$-
zgN0#5ST3U!ww{O01lR#{Pt2>$SI^u5>k90JtjL_W_Q6gwUXh&ZC2?O2bCw*qKk$xA
A>i_@%

literal 0
HcmV?d00001

diff --git a/src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v b/src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v
new file mode 100644
index 00000000..e17d738a
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v
@@ -0,0 +1,29 @@
+Require List.
+Require Import ZArith Bool.
+Require Import Lia.
+Require NArith.
+
+Definition wrapI (minInt : Z) (maxInt : Z) x :=
+  let delta := ((maxInt - minInt) + 1)%Z in
+  let r := Z.modulo x delta in
+  (if (r <=? maxInt) then r else r - delta)%Z.
+
+Lemma wrapI_idem:
+  forall (minInt maxInt x : Z),
+  (minInt <= x <= maxInt)%Z ->
+  (minInt <= 0 < maxInt)%Z ->
+  wrapI minInt maxInt x = x.
+Proof.
+  Open Scope Z.
+  intros.
+  unfold wrapI.
+  pose (delta := ((maxInt - minInt) + 1)).
+  destruct (0 <=? x) eqn: x_neg.
+  - rewrite Z.mod_small by lia.
+    rewrite Zle_imp_le_bool by lia.
+    reflexivity.
+  - rewrite (Znumtheory.Zdivide_mod_minus _ _ (x + delta)).
+    + destruct (x + delta <=? maxInt) eqn: leb; lia.
+    + lia.
+    + exists (-1); lia.
+Qed.
diff --git a/src/example-archive/coq-lemmas/working/recursive-001.c b/src/example-archive/coq-lemmas/coq/broken-export/recursive-001.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/recursive-001.c
rename to src/example-archive/coq-lemmas/coq/broken-export/recursive-001.c
diff --git a/src/example-archive/coq-lemmas/working/recursive-002.c b/src/example-archive/coq-lemmas/coq/broken-export/recursive-002.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/recursive-002.c
rename to src/example-archive/coq-lemmas/coq/broken-export/recursive-002.c
diff --git a/src/example-archive/coq-lemmas/working/trivial-001.c b/src/example-archive/coq-lemmas/coq/working/trivial-001.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/trivial-001.c
rename to src/example-archive/coq-lemmas/coq/working/trivial-001.c
diff --git a/src/example-archive/coq-lemmas/working/trivial-002.c b/src/example-archive/coq-lemmas/coq/working/trivial-002.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/trivial-002.c
rename to src/example-archive/coq-lemmas/coq/working/trivial-002.c
diff --git a/src/example-archive/coq-lemmas/working/trivial-003.c b/src/example-archive/coq-lemmas/coq/working/trivial-003.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/trivial-003.c
rename to src/example-archive/coq-lemmas/coq/working/trivial-003.c
diff --git a/src/example-archive/coq-lemmas/working/trivial-004.c b/src/example-archive/coq-lemmas/coq/working/trivial-004.c
similarity index 100%
rename from src/example-archive/coq-lemmas/working/trivial-004.c
rename to src/example-archive/coq-lemmas/coq/working/trivial-004.c

From 4cee29688e1d930c998eeb269d3f0e7b8f6f6ea5 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 13:19:50 -0400
Subject: [PATCH 12/29] add the script for checking coq extraction

---
 src/example-archive/check.sh | 110 +++++++++++++++++++++++++++++++++--
 1 file changed, 106 insertions(+), 4 deletions(-)

diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index a246a369..013052ab 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+set -x
 
 if [ -n "$1" ]
 then
@@ -54,11 +55,112 @@ check_file() {
   fi
 }
 
-process_files "working" "*.c" check_file 0
+process_files "working" "*.c"               check_file 0
 process_files "broken/error-cerberus" "*.c" check_file 2
-process_files "broken/error-crash" "*.c" check_file 125
-process_files "broken/error-proof" "*.c" check_file 1
-process_files "broken/error-timeout" "*.c" check_file 124
+process_files "broken/error-crash" "*.c"    check_file 125
+process_files "broken/error-proof" "*.c"    check_file 1
+process_files "broken/error-timeout" "*.c"  check_file 124
+process_files "coq/broken-build" "*.c"      check_file 0
+process_files "coq/broken-export" "*.c"     check_file 0
+process_files "coq/working" "*.c"           check_file 0
+
+# ====================
+# Check Coq Exports
+# ====================
+
+
+# We allow several types of failure that can be intended
+readonly SUCCESS=0
+readonly FAIL_EXPORT=1
+readonly FAIL_COQ_BUILD=2
+
+
+check_coq_exports_end() {
+    ## Call this funciton at the end of a coq export check. It will
+    ## print the right message and return to the original directory
+    ## with popd. It will also increse the failure count if necessary.
+    local FAILED=$1
+    local MESSAGE=$2
+    
+    if [[FAILED]]; then
+	printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
+	failures=$(( $failures + 1 ))
+    else
+	printf "\033[32mPASS\033[0m\n"
+    fi
+	
+    # Return to the directory where the parent function was called
+    popd > /dev/null
+}
+          
+check_coq_exports() {
+    local FILE=$1
+    local FAIL_MODE=$2
+    local PROTOTYPE_BUILD_DIR="coq-build"
+    local EXPORTED_LEMMAS="ExportedLemmas.v"
+    local result=0 #^track if the build completed as much as expected
+    
+    printf "[$FILE]... "
+    
+    # Make a copy of the build directory but only if it doesn't
+    # already exists
+    local BUILD_DIR="${FILE%.*}-build"
+
+    # Copy the build directory, and/or missing/new files
+    rsync -a "${PROTOTYPE_BUILD_DIR}/" "$BUILD_DIR"
+    
+    # Export the CN lemmas
+    cn "--lemmata=${BUILD_DIR}/theories/${EXPORTED_LEMMAS}" $FILE > /dev/null 2>&1
+    # Check the result is as expected
+    local cn_result=$?
+    if [[ $cn_result -ne 0 && $FAIL_MODE -eq $FAIL_EXPORT ]]; then
+	# The export is expected to fail and there is nothing else to
+	# be done. Return successfully.
+	check_coq_exports_end ${result} ""
+	return ${result}
+    elif [[ $cn_result -eq 0 && $FAIL_MODE -ne $FAIL_EXPORT ]]; then
+	: # Export succeeded, as expected, continue the build
+    else
+	# Otherwise fail
+        result=1
+	check_coq_exports_end ${result} "Unexpected return code during export: $cn_result"
+	return ${result}
+    fi
+
+    # The rest of the commands must be performed in the build directory 
+    pushd "$BUILD_DIR" > /dev/null
+    
+    # Create the Coq Makefile
+    # (We don't expect this to fail)
+    coq_makefile -f _CoqProject -o Makefile.coq > /dev/null
+
+    # Build the Coq files
+    make -f Makefile.coq > /dev/null
+    # Check the result is as expected
+    local coq_result=$?
+    if [[ $coq_result -ne 0 && $FAIL_MODE -eq $FAIL_COQ_BUILD ]]; then
+	# The coq build is expected to fail and there is nothing else to
+	# be done. Return successfully.
+	check_coq_exports_end ${result} ""
+	return ${result}
+    elif [[ $coq_result -eq 0 && $FAIL_MODE -ne $FAIL_COQ_BUILD ]]; then
+	: # Export succeeded, as expected
+    else
+        result=1
+	check_coq_exports_end ${result} "Unexpected return code during coq build: $coq_result"
+	return ${result}
+    fi
+
+    # At this point everythink built successfully.
+    check_coq_exports_end ${result} ""
+    return ${result}
+    
+}
+
+printf "=========\nChecking Coq builds\n\n"
+check_coq_exports "coq/working/trivial-001.c" ${SUCCESS}
+check_coq_exports "coq/broken-export/recursive-001.c" ${FAIL_EXPORT}
+
 
 if [[ "$failures" = 0 ]]
 then

From b0b7eadbe2d3413214a3535f06325c0c64e7b9a0 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 13:20:40 -0400
Subject: [PATCH 13/29] Explain the new organization, including Coq lemmas.

---
 src/example-archive/README.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/example-archive/README.md b/src/example-archive/README.md
index 22a7d058..dd2a012b 100644
--- a/src/example-archive/README.md
+++ b/src/example-archive/README.md
@@ -25,6 +25,11 @@ are categorized according to the following schema.
 * `<source>/broken/error-proof` - examples where CN fails with error 1,
   indicating the proof failed. 
 * `<source>/broken/error-timeout` - examples where CN times out after 60s. 
+* `<source>/coq/*` - examples that CN verifies without error and have lemmas that should be extracted. According to the following rules
+    * `<source>/coq/working` - Examples where Coq lemmas can be extracted and the Coq project can be built.
+    * `<source>/coq/broken-build` - Examples where Coq lemmas can be extracted, but the Coq build process fails.
+    * `<source>/coq/broken-export` - Examples where Coq extraction fails. These should still be verifiable with CN.
+* `<source>/coq/working` - examples that CN verifies without error. 
 * `<source>/inprogress` - unfinished examples. 
 
 ## Check script

From 6fce7fa3e4324f1578af2644f12611f5d9c6c9f6 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 14:10:08 -0400
Subject: [PATCH 14/29] Generalize process_files and use it to check Coq
 extraction

---
 src/example-archive/check.sh | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index 013052ab..e475b195 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -1,5 +1,4 @@
 #!/usr/bin/env bash
-set -x
 
 if [ -n "$1" ]
 then
@@ -9,13 +8,11 @@ else
     CN=cn
 fi
 
-
-
 process_files() {
   local dir=$1
   local pattern=$2
   local action=$3
-  local expected_exit_code=$4
+  local action_argument=$4
 
   if [ -d "$dir" ]; then
     # Array to hold files matching the pattern
@@ -26,7 +23,7 @@ process_files() {
       for file in "${files[@]}"; do
         # Ensure the file variable is not empty
         if [[ -n "$file" ]]; then
-          "$action" "$file" "$expected_exit_code"
+          "$action" "$file" "$action_argument"
         fi
       done
     else
@@ -39,6 +36,10 @@ process_files() {
 
 failures=0
 
+# ====================
+# Check CN verification
+# ====================
+
 check_file() {
   local file=$1
   local expected_exit_code=$2
@@ -82,7 +83,7 @@ check_coq_exports_end() {
     local FAILED=$1
     local MESSAGE=$2
     
-    if [[FAILED]]; then
+    if [[ $FAILED -ne 0 ]]; then
 	printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
 	failures=$(( $failures + 1 ))
     else
@@ -158,8 +159,10 @@ check_coq_exports() {
 }
 
 printf "=========\nChecking Coq builds\n\n"
-check_coq_exports "coq/working/trivial-001.c" ${SUCCESS}
-check_coq_exports "coq/broken-export/recursive-001.c" ${FAIL_EXPORT}
+
+process_files "coq/working" "*.c"       check_coq_exports $SUCCESS
+process_files "coq/broken-build" "*.c"  check_coq_exports $FAIL_COQ_BUILD
+process_files "coq/broken-export" "*.c" check_coq_exports $FAIL_EXPORT
 
 
 if [[ "$failures" = 0 ]]

From 3fcc4c775394fd1e89bdf7f6611a75ee23e91f40 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 14:23:28 -0400
Subject: [PATCH 15/29] Ignore the build files

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index f12c5c6f..384f6f98 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 build/*
 /.vscode/
+/src/example-archive/**/coq/**/*-build
\ No newline at end of file

From 14988a672a96fa3fa13e3c835aabd03ddbd6bf98 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 16:26:28 -0400
Subject: [PATCH 16/29] Ignore coq files, except the proofs. This affects only
 the example-archive

---
 .gitignore                     | 3 +--
 src/example-archive/.gitignore | 3 +++
 2 files changed, 4 insertions(+), 2 deletions(-)
 create mode 100644 src/example-archive/.gitignore

diff --git a/.gitignore b/.gitignore
index 384f6f98..2a39c64d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,2 @@
 build/*
-/.vscode/
-/src/example-archive/**/coq/**/*-build
\ No newline at end of file
+/.vscode/
\ No newline at end of file
diff --git a/src/example-archive/.gitignore b/src/example-archive/.gitignore
new file mode 100644
index 00000000..c69bf9fd
--- /dev/null
+++ b/src/example-archive/.gitignore
@@ -0,0 +1,3 @@
+/**/coq/**/*-build
+
+!/**/coq/**/*-build/theories/Proofs.v
\ No newline at end of file

From cb04df9b7a3064deefa7c25623bf744ec76adaad Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 16:53:20 -0400
Subject: [PATCH 17/29] Add the proofs

---
 src/example-archive/.gitignore                |  7 +++--
 .../coq-lemmas/coq-build/_CoqProject          |  5 ++--
 .../trivial-002-build/theories/Proofs.v       | 24 +++++++++++++++++
 .../trivial-004-build/theories/Proofs.v       | 27 +++++++++++++++++++
 .../trivial-001-build/theories/Proofs.v       | 21 +++++++++++++++
 .../trivial-003-build/theories/Proofs.v       | 23 ++++++++++++++++
 6 files changed, 102 insertions(+), 5 deletions(-)
 create mode 100644 src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v
 create mode 100644 src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v
 create mode 100644 src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v
 create mode 100644 src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v

diff --git a/src/example-archive/.gitignore b/src/example-archive/.gitignore
index c69bf9fd..d863d5fb 100644
--- a/src/example-archive/.gitignore
+++ b/src/example-archive/.gitignore
@@ -1,3 +1,6 @@
-/**/coq/**/*-build
+/**/coq/**/*-build/*
+/**/coq/**/*-build/theories/*
 
-!/**/coq/**/*-build/theories/Proofs.v
\ No newline at end of file
+!**/coq/**/*-build/
+!**/coq/**/*-build/theories/
+!**/coq/**/*-build/theories/Proofs.v
\ No newline at end of file
diff --git a/src/example-archive/coq-lemmas/coq-build/_CoqProject b/src/example-archive/coq-lemmas/coq-build/_CoqProject
index 065c4ea8..efc08743 100644
--- a/src/example-archive/coq-lemmas/coq-build/_CoqProject
+++ b/src/example-archive/coq-lemmas/coq-build/_CoqProject
@@ -1,4 +1,3 @@
--Q theories CN_Lemmas
+-R theories CN_Lemmas
 
-theories/CN_Lib.v
-theories/ExportedLemmas.v
\ No newline at end of file
+theories
\ No newline at end of file
diff --git a/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v
new file mode 100644
index 00000000..7a08e7ed
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-build/trivial-002-build/theories/Proofs.v
@@ -0,0 +1,24 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_impossible_in_coq : lem_impossible_in_coq_type.
+  Proof. unfold lem_impossible_in_coq_type.
+         (* Goal: forall x : Z, x <= 4294967295*)
+         (* That's impossible to prove! *)
+  Abort. Qed.
+  
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v
new file mode 100644
index 00000000..c17457a0
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/broken-build/trivial-004-build/theories/Proofs.v
@@ -0,0 +1,27 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_impossible_in_Coq : lem_impossible_in_Coq_type.
+  Proof. unfold lem_impossible_in_Coq_type.
+         (* Goal: forall x : Z,
+            CN_Lib.wrapI 0 4294967295
+             (CN_Lib.wrapI 0 4294967295 (x + 1) - 1) = x *)
+         (* That's impossible to prove! The LHS is always in bound,
+            but x can be any Z *)
+  Abort. Qed.
+         
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v
new file mode 100644
index 00000000..6101a8b4
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-001-build/theories/Proofs.v
@@ -0,0 +1,21 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_trivial : lem_trivial_type.
+  Proof. unfold lem_trivial_type; exact I. Qed.
+  
+End ConcreteLemmaSpec.
+
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v b/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v
new file mode 100644
index 00000000..91d03fc8
--- /dev/null
+++ b/src/example-archive/coq-lemmas/coq/working/trivial-003-build/theories/Proofs.v
@@ -0,0 +1,23 @@
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
+
+
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+End ConcreteParameters.
+
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
+
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
+  Import D.
+
+  Definition lem_ineq : lem_ineq_type.
+  Proof. unfold lem_ineq_type.
+         constructor; assumption.
+  Qed.
+  
+End ConcreteLemmaSpec.
+

From cbabefdc1952d96c7f4d0460749a7e0592393cba Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 16:54:33 -0400
Subject: [PATCH 18/29] Move examples that fail to build/incomplete proofs.

---
 .../coq-lemmas/coq/working/trivial-002.c               | 10 ----------
 .../coq-lemmas/coq/working/trivial-004.c               | 10 ----------
 2 files changed, 20 deletions(-)
 delete mode 100644 src/example-archive/coq-lemmas/coq/working/trivial-002.c
 delete mode 100644 src/example-archive/coq-lemmas/coq/working/trivial-004.c

diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-002.c b/src/example-archive/coq-lemmas/coq/working/trivial-002.c
deleted file mode 100644
index 0d2cc978..00000000
--- a/src/example-archive/coq-lemmas/coq/working/trivial-002.c
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-  lemma lem_impossible_in_coq (u32 x)
-  requires true;
-  ensures x <= 4294967295u32; 
-@*/
-
-void nothing() 
-{
-  ; 
-}
diff --git a/src/example-archive/coq-lemmas/coq/working/trivial-004.c b/src/example-archive/coq-lemmas/coq/working/trivial-004.c
deleted file mode 100644
index 51c47e76..00000000
--- a/src/example-archive/coq-lemmas/coq/working/trivial-004.c
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-  lemma lem_impossible_in_Coq (u32 x)
-  requires true;
-  ensures (x + 1u32) - 1u32  == x;
-@*/
-
-void trivial() 
-{
-  ; 
-}

From 156c4f00288c8a661c522e53b90eb3b59c62cf71 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 16:55:15 -0400
Subject: [PATCH 19/29] Fix the popd bug and add titles to the two sections.

---
 src/example-archive/check.sh | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index e475b195..d32eb304 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -56,6 +56,7 @@ check_file() {
   fi
 }
 
+printf "== Check CN verification \n"
 process_files "working" "*.c"               check_file 0
 process_files "broken/error-cerberus" "*.c" check_file 2
 process_files "broken/error-crash" "*.c"    check_file 125
@@ -89,9 +90,6 @@ check_coq_exports_end() {
     else
 	printf "\033[32mPASS\033[0m\n"
     fi
-	
-    # Return to the directory where the parent function was called
-    popd > /dev/null
 }
           
 check_coq_exports() {
@@ -136,30 +134,31 @@ check_coq_exports() {
     coq_makefile -f _CoqProject -o Makefile.coq > /dev/null
 
     # Build the Coq files
-    make -f Makefile.coq > /dev/null
+    make -f Makefile.coq > /dev/null  2>&1
     # Check the result is as expected
     local coq_result=$?
     if [[ $coq_result -ne 0 && $FAIL_MODE -eq $FAIL_COQ_BUILD ]]; then
 	# The coq build is expected to fail and there is nothing else to
 	# be done. Return successfully.
 	check_coq_exports_end ${result} ""
-	return ${result}
     elif [[ $coq_result -eq 0 && $FAIL_MODE -ne $FAIL_COQ_BUILD ]]; then
-	: # Export succeeded, as expected
+	# Export succeeded, as expected
+        check_coq_exports_end ${result} ""
     else
         result=1
 	check_coq_exports_end ${result} "Unexpected return code during coq build: $coq_result"
-	return ${result}
     fi
 
     # At this point everythink built successfully.
-    check_coq_exports_end ${result} ""
-    return ${result}
-    
-}
 
-printf "=========\nChecking Coq builds\n\n"
+    # Return to the directory where the script was called (from the
+    # build directory)
+    popd > /dev/null
+
+    return ${result}    
+}
 
+printf "== Check lemma export\n"
 process_files "coq/working" "*.c"       check_coq_exports $SUCCESS
 process_files "coq/broken-build" "*.c"  check_coq_exports $FAIL_COQ_BUILD
 process_files "coq/broken-export" "*.c" check_coq_exports $FAIL_EXPORT

From b1f959a79f9bfb2b9451e64ebc602fdf414aa561 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 18:08:06 -0400
Subject: [PATCH 20/29] Move the build folder prototype to the parent directory
 to be used by any other examples set.

---
 src/example-archive/check.sh                     |   2 +-
 src/example-archive/coq-build/README.md          |   5 +++++
 .../{coq-lemmas => }/coq-build/_CoqProject       |   0
 .../{coq-lemmas => }/coq-build/theories/CN_Lib.v |   0
 .../coq-lemmas/coq-build/theories/.CN_Lib.aux    |   7 -------
 .../coq-build/theories/.ExportedLemmas.aux       |   2 --
 .../coq-lemmas/coq-build/theories/.lia.cache     | Bin 1312 -> 0 bytes
 7 files changed, 6 insertions(+), 10 deletions(-)
 create mode 100644 src/example-archive/coq-build/README.md
 rename src/example-archive/{coq-lemmas => }/coq-build/_CoqProject (100%)
 rename src/example-archive/{coq-lemmas => }/coq-build/theories/CN_Lib.v (100%)
 delete mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
 delete mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
 delete mode 100644 src/example-archive/coq-lemmas/coq-build/theories/.lia.cache

diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index d32eb304..d3b8d42d 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -95,7 +95,7 @@ check_coq_exports_end() {
 check_coq_exports() {
     local FILE=$1
     local FAIL_MODE=$2
-    local PROTOTYPE_BUILD_DIR="coq-build"
+    local PROTOTYPE_BUILD_DIR="../coq-build"
     local EXPORTED_LEMMAS="ExportedLemmas.v"
     local result=0 #^track if the build completed as much as expected
     
diff --git a/src/example-archive/coq-build/README.md b/src/example-archive/coq-build/README.md
new file mode 100644
index 00000000..7816aca6
--- /dev/null
+++ b/src/example-archive/coq-build/README.md
@@ -0,0 +1,5 @@
+## Lemma export build forlder
+
+This folder will be copied to be used as a build folder for exported lemmas. Lemmas should be extracted into the `theories/ExportedLemmas.v` and proofs, if any, should be written in `theories/Proofs.v`
+
+From the `_CoqProject` a Makefile should be generated automatically.
diff --git a/src/example-archive/coq-lemmas/coq-build/_CoqProject b/src/example-archive/coq-build/_CoqProject
similarity index 100%
rename from src/example-archive/coq-lemmas/coq-build/_CoqProject
rename to src/example-archive/coq-build/_CoqProject
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v b/src/example-archive/coq-build/theories/CN_Lib.v
similarity index 100%
rename from src/example-archive/coq-lemmas/coq-build/theories/CN_Lib.v
rename to src/example-archive/coq-build/theories/CN_Lib.v
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux b/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
deleted file mode 100644
index 540ba548..00000000
--- a/src/example-archive/coq-lemmas/coq-build/theories/.CN_Lib.aux
+++ /dev/null
@@ -1,7 +0,0 @@
-COQAUX1 633e54b5a22b850599c444b8737dbf06 /Users/Santiago/Projects/cn-tutorial/src/example-archive/coq-lemmas/working/trivial-001-build/theories/CN_Lib.v
-0 0 VernacProof "tac:no using:no"
-748 752 proof_build_time "0.009"
-0 0 wrapI_idem "0.009"
-399 412 context_used ""
-748 752 proof_check_time "0.003"
-0 0 vo_compile_time "0.191"
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux b/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
deleted file mode 100644
index a9c2953c..00000000
--- a/src/example-archive/coq-lemmas/coq-build/theories/.ExportedLemmas.aux
+++ /dev/null
@@ -1,2 +0,0 @@
-COQAUX1 3900f32800d8cfc6593331bb6ddc51b3 /Users/Santiago/Projects/cn-tutorial/src/example-archive/coq-lemmas/working/trivial-001-build/theories/ExportedLemmas.v
-0 0 vo_compile_time "0.168"
diff --git a/src/example-archive/coq-lemmas/coq-build/theories/.lia.cache b/src/example-archive/coq-lemmas/coq-build/theories/.lia.cache
deleted file mode 100644
index c936905014c614dd5ec5054ef868ae50e0441f2c..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 1312
zcmb`G&nrbi6vszzQWk`bof50}SaW;IyxvMFJ1MLzgd}@QOJ(jtZ=>9o*s0h311M!-
zX<<)USy?KD?>Tek{&KUqrq0~?dFJyy=iK)G!Gu!t&wID`$494EH%h4!*fQ*qEQ)%q
zR&C+iwJ3_MH72$pbr@mLrp09Lrn=vB-6=~8G}gm%xEp46us&|mGgEGh{gHcPqs!2u
z8GH;LnLPXm1TzNSwo-jVWJOH>dWy%-5^*`9CB%_(M7*2Ri8(8pNy%A1cRDbh`~tU_
zUIZi`QZlx?)D$H>DA|IF0kSeB`9N1xq8n+(yprisC3Al%fk<dGMhBfw(QyqOo6t}r
zE7QRN!X202q;e>j`OIWXgyrf{pBhRO{74#UBspfkiE}+Db;ob&S-FLMs;OLNaAN)I
z?m<MHL&OH`ovbKAs^7m-{006)h*U1Bv5{w%N}@l38r4w!X=hQe&w#rIdn5ae%~3$-
zgN0#5ST3U!ww{O01lR#{Pt2>$SI^u5>k90JtjL_W_Q6gwUXh&ZC2?O2bCw*qKk$xA
A>i_@%


From 03339e5115d1dea07f8562d2d0a7ae9f1b85ff8a Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 18:08:35 -0400
Subject: [PATCH 21/29] Foolproof build

---
 src/example-archive/coq-lemmas/README.md | 107 ++++++++++++-----------
 1 file changed, 57 insertions(+), 50 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 6bd82f61..6996f0f2 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -6,63 +6,70 @@ are split into:
 - Trivial
 - Recursive (Not yet handled by the export)
 
-## Generating Coq Lemmas 
-
-To generate Coq lemma for a given `example-file.c` run
-
-```
-cn --lemmata=build/theories/ExportedLemmas.v example-file.c
-```
-
-File `build/theories/ExportedLemmas.v` should be generated with the
-right definitions. Each lemma is exported as a new definition and then
-added as a parameter in the module named `Lemma_Spec`. It should look
-something like this
+## Batch build
+
+To export and build lemmas for all examples just run
+`../check.sh`. For each file in the `coq` folder, the script first
+checks the CN verification and then exports lemmas to Coq and builds
+the Coq files. When proofs are provided, those will be built too.
+
+To provide proofs or test individual examples, see below.
+
+## Testing individual examples
+
+From this folder, to export lemmas from the example `path/to/example.c`, do the following:
+
+0. (optional) Check CN verification, without exporting lemmas, `cn path/to/example.c`
+1. Create a copy of the build folder with `rsync -a ../coq-build
+   path/to/example-build`. This copies a template build folder that
+   conveniently contains a `_CoqProject` file and the CN coq library
+   `CN_Lib.v`. If the folder already excists, `rsync` just updates the files.
+2. Extract the lemmas with `cn
+   "--lemmata=path/to/example-build/theories/ExportedLemmas.v"
+   path/to/example.c`. This should create a new file
+   `path/to/example-build/theories/ExportedLemmas.v` with all the
+   exported types, definitions and lemmas from the file
+   `path/to/example.c`.
+3. Go to the build directory with `pushd path/to/example-build`. This
+   will also store your current location to return later.
+4. Create or update the Coq Makefile with `coq_makefile -f _CoqProject -o Makefile.coq`
+5. Build the Coq files with `make -f Makefile.coq`. This should create
+   `*.vo` files for every `*.v` file in the `theories` directory.
+6. Return to your starting folder with `popd`
+
+To add proofs, after running the steps above, create a file `Proofs.v`
+in the `theories` folder, next to the generated
+`ExportedLemmas.v`. The file must contain instances of the module
+types defined in `ExportedLemmas.v`: `Parameters`, `Defs`, and
+`Lemma_Spec` module type (see below for more details).
+
+Your file will look something like this:
 
 ```
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+Require Import CN_Lemmas.ExportedLemmas.
 
-Module Defs (P : Parameters).
-
-  Import Types P.
-  Open Scope Z.
 
+(*Parameters*)
+Module ConcreteParameters <:Parameters.
+(*Fill parameters here, if any*)
+End ConcreteParameters.
 
-  Definition my_lemma_type : Prop :=
-    Is_true true.
+(*Definitions*)
+Module ConcreteDefs := Defs(ConcreteParameters).
 
-End Defs.
-
-
-Module Type Lemma_Spec (P : Parameters).
-
-  Module D := Defs(P).
+Module ConcreteLemmaSpec <: Lemma_Spec(ConcreteParameters).
+  Module D := ConcreteDefs.
   Import D.
 
-  Parameter my_lemma : my_lemma_type.
-
-End Lemma_Spec.
-```
-
-## Proving the Coq Lemmas
-
-To prove the lemmas, instantiate a new module with type `Lemma_Spec`
-containing each of parameters as lemmas and their proofs. For the
-example above, the proofs look like this
-
-```
-
-Module MyP: Parameters.
-End MyP.
-
-Module Proofs : Lemma_Spec MyP.
-  Module D := Defs(MyP).
-  Import D.
-
-  Lemma  just_arith2 : my_lemma_type.
-  Proof.
-    solve [hnf; trivial].
-  Qed.
-
-End Proofs.
+  (*Prove the lemmas, if any. *)
+  Definition example_lemma : example_lemma_type.
+  Proof. (*Add here the proof*) . Qed.
   
+End ConcreteLemmaSpec.
 ```
+
+Once all the proofs have been completed in `Proofs.v`, repeat steps
+3-6 above to build all files. If `Proofs.vo` is generated correctly,
+the extracted lemmas have been proven.

From fe58f2971a426ec571100062831a2d5c74f0f944 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 18:11:21 -0400
Subject: [PATCH 22/29] README details

---
 src/example-archive/README.md            | 1 +
 src/example-archive/coq-lemmas/README.md | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/src/example-archive/README.md b/src/example-archive/README.md
index dd2a012b..24480fa3 100644
--- a/src/example-archive/README.md
+++ b/src/example-archive/README.md
@@ -10,6 +10,7 @@ This directory contains examples for CN. Each subdirectory contains examples fro
 * `Rust` - C versions of Rust programs, with CN annotations that provide the same guarantees as the Rust type-checker.
 * `SAW` - Examples derived from the [Software Analysis Workbench (SAW)](https://saw.galois.com) repository and tutorial. 
 * `open-sut` - Examples inspired by the VERSE Open System Under Test (Open SUT).
+* `coq-lemmas` - Examples with declared lemmas that can be exported to Coq for manual proofs.
 
 ## Organization  
 
diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 6996f0f2..57a8488b 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -6,6 +6,8 @@ are split into:
 - Trivial
 - Recursive (Not yet handled by the export)
 
+See README in parent directory for directory organization details.
+
 ## Batch build
 
 To export and build lemmas for all examples just run

From 69a793e78d223c4a468ffd1f47e0557155d46252 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 18:14:49 -0400
Subject: [PATCH 23/29] remove old build folder

---
 src/example-archive/coq-lemmas/build/Makefile |  8 ----
 .../coq-lemmas/build/_CoqProject              |  7 ---
 .../coq-lemmas/build/theories/CN_Lib.v        | 29 -------------
 .../build/theories/ExportedLemmas.v           |  6 ---
 .../coq-lemmas/build/theories/Gen_Spec.v      | 43 -------------------
 5 files changed, 93 deletions(-)
 delete mode 100644 src/example-archive/coq-lemmas/build/Makefile
 delete mode 100644 src/example-archive/coq-lemmas/build/_CoqProject
 delete mode 100644 src/example-archive/coq-lemmas/build/theories/CN_Lib.v
 delete mode 100644 src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
 delete mode 100644 src/example-archive/coq-lemmas/build/theories/Gen_Spec.v

diff --git a/src/example-archive/coq-lemmas/build/Makefile b/src/example-archive/coq-lemmas/build/Makefile
deleted file mode 100644
index 819ea988..00000000
--- a/src/example-archive/coq-lemmas/build/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-
-
-
-all:
-	coq_makefile -f _CoqProject -o Makefile.coq
-	cn ../../SantiagosExamples/trivial-lemma.c --lemmata theories/Gen_Spec.v
-	make -f Makefile.coq
-
diff --git a/src/example-archive/coq-lemmas/build/_CoqProject b/src/example-archive/coq-lemmas/build/_CoqProject
deleted file mode 100644
index 917968e6..00000000
--- a/src/example-archive/coq-lemmas/build/_CoqProject
+++ /dev/null
@@ -1,7 +0,0 @@
-
--Q theories CN_Lemmas
-
-theories/CN_Lib.v
-theories/ExportedLemmas.v
-
-
diff --git a/src/example-archive/coq-lemmas/build/theories/CN_Lib.v b/src/example-archive/coq-lemmas/build/theories/CN_Lib.v
deleted file mode 100644
index e17d738a..00000000
--- a/src/example-archive/coq-lemmas/build/theories/CN_Lib.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Require List.
-Require Import ZArith Bool.
-Require Import Lia.
-Require NArith.
-
-Definition wrapI (minInt : Z) (maxInt : Z) x :=
-  let delta := ((maxInt - minInt) + 1)%Z in
-  let r := Z.modulo x delta in
-  (if (r <=? maxInt) then r else r - delta)%Z.
-
-Lemma wrapI_idem:
-  forall (minInt maxInt x : Z),
-  (minInt <= x <= maxInt)%Z ->
-  (minInt <= 0 < maxInt)%Z ->
-  wrapI minInt maxInt x = x.
-Proof.
-  Open Scope Z.
-  intros.
-  unfold wrapI.
-  pose (delta := ((maxInt - minInt) + 1)).
-  destruct (0 <=? x) eqn: x_neg.
-  - rewrite Z.mod_small by lia.
-    rewrite Zle_imp_le_bool by lia.
-    reflexivity.
-  - rewrite (Znumtheory.Zdivide_mod_minus _ _ (x + delta)).
-    + destruct (x + delta <=? maxInt) eqn: leb; lia.
-    + lia.
-    + exists (-1); lia.
-Qed.
diff --git a/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v b/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
deleted file mode 100644
index e8fec956..00000000
--- a/src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* build/theories/ExportedLemmas.v: generated lemma specifications from CN *)
-
-Require Import ZArith Bool.
-Require CN_Lemmas.CN_Lib.
-
-
diff --git a/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v b/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v
deleted file mode 100644
index 7254a094..00000000
--- a/src/example-archive/coq-lemmas/build/theories/Gen_Spec.v
+++ /dev/null
@@ -1,43 +0,0 @@
-(* theories/Gen_Spec.v: generated lemma specifications from CN *)
-
-Require Import ZArith Bool.
-Require CN_Lemmas.CN_Lib.
-
-
-Module Types.
-
-  (* no type definitions required *)
-
-End Types.
-
-
-Module Type Parameters.
-  Import Types.
-
-  (* no parameters required *)
-
-End Parameters.
-
-
-Module Defs (P : Parameters).
-
-  Import Types P.
-  Open Scope Z.
-
-
-  Definition lem_trivial_type : Prop :=
-    Is_true true.
-
-End Defs.
-
-
-Module Type Lemma_Spec (P : Parameters).
-
-  Module D := Defs(P).
-  Import D.
-
-  Parameter lem_trivial : lem_trivial_type.
-
-End Lemma_Spec.
-
-

From f39bb7f791375b5706242add591da00bd3d2436a Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Wed, 10 Jul 2024 18:17:27 -0400
Subject: [PATCH 24/29] clean up

---
 src/example-archive/coq-lemmas/README.md | 48 +++++++++++++++++-------
 1 file changed, 35 insertions(+), 13 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 57a8488b..9c01a672 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -11,7 +11,9 @@ See README in parent directory for directory organization details.
 ## Batch build
 
 To export and build lemmas for all examples just run
-`../check.sh`. For each file in the `coq` folder, the script first
+`../check.sh`. 
+
+For each file in the `coq` folder, the script first
 checks the CN verification and then exports lemmas to Coq and builds
 the Coq files. When proofs are provided, those will be built too.
 
@@ -19,25 +21,45 @@ To provide proofs or test individual examples, see below.
 
 ## Testing individual examples
 
-From this folder, to export lemmas from the example `path/to/example.c`, do the following:
+From this folder, to export lemmas from example `path/to/example.c`, do the following:
+
+0. (optional) Check CN verification, without exporting lemmas, with
+
+   `cn path/to/example.c`
+
+1. Create a copy of the build folder with 
 
-0. (optional) Check CN verification, without exporting lemmas, `cn path/to/example.c`
-1. Create a copy of the build folder with `rsync -a ../coq-build
+	`rsync -a ../coq-build
+   
    path/to/example-build`. This copies a template build folder that
    conveniently contains a `_CoqProject` file and the CN coq library
    `CN_Lib.v`. If the folder already excists, `rsync` just updates the files.
-2. Extract the lemmas with `cn
-   "--lemmata=path/to/example-build/theories/ExportedLemmas.v"
-   path/to/example.c`. This should create a new file
+2. Extract the lemmas with 
+   
+   `cn --lemmata=path/to/example-build/theories/ExportedLemmas.v path/to/example.c`
+   
+   This should create a new file
    `path/to/example-build/theories/ExportedLemmas.v` with all the
    exported types, definitions and lemmas from the file
    `path/to/example.c`.
-3. Go to the build directory with `pushd path/to/example-build`. This
-   will also store your current location to return later.
-4. Create or update the Coq Makefile with `coq_makefile -f _CoqProject -o Makefile.coq`
-5. Build the Coq files with `make -f Makefile.coq`. This should create
-   `*.vo` files for every `*.v` file in the `theories` directory.
-6. Return to your starting folder with `popd`
+3. Go to the build directory with 
+
+	`pushd path/to/example-build`
+	
+	This will also store your current location to return later.
+4. Create or update the Coq Makefile with 
+
+	`coq_makefile -f _CoqProject -o Makefile.coq`
+	
+5. Build the Coq files with 
+
+	`make -f Makefile.coq`
+	
+	This should create `*.vo` files for every `*.v` file in the
+   `theories` directory.
+6. Return to your starting folder with 
+
+	`popd`
 
 To add proofs, after running the steps above, create a file `Proofs.v`
 in the `theories` folder, next to the generated

From 8570affc28edad381e65173439082113517abe65 Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Thu, 11 Jul 2024 09:41:09 -0400
Subject: [PATCH 25/29] Fix Typos

---
 src/example-archive/coq-lemmas/README.md | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 9c01a672..38fa117e 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -8,6 +8,11 @@ are split into:
 
 See README in parent directory for directory organization details.
 
+## Tools needed
+
+To build the generated Coq lemmas, you will need to [download and
+install Coq](download).
+
 ## Batch build
 
 To export and build lemmas for all examples just run
@@ -29,11 +34,11 @@ From this folder, to export lemmas from example `path/to/example.c`, do the foll
 
 1. Create a copy of the build folder with 
 
-	`rsync -a ../coq-build
-   
-   path/to/example-build`. This copies a template build folder that
-   conveniently contains a `_CoqProject` file and the CN coq library
-   `CN_Lib.v`. If the folder already excists, `rsync` just updates the files.
+	`rsync -a ../coq-build path/to/example-build`
+	
+	This copies a template build folder that conveniently contains a
+   `_CoqProject` file and the CN coq library `CN_Lib.v`. If the folder
+   already excists, `rsync` just updates the files.
 2. Extract the lemmas with 
    
    `cn --lemmata=path/to/example-build/theories/ExportedLemmas.v path/to/example.c`
@@ -65,9 +70,9 @@ To add proofs, after running the steps above, create a file `Proofs.v`
 in the `theories` folder, next to the generated
 `ExportedLemmas.v`. The file must contain instances of the module
 types defined in `ExportedLemmas.v`: `Parameters`, `Defs`, and
-`Lemma_Spec` module type (see below for more details).
+`Lemma_Spec` module type.
 
-Your file will look something like this:
+Your `theories/Proofs.v` file will look something like this:
 
 ```
 Require Import ZArith Bool.

From 5f704cc7037a900b7fe15ec28dc869f0a85d4d6f Mon Sep 17 00:00:00 2001
From: scuellar <cuellar.s@gmail.com>
Date: Thu, 11 Jul 2024 09:46:45 -0400
Subject: [PATCH 26/29] Add clarity

---
 src/example-archive/coq-lemmas/README.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 38fa117e..805426a6 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -16,6 +16,7 @@ install Coq](download).
 ## Batch build
 
 To export and build lemmas for all examples just run
+
 `../check.sh`. 
 
 For each file in the `coq` folder, the script first
@@ -34,9 +35,10 @@ From this folder, to export lemmas from example `path/to/example.c`, do the foll
 
 1. Create a copy of the build folder with 
 
-	`rsync -a ../coq-build path/to/example-build`
+	`rsync -a ../coq-build/ path/to/example-build`
 	
-	This copies a template build folder that conveniently contains a
+	(note trailing `/` after the first directory). This
+   copies a template build folder that conveniently contains a
    `_CoqProject` file and the CN coq library `CN_Lib.v`. If the folder
    already excists, `rsync` just updates the files.
 2. Extract the lemmas with 

From 4d5f28b948ea759f4336f55a2377fcd2e585c067 Mon Sep 17 00:00:00 2001
From: septract <miked@galois.com>
Date: Thu, 11 Jul 2024 14:18:14 -0700
Subject: [PATCH 27/29] Tidy up typos and some script things

---
 src/example-archive/check-all.sh         |  15 +-
 src/example-archive/check.sh             | 176 +++++++++++------------
 src/example-archive/coq-lemmas/README.md |  50 +++----
 3 files changed, 121 insertions(+), 120 deletions(-)

diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh
index 4f712ac3..d7e27562 100755
--- a/src/example-archive/check-all.sh
+++ b/src/example-archive/check-all.sh
@@ -2,10 +2,10 @@
 
 if [ -n "$1" ]
 then
-    echo "check-all.sh: using CN=$1 in $PWD"
-    CN="$1"
+  echo "check-all.sh: using CN=$1 in $PWD"
+  CN="$1"
 else
-    CN=cn
+  CN=cn
 fi
 
 subdirs=(
@@ -17,6 +17,7 @@ subdirs=(
   "Rust" 
   "SAW" 
   "simple-examples"
+  "coq-lemmas"
 )
 FAILURE=0 
 
@@ -35,9 +36,9 @@ done
 
 if [ $FAILURE -eq 0 ];
 then
-    printf "\n\033[32mTest suite passes:\033[0m all CN tests in the example archive produced expected return codes\n"
-    exit 0
+  printf "\n\033[32mTest suite passes:\033[0m all CN tests in the example archive produced expected return codes\n"
+  exit 0
 else 
-    printf "\n\033[31mTest suite fails:\033[0m one or more CN tests in the example archive produced an unexpected return code\n"
-    exit 1
+  printf "\n\033[31mTest suite fails:\033[0m one or more CN tests in the example archive produced an unexpected return code\n"
+  exit 1
 fi
\ No newline at end of file
diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh
index d3b8d42d..ee1b7656 100755
--- a/src/example-archive/check.sh
+++ b/src/example-archive/check.sh
@@ -2,10 +2,10 @@
 
 if [ -n "$1" ]
 then
-    echo "check.sh: using CN=$1 in $PWD"
-    CN="$1"
+  echo "check.sh: using CN=$1 in $PWD"
+  CN="$1"
 else
-    CN=cn
+  CN=cn
 fi
 
 process_files() {
@@ -15,20 +15,20 @@ process_files() {
   local action_argument=$4
 
   if [ -d "$dir" ]; then
-    # Array to hold files matching the pattern
-    local files=($(find "$dir" -maxdepth 1 -type f -name "$pattern" | sort))
-
-    # Check if the array is not empty
-    if [ "${#files[@]}" -gt 0 ]; then
-      for file in "${files[@]}"; do
-        # Ensure the file variable is not empty
-        if [[ -n "$file" ]]; then
-          "$action" "$file" "$action_argument"
-        fi
-      done
-    else
-      echo "No files matching '$pattern' found in $dir"
+  # Array to hold files matching the pattern
+  local files=($(find "$dir" -maxdepth 1 -type f -name "$pattern" | sort))
+
+  # Check if the array is not empty
+  if [ "${#files[@]}" -gt 0 ]; then
+    for file in "${files[@]}"; do
+    # Ensure the file variable is not empty
+    if [[ -n "$file" ]]; then
+      "$action" "$file" "$action_argument"
     fi
+    done
+  else
+    echo "No files matching '$pattern' found in $dir"
+  fi
   else
     echo "Directory $dir does not exist"
   fi
@@ -78,84 +78,84 @@ readonly FAIL_COQ_BUILD=2
 
 
 check_coq_exports_end() {
-    ## Call this funciton at the end of a coq export check. It will
-    ## print the right message and return to the original directory
-    ## with popd. It will also increse the failure count if necessary.
-    local FAILED=$1
-    local MESSAGE=$2
-    
-    if [[ $FAILED -ne 0 ]]; then
-	printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
-	failures=$(( $failures + 1 ))
-    else
-	printf "\033[32mPASS\033[0m\n"
-    fi
+  ## Call this function at the end of a coq export check. It will
+  ## print the right message and return to the original directory
+  ## with popd. It will also increse the failure count if necessary.
+  local FAILED=$1
+  local MESSAGE=$2
+  
+  if [[ $FAILED -ne 0 ]]; then
+    printf "\033[31mFAIL\033[0m (${MESSAGE})\n"
+    failures=$(( $failures + 1 ))
+  else
+    printf "\033[32mPASS\033[0m\n"
+  fi
 }
-          
+
 check_coq_exports() {
-    local FILE=$1
-    local FAIL_MODE=$2
-    local PROTOTYPE_BUILD_DIR="../coq-build"
-    local EXPORTED_LEMMAS="ExportedLemmas.v"
-    local result=0 #^track if the build completed as much as expected
-    
-    printf "[$FILE]... "
-    
-    # Make a copy of the build directory but only if it doesn't
-    # already exists
-    local BUILD_DIR="${FILE%.*}-build"
-
-    # Copy the build directory, and/or missing/new files
-    rsync -a "${PROTOTYPE_BUILD_DIR}/" "$BUILD_DIR"
-    
-    # Export the CN lemmas
-    cn "--lemmata=${BUILD_DIR}/theories/${EXPORTED_LEMMAS}" $FILE > /dev/null 2>&1
-    # Check the result is as expected
-    local cn_result=$?
-    if [[ $cn_result -ne 0 && $FAIL_MODE -eq $FAIL_EXPORT ]]; then
-	# The export is expected to fail and there is nothing else to
-	# be done. Return successfully.
-	check_coq_exports_end ${result} ""
-	return ${result}
-    elif [[ $cn_result -eq 0 && $FAIL_MODE -ne $FAIL_EXPORT ]]; then
-	: # Export succeeded, as expected, continue the build
-    else
-	# Otherwise fail
-        result=1
-	check_coq_exports_end ${result} "Unexpected return code during export: $cn_result"
-	return ${result}
-    fi
+  local FILE=$1
+  local FAIL_MODE=$2
+  local PROTOTYPE_BUILD_DIR="../coq-build"
+  local EXPORTED_LEMMAS="ExportedLemmas.v"
+  local result=0 #^track if the build completed as much as expected
+  
+  printf "[$FILE]... "
+  
+  # Make a copy of the build directory but only if it doesn't
+  # already exists
+  local BUILD_DIR="${FILE%.*}-build"
+
+  # Copy the build directory, and/or missing/new files
+  rsync -a "${PROTOTYPE_BUILD_DIR}/" "$BUILD_DIR"
+  
+  # Export the CN lemmas
+  $CN "--lemmata=${BUILD_DIR}/theories/${EXPORTED_LEMMAS}" $FILE > /dev/null 2>&1
+  # Check the result is as expected
+  local cn_result=$?
+  if [[ $cn_result -ne 0 && $FAIL_MODE -eq $FAIL_EXPORT ]]; then
+    # The export is expected to fail and there is nothing else to
+    # be done. Return successfully.
+    check_coq_exports_end ${result} ""
+    return ${result}
+  elif [[ $cn_result -eq 0 && $FAIL_MODE -ne $FAIL_EXPORT ]]; then
+    : # Export succeeded, as expected, continue the build
+  else
+    # Otherwise fail
+    result=1
+    check_coq_exports_end ${result} "Unexpected return code during export: $cn_result"
+    return ${result}
+  fi
 
-    # The rest of the commands must be performed in the build directory 
-    pushd "$BUILD_DIR" > /dev/null
-    
-    # Create the Coq Makefile
-    # (We don't expect this to fail)
-    coq_makefile -f _CoqProject -o Makefile.coq > /dev/null
-
-    # Build the Coq files
-    make -f Makefile.coq > /dev/null  2>&1
-    # Check the result is as expected
-    local coq_result=$?
-    if [[ $coq_result -ne 0 && $FAIL_MODE -eq $FAIL_COQ_BUILD ]]; then
-	# The coq build is expected to fail and there is nothing else to
-	# be done. Return successfully.
-	check_coq_exports_end ${result} ""
-    elif [[ $coq_result -eq 0 && $FAIL_MODE -ne $FAIL_COQ_BUILD ]]; then
-	# Export succeeded, as expected
-        check_coq_exports_end ${result} ""
-    else
-        result=1
-	check_coq_exports_end ${result} "Unexpected return code during coq build: $coq_result"
-    fi
+  # The rest of the commands must be performed in the build directory 
+  pushd "$BUILD_DIR" > /dev/null
+  
+  # Create the Coq Makefile
+  # (We don't expect this to fail)
+  coq_makefile -f _CoqProject -o Makefile.coq > /dev/null
+
+  # Build the Coq files
+  make -f Makefile.coq > /dev/null  2>&1
+  # Check the result is as expected
+  local coq_result=$?
+  if [[ $coq_result -ne 0 && $FAIL_MODE -eq $FAIL_COQ_BUILD ]]; then
+    # The coq build is expected to fail and there is nothing else to
+    # be done. Return successfully.
+    check_coq_exports_end ${result} ""
+  elif [[ $coq_result -eq 0 && $FAIL_MODE -ne $FAIL_COQ_BUILD ]]; then
+    # Export succeeded, as expected
+    check_coq_exports_end ${result} ""
+  else
+    result=1
+    check_coq_exports_end ${result} "Unexpected return code during coq build: $coq_result"
+  fi
 
-    # At this point everythink built successfully.
+  # At this point everythink built successfully.
 
-    # Return to the directory where the script was called (from the
-    # build directory)
-    popd > /dev/null
+  # Return to the directory where the script was called (from the
+  # build directory)
+  popd > /dev/null
 
-    return ${result}    
+  return ${result}  
 }
 
 printf "== Check lemma export\n"
diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 805426a6..1e3a9698 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -27,46 +27,46 @@ To provide proofs or test individual examples, see below.
 
 ## Testing individual examples
 
-From this folder, to export lemmas from example `path/to/example.c`, do the following:
+From this folder, to export lemmas from example `path/to/EXAMPLENAME.c`, do the following:
 
 0. (optional) Check CN verification, without exporting lemmas, with
 
-   `cn path/to/example.c`
+  `cn path/to/EXAMPLENAME.c`
 
 1. Create a copy of the build folder with 
 
-	`rsync -a ../coq-build/ path/to/example-build`
-	
-	(note trailing `/` after the first directory). This
-   copies a template build folder that conveniently contains a
-   `_CoqProject` file and the CN coq library `CN_Lib.v`. If the folder
-   already excists, `rsync` just updates the files.
+  `rsync -a ../coq-build/ path/to/EXAMPLENAME-build`
+  
+  (note trailing `/` after the first directory). This
+  copies a template build folder that conveniently contains a
+  `_CoqProject` file and the CN coq library `CN_Lib.v`. If the folder
+  already exists, `rsync` just updates the files.
 2. Extract the lemmas with 
-   
-   `cn --lemmata=path/to/example-build/theories/ExportedLemmas.v path/to/example.c`
-   
-   This should create a new file
-   `path/to/example-build/theories/ExportedLemmas.v` with all the
-   exported types, definitions and lemmas from the file
-   `path/to/example.c`.
+  
+  `cn --lemmata=path/to/EXAMPLENAME-build/theories/ExportedLemmas.v path/to/EXAMPLENAME.c`
+  
+  This should create a new file
+  `path/to/EXAMPLENAME-build/theories/ExportedLemmas.v` with all the
+  exported types, definitions and lemmas from the file
+  `path/to/EXAMPLENAME.c`.
 3. Go to the build directory with 
 
-	`pushd path/to/example-build`
-	
-	This will also store your current location to return later.
+  `pushd path/to/EXAMPLENAME-build`
+  
+  This will also store your current location to return later.
 4. Create or update the Coq Makefile with 
 
-	`coq_makefile -f _CoqProject -o Makefile.coq`
-	
+  `coq_makefile -f _CoqProject -o Makefile.coq`
+  
 5. Build the Coq files with 
 
-	`make -f Makefile.coq`
-	
-	This should create `*.vo` files for every `*.v` file in the
-   `theories` directory.
+  `make -f Makefile.coq`
+  
+  This should create `*.vo` files for every `*.v` file in the
+  `theories` directory.
 6. Return to your starting folder with 
 
-	`popd`
+  `popd`
 
 To add proofs, after running the steps above, create a file `Proofs.v`
 in the `theories` folder, next to the generated

From 4ec30239475ce2359989e7bc18e7a7486049d040 Mon Sep 17 00:00:00 2001
From: septract <miked@galois.com>
Date: Thu, 11 Jul 2024 14:43:39 -0700
Subject: [PATCH 28/29] Readme tweaks

---
 src/example-archive/coq-lemmas/README.md | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/example-archive/coq-lemmas/README.md b/src/example-archive/coq-lemmas/README.md
index 1e3a9698..bde0add4 100644
--- a/src/example-archive/coq-lemmas/README.md
+++ b/src/example-archive/coq-lemmas/README.md
@@ -1,17 +1,22 @@
-## Examples
+# Coq Examples
 
 CN examples using lemmas that can be extracted to Coq. The examples
 are split into:
 
-- Trivial
-- Recursive (Not yet handled by the export)
+- Trivial - named `trivial-*.c`
+- Recursive - named `recursive-*.c` _(export for these examples is not supported by CN yet)_
+
+Some examples are accompanied by Coq proofs of the lemmas extracted from CN. These are stored as follows: 
+
+- Originating C file: `coq/working/EXAMPLENAME.c`
+- Coq proof: `coq/working/EXAMPLENAME-build/Proof.v` 
 
 See README in parent directory for directory organization details.
 
 ## Tools needed
 
 To build the generated Coq lemmas, you will need to [download and
-install Coq](download).
+install Coq](https://coq.inria.fr/download).
 
 ## Batch build
 

From 553f94f0e318df0801ab07ea91b926fc4b4edf7c Mon Sep 17 00:00:00 2001
From: septract <miked@galois.com>
Date: Thu, 11 Jul 2024 14:48:11 -0700
Subject: [PATCH 29/29] Deactivate CI for Coq to make the merge easier

---
 src/example-archive/check-all.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh
index d7e27562..8ac928ed 100755
--- a/src/example-archive/check-all.sh
+++ b/src/example-archive/check-all.sh
@@ -17,7 +17,7 @@ subdirs=(
   "Rust" 
   "SAW" 
   "simple-examples"
-  "coq-lemmas"
+  # "coq-lemmas"
 )
 FAILURE=0