Skip to content
This repository was archived by the owner on Aug 27, 2025. It is now read-only.

_sender and _this_address are addresses#801

Merged
jjcnn merged 5 commits into
remote_state_readsfrom
remote_state_reads_sender_this_as_address
Jan 19, 2021
Merged

_sender and _this_address are addresses#801
jjcnn merged 5 commits into
remote_state_readsfrom
remote_state_reads_sender_this_as_address

Conversation

@jjcnn

@jjcnn jjcnn commented Mar 6, 2020

Copy link
Copy Markdown
Contributor

_sender is clearly always a legal address, but there is no way for a transition to declare this, so _sender can only be treated as a ByStr20.

_this_address is also always a legal address, and although the user can force dynamic typechecking of _this_address into an address type:

field self : ByStr20 with end = _this_address

it seems more user-friendly to say that _this_address has type ByStr20 with end by default. (This workaround does not work for _sender, BTW).

I have changed this so that _sender and _this_address now have type ByStr20 with end. I don't think it should be possible to require _sender to have particular fields, and I don't see what the syntax should be anyway.

Making this change revealed a bug in the elaboration of eq. So far, eq required its two argument to have the same type, but since addresses should be compared using their ByStr20 value, I have changed the elaboration to be ByStr20 if an address is involved.

It also revealed an issue with EventInfo.ml, a fix of which was merged to master and onwards through remote_state_reads to this branch. That fix involved introducing a new type equality check, which now needs to be changed to an assignability check instead.

@jjcnn jjcnn marked this pull request as ready for review January 18, 2021 22:39
@jjcnn jjcnn closed this Jan 18, 2021
@jjcnn jjcnn reopened this Jan 18, 2021
@jjcnn jjcnn closed this Jan 18, 2021
@jjcnn

jjcnn commented Jan 18, 2021

Copy link
Copy Markdown
Contributor Author

_origin is also now marked as having an address type.

@jjcnn

jjcnn commented Jan 18, 2021

Copy link
Copy Markdown
Contributor Author

I accidentally marked the PR ready for review when in fact the bug in EventInfo.ml has not yet been fixed. It doesn't look like it is possible to revert to a draft PR again, so I'm temporarily closing it instead. I'll reopen it once it is ready for review.

@jjcnn jjcnn reopened this Jan 18, 2021
@jjcnn

jjcnn commented Jan 18, 2021

Copy link
Copy Markdown
Contributor Author

@vaivaswatha , @anton-trunov : Ready for review.

{
"vname": "_sender",
"type": "ByStr20",
"type": "ByStr20 with end",

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, what does ByStr20 with end mean?

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's the syntax of an address type. The general format is

Bystr20 with
  field_name : type,
  field_name : type,
  ...
end

A ByStr20 with no declared fields just means that the address in question is in use, either as a user account or a contract.

Comment thread src/base/ScillaParser.mly
| LPAREN; t = typ; RPAREN; { t }
| d = scid; { to_type d (toLoc $startpos(d))}
| t = TID; { TypeVar t }
| t = address_typ; { t }

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess I missed where the address_typ production was introduced.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's in the remote_state_reads branch, which this PR is to be merge into.

Comment thread src/base/ContractUtil.ml
(label_name_of_string MessagePayload.sender_label)
ER.address_rep,
bystrx_typ address_length )
Address [] )

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the meaning of Address []? I don't see that introduced in this PR.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Remember that this PR is to be merged into the remote_state_reads branch and not to master. Address is a constructor of the ScillaType.t datatype.

@anton-trunov

Copy link
Copy Markdown
Contributor

Oh, I missed the destination branch. Thanks for your comments.

@jjcnn jjcnn merged commit f4c1430 into remote_state_reads Jan 19, 2021
@jjcnn jjcnn deleted the remote_state_reads_sender_this_as_address branch January 19, 2021 20:32
jjcnn added a commit that referenced this pull request Mar 25, 2021
* Create new branch

