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).
