Simple coq lemmas

src/example-archive/coq-lemmas/.gitignore

@@ -0,0 +1,9 @@
+build/**/*.vo
+build/**/*.vos
+build/**/*.vok
+build/**/*.glob
+build/**/*.aux
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+/build/.lia.cache

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
+- Recursive
+- Lists (WIP)
+- Advanced (WIP)
+
+## 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.
+
+```

src/example-archive/coq-lemmas/broken/error-cerberus/trivial-005.c

@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_and (u32 x)
+  requires true;
+  ensures x & x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}

src/example-archive/coq-lemmas/broken/error-cerberus/trivial-006.c

@@ -0,0 +1,10 @@
+/*@
+  lemma lem_bit_wise_or (u32 x)
+  requires true;
+  ensures x | x == x;
+@*/
+
+void trivial() 
+{
+  ; 
+}

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
+

src/example-archive/coq-lemmas/build/_CoqProject

@@ -0,0 +1,7 @@
+
+-Q theories CN_Lemmas
+
+theories/CN_Lib.v
+theories/ExportedLemmas.v
+
+

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.

src/example-archive/coq-lemmas/build/theories/ExportedLemmas.v

@@ -0,0 +1,6 @@
+(* build/theories/ExportedLemmas.v: generated lemma specifications from CN *)
+
+Require Import ZArith Bool.
+Require CN_Lemmas.CN_Lib.
+
+

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.
+
+

src/example-archive/coq-lemmas/inprogress/trivial-007.c

@@ -0,0 +1,16 @@
+#include <stdbool.h>
+/*@
+  predicate (bool) MyCondition (u32 x){
+    if (x > 4294967295u32){
+      return false;
+    } else {
+      return true; 
+    }
+  } 
+
+@*/
+
+void trivial() 
+{
+  ; 
+}

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() 
+{
+  ; 
+}

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;
+}

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;
+}

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;
+}

src/example-archive/coq-lemmas/working/trivial-001.c

@@ -0,0 +1,10 @@
+/*@
+  lemma lem_trivial ()
+  requires true;
+  ensures true; 
+@*/
+
+void lemma_1() 
+{
+  ; 
+}

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() 
+{
+  ; 
+}

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() 
+{
+  ; 
+}

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() 
+{
+  ; 
+}