* Define Address type (#763)

* Define Address type
* Define legal Address types for messages, parameters and fields.

* Syntax for address types (#767)

* Added address type to syntax, and fixed ambiguous grammar

* Add location info to Address field identifiers

* Type inference rules for addresses (#778)

* assert_type_assignable

* Use assert_type_assignable in TypeUtil.

* Type inference rules for address types

* Fix type_assignable and tests of same, introduce legal_procedure_parameter_type, and fix parser bug

* Fix parser bug and typechecker issue

* Refactor type equivalence tests

* Assignable tests

* Duplicate field check for address types

* Remove fixed TODO

* Move duplicate field check to Recursion.ml

* Remove blank line

* Reintroduce is_ground_type

* Cosmetic change to pp_typ in case the address contains no fields

* Addresses from JSONs should be read as ByStr20s

* Reorder arguments to for_all2_exn in builtin argument traversal

* Do not use type_assignable when comparing types derived from literal values

* Use type_equiv in Schnorr calculations, and rename json_to_lit to json_to_lit_exn

* Remote state read read syntax (#783)

* Remote state read syntax and typechecking

* _balance field must be accessible even when not declared

* Change <- to <-- for remote reads

* Add address type to map key and value types

* Removed incorrect comment

* Simple example contract for remote state reads, plus minor parser fix (#785)

* Field initialiser bugs fixed (#787)

* Fixed two bugs re. initialisers for address fields.

* Update src/base/TypeChecker.ml

Co-Authored-By: Vaivaswatha N <vaivaswatha@users.noreply.github.com>

Co-authored-by: Vaivaswatha N <vaivaswatha@users.noreply.github.com>

* Contract info should specify the defining lib for ADTs (#786)

* Provide an external_fetch function in StateService (#805)

* Add IPC methods to fetch external contract state

* Provide means to specify external states via input JSONs

* Add a dummy fetch_ext_state_value to StateIPCTestServer

* Provide external_fetch service in StateService.ml

* Fix compare function for identifiers and names. (#926)

* Fix outstanding merge issues (#925)

* Fix outstanding merge issues

* fmt

* Use assert_type_assignable rather than assert_type_equiv

* fmt

* `_sender` and `_this_address` are addresses (#801)

* _sender is an address, eq should compare addresses as ByStr20

* Added addresses as legal ADT constructor arguments

* Addresses in event fields output as ByStr20

* fmt

* Missing merge file

* Remote state reads practicalities (#927)

* Name parameters to type_assignable and assert_type_assignable

* address_typ to construct address type nodes

* fmt

* Allow parenthesised address types (#937)

* Fetch external value IPC query cannot provide expected type
as that isn't exactly known.

* Allow fetching type only for remote fields

* fmt

* Remote state reads bugfixes (#945)

* Use declared type rather than actual type in field env

* Allow _this_address to be declared in address types

* Disallow spids other than _this_address in address types

* Remote state reads testserver (#948)

* JSON parsing of external states

* Add testsuite support for external states

* Added remote state reads test contract

* Test contract

* implement remote map read

* Add comment clarifying computing accessed value type

* Fix issue with address types being lost

* fmt

Co-authored-by: Vaivaswatha Nagaraj <vaivaswatha@zilliqa.com>

* Merge

* Push immutable parameters via state service, along with fields

* Push contract parameters to state service during migration

* Revert "Push contract parameters to state service during migration"

This reverts commit 2ea064c.

* Revert "Push immutable parameters via state service, along with fields"

This reverts commit 2cf3978.

* Remote state reads dynamic typecheck (#953)

* Parameter typechecker for addresses

* Ignore types in init.json (not backward compatible), remove faulty assignability check for field initialisers

* Dynamic typecheck of contract parameters

* Missing commit of TypeUtil.mli

* Dynamic typecheck of contract parameters

* Minor tidying up

* Comments added

* Separate prepare_message from handle_message to allow for dynamic typechecks

* Dynamic typecheck of transition parameters, plus some (not all) tests

* Negative tests for addresses and ADTs

* Remote state reads misc bugfixes (#954)

* Address types are legal map value types

* Fix type_assignable

* Added comment about contravariance in custom ADTs

* Tests of _this_address in address types and remote reads

* Tests that messages, events and excetions use ByStr20 and not Address types

* Forgot to add the new tests to Testcontracts.ml

* Added assignability tests

* Decrease sender balance on acceptance (#955)

* make fmt

* Do not pretty-print Lists as JSON arrays. This confuses the (#956)

state parser in the blockchain unit test which cannot know if
its a map or not (yet).

I ended up running `make fmt` which resulted in some other changes
as well, but just whitespace changes.

Co-authored-by: Jacob Johannsen <jajocnn@gmail.com>

* Fix missing stuff in #956 (#957)

* Fix missing stuff in #956

* Change _this_address of test contract

* Update owner address and balance (to cover gas fee in C++ test)

* Remote state reads nonce check (#959)

* Added nonce check

* Tests for nonce > 0 || balance > 0

* New syntax for address types and remote state reads. (#960)

* Added nonce check

* Tests for nonce > 0 || balance > 0

* Changed remote read operator from <-- to <-&

* Change address type syntax

* Remove _this_address production from address_type_field

* Remove _this_address from Address AST nodes

* make fmt

* Change nonce_type to Uint64 (#961)

* Scilla-server wrapper for the disambiguation tool (#964)

* Disambiguator should output init JSON to file (#965)

* Ignore _balance output (#966)

* Remote state reads checker tests (#963)

* Equality tests on address types

* Non-storable types not allowed in address fields. Contract parameters checked for serializability. eq tests on addresses

* Address list traversal tests

* Namespaces not allowed when remote reading

* Polymorphic address types

* Test remote read from non-address

* Additional negative remote read tests

* Test of deep remote reads

* Various deep remote reads tests

* Fix problem map builtins on maps with addresses as key types

* Only address argument types to put should be converted to ByStr20

* fmt

* Merge fixes

* fmt

* Additional tests of assignability (#962)

* Fix contract parameter validation check (#969)

* Disable check. Another check needs to be enabled before merging

* Allow maps as contract parameters

* Validate contract parameters

* fmt

* Fixed elaboration of to_string, strrev and to_ascii for address types (#971)

* Handle migration of contracts with missing state (#972)

* Handle migration of contracts with missing state

* fmt

* Make contract init tests aware of scilla server tests

Co-authored-by: Vaivaswatha N <vaivaswatha@users.noreply.github.com>
Co-authored-by: Vaivaswatha Nagaraj <vaivaswatha@zilliqa.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants