diff --git a/lib/lltz_codegen/lltz_codegen.ml b/lib/lltz_codegen/lltz_codegen.ml index 8ed3649..35339e5 100644 --- a/lib/lltz_codegen/lltz_codegen.ml +++ b/lib/lltz_codegen/lltz_codegen.ml @@ -185,6 +185,8 @@ let convert_primitive (prim : LLTZ.P.t) : Michelson.Ast.t = | Address -> address | Implicit_account -> implicit_account | Is_implicit_account -> is_implicit_account + | Index_address -> index_address + | Get_address_index -> get_address_index | Contract (annot, ty) -> contract ~annot (convert_type ty) | Pack -> pack | Unpack ty -> unpack (convert_type ty) diff --git a/lib/lltz_ir/ast_builder.ml b/lib/lltz_ir/ast_builder.ml index 9aa129f..19ba859 100644 --- a/lib/lltz_ir/ast_builder.ml +++ b/lib/lltz_ir/ast_builder.ml @@ -585,6 +585,20 @@ module Default = struct (mk_type ~range (LLTZ.T.Option (mk_type ~range LLTZ.T.Key_hash))) ;; + let index_address ~range address = + create + ~range + (LLTZ.E.Prim (LLTZ.P.Index_address, [ address ])) + (mk_type ~range LLTZ.T.Nat) + ;; + + let get_address_index ~range address = + create + ~range + (LLTZ.E.Prim (LLTZ.P.Get_address_index, [ address ])) + (mk_type ~range (LLTZ.T.Option (mk_type ~range LLTZ.T.Nat))) + ;; + let contract ~range (opt, ty) address = create ~range @@ -1242,6 +1256,8 @@ module With_dummy = struct let address contract = Default.address ~range:v contract let implicit_account key_hash = Default.implicit_account ~range:v key_hash let is_implicit_account address = Default.is_implicit_account ~range:v address + let index_address address = Default.index_address ~range:v address + let get_address_index address = Default.get_address_index ~range:v address let contract (opt, ty) address = Default.contract ~range:v (opt, ty) address let pack value = Default.pack ~range:v value let unpack ty value = Default.unpack ~range:v ty value diff --git a/lib/lltz_ir/primitive.ml b/lib/lltz_ir/primitive.ml index 38e8bb2..b81f51f 100644 --- a/lib/lltz_ir/primitive.ml +++ b/lib/lltz_ir/primitive.ml @@ -42,6 +42,8 @@ type t = | Not | Size | Address + | Index_address + | Get_address_index | Implicit_account | Is_implicit_account | Contract of string option * Type.t diff --git a/lib/lltz_michelson/lltz_michelson.ml b/lib/lltz_michelson/lltz_michelson.ml index 146362f..61f1171 100644 --- a/lib/lltz_michelson/lltz_michelson.ml +++ b/lib/lltz_michelson/lltz_michelson.ml @@ -156,6 +156,8 @@ let convert_primitive (prim : LLTZ.P.t) : Michelson.Ast.t = | Address -> address | Implicit_account -> implicit_account | Is_implicit_account -> is_implicit_account + | Index_address -> index_address + | Get_address_index -> get_address_index | Contract (opt, ty) -> contract (convert_type ty) (* TODO: resolve tag option*) | Pack -> pack | Unpack ty -> unpack (convert_type ty) diff --git a/lib/michelson/ast.ml b/lib/michelson/ast.ml index 6440da4..e1fad06 100644 --- a/lib/michelson/ast.ml +++ b/lib/michelson/ast.ml @@ -56,6 +56,8 @@ module Prim = struct | Create_contract | Implicit_account | Is_implicit_account + | Index_address + | Get_address_index | Dip | Drop | Dup @@ -170,6 +172,8 @@ module Prim = struct | Create_contract -> "CREATE_CONTRACT" | Implicit_account -> "IMPLICIT_ACCOUNT" | Is_implicit_account -> "IS_IMPLICIT_ACCOUNT" + | Index_address -> "INDEX_ADDRESS" + | Get_address_index -> "GET_ADDRESS_INDEX" | Dip -> "DIP" | Drop -> "DROP" | Dup -> "DUP" @@ -284,6 +288,8 @@ module Prim = struct | "CREATE_CONTRACT" -> Create_contract | "IMPLICIT_ACCOUNT" -> Implicit_account | "IS_IMPLICIT_ACCOUNT" -> Is_implicit_account + | "INDEX_ADDRESS" -> Index_address + | "GET_ADDRESS_INDEX" -> Get_address_index | "DIP" -> Dip | "DROP" -> Drop | "DUP" -> Dup @@ -785,6 +791,8 @@ module Instruction = struct let if_none ~then_ ~else_ = prim ~arguments:[ seq then_; seq else_ ] (I If_none) let implicit_account = prim (I Implicit_account) let is_implicit_account = prim (I Is_implicit_account) + let index_address = prim (I Index_address) + let get_address_index = prim (I Get_address_index) let is_nat = prim (I Is_nat) let iter instrs = prim ~arguments:[ seq instrs ] (I Iter) let join_tickets = prim (I Join_tickets) diff --git a/lib/michelson/optimisations/if_suffix_rewriter.ml b/lib/michelson/optimisations/if_suffix_rewriter.ml index da215de..9874609 100644 --- a/lib/michelson/optimisations/if_suffix_rewriter.ml +++ b/lib/michelson/optimisations/if_suffix_rewriter.ml @@ -28,6 +28,7 @@ let is_injective : string -> bool = function | "CONS" | "IMPLICIT_ACCOUNT" | "IS_IMPLICIT_ACCOUNT" + | "GET_ADDRESS_INDEX" | "EMPTY_MAP" | "EMPTY_SET" | "HASH_KEY" diff --git a/lib/michelson/optimisations/michelson_base/primitive.ml b/lib/michelson/optimisations/michelson_base/primitive.ml index 7a5bfd7..151f983 100644 --- a/lib/michelson/optimisations/michelson_base/primitive.ml +++ b/lib/michelson/optimisations/michelson_base/primitive.ml @@ -44,6 +44,8 @@ type 'ty prim1 = | Concat1 | Size | Address + | Index_address + | Get_address_index | Implicit_account | Is_implicit_account | Contract of string option * 'ty diff --git a/lib/michelson/optimisations/michelson_base/primitive.mli b/lib/michelson/optimisations/michelson_base/primitive.mli index 6a37b7c..9ce2cd5 100644 --- a/lib/michelson/optimisations/michelson_base/primitive.mli +++ b/lib/michelson/optimisations/michelson_base/primitive.mli @@ -45,6 +45,8 @@ type 'ty prim1 = | Concat1 (** Concatenation of a list.*) | Size (** Size / Length.*) | Address (** Address of a contract.*) + | Index_address (** Index of an address in the global registry (Tallinn).*) + | Get_address_index (** Lookup address index in the global registry (Tallinn).*) | Implicit_account (** Implicit Account of a key_hash.*) | Is_implicit_account (** Is_implicit Account of an address.*) | Contract of string option * 'ty (** Contract of an address and entrypoint.*) diff --git a/lib/michelson/optimisations/michelson_base/typing.ml b/lib/michelson/optimisations/michelson_base/typing.ml index 7854514..03f212a 100644 --- a/lib/michelson/optimisations/michelson_base/typing.ml +++ b/lib/michelson/optimisations/michelson_base/typing.ml @@ -106,6 +106,8 @@ let type_prim1 = function | Concat1 | Size | Address + | Index_address + | Get_address_index | Implicit_account | Is_implicit_account | Pack diff --git a/lib/michelson/optimisations/oasis_core/michelson.ml b/lib/michelson/optimisations/oasis_core/michelson.ml index 314d066..968136a 100644 --- a/lib/michelson/optimisations/oasis_core/michelson.ml +++ b/lib/michelson/optimisations/oasis_core/michelson.ml @@ -1422,6 +1422,18 @@ let mi_is_implicit_account = | _ -> None) ;; +let mi_index_address = + mk_spec_basic "INDEX_ADDRESS" ~arities:(1, 1) (function + | { mt = MT0 Address; _ } :: _ -> Some [ mt_nat ] + | _ -> None) +;; + +let mi_get_address_index = + mk_spec_basic "GET_ADDRESS_INDEX" ~arities:(1, 1) (function + | { mt = MT0 Address; _ } :: _ -> Some [ mt_option mt_nat ] + | _ -> None) +;; + let mi_voting_power = mk_spec_basic "VOTING_POWER" ~arities:(1, 1) (function | { mt = MT0 Key_hash; _ } :: _ -> Some [ mt_nat ] @@ -1523,6 +1535,8 @@ let spec_of_prim1 p = | Address -> mi_address | Implicit_account -> mi_implicit_account | Is_implicit_account -> mi_is_implicit_account + | Index_address -> mi_index_address + | Get_address_index -> mi_get_address_index | Voting_power -> mi_voting_power | Size -> mi_size | Car | Cdr -> assert false @@ -1711,6 +1725,8 @@ let name_of_instr_exn = function | Address | Implicit_account | Is_implicit_account + | Index_address + | Get_address_index | Contract _ | Pack | Unpack _ @@ -2134,6 +2150,8 @@ module Of_micheline = struct | "SELF_ADDRESS", [] -> MI0 Self_address | "IMPLICIT_ACCOUNT", [] -> MI1 Implicit_account | "IS_IMPLICIT_ACCOUNT", [] -> MI1 Is_implicit_account + | "INDEX_ADDRESS", [] -> MI1 Index_address + | "GET_ADDRESS_INDEX", [] -> MI1 Get_address_index | "TRANSFER_TOKENS", [] -> MI3 Transfer_tokens | "CHECK_SIGNATURE", [] -> MI3 Check_signature | "SET_DELEGATE", [] -> MI1 Set_delegate @@ -2496,6 +2514,8 @@ module To_micheline = struct | Address | Implicit_account | Is_implicit_account + | Index_address + | Get_address_index | Pack | Hash_key | Blake2b diff --git a/lib/michelson/optimisations/oasis_core/michelson_rewriter.ml b/lib/michelson/optimisations/oasis_core/michelson_rewriter.ml index 8839998..f363bf0 100644 --- a/lib/michelson/optimisations/oasis_core/michelson_rewriter.ml +++ b/lib/michelson/optimisations/oasis_core/michelson_rewriter.ml @@ -165,6 +165,8 @@ let rec may_fail = function | Concat1 | Size | Address + | Index_address + | Get_address_index | Implicit_account | Is_implicit_account | Pack @@ -235,10 +237,132 @@ let may_diverge instr = cata_instr { f_instr; f_literal } { instr } ;; +(** Side effects not reflected in stack outputs. Currently only [Index_address], + which mutates the global address registry, and [Exec]. + + Recurses into sequences and control structures so that e.g. + [IF { INDEX_ADDRESS; ... } { ... }; DROP] is not treated as harmless. Does + not recurse into lambdas: an [INDEX_ADDRESS] inside a lambda only takes + effect if the lambda is executed (so [LAMBDA { INDEX_ADDRESS }; DROP] may + still be eliminated). DIG/DIP bubble rules below gate on this predicate. *) +let rec may_have_side_effects = function + | MI1 Index_address | MI2 Exec -> true + | Michelson.MIseq l -> List.exists ~f:(fun x -> may_have_side_effects x.instr) l + | MIif (i1, i2) | MIif_cons (i1, i2) | MIif_none (i1, i2) | MIif_left (i1, i2) -> + may_have_side_effects i1.instr || may_have_side_effects i2.instr + | MIdip i | MIdipn (_, i) | MIloop i | MIloop_left i | MIiter i | MImap i -> + may_have_side_effects i.instr + | MIcomment _ | MIdrop | MIdropn _ | MIdup _ | MIdig _ | MIdug _ + | MI0 + ( Sender + | Source + | Amount + | Balance + | Level + | Now + | Self _ + | Self_address + | Chain_id + | Total_voting_power + | Sapling_empty_state _ + | Unit_ + | None_ _ + | Nil _ + | Empty_set _ + | Empty_map _ + | Empty_bigmap _ + | Min_block_time ) + | MI1 + ( Car + | Cdr + | Some_ + | Eq + | Abs + | Neg + | Int + | Nat + | Bytes + | IsNat + | Neq + | Le + | Lt + | Ge + | Gt + | Not + | Concat1 + | Size + | Address + | Get_address_index + | Implicit_account + | Is_implicit_account + | Pack + | Hash_key + | Blake2b + | Sha256 + | Sha512 + | Keccak + | Sha3 + | Set_delegate + | Read_ticket + | Join_tickets + | Pairing_check + | Voting_power + | Left _ + | Right _ + | Contract _ + | Unpack _ + | Getn _ + | Cast _ + | Rename _ + | Emit _ ) + | MI1_fail _ + | MI2 + ( Pair _ + | Xor + | Ediv + | And + | Or + | Cons + | Compare + | Concat2 + | Get + | Mem + | Apply + | Sapling_verify_update + | Ticket + | Ticket_deprecated + | Split_ticket + | Updaten _ + | Sub_mutez + | Lsl + | Lsr + | Add + | Sub + | Mul + | View _ ) + | MI3 (Slice | Update | Get_and_update | Transfer_tokens | Check_signature | Open_chest) + | MIerror _ + | MImich _ + | MIswap + | MIpush _ + | MIunpair _ + | MIpairn _ + | MIfield _ + | MIsetField _ + | MIlambda _ + | MIlambda_rec _ + | MIcreate_contract _ + | MIconcat1 + | MIconcat2 + | MIconcat_unresolved + | MIConstant _ -> false +;; + (* - Checks if an instruction is harmless, meaning it neither fails nor diverges. + Checks if an instruction is harmless, meaning it neither fails, diverges, + nor has side effects outside the stack. *) -let harmless i = not (may_fail i || may_diverge i) +let harmless i = not (may_fail i || may_diverge i || may_have_side_effects i) let is_comparison = function | MI1 Eq | MI1 Neq | MI1 Ge | MI1 Gt | MI1 Le | MI1 Lt -> true @@ -733,7 +857,7 @@ let main (expr : instr_list) : (instr_list * instr_list) option = | p1 :: p2 :: MIdig 1 :: rest when is_pure_push p1 && is_pure_push p2 -> [ p2; p1 ] $ rest | i :: (push :: MI1_fail Failwith :: _ as rest) - when is_pure_push push && not (may_fail i) -> [] $ rest + when is_pure_push push && not (may_fail i || may_have_side_effects i) -> [] $ rest | i :: MIdrop :: rest when is_pushy i && harmless i -> [] $ rest | i :: MIdrop :: rest when has_arity (1, 1) i && harmless i -> [ MIdrop ] $ rest | i :: MIdrop :: rest when has_arity (2, 1) i && harmless i -> @@ -748,7 +872,8 @@ let main (expr : instr_list) : (instr_list * instr_list) option = | MIdip { instr = MIdrop } :: rest -> [ MIdig 1; MIdrop ] $ rest | MIdip { instr = Michelson.MIseq [] } :: rest -> [] $ rest | MIdip i1 :: MIdip i2 :: rest -> [ MIdip (iseq [ i1; i2 ]) ] $ rest - | MIdup 1 :: MIdip { instr } :: rest when has_arity (1, 1) instr -> + | MIdup 1 :: MIdip { instr } :: rest + when has_arity (1, 1) instr && not (may_have_side_effects instr) -> [ MIdup 1; instr; MIdig 1 ] $ rest (* Push literals: *) | MIpush (t, l) :: MI1 Some_ :: rest -> @@ -817,14 +942,20 @@ let main (expr : instr_list) : (instr_list * instr_list) option = | MIdig 1 :: MIdrop :: MIdrop :: rest -> [ MIdrop; MIdrop ] $ rest | MIdip i :: MIdrop :: rest -> [ MIdrop; i.instr ] $ rest (* Bubble up DIP: *) - | mono :: MIdip i :: rest when has_arity (1, 1) mono -> [ MIdip i; mono ] $ rest + | mono :: MIdip i :: rest + when has_arity (1, 1) mono && not (may_have_side_effects mono) -> + [ MIdip i; mono ] $ rest | p :: MIdip { instr } :: rest when is_pure_push p -> [ instr; p ] $ rest (* Bubble up SWAP: *) - | p :: MIdig 1 :: mono :: rest when has_arity (1, 1) mono && is_pure_push p -> - [ mono; p; MIdig 1 ] $ rest + | p :: MIdig 1 :: mono :: rest + when has_arity (1, 1) mono + && (not (may_have_side_effects mono)) + && is_pure_push p -> [ mono; p; MIdig 1 ] $ rest | m1 :: MIdig 1 :: m2 :: MIdig 1 :: rest - when has_arity (1, 1) m1 && has_arity (1, 1) m2 -> - [ MIdig 1; m2; MIdig 1; m1 ] $ rest + when has_arity (1, 1) m1 + && has_arity (1, 1) m2 + && (not (may_have_side_effects m1)) + && not (may_have_side_effects m2) -> [ MIdig 1; m2; MIdig 1; m1 ] $ rest (* DIG & DUG: *) | MIdig n1 :: (MIcomment _ as c) :: MIdug n2 :: rest when n1 = n2 -> [ c ] $ rest | MIdug n1 :: (MIcomment _ as c) :: MIdig n2 :: rest when n1 = n2 -> [ c ] $ rest @@ -843,10 +974,14 @@ let main (expr : instr_list) : (instr_list * instr_list) option = then [ MIdig (n - 1); MIdrop; MIdup k ] $ rest else [ MIdig (n - 1); MIdrop; MIdup (k - 1) ] $ rest | MIdup k :: MIdig n :: rest when n = k -> [ MIdig (n - 1); MIdup 1 ] $ rest - | MIdug n1 :: mono :: MIdig n2 :: rest when n1 = n2 && has_arity (1, 1) mono && n1 > 1 - -> [ MIdig 1; mono; MIdig 1 ] $ rest - | MIdig n :: MIdig 1 :: mono :: MIdig 1 :: rest when n >= 1 && has_arity (1, 1) mono - -> [ mono; MIdig n ] $ rest + | MIdug n1 :: mono :: MIdig n2 :: rest + when n1 = n2 + && has_arity (1, 1) mono + && (not (may_have_side_effects mono)) + && n1 > 1 -> [ MIdig 1; mono; MIdig 1 ] $ rest + | MIdig n :: MIdig 1 :: mono :: MIdig 1 :: rest + when n >= 1 && has_arity (1, 1) mono && not (may_have_side_effects mono) -> + [ mono; MIdig n ] $ rest | MIdug n1 :: MIdig n2 :: MIdrop :: rest when n1 <> n2 && n1 >= 1 && n2 >= 1 -> if n1 > n2 then [ MIdig (n2 + 1); MIdrop; MIdug (n1 - 1) ] $ rest @@ -926,7 +1061,8 @@ let main (expr : instr_list) : (instr_list * instr_list) option = | MIcomment comment :: MIdig 1 :: rest -> [ MIdig 1; MIcomment comment ] $ rest | MIcomment comment :: MIdig n :: MIdrop :: rest -> [ MIdig n; MIdrop; MIcomment comment ] $ rest - | mono :: MIdig n :: MIdrop :: rest when n >= 1 && has_arity (1, 1) mono -> + | mono :: MIdig n :: MIdrop :: rest + when n >= 1 && has_arity (1, 1) mono && not (may_have_side_effects mono) -> [ MIdig n; MIdrop; mono ] $ rest | (MIiter { instr = MI2 Cons } as mono) :: MIdig n :: MIdrop :: rest when n > 1 -> [ MIdig (n + 1); MIdrop; mono ] $ rest @@ -1018,16 +1154,20 @@ let main (expr : instr_list) : (instr_list * instr_list) option = | MIdig 1 :: MIdup 1 :: MIdug 2 :: rest -> [ MIdup 2 ] $ rest | MIdup 2 :: MIdig 1 :: MIdrop :: rest -> [ MIdrop; MIdup 1 ] $ rest | (MIdig n | MIdug n) :: _ as instrs -> dig_dug ~with_comments:false n instrs - | MIdup 1 :: MIdug 2 :: p :: MIdig 1 :: rest when has_arity (1, 1) p -> + | MIdup 1 :: MIdug 2 :: p :: MIdig 1 :: rest + when has_arity (1, 1) p && not (may_have_side_effects p) -> [ MIdup 1; p; MIdig 2 ] $ rest | MIdup 1 :: MIfield [ D ] :: MIdug 2 :: MIfield [ A ] :: rest -> [ MIunpair [ true; true ]; MIdig 2; MIdig 1 ] $ rest | MIdup 1 :: MIdup 2 :: rest -> [ MIdup 1; MIdup 1 ] $ rest | MIdup 1 :: MIdup 1 :: f :: push :: MIdig 3 :: rest - when has_arity (1, 1) f && is_pure_push push -> [ MIdup 1; f; push; MIdup 3 ] $ rest + when has_arity (1, 1) f + && (not (may_have_side_effects f)) + && is_pure_push push -> [ MIdup 1; f; push; MIdup 3 ] $ rest | MIdup 1 :: f :: push :: MIdup 3 :: MIdup 1 :: MIdug 4 :: rest - when has_arity (1, 1) f && is_pure_push push -> - [ MIdup 1; MIdup 1; f; push; MIdup 3 ] $ rest + when has_arity (1, 1) f + && (not (may_have_side_effects f)) + && is_pure_push push -> [ MIdup 1; MIdup 1; f; push; MIdup 3 ] $ rest | MI0 (Self None) :: MI1 Address :: rest -> [ MI0 Self_address ] $ rest | _ -> rewrite_none in diff --git a/test/test_nodes.ml b/test/test_nodes.ml index c48041c..25ff40f 100644 --- a/test/test_nodes.ml +++ b/test/test_nodes.ml @@ -2930,6 +2930,43 @@ let%expect_test "is_implicit_account address" = { PUSH address "tz1ABC123" ; IS_IMPLICIT_ACCOUNT } |}] ;; +let%expect_test "index_address address" = + let e = index_address (address_const "tz1ABC123") in + test_expr e; + [%expect + {| + { PUSH address "tz1ABC123" ; INDEX_ADDRESS } + + Optimised: + { PUSH address "tz1ABC123" ; INDEX_ADDRESS } |}] +;; + +let%expect_test "get_address_index address" = + let e = get_address_index (address_const "tz1ABC123") in + test_expr e; + [%expect + {| + { PUSH address "tz1ABC123" ; GET_ADDRESS_INDEX } + + Optimised: + { PUSH address "tz1ABC123" ; GET_ADDRESS_INDEX } |}] +;; + +let%expect_test "discarded index_address is preserved by optimiser" = + (* INDEX_ADDRESS mutates the global address registry; dropping an unused + result must not eliminate the instruction. *) + let e = + let_in (var "idx") ~rhs:(index_address (address_const "tz1ABC123")) ~in_:unit + in + test_expr e; + [%expect + {| + { PUSH address "tz1ABC123" ; INDEX_ADDRESS ; DROP ; UNIT } + + Optimised: + { PUSH address "tz1ABC123" ; INDEX_ADDRESS ; DROP ; UNIT } |}] +;; + let%expect_test "contract opt (bool_ty) address" = let e = contract (None, bool_ty) (address_const "KT1XYZ") in test_expr e;