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>
Same refactor as the risc0 fork: the three stateful hasher wrappers
collapse into one monomorphic sha512_hash3(r, a, m) -> [u8; 64] whose
signature carries no foreign types; extraction builds with
--no-default-features (the no-std From<InternalError> branch avoids the
boxed dyn-Error source path). Semantically Sha512 over r || a || m.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The extractor's generated Lean would otherwise shadow the signature:: crate
namespace with the parameter binder, turning module paths into invalid field
projections. Pure rename.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replaces from_canonical_bytes (subtle CtOption / black_box machinery the
extractor cannot interpret) with an explicit little-endian comparison of
the scalar bytes against ell, then from_bytes_mod_order (the identity on
canonical input). Value-level semantics identical; the verification path is
variable-time throughout, so the constant-time construction is not required.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Four pure refactors in ed25519-dalek (semantics identical, extraction only):
- verifying.rs: verify_sha512/recompute_r_sha512 — the exact unrolling of
raw_verify::<Sha512> (None context, single message slice) with every
digest-trait call behind monomorphic sha512_* wrappers, and from_hash
unrolled to from_bytes_mod_order_wide(finalize(h)). The generic
Digest<OutputSize = U64> machinery (typenum/hybrid-array) defeats the
extractor's type translation.
- verifying.rs: the R comparison as an explicit byte loop (derived
PartialEq on CompressedEdwardsY is uninterpretable).
- signature.rs from_bytes: index loops instead of range-slicing +
copy_from_slice (SliceIndex const-generics wall).
- signature.rs: compressed_from_bytes — an opaque constructor wrapper
(aggregate construction of an extraction-opaque type crashes the
translator).
With these, the full verify path extracts cleanly:
charon --start-from crate::verifying::{verify_sha512,recompute_r_sha512}
with curve25519_dalek/sha2/digest/ed25519/signature/subtle/zeroize opaque
and hybrid_array/typenum excluded.
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.
if the engine25519 hits an illegal opcode, really, that's a
software bug that should be fixed. panic, so that we get
a guru meditation and a bug report.
also fix a bug where the engine was not being powered off
on release.
Things to note:
- in case of an opcode error, the system will enter an infinite
loop complaining about the error. Maybe i should promote that to
a panic -- it's a thing that should be fixed and should just never
happen
- in case of a suspend/resume during an operation, this is
detected by the loaded microcode length not matching what we
had written. This is a heuristic, but relies on the assumption
that the microcode length would change when the engine is put
through a clean reboot (i.e., it is unlikely that it matches
what we had previously written).
