Upload Code
Package Summary Specifications Assumptions Verification Results Our open standard Verify it yourself Install Docker Docker image

Formal Verification Certificate

Dalek Verus Latest — certified snapshot

This software package satisfies these specifications with these assumptions (see below). Specifically, everything shown with green text or background is auto-certified by VeriLib (and you can trivially re-verify it yourself), while what's shown with white background are unverified claims by the project team, included for pedagogy.

Certification date April 15, 2026
Package commit d4c6a94
Functions Verified 1094/1094
Ethereum Proof Etherscan
Package Summary
GitHub VeriLib

This repository is a formal verification project for the curve25519-dalek cryptographic library, using Verus, a verification tool for Rust that checks specifications and proofs via SMT solving. The original dalek library provides the implementations; this project adds machine-checked specifications and proofs that those implementations are correct.

The verified code covers a scalar field (integers modulo the group order), a finite field (integers modulo 2^255 - 19), and elliptic curve point operations in three forms: Edwards, Montgomery, and Ristretto. Verus proofs establish correctness of field arithmetic, scalar operations, group laws, and conversions between curve representations.

This version targets the "Lite" subset of dalek, forked from Signal's fork at tag signal-curve25519-4.1.3. It retains only the serial u64 backend and the core group arithmetic that Signal messenger relies on, reducing the verification surface to what matters most for a widely deployed cryptographic dependency.

Of the 1094 verified functions, 280 are from the original Rust source, and 814 are helper lemmas and functions which were added for verification purposes.

Applications:

  • Scalars can be used in protocols to store private keys and cryptographically secure random numbers.
  • Curve points can be used to represent public keys or encode private data in a secure way.
  • Scalar multiplication is used for multiple cryptographic operations, such as encoding, decoding, shared key generation, zero-knowledge proofs, private-key signing and verification.

Verified Dalek Functions

Specifications

An easier way to view the specifications is to click on the corresponding functions in VeriLib.

Assumptions
fact_check
Verus Verifier

We assume that the Verus verification system, including its standard library (vstd), correctly implements its verification logic and sound reasoning principles.

bug_report
Z3 SMT Solver

Verus relies on the Z3 automated theorem prover for checking logical conditions. We assume that Z3 correctly implements SMT solving algorithms.

view_in_ar
Rust Compiler

We assume that the Rust compiler correctly translates our verified code into machine instructions, and that it respects the semantics Verus reasons about.

computer
Hardware

Like for any software, we assume trust that the hardware correctly executes the compiled machine code.

show_chart
Cryptographic Assumptions

We assume the mathematical foundations of elliptic curve cryptography, including the hardness of the discrete logarithm problem on Curve25519.

rule
Known Properties

Mathematical truths whose known proofs are not replicated within this project.

inventory_2
Dependencies

We assume correctness of the dependencies listed in the Cargo.toml file: subtle, zeroize, sha2 and the Verus standard library.

extension
Rust Features

Some internal functions are trusted without proof because they use Rust features Verus does not yet support (iterators, slice conversions, trait dispatch). These are marked external_body with manually written postconditions.

Verification Results

Below are the formal verification results. Please check if the first test line says "VerificationSuccess": true.

