( arr: &LeanArray<LeanBorrowed<'_>>, )
| 747 | // for humans; f64's 52-bit mantissa is exact far past any real budget. |
| 748 | #[allow(clippy::cast_precision_loss)] |
| 749 | #[unsafe(no_mangle)] |
| 750 | extern "C" fn rs_aiur_toplevel_shard_check_batch( |
| 751 | toplevel_obj: LeanAiurToplevel<LeanBorrowed<'_>>, |
| 752 | fun_idx: LeanNat<LeanBorrowed<'_>>, |
| 753 | env_handle: LeanExternal< |
| 754 | ixvm_codegen::env_handle::EnvHandle, |
| 755 | LeanBorrowed<'_>, |
| 756 | >, |
| 757 | shards_blob: LeanByteArray<LeanBorrowed<'_>>, |
| 758 | use_bytecode: bool, |
| 759 | jobs: LeanNat<LeanBorrowed<'_>>, |
| 760 | commitment_parameters: LeanAiurCommitmentParameters<LeanBorrowed<'_>>, |
| 761 | fri_parameters: LeanAiurFriParameters<LeanBorrowed<'_>>, |
| 762 | max_ram_bytes: LeanNat<LeanBorrowed<'_>>, |
| 763 | ) -> LeanExcept<LeanOwned> { |
| 764 | use rayon::prelude::*; |
| 765 | let toplevel = decode_toplevel(&toplevel_obj); |
| 766 | let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); |
| 767 | let jobs = lean_unbox_nat_as_usize(jobs.inner()); |
| 768 | let max_ram_bytes = lean_unbox_nat_as_usize(max_ram_bytes.inner()); |
| 769 | let shards = match decode_addr_lists(shards_blob.as_bytes()) { |
no test coverage detected