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

A normative spec for DstackKms + DstackApp independent of code — the
deliverable an external FV firm engagement (Runtime Verification,
ChainSecurity, Certora) would build against.

Contents:
- Trust model: principals, what each is trusted for and not for, EVM
  / proxy / off-chain pipeline assumptions
- 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 (both KMS- and App-level)
- State invariants (INV-1 through INV-7) with their current
  verification status
- Cross-contract assumptions: KMS↔App delegation, KMS↔Proxy factory,
  App↔Proxy upgrade authorization
- Adversarial scenarios: malicious registerApp + downstream gates,
  reentrancy structural-impossibility argument, gas-griefing,
  front-running, initializer selector collision
- Known verification gaps (cross-transaction invariants, delegated-
  call universal quantification, KEVM bytecode-level proof)
- Open spec-level questions for the dstack team (renounceOwnership
  semantics, appImplementation drift, OS-image revocation reach,
  gatewayAppId format)

Each property in the spec that has a Halmos symbolic proof cites the
test name; properties without a citation are explicit gaps. The spec
is normative — code and tests track the spec, not the other way around.

Author: h4x3rotab