Manifest
{
  "VerificationSuccess": true,
  "atoms_note": "Verified keys: unified verification-status verified, error/failed (or similar), or proofs.verified; excludes unverified/trusted. Manifest counts: unified data — TBV = verified + error/errored; list = verified keys only. [worker] Counts recomputed from probe-verus extract on disk (status-only rules).",
  "branch": "main",
  "build_arg_commit": "d4c6a944625d7e2473899e28a5129baa05cd3080",
  "cargo_package": "curve25519-dalek",
  "cert_readme_badge_alt": "VeriLib Certified",
  "cert_readme_badge_image_url": "https://verilib.org/assets/img/verilib-certified-badge-wide.svg",
  "cert_readme_page_url": "https://verilib.org/cert/5132",
  "commit": "d4c6a944625d7e2473899e28a5129baa05cd3080",
  "commit_date_utc": "2026-04-14T11:34:16+02:00",
  "image": "cert-probe-docker",
  "image_build_date_utc": "2026-04-15T13:33:28Z",
  "probe_extract_completed_at_utc": "2026-04-15T13:33:28Z",
  "probe_verus_version": "6.9.1",
  "repo": "https://github.com/Beneficial-AI-Foundation/dalek-verus.git",
  "source_tree_sha256": "1d9780b9ea2e4d6ca675f349f222227f74f40ad980a4145f0c0039f29b91c918",
  "to_be_verified": 1094,
  "unified_extract_json_path": "/opt/cert-target-src/.verilib/probes/verus_curve25519-dalek_4.1.3.json",
  "unified_extract_json_sha256": "77145bad148622ead7c6e2ba0910c25a1aac768ee895e9d18721ba312692df7b",
  "verification_source": "unified_extract_json",
  "verified_functions": [
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_add_bounds_propagate()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_edwards_point_weaken_to_54()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_fe51_limbs_bounded_weaken()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_field51_add()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_field_add_16p_no_overflow()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_field_element51_eq_from_limbs_eq()",
    "probe:curve25519-dalek/4.1.3/add_lemmas/field_lemmas/lemmas/lemma_sum_of_limbs_bounded_from_fe51_bounded()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_as_bytes_boundaries1()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_as_bytes_boundaries2()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_as_bytes_equals_spec_fe51_to_bytes()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_as_bytes_from_bytes_roundtrip()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_canonical_bytes_bit255_zero()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_canonical_check_backward()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_ct_eq_iff_canonical_nat()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_fe51_to_bytes_equal_implies_field_element_equal()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_field_element_equal_implies_fe51_to_bytes_equal()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_from_bytes_as_bytes_roundtrip()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_is_negative_equals_parity()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_seq_eq_implies_array_eq()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_seq_to_array_32_roundtrip()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_spec_fe51_to_bytes_matches_array()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_u8_32_as_nat_of_spec_fe51_to_bytes()",
    "probe:curve25519-dalek/4.1.3/as_bytes_lemmas/field_lemmas/lemmas/lemma_xor_sign_bit_preserves_y()",
    "probe:curve25519-dalek/4.1.3/backend/get_selected_backend()",
    "probe:curve25519-dalek/4.1.3/backend/pippenger_optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/backend/straus_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/backend/straus_optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/backend/variable_base_mul()",
    "probe:curve25519-dalek/4.1.3/backend/vartime_double_base_mul()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_compress_body_inv_zero()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_compress_equals_compress_of_double()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_encoding_equals_standard_encoding()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_identity_projective()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_std_case_dispatch()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_batch_std_final_matching()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_curve_eq_batch_identity()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_degenerate_double_compresses_to_zero()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_doubled_affine_from_batch_state()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_dt_squared_factor()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_encoding_equality_core()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_no_rotation_algebraic_setup()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_no_rotation_case()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_no_rotation_s_matching()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_ristretto_compress_affine_zero_xy()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_rotation_algebraic_setup()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_rotation_case()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_rotation_case_body()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_rotation_case_final()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_rotation_s_matching()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_segre_derives_t()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_u1_u2_sq_factoring()",
    "probe:curve25519-dalek/4.1.3/batch_compress_lemmas/ristretto_lemmas/lemmas/lemma_z_inv_std_is_one()",
    "probe:curve25519-dalek/4.1.3/batch_invert_lemmas/field_lemmas/lemmas/lemma_backward_step()",
    "probe:curve25519-dalek/4.1.3/batch_invert_lemmas/field_lemmas/lemmas/lemma_is_zero_iff_canonical_nat_zero()",
    "probe:curve25519-dalek/4.1.3/batch_invert_lemmas/field_lemmas/lemmas/lemma_nat_zero_implies_all_zero_bytes()",
    "probe:curve25519-dalek/4.1.3/batch_invert_lemmas/field_lemmas/lemmas/lemma_partial_product_nonzeros_is_nonzero()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_as_nat_eq_bits_from_index()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_as_nat_lt_pow2_255_implies_msb_false()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_as_nat_rec_eq_pow2_mul_bits_from_index()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_be_as_nat_eq_bits_from_index()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_chunks_eq_bytes_prefix()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_from_bytes_eq_u8_32_as_nat()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_from_index_eq_byte_bits()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_bits_from_index_split()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_byte_bits_value_full()",
    "probe:curve25519-dalek/4.1.3/bits_as_nat_lemmas/common_lemmas/lemmas/lemma_byte_bits_value_is_mod()",
    "probe:curve25519-dalek/4.1.3/bytes_to_scalar_lemmas/scalar_byte_lemmas/lemmas/lemma_byte_to_word_step()",
    "probe:curve25519-dalek/4.1.3/bytes_to_scalar_lemmas/scalar_byte_lemmas/lemmas/lemma_bytes_to_word_equivalence()",
    "probe:curve25519-dalek/4.1.3/bytes_to_scalar_lemmas/scalar_byte_lemmas/lemmas/lemma_words_to_scalar()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_all_carries_bounded_by_3()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_bounded_shr_51()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_carry_propagation_is_division()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_carry_propagation_setup()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_compute_q()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_q_biconditional()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_q_is_binary()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_radix51_remainder_bound()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_radix51_telescoping_direct()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_radix51_telescoping_expansion()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_single_stage_division()",
    "probe:curve25519-dalek/4.1.3/compute_q_lemmas/field_lemmas/lemmas/lemma_stage_division_theorem()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_bridge_local_pow2_d2()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_edwards_d2_is_2d()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_edwards_d2_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_edwards_d2_limbs_bounded_54()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_edwards_d_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_edwards_d_limbs_bounded_54()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/edwards_lemmas/lemmas/lemma_scalar_as_nat_basepoint_order_private_equals_group_order()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_bridge_local_pow2()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_d_minus_one_squared_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_d_minus_one_squared_value()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_d_plus_one_nonzero()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_elligator_constants_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_invsqrt_a_minus_d_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_minus_one_field_element_value()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_minus_one_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_montgomery_a_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_montgomery_a_neg_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_one_field_element_value()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_one_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_one_minus_d_squared_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_one_minus_d_squared_value()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_sqrt_ad_minus_one_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_sqrt_ad_minus_one_nonzero()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_zero_field_element_value()",
    "probe:curve25519-dalek/4.1.3/constants_lemmas/field_lemmas/lemmas/lemma_zero_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/coset_lemmas/ristretto_lemmas/lemmas/lemma_edge_coset_contains_e4()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_affine_curve_implies_projective()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_affine_niels_affine_equals_edwards_affine()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_affine_to_extended_valid()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_completed_point_ratios()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_double_distributes()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_double_identity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_double_is_scalar_mul_2()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_canonical()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_commutative()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_four_way_swap()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_identity_left()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_identity_right()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_identity_right_canonical()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_affine_when_z_is_one()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_double_identity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_double_of_add()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_additive()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_canonical()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_composition()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_identity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_pow2_succ()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_signed_canonical()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_signed_composition()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_succ()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_edwards_to_montgomery_correspondence()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_four_doublings_is_mul_16()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_affine_niels_is_identity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_affine_niels_valid()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_is_valid_extended()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_on_curve()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_projective_niels_is_identity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_projective_niels_valid()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_identity_projective_point_properties()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_neg_distributes_over_add()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_neg_of_signed_scalar_mul()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negate_affine_niels_is_edwards_neg()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negate_affine_niels_preserves_validity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negate_projective_niels_is_edwards_neg()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negate_projective_niels_preserves_validity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negation_preserves_curve()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_negation_preserves_extended_validity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_projective_implies_affine_on_curve()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_projective_niels_affine_equals_edwards_affine()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_recover_xy_from_niels_encoding()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_scalar_mul_distributes_over_neg()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_unique_x_with_parity()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_valid_extended_point_affine_on_curve()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_x_zero_implies_y_squared_one()",
    "probe:curve25519-dalek/4.1.3/curve_equation_lemmas/edwards_lemmas/lemmas/lemma_z_one_affine_implies_projective()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&AffineNielsPoint#Neg<AffineNielsPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&CompletedPoint#CompletedPoint<EdwardsPoint>#as_extended()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&CompletedPoint#CompletedPoint<ProjectivePoint>#as_projective()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&EdwardsPoint#Add<&AffineNielsPoint>#add()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&EdwardsPoint#Add<&ProjectiveNielsPoint>#add()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&EdwardsPoint#Sub<&AffineNielsPoint>#sub()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&EdwardsPoint#Sub<&ProjectiveNielsPoint>#sub()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&ProjectiveNielsPoint#Neg<ProjectiveNielsPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&ProjectivePoint#ProjectivePoint<CompletedPoint>#double()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/&ProjectivePoint#ProjectivePoint<EdwardsPoint>#as_extended()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/AffineNielsPoint#ConditionallySelectable<&Self>#conditional_assign()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/AffineNielsPoint#ConditionallySelectable<&Self>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/AffineNielsPoint#Default<AffineNielsPoint>#default()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/AffineNielsPoint#Identity<AffineNielsPoint>#identity()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/AffineNielsPoint#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectiveNielsPoint#ConditionallySelectable<&Self>#conditional_assign()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectiveNielsPoint#ConditionallySelectable<&Self>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectiveNielsPoint#Default<ProjectiveNielsPoint>#default()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectiveNielsPoint#Identity<ProjectiveNielsPoint>#identity()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectiveNielsPoint#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectivePoint#Identity<ProjectivePoint>#identity()",
    "probe:curve25519-dalek/4.1.3/curve_models/serial/backend/ProjectivePoint#ValidityCheck<bool>#is_valid()",
    "probe:curve25519-dalek/4.1.3/decompress/edwards/step_1()",
    "probe:curve25519-dalek/4.1.3/decompress/edwards/step_2()",
    "probe:curve25519-dalek/4.1.3/decompress/ristretto/step_1()",
    "probe:curve25519-dalek/4.1.3/decompress/ristretto/step_2()",
    "probe:curve25519-dalek/4.1.3/decompress_lemmas/edwards_lemmas/lemmas/lemma_decompress_field_element_sign_bit()",
    "probe:curve25519-dalek/4.1.3/decompress_lemmas/edwards_lemmas/lemmas/lemma_decompress_spec_matches_point()",
    "probe:curve25519-dalek/4.1.3/decompress_lemmas/edwards_lemmas/lemmas/lemma_decompress_valid_branch()",
    "probe:curve25519-dalek/4.1.3/decompress_lemmas/edwards_lemmas/lemmas/lemma_sign_bit_after_conditional_negate()",
    "probe:curve25519-dalek/4.1.3/decompress_lemmas/edwards_lemmas/lemmas/lemma_to_edwards_correctness()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_div_of_sum()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_div_strictly_bounded()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_divisibility_factor()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_double_neg_mod()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_int_nat_mod_equiv()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mod_add_eq()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mod_diff_factor()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mod_sum_both_divisible()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mod_sum_factor()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mul_by_minus_one_is_negation()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mul_distributes_over_neg_mod()",
    "probe:curve25519-dalek/4.1.3/div_mod_lemmas/common_lemmas/lemmas/lemma_mul_le_implies_div_le()",
    "probe:curve25519-dalek/4.1.3/double_correctness/edwards_lemmas/lemmas/lemma_double_projective_completed_valid()",
    "probe:curve25519-dalek/4.1.3/edwards/&CompressedEdwardsY#CompressedEdwardsY<Option<EdwardsPoint>>#decompress()",
    "probe:curve25519-dalek/4.1.3/edwards/&CompressedEdwardsY#CompressedEdwardsY<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/edwards/&CompressedEdwardsY#CompressedEdwardsY<[u8;/32]>#to_bytes()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsBasepointTable#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#Add<&EdwardsPoint>#add()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<AffineNielsPoint>#as_affine_niels()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<CompressedEdwardsY>#compress()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<EdwardsPoint>#double()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<EdwardsPoint>#mul_by_cofactor()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<EdwardsPoint>#mul_by_pow_2()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<MontgomeryPoint>#to_montgomery()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<ProjectiveNielsPoint>#as_projective_niels()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<ProjectivePoint>#as_projective()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<bool>#is_small_order()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#EdwardsPoint<bool>#is_torsion_free()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#Neg<EdwardsPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/edwards/&EdwardsPoint#Sub<&EdwardsPoint>#sub()",
    "probe:curve25519-dalek/4.1.3/edwards/&Scalar#Mul<&EdwardsBasepointTable>#mul()",
    "probe:curve25519-dalek/4.1.3/edwards/&Scalar#Mul<&EdwardsPoint>#mul()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY#ConstantTimeEq<&CompressedEdwardsY>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY#Default<CompressedEdwardsY>#default()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY#Identity<CompressedEdwardsY>#identity()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY#TryFrom<&[u8]>#try_from()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/edwards/CompressedEdwardsY<&[u8]>#from_slice()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsBasepointTable#BasepointTable<&EdwardsPoint>#create()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsBasepointTable#BasepointTable<&Scalar>#mul_base()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsBasepointTable#BasepointTable<EdwardsPoint>#basepoint()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#AddAssign<&EdwardsPoint>#add_assign()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#ConditionallySelectable<&EdwardsPoint>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#ConstantTimeEq<&EdwardsPoint>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#Default<EdwardsPoint>#default()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#EdwardsPoint<[u8;/32]>#mul_clamped()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#Identity<EdwardsPoint>#identity()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#MulAssign<&Scalar>#mul_assign()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#Neg<EdwardsPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#PartialEq<&EdwardsPoint>#eq()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#SubAssign<&EdwardsPoint>#sub_assign()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#Sum<I>#sum()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#ValidityCheck<bool>#is_valid()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<&EdwardsPoint>#vartime_double_scalar_mul_basepoint()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<&Scalar>#mul_base()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<&[EdwardsPoint]>#sum_of_slice()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<&[u8]>#nonspec_map_to_curve_verus()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<J>#multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<J>#optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/edwards/EdwardsPoint<[u8;/32]>#mul_base_clamped()",
    "probe:curve25519-dalek/4.1.3/edwards_specs/specs/lemma_ed25519_basepoint_y()",
    "probe:curve25519-dalek/4.1.3/edwards_specs/specs/lemma_identity_affine_coords()",
    "probe:curve25519-dalek/4.1.3/edwards_specs/specs/lemma_unfold_edwards()",
    "probe:curve25519-dalek/4.1.3/elligator_lemmas/ristretto_lemmas/lemmas/lemma_elligator_nonzero_denominators()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<(Choice,/FieldElement)>#invsqrt()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<(FieldElement,/FieldElement)>#pow22501()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<Choice>#is_negative()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<Choice>#is_zero()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<FieldElement>#invert()",
    "probe:curve25519-dalek/4.1.3/field/&FieldElement51#FieldElement51<FieldElement>#pow_p58()",
    "probe:curve25519-dalek/4.1.3/field/FieldElement51#ConstantTimeEq<&FieldElement>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/field/FieldElement51#PartialEq<&FieldElement>#eq()",
    "probe:curve25519-dalek/4.1.3/field/FieldElement51#batch_invert()",
    "probe:curve25519-dalek/4.1.3/field/FieldElement51<(Choice,/FieldElement)>#sqrt_ratio_i()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#Add<&FieldElement51>#add()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#FieldElement51<FieldElement51>#square()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#FieldElement51<FieldElement51>#square2()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#FieldElement51<u32>#pow2k()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#Mul<&FieldElement51>#mul()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#Neg<FieldElement51>#neg()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&FieldElement51#Sub<&FieldElement51>#sub()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/&mut/FieldElement51#FieldElement51#negate()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#AddAssign<&FieldElement51>#add_assign()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#ConditionallySelectable<&FieldElement51>#conditional_assign()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#ConditionallySelectable<&FieldElement51>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#ConditionallySelectable<&FieldElement51>#conditional_swap()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#FieldElement51<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#MulAssign<&FieldElement51>#mul_assign()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#SubAssign<&FieldElement51>#sub_assign()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51<&[u8;/32]>#from_bytes()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51<FieldElement51>#from_limbs()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/FieldElement51<[u64;/5]>#reduce()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/load8_at()",
    "probe:curve25519-dalek/4.1.3/field/u64/serial/backend/m()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_a_times_inv_ab_is_inv_b()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_add_self_eq_double()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_affine_zero_implies_proj_zero()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_cancel_common_factor()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_cross_mul_iff_div_eq()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_div_mul_cancel()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_double_negation()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_factor_result_component_add()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_factor_result_component_sub()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_abs_mul_sign()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_abs_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_add_recover_double()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_assoc()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_canonical_left()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_comm()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_sub_cancel()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_sub_rearrange()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_add_sub_recover_double()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_curve_eq_x2v_eq_u()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_curve_point_implies_valid_y()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_diff_of_squares()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_element_reduced()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_halve_double()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_inv_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_inv_one()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_assoc()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_comm()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_distributes_over_add()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_distributes_over_sub_right()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_exchange()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_left_cancel()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_one_left()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_one_right()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_square_canonical()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_zero_left()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_mul_zero_right()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_neg_mul_left()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_neg_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_neg_nonzero()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_square_nonzero()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_square_of_pow_mod()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_sub_add_cancel()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_sub_add_common_right()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_sub_antisymmetric()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_sub_eq_add_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_sub_self()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_field_y_sq_one_implies_x_zero()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_foil_add()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_foil_sub()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_foil_sum_reorder()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_four_factor_rearrange()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_inv_mul_cancel()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_inv_of_inv()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_inv_of_product()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_mul_one_identity()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_neg_a_times_inv_ab()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_neg_one_times_is_neg()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_neg_square_eq()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_nonzero_from_mod()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_nonzero_product()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_one_and_neg_one_square_to_one()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pm_minus_mp()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pm_mp_neg_setup()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pm_plus_mp()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pp_minus_mm()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pp_mm_decompose()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_pp_plus_mm()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_product_of_squares_eq_square_of_product()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_quotient_of_squares()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_reassociate_2_z_num()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_reverse_distribute_add()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_reverse_distribute_sub()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_solve_for_left_factor()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_square_matches_field_square()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_square_mod_noop()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_square_sum_expansion()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_sub_neg_eq_add()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_sum_sq_minus_diff_sq()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_swap_sub_negates_mul()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_two_times_one_minus_t()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_two_times_one_plus_t()",
    "probe:curve25519-dalek/4.1.3/field_algebra_lemmas/field_lemmas/lemmas/lemma_v_times_sq_uv3_eq_u_times_w()",
    "probe:curve25519-dalek/4.1.3/field_specs/specs/field_inv_property()",
    "probe:curve25519-dalek/4.1.3/field_specs/specs/field_inv_unique()",
    "probe:curve25519-dalek/4.1.3/field_specs/specs/field_inv_zero()",
    "probe:curve25519-dalek/4.1.3/field_specs/specs/lemma_fermat_for_p()",
    "probe:curve25519-dalek/4.1.3/field_specs/specs/lemma_inverse_unique_core()",
    "probe:curve25519-dalek/4.1.3/field_specs_u64/specs/l51_bit_mask_lt()",
    "probe:curve25519-dalek/4.1.3/field_specs_u64/specs/p_gt_2()",
    "probe:curve25519-dalek/4.1.3/field_specs_u64/specs/pow255_gt_19()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_as_nat_32_mod_255()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_assemble_mod_div()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_assemble_pow_a_pow()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_from_u8_32_as_nat()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_from_u8_32_as_nat_01()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_from_u8_32_as_nat_012()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_from_u8_32_as_nat_0123()",
    "probe:curve25519-dalek/4.1.3/from_bytes_lemmas/field_lemmas/lemmas/lemma_from_u8_32_as_nat_01234()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_correctness()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_equals_field_inv()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_exponent_arithmetic()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_is_multiplicative_inverse()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_power_chain()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_invert_zero_case()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_multiply_by_base_power_addition()",
    "probe:curve25519-dalek/4.1.3/invert_lemmas/field_lemmas/lemmas/lemma_pow2k_to_field_element()",
    "probe:curve25519-dalek/4.1.3/iterator_specs/specs/lemma_sum_ristretto_edwards_equiv()",
    "probe:curve25519-dalek/4.1.3/jacobi_quartic/lizard/&JacobiPoint#JacobiPoint<(Choice,/FieldElement)>#elligator_inv()",
    "probe:curve25519-dalek/4.1.3/jacobi_quartic/lizard/&JacobiPoint#JacobiPoint<JacobiPoint>#dual()",
    "probe:curve25519-dalek/4.1.3/jacobi_quartic/lizard/lemma_elligator_inv_spec_anchor()",
    "probe:curve25519-dalek/4.1.3/lemmas/common_lemmas/bit_lemmas/lemma_mask_bound_implies_bit_clean()",
    "probe:curve25519-dalek/4.1.3/lemmas/common_lemmas/bit_lemmas/lemma_mask_or_bound()",
    "probe:curve25519-dalek/4.1.3/lemmas/common_lemmas/bit_lemmas/lemma_or_bit()",
    "probe:curve25519-dalek/4.1.3/lemmas/common_lemmas/bit_lemmas/lemma_or_bit_all()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_5_bytes_reconstruct()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_5_bytes_scale()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_6_bytes_reconstruct()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_boundary_byte_combines()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_byte_extraction_commutes_with_mod()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_byte_from_limb_shift()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_byte_sum_equals_limb_sum()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limb0_contribution_correctness()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limb1_contribution_correctness()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limb2_contribution_correctness()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limb3_contribution_correctness()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limb4_contribution_correctness()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_limbs_to_bytes()",
    "probe:curve25519-dalek/4.1.3/limbs_to_bytes_lemmas/field_lemmas/lemmas/lemma_sum_equals_byte_nat()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_candidate_from_jq_spec()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_coset_bridge()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_decode_candidate_preimage()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_dp1_over_dm1_limbs_bounded_51()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_elligator_inv_algebraic()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_even_is_slot_in_coset()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_exec_ok_matches_spec_slot()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_h_equals_spec_lizard_fe_bytes()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_invsqrt_bridge()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jacobi_dual_same_edwards()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jacobi_quartic_edge_values()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jacobi_to_edwards_affine_s_canonical_zero()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jacobi_to_edwards_affine_s_zero()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jacobi_to_edwards_affine_y_zero_when_s_sq_one()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jq_edge_case_values()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_jq_four_torsion_images()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_mdouble_invsqrt_a_minus_d_bounded_51()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_midouble_invsqrt_a_minus_d_bounded_51()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_minvsqrt_one_plus_d_bounded_51()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_odd_is_slot_in_coset()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_partial_count_full()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_spec_lizard_fe_bytes_canonical()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_spec_lizard_fe_bytes_injective()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_sqrt_id_limbs_bounded_52()",
    "probe:curve25519-dalek/4.1.3/lizard_lemmas/lemmas/lemma_zero_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/&RistrettoPoint#RistrettoPoint<(u8,/[FieldElement;/8])>#elligator_ristretto_flavor_inverse()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/&RistrettoPoint#RistrettoPoint<(u8,/[[u8;/32];/8])>#decode_253_bits()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/&RistrettoPoint#RistrettoPoint<Option<[u8;/16]>>#lizard_decode_verus()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/&RistrettoPoint#RistrettoPoint<[EdwardsPoint;/4]>#xcoset4()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/RistrettoPoint#RistrettoPoint<[JacobiPoint;/4]>#to_jacobi_quartic_ristretto()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/RistrettoPoint<&[u8;/16]>#lizard_encode_verus()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/RistrettoPoint<&[u8;/32]>#encode_253_bits()",
    "probe:curve25519-dalek/4.1.3/lizard_ristretto/lizard/RistrettoPoint<&[u8;/32]>#from_uniform_bytes_single_elligator()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_decode_ristretto_none()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_decode_ristretto_sound()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_decode_ristretto_witness()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_decode_sound()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_roundtrip()",
    "probe:curve25519-dalek/4.1.3/lizard_specs/specs/lemma_lizard_roundtrip_ristretto()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb0()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb1()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb2()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb3()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb4()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb_X()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_limb_base()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_plus_fits_u64()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_plus_version_is_spec()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_plus_version_is_spec_aux()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_plus_version_rec_is_bounded()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_rec_version_is_exec()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_at_versions_equivalent()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_plus_ver_div_mod()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_shift_mod()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_load8_shift_mod_aux()",
    "probe:curve25519-dalek/4.1.3/load8_lemmas/field_lemmas/lemmas/lemma_spec_load8_at_fits_u64()",
    "probe:curve25519-dalek/4.1.3/mask_lemmas/common_lemmas/lemmas/lemma_low_bits_mask_increases()",
    "probe:curve25519-dalek/4.1.3/montgomery/&MontgomeryPoint#MontgomeryPoint<&[bool]>#mul_bits_be()",
    "probe:curve25519-dalek/4.1.3/montgomery/&MontgomeryPoint#MontgomeryPoint<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/montgomery/&MontgomeryPoint#MontgomeryPoint<[u8;/32]>#to_bytes()",
    "probe:curve25519-dalek/4.1.3/montgomery/&MontgomeryPoint#MontgomeryPoint<u8>#to_edwards()",
    "probe:curve25519-dalek/4.1.3/montgomery/&MontgomeryPoint#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/montgomery/&ProjectivePoint#ProjectivePoint<MontgomeryPoint>#as_affine()",
    "probe:curve25519-dalek/4.1.3/montgomery/&Scalar#Mul<&MontgomeryPoint>#mul()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#ConstantTimeEq<&MontgomeryPoint>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#Default<MontgomeryPoint>#default()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#Hash<&H>#hash()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#Identity<MontgomeryPoint>#identity()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#MontgomeryPoint<[u8;/32]>#mul_clamped()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#MulAssign<&Scalar>#mul_assign()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#PartialEq<&MontgomeryPoint>#eq()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint<&Scalar>#mul_base()",
    "probe:curve25519-dalek/4.1.3/montgomery/MontgomeryPoint<[u8;/32]>#mul_base_clamped()",
    "probe:curve25519-dalek/4.1.3/montgomery/ProjectivePoint#ConditionallySelectable<&ProjectivePoint>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/montgomery/ProjectivePoint#Default<ProjectivePoint>#default()",
    "probe:curve25519-dalek/4.1.3/montgomery/ProjectivePoint#Identity<ProjectivePoint>#identity()",
    "probe:curve25519-dalek/4.1.3/montgomery/differential_add_and_double()",
    "probe:curve25519-dalek/4.1.3/montgomery/elligator_encode()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_bridge_local_pow2_m()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_canonical_montgomery_lift_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_canonical_scalar_mul_u_coord_reduced()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_canonical_sqrt_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_edwards_basepoint_maps_to_montgomery_basepoint()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_elligator_never_minus_one()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_eps_when_d_is_minus_one()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_field_sqrt_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_inv_preserves_non_qr()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_a_neg_is_neg_a()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_a_value()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_add_identity()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_add_identity_left()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_add_inverse()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_add_u_coord_reduced()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_add_zero_point_doubles_to_infinity()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_scalar_mul_add()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_scalar_mul_double()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_scalar_mul_one()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_scalar_mul_succ()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_montgomery_scalar_mul_zero_point_closed()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_nonsquare_branch_r_sq()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_p_gt_small()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_projective_represents_implies_u_coordinate()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_u_coordinate_scalar_mul_canonical_lift_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_curve_lemmas/lemmas/lemma_xdbl_degenerate_gives_w_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_lemmas/lemmas/lemma_ladder_invariant_swap()",
    "probe:curve25519-dalek/4.1.3/montgomery_lemmas/lemmas/lemma_rr_equals_radix_squared()",
    "probe:curve25519-dalek/4.1.3/montgomery_lemmas/lemmas/lemma_zero_limbs_is_zero()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_chain_exp_is_l_minus_2()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_exponent_chain_implies_montgomery_inverse()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_montgomery_mul_exponent_add()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_montgomery_square_exponent_double()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_pow2_chain_multipliers()",
    "probe:curve25519-dalek/4.1.3/montgomery_pow_chain_lemmas/lemmas/lemma_square_multiply_exponent_compose()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_bounded_product_satisfies_input_bounds()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_canonical_product_satisfies_canonical_bound()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_carry8_bound()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_carry_shift_to_nat()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_identity_array_satisfies_canonical_bound()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_identity_array_satisfies_input_bounds()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_l_limb4_is_pow2_44()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_montgomery_reduce_post_sub()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_montgomery_reduce_pre_sub()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_mul_internal_limbs_bounds()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_part1_correctness()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_part1_sum_divisible_by_pow2_52()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_part2_bounds()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_r4_bound_from_canonical()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_two_l_div_pow2_208_eq_pow2_45()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_lemmas/scalar_lemmas_/lemmas/lemma_u128_truncate_and_mask()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part1_chain_lemmas/scalar_lemmas_/lemmas/lemma_n_times_l_expansion()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part1_chain_lemmas/scalar_lemmas_/lemmas/lemma_part1_chain_divisibility()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part1_chain_lemmas/scalar_lemmas_/lemmas/lemma_part1_telescoping_expansion()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part1_chain_lemmas/scalar_lemmas_/lemmas/lemma_poly_mul_5x5_decomposition()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part2_chain_lemmas/scalar_lemmas_/lemmas/lemma_part2_carry_cancellation()",
    "probe:curve25519-dalek/4.1.3/montgomery_reduce_part2_chain_lemmas/scalar_lemmas_/lemmas/lemma_part2_chain_quotient()",
    "probe:curve25519-dalek/4.1.3/montgomery_specs/specs/lemma_x25519_basepoint_u_is_9()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_basepoint_table_select()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_edwards_scalar_mul_signed_of_scalar_mul()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_even_sum_up_to_correct()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_even_sum_up_to_step_even()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_even_sum_up_to_step_odd()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_odd_sum_up_to_canonical()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_odd_sum_up_to_correct()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_pippenger_partial_step_even()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_pippenger_partial_step_odd()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_pippenger_sum_correct()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_pippenger_sum_correct_signed()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_radix16_even_scalar_step()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_radix16_odd_scalar_step()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_radix16_even_odd()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_select_is_signed_scalar_mul()",
    "probe:curve25519-dalek/4.1.3/mul_base_lemmas/edwards_lemmas/lemmas/lemma_select_projective_is_signed_scalar_mul()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_m()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_commutative_8_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_3_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_4_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_5_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_6_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_7_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_distributive_8_terms()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_le()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_lt()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_quad_prod()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_si_vi_and_reorder()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_mul_w0_and_reorder()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_nat_distributive()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/common_lemmas/lemmas/lemma_product_square_factorize()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/field_lemmas/lemmas/lemma_mul_boundary()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/field_lemmas/lemmas/lemma_mul_c_i_0_bounded()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/field_lemmas/lemmas/lemma_mul_c_i_shift_bounded()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/field_lemmas/lemmas/lemma_mul_term_product_bounds()",
    "probe:curve25519-dalek/4.1.3/mul_lemmas/field_lemmas/lemmas/lemma_mul_value()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_digit_bounds()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_even_step()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_high_bits_zero()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_odd_step()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_width_properties()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_window_no_overflow()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_naf_wrapping_sub_correct()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_reconstruct_split()",
    "probe:curve25519-dalek/4.1.3/naf_lemmas/scalar_lemmas_/lemmas/lemma_reconstruct_zero_extend()",
    "probe:curve25519-dalek/4.1.3/negate_lemmas/field_lemmas/lemmas/lemma_neg()",
    "probe:curve25519-dalek/4.1.3/negate_lemmas/field_lemmas/lemmas/lemma_neg_no_underflow()",
    "probe:curve25519-dalek/4.1.3/negate_lemmas/field_lemmas/lemmas/proof_negate()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_add_affine_niels_completed_valid()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_add_projective_niels_completed_valid()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_cancel_z_from_ratios()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_projective_affine_product_factor()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_projective_product_factor()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_segre_t_derivation()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_sub_affine_niels_completed_valid()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_sub_projective_niels_completed_valid()",
    "probe:curve25519-dalek/4.1.3/niels_addition_correctness/edwards_lemmas/lemmas/lemma_sub_via_negation()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_bezout_identity()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_absorption()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_absorption_factorial()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_divisible_by_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_expansion_mod_p()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_factorial_relation()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_n_1()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_prime_divisibility_helper()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_sum_excess_zero()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_binomial_theorem()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_cancellation_mod_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_common_divisor_divides_gcd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_coprime_div_cancel()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_divides_linear_combo()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_divides_linear_combo_sub()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_divisor_of_odd_is_odd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_euclid_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_euclid_prime_helper()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_euler_criterion()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_extended_gcd_is_gcd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_factorial_coprime_to_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_factorial_positive()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_fermat_cancellation()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_fermat_little_theorem()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_fermat_strong()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_divides_both()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_mod_noop()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_positive()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_pow2_odd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_symmetric()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_gcd_with_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mod_difference_zero()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mod_inverse_correct()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mod_is_zero_when_divisible()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mod_sub_eq()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mod_sub_eq_implies_zero()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_mult_maps_to_nonzero()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_multiples_distinct_mod_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_only_odd_divisor_of_pow2()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_p_divisibility_facts()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_p_is_odd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_partial_binomial_sum_mod_p()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_pascal_sum_split()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_pow_2_is_mul()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_prime_gt_2_is_odd()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_product_nonzero_mod_prime()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_product_of_complements()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_product_of_multiples_eq()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_product_of_multiples_mod_eq_factorial()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_shifted_is_a_times()",
    "probe:curve25519-dalek/4.1.3/number_theory_lemmas/common_lemmas/lemmas/lemma_square_root_of_unity()",
    "probe:curve25519-dalek/4.1.3/pippenger/scalar_mul/serial/backend/Pippenger<&Vec<([i8;/64]>#process_column()",
    "probe:curve25519-dalek/4.1.3/pippenger/scalar_mul/serial/backend/Pippenger<&Vec<Option<EdwardsPoint>>>#pair_scalars_points()",
    "probe:curve25519-dalek/4.1.3/pippenger/scalar_mul/serial/backend/Pippenger<J>#optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/pippenger/scalar_mul/serial/backend/Pippenger<usize>#init_buckets()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_bucket_weighted_sum_equals_column_sum()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_intermediate_sum_extend()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_pippenger_horner_correct()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_pippenger_peel_last()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_pippenger_single()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_pippenger_zero_points_from()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_radix_2w_from_eq_helper()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_radix_2w_from_equals_reconstruct()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_running_sum_eq_weighted_from()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_running_sum_equals_weighted()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_weighted_bucket_sum_add_to_bucket()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_weighted_bucket_sum_agree()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_weighted_bucket_sum_all_identity()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_weighted_from_decompose()",
    "probe:curve25519-dalek/4.1.3/pippenger_lemmas/edwards_lemmas/lemmas/lemma_weighted_from_eq_weighted_bucket_sum()",
    "probe:curve25519-dalek/4.1.3/pow22501_t19_lemma/field_lemmas/lemmas/lemma_pow22501_prove_t19()",
    "probe:curve25519-dalek/4.1.3/pow22501_t3_lemma/field_lemmas/lemmas/lemma_pow22501_prove_t3()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_add_then_shift()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_cast_then_mask_51()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_cast_then_mod_51()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_masked_lt_51()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_mul_sub()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_shr_51_fits_u64()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_shr_51_le()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_two_factoring_51()",
    "probe:curve25519-dalek/4.1.3/pow2_51_lemmas/field_lemmas/lemmas/lemma_u64_div_and_mod_51()",
    "probe:curve25519-dalek/4.1.3/pow2k_lemmas/field_lemmas/lemmas/lemma_c_i_0_bounded()",
    "probe:curve25519-dalek/4.1.3/pow2k_lemmas/field_lemmas/lemmas/lemma_c_i_shift_bounded()",
    "probe:curve25519-dalek/4.1.3/pow2k_lemmas/field_lemmas/lemmas/lemma_pow2k_loop_boundary()",
    "probe:curve25519-dalek/4.1.3/pow2k_lemmas/field_lemmas/lemmas/lemma_pow2k_loop_value()",
    "probe:curve25519-dalek/4.1.3/pow2k_lemmas/field_lemmas/lemmas/lemma_term_product_bounds()",
    "probe:curve25519-dalek/4.1.3/pow_chain_lemmas/field_lemmas/lemmas/lemma_prove_geometric_mul_step()",
    "probe:curve25519-dalek/4.1.3/pow_chain_lemmas/field_lemmas/lemmas/lemma_prove_pow2k_step()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_binary_sum_div_decomposition()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_binary_sum_mod_decomposition()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_chunk_extraction_commutes_with_mod()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_div_bound()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_modular_bit_partitioning()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_modular_power_addition()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_distributivity_over_word()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_div_mod()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_even()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_geometric()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_geometric_double()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_bound_general()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_div()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_div_mod_close_mod()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_div_mod_small_div()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_div_mod_small_mod()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_div_mod_small_mul()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_mul_mod()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_plus_one()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow2_square()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow_mod_composition()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow_mod_congruent()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow_mod_one()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow_nat_is_nat()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_pow_nonnegative()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/lemma_two_factoring()",
    "probe:curve25519-dalek/4.1.3/pow_lemmas/common_lemmas/lemmas/pow2_MUL_div()",
    "probe:curve25519-dalek/4.1.3/pow_p58_lemma/field_lemmas/lemmas/lemma_pow_p58_prove()",
    "probe:curve25519-dalek/4.1.3/radix16_lemmas/scalar_lemmas_/lemmas/lemma_bytes32_to_radix16_nibbles()",
    "probe:curve25519-dalek/4.1.3/radix16_lemmas/scalar_lemmas_/lemmas/lemma_carry_preserves_reconstruction()",
    "probe:curve25519-dalek/4.1.3/radix16_lemmas/scalar_lemmas_/lemmas/lemma_nibbles_equal_bytes_prefix()",
    "probe:curve25519-dalek/4.1.3/radix16_lemmas/scalar_lemmas_/lemmas/lemma_valid_radix_16_implies_all_bounded()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_as_radix_2w_postconditions()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_digits_count_radix_bounds()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_last_iter_carry_zero()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_radix_2w_digit_bounds()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_radix_2w_loop_reconstruction_step()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_reconstruct_radix_2w_split()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64_shl_low_bits()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_bit_extraction()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_cross_word_decompose()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_cross_word_extraction()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_cross_word_reduce_to_two()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_lower_words_bounded()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_mod_strip_above()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_u64x4_single_word_decompose_generic()",
    "probe:curve25519-dalek/4.1.3/radix_2w_lemmas/scalar_lemmas_/lemmas/lemma_w_digits_count_concrete()",
    "probe:curve25519-dalek/4.1.3/reduce_lemmas/field_lemmas/lemmas/lemma_reduce_bound_2p()",
    "probe:curve25519-dalek/4.1.3/reduce_lemmas/field_lemmas/lemmas/lemma_reduce_boundaries()",
    "probe:curve25519-dalek/4.1.3/reduce_lemmas/field_lemmas/lemmas/proof_reduce()",
    "probe:curve25519-dalek/4.1.3/ristretto/&BatchCompressState#BatchCompressState<FieldElement>#efgh()",
    "probe:curve25519-dalek/4.1.3/ristretto/&CompressedRistretto#CompressedRistretto<Option<RistrettoPoint>>#decompress()",
    "probe:curve25519-dalek/4.1.3/ristretto/&CompressedRistretto#CompressedRistretto<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/ristretto/&CompressedRistretto#CompressedRistretto<[u8;/32]>#to_bytes()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoBasepointTable#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoBasepointTable#RistrettoBasepointTable<RistrettoPoint>#basepoint()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#Add<&RistrettoPoint>#add()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#Neg<RistrettoPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#RistrettoPoint<CompressedRistretto>#compress()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#RistrettoPoint<[EdwardsPoint;/4]>#coset4()",
    "probe:curve25519-dalek/4.1.3/ristretto/&RistrettoPoint#Sub<&RistrettoPoint>#sub()",
    "probe:curve25519-dalek/4.1.3/ristretto/&Scalar#Mul<&RistrettoBasepointTable>#mul()",
    "probe:curve25519-dalek/4.1.3/ristretto/&Scalar#Mul<&RistrettoPoint>#mul()",
    "probe:curve25519-dalek/4.1.3/ristretto/BatchCompressState#From<&RistrettoPoint>#from()",
    "probe:curve25519-dalek/4.1.3/ristretto/CompressedRistretto#ConstantTimeEq<&CompressedRistretto>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/ristretto/CompressedRistretto#Default<CompressedRistretto>#default()",
    "probe:curve25519-dalek/4.1.3/ristretto/CompressedRistretto#Identity<CompressedRistretto>#identity()",
    "probe:curve25519-dalek/4.1.3/ristretto/CompressedRistretto#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/ristretto/CompressedRistretto<&[u8]>#from_slice()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoBasepointTable<&RistrettoPoint>#create()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#AddAssign<&RistrettoPoint>#add_assign()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#ConditionallySelectable<&RistrettoPoint>#conditional_select()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#ConstantTimeEq<&RistrettoPoint>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#Default<RistrettoPoint>#default()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#Identity<RistrettoPoint>#identity()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#MulAssign<&Scalar>#mul_assign()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#Neg<RistrettoPoint>#neg()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#PartialEq<&RistrettoPoint>#eq()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#SubAssign<&RistrettoPoint>#sub_assign()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#Sum<I>#sum()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&RistrettoPoint>#vartime_double_scalar_mul_basepoint()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&Scalar>#mul_base()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&[RistrettoPoint]>#double_and_compress_batch_verus()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&[RistrettoPoint]>#sum_of_slice()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&[u8;/64]>#from_uniform_bytes()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<&[u8]>#hash_from_bytes_verus()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<J>#multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<J>#optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<RistrettoPoint>#elligator_ristretto_flavor()",
    "probe:curve25519-dalek/4.1.3/ristretto/RistrettoPoint<[u8;/64]>#from_hash_verus()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Add<&Scalar>#add()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Mul<&Scalar>#mul()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Neg<Scalar>#neg()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<Choice>#is_canonical()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<Scalar>#invert()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<Scalar>#reduce()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<UnpackedScalar>#unpack()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[bool;/256]>#bits_le()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[i8;/256]>#non_adjacent_form()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[i8;/64]>#as_radix_16()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[i8;/64]>#as_radix_2w()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Scalar<[u8;/32]>#to_bytes()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar#Sub<&Scalar>#sub()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar52#Scalar52<Scalar>#pack()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar52#Scalar52<UnpackedScalar>#invert()",
    "probe:curve25519-dalek/4.1.3/scalar/&Scalar52#Scalar52<UnpackedScalar>#montgomery_invert()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#AddAssign<&Scalar>#add_assign()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#ConstantTimeEq<&Self>#ct_eq()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Default<Scalar>#default()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#From<u128>#from()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#From<u16>#from()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#From<u32>#from()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#From<u64>#from()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#From<u8>#from()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Index<usize>#index()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#MulAssign<&Scalar>#mul_assign()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Neg<Scalar>#neg()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#PartialEq<&Self>#eq()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Product<I>#product()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#SubAssign<&Scalar>#sub_assign()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Sum<I>#sum()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<&R>#random()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<&[Scalar]>#batch_invert()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<&[u8;/64]>#from_bytes_mod_order_wide()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<&[u8]>#hash_from_bytes_verus()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<[u8;/32]>#from_bytes_mod_order()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<[u8;/32]>#from_canonical_bytes()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<[u8;/64]>#from_hash_verus()",
    "probe:curve25519-dalek/4.1.3/scalar/Scalar<usize>#to_radix_2w_size_hint()",
    "probe:curve25519-dalek/4.1.3/scalar/bot_half()",
    "probe:curve25519-dalek/4.1.3/scalar/clamp_integer()",
    "probe:curve25519-dalek/4.1.3/scalar/read_le_u64_into()",
    "probe:curve25519-dalek/4.1.3/scalar/square_multiply()",
    "probe:curve25519-dalek/4.1.3/scalar/top_half()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/&Scalar52#Scalar52<Scalar52>#as_montgomery()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/&Scalar52#Scalar52<Scalar52>#from_montgomery()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/&Scalar52#Scalar52<Scalar52>#montgomery_square()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/&Scalar52#Scalar52<Scalar52>#square()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/&mut/Scalar52#Scalar52<u64>#conditional_add_l()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52#Index<usize>#index()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52#Scalar52<[u8;/32]>#as_bytes()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52#Zeroize#zeroize()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&Scalar52>#add()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&Scalar52>#montgomery_mul()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&Scalar52>#mul()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&Scalar52>#sub()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&Scalar52>#sub_new()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&[u8;/32]>#from_bytes()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<&[u8;/64]>#from_bytes_wide()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<Scalar52>#montgomery_reduce()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<[u128;/9]>#mul_internal()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<[u128;/9]>#square_internal()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<u128>#part1()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/Scalar52<u128>#part2()",
    "probe:curve25519-dalek/4.1.3/scalar/u64/serial/backend/m()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_backward_loop_acc_invariant()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_backward_loop_is_inverse()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_invert_chain()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_montgomery_mul_partial_product()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_mul_congruence()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_partial_product_full()",
    "probe:curve25519-dalek/4.1.3/scalar_batch_invert_lemmas/lemmas/lemma_partial_product_prefix_eq()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/Scalar<&[Scalar]>#product_of_slice()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/Scalar<&[Scalar]>#sum_of_slice()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/lemma_scalar_one_properties()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/lemma_scalar_zero_properties()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/lemma_u8_32_as_nat_one()",
    "probe:curve25519-dalek/4.1.3/scalar_helpers/lemma_u8_32_as_nat_zero()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_add_carry_and_sum_bounds()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_add_l_loop_invariant()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_add_loop_bounds()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_add_loop_invariant()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_add_sum_simplify()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_borrow_and_mask_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_bound_scalar()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_cancel_coprime_factor()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_cancel_mul_L_mod_R()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_cancel_mul_R_mod_L()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_cancel_mul_montgomery_mod()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_cancel_mul_pow2_mod()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_canonical_bytes_high_bit_clear()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_carry_bounded_after_mask()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_conditional_add_l_correct()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_decompose()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_five_limbs_equals_to_nat()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_from_montgomery_limbs_conversion()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_general_bound()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_group_order_bound()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_group_order_is_odd()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_group_order_smaller_than_pow256()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_invert_correctness()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_is_canonical_correctness()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_l_equals_group_order()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_l_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_l_value_properties()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_limbs_bounded_implies_limbs_bounded_for_sub()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_limbs_bounded_implies_prod_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_mod_cancel()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_montgomery_inverse()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_montgomery_radix_nonzero_mod_group_order()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_mul_factors_congruent_implies_products_congruent()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_mul_internal_correct()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_mul_internal_no_overflow()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_neg_sum_mod()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_negation_sums_to_zero()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_nine_limbs_equals_slice128_as_nat()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_one_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_pow252()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_pow2_260_greater_than_2_group_order()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_r_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_r_equals_spec()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_r_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_rr_equals_spec()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_rr_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_scalar52_lt_pow2_256_if_canonical()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_scalar_subtract_no_overflow()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_seq_u64_as_nat_subrange_extend()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_spec_mul_internal_commutative()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_square_internal_correct()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_square_internal_no_overflow()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_square_multiply_step()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_sub_correct_after_loops()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_sub_loop1_invariant()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_sub_new_correct()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_subrange5_eq_scalar52_as_nat()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas/lemmas/lemma_zero_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_bytes_suffix_matches_word_partial()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_hi_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_high_limbs_encode_high_expr()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_high_low_recombine()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_limb_from_adjacent_words()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_lo_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_low_limbs_encode_low_expr()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_montgomery_reduce_cancels_r()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_montgomery_reduced_sum_congruent()",
    "probe:curve25519-dalek/4.1.3/scalar_lemmas_extra/lemmas/lemma_word_contribution_decomposition()",
    "probe:curve25519-dalek/4.1.3/scalar_montgomery_lemmas/lemmas/lemma_from_montgomery_is_product_with_one()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_as_bytes_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_boundary_byte_combines_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_byte_from_limb_shift_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_limb0_contribution_correctness_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_limb1_contribution_correctness_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_limb2_contribution_correctness_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_limb3_contribution_correctness_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_limb4_contribution_correctness_52()",
    "probe:curve25519-dalek/4.1.3/scalar_to_bytes_lemmas/scalar_byte_lemmas/lemmas/lemma_sum_equals_byte_nat_52()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_fourth_root_of_unity()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_i_inverse_is_neg_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_mul_i_squared_is_neg()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_multiply_by_i_flips_sign()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_neg_u_times_inv_iu_is_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_one_minus_x_times_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_one_plus_x_times_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_q_times_i_eq_y()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_sqrt_m1_limbs_bounded()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_sqrt_m1_nonzero()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_square_root_of_neg_one()",
    "probe:curve25519-dalek/4.1.3/sqrt_m1_lemmas/field_lemmas/lemmas/lemma_u_times_inv_iu_is_neg_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_algebraic_chain_base()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_canonical_nat_lt_p()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_check_fourth_root_pattern()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_conditional_negate_makes_even()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_decode_invsqrt_facts()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_eq_neg_times_i_implies_zero()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_invsqrt_matches_spec()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_invsqrt_unique()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_is_negative_bridge()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_is_sqrt_ratio_to_field()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_nat_invsqrt_satisfies_relation()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_negate_makes_nonnegative()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_no_square_root_when_times_i()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_nonneg_invsqrt_mul_satisfies_sqrt_ratio()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_nonneg_preserves_sqrt_ratio()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_nonneg_sqrt_ratio_unique()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_nonneg_square_root_unique()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_check_value()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_correctness()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_lift_to_uv()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_matches_invsqrt_mul()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_mutual_exclusion()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_sqrt_ratio_zero_propagation()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_uv7_nonzero()",
    "probe:curve25519-dalek/4.1.3/sqrt_ratio_lemmas/field_lemmas/lemmas/lemma_zero_is_sqrt_ratio()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_sqrt_ratio_failure_means_invalid_y()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_sqrt_ratio_implies_on_curve()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_sqrt_ratio_success_means_valid_y()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_step1_case_analysis()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_step1_curve_semantics()",
    "probe:curve25519-dalek/4.1.3/step1_lemmas/edwards_lemmas/lemmas/lemma_u_zero_implies_identity_point()",
    "probe:curve25519-dalek/4.1.3/straus/scalar_mul/serial/backend/Straus<J>#multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/straus/scalar_mul/serial/backend/Straus<J>#optional_multiscalar_mul_verus()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_column_sum_all_zero()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_column_sum_canonical()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_column_sum_prefix_eq()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_column_sum_single()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_column_sum_step_zero_digit()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_edwards_point_as_affine_canonical()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_digit_negative_select_preconditions()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_digit_negative_select_preconditions_width8()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_digit_positive_select_preconditions()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_digit_positive_select_preconditions_width8()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_select_is_signed_scalar_mul_affine8()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_naf_select_is_signed_scalar_mul_projective()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_naf_from_eq_helper()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_naf_from_equals_reconstruct()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_radix_16_from_eq_helper()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_reconstruct_radix_16_from_equals_reconstruct()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_select_is_signed_scalar_mul_projective()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_base()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_correct()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_partial_peel_last()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_single()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_step()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_ct_zero_points_from()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_base()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_correct()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_partial_peel_last()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_single()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_step()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_zero_points_from()",
    "probe:curve25519-dalek/4.1.3/straus_lemmas/edwards_lemmas/lemmas/lemma_straus_vt_zero_suffix()",
    "probe:curve25519-dalek/4.1.3/sum_lemmas/common_lemmas/lemmas/lemma_sub_symmetric_bound()",
    "probe:curve25519-dalek/4.1.3/sum_lemmas/common_lemmas/lemmas/lemma_sum_bounds()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_as_nat_bound_from_51bit_limbs()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_carry_out_equals_q()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_geometric_sum_5_terms()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_mul_upper_bound()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_p_radix_representation()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_reduction_carry_propagation_is_division()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_reduction_telescoping()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_sub_constants_equal_16p()",
    "probe:curve25519-dalek/4.1.3/to_bytes_reduction_lemmas/field_lemmas/lemmas/lemma_to_bytes_reduction()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_bytes_as_nat_prefix_bounded()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_bytes_as_nat_prefix_chunk()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_bytes_seq_as_nat_equals_prefix()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_canonical_bytes_equal()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_decomposition_prefix_rec()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_extract_byte_at_index()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_from_le_bytes()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_horner_to_prefix_step()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_prefix_div_extracts_byte()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_prefix_equal_when_bytes_match()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_prefix_equals_suffix_full()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_prefix_equals_suffix_partial()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_rec_suffix_divisible()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_suffix_zero_when_bytes_zero()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u64x4_from_le_bytes()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_eq_bytes_seq_as_nat()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_equals_rec()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_equals_suffix_64()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_first_byte_only()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_identity()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_lower_bound()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_lt_pow2_255()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_mod_truncates()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_rec_bound()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_u8_32_as_nat_with_trailing_zeros()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_words64_from_bytes_to_nat_wide()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_words_as_nat_equals_bytes()",
    "probe:curve25519-dalek/4.1.3/to_nat_lemmas/common_lemmas/lemmas/lemma_words_as_nat_upper_bound()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_four_torsion_with_neg()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_four_torsion_with_two_torsion()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_two_torsion_four_torsion()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_two_torsion_four_torsion_neg()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_two_torsion_self()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_edwards_add_zero_coord_denom()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_on_curve_x_zero_implies_y_pm_one()",
    "probe:curve25519-dalek/4.1.3/torsion_lemmas/edwards_lemmas/lemmas/lemma_on_curve_y_zero_implies_x_sq_neg_one()",
    "probe:curve25519-dalek/4.1.3/traits/CompressedEdwardsY#IsIdentity<bool>#is_identity()",
    "probe:curve25519-dalek/4.1.3/traits/EdwardsPoint#IsIdentity<bool>#is_identity()",
    "probe:curve25519-dalek/4.1.3/traits/MontgomeryPoint#IsIdentity<bool>#is_identity()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_bridge_pow_as_nat_to_spec()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_fe51_unit_is_one()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_u64_5_as_nat_add()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_u64_5_as_nat_k()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_u64_5_as_nat_product()",
    "probe:curve25519-dalek/4.1.3/u64_5_as_nat_lemmas/field_lemmas/lemmas/lemma_u64_5_as_nat_sub()",
    "probe:curve25519-dalek/4.1.3/variable_base/scalar_mul/serial/backend/mul()",
    "probe:curve25519-dalek/4.1.3/vartime_double_base/scalar_mul/serial/backend/mul()",
    "probe:curve25519-dalek/4.1.3/vartime_double_base_lemmas/edwards_lemmas/lemmas/lemma_vartime_double_base_col_a()",
    "probe:curve25519-dalek/4.1.3/vartime_double_base_lemmas/edwards_lemmas/lemmas/lemma_vartime_double_base_col_ab()",
    "probe:curve25519-dalek/4.1.3/window/&LookupTable<AffineNielsPoint>#LookupTable<i8>#select()",
    "probe:curve25519-dalek/4.1.3/window/&LookupTable<ProjectiveNielsPoint>#LookupTable<i8>#select()",
    "probe:curve25519-dalek/4.1.3/window/&NafLookupTable5<AffineNielsPoint>#NafLookupTable5<usize>#select()",
    "probe:curve25519-dalek/4.1.3/window/&NafLookupTable5<ProjectiveNielsPoint>#NafLookupTable5<usize>#select()",
    "probe:curve25519-dalek/4.1.3/window/&NafLookupTable8<AffineNielsPoint>#NafLookupTable8<usize>#select()",
    "probe:curve25519-dalek/4.1.3/window/&NafLookupTable8<ProjectiveNielsPoint>#NafLookupTable8<usize>#select()",
    "probe:curve25519-dalek/4.1.3/window/LookupTable#Default<LookupTable<AffineNielsPoint>>#default()",
    "probe:curve25519-dalek/4.1.3/window/LookupTable#Default<LookupTable<ProjectiveNielsPoint>>#default()",
    "probe:curve25519-dalek/4.1.3/window/LookupTable<AffineNielsPoint>#From<&EdwardsPoint>#from()",
    "probe:curve25519-dalek/4.1.3/window/LookupTable<ProjectiveNielsPoint>#From<&EdwardsPoint>#from()",
    "probe:curve25519-dalek/4.1.3/window/NafLookupTable5<AffineNielsPoint>#From<&EdwardsPoint>#from()",
    "probe:curve25519-dalek/4.1.3/window/NafLookupTable5<ProjectiveNielsPoint>#From<&EdwardsPoint>#from()",
    "probe:curve25519-dalek/4.1.3/window/NafLookupTable8<AffineNielsPoint>#From<&EdwardsPoint>#from()",
    "probe:curve25519-dalek/4.1.3/window/NafLookupTable8<ProjectiveNielsPoint>#From<&EdwardsPoint>#from()"
  ],
  "verified_functions_count": 1094,
  "verified_functions_missing_atom_record": [],
  "verus_release_tag": "release/0.2026.01.14.88f7396"
}
Our open standard for verification certification

