# Theory More_Bits_Int

(*  Title:      Bits_Int.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹More bit operations on integers›

theory More_Bits_Int
imports
"Word_Lib.Bits_Int"
"Word_Lib.Bit_Comprehension"
begin

text ‹Preliminaries›

declare hd_Nil_eq_last [simp]

lemma nat_LEAST_True: "(LEAST _ :: nat. True) = 0"
by (rule Least_equality) simp_all

text ‹
Use this function to convert numeral @{typ integer}s quickly into @{typ int}s.
By default, it works only for symbolic evaluation; normally generated code raises
an exception at run-time. If theory ‹Code_Target_Bits_Int› is imported,
it works again, because then @{typ int} is implemented in terms of @{typ integer}
even for symbolic evaluation.
›

definition int_of_integer_symbolic :: "integer ⇒ int"
where "int_of_integer_symbolic = int_of_integer"

lemma int_of_integer_symbolic_aux_code [code nbe]:
"int_of_integer_symbolic 0 = 0"
"int_of_integer_symbolic (Code_Numeral.Pos n) = Int.Pos n"
"int_of_integer_symbolic (Code_Numeral.Neg n) = Int.Neg n"
by (simp_all add: int_of_integer_symbolic_def)

section ‹Symbolic bit operations on numerals and @{typ int}s›

fun bitOR_num :: "num ⇒ num ⇒ num"
where
"bitOR_num num.One num.One = num.One"
| "bitOR_num num.One (num.Bit0 n) = num.Bit1 n"
| "bitOR_num num.One (num.Bit1 n) = num.Bit1 n"
| "bitOR_num (num.Bit0 m) num.One = num.Bit1 m"
| "bitOR_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (bitOR_num m n)"
| "bitOR_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"
| "bitOR_num (num.Bit1 m) num.One = num.Bit1 m"
| "bitOR_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (bitOR_num m n)"
| "bitOR_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (bitOR_num m n)"

fun bitAND_num :: "num ⇒ num ⇒ num option"
where
"bitAND_num num.One num.One = Some num.One"
| "bitAND_num num.One (num.Bit0 n) = None"
| "bitAND_num num.One (num.Bit1 n) = Some num.One"
| "bitAND_num (num.Bit0 m) num.One = None"
| "bitAND_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit1 m) num.One = Some num.One"
| "bitAND_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (bitAND_num m n)"
| "bitAND_num (num.Bit1 m) (num.Bit1 n) = (case bitAND_num m n of None ⇒ Some num.One | Some n' ⇒ Some (num.Bit1 n'))"

fun bitXOR_num :: "num ⇒ num ⇒ num option"
where
"bitXOR_num num.One num.One = None"
| "bitXOR_num num.One (num.Bit0 n) = Some (num.Bit1 n)"
| "bitXOR_num num.One (num.Bit1 n) = Some (num.Bit0 n)"
| "bitXOR_num (num.Bit0 m) num.One = Some (num.Bit1 m)"
| "bitXOR_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitXOR_num m n)"
| "bitXOR_num (num.Bit0 m) (num.Bit1 n) = Some (case bitXOR_num m n of None ⇒ num.One | Some n' ⇒ num.Bit1 n')"
| "bitXOR_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
| "bitXOR_num (num.Bit1 m) (num.Bit0 n) = Some (case bitXOR_num m n of None ⇒ num.One | Some n' ⇒ num.Bit1 n')"
| "bitXOR_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitXOR_num m n)"

fun bitORN_num :: "num ⇒ num ⇒ num"
where
"bitORN_num num.One num.One = num.One"
| "bitORN_num num.One (num.Bit0 m) = num.Bit1 m"
| "bitORN_num num.One (num.Bit1 m) = num.Bit1 m"
| "bitORN_num (num.Bit0 n) num.One = num.Bit0 num.One"
| "bitORN_num (num.Bit0 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
| "bitORN_num (num.Bit0 n) (num.Bit1 m) = num.Bit0 (bitORN_num n m)"
| "bitORN_num (num.Bit1 n) num.One = num.One"
| "bitORN_num (num.Bit1 n) (num.Bit0 m) = Num.BitM (bitORN_num n m)"
| "bitORN_num (num.Bit1 n) (num.Bit1 m) = Num.BitM (bitORN_num n m)"

fun bitANDN_num :: "num ⇒ num ⇒ num option"
where
"bitANDN_num num.One num.One = None"
| "bitANDN_num num.One (num.Bit0 n) = Some num.One"
| "bitANDN_num num.One (num.Bit1 n) = None"
| "bitANDN_num (num.Bit0 m) num.One = Some (num.Bit0 m)"
| "bitANDN_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (bitANDN_num m n)"
| "bitANDN_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"
| "bitANDN_num (num.Bit1 m) num.One = Some (num.Bit0 m)"
| "bitANDN_num (num.Bit1 m) (num.Bit0 n) = (case bitANDN_num m n of None ⇒ Some num.One | Some n' ⇒ Some (num.Bit1 n'))"
| "bitANDN_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (bitANDN_num m n)"

lemma int_numeral_bitOR_num: "numeral n OR numeral m = (numeral (bitOR_num n m) :: int)"
by(induct n m rule: bitOR_num.induct) simp_all

lemma int_numeral_bitAND_num: "numeral n AND numeral m = (case bitAND_num n m of None ⇒ 0 :: int | Some n' ⇒ numeral n')"
by(induct n m rule: bitAND_num.induct)(simp_all split: option.split)

lemma int_numeral_bitXOR_num:
"numeral m XOR numeral n = (case bitXOR_num m n of None ⇒ 0 :: int | Some n' ⇒ numeral n')"
by(induct m n rule: bitXOR_num.induct)(simp_all split: option.split)

lemma int_or_not_bitORN_num:
"numeral n OR NOT (numeral m) = (- numeral (bitORN_num n m) :: int)"
by (induction n m rule: bitORN_num.induct) (simp_all add: add_One BitM_inc_eq)

lemma int_and_not_bitANDN_num:
"numeral n AND NOT (numeral m) = (case bitANDN_num n m of None ⇒ 0 :: int | Some n' ⇒ numeral n')"
by (induction n m rule: bitANDN_num.induct) (simp_all add: add_One BitM_inc_eq split: option.split)

lemma int_not_and_bitANDN_num:
"NOT (numeral m) AND numeral n = (case bitANDN_num n m of None ⇒ 0 :: int | Some n' ⇒ numeral n')"
by(simp add: int_and_not_bitANDN_num[symmetric] int_and_comm)

code_identifier
code_module More_Bits_Int ⇀
(SML) Bit_Operations and (OCaml) Bit_Operations and (Haskell) Bit_Operations and (Scala) Bit_Operations

end


# Theory Code_Symbolic_Bits_Int

(*  Title:      Code_Symbolic_Bits_Int.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Symbolic implementation of bit operations on int›

theory Code_Symbolic_Bits_Int
imports
"Word_Lib.Generic_set_bit"
"Word_Lib.Least_significant_bit"
More_Bits_Int
begin

section ‹Implementations of bit operations on \<^typ>‹int› operating on symbolic representation›

lemma test_bit_int_code [code]:
"bit (0::int)          n = False"
"bit (Int.Neg num.One) n = True"
"bit (Int.Pos num.One)      0 = True"
"bit (Int.Pos (num.Bit0 m)) 0 = False"
"bit (Int.Pos (num.Bit1 m)) 0 = True"
"bit (Int.Neg (num.Bit0 m)) 0 = False"
"bit (Int.Neg (num.Bit1 m)) 0 = True"
"bit (Int.Pos num.One)      (Suc n) = False"
"bit (Int.Pos (num.Bit0 m)) (Suc n) = bit (Int.Pos m) n"
"bit (Int.Pos (num.Bit1 m)) (Suc n) = bit (Int.Pos m) n"
"bit (Int.Neg (num.Bit0 m)) (Suc n) = bit (Int.Neg m) n"
"bit (Int.Neg (num.Bit1 m)) (Suc n) = bit (Int.Neg (Num.inc m)) n"

lemma int_not_code [code]:
"NOT (0 :: int) = -1"
"NOT (Int.Pos n) = Int.Neg (Num.inc n)"
"NOT (Int.Neg n) = Num.sub n num.One"

lemma int_and_code [code]: fixes i j :: int shows
"0 AND j = 0"
"i AND 0 = 0"
"Int.Pos n AND Int.Pos m = (case bitAND_num n m of None ⇒ 0 | Some n' ⇒ Int.Pos n')"
"Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)"
"Int.Pos n AND Int.Neg num.One = Int.Pos n"
"Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (bitORN_num (Num.BitM m) n) num.One"
"Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (bitORN_num (num.Bit0 m) n) num.One"
"Int.Neg num.One AND Int.Pos m = Int.Pos m"
"Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (bitORN_num (Num.BitM n) m) num.One"
"Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (bitORN_num (num.Bit0 n) m) num.One"
sub_inc_One_eq inc_BitM_eq not_minus_numeral_inc_eq
flip: int_not_neg_numeral int_or_not_bitORN_num split: option.split)
apply (simp_all add: ac_simps)
done

lemma int_or_code [code]: fixes i j :: int shows
"0 OR j = j"
"i OR 0 = i"
"Int.Pos n OR Int.Pos m = Int.Pos (bitOR_num n m)"
"Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)"
"Int.Pos n OR Int.Neg num.One = Int.Neg num.One"
"Int.Pos n OR Int.Neg (num.Bit0 m) = (case bitANDN_num (Num.BitM m) n of None ⇒ -1 | Some n' ⇒ Int.Neg (Num.inc n'))"
"Int.Pos n OR Int.Neg (num.Bit1 m) = (case bitANDN_num (num.Bit0 m) n of None ⇒ -1 | Some n' ⇒ Int.Neg (Num.inc n'))"
"Int.Neg num.One OR Int.Pos m = Int.Neg num.One"
"Int.Neg (num.Bit0 n) OR Int.Pos m = (case bitANDN_num (Num.BitM n) m of None ⇒ -1 | Some n' ⇒ Int.Neg (Num.inc n'))"
"Int.Neg (num.Bit1 n) OR Int.Pos m = (case bitANDN_num (num.Bit0 n) m of None ⇒ -1 | Some n' ⇒ Int.Neg (Num.inc n'))"
apply (simp_all add: int_numeral_bitOR_num flip: int_not_neg_numeral)
apply (simp_all add: or_int_def int_and_comm int_not_and_bitANDN_num del: int_not_simps(4) split: option.split)
done

lemma int_xor_code [code]: fixes i j :: int shows
"0 XOR j = j"
"i XOR 0 = i"
"Int.Pos n XOR Int.Pos m = (case bitXOR_num n m of None ⇒ 0 | Some n' ⇒ Int.Pos n')"
"Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One"
"Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)"
"Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)"
by(fold int_not_neg_numeral)(simp_all add: int_numeral_bitXOR_num int_xor_not cong: option.case_cong)

lemma bin_rest_code: "bin_rest i = i >> 1"
by (simp add: shiftr_int_def)

lemma set_bits_code [code]:
"set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (λ_. set_bits :: _ ⇒ int)"
by simp

lemma fixes i :: int
shows int_set_bit_True_conv_OR [code]: "set_bit i n True = i OR (1 << n)"
and int_set_bit_False_conv_NAND [code]: "set_bit i n False = i AND NOT (1 << n)"
and int_set_bit_conv_ops: "set_bit i n b = (if b then i OR (1 << n) else i AND NOT (1 << n))"
by(simp_all add: set_bit_int_def bin_set_conv_OR bin_clr_conv_NAND)

declare [[code drop: ‹drop_bit :: nat ⇒ int ⇒ int›]]

lemma drop_bit_int_code [code]: fixes i :: int shows
"drop_bit 0 i = i"
"drop_bit (Suc n) 0 = (0 :: int)"
"drop_bit (Suc n) (Int.Pos num.One) = 0"
"drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)"
"drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)"
"drop_bit (Suc n) (Int.Neg num.One) = - 1"
"drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)"
"drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))"

declare [[code drop: ‹push_bit :: nat ⇒ int ⇒ int›]]

lemma push_bit_int_code [code]:
"push_bit 0 i = i"
"push_bit (Suc n) i = push_bit n (Int.dup i)"
by (simp_all add: ac_simps)

lemma int_lsb_code [code]:
"lsb (0 :: int) = False"
"lsb (Int.Pos num.One) = True"
"lsb (Int.Pos (num.Bit0 w)) = False"
"lsb (Int.Pos (num.Bit1 w)) = True"
"lsb (Int.Neg num.One) = True"
"lsb (Int.Neg (num.Bit0 w)) = False"
"lsb (Int.Neg (num.Bit1 w)) = True"
by simp_all

end


# Theory Bits_Integer

(*  Title:      Bits_Integer.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Bit operations for target language integers›

theory Bits_Integer imports
More_Bits_Int
Code_Symbolic_Bits_Int
begin

lemmas [transfer_rule] =
identity_quotient
fun_quotient
Quotient_integer[folded integer.pcr_cr_eq]

lemma undefined_transfer:
assumes "Quotient R Abs Rep T"
shows "T (Rep undefined) undefined"
using assms unfolding Quotient_alt_def by blast

bundle undefined_transfer = undefined_transfer[transfer_rule]

section ‹More lemmas about @{typ integer}s›

context
includes integer.lifting
begin

lemma bitval_integer_transfer [transfer_rule]:
"(rel_fun (=) pcr_integer) of_bool of_bool"
by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def)

lemma integer_of_nat_less_0_conv [simp]: "¬ integer_of_nat n < 0"
by(transfer) simp

lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n"
by(induct n) simp_all

lemma pow_integer_transfer [transfer_rule]:
"(rel_fun pcr_integer (rel_fun (=) pcr_integer)) (^) (^)"
by(auto 4 3 simp add: integer.pcr_cr_eq cr_integer_def int_of_integer_pow)

lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0 ⟷ False"
by(cases n)(simp_all add: Code_Numeral.sub_code)

lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n"
by transfer simp

lemma nat_of_integer_sub1_conv_pred_numeral [simp]:
"nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n"
by(cases n)(simp_all add: Code_Numeral.sub_code)

lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1"
by transfer simp

lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2"
by transfer simp

section ‹Bit operations on @{typ integer}›

text ‹Bit operations on @{typ integer} are the same as on @{typ int}›

lift_definition bin_rest_integer :: "integer ⇒ integer" is bin_rest .
lift_definition bin_last_integer :: "integer ⇒ bool" is bin_last .
lift_definition Bit_integer :: "integer ⇒ bool ⇒ integer" is ‹λk b. of_bool b + 2 * k› .

end

instance integer :: semiring_bit_syntax ..

context
includes lifting_syntax integer.lifting
begin

lemma test_bit_integer_transfer [transfer_rule]:
‹(pcr_integer ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_integer_transfer [transfer_rule]:
‹(pcr_integer ===> (=) ===> pcr_integer) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_integer_transfer [transfer_rule]:
‹(pcr_integer ===> (=) ===> pcr_integer) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation integer :: lsb begin
context includes integer.lifting begin

lift_definition lsb_integer :: "integer ⇒ bool" is lsb .

instance
by (standard; transfer) (fact lsb_odd)

end
end

instantiation integer :: msb begin
context includes integer.lifting begin

lift_definition msb_integer :: "integer ⇒ bool" is msb .

instance ..

end
end

instantiation integer :: set_bit begin
context includes integer.lifting begin

lift_definition set_bit_integer :: "integer ⇒ nat ⇒ bool ⇒ integer" is set_bit .

instance
apply standard
apply transfer
apply (simp add: bit_simps)
done

end
end

abbreviation (input) wf_set_bits_integer
where "wf_set_bits_integer ≡ wf_set_bits_int"

section ‹Target language implementations›

text ‹
Unfortunately, this is not straightforward,
because these API functions have different signatures and preconditions on the parameters:

\begin{description}
\item[Standard ML] Shifts in IntInf are given as word, but not IntInf.
\item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer.
\end{description}

Additional constants take only parameters of type @{typ integer} rather than @{typ nat}
and check the preconditions as far as possible (e.g., being non-negative) in a portable way.
Manual implementations inside code\_printing perform the remaining range checks and convert
these @{typ integer}s into the right type.

For normalisation by evaluation, we derive custom code equations, because NBE
does not know these code\_printing serialisations and would otherwise loop.
›

code_identifier code_module Bits_Integer ⇀
(SML) Bits_Int and (OCaml) Bits_Int and (Haskell) Bits_Int and (Scala) Bits_Int

code_printing code_module Bits_Integer ⇀ (SML)
‹structure Bits_Integer : sig
val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int
val shiftl : IntInf.int -> IntInf.int -> IntInf.int
val shiftr : IntInf.int -> IntInf.int -> IntInf.int
val test_bit : IntInf.int -> IntInf.int -> bool
end = struct

val maxWord = IntInf.pow (2, Word.wordSize);

fun set_bit x n b =
if n < maxWord then
if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

fun shiftl x n =
if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n))
else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun shiftr x n =
if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
else raise (Fail ("Shift operand too large: " ^ IntInf.toString n));

fun test_bit x n =
if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
else raise (Fail ("Bit index too large: " ^ IntInf.toString n));

end; (*struct Bits_Integer*)›
code_reserved SML Bits_Integer

code_printing code_module Bits_Integer ⇀ (OCaml)
‹module Bits_Integer : sig
val shiftl : Z.t -> Z.t -> Z.t
val shiftr : Z.t -> Z.t -> Z.t
val test_bit : Z.t -> Z.t -> bool
end = struct

(* We do not need an explicit range checks here,
because Big_int.int_of_big_int raises Failure
if the argument does not fit into an int. *)
let shiftl x n = Z.shift_left x (Z.to_int n);;

let shiftr x n = Z.shift_right x (Z.to_int n);;

let test_bit x n =  Z.testbit x (Z.to_int n);;

end;; (*struct Bits_Integer*)›
code_reserved OCaml Bits_Integer

code_printing code_module Data_Bits ⇀ (Haskell)
‹
module Data_Bits where {

import qualified Data.Bits;

{-
The ...Bounded functions assume that the Integer argument for the shift
or bit index fits into an Int, is non-negative and (for types of fixed bit width)
less than bitSize
-}

infixl 7 .&.;
infixl 6 xor;
infixl 5 .|.;

(.&.) :: Data.Bits.Bits a => a -> a -> a;
(.&.) = (Data.Bits..&.);

xor :: Data.Bits.Bits a => a -> a -> a;
xor = Data.Bits.xor;

(.|.) :: Data.Bits.Bits a => a -> a -> a;
(.|.) = (Data.Bits..|.);

complement :: Data.Bits.Bits a => a -> a;
complement = Data.Bits.complement;

testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool;
testBitUnbounded x b
| b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b)
| otherwise = error ("Bit index too large: " ++ show b)
;

testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool;
testBitBounded x b = Data.Bits.testBit x (fromInteger b);

setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
setBitUnbounded x n b
| n <= toInteger (Prelude.maxBound :: Int) =
if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n)
| otherwise = error ("Bit index too large: " ++ show n)
;

setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a;
setBitBounded x n True = Data.Bits.setBit x (fromInteger n);
setBitBounded x n False = Data.Bits.clearBit x (fromInteger n);

shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftlUnbounded x n
| n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n)
| otherwise = error ("Shift operand too large: " ++ show n)
;

shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftlBounded x n = Data.Bits.shiftL x (fromInteger n);

shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a;
shiftrUnbounded x n
| n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n)
| otherwise = error ("Shift operand too large: " ++ show n)
;

shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a;
shiftrBounded x n = Data.Bits.shiftR x (fromInteger n);

}›

and ― ‹@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to
Haskell's Prelude.Int type instead of Integer. For compatibility
with the Haskell target, we nevertheless provide bounded and
unbounded functions.›
‹
module Data_Bits where {

import qualified Data.Bits;

{-
The functions assume that the Int argument for the shift or bit index is
non-negative and (for types of fixed bit width) less than bitSize
-}

infixl 7 .&.;
infixl 6 xor;
infixl 5 .|.;

(.&.) :: Data.Bits.Bits a => a -> a -> a;
(.&.) = (Data.Bits..&.);

xor :: Data.Bits.Bits a => a -> a -> a;
xor = Data.Bits.xor;

(.|.) :: Data.Bits.Bits a => a -> a -> a;
(.|.) = (Data.Bits..|.);

complement :: Data.Bits.Bits a => a -> a;
complement = Data.Bits.complement;

testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
testBitUnbounded = Data.Bits.testBit;

testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool;
testBitBounded = Data.Bits.testBit;

setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
setBitUnbounded x n True = Data.Bits.setBit x n;
setBitUnbounded x n False = Data.Bits.clearBit x n;

setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a;
setBitBounded x n True = Data.Bits.setBit x n;
setBitBounded x n False = Data.Bits.clearBit x n;

shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftlUnbounded = Data.Bits.shiftL;

shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftlBounded = Data.Bits.shiftL;

shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a;
shiftrUnbounded = Data.Bits.shiftR;

shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a;
shiftrBounded = Data.Bits.shiftR;

}›

code_printing code_module Bits_Integer ⇀ (Scala)
‹object Bits_Integer {

def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt =
if (n.isValidInt)
if (b)
x.setBit(n.toInt)
else
x.clearBit(n.toInt)
else
sys.error("Bit index too large: " + n.toString)

def shiftl(x: BigInt, n: BigInt) : BigInt =
if (n.isValidInt)
x << n.toInt
else
sys.error("Shift index too large: " + n.toString)

def shiftr(x: BigInt, n: BigInt) : BigInt =
if (n.isValidInt)
x << n.toInt
else
sys.error("Shift index too large: " + n.toString)

def testBit(x: BigInt, n: BigInt) : Boolean =
if (n.isValidInt)
x.testBit(n.toInt)
else
sys.error("Bit index too large: " + n.toString)

} /* object Bits_Integer */›

