5g      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdef:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-FSTV@-+BitVector datatype, parameterized by width.jConstruct a bit vector with a particular width, where the width is inferrable from the type context. The g 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 20x2 The zero bitvector with width 0.@Unsigned interpretation of a bit vector as a (positive) Integer.4Signed interpretation of a bit vector as an Integer. Bitwise and. Bitwise or. Bitwise xor. $Bitwise complement (flip every bit). .Bitwise shift. Uses an arithmetic right shift.  Left shift. Right arithmetic shift. Right logical shift.Bitwise rotate.Get the width of a . Test if a particular bit is set.Get the number of 1 bits in a .kTruncate a bit vector to a particular width given at runtime, while keeping the type-level width constant. Bitwise add.Bitwise multiply.,Bitwise division (unsigned). Rounds to zero.BBitwise division (signed). Rounds to zero (not negative infinity).BBitwise remainder after division (unsigned), when rounded to zero.ZBitwise remainder after division (signed), when rounded to zero (not negative infinity).Bitwise absolute value.Bitwise negation.Get the sign bit as a .Signed less than.Unsigned less than.Concatenate 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.Infix . Concatenate 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.!  with an explicit h."ySlice out a smaller bit vector from a larger one. The lowest significant bit is given explicitly as an argument of type iE, 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.#Unconstrained variant of " with an explicit h argument.$Zero-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.%Unconstrained variant of $ with an explicit h argument.&Sign-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.'Unconstrained variant of & with an explicit h argument.(|Fully multiply two bit vectors as unsigned integers, returning a bit vector whose length is equal to the sum of the inputs.)zFully multiply two bit vectors as signed integers, returning a bit vector whose length is equal to the sum of the inputs.*Fully multiply two bit vectors, treating the first as a signed integer and the second as an unsigned integer, returning a bit vector whose length is equal to the sum of the inputs.+Given 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.j*Mask for a specified number of lower bits.k-Truncate to a specified number of lower bits.,  !"#$%&'()*+,  !"#$%&'()*+6:(c) Benjamin Selfridge, 2018 Galois Inc. None (yet)benselfridge@galois.com experimentalportableNone &'-FQSTVI< Represents the application of a * operation to one or more subexpressions.V Evaluate a <@ given a monadic evaluation function for the parameterized type expr.W Evaluate a <= given a pure evaluation function for the parameterized type expr.Vexpression evaluator applicationWexpression evaluator application<=>?@ABCDEFGHIJKLMNOPQRSTUVW<=>?@ABCDEFGHIJKLMNOPQRSTUWV<=>?@ABCDEFGHIJKLMNOPQRSTU:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-0;=FQSTV~ X@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 X , 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 XZ to achieve a bidirectional mapping like the one described above, you can either use the l 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)0xfe1YY2 type, parameterized by chunk width. The internal iT 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 Y s comprise a X ; see below.[ Construct a Y= in a context where the chunk width is known at compile time.\Construct an empty X.]Add a Y to a X . If the Y- does not fit, either because the resulting X6 would be too long or because it would overlap with a Y that is already in the X, we throw an error.m7Given a starting position, insert (via "or") a smaller  s with a larger  t at that position.nGiven a list of Y#s, inject each chunk from a source  s into a target  t.^Use a X. to inject a smaller vector into a larger one._Use a X/ to extract a smaller vector from a larger one.`Lens for bit layout.] chunk to add!layout we are adding the chunk to^ The layout The larger vector to inject into!The smaller vector to be injectedowidth of output&where to place the chunk in the result$location/width of chunk in the input input vectorp!determines width of output vector!current position in output vector2list of remaining chunks to place in output vector input vector_ The layout!The larger vector to extract from XYZ[\]^_` YZ[X\]^_`XqYZ]6r      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]]^_`abcdefghijklmnopqrstuvwxyz{\|%bv-sized-0.4.0-5COy1YVpdFVDP9dx7Umgk5Data.BitVector.SizedData.BitVector.Sized.AppData.BitVector.Sized.BitLayout BitVectorBV bitVectorbv0 bvIntegerU bvIntegerSbvAndbvOrbvXor bvComplementbvShiftbvShiftL bvShiftRA bvShiftRLbvRotatebvWidth bvTestBit bvPopCount bvTruncBitsbvAddbvMulbvQuotUbvQuotSbvRemUbvRemSbvAbsbvNegatebvSignumbvLTSbvLTUbvConcat<:> bvConcatManybvConcatManyWithRepr bvExtractbvExtractWithReprbvZextbvZextWithReprbvSextbvSextWithReprbvMulFUbvMulFSbvMulFSU bvGetBytesU$fPrettyBitVector$fRandomBitVector$fArbitraryBitVector$fBoundedBitVector $fIxBitVector$fEnumBitVector$fNumBitVector$fFiniteBitsBitVector$fBitsBitVector$fTestEqualityNatBitVector$fOrdBitVector$fEqFNatBitVector $fEqBitVector$fShowFNatBitVector$fReadBitVector$fShowBitVectorBVAppLitBVAppAndAppOrAppXorAppNotAppSllAppSrlAppSraAppAddAppSubAppMulSAppMulUAppMulSUAppDivUAppDivSAppRemUAppRemSAppEqAppLtuAppLtsAppZExtAppSExtApp ExtractApp ConcatAppIteApp evalBVAppM evalBVApp BitLayoutChunkchunkempty<:injectextract layoutLens $fPrettySome $fPrettyChunk$fShowFNatChunk$fPrettyBitLayout$fShowBitLayout $fShowChunk integer-gmpGHC.Integer.TypeInteger0parameterized-utils-1.0.0-KGmNpUmRrkkKegwHQkEHjSData.Parameterized.NatReprNatReprghc-prim GHC.TypesIntlowMask truncBits"lens-4.16.1-6AeprMDSnGTJeDPO2acAFbControl.Lens.TypeLensbvOrAt bvOrAtAll extractChunk extractAll