We have designed our VeriLib verification certificates to meet three goals:

  • Transparency: Easy to see precisely what has been verified about what code with what tooling & assumptions
  • Reproducibility: Easy for user to automatically reproduce all certified claims, so no need to trust the issuer of the certificate
  • Usability: Quick and easy to build the desired level of trust:
    • Busy users can choose trust crowdsourcing: simply trusting software with the green checkmark, knowing that if it were fraudulent, someone else would probably have tried to reproduce it, failed, sounded the alarm, and permanently destroyed VeriLib’s credibility.
    • More hardcore users can automatically repeat and inspect the entire verification process on their own machine.

Here is how this works in detail. The green checkmark displayed (at the top of certificate pages such as this one) is not static, but dynamically generated if and only if three hashes stored on the Ethereum blockchain satisfy these properties:

a) The GitHub repo hash matches that of the linked repo (certifying that we’re verifying the right code)

b) The DockerHub container hash matches that of the linked container (certifying that we’re using the right verification tooling)

c) The manifest hash matches that of the displayed manifest (certifying that we’re showing the right verification result)

d) That the manifest shows VerificationSuccess = true

Blockchain commit time — (on-chain timestamp: Ethereum proof)
GitHub / repo hash d4c6a944625d7e2473899e28a5129baa05cd3080 (browse tree)
DockerHub / container hash sha256:12b6aa1259da7b8dc167d7a6efc3133d61ab4d854f64db27a466b7d695b838f8
Manifest hash dadaf066eaf9e2dbbdbcbcfac8bd9d6d3c3d0c52942407f5bf7ee7e1aa766843 (SHA-256 of published JSON file)

