SpecAutomation

This module exercises the automatic specification application (applySpec'' and applySpec') on the store instruction and on every jump instruction shape, so that each branch of the instruction-dispatch in Tactics/ApplySpec.lean is covered by a proved Hoare triple.