Fixed dependency versions

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

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}
 ]

theories/Common/dune

@@ -1,5 +1,5 @@
 (coq.theory
  (name CheriCaps.Common)
  (package coq-cheri-capabilities)
- (theories stdpp SailStdpp ExtLib)
+ (theories stdpp SailStdpp)
 )

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.
 

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.

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)
 )

theories/dune

@@ -2,5 +2,5 @@
 (coq.theory
  (name CheriCaps)
  (package coq-cheri-capabilities)
- (theories stdpp SailStdpp ExtLib)
+ (theories stdpp SailStdpp)
 )