Library EVMOpSem.word256
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 helper.
Require Export helper.
Require Import Lem.lem_pervasives.
Require Export Lem.lem_pervasives.
Require Import Lem.lem_word.
Require Export Lem.lem_word.
Definition word256BinTest {a : Type} (binop : bitSequence -> bitSequence -> a) (w1 : (Bvector 256) ) (w2 : (Bvector 256) ) : a:= binop ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w1) ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w2).
Definition word256BinOp (binop : bitSequence -> bitSequence -> bitSequence ) (w1 : (Bvector 256) ) (w2 : (Bvector 256) ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (binop ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w1) ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w2)).
Definition word256NatOp (binop : bitSequence -> nat -> bitSequence ) (w1 : (Bvector 256) ) (n : nat ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (binop ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w1) n).
Definition word256UnaryOp (op : bitSequence -> bitSequence ) (w : (Bvector 256) ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (op ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w)).
Definition size256 : Z := Coq.ZArith.Zpower.Zpower_nat((Z.pred (Z.pos (P_of_succ_nat 2%nat))))( 256%nat).
Definition word256ToNatural (w : (Bvector 256) ) : nat := Z.abs_nat ( Coq.ZArith.Zdiv.Zmod((two_compl_value 255 w)) size256).
Definition word256FromInteger (i : Z ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (bitSeqFromInteger (Some( 256%nat)) i).
Definition word256FromInt (i : Z ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (bitSeqFromInteger (Some( 256%nat)) ( i)).
Definition word256FromNatural (i : nat ) : (Bvector 256) := word256FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word256FromNat (i : nat ) : (Bvector 256) := word256FromInteger ((Z.pred (Z.pos (P_of_succ_nat i)))).
Definition word256FromBoollist (lst : list (bool )) : (Bvector 256) := match ( bitSeqFromBoolList (List.rev lst)) with
| None => (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w))(bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat 0%nat)))))
| Some a => (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) a
end.
Definition boolListFromWord256 (w : (Bvector 256) ) : list (bool ):= List.rev (boolListFrombitSeq( 256%nat) ((fun (w : (Bvector 256) ) => bitSeqFromInteger (Some 256%nat) ((two_compl_value 255 w))) w)).
Definition word256FromNumeral (w : nat ) : (Bvector 256) := (fun (w : bitSequence ) => Z_to_two_compl 255 (integerFromBitSeq w)) (bitSeqFromInteger None ((Z.pred (Z.pos (P_of_succ_nat w))))).
Definition w256Eq : (Bvector 256) -> (Bvector 256) -> bool := classical_boolean_equivalence.
Definition w256Less (bs1 : (Bvector 256) ) (bs2 : (Bvector 256) ) : bool := word256BinTest bitSeqLess bs1 bs2.
Definition w256LessEqual (bs1 : (Bvector 256) ) (bs2 : (Bvector 256) ) : bool := word256BinTest bitSeqLessEqual bs1 bs2.
Definition w256Greater (bs1 : (Bvector 256) ) (bs2 : (Bvector 256) ) : bool := word256BinTest bitSeqGreater bs1 bs2.
Definition w256GreaterEqual (bs1 : (Bvector 256) ) (bs2 : (Bvector 256) ) : bool := word256BinTest bitSeqGreaterEqual bs1 bs2.
Definition w256Compare (bs1 : (Bvector 256) ) (bs2 : (Bvector 256) ) : ordering := word256BinTest bitSeqCompare bs1 bs2.
Instance x19_Ord : Ord (Bvector 256) := {
compare := w256Compare;
isLess := w256Less;
isLessEqual := w256LessEqual;
isGreater := w256Greater;
isGreaterEqual := w256GreaterEqual
}.
Instance x18_SetType : SetType (Bvector 256) := {
setElemCompare := w256Compare
}.
Definition word256Negate : (Bvector 256) -> (Bvector 256) := word256UnaryOp bitSeqNegate.
Definition word256Succ : (Bvector 256) -> (Bvector 256) := word256UnaryOp bitSeqSucc.
Definition word256Pred : (Bvector 256) -> (Bvector 256) := word256UnaryOp bitSeqPred.
Definition word256Lnot : (Bvector 256) -> (Bvector 256) := word256UnaryOp bitSeqNot.
Definition word256Add : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqAdd.
Definition word256Minus : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqMinus.
Definition word256Mult : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqMult.
Definition word256IntegerDivision : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqDiv.
Definition word256Division : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqDiv.
Definition word256Remainder : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqMod.
Definition word256Land : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqAnd.
Definition word256Lor : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqOr.
Definition word256Lxor : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp bitSeqXor.
Definition word256Min : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp (bitSeqMin).
Definition word256Max : (Bvector 256) -> (Bvector 256) -> (Bvector 256) := word256BinOp (bitSeqMax).
Definition word256Power : (Bvector 256) -> nat -> (Bvector 256) := word256NatOp bitSeqPow.
Definition word256Asr : (Bvector 256) -> nat -> (Bvector 256) := word256NatOp bitSeqArithmeticShiftRight.
Definition word256Lsr : (Bvector 256) -> nat -> (Bvector 256) := word256NatOp bitSeqLogicalShiftRight.
Definition word256Lsl : (Bvector 256) -> nat -> (Bvector 256) := word256NatOp bitSeqShiftLeft.
Instance x17_NumNegate : NumNegate (Bvector 256) := {
numNegate := word256Negate
}.
Instance x16_NumAdd : NumAdd (Bvector 256) := {
numAdd := word256Add
}.
Instance x15_NumMinus : NumMinus (Bvector 256) := {
numMinus := word256Minus
}.
Instance x14_NumSucc : NumSucc (Bvector 256) := {
succ := word256Succ
}.
Instance x13_NumPred : NumPred (Bvector 256) := {
pred := word256Pred
}.
Instance x12_NumMult : NumMult (Bvector 256) := {
numMult := word256Mult
}.
Instance x11_NumPow : NumPow (Bvector 256) := {
numPow := word256Power
}.
Instance x10_NumIntegerDivision : NumIntegerDivision (Bvector 256) := {
numIntegerDivision := word256IntegerDivision
}.
Instance x9_NumDivision : NumDivision (Bvector 256) := {
numDivision := word256Division
}.
Instance x8_NumRemainder : NumRemainder (Bvector 256) := {
numRemainder := word256Remainder
}.
Instance x7_OrdMaxMin : OrdMaxMin (Bvector 256) := {
max := word256Max;
min := word256Min
}.
Instance x6_WordNot : WordNot (Bvector 256) := {
lnot := word256Lnot
}.
Instance x5_WordAnd : WordAnd (Bvector 256) := {
conjunction := word256Land
}.
Instance x4_WordOr : WordOr (Bvector 256) := {
inclusive_or := word256Lor
}.
Instance x3_WordXor : WordXor (Bvector 256) := {
exclusive_or := word256Lxor
}.
Instance x2_WordLsl : WordLsl (Bvector 256) := {
left_shift := word256Lsl
}.
Instance x1_WordLsr : WordLsr (Bvector 256) := {
logicial_right_shift := word256Lsr
}.
Instance x0_WordAsr : WordAsr (Bvector 256) := {
arithmetic_right_shift := word256Asr
}.
Definition word256UGT (a : (Bvector 256) ) (b : (Bvector 256) ) : bool := nat_gtb (word256ToNatural a) (word256ToNatural b).
Definition word256ULT (a : (Bvector 256) ) (b : (Bvector 256) ) : bool := nat_ltb (word256ToNatural a) (word256ToNatural b).
Definition word256UGE (a : (Bvector 256) ) (b : (Bvector 256) ) : bool := nat_gteb (word256ToNatural a) (word256ToNatural b).