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. The `activeGame` body
is fully wired with two-pass `simulateQ` semantics, so `activeReal`,
`activeRand`, and `activeSecrecyAdvantage` are now executable
end-to-end (modulo the `send` and `test`-freshness sorries).

Key components:
  * `SessionStatus`, `AliceSessionRecord`, `BobSessionRecord` —
    per-side session state under fixed-roles (Alice always
    initiator, Bob always responder); each carries a
    `transcript : List X3DHMessage` field for partnering
  * `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;
    `newSession` initializes `transcript := []`
  * `AKEStateM` — `StateT (ActiveGameState) (OracleComp ...)`
  * `activeGame` — fully wired two-pass `simulateQ`:
      pass 1 in `AKEStateM` interprets `akeSpec`; `StateT.run'`
      strips the state layer; pass 2 mirrors passive's `execGame`
      to land in `ProbComp`
  * `activeReal` / `activeRand` — instantiate the `getTestKey`
    callback differently (real key pass-through vs fresh-sample)
  * `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"
  * `transcript` field is `List X3DHMessage` on each record;
    only `send` (when implemented) appends to it
  * `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