Simple coq lemmas

.gitignore

@@ -1,2 +1,2 @@
 build/*
-/.vscode/
+/.vscode/

src/example-archive/.gitignore

@@ -0,0 +1,6 @@
+/**/coq/**/*-build/*
+/**/coq/**/*-build/theories/*
+
+!**/coq/**/*-build/
+!**/coq/**/*-build/theories/
+!**/coq/**/*-build/theories/Proofs.v

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  
 
@@ -25,6 +26,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

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

src/example-archive/check.sh

@@ -2,42 +2,44 @@
 
 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() {
   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
-    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" "$expected_exit_code"
-        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
 }
 
 failures=0
 
+# ====================
+# Check CN verification
+# ====================
+
 check_file() {
   local file=$1
   local expected_exit_code=$2
@@ -54,11 +56,113 @@ check_file() {
   fi
 }
 
-process_files "working" "*.c" check_file 0
+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
-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 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
+
+  # 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.
+
+  # 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
+
 
 if [[ "$failures" = 0 ]]
 then

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.

src/example-archive/coq-build/_CoqProject

@@ -0,0 +1,3 @@
+-R theories CN_Lemmas
+
+theories

src/example-archive/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.

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