The session-model parameters for PQXDH sessions (spqrOffSessionParams W.C with V1 SPQR pqxdhSpqrSession W replacing spqrOffB; spqrOffSessionParams W.C stays untouched for the SPQR-off statements, SmDir.lean).

Alice's record extras after init (process_prekey_bundle):

• pending: one-time pre-key id (if any), signed pre-key id, Alice's base key base, timestamp 0 (DEV-PQ8);

• kyber: the Kyber pre-key id and the serialized ciphertext 0x08 ‖ ct (set_kyber_ciphertext, set_unacknowledged_kyber_pre_key_id);

• the registration ids: me's local id and the bundle's remote id;

• alice_base_key: Alice's own base key, serialized.

The model's input to Model.initiateKeys for me, bundle b and tape t:

• Alice's identity key pair is me.idPriv's;

• the base key's scalar is tape bytes 0..32 (KeyPair::generate, which clamps; so does x25519);

• the Kyber coins are initiateKemCoins t (DEV-PQ6);

• the peer is trusted (DEV-PQ5).

Kyber keys are raw (1568 bytes, no type byte), as in the model.

Alice's state after init in the model, for party P, identity me, bundle b and tape t, with the record extras it is encoded under (none: null):

1. Model.initiateKeys gives the handshake keys (rk, ck, pqr) and header (else null);

2. initializeInitiatorSession uses V1 SPQR (pqxdhSpqrSession W), Alice's and the peer's identity keys, the peer's signed pre-key as their ratchet key, and the ratchet key from tape bytes 160..192 (else null: all-zero DH);

3. setUnacknowledgedPreKeyMessage.

The ghost epochs are those of Params.initA (epoch 0, one receiver chain of epoch 0); they are not encoded.

Bob's pre-key material: the pre-keys a pre-key message names, from Bob's stores (preKeysNamedBy, SignalSession/PqDir.lean).

A PQXDH pre-key message (message version 4, with a Kyber payload). The inner SignalMessage is arbitrary bytes.

The wire bytes of a pre-key message, as PreKeySignalMessage::new writes them: versionByte 4 ‖ protobuf { pre_key_id?, base_key, identity_key, message, registration_id, signed_pre_key_id, kyber_pre_key_id, kyber_ciphertext }.

Bob's record extras after his pre-key recv (process_prekey): no pending pre-key (the session model's flag is clear after the successful decryption, so pending / kyber are not written), local registration id me's, remote id the message's, alice_base_key the message's base key, serialized.

The model's input to Model.acceptKeys for me, keys k and message m. Bob's identity and pre-key pairs are derived as libsignal derives them (keyPairOf). The one-time pre-key is k's iff m names its id (otherwise none, and acceptKeys rejects a named but missing key). Trusted peer (DEV-PQ5), no replay refusal (DEV-PQ8).

Bob's state after his pre-key recv in the model, for party P, identity me, keys k, message m, an empty record, and Bob's ratchet coins rc, with its record extras and the plaintext (none: abort; some none: null). Each step's failure gives null:

1. the inner message parses (SignalMessage.tryFrom);

2. m's signed and Kyber pre-key ids are k's (get_signed_pre_key, get_kyber_pre_key);

3. Model.acceptKeys gives (rk, ck, pqr);

4. initializeRecipientSession with V1 SPQR (pqxdhSpqrSession W) and the signed pre-key pair as Bob's ratchet key;

5. tryDecryptFromRecord (type PreKey, the addresses P expects, coins rc) gives the plaintext. A panic aborts.

The ghost epochs are those Params.receive gives from Params.initB on a first message (epoch 1, one receiver chain of epoch 1); they are not encoded.

The bundle's two signatures verify, exactly as Model.initiateKeys checks them (the model's sigVerify, i.e. xeddsaVerifyRef at modelPrims): the signed pre-key's signature on 0x05 ‖ spk_pub and the Kyber pre-key's on 0x08 ‖ kpk_pub, both under id_pub (process_prekey_bundle, rust/protocol/src/session.rs).