Fix lean issue

Author: nadime15

model/riscv_extensions.sail

@@ -291,10 +291,10 @@ function clause currentlyEnabled(Ext_Zvkt) = hartSupports(Ext_Zvkt)
 enum clause extension = Ext_Zvkn
 mapping clause extensionName = Ext_Zvkn <-> "zvkn"
 function clause hartSupports(Ext_Zvkn) =
-hartSupports(Ext_Zvkned) &
-hartSupports(Ext_Zvknhb) &
-hartSupports(Ext_Zvkb)   &
-hartSupports(Ext_Zvkt)
+  hartSupports(Ext_Zvkned) &
+  hartSupports(Ext_Zvknhb) &
+  hartSupports(Ext_Zvkb)   &
+  hartSupports(Ext_Zvkt)
 function clause currentlyEnabled(Ext_Zvkn) = hartSupports(Ext_Zvkn)
 // NIST Algorithm Suite with carryless multiply
 enum clause extension = Ext_Zvknc
@@ -310,10 +310,10 @@ function clause currentlyEnabled(Ext_Zvkng) = hartSupports(Ext_Zvkng)
 enum clause extension = Ext_Zvks
 mapping clause extensionName = Ext_Zvks <-> "zvks"
 function clause hartSupports(Ext_Zvks) =
-hartSupports(Ext_Zvksed) &
-hartSupports(Ext_Zvksh)  &
-hartSupports(Ext_Zvkb)   &
-hartSupports(Ext_Zvkt)
+  hartSupports(Ext_Zvksed) &
+  hartSupports(Ext_Zvksh)  &
+  hartSupports(Ext_Zvkb)   &
+  hartSupports(Ext_Zvkt)
 function clause currentlyEnabled(Ext_Zvks) = hartSupports(Ext_Zvks)
 // ShangMi Algorithm Suite with carryless multiplication
 enum clause extension = Ext_Zvksc

model/riscv_termination.sail

@@ -92,6 +92,20 @@ termination_measure virtual_memory_supported(_) = 3
 function hartSupports_measure(ext : extension) -> int =
   match ext {
     Ext_C => 1,
+    Ext_Zvkned => 0,
+    Ext_Zvknhb => 0,
+    Ext_Zvkb => 0,
+    Ext_Zvkt => 0,
+    Ext_Zvbc => 0,
+    Ext_Zvkg => 0,
+    Ext_Zvksed => 0,
+    Ext_Zvksh => 0,
+    Ext_Zvkn => 1,
+    Ext_Zvks => 1,
+    Ext_Zvknc => 2,
+    Ext_Zvkng => 2,
+    Ext_Zvksc => 2,
+    Ext_Zvksg => 2,
     _ => 0,
   }