From 20d9d5ce2e982c4744ef6911a25a3be9307518f3 Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc-mak@users.noreply.github.com>
Date: Tue, 30 Jul 2024 23:17:13 +0100
Subject: [PATCH] CN: Fix lemmata tests (#454)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

These tests are not enabled in the CI yet (they should be, but I couldn't figure it out and I'm away for the next 1.5 weeks).

`as_auto_mutual_dt` was deleted because there's [a check in CN](https://github.com/rems-project/cerberus/blob/556171a17fca94b6aaf76bccfa7db63833428113/backend/cn/lib/wellTyped.ml#L2443-L2444) which prevents the indirect recursion used in [as_auto_mutual_dt/tree16.error.c](https://github.com/rems-project/cerberus/blob/master/tests/cn/tree16/as_auto_mutual_dt/tree16.error.c) from passing.

Tested with the following:
```sh
➜  coqc --version
The Coq Proof Assistant, version 8.19.2
compiled with OCaml 4.14.1
```
---
 tests/cn/mutual_rec/coq_lemmas/Makefile       |   2 +-
 .../cn/mutual_rec/coq_lemmas/theories/Setup.v |   2 +-
 .../as_auto_mutual_dt/coq_lemmas/Makefile     |   8 -
 .../as_auto_mutual_dt/coq_lemmas/_CoqProject  |   9 -
 .../coq_lemmas/theories/CN_Lib.v              | 174 ------------------
 .../coq_lemmas/theories/Inst_Spec.v           |  86 ---------
 .../coq_lemmas/theories/Setup.v               |  90 ---------
 .../tree16/as_mutual_dt/coq_lemmas/Makefile   |   2 +-
 .../tree16/as_partial_map/coq_lemmas/Makefile |   2 +-
 9 files changed, 4 insertions(+), 371 deletions(-)
 delete mode 100644 tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile
 delete mode 100644 tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject
 delete mode 100644 tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v
 delete mode 100644 tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v
 delete mode 100644 tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v

diff --git a/tests/cn/mutual_rec/coq_lemmas/Makefile b/tests/cn/mutual_rec/coq_lemmas/Makefile
index 28231021e..b248d3425 100644
--- a/tests/cn/mutual_rec/coq_lemmas/Makefile
+++ b/tests/cn/mutual_rec/coq_lemmas/Makefile
@@ -3,6 +3,6 @@
 
 all:
 	coq_makefile -f _CoqProject -o Makefile.coq
-	cn --lemmata theories/Gen_Spec.v ../mutual_rec.c
+	cn verify --lemmata theories/Gen_Spec.v ../mutual_rec.c
 	make -f Makefile.coq
 
diff --git a/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v b/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v
index 70976cbb6..3ed726ab0 100644
--- a/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v
+++ b/tests/cn/mutual_rec/coq_lemmas/theories/Setup.v
@@ -155,7 +155,7 @@ Lemma merge_flip: forall xs ys,
 Proof.
   intros.
   unfold merge.
-  rewrite plus_comm.
+  rewrite PeanoNat.Nat.add_comm.
   apply merge_w_flip.
   auto.
 Qed.
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile
deleted file mode 100644
index 07090e425..000000000
--- a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-
-
-
-all:
-	coq_makefile -f _CoqProject -o Makefile.coq
-	cn --lemmata theories/Gen_Spec.v ../tree16.c
-	make -f Makefile.coq
-
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject
deleted file mode 100644
index 012738ab4..000000000
--- a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/_CoqProject
+++ /dev/null
@@ -1,9 +0,0 @@
-
--Q theories CN_Lemmas
-
-theories/CN_Lib.v
-theories/Gen_Spec.v
-theories/Setup.v
-theories/Inst_Spec.v
-
-
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v
deleted file mode 100644
index 025f32e73..000000000
--- a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/CN_Lib.v
+++ /dev/null
@@ -1,174 +0,0 @@
-Require List.
-Require Import ZArith Bool.
-Open Scope Z.
-Require Import Lia.
-Require NArith.
-
-Fixpoint dec_list {A L_A : Type}
-    (dest : L_A -> option (A * L_A)) (xs : L_A) max_len :=
-  match max_len with
-    | 0%nat => List.nil
-    | S i => match dest xs with
-      | None => List.nil
-      | Some (y, ys) => List.cons y (dec_list dest ys i)
-    end
-  end.
-
-Fixpoint enc_list {A L_A : Type}
-    (nil_c : L_A) (cons_c : A -> L_A -> L_A) xs :=
-  match xs with
-    | List.nil => nil_c
-    | List.cons y ys => cons_c y (enc_list nil_c cons_c ys)
-  end.
-
-Definition nth_list_z {A L_A : Type}
-    dest (i : Z) (xs : L_A) (d : A) :=
-  if (i <? 0)%Z then d
-  else List.nth (Z.to_nat i) (dec_list dest xs (S (Z.to_nat i))) d.
-
-Definition array_to_list {A L_A : Type}
-    (nil_c : L_A) (cons_c : A -> L_A -> L_A)
-    arr i (n : Z) :=
-  if (n <? 0)%Z then nil_c
-  else enc_list nil_c cons_c (List.map (fun j => arr (i + (Z.of_nat j))) (List.seq 0 (Z.to_nat n))).
-
-Lemma enc_list_dec_list:
-  forall {A L_A} nil_c (cons_c : A -> L_A -> L_A) dest,
-  (dest nil_c = None) ->
-  (forall y ys, dest (cons_c y ys) = Some (y, ys)) ->
-  forall xs max_len,
-  dec_list dest (enc_list nil_c cons_c xs) max_len = List.firstn max_len xs.
-Proof.
-  intros until xs.
-  induction xs; intros; destruct max_len.
-  - auto.
-  - simpl.
-    rewrite H.
-    reflexivity.
-  - auto.
-  - simpl.
-    rewrite H0.
-    simpl.
-    rewrite IHxs.
-    auto.
-Qed.
-
-Lemma succ_ltb_mono:
-  forall i j,
-  (S i <? S j)%nat = (i <? j)%nat.
-Proof.
-  intros.
-  destruct (i <? j)%nat eqn: lt; destruct (S i <? S j)%nat eqn:S_lt.
-  - auto.
-  - rewrite Nat.ltb_lt in *; rewrite Nat.ltb_ge in *.
-    lia.
-  - rewrite Nat.ltb_lt in *; rewrite Nat.ltb_ge in *.
-    lia.
-  - auto.
-Qed.
-
-Lemma nth_firstn:
-  forall {A : Type} i j (xs : list A) d,
-  List.nth i (List.firstn j xs) d =
-  if (i <? j)%nat then List.nth i xs d else d.
-Proof.
-  intros until xs.
-  generalize i, j.
-  induction xs.
-  - intros.
-    destruct i0; destruct j0; simpl; try reflexivity.
-    rewrite Tauto.if_same.
-    reflexivity.
-  - intros.
-    destruct i0; destruct j0; simpl; try reflexivity.
-    rewrite IHxs.
-    rewrite succ_ltb_mono.
-    reflexivity.
-Qed.
-
-Lemma nth_map_if_d2:
-  forall {A B : Type} (d2 : A) i (f : A -> B) xs d,
-  List.nth i (List.map f xs) d =
-  if (i <? List.length xs)%nat then f (List.nth i xs d2) else d.
-Proof.
-  intros until i.
-  induction i.
-  - intros.
-    destruct xs; auto.
-  - intros.
-    destruct xs; simpl; try reflexivity.
-    rewrite IHi.
-    rewrite succ_ltb_mono.
-    reflexivity.
-Qed.
-
-Lemma array_to_list_nth_list:
-  forall {A L_A} (arr : Z -> A) nil_c (cons_c : A -> L_A -> L_A) dest,
-  (dest nil_c = None) ->
-  (forall y ys, dest (cons_c y ys) = Some (y, ys)) ->
-  forall (i : Z) n ix d,
-  nth_list_z dest ix (array_to_list nil_c cons_c arr i n) d =
-  if ((0 <=? ix) && (ix <? n))%Z
-  then arr (i + ix)
-  else d.
-Proof.
-  intros.
-  unfold nth_list_z, array_to_list.
-  rewrite Z.leb_antisym.
-  destruct (ix <? 0) eqn: ix_lt0;
-      destruct (n <? 0) eqn: n_lt0.
-  - auto.
-  - auto.
-  - simpl.
-    rewrite H.
-    assert ((ix <? n) = false) by lia.
-    rewrite H1.
-    assert (forall j, List.nth j nil d = d)
-      by (intros; destruct j; auto).
-    rewrite H2.
-    auto.
-  - rewrite enc_list_dec_list by auto.
-    rewrite nth_firstn.
-    assert (forall j, (j <? S j)%nat = true)
-      by (intros; rewrite Nat.ltb_lt; lia).
-    rewrite H1.
-    rewrite (nth_map_if_d2 0%nat).
-    rewrite List.seq_length.
-    destruct (ix <? n) eqn: ix_lt_n.
-    + assert ((Z.to_nat ix <? Z.to_nat n)%nat = true)
-        by (rewrite Nat.ltb_lt; lia).
-      rewrite H2.
-      simpl.
-      f_equal.
-      rewrite List.seq_nth by lia.
-      lia.
-    + assert ((Z.to_nat ix <? Z.to_nat n)%nat = false)
-        by (rewrite Nat.ltb_ge; lia).
-      rewrite H2.
-      auto.
-Qed.
-
-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/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v
deleted file mode 100644
index ee1c774d7..000000000
--- a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Inst_Spec.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(* Instantiation of the CN-exported specification
-   using results from the prior theories. *)
-
-Require Import ZArith Bool Lia.
-Require Import CN_Lemmas.Setup.
-Require Import CN_Lemmas.Gen_Spec.
-Import CN_Lemmas.Gen_Spec.Types.
-Require Import List.
-Import ListNotations.
-Module Inst.
-
-  Definition tree_v := Setup.tree_v.
-
-  Definition in_tree := Setup.in_tree.
-  
-End Inst.
-
-Module Defs := CN_Lemmas.Gen_Spec.Defs (Inst).
-
-Module Proofs.
-
-(* now prove lemmas *)
-Import Defs Inst.
-Open Scope Z.
-
-Lemma z_to_nat_eq_0:
-  forall (z : Z), z <= 0 -> Z.to_nat z = 0%nat.
-Proof.
-  lia.
-Qed.
-
-Lemma arc_from_array_step:
-  forall arr i len, arc_from_array (arr, i, len) =
-  match (len <=? i) with
-  | true => []
-  | false => arr i :: arc_from_array (arr, i + 1, len)
-  end.
-Proof.
-  intros.
-  destruct (len <=? i) eqn: le.
-  - simpl.
-    assert (Z.to_nat (len - i) = 0%nat) as eq by lia.
-    rewrite eq.
-    auto.
-  - simpl.
-    assert (Z.to_nat (len - i) = S (Z.to_nat (len - (i + 1)))) as eq by lia.
-    rewrite eq.
-    auto.
-Qed.
-
-Lemma in_tree_tree_v_lemma : in_tree_tree_v_lemma_type.
-Proof.
-  unfold in_tree_tree_v_lemma_type.
-  intros.
-  destruct arc as [arr_i len].
-  destruct arr_i as [arr i].
-  simpl in H, H0.
-  repeat (apply conj).
-  - unfold tree_v, Setup.tree_v.
-    rewrite (arc_from_array_step _ i).
-    rewrite Z.leb_antisym.
-    cbn.
-    destruct (i <? len) eqn: path_end.
-    + rewrite CN_Lib.wrapI_idem by lia.
-      destruct t; auto.
-    + destruct t; auto.
-  - unfold in_tree, Setup.in_tree.
-    rewrite (arc_from_array_step _ i).
-    rewrite Z.leb_antisym.
-    cbn.
-    destruct (i <? len) eqn: path_end.
-    + rewrite CN_Lib.wrapI_idem by lia.
-      destruct t; auto.
-    + destruct t; auto.
-Qed.
-
-End Proofs.
-
-Module InstOK: CN_Lemmas.Gen_Spec.Lemma_Spec(Inst).
-
-  Module D := CN_Lemmas.Gen_Spec.Defs (Inst).
-
-  Include Proofs.
-
-End InstOK.
-
diff --git a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v b/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v
deleted file mode 100644
index f412fc2e6..000000000
--- a/tests/cn/tree16/as_auto_mutual_dt/coq_lemmas/theories/Setup.v
+++ /dev/null
@@ -1,90 +0,0 @@
-(* Setup of consts and lemmas for lemmas *)
-
-Require Import ZArith Bool.
-Require CN_Lemmas.Gen_Spec CN_Lemmas.CN_Lib.
-Import CN_Lemmas.Gen_Spec.Types.
-Require Import List.
-Import ListNotations.
-Open Scope Z.
-Require Import Lia.
-
-Fixpoint to_list (xs : list_of_tree) : list tree :=
-  match xs with
-  | Nil_of_tree => []
-  | Cons_of_tree y ys => y :: to_list ys
-  end.
-
-Fixpoint of_list (xs : list tree) : list_of_tree :=
-  match xs with
-  | [] => Nil_of_tree
-  | y :: ys => Cons_of_tree y (of_list ys)
-  end.
-
-Lemma to_list_of_list:
-  forall xs, to_list (of_list xs) = xs.
-Proof.
-  intro.
-  induction xs.
-  + auto.
-  + simpl.
-    rewrite IHxs.
-    auto.
-Qed.
-
-Fixpoint get_array_elts {A : Type} (arr : Z -> A) (i : Z) (n : nat) : list A :=
-  match n with
-  | 0%nat => []
-  | S n2 => arr i :: get_array_elts arr (i + 1) n2
-  end.
-
-Lemma nth_get_array_elts:
-  forall {A} (arr : Z -> A) i n ix d, (ix < n)%nat ->
-  nth ix (get_array_elts arr i n) d = arr (i + Z.of_nat ix).
-Proof.
-  intros until n.
-  generalize i.
-  induction n.
-  - intros.
-    lia.
-  - intros.
-    simpl.
-    destruct ix.
-    + f_equal.
-      lia.
-    + simpl.
-      rewrite IHn by lia.
-      f_equal.
-      lia.
-Qed.
-
-Definition arc_in_array : Type := ((Z -> Z) * Z * Z).
- 
-Definition arc_from_array (arc : arc_in_array) :=
-  match arc with
-  | (arr, i, j) => get_array_elts arr i (Z.to_nat (j - i))
-  end.
-
-Definition array_to_list (arr : Z -> tree) (n : Z) :=
-  of_list (get_array_elts arr 0 (Z.to_nat n)).
-
-Fixpoint lookup_tree (t : tree) (arc : list Z) : option Z :=
-  match t with
-  | Empty_Tree => None
-  | Node ts v => match arc with
-    | [] => Some v
-    | ix :: ixs => lookup_tree (CN_Lib.nth_list_z dest_list_of_tree ix ts Empty_Tree) ixs
-    end
-  end.
-
-Definition in_tree (t : tree) (arc : arc_in_array) : bool :=
-  match lookup_tree t (arc_from_array arc) with
-  | Some _ => true
-  | None => false
-  end.
-
-Definition tree_v (t : tree) (arc : arc_in_array) : Z :=
-  match lookup_tree t (arc_from_array arc) with
-  | Some v => v
-  | None => 0
-  end.
-
diff --git a/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile b/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile
index 07090e425..64c061784 100644
--- a/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile
+++ b/tests/cn/tree16/as_mutual_dt/coq_lemmas/Makefile
@@ -3,6 +3,6 @@
 
 all:
 	coq_makefile -f _CoqProject -o Makefile.coq
-	cn --lemmata theories/Gen_Spec.v ../tree16.c
+	cn verify --lemmata theories/Gen_Spec.v ../tree16.c
 	make -f Makefile.coq
 
diff --git a/tests/cn/tree16/as_partial_map/coq_lemmas/Makefile b/tests/cn/tree16/as_partial_map/coq_lemmas/Makefile
index 355da494f..f3f0a1b03 100644
--- a/tests/cn/tree16/as_partial_map/coq_lemmas/Makefile
+++ b/tests/cn/tree16/as_partial_map/coq_lemmas/Makefile
@@ -3,6 +3,6 @@
 
 all:
 	coq_makefile -f _CoqProject -o Makefile.coq
-	cn ../tree16.c --lemmata theories/Gen_Spec.v
+	cn verify ../tree16.c --lemmata theories/Gen_Spec.v
 	make -f Makefile.coq