diff --git a/coq/CheriMemory/CheriMemory.v b/coq/CheriMemory/CheriMemory.v
index bf826661c..019c95344 100644
--- a/coq/CheriMemory/CheriMemory.v
+++ b/coq/CheriMemory/CheriMemory.v
@@ -3,22 +3,18 @@ Require Import Coq.Numbers.BinNums.
 Require Import Coq.ZArith.Zcompare.
 Require Import Coq.Floats.PrimFloat.
 From Coq.Strings Require Import String Ascii HexString.
-Require Import Coq.FSets.FMapAVL.
-Require Import Coq.Structures.OrderedTypeEx.
-Require Coq.Program.Wf.
-Require Recdef.
 Require Import Lia.
 
 From ExtLib.Data Require Import List.
 From ExtLib.Structures Require Import Monad Monads MonadExc MonadState Traversable.
 From ExtLib.Data.Monads Require Import EitherMonad OptionMonad.
 
-From Coq.Lists Require Import List ListSet. (* after exltlib *)
+From Coq.Lists Require Import List. (* after exltlib *)
 
 From CheriCaps.Morello Require Import Capabilities.
 From CheriCaps.Common Require Import Capabilities.
 
-From Common Require Import SimpleError Utils.
+From Common Require Import SimpleError Utils ZMap.
 From Morello Require Import CapabilitiesGS MorelloCapsGS.
 
 Require Import Memory_model CoqMem_common ErrorWithState CoqUndefined ErrorWithState CoqLocation CoqSymbol CoqImplementation CoqTags CoqSwitches CerbSwitches CoqAilTypesAux.
@@ -33,8 +29,6 @@ Require Import AltBinNotations.
 Import ListNotations.
 Import MonadNotation.
 
