Scatter termination.sail (#1376)HEADmaster

Scatter the termination module in such a way that one could require some
termination measures without having to include every single instruction
in the output. This makes building a subset of the model easier.

The termination measures for `vmem_read_addr` and `vmem_write_addr` no
longer need to be protected only for the Rocq output, so they get taken
out of the `$iftarget coq`.

10 files changed, 108 insertions, 126 deletions

diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index 7c57870..aeff0b6 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -251,10 +251,7 @@ Vector (`V`) and cryptography (`Zk*`) extensions.
 
 ### Other modules
 
-The `termination` module specifies
-[functions](../model/termination/termination.sail) that are used to prove
-loop termination for theorem prover backends of Sail. The
-`unit_tests` module collects Sail unit tests for the specification.
+The `unit_tests` module collects Sail unit tests for the specification.
 The `main` module provides a [`main()`](../model/main/main.sail)
 function that is used in other Sail backends.
 
diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt
index 957ab3c..191e77f 100644
--- a/model/CMakeLists.txt
+++ b/model/CMakeLists.txt
@@ -35,8 +35,6 @@ execute_process(
         ${SAIL_BIN}
         ${project_file}
         --require-version ${SAIL_REQUIRED_VER}
-        # include termination.sail in the list of dependencies
-        --variable "TERMINATION_FILE = true"
         --all-modules
         --list-files
     OUTPUT_VARIABLE sail_list_files
@@ -380,7 +378,6 @@ foreach (xlen IN ITEMS 32 64)
             --config ${config_file}
             # Input files.
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -448,7 +445,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_default}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -467,7 +463,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_executable}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
 
diff --git a/model/core/extensions.sail b/model/core/extensions.sail
index fe1de4a..48453b6 100644
--- a/model/core/extensions.sail
+++ b/model/core/extensions.sail
@@ -19,14 +19,31 @@ scattered mapping extensionName
 val hartSupports : extension -> bool
 scattered function hartSupports
 
+function hartSupports_measure(ext : extension) -> int =
+  match ext {
+    Ext_D => 1, // > F
+    Ext_Sstvecd => 1, // > S
+    Ext_Ssu64xl => 1, // > S
+    Ext_Zvkn => 1, // > Zvkned
+    Ext_Zvks => 1, // > Zvksed
+
+    Ext_C => 2, // > D
+    Ext_Zvknc => 2, // > Zvkn
+    Ext_Zvkng => 2, // > Zvkn
+    Ext_Zvksc => 2, // > Zvks
+    Ext_Zvksg => 2, // > Zvks
+
+    _ => 0,
+  }
+
+termination_measure hartSupports(ext) = hartSupports_measure(ext)
+
 // Function used to determine if an extension is currently enabled in the model.
 // This means an extension is supported, *and* any necessary bits are set in the
 // relevant CSRs (misa, mstatus, etc.) to enable its use. It is possible for some
 // extensions to be supported in hardware, but temporarily disabled via a CSR, in
 // which case this function should return false.
-// Note: when adding a new extension, adjust the associated termination measure
-// in the file termination.sail, as explained in the comment in
-// that file.
+// Note: when adding a new extension, adjust the `currentlyEnabled_measure` below.
 val currentlyEnabled : extension -> bool
 scattered function currentlyEnabled
 
@@ -479,6 +496,66 @@ enum clause extension = Ext_Smcntrpmf
 mapping clause extensionName = Ext_Smcntrpmf <-> "smcntrpmf"
 function clause hartSupports(Ext_Smcntrpmf) = config extensions.Smcntrpmf.supported
 
