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-vector.cabal b/liquid-vector.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-vector.cabal
@@ -0,0 +1,54 @@
+cabal-version:      1.24
+name:               liquid-vector
+version:            0.12.1.2
+synopsis:           LiquidHaskell specs for the vector package
+description:        LiquidHaskell specs for the vector 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/Vector.spec
+
+custom-setup
+  setup-depends: Cabal, base, liquidhaskell
+
+library
+  exposed-modules:    Data.Vector.Internal.Check
+                      Data.Vector.Fusion.Util
+                      Data.Vector.Fusion.Stream.Monadic
+                      Data.Vector.Fusion.Bundle.Size
+                      Data.Vector.Fusion.Bundle.Monadic
+                      Data.Vector.Fusion.Bundle
+
+                      Data.Vector.Generic.Mutable.Base
+                      Data.Vector.Generic.Mutable
+                      Data.Vector.Generic.Base
+                      Data.Vector.Generic.New
+                      Data.Vector.Generic
+
+                      Data.Vector.Primitive.Mutable
+                      Data.Vector.Primitive
+
+                      Data.Vector.Storable.Internal
+                      Data.Vector.Storable.Mutable
+                      Data.Vector.Storable
+
+                      Data.Vector.Unboxed.Base
+                      Data.Vector.Unboxed.Mutable
+                      Data.Vector.Unboxed
+
+                      Data.Vector.Mutable
+                      Data.Vector
+  hs-source-dirs:     src
+  build-depends:      liquid-base          < 4.15
+                    , vector               >= 0.12.1.2 && < 0.13
+                    , 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/Vector.hs b/src/Data/Vector.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector.hs
@@ -0,0 +1,3 @@
+module Data.Vector ( module Exports ) where
+
+import "vector" Data.Vector as Exports
diff --git a/src/Data/Vector.spec b/src/Data/Vector.spec
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector.spec
@@ -0,0 +1,40 @@
+module spec Data.Vector where
+
+import GHC.Base
+
+data variance Data.Vector.Vector covariant
+
+
+measure vlen    :: forall a. (Data.Vector.Vector a) -> Int
+
+invariant       {v: Data.Vector.Vector a | 0 <= vlen v } 
+
+!           :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a 
+
+unsafeIndex :: forall a. x:(Data.Vector.Vector a) -> vec:{v:Nat | v < vlen x } -> a 
+
+fromList  :: forall a. x:[a] -> {v: Data.Vector.Vector a  | vlen v = len x }
+
+length    :: forall a. x:(Data.Vector.Vector a) -> {v : Nat | v = vlen x }
+
+replicate :: n:Nat -> a -> {v:Data.Vector.Vector a | vlen v = n} 
+
+imap :: (Nat -> a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }
+
+map :: (a -> b) -> x:(Data.Vector.Vector a) -> {y:Data.Vector.Vector b | vlen y = vlen x }
+
+head :: forall a. {xs: Data.Vector.Vector a | vlen xs > 0} -> a 
+
+qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  =  0 
+qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  >  0 
+qualif VecEmpty(v: Data.Vector.Vector a)    : (vlen v)  >= 0 
+
+qualif Vlen(v:int, x: Data.Vector.Vector a) : (v  =  vlen x)
+qualif Vlen(v:int, x: Data.Vector.Vector a) : (v <=  vlen x) 
+qualif Vlen(v:int, x: Data.Vector.Vector a) : (v  <  vlen x) 
+
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <  vlen x) 
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v <= vlen x) 
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >  vlen x) 
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v >= vlen x) 
+qualif CmpVlen(v:Data.Vector.Vector a, x:Data.Vector.Vector b) : (vlen v =  vlen x) 
diff --git a/src/Data/Vector/Fusion/Bundle.hs b/src/Data/Vector/Fusion/Bundle.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Fusion/Bundle.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Fusion.Bundle (module Exports) where
+
+import "vector" Data.Vector.Fusion.Bundle as Exports
diff --git a/src/Data/Vector/Fusion/Bundle/Monadic.hs b/src/Data/Vector/Fusion/Bundle/Monadic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Fusion/Bundle/Monadic.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Fusion.Bundle.Monadic (module Exports) where
+
+import "vector" Data.Vector.Fusion.Bundle.Monadic as Exports
diff --git a/src/Data/Vector/Fusion/Bundle/Size.hs b/src/Data/Vector/Fusion/Bundle/Size.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Fusion/Bundle/Size.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Fusion.Bundle.Size (module Exports) where
+
+import "vector" Data.Vector.Fusion.Bundle.Size as Exports
diff --git a/src/Data/Vector/Fusion/Stream/Monadic.hs b/src/Data/Vector/Fusion/Stream/Monadic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Fusion/Stream/Monadic.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Fusion.Stream.Monadic (module Exports) where
+
+import "vector" Data.Vector.Fusion.Stream.Monadic as Exports
diff --git a/src/Data/Vector/Fusion/Util.hs b/src/Data/Vector/Fusion/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Fusion/Util.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Fusion.Util (module Exports) where
+
+import "vector" Data.Vector.Fusion.Util as Exports
diff --git a/src/Data/Vector/Generic.hs b/src/Data/Vector/Generic.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Generic.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Generic (module Exports) where
+
+import "vector" Data.Vector.Generic as Exports
diff --git a/src/Data/Vector/Generic/Base.hs b/src/Data/Vector/Generic/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Generic/Base.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Generic.Base (module Exports) where
+
+import "vector" Data.Vector.Generic.Base as Exports
diff --git a/src/Data/Vector/Generic/Mutable.hs b/src/Data/Vector/Generic/Mutable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Generic/Mutable.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Generic.Mutable ( module Exports ) where
+
+import "vector" Data.Vector.Generic.Mutable as Exports
diff --git a/src/Data/Vector/Generic/Mutable/Base.hs b/src/Data/Vector/Generic/Mutable/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Generic/Mutable/Base.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Generic.Mutable.Base (module Exports) where
+
+import "vector" Data.Vector.Generic.Mutable.Base as Exports
diff --git a/src/Data/Vector/Generic/New.hs b/src/Data/Vector/Generic/New.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Generic/New.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Generic.New (module Exports) where
+
+import "vector" Data.Vector.Generic.New as Exports
diff --git a/src/Data/Vector/Internal/Check.hs b/src/Data/Vector/Internal/Check.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Internal/Check.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Internal.Check (module Exports) where
+
+import "vector" Data.Vector.Internal.Check as Exports
diff --git a/src/Data/Vector/Mutable.hs b/src/Data/Vector/Mutable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Mutable.hs
@@ -0,0 +1,4 @@
+
+module Data.Vector.Mutable (module Exports) where
+
+import "vector" Data.Vector.Mutable as Exports
diff --git a/src/Data/Vector/Primitive.hs b/src/Data/Vector/Primitive.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Primitive.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Primitive (module Exports) where
+
+import "vector" Data.Vector.Primitive as Exports
diff --git a/src/Data/Vector/Primitive/Mutable.hs b/src/Data/Vector/Primitive/Mutable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Primitive/Mutable.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Primitive.Mutable (module Exports) where
+
+import "vector" Data.Vector.Primitive.Mutable as Exports
diff --git a/src/Data/Vector/Storable.hs b/src/Data/Vector/Storable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Storable.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Storable (module Exports) where
+
+import "vector" Data.Vector.Storable as Exports
diff --git a/src/Data/Vector/Storable/Internal.hs b/src/Data/Vector/Storable/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Storable/Internal.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Storable.Internal (module Exports) where
+
+import "vector" Data.Vector.Storable.Internal as Exports
diff --git a/src/Data/Vector/Storable/Mutable.hs b/src/Data/Vector/Storable/Mutable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Storable/Mutable.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Storable.Mutable (module Exports) where
+
+import "vector" Data.Vector.Storable.Mutable as Exports
diff --git a/src/Data/Vector/Unboxed.hs b/src/Data/Vector/Unboxed.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Unboxed.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Unboxed (module Exports) where
+
+import "vector" Data.Vector.Unboxed as Exports
diff --git a/src/Data/Vector/Unboxed/Base.hs b/src/Data/Vector/Unboxed/Base.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Unboxed/Base.hs
@@ -0,0 +1,3 @@
+module Data.Vector.Unboxed.Base (module Exports) where
+
+import "vector" Data.Vector.Unboxed.Base as Exports
diff --git a/src/Data/Vector/Unboxed/Mutable.hs b/src/Data/Vector/Unboxed/Mutable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Vector/Unboxed/Mutable.hs
@@ -0,0 +1,4 @@
+module Data.Vector.Unboxed.Mutable (module Exports) where
+
+import "vector" Data.Vector.Unboxed.Mutable as Exports
+