Scatter termination.sail

doc/ReadingGuide.md

@@ -240,10 +240,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.
 

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
@@ -375,7 +373,6 @@ foreach (xlen IN ITEMS 32 64)
             --config ${config_file}
             # Input files.
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -443,7 +440,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_default}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -462,7 +458,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_executable}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
 

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
 
@@ -474,6 +491,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,

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.

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)
 

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

model/riscv.sail_project

@@ -1,4 +1,3 @@
-variable TERMINATION_FILE = false
 variable RMEM = false
 
 core {
@@ -466,18 +465,8 @@ postlude {
     postlude/model.sail
 }
 
-termination {
-  after postlude
-  requires core, sys, extensions
-
-  files
-    if $TERMINATION_FILE then
-      termination/termination.sail
-    else []
-}
-
 unit_tests {
-  after termination
+  after postlude
   requires core, sys, exceptions, postlude
 
   files

model/sys/vmem.sail

@@ -156,6 +156,8 @@ function pt_walk(
   }
 }
 
+termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level
+
 // ****************************************************************
 // Architectural SATP CSR
 

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)