Organize MCD specs taking advantage of proof dependencies

[ehildenb]

Blocked on: #2093

This PR takes advantage of the new proof dependency structure introduce here: #1926. In particular:

• For each contract in MCD, a new spec CONTRACT-ARITHMETIC-SPEC is created containing the internal arithmetic functions.
• For each proof in MCD, it imports the needed specs from the arithmetic spec or other contract specs.
• Master specs are created for each contract importing all the individual behavior specs.
• A single master spec is created for the MCD proof suite that imports all the contract specs.
• Update the proof harness to only run the single master spec.
• Proofs that are not passing are disabled (and their dependents).

This takes advantage of the topological sort on proof claims which allows discharging them in dependency order, and speeds up overall execution. The goal here is to provide a robust test of subproof structure.