Pure refactors for the Charon/Aeneas extraction pipeline; production
behavior unchanged (both default and pinned configs cargo-check clean,
pre-existing warnings only).
- ed_sigs::sha512_hash3: single-call SHA-512 oracle, semantically
Sha512(r || a || m); a monomorphic signature with no foreign types lets
the extractor treat the hash as one opaque oracle (sha2-0.11 stack).
- VerificationKey::verify_sha512 (+ recompute_r_sha512, a_bytes_nonzero,
check_scalar_canonical, is_legacy_excluded_r): semantically identical
to verify_dalek with each step spelled extractor-friendly - derived
array PartialEq/contains as explicit index loops, and
Scalar::from_canonical_bytes (subtle internals defeat the extractor)
as an explicit s < l byte compare + from_bytes_mod_order (the identity
on canonical bytes). Signature accessors each called exactly once.
- SIMD gates: cfg(target_arch = "x86_64") becomes
cfg(all(target_arch = "x86_64", not(curve25519_serial_only))). Default
builds are identical (the new cfg is never set); extraction builds pass
RUSTFLAGS=--cfg curve25519_serial_only so the AVX2 dispatch arm
compiles out and backend selection is the real constant Serial - the
same serial-pin mechanism upstream curve25519-dalek provides natively.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Pure refactor, semantics identical: the read_le_u64_into call (whose
chunks/zip iterators are opaque to the extraction) becomes an explicit
nested index loop, the same shape as the proven from_bytes_wide unpack.
With this the entire vartime_double_base::mul extraction closure is
self-contained: zero external axioms, zero sorries.
* ed25519: add 128-bit NAF path
Add Scalar::non_adjacent_form_128 and use it in the serial and vector triple-base verifier paths for scalars known to fit in 128 bits. The helper computes only the HEEA-readable digit range instead of producing a full 256-entry NAF array for each scalar.
Benchmark notes:
- Ran this repository's Criterion benchmark program, benches/bench.rs, filtering to Single Verification, pinned to CPU 4 with 1s warmup, 2s measurement, and sample size 10.
- local_verify_zebra estimate was 19.740 us, with 95% CI 19.686..19.789 us.
- master measured 20.051 us, with 95% CI 19.938..20.134 us, so this branch was about 1.55% faster in that run.
* Use 128-bit NAF in triple-base paths
---------
Co-authored-by: zz-sol <allaboutshop10@163.com>
The triple-base verifier splits b into zero-extended 128-bit halves, so b_lo and b_hi are already canonical. Add a crate-private unchecked constructor and use it for that internal AVX2 path.
Benchmark notes:
- Ran this repository's Criterion benchmark program, benches/bench.rs, filtering to Single Verification, pinned to CPU 4 with 1s warmup, 2s measurement, and sample size 10.
- local_verify_zebra estimate was 19.996 us, with 95% CI 19.862..20.077 us.
- master measured 20.051 us, with 95% CI 19.938..20.134 us, so this branch was about 0.27% faster in that run.