-Module ZMap := FMapAVL.Make(Z_as_OT).
-
 Module CheriMemory
   (C:CAPABILITY_GS
        (AddressValue)
@@ -388,70 +382,6 @@ Module CheriMemory
         if is_signed then unwrap_cap_value n else n
     end.
 
-  Fixpoint zmap_range_init {T} (a0:Z) (n:nat) (step:Z) (v:T) (m:ZMap.t T) : ZMap.t T
-    :=
-    match n with
-    | O => m
-    | S n =>
-        let m := ZMap.add (Z.add a0 (Z.mul (Z.of_nat n) step)) v m in
-        zmap_range_init a0 n step v m
-    end.
-
-  (* TODO: see if could be generalized and moved to Utils.v.  *)
-  Definition zmap_update_element
-    {A:Type}
-    (key: Z)
-    (v: A)
-    (m: ZMap.t A)
-    : (ZMap.t A)
-    :=
-    ZMap.add key v (ZMap.remove key m).
-
-  (* TODO: see if could be generalized and moved to Utils.v.  *)
-  (** [update key f m] returns a map containing the same bindings as
-  [m], except for the binding of [key]. Depending on the value of [y]
-  where [y] is [f (find_opt key m)], the binding of [key] is added,
-  removed or updated. If [y] is [None], the binding is removed if it
-  exists; otherwise, if [y] is [Some z] then key is associated to [z]
-  in the resulting map. *)
-  Definition zmap_update
-    {A:Type}
-    (key: Z)
-    (f: option A -> option A)
-    (m: ZMap.t A)
-    : (ZMap.t A)
-    :=
-    let y := f (ZMap.find key m) in
-    let m' := ZMap.remove key m in (* could be optimized, as removal may be unecessary in some cases *)
-    match y with
-    | None => m'
-    | Some z => ZMap.add key z m'
-    end.
-
-  Definition zmap_sequence
-    {A: Type}
-    {m: Type -> Type}
-    {M: Monad m}
-    (mv: ZMap.t (m A)): m (ZMap.t A)
-    :=
-    let fix loop (ls: list (ZMap.key*(m A))) (acc:ZMap.t A) : m (ZMap.t A) :=
-      match ls with
-      | [] => ret acc
-      | (k,mv)::ls => mv >>= (fun v => loop ls (ZMap.add k v acc))
-      end
-    in
-    loop (ZMap.elements mv) (ZMap.empty A).
-
-  (* Monadic mapi *)
-  Definition zmap_mmapi
-    {A B : Type}
-    {m : Type -> Type}
-    {M : Monad m}
-    (f : ZMap.key -> A -> m B) (zm: ZMap.t A)
-    : m (ZMap.t B)
-    :=
-    zmap_sequence (ZMap.mapi f zm).
-
   (* Creare new cap meta for region where all tags are unspecified *)
   Program Definition init_ghost_tags
     (addr: AddressValue.t)
diff --git a/coq/Common/ZMap.v b/coq/Common/ZMap.v
new file mode 100644
index 000000000..a4c9d0584
--- /dev/null
+++ b/coq/Common/ZMap.v
@@ -0,0 +1,81 @@
+Require Import Coq.Numbers.BinNums.
+Require Import Coq.ZArith.Zcompare.
+Require Import Coq.FSets.FMapAVL.
+Require Import Coq.Structures.OrderedTypeEx.
+
+From ExtLib.Data Require Import List.
+From ExtLib.Structures Require Import Monad Monads Traversable.
+
+From Coq.Lists Require Import List. (* after exltlib *)
+
+Local Open Scope type_scope.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Open Scope monad_scope.
+
+Import ListNotations.
+Import MonadNotation.
+
+Module ZMap := FMapAVL.Make(Z_as_OT).
+
+Fixpoint zmap_range_init {T} (a0:Z) (n:nat) (step:Z) (v:T) (m:ZMap.t T) : ZMap.t T
+  :=
+  match n with
+  | O => m
+  | S n =>
+      let m := ZMap.add (Z.add a0 (Z.mul (Z.of_nat n) step)) v m in
+      zmap_range_init a0 n step v m
+  end.
+
+Definition zmap_update_element
+  {A:Type}
+  (key: Z)
+  (v: A)
+  (m: ZMap.t A)
+  : (ZMap.t A)
+  :=
+  ZMap.add key v (ZMap.remove key m).
+
+(** [update key f m] returns a map containing the same bindings as
+  [m], except for the binding of [key]. Depending on the value of [y]
+  where [y] is [f (find_opt key m)], the binding of [key] is added,
+  removed or updated. If [y] is [None], the binding is removed if it
+  exists; otherwise, if [y] is [Some z] then key is associated to [z]
+  in the resulting map. *)
+Definition zmap_update
+  {A:Type}
+  (key: Z)
+  (f: option A -> option A)
+  (m: ZMap.t A)
+  : (ZMap.t A)
+  :=
+  let y := f (ZMap.find key m) in
+  let m' := ZMap.remove key m in (* could be optimized, as removal may be unecessary in some cases *)
+  match y with
+  | None => m'
+  | Some z => ZMap.add key z m'
+  end.
+
+Definition zmap_sequence
+  {A: Type}
+  {m: Type -> Type}
+  {M: Monad m}
+  (mv: ZMap.t (m A)): m (ZMap.t A)
+  :=
+  let fix loop (ls: list (ZMap.key*(m A))) (acc:ZMap.t A) : m (ZMap.t A) :=
+    match ls with
+    | [] => ret acc
+    | (k,mv)::ls => mv >>= (fun v => loop ls (ZMap.add k v acc))
+    end
+  in
+  loop (ZMap.elements mv) (ZMap.empty A).
+
+(* Monadic mapi *)
+Definition zmap_mmapi
+  {A B : Type}
+  {m : Type -> Type}
+  {M : Monad m}
+  (f : ZMap.key -> A -> m B) (zm: ZMap.t A)
+  : m (ZMap.t B)
+  :=
+  zmap_sequence (ZMap.mapi f zm).
diff --git a/coq/Common/dune b/coq/Common/dune
index da1c87c0e..4e8265d01 100644
--- a/coq/Common/dune
+++ b/coq/Common/dune
@@ -2,6 +2,6 @@
  (mode vo)
  (name Common)
  (package cerberus-cheri)
- (modules SimpleError Utils)
+ (modules SimpleError Utils ZMap)
  (theories ExtLib StructTact Sail bbv)
 )
diff --git a/coq/dune b/coq/dune
index 58d0cb81c..1de31e42f 100644
--- a/coq/dune
+++ b/coq/dune
@@ -119,6 +119,7 @@
 (copy_files extracted/Ring_polynom.{ml,mli})
 (copy_files extracted/Ring_theory.{ml,mli})
 (copy_files extracted/SimpleError.{ml,mli})
+(copy_files extracted/ZMap.{ml,mli})
 (copy_files extracted/Specif.{ml,mli})
 (copy_files extracted/String0.{ml,mli})
 (copy_files extracted/String1.{ml,mli})
