#!/usr/bin/env bash
# flowrs-core's proofs: the widgets' index, range and geometry rules the interpreter and the
# generated code share (crates/flowrs-core/src/graph/value.rs, graph/widgets/{list,video,dsp,
# audio}.rs). Until Kani 0.68 `make verify` ran these as one `cargo kani -p flowrs-core`, with
# no memory budget; Kani 0.68 verifies harnesses in parallel by default, so each now has a cap
# and the run as a whole a total.
#
#   tools/kani-core.sh              # every harness
#   tools/kani-core.sh PATTERN...   # those whose name contains a pattern
#
# Budgets and results as tools/kani-env.sh describes: 16 GB per harness (KANI_MEM_GB), the
# run under memguard at KANI_TOTAL_GB, KANI_TIMEOUT (default 1800s) per harness, as many at
# once as fit; results in $KANI_OUT/core.json.
set -uo pipefail
cd "$(dirname "$0")/.."
. tools/kani-env.sh
kani_preflight || exit 1
KANI_TIMEOUT=${KANI_TIMEOUT:-1800s}
TABLE=(
  graph::value::proofs::the_intersection_never_exceeds_the_union:16
  graph::value::proofs::overlap_does_not_depend_on_which_box_is_asked:16
  graph::value::proofs::px_is_in_bounds_for_every_coordinate_inside_the_image:16
  graph::value::proofs::nearest_source_stays_inside_the_source_image:16
  graph::value::proofs::nearest_source_never_runs_backwards:16
  graph::value::proofs::crop_rect_answers_none_or_a_rectangle_that_fits:16
  graph::widgets::list::proofs::resolve_index_never_points_outside_the_list:16
  graph::widgets::list::proofs::slice_range_is_always_a_range_rust_accepts:16
  graph::widgets::video::proofs::the_shared_nearest_source_stays_inside_the_source:16
  graph::widgets::video::proofs::the_shared_nearest_source_never_runs_backwards:16
  graph::widgets::video::proofs::the_shared_nearest_source_never_truncates_a_large_product:16
  graph::widgets::video::proofs::resize_produces_exactly_the_frame_that_was_asked_for:16
  graph::widgets::dsp::proofs::the_bit_reversal_is_a_permutation:16
  graph::widgets::dsp::proofs::every_biquad_the_panel_can_build_is_stable:16
  graph::widgets::dsp::proofs::rbj_terms_are_finite_for_every_cutoff_and_q:16
  graph::widgets::audio::proofs::fft_window_is_always_a_power_of_two_that_fits:16
  graph::widgets::audio::proofs::stft_never_reads_past_the_end_of_its_input:16
  graph::widgets::audio::proofs::stft_refuses_a_frame_longer_than_its_input:16
  graph::widgets::audio::proofs::resample_linear_cannot_panic_for_any_rate_the_panel_allows:16
  graph::widgets::audio::proofs::an_empty_input_resamples_to_an_empty_output:16
)
kani_select "$@"
kani_go core ${SELECTED[@]+"${SELECTED[@]}"} -- cargo kani -p flowrs-core