code_printing
constant "(AND) :: integer ⇒ integer ⇒ integer" ⇀
(SML) "IntInf.andb ((_),/ (_))" and
(OCaml) "Z.logand" and
(Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and
(Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
(Scala) infixl 3 "&"
| constant "(OR) :: integer ⇒ integer ⇒ integer" ⇀
(SML) "IntInf.orb ((_),/ (_))" and
(OCaml) "Z.logor" and
(Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and
(Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
(Scala) infixl 1 "|"
| constant "(XOR) :: integer ⇒ integer ⇒ integer" ⇀
(SML) "IntInf.xorb ((_),/ (_))" and
(OCaml) "Z.logxor" and
(Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
(Scala) infixl 2 "^"
| constant "NOT :: integer ⇒ integer" ⇀
(SML) "IntInf.notb" and
(OCaml) "Z.lognot" and
(Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and
(Scala) "_.unary'_~"

code_printing constant bin_rest_integer ⇀
(SML) "IntInf.div ((_), 2)" and
(OCaml) "Z.shift'_right/ _/ 1" and
(Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and
(Scala) "_ >> 1"

context
includes integer.lifting
begin

lemma bitNOT_integer_code [code]:
fixes i :: integer shows
"NOT i = - i - 1"
by transfer(simp add: int_not_def)

lemma bin_rest_integer_code [code nbe]:
"bin_rest_integer i = i div 2"
by transfer rule

lemma bin_last_integer_code [code]:
"bin_last_integer i ⟷ i AND 1 ≠ 0"
by transfer (rule bin_last_conv_AND)

lemma bin_last_integer_nbe [code nbe]:
"bin_last_integer i ⟷ i mod 2 ≠ 0"
by transfer(simp add: bin_last_def)

lemma bitval_bin_last_integer [code_unfold]:
"of_bool (bin_last_integer i) = i AND 1"
by transfer(rule bitval_bin_last)

end

definition integer_test_bit :: "integer ⇒ integer ⇒ bool"
where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))"

declare [[code drop: ‹bit :: integer ⇒ nat ⇒ bool›]]

lemma bit_integer_code [code]:
"bit x n ⟷ integer_test_bit x (integer_of_nat n)"
by (simp add: integer_test_bit_def)

lemma integer_test_bit_code [code]:
"integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
"integer_test_bit 0 0 = False"
"integer_test_bit 0 (Code_Numeral.Pos n) = False"
"integer_test_bit (Code_Numeral.Pos num.One)      0 = True"
"integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False"
"integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True"
"integer_test_bit (Code_Numeral.Pos num.One)      (Code_Numeral.Pos n') = False"
"integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') =
integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
"integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') =
integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)"
"integer_test_bit (Code_Numeral.Neg num.One)      0 = True"
"integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False"
"integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True"
"integer_test_bit (Code_Numeral.Neg num.One)      (Code_Numeral.Pos n') = True"
"integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') =
integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)"
"integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') =
integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)"
apply (simp_all add: integer_test_bit_def bit_integer_def)
using bin_nth_numeral_simps bit_numeral_int_simps(6)
by presburger

code_printing constant integer_test_bit ⇀
(SML) "Bits'_Integer.test'_bit" and
(OCaml) "Bits'_Integer.test'_bit" and
(Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and
(Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and
(Scala) "Bits'_Integer.testBit"

context
includes integer.lifting
begin

lemma lsb_integer_code [code]:
fixes x :: integer shows
"lsb x = bit x 0"
by transfer(simp add: lsb_int_def)

definition integer_set_bit :: "integer ⇒ integer ⇒ bool ⇒ integer"
where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)"

lemma set_bit_integer_code [code]:
"set_bit x i b = integer_set_bit x (integer_of_nat i) b"

fixes x :: integer shows
"set_bit x i b = (if b then x OR (1 << i) else x AND NOT (1 << i))"
by transfer (simp add: int_set_bit_False_conv_NAND int_set_bit_True_conv_OR shiftl_eq_push_bit)

end

code_printing constant integer_set_bit ⇀
(SML) "Bits'_Integer.set'_bit" and
(Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and
(Scala) "Bits'_Integer.setBit"

text ‹
OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks.
We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR.
›
lemma integer_set_bit_code [code]:
"integer_set_bit x n b =
(if n < 0 then undefined x n b else
if b then x OR (push_bit (nat_of_integer n) 1)
else x AND NOT (push_bit (nat_of_integer n) 1))"
by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def)

definition integer_shiftl :: "integer ⇒ integer ⇒ integer"
where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)"

declare [[code drop: ‹push_bit :: nat ⇒ integer ⇒ integer›]]

lemma shiftl_integer_code [code]:
fixes x :: integer shows
"push_bit n x = integer_shiftl x (integer_of_nat n)"
by(auto simp add: integer_shiftl_def)

context
includes integer.lifting
begin

lemma shiftl_integer_conv_mult_pow2:
fixes x :: integer shows
"x << n = x * 2 ^ n"
by (simp add: push_bit_eq_mult shiftl_eq_push_bit)

lemma integer_shiftl_code [code]:
"integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
"integer_shiftl x 0 = x"
"integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)"
"integer_shiftl 0 (Code_Numeral.Pos n) = 0"
apply (simp_all add: integer_shiftl_def numeral_eq_Suc)
apply transfer
apply (simp add: ac_simps)
done

end

code_printing constant integer_shiftl ⇀
(SML) "Bits'_Integer.shiftl" and
(OCaml) "Bits'_Integer.shiftl" and
(Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
(Scala) "Bits'_Integer.shiftl"

definition integer_shiftr :: "integer ⇒ integer ⇒ integer"
where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)"

declare [[code drop: ‹drop_bit :: nat ⇒ integer ⇒ integer›]]

lemma shiftr_integer_conv_div_pow2:
includes integer.lifting fixes x :: integer shows
"x >> n = x div 2 ^ n"
by (simp add: drop_bit_eq_div shiftr_eq_drop_bit)

lemma shiftr_integer_code [code]:
fixes x :: integer shows
"drop_bit n x = integer_shiftr x (integer_of_nat n)"
by(auto simp add: integer_shiftr_def)

code_printing constant integer_shiftr ⇀
(SML) "Bits'_Integer.shiftr" and
(OCaml) "Bits'_Integer.shiftr" and
(Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and
(Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and
(Scala) "Bits'_Integer.shiftr"

lemma integer_shiftr_code [code]:
includes integer.lifting
shows
"integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)"
"integer_shiftr x 0 = x"
"integer_shiftr 0 (Code_Numeral.Pos n) = 0"
"integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0"
"integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) =
integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
"integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) =
integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)"
"integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1"
"integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) =
integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)"
"integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) =
integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)"
apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc)
apply transfer apply simp
apply transfer apply simp
done

context
includes integer.lifting
begin

lemma Bit_integer_code [code]:
"Bit_integer i False = push_bit 1 i"
"Bit_integer i True = (push_bit 1 i) + 1"
by (transfer; simp add: shiftl_int_def)+

lemma msb_integer_code [code]:
"msb (x :: integer) ⟷ x < 0"
by transfer(simp add: msb_int_def)

end

context
includes integer.lifting natural.lifting
begin

lemma bitAND_integer_unfold [code]:
"x AND y =
(if x = 0 then 0
else if x = - 1 then y
else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x ∧ bin_last_integer y))"
by transfer
(auto simp add: algebra_simps
and_int_rec [of _ ‹_ * 2›] and_int_rec [of ‹_ * 2›] and_int_rec [of ‹1 + _ * 2›]
elim!: evenE oddE)

lemma bitOR_integer_unfold [code]:
"x OR y =
(if x = 0 then y
else if x = - 1 then - 1
else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x ∨ bin_last_integer y))"
by transfer
(auto simp add: algebra_simps
or_int_rec [of _ ‹_ * 2›] or_int_rec [of _ ‹1 + _ * 2›] or_int_rec [of ‹1 + _ * 2›]
elim!: evenE oddE)

lemma bitXOR_integer_unfold [code]:
"x XOR y =
(if x = 0 then y
else if x = - 1 then NOT y
else Bit_integer (bin_rest_integer x XOR bin_rest_integer y)
(¬ bin_last_integer x ⟷ bin_last_integer y))"
by transfer
(auto simp add: algebra_simps
xor_int_rec [of _ ‹_ * 2›] xor_int_rec [of ‹_ * 2›] xor_int_rec [of ‹1 + _ * 2›]
elim!: evenE oddE)

end

section ‹Test code generator setup›

definition bit_integer_test :: "bool" where
"bit_integer_test =
(([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5)
, -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5)
, NOT 1, NOT (- 3)
, -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3)
, set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False
, 1 << 2, -1 << 3
, 100 >> 3, -100 >> 3] :: integer list)
= [ 3, 1, 1, -7
, -3, -3, 7, -1
, -2, 2
, -4, -4, 6, 6
, 21, -1, 4, -7
, 4, -8
, 12, -13] ∧
[ (5 :: integer) !! 4, (5 :: integer) !! 2, (-5 :: integer) !! 4, (-5 :: integer) !! 2
, lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer),
msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)]
= [ False, True, True, False,
True, False, True, False,
False, False, True, True])"

export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala

have bit_integer_test by eval
have bit_integer_test by normalization
have bit_integer_test by code_simp
end
ML_val ‹val true = @{code bit_integer_test}›

lemma "x AND y = x OR (y :: integer)"
quickcheck[random, expect=counterexample]
quickcheck[exhaustive, expect=counterexample]
oops

lemma "(x :: integer) AND x = x OR x"
quickcheck[narrowing, expect=no_counterexample]
oops

lemma "(f :: integer ⇒ unit) = g"
quickcheck[narrowing, size=3, expect=no_counterexample]

hide_const bit_integer_test
hide_fact bit_integer_test_def

end


# Theory Code_Target_Bits_Int

(*  Title:      Code_Target_Bits_Int.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Implementation of bit operations on int by target language operations›

theory Code_Target_Bits_Int
imports
Bits_Integer
"HOL-Library.Code_Target_Int"
begin

declare [[code drop:
"(AND) :: int ⇒ _" "(OR) :: int ⇒ _" "(XOR) :: int ⇒ _" "(NOT) :: int ⇒ _"
"lsb :: int ⇒ _" "set_bit :: int ⇒ _" "bit :: int ⇒ _"
"push_bit :: _ ⇒ int ⇒ _" "drop_bit :: _ ⇒ int ⇒ _"
int_of_integer_symbolic
]]

declare bitval_bin_last [code_unfold]

lemma [code_unfold]:
‹bit x n ⟷ x AND (push_bit n 1) ≠ 0› for x :: int
by (fact bit_iff_and_push_bit_not_eq_0)

context
includes integer.lifting
begin

lemma bit_int_code [code]:
"bit (int_of_integer x) n = bit x n"
by transfer simp

lemma and_int_code [code]:
"int_of_integer i AND int_of_integer j = int_of_integer (i AND j)"
by transfer simp

lemma or_int_code [code]:
"int_of_integer i OR int_of_integer j = int_of_integer (i OR j)"
by transfer simp

lemma xor_int_code [code]:
"int_of_integer i XOR int_of_integer j = int_of_integer (i XOR j)"
by transfer simp

lemma not_int_code [code]:
"NOT (int_of_integer i) = int_of_integer (NOT i)"
by transfer simp

lemma push_bit_int_code [code]:
‹push_bit n (int_of_integer x) = int_of_integer (push_bit n x)›
by transfer simp

lemma drop_bit_int_code [code]:
‹drop_bit n (int_of_integer x) = int_of_integer (drop_bit n x)›
by transfer simp

lemma take_bit_int_code [code]:
‹take_bit n (int_of_integer x) = int_of_integer (take_bit n x)›
by transfer simp

lemma lsb_int_code [code]:
"lsb (int_of_integer x) = lsb x"
by transfer simp

lemma set_bit_int_code [code]:
"set_bit (int_of_integer x) n b = int_of_integer (set_bit x n b)"
by transfer simp

lemma int_of_integer_symbolic_code [code]:
"int_of_integer_symbolic = int_of_integer"
by (simp add: int_of_integer_symbolic_def)

context
begin

qualified definition even :: ‹int ⇒ bool›
where [code_abbrev]: ‹even = Parity.even›

end

lemma [code]:
‹Code_Target_Bits_Int.even i ⟷ i AND 1 = 0›
by (simp add: Code_Target_Bits_Int.even_def even_iff_mod_2_eq_zero and_one_eq)

lemma bin_rest_code:
"bin_rest (int_of_integer i) = int_of_integer (bin_rest_integer i)"
by transfer simp

end

end


# Theory Code_Target_Word_Base

(*  Title:      Code_Target_Word_Base.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Common base for target language implementations of word types›

theory Code_Target_Word_Base imports
"HOL-Library.Word"
"Word_Lib.Signed_Division_Word"
Bits_Integer
begin

text ‹More lemmas›

lemma div_half_nat:
fixes x y :: nat
assumes "y ≠ 0"
shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y ≤ r then (q + 1, r - y) else (q, r))"
proof -
let ?q = "2 * (x div 2 div y)"
have q: "?q = x div y - x div y mod 2"
by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric])
let ?r = "x - ?q * y"
have r: "?r = x mod y + x div y mod 2 * y"
by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute)

show ?thesis
proof(cases "y ≤ x - ?q * y")
case True
with assms q have "x div y mod 2 ≠ 0" unfolding r
by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1))
hence "x div y = ?q + 1" unfolding q
by simp
moreover hence "x mod y = ?r - y"
by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc)
ultimately show ?thesis using True by(simp add: Let_def)
next
case False
hence "x div y mod 2 = 0" unfolding r
by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute)
hence "x div y = ?q" unfolding q by simp
moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric])
ultimately show ?thesis using False by(simp add: Let_def)
qed
qed

lemma div_half_word:
fixes x y :: "'a :: len word"
assumes "y ≠ 0"
shows "(x div y, x mod y) = (let q = (x >> 1) div y << 1; r = x - q * y in if y ≤ r then (q + 1, r - y) else (q, r))"
proof -
obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)"
by (rule that [of ‹unat x›]) simp_all
moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)"
by (rule that [of ‹unat y›]) simp_all
ultimately have [simp]: ‹unat (of_nat n :: 'a word) = n› ‹unat (of_nat m :: 'a word) = m›
by (transfer, simp add: take_bit_of_nat take_bit_nat_eq_self_iff)+
let ?q = "(x >> 1) div y << 1"
let ?q' = "2 * (n div 2 div m)"
have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse unat_lt2p uno_simps(2))
hence q: "?q = of_nat ?q'" using n m
by (auto simp add: shiftr_word_eq drop_bit_eq_div shiftl_t2n word_arith_nat_div uno_simps take_bit_nat_eq_self)
from assms have "m ≠ 0" using m by -(rule notI, simp)

from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)"
by(metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unat_lt2p uno_simps(2))
moreover
have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric]
by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq)
moreover have "2 * (n div 2 div m) * m ≤ n"
by (simp flip: div_mult2_eq ac_simps)
ultimately
have r: "x - ?q * y = of_nat (n - ?q' * m)"
and "y ≤ x - ?q * y ⟹ of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)"
using n m unfolding q
apply (simp_all add: of_nat_diff)
apply (subst of_nat_diff)
apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths)
done
then show ?thesis using n m div_half_nat [OF ‹m ≠ 0›, of n] unfolding q
by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self
flip: zdiv_int zmod_int
split del: if_split split: if_split_asm)
qed

lemma word_test_bit_set_bits: "(BITS n. f n :: 'a :: len word) !! n ⟷ n < LENGTH('a) ∧ f n"
by (simp add: test_bit_eq_bit bit_set_bits_word_iff)

lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. i !! n)"
by (rule word_eqI) (auto simp add: word_test_bit_set_bits)

"n !! index ⟹ (n AND mask index) OR (1 << index) = n AND mask (index + 1)"
for n :: ‹'a::len word›
by(rule word_eqI)(auto simp add: word_ao_nth word_size nth_shiftl simp del: shiftl_1)

fixes n :: "'a :: len word"
assumes "n !! (LENGTH('a) - 1)"
and "mask1 = mask (LENGTH('a) - 1)"
and "mask2 = 1 << LENGTH('a) - 1"
shows "uint (n AND mask1) OR mask2 = uint n"
proof -
have "mask2 = uint (1 << LENGTH('a) - 1 :: 'a word)" using assms
by (simp add: uint_shiftl word_size bintrunc_shiftl del: shiftl_1)
hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (1 << LENGTH('a) - 1 :: 'a word))"
also have "… = uint (n AND mask (LENGTH('a) - 1 + 1))"
also have "… = uint n" by simp
finally show ?thesis .
qed

text ‹Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.›

lemmas word_sdiv_def = sdiv_word_def
lemmas word_smod_def = smod_word_def

lemma [code]:
"x sdiv y =
(let x' = sint x; y' = sint y;
negative = (x' < 0) ≠ (y' < 0);
result = abs x' div abs y'
in word_of_int (if negative then -result else result))"
for x y :: ‹'a::len word›
by (simp add: sdiv_word_def signed_divide_int_def sgn_if Let_def not_less not_le)

