Add automatically generated Bolero harnesses

[cvick32]

Adds 228 Bolero harnesses and all corresponding TypeGenerator derivations. These harnesses were automatically generated by a tool currently under development by the Kani team.

Note that this was run a previous commit of Hifitime (tag: 4.0.0-alpha) to avoid any collisions with the automatically generated Kani harnesses.

Summary of running cargo test listed below.

failures:
    duration::bolero_harnesses::bolero_test_172_compose_f64
    duration::bolero_harnesses::bolero_test_176_total_nanoseconds
    duration::bolero_harnesses::bolero_test_177_try_truncated_nanoseconds
    duration::bolero_harnesses::bolero_test_178_truncated_nanoseconds
    duration::bolero_harnesses::bolero_test_184_subdivision
    duration::bolero_harnesses::bolero_test_185_floor
    duration::bolero_harnesses::bolero_test_186_ceil
    duration::bolero_harnesses::bolero_test_187_round
    duration::bolero_harnesses::bolero_test_188_approx
    duration::bolero_harnesses::bolero_test_192_eq
    epoch::bolero_harnesses::bolero_test_151_hours
    epoch::bolero_harnesses::bolero_test_152_minutes
    epoch::bolero_harnesses::bolero_test_154_milliseconds
    epoch::bolero_harnesses::bolero_test_156_nanoseconds
    epoch::bolero_harnesses::bolero_test_26_from_tai_seconds
    epoch::bolero_harnesses::bolero_test_27_from_tai_days
    epoch::bolero_harnesses::bolero_test_35_from_mjd_tai
    epoch::bolero_harnesses::bolero_test_36_from_mjd_in_time_scale
    epoch::bolero_harnesses::bolero_test_37_from_mjd_utc
    epoch::bolero_harnesses::bolero_test_38_from_mjd_gpst
    epoch::bolero_harnesses::bolero_test_39_from_mjd_qzsst
    epoch::bolero_harnesses::bolero_test_40_from_mjd_gst
    epoch::bolero_harnesses::bolero_test_41_from_mjd_bdt
    epoch::bolero_harnesses::bolero_test_42_from_jde_tai
    epoch::bolero_harnesses::bolero_test_43_from_jde_in_time_scale
    epoch::bolero_harnesses::bolero_test_44_from_jde_utc
    epoch::bolero_harnesses::bolero_test_45_from_jde_gpst
    epoch::bolero_harnesses::bolero_test_46_from_jde_qzsst
    epoch::bolero_harnesses::bolero_test_47_from_jde_gst
    epoch::bolero_harnesses::bolero_test_48_from_jde_bdt
    epoch::bolero_harnesses::bolero_test_49_from_tt_seconds
    epoch::bolero_harnesses::bolero_test_53_from_tdb_seconds
    epoch::bolero_harnesses::bolero_test_55_from_jde_et
    epoch::bolero_harnesses::bolero_test_56_from_jde_tdb
    epoch::bolero_harnesses::bolero_test_76_from_day_of_year
    timeseries::bolero_harnesses::bolero_test_213_next
    timeseries::bolero_harnesses::bolero_test_215_next_back
    weekday::bolero_harnesses::bolero_test_223_add
    weekday::bolero_harnesses::bolero_test_224_sub
    weekday::bolero_harnesses::bolero_test_225_add_assign
    weekday::bolero_harnesses::bolero_test_226_sub_assign

test result: FAILED. 187 passed; 41 failed; 0 ignored; 0 measured; 24 filtered out; finished in 17.03s

[ChristopherRabotin]

Hi Cole,

Thanks for the PR. Could you remind me the difference between kani and bolero? IIRC, kani is proof mechanism whereas bolero is closer to property testing. Is that right?

Further, is there any way to have bolero and kani work together in two different steps of the CI, or are they XOR'ing each other?

Thanks

[cvick32]

Hey Chris,

In this PR, I'm using bolero as a front-end for kani. Bolero is a generic front-end for property-based testing, fuzzing, and model checking. So, using the definitions in this PR, you could run cargo test to run the randomized tester in CI then run cargo bolero test --engine kani to run kani in CI.

Using the bolero definitions does not prevent proving properties with kani but rather unlocks randomized testing and fuzzing alongside kani. This blog post goes into more detail about using bolero and kani in tandem.

Thanks, Cole