class DY.KEM.CanKem (Bytes : Type u) : Type u

• kemPk (sk : Bytes) : Bytes
• kemEncap (pk entropy : Bytes) : Bytes × Bytes
• kemDecap (sk cipher : Bytes) : Err Bytes

structure DY.KEM.Pk.SubF (Bytes : Type) : Type

• sk : Bytes

@[instance_reducible]

instance DY.KEM.Pk.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• DY.KEM.Pk.instFunctorSizeOfSubF = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.KEM.Pk.SubF t) => match x with | { sk := sk } => sizeOf sk }

@[instance_reducible]

instance DY.KEM.Pk.instRepresentableSubF : ALaCarte.Representable SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Pk.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Pk.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Pk.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.Pk.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 800

structure DY.KEM.Encap.SubF (Bytes : Type) : Type

• pk : Bytes
• entropy : Bytes

@[instance_reducible]

instance DY.KEM.Encap.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Encap.instRepresentableSubF : ALaCarte.Representable SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Encap.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Encap.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.Encap.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.Encap.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 768

structure DY.KEM.SharedSecret.SubF (Bytes : Type) : Type

• entropy : Bytes

@[instance_reducible]

instance DY.KEM.SharedSecret.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

• DY.KEM.SharedSecret.instFunctorSizeOfSubF = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.KEM.SharedSecret.SubF t) => match x with | { entropy := entropy } => sizeOf entropy }

@[instance_reducible]

instance DY.KEM.SharedSecret.instRepresentableSubF : ALaCarte.Representable SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.SharedSecret.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.SharedSecret.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DY.KEM.SharedSecret.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.SharedSecret.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• x✝¹.length x✝ = 32

def DY.KEM.SubF.internal : Fin 3 → Type → Type

Equations

• DY.KEM.SubF.internal 0 = DY.KEM.Pk.SubF
• DY.KEM.SubF.internal 1 = DY.KEM.Encap.SubF
• DY.KEM.SubF.internal 2 = DY.KEM.SharedSecret.SubF
• DY.KEM.SubF.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

def DY.KEM.SubF.length.internal [BytesFunctor] (id✝ : Fin 3) : Bytes.PartialLength (SubF.internal id✝)

Equations

• DY.KEM.SubF.length.internal 0 = DY.KEM.Pk.SubF.length
• DY.KEM.SubF.length.internal 1 = DY.KEM.Encap.SubF.length
• DY.KEM.SubF.length.internal 2 = DY.KEM.SharedSecret.SubF.length
• DY.KEM.SubF.length.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.KEM.SubF : Type → Type

Equations

• DY.KEM.SubF = DY.BytesFunctor.combine DY.KEM.SubF.internal

@[instance_reducible]

def DY.KEM.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.KEM.SubF.length = DY.Bytes.PartialLength.combine DY.KEM.SubF.length.internal

@[reducible, inline]

abbrev DY.KEM.Pk.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[reducible, inline]

abbrev DY.KEM.Encap.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[reducible, inline]

abbrev DY.KEM.SharedSecret.SubF.pack [BytesFunctor] [BytesFunctor.Has SubF] (x : SubF Bytes) : Bytes

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.KEM.instCanKemBytes [BytesFunctor] [BytesFunctor.Has SubF] : CanKem Bytes

Equations

• One or more equations did not get rendered due to their size.

theorem DY.KEM.kemDecap_kemEncap [BytesFunctor] [BytesFunctor.Has SubF] (sk entropy : Bytes) : match kemEncap (kemPk sk) entropy with | (cipher, ss) => kemDecap sk cipher = some ss

def DY.KEM.kemPkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : Err Bytes

Equations

• DY.KEM.kemPkInvert pk = match pk.view? DY.KEM.Pk.SubF with | some { sk := sk } => some sk | none => none

theorem DY.KEM.kemPkInvert_kemPk [BytesFunctor] [BytesFunctor.Has SubF] (sk : Bytes) : kemPkInvert (kemPk sk) = some sk

theorem DY.KEM.kemPk_kemPkInvert [BytesFunctor] [BytesFunctor.Has SubF] (pk : Bytes) : match kemPkInvert pk with | none => True | some sk => kemPk sk = pk

