Library EVMOpSem.word64
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.
Require Import Lem.coqharness.
Open Scope nat_scope.
Open Scope string_scope.
Require Import Lem.lem_pervasives.
Require Export Lem.lem_pervasives.
Require Import Lem.lem_word.
Require Export Lem.lem_word.
Inductive word64 : Type := W64: bool -> list bool -> word64 .
Definition word64_default: word64 := W64 bool_default DAEMON.
Definition bs_to_w64 (seq : bitSequence ) : word64 := match ( resizeBitSeq (Some( 64%nat)) seq) with
| BitSeq _ s b => W64 s b
end.
Definition w64_to_bs (w : word64 ) : bitSequence :=
match ( (w)) with (( W64 s b)) => BitSeq (Some ( 64%nat)) s b end.
Definition word64BinTest {a : Type} (binop : bitSequence -> bitSequence -> a) (w1 : word64 ) (w2 : word64 ) : a:= binop (w64_to_bs w1) (w64_to_bs w2).
Definition word64BinOp (binop : bitSequence -> bitSequence -> bitSequence ) (w1 : word64 ) (w2 : word64 ) : word64 := bs_to_w64 (binop (w64_to_bs w1) (w64_to_bs w2)).
Definition word64NatOp (binop : bitSequence -> nat -> bitSequence ) (w1 : word64 ) (n : nat ) : word64 := bs_to_w64 (binop (w64_to_bs w1) n).
Definition word64UnaryOp (op : bitSequence -> bitSequence ) (w : word64 ) : word64 := bs_to_w64 (op (w64_to_bs w)).
Definition size64 : Z := Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 64%nat).
Definition word64ToInteger (w : word64 ) : Z := integerFromBitSeq (w64_to_bs w).
Definition word64ToNatural (w : word64 ) : nat := Z.abs_nat ( Coq.ZArith.Zdiv.Zmod(word64ToInteger w) size64).
Definition word64FromInteger (i : Z ) : word64 := bs_to_w64 (bitSeqFromInteger (Some( 64%nat)) i).
Definition word64FromInt (i : Z ) : word64 := bs_to_w64 (bitSeqFromInteger (Some( 64%nat)) ( i)).
Definition word64FromNatural (i : nat ) : word64 := word64FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word64FromNat (i : nat ) : word64 := word64FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word64FromBoollist (lst : list (bool )) : word64 := match ( bitSeqFromBoolList (List.rev lst)) with
| None => bs_to_w64(bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| Some a => bs_to_w64 a
end.
Definition boolListFromWord64 (w : word64 ) : list (bool ):= List.rev (boolListFrombitSeq( 64%nat) (w64_to_bs w)).
Definition word64FromNumeral (w : nat ) : word64 := bs_to_w64 (bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat w))))).
Definition w64Eq : word64 -> word64 -> bool := classical_boolean_equivalence.
Definition w64Less (bs1 : word64 ) (bs2 : word64 ) : bool := word64BinTest bitSeqLess bs1 bs2.
Definition w64LessEqual (bs1 : word64 ) (bs2 : word64 ) : bool := word64BinTest bitSeqLessEqual bs1 bs2.
Definition w64Greater (bs1 : word64 ) (bs2 : word64 ) : bool := word64BinTest bitSeqGreater bs1 bs2.
Definition w64GreaterEqual (bs1 : word64 ) (bs2 : word64 ) : bool := word64BinTest bitSeqGreaterEqual bs1 bs2.
Definition w64Compare (bs1 : word64 ) (bs2 : word64 ) : ordering := word64BinTest bitSeqCompare bs1 bs2.
Instance x40_Ord : Ord word64 := {
compare := w64Compare;
isLess := w64Less;
isLessEqual := w64LessEqual;
isGreater := w64Greater;
isGreaterEqual := w64GreaterEqual
}.
Instance x39_SetType : SetType word64 := {
setElemCompare := w64Compare
}.
Definition word64Negate : word64 -> word64 := word64UnaryOp bitSeqNegate.
Definition word64Succ : word64 -> word64 := word64UnaryOp bitSeqSucc.
Definition word64Pred : word64 -> word64 := word64UnaryOp bitSeqPred.
Definition word64Lnot : word64 -> word64 := word64UnaryOp bitSeqNot.
Definition word64Add : word64 -> word64 -> word64 := word64BinOp bitSeqAdd.
Definition word64Minus : word64 -> word64 -> word64 := word64BinOp bitSeqMinus.
Definition word64Mult : word64 -> word64 -> word64 := word64BinOp bitSeqMult.
Definition word64IntegerDivision : word64 -> word64 -> word64 := word64BinOp bitSeqDiv.
Definition word64Division : word64 -> word64 -> word64 := word64BinOp bitSeqDiv.
Definition word64Remainder : word64 -> word64 -> word64 := word64BinOp bitSeqMod.
Definition word64Land : word64 -> word64 -> word64 := word64BinOp bitSeqAnd.
Definition word64Lor : word64 -> word64 -> word64 := word64BinOp bitSeqOr.
Definition word64Lxor : word64 -> word64 -> word64 := word64BinOp bitSeqXor.
Definition word64Min : word64 -> word64 -> word64 := word64BinOp (bitSeqMin).
Definition word64Max : word64 -> word64 -> word64 := word64BinOp (bitSeqMax).
Definition word64Power (a : word64 ) (b : nat ) : word64 := gen_pow(word64FromNumeral 1%nat) word64Mult a b.
Definition word64Asr : word64 -> nat -> word64 := word64NatOp bitSeqArithmeticShiftRight.
Definition word64Lsr : word64 -> nat -> word64 := word64NatOp bitSeqLogicalShiftRight.
Definition word64Lsl : word64 -> nat -> word64 := word64NatOp bitSeqShiftLeft.
Instance x38_NumNegate : NumNegate word64 := {
numNegate := word64Negate
}.
Instance x37_NumAdd : NumAdd word64 := {
numAdd := word64Add
}.
Instance x36_NumMinus : NumMinus word64 := {
numMinus := word64Minus
}.
Instance x35_NumSucc : NumSucc word64 := {
succ := word64Succ
}.
Instance x34_NumPred : NumPred word64 := {
pred := word64Pred
}.
Instance x33_NumMult : NumMult word64 := {
numMult := word64Mult
}.
Instance x32_NumPow : NumPow word64 := {
numPow := word64Power
}.
Instance x31_NumIntegerDivision : NumIntegerDivision word64 := {
numIntegerDivision := word64IntegerDivision
}.
Instance x30_NumDivision : NumDivision word64 := {
numDivision := word64Division
}.
Instance x29_NumRemainder : NumRemainder word64 := {
numRemainder := word64Remainder
}.
Instance x28_OrdMaxMin : OrdMaxMin word64 := {
max := word64Max;
min := word64Min
}.
Instance x27_WordNot : WordNot word64 := {
lnot := word64Lnot
}.
Instance x26_WordAnd : WordAnd word64 := {
conjunction := word64Land
}.
Instance x25_WordOr : WordOr word64 := {
inclusive_or := word64Lor
}.
Instance x24_WordXor : WordXor word64 := {
exclusive_or := word64Lxor
}.
Instance x23_WordLsl : WordLsl word64 := {
left_shift := word64Lsl
}.
Instance x22_WordLsr : WordLsr word64 := {
logicial_right_shift := word64Lsr
}.
Instance x21_WordAsr : WordAsr word64 := {
arithmetic_right_shift := word64Asr
}.
Definition word64UGT (a : word64 ) (b : word64 ) : bool := nat_gtb (word64ToNatural a) (word64ToNatural b).
Definition word64ULT (a : word64 ) (b : word64 ) : bool := nat_ltb (word64ToNatural a) (word64ToNatural b).
Definition word64UGE (a : word64 ) (b : word64 ) : bool := nat_gteb (word64ToNatural a) (word64ToNatural b).