úÎjòf˜D      !"#$%&'()*+,-./0123456789:;<=>?@ABC:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-0FSTV0L'+BitVector datatype, parameterized by width.jConstruct a bit vector with a particular width, where the width is inferrable from the type context. The DÂ 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 40xa:type itit :: BitVector 4@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.  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).Bitwise division (signed).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 .ySlice out a smaller bit vector from a larger one. The lowest significant bit is given explicitly as an argument of type EE, 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 F 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 F 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 F 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.G*Mask for a specified number of lower bits.H-Truncate to a specified number of lower bits.&  !"#$%&  !"#$%6:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-0;=FQSTVf% 5@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 5 , use the 9 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 5Z to achieve a bidirectional mapping like the one described above, you can either use the I 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)0xfe1662 type, parameterized by chunk width. The internal ET 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 6 s comprise a 5 ; see below.8 Construct a 6= in a context where the chunk width is known at compile time.9Construct an empty 5.:Add a 6 to a 5 . If the 6- does not fit, either because the resulting 56 would be too long or because it would overlap with a 6 that is already in the 5, we throw an error.J7Given a starting position, insert (via "or") a smaller  s with a larger  t at that position.KGiven a list of 6#s, inject each chunk from a source  s into a target  t.;Use a 5. to inject a smaller vector into a larger one.<Use a 5/ 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 injectedLwidth of output&where to place the chunk in the result$location/width of chunk in the input input vectorM!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 56789:;<= 67859:;<=5N67:6O      !"#$%&'()*+,-./01234567899:;<=>?@ABCDEFGHIJKLMNOPQRSTUVW8X%bv-sized-0.2.1-4AhgGHqQZ0y5gD0S6hk6DJData.BitVector.SizedData.BitVector.Sized.BitLayout BitVectorBV bitVector bvIntegerU bvIntegerSbvAndbvOrbvXor bvComplementbvShiftbvShiftL bvShiftRA bvShiftRLbvRotatebvWidth bvTestBit bvPopCount bvTruncBitsbvAddbvMulbvDivUbvDivSbvAbsbvNegatebvSignumbvLTSbvLTUbvConcat<:> bvExtractbvExtractWithReprbvZextbvZextWithReprbvSextbvSextWithReprbvMulFUbvMulFSbvMulFSU$fPrettyBitVector$fRandomBitVector$fArbitraryBitVector$fBoundedBitVector$fEnumBitVector$fNumBitVector$fFiniteBitsBitVector$fBitsBitVector$fTestEqualityNatBitVector$fOrdBitVector$fEqFNatBitVector $fEqBitVector$fShowFNatBitVector$fReadBitVector$fShowBitVector BitLayoutChunkchunkempty<:injectextract layoutLens $fPrettySome $fPrettyChunk$fShowFNatChunk$fPrettyBitLayout$fShowBitLayout $fShowChunk integer-gmpGHC.Integer.TypeIntegerghc-prim GHC.TypesInt0parameterized-utils-1.0.0-L8y7pJmkvsGFirJFcel6uKData.Parameterized.NatReprNatReprlowMask truncBits"lens-4.16.1-LRyR4t2gNo5El5fD03pEDoControl.Lens.TypeLensbvOrAt bvOrAtAll extractChunk extractAll