class DY.Hash.CanHash (Bytes : Type u) : Type u

• hash (msg : Bytes) : Bytes

def DY.Hash.hashLength : Nat

Equations

• DY.Hash.hashLength = 32

@[simp]

theorem DY.Hash.hashLength_neq_0 : hashLength ≠ 0

structure DY.Hash.Hash.SubF (Bytes : Type) : Type

• input : Bytes

@[instance_reducible]

instance DY.Hash.Hash.instFunctorSizeOfSubF : ALaCarte.FunctorSizeOf SubF

Equations

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

@[instance_reducible]

instance DY.Hash.Hash.instRepresentableSubF : ALaCarte.Representable SubF

Equations

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

@[instance_reducible]

instance DY.Hash.Hash.instRepresentableDecidableEqSubF : ALaCarte.RepresentableDecidableEq SubF

Equations

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

@[instance_reducible]

instance DY.Hash.Hash.instRepresentableOrdSubF : ALaCarte.RepresentableOrd SubF

Equations

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

@[instance_reducible]

instance DY.Hash.Hash.instSubBytesFunctorSubF : SubBytesFunctor SubF

Equations

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

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

Equations

• x✝¹.length x✝ = DY.Hash.hashLength

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

Equations

• DY.Hash.SubF.length.internal 0 = DY.Hash.Hash.SubF.length
• DY.Hash.SubF.length.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

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

Equations

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

@[instance_reducible]

def DY.Hash.SubF : Type → Type

Equations

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

def DY.Hash.SubF.internal : Fin 1 → Type → Type

Equations

• DY.Hash.SubF.internal 0 = DY.Hash.Hash.SubF
• DY.Hash.SubF.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[reducible, inline]

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

Equations

• x.pack = DY.BytesView.pack x

@[instance_reducible]

instance DY.Hash.instCanHashBytes [BytesFunctor] [BytesFunctor.Has SubF] : CanHash Bytes

Equations

• DY.Hash.instCanHashBytes = { hash := fun (input : DY.Bytes) => { input := input }.pack }

theorem DY.Hash.hash_inj [BytesFunctor] [BytesFunctor.Has SubF] (inp1 inp2 : Bytes) : hash inp1 = hash inp2 → inp1 = inp2

@[simp]

theorem DY.Hash.length_hash [BytesFunctor] [BytesFunctor.Has SubF] [BytesLength] [BytesLength.Has SubF.length] (inp : Bytes) : (hash inp).length = hashLength

def DY.Hash.hash.attackerKnowledge [BytesFunctor] [BytesFunctor.Has SubF] : SubAttackerKnowledge SubF

Equations

• DY.Hash.hash.attackerKnowledge = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => ∃ (inp : DY.Bytes), out = DY.Hash.hash inp ∧ p inp, pred_isScottContinuous := ⋯ }

def DY.Hash.attackerKnowledge.internal [BytesFunctor] [BytesFunctor.Has SubF] : Fin 1 → SubAttackerKnowledge SubF

Equations

• DY.Hash.attackerKnowledge.internal 0 = DY.Hash.hash.attackerKnowledge
• DY.Hash.attackerKnowledge.internal ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

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

Equations

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

theorem DY.Hash.attacker_knows_hash [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [BaseAttackerKnowledge] [AttackerKnowledge] [AttackerKnowledge.Has attackerKnowledge] (inp : Bytes) (tr : ExecTrace) : inp.AttackerKnows tr → (hash inp).AttackerKnows tr

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

Equations

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

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

def DY.Hash.invariants.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] (id✝ : Fin 1) : Bytes.PartialInvariants (SubF.internal id✝)

Equations

• DY.Hash.invariants.internal 0 = DY.Hash.Hash.invariants
• DY.Hash.invariants.internal ⟨n.succ, isLt⟩ = ⋯.elim

theorem DY.Hash.invariantsProofs.internal [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [BytesInvariants] (id✝ : Fin 1) : Bytes.PartialInvariantsProofs (invariants.internal id✝)

@[instance_reducible]

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

Equations

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

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

@[simp]

theorem DY.Hash.hash.WellFormed [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (inp : Bytes) (tr : ProofTrace) : (hash inp).WellFormed tr = inp.WellFormed tr

@[simp]

theorem DY.Hash.hash.label [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (inp : Bytes) (tr : ProofTrace) : (hash inp).label tr = inp.label tr

@[simp]

theorem DY.Hash.hash.Invariant [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesFunctor.Has SubF] [BytesInvariants] [BytesInvariants.Has invariants] (inp : Bytes) (tr : ProofTrace) : (hash inp).Invariant tr = inp.Invariant tr

instance DY.Hash.instSubAttackerKnowledgeTheoremSubFAttackerKnowledge [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] [BytesFunctor.Has SubF] [BytesInvariants.Has invariants] : SubAttackerKnowledgeTheorem hash.attackerKnowledge