Merge pull request #761 from PrincetonUniversity/adapt-coq8.19

Adapt to Coq 8.19 and CompCert 3.13.1

.github/workflows/coq-action.yml

@@ -21,20 +21,20 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         bit_size:
           - 32
           - 64
         make_target:
           - vst
         exclude:   
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
     steps:
@@ -53,7 +53,7 @@ jobs:
             endGroup
           install: |
             startGroup "Install dependencies"
-              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
+              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }}
               # Required by test2
               opam install -y coq-ext-lib
             endGroup
@@ -89,9 +89,9 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -104,10 +104,10 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
           - bit_size: 64

Makefile

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1 or-else 8.18.0
+COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)

aes/spec_AES256_HL.v

@@ -199,7 +199,7 @@ Definition KeyExpansion (k : list word) : list block :=
     let b1 := (w1, w2, w3, w4) in
 	let b2 := (w5, w6, w7, w8) in
 	b1 :: b2 :: (grow_key b1 b2 RCon)
-  | l => [] (* should not happen *)
+  | _ => [] (* should not happen *)
   end.
 
 (* AddRoundKey() described in section 5.1.4: it uses a block from the expanded key, xoring
@@ -299,7 +299,7 @@ Definition InverseKeyExpansion (k : list word) : list block :=
   match exp_key with
   (* don't apply inv mix columns to first round key either *)
   | k1 :: tl => k1 :: grow_inv_key tl
-  | ek => [] (* should not happen *)
+  | _ => [] (* should not happen *)
   end.
 
 (* Inverse cipher described in figure 15 *)
@@ -324,5 +324,5 @@ Fixpoint apply_inv_rounds (s: state) (ek: list block) : state :=
 Definition EqInvCipher (exp_key: list block) (init: state) : state :=
   match exp_key with
   | kb :: tl => apply_inv_rounds (AddRoundKey init kb) tl
-  | l => init (* should not happen *)
+  | _ => init (* should not happen *)
   end.

aes/verif_gen_tables_LL.v

@@ -265,19 +265,19 @@ Proof.
           - rewrite upd_Znth_diff.
               + assumption.
               + lia.
-              + replace (Zlength log) with 256 by assumption. apply pow3_range; lia.
+              + rewrite H2. apply pow3_range; lia.
               + intro E. change 0 with (Int.unsigned Int.zero) in E. apply unsigned_eq_eq in E.
                 symmetry in E. apply (pow3_not0 i E).
           - intros. assert (1 <= j < i \/ j = i) as C by lia. destruct C as [C | C].
             * rewrite upd_Znth_diff.
               + auto.
-              + replace (Zlength log) with 256 by assumption. apply pow3_range; lia.
-              + replace (Zlength log) with 256 by assumption. apply pow3_range; lia.
+              + rewrite H2. apply pow3_range; lia.
+              + rewrite H2. apply pow3_range; lia.
               + intro E. apply unsigned_eq_eq in E.
                 apply pow3_inj in E. unfold Zbits.eqmod in E. destruct E as [k E]. lia.
             * subst. rewrite upd_Znth_same.
               + reflexivity.
-              + replace (Zlength log) with 256 by assumption. apply pow3_range; lia.
+              + rewrite H2. apply pow3_range; lia.
           - intros. assert (0 <= j < i \/ j = i) as C by lia. destruct C as [C | C].
             * rewrite upd_Znth_diff by lia. auto.
             * subst. rewrite upd_Znth_same by lia. reflexivity.
@@ -449,23 +449,23 @@ Proof.
           by lia. destruct C as [C | C].
           { rewrite upd_Znth_diff.
             - auto.
-            - replace (Zlength rsb) with 256 by assumption. apply FSb_range.
-            - replace (Zlength rsb) with 256 by assumption. apply FSb_range.
+            - rewrite H6. apply FSb_range.
+            - rewrite H6. apply FSb_range.
             - intro HH. apply unsigned_eq_eq in HH.
               apply FSb_inj in HH; lia.
           }
           { subst j. rewrite upd_Znth_same.
             - repeat rewrite zero_ext_nop; try reflexivity; rewrite Int.unsigned_repr; rep_lia.
-            - replace (Zlength rsb) with 256 by assumption. apply FSb_range.
+            - rewrite H6. apply FSb_range.
           }
         + rewrite upd_Znth_diff.
           { auto. }
           { lia. }
-          { replace (Zlength rsb) with 256 by assumption. apply FSb_range. }
+          { rewrite H6. apply FSb_range. }
           { replace 99 with (Int.unsigned (Znth 0 FSb)) by reflexivity.
             intro HH. apply unsigned_eq_eq in HH. apply FSb_inj in HH; lia. }
         + rewrite upd_Znth_Zlength; [ lia | ].
-          replace (Zlength rsb) with 256 by reflexivity. apply FSb_range.
+          rewrite H6. apply FSb_range.
   }
 
   thaw Fr.

aes/verif_setkey_enc_LL.v

@@ -145,7 +145,7 @@ Proof.
     replace (4 * i)%Z with (i * 4)%Z by lia.
     assert (forall sh t gfs v1 v2 p, v1 = v2 -> field_at sh t gfs v1 p |-- field_at sh t gfs v2 p)
     as field_at_change_value. (* TODO floyd: this might be useful elsewhere *)
-    { intros. replace v1 with v2 by assumption. apply derives_refl. }
+    { intros. rewrite H0. apply derives_refl. }
     apply field_at_change_value.
     fold ((fun i0 => get_uint32_le key_chars (i0 * 4)) i).
    rewrite <- update_partially_filled by lia. f_equal. f_equal. 

hmacdrbg/HMAC_DRBG_nonadaptive.v

@@ -4385,7 +4385,7 @@ Proof.
       rewrite forNats_length.
       unfold Pr_collisions.
       eapply leRat_terms; intuition.
-      eapply Nat.pow_le_mono; lia.
+all:      eapply Nat.pow_le_mono; lia.  (* needed before Coq 8.19 *)
     + unfold PRG.compMap_v.
       rewrite compMap_hasDups_cons_prob.
       rewrite forNats_length.

msl/tree_shares.v

@@ -2040,7 +2040,7 @@ Module Share <: SHARE_MODEL.
          ( n < m -> False ) /\
          ( n > m -> shareTreeEq (union_tree tok fac) (Leaf true) -> False).
     Proof.
-      intros fac n H; induction H; simpl; intuition.
+      intros fac n H; induction H; simpl; intuition auto with *.
       subst m; inv H.
       simpl; auto.
       inv H.

sha/ByteBitRelations.v

@@ -2,7 +2,7 @@ Require Import compcert.lib.Coqlib.
 Require Import List. Import ListNotations.
 Require Import ZArith Lia.
 Require Import compcert.lib.Integers.          (* byte *)
-Require Import Coq.Numbers.Natural.Peano.NPeano.
+(*Require Import Coq.Numbers.Natural.Peano.NPeano.*)
 
 Require Import Coq.Strings.Ascii.
 Require Import Coq.Program.Tactics.

sha/HMAC256_equivalence.v

@@ -120,7 +120,7 @@ Proof.
            rewrite Heql in pf. apply Forall_inv in pf.  clear Heql.
            rewrite firstn_length in pf.
            symmetry in Heqd. apply leb_complete in Heqd.
-           eapply NPeano.Nat.min_l_iff in pf. lia.
+           eapply Nat.min_l_iff in pf. lia.
     rewrite splitAndPad_aux_consD.
     constructor.
       rewrite of_length_proof_irrel. trivial.
@@ -164,7 +164,7 @@ Lemma length_splitandpad_inner m :
      (splitAndPad_v m) (sha_splitandpad_blocks m).
 Proof. apply length_splitandpad_inner_aux. Qed.
 
-Lemma C: NPeano.Nat.divide 8 c.
+Lemma C: Nat.divide 8 c.
   exists 32%nat. reflexivity.
 Qed.
 
@@ -233,7 +233,7 @@ Module EQ256 <: EQUIV_Inst SHA256.
   Lemma D: (d * 32)%nat = b. reflexivity. Qed.
 
   Definition gap:list byte -> list int := SHA256.generate_and_pad.
-  Lemma GAP: forall bits, NPeano.Nat.divide d (length (gap (bitsToBytes bits))).
+  Lemma GAP: forall bits, Nat.divide d (length (gap (bitsToBytes bits))).
     intros. rewrite <- pad_compose_equal. apply gap_divide16. Qed.
 
   Lemma sap_gap: splitAndPad = fun bits => bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))).