lemma [code]:
"x smod y =
(let x' = sint x; y' = sint y;
negative = (x' < 0);
result = abs x' mod abs y'
in word_of_int (if negative then -result else result))"
for x y :: ‹'a::len word›
proof -
have *: ‹k mod l = k - k div l * l› for k l :: int
by (simp add: minus_div_mult_eq_mod)
show ?thesis
by (simp add: smod_word_def signed_modulo_int_def signed_divide_int_def * sgn_if Let_def)
qed

text ‹
This algorithm implements unsigned division in terms of signed division.
Taken from Hacker's Delight.
›

lemma divmod_via_sdivmod:
fixes x y :: "'a :: len word"
assumes "y ≠ 0"
shows
"(x div y, x mod y) =
(if 1 << (LENGTH('a) - 1) ≤ y then if x < y then (0, x) else (1, x - y)
else let q = ((x >> 1) sdiv y) << 1;
r = x - q * y
in if r ≥ y then (q + 1, r - y) else (q, r))"
proof(cases "1 << (LENGTH('a) - 1) ≤ y")
case True
note y = this
show ?thesis
proof(cases "x < y")
case True
then have "x mod y = x"
by transfer simp
thus ?thesis using True y by(simp add: word_div_lt_eq_0)
next
case False
obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)"
by (rule that [of ‹unat y›]) simp_all
have "unat x < 2 ^ LENGTH('a)" by(rule unat_lt2p)
also have "… = 2 * 2 ^ (LENGTH('a) - 1)"
by(metis Suc_pred len_gt_0 power_Suc One_nat_def)
also have "… ≤ 2 * n" using y n
by transfer (simp add: push_bit_of_1 take_bit_eq_mod)
finally have div: "x div of_nat n = 1" using False n
by (simp add: word_div_eq_1_iff take_bit_nat_eq_self)
moreover have "x mod y = x - x div y * y"
by (simp add: minus_div_mult_eq_mod)
with div n have "x mod y = x - y" by simp
ultimately show ?thesis using False y n by simp
qed
next
case False
note y = this
obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)"
by (rule that [of ‹unat x›]) simp_all
hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
by (cases ‹LENGTH('a)›)
(auto dest: less_imp_of_nat_less [where ?'a = int])
with y n have "sint (x >> 1) = uint (x >> 1)"
by (simp add: sint_uint sbintrunc_mod2p shiftr_div_2n take_bit_nat_eq_self)
moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)"
using y by (cases "LENGTH('a)")
(simp_all add: not_le word_2p_lem word_size)
then have "sint y = uint y"
by (simp add: sint_uint sbintrunc_mod2p)
ultimately show ?thesis using y
apply (subst div_half_word [OF assms])
apply (simp add: sdiv_word_def signed_divide_int_def flip: uint_div)
done
qed

text ‹More implementations tailored towards target-language implementations›

context
includes integer.lifting
begin
lift_definition word_of_integer :: "integer ⇒ 'a :: len word" is word_of_int .

lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)"
end

lemma word_of_int_code:
"uint (word_of_int x :: 'a word) = x AND mask (LENGTH('a :: len))"

context fixes f :: "nat ⇒ bool" begin

definition set_bits_aux :: ‹'a word ⇒ nat ⇒ 'a :: len word›
where ‹set_bits_aux w n = push_bit n w OR take_bit n (set_bits f)›

lemma set_bits_aux_conv:
‹set_bits_aux w n = (w << n) OR (set_bits f AND mask n)›
for w :: ‹'a::len word›
by (rule bit_word_eqI)
(auto simp add: set_bits_aux_def shiftl_word_eq bit_and_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_mask_iff bit_set_bits_word_iff)

corollary set_bits_conv_set_bits_aux:
‹set_bits f = (set_bits_aux 0 (LENGTH('a)) :: 'a :: len word)›
by (simp add: set_bits_aux_conv)

lemma set_bits_aux_0 [simp]:
‹set_bits_aux w 0 = w›
by  (simp add: set_bits_aux_conv)

lemma set_bits_aux_Suc [simp]:
‹set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n›
by (simp add: set_bits_aux_def shiftl_word_eq bit_eq_iff bit_or_iff bit_push_bit_iff bit_take_bit_iff bit_set_bits_word_iff)
(auto simp add: bit_exp_iff not_less bit_1_iff less_Suc_eq_le)

lemma set_bits_aux_simps [code]:
‹set_bits_aux w 0 = w›
‹set_bits_aux w (Suc n) = set_bits_aux ((w << 1) OR (if f n then 1 else 0)) n›
by simp_all

end

lemma word_of_int_via_signed:
and shift_def: "shift = 1 << LENGTH('a)"
and index_def: "index = LENGTH('a) - 1"
and overflow_def:"overflow = 1 << (LENGTH('a) - 1)"
and least_def: "least = - overflow"
shows
"(word_of_int i :: 'a :: len word) =
(let i' = i AND mask
in if i' !! index then
if i' - shift < least ∨ overflow ≤ i' - shift then arbitrary1 i' else word_of_int (i' - shift)
else if i' < least ∨ overflow ≤ i' then arbitrary2 i' else word_of_int i')"
proof -
define i' where "i' = i AND mask"
have "shift = mask + 1" unfolding assms by(simp add: bin_mask_p1_conv_shift)
hence "i' < shift" by(simp add: mask_def i'_def int_and_le)
show ?thesis
proof(cases "i' !! index")
case True
then have unf: "i' = overflow OR i'"
apply (simp add: assms i'_def shiftl_eq_push_bit push_bit_of_1 flip: take_bit_eq_mask)
apply (rule bit_eqI)
apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff)
done
have "overflow ≤ i'" by(subst unf)(rule le_int_or, simp add: bin_sign_and assms i'_def)
hence "i' - shift < least ⟷ False" unfolding assms
by(cases "LENGTH('a)")(simp_all add: not_less)
moreover
have "overflow ≤ i' - shift ⟷ False" using ‹i' < shift› unfolding assms
by(cases "LENGTH('a)")(auto simp add: not_le elim: less_le_trans)
moreover
have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using ‹i' < shift›
by (simp add: i'_def shift_def mask_def shiftl_eq_push_bit push_bit_of_1 word_of_int_eq_iff flip: take_bit_eq_mask)
ultimately show ?thesis using True by(simp add: Let_def i'_def)
next
case False
hence "i' = i AND Bit_Operations.mask (LENGTH('a) - 1)" unfolding assms i'_def
by(clarsimp simp add: i'_def bin_nth_ops intro!: bin_eqI)(cases "LENGTH('a)", auto simp add: less_Suc_eq)
also have "… ≤ Bit_Operations.mask (LENGTH('a) - 1)" by(rule int_and_le) simp
also have "… < overflow" unfolding overflow_def
also
have "least ≤ 0" unfolding least_def overflow_def by simp
have "0 ≤ i'" by (simp add: i'_def mask_def)
hence "least ≤ i'" using ‹least ≤ 0› by simp
moreover
have "word_of_int i' = (word_of_int i :: 'a word)"
by(rule word_eqI)(auto simp add: i'_def bin_nth_ops mask_def)
ultimately show ?thesis using False by(simp add: Let_def i'_def)
qed
qed

text ‹Quickcheck conversion functions›

context
includes state_combinator_syntax
begin

definition qc_random_cnv ::
"(natural ⇒ 'a::term_of) ⇒ natural ⇒ Random.seed
⇒ ('a × (unit ⇒ Code_Evaluation.term)) × Random.seed"
where "qc_random_cnv a_of_natural i = Random.range (i + 1) ∘→ (λk. Pair (
let n = a_of_natural k
in (n, λ_. Code_Evaluation.term_of n)))"

end

definition qc_exhaustive_cnv :: "(natural ⇒ 'a) ⇒ ('a ⇒ (bool × term list) option)
⇒ natural ⇒ (bool × term list) option"
where
"qc_exhaustive_cnv a_of_natural f d =
Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d"

definition qc_full_exhaustive_cnv ::
"(natural ⇒ ('a::term_of)) ⇒ ('a × (unit ⇒ term) ⇒ (bool × term list) option)
⇒ natural ⇒ (bool × term list) option"
where
"qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive
(%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d"

declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]]

definition qc_narrowing_drawn_from :: "'a list ⇒ integer ⇒ _"
where
"qc_narrowing_drawn_from xs =
foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))"

locale quickcheck_narrowing_samples =
fixes a_of_integer :: "integer ⇒ 'a × 'a :: {partial_term_of, term_of}"
and zero :: "'a"
and tr :: "typerep"
begin

function narrowing_samples :: "integer ⇒ 'a list"
where
"narrowing_samples i =
(if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])"
by pat_completeness auto
termination including integer.lifting
proof(relation "measure nat_of_integer")
fix i :: integer
assume "0 < i"
thus "(i - 1, i) ∈ measure nat_of_integer"
by simp(transfer, simp)
qed simp

definition partial_term_of_sample :: "integer ⇒ 'a"
where
"partial_term_of_sample i =
(if i < 0 then undefined
else if i = 0 then zero
else if i mod 2 = 0 then snd (a_of_integer (i div 2))
else fst (a_of_integer (i div 2 + 1)))"

lemma partial_term_of_code:
"partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) ≡
Code_Evaluation.Free (STR ''_'') tr"
"partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) ≡
Code_Evaluation.term_of (partial_term_of_sample i)"
by (rule partial_term_of_anything)+

end

lemmas [code] =
quickcheck_narrowing_samples.narrowing_samples.simps
quickcheck_narrowing_samples.partial_term_of_sample_def

text ‹
The separate code target ‹SML_word› collects setups for the
code generator that PolyML does not provide.
›

setup ‹Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])›

code_identifier code_module Code_Target_Word_Base ⇀
(SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word

end


# Theory Uint64

(*  Title:      Uint64.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 64 bits›

theory Uint64 imports
Code_Target_Word_Base
begin

text ‹
PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode.
Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and
masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations
directly to the \verb$Word64$ structure provided by the Standard ML implementations.

The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at
runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit
version which does not suffer from a division bug found in PolyML 5.6.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint64 = "UNIV :: 64 word set" ..

setup_lifting type_definition_uint64

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint64}.›
declare Rep_uint64_inverse[code abstype]

declare Quotient_uint64[transfer_rule]

instantiation uint64 :: comm_ring_1
begin
lift_definition zero_uint64 :: uint64 is "0 :: 64 word" .
lift_definition one_uint64 :: uint64 is "1" .
lift_definition plus_uint64 :: "uint64 ⇒ uint64 ⇒ uint64" is "(+) :: 64 word ⇒ _" .
lift_definition minus_uint64 :: "uint64 ⇒ uint64 ⇒ uint64" is "(-)" .
lift_definition uminus_uint64 :: "uint64 ⇒ uint64" is uminus .
lift_definition times_uint64 :: "uint64 ⇒ uint64 ⇒ uint64" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint64 :: semiring_modulo
begin
lift_definition divide_uint64 :: "uint64 ⇒ uint64 ⇒ uint64" is "(div)" .
lift_definition modulo_uint64 :: "uint64 ⇒ uint64 ⇒ uint64" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint64 :: linorder begin
lift_definition less_uint64 :: "uint64 ⇒ uint64 ⇒ bool" is "(<)" .
lift_definition less_eq_uint64 :: "uint64 ⇒ uint64 ⇒ bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint64.rep_eq less_eq_uint64.rep_eq

context
includes lifting_syntax
notes
transfer_rule_of_bool [transfer_rule]
transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
"((=) ===> cr_uint64) of_bool of_bool"
by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
"((=) ===> cr_uint64) numeral numeral"
by transfer_prover

lemma [transfer_rule]:
‹(cr_uint64 ===> (⟷)) even ((dvd) 2 :: uint64 ⇒ bool)›
by (unfold dvd_def) transfer_prover

end

instantiation uint64 :: semiring_bits
begin

lift_definition bit_uint64 :: ‹uint64 ⇒ nat ⇒ bool› is bit .

instance
by (standard; transfer)
(fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint64 :: semiring_bit_shifts
begin
lift_definition push_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is push_bit .
lift_definition drop_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is drop_bit .
lift_definition take_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is take_bit .
instance by (standard; transfer)
(fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint64 :: ring_bit_operations
begin
lift_definition not_uint64 :: ‹uint64 ⇒ uint64› is NOT .
lift_definition and_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(AND)› .
lift_definition or_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(OR)› .
lift_definition xor_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(XOR)› .
lift_definition mask_uint64 :: ‹nat ⇒ uint64› is mask .
instance by (standard; transfer)
(simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
‹take_bit n a = a AND mask n› for a :: uint64

lemma [code]:
‹mask (Suc n) = push_bit n (1 :: uint64) OR mask n›
‹mask 0 = (0 :: uint64)›

instance uint64 :: semiring_bit_syntax ..

context
includes lifting_syntax
begin

lemma test_bit_uint64_transfer [transfer_rule]:
‹(cr_uint64 ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint64_transfer [transfer_rule]:
‹(cr_uint64 ===> (=) ===> cr_uint64) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint64_transfer [transfer_rule]:
‹(cr_uint64 ===> (=) ===> cr_uint64) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint64 :: lsb
begin
lift_definition lsb_uint64 :: ‹uint64 ⇒ bool› is lsb .
instance by (standard; transfer)
(fact lsb_odd)
end

instantiation uint64 :: msb
begin
lift_definition msb_uint64 :: ‹uint64 ⇒ bool› is msb .
instance ..
end

instantiation uint64 :: set_bit
begin
lift_definition set_bit_uint64 :: ‹uint64 ⇒ nat ⇒ bool ⇒ uint64› is set_bit .
instance
apply standard
apply transfer
apply (simp add: bit_simps)
done
end

instantiation uint64 :: bit_comprehension begin
lift_definition set_bits_uint64 :: "(nat ⇒ bool) ⇒ uint64" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint64.rep_eq lsb_uint64.rep_eq msb_uint64.rep_eq

instantiation uint64 :: equal begin
lift_definition equal_uint64 :: "uint64 ⇒ uint64 ⇒ bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint64.rep_eq

instantiation uint64 :: size begin
lift_definition size_uint64 :: "uint64 ⇒ nat" is "size" .
instance ..
end

lemmas [code] = size_uint64.rep_eq

lift_definition sshiftr_uint64 :: "uint64 ⇒ nat ⇒ uint64" (infixl ">>>" 55) is ‹λw n. signed_drop_bit n w› .

lift_definition uint64_of_int :: "int ⇒ uint64" is "word_of_int" .

definition uint64_of_nat :: "nat ⇒ uint64"
where "uint64_of_nat = uint64_of_int ∘ int"

lift_definition int_of_uint64 :: "uint64 ⇒ int" is "uint" .
lift_definition nat_of_uint64 :: "uint64 ⇒ nat" is "unat" .

definition integer_of_uint64 :: "uint64 ⇒ integer"
where "integer_of_uint64 = integer_of_int o int_of_uint64"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint64 :: "integer ⇒ uint64" is "word_of_int" .

lemma Rep_uint64_numeral [simp]: "Rep_uint64 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint64_def Abs_uint64_inverse numeral.simps plus_uint64_def)

lemma numeral_uint64_transfer [transfer_rule]:
"(rel_fun (=) cr_uint64) numeral numeral"
by(auto simp add: cr_uint64_def)

lemma numeral_uint64 [code_unfold]: "numeral n = Uint64 (numeral n)"
by transfer simp

lemma Rep_uint64_neg_numeral [simp]: "Rep_uint64 (- numeral n) = - numeral n"
by(simp only: uminus_uint64_def)(simp add: Abs_uint64_inverse)

lemma neg_numeral_uint64 [code_unfold]: "- numeral n = Uint64 (- numeral n)"
by transfer(simp add: cr_uint64_def)

end

lemma Abs_uint64_numeral [code_post]: "Abs_uint64 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint64_def numeral.simps plus_uint64_def Abs_uint64_inverse)

lemma Abs_uint64_0 [code_post]: "Abs_uint64 0 = 0"

lemma Abs_uint64_1 [code_post]: "Abs_uint64 1 = 1"

section ‹Code setup›

text ‹ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$.
If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume
that there is also a ‹Word64› structure available and accordingly replace the implementation
for the target \verb$Eval$.
›
code_printing code_module "Uint64" ⇀ (SML) ‹(* Test that words can handle numbers between 0 and 63 *)
val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6"));

structure Uint64 : sig
eqtype uint64;
val zero : uint64;
val one : uint64;
val fromInt : IntInf.int -> uint64;
val toInt : uint64 -> IntInf.int;
val toLarge : uint64 -> LargeWord.word;
val fromLarge : LargeWord.word -> uint64
val plus : uint64 -> uint64 -> uint64;
val minus : uint64 -> uint64 -> uint64;
val times : uint64 -> uint64 -> uint64;
val divide : uint64 -> uint64 -> uint64;
val modulus : uint64 -> uint64 -> uint64;
val negate : uint64 -> uint64;
val less_eq : uint64 -> uint64 -> bool;
val less : uint64 -> uint64 -> bool;
val notb : uint64 -> uint64;
val andb : uint64 -> uint64 -> uint64;
val orb : uint64 -> uint64 -> uint64;
val xorb : uint64 -> uint64 -> uint64;
val shiftl : uint64 -> IntInf.int -> uint64;
val shiftr : uint64 -> IntInf.int -> uint64;
val shiftr_signed : uint64 -> IntInf.int -> uint64;
val set_bit : uint64 -> IntInf.int -> bool -> uint64;
val test_bit : uint64 -> IntInf.int -> bool;
end = struct

type uint64 = IntInf.int;

val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int;

val zero = 0 : IntInf.int;

val one = 1 : IntInf.int;

fun fromInt x = IntInf.andb(x, mask);

fun toInt x = x

fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x);

fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x);

fun plus x y = IntInf.andb(IntInf.+(x, y), mask);

fun minus x y = IntInf.andb(IntInf.-(x, y), mask);

fun negate x = IntInf.andb(IntInf.~(x), mask);

fun times x y = IntInf.andb(IntInf.*(x, y), mask);

fun divide x y = IntInf.div(x, y);

fun modulus x y = IntInf.mod(x, y);

fun less_eq x y = IntInf.<=(x, y);

fun less x y = IntInf.<(x, y);

fun notb x = IntInf.andb(IntInf.notb(x), mask);

fun orb x y = IntInf.orb(x, y);

fun andb x y = IntInf.andb(x, y);

fun xorb x y = IntInf.xorb(x, y);

val maxWord = IntInf.pow (2, Word.wordSize);

fun shiftl x n =
if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask)
else 0;

fun shiftr x n =
if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n))
else 0;

val msb_mask = 0x8000000000000000 : IntInf.int;

fun shiftr_signed x i =
if IntInf.andb(x, msb_mask) = 0 then shiftr x i
else if i >= 64 then 0xFFFFFFFFFFFFFFFF
else let
val x' = shiftr x i
val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask)
in IntInf.orb(x', m') end;

fun test_bit x n =
if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0
else false;

fun set_bit x n b =
if n < 64 then
if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))
else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))))
else x;

end
›
code_reserved SML Uint64

setup ‹
let
val polyml64 = LargeWord.wordSize > 63;
(* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain
from using Word64 in that case. Testing is done with dynamic code evaluation such that
the compiler does not choke on the Word64 structure, which need not be present in a 32bit
environment. *)
val error_msg = "Buggy Word64 structure";
val test_code =
"val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^
"else raise (Fail \"" ^ error_msg ^ "\");";
val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code))
val use_Word64 = polyml64 andalso
(case f () of
Exn.Res _ => true
| Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e
| Exn.Exn e => Exn.reraise e)
;

val newline = "\n";
val content =
"structure Uint64 : sig" ^ newline ^
"  eqtype uint64;" ^ newline ^
"  val zero : uint64;" ^ newline ^
"  val one : uint64;" ^ newline ^
"  val fromInt : IntInf.int -> uint64;" ^ newline ^
"  val toInt : uint64 -> IntInf.int;" ^ newline ^
"  val toLarge : uint64 -> LargeWord.word;" ^ newline ^
"  val fromLarge : LargeWord.word -> uint64" ^ newline ^
"  val plus : uint64 -> uint64 -> uint64;" ^ newline ^
"  val minus : uint64 -> uint64 -> uint64;" ^ newline ^
"  val times : uint64 -> uint64 -> uint64;" ^ newline ^
"  val divide : uint64 -> uint64 -> uint64;" ^ newline ^
"  val modulus : uint64 -> uint64 -> uint64;" ^ newline ^
"  val negate : uint64 -> uint64;" ^ newline ^
"  val less_eq : uint64 -> uint64 -> bool;" ^ newline ^
"  val less : uint64 -> uint64 -> bool;" ^ newline ^
"  val notb : uint64 -> uint64;" ^ newline ^
"  val andb : uint64 -> uint64 -> uint64;" ^ newline ^
"  val orb : uint64 -> uint64 -> uint64;" ^ newline ^
"  val xorb : uint64 -> uint64 -> uint64;" ^ newline ^
"  val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^
"  val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^
"  val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^
"  val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^
"  val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^
"end = struct" ^ newline ^
"" ^ newline ^
"type uint64 = Word64.word;" ^ newline ^
"" ^ newline ^
"val zero = (0wx0 : uint64);" ^ newline ^
"" ^ newline ^
"val one = (0wx1 : uint64);" ^ newline ^
"" ^ newline ^
"fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^
"" ^ newline ^
"fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);"  ^ newline ^
"" ^ newline ^
"fun fromLarge x = Word64.fromLarge x;" ^ newline ^
"" ^ newline ^
"fun toLarge x = Word64.toLarge x;"  ^ newline ^
"" ^ newline ^
"fun plus x y = Word64.+(x, y);" ^ newline ^
"" ^ newline ^
"fun minus x y = Word64.-(x, y);" ^ newline ^
"" ^ newline ^
"fun negate x = Word64.~(x);" ^ newline ^
"" ^ newline ^
"fun times x y = Word64.*(x, y);" ^ newline ^
"" ^ newline ^
"fun divide x y = Word64.div(x, y);" ^ newline ^
"" ^ newline ^
"fun modulus x y = Word64.mod(x, y);" ^ newline ^
"" ^ newline ^
"fun less_eq x y = Word64.<=(x, y);" ^ newline ^
"" ^ newline ^
"fun less x y = Word64.<(x, y);" ^ newline ^
"" ^ newline ^
"fun set_bit x n b =" ^ newline ^
"  let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
"  in if b then Word64.orb (x, mask)" ^ newline ^
"     else Word64.andb (x, Word64.notb mask)" ^ newline ^
"  end" ^ newline ^
"" ^ newline ^
"fun shiftl x n =" ^ newline ^
"  Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
"" ^ newline ^
"fun shiftr x n =" ^ newline ^
"  Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
"" ^ newline ^
"fun shiftr_signed x n =" ^ newline ^
"  Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^
"" ^ newline ^
"fun test_bit x n =" ^ newline ^
"  Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^
"" ^ newline ^
"val notb = Word64.notb" ^ newline ^
"" ^ newline ^
"fun andb x y = Word64.andb(x, y);" ^ newline ^
"" ^ newline ^
"fun orb x y = Word64.orb(x, y);" ^ newline ^
"" ^ newline ^
"fun xorb x y = Word64.xorb(x, y);" ^ newline ^
"" ^ newline ^
"end (*struct Uint64*)"
val target_SML64 = "SML_word";
in
(if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I)
#> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))]))
end
›

code_printing code_module Uint64 ⇀ (Haskell)
‹module Uint64(Int64, Word64) where

import Data.Int(Int64)
import Data.Word(Word64)›

text ‹
OCaml and Scala provide only signed 64bit numbers, so we use these and
implement sign-sensitive operations like comparisons manually.
›
code_printing code_module "Uint64" ⇀ (OCaml)
‹module Uint64 : sig
val less : int64 -> int64 -> bool
val less_eq : int64 -> int64 -> bool
val set_bit : int64 -> Z.t -> bool -> int64
val shiftl : int64 -> Z.t -> int64
val shiftr : int64 -> Z.t -> int64
val shiftr_signed : int64 -> Z.t -> int64
val test_bit : int64 -> Z.t -> bool
end = struct

(* negative numbers have their highest bit set,
so they are greater than positive ones *)
let less x y =
if Int64.compare x Int64.zero < 0 then
Int64.compare y Int64.zero < 0 && Int64.compare x y < 0
else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;;

let less_eq x y =
if Int64.compare x Int64.zero < 0 then
Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0
else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;;

let set_bit x n b =
let mask = Int64.shift_left Int64.one (Z.to_int n)
in if b then Int64.logor x mask
else Int64.logand x (Int64.lognot mask);;

let shiftl x n = Int64.shift_left x (Z.to_int n);;

let shiftr x n = Int64.shift_right_logical x (Z.to_int n);;

let shiftr_signed x n = Int64.shift_right x (Z.to_int n);;

let test_bit x n =
Int64.compare
(Int64.logand x (Int64.shift_left Int64.one (Z.to_int n)))
Int64.zero
<> 0;;

end;; (*struct Uint64*)›
code_reserved OCaml Uint64

code_printing code_module Uint64 ⇀ (Scala)
‹object Uint64 {

def less(x: Long, y: Long) : Boolean =
if (x < 0) y < 0 && x < y
else y < 0 || x < y

def less_eq(x: Long, y: Long) : Boolean =
if (x < 0) y < 0 && x <= y
else y < 0 || x <= y

def set_bit(x: Long, n: BigInt, b: Boolean) : Long =
if (b)
x | (1L << n.intValue)
else
x & (1L << n.intValue).unary_~

def shiftl(x: Long, n: BigInt) : Long = x << n.intValue

def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue

def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue

def test_bit(x: Long, n: BigInt) : Boolean =
(x & (1L << n.intValue)) != 0

} /* object Uint64 */›
code_reserved Scala Uint64

text ‹
OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer.
The following justifies the implementation.
›

definition Uint64_signed :: "integer ⇒ uint64"
where "Uint64_signed i = (if i < -(0x8000000000000000) ∨ i ≥ 0x8000000000000000 then undefined Uint64 i else Uint64 i)"

lemma Uint64_code [code]:
"Uint64 i =
(let i' = i AND 0xFFFFFFFFFFFFFFFF
in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')"
including undefined_transfer integer.lifting unfolding Uint64_signed_def
apply transfer
apply (subst word_of_int_via_signed)
apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong)
done

lemma Uint64_signed_code [code abstract]:
"Rep_uint64 (Uint64_signed i) =
(if i < -(0x8000000000000000) ∨ i ≥ 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))"
unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def word_of_integer_def

text ‹
Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint64}.

The new destructor @{term Rep_uint64'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop.

If code generation raises Match, some equation probably contains @{term Rep_uint64}
([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because
these instances will be folded away.)

To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}.
›

definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64"

lemma Rep_uint64'_transfer [transfer_rule]:
"rel_fun cr_uint64 (=) (λx. x) Rep_uint64'"
unfolding Rep_uint64'_def by(rule uint64.rep_transfer)

lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)"
by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint64' :: "64 word ⇒ uint64" is "λx :: 64 word. x" .

lemma Abs_uint64'_code [code]:
"Abs_uint64' x = Uint64 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint64 ⇒ _"]]

lemma term_of_uint64_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''"
shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []]))
(term_of_class.term_of (Rep_uint64' x))"

code_printing
type_constructor uint64 ⇀
(SML) "Uint64.uint64" and
(OCaml) "int64" and
(Scala) "Long"
| constant Uint64 ⇀
(SML) "Uint64.fromInt" and
(Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and
(Scala) "_.longValue"
| constant Uint64_signed ⇀
(OCaml) "Z.to'_int64"
| constant "0 :: uint64" ⇀
(SML) "Uint64.zero" and
(Haskell) "(0 :: Uint64.Word64)" and
(OCaml) "Int64.zero" and
(Scala) "0"
| constant "1 :: uint64" ⇀
(SML) "Uint64.one" and
(Haskell) "(1 :: Uint64.Word64)" and
(OCaml) "Int64.one" and
(Scala) "1"
| constant "plus :: uint64 ⇒ _ " ⇀
(SML) "Uint64.plus" and
(Haskell) infixl 6 "+" and
(Scala) infixl 7 "+"
| constant "uminus :: uint64 ⇒ _" ⇀
(SML) "Uint64.negate" and
(OCaml) "Int64.neg" and
(Scala) "!(- _)"
| constant "minus :: uint64 ⇒ _" ⇀
(SML) "Uint64.minus" and
(Haskell) infixl 6 "-" and
(OCaml) "Int64.sub" and
(Scala) infixl 7 "-"
| constant "times :: uint64 ⇒ _ ⇒ _" ⇀
(SML) "Uint64.times" and
(Haskell) infixl 7 "*" and
(OCaml) "Int64.mul" and
(Scala) infixl 8 "*"
| constant "HOL.equal :: uint64 ⇒ _ ⇒ bool" ⇀
(SML) "!((_ : Uint64.uint64) = _)" and
(Haskell) infix 4 "==" and
(OCaml) "(Int64.compare _ _ = 0)" and
(Scala) infixl 5 "=="
| class_instance uint64 :: equal ⇀
| constant "less_eq :: uint64 ⇒ _ ⇒ bool" ⇀
(SML) "Uint64.less'_eq" and
(Haskell) infix 4 "<=" and
(OCaml) "Uint64.less'_eq" and
(Scala) "Uint64.less'_eq"
| constant "less :: uint64 ⇒ _ ⇒ bool" ⇀
(SML) "Uint64.less" and
(Haskell) infix 4 "<" and
(OCaml) "Uint64.less" and
(Scala) "Uint64.less"
| constant "NOT :: uint64 ⇒ _" ⇀
(SML) "Uint64.notb" and
(OCaml) "Int64.lognot" and
(Scala) "_.unary'_~"
| constant "(AND) :: uint64 ⇒ _" ⇀
(SML) "Uint64.andb" and
(Haskell) infixl 7 "Data_Bits..&." and
(OCaml) "Int64.logand" and
(Scala) infixl 3 "&"
| constant "(OR) :: uint64 ⇒ _" ⇀
(SML) "Uint64.orb" and
(Haskell) infixl 5 "Data_Bits..|." and
(OCaml) "Int64.logor" and
(Scala) infixl 1 "|"
| constant "(XOR) :: uint64 ⇒ _" ⇀
(SML) "Uint64.xorb" and
(OCaml) "Int64.logxor" and
(Scala) infixl 2 "^"

definition uint64_divmod :: "uint64 ⇒ uint64 ⇒ uint64 × uint64" where
"uint64_divmod x y =
(if y = 0 then (undefined ((div) :: uint64 ⇒ _) x (0 :: uint64), undefined ((mod) :: uint64 ⇒ _) x (0 :: uint64))
else (x div y, x mod y))"

definition uint64_div :: "uint64 ⇒ uint64 ⇒ uint64"
where "uint64_div x y = fst (uint64_divmod x y)"

definition uint64_mod :: "uint64 ⇒ uint64 ⇒ uint64"
where "uint64_mod x y = snd (uint64_divmod x y)"

lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)"
including undefined_transfer unfolding uint64_divmod_def uint64_div_def
by transfer (simp add: word_div_def)

lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)"
including undefined_transfer unfolding uint64_mod_def uint64_divmod_def
by transfer (simp add: word_mod_def)

definition uint64_sdiv :: "uint64 ⇒ uint64 ⇒ uint64"
where [code del]:
"uint64_sdiv x y =
(if y = 0 then undefined ((div) :: uint64 ⇒ _) x (0 :: uint64)
else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))"

definition div0_uint64 :: "uint64 ⇒ uint64"
where [code del]: "div0_uint64 x = undefined ((div) :: uint64 ⇒ _) x (0 :: uint64)"
declare [[code abort: div0_uint64]]