Running the Verify it yourself script (instructions below) checks that applying the verification tooling (b) to the code (a) reproduces the manifest (c).

To save you time, VeriLib has already auto-run this same script, which produces both pedagogical output to the terminal and the result summary file manifest.json.

We encourage you to not only run this tooling, but also inspect it for correctness. You can build trust in this certificate page by checking the text in green against the manifest, and by noting that the manifest lists as successfully verified all functions in the Specifications section.

Verify it yourself

You do not need to clone any repository. Download the small bash script below using wget or curl. Running it pulls the prebuilt image from Docker Hub and writes the same manifests and lists this page publishes. A full run can take a long time and use significant disk space—plan for that before you start.

  1. Get the script with wget (saves as verify.sh in the current directory):
    wget -O verify.sh https://verilib.org/cert/5132/verify-script

    Same URL with curl: curl -fsSL -o verify.sh https://verilib.org/cert/5132/verify-script

  2. bash verify.sh --cert-verify-url 'https://verilib.org' 'verilib/repo-5132@sha256:12b6aa1259da7b8dc167d7a6efc3133d61ab4d854f64db27a466b7d695b838f8' 'VERIFICATION_RESULTS'

Once you have finished running the script, the file VERIFICATION_RESULTS/manifest.json should match what is shown in the Results section above (downloadable here).

