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