inductive Settlement.Relation.Rel (i : InputInfo) (sett : State.SettlementSt) (sch : Scheduler.State.SchedulerDatum) : State.Actions → State.SettlementSt → Prop

• Spawn {i : InputInfo} {sett : State.SettlementSt} {sch : Scheduler.State.SchedulerDatum} {merged_block : StateQueue.State.HashHeader} : Rel i sett sch (State.Actions.Spawn merged_block) (Tokens.State.Tokens.mint (Nat.repr merged_block.hash) { deposits_root := merged_block.header.deposits_root, withdrawals_root := merged_block.header.withdrawals_root, transactions_root := merged_block.header.transactions_root, resolution_claim := none } sett)
• Remove {i : InputInfo} {sett : State.SettlementSt} {sch : Scheduler.State.SchedulerDatum} (tid : Tokens.Elem.TId) (settlement_node : Tokens.Elem.TokenD State.Settlement) (resolution : State.ResolutionClaim) (lower_bound : PosixTime) (sett' : Tokens.State.Tokens State.Settlement) : Tokens.State.Tokens.get tid sett = some settlement_node → settlement_node.data.resolution_claim = some resolution → (resolution.operator == i.validator) = true → i.validityInternal.lower = some lower_bound → resolution.time ≤ lower_bound → Tokens.State.Tokens.burn tid sett = some sett' → Rel i sett sch (State.Actions.Remove tid) sett'
• AttachResolutionClaim {i : InputInfo} {sett : State.SettlementSt} {sch : Scheduler.State.SchedulerDatum} {settId : Tokens.Elem.TId} {sett_tkn : Tokens.Elem.TokenD State.Settlement} {resol_time : PosixTime} {ops : VKeyHash} {sett' : Tokens.State.Tokens State.Settlement} : Tokens.State.Tokens.get settId sett = some sett_tkn → sett_tkn.data.resolution_claim.isNone = true → i.validator = ops → sch.operator_id = ops → Tokens.State.Tokens.update_data settId (fun (t : State.Settlement) => { deposits_root := t.deposits_root, withdrawals_root := t.withdrawals_root, transactions_root := t.transactions_root, resolution_claim := some { time := resol_time, operator := ops } }) sett = some sett' → Rel i sett sch (State.Actions.AttachResolutionClaim settId resol_time ops) sett'
• DisproveClaim {i : InputInfo} {sett : State.SettlementSt} {sch : Scheduler.State.SchedulerDatum} {sett_id : Tokens.Elem.TId} {sett_tkn : Tokens.Elem.TokenD State.Settlement} {claim : State.ResolutionClaim} {sett' : Tokens.State.Tokens State.Settlement} {upper : PosixTime} : Tokens.State.Tokens.get sett_id sett = some sett_tkn → sett_tkn.data.resolution_claim = some claim → Tokens.State.Tokens.update_data sett_id (fun (t : State.Settlement) => { deposits_root := t.deposits_root, withdrawals_root := t.withdrawals_root, transactions_root := t.transactions_root, resolution_claim := none }) sett = some sett' → i.validityInternal.upper = some upper → upper < claim.time → Rel i sett sch (State.Actions.DisproveResolutionClaim sett_id) sett'

def Settlement.Notation.«term_=>SETT⟨_,_;_⟩_» : Lean.TrailingParserDescr

Equations

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