structure DY.PersistentGlobalState.State.ExecEntryT (StateT : Type) : Type

• st : StateT

def DY.PersistentGlobalState.State.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] (StateT : Type) : SubBaseAttackerKnowledge (ExecEntryT StateT)

Equations

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

def DY.PersistentGlobalState.storeGlobalState {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (State.ExecEntryT StateT)] (st : StateT) : Traceful Nat

Equations

• DY.PersistentGlobalState.storeGlobalState st = DY.appendEntry { st := st }

def DY.PersistentGlobalState.getGlobalState {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (State.ExecEntryT StateT)] (handle : Nat) : Traceful StateT

Equations

• DY.PersistentGlobalState.getGlobalState handle = do let e ← DY.getEntry handle pure e.st

class DY.PersistentGlobalState.GlobalStateInv [ExecTraceTypes] [ProofTraceTypes] (StateT : Type) : Type

• invariant : StateT → ProofTrace → Prop
• invariant_later (st : StateT) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → invariant st tr1 → invariant st tr2

@[reducible, inline]

abbrev DY.PersistentGlobalState.State.ProofEntryT (StateT : Type) : Type

Equations

• DY.PersistentGlobalState.State.ProofEntryT StateT = DY.PersistentGlobalState.State.ExecEntryT StateT

@[instance_reducible]

instance DY.PersistentGlobalState.State.instErasableProofEntryExecEntryTProofEntryT (StateT : Type) : ErasableProofEntry (ExecEntryT StateT) (ProofEntryT StateT)

Equations

• DY.PersistentGlobalState.State.instErasableProofEntryExecEntryTProofEntryT StateT = DY.ErasableProofEntry.default (DY.PersistentGlobalState.State.ExecEntryT StateT)

@[instance_reducible]

instance DY.PersistentGlobalState.State.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT (StateT : Type) : ExecEntryAssociatedWithProofEntry (ExecEntryT StateT) (ProofEntryT StateT)

Equations

• DY.PersistentGlobalState.State.instExecEntryAssociatedWithProofEntryExecEntryTProofEntryT StateT = { }

@[instance_reducible]

instance DY.PersistentGlobalState.State.instSubTraceInvariantExecEntryTProofEntryTOfGlobalStateInv [ExecTraceTypes] [ProofTraceTypes] (StateT : Type) [GlobalStateInv StateT] : SubTraceInvariant (ProofEntryT StateT)

Equations

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

