monad.proofs.reservebal2

Alternative execution-side reserve check model.

This file keeps only the reservebal2-specific execution predicate (finalBalSufficient) plus the minimal extra definitions it depends on. Everything else is imported from reservebal.

Section ReserveBal2.
Variable K : N.
Variable evmExecTxCore : StateOfAccounts → TxWithHdr → EvmExecResult.
Variable revertTx : StateOfAccounts → TxWithHdr → (StateOfAccounts × TxResult).
Context {eas: EVMAssupmtions evmExecTxCore revertTx}.

Address-parameterized variant of reservebal.indexWithinK.

Definition indexWithinKForAddr
    (proj: ExtraAcState → option N)
    (state : ExtraAcStates)
    (blkNum: N)
    (addr: EvmAddr) : bool :=
  let startIndex := blkNum - (K - 1) in
  match proj (state addr) with
  | Some index ⇒ asbool (startIndex ≤ index ≤ blkNum)
  | None ⇒ false
  end.

Definition existsTxWithinKForAddr
    (state : AugmentedState) (blkNum: N) (addr: EvmAddr) : bool :=
  indexWithinKForAddr lastTxInBlockIndex (snd state) blkNum addr.

Definition existsDelUndelTxWithinKForAddr
    (state : AugmentedState) (blkNum: N) (addr: EvmAddr) : bool :=
  indexWithinKForAddr lastDelUndelInBlockIndex (snd state) blkNum addr.

Address-parameterized “allowed to empty” predicate.

Definition isAllowedToEmptyG
  (preIntermediatesState : AugmentedState)
  (intermediates: list TxWithHdr)
  (candTx: TxWithHdr)
  (addr: EvmAddr) : bool :=
  let consideredDelegated :=
    (addrDelegated (fst preIntermediatesState) addr )
      || existsDelUndelTxWithinKForAddr preIntermediatesState (txBlockNum candTx) addr
      || asbool (elem_of addr (flat_map addrsDelUndelByTx (candTx :: intermediates))) in
  let existsSameSenderTxInWindow :=
    existsTxWithinKForAddr preIntermediatesState (txBlockNum candTx) addr
      || asbool (elem_of addr (map sender intermediates)) in
  (negb consideredDelegated ) && (negb existsSameSenderTxInWindow ).

reservebal2 variant: exemption uses isAllowedToEmptyG per-account.

Definition finalBalSufficientPiotr
    (preTxState: AugmentedState)
    (postTxState : StateOfAccounts)
    (t: TxWithHdr)
    (a: EvmAddr) : bool :=
  let ReserveBal := configuredReserveBalOfAddr (snd preTxState) a in
  let erb : N := N.min ReserveBal (balanceOfAc (fst preTxState) a) in
  if isSC postTxState a then true
  else if isAllowedToEmptyG preTxState [] t a then true
       else if asbool (sender t = a)
            then asbool (erb - maxTxFee t ≤ balanceOfAc postTxState a)
            else asbool (erb ≤ balanceOfAc postTxState a).

Lemma finalBalSufficient_if_balance_not_decreased:
  ∀ preTxState postTxState t a,
    balanceOfAc (fst preTxState) a ≤ balanceOfAc postTxState a →
    finalBalSufficientPiotr preTxState postTxState t a = true.

Conditional equivalence: if a's balance did not decrease, both execution checks accept a.

Lemma finalBalSufficient_equiv_if_balance_not_decreased:
  ∀ preTxState postTxState execAs t a,
    balanceOfAc (fst preTxState) a ≤ balanceOfAc postTxState a →
    finalBalSufficient K preTxState postTxState execAs t a =
    finalBalSufficientPiotr preTxState postTxState t a.

Lemma isAllowedToEmptyG_sender_equiv :
  ∀ pre t,
    isAllowedToEmptyG pre [] t (sender t) = isAllowedToEmpty K pre [] t.

Lemma isAllowedToEmptyG_if_no_history :
  ∀ pre t a,
    addrDelegated (fst pre) a = false →
    lastTxInBlockIndex (snd pre a) = None →
    lastDelUndelInBlockIndex (snd pre a) = None →
    asbool (a ∈ addrsDelUndelByTx t) = false →
    isAllowedToEmptyG pre [] t a = true.

Lemma finalBalSufficient_equiv_under_evmExecTxCore_if_no_history :
  ∀ (pre : AugmentedState) t a,
    reserveBalUpdateOfTx t = None →
    asbool (sender t ∈ codeExecSCAccountsOfResult (evmExecTxCore (fst pre) t)) = false →
    addrDelegated (fst pre) a = false →
    lastTxInBlockIndex (snd pre a) = None →
    lastDelUndelInBlockIndex (snd pre a) = None →
    asbool (a ∈ addrsDelUndelByTx t) = false →
    finalBalSufficient K pre (postState (evmExecTxCore (fst pre) t))
      (codeExecSCAccountsOfResult (evmExecTxCore (fst pre) t)) t a =
    finalBalSufficientPiotr pre (postState (evmExecTxCore (fst pre) t)) t a.

we prove finalBalSufficient and finalBalSufficientPiotr equivalent under no-recent-history assumptions only for the accounts for which reservebal.finalBalSufficient has an extra exemption:

those that ran code but were not delegated at the time
StakingContractAddr

The post-state isSC case needs no extra assumptions because both predicates immediately return true there.

Theorem finalBalSufficient_equiv:
  ∀ (pre : AugmentedState) (t:TxWithHdr) (a:EvmAddr),
    reserveBalUpdateOfTx t = None →
    asbool (sender t ∈ codeExecSCAccountsOfResult (evmExecTxCore (fst pre) t)) = false →
    ((asbool (a ∈ codeExecSCAccountsOfResult (evmExecTxCore (fst pre) t)) = true
      ∨ asbool (a = StakingContractAddr) = true ) →
        (addrDelegated (fst pre) a = false
        ∧ lastTxInBlockIndex (snd pre a) = None
        ∧ lastDelUndelInBlockIndex (snd pre a) = None
        ∧ asbool (a ∈ addrsDelUndelByTx t) = false )) →
    finalBalSufficient K pre (postState (evmExecTxCore (fst pre) t))
      (codeExecSCAccountsOfResult (evmExecTxCore (fst pre) t)) t a =
    finalBalSufficientPiotr pre (postState (evmExecTxCore (fst pre) t)) t a.
End ReserveBal2.

This page has been generated by coqdoc