Reorganise project into 3 folders

rems-project · Feb 11, 2025 · 4b652ed · 4b652ed
1 parent 01ec33c
commit 4b652ed
Show file tree

Hide file tree

Showing 30 changed files with 106 additions and 196 deletions.
diff --git a/GenModels/CandidateExecutions.v → ArchSem/CandidateExecutions.v b/GenModels/CandidateExecutions.v → ArchSem/CandidateExecutions.v
@@ -66,7 +66,7 @@ Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
 Require Import ASCommon.StateT.
 
-Require Import ISASem.Interface.
+Require Import Interface.
 Require Import TermModels.
 
 Open Scope Z_scope.

diff --git a/promising-arm/GenPromising.v → ArchSem/GenPromising.v b/promising-arm/GenPromising.v → ArchSem/GenPromising.v
@@ -60,12 +60,11 @@ Require Import Program.
 
 From stdpp Require Import relations.
 
-Open Scope Z_scope.
-Open Scope stdpp_scope.
+#[local] Open Scope Z_scope.
+#[local] Open Scope stdpp_scope.
 
-Require Import ISASem.Interface.
-
-Require Import GenModels.TermModels.
+Require Import Interface.
+Require Import TermModels.
 
 
 
@@ -131,7 +130,7 @@ Arguments t : clear implicits.
 End PromMemory.
 
 (* to be imported *)