+// When adding a new extension X, we need to make sure that if X being enabled
+// depends on Y being enabled, then the value associated to X is _greater_ than
+// the value associated to Y. The default value is 2, so that if it does not
+// depend on anything or only on extensions A, B, C, D, F, M, S, Zve32x, Zvl* or Zicsr,
+// nothing needs to be done.
+
+function currentlyEnabled_measure(ext : extension) -> int =
+  match ext {
+    Ext_A => 0,
+    Ext_B => 0,
+    Ext_C => 0,
+    Ext_M => 0,
+    Ext_Zicsr => 0,
+    Ext_Zvl128b => 0,
+    Ext_Zvl32b => 0,
+    Ext_Zvl64b => 0,
+
+    Ext_D => 1, // > Zicsr
+    Ext_F => 1, // > Zicsr
+    Ext_S => 1, // > Zicsr
+    Ext_Zaamo => 1, // > A
+    Ext_Zalrsc => 1, // > A
+    Ext_Zca => 1, // > C
+    Ext_Zfinx => 1, // > Zicsr
+    Ext_Zicntr => 1, // > Zicsr
+    Ext_Zihpm => 1, // > Zicsr
+    Ext_Zve32x => 1, // > Zvl32b
+
+    // Note: even though these match the default case, making them explicit to
+    // annotate the chain of dependencies
+    Ext_Sv39 => 2, // > S
+    Ext_Zfh => 2, // > F
+    Ext_Zhinx => 2, // > Zfinx
+    Ext_Zvbb => 2, // > Zve32x
+    Ext_Zve32f => 2, // > Zve32x
+    Ext_Zve64x => 2, // > Zve32x
+
+    Ext_Svrsw60t59b => 3, // > Sv39
+    Ext_Zfhmin => 3, // > Zfh
+    Ext_Zhinxmin => 3, // > Zhinx
+    Ext_Zicfilp => 3, // > get_xLPE
+    Ext_Zvbc => 3, // > Zve64x
+    Ext_Zve64f => 3, // > Zve64x
+    Ext_Zvfbfmin => 3, // > Zve32f
+    Ext_Zvkb => 3, // > Zvbb
+    Ext_Zvknhb => 3, // > Zve64x
+
+    Ext_H => 4, // > virtual_mem_supported
+    Ext_Zve64d => 4, // > Zve64f
+    Ext_Zvfbfwma => 4, // > Zvfbfmin
+    Ext_Zvfh => 4, // > Zfhmin
+
+    Ext_V => 5, // > Zve64d
+    Ext_Zvfhmin => 5, // > Zvfh
+
+    _ => 2
+  }
+
+termination_measure currentlyEnabled(ext) = currentlyEnabled_measure(ext)
+
 let extensions_ordered_for_isa_string = [
   // Single letter extensions.
   Ext_M,
diff --git a/model/core/sys_regs.sail b/model/core/sys_regs.sail
index d21e370..a844ff2 100644
--- a/model/core/sys_regs.sail
+++ b/model/core/sys_regs.sail
@@ -146,6 +146,10 @@ function virtual_memory_supported() -> bool = {
   currentlyEnabled(Ext_Sv32) | currentlyEnabled(Ext_Sv39) | currentlyEnabled(Ext_Sv48) | currentlyEnabled(Ext_Sv57)
 }
 
+// This measure needs to be > currentlyEnabled_measure(Ext_Sv{32,39,48,57}),
+// currently all equal to 2, see currentlyEnabled_measure in extensions.sail
+termination_measure virtual_memory_supported(_) = 3
+
 //
 // Illegal values legalized to least privileged mode supported.
 // Note: the only valid combinations of supported modes are M, M+U, M+S+U.
diff --git a/model/extensions/cfi/zicfilp_regs.sail b/model/extensions/cfi/zicfilp_regs.sail
index ee8d3cf..6d15680 100644
--- a/model/extensions/cfi/zicfilp_regs.sail
+++ b/model/extensions/cfi/zicfilp_regs.sail
@@ -32,6 +32,10 @@ function get_xLPE(p : Privilege) -> bool =
     VirtualUser       => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
   }
 
+// This measure needs to be > currentlyEnabled_measure(Ext_S), currently equal
+// to 1, see currentlyEnabled_measure in extensions.sail
+termination_measure get_xLPE(_) = 2
+
 function clause currentlyEnabled(Ext_Zicfilp) =
   currentlyEnabled(Ext_Zicsr) & hartSupports(Ext_Zicfilp) & get_xLPE(cur_privilege)
 
diff --git a/model/postlude/step.sail b/model/postlude/step.sail
index e8a800f..7bf3cc5 100644
--- a/model/postlude/step.sail
+++ b/model/postlude/step.sail
@@ -296,3 +296,13 @@ function loop () : unit -> unit = {
     }
   }
 }
+
+// Termination measures for loops are not supported by the Lean backend, so they
+// should be guarded by this condition:
+$iftarget coq
+
+// The top-level loop isn't terminating, but we put a limit so that it can still
+// be included in the Coq output
+termination_measure loop while 100
+
+$endif
diff --git a/model/riscv.sail_project b/model/riscv.sail_project
index 1bdda62..c2a4bbd 100644
--- a/model/riscv.sail_project
+++ b/model/riscv.sail_project
@@ -1,4 +1,3 @@
-variable TERMINATION_FILE = false
 variable RMEM = false
 
 prelude {
@@ -477,18 +476,8 @@ postlude {
     postlude/model.sail
 }
 
-termination {
-  after postlude
-  requires prelude, core, sys, extensions
-
-  files
-    if $TERMINATION_FILE then
-      termination/termination.sail
-    else []
-}
-
 unit_tests {
-  after termination
+  after postlude
   requires prelude, core, sys, exceptions, postlude
 
   files
diff --git a/model/sys/vmem.sail b/model/sys/vmem.sail
index 875ba7a..45150c2 100644
--- a/model/sys/vmem.sail
+++ b/model/sys/vmem.sail
@@ -156,6 +156,8 @@ function pt_walk(
   }
 }
 
+termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level
+
 // ****************************************************************
 // Architectural SATP CSR
 
diff --git a/model/sys/vmem_utils.sail b/model/sys/vmem_utils.sail
index c07b661..1b6216c 100644
--- a/model/sys/vmem_utils.sail
+++ b/model/sys/vmem_utils.sail
@@ -172,6 +172,9 @@ function vmem_read_addr(vaddr, offset, width, acc, aq, rl, res) = {
   Ok(data)
 }
 
+// This lets the Rocq extraction know why the repeat loop above terminates
+termination_measure vmem_read_addr repeat n
+
 val vmem_write_addr : forall 'width, is_mem_width('width).
   (virtaddr, int('width), bits(8 * 'width), MemoryAccessType(ext_access_type), bool, bool, bool)
   -> result(bool, ExecutionResult)
