From 90db4e646a5c63fd3905a544c813be3e35562098 Mon Sep 17 00:00:00 2001 From: wyn Date: Wed, 5 Aug 2026 10:45:54 +0100 Subject: [PATCH] Add Tallinn INDEX_ADDRESS/GET_ADDRESS_INDEX and preserve side effects Wire the Tallinn address-registry opcodes through LLTZ IR, Michelson AST, codegen, and oasis specs. Port SmartPy's may_have_side_effects handling so unused INDEX_ADDRESS is not dropped by the Michelson rewriter (it mutates the global address registry), and add regression expect tests. Do not treat MImich as having side effects MImich only tracks CONCAT1/CONCAT2 ambiguity and Michelson parse errors. It already has may_fail = true; marking it side-effecting is too conservative and changes optimizer baselines. Co-authored-by: Cursor --- lib/lltz_codegen/lltz_codegen.ml | 2 + lib/lltz_ir/ast_builder.ml | 16 ++ lib/lltz_ir/primitive.ml | 2 + lib/lltz_michelson/lltz_michelson.ml | 2 + lib/michelson/ast.ml | 8 + .../optimisations/if_suffix_rewriter.ml | 1 + .../optimisations/michelson_base/primitive.ml | 2 + .../michelson_base/primitive.mli | 2 + .../optimisations/michelson_base/typing.ml | 2 + .../optimisations/oasis_core/michelson.ml | 20 ++ .../oasis_core/michelson_rewriter.ml | 176 ++++++++++++++++-- test/test_nodes.ml | 37 ++++ 12 files changed, 252 insertions(+), 18 deletions(-) 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;