research: Coq formalization of Path ORAM + stash overflow bound (P0)

[hyperpolymath]

Also makes the wiki's Coq claim real (downgraded to "Planned" in PR #59 pending this). Source: docs/academic/TODO.adoc §Verification.

https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