private static @NotNull ContractProvider getArraycopyContract() {
    ContractValue src = ContractValue.argument(0);
    ContractValue srcPos = ContractValue.argument(1);
    ContractValue dest = ContractValue.argument(2);
    ContractValue destPos = ContractValue.argument(3);
    ContractValue length = ContractValue.argument(4);
    ContractValue srcLength = src.specialField(SpecialField.ARRAY_LENGTH);
    ContractValue dstLength = dest.specialField(SpecialField.ARRAY_LENGTH);
    return ContractProvider.of(
      singleConditionContract(srcPos, RelationType.GT, srcLength, fail()),
      singleConditionContract(destPos, RelationType.GT, dstLength, fail()),
      singleConditionContract(srcPos, RelationType.LT, ContractValue.zero(), fail()),
      singleConditionContract(destPos, RelationType.LT, ContractValue.zero(), fail()),
      singleConditionContract(length, RelationType.LT, ContractValue.zero(), fail()),
      singleConditionContract(length, RelationType.GT, srcLength, fail()),
      singleConditionContract(length, RelationType.GT, dstLength, fail())
    );
  }
private static @NotNull ContractProvider getArraycopyContract()