Install Docker

You need a working Docker install before you can pull the certificate image or run the verification script. For the canonical, up-to-date steps (including licensing and system requirements), use Docker’s official guide: Get Docker.

  • macOS: Install Docker Desktop for Mac (Apple Silicon or Intel per your Mac). Open the app from Applications, complete onboarding, and wait until Docker reports “running”. Detailed steps: Install Docker Desktop on Mac.
  • Windows: Install Docker Desktop for Windows. Use WSL 2 backend when prompted. After install, start Docker Desktop and wait until it is ready. Detailed steps: Install Docker Desktop on Windows.
  • Linux: Install Docker Engine (and optionally Docker Compose plugin) for your distribution—do not rely on a random apt package without checking Docker’s repo instructions. Detailed steps: Install Docker Engine (choose your distro: Ubuntu, Debian, Fedora, etc.).

Smoke test: In a terminal, run docker version. You should see both Client and Server sections. If you see docker: command not found, the CLI is not on your PATH yet—restart the terminal or finish Docker Desktop’s setup.

Reproducible Docker image (open source)

Latest certificate: v1 — /cert/5132 and /cert/5132?p=1&c=v1 pin the image below.

The Docker image verilib/repo-5132@sha256:12b6aa1259da7b8dc167d7a6efc3133d61ab4d854f64db27a466b7d695b838f8 on Docker Hub matches this certificate’s published dockerHubImageDigest / manifest image. Use Verify it yourself to pull and run—no clone required.