-Module Gen (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
+Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
   Import IWA.Arch.
   Import IWA.Interface.
   Import TM.
@@ -385,8 +384,8 @@ Module Gen (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     (* TODO state some soundness lemma between Promising_to_Modelnc and
         Promising_Modelc *)
 
-End Gen.
+End GenPromising.
 
-Module Type GenT (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
-  Include Gen IWA TM.
-End GenT.
+Module Type GenPromisingT (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
+  Include GenPromising IWA TM.
+End GenPromisingT.
diff --git a/ISASem/Interface.v → ArchSem/Interface.v b/ISASem/Interface.v → ArchSem/Interface.v
@@ -200,7 +200,7 @@ End Arch.
 
 Module Interface (A : Arch).
   Import A.
-  Open Scope N.
+  #[local] Open Scope N.
 
   (** ** Memory utility *)
   (** Virtual address are tag-less bitvectors *)

diff --git a/GenModels/TermModels.v → ArchSem/TermModels.v b/GenModels/TermModels.v → ArchSem/TermModels.v
@@ -51,10 +51,10 @@ Require Import ASCommon.Exec.
 Require Import Relations.
 Require Import Program.
 
-Open Scope Z_scope.
-Open Scope stdpp_scope.
+#[local] Open Scope Z_scope.
+#[local] Open Scope stdpp_scope.
 
-Require Import ISASem.Interface.
+Require Import Interface.
 
 
 (** This module specify general definitions of hardware models over finite

diff --git a/ISASem/_CoqProject → ArchSem/_CoqProject b/ISASem/_CoqProject → ArchSem/_CoqProject
@@ -1,2 +1,2 @@
--R ../_build/default/ISASem ISASem
 -Q ../_build/default/Common ASCommon
+-R ../_build/default/ArchSem ArchSem
diff --git a/GenModels/dune → ArchSem/dune b/GenModels/dune → ArchSem/dune
@@ -1,16 +1,21 @@
 (coq.theory
- (name GenModels)
+ (name ArchSem)
  (package coq-archsem)
- (modules TermModels CandidateExecutions ArmInst ArmSeqModel)
- (theories ISASem ASCommon)
+ (modules
+   Interface
+   TermModels
+   CandidateExecutions
+   GenPromising
+ )
+ (theories SailStdpp ASCommon)
  (coqdoc_flags :standard --utf8
                --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp
                --external ../../Common/ASCommon.html ASCommon
-               --external ../../ISASem/ISASem.html ISASem
                --coqlib_url https://coq.inria.fr/doc/V8.20.1/stdlib
  )
 )
 
+; This alias is useful to build all the coq libaries without extraction
 (alias
  (name coq)
  (deps (alias_rec all))

diff --git a/ISASem/ArmInst.v → ArchSemArm/ArmInst.v b/ISASem/ArmInst.v → ArchSemArm/ArmInst.v
@@ -49,12 +49,12 @@ Require Import stdpp.base.
 Require Import stdpp.countable.
 Require Import stdpp.vector.
 Require Import ASCommon.Options.
-Require Import Interface.
 Require Import SailStdpp.Base.
 Require Export SailArmInstTypes.
 Require Import Coq.Reals.Rbase.
 From RecordUpdate Require Import RecordSet.
 From ASCommon Require Import Common Effects CDestruct.
+From ArchSem Require Import Interface TermModels CandidateExecutions GenPromising.
 
 
 From Equations Require Import Equations.
@@ -63,6 +63,8 @@ From Equations Require Import Equations.
 Require Import stdpp.decidable.
 Require Import stdpp.list.
 
+#[global] Open Scope stdpp.
+
 #[global] Typeclasses Transparent bits.
 
 Unset Elimination Schemes.
@@ -561,5 +563,13 @@ End Arm.
 
 Bind Scope string_scope with Arm.Arch.reg.
 
+Module ArmTM := TermModels Arm.
+Module ArmCand := CandidateExecutions Arm ArmTM.
+Module ArmGenPro := GenPromising Arm ArmTM.
+
 Export Arm.Arch.
 Export Arm.Interface.
+Export ArmTM.
+Export ArmCand.
+Export ArmGenPro.
+
diff --git a/GenModels/ArmSeqModel.v → ArchSemArm/ArmSeqModel.v b/GenModels/ArmSeqModel.v → ArchSemArm/ArmSeqModel.v
diff --git a/AxiomaticModels/GenAxiomaticArm.v → ArchSemArm/GenAxiomaticArm.v b/AxiomaticModels/GenAxiomaticArm.v → ArchSemArm/GenAxiomaticArm.v
@@ -46,7 +46,7 @@ Require Import ASCommon.Options.
 Require Import ASCommon.Common.
 Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
-Require Import GenModels.ArmInst.
+Require Import ArmInst.
 
 (* NOTE: TODO change this.
  This file defines the VMSA and User Arm axiomatic models. It starts with some

diff --git a/ISASem/SailArmInstTypes.v → ArchSemArm/SailArmInstTypes.v b/ISASem/SailArmInstTypes.v → ArchSemArm/SailArmInstTypes.v
diff --git a/AxiomaticModels/UMArm.v → ArchSemArm/UMArm.v b/AxiomaticModels/UMArm.v → ArchSemArm/UMArm.v
@@ -46,7 +46,7 @@ Require Import ASCommon.Options.
 Require Import ASCommon.Common.
 Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
-Require Import GenModels.ArmInst.
+Require Import ArmInst.
 Require Import GenAxiomaticArm.
 
 (** This is an implementation of a user-mode Axiomatic model for ARM. It does

diff --git a/promising-arm/UMPromising.v → ArchSemArm/UMPromising.v b/promising-arm/UMPromising.v → ArchSemArm/UMPromising.v
@@ -42,19 +42,18 @@
 (*                                                                            *)
 (******************************************************************************)
 
+Require Import Coq.Program.Equality.
+From stdpp Require Import decidable.
 Require Import ASCommon.Options.
 Require Import ASCommon.Common.
 Require Import ASCommon.Exec.
 Require Import ASCommon.StateT.
 Require Import ASCommon.FMon.
-Require Import Coq.Program.Equality.
 
-From stdpp Require Import decidable.
+Require Import ArchSem.GenPromising.
+Require Import ArmInst.
+
 
-Require Import GenModels.ArmInst.
-Require Import GenPromising.
-Module ArmGP := Gen Arm ArmTM.
-Import ArmGP.
 
 (** The goal of this module is to define an User-mode promising model,
     without mixed-size on top of the new interface *)
@@ -76,6 +75,7 @@ Module Loc.
       FullAddress_address := bv_concat 52 loc (bv_0 3)
     |}.
 
+
   (** Recover a location from an ARM physical address. *)
   Definition from_pa (pa : FullAddress) : option t :=
     match FullAddress_paspace pa with

diff --git a/AxiomaticModels/UMSeqArm.v → ArchSemArm/UMSeqArm.v b/AxiomaticModels/UMSeqArm.v → ArchSemArm/UMSeqArm.v
@@ -46,7 +46,7 @@ Require Import ASCommon.Options.
 Require Import ASCommon.Common.
 Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
-Require Import GenModels.ArmInst.
+Require Import ArmInst.
 Require Import GenAxiomaticArm.
 
 (** This is an implementation of a user-mode SC Axiomatic model in ARM style.

diff --git a/promising-arm/VMPromising.v → ArchSemArm/VMPromising.v b/promising-arm/VMPromising.v → ArchSemArm/VMPromising.v
@@ -55,9 +55,8 @@ From stdpp Require Import pretty.
 
 Require UMPromising.
 
-Require Import GenModels.ArmInst.
-Require Import GenPromising.
-Import UMPromising.ArmGP.
+Require Import ArchSem.GenPromising.
+Require Import ArmInst.
 
 (** The goal of this module is to define an Virtual memory promising model,
     without mixed-size on top of the new interface *)

diff --git a/AxiomaticModels/VMSA22Arm.v → ArchSemArm/VMSA22Arm.v b/AxiomaticModels/VMSA22Arm.v → ArchSemArm/VMSA22Arm.v
@@ -46,7 +46,7 @@ Require Import ASCommon.Options.
 Require Import ASCommon.Common.
 Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
-Require Import GenModels.ArmInst.
+Require Import ArmInst.
 Require Import GenAxiomaticArm.
 
 Import Candidate.

diff --git a/AxiomaticModels/VMUMEquivThm.v → ArchSemArm/VMUMEquivThm.v b/AxiomaticModels/VMUMEquivThm.v → ArchSemArm/VMUMEquivThm.v
@@ -51,8 +51,7 @@ Require Import ASCommon.Common.
 Require Import ASCommon.GRel.
 
 Require Import ASCommon.FMon.
-Require Import ISASem.ArmInst.
-Require Import GenModels.ArmInst.
+Require Import ArmInst.
 Require Import GenAxiomaticArm.
 Require UMArm.
 Module UM := UMArm.

diff --git a/ArchSemArm/_CoqProject b/ArchSemArm/_CoqProject
@@ -0,0 +1,3 @@
+-Q ../_build/default/Common ASCommon
+-Q ../_build/default/ArchSem ArchSem
+-R ../_build/default/ArchSemArm ArchSemArm
diff --git a/ArchSemArm/dune b/ArchSemArm/dune
@@ -0,0 +1,29 @@
+(coq.theory
+ (name ArchSemArm)
+ (package coq-archsem)
+ (modules
+   SailArmInstTypes
+   ArmInst
+   ArmSeqModel
+   UMPromising
+   VMPromising
+   GenAxiomaticArm
+   UMArm
+   UMSeqArm
+   VMSA22Arm
+   VMUMEquivThm
+ )
+ (theories ASCommon ArchSem)
+ (coqdoc_flags :standard --utf8
+               --external https://plv.mpi-sws.org/coqdoc/stdpp stdpp
+               --external ../../Common/ASCommon.html ASCommon
+               --external ../../ArchSem/ArchSem.html ArchSem
+               --coqlib_url https://coq.inria.fr/doc/V8.20.1/stdlib
+ )
+)
+
+; This alias is useful to build all the coq libaries without extraction
+(alias
+ (name coq)
+ (deps (alias_rec all))
+)
diff --git a/AxiomaticModels/_CoqProject b/AxiomaticModels/_CoqProject
diff --git a/AxiomaticModels/dune b/AxiomaticModels/dune
diff --git a/Common/dune b/Common/dune
@@ -20,7 +20,8 @@
    StateT
    Effects
    FMon
-   Exec)
+   Exec
+ )
  (theories stdpp Hammer RecordUpdate Equations Ltac2)
  (coqdoc_flags :standard --utf8
                --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp

diff --git a/Extraction/ArmInstExtr.v b/Extraction/ArmInstExtr.v
@@ -1,5 +1,5 @@
 Require Import ASCommon.CExtraction.
-Require Import GenModels.ArmSeqModel.
+Require Import ArchSemArm.ArmSeqModel.
 
 Unset Extraction SafeImplicits.
 

diff --git a/Extraction/dune b/Extraction/dune
@@ -2,9 +2,9 @@
 
 (coq.extraction
   (prelude ArmInstExtr)
-  (theories ISASem ASCommon stdpp SailStdpp Hammer RecordUpdate Equations
-            GenModels Ltac2)
-  (extracted_modules ArmInst0 ArmInst ArmSeqModel Ascii base Basics BinInt
+  (theories Ltac2 stdpp SailStdpp Hammer RecordUpdate Equations
+            ASCommon ArchSem ArchSemArm)
+  (extracted_modules ArmInst ArmSeqModel Ascii base Basics BinInt
                      BinNat BinNums BinPosDef BinPos CBase CBitvector CBool
                      CList CMaps COption countable CResult CSets Datatypes
                      decidable definitions Effects Exec fin0 finite fin_maps Fin

diff --git a/GenModels/ArmInst.v b/GenModels/ArmInst.v
diff --git a/GenModels/_CoqProject b/GenModels/_CoqProject
diff --git a/ISASem/README.md b/ISASem/README.md
-Original file line number
+Diff line change
@@ Expand Up / @@ -20,7 +20,8 @@ @@
        StateT
        Effects
        FMon
-       Exec)
+       Exec
+     )
      (theories stdpp Hammer RecordUpdate Equations Ltac2)
      (coqdoc_flags :standard --utf8
                    --external https://plv.mpi-sws.org/coqdoc/stdpp/ stdpp
@@ Expand Down @@