!è      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~None(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&'.7:HUVX`gkʎobv-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.ySecondly, 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-sizedjInternal function for masking the input integer *without* checking that the width is representable as an . We use this instead of B whenever we already have some guarantee that the width is legal.bv-sized[Construct 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 J 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 k 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-sizedEThe minimum unsigned value for bitvector with given width (always 0).bv-sized:The maximum unsigned value for bitvector with given width.bv-sizedEThe minimum value for bitvector in two's complement with given width. bv-sizedEThe 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.Dcase bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) (24,BV 257)bv-sized Construct a ! from a little-endian bytestring.Dcase 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.-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.0bv-sizedThe : that has a particular bit set, and is 0 everywhere else.1bv-sizedLike 0X, but without the requirement that the index bit refers to an actual bit in the output B. 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 2W, but without the requirement that the index bit refers to an actual bit in the input B. 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 4W, but without the requirement that the index bit refers to an actual bit in the input B. 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 6W, but without the requirement that the index bit refers to an actual bit in the input B. 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-sizedjTruncate 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-sizedXBitvector division (unsigned). Rounds to zero. Division by zero yields a runtime error.Bbv-sizednBitvector remainder after division (unsigned), when rounded to zero. Division by zero yields a runtime error.Cbv-sizedA and B returned as a pair.Dbv-sizedVBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.Ebv-sizedlBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.Fbv-sizedD and E returned as a pair.Gbv-sizedcBitvector division (signed). Rounds to negative infinity. Division by zero yields a runtime error.Hbv-sizedyBitvector 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-sizedTBitvector 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-sizedUConcatenate two bitvectors. The first argument gets placed in the higher order bits.Dconcat 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.Gselect (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)BV 3:type it it :: BV 4Xbv-sizedLike W, but takes a s 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.<select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)BV 6:type it it :: BV 4Ybv-sized9Zero-extend a bitvector to one of strictly greater width..zext (knownNat @8) (mkBV (knownNat @4) 0b1101)BV 13:type it it :: BV 8Zbv-sized9Sign-extend a bitvector to one of strictly greater width.[bv-sized6Truncate a bitvector to one of strictly smaller width.\bv-sizedLike [, but allows the input width to be greater than or equal to the output width, in which case it just performs a zero extension.]bv-sized Wide multiply of two bitvectors.^bv-sizedUnsigned successor. succUnsigned w (maxUnsigned w) returns ._bv-sizedSigned successor. succSigned w (maxSigned w) returns .`bv-sizedUnsigned predecessor. predUnsigned w zero returns .abv-sizedSigned predecessor. predSigned w (minSigned w) returns .bbv-sizedKList of all unsigned bitvectors from a lower to an upper bound, inclusive.cbv-sizedIList of all signed bitvectors from a lower to an upper bound, inclusive.dbv-sizedPretty print in hexebv-sizedPretty print in binaryfbv-sizedPretty print in octalgbv-sizedPretty print in decimalbv-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 bounds  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefg(c) Galois Inc. 2020BSD-3'Ben Selfridge <benselfridge@galois.com> experimentalportableNone&'.UVqhbv-sized,A value annotated with overflow information.jbv-sized9Datatype representing the possibility of signed overflow.mbv-sized;Datatype representing the possibility of unsigned overflow.pbv-sizedReturn + if a computation caused unsigned overflow.qbv-sizedReturn ) if a computation caused signed overflow.rbv-sized#Return the result of a computation.bv-sizedcThis only works if the operation has equivalent signed and unsigned interpretations on bitvectors.sbv-sizedBitvector add.tbv-sizedBitvector subtract.ubv-sizedBitvector multiply.vbv-sizedLeft shift by positive .wbv-sizedVBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.xbv-sizedlBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.ybv-sizedVBitvector division (signed). Rounds to zero. Division by zero yields a runtime error.zbv-sizedlBitvector remainder after division (signed), when rounded to zero. Division by zero yields a runtime error.bv-sizedPMonad for bitvector operations which might produce signed or unsigned overflow.hijklmnopqrstuvwxyzhimnojklpqrvstuwxyz(c) Galois Inc. 2018BSD-3'Ben Selfridge <benselfridge@galois.com> experimentalportableNone &'.HUVXgbv-sizedGet the underlying  representation from a . We guarantee that "(\(BV.BV x) -> x) == BV.toUnsigned.i  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefgi   !"#$%&'(*)+,-./0123456789:;<=>?@ADGBEHCFIJKLMNOPQRSTUVWXYZ[\]^_`abcdefg(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&'.7HUVX`gkbv-sizedSigned bit vector.bv-sizedConvenience wrapper for .(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&'.7HUVXgkbv-sizedSigned bit vector.bv-sizedConvenience wrapper for .      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqqrrsttuvwxyz{|}~  %bv-sized-1.0.0-7ojTcINbUEOBofHAbwvbSSData.BitVector.SizedData.BitVector.Sized.OverflowData.BitVector.Sized.SignedData.BitVector.Sized.UnsignedData.BitVector.Sized.PanicData.BitVector.Sized.Internal0parameterized-utils-2.0.2-Dcnlx9tmQvCDLBGSE0g8xz#Data.Parameterized.NatRepr.InternalknownNatNatReprBVmkBV mkBVUnsigned mkBVSigned minUnsigned maxUnsigned minSigned maxSigned unsignedClamp signedClampboolword8word16word32word64int8int16int32int64bitsBEbitsLE bytestringBE bytestringLEbytesBEbytesLE asUnsignedasSigned asNaturalasBitsBEasBitsLE asBytesBE asBytesLEasBytestringBEasBytestringLEandorxor complementshlashrlshrrotateLrotateRzeroonewidthbitbit'setBitsetBit'clearBit clearBit' complementBitcomplementBit'testBittestBit'popCountctzclz truncBitsaddsubmuluquoturemuquotRemsquotsremsquotRemsdivsmodsdivModabsnegatesignBitsignumsltsleultuleuminumaxsminsmaxconcatselectselect'zextsexttrunctrunc'mulWide succUnsigned succSigned predUnsigned predSignedenumFromToUnsignedenumFromToSignedppHexppBinppOctppDecOverflowSignedOverflowNoSignedOverflowUnsignedOverflowNoUnsignedOverflow ofUnsignedofSignedofResultaddOfsubOfmulOfshlOfsquotOfsremOfsdivOfsmodOf$fMonoidUnsignedOverflow$fSemigroupUnsignedOverflow$fMonoidSignedOverflow$fSemigroupSignedOverflow$fMonadOverflow$fApplicativeOverflow$fFunctorOverflow$fTraversableOverflow$fFoldableOverflow$fShowUnsignedOverflow$fEqUnsignedOverflow$fShowSignedOverflow$fEqSignedOverflow$fShowOverflow $fEqOverflowSignedBV mkSignedBV$fBoundedSignedBV $fIxSignedBV$fEnumSignedBV $fNumSignedBV$fFiniteBitsSignedBV$fBitsSignedBV $fOrdSignedBV$fGenericSignedBV$fShowSignedBV$fReadSignedBV $fEqSignedBV UnsignedBVasBV mkUnsignedBV$fBoundedUnsignedBV$fIxUnsignedBV$fEnumUnsignedBV$fNumUnsignedBV$fFiniteBitsUnsignedBV$fBitsUnsignedBV$fGenericUnsignedBV$fShowUnsignedBV$fReadUnsignedBV$fEqUnsignedBV$fOrdUnsignedBVpanic integer-gmpGHC.Integer.TypeIntegerbase GHC.NaturalNatural checkNatReprghc-prim GHC.TypesInt checkNatural fromNaturalmkBV' checkUnsigned GHC.MaybeNothingsignedToUnsignedBoolGHC.WordWord8Word16Word32Word64GHC.IntInt8Int16Int32Int64bytestringToIntegerBE shiftAmountFalseintegerToBytesBEintegerToBytesLEbytestringToIntegerLEppWidthTrue liftBinary