structure DY.Random.ExecEntryT : Type

• length : Nat

def DY.Random.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] : SubBaseAttackerKnowledge ExecEntryT

Equations

• DY.Random.baseAttackerKnowledge = { attackerKnows := fun (x : DY.ExecTrace) (x_1 : DY.Random.ExecEntryT) (x_2 : DY.Bytes) => False }

structure DY.Random.ProofEntryT [BytesFunctor] [ExecTraceTypes] : Type

• length : Nat
• label : Label
• usage : Usage

@[instance_reducible]

instance DY.Random.instErasableProofEntryExecEntryTProofEntryT [BytesFunctor] [ExecTraceTypes] : ErasableProofEntry ExecEntryT ProofEntryT

Equations

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

@[instance_reducible]

instance DY.Random.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT [BytesFunctor] [ExecTraceTypes] : ExecEntryAssociatedWithProofEntry ExecEntryT ProofEntryT

Equations

• DY.Random.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT = { }

@[instance_reducible]

instance DY.Random.instSubTraceInvariantExecEntryTProofEntryT [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] : SubTraceInvariant ProofEntryT

Equations

• DY.Random.instSubTraceInvariantExecEntryTProofEntryT = { invariant := fun (x : DY.ProofTrace) (x_1 : DY.Random.ProofEntryT) => True }

instance DY.Random.baseAttackerKnowledgeTheorem [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] : SubBaseAttackerKnowledgeTheorem ProofEntryT baseAttackerKnowledge

structure DY.Random.Random (Bytes : Type) : Type

• timestamp : Nat
• size : Nat

@[instance_reducible]

instance DY.Random.instFunctorSizeOfRandom : ALaCarte.FunctorSizeOf Random

Equations

• DY.Random.instFunctorSizeOfRandom = { sizeOf := fun {t : Type} [SizeOf t] (x : DY.Random.Random t) => match x with | { timestamp := timestamp, size := size } => 0 }

@[instance_reducible]

instance DY.Random.instRepresentableRandom : ALaCarte.Representable Random

Equations

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

@[instance_reducible]

instance DY.Random.instRepresentableDecidableEqRandom : ALaCarte.RepresentableDecidableEq Random

Equations

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

@[instance_reducible]

instance DY.Random.instRepresentableOrdRandom : ALaCarte.RepresentableOrd Random

Equations

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

@[instance_reducible]

instance DY.Random.instSubBytesFunctorRandom : SubBytesFunctor Random

Equations

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

@[reducible, inline]

abbrev DY.Random.SubF (Bytes : Type) : Type

Equations

• DY.Random.SubF = DY.Random.Random

def DY.Random.Random.length [BytesFunctor] : Bytes.PartialLength Random

Equations

• { timestamp := timestamp, size := size }.length x_2 = size

@[reducible, inline]

abbrev DY.Random.SubF.length [BytesFunctor] : Bytes.PartialLength SubF

Equations

• DY.Random.SubF.length = DY.Random.Random.length

@[reducible, inline]

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

Equations

• x.pack = DY.BytesView.pack x

def DY.Random.attKnowsRand [BytesFunctor] : SubAttackerKnowledge Random

Equations

• DY.Random.attKnowsRand = { pred := fun (p : DY.Bytes → Prop) (out : DY.Bytes) => False, pred_isScottContinuous := ⋯ }

@[reducible, inline]

abbrev DY.Random.attackerKnowledge [BytesFunctor] : SubAttackerKnowledge Random

Equations

• DY.Random.attackerKnowledge = DY.Random.attKnowsRand

def DY.Random.Random.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] : Bytes.PartialInvariants Random

Equations

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

@[reducible, inline]

abbrev DY.Random.invariants [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] : Bytes.PartialInvariants SubF

Equations

• DY.Random.invariants = DY.Random.Random.invariants

theorem DY.Random.Random.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

@[reducible, inline]

abbrev DY.Random.invariantsProofs [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [BytesInvariants] : Bytes.PartialInvariantsProofs invariants

Equations

• ⋯ = ⋯

instance DY.Random.instSubAttackerKnowledgeTheoremRandomAttKnowsRand [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] : SubAttackerKnowledgeTheorem attKnowsRand

def DY.Random.genRand [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (size : Nat) : Traceful Bytes

Equations

• DY.Random.genRand size = do let time ← DY.appendEntry { length := size } pure (DY.Random.makeRand✝ time size)

@[instance_reducible]

instance DY.Random.instHasGhostArgumentTypeTracefulBytesGenRandProdForallLabelUsage [BytesFunctor] [BytesFunctor.Has SubF] [ExecTraceTypes] [ExecTraceTypes.Has ExecEntryT] (size : Nat) : HasGhostArgumentType (genRand size) ((Bytes → Label) × Usage)

Equations

• DY.Random.instHasGhostArgumentTypeTracefulBytesGenRandProdForallLabelUsage size = { dummy := () }

instance DY.Random.genRand.spec [BytesFunctor] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesInvariants] [BytesInvariantsProofs] [BytesFunctor.Has SubF] [ExecTraceTypes.Has ExecEntryT] [ProofTraceTypes.Has ProofEntryT] [TraceInvariant.Has ProofEntryT] [BytesInvariants.Has invariants] (size : Nat) (label : Bytes → Label) (usage : Usage) : HoareTripleGhost (genRand size) (label, usage) (fun (x : ProofTrace) => True) fun (res : Bytes) (tr : ProofTrace) => res.Invariant tr ∧ res.label tr = label res ∧ res.HasUsage usage tr