@@ -269,7 +269,7 @@ End EQ256.
 Module EQ := HMAC_Equiv SHA256 EQ256.
 
 (* Note we're comparing to HP.HMAC_SHA256.HmacCore, not HMAC. *)
-Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> NPeano.Nat.divide 8 (length msg))
+Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> Nat.divide 8 (length msg))
       (kv : Bvector b) (m : HMAC_Abstract.Message P):
       Vector.to_list (HMAC_spec.HMAC EQ.h_v iv_v (HMAC_Abstract.wrappedSAP _ _ splitAndPad_v)
                       fpad_v EQ.opad_v EQ.ipad_v kv m) =

sha/HMAC256_isPRF.v

@@ -28,8 +28,8 @@ Proof. intros. do 2 rewrite <- splitAndPad_v_to_sha_splitandpad_blocks.
 Qed.
 
 Lemma splitAndPad_1to1 b1 b2 (B:splitAndPad_v b1 = splitAndPad_v b2)
-       (L1: NPeano.Nat.divide 8 (length b1))
-       (L2: NPeano.Nat.divide 8 (length b2)): b1 = b2.
+       (L1: PeanoNat.Nat.divide 8 (length b1))
+       (L2: PeanoNat.Nat.divide 8 (length b2)): b1 = b2.
 Proof. intros.
   apply splitAndPad_v_eq_inverse in B.
   unfold sha_splitandpad_blocks in B.
