feat: Share repeated type annotations during noir_def elaboration

[TomAFrench]

Summary

Extracted code repeats the same — often enormous — type annotation on every call, builtin, and reference that touches a type (e.g. encode_var in extracted noir_base64 repeats its ~15-operator output-length type over a dozen times). The DSL previously re-built and re-elaborated the type term for every occurrence, so a definition's elaboration cost grew with the number of annotations rather than the number of distinct types.

This PR shares those terms: within one noir_def, the first occurrence of a sufficiently large type binds its term to a fresh identifier (#tp_0, #tp_1, …) and every further occurrence elaborates to just that identifier.

Benchmark: elaboration time is halved (918ms → 480ms) on a file of ten definitions each repeating a encode_var-sized type sixteen times. Definitions whose types fall below the sharing threshold are unaffected. The win exceeds the raw re-elaboration saving because sharing also shrinks every downstream term: letIn binder types, unification problems, and metavariable assignments carry a short identifier instead of a copy of the type.

How it works

• Syntax/State.lean: DSLState gains a cache from printed type syntax to a generated identifier plus the backing bindings in creation order. makeNoirTypeShared builds a type term on first sight and returns the cached identifier on repeats; wrapSharedTypeLets emits the collected lets. Types under a size threshold (16 syntax nodes) and types containing context-dependent holes (_) fall back to plain makeNoirType.
• Syntax/Builders.lean: the type-bearing call sites in expression building (builtin returning types, funcref signatures, literals, lambdas, trait self types) go through the shared path. makeFnDecl now builds parameter types, return type, and body in a single DSL-monad run and wraps the result tuple in the collected lets — inside the generics match, since shared types may mention the generic binders. let-bound variables are definitionally transparent, so elaboration semantics are unchanged.
• Tactic/Steps.lean: the two body-reduction sites (enter_decl's reduceOne and reduceBetaIotaMatch) now zeta-reduce the head let bindings, so proof goals keep exactly their existing fully-expanded shape. The change is invisible to proof authors.

Validation

• Full Lampe and Tests builds pass.
• The existing proof tests (LenBuiltin, Syntax) prove theorems via enter_decl/steps over definitions that do receive shared types (even Array<u8, M> crosses the threshold), so the proof path over shared bindings is exercised by the suite.
• Verified via #print that generated definitions bind each large type once and reference it from all use sites, including inferred callBuiltin type indices.

Notes / future work

• The 16-node threshold triggers on modest types as well as giant ones; harmless per the benchmarks, but tunable if the extra bindings bother anyone reading #print output.
• Call-site generic values (the same giant arithmetic appearing in f<…, EXPR: u32> positions) are not yet shared — they would need a typed ascription to be let-bound, and are the natural follow-up if more elaboration speed is wanted.

[iamrecursion]

Looks great!

[iamrecursion]

Suggested change

	/--
	Maps the (printed) syntax of a type annotation to the identifier its built term has been bound
	to, so that repeated annotations reuse one binding. See `makeNoirTypeShared`.
	-/
	sharedTypeCache : Std.HashMap String Lean.Ident := {}
	/--
	The bindings backing `sharedTypeCache`, in creation order. `wrapSharedTypeLets` emits these as
	`let`s around the finished term.
	-/
	sharedTypeLets : Array (Lean.Ident × TSyntax `term) := #[]
	/--
	Maps the (printed) syntax of a type annotation to the identifier its built term has been bound
	to, so that repeated annotations reuse one binding. See `makeNoirTypeShared`.
	-/
	sharedTypeCache : Std.HashMap String Lean.Ident := {}
	/--
	The bindings backing `sharedTypeCache`, in creation order. `wrapSharedTypeLets` emits these as
	`let`s around the finished term.
	-/
	sharedTypeLets : Array (Lean.Ident × TSyntax `term) := #[]