Theory Native_Word.Uint64
chapter ‹Unsigned words of 64 bits›
theory Uint64 imports
Word_Type_Copies
Code_Target_Integer_Bit
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.
›
section ‹Type definition and primitive operations›
typedef uint64 = ‹UNIV :: 64 word set› ..
global_interpretation uint64: word_type_copy Abs_uint64 Rep_uint64
using type_definition_uint64 by (rule word_type_copy.intro)
setup_lifting type_definition_uint64
declare uint64.of_word_of [code abstype]
declare Quotient_uint64 [transfer_rule]
instantiation uint64 :: ‹{comm_ring_1, semiring_modulo, equal, linorder}›
begin
lift_definition zero_uint64 :: uint64 is 0 .
lift_definition one_uint64 :: uint64 is 1 .
lift_definition plus_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(+)› .
lift_definition uminus_uint64 :: ‹uint64 ⇒ uint64› is uminus .
lift_definition minus_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(-)› .
lift_definition times_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(*)› .
lift_definition divide_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(div)› .
lift_definition modulo_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹(mod)› .
lift_definition equal_uint64 :: ‹uint64 ⇒ uint64 ⇒ bool› is ‹HOL.equal› .
lift_definition less_eq_uint64 :: ‹uint64 ⇒ uint64 ⇒ bool› is ‹(≤)› .
lift_definition less_uint64 :: ‹uint64 ⇒ uint64 ⇒ bool› is ‹(<)› .
global_interpretation uint64: word_type_copy_ring Abs_uint64 Rep_uint64
by standard (fact zero_uint64.rep_eq one_uint64.rep_eq
plus_uint64.rep_eq uminus_uint64.rep_eq minus_uint64.rep_eq
times_uint64.rep_eq divide_uint64.rep_eq modulo_uint64.rep_eq
equal_uint64.rep_eq less_eq_uint64.rep_eq less_uint64.rep_eq)+
instance proof -
show ‹OFCLASS(uint64, comm_ring_1_class)›
by (rule uint64.of_class_comm_ring_1)
show ‹OFCLASS(uint64, semiring_modulo_class)›
by (fact uint64.of_class_semiring_modulo)
show ‹OFCLASS(uint64, equal_class)›
by (fact uint64.of_class_equal)
show ‹OFCLASS(uint64, linorder_class)›
by (fact uint64.of_class_linorder)
qed
end
instantiation uint64 :: ring_bit_operations
begin
lift_definition bit_uint64 :: ‹uint64 ⇒ nat ⇒ bool› is bit .
lift_definition not_uint64 :: ‹uint64 ⇒ uint64› is ‹Bit_Operations.not› .
lift_definition and_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹Bit_Operations.and› .
lift_definition or_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹Bit_Operations.or› .
lift_definition xor_uint64 :: ‹uint64 ⇒ uint64 ⇒ uint64› is ‹Bit_Operations.xor› .
lift_definition mask_uint64 :: ‹nat ⇒ uint64› is mask .
lift_definition push_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is push_bit .
lift_definition drop_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is drop_bit .
lift_definition signed_drop_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is signed_drop_bit .
lift_definition take_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is take_bit .
lift_definition set_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is Bit_Operations.set_bit .
lift_definition unset_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is unset_bit .
lift_definition flip_bit_uint64 :: ‹nat ⇒ uint64 ⇒ uint64› is flip_bit .
global_interpretation uint64: word_type_copy_bits Abs_uint64 Rep_uint64 signed_drop_bit_uint64
by standard (fact bit_uint64.rep_eq not_uint64.rep_eq and_uint64.rep_eq or_uint64.rep_eq xor_uint64.rep_eq
mask_uint64.rep_eq push_bit_uint64.rep_eq drop_bit_uint64.rep_eq signed_drop_bit_uint64.rep_eq take_bit_uint64.rep_eq
set_bit_uint64.rep_eq unset_bit_uint64.rep_eq flip_bit_uint64.rep_eq)+
instance
by (fact uint64.of_class_ring_bit_operations)
end
lift_definition uint64_of_nat :: ‹nat ⇒ uint64›
is word_of_nat .
lift_definition nat_of_uint64 :: ‹uint64 ⇒ nat›
is unat .
lift_definition uint64_of_int :: ‹int ⇒ uint64›
is word_of_int .
lift_definition int_of_uint64 :: ‹uint64 ⇒ int›
is uint .
context
includes integer.lifting
begin
lift_definition Uint64 :: ‹integer ⇒ uint64›
is word_of_int .
lift_definition integer_of_uint64 :: ‹uint64 ⇒ integer›
is uint .
end
global_interpretation uint64: word_type_copy_more Abs_uint64 Rep_uint64 signed_drop_bit_uint64
uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64
apply standard
apply (simp_all add: uint64_of_nat.rep_eq nat_of_uint64.rep_eq
uint64_of_int.rep_eq int_of_uint64.rep_eq
Uint64.rep_eq integer_of_uint64.rep_eq integer_eq_iff)
done
instantiation uint64 :: "{size, msb, lsb, set_bit, bit_comprehension}"
begin
lift_definition size_uint64 :: ‹uint64 ⇒ nat› is size .
lift_definition msb_uint64 :: ‹uint64 ⇒ bool› is msb .
lift_definition lsb_uint64 :: ‹uint64 ⇒ bool› is lsb .
text ‹Workaround: avoid name space clash by spelling out \<^text>‹lift_definition› explicitly.›
definition set_bit_uint64 :: ‹uint64 ⇒ nat ⇒ bool ⇒ uint64›
where set_bit_uint64_eq: ‹set_bit_uint64 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a›
context
includes lifting_syntax
begin
lemma set_bit_uint64_transfer [transfer_rule]:
‹(cr_uint64 ===> (=) ===> (⟷) ===> cr_uint64) Generic_set_bit.set_bit Generic_set_bit.set_bit›
by (simp only: set_bit_eq [abs_def] set_bit_uint64_eq [abs_def]) transfer_prover
end
lift_definition set_bits_uint64 :: ‹(nat ⇒ bool) ⇒ uint64› is set_bits .
lift_definition set_bits_aux_uint64 :: ‹(nat ⇒ bool) ⇒ nat ⇒ uint64 ⇒ uint64› is set_bits_aux .
global_interpretation uint64: word_type_copy_misc Abs_uint64 Rep_uint64 signed_drop_bit_uint64
uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 64 set_bits_aux_uint64
by (standard; transfer) simp_all
instance using uint64.of_class_bit_comprehension
uint64.of_class_set_bit uint64.of_class_lsb
by simp_all standard
end
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;
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.result (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)›
code_reserved Haskell Uint64
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 =
x < 0 match {
case true => y < 0 && x < y
case false => y < 0 || x < y
}
def less_eq(x: Long, y: Long) : Boolean =
x < 0 match {
case true => y < 0 && x <= y
case false => y < 0 || x <= y
}
def set_bit(x: Long, n: BigInt, b: Boolean) : Long =
b match {
case true => x | (1L << n.intValue)
case false => 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.
›
context
includes bit_operations_syntax
begin
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: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong)
done
lemma Uint64_signed_code [code]:
"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
by(simp add: Abs_uint64_inverse)
end
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))"
by(simp add: term_of_anything)
code_printing
type_constructor uint64 ⇀
(SML) "Uint64.uint64" and
(Haskell) "Uint64.Word64" 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
(OCaml) "Int64.add" and
(Scala) infixl 7 "+"
| constant "uminus :: uint64 ⇒ _" ⇀
(SML) "Uint64.negate" and
(Haskell) "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 ⇀
(Haskell) -
| 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 "Bit_Operations.not :: uint64 ⇒ _" ⇀
(SML) "Uint64.notb" and
(Haskell) "Data'_Bits.complement" and
(OCaml) "Int64.lognot" and
(Scala) "_.unary'_~"
| constant "Bit_Operations.and :: uint64 ⇒ _" ⇀
(SML) "Uint64.andb" and
(Haskell) infixl 7 "Data_Bits..&." and
(OCaml) "Int64.logand" and
(Scala) infixl 3 "&"
| constant "Bit_Operations.or :: uint64 ⇒ _" ⇀
(SML) "Uint64.orb" and
(Haskell) infixl 5 "Data_Bits..|." and
(OCaml) "Int64.logor" and
(Scala) infixl 1 "|"
| constant "Bit_Operations.xor :: uint64 ⇒ _" ⇀
(SML) "Uint64.xorb" and
(Haskell) "Data'_Bits.xor" 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
less_eq_uint64.rep_eq
apply transfer
apply (simp add: divmod_via_sdivmod push_bit_eq_mult)
done
lemma uint64_sdiv_code [code]:
"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
(Haskell) "Prelude.div"
| constant uint64_mod ⇀
(SML) "Uint64.modulus" and
(Haskell) "Prelude.mod"
| constant uint64_divmod ⇀
(Haskell) "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 (auto dest: bit_imp_le_length)
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
(Haskell) "Data'_Bits.testBitBounded" 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]:
"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
(Haskell) "Data'_Bits.setBitBounded" 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)"
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]:
"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
(Haskell) "Data'_Bits.shiftlBounded" 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]:
"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
(Haskell) "Data'_Bits.shiftrBounded" 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 signed_drop_bit_uint64 n x else signed_drop_bit_uint64 (nat_of_integer n) x)"
lemma sshiftr_uint64_code [code]:
"signed_drop_bit_uint64 n x =
(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]:
"Rep_uint64 (uint64_sshiftr w n) =
(if n < 0 ∨ 64 ≤ n then Rep_uint64 (undefined signed_drop_bit_uint64 n w) 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
(Haskell)
"(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)"
context
includes bit_operations_syntax
begin
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)"
including integer.lifting by transfer simp
lemma uint64_of_nat_code [code]:
"uint64_of_nat = uint64_of_int ∘ int"
by transfer (simp add: fun_eq_iff)
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)))"
by (simp add: integer_of_uint64_signed_def integer_of_uint64_def)
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 ‹integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 = Bit_Operations.set_bit 63 (integer_of_uint64_signed (take_bit 63 n))›
by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1)
moreover have ‹integer_of_uint64 n = Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))› if ‹bit n 63›
proof (rule bit_eqI)
fix m
from that show ‹bit (integer_of_uint64 n) m = bit (Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))) m› for m
including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length)
qed
ultimately show ?thesis
by simp (simp add: integer_of_uint64_signed_def bit_simps)
qed
end
code_printing
constant "integer_of_uint64" ⇀
(SML) "Uint64.toInt" and
(Haskell) "Prelude.toInteger"
| 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
end