definition mod0_uint64 :: "uint64 ⇒ uint64"
where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 ⇒ _) x (0 :: uint64)"
declare [[code abort: mod0_uint64]]

lemma uint64_divmod_code [code]:
"uint64_divmod x y =
(if 0x8000000000000000 ≤ y then if x < y then (0, x) else (1, x - y)
else if y = 0 then (div0_uint64 x, mod0_uint64 x)
else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y);
r = x - q * y
in if r ≥ y then (q + 1, r - y) else (q, r))"
including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def
by transfer (simp add: divmod_via_sdivmod shiftr_eq_drop_bit shiftl_eq_push_bit ac_simps)

lemma uint64_sdiv_code [code abstract]:
"Rep_uint64 (uint64_sdiv x y) =
(if y = 0 then Rep_uint64 (undefined ((div) :: uint64 ⇒ _) x (0 :: uint64))
else Rep_uint64 x sdiv Rep_uint64 y)"
unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse)

text ‹
Note that we only need a translation for signed division, but not for the remainder
because @{thm uint64_divmod_code} computes both with division only.
›

code_printing
constant uint64_div ⇀
(SML) "Uint64.divide" and
| constant uint64_mod ⇀
(SML) "Uint64.modulus" and
| constant uint64_divmod ⇀
| constant uint64_sdiv ⇀
(OCaml) "Int64.div" and
(Scala) "_ '/ _"

definition uint64_test_bit :: "uint64 ⇒ integer ⇒ bool"
where [code del]:
"uint64_test_bit x n =
(if n < 0 ∨ 63 < n then undefined (bit :: uint64 ⇒ _) x n
else bit x (nat_of_integer n))"

lemma bit_uint64_code [code]:
"bit x n ⟷ n < 64 ∧ uint64_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint64_test_bit_def
by (transfer, simp, transfer, simp)

lemma uint64_test_bit_code [code]:
"uint64_test_bit w n =
(if n < 0 ∨ 63 < n then undefined (bit :: uint64 ⇒ _) w n else bit (Rep_uint64 w) (nat_of_integer n))"
unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq)

code_printing constant uint64_test_bit ⇀
(SML) "Uint64.test'_bit" and
(OCaml) "Uint64.test'_bit" and
(Scala) "Uint64.test'_bit" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)"

definition uint64_set_bit :: "uint64 ⇒ integer ⇒ bool ⇒ uint64"
where [code del]:
"uint64_set_bit x n b =
(if n < 0 ∨ 63 < n then undefined (set_bit :: uint64 ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint64_code [code]:
"set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint64_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint64_set_bit_code [code abstract]:
"Rep_uint64 (uint64_set_bit w n b) =
(if n < 0 ∨ 63 < n then Rep_uint64 (undefined (set_bit :: uint64 ⇒ _) w n b)
else set_bit (Rep_uint64 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint64_set_bit_def by transfer simp

code_printing constant uint64_set_bit ⇀
(SML) "Uint64.set'_bit" and
(OCaml) "Uint64.set'_bit" and
(Scala) "Uint64.set'_bit" and
(Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)"

lift_definition uint64_set_bits :: "(nat ⇒ bool) ⇒ uint64 ⇒ nat ⇒ uint64" is set_bits_aux .

lemma uint64_set_bits_code [code]:
"uint64_set_bits f w n =
(if n = 0 then w
else let n' = n - 1 in uint64_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
apply (transfer fixing: n)
apply (cases n)
apply (simp_all add: shiftl_eq_push_bit)
done

lemma set_bits_uint64 [code]:
"(BITS n. f n) = uint64_set_bits f 0 64"
by transfer(simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint64 shows "lsb x = bit x 0"
by transfer (simp add: lsb_word_eq)

definition uint64_shiftl :: "uint64 ⇒ integer ⇒ uint64"
where [code del]:
"uint64_shiftl x n = (if n < 0 ∨ 64 ≤ n then undefined (push_bit :: nat ⇒ uint64 ⇒ _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint64_shiftl_def
by transfer simp

lemma uint64_shiftl_code [code abstract]:
"Rep_uint64 (uint64_shiftl w n) =
(if n < 0 ∨ 64 ≤ n then Rep_uint64 (undefined (push_bit :: nat ⇒ uint64 ⇒ _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))"
including undefined_transfer unfolding uint64_shiftl_def by transfer simp

code_printing constant uint64_shiftl ⇀
(SML) "Uint64.shiftl" and
(OCaml) "Uint64.shiftl" and
(Scala) "Uint64.shiftl" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)"

definition uint64_shiftr :: "uint64 ⇒ integer ⇒ uint64"
where [code del]:
"uint64_shiftr x n = (if n < 0 ∨ 64 ≤ n then undefined (drop_bit :: nat ⇒ uint64 ⇒ _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint64_shiftr_def
by transfer simp

lemma uint64_shiftr_code [code abstract]:
"Rep_uint64 (uint64_shiftr w n) =
(if n < 0 ∨ 64 ≤ n then Rep_uint64 (undefined (drop_bit :: nat ⇒ uint64 ⇒ _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))"
including undefined_transfer unfolding uint64_shiftr_def by transfer simp

code_printing constant uint64_shiftr ⇀
(SML) "Uint64.shiftr" and
(OCaml) "Uint64.shiftr" and
(Scala) "Uint64.shiftr" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)"

definition uint64_sshiftr :: "uint64 ⇒ integer ⇒ uint64"
where [code del]:
"uint64_sshiftr x n =
(if n < 0 ∨ 64 ≤ n then undefined sshiftr_uint64 x n else sshiftr_uint64 x (nat_of_integer n))"

lemma sshiftr_uint64_code [code]:
"x >>> n =
(if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)"
including undefined_transfer integer.lifting unfolding uint64_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond)

lemma uint64_sshiftr_code [code abstract]:
"Rep_uint64 (uint64_sshiftr w n) =
(if n < 0 ∨ 64 ≤ n then Rep_uint64 (undefined sshiftr_uint64 w n) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))"
including undefined_transfer unfolding uint64_sshiftr_def by transfer simp

code_printing constant uint64_sshiftr ⇀
(SML) "Uint64.shiftr'_signed" and
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and
(OCaml) "Uint64.shiftr'_signed" and
(Scala) "Uint64.shiftr'_signed" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)"

lemma uint64_msb_test_bit: "msb x ⟷ bit (x :: uint64) 63"
by transfer (simp add: msb_word_iff_bit)

lemma msb_uint64_code [code]: "msb x ⟷ uint64_test_bit x 63"
by (simp add: uint64_test_bit_def uint64_msb_test_bit)

lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint64_code [code]:
"int_of_uint64 x = int_of_integer (integer_of_uint64 x)"

lemma nat_of_uint64_code [code]:
"nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)"
unfolding integer_of_uint64_def including integer.lifting by transfer simp

definition integer_of_uint64_signed :: "uint64 ⇒ integer"
where
"integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)"

lemma integer_of_uint64_signed_code [code]:
"integer_of_uint64_signed n =
(if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))"
unfolding integer_of_uint64_signed_def integer_of_uint64_def
including undefined_transfer by transfer simp

lemma integer_of_uint64_code [code]:
"integer_of_uint64 n =
(if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)"
proof -
have ‹(0x7FFFFFFFFFFFFFFF :: uint64) = mask 63›
then have *: ‹n AND 0x7FFFFFFFFFFFFFFF = take_bit 63 n›
have **: ‹(0x8000000000000000 :: int) = 2 ^ 63›
by simp
show ?thesis
unfolding integer_of_uint64_def integer_of_uint64_signed_def o_def *
including undefined_transfer integer.lifting
apply transfer
apply (rule bit_eqI)
apply (simp add: test_bit_eq_bit bit_or_iff bit_take_bit_iff bit_uint_iff)
apply (simp only: bit_exp_iff bit_or_iff **)
apply auto
done
qed

code_printing
constant "integer_of_uint64" ⇀
(SML) "Uint64.toInt" and
| constant "integer_of_uint64_signed" ⇀
(OCaml) "Z.of'_int64" and
(Scala) "BigInt"

section ‹Quickcheck setup›

definition uint64_of_natural :: "natural ⇒ uint64"
where "uint64_of_natural x ≡ Uint64 (integer_of_natural x)"

instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint64 ≡ qc_random_cnv uint64_of_natural"
definition "exhaustive_uint64 ≡ qc_exhaustive_cnv uint64_of_natural"
definition "full_exhaustive_uint64 ≡ qc_full_exhaustive_cnv uint64_of_natural"
instance ..
end

instantiation uint64 :: narrowing begin

interpretation quickcheck_narrowing_samples
"λi. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0"
"Typerep.Typerep (STR ''Uint64.uint64'') []" .

definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint64 itself ⇒ _"]]
lemmas partial_term_of_uint64 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint64 (infixl ">>>" 55)

end


# Theory Uint32

(*  Title:      Uint32.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 32 bits›

theory Uint32 imports
Code_Target_Word_Base
begin

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint32 = "UNIV :: 32 word set" ..

setup_lifting type_definition_uint32

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint32}.›
declare Rep_uint32_inverse[code abstype]

declare Quotient_uint32[transfer_rule]

instantiation uint32 :: comm_ring_1
begin
lift_definition zero_uint32 :: uint32 is "0 :: 32 word" .
lift_definition one_uint32 :: uint32 is "1" .
lift_definition plus_uint32 :: "uint32 ⇒ uint32 ⇒ uint32" is "(+) :: 32 word ⇒ _" .
lift_definition minus_uint32 :: "uint32 ⇒ uint32 ⇒ uint32" is "(-)" .
lift_definition uminus_uint32 :: "uint32 ⇒ uint32" is uminus .
lift_definition times_uint32 :: "uint32 ⇒ uint32 ⇒ uint32" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint32 :: semiring_modulo
begin
lift_definition divide_uint32 :: "uint32 ⇒ uint32 ⇒ uint32" is "(div)" .
lift_definition modulo_uint32 :: "uint32 ⇒ uint32 ⇒ uint32" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint32 :: linorder begin
lift_definition less_uint32 :: "uint32 ⇒ uint32 ⇒ bool" is "(<)" .
lift_definition less_eq_uint32 :: "uint32 ⇒ uint32 ⇒ bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint32.rep_eq less_eq_uint32.rep_eq

context
includes lifting_syntax
notes
transfer_rule_of_bool [transfer_rule]
transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
"((=) ===> cr_uint32) of_bool of_bool"
by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
"((=) ===> cr_uint32) numeral numeral"
by transfer_prover

lemma [transfer_rule]:
‹(cr_uint32 ===> (⟷)) even ((dvd) 2 :: uint32 ⇒ bool)›
by (unfold dvd_def) transfer_prover

end

instantiation uint32:: semiring_bits
begin

lift_definition bit_uint32 :: ‹uint32 ⇒ nat ⇒ bool› is bit .

instance
by (standard; transfer)
(fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint32 :: semiring_bit_shifts
begin
lift_definition push_bit_uint32 :: ‹nat ⇒ uint32 ⇒ uint32› is push_bit .
lift_definition drop_bit_uint32 :: ‹nat ⇒ uint32 ⇒ uint32› is drop_bit .
lift_definition take_bit_uint32 :: ‹nat ⇒ uint32 ⇒ uint32› is take_bit .
instance by (standard; transfer)
(fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint32 :: ring_bit_operations
begin
lift_definition not_uint32 :: ‹uint32 ⇒ uint32› is NOT .
lift_definition and_uint32 :: ‹uint32 ⇒ uint32 ⇒ uint32› is ‹(AND)› .
lift_definition or_uint32 :: ‹uint32 ⇒ uint32 ⇒ uint32› is ‹(OR)› .
lift_definition xor_uint32 :: ‹uint32 ⇒ uint32 ⇒ uint32› is ‹(XOR)› .
lift_definition mask_uint32 :: ‹nat ⇒ uint32› is mask .
instance by (standard; transfer)
(simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
‹take_bit n a = a AND mask n› for a :: uint32

lemma [code]:
‹mask (Suc n) = push_bit n (1 :: uint32) OR mask n›
‹mask 0 = (0 :: uint32)›

instance uint32 :: semiring_bit_syntax ..

context
includes lifting_syntax
begin

lemma test_bit_uint32_transfer [transfer_rule]:
‹(cr_uint32 ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint32_transfer [transfer_rule]:
‹(cr_uint32 ===> (=) ===> cr_uint32) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint32_transfer [transfer_rule]:
‹(cr_uint32 ===> (=) ===> cr_uint32) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint32 :: lsb
begin
lift_definition lsb_uint32 :: ‹uint32 ⇒ bool› is lsb .
instance by (standard; transfer)
(fact lsb_odd)
end

instantiation uint32 :: msb
begin
lift_definition msb_uint32 :: ‹uint32 ⇒ bool› is msb .
instance ..
end

instantiation uint32 :: set_bit
begin
lift_definition set_bit_uint32 :: ‹uint32 ⇒ nat ⇒ bool ⇒ uint32› is set_bit .
instance
apply standard
apply transfer
apply (simp add: bit_simps)
done
end

instantiation uint32 :: bit_comprehension begin
lift_definition set_bits_uint32 :: "(nat ⇒ bool) ⇒ uint32" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint32.rep_eq lsb_uint32.rep_eq msb_uint32.rep_eq

instantiation uint32 :: equal begin
lift_definition equal_uint32 :: "uint32 ⇒ uint32 ⇒ bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint32.rep_eq

instantiation uint32 :: size begin
lift_definition size_uint32 :: "uint32 ⇒ nat" is "size" .
instance ..
end

lemmas [code] = size_uint32.rep_eq

lift_definition sshiftr_uint32 :: "uint32 ⇒ nat ⇒ uint32" (infixl ">>>" 55) is ‹λw n. signed_drop_bit n w› .

lift_definition uint32_of_int :: "int ⇒ uint32" is "word_of_int" .

definition uint32_of_nat :: "nat ⇒ uint32"
where "uint32_of_nat = uint32_of_int ∘ int"

lift_definition int_of_uint32 :: "uint32 ⇒ int" is "uint" .
lift_definition nat_of_uint32 :: "uint32 ⇒ nat" is "unat" .

definition integer_of_uint32 :: "uint32 ⇒ integer"
where "integer_of_uint32 = integer_of_int o int_of_uint32"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint32 :: "integer ⇒ uint32" is "word_of_int" .

lemma Rep_uint32_numeral [simp]: "Rep_uint32 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint32_def Abs_uint32_inverse numeral.simps plus_uint32_def)

lemma numeral_uint32_transfer [transfer_rule]:
"(rel_fun (=) cr_uint32) numeral numeral"
by(auto simp add: cr_uint32_def)

lemma numeral_uint32 [code_unfold]: "numeral n = Uint32 (numeral n)"
by transfer simp

lemma Rep_uint32_neg_numeral [simp]: "Rep_uint32 (- numeral n) = - numeral n"
by(simp only: uminus_uint32_def)(simp add: Abs_uint32_inverse)

lemma neg_numeral_uint32 [code_unfold]: "- numeral n = Uint32 (- numeral n)"
by transfer(simp add: cr_uint32_def)

end

lemma Abs_uint32_numeral [code_post]: "Abs_uint32 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint32_def numeral.simps plus_uint32_def Abs_uint32_inverse)

lemma Abs_uint32_0 [code_post]: "Abs_uint32 0 = 0"

lemma Abs_uint32_1 [code_post]: "Abs_uint32 1 = 1"

section ‹Code setup›

code_printing code_module Uint32 ⇀ (SML)
‹(* Test that words can handle numbers between 0 and 31 *)
val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5"));

structure Uint32 : sig
val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word
val shiftl : Word32.word -> IntInf.int -> Word32.word
val shiftr : Word32.word -> IntInf.int -> Word32.word
val shiftr_signed : Word32.word -> IntInf.int -> Word32.word
val test_bit : Word32.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
in if b then Word32.orb (x, mask)
else Word32.andb (x, Word32.notb mask)
end

fun shiftl x n =
Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0

end; (* struct Uint32 *)›
code_reserved SML Uint32

code_printing code_module Uint32 ⇀ (Haskell)
‹module Uint32(Int32, Word32) where

import Data.Int(Int32)
import Data.Word(Word32)›

text ‹
OCaml and Scala provide only signed 32bit numbers, so we use these and
implement sign-sensitive operations like comparisons manually.
›
code_printing code_module "Uint32" ⇀ (OCaml)
‹module Uint32 : sig
val less : int32 -> int32 -> bool
val less_eq : int32 -> int32 -> bool
val set_bit : int32 -> Z.t -> bool -> int32
val shiftl : int32 -> Z.t -> int32
val shiftr : int32 -> Z.t -> int32
val shiftr_signed : int32 -> Z.t -> int32
val test_bit : int32 -> Z.t -> bool
end = struct

(* negative numbers have their highest bit set,
so they are greater than positive ones *)
let less x y =
if Int32.compare x Int32.zero < 0 then
Int32.compare y Int32.zero < 0 && Int32.compare x y < 0
else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;;

let less_eq x y =
if Int32.compare x Int32.zero < 0 then
Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0
else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;;

let set_bit x n b =
let mask = Int32.shift_left Int32.one (Z.to_int n)
in if b then Int32.logor x mask
else Int32.logand x (Int32.lognot mask);;

let shiftl x n = Int32.shift_left x (Z.to_int n);;

let shiftr x n = Int32.shift_right_logical x (Z.to_int n);;

let shiftr_signed x n = Int32.shift_right x (Z.to_int n);;

let test_bit x n =
Int32.compare
(Int32.logand x (Int32.shift_left Int32.one (Z.to_int n)))
Int32.zero
<> 0;;

end;; (*struct Uint32*)›
code_reserved OCaml Uint32

code_printing code_module Uint32 ⇀ (Scala)
‹object Uint32 {

def less(x: Int, y: Int) : Boolean =
if (x < 0) y < 0 && x < y
else y < 0 || x < y

def less_eq(x: Int, y: Int) : Boolean =
if (x < 0) y < 0 && x <= y
else y < 0 || x <= y

def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
if (b)
x | (1 << n.intValue)
else
x & (1 << n.intValue).unary_~

def shiftl(x: Int, n: BigInt) : Int = x << n.intValue

def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue

def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue

def test_bit(x: Int, n: BigInt) : Boolean =
(x & (1 << n.intValue)) != 0

} /* object Uint32 */›
code_reserved Scala Uint32

text ‹
OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer.
The following justifies the implementation.
›

definition Uint32_signed :: "integer ⇒ uint32"
where "Uint32_signed i = (if i < -(0x80000000) ∨ i ≥ 0x80000000 then undefined Uint32 i else Uint32 i)"

lemma Uint32_code [code]:
"Uint32 i =
(let i' = i AND 0xFFFFFFFF
in if bit i' 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')"
including undefined_transfer integer.lifting unfolding Uint32_signed_def
apply transfer
apply (subst word_of_int_via_signed)
apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong)
done

lemma Uint32_signed_code [code abstract]:
"Rep_uint32 (Uint32_signed i) =
(if i < -(0x80000000) ∨ i ≥ 0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))"
unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def word_of_integer_def

text ‹
Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint32}.

The new destructor @{term Rep_uint32'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop.

If code generation raises Match, some equation probably contains @{term Rep_uint32}
([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because
these instances will be folded away.)

To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}.
›

definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32"

lemma Rep_uint32'_transfer [transfer_rule]:
"rel_fun cr_uint32 (=) (λx. x) Rep_uint32'"
unfolding Rep_uint32'_def by(rule uint32.rep_transfer)

lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. bit x n)"
by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint32' :: "32 word ⇒ uint32" is "λx :: 32 word. x" .

lemma Abs_uint32'_code [code]:
"Abs_uint32' x = Uint32 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint32 ⇒ _"]]

lemma term_of_uint32_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''"
shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
(term_of_class.term_of (Rep_uint32' x))"

code_printing
type_constructor uint32 ⇀
(SML) "Word32.word" and
(OCaml) "int32" and
(Scala) "Int" and
(Eval) "Word32.word"
| constant Uint32 ⇀
(SML) "Word32.fromLargeInt (IntInf.toLarge _)" and
(Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and
(Scala) "_.intValue"
| constant Uint32_signed ⇀
(OCaml) "Z.to'_int32"
| constant "0 :: uint32" ⇀
(SML) "(Word32.fromInt 0)" and
(Haskell) "(0 :: Uint32.Word32)" and
(OCaml) "Int32.zero" and
(Scala) "0"
| constant "1 :: uint32" ⇀
(SML) "(Word32.fromInt 1)" and
(Haskell) "(1 :: Uint32.Word32)" and
(OCaml) "Int32.one" and
(Scala) "1"
| constant "plus :: uint32 ⇒ _ " ⇀
(SML) "Word32.+ ((_), (_))" and
(Haskell) infixl 6 "+" and
(Scala) infixl 7 "+"
| constant "uminus :: uint32 ⇒ _" ⇀
(SML) "Word32.~" and
(OCaml) "Int32.neg" and
(Scala) "!(- _)"
| constant "minus :: uint32 ⇒ _" ⇀
(SML) "Word32.- ((_), (_))" and
(Haskell) infixl 6 "-" and
(OCaml) "Int32.sub" and
(Scala) infixl 7 "-"
| constant "times :: uint32 ⇒ _ ⇒ _" ⇀
(SML) "Word32.* ((_), (_))" and
(Haskell) infixl 7 "*" and
(OCaml) "Int32.mul" and
(Scala) infixl 8 "*"
| constant "HOL.equal :: uint32 ⇒ _ ⇒ bool" ⇀
(SML) "!((_ : Word32.word) = _)" and
(Haskell) infix 4 "==" and
(OCaml) "(Int32.compare _ _ = 0)" and
(Scala) infixl 5 "=="
| class_instance uint32 :: equal ⇀
| constant "less_eq :: uint32 ⇒ _ ⇒ bool" ⇀
(SML) "Word32.<= ((_), (_))" and
(Haskell) infix 4 "<=" and
(OCaml) "Uint32.less'_eq" and
(Scala) "Uint32.less'_eq"
| constant "less :: uint32 ⇒ _ ⇒ bool" ⇀
(SML) "Word32.< ((_), (_))" and
(Haskell) infix 4 "<" and
(OCaml) "Uint32.less" and
(Scala) "Uint32.less"
| constant "NOT :: uint32 ⇒ _" ⇀
(SML) "Word32.notb" and
(OCaml) "Int32.lognot" and
(Scala) "_.unary'_~"
| constant "(AND) :: uint32 ⇒ _" ⇀
(SML) "Word32.andb ((_),/ (_))" and
(Haskell) infixl 7 "Data_Bits..&." and
(OCaml) "Int32.logand" and
(Scala) infixl 3 "&"
| constant "(OR) :: uint32 ⇒ _" ⇀
(SML) "Word32.orb ((_),/ (_))" and
(Haskell) infixl 5 "Data_Bits..|." and
(OCaml) "Int32.logor" and
(Scala) infixl 1 "|"
| constant "(XOR) :: uint32 ⇒ _" ⇀
(SML) "Word32.xorb ((_),/ (_))" and
(OCaml) "Int32.logxor" and
(Scala) infixl 2 "^"

definition uint32_divmod :: "uint32 ⇒ uint32 ⇒ uint32 × uint32" where
"uint32_divmod x y =
(if y = 0 then (undefined ((div) :: uint32 ⇒ _) x (0 :: uint32), undefined ((mod) :: uint32 ⇒ _) x (0 :: uint32))
else (x div y, x mod y))"

definition uint32_div :: "uint32 ⇒ uint32 ⇒ uint32"
where "uint32_div x y = fst (uint32_divmod x y)"

definition uint32_mod :: "uint32 ⇒ uint32 ⇒ uint32"
where "uint32_mod x y = snd (uint32_divmod x y)"

lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)"
including undefined_transfer unfolding uint32_divmod_def uint32_div_def
by transfer (simp add: word_div_def)

lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)"
including undefined_transfer unfolding uint32_mod_def uint32_divmod_def
by transfer (simp add: word_mod_def)

definition uint32_sdiv :: "uint32 ⇒ uint32 ⇒ uint32"
where [code del]:
"uint32_sdiv x y =
(if y = 0 then undefined ((div) :: uint32 ⇒ _) x (0 :: uint32)
else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))"

definition div0_uint32 :: "uint32 ⇒ uint32"
where [code del]: "div0_uint32 x = undefined ((div) :: uint32 ⇒ _) x (0 :: uint32)"
declare [[code abort: div0_uint32]]

definition mod0_uint32 :: "uint32 ⇒ uint32"
where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32 ⇒ _) x (0 :: uint32)"
declare [[code abort: mod0_uint32]]

