zmap module

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)

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

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

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

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

memory/cheri-coq/impl_mem.ml

@@ -9,6 +9,7 @@ open CoqImplementation
 open Strfcap
 open CoqSwitches
 open Switches
+open ZMap
 
 module CerbSwitchesProxy = struct