Function Status ​

This table shows the verification status of all functions in the project. Click on a function to see more details.

Total:105

Extracted:105

Verified:75

Spec only:22

AI Proveable:17

All (Extracted)ExtractedNot ExtractedAll (Status)VerifiedSpecifiedDraft SpecNo Status

Function ▲	Rust Source	Extracted	Verified	Issue	Notes
add	backend/serial/curve_models/mod.rs	✓	✓	—
as_extended	backend/serial/curve_models/mod.rs	✓	✓	—
as_projective	backend/serial/curve_models/mod.rs	✓	✓	—
as_extended	backend/serial/curve_models/mod.rs	✓	✓	—
double	backend/serial/curve_models/mod.rs	✓	✓	—
EDWARDS_D	backend/serial/u64/constants.rs	✓	✓	—
EDWARDS_D_MINUS_ONE_SQUARED	backend/serial/u64/constants.rs	✓	✓	—
EDWARDS_D2	backend/serial/u64/constants.rs	✓	✓	—
INVSQRT_A_MINUS_D	backend/serial/u64/constants.rs	✓	✓	—
L	backend/serial/u64/constants.rs	✓	✓	—
LFACTOR	backend/serial/u64/constants.rs	✓	✓	—
MINUS_ONE	backend/serial/u64/constants.rs	✓	✓	—
ONE_MINUS_EDWARDS_D_SQUARED	backend/serial/u64/constants.rs	✓	✓	—
R	backend/serial/u64/constants.rs	✓	✓	—
RR	backend/serial/u64/constants.rs	✓	✓	—
SQRT_AD_MINUS_ONE	backend/serial/u64/constants.rs	✓	✓	—
SQRT_M1	backend/serial/u64/constants.rs	✓	✓	—
add	backend/serial/u64/field.rs	✓	✓	—
add_assign	backend/serial/u64/field.rs	✓	✓	—
as_bytes	backend/serial/u64/field.rs	✓	✓	—
conditional_assign	backend/serial/u64/field.rs	✓	✓	—
conditional_select	backend/serial/u64/field.rs	✓	✓	—
ct_eq	field.rs	✓	✓	—
from_bytes	backend/serial/u64/field.rs	✓	✓	—
from_limbs	backend/serial/u64/field.rs	✓	✓	—
MINUS_ONE	backend/serial/u64/field.rs	✓	✓	—
mul	backend/serial/u64/field.rs	✓	📋	●#333Verify : FieldElement51::mul
neg	backend/serial/u64/field.rs	✓	✓	—
negate	backend/serial/u64/field.rs	✓	✓	—
ONE	backend/serial/u64/field.rs	✓	✓	—
pow2k	backend/serial/u64/field.rs	✓	✓	—
reduce	backend/serial/u64/field.rs	✓	✓	—
square	backend/serial/u64/field.rs	✓	✓	—
square2	backend/serial/u64/field.rs	✓	✓	—
sub	backend/serial/u64/field.rs	✓	✓	—
to_bytes	backend/serial/u64/field.rs	✓	📋	●#127Verify: to_bytes
ZERO	backend/serial/u64/field.rs	✓	✓	—
m	backend/serial/u64/scalar.rs	✓	✓	—
add	backend/serial/u64/scalar.rs	✓	✓	—
as_montgomery	backend/serial/u64/scalar.rs	✓	✓	—	🤖🏆🌈🎉⭐
conditional_add_l	backend/serial/u64/scalar.rs	✓	📋	⎇#346✏️Verify: Scalar52.sub & conditional_add_l●#129Verify: conditional_add_l
from_bytes	backend/serial/u64/scalar.rs	✓	📋	●#130Verify: from_bytes
from_bytes_wide	backend/serial/u64/scalar.rs	✓	📋	●#131Verify: from_bytes_wide
from_montgomery	backend/serial/u64/scalar.rs	✓	✓	—
invert	scalar.rs	✓	✓	—
montgomery_invert	scalar.rs	✓	📋	●#337Verify: scalar52 Montgomery invert
montgomery_mul	backend/serial/u64/scalar.rs	✓	✓	●#320Specify: bound for Scalar52::montgomery_mul
montgomery_reduce	backend/serial/u64/scalar.rs	✓	📋	●#319Specify: bounds for Scalar52::montgomery_reduce
montgomery_square	backend/serial/u64/scalar.rs	✓	✓	●#322Specify: bound for Scalar52::montgomery_square
mul_internal	backend/serial/u64/scalar.rs	✓	✓	●#323Specify: bound for Scalar52::mul_internal
square_internal	backend/serial/u64/scalar.rs	✓	✓	—
sub	backend/serial/u64/scalar.rs	✓	📋	⎇#346✏️Verify: Scalar52.sub & conditional_add_l●#344Verify: Scalar52::sub
to_bytes	backend/serial/u64/scalar.rs	✓	📋	●#336Verify Scalat52 to_bytes
ZERO	backend/serial/u64/scalar.rs	✓	✓	—
compress	edwards/affine.rs	✓	📋	—
as_bytes	edwards.rs	✓	✓	—
decompress	edwards.rs	✓	📋	—
step_1	edwards.rs	✓	☐	—
step_2	edwards.rs	✓	☐	—
add	edwards.rs	✓	📋	—
add	edwards.rs	✓	☐	—	trait wrapper
as_projective	edwards.rs	✓	✓	—
as_projective_niels	edwards.rs	✓	✓	—
compress	edwards.rs	✓	📋	—
ct_eq	edwards.rs	✓	✓	—
double	edwards.rs	✓	📋	—
identity	edwards.rs	✓	✓	—
is_small_order	edwards.rs	✓	📋	●#244Verify: is_small_order
mul_by_cofactor	edwards.rs	✓	✓	—
mul_by_pow_2	edwards.rs	✓	📋	—
to_affine	edwards.rs	✓	✓	—
to_montgomery	edwards.rs	✓	✓	—
invert	field.rs	✓	✓	—
invsqrt	field.rs	✓	✓	—
is_negative	field.rs	✓	✓	—
is_zero	field.rs	✓	✓	—
pow_p58	field.rs	✓	✓	—
pow22501	field.rs	✓	✓	—
sqrt_ratio_i	field.rs	✓	📋	●#291Verify: FieldElement51::sqrt_ratio_i
to_edwards	montgomery.rs	✓	📋	—
as_bytes	ristretto.rs	✓	✓	—
decompress	ristretto.rs	✓	📋	—
to_bytes	ristretto.rs	✓	✓	—
step_1	ristretto.rs	✓	☐	—
step_2	ristretto.rs	✓	☐	—
add	ristretto.rs	✓	📋	—
add	ristretto.rs	✓	☐	—	trait wrapper
compress	ristretto.rs	✓	☐	●#165Specify: curve25519_dalek::ristretto::RistrettoPoint::compress
elligator_ristretto_flavor	ristretto.rs	✓	📋	—
from_uniform_bytes	ristretto.rs	✓	📋	—
pack	scalar.rs	✓	✓	—
clamp_integer	scalar.rs	✓	✓	—
read_le_u64_into	scalar.rs	✓	☐	—
as_bytes	scalar.rs	✓	✓	—
ct_eq	scalar.rs	✓	✓	—
from_bytes_mod_order	scalar.rs	✓	✓	—
from_bytes_mod_order_wide	scalar.rs	✓	✓	—
from_canonical_bytes	scalar.rs	✓	✓	—
invert	scalar.rs	✓	✓	—
is_canonical	scalar.rs	✓	✓	—

Show columns:SourceExtractedVerifiedIssueNotes

Showing 1–100 of 105 functions

← Previous 12 Next →

10 per page25 per page50 per page100 per page

Extracted

✓Rust code has been extracted to Lean

☐Extraction pending

Verified

✓Function has been formally verified

📋Formal specifications but no proofs

✏️Natural language specifications

☐No verification work completed yet