From eb9e96a847369126c631485c8cf89c37a2dd5f18 Mon Sep 17 00:00:00 2001
From: Ricardo Almeida <3705908+ric-almeida@users.noreply.github.com>
Date: Tue, 11 Jun 2024 18:05:34 +0100
Subject: [PATCH] Fixed dependency versions

---
 README.md                       |  2 +-
 coq-cheri-capabilities.opam     |  3 +--
 theories/Common/dune            |  2 +-
 theories/Morello/Capabilities.v |  2 +-
 theories/Morello/MorelloTests.v | 17 +----------------
 theories/Morello/dune           |  2 +-
 theories/dune                   |  2 +-
 7 files changed, 7 insertions(+), 23 deletions(-)

diff --git a/README.md b/README.md
index 39f1b1f..534dcad 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,7 @@ Make sure to run `eval $(opam env --switch=coq-cheri-capabilities)` (or whicheve
 ```
 opam repo add --this-switch coq-released https://coq.inria.fr/opam/released
 opam repo add --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-opam pin -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git
+opam pin -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
 ```
 
 4. You may now install the opam package `coq-cheri-capabilities` and its dependencies with
diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam
index 1ff8a81..94872e2 100644
--- a/coq-cheri-capabilities.opam
+++ b/coq-cheri-capabilities.opam
@@ -6,14 +6,13 @@ maintainer: ["ricardo.almeida@ed.ac.uk"]
 authors: ["Ricardo Almeida" "Vadim Zaliva"]
 license: "BSD-3-clause"
 homepage: "https://github.com/rems-project/coq-cheri-capabilities"
-version: "20240610"
+version: "20240611"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
   "dune" {>= "3.7"}
   "coq"
   "coq-stdpp" { (= "dev") | (>= "dev.2022-12-05.0.0231fed2" & <= "dev.2024-03-11.0.a8c0c0f8") }
   "coq-sail-stdpp"
-  "coq-ext-lib"
   "coq-stdpp-unstable"
   "odoc" {with-doc}
 ]
diff --git a/theories/Common/dune b/theories/Common/dune
index 8f558d1..ea41660 100644
--- a/theories/Common/dune
+++ b/theories/Common/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name CheriCaps.Common)
  (package coq-cheri-capabilities)
- (theories stdpp SailStdpp ExtLib)
+ (theories stdpp SailStdpp)
 )
diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v
index f58dc71..aca9b02 100644
--- a/theories/Morello/Capabilities.v
+++ b/theories/Morello/Capabilities.v
@@ -5,7 +5,7 @@ Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.HexString.
 From Coq.Structures Require Import OrderedType OrderedTypeEx.
 
-From stdpp.unstable Require Import bitvector bitvector_tactics bitblast. 
+From stdpp Require Import bitvector bitblast bitvector_tactics.
 
 From SailStdpp Require Import Base Values Values_lemmas Operators_mwords MachineWord Operators_mwords MachineWordInterface.
 
diff --git a/theories/Morello/MorelloTests.v b/theories/Morello/MorelloTests.v
index 9b28778..be8cb87 100644
--- a/theories/Morello/MorelloTests.v
+++ b/theories/Morello/MorelloTests.v
@@ -6,27 +6,12 @@ Require Import Coq.Strings.Ascii.
 Require Import Coq.Strings.HexString.
 
 From stdpp.unstable Require Import bitvector bitvector_tactics. 
+From stdpp Require Import bitvector.
 From SailStdpp Require Import Values Operators_mwords.
 Require Import CapFns.
 
 From CheriCaps.Common Require Import Utils Addr Capabilities.
 
-Module tests_convertors.
-
-  (* Example converters_sound_1 : Z_to_bv 3 5 = mword_to_bv (bv_to_mword (Z_to_bv 3 5)).
-  Proof. vm_compute (Z_to_bv 3 5). Admitted. (*reflexivity. Qed. *)
-  Example converters_sound_2 : Z_to_bv 11 1000 = mword_to_bv (bv_to_mword'' (Z_to_bv 11 1000)).
-  Proof. Admitted. (*reflexivity. Qed. *)
-  Example converters_sound_3 : @mword_of_int 12 2049 = bv_to_mword'' (mword_to_bv (@mword_of_int 12 2049)).
-  Proof. vm_compute (mword_of_int 2049). vm_compute (mword_to_bv _). Admitted. (*reflexivity. Qed. *)
-  Definition max_value : Z := 680564733841876926926749214863536422911. (* 2^129 - 1 *)
-  Example converters_sound_4 : @mword_of_int 129 max_value = bv_to_mword (mword_to_bv (@mword_of_int 129 max_value)).
-  Proof. Admitted. (*reflexivity. Qed. *)
-  Example converters_sound_5 : Z_to_bv 129 max_value = mword_to_bv (bv_to_mword'' (Z_to_bv 129 max_value)).
-  Proof. Admitted. reflexivity. Qed. *)
-
-End tests_convertors. 
-
 Module test_cap_getters_and_setters.
 
   Import Capability.
diff --git a/theories/Morello/dune b/theories/Morello/dune
index c5ceb79..d19f4ee 100644
--- a/theories/Morello/dune
+++ b/theories/Morello/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name CheriCaps.Morello)
  (package coq-cheri-capabilities)
- (theories CheriCaps.Common stdpp SailStdpp ExtLib)
+ (theories CheriCaps.Common stdpp SailStdpp)
 )
diff --git a/theories/dune b/theories/dune
index 88d3b9f..fc6ce73 100644
--- a/theories/dune
+++ b/theories/dune
@@ -2,5 +2,5 @@
 (coq.theory
  (name CheriCaps)
  (package coq-cheri-capabilities)
- (theories stdpp SailStdpp ExtLib)
+ (theories stdpp SailStdpp)
 )