diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2014, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main where
+
+import Language.Haskell.Liquid.Cabal (liquidHaskellMain)
+
+main :: IO ()
+main = liquidHaskellMain
diff --git a/liquid-bytestring.cabal b/liquid-bytestring.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-bytestring.cabal
@@ -0,0 +1,56 @@
+cabal-version:      1.24
+name:               liquid-bytestring
+version:            0.10.10.0
+synopsis:           LiquidHaskell specs for the bytestring package
+description:        LiquidHaskell specs for the bytestring package.
+license:            BSD3
+license-file:       LICENSE
+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
+author:             Ranjit Jhala, Niki Vazou, Eric Seidel
+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
+category:           Language
+homepage:           https://github.com/ucsd-progsys/liquidhaskell
+build-type:         Custom
+
+data-files:           src/Data/ByteString.spec
+                      src/Data/ByteString/Short.spec
+                      src/Data/ByteString/Lazy.spec
+                      src/Data/ByteString/Unsafe.spec
+                      src/Data/ByteString/Char8.spec
+                      src/Data/ByteString/Lazy/Char8.spec
+
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
+library
+  exposed-modules:    Data.ByteString
+                      Data.ByteString.Char8
+                      Data.ByteString.Unsafe
+                      Data.ByteString.Internal
+                      Data.ByteString.Lazy
+                      Data.ByteString.Lazy.Internal
+                      Data.ByteString.Short
+                      Data.ByteString.Short.Internal
+
+                      Data.ByteString.Builder
+                      Data.ByteString.Builder.Extra
+                      Data.ByteString.Builder.Prim
+
+                      Data.ByteString.Builder.Internal
+                      Data.ByteString.Builder.Prim.Internal
+                      Data.ByteString.Lazy.Builder
+                      Data.ByteString.Lazy.Builder.Extras
+                      Data.ByteString.Lazy.Builder.ASCII
+
+                      -- FIXME: This is commented out as unfortunately it doesn't refine
+                      -- correctly with modern versions of bytestring.
+                      -- Data.ByteString.Lazy.Char8
+
+  hs-source-dirs:     src
+  build-depends:      liquid-base          < 5
+                    , bytestring           >= 0.10.10.0 && < 0.11
+                    , liquidhaskell        >= 0.8.10.1
+  default-language:   Haskell2010
+  default-extensions: PackageImports
+  if impl(ghc >= 8.10)
+    ghc-options: -fplugin=LiquidHaskell
diff --git a/src/Data/ByteString.hs b/src/Data/ByteString.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString.hs
@@ -0,0 +1,4 @@
+module Data.ByteString ( module Exports ) where
+
+import Data.String
+import "bytestring" Data.ByteString as Exports
diff --git a/src/Data/ByteString.spec b/src/Data/ByteString.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString.spec
@@ -0,0 +1,375 @@
+module spec Data.ByteString where
+
+import Data.String
+
+measure bslen :: Data.ByteString.ByteString -> { n : Int | 0 <= n }
+
+invariant { bs : Data.ByteString.ByteString  | 0 <= bslen bs }
+
+invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs }
+
+empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }
+
+singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 }
+
+pack :: w8s : [_]
+     -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }
+
+unpack :: bs : Data.ByteString.ByteString
+       -> { w8s : [_] | len w8s == bslen bs }
+
+cons :: _
+     -> i : Data.ByteString.ByteString
+     -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }
+
+snoc :: i : Data.ByteString.ByteString
+     -> _
+     -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }
+
+append :: l : Data.ByteString.ByteString
+       -> r : Data.ByteString.ByteString
+       -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }
+
+head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _
+
+unsnoc :: i:Data.ByteString.ByteString 
+       -> (Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, _))
+
+last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _
+
+tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _
+
+init 
+  :: {i:Data.ByteString.ByteString | 1 <= bslen i } 
+  -> {o:Data.ByteString.ByteString | bslen o == bslen i - 1 }
+
+null 
+  :: bs : Data.ByteString.ByteString
+  -> { b : GHC.Types.Bool | b <=> bslen bs == 0 }
+
+length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }
+
+map 
+  :: (_ -> _)
+  -> i : Data.ByteString.ByteString
+  -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+reverse 
+  :: i : Data.ByteString.ByteString
+  -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+intersperse 
+  :: _
+  -> i : Data.ByteString.ByteString
+  -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }
+
+intercalate 
+  :: l : Data.ByteString.ByteString
+  -> rs : [Data.ByteString.ByteString]
+  -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }
+
+transpose 
+  :: is : [Data.ByteString.ByteString]
+  -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}
+
+foldl1 
+  :: (_ -> _ -> _)
+  -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+  -> _
+
+foldl1' 
+  :: (_ -> _ -> _)
+  -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+  -> _
+
+foldr1 
+  :: (_ -> _ -> _)
+  -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+  -> _
+
+foldr1' 
+  :: (_ -> _ -> _)
+  -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+  -> _
+
+concat 
+  :: is : [Data.ByteString.ByteString] 
+  -> { o : Data.ByteString.ByteString | (len is == 0) ==> (bslen o == 0) }
+
+concatMap 
+  :: (_ -> Data.ByteString.ByteString)
+  -> i : Data.ByteString.ByteString
+  -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }
+
+any 
+  :: (_ -> GHC.Types.Bool)
+  -> bs : Data.ByteString.ByteString
+  -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }
+
+all 
+  :: (_ -> GHC.Types.Bool)
+  -> bs : Data.ByteString.ByteString
+  -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }
+
+maximum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _
+
+minimum :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _
+
+scanl :: (_ -> _ -> _)
+      -> _
+      -> i : Data.ByteString.ByteString
+      -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+scanl1 :: (_ -> _ -> _)
+       -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }
+       -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+scanr
+    :: (_ -> _ -> _)
+    -> _
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+scanr1
+    :: (_ -> _ -> _)
+    -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+mapAccumL
+    :: (acc -> _ -> (acc, _))
+    -> acc
+    -> i : Data.ByteString.ByteString
+    -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })
+
+mapAccumR
+    :: (acc -> _ -> (acc, _))
+    -> acc
+    -> i : Data.ByteString.ByteString
+    -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })
+
+replicate
+    :: n : Int
+    -> _
+    -> { bs : Data.ByteString.ByteString | bslen bs == n }
+
+unfoldrN
+    :: n : Int
+    -> (a -> Maybe (_, a))
+    -> a
+    -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)
+
+take
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&
+                                          ((0 <= n && n <= bslen i) <=> bslen o == n) &&
+                                          (bslen i <= n <=> bslen o = bslen i) }
+
+drop
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&
+                                          ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) &&
+                                          (bslen i <= n <=> bslen o == 0) }
+
+splitAt
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&
+                                            ((0 <= n && n <= bslen i) <=> bslen l == n) &&
+                                            (bslen i <= n <=> bslen l == bslen i) }
+       , { r : Data.ByteString.ByteString | (n <= 0 <=> bslen r == bslen i) &&
+                                            ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) &&
+                                            (bslen i <= n <=> bslen r == 0) }
+       )
+
+takeWhile
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+dropWhile
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+span
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+spanEnd
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+break
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+breakEnd
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+group
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]
+
+groupBy
+    :: (_ -> _ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]
+
+inits
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+tails
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+split
+    :: _
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+splitWith
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+isPrefixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b }
+
+isSuffixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }
+
+isInfixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }
+
+breakSubstring
+    :: il : Data.ByteString.ByteString
+    -> ir : Data.ByteString.ByteString
+    -> ( { ol : Data.ByteString.ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}
+       , { or : Data.ByteString.ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) }
+       )
+
+elem
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }
+
+notElem
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }
+
+find
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> (Maybe { w8 : _ | bslen bs /= 0 })
+
+filter
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+partition
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+index :: bs : Data.ByteString.ByteString -> { n : Int | 0 <= n && n < bslen bs } -> _
+
+elemIndex
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> (Maybe { n : Int | 0 <= n && n < bslen bs })
+
+elemIndices
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> [{ n : Int | 0 <= n && n < bslen bs }]
+
+elemIndexEnd
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> (Maybe { n : Int | 0 <= n && n < bslen bs })
+
+findIndex
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> (Maybe { n : Int | 0 <= n && n < bslen bs })
+
+findIndices
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> [{ n : Int | 0 <= n && n < bslen bs }]
+
+count
+    :: _
+    -> bs : Data.ByteString.ByteString
+    -> { n : Int | 0 <= n && n < bslen bs }
+
+zip
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { o : [(_, _)] | len o <= bslen l && len o <= bslen r }
+
+zipWith
+    :: (_ -> _ -> a)
+    -> l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { o : [a] | len o <= bslen l && len o <= bslen r }
+
+unzip
+    :: i : [(_, _)]
+    -> ( { l : Data.ByteString.ByteString | bslen l == len i }
+       , { r : Data.ByteString.ByteString | bslen r == len i }
+       )
+
+sort
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+copy
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+hGet
+    :: _
+    -> n : { n : Int | 0 <= n }
+    -> (IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 })
+
+hGetSome
+    :: _
+    -> n : { n : Int | 0 <= n }
+    -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })
+
+hGetNonBlocking
+    :: _
+    -> n : { n : Int | 0 <= n }
+    -> (IO { bs : Data.ByteString.ByteString | bslen bs <= n })
+
+uncons
+    :: i : Data.ByteString.ByteString
+    -> (Maybe (_, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 }))
+    
diff --git a/src/Data/ByteString/Builder.hs b/src/Data/ByteString/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Builder.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Builder (module Exports) where
+
+import "bytestring" Data.ByteString.Builder as Exports
diff --git a/src/Data/ByteString/Builder/Extra.hs b/src/Data/ByteString/Builder/Extra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Builder/Extra.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Builder.Extra (module Exports) where
+
+import "bytestring" Data.ByteString.Builder.Extra as Exports
diff --git a/src/Data/ByteString/Builder/Internal.hs b/src/Data/ByteString/Builder/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Builder/Internal.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Builder.Internal (module Exports) where
+
+import "bytestring" Data.ByteString.Builder.Internal as Exports
diff --git a/src/Data/ByteString/Builder/Prim.hs b/src/Data/ByteString/Builder/Prim.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Builder/Prim.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Builder.Prim (module Exports) where
+
+import "bytestring" Data.ByteString.Builder.Prim as Exports
diff --git a/src/Data/ByteString/Builder/Prim/Internal.hs b/src/Data/ByteString/Builder/Prim/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Builder/Prim/Internal.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Builder.Prim.Internal (module Exports) where
+
+import "bytestring" Data.ByteString.Builder.Prim.Internal as Exports
diff --git a/src/Data/ByteString/Char8.hs b/src/Data/ByteString/Char8.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Char8.hs
@@ -0,0 +1,6 @@
+module Data.ByteString.Char8 ( module Exports ) where
+
+import Data.Int
+import Data.ByteString
+import GHC.IO.Handle
+import "bytestring" Data.ByteString.Char8 as Exports
diff --git a/src/Data/ByteString/Char8.spec b/src/Data/ByteString/Char8.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Char8.spec
@@ -0,0 +1,402 @@
+module spec Data.ByteString.Char8 where
+
+import Data.ByteString 
+
+assume empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }
+
+assume singleton
+    :: Char -> { bs : Data.ByteString.ByteString | bslen bs == 1 }
+
+assume pack
+    :: w8s : [Char]
+    -> { bs : Data.ByteString.ByteString | bslen bs == len w8s }
+
+assume unpack
+    :: bs : Data.ByteString.ByteString
+    -> { w8s : [Char] | len w8s == bslen bs }
+
+assume cons
+    :: Char
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }
+
+assume snoc
+    :: i : Data.ByteString.ByteString
+    -> Char
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i + 1 }
+
+assume append
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen l + bslen r }
+
+head :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char
+
+assume uncons
+    :: i : Data.ByteString.ByteString
+    -> Maybe (Char, { o : Data.ByteString.ByteString | bslen o == bslen i - 1 })
+
+assume unsnoc
+    :: i : Data.ByteString.ByteString
+    -> Maybe ({ o : Data.ByteString.ByteString | bslen o == bslen i - 1 }, Char)
+
+assume last :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char
+
+assume tail :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.ByteString.ByteString
+
+assume init :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Data.ByteString.ByteString
+
+assume null
+    :: bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | b <=> bslen bs == 0 }
+
+assume length :: bs : Data.ByteString.ByteString -> { n : Int | bslen bs == n }
+
+assume map
+    :: (Char -> Char)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume reverse
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume intersperse
+    :: Char
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | (bslen i == 0 <=> bslen o == 0) && (1 <= bslen i <=> bslen o == 2 * bslen i - 1) }
+
+assume intercalate
+    :: l : Data.ByteString.ByteString
+    -> rs : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.ByteString | len rs == 0 ==> bslen o == 0 }
+
+assume transpose
+    :: is : [Data.ByteString.ByteString]
+    -> { os : [{ bs : Data.ByteString.ByteString | bslen bs <= len is }] | len is == 0 ==> len os == 0}
+
+foldl1
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+    -> Char
+
+foldl1'
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+    -> Char
+
+foldr1
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+    -> Char
+
+foldr1'
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.ByteString | 1 <= bslen bs }
+    -> Char
+
+assume concat
+    :: is : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.ByteString | len is == 0 ==> bslen o == 0 }
+
+assume concatMap
+    :: (Char -> Data.ByteString.ByteString)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen i == 0 ==> bslen o == 0 }
+
+assume any :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }
+
+assume all :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }
+
+maximum
+    :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char
+
+minimum
+    :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> Char
+
+assume scanl
+    :: (Char -> Char -> Char)
+    -> Char
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume scanl1
+    :: (Char -> Char -> Char)
+    -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume scanr
+    :: (Char -> Char -> Char)
+    -> Char
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume scanr1
+    :: (Char -> Char -> Char)
+    -> i : { i : Data.ByteString.ByteString | 1 <= bslen i }
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume mapAccumL
+    :: (acc -> Char -> (acc, Char))
+    -> acc
+    -> i : Data.ByteString.ByteString
+    -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })
+
+assume mapAccumR
+    :: (acc -> Char -> (acc, Char))
+    -> acc
+    -> i : Data.ByteString.ByteString
+    -> (acc, { o : Data.ByteString.ByteString | bslen o == bslen i })
+
+assume replicate
+    :: n : Int
+    -> Char
+    -> { bs : Data.ByteString.ByteString | bslen bs == n }
+
+assume unfoldrN
+    :: n : Int
+    -> (a -> Maybe (Char, a))
+    -> a
+    -> ({ bs : Data.ByteString.ByteString | bslen bs <= n }, Maybe a)
+
+assume take
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == 0) &&
+                                          ((0 <= n && n <= bslen i) <=> bslen o == n) &&
+                                          (bslen i <= n <=> bslen o = bslen i) }
+
+assume drop
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | (n <= 0 <=> bslen o == bslen i) &&
+                                          ((0 <= n && n <= bslen i) <=> bslen o == bslen i - n) &&
+                                          (bslen i <= n <=> bslen o == 0) }
+
+assume splitAt
+    :: n : Int
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | (n <= 0 <=> bslen l == 0) &&
+                                            ((0 <= n && n <= bslen i) <=> bslen l == n) &&
+                                            (bslen i <= n <=> bslen l == bslen i) }
+       , { r : Data.ByteString.ByteString | (n <= 0 <=> bslen r == bslen i) &&
+                                            ((0 <= n && n <= bslen i) <=> bslen r == bslen i - n) &&
+                                            (bslen i <= n <=> bslen r == 0) }
+       )
+
+assume takeWhile
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+assume dropWhile
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+assume span
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+assume spanEnd
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+assume break
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+assume breakEnd
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       )
+
+assume group
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]
+
+assume groupBy
+    :: (Char -> Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | 1 <= bslen o && bslen o <= bslen i }]
+
+assume inits
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume tails
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume split
+    :: Char
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume splitWith
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume lines
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume words
+    :: i : Data.ByteString.ByteString
+    -> [{ o : Data.ByteString.ByteString | bslen o <= bslen i }]
+
+assume unlines
+    :: is : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.ByteString | (len is == 0 <=> bslen o == 0) && bslen o >= len is }
+
+assume unwords
+    :: is : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.ByteString | (len is == 0 ==> bslen o == 0) && (1 <= len is ==> bslen o >= len is - 1) }
+
+assume isPrefixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l >= bslen r ==> not b }
+
+assume isSuffixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }
+
+assume isInfixOf
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen l > bslen r ==> not b }
+
+assume breakSubstring
+    :: il : Data.ByteString.ByteString
+    -> ir : Data.ByteString.ByteString
+    -> ( { ol : Data.ByteString.ByteString | bslen ol <= bslen ir && (bslen il > bslen ir ==> bslen ol == bslen ir)}
+       , { or : Data.ByteString.ByteString | bslen or <= bslen ir && (bslen il > bslen ir ==> bslen or == 0) }
+       )
+
+assume elem
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> not b }
+
+assume notElem
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> { b : GHC.Types.Bool | bslen bs == 0 ==> b }
+
+assume find
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> Maybe { w8 : Char | bslen bs /= 0 }
+
+assume filter
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o <= bslen i }
+
+index
+    :: bs : Data.ByteString.ByteString
+    -> { n : Int | 0 <= n && n < bslen bs }
+    -> Char
+
+assume elemIndex
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> Maybe { n : Int | 0 <= n && n < bslen bs }
+
+assume elemIndices
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> [{ n : Int | 0 <= n && n < bslen bs }]
+
+assume elemIndexEnd
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> Maybe { n : Int | 0 <= n && n < bslen bs }
+
+assume findIndex
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> Maybe { n : Int | 0 <= n && n < bslen bs }
+
+assume findIndices
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.ByteString
+    -> [{ n : Int | 0 <= n && n < bslen bs }]
+
+assume count
+    :: Char
+    -> bs : Data.ByteString.ByteString
+    -> { n : Int | 0 <= n && n < bslen bs }
+
+assume zip
+    :: l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { o : [(Char, Char)] | len o <= bslen l && len o <= bslen r }
+
+assume zipWith
+    :: (Char -> Char -> a)
+    -> l : Data.ByteString.ByteString
+    -> r : Data.ByteString.ByteString
+    -> { o : [a] | len o <= bslen l && len o <= bslen r }
+
+assume unzip
+    :: i : [(Char, Char)]
+    -> ( { l : Data.ByteString.ByteString | bslen l == len i }
+       , { r : Data.ByteString.ByteString | bslen r == len i }
+       )
+
+assume sort
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume readInt
+    :: i : Data.ByteString.ByteString
+    -> Maybe { p : (Int, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }
+
+assume readInteger
+    :: i : Data.ByteString.ByteString
+    -> Maybe { p : (Integer, { o : Data.ByteString.ByteString | bslen o < bslen i}) | bslen i /= 0 }
+
+assume copy
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i }
+
+assume hGet
+    :: GHC.IO.Handle
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.ByteString | bslen bs == n || bslen bs == 0 }
+
+assume hGetSome
+    :: GHC.IO.Handle
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }
+
+assume hGetNonBlocking
+    :: GHC.IO.Handle
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.ByteString | bslen bs <= n }
+
+// assume partition
+    // :: (Char -> GHC.Types.Bool)
+    // -> i : Data.ByteString.ByteString
+    // -> ( { l : Data.ByteString.ByteString | bslen l <= bslen i }
+       // , { r : Data.ByteString.ByteString | bslen r <= bslen i }
+       // )
diff --git a/src/Data/ByteString/Internal.hs b/src/Data/ByteString/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Internal.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Internal (module Exports) where
+
+import "bytestring" Data.ByteString.Internal as Exports
diff --git a/src/Data/ByteString/Lazy.hs b/src/Data/ByteString/Lazy.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy.hs
@@ -0,0 +1,5 @@
+module Data.ByteString.Lazy ( module Exports ) where
+
+import Data.String
+import Data.ByteString
+import "bytestring" Data.ByteString.Lazy as Exports
diff --git a/src/Data/ByteString/Lazy.spec b/src/Data/ByteString/Lazy.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy.spec
@@ -0,0 +1,338 @@
+module spec Data.ByteString.Lazy where
+
+import Data.String
+import Data.ByteString
+
+measure bllen :: Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | 0 <= n }
+
+invariant { bs : Data.ByteString.Lazy.ByteString | 0 <= bllen bs }
+
+invariant { bs : Data.ByteString.Lazy.ByteString | bllen bs == stringlen bs }
+
+assume empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 }
+
+assume singleton
+    :: _ -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }
+
+assume pack
+    :: w8s : [_]
+    -> { bs : _ | bllen bs == len w8s }
+
+assume unpack
+    :: bs : Data.ByteString.Lazy.ByteString
+    -> { w8s : [_] | len w8s == bllen bs }
+
+assume fromStrict
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i }
+
+assume toStrict
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bllen i }
+
+assume fromChunks
+    :: i : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 }
+
+assume toChunks
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 }
+
+assume cons
+    :: _
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }
+
+assume snoc
+    :: i : Data.ByteString.Lazy.ByteString
+    -> _
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }
+
+assume append
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r }
+
+assume head
+    :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> _
+
+assume uncons
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe (_, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })
+
+assume unsnoc
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, _)
+
+assume last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _
+
+assume tail :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _
+
+assume init :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _
+
+assume null :: bs : Data.ByteString.Lazy.ByteString -> { b : GHC.Types.Bool | b <=> bllen bs == 0 }
+
+assume length
+    :: bs : Data.ByteString.Lazy.ByteString -> { n : GHC.Int.Int64 | bllen bs == n }
+
+assume map
+    :: (_ -> _)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume reverse
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume intersperse
+    :: _
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) }
+
+assume intercalate
+    :: l : Data.ByteString.Lazy.ByteString
+    -> rs : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 }
+
+assume transpose
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0}
+
+assume foldl1
+    :: (_ -> _ -> _)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> _
+
+assume foldl1'
+    :: (_ -> _ -> _)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> _
+
+assume foldr1
+    :: (_ -> _ -> _)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> _
+
+assume concat
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | (len is == 0) ==> (bllen o == 0) }
+
+assume concatMap
+    :: (_ -> Data.ByteString.Lazy.ByteString)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }
+
+assume any :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }
+
+assume all :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }
+
+assume maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _
+
+assume minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> _
+
+assume scanl
+    :: (_ -> _ -> _)
+    -> _
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume mapAccumL
+    :: (acc -> _ -> (acc, _))
+    -> acc
+    -> i : Data.ByteString.Lazy.ByteString
+    -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })
+
+assume mapAccumR
+    :: (acc -> _ -> (acc, _))
+    -> acc
+    -> i : Data.ByteString.Lazy.ByteString
+    -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })
+
+assume replicate
+    :: n : GHC.Int.Int64
+    -> _
+    -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }
+
+assume take
+    :: n : GHC.Int.Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) &&
+                                               ((0 <= n && n <= bllen i) <=> bllen o == n) &&
+                                               (bllen i <= n <=> bllen o = bllen i) }
+
+assume drop
+    :: n : GHC.Int.Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) &&
+                                               ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) &&
+                                               (bllen i <= n <=> bllen o == 0) }
+
+assume splitAt
+    :: n : GHC.Int.Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) &&
+                                                 ((0 <= n && n <= bllen i) <=> bllen l == n) &&
+                                                 (bllen i <= n <=> bllen l == bllen i) }
+       , { r : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen r == bllen i) &&
+                                                 ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) &&
+                                                 (bllen i <= n <=> bllen r == 0) }
+       )
+
+assume takeWhile
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+assume dropWhile
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+assume span
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }
+       )
+
+assume break
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }
+       )
+
+assume group
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]
+
+assume groupBy
+    :: (_ -> _ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]
+
+assume inits
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume tails
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume split
+    :: _
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume splitWith
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume isPrefixOf
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }
+
+assume isSuffixOf
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }
+
+assume elem
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | (bllen bs == 0) ==> not b }
+
+assume notElem
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | (bllen bs == 0) ==> b }
+
+assume find
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { w8 : _ | bllen bs /= 0 }
+
+assume filter
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+assume partition
+    :: (_ -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }
+       )
+
+assume index
+    :: bs : Data.ByteString.Lazy.ByteString
+    -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }
+    -> _
+
+assume elemIndex
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }
+
+assume elemIndices
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]
+
+assume elemIndexEnd
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }
+
+assume findIndex
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }
+
+assume findIndices
+    :: (_ -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> [{ n : GHC.Int.Int64 | 0 <= n && n < bllen bs }]
+
+assume count
+    :: _
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { n : GHC.Int.Int64 | 0 <= n && n < bllen bs }
+
+assume zip
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : [(_, _)] | len o <= bllen l && len o <= bllen r }
+
+assume zipWith
+    :: (_ -> _ -> a)
+    -> l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : [a] | len o <= bllen l && len o <= bllen r }
+
+assume unzip
+    :: i : [(_, _)]
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }
+       )
+
+assume copy
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume hGet
+    :: _
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 }
+
+assume hGetNonBlocking
+    :: _
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n }
diff --git a/src/Data/ByteString/Lazy/Builder.hs b/src/Data/ByteString/Lazy/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy/Builder.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Lazy.Builder (module Exports) where
+
+import "bytestring" Data.ByteString.Lazy.Builder as Exports
diff --git a/src/Data/ByteString/Lazy/Builder/ASCII.hs b/src/Data/ByteString/Lazy/Builder/ASCII.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy/Builder/ASCII.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Lazy.Builder.ASCII (module Exports) where
+
+import "bytestring" Data.ByteString.Lazy.Builder.ASCII as Exports
diff --git a/src/Data/ByteString/Lazy/Builder/Extras.hs b/src/Data/ByteString/Lazy/Builder/Extras.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy/Builder/Extras.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Lazy.Builder.Extras (module Exports) where
+
+import "bytestring" Data.ByteString.Lazy.Builder.Extras as Exports
diff --git a/src/Data/ByteString/Lazy/Char8.spec b/src/Data/ByteString/Lazy/Char8.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy/Char8.spec
@@ -0,0 +1,355 @@
+module spec Data.ByteString.Lazy.Char8 where
+
+last :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char
+
+assume empty :: { bs : Data.ByteString.Lazy.ByteString | bllen bs == 0 }
+
+assume singleton
+    :: Char -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == 1 }
+
+assume pack
+    :: w8s : [Char]
+    -> { bs : Data.ByteString.ByteString | bllen bs == len w8s }
+
+assume unpack
+    :: bs : Data.ByteString.Lazy.ByteString
+    -> { w8s : [Char] | len w8s == bllen bs }
+
+assume fromStrict
+    :: i : Data.ByteString.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bslen i }
+
+assume toStrict
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.ByteString | bslen o == bllen i }
+
+assume fromChunks
+    :: i : [Data.ByteString.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | len i == 0 <=> bllen o == 0 }
+
+assume toChunks
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { os : [{ o : Data.ByteString.ByteString | bslen o <= bllen i}] | len os == 0 <=> bllen i == 0 }
+
+assume cons
+    :: Char
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }
+
+assume snoc
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Char
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i + 1 }
+
+assume append
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen l + bllen r }
+
+head
+    :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> Char
+
+assume uncons
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe (Char, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 })
+
+assume unsnoc
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe ({ o : Data.ByteString.Lazy.ByteString | bllen o == bllen i - 1 }, Char)
+
+assume null
+    :: bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | b <=> bllen bs == 0 }
+
+assume length
+    :: bs : Data.ByteString.Lazy.ByteString -> { n : Int64 | bllen bs == n }
+
+assume map
+    :: (Char -> Char)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume reverse
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume intersperse
+    :: Char
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (bllen i == 0 <=> bllen o == 0) && (1 <= bllen i <=> bllen o == 2 * bllen i - 1) }
+
+assume intercalate
+    :: l : Data.ByteString.Lazy.ByteString
+    -> rs : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | len rs == 0 ==> bllen o == 0 }
+
+assume transpose
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { os : [{ bs : Data.ByteString.Lazy.ByteString | bllen bs <= len is }] | len is == 0 ==> len os == 0}
+
+foldl1
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> Char
+
+foldl1'
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> Char
+
+foldr1
+    :: (Char -> Char -> Char)
+    -> { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs }
+    -> Char
+
+assume concat
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | len is == 0 ==> bllen o }
+
+assume concatMap
+    :: (Char -> Data.ByteString.Lazy.ByteString)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen i == 0 ==> bllen o == 0 }
+
+assume any :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen bs == 0 ==> not b }
+
+assume all :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen bs == 0 ==> b }
+
+maximum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char
+
+minimum :: { bs : Data.ByteString.Lazy.ByteString | 1 <= bllen bs } -> Char
+
+assume scanl
+    :: (Char -> Char -> Char)
+    -> Char
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume scanl1
+    :: (Char -> Char -> Char)
+    -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume scanr
+    :: (Char -> Char -> Char)
+    -> Char
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume scanr1
+    :: (Char -> Char -> Char)
+    -> i : { i : Data.ByteString.Lazy.ByteString | 1 <= bllen i }
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume mapAccumL
+    :: (acc -> Char -> (acc, Char))
+    -> acc
+    -> i : Data.ByteString.Lazy.ByteString
+    -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })
+
+assume mapAccumR
+    :: (acc -> Char -> (acc, Char))
+    -> acc
+    -> i : Data.ByteString.Lazy.ByteString
+    -> (acc, { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i })
+
+assume replicate
+    :: n : Int64
+    -> Char
+    -> { bs : Data.ByteString.Lazy.ByteString | bllen bs == n }
+
+assume take
+    :: n : Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 ==> bllen o == 0) &&
+                                               ((0 <= n && n <= bllen i) <=> bllen o == n) &&
+                                               (bllen i <= n <=> bllen o = bllen i) }
+
+assume drop
+    :: n : Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen o == bllen i) &&
+                                               ((0 <= n && n <= bllen i) <=> bllen o == bllen i - n) &&
+                                               (bllen i <= n <=> bllen o == 0) }
+
+assume splitAt
+    :: n : Int64
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen l == 0) &&
+                                                 ((0 <= n && n <= bllen i) <=> bllen l == n) &&
+                                                 (bllen i <= n <=> bllen l == bllen i) }
+       , { r : Data.ByteString.Lazy.ByteString | (n <= 0 <=> bllen r == bllen i) &&
+                                                 ((0 <= n && n <= bllen i) <=> bllen r == bllen i - n) &&
+                                                 (bllen i <= n <=> bllen r == 0) }
+       )
+
+assume takeWhile
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+assume dropWhile
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+assume span
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }
+       )
+
+assume break
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l <= bllen i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r <= bllen i }
+       )
+
+assume group
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]
+
+assume groupBy
+    :: (Char -> Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | 1 <= bllen o && bllen o <= bllen i }]
+
+assume inits
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume tails
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume split
+    :: Char
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume splitWith
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume lines
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume words
+    :: i : Data.ByteString.Lazy.ByteString
+    -> [{ o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }]
+
+assume unlines
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 <=> bllen o == 0) && bllen o >= len is }
+
+assume unwords
+    :: is : [Data.ByteString.Lazy.ByteString]
+    -> { o : Data.ByteString.Lazy.ByteString | (len is == 0 ==> bllen o == 0) && (1 <= len is ==> bllen o >= len is - 1) }
+
+assume isPrefixOf
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }
+
+assume isSuffixOf
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen l >= bllen r ==> not b }
+
+assume elem
+    :: Char
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen b == 0 ==> not b }
+
+assume notElem
+    :: Char
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { b : GHC.Types.Bool | bllen b == 0 ==> b }
+
+assume find
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { w8 : Char | bllen bs /= 0 }
+
+assume filter
+    :: (Char -> GHC.Types.Bool)
+    -> i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o <= bllen i }
+
+index
+    :: bs : Data.ByteString.Lazy.ByteString
+    -> { n : Int64 | 0 <= n && n < bllen bs }
+    -> Char
+
+assume elemIndex
+    :: Char
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { n : Int64 | 0 <= n && n < bllen bs }
+
+assume elemIndices
+    :: Char
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> [{ n : Int64 | 0 <= n && n < bllen bs }]
+
+assume findIndex
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> Maybe { n : Int64 | 0 <= n && n < bllen bs }
+
+assume findIndices
+    :: (Char -> GHC.Types.Bool)
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> [{ n : Int64 | 0 <= n && n < bllen bs }]
+
+assume count
+    :: Char
+    -> bs : Data.ByteString.Lazy.ByteString
+    -> { n : Int64 | 0 <= n && n < bllen bs }
+
+assume zip
+    :: l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : [(Char, Char)] | len o <= bllen l && len o <= bllen r }
+
+assume zipWith
+    :: (Char -> Char -> a)
+    -> l : Data.ByteString.Lazy.ByteString
+    -> r : Data.ByteString.Lazy.ByteString
+    -> { o : [a] | len o <= bllen l && len o <= bllen r }
+
+assume unzip
+    :: i : [(Char, Char)]
+    -> ( { l : Data.ByteString.Lazy.ByteString | bllen l == len i }
+       , { r : Data.ByteString.Lazy.ByteString | bllen r == len i }
+       )
+
+assume readInt
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe { p : (Int, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }
+
+assume readInteger
+    :: i : Data.ByteString.Lazy.ByteString
+    -> Maybe { p : (Integer, { o : Data.ByteString.Lazy.ByteString | bllen o < bllen i}) | bllen i /= 0 }
+
+assume copy
+    :: i : Data.ByteString.Lazy.ByteString
+    -> { o : Data.ByteString.Lazy.ByteString | bllen o == bllen i }
+
+assume hGet
+    :: GHC.IO.Handle
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs == n || bllen bs == 0 }
+
+assume hGetNonBlocking
+    :: GHC.IO.Handle
+    -> n : { n : Int | 0 <= n }
+    -> IO { bs : Data.ByteString.Lazy.ByteString | bllen bs <= n }
diff --git a/src/Data/ByteString/Lazy/Internal.hs b/src/Data/ByteString/Lazy/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Lazy/Internal.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Lazy.Internal (module Exports) where
+
+import "bytestring" Data.ByteString.Lazy.Internal as Exports
diff --git a/src/Data/ByteString/Short.hs b/src/Data/ByteString/Short.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Short.hs
@@ -0,0 +1,5 @@
+module Data.ByteString.Short ( module Exports ) where
+
+import Data.ByteString
+import Data.Word
+import "bytestring" Data.ByteString.Short as Exports
diff --git a/src/Data/ByteString/Short.spec b/src/Data/ByteString/Short.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Short.spec
@@ -0,0 +1,25 @@
+module spec Data.ByteString.Short where
+
+import Data.String
+
+measure sbslen :: Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n }
+
+invariant { bs : Data.ByteString.Short.ShortByteString  | 0 <= sbslen bs }
+
+invariant { bs : Data.ByteString.Short.ShortByteString | sbslen bs == stringlen bs }
+
+toShort :: i : Data.ByteString.ByteString -> { o : Data.ByteString.Short.ShortByteString | sbslen o == bslen i }
+
+fromShort :: o : Data.ByteString.Short.ShortByteString -> { i : Data.ByteString.ByteString | bslen i == sbslen o }
+
+pack :: w8s : [Word8] -> { bs : Data.ByteString.Short.ShortByteString | sbslen bs == len w8s }
+
+unpack :: bs : Data.ByteString.Short.ShortByteString -> { w8s : [Word8] | len w8s == sbslen bs }
+
+empty :: { bs : Data.ByteString.Short.ShortByteString | sbslen bs == 0 }
+
+null :: bs : Data.ByteString.Short.ShortByteString -> { b : GHC.Types.Bool | b <=> sbslen bs == 0 }
+
+length :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | sbslen bs == n }
+
+index :: bs : Data.ByteString.Short.ShortByteString -> { n : Int | 0 <= n && n < sbslen bs } -> Word8
diff --git a/src/Data/ByteString/Short/Internal.hs b/src/Data/ByteString/Short/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Short/Internal.hs
@@ -0,0 +1,3 @@
+module Data.ByteString.Short.Internal (module Exports) where
+
+import "bytestring" Data.ByteString.Short.Internal as Exports
diff --git a/src/Data/ByteString/Unsafe.hs b/src/Data/ByteString/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Unsafe.hs
@@ -0,0 +1,5 @@
+module Data.ByteString.Unsafe ( module Exports ) where
+
+import Data.ByteString
+import Data.Word
+import "bytestring" Data.ByteString.Unsafe as Exports
diff --git a/src/Data/ByteString/Unsafe.spec b/src/Data/ByteString/Unsafe.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/ByteString/Unsafe.spec
@@ -0,0 +1,29 @@
+module spec Data.ByteString.Unsafe where
+
+unsafeHead
+    :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ 
+
+unsafeTail
+    :: bs : { v : Data.ByteString.ByteString | bslen v > 0 }
+    -> { v : Data.ByteString.ByteString | bslen v = bslen bs - 1 }
+
+unsafeInit
+    :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ 
+
+unsafeLast
+    :: { bs : Data.ByteString.ByteString | 1 <= bslen bs } -> _ 
+
+unsafeIndex
+    :: bs : Data.ByteString.ByteString
+    -> { n : Int | 0 <= n && n < bslen bs }
+    -> _ 
+
+unsafeTake
+    :: n : { n : Int | 0 <= n }
+    -> i : { i : Data.ByteString.ByteString | n <= bslen i }
+    -> { o : Data.ByteString.ByteString | bslen o == n }
+
+unsafeDrop
+    :: n : { n : Int | 0 <= n }
+    -> i : { i : Data.ByteString.ByteString | n <= bslen i }
+    -> { o : Data.ByteString.ByteString | bslen o == bslen i - n }