h$IEJ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~None%(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone'(/8:;<5bv-sized+Bitvector datatype, parameterized by width.bv-sizedWe store the value as an  rather than a , since many of the operations on bitvectors rely on a two's complement representation. However, an invariant on the value is that it must always be positive.Secondly, we maintain the invariant that any constructed BV value has a width whose value is representable in a Haskell Int.bv-sized Check that a  is representable as an .bv-sized Check that a  is representable as an .bv-sizedUnsafe coercion from Natural to Int:. We mostly use this to interact with operations from  Data.Bits. This should only be called when we already know the input Natural8 is small enough, e.g., because we previously called  checkNatural.bv-sizedInternal function for masking the input integer *without* checking that the width is representable as an . We use this instead of  whenever we already have some guarantee that the width is legal.bv-sizedConstruct a bitvector with a particular width, where the width is provided as an explicit  argument. The input , whether positive or negative, is silently truncated to fit into the number of bits demanded by the return type. The width cannot be arbitrarily large; it must be representable as an .mkBV (knownNat @4) 10BV 10mkBV (knownNat @2) 10BV 2mkBV (knownNat @4) (-2)BV 14bv-sizedReturn  if the unsigned  does not fit in the required number of bits, otherwise return the input.bv-sizedLike , but returns 5 if unsigned input integer cannot be represented in w bits.bv-sizedReturn 'Nothing if the signed  does not fit in the required number of bits, otherwise return an unsigned positive integer that fits in w bits.bv-sizedLike , but returns 3 if signed input integer cannot be represented in w bits.bv-sized The zero bitvector of any width.bv-sized2The bitvector with value 1, of any positive width.bv-sized9The bitvector whose value is its own width, of any width. bv-sizedThe minimum unsigned value for bitvector with given width (always 0). bv-sized:The maximum unsigned value for bitvector with given width. bv-sizedThe minimum value for bitvector in two's complement with given width. bv-sizedThe maximum value for bitvector in two's complement with given width. bv-sizedunsignedClamp w i rounds i to the nearest value between 0 and 2^w - 1 (inclusive).bv-sizedsignedClamp w i rounds i to the nearest value between -2^(w-1) and  2^(w-1) - 1 (inclusive).bv-sized Construct a  from a .bv-sized Construct a  from a .bv-sized Construct a  from a .bv-sized Construct a  from a .bv-sized Construct a  from a .bv-sized Construct a  from an .bv-sized Construct a  from an .bv-sized Construct a  from an .bv-sized Construct a  from an .bv-sized Construct a  from a list of bits, in big endian order (bits with lower value index in the list are mapped to higher order bits in the output bitvector). Return the resulting  along with its width.8case bitsBE [True, False] of p -> (fstPair p, sndPair p)(2,BV 2)bv-sized Construct a  from a list of bits, in little endian order (bits with lower value index in the list are mapped to lower order bits in the output bitvector). Return the resulting  along with its width.8case bitsLE [True, False] of p -> (fstPair p, sndPair p)(2,BV 1)bv-sized Convert a  ByteString (big-endian) of length n to an  with 8*n= bits. This function uses a balanced binary fold to achieve  O(n log n); total memory allocation and run-time, in contrast to the O(n^2). that would be required by a naive left-fold.bv-sized Construct a  from a big-endian bytestring.case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) (24,BV 257)bv-sized Construct a ! from a little-endian bytestring.case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) (24,BV 65792)bv-sized Construct a  from a list of bytes, in big endian order (bytes with lower value index in the list are mapped to higher order bytes in the output bitvector).5case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p) (24,BV 257)bv-sized Construct a  from a list of bytes, in little endian order (bytes with lower value index in the list are mapped to lower order bytes in the output bitvector).5case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p) (24,BV 65792)bv-sized=Unsigned interpretation of a bitvector as a positive Integer.bv-sized3Signed interpretation of a bitvector as an Integer. bv-sized4Unsigned interpretation of a bitvector as a Natural.!bv-sizedConvert a bitvector to a list of bits, in big endian order (higher order bits in the bitvector are mapped to lower indices in the output list).-asBitsBE (knownNat @5) (mkBV knownNat 0b1101)[False,True,True,False,True]"bv-sizedConvert a bitvector to a list of bits, in little endian order (lower order bits in the bitvector are mapped to lower indices in the output list).-asBitsLE (knownNat @5) (mkBV knownNat 0b1101)[True,False,True,True,False]#bv-sizedConvert a bitvector to a list of bytes, in big endian order (higher order bytes in the bitvector are mapped to lower indices in the output list). Return & if the width is not a multiple of 8.3asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)Just [170,187,204,221]$bv-sizedConvert a bitvector to a list of bytes, in little endian order (lower order bytes in the bitvector are mapped to lower indices in the output list). Return & if the width is not a multiple of 8.3asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)Just [221,204,187,170]%bv-sized#, but for bytestrings.&bv-sized$, but for bytestrings.'bv-sized Bitwise and.(bv-sized Bitwise or.)bv-sized Bitwise xor.*bv-sized$Bitwise complement (flip every bit).bv-sized:Clamp shift amounts to the word width and coerce to an Int+bv-sizedLeft shift by positive .,bv-sized#Right arithmetic shift by positive .-bv-sized Right logical shift by positive ..bv-sizedBitwise rotate left./bv-sizedBitwise rotate right.0bv-sizedThe : that has a particular bit set, and is 0 everywhere else.1bv-sizedLike 0, but without the requirement that the index bit refers to an actual bit in the output . If it is out of range, just silently return the zero bitvector.2bv-sized setBit bv ix is the same as or bv (bit knownNat ix).3bv-sizedLike 2, but without the requirement that the index bit refers to an actual bit in the input . If it is out of range, just silently return the original input.4bv-sizedclearBit w bv ix is the same as and bv (complement (bit w ix)).5bv-sizedLike 4, but without the requirement that the index bit refers to an actual bit in the input . If it is out of range, just silently return the original input.6bv-sizedcomplementBit bv ix is the same as xor bv (bit knownNat ix).7bv-sizedLike 6, but without the requirement that the index bit refers to an actual bit in the input . If it is out of range, just silently return the original input.8bv-sized Test if a particular bit is set.9bv-sizedLike 8, but takes a ; for the bit index. If the index is out of bounds, return .:bv-sizedGet the number of 1 bits in a .;bv-sizedCount trailing zeros in a .<bv-sizedCount leading zeros in a .=bv-sizedTruncate a bitvector to a particular width given at runtime, while keeping the type-level width constant.>bv-sizedBitvector add.?bv-sizedBitvector subtract.@bv-sizedBitvector multiply.Abv-sizedBitvector division (unsigned). Rounds to zero. Division by zero yields a runtime error.Bbv-sizedBitvector remainder after division (unsigned), when rounded to zero. Division by zero yields a runtime error.Cbv-sizedA and B returned as a pair.Dbv-sizedBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.Ebv-sizedBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.Fbv-sizedD and E returned as a pair.Gbv-sizedBitvector division (signed). Rounds to negative infinity. Division by zero yields a runtime error.Hbv-sizedBitvector remainder after division (signed), when rounded to negative infinity. Division by zero yields a runtime error.Ibv-sizedG and H returned as a pair.Jbv-sizedBitvector absolute value. Returns the 2's complement magnitude of the bitvector.Kbv-sized"2's complement bitvector negation.Lbv-sizedGet the sign bit as a .Mbv-sized1Return 1 if positive, -1 if negative, and 0 if 0.Nbv-sizedSigned less than.Obv-sizedSigned less than or equal.Pbv-sizedUnsigned less than.Qbv-sizedUnsigned less than or equal.Rbv-sized#Unsigned minimum of two bitvectors.Sbv-sized#Unsigned maximum of two bitvectors.Tbv-sized!Signed minimum of two bitvectors.Ubv-sized!Signed maximum of two bitvectors.Vbv-sizedConcatenate two bitvectors. The first argument gets placed in the higher order bits.concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)BV 6:type it it :: BV 5Wbv-sized0Slice out a smaller bitvector from a larger one.select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)BV 3:type it it :: BV 4Xbv-sizedLike W, but takes a  as the index to start selecting from. Neither the index nor the output width is checked to ensure the resulting  lies entirely within the bounds of the original bitvector. Any bits "selected" from beyond the bounds of the input bitvector will be 0. are preferred. We provide this instance to allow the use of  in situations where an arbitrary ordering is required (e.g., as the keys in a map)bv-sizedDesired bitvector widthbv-sized,Integer value to truncate to bitvector widthbv-sizedDesired bitvector widthbv-sized Integer valuebv-sizedWidth of outputbv-sizedDesired bitvector widthbv-sized Integer valuebv-sizednumber of bytesbv-sizednumber of bytes0bv-sizedDesired output widthbv-sizedIndex of bit to set1bv-sizedDesired output widthbv-sizedIndex of bit to set2bv-sizedIndex of bit to setbv-sizedOriginal bitvector3bv-sizedDesired output widthbv-sizedIndex of bit to setbv-sizedOriginal bitvector4bv-sizedDesired output widthbv-sizedIndex of bit to clearbv-sizedOriginal bitvector5bv-sizedDesired output widthbv-sizedIndex of bit to clearbv-sizedOriginal bitvector6bv-sizedIndex of bit to flipbv-sizedOriginal bitvector7bv-sizedDesired output widthbv-sizedIndex of bit to flipbv-sizedOriginal bitvectorVbv-sizedWidth of higher-order bitsbv-sizedWidth of lower-order bitsbv-sizedHigher-order bitsbv-sizedLower-order bitsWbv-sizedIndex to start selecting frombv-sizedDesired output widthbv-sizedBitvector to select fromXbv-sizedIndex to start selecting frombv-sizedDesired output widthbv-sizedBitvector to select fromYbv-sizedDesired output widthbv-sizedBitvector to extendZbv-sizedWidth of input bitvectorbv-sizedDesired output widthbv-sizedBitvector to extend[bv-sizedDesired output widthbv-sizedBitvector to truncate\bv-sizedDesired output widthbv-sizedBitvector to truncatebbv-sized Lower boundbv-sized Upper boundcbv-sized Lower boundbv-sized Upper bound  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghij(c) Galois Inc. 2020BSD-3'Ben Selfridge  experimentalportableNone'(/A|kbv-sized,A value annotated with overflow information.mbv-sized9Datatype representing the possibility of signed overflow.pbv-sized;Datatype representing the possibility of unsigned overflow.sbv-sizedReturn + if a computation caused unsigned overflow.tbv-sizedReturn ) if a computation caused signed overflow.ubv-sized#Return the result of a computation.vbv-sizedBitvector add.wbv-sizedBitvector subtract.xbv-sizedBitvector multiply.ybv-sizedLeft shift by positive .zbv-sizedBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.{bv-sizedBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.|bv-sizedBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.}bv-sizedBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.bv-sizedMonad for bitvector operations which might produce signed or unsigned overflow.klmnopqrstuvwxyz{|}klpqrmnostuyvwxz{|}(c) Galois Inc. 2018BSD-3'Ben Selfridge  experimentalportableNone '(/Bbv-sizedGet the underlying  representation from a . We guarantee that "(\(BV.BV x) -> x) == BV.asUnsigned.  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghij   !"#$%&'()*+-,./0123456789:;<=>?@ADGBEHCFIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghij(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone'(/8DZbv-sizedSigned bit vector.bv-sizedConvenience wrapper for .(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone'(/8E6bv-sizedSigned bit vector.bv-sizedConvenience wrapper for .      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrsttuuvwwxyz{|}~  m%bv-sized-1.0.3-G3lfCRRp5IxDUT13KXmGibData.BitVector.SizedData.BitVector.Sized.OverflowData.BitVector.Sized.SignedData.BitVector.Sized.UnsignedData.BitVector.Sized.PanicData.BitVector.Sized.Internal2parameterized-utils-2.1.3.0-3h8MobDueSiHzJkMv1I5vi#Data.Parameterized.NatRepr.InternalknownNatNatReprBVmkBV mkBVUnsigned mkBVSignedzeroonewidth minUnsigned maxUnsigned minSigned maxSigned unsignedClamp signedClampboolword8word16word32word64int8int16int32int64bitsBEbitsLE bytestringBE bytestringLEbytesBEbytesLE asUnsignedasSigned asNaturalasBitsBEasBitsLE asBytesBE asBytesLEasBytestringBEasBytestringLEandorxor complementshlashrlshrrotateLrotateRbitbit'setBitsetBit'clearBit clearBit' complementBitcomplementBit'testBittestBit'popCountctzclz truncBitsaddsubmuluquoturemuquotRemsquotsremsquotRemsdivsmodsdivModabsnegatesignBitsignumsltsleultuleuminumaxsminsmaxconcatselectselect'zextsexttrunctrunc'mulWide succUnsigned succSigned predUnsigned predSignedenumFromToUnsignedenumFromToSigneduniformM uUniformRM sUniformRMppHexppBinppOctppDecOverflowSignedOverflowNoSignedOverflowUnsignedOverflowNoUnsignedOverflow ofUnsignedofSignedofResultaddOfsubOfmulOfshlOfsquotOfsremOfsdivOfsmodOf$fMonoidUnsignedOverflow$fSemigroupUnsignedOverflow$fMonoidSignedOverflow$fSemigroupSignedOverflow$fMonadOverflow$fApplicativeOverflow$fFunctorOverflow$fTraversableOverflow$fFoldableOverflow$fShowOverflow $fEqOverflow$fShowSignedOverflow$fEqSignedOverflow$fShowUnsignedOverflow$fEqUnsignedOverflowSignedBVasBV mkSignedBV$fRandomSignedBV$fUniformRangeSignedBV$fUniformSignedBV$fBoundedSignedBV $fIxSignedBV$fEnumSignedBV $fNumSignedBV$fFiniteBitsSignedBV$fBitsSignedBV $fOrdSignedBV$fGenericSignedBV$fShowSignedBV$fReadSignedBV $fEqSignedBV UnsignedBV mkUnsignedBV$fRandomUnsignedBV$fUniformRangeUnsignedBV$fUniformUnsignedBV$fBoundedUnsignedBV$fIxUnsignedBV$fEnumUnsignedBV$fNumUnsignedBV$fFiniteBitsUnsignedBV$fBitsUnsignedBV$fGenericUnsignedBV$fShowUnsignedBV$fReadUnsignedBV$fEqUnsignedBV$fOrdUnsignedBVpanicinteger-wired-inGHC.Integer.TypeIntegerbase GHC.NaturalNatural checkNatReprghc-prim GHC.TypesInt checkNatural fromNaturalmkBV' checkUnsigned GHC.MaybeNothingsignedToUnsignedBoolGHC.WordWord8Word16Word32Word64GHC.IntInt8Int16Int32Int64bytestringToIntegerBE shiftAmountFalse#random-1.2.0-7h4RyWOayRNDypmvRo2ybfSystem.Random.Internal uniformRM$fOrdBVintegerToBytesBEintegerToBytesLEbytestringToIntegerLEppWidthTrue