Library EVMOpSem.word160
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 word160 : Type := W160: bool -> list bool -> word160 .
Definition word160_default: word160 := W160 bool_default DAEMON.
Definition bs_to_w160 (seq : bitSequence ) : word160 := match ( resizeBitSeq (Some( 160%nat)) seq) with
| BitSeq _ s b => W160 s b
end.
Definition w160_to_bs (w : word160 ) : bitSequence :=
match ( (w)) with (( W160 s b)) => BitSeq (Some ( 160%nat)) s b end.
Definition word160BinTest {a : Type} (binop : bitSequence -> bitSequence -> a) (w1 : word160 ) (w2 : word160 ) : a:= binop (w160_to_bs w1) (w160_to_bs w2).
Definition word160BinOp (binop : bitSequence -> bitSequence -> bitSequence ) (w1 : word160 ) (w2 : word160 ) : word160 := bs_to_w160 (binop (w160_to_bs w1) (w160_to_bs w2)).
Definition word160NatOp (binop : bitSequence -> nat -> bitSequence ) (w1 : word160 ) (n : nat ) : word160 := bs_to_w160 (binop (w160_to_bs w1) n).
Definition word160UnaryOp (op : bitSequence -> bitSequence ) (w : word160 ) : word160 := bs_to_w160 (op (w160_to_bs w)).
Definition word160ToInteger (w : word160 ) : Z := integerFromBitSeq (w160_to_bs w).
Definition size160 : Z := Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 160%nat).
Definition word160ToNatural (w : word160 ) : nat := Z.abs_nat ( Coq.ZArith.Zdiv.Zmod(word160ToInteger w) size160).
Definition word160FromInteger (i : Z ) : word160 := bs_to_w160 (bitSeqFromInteger (Some( 160%nat)) i).
Definition word160FromInt (i : Z ) : word160 := bs_to_w160 (bitSeqFromInteger (Some( 160%nat)) ( i)).
Definition word160FromNatural (i : nat ) : word160 := word160FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word160FromBoollist (lst : list (bool )) : word160 := match ( bitSeqFromBoolList (List.rev lst)) with
| None => bs_to_w160(bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| Some a => bs_to_w160 a
end.
Definition boolListFromWord160 (w : word160 ) : list (bool ):= List.rev (boolListFrombitSeq( 160%nat) (w160_to_bs w)).
Definition word160FromNumeral (w : nat ) : word160 := bs_to_w160 (bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat w))))).
Definition w160Eq : word160 -> word160 -> bool := classical_boolean_equivalence.
Definition w160Less (bs1 : word160 ) (bs2 : word160 ) : bool := word160BinTest bitSeqLess bs1 bs2.
Definition w160LessEqual (bs1 : word160 ) (bs2 : word160 ) : bool := word160BinTest bitSeqLessEqual bs1 bs2.
Definition w160Greater (bs1 : word160 ) (bs2 : word160 ) : bool := word160BinTest bitSeqGreater bs1 bs2.
Definition w160GreaterEqual (bs1 : word160 ) (bs2 : word160 ) : bool := word160BinTest bitSeqGreaterEqual bs1 bs2.
Definition w160Compare (bs1 : word160 ) (bs2 : word160 ) : ordering := word160BinTest bitSeqCompare bs1 bs2.
Instance x82_Ord : Ord word160 := {
compare := w160Compare;
isLess := w160Less;
isLessEqual := w160LessEqual;
isGreater := w160Greater;
isGreaterEqual := w160GreaterEqual
}.
Instance x81_SetType : SetType word160 := {
setElemCompare := w160Compare
}.
Definition word160Negate : word160 -> word160 := word160UnaryOp bitSeqNegate.
Definition word160Succ : word160 -> word160 := word160UnaryOp bitSeqSucc.
Definition word160Pred : word160 -> word160 := word160UnaryOp bitSeqPred.
Definition word160Lnot : word160 -> word160 := word160UnaryOp bitSeqNot.
Definition word160Add : word160 -> word160 -> word160 := word160BinOp bitSeqAdd.
Definition word160Minus : word160 -> word160 -> word160 := word160BinOp bitSeqMinus.
Definition word160Mult : word160 -> word160 -> word160 := word160BinOp bitSeqMult.
Definition word160IntegerDivision : word160 -> word160 -> word160 := word160BinOp bitSeqDiv.
Definition word160Division : word160 -> word160 -> word160 := word160BinOp bitSeqDiv.
Definition word160Remainder : word160 -> word160 -> word160 := word160BinOp bitSeqMod.
Definition word160Land : word160 -> word160 -> word160 := word160BinOp bitSeqAnd.
Definition word160Lor : word160 -> word160 -> word160 := word160BinOp bitSeqOr.
Definition word160Lxor : word160 -> word160 -> word160 := word160BinOp bitSeqXor.
Definition word160Min : word160 -> word160 -> word160 := word160BinOp (bitSeqMin).
Definition word160Max : word160 -> word160 -> word160 := word160BinOp (bitSeqMax).
Definition word160Power : word160 -> nat -> word160 := word160NatOp bitSeqPow.
Definition word160Asr : word160 -> nat -> word160 := word160NatOp bitSeqArithmeticShiftRight.
Definition word160Lsr : word160 -> nat -> word160 := word160NatOp bitSeqLogicalShiftRight.
Definition word160Lsl : word160 -> nat -> word160 := word160NatOp bitSeqShiftLeft.
Instance x80_NumNegate : NumNegate word160 := {
numNegate := word160Negate
}.
Instance x79_NumAdd : NumAdd word160 := {
numAdd := word160Add
}.
Instance x78_NumMinus : NumMinus word160 := {
numMinus := word160Minus
}.
Instance x77_NumSucc : NumSucc word160 := {
succ := word160Succ
}.
Instance x76_NumPred : NumPred word160 := {
pred := word160Pred
}.
Instance x75_NumMult : NumMult word160 := {
numMult := word160Mult
}.
Instance x74_NumPow : NumPow word160 := {
numPow := word160Power
}.
Instance x73_NumIntegerDivision : NumIntegerDivision word160 := {
numIntegerDivision := word160IntegerDivision
}.
Instance x72_NumDivision : NumDivision word160 := {
numDivision := word160Division
}.
Instance x71_NumRemainder : NumRemainder word160 := {
numRemainder := word160Remainder
}.
Instance x70_OrdMaxMin : OrdMaxMin word160 := {
max := word160Max;
min := word160Min
}.
Instance x69_WordNot : WordNot word160 := {
lnot := word160Lnot
}.
Instance x68_WordAnd : WordAnd word160 := {
conjunction := word160Land
}.
Instance x67_WordOr : WordOr word160 := {
inclusive_or := word160Lor
}.
Instance x66_WordXor : WordXor word160 := {
exclusive_or := word160Lxor
}.
Instance x65_WordLsl : WordLsl word160 := {
left_shift := word160Lsl
}.
Instance x64_WordLsr : WordLsr word160 := {
logicial_right_shift := word160Lsr
}.
Instance x63_WordAsr : WordAsr word160 := {
arithmetic_right_shift := word160Asr
}.