Library EVMOpSem.Lem.lem_word

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.

Require Import lem_bool.
Require Export lem_bool.
Require Import lem_maybe.
Require Export lem_maybe.
Require Import lem_num.
Require Export lem_num.
Require Import lem_basic_classes.
Require Export lem_basic_classes.
Require Import lem_list.
Require Export lem_list.


Inductive bitSequence : Type := BitSeq:
   option nat ->
   bool ->
   list bool -> bitSequence .
Definition bitSequence_default: bitSequence := BitSeq DAEMON bool_default DAEMON.

Instance x214_Eq : Eq bitSequence := {
   isEqual := classical_boolean_equivalence;
   isInequal n1 n2 := negb (classical_boolean_equivalence n1 n2)
}.


Program Fixpoint boolListFrombitSeqAux {a : Type} (n : nat ) (s : a) (bl : list a) : list a:=
  if beq_nat n( 0%nat) then [] else
  match ( bl) with
    | [] => replicate n s
    | b :: bl' => b :: (boolListFrombitSeqAux (Coq.Init.Peano.minus n( 1%nat)) s bl')
  end.

Definition boolListFrombitSeq (n : nat ) (b : bitSequence ) : list (bool ):=
  match ( (n,b)) with ( n, ( BitSeq _ s bl)) => boolListFrombitSeqAux n s bl
  end.

Definition bitSeqFromBoolList (bl : list (bool )) : option (bitSequence ) :=
  match ( dest_init bl) with
    | None => None
    | Some (bl', s) => Some (BitSeq (Some (List.length bl)) s bl')
  end.

Definition cleanBitSeq (b : bitSequence ) : bitSequence :=
  match ( (b)) with (( BitSeq len s bl)) =>
    match ( len) with | None =>
      (BitSeq len s (List.rev (dropWhile (Bool.eqb s) (List.rev bl))))
      | Some n =>
      (BitSeq len s
         (List.rev
            (dropWhile (Bool.eqb s)
               (List.rev (lem_list.take (Coq.Init.Peano.minus n ( 1%nat)) bl)))))
    end end.

Definition bitSeqTestBit (b : bitSequence ) (pos : nat ) : option (bool ) :=
  match ( (b,pos)) with (( BitSeq len s bl), pos) =>
    match ( len) with | None =>
      if nat_ltb pos (List.length bl) then index bl pos else Some s
      | Some l =>
      if ( nat_gteb pos l) then None else
        if ( beq_nat pos ( Coq.Init.Peano.minus l ( 1%nat)) ||
             nat_gteb pos (List.length bl)) then Some s else index bl pos end
  end.

Definition bitSeqSetBit (b : bitSequence ) (pos : nat ) (v : bool ) : bitSequence :=
  match ( (b,pos,v)) with (( BitSeq len s bl), pos, v) => let bl' :=
  if ( nat_ltb pos (List.length bl)) then bl else
    (@ List.app _) bl (replicate pos s) in
  let bl'' := lem_list.update bl' pos v in let bs' := BitSeq len s bl'' in
  cleanBitSeq bs' end.

