feat(X3DH): add skeleton for active-adversary message secrecy

Introduces PQXDHLean/X3DH/X3DHActiveMessageSecrecy.lean — a structured
skeleton for the active (AKE-game) version of X3DH message secrecy,
mirroring the passive proof in X3DHPassiveMessageSecrecy.lean.

The file compiles with `sorry` placeholders for the proof bodies
and the most complex oracle handler (`send`). Three of five oracle
handlers are fully implemented (`corrupt`, `revealSK`, `newSession`).
A fourth (`test`) is partially implemented — once-per-game guard,
session lookup, and dispatch to a `getTestKey` callback are in
place; full freshness checks are deferred.

Key components:
  * `SessionStatus`, `AliceSessionRecord`, `BobSessionRecord` —
    per-side session state under fixed-roles (Alice always
    initiator, Bob always responder)
  * `ActiveGameState` — session tables, corruption flags,
    sk_revealed set, designated test session
  * `Party`, `AKEQuery`, `akeSpec` — the 5-query AKE oracle spec
  * `ActiveAdversary := OracleComp (unifSpec + akeSpec + KDFOracle) Bool`
  * `akeQueryImpl` — unified QueryImpl over the 5 queries
  * `activeGame` / `activeReal` / `activeRand` —
    two-game distinguishing formulation matching passive's pattern
  * `activeSecrecyAdvantage` — boolDistAdvantage between the games
  * `x3dh_active_message_secrecy` — main theorem statement

Design choices documented inline:
  * Fixed roles (Alice=init, Bob=resp): valid by symmetry; loses
    no theorem strength
  * Multi-session (paper Theorem 2 scope): per-party session tables
  * 2 honest parties: third parties simulated via `Corrupt`
  * `recv_*` peer-key fields are `Option G` to distinguish
    "not yet received" from "received and was X"
  * `getTestKey` callback parameterizes the real-vs-random split
  * Local `X3DH_ActiveMessageSecrecy` opaque Prop (KEM-free
    variant of `SecurityDefs.MessageSecrecy`)

The `## Follow-up work` section at the end of the file enumerates
11 remaining items with status markers (✓/🚧/☐) and their
dependencies.

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

Author: jinxinglim