Library EVMOpSem.word32
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 word32 : Type := W32: bool -> list bool -> word32 .
Definition word32_default: word32 := W32 bool_default DAEMON.
Definition bs_to_w32 (seq : bitSequence ) : word32 := match ( resizeBitSeq (Some( 32%nat)) seq) with
| BitSeq _ s b => W32 s b
end.
Definition w32_to_bs (w : word32 ) : bitSequence :=
match ( (w)) with (( W32 s b)) => BitSeq (Some ( 32%nat)) s b end.
Definition word32BinTest {a : Type} (binop : bitSequence -> bitSequence -> a) (w1 : word32 ) (w2 : word32 ) : a:= binop (w32_to_bs w1) (w32_to_bs w2).
Definition word32BinOp (binop : bitSequence -> bitSequence -> bitSequence ) (w1 : word32 ) (w2 : word32 ) : word32 := bs_to_w32 (binop (w32_to_bs w1) (w32_to_bs w2)).
Definition word32NatOp (binop : bitSequence -> nat -> bitSequence ) (w1 : word32 ) (n : nat ) : word32 := bs_to_w32 (binop (w32_to_bs w1) n).
Definition word32UnaryOp (op : bitSequence -> bitSequence ) (w : word32 ) : word32 := bs_to_w32 (op (w32_to_bs w)).
Definition size32 : Z := Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 32%nat).
Definition word32ToInteger (w : word32 ) : Z := integerFromBitSeq (w32_to_bs w).
Definition word32ToNatural (w : word32 ) : nat := Z.abs_nat ( Coq.ZArith.Zdiv.Zmod(word32ToInteger w) size32).
Definition word32FromInteger (i : Z ) : word32 := bs_to_w32 (bitSeqFromInteger (Some( 32%nat)) i).
Definition word32FromInt (i : Z ) : word32 := bs_to_w32 (bitSeqFromInteger (Some( 32%nat)) ( i)).
Definition word32FromNatural (i : nat ) : word32 := word32FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word32FromNat (i : nat ) : word32 := word32FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word32FromBoollist (lst : list (bool )) : word32 := match ( bitSeqFromBoolList (List.rev lst)) with
| None => bs_to_w32(bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| Some a => bs_to_w32 a
end.
Definition boolListFromWord32 (w : word32 ) : list (bool ):= List.rev (boolListFrombitSeq( 32%nat) (w32_to_bs w)).
Definition word32FromNumeral (w : nat ) : word32 := bs_to_w32 (bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat w))))).
Definition w32Eq : word32 -> word32 -> bool := classical_boolean_equivalence.
Definition w32Less (bs1 : word32 ) (bs2 : word32 ) : bool := word32BinTest bitSeqLess bs1 bs2.
Definition w32LessEqual (bs1 : word32 ) (bs2 : word32 ) : bool := word32BinTest bitSeqLessEqual bs1 bs2.
Definition w32Greater (bs1 : word32 ) (bs2 : word32 ) : bool := word32BinTest bitSeqGreater bs1 bs2.
Definition w32GreaterEqual (bs1 : word32 ) (bs2 : word32 ) : bool := word32BinTest bitSeqGreaterEqual bs1 bs2.
Definition w32Compare (bs1 : word32 ) (bs2 : word32 ) : ordering := word32BinTest bitSeqCompare bs1 bs2.
Instance x140_Ord : Ord word32 := {
compare := w32Compare;
isLess := w32Less;
isLessEqual := w32LessEqual;
isGreater := w32Greater;
isGreaterEqual := w32GreaterEqual
}.
Instance x139_SetType : SetType word32 := {
setElemCompare := w32Compare
}.
Definition word32Negate : word32 -> word32 := word32UnaryOp bitSeqNegate.
Definition word32Succ : word32 -> word32 := word32UnaryOp bitSeqSucc.
Definition word32Pred : word32 -> word32 := word32UnaryOp bitSeqPred.
Definition word32Lnot : word32 -> word32 := word32UnaryOp bitSeqNot.
Definition word32Add : word32 -> word32 -> word32 := word32BinOp bitSeqAdd.
Definition word32Minus : word32 -> word32 -> word32 := word32BinOp bitSeqMinus.
Definition word32Mult : word32 -> word32 -> word32 := word32BinOp bitSeqMult.
Definition word32IntegerDivision : word32 -> word32 -> word32 := word32BinOp bitSeqDiv.
Definition word32Division : word32 -> word32 -> word32 := word32BinOp bitSeqDiv.
Definition word32Remainder : word32 -> word32 -> word32 := word32BinOp bitSeqMod.
Definition word32Land : word32 -> word32 -> word32 := word32BinOp bitSeqAnd.
Definition word32Lor : word32 -> word32 -> word32 := word32BinOp bitSeqOr.
Definition word32Lxor : word32 -> word32 -> word32 := word32BinOp bitSeqXor.
Definition word32Min : word32 -> word32 -> word32 := word32BinOp (bitSeqMin).
Definition word32Max : word32 -> word32 -> word32 := word32BinOp (bitSeqMax).
Definition word32Power : word32 -> nat -> word32 := word32NatOp bitSeqPow.
Definition word32Asr : word32 -> nat -> word32 := word32NatOp bitSeqArithmeticShiftRight.
Definition word32Lsr : word32 -> nat -> word32 := word32NatOp bitSeqLogicalShiftRight.
Definition word32Lsl : word32 -> nat -> word32 := word32NatOp bitSeqShiftLeft.
Instance x138_NumNegate : NumNegate word32 := {
numNegate := word32Negate
}.
Instance x137_NumAdd : NumAdd word32 := {
numAdd := word32Add
}.
Instance x136_NumMinus : NumMinus word32 := {
numMinus := word32Minus
}.
Instance x135_NumSucc : NumSucc word32 := {
succ := word32Succ
}.
Instance x134_NumPred : NumPred word32 := {
pred := word32Pred
}.
Instance x133_NumMult : NumMult word32 := {
numMult := word32Mult
}.
Instance x132_NumPow : NumPow word32 := {
numPow := word32Power
}.
Instance x131_NumIntegerDivision : NumIntegerDivision word32 := {
numIntegerDivision := word32IntegerDivision
}.
Instance x130_NumDivision : NumDivision word32 := {
numDivision := word32Division
}.
Instance x129_NumRemainder : NumRemainder word32 := {
numRemainder := word32Remainder
}.
Instance x128_OrdMaxMin : OrdMaxMin word32 := {
max := word32Max;
min := word32Min
}.
Instance x127_WordNot : WordNot word32 := {
lnot := word32Lnot
}.
Instance x126_WordAnd : WordAnd word32 := {
conjunction := word32Land
}.
Instance x125_WordOr : WordOr word32 := {
inclusive_or := word32Lor
}.
Instance x124_WordXor : WordXor word32 := {
exclusive_or := word32Lxor
}.
Instance x123_WordLsl : WordLsl word32 := {
left_shift := word32Lsl
}.
Instance x122_WordLsr : WordLsr word32 := {
logicial_right_shift := word32Lsr
}.
Instance x121_WordAsr : WordAsr word32 := {
arithmetic_right_shift := word32Asr
}.
Definition word32UGT (a : word32 ) (b : word32 ) : bool := nat_gtb (word32ToNatural a) (word32ToNatural b).
Definition word32ULT (a : word32 ) (b : word32 ) : bool := nat_ltb (word32ToNatural a) (word32ToNatural b).
Definition word32UGE (a : word32 ) (b : word32 ) : bool := nat_gteb (word32ToNatural a) (word32ToNatural b).