@[reducible, inline]

abbrev DY.Participant : Type

Equations

• DY.Participant = String

structure DY.PersistentLocalState.LocalState (StateT : Type) : Type

• participant : Participant
• state : StateT

theorem DY.PersistentLocalState.LocalState.IsWellFormed_eq {τ : Sort u_1} [BytesFunctor] [BytesLength] [BytesFunctor.Has Literal.SubF] [BytesLength.Has Literal.SubF.length] [BytesFunctor.Has Concat.SubF] [BytesLength.Has Concat.SubF.length] {StateT : Type} [Comparse.ParseableSerializeable StateT] (pre : Bytes → τ → Prop) [Comparse.BytesCompatibleTracePred pre] (x : LocalState StateT) (tr : τ) : Comparse.IsWellFormed pre x tr = Comparse.IsWellFormed pre x.state tr

def DY.PersistentLocalState.State.ExecEntryT.internal (StateT : Type) : Fin 1 → Type

Equations

• DY.PersistentLocalState.State.ExecEntryT.internal StateT 0 = DY.PersistentGlobalState.State.ExecEntryT (DY.PersistentLocalState.LocalState StateT)
• DY.PersistentLocalState.State.ExecEntryT.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentLocalState.State.ExecEntryT (StateT : Type) : Type

Equations

• DY.PersistentLocalState.State.ExecEntryT StateT = DY.ExecTraceTypes.combine (DY.PersistentLocalState.State.ExecEntryT.internal StateT)

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

Equations

• DY.PersistentLocalState.State.baseAttackerKnowledge.internal StateT 0 = DY.PersistentGlobalState.State.baseAttackerKnowledge (DY.PersistentLocalState.LocalState StateT)
• DY.PersistentLocalState.State.baseAttackerKnowledge.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

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

Equations

• DY.PersistentLocalState.State.baseAttackerKnowledge StateT = DY.SubBaseAttackerKnowledge.combine (DY.PersistentLocalState.State.baseAttackerKnowledge.internal StateT)

def DY.PersistentLocalState.storeLocalState {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (State.ExecEntryT StateT)] (participant : Participant) (state : StateT) : Traceful Nat

Equations

• DY.PersistentLocalState.storeLocalState participant state = DY.PersistentGlobalState.storeGlobalState { participant := participant, state := state }

def DY.PersistentLocalState.getLocalState {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (State.ExecEntryT StateT)] (participant : Participant) (handle : Nat) : Traceful StateT

Equations

• DY.PersistentLocalState.getLocalState participant handle = do let st ← DY.PersistentGlobalState.getGlobalState handle guard (st.participant = participant) pure st.state

class DY.PersistentLocalState.LocalStateInv [ExecTraceTypes] [ProofTraceTypes] (StateT : Type) : Type

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

@[instance_reducible]

instance DY.PersistentLocalState.State.instGlobalStateInvLocalStateOfLocalStateInv [ExecTraceTypes] [ProofTraceTypes] (StateT : Type) [LocalStateInv StateT] : PersistentGlobalState.GlobalStateInv (LocalState StateT)

Equations

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

def DY.PersistentLocalState.State.ProofEntryT.internal (StateT : Type) : Fin 1 → Type

Equations

• DY.PersistentLocalState.State.ProofEntryT.internal StateT 0 = DY.PersistentGlobalState.State.ProofEntryT (DY.PersistentLocalState.LocalState StateT)
• DY.PersistentLocalState.State.ProofEntryT.internal StateT ⟨n.succ, isLt⟩ = ⋯.elim

@[instance_reducible]

def DY.PersistentLocalState.State.ProofEntryT (StateT : Type) : Type

Equations

• DY.PersistentLocalState.State.ProofEntryT StateT = DY.ProofTraceTypes.combine (DY.PersistentLocalState.State.ProofEntryT.internal StateT)

instance DY.PersistentLocalState.storeLocalState.spec {StateT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [LocalStateInv StateT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ProofTraceTypes.Has (State.ProofEntryT StateT)] [TraceInvariant.Has (State.ProofEntryT StateT)] (participant : Participant) (state : StateT) : HoareTriple (storeLocalState participant state) (fun (tr : ProofTrace) => LocalStateInv.invariant participant state tr) fun (x : Nat) (x_1 : ProofTrace) => True

instance DY.PersistentLocalState.getLocalState.spec {StateT : Type} [ExecTraceTypes] [ProofTraceTypes] [TraceInvariant] [LocalStateInv StateT] [ExecTraceTypes.Has (State.ExecEntryT StateT)] [ProofTraceTypes.Has (State.ProofEntryT StateT)] [TraceInvariant.Has (State.ProofEntryT StateT)] (participant : Participant) (handle : Nat) : HoareTriple (getLocalState participant handle) (fun (x : ProofTrace) => True) fun (st : StateT) (tr : ProofTrace) => LocalStateInv.invariant participant st tr

@[instance_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

def DY.PersistentLocalState.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

• DY.PersistentLocalState.compromise StateT handle = DY.PersistentGlobalState.compromise (DY.PersistentLocalState.LocalState StateT) handle

def DY.PersistentLocalState.LocalStateCompromised {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (participant : Participant) (state : StateT) (tr : ExecTrace) : Prop

Equations

• DY.PersistentLocalState.LocalStateCompromised participant state tr = DY.PersistentGlobalState.GlobalStateCompromised { participant := participant, state := state } tr

theorem DY.PersistentLocalState.LocalStateCompromised_le {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (participant : Participant) (state : StateT) (tr1 tr2 : ExecTrace) : tr1 ≤ tr2 → LocalStateCompromised participant state tr1 → LocalStateCompromised participant state tr2

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

• DY.PersistentLocalState.label participant state = DY.PersistentGlobalState.label { participant := participant, state := state }

theorem DY.PersistentLocalState.label_isCorrupt {StateT : Type} [ExecTraceTypes] [ExecTraceTypes.Has (Compromise.ExecEntryT StateT)] (participant : Participant) (state : StateT) (tr : ExecTrace) : (label participant state).isCorrupt tr = LocalStateCompromised participant state tr

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

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

instance DY.PersistentLocalState.compromise.spec {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] [BytesInvariants.Has Literal.invariants] [BytesInvariants.Has Concat.invariants] [Comparse.ParseableSerializeable StateT] [CompromisableLocalStateInv 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.PersistentLocalState.CompromisableState.baseAttackerKnowledge.internal [BytesFunctor] [ExecTraceTypes] (StateT : Type) (id✝ : Fin 2) : SubBaseAttackerKnowledge (ExecEntryT.internal StateT id✝)

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

• DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge StateT = DY.SubBaseAttackerKnowledge.combine (DY.PersistentLocalState.CompromisableState.baseAttackerKnowledge.internal StateT)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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