Fix deprecations for Rocq 9

.github/workflows/coq-action.yml

@@ -21,19 +21,12 @@ 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.19'
-          - '8.20'
           - 'dev'
         bit_size:
           - 32
           - 64
         make_target:
           - vst
-        exclude:   
-          - coq_version: 8.19
-            bit_size: 32
-          - coq_version: dev
-            bit_size: 32
     steps:
       - uses: actions/checkout@v4
         with:
@@ -53,6 +46,7 @@ jobs:
               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
+              opam install -y coq-paco
             endGroup
           # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions
           before_script: |
@@ -88,8 +82,6 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.19'
-          - '8.20'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -102,10 +94,6 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.19
-            bit_size: 32
-          - coq_version: dev
-            bit_size: 32
           - bit_size: 64
             make_target: test3
           - bit_size: 32

Makefile

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1
+COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1 or-else 9.0.0 orelse 9.1.0 or-else 9.2+alpha
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)
@@ -303,6 +303,7 @@ CGFLAGS =  -DCOMPCERT -short-idents
 
 # ##### Interaction Trees Flags #####
 
+# as of 1 July 2025, coq-itree package seems not compatible with rocq 9.2+alpha, so still using submodule
 ifneq ($(wildcard InteractionTrees/theories),)
 EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
 endif
@@ -315,9 +316,10 @@ endif#
 
 # ##### PaCo (Parameterized Coinduction) Flags #####
 
-ifneq ($(wildcard paco/src),)
-EXTFLAGS:=$(EXTFLAGS) -Q paco/src Paco
-endif
+# the following commented out, because we get from opam instead of submodules
+# ifneq ($(wildcard paco/src),)
+# EXTFLAGS:=$(EXTFLAGS) -Q paco/src Paco
+# endif
 
 # ##### SSReflect Flags #####
 
@@ -327,7 +329,10 @@ endif
 
 # ##### Flag summary #####
 
-COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../paco/src Paco -Q ../coq-ext-lib/theories ExtLib -Q ../fcf/src/fcf FCF
+COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../fcf/src/fcf FCF
+
+# old version with paco, coq-ext-lib; we now obtain these from opam environment instead of submodules
+# COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS) $(SHIM) # -Q ../stdpp/theories stdpp -Q ../iris/iris iris -Q ../InteractionTrees/theories ITree -Q ../paco/src Paco -Q ../coq-ext-lib/theories ExtLib -Q ../fcf/src/fcf FCF
 
 
 DEPFLAGS:=$(COQFLAGS)
@@ -829,7 +834,7 @@ VST.config:
 
 # Note: doc files are installed into the coq destination folder.
 # This is not ideal but otherwise it gets tricky to handle variants
