A formal model of Algorand smart contracts

Coherence-checking experiments

• Account

  • Delete
  • Recover
  • Generate random (malformed) address
  • Client - Close
  • Client - Create
  • Client - Create wallet
  • Client - Info

• Interaction with a node

  • Check node status
  • Open a shell

• Smart contract

  • Stateless
    • Create a Contract account
    • Close a Contract account
    • Creating the same Contract account
    • Re-create a Contract account
    • Multisig
  • Stateful
    • Example stateful contract
    • Local state
    • Global state

• Transactions

  • Single transaction
  • Single transaction with no sign
  • Client - Send transaction
  • Pay from a sender to itself
  • Close to another address
  • Close to the sender
  • Asset generation
  • Asset opt-in
  • Asset burn (creator without all token units)
  • Asset burn (creator is manager)
  • Asset burn (creator is not manager)
  • Asset delegate
  • Send frozen asset
  • Freeze twice
  • Unfreezeing an asset
  • Receive frozen asset
  • Freeze non-existing asset
  • Freeze non-owned asset
  • Freezing in the freezer manager
  • Opt-in a frozen asset
  • Sending zero asset units

• Labels

  • Empty label

• Use cases

  • Stateless
    • Oracle
  • Stateful
    • Permissionless voting
    • Permissioned voting
    • Crowdfunding
    • Multi-player lottery