Release new version

Dockerfile

@@ -1,5 +1,5 @@
 ARG BASE_TAG="latest"
-FROM coqorg/coq:8.16.1-ocaml-4.14.1-flambda
+FROM coqorg/coq:8.18.0-ocaml-4.14.2-flambda
 
 COPY --chown=coq . /artifact/axsl
 WORKDIR /artifact
@@ -9,19 +9,20 @@ RUN sudo apt-get update && sudo apt-get install zlib1g-dev -y
 
 RUN eval $(opam env --set-switch) \
     && opam update -y -u \
-    && opam config list && opam repo list && opam list \
-    && opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+    && opam config list && opam repo list && opam list
+    # Uncomment below to use dev stdpp and Iris
+    #\ && opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+RUN opam install axsl/. --deps-only -y
 
 RUN git clone https://github.com/rems-project/coq-sail \
     && cd coq-sail \
-    && git checkout aeca2c5 \
+    && git checkout 5150697 \
     && opam pin . -y
 
-RUN opam install axsl/. --deps-only -y
-
 RUN git clone https://github.com/tchajed/iris-named-props.git \
     && cd iris-named-props \
-    && git checkout 327119f \
+    && git checkout a890750 \
     && opam pin . -y
 
 RUN opam list \

INSTALL.md

