Benchmarks

Ghc.List, Data.List: size-related properties
Data.Map, Data.Splay: binary-search ordered trees
Vector-Algorithms: safe indexing
Bytestring, Text: size-based low-level memory safety

Lines of Code:	10204
Lines of Annotations:	2030
Verification Time:	38min

Invariants in ByteString

Invariants on the definition of Bytestring:

184: measure fplen :: ForeignPtr a -> Int
185: 
186: data ByteString = PS
187:   { pay :: ForeignPtr Word8
188:   , off :: {v:Nat | v <= (fplen pay)}
189:   , len :: {v:Nat | off + v <= (fplen pay)} }

Allow us to enforce low-level memory safety.