def DY.KEM.kemPk.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.KEM.kemPk.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (sk : DY.Bytes), out = DY.KEM.kemPk sk ∧ p sk, pred_isScottContinuous := ⋯ }

def DY.KEM.kemEncapCipher.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.kemEncapSS.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.kemDecap.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

def DY.KEM.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.KEM.attackerKnowledge = DY.SubAttackerKnowledge.combine' DY.KEM.attackerKnowledge.internal

def DY.KEM.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 4 → SubAttackerKnowledge SubF

Equations

• DY.KEM.attackerKnowledge.internal 0 = DY.KEM.kemPk.attackerKnowledge
• DY.KEM.attackerKnowledge.internal 1 = DY.KEM.kemEncapCipher.attackerKnowledge
• DY.KEM.attackerKnowledge.internal 2 = DY.KEM.kemEncapSS.attackerKnowledge
• DY.KEM.attackerKnowledge.internal 3 = DY.KEM.kemDecap.attackerKnowledge
• DY.KEM.attackerKnowledge.internal ⟨n.succ.succ.succ.succ, isLt⟩ = ⋯.elim

theorem DY.KEM.kemPk.attacker_knows [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (sk : Bytes) (tr : ExecTrace) : sk.AttackerKnows tr → (kemPk sk).AttackerKnows tr

theorem DY.KEM.kemEncap.attacker_knows [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (pk entropy : Bytes) (tr : ExecTrace) : pk.AttackerKnows tr → entropy.AttackerKnows tr → (kemEncap pk entropy).fst.AttackerKnows tr ∧ (kemEncap pk entropy).snd.AttackerKnows tr

theorem DY.KEM.kemDecap.attacker_knows [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (sk cipher : Bytes) (tr : ExecTrace) : sk.AttackerKnows tr → cipher.AttackerKnows tr → match kemDecap sk cipher with | none => True | some ss => ss.AttackerKnows tr

structure DY.KEM.Broken.BrokenKemEvent [BytesFunctor] : Type

• brokenPk : Bytes

@[instance_reducible]

def DY.KEM.Broken.ExecEntryT [BytesFunctor] : Type

Equations

• DY.KEM.Broken.ExecEntryT = DY.ExecTraceTypes.combine DY.KEM.Broken.ExecEntryT.internal

def DY.KEM.Broken.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (id✝ : Fin 1) : SubBaseAttackerKnowledge (ExecEntryT.internal id✝)

Equations

• DY.KEM.Broken.baseAttackerKnowledge.internal 0 = DY.ProtocolEvent.baseAttackerKnowledge DY.KEM.Broken.BrokenKemEvent
• DY.KEM.Broken.baseAttackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.KEM.Broken.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.KEM.Broken.baseAttackerKnowledge = DY.SubBaseAttackerKnowledge.combine DY.KEM.Broken.baseAttackerKnowledge.internal

def DY.KEM.Broken.ExecEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.KEM.Broken.ExecEntryT.internal 0 = DY.ProtocolEvent.ExecEntryT DY.KEM.Broken.BrokenKemEvent
• DY.KEM.Broken.ExecEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

def DY.KEM.Broken.ThisKemPkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) (tr : ExecTrace) : Prop

Equations

• DY.KEM.Broken.ThisKemPkHasBeenBroken brokenPk tr = DY.Trace.EventLogged { brokenPk := brokenPk } tr

def DY.KEM.Broken.OneKemPkHasBeenBroken [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (tr : ExecTrace) : Prop

Equations

• DY.KEM.Broken.OneKemPkHasBeenBroken tr = ∃ (brokenPk : DY.Bytes), DY.KEM.Broken.ThisKemPkHasBeenBroken brokenPk tr

def DY.KEM.Broken.label [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (brokenPk : Bytes) : Label

Equations

• DY.KEM.Broken.label brokenPk = { isCorrupt := fun (tr : DY.ExecTrace) => DY.KEM.Broken.ThisKemPkHasBeenBroken brokenPk tr, isCorruptLater := ⋯ }

def DY.KEM.Broken.breakKemPk [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] (msgHandle : Nat) : Traceful Nat

Equations

• One or more equations did not get rendered due to their size.

def DY.KEM.Broken.breakKemPk.reachability [BytesFunctor] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Network.ExecEntryT] : ReachabilityConfig

Equations

• DY.KEM.Broken.breakKemPk.reachability = DY.ReachabilityConfig.make fun (handle : Nat) => DY.KEM.Broken.breakKemPk handle

def DY.KEM.Pk.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

• One or more equations did not get rendered due to their size.

theorem DY.KEM.Pk.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[simp]

theorem DY.KEM.kemPk.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Pk.invariants] (inp : Bytes) (tr : ProofTrace) : (kemPk inp).WellFormed tr = inp.WellFormed tr

@[simp]

theorem DY.KEM.kemPk.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Pk.invariants] (inp : Bytes) (tr : ProofTrace) : (kemPk inp).label tr = Label.pub

@[simp]

theorem DY.KEM.kemPk.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has Pk.invariants] (sk : Bytes) (tr : ProofTrace) : sk.Invariant tr → (sk.label tr).canFlow (Broken.label (kemPk sk)) (Trace.erase tr) → (kemPk sk).Invariant tr

