Circomlib/Poseidon.lean is outside the module graph, so CI never checks it

[pirapira]

Note

This issue was written by Claude Code, at the request of @pirapira (filed while reviewing #375).

Problem

Clean/Circomlib/Poseidon.lean is not imported by any module (nothing in the repo imports Clean.Circomlib.Poseidon), so lake build / CI never elaborates it. Any refactor can silently break the file.

This already bit us in #375: the PR description notes Poseidon was "not in the module graph, so it's easily missed" and had to be fixed separately as a checklist item.

Why it is out of the graph

The file contains one sorry — the BN254 primality fact at Clean/Circomlib/Poseidon.lean:22:

instance : Fact (Nat.Prime BN254_PRIME) := ⟨by sorry⟩

Clean/Circomlib/Poseidon.md documents that closing it needs a Pratt/Lucas primality certificate. Keeping the sorry out of the main graph is intentional; the side effect is zero CI coverage for ~480 lines of verified-circuit code.

Suggested fixes (either or both)

1. Close the sorry with a primality certificate (e.g. Mathlib.NumberTheory.LucasLehmer-style certificate or Nat.Prime via pratt-certificate tooling), then import the file from the module graph like every other Circomlib port.
2. Short term: add an explicit CI step that builds the module despite the sorry, e.g. lake build Clean.Circomlib.Poseidon, so regressions surface as build failures (the sorry only produces a warning, not an error).

Option 2 is cheap and immediately prevents silent breakage; option 1 is the proper end state.

[mitschabaude]

my favored version of option 2 would be to just add Poseidon to the existing CleanTests target which allows sorries

proper fix is downstream of #370