Summary
The subspecs/poseidon2/permutation.py module requires numpy and numba for the Poseidon2 hash permutation implementation. These are large external dependencies not available in the LeanPython interpreter.
Current behavior
ModuleNotFoundError: No module named 'numpy'
- The XMSS pure-Python Poseidon2 wrapper (
xmss/poseidon.py) delegates to this module
Impact
poseidon2/ subspec cannot be interpreted
xmss/ subspec depends on poseidon2 for hash computations
- The pure-Lean Poseidon2 implementation (tested in Phase 9f) covers the same algorithm but through the internal test harness, not via the real leanSpec files
Possible approaches
- Implement numpy subset in Lean4 — only the array operations used by permutation.py (ndarray creation, element-wise ops, reshape)
- Pure-Python Poseidon2 fallback — rewrite permutation.py without numpy dependency (upstream change)
- Skip — the Lean4-native Poseidon2 (already implemented and tested) covers this functionality
Reference
references/leanSpec/src/lean_spec/subspecs/poseidon2/permutation.py
- Phase 9f already implements and tests Poseidon2 in pure Lean4
Summary
The
subspecs/poseidon2/permutation.pymodule requiresnumpyandnumbafor the Poseidon2 hash permutation implementation. These are large external dependencies not available in the LeanPython interpreter.Current behavior
ModuleNotFoundError: No module named 'numpy'xmss/poseidon.py) delegates to this moduleImpact
poseidon2/subspec cannot be interpretedxmss/subspec depends on poseidon2 for hash computationsPossible approaches
Reference
references/leanSpec/src/lean_spec/subspecs/poseidon2/permutation.py