Replace CoqSail (which uses bbv for bitvectors) with CoqSailStdpp

rems-project · Feb 9, 2024 · dde5d79 · dde5d79
1 parent 15ea240
commit dde5d79
Show file tree

Hide file tree

Showing 11 changed files with 1,245 additions and 175 deletions.
diff --git a/CoqMakefile b/CoqMakefile
diff --git a/CoqMakefile.conf b/CoqMakefile.conf
@@ -0,0 +1,71 @@
+# This configuration file was generated by running:
+# coq_makefile -f _CoqProject -o CoqMakefile
+
+COQBIN?=
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+COQMKFILE ?= "$(COQBIN)coq_makefile"
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_CMDLINE_VFILES := 
+COQMF_SOURCES := $(shell $(COQMKFILE) -sources-of -f _CoqProject $(COQMF_CMDLINE_VFILES))
+COQMF_VFILES := $(filter %.v, $(COQMF_SOURCES))
+COQMF_MLIFILES := $(filter %.mli, $(COQMF_SOURCES))
+COQMF_MLFILES := $(filter %.ml, $(COQMF_SOURCES))
+COQMF_MLGFILES := $(filter %.mlg, $(COQMF_SOURCES))
+COQMF_MLPACKFILES := $(filter %.mlpack, $(COQMF_SOURCES))
+COQMF_MLLIBFILES := $(filter %.mllib, $(COQMF_SOURCES))
+COQMF_METAFILE = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = 
+COQMF_SRC_SUBDIRS = 
+COQMF_COQLIBS =   -R theories CheriCaps
+COQMF_COQLIBS_NOML =  -R theories CheriCaps
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_COQLIB=/home/ricardo/.opam/coq-cheri-capabilities/lib/coq/
+COQMF_COQCORELIB=/home/ricardo/.opam/coq-cheri-capabilities/lib/coq/../coq-core/
+COQMF_DOCDIR=/home/ricardo/.opam/coq-cheri-capabilities/share/doc/
+COQMF_OCAMLFIND=/home/ricardo/.opam/coq-cheri-capabilities/bin/ocamlfind
+COQMF_CAMLFLAGS=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
+COQMF_WARN=-warn-error +a-3
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=boot config lib clib kernel library engine pretyping interp gramlib parsing proofs tactics toplevel printing ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/ltac2 plugins/micromega plugins/nsatz plugins/ring plugins/rtauto plugins/ssr plugins/ssrmatching plugins/syntax
+COQMF_COQ_NATIVE_COMPILER_DEFAULT=no
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Native compiler.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_COQPROJECTNATIVEFLAG = 
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = CheriCaps
diff --git a/_CoqProject b/_CoqProject
@@ -0,0 +1,8 @@
+# To use _CoqProject with VS Code + VsCoq extension, from the root directory of this file run
+## coq_makefile -f _CoqProject -o CoqMakefile
+## make -f CoqMakefile
+# and then code .
+
+-R theories CheriCaps
+
+theories
diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam
@@ -11,7 +11,7 @@ bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
   "dune" {>= "3.7"}
   "coq"
-  "coq-sail"
+  "coq-sail-stdpp"
   "coq-ext-lib"
   "coq-stdpp-unstable"
   "odoc" {with-doc}

diff --git a/dune-project b/dune-project
@@ -18,7 +18,7 @@
  )
  (depends 
  	(coq (< 8.17.0))
-  coq-sail
+  coq-sail-stdpp
   coq-ext-lib
   (coq-stdpp-unstable (= dev.2023-02-17.2.2d8ccea3))
  )

diff --git a/theories/Common/Utils.v b/theories/Common/Utils.v
@@ -11,7 +11,7 @@ Require Import Coq.Strings.Ascii.
 
 Import ListNotations.
 
-From Sail Require Import Values.
+From SailStdpp Require Import Values.
 
 Local Open Scope list_scope.
 Local Open Scope string_scope.
@@ -122,16 +122,6 @@ Fixpoint List_bool_eqb (l1:list bool) (l2:list bool) : bool :=
   | (_,[]) => false 
   | (h1::t1,h2::t2) => (Bool.eqb h1 h2) && List_bool_eqb t1 t2
   end.
-
-Fixpoint word_to_list_bool {n} w :=
-  match w with
-  | Word.WO => []
-  | Word.WS b w => b :: word_to_list_bool w
-  end.
-
-(* Stores less-significant bits in lower indices *)
-Definition mword_to_list_bool {n} (w : mword n) : list bool := 
-  word_to_list_bool (get_word w). 
 
 Definition string_of_bool (b:bool) :=
   match b with

diff --git a/theories/Morello/CapFns.v b/theories/Morello/CapFns.v
@@ -1,6 +1,6 @@
 (*Generated by Sail from capfns.*)
-Require Import Sail.Base.
-Require Import Sail.Real.
+Require Import SailStdpp.Base.
+Require Import SailStdpp.Real.
 From CheriCaps Require Import CapFnsTypes.
 Import ListNotations.
 Open Scope string.

diff --git a/theories/Morello/CapFnsTypes.v b/theories/Morello/CapFnsTypes.v
@@ -1,6 +1,6 @@
 (*Generated by Sail from capfns.*)
-Require Import Sail.Base.
-Require Import Sail.Real.
+Require Import SailStdpp.Base.
+Require Import SailStdpp.Real.
 Import ListNotations.
 Open Scope string.
 Open Scope bool.