content: 
  Case Study: Pointers & Bytes {#case-study-pointers}
  ===================================================
  
  \begin{comment}
  \begin{code}
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names"    @-}
  {-@ LIQUID "--prune"          @-}
  
  {-# LANGUAGE ForeignFunctionInterface #-}
  
  module Tutorial_11_Case_Study_Pointers where
  
  import Prelude hiding (null)
  
  import Data.Word
  import Foreign.C.Types
  import Foreign.ForeignPtr
  import Foreign.Ptr
  import Foreign.Storable
  import System.IO.Unsafe
  import Data.ByteString.Internal (c2w, w2c)
  -- import Language.Haskell.Liquid.Prelude
  
  spanByte         :: Word8 -> ByteString -> (ByteString, ByteString)
  unsafeHead       :: ByteString -> Word8
  create, create'  :: Int -> (Ptr Word8 -> IO ()) -> ByteString
  
  -- boilerplate
  {-@ type TRUE = {v:Bool | v } @-}
  
  -- TODO: we really shouldn't need this...
  -- {- bLen :: b:ByteString -> {v:Nat | v = bLen b} @-}
  
  {-@ type StringN N = {v:String | len v = N} @-}
  {-@ type BNat N    = {v:Nat    | v <= N}    @-}
  
  {- ignore spanByte @-}
  -- {-@ ignore chop' @-}
  -- {-@ fail zero4' @-}
  -- {-@ fail exBad @-}
  -- {-@ fail bad1 @-}
  -- {-@ fail bad2 @-}
  -- {-@ fail bsGHC @-}
  -- {-@ fail prop_pack_length @-}
  -- {-@ fail prop_unpack_length @-}
  -- {-@ fail prop_chop_length @-}
  -- {-@ fail demo @-}
  -- {-@ ignore pLoop @-}
  -- {-@ ignore safeChop @-}
  -- {-@ ignore unsafeTake @-}
  -- {-@ ignore unsafeDrop @-}
  
  
  \end{code}
  \end{comment}
  
  A large part of the allure of Haskell is its elegant, high-level ADTs
  that ensure that programs won't be plagued by problems like the infamous
  [SSL heartbleed bug](heartbleed.com).^[Assuming, of course, the absence of errors in the compiler and run-time...]
  However, another part of Haskell's charm is that when you really really
  need to, you can drop down to low-level pointer twiddling to squeeze the
  most performance out of your machine. But of course, that opens the door
  to the heartbleeds.
  
  Wouldn't it be nice to have our cake and eat it too?
  Wouldn't it be great if we could twiddle pointers at a
  low-level and still get the nice safety assurances of
  high-level types? Lets see how LiquidHaskell lets us
  have our cake and eat it too.
  
  
  HeartBleeds in Haskell
  ----------------------
  
  \newthought{Modern Languages} like Haskell are ultimately built upon the
  foundation of `C`. Thus, implementation errors could open up unpleasant
  vulnerabilities that could easily slither past the type system and even
  code inspection. As a concrete example, let's look at a function that
  uses the `ByteString` library to truncate strings:
  
  \begin{code}
  chop'     :: String -> Int -> String
  chop' s n = s'
    where
      b     = pack s          -- down to low-level
      b'    = unsafeTake n b  -- grab n chars
      s'    = unpack b'       -- up to high-level
  \end{code}
  
  \noindent First, the function `pack`s the string into a low-level
  bytestring `b`, then it grabs the first `n` `Char`acters from `b`
  and translates them back into a high-level `String`. Lets see how
  the function works on a small test:
  
  ~~~~~{.spec}
  ghci> let ex = "Ranjit Loves Burritos"
  ~~~~~
  
  \noindent We get the right result when we `chop` a *valid* prefix:
  
  ~~~~~{.spec}
  ghci> chop' ex 10
  "Ranjit Lov"
  ~~~~~
  
  \noindent But, as illustrated in Figure [auto](#fig:overflow), the
  machine silently reveals (or more colorfully, *bleeds*) the contents
  of adjacent memory or if we use an *invalid* prefix:
  
  ~~~~~{.spec}
  ghci> chop' ex 30
  "Ranjit Loves Burritos\NUL\201\&1j\DC3\SOH\NUL"
  ~~~~~
  
  
  <div class="figure"
    id="fig:overflow"
    caption="Can we prevent the program from leaking secrets via overflows?"
    height="100px"
    file="img/overflow.png">
  </div>
  
  
  \newthought{Types against Overflows} Now that we have stared the problem
  straight in the eye, look at how we can use LiquidHaskell to prevent the
  above at compile time. To this end, we decompose the system into
  a hierarchy of levels (i.e. modules). Here, we have three levels:
  
  1. *Machine* level `Pointers`
  2. *Library* level `ByteString`
  3. *User*    level `Application`
  
  \noindent Our strategy, as before, is to develop an *refined API* for
  each level such that errors at each level are prevented by using the typed
  interfaces for the lower levels. Next, let's see how this strategy lets us
  safely manipulate pointers.
  
  Low-level Pointer API
  ---------------------
  
  To get started, let's look at the low-level pointer API that is
  offered by GHC and the run-time. First, let's see who the
  *dramatis personae* are and how they might let heartbleeds in.
  Then we will see how to batten down the hatches with LiquidHaskell.
  
  \newthought{Pointers} are an (abstract) type `Ptr a` implemented by GHC.
  
  ~~~~~{.spec}
  -- | A value of type `Ptr a` represents a pointer to an object,
  --   or an array of objects, which may be marshalled to or from
  --   Haskell values of type `a`.
  
  data Ptr a
  ~~~~~
  
  \newthought{Foreign Pointers} are *wrapped* pointers that can be
  exported to and from C code via the [Foreign Function Interface][foreignptr].
  
  ~~~~~{.spec}
  data ForeignPtr a
  ~~~~~
  
  \newthought{To Create} a pointer we use `mallocForeignPtrBytes n`
  which creates a `Ptr` to a buffer of size `n` and wraps it as a
  `ForeignPtr`
  
  ~~~~~{.spec}
  mallocForeignPtrBytes :: Int -> ForeignPtr a
  ~~~~~
  
  \newthought{To Unwrap} and actually use the `ForeignPtr` we use
  
  ~~~~~{.spec}
  withForeignPtr :: ForeignPtr a     -- pointer
                 -> (Ptr a -> IO b)  -- action
                 -> IO b             -- result
  ~~~~~
  
  \noindent That is, `withForeignPtr fp act` lets us execute a
  action `act` on the actual `Ptr` wrapped within the `fp`.
  These actions are typically sequences of *dereferences*,
  i.e. reads or writes.
  
  \newthought{To Dereference} a pointer, i.e. to read or update
  the contents at the corresponding memory location, we use
  `peek` and `poke` respectively. ^[We elide the `Storable`
  type class constraint to strip this presentation down to
  the absolute essentials.]
  
  ~~~~~{.spec}
  peek :: Ptr a -> IO a         -- Read
  poke :: Ptr a -> a -> IO ()   -- Write
  ~~~~~
  
  \newthought{For Fine Grained Access} we can directly shift
  pointers to arbitrary offsets using the *pointer arithmetic*
  operation `plusPtr p off` which takes a pointer `p` an integer
  `off` and returns the address obtained shifting `p` by `off`:
  
  ~~~~~{.spec}
  plusPtr :: Ptr a -> Int -> Ptr b
  ~~~~~
  
  \newthought{Example} That was rather dry; let's look at a concrete
  example of how one might use the low-level API. The following
  function allocates a block of 4 bytes and fills it with zeros:
  
  \begin{code}
  zero4 = do fp <- mallocForeignPtrBytes 4
             withForeignPtr fp $ \p -> do
               poke (p `plusPtr` 0) zero
               poke (p `plusPtr` 1) zero
               poke (p `plusPtr` 2) zero
               poke (p `plusPtr` 3) zero
             return fp
          where
             zero = 0 :: Word8
  \end{code}
  
  \noindent While the above is perfectly all right, a small typo could
  easily slip past the type system (and run-time!) leading to hard to find
  errors:
  
  \begin{code}
  zero4' = do fp <- mallocForeignPtrBytes 4
              withForeignPtr fp $ \p -> do
                poke (p `plusPtr` 0) zero
                poke (p `plusPtr` 1) zero
                poke (p `plusPtr` 2) zero
                poke (p `plusPtr` 8) zero
              return fp
           where
              zero = 0 :: Word8
  \end{code}
  
  A Refined Pointer API
  ---------------------
  
  Wouldn't it be great if we had an assistant to helpfully point out
  the error above as soon as we *wrote* it? ^[In Vim or Emacs or online,
  you'd see the error helpfully highlighted.] We will use the following
  strategy to turn LiquidHaskell into such an assistant:
  
  1. *Refine* pointers with allocated buffer size,
  2. *Track* sizes in pointer operations,
  3. *Enforce* pointer are valid at reads and writes.
  
  \newthought{To Refine Pointers} with the *size* of their
  associated buffers, we can use an *abstract measure*,
  i.e. a measure specification *without* any underlying
  implementation.
  
  ~~~~~{.spec}
  -- | Size of `Ptr`
  measure plen  :: Ptr a -> Int
  
  -- | Size of `ForeignPtr`
  measure fplen :: ForeignPtr a -> Int
  ~~~~~
  
  \noindent It is helpful to define aliases for pointers of a given size `N`:
  
  ~~~~~{.spec}
  type PtrN a N        = {v:Ptr a        | plen v  = N}
  type ForeignPtrN a N = {v:ForeignPtr a | fplen v = N}
  ~~~~~
  
  \newthought{Abstract Measures} are extremely useful when we don't have
  a concrete implementation of the underlying value, but we know that
  the value *exists*.   Here, we don't have the value -- inside Haskell
  -- because the buffers are manipulated within C. However, this is no
  cause for alarm as we will simply use measures to refine the API, not
  to perform any computations. ^[This is another *ghost* specification.]
  
  
  \newthought{To Refine Allocation} we stipulate that
  the size parameter be non-negative, and that the returned
  pointer indeed refers to a buffer with exactly `n` bytes:
  
  ~~~~~{.spec}
  mallocForeignPtrBytes :: n:Nat -> ForeignPtrN a n
  ~~~~~
  
  \newthought{To Refine Unwrapping} we specify that the *action*
  gets as input, an unwrapped `Ptr` whose size *equals* that of the
  given `ForeignPtr`.
  
  ~~~~~{.spec}
  withForeignPtr :: fp:ForeignPtr a
                 -> (PtrN a (fplen fp) -> IO b)
                 -> IO b
  ~~~~~
  
  \noindent This is a rather interesting *higher-order* specification.
  Consider a call `withForeignPtr fp act`. If the `act` requires a `Ptr`
  whose size *exceeds* that of `fp` then LiquidHaskell will flag a
  (subtyping) error indicating the overflow. If instead the `act`
  requires a buffer of size less than `fp` then it is always safe
  to run the `act` on a larger buffer. For example, the below
  variant of `zero4` where we only set the first three bytes
  is fine as the `act`, namely the function `\p -> ...`, can be
  typed with the requirement that the buffer `p` has size `4`,
  even though only `3` bytes are actually touched.
  
  \begin{code}
  zero3 = do fp <- mallocForeignPtrBytes 4
             withForeignPtr fp $ \p -> do
               poke (p `plusPtr` 0) zero
               poke (p `plusPtr` 1) zero
               poke (p `plusPtr` 2) zero
             return fp
          where
             zero = 0 :: Word8
  \end{code}
  
  \newthought{To Refine Reads and Writes} we specify that they can
  only be done if the pointer refers to a non-empty (remaining) buffer.
  That is, we define an alias:
  
  ~~~~~{.spec}
  type OkPtr a = {v:Ptr a | 0 < plen v}
  ~~~~~
  
  \noindent that describes pointers referring to *non-empty* buffers
  (of strictly positive `plen`), and then use the alias to refine:
  
  ~~~~~{.spec}
  peek :: OkPtr a -> IO a
  poke :: OkPtr a -> a -> IO ()
  ~~~~~
  
  \noindent In essence the above type says that no matter how arithmetic
  was used to shift pointers around, when the actual dereference happens,
  the size *remaining* after the pointer must be non-negative, so that a
  byte can be safely read from or written to the underlying buffer.
  
  \newthought{To Refine the Shift} operations, we simply check that the
  pointer *remains* within the bounds of the buffer, and update the `plen`
  to reflect the size remaining after the shift: ^[This signature precludes
  *left* or *backward* shifts; for that there is an analogous `minusPtr`
  which we elide for simplicity.]
  
  ~~~~~{.spec}
  plusPtr :: p:Ptr a -> off:BNat (plen p) -> PtrN b (plen p - off)
  ~~~~~
  
  \noindent using the alias `BNat`, defined as:
  
  ~~~~~{.spec}
  type BNat N = {v:Nat | v <= N}
  ~~~~~
  
  ^[Did you notice that we have strengthened the type of `plusPtr` to
  prevent the pointer from wandering outside the boundary of the buffer?
  We could instead use a weaker requirement for `plusPtr` that omits
  this requirement, and instead have the error be flagged when the
  pointer was used to read or write memory.]
  
  \newthought{Types Prevent Overflows} Lets revisit the zero-fill example
  from above to understand how the refinements help detect the error:
  
  \begin{code}
  exBad = do fp <- mallocForeignPtrBytes 4
             withForeignPtr fp $ \p -> do
               poke (p `plusPtr` 0) zero
               poke (p `plusPtr` 1) zero
               poke (p `plusPtr` 2) zero
               poke (p `plusPtr` 5) zero     -- LH complains
             return fp
          where
             zero = 0 :: Word8
  \end{code}
  
  \noindent Lets read the tea leaves to understand the above error:
  
  ~~~~~{.liquiderror}
    Error: Liquid Type Mismatch
     Inferred type
       VV : {VV : Int | VV == ?a && VV == 5}
  
     not a subtype of Required type
       VV : {VV : Int | VV <= plen p}
  
     in Context
       zero : {zero : Word8 | zero == ?b}
       VV   : {VV : Int | VV == ?a && VV == (5  :  int)}
       fp   : {fp : ForeignPtr a | fplen fp == ?c && 0 <= fplen fp}
       p    : {p  : Ptr a | fplen fp == plen p && ?c <= plen p && ?b <= plen p && zero <= plen p}
       ?a   : {?a : Int | ?a == 5}
       ?c   : {?c : Int | ?c == 4}
       ?b   : {?b : Integer | ?b == 0}
  ~~~~~
  
  \noindent The error says we're bumping `p` up by `VV == 5`
  using `plusPtr` but the latter *requires* that bump-offset
  be within the size of the buffer referred to by `p`, i.e.
  `VV <= plen p`. Indeed, in this context, we have:
  
  ~~~~~{.liquiderror}
       p    : {p : Ptr a | fplen fp == plen p && ?c <= plen p && ?b <= plen p && zero <= plen p}
       fp   : {fp : ForeignPtr a | fplen fp == ?c && 0 <= fplen fp}
  ~~~~~
  
  \noindent that is, the size of `p`, namely `plen p` equals the size of
  `fp`, namely `fplen fp` (thanks to the `withForeignPtr` call).  The
  latter equals to `?c` which is `4` bytes. Thus, since the offset `5`
  is not less than the buffer size `4`, LiquidHaskell cannot prove that
  the call to `plusPtr` is safe, hence the error.
  
  
  Assumptions vs Guarantees
  -------------------------
  
  At this point you ought to wonder: where is the code for `peek`,
  `poke` or `mallocForeignPtrBytes` and so on? How can we be sure
  that the types we assigned to them are in fact legitimate?
  
  \newthought{Frankly, we cannot} as those functions are *externally*
  implemented (in this case, in `C`), and hence, invisible to the
  otherwise all-seeing eyes of LiquidHaskell. Thus, we are *assuming* or
  *trusting* that those functions behave according to their types. Put
  another way, the types for the low-level API are our *specification*
  for what low-level pointer safety. We shall now *guarantee* that the
  higher level modules that build upon this API in fact use the
  low-level function in a manner consistent with this specification.
  
  \newthought{Assumptions are a Feature} and not a bug, as they let
  us to verify systems that use some modules for which we do not have
  the code. Here, we can *assume* a boundary specification, and then
  *guarantee* that the rest of the system is safe with respect to
  that specification. ^[If we so desire, we can also *check* the boundary
  specifications at [run-time](http://en.wikipedia.org/wiki/Design_by_contract),
  but that is outside the scope of LiquidHaskell.]
  
  ByteString API
  --------------
  
  Next, let's see how the low-level API can be used to implement
  to implement [ByteStrings][bytestring], in a way that lets us
  perform fast string operations without opening the door to
  overflows.
  
  
  \newthought{A ByteString} is implemented as a record of three fields:
  
  \begin{code}
  data ByteString = BS {
      bPtr :: ForeignPtr Word8
    , bOff :: !Int
    , bLen :: !Int
    }
  \end{code}
  
  + `bPtr` is a *pointer* to a block of memory,
  + `bOff` is the *offset* in the block where the string begins,
  + `bLen` is the number of bytes from the offset that belong to the string.
  
  These entities are illustrated in Figure [auto](#fig:bytestring); the
  green portion represents the actual contents of a particular
  `ByteString`.  This representation makes it possible to implement
  various operations like computing prefixes and suffixes extremely
  quickly, simply by pointer arithmetic.
  
  <div class="figure"
       id="fig:bytestring"
       height="100px"
       file="img/bytestring.png"
       caption="Representing ByteStrings in memory.">
  </div>
  
  \newthought{In a Legal ByteString} the *start* (`bOff`) and *end*
  (`bOff + bLen`) offsets lie inside the buffer referred to by the
  pointer `bPtr`. We can formalize this invariant with a data definition
  that will then make it impossible to create illegal `ByteString`s:
  
  \begin{code}
  {-@ data ByteString = BS {
        bPtr :: ForeignPtr Word8
      , bOff :: {v:Nat| v        <= fplen bPtr}
      , bLen :: {v:Nat| v + bOff <= fplen bPtr}
      }
    @-}
  \end{code}
  
  
  \noindent The refinements on `bOff` and `bLen` correspond exactly
  to the legality requirements that the start and end of the `ByteString`
  be *within* the block of memory referred to by `bPtr`.
  
  
  \newthought{For brevity} let's define an alias for `ByteString`s of
  a given size:
  
  \begin{code}
  {-@ type ByteStringN N = {v:ByteString | bLen v = N} @-}
  \end{code}
  
  \newthought{Legal Bytestrings}  can be created by directly using
  the constructor, as long as we pass in suitable offsets and lengths.
  For example,
  
  \begin{code}
  {-@ good1 :: IO (ByteStringN 5) @-}
  good1 = do fp <- mallocForeignPtrBytes 5
             return (BS fp 0 5)
  \end{code}
  
  \noindent creates a valid `ByteString` of size `5`; however we
  need not start at the beginning of the block, or use up all
  the buffer, and can instead create `ByteString`s whose length
  is less than the size of the allocated block, as shown in `good2`
  whose length is `2` while the allocated block has size `5`.
  
  \begin{code}
  {-@ good2 :: IO (ByteStringN 2) @-}
  good2 = do fp <- mallocForeignPtrBytes 5
             return (BS fp 3 2)
  \end{code}
  
  \newthought{Illegal Bytestrings} are rejected by LiquidHaskell.
  For example, `bad1`'s length is exceeds its buffer
  size, and is flagged as such:
  
  \begin{code}
  bad1 = do fp <- mallocForeignPtrBytes 3
            return (BS fp 0 10)
  \end{code}
  
  \noindent Similarly, `bad2` does have `2` bytes but *not* if
  we start at the offset of `2`:
  
  \begin{code}
  bad2 = do fp <- mallocForeignPtrBytes 3
            return (BS fp 2 2)
  \end{code}
  
  <div class="hwex" id="Legal ByteStrings">
  Modify the definitions of `bad1` and `bad2` so they are *accepted* by LiquidHaskell.
  </div>
  
  <div class="toolinfo">
  \newthought{Measures are generated from Fields} in the datatype
  definition.  As GHC lets us use the fields as accessor functions, we
  can *refine* the types of those functions to specify their behavior to
  LiquidHaskell. For example, we can type the (automatically generated)
  field-accessor function `bLen` so that it actually returns the exact
  size of the `ByteString` argument.
  </div>
  
  \begin{code}
  {-@ bLen :: b:ByteString -> {v: Nat | v = bLen b} @-}
  \end{code}
  
  \newthought{To Safely Create} a `ByteString` the
  implementation defines a higher order `create` function, that
  takes a size `n` and accepts a `fill` action, and runs the
  action after allocating the pointer. After running the action,
  the function tucks the pointer into and returns a `ByteString`
  of size `n`.
  
  \begin{code}
  {-@ create :: n:Nat -> (Ptr Word8 -> IO ()) -> ByteStringN n @-}
  create n fill = unsafePerformIO $ do
    fp  <- mallocForeignPtrBytes n
    withForeignPtr fp fill
    return (BS fp 0 n)
  \end{code}
  
  <div class="hwex" id="Create">
  \singlestar Why does LiquidHaskell *reject* the following function
  that creates a `ByteString` corresponding to `"GHC"`?
  </div>
  
  \begin{code}
  bsGHC = create 3 $ \p -> do
    poke (p `plusPtr` 0) (c2w 'G')
    poke (p `plusPtr` 1) (c2w 'H')
    poke (p `plusPtr` 2) (c2w 'C')
  \end{code}
  
  \hint The function writes into 3 slots starting at `p`.
  How big should `plen p` be to allow this? What type
  does LiquidHaskell infer for `p` above? Does it meet
  the requirement? Which part of the *specification*
  or *implementation* needs to be modified so that the
  relevant information about `p` becomes available within
  the `do`-block above? Make sure you figure out the above
  before proceeding.
  
  \newthought{To Pack} a `String` into a `ByteString`
  we simply call `create` with the appropriate fill
  action:^[The code uses `create'` which is just `create`
  with the *correct* signature in case you want to skip
  the previous exercise. (But don't!)]
  
  \begin{code}
  pack str      = create' n $ \p -> go p xs
    where
    n           = length str
    xs          = map c2w str
    go p (x:xs) = poke p x >> go (plusPtr p 1) xs
    go _ []     = return  ()
  \end{code}
  
  <div class="hwex" id="Pack">
  We can compute the size of a `ByteString` by using the function:
  Fix the specification for `pack` so that (it still typechecks!)
  and furthermore, the following [QuickCheck style property](#quickcheck)
  is proved.
  </div>
  
  \begin{code}
  {-@ prop_pack_length  :: String -> TRUE @-}
  prop_pack_length xs   = bLen (pack xs) == length xs
  \end{code}
  
  \hint Look at the type of `length`, and recall that `len`
  is a [numeric measure](#numericmeasure) denoting the size
  of a list.
  
  \newthought{The magic of inference} ensures that `pack`
  just works. Notice there is a tricky little recursive loop
  `go` that is used to recursively fill in the `ByteString`
  and actually, it has a rather subtle type signature that
  LiquidHaskell is able to automatically infer.
  
  <div class="hwex" id="Pack Invariant">
  \exercise \singlestar Still, we're here to learn, so can you
  *write down* the type signature for the `pLoop` so that the below
  variant of `pack` is accepted by LiquidHaskell (Do this *without*
  cheating by peeping at the type inferred for `go` above!)
  </div>
  
  \begin{code}
  packEx str     = create' n $ \p -> pLoop p xs
    where
    n            = length str
    xs           = map c2w str
  
  {-@ pLoop      :: (Storable a) => p:Ptr a -> xs:[a] -> IO () @-}
  pLoop p (x:xs) = poke p x >> pLoop (plusPtr p 1) xs
  pLoop _ []     = return ()
  \end{code}
  
  \hint Remember that `len xs` denotes the size of the list `xs`.
  
  <div class="hwex" id="Unsafe Take and Drop">
  The functions `unsafeTake` and `unsafeDrop` respectively extract
  the prefix and suffix of a `ByteString` from a given position.
  They are really fast since we only have to change the offsets.
  But why does LiquidHaskell reject them? Can you fix the
  specifications so that they are accepted?
  </div>
  
  \begin{code}
  {-@ unsafeTake :: n:Nat -> b:_ -> ByteStringN n @-}
  unsafeTake n (BS x s _) = BS x s n
  
  {-@ unsafeDrop :: n:Nat -> b:_ -> ByteStringN {bLen b - n} @-}
  unsafeDrop n (BS x s l) = BS x (s + n) (l - n)
  \end{code}
  
  \hint Under what conditions are the returned `ByteString`s legal?
  
  
  \newthought{To Unpack} a `ByteString` into a plain old `String`,
  we essentially run `pack` in reverse, by walking over the pointer,
  and reading out the characters one by one till we reach the end:
  
  \begin{code}
  unpack              :: ByteString -> String
  unpack (BS _  _ 0)  = []
  unpack (BS ps s l)  = unsafePerformIO
                          $ withForeignPtr ps
                          $ \p -> go (p `plusPtr` s) (l - 1) []
    where
      {-@ go     :: p:_ -> n:_ -> acc:_ -> IO {v:_ | true } @-}
      go p 0 acc = peekAt p 0 >>= \e -> return (w2c e : acc)
      go p n acc = peekAt p n >>= \e -> go p (n-1) (w2c e : acc)
      peekAt p n = peek (p `plusPtr` n)
  \end{code}
  
  <div class="hwex" id="Unpack">
  \singlestar Fix the specification for `unpack`
  so that the below QuickCheck style property is proved by LiquidHaskell.
  </div>
  
  \begin{code}
  {-@ prop_unpack_length :: ByteString -> TRUE @-}
  prop_unpack_length b   = bLen b == length (unpack b)
  \end{code}
  
  \hint You will also have to fix the specification of the helper `go`.
  Can you determine the output refinement should be (instead of just `true`?)
  How *big* is the output list in terms of `p`, `n` and `acc`.
  
  
  Application API
  ---------------
  
  Finally, let's revisit our potentially "bleeding" `chop` function to
  see how the refined `ByteString` API can prevent errors.  We require
  that the prefix size `n` be less than the size of the input string `s`:
  
  \begin{code}
  {-@ chop :: s:String -> n:BNat (len s) -> String @-}
  chop s n = s'
    where
      b    = pack s          -- down to low-level
      b'   = unsafeTake n b  -- grab n chars
      s'   = unpack b'       -- up to high-level
  \end{code}
  
  \newthought{Overflows are prevented} by LiquidHaskell, as it
  rejects calls to `chop` where the prefix size is too large
  which is what led to the overflow that spilled the contents
  of memory after the string (cf. Figure [auto](#fig:overflow)).
  In the code below, the first use of `chop` which
  defines `ex6` is accepted as `6 <= len ex` but the second
  call is rejected as `30 > len ex`.
  
  \begin{code}
  demo     = [ex6, ex30]
    where
      ex   = ['L','I','Q','U','I','D']
      ex6  = chop ex 6   -- accepted by LH
      ex30 = chop ex 30  -- rejected by LH
  \end{code}
  
  <div class="hwex" id="Chop"> Fix the specification for `chop` so that
  the following property is proved:
  
  \begin{code}
  {-@ prop_chop_length  :: String -> Nat -> TRUE @-}
  prop_chop_length s n
    | n <= length s     = length (chop s n) == n
    | otherwise         = True
  \end{code}
  
  <div class="hwex" id="Checked Chop"> In the above, we know statically
  that the string is longer than the prefix, but what if the string and prefix
  are obtained *dynamically*, e.g. as inputs from the user? Fill in the implementation
  of `ok` below to ensure that `chop` is called safely with user specified values:
  </div>
  
  
  \begin{code}
  safeChop      :: String -> Int -> String
  safeChop str n
    | ok        = chop str n
    | otherwise = ""
    where
      ok        = True
  
  queryAndChop  :: IO String
  queryAndChop  = do putStrLn "Give me a string:"
                     str  <-  getLine
                     putStrLn "Give me a number:"
                     ns   <-  getLine
                     let n =  read ns :: Int
                     return $ safeChop str n
  \end{code}
  
  Nested ByteStrings
  ------------------
  
  For a more in-depth example, let's take a look at `group`,
  which transforms strings like `"foobaaar"` into *lists* of
  strings like `["f","oo", "b", "aaa", "r"]`.
  The specification is that `group` should produce a
  
  1. list of *non-empty* `ByteStrings`,
  2. the *sum of* whose lengths equals that of the input string.
  
  \newthought{Non-empty ByteStrings} are those whose length is non-zero:
  
  \begin{code}
  {-@ predicate Null B  = bLen B == 0                   @-}
  {-@ type ByteStringNE = {v:ByteString | not (Null v)} @-}
  \end{code}
  
  \noindent We can use these to enrich the API with a `null` check
  
  \begin{code}
  {-@ null :: b:_ -> {v:Bool | v <=> Null b} @-}
  null (BS _ _ l) = l == 0
  \end{code}
  
  \noindent This check is used to determine if it is safe
  to extract the head and tail of the `ByteString`.
  we can use refinements to ensure the safety of
  the operations and also track the sizes. ^[`peekByteOff p i` is equivalent to `peek (plusPtr p i)`.]
  
  \begin{code}
  {-@ unsafeHead :: ByteStringNE -> Word8 @-}
  unsafeHead (BS x s _) = unsafePerformIO $
                            withForeignPtr x $ \p ->
                              peekByteOff p s
  
  {-@ unsafeTail :: b:ByteStringNE -> ByteStringN {bLen b -1} @-}
  unsafeTail (BS ps s l) = BS ps (s + 1) (l - 1)
  \end{code}
  
  \newthought{The Group`} function recursively calls `spanByte` to carve off
  the next group, and then returns the accumulated results:
  
  \begin{code}
  {-@ group :: b:_ -> {v: [ByteStringNE] | bsLen v = bLen b} @-}
  group xs
      | null xs   = []
      | otherwise = let  y        = unsafeHead xs
                         (ys, zs) = spanByte y (unsafeTail xs)
                    in (y `cons` ys) : group zs
  \end{code}
  
  \noindent The first requirement, that the groups be non-empty is captured by the fact that
  the output is a `[ByteStringNE]`. The second requirement, that the sum of the lengths is
  preserved, is expressed by a writing a [numeric measure](#numericmeasure):
  
  \begin{code}
  {-@ measure bsLen @-}
  bsLen        :: [ByteString] -> Int
  bsLen []     = 0
  bsLen (b:bs) = bLen b + bsLen bs
  \end{code}
  
  
  \newthought{SpanByte} does a lot of the heavy lifting. It uses low-level pointer
  arithmetic to find the *first* position in the `ByteString` that is different from
  the input character `c` and then splits the `ByteString` into a pair comprising the
  prefix and suffix at that point. (If you filled in the relevant type signatures above,
  the below code should typecheck even after you _delete_ the `assume` from the specification.)
  
  \begin{code}
  {-@ assume spanByte :: Word8 -> b:ByteString -> ByteString2 b @-}
  spanByte c ps@(BS x s ln)
    = unsafePerformIO
        $ withForeignPtr x $ \p ->
           go (p `plusPtr` s) 0
    where
      go p i
        | i >= ln   = return (ps, empty)
        | otherwise = do c' <- peekByteOff p i
                         if c /= c'
                           then return (splitAt i)
                           else go p (i+1)
      splitAt i     = (unsafeTake i ps, unsafeDrop i ps)
  \end{code}
  
  LiquidHaskell infers that `0 <= i <= l` and therefore that
  all of the memory accesses are safe. Furthermore, due to
  the precise specifications given to `unsafeTake` and
  `unsafeDrop`, it is able to prove that the output pair's
  lengths add up to the size of the input `ByteString`.
  
  \begin{code}
  {-@ type ByteString2 B
        = {v:_ | bLen (fst v) + bLen (snd v) = bLen B} @-}
  \end{code}
  
  Recap: Types Against Overflows
  ------------------------------
  
  In this chapter we saw a case study illustrating how measures
  and refinements enable safe low-level pointer arithmetic in
  Haskell. The take away messages are that we can:
  
  1. *compose* larger systems from layers of smaller ones,
  2. *refine* APIs for each layer, which can be used to
  3. *design and validate* the layers above.
  
  We saw this recipe in action by developing a low-level
  `Pointer` API, using it to implement fast `ByteString`s
  API, and then building some higher-level functions on
  top of the `ByteStrings`.
  
  \newthought{The Trusted Computing Base} in this approach includes
  exactly those layers for which the code is *not* available, for
  example, because they are implemented outside the language and
  accessed via the FFI as with `mallocForeignPtrBytes` and `peek` and
  `poke`. In this case, we can make progress by *assuming* the APIs hold
  for those layers and verify the rest of the system with respect to
  that API.  It is important to note that in the entire case study, it
  is only the above FFI signatures that are *trusted*; the rest are all
  verified by LiquidHaskell.
  
  \begin{comment}
  \begin{code}
  -----------------------------------------------------------------------
  -- Helper Code
  -----------------------------------------------------------------------
  
  {-@ unsafeCreate :: l:Nat -> (PtrN Word8 l -> IO ()) -> ByteStringN l @-}
  unsafeCreate n f = create' n f -- unsafePerformIO $ create n f
  
  {-@ qualif PLLen(v:a, p:b) : len v <= plen p @-}
  {-@ qualif ForeignPtrN(v:ForeignPtr a, n:int): fplen v = n @-}
  {-@ qualif FPLenPLen(v:Ptr a, fp:ForeignPtr a): fplen fp = plen v @-}
  {-@ qualif PtrLen(v:Ptr a, xs:List b): plen v = len xs @-}
  {-@ qualif PlenEq(v: Ptr a, x: int): x <= plen v @-}
  
  {-@ cons :: Word8 -> b:ByteString -> {v:ByteStringNE | bLen v = bLen b + 1} @-}
  cons :: Word8 -> ByteString -> ByteString
  cons c (BS x s l) = unsafeCreate (l+1) $ \p -> withForeignPtr x $ \f -> do
          poke p c
          memcpy (p `plusPtr` 1) (f `plusPtr` s) (fromIntegral l)
  
  {-@ empty :: {v:ByteString | bLen v = 0} @-}
  empty :: ByteString
  empty = BS nullForeignPtr 0 0
  
  {-@ assume mallocForeignPtrBytes :: n:Nat -> IO (ForeignPtrN a n) @-}
  {-@ type ForeignPtrN a N = {v:ForeignPtr a | fplen v = N} @-}
  {-@ malloc :: n:Nat -> IO (ForeignPtrN a n) @-}
  malloc = mallocForeignPtrBytes
  
  {-@ assume
      c_memcpy :: dst:PtrV Word8
               -> src:PtrV Word8
               -> size:{CSize | size <= plen src && size <= plen dst}
               -> IO (Ptr Word8)
    @-}
  foreign import ccall unsafe "string.h memcpy" c_memcpy
      :: Ptr Word8 -> Ptr Word8 -> CSize -> IO (Ptr Word8)
  
  {-@ memcpy :: dst:PtrV Word8
             -> src:PtrV Word8
             -> size:{CSize | size <= plen src && size <= plen dst}
             -> IO ()
    @-}
  memcpy :: Ptr Word8 -> Ptr Word8 -> CSize -> IO ()
  memcpy p q s = c_memcpy p q s >> return ()
  
  {-@ assume nullForeignPtr :: {v: ForeignPtr Word8 | fplen v = 0} @-}
  nullForeignPtr :: ForeignPtr Word8
  nullForeignPtr = unsafePerformIO $ newForeignPtr_ nullPtr
  {-# NOINLINE nullForeignPtr #-}
  
  {-@ create' :: n:Nat -> (PtrN Word8 n -> IO ()) -> ByteStringN n @-}
  create' n fill = unsafePerformIO $ do
    fp  <- mallocForeignPtrBytes n
    withForeignPtr fp fill
    return (BS fp 0 n)
  \end{code}
  \end{comment}
  