Library EVMOpSem.word8
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 word8 : Type := W8: bool -> list bool -> word8 .
Definition word8_default: word8 := W8 bool_default DAEMON.
Definition bs_to_w8 (seq : bitSequence ) : word8 := match ( resizeBitSeq (Some( 8%nat)) seq) with
| BitSeq _ s b => W8 s b
end.
Definition w8_to_bs (w : word8 ) : bitSequence :=
match ( (w)) with (( W8 s b)) => BitSeq (Some ( 8%nat)) s b end.
Definition word8BinTest {a : Type} (binop : bitSequence -> bitSequence -> a) (w1 : word8 ) (w2 : word8 ) : a:= binop (w8_to_bs w1) (w8_to_bs w2).
Definition word8BinOp (binop : bitSequence -> bitSequence -> bitSequence ) (w1 : word8 ) (w2 : word8 ) : word8 := bs_to_w8 (binop (w8_to_bs w1) (w8_to_bs w2)).
Definition word8NatOp (binop : bitSequence -> nat -> bitSequence ) (w1 : word8 ) (n : nat ) : word8 := bs_to_w8 (binop (w8_to_bs w1) n).
Definition word8UnaryOp (op : bitSequence -> bitSequence ) (w : word8 ) : word8 := bs_to_w8 (op (w8_to_bs w)).
Definition word8ToNat (w : word8 ) : nat := Z.abs_nat ( Coq.ZArith.Zdiv.Zmod( (integerFromBitSeq (w8_to_bs w)))((Z.pred (Z.pos (P_of_succ_nat 256%nat))))).
Definition word8ToNatural (w : word8 ) : nat := (Z.abs_nat ( Coq.ZArith.Zdiv.Zmod( (integerFromBitSeq (w8_to_bs w)))((Z.pred (Z.pos (P_of_succ_nat 256%nat)))))).
Definition word8ToInt (w : word8 ) : Z := (integerFromBitSeq (w8_to_bs w)).
Definition word8ToUInt (w : word8 ) : Z := (Z.pred (Z.pos (P_of_succ_nat (word8ToNat w)))).
Definition word8FromInteger (i : Z ) : word8 := bs_to_w8 (bitSeqFromInteger (Some( 8%nat)) i).
Definition word8FromInt (i : Z ) : word8 := bs_to_w8 (bitSeqFromInteger (Some( 8%nat)) ( i)).
Definition word8FromNat (i : nat ) : word8 := word8FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word8FromNatural (i : nat ) : word8 := word8FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word8FromBoollist (lst : list (bool )) : word8 := match ( bitSeqFromBoolList (List.rev lst)) with
| None => bs_to_w8(bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| Some a => bs_to_w8 a
end.
Definition boolListFromWord8 (w : word8 ) : list (bool ):= List.rev (boolListFrombitSeq( 8%nat) (w8_to_bs w)).
Definition word8FromNumeral (w : nat ) : word8 := bs_to_w8 (bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat w))))).
Definition w8Eq : word8 -> word8 -> bool := classical_boolean_equivalence.
Definition w8Less (bs1 : word8 ) (bs2 : word8 ) : bool := word8BinTest bitSeqLess bs1 bs2.
Definition w8LessEqual (bs1 : word8 ) (bs2 : word8 ) : bool := word8BinTest bitSeqLessEqual bs1 bs2.
Definition w8Greater (bs1 : word8 ) (bs2 : word8 ) : bool := word8BinTest bitSeqGreater bs1 bs2.
Definition w8GreaterEqual (bs1 : word8 ) (bs2 : word8 ) : bool := word8BinTest bitSeqGreaterEqual bs1 bs2.
Definition w8Compare (bs1 : word8 ) (bs2 : word8 ) : ordering := word8BinTest bitSeqCompare bs1 bs2.
Instance x61_Ord : Ord word8 := {
compare := w8Compare;
isLess := w8Less;
isLessEqual := w8LessEqual;
isGreater := w8Greater;
isGreaterEqual := w8GreaterEqual
}.
Instance x60_SetType : SetType word8 := {
setElemCompare := w8Compare
}.
Definition word8Negate : word8 -> word8 := word8UnaryOp bitSeqNegate.
Definition word8Succ : word8 -> word8 := word8UnaryOp bitSeqSucc.
Definition word8Pred : word8 -> word8 := word8UnaryOp bitSeqPred.
Definition word8Lnot : word8 -> word8 := word8UnaryOp bitSeqNot.
Definition word8Add : word8 -> word8 -> word8 := word8BinOp bitSeqAdd.
Definition word8Minus : word8 -> word8 -> word8 := word8BinOp bitSeqMinus.
Definition word8Mult : word8 -> word8 -> word8 := word8BinOp bitSeqMult.
Definition word8IntegerDivision : word8 -> word8 -> word8 := word8BinOp bitSeqDiv.
Definition word8Division : word8 -> word8 -> word8 := word8BinOp bitSeqDiv.
Definition word8Remainder : word8 -> word8 -> word8 := word8BinOp bitSeqMod.
Definition word8Land : word8 -> word8 -> word8 := word8BinOp bitSeqAnd.
Definition word8Lor : word8 -> word8 -> word8 := word8BinOp bitSeqOr.
Definition word8Lxor : word8 -> word8 -> word8 := word8BinOp bitSeqXor.
Definition word8Min : word8 -> word8 -> word8 := word8BinOp (bitSeqMin).
Definition word8Max : word8 -> word8 -> word8 := word8BinOp (bitSeqMax).
Definition word8Power : word8 -> nat -> word8 := word8NatOp bitSeqPow.
Definition word8Asr : word8 -> nat -> word8 := word8NatOp bitSeqArithmeticShiftRight.
Definition word8Lsr : word8 -> nat -> word8 := word8NatOp bitSeqLogicalShiftRight.
Definition word8Lsl : word8 -> nat -> word8 := word8NatOp bitSeqShiftLeft.
Instance x59_NumNegate : NumNegate word8 := {
numNegate := word8Negate
}.
Instance x58_NumAdd : NumAdd word8 := {
numAdd := word8Add
}.
Instance x57_NumMinus : NumMinus word8 := {
numMinus := word8Minus
}.
Instance x56_NumSucc : NumSucc word8 := {
succ := word8Succ
}.
Instance x55_NumPred : NumPred word8 := {
pred := word8Pred
}.
Instance x54_NumMult : NumMult word8 := {
numMult := word8Mult
}.
Instance x53_NumPow : NumPow word8 := {
numPow := word8Power
}.
Instance x52_NumIntegerDivision : NumIntegerDivision word8 := {
numIntegerDivision := word8IntegerDivision
}.
Instance x51_NumDivision : NumDivision word8 := {
numDivision := word8Division
}.
Instance x50_NumRemainder : NumRemainder word8 := {
numRemainder := word8Remainder
}.
Instance x49_OrdMaxMin : OrdMaxMin word8 := {
max := word8Max;
min := word8Min
}.
Instance x48_WordNot : WordNot word8 := {
lnot := word8Lnot
}.
Instance x47_WordAnd : WordAnd word8 := {
conjunction := word8Land
}.
Instance x46_WordOr : WordOr word8 := {
inclusive_or := word8Lor
}.
Instance x45_WordXor : WordXor word8 := {
exclusive_or := word8Lxor
}.
Instance x44_WordLsl : WordLsl word8 := {
left_shift := word8Lsl
}.
Instance x43_WordLsr : WordLsr word8 := {
logicial_right_shift := word8Lsr
}.
Instance x42_WordAsr : WordAsr word8 := {
arithmetic_right_shift := word8Asr
}.
Definition word8UGT (a : word8 ) (b : word8 ) : bool := nat_gtb (word8ToNat a) (word8ToNat b).