docs(kms/auth-eth): add formal specification

Normative pre/post/frame conditions, state invariants, cross-contract
assumptions, and adversarial scenarios for DstackKms + DstackApp,
independent of code. Each property cites the Halmos test that verifies
it; properties without a citation are explicit gaps.

Sections:
- Trust model (principals, environment, off-chain pipeline)
- Storage layout per contract with frame-condition rules
- Per-function pre/post/frame/events/reverts specs for the entire
  public surface
- Decision-table semantics for isAppAllowed
- State invariants INV-1 through INV-7 with verification status
- Adversarial scenarios: malicious registerApp + downstream gates,
  reentrancy structural-impossibility argument, gas-griefing,
  front-running, initializer selector collision
- Known verification gaps (cross-transaction invariants,
  universal-quantification over registered apps, KEVM bytecode-level)
- Open product-level questions for the team:
  1. Should renounceOwnership be overridden to revert?
  2. Should KMS track which appImplementation was current per app?
  3. Should removeOsImageHash retroactively un-authorize?
  4. Should gatewayAppId validate format?

Deliverable for any future external audit-firm engagement.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: h4x3rotab