Implement count_leading_zeros in Lem

3 files changed, 15 insertions, 0 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 8b75fa38..c9892e4c 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -304,3 +304,5 @@ val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 let eq_vec    = eq_bv
 let neq_vec   = neq_bv
+
+let inline count_leading_zeros v = count_leading_zero_bits v
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 181fa149..c8524e16 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -329,3 +329,6 @@ val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
+
+val count_leading_zeros : forall 'a. Size 'a => mword 'a -> integer
+let count_leading_zeros v = count_leading_zeros_bv v
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 9de28cca..f657803f 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -656,6 +656,16 @@ let int_of_bit b =
   | _ -> failwith "int_of_bit saw unknown"
   end
 
+val count_leading_zero_bits : list bitU -> integer
+let rec count_leading_zero_bits v =
+  match v with
+  | B0 :: v' -> count_leading_zero_bits v' + 1
+  | _ -> 0
+  end
+
+val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer
+let count_leading_zeros_bv v = count_leading_zero_bits (bits_of v)
+
 val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let decimal_string_of_bv bv =
   let place_values =