theorem X3DH_handshake_correct.{u_1, u_2, u_3,
    u_4, u_5}
  {FType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  FType u_5] {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  FType u_5 GType u_1]
  {SKType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PTType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {CT_aeadType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (kdfKDF (G × G × G × G) SK : KDFKDF.{u_1, u_2} (I : Type u_1) (K : Type u_2) : Type (max u_1 u_2)KDF as a deterministic function, for correctness proofs.  (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. SKType u_2)
  (aeadAEAD SK PT CT_aead (G × G) : AEADAEAD.{u_1, u_2, u_3, u_4} (K : Type u_1) (PT : Type u_2) (CT : Type u_3) (AD : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
and associated data `AD`. The `correctness` field guarantees that decrypting
an honestly encrypted ciphertext with the correct key and AD recovers the
original plaintext.  SKType u_2 PTType u_3 CT_aeadType u_4 (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.GType u_1 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. GType u_1)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.)
  {G₀G : GType u_1}
  (ikₐKeyPair F G G₀ ekₐKeyPair F G G₀ ikᵦKeyPair F G G₀ spkᵦKeyPair F G G₀ : KeyPairKeyPair.{u_1, u_2} (F : Type u_1) (G : Type u_2) [Field F] [AddCommGroup G] [Module F G] (G₀ : G) : Type (max u_1 u_2)A key pair: private scalar and public group element satisfying
pub = DH(priv, G₀). The paper defines four key types: identity (IK),
signed prekey (SPK), one-time prekey (OPK), and ephemeral (EK).  FType u_5 GType u_1 G₀G)
  (opkᵦOption (KeyPair F G G₀) : OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 (KeyPairKeyPair.{u_1, u_2} (F : Type u_1) (G : Type u_2) [Field F] [AddCommGroup G] [Module F G] (G₀ : G) : Type (max u_1 u_2)A key pair: private scalar and public group element satisfying
pub = DH(priv, G₀). The paper defines four key types: identity (IK),
signed prekey (SPK), one-time prekey (OPK), and ephemeral (EK).  FType u_5 GType u_1 G₀G))
  (msgPT : PTType u_3) (ctCT_aead : CT_aeadType u_4)
  (h_encct =
  aead.encrypt (X3DH_SK_Alice kdf ikₐ.priv ekₐ.priv ikᵦ.pub spkᵦ.pub (Option.map KeyPair.pub opkᵦ)) msg
    (ikₐ.pub, ikᵦ.pub) :
    ctCT_aead =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      aeadAEAD SK PT CT_aead (G × G).encryptAEAD.encrypt.{u_1, u_2, u_3, u_4} {K : Type u_1} {PT : Type u_2} {CT : Type u_3} {AD : Type u_4}
  (self : AEAD K PT CT AD) : K → PT → AD → CT
        (X3DH_SK_AliceX3DH_SK_Alice.{u_1, u_2, u_3} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] {SK : Type u_3}
  (kdf : KDF (G × G × G × G) SK) (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G) (OPKᵦ : Option G) : SKAlice derives the session key SKₐ = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4).  kdfKDF (G × G × G × G) SK ikₐKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F
          ekₐKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F ikᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G spkᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G
          (Option.mapOption.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option βApply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
 KeyPair.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G opkᵦOption (KeyPair F G G₀)))
        msgPT (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.ikₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ikᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.) :
  aeadAEAD SK PT CT_aead (G × G).decryptAEAD.decrypt.{u_1, u_2, u_3, u_4} {K : Type u_1} {PT : Type u_2} {CT : Type u_3} {AD : Type u_4}
  (self : AEAD K PT CT AD) : K → CT → AD → Option PT
      (X3DH_SK_BobX3DH_SK_Bob.{u_1, u_2, u_3} {F : Type u_1} [Field F] {G : Type u_2} [AddCommGroup G] [Module F G] {SK : Type u_3}
  (kdf : KDF (G × G × G × G) SK) (ikᵦ spkᵦ : F) (opkᵦ : Option F) (IKₐ EKₐ : G) : SKBob derives the session key SKᵦ = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4).  kdfKDF (G × G × G × G) SK ikᵦKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F spkᵦKeyPair F G G₀.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F
        (Option.mapOption.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) : Option α → Option βApply a function to an optional value, if present.

From the perspective of `Option` as a container with at most one value, this is analogous to
`List.map`. It can also be accessed via the `Functor Option` instance.

Examples:
 * `(none : Option Nat).map (· + 1) = none`
 * `(some 3).map (· + 1) = some 4`
 KeyPair.privKeyPair.priv.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : F opkᵦOption (KeyPair F G G₀))
        ikₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G ekₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G)
      ctCT_aead (Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`.ikₐKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G,Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. ikᵦKeyPair F G G₀.pubKeyPair.pub.{u_1, u_2} {F : Type u_1} {G : Type u_2} [Field F] [AddCommGroup G] [Module F G] {G₀ : G}
  (self : KeyPair F G G₀) : G)Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × βConstructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    someOption.some.{u} {α : Type u} (val : α) : Option αSome value of type `α`.  msgPT