úÎg?cG<      !"#$%&'()*+,-./0123456789:;:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-FSTV.%+BitVector datatype, parameterized by width.^Construct a bit vector in a context 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 40xa<4>0xA :: BitVector 40xA :: BitVector 30x2<3>(-1) :: BitVector 80xff<8>(-1) :: BitVector 320xffffffff<32>@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 absolute value.Bitwise negation.Get the sign bit as a .Signed less than.Unsigned less than.Concatenate two bit vectors.9(0xAA :: BitVector 8 `bvConcat` 0xBCDEF0 :: BitVector 24)0xaabcdef0<32>: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 =E, and the length of the slice is inferred from a type-level context.8bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 80xcd<8> 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 > 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 > 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 > 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.?2Print an integral value in hex with a leading "0x"@*Mask for a specified number of lower bits.A-Truncate to a specified number of lower bits.#  !"#  !"6:(c) Benjamin Selfridge, 2018 Galois Inc.BSD3benselfridge@galois.com experimentalportableNone &'-FQSTVbÔ 0@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 0 , use the 4 constructor and the 5 operator, like so:empty :: BitLayout 32 0[]Wlet layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)layout[[25...31],[7...11]]: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 0Z to achieve a bidirectional mapping like the one described above, you can either use the B interface or the functions 6 and 79, 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)bl[[25...31],[7...11]],let sVec = bv 0b111111100001 :: BitVector 12sVec 0xfe1<12>$inject bl (bv 0) (bv 0b111111100001)0xfe000080<32>1extract bl $ inject bl (bv 0) (bv 0b111111100001) 0xfe1<12>112 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[2...6]: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 1 s comprise a 0 ; see below.3 Construct a 1= in a context where the chunk width is known at compile time.4Construct an empty 0.5Add a 1 to a 0 . If the 1- does not fit, either because the resulting 06 would be too long or because it would overlap with a 1 that is already in the 0, we throw an error.C7Given a starting position, insert (via "or") a smaller  s with a larger  t at that position.DGiven a list of 1#s, inject each chunk from a source  s into a target  t.6Use a 0. to inject a smaller vector into a larger one.7Use a 0/ to extract a smaller vector from a larger one.8Lens for bit layout.5 chunk to add!layout we are adding the chunk to6 The layout The larger vector to inject into!The smaller vector to be injectedEwidth of output&where to place the chunk in the result$location/width of chunk in the input input vectorF!determines width of output vector!current position in output vector2list of remaining chunks to place in output vector input vector7 The layout!The larger vector to extract from 012345678 1230456780G1256H      !"#$%&'()*+,-./01234456789:;<=>?@ABCDEFGHIJKLMNOP3Q%bv-sized-0.2.0-B3h3zsVURguJ8ftIOwUdAWData.BitVector.SizedData.BitVector.Sized.BitLayout BitVectorBV bitVector bvIntegerU bvIntegerSbvAndbvOrbvXor bvComplementbvShiftbvShiftL bvShiftRA bvShiftRLbvRotatebvWidth bvTestBit bvPopCount bvTruncBitsbvAddbvMulbvAbsbvNegatebvSignumbvLTSbvLTUbvConcat<:> bvExtractbvExtractWithReprbvZextbvZextWithReprbvSextbvSextWithReprbvMulFUbvMulFS$fRandomBitVector$fArbitraryBitVector$fBoundedBitVector$fEnumBitVector$fNumBitVector$fFiniteBitsBitVector$fBitsBitVector$fTestEqualityNatBitVector$fOrdBitVector$fEqFNatBitVector $fEqBitVector$fShowFNatBitVector$fShowBitVector BitLayoutChunkchunkempty<:injectextract layoutLens$fShowFNatChunk $fShowChunk$fShowBitLayout integer-gmpGHC.Integer.TypeIntegerghc-prim GHC.TypesInt0parameterized-utils-1.0.0-6xQHiGdOsKbJaCMZWBscMVData.Parameterized.NatReprNatRepr prettyHexlowMask truncBits lens-4.16-92u59vXo1mk8zm2scb776HControl.Lens.TypeLensbvOrAt bvOrAtAll extractChunk extractAll