Skip to content

Latest commit

 

History

History
247 lines (177 loc) · 7.74 KB

token-transfer-steps.md

File metadata and controls

247 lines (177 loc) · 7.74 KB
Raw

Typing the specification and checking it

Version 1: Introducing data structures

  1. Open TokenTransfer1.tla and MC1.tla.

  2. Notice how CHAINS, ACCOUNTS, and banks are declared.

  3. Run:

    $ apalache-mc check MC1.tla

  4. The tool reports no errors.

Version 2: Let the banks do local banking

  1. Open TokenTransfer2.tla and MC2.tla.

  2. Inspect the operators LocalTransfer and Next. Do you see any issues?

  3. Inspect the expected invariants ReservesInv and NoNegativeAccounts. Do you see any issues?

  4. Check the property ReservesInv by running:

    $ apalache-mc check --inv=ReservesInv MC2.tla

  5. The tool reports on a counterexample. Check counterexample.tla. Can you fix the issue?

  6. Check the property NoNegativeAccounts by running:

    $ apalache-mc check --inv=NoNegativeAccounts MC2.tla

  7. The tool reports on a counterexample. Check counterexample.tla. Can you fix the issue?

Version 3: Fixing the invariants and introducing more properties

  1. Open TokenTransfer3.tla and MC3.tla.

  2. See how we have fixed NoNegativeAccounts by using Nat instead of Int.

  3. Notice how we introduced the constant GENESIS_SUPPLY and the operators SumAddresses and ChainSupply.

  4. Check what has changed in Init and Next.

  5. Inspect the new invariant ChainSupplyUnchanged.

  6. Observe how we have introduced GENESIS_SUPPLY in MC3.tla.

  7. Check the property ChainSupplyUnchanged by running:

    $ apalache-mc check --inv=ChainSupplyUnchanged MC3.tla

  8. Apalache is stuck after some time. Any ideas why?

  9. Check the detailed log by typing:

    $ tail -f detailed.log

  10. You can see the results of preprocessing steps in the directory that is called like x/hh.mm-DD.MM.YYYY-.*. The file out-analysis.tla is the final result of all preprocessing steps.

  11. You can tell Apalache to produce the log of SMT constraints:

    $ apalache-mc check --inv=ChainSupplyUnchanged --debug MC3.tla

  12. The log file can be found in log0.smt. If you are feeling adventurous today, you can install Microsoft Z3 and run the log directly with z3:

    $ z3 -smt2 log0.smt

Version 4: skipped

Version 5: Make Apalache fast again

  1. Open TokenTransfer5.tla and MC5.tla.

  2. Notice that we have added two new operators: TypeOK and IndInv.

  3. Run Apalache as follows:

    $ apalache-mc check --init=IndInv --inv=IndInv --length=1 MC5.tla
$ apalache-mc check --init=Init --inv=IndInv --length=0 MC5.tla
$ apalache-mc check --init=IndInv --inv=ChainSupplyUnchanged --length=0 MC5.tla

  4. Why do you think we have checked ChainSupplyUnchanged for the executions of arbitrary length?

Version 6: Send packets!

  1. Open TokenTransfer6.tla and MC6.tla.
  2. Notice the changes:
  • new constant CHANNELS
  • new variable sentPackets
  • new definition Escrow == "escrow"
  • update in Init and Next
  • new operators LocalStep and SendPacketFromSource

  1. Check the invariant InFlyPacketIsSecured by running:

    $ apalache-mc check --inv=InFlyPacketIsSecured MC6.tla

  2. Do you think it is a good invariant? Can we improve it?

  3. Can you write a version of InFlyPacketIsSecured that counts the sum of token over all in-fly packets?

Version 7: Receive packets

  1. Open TokenTransfer7.tla and MC7.tla.

  2. Notice the changes:

    • new field seqno in sentPackets
    • new variable seqno
    • new variable deliveredNums
    • new operators MintCoins and ReceivePacketFromSource
    • updates in Init and Next

  3. Do you think our spec is still OK?

  4. Check the property ChainSupplyUnchanged by running:

    $ apalache-mc check --inv=ChainSupplyUnchanged MC7.tla

  5. If it takes too long, let's cheat a bit and check how to tune the model checker. Read the page on tuning parameters.

  6. Create the file apalache.properties and write the follows:

    search.invariantFilter=[2-4]
search.invariant.mode=after

The first option instructs Apalache to check the invariant only after 2, 3, or 4 steps. The second option instructs Apalache to check the invariant after choosing a transition in a step, not before.

  1. Run Apalache with the tuning options:

    $ apalache-mc check --inv=ChainSupplyUnchanged --tuning=apalache.properties MC7.tla

  2. Apalache should find an error very quickly. Check counterexample1.tla. Do you understand what happened?

Version 8: Introducing denominations

  1. Open TokenTransfer8.tla and MC8.tla.

  2. Notice the changes:

    • new constants DENOMS and MK_DENOM
    • new operator Native
    • updates in many operators to attach denomination to an account

  3. Check the property NoForeignCoins by running:

    $ apalache-mc check --inv=NoForeignCoins MC8.tla

  4. Check counterexample.tla for an example.

  5. We can run Apalache again to check ChainSupplyUnchanged:

    $ apalache-mc check --inv=ChainSupplyUnchanged --tuning=apalache.properties MC7.tla

  6. This time, Apalache does not come back that fast. If you want to prove this property for all executions, construct an inductive invariant, similar to what we did with MC5.tla.

Version 9: Sending coins back

  1. Open TokenTransfer9.tla and MC9.tla.
  2. Notice the changes:
  • new constant UNMK_DENOM
  • new operators: SendPacket, BurnCoins, SendPacketToSource, ReceivePacketOnSource

  1. Check the property InFlyPacketIsSecured by running:

    $ apalache-mc check --inv=InFlyPacketIsSecured MC9.tla

  2. Check counterexample.tla for an example.

  3. Uncomment the precondition in the definition of InFlyPacketIsSecured and check the property again.

Version 10: Adding timeouts

  1. Open TokenTransfer10.tla and MC10.tla.
  2. Notice the changes:
  • new variables: srcTimeoutNums and dstTimeoutNums
  • new operators: RegisterTimeout and ApplyTimeout

  1. Check the property InFlyPacketIsSecured by running:

    $ apalache-mc check --inv=InFlyPacketIsSecured MC10.tla

  2. Check the property AllChainsSupplyUnchanged by running:

    $ apalache-mc check --inv=AllChainsSupplyUnchanged MC10.tla

Writing unit tests

  1. Open Test10.tla.

  2. Read the definitions of operators TestApplyTimeoutRequires, TestApplyTimeoutAction, and TestApplyTimeoutEnsures.

  3. Run the test as follows:

    $ apalache-mc check --init=TestApplyTimeoutRequires \
  --next=TestApplyTimeoutAction --inv=TestApplyTimeoutEnsures --length=1 Test10.tla

Version NNN: Fungible token transfer

If you are not tired, you can check ICS20 and improve TokenTransfer10.tla to support the full token transfer protocol.