Model Payment V1 authorization wire shape

[weikengchen]

What changed

• models the independently selected per-server Payment V1 authorization round in EasyCrypt
• binds the fixed 16,414-byte encrypted request record and variable response-shape leakage
• separates the no-key network observer view from the provider after channel decryption
• updates the proof manifest to 9 sources, 56 lemmas, and 8 contract claims

Why

BitcoinPIR now supports five provider-scoped admission methods. The proof contract must explicitly admit authorization occurrence, timing, and response-shape leakage while proving that request length does not reveal the selected method, scope, operation, or credential proof length to a network observer without channel keys.

Validation

• manifest/source closure: passed
• generated product contract binding: passed
• pinned local EasyCrypt toolchain compile: passed
• local linux/amd64 Docker build was stopped at the 40-minute Apple Silicon QEMU limit during toolchain construction; GitHub native linux/amd64 CI is the trusted verification-record authority

No payment service, network endpoint, or funds are used by this proof-only change.