( toplevel: &aiur::bytecode::Toplevel, fun_idx: aiur::bytecode::FunIdx, input: Vec<G>, io_buffer: &mut IOBuffer, use_bytecode: bool, )
| 397 | /// Rust-owned `EnvHandle`. `use_bytecode` selects the executor: |
| 398 | /// `false` = codegen'd IxVM kernel (`execute_ixvm`), |
| 399 | /// `true` = generic Aiur bytecode interpreter |
| 400 | /// (`Toplevel::execute`). |
| 401 | #[unsafe(no_mangle)] |
| 402 | extern "C" fn rs_aiur_toplevel_check_addr_with_env( |
| 403 | toplevel: LeanAiurToplevel<LeanBorrowed<'_>>, |
| 404 | fun_idx: LeanNat<LeanBorrowed<'_>>, |
| 405 | env_handle: LeanExternal< |
| 406 | ixvm_codegen::env_handle::EnvHandle, |
| 407 | LeanBorrowed<'_>, |
| 408 | >, |
| 409 | addr_bytes: LeanByteArray<LeanBorrowed<'_>>, |
| 410 | use_bytecode: bool, |
| 411 | ) -> LeanExcept<LeanOwned> { |
| 412 | let toplevel = decode_toplevel(&toplevel); |
| 413 | let fun_idx = lean_unbox_nat_as_usize(fun_idx.inner()); |
| 414 | let addr = match decode_addr(&addr_bytes) { |
| 415 | Ok(a) => a, |
| 416 | Err(e) => return LeanExcept::error_string(&e), |
| 417 | }; |
| 418 | let env = &env_handle.get().env; |
| 419 |
no test coverage detected