def DY.Bytes.KemSkHasUsage [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (pk : Bytes) (skUsg : Usage) (tr : ProofTrace) : Prop

Equations

• pk.KemSkHasUsage skUsg tr = DY.Bytes.XXXHasUsage DY.KEM.extractKemSk✝ pk skUsg tr

theorem DY.Bytes.KemSkHasUsage_kemPk [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (sk : Bytes) (skUsg : Usage) (tr : ProofTrace) : (KEM.kemPk sk).KemSkHasUsage skUsg tr = sk.HasUsage skUsg tr

theorem DY.Bytes.KemSkHasUsage_later [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ExecTraceTypes.Has KEM.Broken.ExecEntryT] [BytesInvariants.Has KEM.Pk.invariants] [GetUsageLater] [GetLabelLater] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.KemSkHasUsage usg tr1 → b.KemSkHasUsage usg tr2

theorem DY.Bytes.KemSkHasUsage_later_fast [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has KEM.Broken.ExecEntryT] [BytesInvariants.Has KEM.Pk.invariants] (b : Bytes) (usg : Usage) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.KemSkHasUsage usg tr1 → b.KemSkHasUsage usg tr2

noncomputable def DY.Bytes.kemSkLabel [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [GetLabel] (pk : Bytes) (tr : ProofTrace) : Label

Equations

• pk.kemSkLabel tr = DY.Bytes.xxxLabel DY.KEM.extractKemSk✝ pk tr

theorem DY.Bytes.kemSkLabel_kemPk [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ExecTraceTypes.Has KEM.Broken.ExecEntryT] [BytesInvariants.Has KEM.Pk.invariants] (sk : Bytes) (tr : ProofTrace) : (KEM.kemPk sk).kemSkLabel tr = sk.label tr

theorem DY.Bytes.kemSkLabel_later [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [ExecTraceTypes.Has KEM.Broken.ExecEntryT] [BytesInvariants.Has KEM.Pk.invariants] [GetLabelLater] (b : Bytes) (tr1 tr2 : ProofTrace) : b.WellFormed tr1 → tr1 ≤ tr2 → b.kemSkLabel tr1 = b.kemSkLabel tr2

theorem DY.Bytes.kemSkLabel_later_fast [BytesFunctor] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesInvariantsProofs] [ExecTraceTypes.Has KEM.Broken.ExecEntryT] [BytesInvariants.Has KEM.Pk.invariants] (b : Bytes) (tr1 tr2 : ProofTrace) : b.Invariant tr1 → tr1 ≤ tr2 → b.kemSkLabel tr1 = b.kemSkLabel tr2

def DY.KEM.Encap.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has KEM.SubF] : Bytes.PartialInvariants SubF

Equations

• One or more equations did not get rendered due to their size.

theorem DY.KEM.Encap.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has KEM.SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has Pk.invariants] : Bytes.PartialInvariantsProofs invariants

def DY.KEM.SharedSecret.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] : Bytes.PartialInvariants SubF

Equations

• One or more equations did not get rendered due to their size.

theorem DY.KEM.SharedSecret.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

def DY.KEM.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] (id✝ : Fin 3) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.KEM.invariants.internal 0 = DY.KEM.Pk.invariants
• DY.KEM.invariants.internal 1 = DY.KEM.Encap.invariants
• DY.KEM.invariants.internal 2 = DY.KEM.SharedSecret.invariants
• DY.KEM.invariants.internal ⟨n.succ.succ.succ, isLt⟩ = ⋯.elim

