diff options
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 13 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 4 |
2 files changed, 15 insertions, 2 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 739a22d0..697bc4a8 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -527,5 +527,18 @@ destruct (sumbool_of_bool _). f_equal. *) +Import ListNotations. +Definition count_leading_zeros {N : Z} (x : mword N) `{ArithFact (N >= 1)} +: {n : Z & ArithFact (0 <= n /\ n <= N)} := + let r : {n : Z & ArithFact (0 <= n /\ n <= N)} := build_ex N in + foreach_Z_up 0 (N - 1) 1 r + (fun i _ r => + (if ((eq_vec (vec_of_bits [access_vec_dec x i] : mword 1) (vec_of_bits [B1] : mword 1))) + then build_ex + (Z.sub (Z.sub (length_mword x) i) 1) + : {n : Z & ArithFact (0 <= n /\ n <= N)} + else r)) + . + Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt. Definition print_bits {a} (s : string) (bs : mword a) : unit := tt. diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 15bdaea4..208f5c8a 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -2288,9 +2288,9 @@ Definition negate_range {n m} (l : {l : Z & ArithFact (n <= l <= m)}) : {x : Z & ArithFact ((- m) <= x <= (- n))} := build_ex (- (projT1 l)). -Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <= a /\ c <= b)} := +Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c <= a /\ c <= b)} := build_ex (Z.min a b). -Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} := +Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact ((c = a \/ c = b) /\ c >= a /\ c >= b)} := build_ex (Z.max a b). |