!      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone &'-FSTV@*bv-sized+BitVector datatype, parameterized by width.bv-sizedjConstruct a bit vector with a particular width, where the width is inferrable from the type context. The  input (an unbounded data type, hence with an infinite-width bit representation), whether positive or negative, is silently truncated to fit into the number of bits demanded by the return type.bitVector 0xA :: BitVector 40xabitVector 0xA :: BitVector 20x2bv-sized The zero bitvector with width 0.bv-sized@Unsigned interpretation of a bit vector as a (positive) Integer.bv-sized4Signed interpretation of a bit vector as an Integer.bv-sized Bitwise and.bv-sized Bitwise or.bv-sized Bitwise xor. bv-sized$Bitwise complement (flip every bit). bv-sized.Bitwise shift. Uses an arithmetic right shift. bv-sized Left shift. bv-sizedRight arithmetic shift. bv-sizedRight logical shift.bv-sizedBitwise rotate.bv-sizedGet the width of a .bv-sized Test if a particular bit is set.bv-sizedGet the number of 1 bits in a .bv-sizedkTruncate a bit vector to a particular width given at runtime, while keeping the type-level width constant.bv-sized Bitwise add.bv-sizedBitwise multiply.bv-sized,Bitwise division (unsigned). Rounds to zero.bv-sizedBBitwise division (signed). Rounds to zero (not negative infinity).bv-sizedBBitwise remainder after division (unsigned), when rounded to zero.bv-sizedZBitwise remainder after division (signed), when rounded to zero (not negative infinity).bv-sizedBitwise absolute value.bv-sizedBitwise negation.bv-sizedGet the sign bit as a .bv-sizedSigned less than.bv-sizedUnsigned less than.bv-sizedConcatenate two bit vectors.;(0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24) 0xaabcdef0:type itit :: BitVector 32tNote that the first argument gets placed in the higher-order bits. The above example should be illustrative enough.bv-sizedInfix . bv-sizedConcatenate a list of  s into a 3 of arbitrary width. The ordering is little endian:8bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 160xbbaa>bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 160xbbaa&If the sum of the widths of the input @s exceeds the output width, we ignore the tail end of the list.!bv-sized  with an explicit ."bv-sizedySlice out a smaller bit vector from a larger one. The lowest significant bit is given explicitly as an argument of type E, and the length of the slice is inferred from a type-level context.8bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 80xcd Note that "} does not do any bounds checking whatsoever; if you try and extract bits that aren't present in the input, you will get 0's.#bv-sizedUnconstrained variant of " with an explicit  argument.$bv-sizedZero-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.%bv-sizedUnconstrained variant of $ with an explicit  argument.&bv-sizedSign-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.'bv-sizedUnconstrained variant of & with an explicit  argument.(bv-sizedGiven a  of arbitrary length, decompose it into a list of bytes. Uses an unsigned interpretation of the input vector, so if you ask for more bytes that the  contains, you get zeros. The result is little-endian, so the first element of the list will be the least significant byte of the input vector.bv-sized*Mask for a specified number of lower bits.bv-sized-Truncate to a specified number of lower bits.)  !"#$%&'()  !"#$%&'(6(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone &',-0FQSTV]:bv-sized Represents the application of a * operation to one or more subexpressions.Rbv-sizedTypeclass for embedding :+ constructors into larger expression types.Tbv-sized Evaluate a :@ given a monadic evaluation function for the parameterized type expr.Ubv-sized Evaluate a := given a pure evaluation function for the parameterized type expr.Vbv-sizedLiteral bit vector.Wbv-sized Bitwise and.Xbv-sized Bitwise or.Ybv-sized Bitwise xor.Zbv-sized Bitwise not.[bv-sizedAdd two expressions.\bv-sized.Subtract the second expression from the first.]bv-sizedSigned multiply two  BitVectorsI, doubling the width of the result to hold all arithmetic overflow bits.^bv-sizedSigned divide two  BitVectors, rounding to zero._bv-sizedUnsigned divide two  BitVectors, rounding to zero.`bv-sized'Remainder after signed division of two  BitVectors, when rounded to zero.abv-sized)Remainder after unsigned division of two  BitVectors, when rounded to zero.bbv-sized6Left logical shift the first expression by the second.cbv-sized6Left logical shift the first expression by the second.dbv-sized6Left logical shift the first expression by the second.ebv-sized%Test for equality of two expressions.fbv-sizedSigned less thangbv-sizedUnsigned less thanhbv-sizedZero-extensionibv-sized.Zero-extension with an explicit width argumentjbv-sizedSign-extensionkbv-sized.Sign-extension with an explicit width argumentlbv-sized Extract bitsmbv-sized,Extract bits with an explicit width argumentnbv-sized Concatenationobv-sizedConditional branch.Tbv-sizedexpression evaluatorbv-sized applicationUbv-sizedexpression evaluatorbv-sized application6:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmno6:;<=>?@ABCDEFGHIJKLMNOPQUTRSVWXYZ[\]_^a`bcdegfhijklmno(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&',-0;=FQSTV wbv-sized@BitLayout type, parameterized by target width and source width. t is the target width, s is the source width. s) should always be less than or equal to t.To construct a w , use the { constructor and the } operator, like so:empty :: BitLayout 32 0BitLayout 32 0 (fromList [])Wlet layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)layout1BitLayout 32 12 (fromList [Chunk 5 7,Chunk 7 25]):type itit :: BitLayout 32 12In the above example  bitLayout defines a chunk-by-chunk mapping from a bit vector of width 12 to one of width 32. We imagine the input vector of width 12 listed like so: +0bAXXXXXBCXXXD |-----||---| 7 5  Here, bits A, B, C, and DL are just labeled as such to illustrate their place after the mapping. The BitLayout 32 12 defined above as the layoutG variable would map that 12-bit vector to the following 32-bit vector:  (Bit 25) (Bit 5) | | | | v v 0bAXXXXXB0000000000000CXXXD0000000 |-----| |---| 7 5  To use a wZ to achieve a bidirectional mapping like the one described above, you can either use the  interface or the functions ~ and 9, which give an explicit setter and getter, respectively.Example use of inject/extract:Slet bl = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)3let sVec = bitVector 0b111111100001 :: BitVector 12sVec0xfe12inject bl (bitVector 0) (bitVector 0b111111100001) 0xfe000080?extract bl $ inject bl (bitVector 0) (bitVector 0b111111100001)0xfe1xbv-sizedx2 type, parameterized by chunk width. The internal T is the position of the least significant bit of the chunk, and the type-level nat w is the width of the chunk.chunk 2 :: Chunk 5 Chunk 5 2:Intuitively, the above chunk index captures the notion of  embedding a  5' (bit vector of width 5) into a larger M at index 2, preserving the order of the input bits. So an 5-bit input like 10011Y would map to some larger bit vector containing the input starting at position 2, like  000001001100. Multiple x s comprise a w ; see below.zbv-sized Construct a x= in a context where the chunk width is known at compile time.{bv-sizedConstruct an empty w.|bv-sized Construct a w with one chunk.}bv-sizedAdd a x to a w . If the x- does not fit, either because the resulting w6 would be too long or because it would overlap with a x that is already in the w, we throw an error.bv-sized7Given a starting position, insert (via "or") a smaller  s with a larger  t at that position.bv-sizedGiven a list of x#s, inject each chunk from a source  s into a target  t.~bv-sizedUse a w. to inject a smaller vector into a larger one.bv-sizedUse a w/ to extract a smaller vector from a larger one.bv-sized Lens for a w.bv-sizedLens for a parameterized  of ws.}bv-sized chunk to addbv-sized!layout we are adding the chunk to~bv-sized The layoutbv-sized The larger vector to inject intobv-sized!The smaller vector to be injectedbv-sizedwidth of outputbv-sized&where to place the chunk in the resultbv-sized$location/width of chunk in the inputbv-sized input vectorbv-sized!determines width of output vectorbv-sized!current position in output vectorbv-sized2list of remaining chunks to place in output vectorbv-sized input vectorbv-sized The layoutbv-sized!The larger vector to extract from wxyz{|}~ xyzw{|}~}6      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{||}~%bv-sized-0.5.0-EHELiWGQk9B6Vt64ItMfteData.BitVector.SizedData.BitVector.Sized.AppData.BitVector.Sized.BitLayout BitVectorBV bitVectorbv0 bvIntegerU bvIntegerSbvAndbvOrbvXor bvComplementbvShiftbvShiftL bvShiftRA bvShiftRLbvRotatebvWidth bvTestBit bvPopCount bvTruncBitsbvAddbvMulbvQuotUbvQuotSbvRemUbvRemSbvAbsbvNegatebvSignumbvLTSbvLTUbvConcat<:> bvConcatManybvConcatManyWithRepr bvExtractbvExtractWithReprbvZextbvZextWithReprbvSextbvSextWithRepr bvGetBytesU$fPrettyBitVector$fRandomBitVector$fArbitraryBitVector$fBoundedBitVector $fIxBitVector$fEnumBitVector$fNumBitVector$fFiniteBitsBitVector$fBitsBitVector$fTestEqualityNatBitVector$fOrdFNatBitVector$fOrdBitVector$fEqFNatBitVector $fEqBitVector$fShowFNatBitVector$fReadBitVector$fShowBitVectorBVAppLitBVAppAndAppOrAppXorAppNotAppSllAppSrlAppSraAppAddAppSubAppMulAppQuotUAppQuotSAppRemUAppRemSAppEqAppLtuAppLtsAppZExtAppSExtApp ExtractApp ConcatAppIteAppBVExprappExpr evalBVAppM evalBVApplitBVandEorExorEnotEaddEsubEmulEquotsEquotuEremsEremuEsllEsrlEsraEeqEltsEltuEzextE zextEWithReprsextE sextEWithReprextractEextractEWithReprconcatEiteE$fTraversableFCNatNatBVApp$fFoldableFCNatNatBVApp$fFunctorFCNatNatBVApp $fOrdBVApp$fOrdFNatBVApp $fEqBVApp$fTestEqualityNatBVApp BitLayoutChunkchunkempty singleChunk<:injectextract layoutLens layoutsLens $fPrettySome $fPrettyChunk$fShowFNatChunk$fPrettyBitLayout$fShowBitLayout $fShowChunk integer-gmpGHC.Integer.TypeInteger0parameterized-utils-1.0.1-LAKCPbSrVFZ7Jw9vBHR1hHData.Parameterized.NatReprNatReprghc-prim GHC.TypesIntlowMask truncBits lens-4.17-1uwTjOdtpkC2Pn6pgio8H2Control.Lens.TypeLensbvOrAt bvOrAtAllData.Parameterized.ListList extractChunk extractAll