`circuit`: `Assert_failure` anomaly when a context-local definition is a function-valued bitvector operator (e.g. `\bitsN` applied only to its value)

[strub]

Summary

The circuit tactic aborts with an anomaly

anomaly: File "src/ecLowCircuits.ml", line 1143, characters 13-19: Assertion failed

when the local context contains a posed definition whose body is a bitvector operator applied to fewer arguments than the circuit backend expects — i.e. a function-valued occurrence such as uw := (\bits32) u : int -> W32. The definition need not appear in the goal.

Root cause

1. circuit (phl/ecPhlBDep.ml) builds its translation state with circuit_state_of_hyps (ecCircuits.ml:1046), which eagerly walks every hypothesis and translates each local definition body LD_var (t, Some f) (ecCircuits.ml:1060), guarded by:

   try update_state st id (circuit_of_form st hyps f)
   with CircError e -> (* skip: treat as uninitialized input *)

2. Translating a function-valued extract like (\bits32) u reaches the parametric-bvop lowering EcLowCircuits.BVOps.circuit_of_parametric_bvop, `Extract case (ecLowCircuits.ml:1143), which only matches the fully-applied [`Circuit (CBitstring _); `Constant i] and otherwise does assert false.
3. assert false raises Assert_failure, not CircError, so it bypasses the with CircError -> skip fallback in circuit_state_of_hyps and propagates as an anomaly.

Why it matters

The offending local isn't part of the goal — clearing it (clear uw ...) makes circuit succeed, since the goal uses the extracts fully applied. The eager translation of local definitions combined with a non-CircError failure turns an irrelevant local into a hard anomaly.

Expected behavior

Either (a) the parametric-bvop lowering handles the under-applied / function-valued form — e.g. eta-expand into an Init/array circuit, mirroring what arg_of_form's Tfun (int, bv) branch already does when such an extract appears as an argument; or at minimum (b) it raises a CircError for unsupported shapes, so the existing try ... with CircError -> skip in circuit_state_of_hyps skips the local cleanly (no anomaly).

Suggested fix

Replace the assert false fall-throughs in the parametric-bvop cases (`Extract, and siblings `ASliceGet/`ASliceSet/`Insert/`Map/...) in ecLowCircuits.ml with lowcircerror (...).

Reproduction

Surfaced in the formosa-mldsa AVX2 NTT proofs (nttcorrect.ec, lemma mmrP), where pose uw (i:int) := u \bits32 i (and vw, F) sit in context when circuit runs. Minimal trigger: any goal where circuit is called with a context-local of the form x := (\bitsN) w (a W_ -> int -> W_' extract applied to just the value).