theorem DY.KEM.invariantsProofs [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has Pk.invariants] : Bytes.PartialInvariantsProofs invariants

theorem DY.KEM.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has Pk.invariants] (id✝ : Fin 3) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

@[instance_reducible]

def DY.KEM.invariants [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] : Bytes.PartialInvariants SubF

Equations

• DY.KEM.invariants = DY.Bytes.PartialInvariants.combine DY.KEM.invariants.internal

theorem DY.KEM.kemEncap.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk entropy : Bytes) (tr : ProofTrace) : match kemEncap pk entropy with | (cipher, ss) => cipher.WellFormed tr = (pk.WellFormed tr ∧ entropy.WellFormed tr) ∧ ss.WellFormed tr = entropy.WellFormed tr

theorem DY.KEM.kemEncap.ss_label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk entropy : Bytes) (tr : ProofTrace) : match kemEncap pk entropy with | (fst, ss) => ss.label tr = entropy.label tr

theorem DY.KEM.kemDecap.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (sk cipher : Bytes) (tr : ProofTrace) : match kemDecap sk cipher with | none => True | some ss => (sk.WellFormed tr ∧ ss.WellFormed tr) = cipher.WellFormed tr

instance DY.KEM.kemPk_hoareTriple [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (sk : Bytes) : HoareTriplePure (kemPk sk) (fun (tr : ProofTrace) => sk.Invariant tr ∧ (sk.label tr).canFlow (Broken.label (kemPk sk)) (Trace.erase tr)) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = Label.pub

instance DY.KEM.kemEncap_hoareTriple [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] (pk entropy : Bytes) : HoareTriplePure (kemEncap pk entropy) (fun (tr : ProofTrace) => pk.Invariant tr ∧ entropy.Invariant tr ∧ (entropy.label tr).canFlow (pk.kemSkLabel tr) (Trace.erase tr)) fun (x : Bytes × Bytes) (tr : ProofTrace) => match x with | (cipher, ss) => cipher.Publishable tr ∧ ss.Invariant tr ∧ ss.label tr = entropy.label tr

instance DY.KEM.kemDecap_hoareTriple [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants] [BytesInvariants.Has invariants] [TraceInvariant] (sk cipher : Bytes) : HoareTriple (kemDecap sk cipher) (fun (tr : ProofTrace) => sk.Invariant tr ∧ cipher.Invariant tr) fun (ss : Bytes) (tr : ProofTrace) => kemDecap sk cipher = some ss ∧ ss.Invariant tr ∧ (ss.label tr).canFlow (sk.label tr) (Trace.erase tr)

instance DY.KEM.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem kemPk.attackerKnowledge

instance DY.KEM.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_1 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem kemEncapCipher.attackerKnowledge

instance DY.KEM.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_2 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem kemEncapSS.attackerKnowledge

instance DY.KEM.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge_3 [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has Broken.ExecEntryT] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem kemDecap.attackerKnowledge

@[instance_reducible]

instance DY.KEM.Broken.instEventInvBrokenKemEvent [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : ProtocolEvent.EventInv BrokenKemEvent

Equations

• DY.KEM.Broken.instEventInvBrokenKemEvent = { invariant := fun (x : DY.ProofTrace) (x_1 : DY.KEM.Broken.BrokenKemEvent) => True }

def DY.KEM.Broken.ProofEntryT.internal [BytesFunctor] : Fin 1 → Type

Equations

• DY.KEM.Broken.ProofEntryT.internal 0 = DY.ProtocolEvent.ProofEntryT DY.KEM.Broken.BrokenKemEvent
• DY.KEM.Broken.ProofEntryT.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.KEM.Broken.ProofEntryT [BytesFunctor] : Type

Equations

• DY.KEM.Broken.ProofEntryT = DY.ProofTraceTypes.combine DY.KEM.Broken.ProofEntryT.internal

instance DY.KEM.Broken.instReachableImpliesInvariantReachability [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesFunctor.Has SubF] [ExecTraceTypes.Has ExecEntryT] [BytesInvariants.Has invariants] [BytesInvariantsProofs] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has ProofEntryT] : ReachableImpliesInvariant breakKemPk.reachability