!<b      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone &'.HUVXgC,bv-sized+BitVector datatype, parameterized by width.bv-sizedl can be treated as a constructor for pattern matching, but to build one you must use the smart constructor .bv-sized,Construct 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-sizedLike , but with an explict .bv-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.0  !"#$%&'() 6(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&'-.1=?HSUVXz *bv-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 * , use the . constructor and the 0 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 *Z to achieve a bidirectional mapping like the one described above, you can either use the  interface or the functions 1 and 29, 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)0xfe1+bv-sized+2 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 + s comprise a * ; see below.-bv-sized Construct a += in a context where the chunk width is known at compile time..bv-sizedConstruct an empty *./bv-sized Construct a * with one chunk.0bv-sizedAdd a + to a * . If the +- does not fit, either because the resulting *6 would be too long or because it would overlap with a + that is already in the *, 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 +#s, inject each chunk from a source  s into a target  t.1bv-sizedUse a *. to inject a smaller vector into a larger one.2bv-sizedUse a */ to extract a smaller vector from a larger one.3bv-sized Lens for a *.4bv-sizedLens for a parameterized  of *s.5bv-sizedFrom a *[, get a list representing the position of each bit from the source to the target. The list [3,4,5,10,11,12,13] |means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the source is placed in bit 4 of the target, etc.0bv-sized chunk to addbv-sized!layout we are adding the chunk to1bv-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 vector2bv-sized The layoutbv-sized!The larger vector to extract from *+,-./012345 +,-*./01234506(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone &'.HUVXg*  !"#$%&'()*  !"#$%&'()(c) Galois Inc. 2018BSD-3benselfridge@galois.com experimentalportableNone&'-.1=?HSUVXv<bv-sized Represents the application of a * operation to one or more subexpressions.Wbv-sizedTypeclass for embedding <+ constructors into larger expression types.[bv-sized Evaluate a <@ given a monadic evaluation function for the parameterized type expr.\bv-sized Evaluate a <= given a pure evaluation function for the parameterized type expr.]bv-sized Bitwise and.^bv-sized Bitwise or._bv-sized Bitwise xor.`bv-sized Bitwise not.abv-sizedAdd two expressions.bbv-sized.Subtract the second expression from the first.cbv-sizedSigned multiply two Js, doubling the width of the result to hold all arithmetic overflow bits.dbv-sizedSigned divide two s, rounding to zero.ebv-sizedUnsigned divide two s, rounding to zero.fbv-sized'Remainder after signed division of two s, when rounded to zero.gbv-sized)Remainder after unsigned division of two s, when rounded to zero.kbv-sized6Left logical shift the first expression by the second.lbv-sized6Left logical shift the first expression by the second.mbv-sized6Left logical shift the first expression by the second.nbv-sized%Test for equality of two expressions.obv-sizedSigned less thanpbv-sizedUnsigned less thanqbv-sizedZero-extensionrbv-sized.Zero-extension with an explicit width argumentsbv-sizedSign-extensiontbv-sized.Sign-extension with an explicit width argumentubv-sized Extract bitsvbv-sized,Extract bits with an explicit width argumentwbv-sized Concatenationxbv-sizedConditional branch.[bv-sizedexpression evaluatorbv-sized application\bv-sizedexpression evaluatorbv-sized application=<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwx=<=>?@ABCDEFGHIJKLMNOPQRSTU\[VWXYZ]^_`abcedgfhijklmnpoqrstuvwx      !"#$%&'()*+,-.//0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~%bv-sized-0.7.0-Av6IFiqKvQ2HyhrWYOA8CHData.BitVector.SizedData.BitVector.Sized.BitLayoutData.BitVector.Sized.AppData.BitVector.Sized.Internal BitVector bitVector bitVector'bv0 bvIntegerU bvIntegerSbvAndbvOrbvXor bvComplementbvShiftbvShiftL bvShiftRA bvShiftRLbvRotatebvWidth bvTestBit bvPopCount bvTruncBitsbvAddbvMulbvQuotUbvQuotSbvRemUbvRemSbvAbsbvNegatebvSignumbvLTSbvLTUbvConcat<:> bvConcatMany bvConcatMany' bvExtract bvExtract'bvZextbvZext'bvSextbvSext' bvGetBytesU BitLayoutChunkchunkempty singleChunk<:injectextract layoutLens layoutsLensbitLayoutAssignmentList $fPrettySome $fPrettyChunk$fShowFNatChunk$fPrettyBitLayout$fShowBitLayout $fShowChunkBVAppAndAppOrAppXorAppNotAppSllAppSrlAppSraAppAddAppSubAppMulAppQuotUAppQuotSAppRemUAppRemSApp NegateAppAbsApp SignumAppEqAppLtuAppLtsAppZExtAppSExtApp ExtractApp ConcatAppIteApp bvAppWidthBVExprlitBV exprWidthappExpr evalBVAppM evalBVAppandEorExorEnotEaddEsubEmulEquotsEquotuEremsEremuEnegateEabsEsignumEsllEsrlEsraEeqEltsEltuEzextEzextE'sextEsextE'extractE extractE'concatEiteE$fTraversableFCNatNatBVApp$fFoldableFCNatNatBVApp$fFunctorFCNatNatBVApp $fOrdBVApp$fOrdFNatBVApp $fEqFNatBVApp $fEqBVApp$fTestEqualityNatBVApp.parameterized-utils-2.0-5EcWvL4VBZEIQmbRZzaRMZ#Data.Parameterized.NatRepr.InternalNatReprghc-prim GHC.TypesIntlowMask truncBitsBVtoPos bvConcatSome prettyHex lens-4.17-5R1nkIDzovdC6jcuCd3LNEControl.Lens.TypeLensbvOrAt bvOrAtAllData.Parameterized.ListList extractChunk extractAll