-install: VST.config
+install: VST.config vst
 	install -d "$(INSTALLDIR)"
 	for d in $(sort $(dir $(INSTALL_FILES) $(EXTRA_INSTALL_FILES))); do install -d "$(INSTALLDIR)/$$d"; done
 	for f in $(INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
@@ -923,15 +928,16 @@ endif
 # ifneq ($(wildcard coq-ext-lib/theories),)
 # 	$(COQDEP) -Q coq-ext-lib/theories ExtLib coq-ext-lib/theories >>.depend
 # endif
+
 ifneq ($(wildcard InteractionTrees/theories),)
-#	$(COQDEP) -Q coq-ext-lib/theories ExtLib -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
-	$(COQDEP) -Q paco/src Paco -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
+	$(COQDEP) -Q InteractionTrees/theories ITree InteractionTrees/theories >>.depend
 endif
+# the following commented out, because we get from opam instead of submodules
+# ifneq ($(wildcard paco/src),)
+# 	$(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend
+# endif
 ifneq ($(wildcard fcf/src/FCF),)
 	$(COQDEP) -Q fcf/src/FCF FCF fcf/src/FCF/*.v >>.depend
-endif
-ifneq ($(wildcard paco/src),)
-	$(COQDEP) -Q paco/src Paco paco/src/*.v >>.depend
 endif
 	wc .depend
 

Makefile.bundled

@@ -134,7 +134,7 @@ ifdef CLIGHTGEN
 VERSION1= $(lastword $(shell $(CLIGHTGEN) --version))
 VERSION2= $(subst version=,,$(shell grep version $(COMPCERT_SRC_DIR)/VERSION))
 ifneq ($(VERSION1),$(VERSION2))
-$(warning clightgen version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2))
+$(warning $(CLIGHTGEN) version $(VERSION1) does not match VST/compcert/VERSION $(VERSION2))
 endif
 endif
 

aes/list_utils.v

@@ -37,7 +37,7 @@ Qed.
 Lemma repeat_op_table_nat_length: forall {T: Type} (i: nat) (x: T) (f: T -> T),
   length (repeat_op_table_nat i x f) = i.
 Proof.
-  intros. induction i. reflexivity. simpl. rewrite app_length. simpl.
+  intros. induction i. reflexivity. simpl. rewrite length_app. simpl.
   rewrite IHi. lia.
 Qed.
 

atomics/SC_atomics_base.v

@@ -1,6 +1,6 @@
 (* SC atomics without importing Iris *)
 
-Require Import Ensembles.
+From Stdlib Require Import Ensembles.
 Require Import VST.veric.rmaps.
 Require Import VST.veric.compcert_rmaps.
 Require Import VST.concurrency.ghosts.

atomics/verif_hashtable1.v

@@ -1098,7 +1098,7 @@ Proof.
       rewrite Z2Nat.inj_add, repeat_plus by omega; simpl.
       rewrite !combine_app, map_app, sepcon_app; simpl.
       unfold atomic_entry, atomic_loc_hist; entailer!.
-      { rewrite combine_length, repeat_length, Zlength_correct, Nat2Z.id, Nat.min_l; auto.
+      { rewrite length_combine, repeat_length, Zlength_correct, Nat2Z.id, Nat.min_l; auto.
         apply Nat2Z.inj_le; rewrite <- !Zlength_correct; omega. }
       { apply Nat2Z.inj; rewrite <- !Zlength_correct; omega. }
   - Intros entries ghosts.

compcert/Makefile.config

@@ -6,7 +6,7 @@ SHAREDIR=$(PREFIX)/share
 COQDEVDIR=$(PREFIX)/lib/compcert/coq
 OCAML_NATIVE_COMP=true
 OCAML_OPT_COMP=true
-MENHIR_DIR=/Users/appel/.opam/coq8.19/lib/menhirLib
+MENHIR_DIR=/Users/appel/.opam/CP.2024.10.1~8.20~2025.01/lib/menhirLib
 COMPFLAGS=-bin-annot
 ABI=apple
 ARCH=aarch64
@@ -31,4 +31,4 @@ MODEL=default
 SYSTEM=macos
 RESPONSEFILE=gnu
 LIBRARY_FLOCQ=external
-LIBRARY_MENHIRLIB=local
+LIBRARY_MENHIRLIB=external

compcert/VERSION

@@ -1,4 +1,4 @@
-version=3.15
+version=3.16
 buildnr=
 tag=
 branch=

compcert/cfrontend/Clight.v

@@ -361,7 +361,7 @@ Variable e: env.
 Variable le: temp_env.
 Variable m: mem.
 
-(** [eval_expr ge e m a v] defines the evaluation of expression [a]
+(** [eval_expr ge e le m a v] defines the evaluation of expression [a]
   in r-value position.  [v] is the value of the expression.
   [e] is the current environment and [m] is the current memory state. *)
 

compcert/cfrontend/Cstrategy.v

@@ -16,23 +16,10 @@
 
 (** A deterministic evaluation strategy for C. *)
 
-Require Import Axioms.
-Require Import Classical.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
+From Coq Require Import Classical.
+Require Import Axioms Coqlib Errors Maps.
+Require Import Integers Floats Values AST Memory Events Globalenvs Smallstep.
+Require Import Ctypes Cop Csyntax Csem.
 
 Section STRATEGY.
 

compcert/common/AST.v

@@ -17,7 +17,7 @@
 (** This file defines a number of data types and operations used in
   the abstract syntax trees of many of the intermediate languages. *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib Maps Errors Integers Floats.
 Require Archi.
 
@@ -715,6 +715,25 @@ Inductive builtin_res (A: Type) : Type :=
   | BR_none
   | BR_splitlong (hi lo: builtin_res A).
 
+Definition eq_builtin_arg (A: Type) (eq: forall x y: A, {x=y} + {x<>y}) :
+  forall x y : builtin_arg A, {x=y} + {x<>y}.
+Proof.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec
+             chunk_eq ident_eq; intros.
+  decide equality.
+Defined.
+
+Definition eq_builtin_res (A: Type) (eq: forall x y: A, {x=y} + {x<>y}) :
+  forall x y : builtin_res A, {x=y} + {x<>y}.
+Proof.
+  decide equality.
+Defined.
+
+Arguments eq_builtin_arg {A}.
+Arguments eq_builtin_res {A}.
+
+Global Opaque eq_builtin_arg eq_builtin_res.
+
 Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
   match a with
   | BA_loadglobal chunk id ofs => id :: nil

compcert/common/Behaviors.v

@@ -16,13 +16,9 @@
 
 (** Whole-program behaviors *)
 
-Require Import Classical.
-Require Import ClassicalEpsilon.
+From Coq Require Import Classical ClassicalEpsilon.
 Require Import Coqlib.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Integers.
-Require Import Smallstep.
+Require Import Events Globalenvs Integers Smallstep.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.

compcert/common/Builtins.v

@@ -16,14 +16,21 @@
 
 (** Known built-in functions *)
 
-Require Import String Coqlib.
+From Coq Require Import String.
+Require Import Coqlib.
 Require Import AST Integers Floats Values.
 Require Export Builtins0 Builtins1.
 
 Inductive builtin_function : Type :=
   | BI_standard (b: standard_builtin)
   | BI_platform (b: platform_builtin).
 
+Definition eq_builtin_function: forall (x y: builtin_function), {x=y} + {x<>y}.
+Proof.
+  generalize eq_standard_builtin eq_platform_builtin; decide equality.
+Defined.
+Global Opaque eq_builtin_function.
+
 Definition builtin_function_sig (b: builtin_function) : signature :=
   match b with
   | BI_standard b => standard_builtin_sig b
@@ -36,6 +43,28 @@ Definition builtin_function_sem (b: builtin_function) : builtin_sem (sig_res (bu
   | BI_platform b => platform_builtin_sem b
   end.
 
+Lemma builtin_function_sem_inject: forall b vargs vres f vargs',
+  builtin_function_sem b vargs = Some vres ->
+  Val.inject_list f vargs vargs' ->
+  exists vres', builtin_function_sem b vargs' = Some vres' /\ Val.inject f vres vres'.
+Proof.
+  intros. exploit (bs_inject _ (builtin_function_sem b)); eauto.
+  unfold val_opt_inject; rewrite H; intro J.
+  destruct (builtin_function_sem b vargs') as [vres'|]; try contradiction.
+  exists vres'; auto.
+Qed.
+
+Lemma builtin_function_sem_lessdef: forall b vargs vres vargs',
+  builtin_function_sem b vargs = Some vres ->
+  Val.lessdef_list vargs vargs' ->
+  exists vres', builtin_function_sem b vargs' = Some vres' /\ Val.lessdef vres vres'.
+Proof.
+  intros. apply val_inject_list_lessdef in H0. 
+  exploit builtin_function_sem_inject; eauto.
+  intros (vres' & A & B). apply val_inject_lessdef in B.
+  exists vres'; auto.
+Qed.
+
 Definition lookup_builtin_function (name: string) (sg: signature) : option builtin_function :=
   match lookup_builtin standard_builtin_sig name sg standard_builtin_table with
   | Some b => Some (BI_standard b)

compcert/common/Builtins0.v

@@ -16,7 +16,8 @@
 
 (** Associating semantics to built-in functions *)
 
-Require Import String Coqlib.
+From Coq Require Import String.
+Require Import Coqlib.
 Require Import AST Integers Floats Values Memdata.
 Local Open Scope asttyp_scope.
 
@@ -383,6 +384,11 @@ Inductive standard_builtin : Type :=
   | BI_i64_stof
   | BI_i64_utof.
 
+Definition eq_standard_builtin: forall (x y: standard_builtin), {x=y} + {x<>y}.
+Proof.
+  generalize typ_eq; decide equality.
+Defined.
+
 Local Open Scope string_scope.
 
 Definition standard_builtin_table : list (string * standard_builtin) :=
@@ -440,7 +446,7 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
   | BI_i64_bswap =>
       [Xlong ---> Xlong]
   | BI_i16_bswap =>
-      [Xint ---> Xint]
+      [Xint16unsigned ---> Xint16unsigned]
   | BI_unreachable =>
       mksignature nil Xvoid cc_default
   | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
@@ -469,7 +475,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
   | BI_subl => mkbuiltin_v2t Xlong Val.subl _ _
   | BI_mull => mkbuiltin_v2t Xlong Val.mull' _ _
   | BI_i16_bswap =>
-    mkbuiltin_n1t Tint Xint
+    mkbuiltin_n1t Tint Xint16unsigned
                   (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n)))))
   | BI_i32_bswap =>
     mkbuiltin_n1t Tint Xint
@@ -522,6 +528,17 @@ Qed.
 Next Obligation.
   inv H; simpl; auto. inv H0; auto.
 Qed.
+Next Obligation.
+  set (bl := rev (encode_int 2 (Int.unsigned n))).
+  set (x := decode_int bl).
+  assert (length bl = 2%nat).
+  { unfold bl. rewrite List.rev_length. apply encode_int_length. }
+  assert (0 <= x < two_p 16).
+  { generalize (int_of_bytes_range (rev_if_be bl)). rewrite rev_if_be_length, H. auto. }
+  assert (two_p 16 < Int.max_unsigned) by (compute; auto).
+  apply Int.eqm_samerepr. rewrite Int.unsigned_repr by lia. rewrite Zbits.Zzero_ext_mod by lia.
+  apply Int.eqm_refl2. rewrite Z.mod_small; auto.
+Qed.
 Next Obligation.
   red. destruct v1; simpl; auto. destruct v2; auto. destruct orb; exact I.
 Qed.

compcert/common/Determinism.v

@@ -17,14 +17,9 @@
 (** Characterization and properties of deterministic external worlds
   and deterministic semantics *)
 
-Require Import String.
+From Coq Require Import String.
 Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Behaviors.
+Require Import AST Integers Events Globalenvs Smallstep Behaviors.
 
 (** * Deterministic worlds *)