lemma uint32_divmod_code [code]:
"uint32_divmod x y =
(if 0x80000000 ≤ y then if x < y then (0, x) else (1, x - y)
else if y = 0 then (div0_uint32 x, mod0_uint32 x)
else let q = (uint32_sdiv (drop_bit 1 x) y) << 1;
r = x - q * y
in if r ≥ y then (q + 1, r - y) else (q, r))"
including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def
by transfer (simp add: divmod_via_sdivmod shiftr_eq_drop_bit shiftl_eq_push_bit ac_simps)

lemma uint32_sdiv_code [code abstract]:
"Rep_uint32 (uint32_sdiv x y) =
(if y = 0 then Rep_uint32 (undefined ((div) :: uint32 ⇒ _) x (0 :: uint32))
else Rep_uint32 x sdiv Rep_uint32 y)"
unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse)

text ‹
Note that we only need a translation for signed division, but not for the remainder
because @{thm uint32_divmod_code} computes both with division only.
›

code_printing
constant uint32_div ⇀
(SML) "Word32.div ((_), (_))" and
| constant uint32_mod ⇀
(SML) "Word32.mod ((_), (_))" and
| constant uint32_divmod ⇀
| constant uint32_sdiv ⇀
(OCaml) "Int32.div" and
(Scala) "_ '/ _"

definition uint32_test_bit :: "uint32 ⇒ integer ⇒ bool"
where [code del]:
"uint32_test_bit x n =
(if n < 0 ∨ 31 < n then undefined (bit :: uint32 ⇒ _) x n
else bit x (nat_of_integer n))"

lemma test_bit_uint32_code [code]:
"bit x n ⟷ n < 32 ∧ uint32_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint32_test_bit_def
by (transfer, simp, transfer, simp)

lemma uint32_test_bit_code [code]:
"uint32_test_bit w n =
(if n < 0 ∨ 31 < n then undefined (bit :: uint32 ⇒ _) w n else bit (Rep_uint32 w) (nat_of_integer n))"
unfolding uint32_test_bit_def by(simp add: bit_uint32.rep_eq)

code_printing constant uint32_test_bit ⇀
(SML) "Uint32.test'_bit" and
(OCaml) "Uint32.test'_bit" and
(Scala) "Uint32.test'_bit" and
(Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)"

