Sparse matrix formats are typically implemented with low-level imperative programs. The optimized nature of these implementations hides the structural organization of the sparse format and complicates its verification. We formalize a proof system based on parametric predicates for tracking relationship between mathematical vectors and their concrete representations. This proof theory automatically verifies full functional correctness of many formats. This document contains the theories described in Specifying and verifying sparse matrix codes by Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík,and Mooly Sagiv Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICP 2010) Pages 249 to 260 (doi: 10.1145/1863543.1863581) This formalization works with Isabelle 2015.