@@ -227,6 +230,9 @@ function vmem_write_addr(vaddr, width, data, acc, aq, rl, res) = {
   Ok(write_success)
 }
 
+// This lets the Rocq extraction know why the repeat loop above terminates
+termination_measure vmem_write_addr repeat n
+
 val vmem_read : forall 'width, is_mem_width('width).
   (regidx, xlenbits, int('width), MemoryAccessType(ext_access_type), bool, bool, bool)
   -> result(bits(8 * 'width), ExecutionResult)
diff --git a/model/termination/termination.sail b/model/termination/termination.sail
deleted file mode 100644
index 5964abd..0000000
--- a/model/termination/termination.sail
+++ /dev/null
@@ -1,102 +0,0 @@
-// =======================================================================================
-// This Sail RISC-V architecture model, comprising all files and
-// directories except where otherwise noted is subject the BSD
-// two-clause license in the LICENSE file.
-//
-// SPDX-License-Identifier: BSD-2-Clause
-// =======================================================================================
-
-termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level
-
-// When adding a new extension X, we need to make sure that if X being enabled
-// depends on Y being enabled, then the value associated to X is _greater_ than
-// the value associated to Y. The default value is 2, so that if it does not
-// depend on anything or only on extensions A, B, C, D, F, M, S, Zve32x, Zvl* or Zicsr,
-// nothing needs to be done.
-function currentlyEnabled_measure(ext : extension) -> int =
-  match ext {
-    Ext_Zicsr => 0,
-    Ext_A => 1,
-    Ext_B => 1,
-    Ext_C => 1,
-    Ext_D => 1,
-    Ext_F => 1,
-    Ext_M => 1,
-    Ext_S => 1,
-    Ext_V => 5,
-    Ext_H => 4,
-    Ext_Smcntrpmf => 3,
-    Ext_Zabha => 3,
-    Ext_Zacas => 3,
-    Ext_Za64rs => 3,
-    Ext_Za128rs => 3,
-    Ext_Zcb => 3,
-    Ext_Zcd => 3,
-    Ext_Zcf => 3,
-    Ext_Zcmop => 3,
-    Ext_Zfhmin => 3,
-    Ext_Zhinx => 3,
-    Ext_Zicfilp => 3,
-    Ext_Zvl32b => 0,
-    Ext_Zvl64b => 0,
-    Ext_Zvl128b => 0,
-    Ext_Zvl256b => 0,
-    Ext_Zvl512b => 0,
-    Ext_Zvl1024b => 0,
-    Ext_Zve32x => 1,
-    Ext_Zvfbfmin => 3,
-    Ext_Zvfbfwma => 4,
-    Ext_Zve64f => 3,
-    Ext_Zve64d => 4,
-    Ext_Zvfh => 4,
-    Ext_Zvfhmin => 5,
-    Ext_Zvbb => 6,
-    Ext_Zvbc => 6,
-    Ext_Zvkb => 7,
-    Ext_Zvkg => 6,
-    Ext_Zvkned => 6,
-    Ext_Zvknha => 6,
-    Ext_Zvknhb => 6,
-    Ext_Zvksed => 6,
-    Ext_Zvksh => 6,
-    Ext_Sscofpmf => 3,
-    Ext_Svrsw60t59b => 3,
-    Ext_Zhinxmin => 4,
-    _ => 2
-  }
-
-termination_measure currentlyEnabled(ext) = currentlyEnabled_measure(ext)
-termination_measure virtual_memory_supported(_) = 3
-
-// get_xLPE() and currentlyEnabled() are mutually recursive
-termination_measure get_xLPE(_) = 2
-
-function hartSupports_measure(ext : extension) -> int =
-  match ext {
-    Ext_D => 1,
-    Ext_V => 1,
-    Ext_Zvkn => 1,
-    Ext_Zvks => 1,
-    Ext_C => 2,
-    Ext_Zvknc => 2,
-    Ext_Zvkng => 2,
-    Ext_Zvksc => 2,
-    Ext_Zvksg => 2,
-    Ext_Sstvecd => 1,
-    Ext_Ssu64xl => 1,
-    _ => 0,
-  }
-
-termination_measure hartSupports(ext) = hartSupports_measure(ext)
-
-// Termination measures for loops are not supported by the Lean backend, so they
-// should be guarded by this condition:
-$iftarget coq
-
-termination_measure vmem_write_addr repeat n
-termination_measure vmem_read_addr repeat n
-
-// The top-level loop isn't terminating, but we put a limit so that it can still be included in the Coq output
-termination_measure loop while 100
-
-$endif