More storage files spec
Closes #508 (closed) , #519 (closed) , #493 (closed) , #495 (closed) , #498 (closed) , #480 (closed) , #487 (closed)
Specification only (no proofs).
Edited by Guillaume Claret
Closes #508 (closed) , #519 (closed) , #493 (closed) , #495 (closed) , #498 (closed) , #480 (closed) , #487 (closed)
Specification only (no proofs).