@@ -1,24 +1,23 @@
-# Building from scratch
-
 ## Compiling the development with Docker
 
 We recommend compiling the development using Docker. To do this,
 
 1. Make sure you have [Docker](https://docs.docker.com/get-docker/) installed.
-2. Run `docker build -t="axsl:popl" .` in the source code directory (which contains a `Dockerfile`) 
-to build the Docker image.
+2. Run `docker build -t="axsl:popl" .` to build the Docker image.
 
 The building process may take up to one hour, including installing dependencies and compilation. 
 
-Optionally, you can follow this by executing `docker run -i -t axsl:popl` to start a container with
-the freshly built image and access an interactive shell inside it.
+Optionally, you can follow this by executing `docker run -i -t axsl:popl` to start a container with the freshly built image and access
+an interactive shell inside it.
 
 ### Troubleshooting
 
 In order to build the development, you might have to increase the amount of
-memory allocated to a running Docker container. For instructions, see
+memory allocated to a running Docker container. For
+instructions, see
 [here](https://stackoverflow.com/questions/44533319/how-to-assign-more-memory-to-docker-container).
 
+
 ## Manually Installing with opam
 
 ### Opam and ocaml
@@ -42,9 +41,9 @@ opam install dune
 
 ### Coq
 
-Install Coq `8.16.1`
+Install Coq `8.18.0`
 ```
-opam pin coq 8.16.1
+opam pin coq 8.18.0
 ```
 
 ### Coq libraries
@@ -56,14 +55,15 @@ You need to add the iris opam repository to install Iris and stdpp :
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 ```
 
-This development uses a development version of Iris and stdpp:
+This development uses Iris 4.2.0:
 ```
-opam install coq-iris.dev.2023-08-11.1.81f394da -y
+opam install coq-iris.4.2.0 -y
 ```
 
-This development uses an unstable extension of `stdpp`: 
+This development uses `stdpp` and `stdpp-bitvector` 1.10.0: 
 ```
-opam install coq-stdpp-unstable.dev.2023-08-03.3.4be5fd62 -y
+opam install coq-stdpp.1.10.0 -y
+opam install coq-stdpp-bitvector.1.10.0 -y
 ```
 
 #### iris-named-props

coq-iris-axiomatic-arm.opam

@@ -1,22 +1,13 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-maintainer: ["Zongyuan Liu <[email protected]>"]
-authors: [
-  "Zongyuan Liu <[email protected]>"
-  "Angus Hammond <[email protected]>"
-  "Jean Pichon-Pharabod <[email protected]>"
-  "Thibaut Pérami <[email protected]>"
-]
-homepage: "https://github.com/logsem/AxSL"
-bug-reports: "https://github.com/logsem/AxSL/issues"
 depends: [
   "dune" {>= "3.9"}
-  "coq" {= "8.16.1"}
-  "coq-record-update" {= "0.3.2"}
-  "coq-hammer-tactics" {= "1.3.2+8.16"}
-  "coq-stdpp" {= "dev.2023-08-03.3.4be5fd62"}
-  "coq-stdpp-unstable" {= "dev.2023-08-03.3.4be5fd62"}
-  "coq-iris" {= "dev.2023-08-11.1.81f394da"}
+  "coq" {= "8.18.0"}
+  "coq-record-update" {= "0.3.3"}
+  "coq-hammer-tactics" {= "1.3.2+8.18"}
+  "coq-stdpp" {= "1.10.0"}
+  "coq-stdpp-bitvector" {= "1.10.0"}
+  "coq-iris" {= "4.2.0"}
   "odoc" {with-doc}
 ]
 build: [
@@ -33,4 +24,3 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/logsem/AxSL.git"

coqc-timing.sh

@@ -0,0 +1,21 @@
+#!/bin/bash
+# based on a script from the RefinedC project:
+# https://gitlab.mpi-sws.org/iris/refinedc/-/blob/master/tools/coqc_timing.sh?ref_type=heads
+
+set -e
+
+# Wrapper for coqc that is used when running the perf script in the CI.
+# Variable TIMECMD is expected to contain an absolute path to the perf script.
+# If TIMECMD is not set (or empty), fallback to just calling coqc.
+# we need to use opam exec -- coqc to get the coqc installed by opam, not this script
+# If PROFILE is set, generate a profile in the $PROFILE file (relative to the root of the repo).
+
+## use time if available
+if env time echo >/dev/null 2>/dev/null; then
+   export TIMECMD="time"
+fi
+
+# This file is in "_build/default/tools"
+REPO_DIR="$(dirname $(readlink -f $0))/../../"
+
+opam exec -- ${TIMECMD} coqc "$@"

dune

@@ -0,0 +1,5 @@
+; Add project-wide flags here.
+(env
+ (dev
+  (binaries (coqc-timing.sh as coqc))
+  (flags :standard)))

dune-project

@@ -4,27 +4,15 @@
 
 (generate_opam_files true)
 
-(authors
- "Zongyuan Liu <[email protected]>"
- "Angus Hammond <[email protected]>"
- "Jean Pichon-Pharabod <[email protected]>"
- "Thibaut Pérami <[email protected]>")
-
-(maintainers
- "Zongyuan Liu <[email protected]>")
-
-(source
- (github logsem/AxSL))
-
 (package
   (name coq-iris-axiomatic-arm)
   (allow_empty)
   (depends
-    (coq (= 8.16.1))
-    (coq-record-update (= 0.3.2))
-    (coq-hammer-tactics (= "1.3.2+8.16"))
-    (coq-stdpp (= "dev.2023-08-03.3.4be5fd62"))
-    (coq-stdpp-unstable (= "dev.2023-08-03.3.4be5fd62"))
-    (coq-iris (= "dev.2023-08-11.1.81f394da"))
+    (coq (= 8.18.0))
+    (coq-record-update (= 0.3.3))
+    (coq-hammer-tactics (= "1.3.2+8.18"))
+    (coq-stdpp (= "1.10.0"))
+    (coq-stdpp-bitvector (= "1.10.0"))
+    (coq-iris (= "4.2.0"))
   )
 )

system-semantics/Common/CBase.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -52,7 +52,7 @@ Require Import ZArith.
 
 (** Functional pipe notation.
 
-    Currently parsing level is just below relation so
+    TODO figure out a correct parsing level. Currently is just below relation so
     that a = b |> f will be parsed as a = (b |> f). *)
 Notation "v |> f" := (f v) (at level 69, only parsing, left associativity).
 

system-semantics/Common/CBitvector.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -41,8 +41,8 @@
     The module will attempt to provide smooth interoperability between the two *)
 
 Require Import Lia.
-Require Export stdpp.unstable.bitvector.
-Require Export stdpp.unstable.bitvector_tactics.
+Require Export stdpp.bitvector.definitions.
+Require Export stdpp.bitvector.tactics.
 Require Export bbv.Word.
 Require Import CBase.
 Require Import CBool.
@@ -450,6 +450,7 @@ Ltac remove_words :=
 (* Full bitvector simplification for both word and bv, contrary to bv_simplify,
    it does not move the goal to Z. Equalities in bv will stay in bv *)
 Ltac bv_word_simp :=
+  (* TODO maybe move to rewrite_strat if quantifier rewriting is needed *)
   repeat (autorewrite with bv word transport arith in *;
           try bv_to_word_to_bv;
           try word_to_bv_to_word).
@@ -493,6 +494,9 @@ Ltac bv_word_solve :=
   end; bv_word_solve'.
 
 
+
+(* TODO improve performance *)
+
 (*** Convert word operation to bv operations ***)
 
 Lemma word_to_bv_ZToWord n z :
@@ -557,6 +561,7 @@ Qed.
 
 
 (* This section might be upstreamed to stdpp. *)
+(* TODO add bv_solve support for this section *)
 
 (* Give minimal number of block of size n to cover m
 

system-semantics/Common/CBool.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -127,7 +127,10 @@ Notation "x =? y" := (bool_decide (x = y)) (at level 70, no associativity)
     : stdpp_scope.
 
 (** Convert automatical a Decidable instance (Coq standard library) to
-    a Decision instance (stdpp) *)
+    a Decision instance (stdpp)
+
+    TODO: Decide (no pun intended) if we actually want to use Decidable or
+    Decision in this development. *)
 Global Instance Decidable_to_Decision P `{dec : Decidable P} : Decision P :=
   match dec with
   | {| Decidable_witness := true; Decidable_spec := spec |} =>

system-semantics/Common/CInduction.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -93,6 +93,7 @@ Ltac instanciate_as_found e :=
    If someone finds a Ltac hack to have exactly the same semantics for any
    number of arguments, Please replace and check that everything depending still
    builds *)
+(* TODO make it recursive *)
 Ltac pattern_for H :=
   lazymatch (type of H) with
   | _ ?a ?b ?c =>

system-semantics/Common/CList.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -53,6 +53,8 @@ Qed.
 
 (*** List simplification ***)
 
+(* TODO all list simplification about x ∈ l should be superseded by set_unfold *)
+
 (** Automation for list simplifications *)
 Tactic Notation "list_simp" "in" "|-*" :=
   rewrite_strat topdown hints list.
@@ -104,6 +106,7 @@ Qed.
 Lemma Permutation_elem_of A (l l' : list A) x: l ≡ₚ l' → x ∈ l → x ∈ l'.
 Proof. setoid_rewrite elem_of_list_In. apply Permutation_in. Qed.
 
+(* TODO add some standard proof search for NoDup *)
 Global Instance set_unfold_list_permutation A (l l' : list A) P Q:
   TCFastDone (NoDup l) ->
   TCFastDone (NoDup l') ->
@@ -162,6 +165,7 @@ Qed.
 
 (*** List as sets ***)
 
+(* TODO make a PR to stdpp with this: *)
 Global Instance list_omap : OMap listset := λ A B f '(Listset l),
     Listset (omap f l).
 

system-semantics/Common/CMaps.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)

system-semantics/Common/CSets.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)

system-semantics/Common/Common.v

@@ -1,8 +1,8 @@
 (*                                                                               *)
 (*  BSD 2-clause License                                                         *)
 (*                                                                               *)
-(*  This applies to all files in this archive except where                       *)
-(*  specified otherwise.                                                         *)
+(*  This applies to all files in this archive except folder                      *)
+(*  "armv9-instantiation-types" or where specified otherwise.                    *)
 (*                                                                               *)
 (*  Copyright (c) 2022                                                           *)
 (*    Thibaut Pérami                                                             *)
@@ -122,6 +122,11 @@ Create HintDb vec discriminated.
 
 (*** Finite decidable quantifiers ***)
 
+(* TODO maybe express with a decidable instance instead : There are consequences
+   for extraction though
+   TODO: That is the new plan now: move everything to Decision.
+ *)
+
 Definition fforallb `{Finite A} (P : A -> bool) : bool :=
   forallb P (enum A).
 
@@ -151,6 +156,7 @@ Qed.
 
 (*** Finite number utilities *)
 
+(* TODO upstream to stdpp *)
 Bind Scope fin_scope with fin.
 
 (* stdpp provides notation from 0 to 10. We need them up to 30 for