pub unsafe extern "C" fn Hacl_SHA3_sha3_384(
    inputByteLen: u32,
    input: *mut u8,
    output: *mut u8
)