@@ -53,11 +53,11 @@ Qed.
 Module PARS256 <: HMAC_is_PRF_Parameters SHA256 EQ256.
 
   Parameter P : Blist -> Prop.
-  Parameter HP: forall m, P m -> NPeano.Nat.divide 8 (length m).
+  Parameter HP: forall m, P m -> PeanoNat.Nat.divide 8 (length m).
 
   Lemma splitAndPad_1to1: forall b1 b2 (B:EQ256.splitAndPad_v b1 = EQ256.splitAndPad_v b2)
-       (L1: NPeano.Nat.divide 8 (length b1))
-       (L2: NPeano.Nat.divide 8 (length b2)), b1 = b2.
+       (L1: PeanoNat.Nat.divide 8 (length b1))
+       (L2: PeanoNat.Nat.divide 8 (length b2)), b1 = b2.
    Proof. apply splitAndPad_1to1. Qed.
 End PARS256.
 

sha/HMAC256_spec_pad.v

@@ -62,7 +62,7 @@ Proof.
   apply bytes_bits_def_eq.
 Qed.
 
-Lemma gap_divide16 bits: NPeano.Nat.divide 16 (length (generate_and_pad' (bitsToBytes bits))).
+Lemma gap_divide16 bits: Nat.divide 16 (length (generate_and_pad' (bitsToBytes bits))).
 Proof.
     unfold generate_and_pad'.
     destruct (pad_len_64_nat (bitsToBytes bits)).

sha/HMAC_equivalence.v

@@ -24,7 +24,7 @@ Module Type EQUIV_Inst (HF:HP.HASH_FUNCTION).
 
 (*Section EQUIV.*)
   Parameter c:nat.
-  Parameter C: NPeano.Nat.divide 8 c.
+  Parameter C: Nat.divide 8 c.
   Parameter p:nat.
   Definition b := (c+p)%nat.
   Parameter B: (0<b)%nat.
@@ -88,7 +88,7 @@ Module Type EQUIV_Inst (HF:HP.HASH_FUNCTION).
   Parameter D: (d * 32)%nat = b.
 
   Parameter gap:list byte -> list int.
-  Parameter GAP: forall bits, NPeano.Nat.divide d (length (gap (bitsToBytes bits))).
+  Parameter GAP: forall bits, Nat.divide d (length (gap (bitsToBytes bits))).
   Parameter sap_gap: splitAndPad = fun bits => bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))).
 
   Parameter HASH: forall m, HF.Hash m = intlist_to_bytelist (hashblocks ir (gap m)).
@@ -189,7 +189,7 @@ Qed.
   apply BS_pos.
 Qed.
 
-Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> NPeano.Nat.divide 8 (length msg))
+Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> Nat.divide 8 (length msg))
       (kv : Bvector EQ.b) (m : HMAC_Abstract.Message P):
       Vector.to_list (HMAC_spec.HMAC h_v EQ.iv_v (HMAC_Abstract.wrappedSAP _ _ EQ.splitAndPad_v)
                       EQ.fpad_v opad_v ipad_v kv m) =

