Stdlib/Hash/Pedersen: deterministic _spec_canonical via MSM canonicality

All four pedersen_*_spec_canonical variants are now deterministic with
NO caller-supplied h_canon_witness:

  pedersen_commitment_with_separator_spec_canonical
  pedersen_commitment_spec_canonical
  pedersen_hash_with_separator_spec_canonical
  pedersen_hash_spec_canonical

Mechanism

The base pedersen_*_with_separator_spec gain a 4th existential conjunct
∀ i, Scalar.Canonical (Ss.get i). For commitment, that fact is surfaced
from multi_scalar_mul_combined_spec (the wrapper-level combined post);
for hash it comes from multi_scalar_mul_builtin_combined_spec directly,
since the hash body invokes the builtin (multi_scalar_mul_array_return)
without going through the multi_scalar_mul wrapper.

The deterministic corollary then collapses the 4-conjunct existential
via Scalar.canonical_decomp_unique:

  canonicality + limb relation + canonical-range disjunction →
    Ss.get i = canonicalDecomp (input.get i)

so the sum reduces to the closed form ∑ scalarValueNat (canonicalDecomp
inputᵢ) • generator. No caller obligation.

Hash proof refactor

pedersen_hash_with_separator_spec was 435 lines of inline manipulation.
Extracted named helpers (Ss, hSs_get, hsFull_get, hLenScalar_value) to
compress the refine branches, taking the proof to 383 lines. The
remaining length is genuine work — loop body, h_enc proof, and the
Fin (N+1).toNat ↔ Fin (N.toNat+1) transport in the result-equality
branch.

Author: Eduardogbg