Incorrect documentation for little-endian functions in What4.SWord

[RyanGlScott]

The What4.SWord module has various functions that work over bit-endian and little-endian functions, suffixed with -BE and -LE, respectively. However, the litte-endian variants of each function have various inaccuracies in their documentation. Here are the ones that I have found:

• what4/what4/src/What4/SWord.hs

  Lines 251 to 262 in 1748341

  	-- | Returns true if the corresponding bit in the bitvector is set.
  	-- NOTE bits are numbered in little-endian ordering, meaning the
  	-- least-significant bit is bit 0
  	bvAtLE :: forall sym.
  	IsExprBuilder sym =>
  	sym ->
  	SWord sym ->
  	Integer {- ^ Index of bit (0 is the most significant bit) -} ->
  	IO (Pred sym)
  	bvAtLE sym (DBV bv) i =
  	W.testBitBV sym (fromInteger i) bv
  	bvAtLE _ ZBV _ = panic "bvAtLE" ["cannot index into empty bitvector"]

  This says Index of bit (0 is the most significant bit), but I believe that should be least significant bit.

• what4/what4/src/What4/SWord.hs

  Lines 281 to 294 in 1748341

  	-- | Set the numbered bit in the given bitvector to the given
  	-- bit value.
  	-- NOTE bits are numbered in big-endian ordering, meaning the
  	-- most-significant bit is bit 0
  	bvSetLE :: forall sym.
  	IsExprBuilder sym =>
  	sym ->
  	SWord sym ->
  	Integer {- ^ Index of bit (0 is the most significant bit) -} ->
  	Pred sym ->
  	IO (SWord sym)
  	bvSetLE _ ZBV _ _ = return ZBV
  	bvSetLE sym (DBV bv) i b =
  	DBV <$> W.bvSet sym bv (fromInteger i) b

  This says Index of bit (0 is the most significant bit), but I believe that should be least significant bit. This also says NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0, but I believe that should be NOTE bits are numbered in little-endian ordering, meaning the least-significant bit is bit 0.

• what4/what4/src/What4/SWord.hs

  Lines 340 to 357 in 1748341

  	-- | Select a subsequence from a bitvector, with bits
  	-- numbered in Little Endian order (least significant bit is 0).
  	-- This fails if idx + n is >= w
  	bvSliceLE :: forall sym. IsExprBuilder sym => sym
  	-> Integer
  	-- ^ Starting index, from 0 as most significant bit
  	-> Integer
  	-- ^ Number of bits to take
  	-> SWord sym
  	-> IO (SWord sym)
  	bvSliceLE _ _m 0 _ = return ZBV
  	bvSliceLE sym m n (DBV bv)
  	| Just (Some nr) <- someNat n,
  	Just LeqProof <- isPosNat nr,
  	Just (Some mr) <- someNat m,
  	let wr = W.bvWidth bv,
  	Just LeqProof <- testLeq (addNat mr nr) wr
  	= DBV <$> W.bvSelect sym mr nr bv

  This says Starting index, from 0 as most significant bit, but I believe that should be Starting index, from 0 as least significant bit.