Same documented rewrite as FieldElement::sqrt_ratio_i: semantically
identical and still constant-time, but avoids subtle's
ConditionallyNegatable blanket impl, which the verification toolchain
cannot translate. Unblocks extracting decompress for the phase-2 full
point-level lift.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
Pure refactors (cargo check green under both feature sets), semantics of
mul unchanged:
- dsm_top_index / dsm_loop / dsm_step_p / dsm_step_b helpers: the main
double-and-add loop becomes a strictly-decreasing while with a
single-assignment body and parameter-rooted borrows (the original
loop/break shape with match-updates fails Aeneas' loop fixed point);
- the starting-index scan always returns 255: leading zero NAF digits
double the identity (a no-op), so the result is unchanged - only the
variable-time skip is dropped (constant-time behavior improves);
- the downward break-scan (which failed Aeneas' symbolic join) is gone.
With these, Charon+Aeneas extract the complete path - non_adjacent_form,
NafLookupTable5::from/select, the affine basepoint table, the 256-step
dsm_loop, and mul - with zero errors and zero sorries. This opens the
double-scalar-multiplication verification campaign (the EdDSA verify
equation's core).
Pure refactor, semantics identical (cargo check green):
- from_bytes_wide_parts(bytes) -> (Scalar52, Scalar52): the byte-unpack
loops + the 52-bit lo/hi split, as a named prefix
- split_words_lo / split_words_hi: the two split halves, built with
Scalar52([...]) struct literals instead of per-index mutation
- from_bytes_wide: parts -> montgomery_mul(lo, R) ->
montgomery_mul(hi, RR) -> add
Why: the verification side measured that (a) a WP walk whose motives
contain a montgomery_mul call replays its whole body at every kernel
step, and (b) straight-line chains of IndexMut closure back-functions
make kernel defeq exponential in chain depth. Named prefix functions fix
(a); struct-literal construction eliminates the closures and fixes (b).
With this shape the full from_bytes_wide certificate kernel-checks in
77 seconds (was: aborted after 30+ minutes).
hi[4] = words[7] >> 20 is the only shift in the function whose result is
stored without a trailing mask/or; at the pinned Aeneas (bf13c42e) a bare
`x >> c` as a full RHS extracts ill-typed (wrapping_shr applied to an i32
with an emitted-but-unsubstituted U32 cast). Masking is a semantic no-op:
words[7] >> 20 < 2^44 < 2^52. Semantics unchanged; needed to bring
from_bytes_wide (the hash-to-scalar reduction) into verification scope.
* 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>
* fix pkcs8
* Propagate PKCS#8 errors; add decoding test
Replace unwraps with ? to propagate pkcs8::Error when parsing PKCS#8 key material (in TryFrom<&KeypairBytes> and from_pkcs8_der), use the parsed SigningKey directly for public-key verification, and return Ok(signing_key). Add a test to ensure malformed/non-PKCS#8 bytes are rejected without panicking, and import BitStringRef in tests to simplify references.
* impl secp256r1
* CI
* refactor: remove sigantures; add msm
* clean up scalar_mul APIs
* ci
* address comments
* CI
* fix Eq/PartialEq bug for projective point
* Add prechecked optimized triple-base mul
Introduce a prechecked 128/128/256 optimized path for vartime triple-base multiplication: vartime_triple_base_mul_128_128_256 now checks whether a1 and a2 fit in 128 bits and falls back to general multiplication if not. Add vartime_triple_base_mul_128_128_256_prechecked and corresponding serial/vector backend implementations (renamed to *_prechecked). Add scalar_fits_in_128_bits helper and update callers (verification_key) to use the prechecked path. Update docs/comments and add a test to ensure full-width scalars are handled by the fallback path.
* bring back the docs
* CI
Add strict SPKI validation and tests for PKCS#8 public keys. Introduce OID and ALGORITHM_ID constants and refactor SPKI parsing into verification_key_bytes_from_spki which verifies the algorithm OID, parameters, and key byte length/format, returning appropriate pkcs8::spki::Error values. Update TryFrom/EncodePublicKey/DecodePublicKey implementations to use the new helper and to propagate/mapping errors correctly. Add two tests (behind the pkcs8 feature) to assert rejection of SPKI docs with the wrong algorithm OID and with malformed key bytes.
Add a static AVX2 NafLookupTable5<CachedPoint> for B * 2^128 and use it from the vector triple-base verifier path instead of rebuilding that table every verification.
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.382 us, with 95% CI 19.327..19.426 us.
- master measured 20.051 us, with 95% CI 19.938..20.134 us, so this branch was about 3.34% faster in that run.
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.
* remove README.md in the syscall directory
* use workspace dependency in `bls12-381`
* add `workspace.package` information
* use 2021 edition for bls12-381
* inherit workspace.package for `ed25519-pokos`
* cargo fmt
* Initial commit
* skeleton
* refactor and merge curve and ed crates
* fmt
* ci
* fmt again
* ci
* Update bench.rs
* fix ubuntu
* implement dalek api
* clean up