diff --git a/coq/extracted/dune b/coq/extracted/dune
index ca5ef46e3..acb998045 100644
--- a/coq/extracted/dune
+++ b/coq/extracted/dune
@@ -1,6 +1,6 @@
 (coq.extraction
  (mode vo)
  (prelude Extract)
- (extracted_modules Addr BinaryString Capabilities Capabilities0 CapabilitiesGS CoqAilSyntax CoqAnnot Applicative Ascii BinInt BinList BinNat BinNatDef BinNums BinPos BinPosDef  bitvector Compare_dec Qcanon Relation_Definitions Bool0 Byte CapFns CapFnsTypes CarryType CheriMemory ClassicalDedekindReals CMorphisms ConstructiveCauchyAbs ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveEpsilon ConstructiveExtra ConstructiveRcomplete ConstructiveReals CRelationClasses CoqCtype Datatypes DecidableClass Decimal DepEqNat EitherMonad Eqdep_dec Equalities EquivDec ErrorWithState Fin FloatClass FMapAVL0 FMapList Functor Hexadecimal HexString CoqImplementation Init Injection Instr_kinds Int0 List0 List1 ListSet CoqLocation Logic Monad0 MonadExc MonadFix MonadPlus MonadReader MonadState MonadTrans MonadWriter MonadZero Monoid MorelloCapsGS Nat0 NatLib Number Operators_mwords OrderedType0 OrderedTypeEx Orders OrdersTac PeanoNat PrimFloat PrimInt63 Prompt Prompt_monad Qabs QArith_base QExtra Qreduction Qround Rdefinitions RelDec Ring_polynom Ring_theory SimpleError Specif String0 String1 Sumbool CoqSwitches CoqSymbol CoqTags CerbSwitches Traversable CoqUndefined Undefined Utils Utils0  TypeCasts MachineWord Values Vector0 VectorDef Wf Word ZArith_dec Zbool Bvector Zdigits Zeven base0 Basics countable decidable fin0 list2 numbers0 option0 finite list_numbers)
+ (extracted_modules Addr BinaryString Capabilities Capabilities0 CapabilitiesGS CoqAilSyntax CoqAnnot Applicative Ascii BinInt BinList BinNat BinNatDef BinNums BinPos BinPosDef  bitvector Compare_dec Qcanon Relation_Definitions Bool0 Byte CapFns CapFnsTypes CarryType CheriMemory ClassicalDedekindReals CMorphisms ConstructiveCauchyAbs ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveEpsilon ConstructiveExtra ConstructiveRcomplete ConstructiveReals CRelationClasses CoqCtype Datatypes DecidableClass Decimal DepEqNat EitherMonad Eqdep_dec Equalities EquivDec ErrorWithState Fin FloatClass FMapAVL0 FMapList Functor Hexadecimal HexString CoqImplementation Init Injection Instr_kinds Int0 List0 List1 ListSet CoqLocation Logic Monad0 MonadExc MonadFix MonadPlus MonadReader MonadState MonadTrans MonadWriter MonadZero Monoid MorelloCapsGS Nat0 NatLib Number Operators_mwords OrderedType0 OrderedTypeEx Orders OrdersTac PeanoNat PrimFloat PrimInt63 Prompt Prompt_monad Qabs QArith_base QExtra Qreduction Qround Rdefinitions RelDec Ring_polynom Ring_theory SimpleError ZMap Specif String0 String1 Sumbool CoqSwitches CoqSymbol CoqTags CerbSwitches Traversable CoqUndefined Undefined Utils Utils0  TypeCasts MachineWord Values Vector0 VectorDef Wf Word ZArith_dec Zbool Bvector Zdigits Zeven base0 Basics countable decidable fin0 list2 numbers0 option0 finite list_numbers)
  (theories CheriMemory Common Morello ExtLib stdpp Sail bbv StructTact CheriCaps)
 )
diff --git a/memory/cheri-coq/impl_mem.ml b/memory/cheri-coq/impl_mem.ml
index 4de7f9c6b..5db7a93c1 100644
--- a/memory/cheri-coq/impl_mem.ml
+++ b/memory/cheri-coq/impl_mem.ml
@@ -9,6 +9,7 @@ open CoqImplementation
 open Strfcap
 open CoqSwitches
 open Switches
+open ZMap
 
 module CerbSwitchesProxy = struct