LoopProps: make loop_unfold a theorem, not an axiom (pure loopGo fixpoint)

[junjihashimoto]

Summary

Removes the custom loop_unfold axiom introduced in PR #65,
replacing it with a proved theorem. Signal.loop is now a pure
definition (⟨loopGo f⟩, the strong-recursion fixpoint) instead of an
opaque wrapper around the unsafe memoizing loopImpl. Execution
stays fast via @[implemented_by loopImpl]; only the logical value
changes from "unknowable opaque" to "the pure fixpoint the kernel can
unfold".

Prompted by the review question on PR #65: "loop is a Lean
expression, so why does it need an axiom?" — the answer was "because
it was opaque", and this PR removes that opaque.

What changed

Sparkle/Core/Signal.lean

• loopGo f t — fixpoint value at time t by strong recursion on t:
  apply f to a signal supplying the already-computed values for
  i < t and default at ≥ t. if i < t guard ⇒ well-founded
  (termination_by t). Total, no axiom, no unsafe.
• loop f := ⟨loopGo f⟩ — a def, not opaque, still
  @[implemented_by loopImpl] for O(n) execution.
• loopGo_eq — defining equation exposed for proofs.

Sparkle/Verification/LoopProps.lean

• loop_unfold : axiom → theorem, proved from loopGo_eq +
  StrictlyCausal (a strictly causal body never observes the
  default placeholder at cycles ≥ t).
• Docstring rewritten.

Trust base (the point of the PR)

#print axioms dividerSignal_result_gen (downstream RV32 divider
theorem from PR #65) no longer lists loop_unfold. Remaining
axioms are all Lean-standard:

propext, Classical.choice, Quot.sound,     -- Lean core
Lean.ofReduceBool,                          -- bv_decide/native_decide (pre-existing)
Lean.trustCompiler                          -- @[implemented_by] (standard)

The bespoke fixpoint axiom is gone. The only loop-specific trust is
now Lean.trustCompiler (that loopImpl computes the same value as
loopGo), which is the same compiler-trust every @[implemented_by]
in the codebase already relies on — a much weaker and more standard
assumption than a hand-written fixpoint axiom.

Performance

@[implemented_by loopImpl] keeps simulation at O(n):

• direct Signal.loop counter: .val 2000 in ~0 ms (probe).
• matched lake exe test: main 7m52s vs this branch 8m02s —
  within noise, no regression.

Also fixed (latent main bugs surfaced by the first clean build)

lakefile.lean's sparkleModuleDeps monolithic-link list was stale;
a from-scratch .lake/build wipe exposed two missing/renamed .so:

• sparkle_Sparkle_Backend_CppSim.so → _CSim.so (CppSim was
  replaced by the C-only CSim backend; the old .so no longer exists).
• added sparkle_Sparkle_Core_SignalLeavesDerive.so (the
  SignalLeaves deriving handler from the per-leaf output-port split
  was never registered).

Both only bite a clean build — incremental builds kept the stale .so
around, which is why CI hadn't caught them.

Verification

• lake build clean.
• lake exe test: 13/13 lspec pass.
• Both Sparkle.Verification.Divider.{Correct,States33} build against
  the new pure loop with zero proof changes — PR Prove that Divider divides #65's divider
  proof is now the regression test confirming loopGo is the correct
  fixpoint.