Benchmarks

• Ghc.List, Data.List: size-related properties and termination

• Data.Splay: well-ordered trees and termination

• Data.Map: binary-search ordered trees and termination

• Vector-Algorithms: correctness of accessing, indexing and slicing

• Bytestring: size-based low-level memory safety and termination

• Text: size-based pointer-safety and termination

Invariants in 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.