sha/HMAC_isPRF.v

@@ -68,11 +68,11 @@ Require Import hmacfcf.HMAC_PRF.
 
 Module Type HMAC_is_PRF_Parameters (HF:HP.HASH_FUNCTION) (EQ: EQUIV_Inst HF).
   Parameter P : Blist -> Prop.
-  Parameter HP: forall m, P m -> NPeano.Nat.divide 8 (length m).
+  Parameter HP: forall m, P m -> Nat.divide 8 (length m).
 
   Parameter splitAndPad_1to1: forall b1 b2 (B:EQ.splitAndPad_v b1 = EQ.splitAndPad_v b2)
-       (L1: NPeano.Nat.divide 8 (length b1))
-       (L2: NPeano.Nat.divide 8 (length b2)), b1 = b2.
+       (L1: Nat.divide 8 (length b1))
+       (L2: Nat.divide 8 (length b2)), b1 = b2.
 End HMAC_is_PRF_Parameters.
 
 Module HMAC_is_PRF (HF:HP.HASH_FUNCTION) (EQ: EQUIV_Inst HF) (PARS:HMAC_is_PRF_Parameters HF EQ).

sha/HMAC_spec_concat.v

@@ -78,7 +78,7 @@ Lemma h_star_eq :
   sha.HMAC_spec_pad.h_star = h_star.
 Proof. reflexivity. Qed.
 
-Theorem HMAC_concat_pad c p (C: NPeano.Nat.divide 8 c) B sap sap' fp
+Theorem HMAC_concat_pad c p (C: PeanoNat.Nat.divide 8 c) B sap sap' fp
         (sap_sap': forall l m, length l = (c+p)%nat ->
                           sap (l ++ m) = l ++ sap' m)
         (sap_appfpad: forall (l m : Blist),

sha/HMAC_spec_pad.v

@@ -269,7 +269,7 @@ Qed.
 
 Lemma equiv_pad shaiv shasplitandpad c p (B: (0< b c p)%nat) (DB32: (I.d*32 =b c p)%nat)
      ir (IVIR: shaiv = convert ir)
-       gap (GAP: forall bits, NPeano.Nat.divide I.d (length (gap (bitsToBytes bits))))
+       gap (GAP: forall bits, Nat.divide I.d (length (gap (bitsToBytes bits))))
        (sap_gap: forall bits, shasplitandpad bits = bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))))
        HASH
        (HSH: forall (m:list byte), HASH m = intlist_to_bytelist (I.hashblocks ir (gap m))):
@@ -303,7 +303,7 @@ Qed.
 Theorem HMAC_pad_concrete splitandpad c p (B: (0< b c p)%nat) (BS: (HF.BlockSize * 8)%nat = b c p)
         (DB32: (I.d*32 =b c p)%nat)
          ir (*ie initial_regs*) gap (*ie generate_and_pad*)
-         (GAP: forall bits, NPeano.Nat.divide I.d (length (gap (bitsToBytes bits))))
+         (GAP: forall bits, Nat.divide I.d (length (gap (bitsToBytes bits))))
          (sap_gap: forall bits, splitandpad bits = bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))))
          (HSH: forall (m:list byte), HF.Hash m = intlist_to_bytelist (I.hashblocks ir (gap m)))
          (K : list byte) (M H : list byte) (OP IP : byte)
@@ -347,7 +347,7 @@ Qed.
 Theorem HMAC_pad_concrete' splitandpad c p (B: (0< b c p)%nat) (BS: (HF.BlockSize * 8)%nat =b c p)
         (DB32: (I.d*32 =b c p)%nat)
          ir (*ie initial_regs*) gap (*ie generate_and_pad*)
