Type inference rules for addresses #778
Conversation
…meter_type, and fix parser bug
|
I just made a small change. The check for duplicate fields in address types has now been moved to Recursion.ml. It fits better there, and it's sufficient to check each of the declared type, because there is no way to combine address types dynamically. |
|
I have reintroduced Addresses should be considered ground types, because they are represented as ByStr20. |
src/base/Datatypes.ml
Outdated
| @@ -232,7 +232,7 @@ module SnarkTypes = struct | |||
| let scilla_g1point_to_ocaml g1p = | |||
| match g1p with | |||
| | ADTValue ("Pair", [ pxt; pyt ], [ ByStrX px; ByStrX py ]) | |||
| when type_equiv pxt scalar_type && type_equiv pyt scalar_type | |||
| when type_assignable pxt scalar_type && type_assignable pyt scalar_type | |||
There was a problem hiding this comment.
I think we're better off sticking to the stricter type_equiv here (and below in this file). I can't imagine how we can have Addresses come in here, so until then, it's safer to have the stricter comparison.
There was a problem hiding this comment.
Are these functions (i.e., the associated builtins) not accessible for developers? I'm ok with with using type_equiv, but the question is whether someone would want to use an Address (viewed as a ByStr20) as a point in this calculation.
In essence it boils down to whether we should make an exception to the rule that we always al allow implicit coercion from Address to ByStr20. As I mentioned in the PR description I think we should remove that implicit coercion in the next major version, but we can't do that without introducing builtins for expliti type coercion, and that would not be backward compatible.
There was a problem hiding this comment.
the question is whether someone would want to use an Address (viewed as a ByStr20) as a point in this calculation.
No. The ByStrX here, even when it's ByStr20 will not / cannot refer to addresses. It is actually just a byte string for snark computations.
Regarding allowing implicit coercion from Address to ByStr20, I'm not convinced that it shouldn't be allowed. It looks to be fully compatible with the idea that you can move (assign) from a type with more information (say Address with x : Uint32, y : Uint32 end) to a type with less information (Address with x : Uint32 end). The basic ByStr20 just loses all extra information about the address. I can't see how it could be a reason for the programmer to introduce bugs.
There was a problem hiding this comment.
the question is whether someone would want to use an Address (viewed as a ByStr20) as a point in this calculation.
No. The
ByStrXhere, even when it'sByStr20will not / cannot refer to addresses. It is actually just a byte string for snark computations.
Got it. Then it should indeed be type_equiv.
Regarding allowing implicit coercion from
AddresstoByStr20, I'm not convinced that it shouldn't be allowed. It looks to be fully compatible with the idea that you can move (assign) from a type with more information (sayAddress with x : Uint32, y : Uint32end) to a type with less information (Address with x : Uint32 end). The basicByStr20just loses all extra information about the address. I can't see how it could be a reason for the programmer to introduce bugs.
Except that there is a difference between ByStr20 with end and ByStr20. The former is an address on the network which has (dynamically) been verified as containing a contract (though we don't know anything about its fields). The latter is just any byte string which may or may not refer to an address on the network, and if it does, then it may refer to any address, including user addresses or unused addresses.
The point I am trying to make is that with this change, addresses and byte strings are conceptually different, and should therefore be treated as such, and since we don't allow implicit type coercions anywhere else in Scilla, I don't think we should allow them here, either.
There was a problem hiding this comment.
The point I am trying to make is that with this change, addresses and byte strings are conceptually different, and should therefore be treated as such, and since we don't allow implicit type coercions anywhere else in Scilla, I don't think we should allow them here, either.
I agree 👍
The latter is just any byte string which may or may not refer to an address on the network, and if it does, then it may refer to any address, including user addresses or unused addresses.
Let us not differentiate contract and non-contract addresses. That's because we may want to fetch _balance of non-contract addresses.
Just as a follow-up: I do think we should change the syntax of Address types in version 1. Rather than using |
| | PolyFun _ | ||
| | Unit -> | ||
| let exn () = | ||
| mk_invalid_json ("Invalid type " ^ pp_typ t ^ " in JSON") |
There was a problem hiding this comment.
Should we now name this function json_to_lit_exn (conforming to the other functions above that have _exn to mark that they throw exceptions).
* 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>
This PR implements type inference rules for address types, and fixes a bug in the parsing of address types.
Addresses are legal if they do not contain duplicate fields, and all field types in the Address type are legal field types.
The general rule for assignability is that an address type T2 can be assigned to an address type T1 if every field declared in T1 with type T1T are also declared in T2 with types T2T such that T2T can be assigned to T1T.
Example:
fis assignable tog, because every field declared ingexists infwith a type that is assignable fromftog.gis not assignable tof, becausefcontains a fieldy, which does not exist ing.his not assignable to either of the other two fields, nor vice versa, since the type ofxinhis not assignable to the types ofxinforg, or vice versa.More elaborate example:
Since
ByStr20 with x1 : Int32, y1 : Int32 endis assignable toByStr20 with x1 : Int32 endbut not vice versa,fis assignable togbut not vice versa.All addresses are also assignable to ByStr20, though I think we ought to change that in the next version, since this in essence amounts to an implicit type coercion. Instead, we ought to have two new builtins:
bystr20_of_address : ByStr20 with end -> ByStr20: Takes any address, and returns the raw ByStr20 value.address_of_bystr20 : forall 'A => ByStr20 -> Option 'A: Takes an address type and a ByStr20, checks (using IPC) whether the ByStr20 corresponds to an address of a contract satisfying the address type, and returns eitherSome A, if the address type was satisfied, where A is a "verified" address, orNoneif the ByStr20 did not correspond to the provided type (this could happen if 'A is instantiated with a non-address type).is_serializable_storable_helperhas been rewritten, so that it can distinguish between cases where address types need to be checked for content (such as when they occur as transition parameters) or when they can just be considered a ByStr20 (such as when they are used to initialise a message field).This also eliminates the need for the functions is_ground_type and is_non_map_ground_type, so I have removed those functions.
I have refactored tests/typecheck/good/Testttypes.ml, and addedtest cases for assignability, which hopefully catches all the corner cases.
I have also had to make some changes to the parser error messages. It's still dark magic to me how to identify the states that relate to which error messages, but it seems to work.