Definition resizeBitSeq (new_len : option (nat ) ) (bs : bitSequence ) : bitSequence :=
  match ( cleanBitSeq bs) with ( BitSeq len s bl) =>
    let shorten_opt := match ( (new_len, len)) with | (None, _) => None
                         | (Some l1, None) => Some l1
                         | (Some l1, Some l2) =>
                         if ( nat_ltb l1 l2) then Some l1 else None end in
  match ( shorten_opt) with | None => BitSeq new_len s bl | Some l1 => (
  let bl' := lem_list.take l1 ( (@ List.app _) bl [s]) in
  match ( dest_init bl') with | None =>
    (BitSeq len s bl)
    | Some (bl'', s') => cleanBitSeq (BitSeq new_len s' bl'') end) end end.

Definition bitSeqNot (b : bitSequence ) : bitSequence :=
  match ( (b)) with (( BitSeq len s bl)) =>
    BitSeq len (negb s) (List.map negb bl) end.



Definition bitSeqBinop (binop : bool -> bool -> bool ) (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := (
  match ( cleanBitSeq bs1) with ( BitSeq len1 s1 bl1) =>
    match ( cleanBitSeq bs2) with ( BitSeq len2 s2 bl2) =>
      let len := match ( (len1, len2)) with | (Some l1, Some l2) =>
                   Some (nat_max l1 l2) | _ => None end in
    let s := binop s1 s2 in let bl := bitSeqBinopAux binop s1 bl1 s2 bl2 in
    cleanBitSeq (BitSeq len s bl) end end
).

Definition bitSeqAnd : bitSequence -> bitSequence -> bitSequence := bitSeqBinop (fun x y => x && y).
Definition bitSeqOr : bitSequence -> bitSequence -> bitSequence := bitSeqBinop (fun x y => x || y).
Definition bitSeqXor : bitSequence -> bitSequence -> bitSequence := bitSeqBinop (fun (b1 : bool ) (b2 : bool )=>negb ( Bool.eqb b1 b2)).

Definition bitSeqShiftLeft (b : bitSequence ) (n : nat ) : bitSequence :=
  match ( (b,n)) with (( BitSeq len s bl), n) =>
    cleanBitSeq (BitSeq len s ( (@ List.app _) (replicate n false) bl)) end.

Definition bitSeqArithmeticShiftRight (bs : bitSequence ) (n : nat ) : bitSequence :=
  match ( cleanBitSeq bs) with ( BitSeq len s bl) =>
    cleanBitSeq (BitSeq len s (drop n bl)) end.

Definition bitSeqLogicalShiftRight (bs : bitSequence ) (n : nat ) : bitSequence :=
  if ( beq_nat n( 0%nat)) then cleanBitSeq bs else
  match ( cleanBitSeq bs) with ( BitSeq len s bl) =>
    match ( len) with | None => cleanBitSeq (BitSeq len s (drop n bl))
      | Some l =>
      cleanBitSeq
        (BitSeq len false ( (@ List.app _) (drop n bl) (replicate l s))) end
  end.

Program Fixpoint integerFromBoolListAux (acc : Z ) (bl : list bool ) : Z :=
  match ( bl) with
    | [] => acc
    |( true :: bl') => integerFromBoolListAux ( Coq.ZArith.BinInt.Z.add( Coq.ZArith.BinInt.Z.mul acc((Z.pred (Z.pos (P_of_succ_nat 2%nat)))))((Z.pred (Z.pos (P_of_succ_nat 1%nat))))) bl'
    |( false :: bl') => integerFromBoolListAux ( Coq.ZArith.BinInt.Z.mul acc((Z.pred (Z.pos (P_of_succ_nat 2%nat))))) bl'
  end.

Definition integerFromBoolList (p : (bool *list (bool )) % type) : Z :=
  match ( (p)) with ( (sign, bl)) =>
    if sign then
      (Coq.ZArith.BinInt.Z.sub Z0
         ( Coq.ZArith.BinInt.Z.add
             (integerFromBoolListAux ((Z.pred (Z.pos (P_of_succ_nat 0%nat))))
                (List.rev (List.map negb bl)))
             ((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))) else
      integerFromBoolListAux ((Z.pred (Z.pos (P_of_succ_nat 0%nat))))
        (List.rev bl) end.


Definition boolListFromInteger (i : Z ) : (bool *list (bool )) % type:=
  if ( int_ltb i((Z.pred (Z.pos (P_of_succ_nat 0%nat))))) then
    (true, List.map negb (boolListFromNatural [] (Z.abs_nat ((Coq.ZArith.BinInt.Z.sub Z0 ( Coq.ZArith.BinInt.Z.add i((Z.pred (Z.pos (P_of_succ_nat 1%nat))))))))))
  else
    (false, boolListFromNatural [] (Z.abs_nat i)).

Definition bitSeqFromInteger (len_opt : option (nat ) ) (i : Z ) : bitSequence :=
  match ( boolListFromInteger i) with (s, bl) =>
    resizeBitSeq len_opt (BitSeq None s bl) end.

Definition integerFromBitSeq (bs : bitSequence ) : Z :=
  match ( cleanBitSeq bs) with ( BitSeq len s bl) =>
    integerFromBoolList (s, bl) end.

Definition bitSeqArithUnaryOp (uop : Z -> Z ) (bs : bitSequence ) : bitSequence :=
  match ( bs) with ( BitSeq len _ _) =>
    bitSeqFromInteger len (uop (integerFromBitSeq bs)) end.

Definition bitSeqArithBinOp (binop : Z -> Z -> Z ) (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence :=
  match ( bs1) with ( BitSeq len1 _ _) =>
    match ( bs2) with ( BitSeq len2 _ _) =>
      let len := match ( (len1, len2)) with | (Some l1, Some l2) =>
                   Some (nat_max l1 l2) | _ => None end in
    bitSeqFromInteger len
      (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2)) end end.

Definition bitSeqArithBinTest {a : Type} (binop : Z -> Z -> a) (bs1 : bitSequence ) (bs2 : bitSequence ) : a:= binop (integerFromBitSeq bs1) (integerFromBitSeq bs2).


Definition bitSeqLess (bs1 : bitSequence ) (bs2 : bitSequence ) : bool := bitSeqArithBinTest int_ltb bs1 bs2.

Definition bitSeqLessEqual (bs1 : bitSequence ) (bs2 : bitSequence ) : bool := bitSeqArithBinTest int_lteb bs1 bs2.

Definition bitSeqGreater (bs1 : bitSequence ) (bs2 : bitSequence ) : bool := bitSeqArithBinTest int_gtb bs1 bs2.

Definition bitSeqGreaterEqual (bs1 : bitSequence ) (bs2 : bitSequence ) : bool := bitSeqArithBinTest int_gteb bs1 bs2.

Definition bitSeqCompare (bs1 : bitSequence ) (bs2 : bitSequence ) : ordering := bitSeqArithBinTest (genericCompare int_ltb Z.eqb) bs1 bs2.

Instance x212_Ord : Ord bitSequence := {
   compare := bitSeqCompare;
   isLess := bitSeqLess;
   isLessEqual := bitSeqLessEqual;
   isGreater := bitSeqGreater;
   isGreaterEqual := bitSeqGreaterEqual
}.

Instance x211_SetType : SetType bitSequence := {
   setElemCompare := bitSeqCompare
}.


Definition bitSeqNegate (bs : bitSequence ) : bitSequence := bitSeqArithUnaryOp (fun (i : Z )=>(Coq.ZArith.BinInt.Z.sub Z0 i)) bs.

Instance x210_NumNegate : NumNegate bitSequence := {
   numNegate := bitSeqNegate
}.


Definition bitSeqAdd (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Coq.ZArith.BinInt.Z.add bs1 bs2.

Instance x209_NumAdd : NumAdd bitSequence := {
   numAdd := bitSeqAdd
}.


Definition bitSeqMinus (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Coq.ZArith.BinInt.Z.sub bs1 bs2.

Instance x208_NumMinus : NumMinus bitSequence := {
   numMinus := bitSeqMinus
}.


Definition bitSeqSucc (bs : bitSequence ) : bitSequence := bitSeqArithUnaryOp (fun (n : Z )=> Coq.ZArith.BinInt.Z.add n((Z.pred (Z.pos (P_of_succ_nat 1%nat))))) bs.

Instance x207_NumSucc : NumSucc bitSequence := {
   succ := bitSeqSucc
}.


Definition bitSeqPred (bs : bitSequence ) : bitSequence := bitSeqArithUnaryOp (fun (n : Z )=> Coq.ZArith.BinInt.Z.sub n((Z.pred (Z.pos (P_of_succ_nat 1%nat))))) bs.

Instance x206_NumPred : NumPred bitSequence := {
   pred := bitSeqPred
}.


Definition bitSeqMult (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Coq.ZArith.BinInt.Z.mul bs1 bs2.

Instance x205_NumMult : NumMult bitSequence := {
   numMult := bitSeqMult
}.


Definition bitSeqPow (bs : bitSequence ) (n : nat ) : bitSequence := bitSeqArithUnaryOp (fun (i : Z ) => Coq.ZArith.Zpower.Zpower_nat i n) bs.

Instance x204_NumPow : NumPow bitSequence := {
   numPow := bitSeqPow
}.


Definition bitSeqDiv (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Z.div bs1 bs2.

Instance x203_NumIntegerDivision : NumIntegerDivision bitSequence := {
   numIntegerDivision := bitSeqDiv
}.

Instance x202_NumDivision : NumDivision bitSequence := {
   numDivision := bitSeqDiv
}.


Definition bitSeqMod (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Coq.ZArith.Zdiv.Zmod bs1 bs2.

Instance x201_NumRemainder : NumRemainder bitSequence := {
   numRemainder := bitSeqMod
}.


Definition bitSeqMin (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Z.min bs1 bs2.

Definition bitSeqMax (bs1 : bitSequence ) (bs2 : bitSequence ) : bitSequence := bitSeqArithBinOp Z.max bs1 bs2.

Instance x200_OrdMaxMin : OrdMaxMin bitSequence := {
   max := bitSeqMax;
   min := bitSeqMin
}.


Class WordNot (a: Type): Type := {
  lnot: a ->a
}.

Class WordAnd (a: Type): Type := {
  conjunction: a ->a ->a
}.
Notation " X 'land' Y" := (conjunction X Y) (at level 70, no associativity).

Class WordOr (a: Type): Type := {
  inclusive_or: a ->a ->a
}.
Notation " X 'lor' Y" := (inclusive_or X Y) (at level 70, no associativity).

Class WordXor (a: Type): Type := {
  exclusive_or: a ->a ->a
}.
Notation " X 'lxor' Y" := (exclusive_or X Y) (at level 70, no associativity).

Class WordLsl (a: Type): Type := {
  left_shift: a -> nat ->a
}.
Notation " X 'lsl' Y" := (left_shift X Y) (at level 70, no associativity).

Class WordLsr (a: Type): Type := {
  logicial_right_shift: a -> nat ->a
}.
Notation " X 'lsr' Y" := (logicial_right_shift X Y) (at level 70, no associativity).

Class WordAsr (a: Type): Type := {
  arithmetic_right_shift: a -> nat ->a
}.
Notation " X 'asr' Y" := (arithmetic_right_shift X Y) (at level 70, no associativity).


Instance x199_WordNot : WordNot bitSequence := {
   lnot := bitSeqNot
}.

Instance x198_WordAnd : WordAnd bitSequence := {
   conjunction := bitSeqAnd
}.

Instance x197_WordOr : WordOr bitSequence := {
   inclusive_or := bitSeqOr
}.

Instance x196_WordXor : WordXor bitSequence := {
   exclusive_or := bitSeqXor
}.

Instance x195_WordLsl : WordLsl bitSequence := {
   left_shift := bitSeqShiftLeft
}.

Instance x194_WordLsr : WordLsr bitSequence := {
   logicial_right_shift := bitSeqLogicalShiftRight
}.

Instance x193_WordAsr : WordAsr bitSequence := {
   arithmetic_right_shift := bitSeqArithmeticShiftRight
}.


Instance x192_WordNot : WordNot Z := {
   lnot := (fun w=>w)
}.


Instance x191_WordOr : WordOr Z := {
   inclusive_or := (fun q w=>w)
}.


Instance x190_WordXor : WordXor Z := {
   exclusive_or := (fun q w=>w)
}.


Instance x189_WordAnd : WordAnd Z := {
   conjunction := (fun q w=>w)
}.


Instance x188_WordLsl : WordLsl Z := {
   left_shift := (fun q w=>q)
}.


Instance x187_WordLsr : WordLsr Z := {
   logicial_right_shift := (fun q w=>q)
}.


Instance x186_WordAsr : WordAsr Z := {
   arithmetic_right_shift := (fun q w=>q)
}.


Instance x185_WordNot : WordNot Z := {
   lnot := (fun w=>w)
}.


Instance x184_WordOr : WordOr Z := {
   inclusive_or := (fun q w=>w)
}.


Instance x183_WordXor : WordXor Z := {
   exclusive_or := (fun q w=>w)
}.


Instance x182_WordAnd : WordAnd Z := {
   conjunction := (fun q w=>w)
}.


Instance x181_WordLsl : WordLsl Z := {
   left_shift := (fun q w=>q)
}.


Instance x180_WordLsr : WordLsr Z := {
   logicial_right_shift := (fun q w=>q)
}.


Instance x179_WordAsr : WordAsr Z := {
   arithmetic_right_shift := (fun q w=>q)
}.


Definition defaultLnot {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x : a) : a:= fromBitSeq (bitSeqNegate (toBitSeq x)).

Definition defaultLand {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x1 : a) (x2 : a) : a:= fromBitSeq (bitSeqAnd (toBitSeq x1) (toBitSeq x2)).

Definition defaultLor {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x1 : a) (x2 : a) : a:= fromBitSeq (bitSeqOr (toBitSeq x1) (toBitSeq x2)).

Definition defaultLxor {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x1 : a) (x2 : a) : a:= fromBitSeq (bitSeqXor (toBitSeq x1) (toBitSeq x2)).

Definition defaultLsl {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x : a) (n : nat ) : a:= fromBitSeq (bitSeqShiftLeft (toBitSeq x) n).

Definition defaultLsr {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x : a) (n : nat ) : a:= fromBitSeq (bitSeqLogicalShiftRight (toBitSeq x) n).

Definition defaultAsr {a : Type} (fromBitSeq : bitSequence -> a) (toBitSeq : a -> bitSequence ) (x : a) (n : nat ) : a:= fromBitSeq (bitSeqArithmeticShiftRight (toBitSeq x) n).

Definition integerLnot (i : Z ) : Z := (Coq.ZArith.BinInt.Z.sub Z0 ( Coq.ZArith.BinInt.Z.add i((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))).

Instance x178_WordNot : WordNot Z := {
   lnot := integerLnot
}.


Definition integerLor (i1 : Z ) (i2 : Z ) : Z := defaultLor integerFromBitSeq (bitSeqFromInteger None) i1 i2.

Instance x177_WordOr : WordOr Z := {
   inclusive_or := integerLor
}.


Definition integerLxor (i1 : Z ) (i2 : Z ) : Z := defaultLxor integerFromBitSeq (bitSeqFromInteger None) i1 i2.

Instance x176_WordXor : WordXor Z := {
   exclusive_or := integerLxor
}.


Definition integerLand (i1 : Z ) (i2 : Z ) : Z := defaultLand integerFromBitSeq (bitSeqFromInteger None) i1 i2.

Instance x175_WordAnd : WordAnd Z := {
   conjunction := integerLand
}.


Definition integerLsl (i : Z ) (n : nat ) : Z := defaultLsl integerFromBitSeq (bitSeqFromInteger None) i n.

Instance x174_WordLsl : WordLsl Z := {
   left_shift := integerLsl
}.


Definition integerAsr (i : Z ) (n : nat ) : Z := defaultAsr integerFromBitSeq (bitSeqFromInteger None) i n.

Instance x173_WordLsr : WordLsr Z := {
   logicial_right_shift := integerAsr
}.

Instance x172_WordAsr : WordAsr Z := {
   arithmetic_right_shift := integerAsr
}.


Definition intFromBitSeq (bs : bitSequence ) : Z := (integerFromBitSeq (resizeBitSeq (Some( 31%nat)) bs)).

Definition bitSeqFromInt (i : Z ) : bitSequence := bitSeqFromInteger (Some( 31%nat)) ( i).

Definition intLnot (i : Z ) : Z := (Coq.ZArith.BinInt.Z.sub Z0 ( Coq.ZArith.BinInt.Z.add i((Z.pred (Z.pos (P_of_succ_nat 1%nat)))))).

Instance x171_WordNot : WordNot Z := {
   lnot := intLnot
}.


Definition intLor (i1 : Z ) (i2 : Z ) : Z := defaultLor intFromBitSeq bitSeqFromInt i1 i2.

Instance x170_WordOr : WordOr Z := {
   inclusive_or := intLor
}.


Definition intLxor (i1 : Z ) (i2 : Z ) : Z := defaultLxor intFromBitSeq bitSeqFromInt i1 i2.

Instance x169_WordXor : WordXor Z := {
   exclusive_or := intLxor
}.


Definition intLand (i1 : Z ) (i2 : Z ) : Z := defaultLand intFromBitSeq bitSeqFromInt i1 i2.

Instance x168_WordAnd : WordAnd Z := {
   conjunction := intLand
}.


Definition intLsl (i : Z ) (n : nat ) : Z := defaultLsl intFromBitSeq bitSeqFromInt i n.

Instance x167_WordLsl : WordLsl Z := {
   left_shift := intLsl
}.


Definition intAsr (i : Z ) (n : nat ) : Z := defaultAsr intFromBitSeq bitSeqFromInt i n.

Instance x166_WordAsr : WordAsr Z := {
   arithmetic_right_shift := intAsr
}.


Definition naturalFromBitSeq (bs : bitSequence ) : nat := Z.abs_nat (integerFromBitSeq bs).

Definition bitSeqFromNatural (len : option (nat ) ) (n : nat ) : bitSequence := bitSeqFromInteger len ((Z.pred (Z.pos (P_of_succ_nat n)))).

Definition naturalLor (i1 : nat ) (i2 : nat ) : nat := defaultLor naturalFromBitSeq (bitSeqFromNatural None) i1 i2.

Instance x165_WordOr : WordOr nat := {
   inclusive_or := naturalLor
}.


Definition naturalLxor (i1 : nat ) (i2 : nat ) : nat := defaultLxor naturalFromBitSeq (bitSeqFromNatural None) i1 i2.

Instance x164_WordXor : WordXor nat := {
   exclusive_or := naturalLxor
}.


Definition naturalLand (i1 : nat ) (i2 : nat ) : nat := defaultLand naturalFromBitSeq (bitSeqFromNatural None) i1 i2.

Instance x163_WordAnd : WordAnd nat := {
   conjunction := naturalLand
}.


Definition naturalLsl (i : nat ) (n : nat ) : nat := defaultLsl naturalFromBitSeq (bitSeqFromNatural None) i n.

Instance x162_WordLsl : WordLsl nat := {
   left_shift := naturalLsl
}.


Definition naturalAsr (i : nat ) (n : nat ) : nat := defaultAsr naturalFromBitSeq (bitSeqFromNatural None) i n.

Instance x161_WordLsr : WordLsr nat := {
   logicial_right_shift := naturalAsr
}.

Instance x160_WordAsr : WordAsr nat := {
   arithmetic_right_shift := naturalAsr
}.


Definition natFromBitSeq (bs : bitSequence ) : nat := (naturalFromBitSeq (resizeBitSeq (Some( 31%nat)) bs)).

Definition bitSeqFromNat (i : nat ) : bitSequence := bitSeqFromNatural (Some( 31%nat)) ( i).

Definition natLor (i1 : nat ) (i2 : nat ) : nat := defaultLor natFromBitSeq bitSeqFromNat i1 i2.

Instance x159_WordOr : WordOr nat := {
   inclusive_or := natLor
}.


Definition natLxor (i1 : nat ) (i2 : nat ) : nat := defaultLxor natFromBitSeq bitSeqFromNat i1 i2.

Instance x158_WordXor : WordXor nat := {
   exclusive_or := natLxor
}.


Definition natLand (i1 : nat ) (i2 : nat ) : nat := defaultLand natFromBitSeq bitSeqFromNat i1 i2.

Instance x157_WordAnd : WordAnd nat := {
   conjunction := natLand
}.


Definition natLsl (i : nat ) (n : nat ) : nat := defaultLsl natFromBitSeq bitSeqFromNat i n.

Instance x156_WordLsl : WordLsl nat := {
   left_shift := natLsl
}.


Definition natAsr (i : nat ) (n : nat ) : nat := defaultAsr natFromBitSeq bitSeqFromNat i n.

Instance x155_WordAsr : WordAsr nat := {
   arithmetic_right_shift := natAsr
}.