definition uint32_set_bit :: "uint32 ⇒ integer ⇒ bool ⇒ uint32"
where [code del]:
"uint32_set_bit x n b =
(if n < 0 ∨ 31 < n then undefined (set_bit :: uint32 ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint32_code [code]:
"set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint32_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint32_set_bit_code [code abstract]:
"Rep_uint32 (uint32_set_bit w n b) =
(if n < 0 ∨ 31 < n then Rep_uint32 (undefined (set_bit :: uint32 ⇒ _) w n b)
else set_bit (Rep_uint32 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint32_set_bit_def by transfer simp

code_printing constant uint32_set_bit ⇀
(SML) "Uint32.set'_bit" and
(OCaml) "Uint32.set'_bit" and
(Scala) "Uint32.set'_bit" and
(Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)"

lift_definition uint32_set_bits :: "(nat ⇒ bool) ⇒ uint32 ⇒ nat ⇒ uint32" is set_bits_aux .

lemma uint32_set_bits_code [code]:
"uint32_set_bits f w n =
(if n = 0 then w
else let n' = n - 1 in uint32_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
apply (transfer fixing: n)
apply (cases n)
apply (simp_all add: shiftl_eq_push_bit)
done

lemma set_bits_uint32 [code]:
"(BITS n. f n) = uint32_set_bits f 0 32"
by transfer(simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint32 shows "lsb x ⟷ bit x 0"
by transfer (simp add: lsb_word_eq)

definition uint32_shiftl :: "uint32 ⇒ integer ⇒ uint32"
where [code del]:
"uint32_shiftl x n = (if n < 0 ∨ 32 ≤ n then undefined (push_bit :: nat ⇒ uint32 ⇒ _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint32_code [code]: "push_bit n x = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint32_shiftl_def
by transfer simp

lemma uint32_shiftl_code [code abstract]:
"Rep_uint32 (uint32_shiftl w n) =
(if n < 0 ∨ 32 ≤ n then Rep_uint32 (undefined (push_bit :: nat ⇒ uint32 ⇒ _) w n) else push_bit (nat_of_integer n) (Rep_uint32 w))"
including undefined_transfer unfolding uint32_shiftl_def
by transfer (simp add: shiftl_eq_push_bit)

code_printing constant uint32_shiftl ⇀
(SML) "Uint32.shiftl" and
(OCaml) "Uint32.shiftl" and
(Scala) "Uint32.shiftl" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)"

definition uint32_shiftr :: "uint32 ⇒ integer ⇒ uint32"
where [code del]:
"uint32_shiftr x n = (if n < 0 ∨ 32 ≤ n then undefined (drop_bit :: nat ⇒ uint32 ⇒ _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint32_code [code]: "drop_bit n x = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint32_shiftr_def
by transfer simp

lemma uint32_shiftr_code [code abstract]:
"Rep_uint32 (uint32_shiftr w n) =
(if n < 0 ∨ 32 ≤ n then Rep_uint32 (undefined (drop_bit :: nat ⇒ uint32 ⇒ _) w n) else drop_bit (nat_of_integer n) (Rep_uint32 w))"
including undefined_transfer unfolding uint32_shiftr_def by transfer simp

code_printing constant uint32_shiftr ⇀
(SML) "Uint32.shiftr" and
(OCaml) "Uint32.shiftr" and
(Scala) "Uint32.shiftr" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)"

definition uint32_sshiftr :: "uint32 ⇒ integer ⇒ uint32"
where [code del]:
"uint32_sshiftr x n =
(if n < 0 ∨ 32 ≤ n then undefined sshiftr_uint32 x n else sshiftr_uint32 x (nat_of_integer n))"

lemma sshiftr_uint32_code [code]:
"x >>> n =
(if n < 32 then uint32_sshiftr x (integer_of_nat n) else if bit x 31 then - 1 else 0)"
including undefined_transfer integer.lifting unfolding uint32_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond)

lemma uint32_sshiftr_code [code abstract]:
"Rep_uint32 (uint32_sshiftr w n) =
(if n < 0 ∨ 32 ≤ n then Rep_uint32 (undefined sshiftr_uint32 w n) else signed_drop_bit (nat_of_integer n) (Rep_uint32 w))"
including undefined_transfer unfolding uint32_sshiftr_def by transfer simp

code_printing constant uint32_sshiftr ⇀
(SML) "Uint32.shiftr'_signed" and
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and
(OCaml) "Uint32.shiftr'_signed" and
(Scala) "Uint32.shiftr'_signed" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)"

lemma uint32_msb_test_bit: "msb x ⟷ bit (x :: uint32) 31"
by transfer (simp add: msb_word_iff_bit)

lemma msb_uint32_code [code]: "msb x ⟷ uint32_test_bit x 31"
by (simp add: uint32_test_bit_def uint32_msb_test_bit)

lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint32_code [code]:
"int_of_uint32 x = int_of_integer (integer_of_uint32 x)"

lemma nat_of_uint32_code [code]:
"nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)"
unfolding integer_of_uint32_def including integer.lifting by transfer simp

definition integer_of_uint32_signed :: "uint32 ⇒ integer"
where
"integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_uint32 n)"

lemma integer_of_uint32_signed_code [code]:
"integer_of_uint32_signed n =
(if bit n 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))"
unfolding integer_of_uint32_signed_def integer_of_uint32_def
including undefined_transfer by transfer simp

lemma integer_of_uint32_code [code]:
"integer_of_uint32 n =
(if bit n 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)"
proof -
have ‹(0x7FFFFFFF :: uint32) = mask 31›
then have *: ‹n AND 0x7FFFFFFF = take_bit 31 n›
have **: ‹(0x80000000 :: int) = 2 ^ 31›
by simp
show ?thesis
unfolding integer_of_uint32_def integer_of_uint32_signed_def o_def *
including undefined_transfer integer.lifting
apply transfer
apply (rule bit_eqI)
apply (simp add: test_bit_eq_bit bit_or_iff bit_take_bit_iff bit_uint_iff)
apply (simp only: bit_exp_iff bit_or_iff **)
apply auto
done
qed

code_printing
constant "integer_of_uint32" ⇀
(SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and
| constant "integer_of_uint32_signed" ⇀
(OCaml) "Z.of'_int32" and
(Scala) "BigInt"

section ‹Quickcheck setup›

definition uint32_of_natural :: "natural ⇒ uint32"
where "uint32_of_natural x ≡ Uint32 (integer_of_natural x)"

instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint32 ≡ qc_random_cnv uint32_of_natural"
definition "exhaustive_uint32 ≡ qc_exhaustive_cnv uint32_of_natural"
definition "full_exhaustive_uint32 ≡ qc_full_exhaustive_cnv uint32_of_natural"
instance ..
end

instantiation uint32 :: narrowing begin

interpretation quickcheck_narrowing_samples
"λi. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0"
"Typerep.Typerep (STR ''Uint32.uint32'') []" .

definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint32 itself ⇒ _"]]
lemmas partial_term_of_uint32 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint32 (infixl ">>>" 55)

end


# Theory Uint16

(*  Title:      Uint16.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 16 bits›

theory Uint16 imports
Code_Target_Word_Base
begin

text ‹
Restriction for ML code generation:
This theory assumes that the ML system provides a Word16
implementation (mlton does, but PolyML 5.5 does not).
Therefore, the code setup lives in the target ‹SML_word›
rather than ‹SML›.  This ensures that code generation still
works as long as ‹uint16› is not involved.
For the target ‹SML› itself, no special code generation
for this type is set up. Nevertheless, it should work by emulation via @{typ "16 word"}
if the theory ‹Code_Target_Bits_Int› is imported.

Restriction for OCaml code generation:
OCaml does not provide an int16 type, so no special code generation
for this type is set up.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint16 = "UNIV :: 16 word set" ..

setup_lifting type_definition_uint16

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint16}.›
declare Rep_uint16_inverse[code abstype]

declare Quotient_uint16[transfer_rule]

instantiation uint16 :: comm_ring_1
begin
lift_definition zero_uint16 :: uint16 is "0 :: 16 word" .
lift_definition one_uint16 :: uint16 is "1" .
lift_definition plus_uint16 :: "uint16 ⇒ uint16 ⇒ uint16" is "(+) :: 16 word ⇒ _" .
lift_definition minus_uint16 :: "uint16 ⇒ uint16 ⇒ uint16" is "(-)" .
lift_definition uminus_uint16 :: "uint16 ⇒ uint16" is uminus .
lift_definition times_uint16 :: "uint16 ⇒ uint16 ⇒ uint16" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint16 :: semiring_modulo
begin
lift_definition divide_uint16 :: "uint16 ⇒ uint16 ⇒ uint16" is "(div)" .
lift_definition modulo_uint16 :: "uint16 ⇒ uint16 ⇒ uint16" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint16 :: linorder begin
lift_definition less_uint16 :: "uint16 ⇒ uint16 ⇒ bool" is "(<)" .
lift_definition less_eq_uint16 :: "uint16 ⇒ uint16 ⇒ bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint16.rep_eq less_eq_uint16.rep_eq

context
includes lifting_syntax
notes
transfer_rule_of_bool [transfer_rule]
transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
"((=) ===> cr_uint16) of_bool of_bool"
by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
"((=) ===> cr_uint16) numeral numeral"
by transfer_prover

lemma [transfer_rule]:
‹(cr_uint16 ===> (⟷)) even ((dvd) 2 :: uint16 ⇒ bool)›
by (unfold dvd_def) transfer_prover

end

instantiation uint16 :: semiring_bits
begin

lift_definition bit_uint16 :: ‹uint16 ⇒ nat ⇒ bool› is bit .

instance
by (standard; transfer)
(fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint16 :: semiring_bit_shifts
begin
lift_definition push_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is push_bit .
lift_definition drop_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is drop_bit .
lift_definition take_bit_uint16 :: ‹nat ⇒ uint16 ⇒ uint16› is take_bit .
instance by (standard; transfer)
(fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint16 :: ring_bit_operations
begin
lift_definition not_uint16 :: ‹uint16 ⇒ uint16› is NOT .
lift_definition and_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(AND)› .
lift_definition or_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(OR)› .
lift_definition xor_uint16 :: ‹uint16 ⇒ uint16 ⇒ uint16› is ‹(XOR)› .
lift_definition mask_uint16 :: ‹nat ⇒ uint16› is mask .
instance by (standard; transfer)
(simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
‹take_bit n a = a AND mask n› for a :: uint16

lemma [code]:
‹mask (Suc n) = push_bit n (1 :: uint16) OR mask n›
‹mask 0 = (0 :: uint16)›

instance uint16 :: semiring_bit_syntax ..

context
includes lifting_syntax
begin

lemma test_bit_uint16_transfer [transfer_rule]:
‹(cr_uint16 ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint16_transfer [transfer_rule]:
‹(cr_uint16 ===> (=) ===> cr_uint16) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint16_transfer [transfer_rule]:
‹(cr_uint16 ===> (=) ===> cr_uint16) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint16 :: lsb
begin
lift_definition lsb_uint16 :: ‹uint16 ⇒ bool› is lsb .
instance by (standard; transfer)
(fact lsb_odd)
end

instantiation uint16 :: msb
begin
lift_definition msb_uint16 :: ‹uint16 ⇒ bool› is msb .
instance ..
end

instantiation uint16 :: set_bit
begin
lift_definition set_bit_uint16 :: ‹uint16 ⇒ nat ⇒ bool ⇒ uint16› is set_bit .
instance
apply standard
apply transfer
apply (simp add: bit_simps)
done
end

instantiation uint16 :: bit_comprehension begin
lift_definition set_bits_uint16 :: "(nat ⇒ bool) ⇒ uint16" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint16.rep_eq lsb_uint16.rep_eq msb_uint16.rep_eq

instantiation uint16 :: equal begin
lift_definition equal_uint16 :: "uint16 ⇒ uint16 ⇒ bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint16.rep_eq

instantiation uint16 :: size begin
lift_definition size_uint16 :: "uint16 ⇒ nat" is "size" .
instance ..
end

lemmas [code] = size_uint16.rep_eq

lift_definition sshiftr_uint16 :: "uint16 ⇒ nat ⇒ uint16" (infixl ">>>" 55) is ‹λw n. signed_drop_bit n w› .

lift_definition uint16_of_int :: "int ⇒ uint16" is "word_of_int" .

definition uint16_of_nat :: "nat ⇒ uint16"
where "uint16_of_nat = uint16_of_int ∘ int"

lift_definition int_of_uint16 :: "uint16 ⇒ int" is "uint" .
lift_definition nat_of_uint16 :: "uint16 ⇒ nat" is "unat" .

definition integer_of_uint16 :: "uint16 ⇒ integer"
where "integer_of_uint16 = integer_of_int o int_of_uint16"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint16 :: "integer ⇒ uint16" is "word_of_int" .

lemma Rep_uint16_numeral [simp]: "Rep_uint16 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint16_def Abs_uint16_inverse numeral.simps plus_uint16_def)

lemma Rep_uint16_neg_numeral [simp]: "Rep_uint16 (- numeral n) = - numeral n"
by(simp only: uminus_uint16_def)(simp add: Abs_uint16_inverse)

lemma numeral_uint16_transfer [transfer_rule]:
"(rel_fun (=) cr_uint16) numeral numeral"
by(auto simp add: cr_uint16_def)

lemma numeral_uint16 [code_unfold]: "numeral n = Uint16 (numeral n)"
by transfer simp

lemma neg_numeral_uint16 [code_unfold]: "- numeral n = Uint16 (- numeral n)"
by transfer(simp add: cr_uint16_def)

end

lemma Abs_uint16_numeral [code_post]: "Abs_uint16 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint16_def numeral.simps plus_uint16_def Abs_uint16_inverse)

lemma Abs_uint16_0 [code_post]: "Abs_uint16 0 = 0"

lemma Abs_uint16_1 [code_post]: "Abs_uint16 1 = 1"

section ‹Code setup›

code_printing code_module Uint16 ⇀ (SML_word)
‹(* Test that words can handle numbers between 0 and 15 *)
val _ = if 4 <= Word.wordSize then () else raise (Fail ("wordSize less than 4"));

structure Uint16 : sig
val set_bit : Word16.word -> IntInf.int -> bool -> Word16.word
val shiftl : Word16.word -> IntInf.int -> Word16.word
val shiftr : Word16.word -> IntInf.int -> Word16.word
val shiftr_signed : Word16.word -> IntInf.int -> Word16.word
val test_bit : Word16.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
let val mask = Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
in if b then Word16.orb (x, mask)
else Word16.andb (x, Word16.notb mask)
end

fun shiftl x n =
Word16.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
Word16.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
Word16.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
Word16.andb (x, Word16.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word16.fromInt 0

end; (* struct Uint16 *)›
code_reserved SML_word Uint16

code_printing code_module Uint16 ⇀ (Haskell)
‹module Uint16(Int16, Word16) where

import Data.Int(Int16)
import Data.Word(Word16)›

text ‹Scala provides unsigned 16-bit numbers as Char.›

code_printing code_module Uint16 ⇀ (Scala)
‹object Uint16 {

def set_bit(x: scala.Char, n: BigInt, b: Boolean) : scala.Char =
if (b)
(x | (1.toChar << n.intValue)).toChar
else
(x & (1.toChar << n.intValue).unary_~).toChar

def shiftl(x: scala.Char, n: BigInt) : scala.Char = (x << n.intValue).toChar

def shiftr(x: scala.Char, n: BigInt) : scala.Char = (x >>> n.intValue).toChar

def shiftr_signed(x: scala.Char, n: BigInt) : scala.Char = (x.toShort >> n.intValue).toChar

def test_bit(x: scala.Char, n: BigInt) : Boolean = (x & (1.toChar << n.intValue)) != 0

} /* object Uint16 */›
code_reserved Scala Uint16

text ‹
Avoid @{term Abs_uint16} in generated code, use @{term Rep_uint16'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint16}.

The new destructor @{term Rep_uint16'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint16} directly, because that makes code\_simp loop.

If code generation raises Match, some equation probably contains @{term Rep_uint16}
([code abstract] equations for @{typ uint16} may use @{term Rep_uint16} because
these instances will be folded away.)

To convert @{typ "16 word"} values into @{typ uint16}, use @{term "Abs_uint16'"}.
›

definition Rep_uint16' where [simp]: "Rep_uint16' = Rep_uint16"

lemma Rep_uint16'_transfer [transfer_rule]:
"rel_fun cr_uint16 (=) (λx. x) Rep_uint16'"
unfolding Rep_uint16'_def by(rule uint16.rep_transfer)

lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)"
by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint16' :: "16 word ⇒ uint16" is "λx :: 16 word. x" .

lemma Abs_uint16'_code [code]:
"Abs_uint16' x = Uint16 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint16 ⇒ _"]]

lemma term_of_uint16_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''" shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint16.uint16.Abs_uint16'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]], TR (STR ''Uint16.uint16'') []]))
(term_of_class.term_of (Rep_uint16' x))"

lemma Uin16_code [code abstract]: "Rep_uint16 (Uint16 i) = word_of_int (int_of_integer_symbolic i)"
unfolding Uint16_def int_of_integer_symbolic_def by(simp add: Abs_uint16_inverse)

code_printing
type_constructor uint16 ⇀
(SML_word) "Word16.word" and
(Scala) "scala.Char"
| constant Uint16 ⇀
(SML_word) "Word16.fromLargeInt (IntInf.toLarge _)" and
(Haskell) "(Prelude.fromInteger _ :: Uint16.Word16)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Word16)" and
(Scala) "_.charValue"
| constant "0 :: uint16" ⇀
(SML_word) "(Word16.fromInt 0)" and
(Haskell) "(0 :: Uint16.Word16)" and
(Scala) "0"
| constant "1 :: uint16" ⇀
(SML_word) "(Word16.fromInt 1)" and
(Haskell) "(1 :: Uint16.Word16)" and
(Scala) "1"
| constant "plus :: uint16 ⇒ _ ⇒ _" ⇀
(SML_word) "Word16.+ ((_), (_))" and
(Haskell) infixl 6 "+" and
(Scala) "(_ +/ _).toChar"
| constant "uminus :: uint16 ⇒ _" ⇀
(SML_word) "Word16.~" and
(Scala) "(- _).toChar"
| constant "minus :: uint16 ⇒ _" ⇀
(SML_word) "Word16.- ((_), (_))" and
(Haskell) infixl 6 "-" and
(Scala) "(_ -/ _).toChar"
| constant "times :: uint16 ⇒ _ ⇒ _" ⇀
(SML_word) "Word16.* ((_), (_))" and
(Haskell) infixl 7 "*" and
(Scala) "(_ */ _).toChar"
| constant "HOL.equal :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "!((_ : Word16.word) = _)" and
(Haskell) infix 4 "==" and
(Scala) infixl 5 "=="
| class_instance uint16 :: equal ⇀ (Haskell) -
| constant "less_eq :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "Word16.<= ((_), (_))" and
(Haskell) infix 4 "<=" and
(Scala) infixl 4 "<="
| constant "less :: uint16 ⇒ _ ⇒ bool" ⇀
(SML_word) "Word16.< ((_), (_))" and
(Haskell) infix 4 "<" and
(Scala) infixl 4 "<"
| constant "NOT :: uint16 ⇒ _" ⇀
(SML_word) "Word16.notb" and
(Scala) "_.unary'_~.toChar"
| constant "(AND) :: uint16 ⇒ _" ⇀
(SML_word) "Word16.andb ((_),/ (_))" and
(Haskell) infixl 7 "Data_Bits..&." and
(Scala) "(_ & _).toChar"
| constant "(OR) :: uint16 ⇒ _" ⇀
(SML_word) "Word16.orb ((_),/ (_))" and
(Haskell) infixl 5 "Data_Bits..|." and
(Scala) "(_ | _).toChar"
| constant "(XOR) :: uint16 ⇒ _" ⇀
(SML_word) "Word16.xorb ((_),/ (_))" and
(Scala) "(_ ^ _).toChar"

definition uint16_div :: "uint16 ⇒ uint16 ⇒ uint16"
where "uint16_div x y = (if y = 0 then undefined ((div) :: uint16 ⇒ _) x (0 :: uint16) else x div y)"

definition uint16_mod :: "uint16 ⇒ uint16 ⇒ uint16"
where "uint16_mod x y = (if y = 0 then undefined ((mod) :: uint16 ⇒ _) x (0 :: uint16) else x mod y)"

context includes undefined_transfer begin

lemma div_uint16_code [code]: "x div y = (if y = 0 then 0 else uint16_div x y)"
unfolding uint16_div_def by transfer (simp add: word_div_def)

lemma mod_uint16_code [code]: "x mod y = (if y = 0 then x else uint16_mod x y)"
unfolding uint16_mod_def by transfer (simp add: word_mod_def)

lemma uint16_div_code [code abstract]:
"Rep_uint16 (uint16_div x y) =
(if y = 0 then Rep_uint16 (undefined ((div) :: uint16 ⇒ _) x (0 :: uint16)) else Rep_uint16 x div Rep_uint16 y)"
unfolding uint16_div_def by transfer simp

lemma uint16_mod_code [code abstract]:
"Rep_uint16 (uint16_mod x y) =
(if y = 0 then Rep_uint16 (undefined ((mod) :: uint16 ⇒ _) x (0 :: uint16)) else Rep_uint16 x mod Rep_uint16 y)"
unfolding uint16_mod_def by transfer simp

end

code_printing constant uint16_div ⇀
(SML_word) "Word16.div ((_), (_))" and
(Scala) "(_ '/ _).toChar"
| constant uint16_mod ⇀
(SML_word) "Word16.mod ((_), (_))" and
(Scala) "(_ % _).toChar"

definition uint16_test_bit :: "uint16 ⇒ integer ⇒ bool"
where [code del]:
"uint16_test_bit x n =
(if n < 0 ∨ 15 < n then undefined (bit :: uint16 ⇒ _) x n
else bit x (nat_of_integer n))"

lemma test_bit_uint16_code [code]:
"bit x n ⟷ n < 16 ∧ uint16_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint16_test_bit_def
by (transfer, simp, transfer, simp)

lemma uint16_test_bit_code [code]:
"uint16_test_bit w n =
(if n < 0 ∨ 15 < n then undefined (bit :: uint16 ⇒ _) w n else bit (Rep_uint16 w) (nat_of_integer n))"
unfolding uint16_test_bit_def by (simp add: bit_uint16.rep_eq)

code_printing constant uint16_test_bit ⇀
(SML_word) "Uint16.test'_bit" and
(Scala) "Uint16.test'_bit"

definition uint16_set_bit :: "uint16 ⇒ integer ⇒ bool ⇒ uint16"
where [code del]:
"uint16_set_bit x n b =
(if n < 0 ∨ 15 < n then undefined (set_bit :: uint16 ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint16_code [code]:
"set_bit x n b = (if n < 16 then uint16_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint16_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint16_set_bit_code [code abstract]:
"Rep_uint16 (uint16_set_bit w n b) =
(if n < 0 ∨ 15 < n then Rep_uint16 (undefined (set_bit :: uint16 ⇒ _) w n b)
else set_bit (Rep_uint16 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint16_set_bit_def by transfer simp

code_printing constant uint16_set_bit ⇀
(SML_word) "Uint16.set'_bit" and
(Scala) "Uint16.set'_bit"

lift_definition uint16_set_bits :: "(nat ⇒ bool) ⇒ uint16 ⇒ nat ⇒ uint16" is set_bits_aux .

lemma uint16_set_bits_code [code]:
"uint16_set_bits f w n =
(if n = 0 then w
else let n' = n - 1 in uint16_set_bits f ((push_bit 1 w) OR (if f n' then 1 else 0)) n')"
apply (transfer fixing: n)
apply (cases n)
apply (simp_all add: shiftl_eq_push_bit)
done

lemma set_bits_uint16 [code]:
"(BITS n. f n) = uint16_set_bits f 0 16"
by transfer(simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint16 shows "lsb x ⟷ bit x 0"
by transfer (simp add: lsb_odd)

definition uint16_shiftl :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_shiftl x n = (if n < 0 ∨ 16 ≤ n then undefined (push_bit :: nat ⇒ uint16 ⇒ _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint16_code [code]: "push_bit n x = (if n < 16 then uint16_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint16_shiftl_def
by transfer simp

lemma uint16_shiftl_code [code abstract]:
"Rep_uint16 (uint16_shiftl w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined (push_bit :: nat ⇒ uint16 ⇒ _) w n)
else push_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_shiftl_def
by transfer simp

code_printing constant uint16_shiftl ⇀
(SML_word) "Uint16.shiftl" and
(Scala) "Uint16.shiftl"

definition uint16_shiftr :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_shiftr x n = (if n < 0 ∨ 16 ≤ n then undefined (drop_bit :: nat ⇒ uint16 ⇒ _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint16_code [code]: "drop_bit n x = (if n < 16 then uint16_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint16_shiftr_def
by transfer simp

lemma uint16_shiftr_code [code abstract]:
"Rep_uint16 (uint16_shiftr w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined (drop_bit :: nat ⇒ uint16 ⇒ _) w n)
else drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_shiftr_def by transfer simp

code_printing constant uint16_shiftr ⇀
(SML_word) "Uint16.shiftr" and
(Scala) "Uint16.shiftr"

definition uint16_sshiftr :: "uint16 ⇒ integer ⇒ uint16"
where [code del]:
"uint16_sshiftr x n =
(if n < 0 ∨ 16 ≤ n then undefined sshiftr_uint16 x n else sshiftr_uint16 x (nat_of_integer n))"

lemma sshiftr_uint16_code [code]:
"x >>> n =
(if n < 16 then uint16_sshiftr x (integer_of_nat n) else if bit x 15 then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint16_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond word_size)

lemma uint16_sshiftr_code [code abstract]:
"Rep_uint16 (uint16_sshiftr w n) =
(if n < 0 ∨ 16 ≤ n then Rep_uint16 (undefined sshiftr_uint16 w n)
else signed_drop_bit (nat_of_integer n) (Rep_uint16 w))"
including undefined_transfer unfolding uint16_sshiftr_def by transfer simp

code_printing constant uint16_sshiftr ⇀
(SML_word) "Uint16.shiftr'_signed" and
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint16.Int16) _)) :: Uint16.Word16)" and
(Scala) "Uint16.shiftr'_signed"

lemma uint16_msb_test_bit: "msb x ⟷ bit (x :: uint16) 15"
by transfer (simp add: msb_word_iff_bit)

lemma msb_uint16_code [code]: "msb x ⟷ uint16_test_bit x 15"
by (simp add: uint16_test_bit_def uint16_msb_test_bit)

lemma uint16_of_int_code [code]: "uint16_of_int i = Uint16 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint16_code [code]:
"int_of_uint16 x = int_of_integer (integer_of_uint16 x)"

lemma nat_of_uint16_code [code]:
"nat_of_uint16 x = nat_of_integer (integer_of_uint16 x)"
unfolding integer_of_uint16_def including integer.lifting by transfer simp

lemma integer_of_uint16_code [code]:
"integer_of_uint16 n = integer_of_int (uint (Rep_uint16' n))"
unfolding integer_of_uint16_def by transfer auto

code_printing
constant "integer_of_uint16" ⇀
(SML_word) "Word16.toInt _ : IntInf.int" and
(Scala) "BigInt"

section ‹Quickcheck setup›

definition uint16_of_natural :: "natural ⇒ uint16"
where "uint16_of_natural x ≡ Uint16 (integer_of_natural x)"

instantiation uint16 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint16 ≡ qc_random_cnv uint16_of_natural"
definition "exhaustive_uint16 ≡ qc_exhaustive_cnv uint16_of_natural"
definition "full_exhaustive_uint16 ≡ qc_full_exhaustive_cnv uint16_of_natural"
instance ..
end

instantiation uint16 :: narrowing begin

interpretation quickcheck_narrowing_samples
"λi. let x = Uint16 i in (x, 0xFFFF - x)" "0"
"Typerep.Typerep (STR ''Uint16.uint16'') []" .

definition "narrowing_uint16 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint16 itself ⇒ _"]]
lemmas partial_term_of_uint16 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint16 (infixl ">>>" 55)

end


# Theory Uint8

(*  Title:      Uint8.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of 8 bits›

theory Uint8 imports
Code_Target_Word_Base
begin

text ‹
Restriction for OCaml code generation:
OCaml does not provide an int8 type, so no special code generation
for this type is set up. If the theory ‹Code_Target_Bits_Int›
is imported, the type ‹uint8› is emulated via @{typ "8 word"}.
›

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint8 = "UNIV :: 8 word set" ..

setup_lifting type_definition_uint8

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint8}.›
declare Rep_uint8_inverse[code abstype]

declare Quotient_uint8[transfer_rule]

instantiation uint8 :: comm_ring_1
begin
lift_definition zero_uint8 :: uint8 is "0 :: 8 word" .
lift_definition one_uint8 :: uint8 is "1" .
lift_definition plus_uint8 :: "uint8 ⇒ uint8 ⇒ uint8" is "(+) :: 8 word ⇒ _" .
lift_definition minus_uint8 :: "uint8 ⇒ uint8 ⇒ uint8" is "(-)" .
lift_definition uminus_uint8 :: "uint8 ⇒ uint8" is uminus .
lift_definition times_uint8 :: "uint8 ⇒ uint8 ⇒ uint8" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint8 :: semiring_modulo
begin
lift_definition divide_uint8 :: "uint8 ⇒ uint8 ⇒ uint8" is "(div)" .
lift_definition modulo_uint8 :: "uint8 ⇒ uint8 ⇒ uint8" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint8 :: linorder begin
lift_definition less_uint8 :: "uint8 ⇒ uint8 ⇒ bool" is "(<)" .
lift_definition less_eq_uint8 :: "uint8 ⇒ uint8 ⇒ bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint8.rep_eq less_eq_uint8.rep_eq

context
includes lifting_syntax
notes
transfer_rule_of_bool [transfer_rule]
transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
"((=) ===> cr_uint8) of_bool of_bool"
by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
"((=) ===> cr_uint8) numeral numeral"
by transfer_prover

lemma [transfer_rule]:
‹(cr_uint8 ===> (⟷)) even ((dvd) 2 :: uint8 ⇒ bool)›
by (unfold dvd_def) transfer_prover

end

instantiation uint8 :: semiring_bits
begin

lift_definition bit_uint8 :: ‹uint8 ⇒ nat ⇒ bool› is bit .

instance
by (standard; transfer)
(fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint8 :: semiring_bit_shifts
begin
lift_definition push_bit_uint8 :: ‹nat ⇒ uint8 ⇒ uint8› is push_bit .
lift_definition drop_bit_uint8 :: ‹nat ⇒ uint8 ⇒ uint8› is drop_bit .
lift_definition take_bit_uint8 :: ‹nat ⇒ uint8 ⇒ uint8› is take_bit .
instance by (standard; transfer)
(fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint8 :: ring_bit_operations
begin
lift_definition not_uint8 :: ‹uint8 ⇒ uint8› is NOT .
lift_definition and_uint8 :: ‹uint8 ⇒ uint8 ⇒ uint8› is ‹(AND)› .
lift_definition or_uint8 :: ‹uint8 ⇒ uint8 ⇒ uint8› is ‹(OR)› .
lift_definition xor_uint8 :: ‹uint8 ⇒ uint8 ⇒ uint8› is ‹(XOR)› .
lift_definition mask_uint8 :: ‹nat ⇒ uint8› is mask .
instance by (standard; transfer)
(simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
‹take_bit n a = a AND mask n› for a :: uint8

lemma [code]:
‹mask (Suc n) = push_bit n (1 :: uint8) OR mask n›
‹mask 0 = (0 :: uint8)›

instance uint8 :: semiring_bit_syntax ..

context
includes lifting_syntax
begin

lemma test_bit_uint8_transfer [transfer_rule]:
‹(cr_uint8 ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint8_transfer [transfer_rule]:
‹(cr_uint8 ===> (=) ===> cr_uint8) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint8_transfer [transfer_rule]:
‹(cr_uint8 ===> (=) ===> cr_uint8) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint8 :: lsb
begin
lift_definition lsb_uint8 :: ‹uint8 ⇒ bool› is lsb .
instance by (standard; transfer)
(fact lsb_odd)
end

instantiation uint8 :: msb
begin
lift_definition msb_uint8 :: ‹uint8 ⇒ bool› is msb .
instance ..
end

instantiation uint8 :: set_bit
begin
lift_definition set_bit_uint8 :: ‹uint8 ⇒ nat ⇒ bool ⇒ uint8› is set_bit .
instance
apply standard
apply transfer
apply (simp add: bit_simps)
done
end

instantiation uint8 :: bit_comprehension begin
lift_definition set_bits_uint8 :: "(nat ⇒ bool) ⇒ uint8" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint8.rep_eq lsb_uint8.rep_eq msb_uint8.rep_eq

instantiation uint8 :: equal begin
lift_definition equal_uint8 :: "uint8 ⇒ uint8 ⇒ bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint8.rep_eq

instantiation uint8 :: size begin
lift_definition size_uint8 :: "uint8 ⇒ nat" is "size" .
instance ..
end

lemmas [code] = size_uint8.rep_eq

lift_definition sshiftr_uint8 :: "uint8 ⇒ nat ⇒ uint8" (infixl ">>>" 55) is ‹λw n. signed_drop_bit n w› .

lift_definition uint8_of_int :: "int ⇒ uint8" is "word_of_int" .

definition uint8_of_nat :: "nat ⇒ uint8"
where "uint8_of_nat = uint8_of_int ∘ int"

lift_definition int_of_uint8 :: "uint8 ⇒ int" is "uint" .
lift_definition nat_of_uint8 :: "uint8 ⇒ nat" is "unat" .

definition integer_of_uint8 :: "uint8 ⇒ integer"
where "integer_of_uint8 = integer_of_int o int_of_uint8"

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint8 :: "integer ⇒ uint8" is "word_of_int" .

lemma Rep_uint8_numeral [simp]: "Rep_uint8 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint8_def Abs_uint8_inverse numeral.simps plus_uint8_def)

lemma numeral_uint8_transfer [transfer_rule]:
"(rel_fun (=) cr_uint8) numeral numeral"
by(auto simp add: cr_uint8_def)

lemma numeral_uint8 [code_unfold]: "numeral n = Uint8 (numeral n)"
by transfer simp

lemma Rep_uint8_neg_numeral [simp]: "Rep_uint8 (- numeral n) = - numeral n"
by(simp only: uminus_uint8_def)(simp add: Abs_uint8_inverse)

lemma neg_numeral_uint8 [code_unfold]: "- numeral n = Uint8 (- numeral n)"
by transfer(simp add: cr_uint8_def)

end

lemma Abs_uint8_numeral [code_post]: "Abs_uint8 (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint8_def numeral.simps plus_uint8_def Abs_uint8_inverse)

lemma Abs_uint8_0 [code_post]: "Abs_uint8 0 = 0"

lemma Abs_uint8_1 [code_post]: "Abs_uint8 1 = 1"

section ‹Code setup›

code_printing code_module Uint8 ⇀ (SML)
‹(* Test that words can handle numbers between 0 and 3 *)
val _ = if 3 <= Word.wordSize then () else raise (Fail ("wordSize less than 3"));

structure Uint8 : sig
val set_bit : Word8.word -> IntInf.int -> bool -> Word8.word
val shiftl : Word8.word -> IntInf.int -> Word8.word
val shiftr : Word8.word -> IntInf.int -> Word8.word
val shiftr_signed : Word8.word -> IntInf.int -> Word8.word
val test_bit : Word8.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
let val mask = Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
in if b then Word8.orb (x, mask)
else Word8.andb (x, Word8.notb mask)
end

fun shiftl x n =
Word8.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
Word8.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
Word8.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
Word8.andb (x, Word8.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word8.fromInt 0

end; (* struct Uint8 *)›
code_reserved SML Uint8

code_printing code_module Uint8 ⇀ (Haskell)
‹module Uint8(Int8, Word8) where

import Data.Int(Int8)
import Data.Word(Word8)›

text ‹
Scala provides only signed 8bit numbers, so we use these and
implement sign-sensitive operations like comparisons manually.
›

code_printing code_module Uint8 ⇀ (Scala)
‹object Uint8 {

def less(x: Byte, y: Byte) : Boolean =
if (x < 0) y < 0 && x < y
else y < 0 || x < y

def less_eq(x: Byte, y: Byte) : Boolean =
if (x < 0) y < 0 && x <= y
else y < 0 || x <= y

def set_bit(x: Byte, n: BigInt, b: Boolean) : Byte =
if (b)
(x | (1 << n.intValue)).toByte
else
(x & (1 << n.intValue).unary_~).toByte

def shiftl(x: Byte, n: BigInt) : Byte = (x << n.intValue).toByte

def shiftr(x: Byte, n: BigInt) : Byte = ((x & 255) >>> n.intValue).toByte

def shiftr_signed(x: Byte, n: BigInt) : Byte = (x >> n.intValue).toByte

def test_bit(x: Byte, n: BigInt) : Boolean =
(x & (1 << n.intValue)) != 0

} /* object Uint8 */›
code_reserved Scala Uint8

text ‹
Avoid @{term Abs_uint8} in generated code, use @{term Rep_uint8'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint8}.

The new destructor @{term Rep_uint8'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint8} directly, because that makes code\_simp loop.

If code generation raises Match, some equation probably contains @{term Rep_uint8}
([code abstract] equations for @{typ uint8} may use @{term Rep_uint8} because
these instances will be folded away.)

To convert @{typ "8 word"} values into @{typ uint8}, use @{term "Abs_uint8'"}.
›

definition Rep_uint8' where [simp]: "Rep_uint8' = Rep_uint8"

lemma Rep_uint8'_transfer [transfer_rule]:
"rel_fun cr_uint8 (=) (λx. x) Rep_uint8'"
unfolding Rep_uint8'_def by(rule uint8.rep_transfer)

lemma Rep_uint8'_code [code]: "Rep_uint8' x = (BITS n. bit x n)"
by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint8' :: "8 word ⇒ uint8" is "λx :: 8 word. x" .

lemma Abs_uint8'_code [code]: "Abs_uint8' x = Uint8 (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint8 ⇒ _"]]

lemma term_of_uint8_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''" shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint8.uint8.Abs_uint8'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]], TR (STR ''Uint8.uint8'') []]))
(term_of_class.term_of (Rep_uint8' x))"

lemma Uin8_code [code abstract]: "Rep_uint8 (Uint8 i) = word_of_int (int_of_integer_symbolic i)"
unfolding Uint8_def int_of_integer_symbolic_def by(simp add: Abs_uint8_inverse)

code_printing type_constructor uint8 ⇀
(SML) "Word8.word" and
(Scala) "Byte"
| constant Uint8 ⇀
(SML) "Word8.fromLargeInt (IntInf.toLarge _)" and
(Haskell) "(Prelude.fromInteger _ :: Uint8.Word8)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Word8)" and
(Scala) "_.byteValue"
| constant "0 :: uint8" ⇀
(SML) "(Word8.fromInt 0)" and
(Haskell) "(0 :: Uint8.Word8)" and
(Scala) "0.toByte"
| constant "1 :: uint8" ⇀
(SML) "(Word8.fromInt 1)" and
(Haskell) "(1 :: Uint8.Word8)" and
(Scala) "1.toByte"
| constant "plus :: uint8 ⇒ _ ⇒ _" ⇀
(SML) "Word8.+ ((_), (_))" and
(Haskell) infixl 6 "+" and
(Scala) "(_ +/ _).toByte"
| constant "uminus :: uint8 ⇒ _" ⇀
(SML) "Word8.~" and
(Scala) "(- _).toByte"
| constant "minus :: uint8 ⇒ _" ⇀
(SML) "Word8.- ((_), (_))" and
(Haskell) infixl 6 "-" and
(Scala) "(_ -/ _).toByte"
| constant "times :: uint8 ⇒ _ ⇒ _" ⇀
(SML) "Word8.* ((_), (_))" and
(Haskell) infixl 7 "*" and
(Scala) "(_ */ _).toByte"
| constant "HOL.equal :: uint8 ⇒ _ ⇒ bool" ⇀
(SML) "!((_ : Word8.word) = _)" and
(Haskell) infix 4 "==" and
(Scala) infixl 5 "=="
| class_instance uint8 :: equal ⇀ (Haskell) -
| constant "less_eq :: uint8 ⇒ _ ⇒ bool" ⇀
(SML) "Word8.<= ((_), (_))" and
(Haskell) infix 4 "<=" and
(Scala) "Uint8.less'_eq"
| constant "less :: uint8 ⇒ _ ⇒ bool" ⇀
(SML) "Word8.< ((_), (_))" and
(Haskell) infix 4 "<" and
(Scala) "Uint8.less"
| constant "NOT :: uint8 ⇒ _" ⇀
(SML) "Word8.notb" and
(Scala) "_.unary'_~.toByte"
| constant "(AND) :: uint8 ⇒ _" ⇀
(SML) "Word8.andb ((_),/ (_))" and
(Haskell) infixl 7 "Data_Bits..&." and
(Scala) "(_ & _).toByte"
| constant "(OR) :: uint8 ⇒ _" ⇀
(SML) "Word8.orb ((_),/ (_))" and
(Haskell) infixl 5 "Data_Bits..|." and
(Scala) "(_ | _).toByte"
| constant "(XOR) :: uint8 ⇒ _" ⇀
(SML) "Word8.xorb ((_),/ (_))" and
(Scala) "(_ ^ _).toByte"

definition uint8_divmod :: "uint8 ⇒ uint8 ⇒ uint8 × uint8" where
"uint8_divmod x y =
(if y = 0 then (undefined ((div) :: uint8 ⇒ _) x (0 :: uint8), undefined ((mod) :: uint8 ⇒ _) x (0 :: uint8))
else (x div y, x mod y))"

definition uint8_div :: "uint8 ⇒ uint8 ⇒ uint8"
where "uint8_div x y = fst (uint8_divmod x y)"

definition uint8_mod :: "uint8 ⇒ uint8 ⇒ uint8"
where "uint8_mod x y = snd (uint8_divmod x y)"

lemma div_uint8_code [code]: "x div y = (if y = 0 then 0 else uint8_div x y)"
including undefined_transfer unfolding uint8_divmod_def uint8_div_def
by transfer (simp add: word_div_def)

lemma mod_uint8_code [code]: "x mod y = (if y = 0 then x else uint8_mod x y)"
including undefined_transfer unfolding uint8_mod_def uint8_divmod_def
by transfer (simp add: word_mod_def)

definition uint8_sdiv :: "uint8 ⇒ uint8 ⇒ uint8"
where
"uint8_sdiv x y =
(if y = 0 then undefined ((div) :: uint8 ⇒ _) x (0 :: uint8)
else Abs_uint8 (Rep_uint8 x sdiv Rep_uint8 y))"

definition div0_uint8 :: "uint8 ⇒ uint8"
where [code del]: "div0_uint8 x = undefined ((div) :: uint8 ⇒ _) x (0 :: uint8)"
declare [[code abort: div0_uint8]]

definition mod0_uint8 :: "uint8 ⇒ uint8"
where [code del]: "mod0_uint8 x = undefined ((mod) :: uint8 ⇒ _) x (0 :: uint8)"
declare [[code abort: mod0_uint8]]

lemma uint8_divmod_code [code]:
"uint8_divmod x y =
(if 0x80 ≤ y then if x < y then (0, x) else (1, x - y)
else if y = 0 then (div0_uint8 x, mod0_uint8 x)
else let q = (uint8_sdiv (x >> 1) y) << 1;
r = x - q * y
in if r ≥ y then (q + 1, r - y) else (q, r))"
including undefined_transfer unfolding uint8_divmod_def uint8_sdiv_def div0_uint8_def mod0_uint8_def
apply transfer
apply (simp add: divmod_via_sdivmod)
apply (simp add: shiftl_eq_push_bit shiftr_eq_drop_bit)
done

lemma uint8_sdiv_code [code abstract]:
"Rep_uint8 (uint8_sdiv x y) =
(if y = 0 then Rep_uint8 (undefined ((div) :: uint8 ⇒ _) x (0 :: uint8))
else Rep_uint8 x sdiv Rep_uint8 y)"
unfolding uint8_sdiv_def by(simp add: Abs_uint8_inverse)

text ‹
Note that we only need a translation for signed division, but not for the remainder
because @{thm uint8_divmod_code} computes both with division only.
›

code_printing
constant uint8_div ⇀
(SML) "Word8.div ((_), (_))" and
| constant uint8_mod ⇀
(SML) "Word8.mod ((_), (_))" and
| constant uint8_divmod ⇀
| constant uint8_sdiv ⇀
(Scala) "(_ '/ _).toByte"

definition uint8_test_bit :: "uint8 ⇒ integer ⇒ bool"
where [code del]:
"uint8_test_bit x n =
(if n < 0 ∨ 7 < n then undefined (test_bit :: uint8 ⇒ _) x n
else x !! (nat_of_integer n))"

lemma bit_uint8_code [code]:
"bit x n ⟷ n < 8 ∧ uint8_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint8_test_bit_def
by (transfer, simp, transfer, simp)

lemma uint8_test_bit_code [code]:
"uint8_test_bit w n =
(if n < 0 ∨ 7 < n then undefined (test_bit :: uint8 ⇒ _) w n else Rep_uint8 w !! nat_of_integer n)"
unfolding uint8_test_bit_def
by (simp add: bit_uint8.rep_eq test_bit_eq_bit)

code_printing constant uint8_test_bit ⇀
(SML) "Uint8.test'_bit" and
(Scala) "Uint8.test'_bit" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_test'_bit out of bounds\") else Uint8.test'_bit x i)"

definition uint8_set_bit :: "uint8 ⇒ integer ⇒ bool ⇒ uint8"
where [code del]:
"uint8_set_bit x n b =
(if n < 0 ∨ 7 < n then undefined (set_bit :: uint8 ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint8_code [code]:
"set_bit x n b = (if n < 8 then uint8_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint8_set_bit_def
by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint8_set_bit_code [code abstract]:
"Rep_uint8 (uint8_set_bit w n b) =
(if n < 0 ∨ 7 < n then Rep_uint8 (undefined (set_bit :: uint8 ⇒ _) w n b)
else set_bit (Rep_uint8 w) (nat_of_integer n) b)"
including undefined_transfer unfolding uint8_set_bit_def by transfer simp

code_printing constant uint8_set_bit ⇀
(SML) "Uint8.set'_bit" and
(Scala) "Uint8.set'_bit" and
(Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_set'_bit out of bounds\") else Uint8.set'_bit x i b)"

lift_definition uint8_set_bits :: "(nat ⇒ bool) ⇒ uint8 ⇒ nat ⇒ uint8" is set_bits_aux .

lemma uint8_set_bits_code [code]:
"uint8_set_bits f w n =
(if n = 0 then w
else let n' = n - 1 in uint8_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
apply (transfer fixing: n)
apply (cases n)
apply (simp_all add: shiftl_eq_push_bit)
done

lemma set_bits_uint8 [code]:
"(BITS n. f n) = uint8_set_bits f 0 8"
by transfer(simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint8 shows "lsb x = x !! 0"
by transfer (simp add: lsb_odd)

definition uint8_shiftl :: "uint8 ⇒ integer ⇒ uint8"
where [code del]:
"uint8_shiftl x n = (if n < 0 ∨ 8 ≤ n then undefined (push_bit :: nat ⇒ uint8 ⇒ _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint8_code [code]:
"push_bit n x = (if n < 8 then uint8_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint8_shiftl_def
by transfer simp

lemma uint8_shiftl_code [code abstract]:
"Rep_uint8 (uint8_shiftl w n) =
(if n < 0 ∨ 8 ≤ n then Rep_uint8 (undefined (push_bit :: nat ⇒ uint8 ⇒ _) w n)
else push_bit (nat_of_integer n) (Rep_uint8 w))"
including undefined_transfer unfolding uint8_shiftl_def
by transfer simp

code_printing constant uint8_shiftl ⇀
(SML) "Uint8.shiftl" and
(Scala) "Uint8.shiftl" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftl out of bounds\") else Uint8.shiftl x i)"

definition uint8_shiftr :: "uint8 ⇒ integer ⇒ uint8"
where [code del]:
"uint8_shiftr x n = (if n < 0 ∨ 8 ≤ n then undefined (shiftr :: uint8 ⇒ _) x n else x >> (nat_of_integer n))"

lemma shiftr_uint8_code [code]:
"drop_bit n x = (if n < 8 then uint8_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint8_shiftr_def
by transfer simp

lemma uint8_shiftr_code [code abstract]:
"Rep_uint8 (uint8_shiftr w n) =
(if n < 0 ∨ 8 ≤ n then Rep_uint8 (undefined (shiftr :: uint8 ⇒ _) w n)
else drop_bit (nat_of_integer n) (Rep_uint8 w))"
including undefined_transfer unfolding uint8_shiftr_def by transfer simp

code_printing constant uint8_shiftr ⇀
(SML) "Uint8.shiftr" and
(Scala) "Uint8.shiftr" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_shiftr out of bounds\") else Uint8.shiftr x i)"

definition uint8_sshiftr :: "uint8 ⇒ integer ⇒ uint8"
where [code del]:
"uint8_sshiftr x n =
(if n < 0 ∨ 8 ≤ n then undefined sshiftr_uint8 x n else sshiftr_uint8 x (nat_of_integer n))"

lemma sshiftr_uint8_code [code]:
"x >>> n =
(if n < 8 then uint8_sshiftr x (integer_of_nat n) else if x !! 7 then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint8_sshiftr_def
by transfer (simp add: not_less signed_drop_bit_beyond word_size)

lemma uint8_sshiftr_code [code abstract]:
"Rep_uint8 (uint8_sshiftr w n) =
(if n < 0 ∨ 8 ≤ n then Rep_uint8 (undefined sshiftr_uint8 w n)
else signed_drop_bit (nat_of_integer n) (Rep_uint8 w))"
including undefined_transfer unfolding uint8_sshiftr_def
by transfer simp

code_printing constant uint8_sshiftr ⇀
(SML) "Uint8.shiftr'_signed" and
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint8.Int8) _)) :: Uint8.Word8)" and
(Scala) "Uint8.shiftr'_signed" and
(Eval) "(fn x => fn i => if i < 0 orelse i >= 8 then raise (Fail \"argument to uint8'_sshiftr out of bounds\") else Uint8.shiftr'_signed x i)"

lemma uint8_msb_test_bit: "msb x ⟷ (x :: uint8) !! 7"
by transfer (simp add: msb_word_iff_bit)

lemma msb_uint16_code [code]: "msb x ⟷ uint8_test_bit x 7"
by (simp add: uint8_test_bit_def uint8_msb_test_bit)

lemma uint8_of_int_code [code]: "uint8_of_int i = Uint8 (integer_of_int i)"
including integer.lifting by transfer simp

lemma int_of_uint8_code [code]:
"int_of_uint8 x = int_of_integer (integer_of_uint8 x)"

lemma nat_of_uint8_code [code]:
"nat_of_uint8 x = nat_of_integer (integer_of_uint8 x)"
unfolding integer_of_uint8_def including integer.lifting by transfer simp

definition integer_of_uint8_signed :: "uint8 ⇒ integer"
where
"integer_of_uint8_signed n = (if n !! 7 then undefined integer_of_uint8 n else integer_of_uint8 n)"

lemma integer_of_uint8_signed_code [code]:
"integer_of_uint8_signed n =
(if bit n 7 then undefined integer_of_uint8 n else integer_of_int (uint (Rep_uint8' n)))"
unfolding integer_of_uint8_signed_def integer_of_uint8_def
including undefined_transfer by transfer simp

lemma integer_of_uint8_code [code]:
"integer_of_uint8 n =
(if bit n 7 then integer_of_uint8_signed (n AND 0x7F) OR 0x80 else integer_of_uint8_signed n)"
proof -
have ‹(0x7F :: uint8) = mask 7›
then have *: ‹n AND 0x7F = take_bit 7 n›
by (simp only: take_bit_eq_mask)
have **: ‹(0x80 :: int) = 2 ^ 7›
by simp
show ?thesis
unfolding integer_of_uint8_def integer_of_uint8_signed_def o_def *
including undefined_transfer integer.lifting
apply transfer
apply (auto simp add: bit_take_bit_iff uint_take_bit_eq)
apply (rule bit_eqI)
apply (simp add: bit_uint_iff bit_or_iff bit_take_bit_iff)
apply (simp only: ** bit_exp_iff)
apply auto
done
qed

code_printing
constant "integer_of_uint8" ⇀
(SML) "IntInf.fromLarge (Word8.toLargeInt _)" and
| constant "integer_of_uint8_signed" ⇀
(Scala) "BigInt"

section ‹Quickcheck setup›

definition uint8_of_natural :: "natural ⇒ uint8"
where "uint8_of_natural x ≡ Uint8 (integer_of_natural x)"

instantiation uint8 :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint8 ≡ qc_random_cnv uint8_of_natural"
definition "exhaustive_uint8 ≡ qc_exhaustive_cnv uint8_of_natural"
definition "full_exhaustive_uint8 ≡ qc_full_exhaustive_cnv uint8_of_natural"
instance ..
end

instantiation uint8 :: narrowing begin

interpretation quickcheck_narrowing_samples
"λi. let x = Uint8 i in (x, 0xFF - x)" "0"
"Typerep.Typerep (STR ''Uint8.uint8'') []" .

definition "narrowing_uint8 d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint8 itself ⇒ _"]]
lemmas partial_term_of_uint8 [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint8 (infixl ">>>" 55)

end


# Theory Uint

(*  Title:      Uint.thy
Author:     Peter Lammich, TU Munich
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Unsigned words of default size›

theory Uint imports
Code_Target_Word_Base
begin

text ‹
This theory provides access to words in the target languages of the code generator
whose bit width is the default of the target language. To that end, the type ‹uint›
models words of width ‹dflt_size›, but ‹dflt_size› is known only to be positive.

Usage restrictions:
Default-size words (type ‹uint›) cannot be used for evaluation, because
the results depend on the particular choice of word size in the target language
and implementation. Symbolic evaluation has not yet been set up for ‹uint›.
›

text ‹The default size type›
typedecl dflt_size

instantiation dflt_size :: typerep begin
definition "typerep_class.typerep ≡  λ_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []"
instance ..
end

consts dflt_size_aux :: "nat"
specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0"
by auto
hide_fact dflt_size_aux_def

instantiation dflt_size :: len begin
definition "len_of_dflt_size (_ :: dflt_size itself) ≡ dflt_size_aux"
instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0)
end

abbreviation "dflt_size ≡ len_of (TYPE (dflt_size))"

context includes integer.lifting begin
lift_definition dflt_size_integer :: integer is "int dflt_size" .
declare dflt_size_integer_def[code del]
― ‹The code generator will substitute a machine-dependent value for this constant›

lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer"
by transfer simp

lemma dflt_size[simp]:
"dflt_size > 0"
"dflt_size ≥ Suc 0"
"¬ dflt_size < Suc 0"
using len_gt_0[where 'a=dflt_size]
by (simp_all del: len_gt_0)
end

declare prod.Quotient[transfer_rule]

section ‹Type definition and primitive operations›

typedef uint = "UNIV :: dflt_size word set" ..

setup_lifting type_definition_uint

text ‹Use an abstract type for code generation to disable pattern matching on @{term Abs_uint}.›
declare Rep_uint_inverse[code abstype]

declare Quotient_uint[transfer_rule]

instantiation uint :: comm_ring_1
begin
lift_definition zero_uint :: uint is "0 :: dflt_size word" .
lift_definition one_uint :: uint is "1" .
lift_definition plus_uint :: "uint ⇒ uint ⇒ uint" is "(+) :: dflt_size word ⇒ _" .
lift_definition minus_uint :: "uint ⇒ uint ⇒ uint" is "(-)" .
lift_definition uminus_uint :: "uint ⇒ uint" is uminus .
lift_definition times_uint :: "uint ⇒ uint ⇒ uint" is "(*)" .
instance by (standard; transfer) (simp_all add: algebra_simps)
end

instantiation uint :: semiring_modulo
begin
lift_definition divide_uint :: "uint ⇒ uint ⇒ uint" is "(div)" .
lift_definition modulo_uint :: "uint ⇒ uint ⇒ uint" is "(mod)" .
instance by (standard; transfer) (fact word_mod_div_equality)
end

instantiation uint :: linorder begin
lift_definition less_uint :: "uint ⇒ uint ⇒ bool" is "(<)" .
lift_definition less_eq_uint :: "uint ⇒ uint ⇒ bool" is "(≤)" .
instance by (standard; transfer) (simp_all add: less_le_not_le linear)
end

lemmas [code] = less_uint.rep_eq less_eq_uint.rep_eq

context
includes lifting_syntax
notes
transfer_rule_of_bool [transfer_rule]
transfer_rule_numeral [transfer_rule]
begin

lemma [transfer_rule]:
"((=) ===> cr_uint) of_bool of_bool"
by transfer_prover

lemma transfer_rule_numeral_uint [transfer_rule]:
"((=) ===> cr_uint) numeral numeral"
by transfer_prover

lemma [transfer_rule]:
‹(cr_uint ===> (⟷)) even ((dvd) 2 :: uint ⇒ bool)›
by (unfold dvd_def) transfer_prover

end

instantiation uint :: semiring_bits
begin

lift_definition bit_uint :: ‹uint ⇒ nat ⇒ bool› is bit .

instance
by (standard; transfer)
(fact bit_iff_odd even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one odd_one bits_induct
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
even_mask_div_iff exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq
div_exp_mod_exp_eq even_mult_exp_div_exp_iff)+

end

instantiation uint :: semiring_bit_shifts
begin
lift_definition push_bit_uint :: ‹nat ⇒ uint ⇒ uint› is push_bit .
lift_definition drop_bit_uint :: ‹nat ⇒ uint ⇒ uint› is drop_bit .
lift_definition take_bit_uint :: ‹nat ⇒ uint ⇒ uint› is take_bit .
instance by (standard; transfer)
(fact push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)+
end

instantiation uint :: ring_bit_operations
begin
lift_definition not_uint :: ‹uint ⇒ uint› is NOT .
lift_definition and_uint :: ‹uint ⇒ uint ⇒ uint› is ‹(AND)› .
lift_definition or_uint :: ‹uint ⇒ uint ⇒ uint› is ‹(OR)› .
lift_definition xor_uint :: ‹uint ⇒ uint ⇒ uint› is ‹(XOR)› .
lift_definition mask_uint :: ‹nat ⇒ uint› is mask .
instance by (standard; transfer)
(simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff minus_eq_not_minus_1 mask_eq_decr_exp)
end

lemma [code]:
‹take_bit n a = a AND mask n› for a :: uint

lemma [code]:
‹mask (Suc n) = push_bit n (1 :: uint) OR mask n›
‹mask 0 = (0 :: uint)›

instance uint :: semiring_bit_syntax ..

context
includes lifting_syntax
begin

lemma test_bit_uint_transfer [transfer_rule]:
‹(cr_uint ===> (=)) bit (!!)›
unfolding test_bit_eq_bit by transfer_prover

lemma shiftl_uint_transfer [transfer_rule]:
‹(cr_uint ===> (=) ===> cr_uint) (λk n. push_bit n k) (<<)›
unfolding shiftl_eq_push_bit by transfer_prover

lemma shiftr_uint_transfer [transfer_rule]:
‹(cr_uint ===> (=) ===> cr_uint) (λk n. drop_bit n k) (>>)›
unfolding shiftr_eq_drop_bit by transfer_prover

end

instantiation uint :: lsb
begin
lift_definition lsb_uint :: ‹uint ⇒ bool› is lsb .
instance by (standard; transfer)
(fact lsb_odd)
end

instantiation uint :: msb
begin
lift_definition msb_uint :: ‹uint ⇒ bool› is msb .
instance ..
end

instantiation uint :: set_bit
begin
lift_definition set_bit_uint :: ‹uint ⇒ nat ⇒ bool ⇒ uint› is set_bit .
instance
apply standard
apply transfer
apply (simp add: bit_simps)
done
end

instantiation uint :: bit_comprehension begin
lift_definition set_bits_uint :: "(nat ⇒ bool) ⇒ uint" is "set_bits" .
instance by (standard; transfer) (fact set_bits_bit_eq)
end

lemmas [code] = bit_uint.rep_eq lsb_uint.rep_eq msb_uint.rep_eq

instantiation uint :: equal begin
lift_definition equal_uint :: "uint ⇒ uint ⇒ bool" is "equal_class.equal" .
instance by standard (transfer, simp add: equal_eq)
end

lemmas [code] = equal_uint.rep_eq

instantiation uint :: size begin
lift_definition size_uint :: "uint ⇒ nat" is "size" .
instance ..
end

lemmas [code] = size_uint.rep_eq

lift_definition sshiftr_uint :: "uint ⇒ nat ⇒ uint" (infixl ">>>" 55) is ‹λw n. signed_drop_bit n w› .

lift_definition uint_of_int :: "int ⇒ uint" is "word_of_int" .

text ‹Use pretty numerals from integer for pretty printing›

context includes integer.lifting begin

lift_definition Uint :: "integer ⇒ uint" is "word_of_int" .

lemma Rep_uint_numeral [simp]: "Rep_uint (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint_def Abs_uint_inverse numeral.simps plus_uint_def)

lemma numeral_uint_transfer [transfer_rule]:
"(rel_fun (=) cr_uint) numeral numeral"
by(auto simp add: cr_uint_def)

lemma numeral_uint [code_unfold]: "numeral n = Uint (numeral n)"
by transfer simp

lemma Rep_uint_neg_numeral [simp]: "Rep_uint (- numeral n) = - numeral n"
by(simp only: uminus_uint_def)(simp add: Abs_uint_inverse)

lemma neg_numeral_uint [code_unfold]: "- numeral n = Uint (- numeral n)"
by transfer(simp add: cr_uint_def)

end

lemma Abs_uint_numeral [code_post]: "Abs_uint (numeral n) = numeral n"
by(induction n)(simp_all add: one_uint_def numeral.simps plus_uint_def Abs_uint_inverse)

lemma Abs_uint_0 [code_post]: "Abs_uint 0 = 0"

lemma Abs_uint_1 [code_post]: "Abs_uint 1 = 1"

section ‹Code setup›

code_printing code_module Uint ⇀ (SML)
‹
structure Uint : sig
val set_bit : Word.word -> IntInf.int -> bool -> Word.word
val shiftl : Word.word -> IntInf.int -> Word.word
val shiftr : Word.word -> IntInf.int -> Word.word
val shiftr_signed : Word.word -> IntInf.int -> Word.word
val test_bit : Word.word -> IntInf.int -> bool
end = struct

fun set_bit x n b =
let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))
in if b then Word.orb (x, mask)
else Word.andb (x, Word.notb mask)
end

fun shiftl x n =
Word.<< (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr x n =
Word.>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun shiftr_signed x n =
Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n))

fun test_bit x n =
Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0

end; (* struct Uint *)›
code_reserved SML Uint

code_printing code_module Uint ⇀ (Haskell)
‹module Uint(Int, Word, dflt_size) where

import qualified Prelude
import Data.Int(Int)
import Data.Word(Word)
import qualified Data.Bits

dflt_size :: Prelude.Integer
dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where
bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
bitSize_aux = Data.Bits.bitSize›
‹module Uint(Int, Word, dflt_size) where

import qualified Prelude
import Data.Int(Int)
import Data.Word(Word)
import qualified Data.Bits

dflt_size :: Prelude.Int
dflt_size = bitSize_aux (0::Word) where
bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int
bitSize_aux = Data.Bits.bitSize
›
code_reserved Haskell Uint dflt_size

text ‹
OCaml and Scala provide only signed bit numbers, so we use these and
implement sign-sensitive operations like comparisons manually.
›

code_printing code_module "Uint" ⇀ (OCaml)
‹module Uint : sig
type t = int
val dflt_size : Z.t
val less : t -> t -> bool
val less_eq : t -> t -> bool
val set_bit : t -> Z.t -> bool -> t
val shiftl : t -> Z.t -> t
val shiftr : t -> Z.t -> t
val shiftr_signed : t -> Z.t -> t
val test_bit : t -> Z.t -> bool
val int_mask : int
val int32_mask : int32
val int64_mask : int64
end = struct

type t = int

let dflt_size = Z.of_int Sys.int_size;;

(* negative numbers have their highest bit set,
so they are greater than positive ones *)
let less x y =
if x<0 then
y<0 && x<y
else y < 0 || x < y;;

let less_eq x y =
if x < 0 then
y < 0 &&  x <= y
else y < 0 || x <= y;;

let set_bit x n b =
let mask = 1 lsl (Z.to_int n)
in if b then x lor mask
else x land (lnot mask);;

let shiftl x n = x lsl (Z.to_int n);;

let shiftr x n = x lsr (Z.to_int n);;

let shiftr_signed x n = x asr (Z.to_int n);;

let test_bit x n = x land (1 lsl (Z.to_int n)) <> 0;;

if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;;

if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size)
else Int32.of_string "0xFFFFFFFF";;

if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size)
else Int64.of_string "0xFFFFFFFFFFFFFFFF";;

end;; (*struct Uint*)›
code_reserved OCaml Uint

code_printing code_module Uint ⇀ (Scala)
‹object Uint {
def dflt_size : BigInt = BigInt(32)

def less(x: Int, y: Int) : Boolean =
if (x < 0) y < 0 && x < y
else y < 0 || x < y

def less_eq(x: Int, y: Int) : Boolean =
if (x < 0) y < 0 && x <= y
else y < 0 || x <= y

def set_bit(x: Int, n: BigInt, b: Boolean) : Int =
if (b)
x | (1 << n.intValue)
else
x & (1 << n.intValue).unary_~

def shiftl(x: Int, n: BigInt) : Int = x << n.intValue

def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue

def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue

def test_bit(x: Int, n: BigInt) : Boolean =
(x & (1 << n.intValue)) != 0

} /* object Uint */›
code_reserved Scala Uint

text ‹
OCaml's conversion from Big\_int to int demands that the value fits into a signed integer.
The following justifies the implementation.
›

context includes integer.lifting begin
definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1"
lift_definition wivs_mask_integer :: integer is wivs_mask .
lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1"

definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size"
lift_definition wivs_shift_integer :: integer is wivs_shift .
lemma [code]: "wivs_shift_integer = 2 ^ dflt_size"
by transfer (simp add: wivs_shift_def)

definition wivs_index :: nat where "wivs_index == dflt_size - 1"
lift_definition wivs_index_integer :: integer is "int wivs_index".
lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1"
by transfer (simp add: wivs_index_def of_nat_diff)

definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)"
lift_definition wivs_overflow_integer :: integer is wivs_overflow .
lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)"
by transfer (simp add: wivs_overflow_def)

definition wivs_least :: int where "wivs_least == - wivs_overflow"
lift_definition wivs_least_integer :: integer is wivs_least .
lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))"
by transfer (simp add: wivs_overflow_def wivs_least_def)

definition Uint_signed :: "integer ⇒ uint" where
"Uint_signed i = (if i < wivs_least_integer ∨ wivs_overflow_integer ≤ i then undefined Uint i else Uint i)"

lemma Uint_code [code]:
"Uint i =
(let i' = i AND wivs_mask_integer in
if bit i' wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')"
including undefined_transfer
unfolding Uint_signed_def
apply transfer
apply (subst word_of_int_via_signed)
apply (auto simp add: shiftl_eq_push_bit push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed
wivs_mask_def wivs_index_def wivs_overflow_def wivs_least_def wivs_shift_def)
done

lemma Uint_signed_code [code abstract]:
"Rep_uint (Uint_signed i) =
(if i < wivs_least_integer ∨ i ≥ wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))"
unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def word_of_integer_def
end

text ‹
Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead.
The symbolic implementations for code\_simp use @{term Rep_uint}.

The new destructor @{term Rep_uint'} is executable.
As the simplifier is given the [code abstract] equations literally,
we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop.

If code generation raises Match, some equation probably contains @{term Rep_uint}
([code abstract] equations for @{typ uint} may use @{term Rep_uint} because
these instances will be folded away.)
›

definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint"

lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. bit x n)"
unfolding Rep_uint'_def by transfer (simp add: set_bits_bit_eq)

lift_definition Abs_uint' :: "dflt_size word ⇒ uint" is "λx :: dflt_size word. x" .

lemma Abs_uint'_code [code]:
"Abs_uint' x = Uint (integer_of_int (uint x))"
including integer.lifting by transfer simp

declare [[code drop: "term_of_class.term_of :: uint ⇒ _"]]

lemma term_of_uint_code [code]:
defines "TR ≡ typerep.Typerep" and "bit0 ≡ STR ''Numeral_Type.bit0''"
shows
"term_of_class.term_of x =
Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'')  [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []]))
(term_of_class.term_of (Rep_uint' x))"

text ‹Important:
We must prevent the reflection oracle (eval-tac) to
use our machine-dependent type.
›

code_printing
type_constructor uint ⇀
(SML) "Word.word" and
(OCaml) "Uint.t" and
(Scala) "Int" and
(Eval) "*** \"Error: Machine dependent type\" ***" and
(Quickcheck) "Word.word"
| constant dflt_size_integer ⇀
(SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.wordSize" and
(OCaml) "Uint.dflt'_size" and
(Scala) "Uint.dflt'_size"
| constant Uint ⇀
(SML) "Word.fromLargeInt (IntInf.toLarge _)" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.fromInt" and
(Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and
(Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and
(Scala) "_.intValue"
| constant Uint_signed ⇀
(OCaml) "Z.to'_int"
| constant "0 :: uint" ⇀
(SML) "(Word.fromInt 0)" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "(Word.fromInt 0)" and
(Haskell) "(0 :: Uint.Word)" and
(OCaml) "0" and
(Scala) "0"
| constant "1 :: uint" ⇀
(SML) "(Word.fromInt 1)" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "(Word.fromInt 1)" and
(Haskell) "(1 :: Uint.Word)" and
(OCaml) "1" and
(Scala) "1"
| constant "plus :: uint ⇒ _ " ⇀
(SML) "Word.+ ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.+ ((_), (_))" and
(Haskell) infixl 6 "+" and
(OCaml) "Pervasives.(+)" and
(Scala) infixl 7 "+"
| constant "uminus :: uint ⇒ _" ⇀
(SML) "Word.~" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.~" and
(OCaml) "Pervasives.(~-)" and
(Scala) "!(- _)"
| constant "minus :: uint ⇒ _" ⇀
(SML) "Word.- ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.- ((_), (_))" and
(Haskell) infixl 6 "-" and
(OCaml) "Pervasives.(-)" and
(Scala) infixl 7 "-"
| constant "times :: uint ⇒ _ ⇒ _" ⇀
(SML) "Word.* ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.* ((_), (_))" and
(Haskell) infixl 7 "*" and
(OCaml) "Pervasives.( * )" and
(Scala) infixl 8 "*"
| constant "HOL.equal :: uint ⇒ _ ⇒ bool" ⇀
(SML) "!((_ : Word.word) = _)" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "!((_ : Word.word) = _)" and
(Haskell) infix 4 "==" and
(OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and
(Scala) infixl 5 "=="
| class_instance uint :: equal ⇀
| constant "less_eq :: uint ⇒ _ ⇒ bool" ⇀
(SML) "Word.<= ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.<= ((_), (_))" and
(Haskell) infix 4 "<=" and
(OCaml) "Uint.less'_eq" and
(Scala) "Uint.less'_eq"
| constant "less :: uint ⇒ _ ⇒ bool" ⇀
(SML) "Word.< ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.< ((_), (_))" and
(Haskell) infix 4 "<" and
(OCaml) "Uint.less" and
(Scala) "Uint.less"
| constant "NOT :: uint ⇒ _" ⇀
(SML) "Word.notb" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.notb" and
(OCaml) "Pervasives.lnot" and
(Scala) "_.unary'_~"
| constant "(AND) :: uint ⇒ _" ⇀
(SML) "Word.andb ((_),/ (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.andb ((_),/ (_))" and
(Haskell) infixl 7 "Data_Bits..&." and
(OCaml) "Pervasives.(land)" and
(Scala) infixl 3 "&"
| constant "(OR) :: uint ⇒ _" ⇀
(SML) "Word.orb ((_),/ (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.orb ((_),/ (_))" and
(Haskell) infixl 5 "Data_Bits..|." and
(OCaml) "Pervasives.(lor)" and
(Scala) infixl 1 "|"
| constant "(XOR) :: uint ⇒ _" ⇀
(SML) "Word.xorb ((_),/ (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.xorb ((_),/ (_))" and
(OCaml) "Pervasives.(lxor)" and
(Scala) infixl 2 "^"

definition uint_divmod :: "uint ⇒ uint ⇒ uint × uint" where
"uint_divmod x y =
(if y = 0 then (undefined ((div) :: uint ⇒ _) x (0 :: uint), undefined ((mod) :: uint ⇒ _) x (0 :: uint))
else (x div y, x mod y))"

definition uint_div :: "uint ⇒ uint ⇒ uint"
where "uint_div x y = fst (uint_divmod x y)"

definition uint_mod :: "uint ⇒ uint ⇒ uint"
where "uint_mod x y = snd (uint_divmod x y)"

lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)"
including undefined_transfer unfolding uint_divmod_def uint_div_def
by transfer(simp add: word_div_def)

lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)"
including undefined_transfer unfolding uint_mod_def uint_divmod_def
by transfer(simp add: word_mod_def)

definition uint_sdiv :: "uint ⇒ uint ⇒ uint"
where [code del]:
"uint_sdiv x y =
(if y = 0 then undefined ((div) :: uint ⇒ _) x (0 :: uint)
else Abs_uint (Rep_uint x sdiv Rep_uint y))"

definition div0_uint :: "uint ⇒ uint"
where [code del]: "div0_uint x = undefined ((div) :: uint ⇒ _) x (0 :: uint)"
declare [[code abort: div0_uint]]

definition mod0_uint :: "uint ⇒ uint"
where [code del]: "mod0_uint x = undefined ((mod) :: uint ⇒ _) x (0 :: uint)"
declare [[code abort: mod0_uint]]

definition wivs_overflow_uint :: uint
where "wivs_overflow_uint ≡ push_bit (dflt_size - 1) 1"

lemma uint_divmod_code [code]:
"uint_divmod x y =
(if wivs_overflow_uint ≤ y then if x < y then (0, x) else (1, x - y)
else if y = 0 then (div0_uint x, mod0_uint x)
else let q = push_bit 1 (uint_sdiv (drop_bit 1 x) y);
r = x - q * y
in if r ≥ y then (q + 1, r - y) else (q, r))"
proof (cases ‹y = 0›)
case True
moreover have ‹x ≥ 0›
by transfer simp
moreover have ‹wivs_overflow_uint > 0›
apply (simp add: wivs_overflow_uint_def push_bit_of_1)
apply transfer
apply transfer
apply simp
done
ultimately show ?thesis
by (auto simp add: uint_divmod_def div0_uint_def mod0_uint_def not_less)
next
case False
then show ?thesis
including undefined_transfer
unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def
wivs_overflow_uint_def
apply transfer
apply (simp add: divmod_via_sdivmod push_bit_of_1 shiftl_eq_push_bit shiftr_eq_drop_bit)
done
qed

lemma uint_sdiv_code [code abstract]:
"Rep_uint (uint_sdiv x y) =
(if y = 0 then Rep_uint (undefined ((div) :: uint ⇒ _) x (0 :: uint))
else Rep_uint x sdiv Rep_uint y)"
unfolding uint_sdiv_def by(simp add: Abs_uint_inverse)

text ‹
Note that we only need a translation for signed division, but not for the remainder
because @{thm uint_divmod_code} computes both with division only.
›

code_printing
constant uint_div ⇀
(SML) "Word.div ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.div ((_), (_))" and
| constant uint_mod ⇀
(SML) "Word.mod ((_), (_))" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Word.mod ((_), (_))" and
| constant uint_divmod ⇀
| constant uint_sdiv ⇀
(OCaml) "Pervasives.('/)" and
(Scala) "_ '/ _"

definition uint_test_bit :: "uint ⇒ integer ⇒ bool"
where [code del]:
"uint_test_bit x n =
(if n < 0 ∨ dflt_size_integer ≤ n then undefined (bit :: uint ⇒ _) x n
else bit x (nat_of_integer n))"

lemma test_bit_uint_code [code]:
"bit x n ⟷ n < dflt_size ∧ uint_test_bit x (integer_of_nat n)"
including undefined_transfer integer.lifting unfolding uint_test_bit_def
by (transfer, simp, transfer, simp)

lemma uint_test_bit_code [code]:
"uint_test_bit w n =
(if n < 0 ∨ dflt_size_integer ≤ n then undefined (bit :: uint ⇒ _) w n else bit (Rep_uint w) (nat_of_integer n))"
unfolding uint_test_bit_def by(simp add: bit_uint.rep_eq)

code_printing constant uint_test_bit ⇀
(SML) "Uint.test'_bit" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Uint.test'_bit" and
(OCaml) "Uint.test'_bit" and
(Scala) "Uint.test'_bit"

definition uint_set_bit :: "uint ⇒ integer ⇒ bool ⇒ uint"
where [code del]:
"uint_set_bit x n b =
(if n < 0 ∨ dflt_size_integer ≤ n then undefined (set_bit :: uint ⇒ _) x n b
else set_bit x (nat_of_integer n) b)"

lemma set_bit_uint_code [code]:
"set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)"
including undefined_transfer integer.lifting unfolding uint_set_bit_def
by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size)

lemma uint_set_bit_code [code abstract]:
"Rep_uint (uint_set_bit w n b) =
(if n < 0 ∨ dflt_size_integer ≤ n then Rep_uint (undefined (set_bit :: uint ⇒ _) w n b)
else set_bit (Rep_uint w) (nat_of_integer n) b)"
including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp

code_printing constant uint_set_bit ⇀
(SML) "Uint.set'_bit" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Uint.set'_bit" and
(OCaml) "Uint.set'_bit" and
(Scala) "Uint.set'_bit"

lift_definition uint_set_bits :: "(nat ⇒ bool) ⇒ uint ⇒ nat ⇒ uint" is set_bits_aux .

lemma uint_set_bits_code [code]:
"uint_set_bits f w n =
(if n = 0 then w
else let n' = n - 1 in uint_set_bits f (push_bit 1 w OR (if f n' then 1 else 0)) n')"
apply (transfer fixing: n)
apply (cases n)
apply (simp_all add: shiftl_eq_push_bit)
done

lemma set_bits_uint [code]:
"(BITS n. f n) = uint_set_bits f 0 dflt_size"
by transfer (simp add: set_bits_conv_set_bits_aux)

lemma lsb_code [code]: fixes x :: uint shows "lsb x = bit x 0"
by transfer (simp add: lsb_word_eq)

definition uint_shiftl :: "uint ⇒ integer ⇒ uint"
where [code del]:
"uint_shiftl x n = (if n < 0 ∨ dflt_size_integer ≤ n then undefined (push_bit :: nat ⇒ uint ⇒ _) x n else push_bit (nat_of_integer n) x)"

lemma shiftl_uint_code [code]: "push_bit n x = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint_shiftl_def
by (transfer fixing: n) simp

lemma uint_shiftl_code [code abstract]:
"Rep_uint (uint_shiftl w n) =
(if n < 0 ∨ dflt_size_integer ≤ n then Rep_uint (undefined (push_bit :: nat ⇒ uint ⇒ _) w n) else push_bit (nat_of_integer n) (Rep_uint w))"
including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp

code_printing constant uint_shiftl ⇀
(SML) "Uint.shiftl" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Uint.shiftl" and
(OCaml) "Uint.shiftl" and
(Scala) "Uint.shiftl"

definition uint_shiftr :: "uint ⇒ integer ⇒ uint"
where [code del]:
"uint_shiftr x n = (if n < 0 ∨ dflt_size_integer ≤ n then undefined (drop_bit :: nat ⇒ uint ⇒ _) x n else drop_bit (nat_of_integer n) x)"

lemma shiftr_uint_code [code]: "drop_bit n x = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)"
including undefined_transfer integer.lifting unfolding uint_shiftr_def
by (transfer fixing: n) simp

lemma uint_shiftr_code [code abstract]:
"Rep_uint (uint_shiftr w n) =
(if n < 0 ∨ dflt_size_integer ≤ n then Rep_uint (undefined (drop_bit :: nat ⇒ uint ⇒ _) w n) else drop_bit (nat_of_integer n) (Rep_uint w))"
including undefined_transfer unfolding uint_shiftr_def by transfer simp

code_printing constant uint_shiftr ⇀
(SML) "Uint.shiftr" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Uint.shiftr" and
(OCaml) "Uint.shiftr" and
(Scala) "Uint.shiftr"

definition uint_sshiftr :: "uint ⇒ integer ⇒ uint"
where [code del]:
"uint_sshiftr x n =
(if n < 0 ∨ dflt_size_integer ≤ n then undefined sshiftr_uint x n else sshiftr_uint x (nat_of_integer n))"

lemma sshiftr_uint_code [code]:
"x >>> n =
(if n < dflt_size then uint_sshiftr x (integer_of_nat n) else
if bit x wivs_index then -1 else 0)"
including undefined_transfer integer.lifting unfolding uint_sshiftr_def
by transfer(simp add: not_less signed_drop_bit_beyond word_size wivs_index_def)

lemma uint_sshiftr_code [code abstract]:
"Rep_uint (uint_sshiftr w n) =
(if n < 0 ∨ dflt_size_integer ≤ n then Rep_uint (undefined sshiftr_uint w n) else signed_drop_bit (nat_of_integer n) (Rep_uint w))"
including undefined_transfer unfolding uint_sshiftr_def by transfer simp

code_printing constant uint_sshiftr ⇀
(SML) "Uint.shiftr'_signed" and
(Eval) "(raise (Fail \"Machine dependent code\"))" and
(Quickcheck) "Uint.shiftr'_signed" and
"(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and
(OCaml) "Uint.shiftr'_signed" and
(Scala) "Uint.shiftr'_signed"

lemma uint_msb_test_bit: "msb x ⟷ bit (x :: uint) wivs_index"
by transfer (simp add: msb_word_iff_bit wivs_index_def)

lemma msb_uint_code [code]: "msb x ⟷ uint_test_bit x wivs_index_integer"
apply(simp add: uint_test_bit_def uint_msb_test_bit
wivs_index_integer_code dflt_size_integer_def wivs_index_def)
by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0
nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def)

lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. bit i n)"
by transfer (simp add: word_of_int_conv_set_bits)

section ‹Quickcheck setup›

definition uint_of_natural :: "natural ⇒ uint"
where "uint_of_natural x ≡ Uint (integer_of_natural x)"

instantiation uint :: "{random, exhaustive, full_exhaustive}" begin
definition "random_uint ≡ qc_random_cnv uint_of_natural"
definition "exhaustive_uint ≡ qc_exhaustive_cnv uint_of_natural"
definition "full_exhaustive_uint ≡ qc_full_exhaustive_cnv uint_of_natural"
instance ..
end

instantiation uint :: narrowing begin

interpretation quickcheck_narrowing_samples
"λi. (Uint i, Uint (- i))" "0"
"Typerep.Typerep (STR ''Uint.uint'') []" .

definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d"
declare [[code drop: "partial_term_of :: uint itself ⇒ _"]]
lemmas partial_term_of_uint [code] = partial_term_of_code

instance ..
end

no_notation sshiftr_uint (infixl ">>>" 55)

end


# Theory Native_Cast

(*  Title:      Native_Cast.thy
Author:     Andreas Lochbihler, ETH Zurich
*)

chapter ‹Conversions between unsigned words and between char›

theory Native_Cast
imports
Uint8
Uint16
Uint32
Uint64
begin

text ‹Auxiliary stuff›

lemma integer_of_char_char_of_integer [simp]:
"integer_of_char (char_of_integer x) = x mod 256"
by (simp add: integer_of_char_def char_of_integer_def)

lemma char_of_integer_integer_of_char [simp]:
"char_of_integer (integer_of_char x) = x"
by (simp add: integer_of_char_def char_of_integer_def)

lemma int_lt_numeral [simp]: "int x < numeral n ⟷ x < numeral n"
by (metis nat_numeral zless_nat_eq_int_zless)

lemma int_of_integer_ge_0: "0 ≤ int_of_integer x ⟷ 0 ≤ x"
including integer.lifting by transfer simp

lemma integer_of_char_ge_0 [simp]: "0 ≤ integer_of_char x"
including integer.lifting unfolding integer_of_char_def
by transfer (simp add: of_char_def)

section ‹Conversion between native words›

lift_definition uint8_of_uint16 :: "uint16 ⇒ uint8" is ucast .
lift_definition uint8_of_uint32 :: "uint32 ⇒ uint8" is ucast .
lift_definition uint8_of_uint64 :: "uint64 ⇒ uint8" is ucast .

lift_definition uint16_of_uint8 :: "uint8 ⇒ uint16" is ucast .
lift_definition uint16_of_uint32 :: "uint32 ⇒ uint16" is ucast .
lift_definition uint16_of_uint64 :: "uint64 ⇒ uint16" is ucast .

lift_definition uint32_of_uint8 :: "uint8 ⇒ uint32" is ucast .
lift_definition uint32_of_uint16 :: "uint16 ⇒ uint32" is ucast .
lift_definition uint32_of_uint64 :: "uint64 ⇒ uint32" is ucast .

lift_definition uint64_of_uint8 :: "uint8 ⇒ uint64" is ucast .
lift_definition uint64_of_uint16 :: "uint16 ⇒ uint64" is ucast .
lift_definition uint64_of_uint32 :: "uint32 ⇒ uint64" is ucast .

context
begin

qualified definition mask :: integer
where ‹mask = (0xFFFFFFFF :: integer)›

end

code_printing
constant uint8_of_uint16 ⇀
(SML_word) "Word8.fromLarge (Word16.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
(Scala) "_.toByte"
| constant uint8_of_uint32 ⇀
(SML) "Word8.fromLarge (Word32.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
(Scala) "_.toByte"
| constant uint8_of_uint64 ⇀
(SML) "Word8.fromLarge (Uint64.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint8.Word8)" and
(Scala) "_.toByte"
| constant uint16_of_uint8 ⇀
(SML_word) "Word16.fromLarge (Word8.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
(Scala) "((_).toInt & 0xFF).toChar"
| constant uint16_of_uint32 ⇀
(SML_word) "Word16.fromLarge (Word32.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
(Scala) "_.toChar"
| constant uint16_of_uint64 ⇀
(SML_word) "Word16.fromLarge (Uint64.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint16.Word16)" and
(Scala) "_.toChar"
| constant uint32_of_uint8 ⇀
(SML) "Word32.fromLarge (Word8.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
(Scala) "((_).toInt & 0xFF)"
| constant uint32_of_uint16 ⇀
(SML_word) "Word32.fromLarge (Word16.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
(Scala) "(_).toInt"
| constant uint32_of_uint64 ⇀
(SML_word) "Word32.fromLarge (Uint64.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint32.Word32)" and
(Scala) "(_).toInt" and
(OCaml) "Int64.to'_int32"
| constant uint64_of_uint8 ⇀
(SML_word) "Word64.fromLarge (Word8.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
(Scala) "((_).toLong & 0xFF)"
| constant uint64_of_uint16 ⇀
(SML_word) "Word64.fromLarge (Word16.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
(Scala) "_.toLong"
| constant uint64_of_uint32 ⇀
(SML_word) "Word64.fromLarge (Word32.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint64.Word64)" and
(Scala) "((_).toLong & 0xFFFFFFFFL)" and
(OCaml) "Int64.logand (Int64.of'_int32 _) (Int64.of'_string \"4294967295\")"

text ‹
Use @{const Abs_uint8'} etc. instead of @{const Rep_uint8} in code equations
for conversion functions to avoid exceptions during code generation when the
target language provides only some of the uint types.
›

lemma uint8_of_uint16_code [code]:
"uint8_of_uint16 x = Abs_uint8' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint8_of_uint32_code [code]:
"uint8_of_uint32 x = Abs_uint8' (ucast (Rep_uint32' x))"
by transfer simp

lemma uint8_of_uint64_code [code]:
"uint8_of_uint64 x = Abs_uint8' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint16_of_uint8_code [code]:
"uint16_of_uint8 x = Abs_uint16' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint16_of_uint32_code [code]:
"uint16_of_uint32 x = Abs_uint16' (ucast (Rep_uint32' x))"
by transfer simp

lemma uint16_of_uint64_code [code]:
"uint16_of_uint64 x = Abs_uint16' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint32_of_uint8_code [code]:
"uint32_of_uint8 x = Abs_uint32' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint32_of_uint16_code [code]:
"uint32_of_uint16 x = Abs_uint32' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint32_of_uint64_code [code]:
"uint32_of_uint64 x = Abs_uint32' (ucast (Rep_uint64' x))"
by transfer simp

lemma uint64_of_uint8_code [code]:
"uint64_of_uint8 x = Abs_uint64' (ucast (Rep_uint8' x))"
by transfer simp

lemma uint64_of_uint16_code [code]:
"uint64_of_uint16 x = Abs_uint64' (ucast (Rep_uint16' x))"
by transfer simp

lemma uint64_of_uint32_code [code]:
"uint64_of_uint32 x = Abs_uint64' (ucast (Rep_uint32' x))"
by transfer simp

end


# Theory Native_Cast_Uint

(*  Title:      Native_Cast_Uint.thy
Author:     Andreas Lochbihler, Digital Asset
*)

theory Native_Cast_Uint imports
Native_Cast
Uint
begin

lift_definition uint_of_uint8 :: "uint8 ⇒ uint" is ucast .
lift_definition uint_of_uint16 :: "uint16 ⇒ uint" is ucast .
lift_definition uint_of_uint32 :: "uint32 ⇒ uint" is ucast .
lift_definition uint_of_uint64 :: "uint64 ⇒ uint" is ucast .

lift_definition uint8_of_uint :: "uint ⇒ uint8" is ucast .
lift_definition uint16_of_uint :: "uint ⇒ uint16" is ucast .
lift_definition uint32_of_uint :: "uint ⇒ uint32" is ucast .
lift_definition uint64_of_uint :: "uint ⇒ uint64" is ucast .

code_printing
constant uint_of_uint8 ⇀
(SML) "Word.fromLarge (Word8.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint.Word)" and
(Scala) "((_).toInt & 0xFF)"
| constant uint_of_uint16 ⇀
(SML_word) "Word.fromLarge (Word16.toLarge _)" and
(Haskell) "(Prelude.fromIntegral _ :: Uint.Word)" and
(Scala) "(_).toInt"
| constant