> {-@ LIQUID "--no-termination" @-}
> {-@ LIQUID "--short-names"    @-}
> {-@  LIQUID "--diffcheck"     @-}
> {-# LANGUAGE ForeignFunctionInterface #-}
> 
> module Bytestring where
> 
> import Prelude hiding (null)
> import Data.Char
> import Data.Word
> import Foreign.C.Types
> import Foreign.ForeignPtr
> import Foreign.Ptr
> import Foreign.Storable
> import System.IO.Unsafe
> import Language.Haskell.Liquid.Prelude

Now for some real fun, let's try to prove that `ByteString` is memory-safe! 

`ByteString`s are at the heart of many Haskell applications, e.g. web servers, 
and, as we saw at the beginning of the talk, a bad access can lead to a segfault 
or, even worse, leaking arbitrary memory.

A `ByteString` consists of a pointer into a region of memory, an offset into 
the region, and a length.

> data ByteString = PS { bPayload :: ForeignPtr Word8
>                      , bOffset  :: !Int
>                      , bLength  :: !Int
>                      }

The crucial invariant is that we should only be able to reach valid memory 
locations via the offset and length, i.e. the sum `off + len` *must not exceed* 
the "length" of the pointer.

> {-@ data ByteString = PS
>       { bPayload :: ForeignPtr Word8
>       , bOffset  :: {v:Nat | v           <= fplen bPayload}
>       , bLength  :: {v:Nat | bOffset + v <= fplen bPayload}
>       }
>   @-}

What is the "length" of a pointer? It's the number of bytes that are
addressable from the base of the pointer. We can't compute it, but that
won't stop us from talking about it in our types. We provide a "ghost"
measure called `fplen` to refer to this length.

NV: "ghost measure" is more complicated than uninterpreted function

< {-@ measure fplen :: ForeignPtr a -> Int @-}

and use it to define a foreign-pointer to a segment containing *N* bytes

> {-@ type ForeignN a N = {v:ForeignPtr a | fplen v = N} @-}

Since we haven't defined any equations for `fplen` we won't get strengthed 
constructors. Instead, we will *assume* that `malloc` behaves sensibly and
allocates the number of bytes you asked for.

> {-@ assume mallocForeignPtrBytes :: n:Nat -> IO (ForeignN a n) @-}

Now let's create a few `ByteString`s. Here's a `ByteString` with 5 valid 
indices. 

> good_bs1 = do fp <- mallocForeignPtrBytes 5
>               return $ PS fp 0 5

Note that the *length* of the BS is *not* the same as the region
of allocated memory. 

Here's a `ByteString` whose pointer region has 5-bytes, but the BS itself
is of size 4.
 
> good_bs2 = do fp <- mallocForeignPtrBytes 5
>               return $ PS fp 2 4

LiquidHaskell won't let us build a `ByteString` that claims to have more valid 
indices than it *actually* does

> bad_bs1 = do
>   fp <- mallocForeignPtrBytes 0 
>   return $ PS fp 0 10 

even if we try to be sneaky with the length parameter.

> bad_bs2 = do fp <- mallocForeignPtrBytes 3
>              return $ PS fp 2 2


Creating ByteStrings
--------------------

Nobody actually builds `ByteString`s like this though.

The authors have kindly provided a higher-order function
called `create` to handle the actual allocation. To `create`
a `ByteString` you have to say how many bytes you want and
provide a function that will fill in the newly allocated memory.

> create :: Int -> (Ptr Word8 -> IO ()) -> IO ByteString
> create l f = do
>     fp <- mallocForeignPtrBytes l
>     withForeignPtr fp $ \p -> f p
>     return $! PS fp 0 l

But this seems horribly unsafe!

What's to stop the parameter `f` from poking any random,
invalid offset from the pointer it wants to?

We could, e.g.

* create a BS of size `5`, and
* write a `0` at the index `10`.

ASIDE: have these assumed types around to suppress the type-errors that LH will 
       show, just remove them when script introduces type

> {- assume plusPtr :: p:Ptr a -> n:Int -> Ptr b      @-}
> {- assume poke :: Storable a => Ptr a -> a -> IO () @-}

END ASIDE

> bad_create = create 5 $ \p -> poke (p `plusPtr` 10) (0 :: Word8)

which clearly isn't correct. We'd like to say that the provided
function can only address locations a up to a certain offset
from the pointer.

Just as we had `fplen` to talk about the "length" of a `ForeignPtr`,
we have provided `plen` to talk about the "length" of a `Ptr`, and
we've defined a helpful alias

< {-@ type PtrN a N = {v:Ptr a | plen v = N} @-}

which says that a `PtrN a n` has precisely `n` addressable bytes
from its base.


Pointer Arithmetic
------------------

We have also given `plusPtr` the type

< {-@ plusPtr :: p:Ptr a -> n:Int -> {v:Ptr a | plen v = plen p - n} @-}

which says that as you increment a `Ptr`, you're left with fewer addressable
bytes.

Finally, we type `poke` as 

< {-@ poke :: Storable a => {v:Ptr a | 0 <= plen v } -> a -> IO () @-}

which says that the given `Ptr` must be addressable in order to safely `poke` it.

Now we have all of the necessary tools to *prevent* ourselves from
shooting ourselves in the foot with functions like `bad_create`.

We'll just give `create` the type
 
> {-@ create :: l:Nat -> (PtrN Word8 l -> IO ()) -> IO (ByteStringN l) @-}

where the alias

> {-@ type ByteStringN N = {v:ByteString | bLength v = N} @-}

describes `ByteString`s of length `N`.

Lo and behold, LiquidHaskell has flagged `bad_create` as unsafe! 

Furthermore, we can write things like

> good_create = create 5 $ \p -> poke (p `plusPtr` 2) (0 :: Word8)

Here's a real example from the BS library:

> packWith        :: (a -> Word8) -> [a] -> ByteString
> packWith k str  = unsafeCreate (length str) $ \p -> go p str
>   where
>     go _ []     = return ()
>     go p (x:xs) = poke p (k x) >> go (p `plusPtr` 1) xs

proving that `pack` will *never* write out-of-bounds!


ES: CUT


Nested Data
-----------

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 list of `ByteStrings`

1. that are all *non-empty* (safety)
2. the sum of whose lengths is equal to the length of the input string (precision)

We use the type alias

> {-@ type ByteStringNE = {v:ByteString | bLength v > 0} @-}

to specify (safety) and introduce a new measure

> {-@ measure bLengths  :: [ByteString] -> Int
>     bLengths ([])   = 0
>     bLengths (x:xs) = (bLength x) + (bLengths xs)
>   @-}

to specify (precision). The full type-specification looks like this:

> {-@ group :: b:ByteString -> {v: [ByteStringNE] | bLengths v = bLength b} @-}
> group xs
>     | null xs   = []
>     | otherwise = let y = unsafeHead xs
>                       (ys, zs) = spanByte (unsafeHead xs) (unsafeTail xs)
>                   in (y `cons` ys) : group zs

As you can probably tell, `spanByte` appears to be doing a lot of the work here,
so let's take a closer look at it to see why the post-condition holds.

> spanByte :: Word8 -> ByteString -> (ByteString, ByteString)
> spanByte c ps@(PS x s l) = unsafePerformIO $ withForeignPtr x $ \p ->
>     go (p `plusPtr` s) 0
>   where
>     go p i | i >= l    = return (ps, empty)
>            | otherwise = do c' <- peekByteOff p i
>                             if c /= c'
>                                 then return (unsafeTake i ps, unsafeDrop i ps)
>                                 else go p (i+1)

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 `spanByte` has the type

> {-@ spanByte :: Word8 -> b:ByteString -> (ByteStringPair b) @-}

where `ByteStringPair b` describes a pair of `ByteString`s whose lengths sum to
the length of `b`.

> {-@ type ByteStringPair B = (ByteString, ByteString)<{\x1 x2 ->
>       bLength x1 + bLength x2 = bLength B}> @-}


RJ:LIMITATIONS

Those familiar with the internals of ByteString may notice that we have made a
small change in `group`, the original implementation was

< group :: ByteString -> [ByteString]
< group xs
<     | null xs   = []
<     | otherwise = ys : group zs
<     where
<         (ys, zs) = spanByte (unsafeHead xs) xs

Unfortunately this change was necessary in order to prove the safety invariant,
that `group` returns a list of non-empty `ByteString`s. The real type we would
like to give to `spanByte` (which would enable verification of the original
`group`) would say something like

  `spanByte x b` returns a pair of `ByteString`s, the first of which is non-empty
  *iff* `x = head b`

but it is unclear how to prove this at the moment in LiquidHaskell
(TODO: figure out what would need to change to prove this.)

> -----------------------------------------------------------------------
> -- Helper Code
> -----------------------------------------------------------------------
> {-@ unsafeCreate :: l:Nat -> ((PtrN Word8 l) -> IO ()) -> (ByteStringN l) @-}
> unsafeCreate n f = unsafePerformIO $ create n f
>
> {-@ invariant {v:ByteString   | bLength  v >= 0} @-}
> {-@ invariant {v:[ByteString] | bLengths v >= 0} @-}
> 
> {-@ 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) @-}
>
> {-@ unsafeHead :: {v:ByteString | (bLength v) > 0} -> Word8 @-}
> unsafeHead :: ByteString -> Word8
> unsafeHead (PS x s l) = liquidAssert (l > 0) $
>   unsafePerformIO  $  withForeignPtr x $ \p -> peekByteOff p s
> 
> {-@ unsafeTail :: b:{v:ByteString | (bLength v) > 0}
>                -> {v:ByteString | (bLength v) = (bLength b) - 1} @-}
> unsafeTail :: ByteString -> ByteString
> unsafeTail (PS ps s l) = liquidAssert (l > 0) $ PS ps (s+1) (l-1)
> 
> {-@ null :: b:ByteString -> {v:Bool | ((Prop v) <=> ((bLength b) = 0))} @-}
> null :: ByteString -> Bool
> null (PS _ _ l) = liquidAssert (l >= 0) $ l <= 0
> 
> {-@ unsafeTake :: n:Nat -> b:{v: ByteString | n <= (bLength v)} -> (ByteStringN n) @-}
> unsafeTake :: Int -> ByteString -> ByteString
> unsafeTake n (PS x s l) = liquidAssert (0 <= n && n <= l) $ PS x s n
> 
> {-@ unsafeDrop :: n:Nat
>                -> b:{v: ByteString | n <= (bLength v)} 
>                -> {v:ByteString | (bLength v) = (bLength b) - n} @-}
> unsafeDrop  :: Int -> ByteString -> ByteString
> unsafeDrop n (PS x s l) = liquidAssert (0 <= n && n <= l) $ PS x (s+n) (l-n)
> 
> {-@ cons :: Word8 -> b:ByteString -> {v:ByteString | (bLength v) = 1 + (bLength b)} @-}
> cons :: Word8 -> ByteString -> ByteString
> cons c (PS 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 | (bLength v) = 0} @-} 
> empty :: ByteString
> empty = PS nullForeignPtr 0 0
> 
> {-@ assume
>     c_memcpy :: dst:(PtrV Word8)
>              -> src:(PtrV Word8) 
>              -> size: {v:CSize | (v <= (plen src) && v <= (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: {v:CSize | (v <= (plen src) && v <= (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 #-}