[Certora] Documentation & cleaning

[QGarchery]

Done in this PR:

• [x] wait for certora-cli to catch up before merging this postponed and created an issue instead (see #407)
• [x] complete high level description
• [x] rename harness to helpers
• [x] use functions to return structs instead of splitting them every time
• [x] fix CI's warning
• [x] clarify the specification imports, see this comment. Done in 009227762711c53e25fb98e0c9e8210340d960ca
• [x] rename CI step from "Verify Rule [spec]" to "Verify [spec] specification"
• [x] update to the Tokens PR, in particular for the enabledHasConsistentAsset invariant