inductive UserEvent.Relation.DepositRel (p : MidgardParameters) (hub : OracleHub.State.OracleHub) (i : InputInfo) (deposits : Bridge.State.Deposits) : Bridge.State.DepositActions → Bridge.State.Deposits → Prop

• Authenticate {p : MidgardParameters} {hub : OracleHub.State.OracleHub} {i : InputInfo} {deposits : Bridge.State.Deposits} {l2_id : TxId} {deps' : UTxO.UTxOMap Bridge.State.DepositDatum} {tkns' : Tokens.State.Tokens Unit} {upper : PosixTime} : l2_id = i.txId → Tokens.State.Tokens.mint (Nat.repr l2_id) () deposits.depositTokens = tkns' → deposits.deposits.mint { event := { id := sorry, info := { l2_address := sorry, l2_datum := sorry } }, inclusion_time := upper + p.event_wait_duration, witness := sorry } = deps' → i.value ≤ p.max_transfer_token_count → i.validityInternal.upper = some upper → DepositRel p hub i deposits Bridge.State.DepositActions.AuthDeposit { deposits := deps', depositTokens := tkns' }

inductive UserEvent.Relation.WithdrawalRel (p : MidgardParameters) (hub : OracleHub.State.OracleHub) (i : InputInfo) (wts : Bridge.State.Withdrawals) : Bridge.State.WithdrawalActions → Bridge.State.Withdrawals → Prop

inductive UserEvent.Relation.TxOrderRel (p : MidgardParameters) (hub : OracleHub.State.OracleHub) (i : InputInfo) (txords : Bridge.State.TxOrders) : Bridge.State.TxOrderActions → Bridge.State.TxOrders → Prop

inductive UserEvent.Relation.Rel (p : MidgardParameters) (hub : OracleHub.State.OracleHub) (i : InputInfo) (s_in : Bridge.State.EventMap) : Bridge.State.Actions → Bridge.State.EventMap → Prop

Composed Machine

• DepositM {p : MidgardParameters} {hub : OracleHub.State.OracleHub} {i : InputInfo} {s_in : Bridge.State.EventMap} (dA : Bridge.State.DepositActions) (d : Bridge.State.Deposits) : DepositRel p hub i s_in.deposits dA d → Rel p hub i s_in (Bridge.State.Actions.Deposit dA) { deposits := d, withdrawals := s_in.withdrawals, txOrders := s_in.txOrders }
• WithdrawalM {p : MidgardParameters} {hub : OracleHub.State.OracleHub} {i : InputInfo} {s_in : Bridge.State.EventMap} (dA : Bridge.State.WithdrawalActions) (d : Bridge.State.Withdrawals) : WithdrawalRel p hub i s_in.withdrawals dA d → Rel p hub i s_in (Bridge.State.Actions.Withdrawal dA) { deposits := s_in.deposits, withdrawals := d, txOrders := s_in.txOrders }
• TxOrderM {p : MidgardParameters} {hub : OracleHub.State.OracleHub} {i : InputInfo} {s_in : Bridge.State.EventMap} (dA : Bridge.State.TxOrderActions) (d : Bridge.State.TxOrders) : TxOrderRel p hub i s_in.txOrders dA d → Rel p hub i s_in (Bridge.State.Actions.TxOrder dA) { deposits := s_in.deposits, withdrawals := s_in.withdrawals, txOrders := d }

def UserEvent.Notation.«term_=>UE__⟨_⟩_» : Lean.TrailingParserDescr

Equations

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