-         (GAP: forall bits, NPeano.Nat.divide I.d (length (gap (bitsToBytes bits))))
+         (GAP: forall bits, Nat.divide I.d (length (gap (bitsToBytes bits))))
          (sap_gap: splitandpad = fun bits => bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))))
          (HSH: forall (m:list byte), HF.Hash m = intlist_to_bytelist (I.hashblocks ir (gap m)))
          (K : list byte) (M : list byte) (OP IP : byte)

sha/ShaInstantiation.v

@@ -136,7 +136,7 @@ Proof. unfold pad_inc.
    destruct H. rewrite H. clear H.
    assert (Z.to_nat (zz mod 64 - 1) = minus (Z.to_nat (zz mod 64)) 1).
      clear - n H0. remember (zz mod 64).  clear Heqz. rewrite Z2Nat.inj_sub. reflexivity. lia.
-   rewrite H; clear H. rewrite <- NPeano.Nat.add_sub_swap. rewrite <- Nat.sub_succ_l. simpl. exists k. lia.
+   rewrite H; clear H. rewrite <- Nat.add_sub_swap. rewrite <- Nat.sub_succ_l. simpl. exists k. lia.
    lia. apply (Z2Nat.inj_le 1). lia. lia. lia.
 Qed.
 

sha/pure_lemmas.v

@@ -105,7 +105,7 @@ exists (Z.to_nat i).
 rewrite Zlength_correct in H0.
 destruct (zeq n 0). subst.
 simpl. rewrite Z.mul_0_r in H0. destruct al; inv H0.
-rewrite mult_0_r. reflexivity.
+rewrite Nat.mul_0_r. reflexivity.
 assert (0 <= i).
 assert (0 <= i * n) by lia.
 apply Z.mul_nonneg_cancel_r in H1; auto; lia.
@@ -132,7 +132,7 @@ Proof.
 induction n; intros.
 destruct l; inv H; reflexivity.
 replace (S n) with (1 + n)%nat in H by lia.
-rewrite mult_plus_distr_l in H.
+rewrite Nat.mul_add_distr_l in H.
 destruct l as [|i0 l]; [ inv H |].
 destruct l as [|i1 l]; [ inv H |].
 destruct l as [|i2 l]; [ inv H |].
@@ -310,7 +310,7 @@ Qed.
 
 Theorem Zmod_mod_mult :
   forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
-  Zmod (Zmod n (a * b)) b = Zmod n b.
+  Z.modulo (Z.modulo n (a * b)) b = Z.modulo n b.
 Proof.
 intros n a [|b|b] Ha Hb.
 rewrite ?Z.mul_0_r.

sha/verif_hmac_crypto.v

@@ -30,7 +30,7 @@ Lemma key_vector l:
   length (bytesToBits (HMAC_SHA256.mkKey l)) = b.
 Proof. rewrite bytesToBits_len, hmac_common_lemmas.mkKey_length; reflexivity. Qed.
 
-Definition mkCont (l:list byte) : HMAC_spec_abstract.HMAC_Abstract.Message (fun x => x=bytesToBits l /\ NPeano.Nat.divide 8 (length x)).
+Definition mkCont (l:list byte) : HMAC_spec_abstract.HMAC_Abstract.Message (fun x => x=bytesToBits l /\ Nat.divide 8 (length x)).
 eapply exist. split. reflexivity.
 rewrite bytesToBits_len. exists (length l). trivial.
 Qed.

sha/verif_sha_bdo4.v

@@ -139,8 +139,9 @@ forward_call (* l = __builtin_read32_reversed(_data) *)
  autorewrite with sublist; lia.
 gather_SEP (array_at _ _ _ 0 _ _ data) (data_at _ _ _ (offset_val (i*4) data)) (array_at _ _ _ (i*4+4) _ _ data).
  match goal with |- context [SEPx (?A::_)] =>
-  replace A with (data_block sh (intlist_to_bytelist b) data)
-    by (rewrite H1,<- !sepcon_assoc; auto)
+  replace A with (data_block sh (intlist_to_bytelist b) data);
+   (* next line needed only before Coq 8.19 *)
+   try solve [rewrite H1,<- !sepcon_assoc; auto]
  end.
  clear H1.
 rewrite <- Znth_big_endian_integer by lia.