instance DY.PersistentGlobalState.State.baseAttackerKnowledgeTheorem [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [BytesFunctor] [BytesInvariants] (StateT : Type) [ExecTraceTypes.Has (ExecEntryT StateT)] [ProofTraceTypes.Has (ProofEntryT StateT)] [GlobalStateInv StateT] [TraceInvariant.Has (ProofEntryT StateT)] : SubBaseAttackerKnowledgeTheorem (ProofEntryT StateT) (baseAttackerKnowledge StateT)

instance DY.PersistentGlobalState.storeGlobalState.proof {StateT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [GlobalStateInv StateT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ProofTraceTypes.Has (State.ProofEntryT StateT)] [TraceInvariant.Has (State.ProofEntryT StateT)] (st : StateT) : HoareTriple (storeGlobalState st) (fun (tr : ProofTrace) => GlobalStateInv.invariant st tr) fun (x : Nat) (x_1 : ProofTrace) => True

instance DY.PersistentGlobalState.getGlobalState.proof {StateT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [GlobalStateInv StateT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ProofTraceTypes.Has (State.ProofEntryT StateT)] [TraceInvariant.Has (State.ProofEntryT StateT)] (handle : Nat) : HoareTriple (getGlobalState handle) (fun (x : ProofTrace) => True) fun (st : StateT) (tr : ProofTrace) => GlobalStateInv.invariant st tr

structure DY.PersistentGlobalState.Compromise.CompromiseEvent (StateT : Type) : Type

• state : StateT

def DY.PersistentGlobalState.Compromise.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (StateT : Type) (id✝ : Fin 1) : SubBaseAttackerKnowledge (ExecEntryT.internal StateT id✝)

Equations

• DY.PersistentGlobalState.Compromise.baseAttackerKnowledge.internal StateT 0 = DY.ProtocolEvent.baseAttackerKnowledge (DY.PersistentGlobalState.Compromise.CompromiseEvent StateT)
• DY.PersistentGlobalState.Compromise.baseAttackerKnowledge.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentGlobalState.Compromise.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] (StateT : Type) : SubBaseAttackerKnowledge (ExecEntryT StateT)

Equations

• DY.PersistentGlobalState.Compromise.baseAttackerKnowledge StateT = DY.SubBaseAttackerKnowledge.combine (DY.PersistentGlobalState.Compromise.baseAttackerKnowledge.internal StateT)

def DY.PersistentGlobalState.Compromise.ExecEntryT.internal (StateT : Type) : Fin 1 → Type

Equations

• DY.PersistentGlobalState.Compromise.ExecEntryT.internal StateT 0 = DY.ProtocolEvent.ExecEntryT (DY.PersistentGlobalState.Compromise.CompromiseEvent StateT)
• DY.PersistentGlobalState.Compromise.ExecEntryT.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentGlobalState.Compromise.ExecEntryT (StateT : Type) : Type

Equations

• DY.PersistentGlobalState.Compromise.ExecEntryT StateT = DY.ExecTraceTypes.combine (DY.PersistentGlobalState.Compromise.ExecEntryT.internal StateT)

def DY.PersistentGlobalState.compromise (StateT : Type) [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [Comparse.ParseableSerializeable StateT] [ExecTraceTypes] [ExecTraceTypes.Has Network.ExecEntryT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (handle : Nat) : Traceful Nat

Equations

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

def DY.PersistentGlobalState.GlobalStateCompromised {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (state : StateT) (tr : ExecTrace) : Prop

Equations

• DY.PersistentGlobalState.GlobalStateCompromised state tr = DY.Trace.EventLogged { state := state } tr

theorem DY.PersistentGlobalState.GlobalStateCompromised_le {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (state : StateT) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → GlobalStateCompromised state tr1 → GlobalStateCompromised state tr2

@[instance_reducible]

instance DY.PersistentGlobalState.Compromise.instEventInvCompromiseEvent {StateT : Type} [ExecTraceTypes] [ProofTraceTypes] : ProtocolEvent.EventInv (CompromiseEvent StateT)

Equations

• DY.PersistentGlobalState.Compromise.instEventInvCompromiseEvent = { invariant := fun (x : DY.ProofTrace) (x_1 : DY.PersistentGlobalState.Compromise.CompromiseEvent StateT) => True }

@[instance_reducible]

def DY.PersistentGlobalState.Compromise.ProofEntryT (StateT : Type) : Type

Equations

• DY.PersistentGlobalState.Compromise.ProofEntryT StateT = DY.ProofTraceTypes.combine (DY.PersistentGlobalState.Compromise.ProofEntryT.internal StateT)

def DY.PersistentGlobalState.Compromise.ProofEntryT.internal (StateT : Type) : Fin 1 → Type

Equations

• DY.PersistentGlobalState.Compromise.ProofEntryT.internal StateT 0 = DY.ProtocolEvent.ProofEntryT (DY.PersistentGlobalState.Compromise.CompromiseEvent StateT)
• DY.PersistentGlobalState.Compromise.ProofEntryT.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

def DY.PersistentGlobalState.label {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (state : StateT) : Label

Equations

• DY.PersistentGlobalState.label state = DY.ProtocolEvent.label { state := state }

theorem DY.PersistentGlobalState.label_isCorrupt {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (state : StateT) (tr : ExecTrace) : (label state).isCorrupt tr = GlobalStateCompromised state tr

class DY.PersistentGlobalState.CompromisableGlobalStateInv (StateT : Type) [ExecTraceTypes] [ProofTraceTypes] [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [BytesInvariants] [Comparse.ParseableSerializeable StateT] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] extends DY.PersistentGlobalState.GlobalStateInv StateT : Type

• invariant : StateT → ProofTrace → Prop
• invariant_later (st : StateT) (tr1 tr2 : ProofTrace) : tr1 ≤ tr2 → invariant st tr1 → invariant st tr2
• invariant_implies_KnowableBy (state : StateT) (tr : ProofTrace) : GlobalStateInv.invariant state tr → Comparse.IsWellFormed (Bytes.KnowableBy (label state)) state tr

instance DY.PersistentGlobalState.compromise.proof {StateT : Type} [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] [Comparse.ParseableSerializeable StateT] [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [ExecTraceTypes.Has Network.ExecEntryT] [ProofTraceTypes.Has Network.ProofEntryT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ProofTraceTypes.Has (State.ProofEntryT StateT)] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] [ProofTraceTypes.Has (Compromise.ProofEntryT StateT)] [BytesInvariants] [BytesInvariantsProofs] [Comparse.ParseableSerializeable StateT] [CompromisableGlobalStateInv StateT] [TraceInvariant.Has Network.ProofEntryT] [TraceInvariant.Has (State.ProofEntryT StateT)] [TraceInvariant.Has (Compromise.ProofEntryT StateT)] (handle : Nat) : HoareTriple (compromise StateT handle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

def DY.PersistentGlobalState.CompromisableState.ExecEntryT.internal (StateT : Type) : Fin 2 → Type

Equations

• DY.PersistentGlobalState.CompromisableState.ExecEntryT.internal StateT 0 = DY.PersistentGlobalState.State.ExecEntryT StateT
• DY.PersistentGlobalState.CompromisableState.ExecEntryT.internal StateT 1 = DY.PersistentGlobalState.Compromise.ExecEntryT StateT
• DY.PersistentGlobalState.CompromisableState.ExecEntryT.internal StateT ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge [BytesFunctor] [ExecTraceTypes] (StateT : Type) : SubBaseAttackerKnowledge (ExecEntryT StateT)

Equations

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

@[instance_reducible]

def DY.PersistentGlobalState.CompromisableState.ExecEntryT (StateT : Type) : Type

Equations

• DY.PersistentGlobalState.CompromisableState.ExecEntryT StateT = DY.ExecTraceTypes.combine (DY.PersistentGlobalState.CompromisableState.ExecEntryT.internal StateT)

def DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (StateT : Type) (id✝ : Fin 2) : SubBaseAttackerKnowledge (ExecEntryT.internal StateT id✝)

Equations

• DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge.internal StateT 0 = DY.PersistentGlobalState.State.baseAttackerKnowledge StateT
• DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge.internal StateT 1 = DY.PersistentGlobalState.Compromise.baseAttackerKnowledge StateT
• DY.PersistentGlobalState.CompromisableState.baseAttackerKnowledge.internal StateT ⟨n.succ.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentGlobalState.CompromisableState.ProofEntryT (StateT : Type) : Type

Equations

• DY.PersistentGlobalState.CompromisableState.ProofEntryT StateT = DY.ProofTraceTypes.combine (DY.PersistentGlobalState.CompromisableState.ProofEntryT.internal StateT)

def DY.PersistentGlobalState.CompromisableState.ProofEntryT.internal (StateT : Type) : Fin 2 → Type

Equations

• DY.PersistentGlobalState.CompromisableState.ProofEntryT.internal StateT 0 = DY.PersistentGlobalState.State.ProofEntryT StateT
• DY.PersistentGlobalState.CompromisableState.ProofEntryT.internal StateT 1 = DY.PersistentGlobalState.Compromise.ProofEntryT StateT
• DY.PersistentGlobalState.CompromisableState.ProofEntryT.internal StateT ⟨n.succ.succ, isLt⟩ = ⋯.elim