Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Writing Token Contract with F* #314

Merged
merged 10 commits into from Feb 5, 2020
Merged

Conversation

@mariari
Copy link
Contributor

mariari commented Feb 1, 2020

Currently this contract is not complete, but it should have enough form to understand the approach

@mariari mariari requested review from cwgoes and thealmarty Feb 1, 2020
mariari added 2 commits Feb 2, 2020
corresponding Idris
Copy link
Collaborator

cwgoes left a comment

Nice start, see comments, can we also add:

  • An explicit "transaction" type with fields
  • A proof that if an account's balance is decremented, the account must have sent the transaction
experimental/examples/token/Token.fst Outdated Show resolved Hide resolved
experimental/examples/token/Token.fst Outdated Show resolved Hide resolved

let transfer_add acc add num =
match Map.select add acc with
| Some balance -> admit ()

This comment has been minimized.

Copy link
@cwgoes

cwgoes Feb 2, 2020

Collaborator

Looks like this needs a proof?

match Map.select add acc with
| Some balance ->
let remaining : nat = balance - num in
admit ()

This comment has been minimized.

Copy link
@cwgoes

cwgoes Feb 2, 2020

Collaborator

Looks like this needs a proof?

@cwgoes

This comment has been minimized.

Copy link
Collaborator

cwgoes commented Feb 2, 2020

Let's also add another two transaction types, mint and burn, which do change the total supply. mint can only be performed by a fixed owner (another field in the contract storage), while burn can be called by anyone to burn their own tokens.

Then we should prove that mint changes the total supply iff. the owner sends the tx, and that burn can only change the total supply by up to the balance of the sending account.

We don't have authorisation directly (that would be handled by the host chain), we should just put a "from" field in the transaction type which is assumed to have been previously authenticated (e.g. with a signature).

Example transaction type.

let execute_transaction token tx =
match tx.tx_data with
| Transfer _ ->
if valid_transfer token tx

This comment has been minimized.

Copy link
@cwgoes

cwgoes Feb 3, 2020

Collaborator

This reads storage once more than necessary (Map.select), can we abstract it away somehow to avoid it?

This comment has been minimized.

Copy link
@cwgoes

cwgoes Feb 3, 2020

Collaborator

or perhaps leave this out of F* for now but take notes on the general problem

This comment has been minimized.

Copy link
@mariari

mariari Feb 4, 2020

Author Contributor

We should probbaly leave it out, as it's not too exciting without say a reader monad (F* has them I think, just lacking effect polymorphism is a pain!)

A future PR will be had adding it to the documents.

Which folder should we use?

This comment has been minimized.

Copy link
@cwgoes

cwgoes Feb 4, 2020

Collaborator

I think this is relevant to a standard library or examples section of language design choices - #312.

mariari added 2 commits Feb 3, 2020
@cwgoes
cwgoes approved these changes Feb 4, 2020
Copy link
Collaborator

cwgoes left a comment

ACK, it would be nice if we could fill in the admit ()s later.

@mariari mariari merged commit 3317b53 into develop Feb 5, 2020
2 checks passed
2 checks passed
ci/circleci: setup_dependencies Your tests passed on CircleCI!
Details
ci/circleci: test_suite Your tests passed on CircleCI!
Details
@mariari mariari deleted the mariari/token-contract-example-fstar branch Feb 5, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

2 participants
You can’t perform that action at this time.