pub fn check_contract<'tcx>( contract: &Contract<'tcx>, abstate_item: &AbstractStateItem<'tcx>, ) -> bool