diff --git a/src/proto_alpha/lib_benchmark/test/test_distribution.ml b/src/proto_alpha/lib_benchmark/test/test_distribution.ml index 74ad9d815f44f18a13d618fa35925823295e9c57..4b5115aaf143f1f5276a47f43d2a961c4b7ebb45 100644 --- a/src/proto_alpha/lib_benchmark/test/test_distribution.ml +++ b/src/proto_alpha/lib_benchmark/test/test_distribution.ml @@ -105,30 +105,30 @@ and tnames_of_comparable_type : = fun t acc -> match t with - | Script_typed_ir.Unit_key -> `TUnit :: acc - | Script_typed_ir.Never_key -> assert false - | Script_typed_ir.Int_key -> `TInt :: acc - | Script_typed_ir.Nat_key -> `TNat :: acc - | Script_typed_ir.Signature_key -> `TSignature :: acc - | Script_typed_ir.String_key -> `TString :: acc - | Script_typed_ir.Bytes_key -> `TBytes :: acc - | Script_typed_ir.Mutez_key -> `TMutez :: acc - | Script_typed_ir.Bool_key -> `TBool :: acc - | Script_typed_ir.Key_hash_key -> `TKey_hash :: acc - | Script_typed_ir.Key_key -> `TKey :: acc - | Script_typed_ir.Timestamp_key -> `TTimestamp :: acc - | Script_typed_ir.Chain_id_key -> `TChain_id :: acc - | Script_typed_ir.Address_key -> `TAddress :: acc - | Script_typed_ir.Tx_rollup_l2_address_key -> `TTx_rollup_l2_address :: acc - | Script_typed_ir.Pair_key (lty, rty, _, YesYes) -> + | Script_typed_ir.Unit_t -> `TUnit :: acc + | Script_typed_ir.Never_t -> assert false + | Script_typed_ir.Int_t -> `TInt :: acc + | Script_typed_ir.Nat_t -> `TNat :: acc + | Script_typed_ir.Signature_t -> `TSignature :: acc + | Script_typed_ir.String_t -> `TString :: acc + | Script_typed_ir.Bytes_t -> `TBytes :: acc + | Script_typed_ir.Mutez_t -> `TMutez :: acc + | Script_typed_ir.Bool_t -> `TBool :: acc + | Script_typed_ir.Key_hash_t -> `TKey_hash :: acc + | Script_typed_ir.Key_t -> `TKey :: acc + | Script_typed_ir.Timestamp_t -> `TTimestamp :: acc + | Script_typed_ir.Chain_id_t -> `TChain_id :: acc + | Script_typed_ir.Address_t -> `TAddress :: acc + | Script_typed_ir.Tx_rollup_l2_address_t -> `TTx_rollup_l2_address :: acc + | Script_typed_ir.Pair_t (lty, rty, _, YesYes) -> tnames_of_comparable_type lty (tnames_of_comparable_type rty (`TPair :: acc)) - | Script_typed_ir.Union_key (lty, rty, _, YesYes) -> + | Script_typed_ir.Union_t (lty, rty, _, YesYes) -> tnames_of_comparable_type lty (tnames_of_comparable_type rty (`TUnion :: acc)) - | Script_typed_ir.Option_key (ty, _, Yes) -> + | Script_typed_ir.Option_t (ty, _, Yes) -> tnames_of_comparable_type ty (`TOption :: acc) module Crypto_samplers = Crypto_samplers.Make_finite_key_pool (struct diff --git a/src/proto_alpha/lib_plugin/plugin.ml b/src/proto_alpha/lib_plugin/plugin.ml index e879139a456b682d4d68d57d2c575cf1f8b0586b..ee70bf19b39c63547f9c0025aa1b9fcd7bd5d10d 100644 --- a/src/proto_alpha/lib_plugin/plugin.ml +++ b/src/proto_alpha/lib_plugin/plugin.ml @@ -1986,30 +1986,30 @@ module RPC = struct type a loc. loc:loc -> a comparable_ty -> (loc, Script.prim) Micheline.node = fun ~loc -> function - | Unit_key -> Prim (loc, T_unit, [], []) - | Never_key -> Prim (loc, T_never, [], []) - | Int_key -> Prim (loc, T_int, [], []) - | Nat_key -> Prim (loc, T_nat, [], []) - | Signature_key -> Prim (loc, T_signature, [], []) - | String_key -> Prim (loc, T_string, [], []) - | Bytes_key -> Prim (loc, T_bytes, [], []) - | Mutez_key -> Prim (loc, T_mutez, [], []) - | Bool_key -> Prim (loc, T_bool, [], []) - | Key_hash_key -> Prim (loc, T_key_hash, [], []) - | Key_key -> Prim (loc, T_key, [], []) - | Timestamp_key -> Prim (loc, T_timestamp, [], []) - | Address_key -> Prim (loc, T_address, [], []) - | Tx_rollup_l2_address_key -> Prim (loc, T_tx_rollup_l2_address, [], []) - | Chain_id_key -> Prim (loc, T_chain_id, [], []) - | Pair_key (l, r, _meta, YesYes) -> + | Unit_t -> Prim (loc, T_unit, [], []) + | Never_t -> Prim (loc, T_never, [], []) + | Int_t -> Prim (loc, T_int, [], []) + | Nat_t -> Prim (loc, T_nat, [], []) + | Signature_t -> Prim (loc, T_signature, [], []) + | String_t -> Prim (loc, T_string, [], []) + | Bytes_t -> Prim (loc, T_bytes, [], []) + | Mutez_t -> Prim (loc, T_mutez, [], []) + | Bool_t -> Prim (loc, T_bool, [], []) + | Key_hash_t -> Prim (loc, T_key_hash, [], []) + | Key_t -> Prim (loc, T_key, [], []) + | Timestamp_t -> Prim (loc, T_timestamp, [], []) + | Address_t -> Prim (loc, T_address, [], []) + | Tx_rollup_l2_address_t -> Prim (loc, T_tx_rollup_l2_address, [], []) + | Chain_id_t -> Prim (loc, T_chain_id, [], []) + | Pair_t (l, r, _meta, YesYes) -> let tl = unparse_comparable_ty ~loc l in let tr = unparse_comparable_ty ~loc r in Prim (loc, T_pair, [tl; tr], []) - | Union_key (l, r, _meta, YesYes) -> + | Union_t (l, r, _meta, YesYes) -> let tl = unparse_comparable_ty ~loc l in let tr = unparse_comparable_ty ~loc r in Prim (loc, T_or, [tl; tr], []) - | Option_key (t, _meta, Yes) -> + | Option_t (t, _meta, Yes) -> Prim (loc, T_option, [unparse_comparable_ty ~loc t], []) let unparse_memo_size ~loc memo_size = diff --git a/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml b/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml index 040574b5c01bdf3535c6a010876ae68e29a00612..6e90810eba69245b1d1a8a0d80ea9223cdf70815 100644 --- a/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml +++ b/src/proto_alpha/lib_protocol/gas_comparable_input_size.ml @@ -110,33 +110,33 @@ let rec size_of_comparable_value : type a. a Script_typed_ir.comparable_ty -> a -> t = fun (type a) (wit : a Script_typed_ir.comparable_ty) (v : a) -> match wit with - | Never_key -> ( match v with _ -> .) - | Unit_key -> unit - | Int_key -> integer v - | Nat_key -> integer v - | String_key -> script_string v - | Bytes_key -> bytes v - | Mutez_key -> mutez v - | Bool_key -> bool v - | Key_hash_key -> key_hash v - | Timestamp_key -> timestamp v - | Address_key -> address v - | Tx_rollup_l2_address_key -> tx_rollup_l2_address v - | Pair_key (leaf, node, _, YesYes) -> + | Never_t -> ( match v with _ -> .) + | Unit_t -> unit + | Int_t -> integer v + | Nat_t -> integer v + | String_t -> script_string v + | Bytes_t -> bytes v + | Mutez_t -> mutez v + | Bool_t -> bool v + | Key_hash_t -> key_hash v + | Timestamp_t -> timestamp v + | Address_t -> address v + | Tx_rollup_l2_address_t -> tx_rollup_l2_address v + | Pair_t (leaf, node, _, YesYes) -> let (lv, rv) = v in let size = size_of_comparable_value leaf lv + size_of_comparable_value node rv in size + 1 - | Union_key (left, right, _, YesYes) -> + | Union_t (left, right, _, YesYes) -> let size = match v with | L v -> size_of_comparable_value left v | R v -> size_of_comparable_value right v in size + 1 - | Option_key (ty, _, Yes) -> ( + | Option_t (ty, _, Yes) -> ( match v with None -> 1 | Some x -> size_of_comparable_value ty x + 1) - | Signature_key -> signature v - | Key_key -> public_key v - | Chain_id_key -> chain_id v + | Signature_t -> signature v + | Key_t -> public_key v + | Chain_id_t -> chain_id v diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 39eb3d58ee201231b8cbc59b0ba95f15f09d7119..d0700459e313e65f96c56539f1f15ed0da3c7779 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -1402,24 +1402,24 @@ module Cost_of = struct a Script_typed_ir.comparable_ty -> a -> a -> cost -> cont -> cost = fun ty x y acc k -> match ty with - | Unit_key -> (apply [@tailcall]) Gas.(acc +@ compare_unit) k - | Never_key -> ( match x with _ -> .) - | Bool_key -> (apply [@tailcall]) Gas.(acc +@ compare_bool) k - | String_key -> (apply [@tailcall]) Gas.(acc +@ compare_string x y) k - | Signature_key -> (apply [@tailcall]) Gas.(acc +@ compare_signature) k - | Bytes_key -> (apply [@tailcall]) Gas.(acc +@ compare_bytes x y) k - | Mutez_key -> (apply [@tailcall]) Gas.(acc +@ compare_mutez) k - | Int_key -> (apply [@tailcall]) Gas.(acc +@ compare_int x y) k - | Nat_key -> (apply [@tailcall]) Gas.(acc +@ compare_nat x y) k - | Key_hash_key -> (apply [@tailcall]) Gas.(acc +@ compare_key_hash) k - | Key_key -> (apply [@tailcall]) Gas.(acc +@ compare_key) k - | Timestamp_key -> + | Unit_t -> (apply [@tailcall]) Gas.(acc +@ compare_unit) k + | Never_t -> ( match x with _ -> .) + | Bool_t -> (apply [@tailcall]) Gas.(acc +@ compare_bool) k + | String_t -> (apply [@tailcall]) Gas.(acc +@ compare_string x y) k + | Signature_t -> (apply [@tailcall]) Gas.(acc +@ compare_signature) k + | Bytes_t -> (apply [@tailcall]) Gas.(acc +@ compare_bytes x y) k + | Mutez_t -> (apply [@tailcall]) Gas.(acc +@ compare_mutez) k + | Int_t -> (apply [@tailcall]) Gas.(acc +@ compare_int x y) k + | Nat_t -> (apply [@tailcall]) Gas.(acc +@ compare_nat x y) k + | Key_hash_t -> (apply [@tailcall]) Gas.(acc +@ compare_key_hash) k + | Key_t -> (apply [@tailcall]) Gas.(acc +@ compare_key) k + | Timestamp_t -> (apply [@tailcall]) Gas.(acc +@ compare_timestamp x y) k - | Address_key -> (apply [@tailcall]) Gas.(acc +@ compare_address) k - | Tx_rollup_l2_address_key -> + | Address_t -> (apply [@tailcall]) Gas.(acc +@ compare_address) k + | Tx_rollup_l2_address_t -> (apply [@tailcall]) Gas.(acc +@ compare_tx_rollup_l2_address) k - | Chain_id_key -> (apply [@tailcall]) Gas.(acc +@ compare_chain_id) k - | Pair_key (tl, tr, _, YesYes) -> + | Chain_id_t -> (apply [@tailcall]) Gas.(acc +@ compare_chain_id) k + | Pair_t (tl, tr, _, YesYes) -> (* Reasonable over-approximation of the cost of lexicographic comparison. *) let (xl, xr) = x in let (yl, yr) = y in @@ -1429,7 +1429,7 @@ module Cost_of = struct yl Gas.(acc +@ compare_pair_tag) (Compare (tr, xr, yr, k)) - | Union_key (tl, tr, _, YesYes) -> ( + | Union_t (tl, tr, _, YesYes) -> ( match (x, y) with | (L x, L y) -> (compare [@tailcall]) tl x y Gas.(acc +@ compare_union_tag) k @@ -1437,7 +1437,7 @@ module Cost_of = struct | (R _, L _) -> (apply [@tailcall]) Gas.(acc +@ compare_union_tag) k | (R x, R y) -> (compare [@tailcall]) tr x y Gas.(acc +@ compare_union_tag) k) - | Option_key (t, _, Yes) -> ( + | Option_t (t, _, Yes) -> ( match (x, y) with | (None, None) -> (apply [@tailcall]) Gas.(acc +@ compare_option_tag) k diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml index cf152247ac95334d0205591372e072ebf1a9196c..394285268528aadc04b8275f59be06ab9dc0bcc4 100644 --- a/src/proto_alpha/lib_protocol/script_comparable.ml +++ b/src/proto_alpha/lib_protocol/script_comparable.ml @@ -47,43 +47,41 @@ let compare_comparable : type a. a comparable_ty -> a -> a -> int = type a. a comparable_ty -> compare_comparable_cont -> a -> a -> int = fun kind k x y -> match (kind, x, y) with - | (Unit_key, (), ()) -> (apply [@tailcall]) 0 k - | (Never_key, _, _) -> . - | (Signature_key, x, y) -> + | (Unit_t, (), ()) -> (apply [@tailcall]) 0 k + | (Never_t, _, _) -> . + | (Signature_t, x, y) -> (apply [@tailcall]) (Script_signature.compare x y) k - | (String_key, x, y) -> (apply [@tailcall]) (Script_string.compare x y) k - | (Bool_key, x, y) -> (apply [@tailcall]) (Compare.Bool.compare x y) k - | (Mutez_key, x, y) -> (apply [@tailcall]) (Tez.compare x y) k - | (Key_hash_key, x, y) -> + | (String_t, x, y) -> (apply [@tailcall]) (Script_string.compare x y) k + | (Bool_t, x, y) -> (apply [@tailcall]) (Compare.Bool.compare x y) k + | (Mutez_t, x, y) -> (apply [@tailcall]) (Tez.compare x y) k + | (Key_hash_t, x, y) -> (apply [@tailcall]) (Signature.Public_key_hash.compare x y) k - | (Key_key, x, y) -> - (apply [@tailcall]) (Signature.Public_key.compare x y) k - | (Int_key, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k - | (Nat_key, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k - | (Timestamp_key, x, y) -> + | (Key_t, x, y) -> (apply [@tailcall]) (Signature.Public_key.compare x y) k + | (Int_t, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k + | (Nat_t, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k + | (Timestamp_t, x, y) -> (apply [@tailcall]) (Script_timestamp.compare x y) k - | (Address_key, x, y) -> (apply [@tailcall]) (compare_address x y) k - | (Tx_rollup_l2_address_key, x, y) -> + | (Address_t, x, y) -> (apply [@tailcall]) (compare_address x y) k + | (Tx_rollup_l2_address_t, x, y) -> (apply [@tailcall]) (compare_tx_rollup_l2_address x y) k - | (Bytes_key, x, y) -> (apply [@tailcall]) (Compare.Bytes.compare x y) k - | (Chain_id_key, x, y) -> - (apply [@tailcall]) (Script_chain_id.compare x y) k - | (Pair_key (tl, tr, _, YesYes), (lx, rx), (ly, ry)) -> + | (Bytes_t, x, y) -> (apply [@tailcall]) (Compare.Bytes.compare x y) k + | (Chain_id_t, x, y) -> (apply [@tailcall]) (Script_chain_id.compare x y) k + | (Pair_t (tl, tr, _, YesYes), (lx, rx), (ly, ry)) -> (compare_comparable [@tailcall]) tl (Compare_comparable (tr, rx, ry, k)) lx ly - | (Union_key (tl, _, _, YesYes), L x, L y) -> + | (Union_t (tl, _, _, YesYes), L x, L y) -> (compare_comparable [@tailcall]) tl k x y - | (Union_key _, L _, R _) -> -1 - | (Union_key _, R _, L _) -> 1 - | (Union_key (_, tr, _, YesYes), R x, R y) -> + | (Union_t _, L _, R _) -> -1 + | (Union_t _, R _, L _) -> 1 + | (Union_t (_, tr, _, YesYes), R x, R y) -> (compare_comparable [@tailcall]) tr k x y - | (Option_key _, None, None) -> (apply [@tailcall]) 0 k - | (Option_key _, None, Some _) -> -1 - | (Option_key _, Some _, None) -> 1 - | (Option_key (t, _, Yes), Some x, Some y) -> + | (Option_t _, None, None) -> (apply [@tailcall]) 0 k + | (Option_t _, None, Some _) -> -1 + | (Option_t _, Some _, None) -> 1 + | (Option_t (t, _, Yes), Some x, Some y) -> (compare_comparable [@tailcall]) t k x y and apply ret k = match (ret, k) with diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index dcef099c0b7f2a914614e386debcee1977e73b41..84689e7eb084a6f8d20befdd47b6f441568afcd9 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -163,46 +163,46 @@ let check_kind kinds expr = let rec ty_of_comparable_ty : type a. a comparable_ty -> (a, Dependent_bool.yes) ty = function - | Unit_key -> Unit_t - | Never_key -> Never_t - | Int_key -> Int_t - | Nat_key -> Nat_t - | Signature_key -> Signature_t - | String_key -> String_t - | Bytes_key -> Bytes_t - | Mutez_key -> Mutez_t - | Bool_key -> Bool_t - | Key_hash_key -> Key_hash_t - | Key_key -> Key_t - | Timestamp_key -> Timestamp_t - | Address_key -> Address_t - | Tx_rollup_l2_address_key -> Tx_rollup_l2_address_t - | Chain_id_key -> Chain_id_t - | Pair_key (l, r, meta, YesYes) -> + | Unit_t -> Unit_t + | Never_t -> Never_t + | Int_t -> Int_t + | Nat_t -> Nat_t + | Signature_t -> Signature_t + | String_t -> String_t + | Bytes_t -> Bytes_t + | Mutez_t -> Mutez_t + | Bool_t -> Bool_t + | Key_hash_t -> Key_hash_t + | Key_t -> Key_t + | Timestamp_t -> Timestamp_t + | Address_t -> Address_t + | Tx_rollup_l2_address_t -> Tx_rollup_l2_address_t + | Chain_id_t -> Chain_id_t + | Pair_t (l, r, meta, YesYes) -> Pair_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, YesYes) - | Union_key (l, r, meta, YesYes) -> + | Union_t (l, r, meta, YesYes) -> Union_t (ty_of_comparable_ty l, ty_of_comparable_ty r, meta, YesYes) - | Option_key (t, meta, Yes) -> Option_t (ty_of_comparable_ty t, meta, Yes) + | Option_t (t, meta, Yes) -> Option_t (ty_of_comparable_ty t, meta, Yes) let rec unparse_comparable_ty_uncarbonated : type a loc. loc:loc -> a comparable_ty -> loc Script.michelson_node = fun ~loc -> function - | Unit_key -> Prim (loc, T_unit, [], []) - | Never_key -> Prim (loc, T_never, [], []) - | Int_key -> Prim (loc, T_int, [], []) - | Nat_key -> Prim (loc, T_nat, [], []) - | Signature_key -> Prim (loc, T_signature, [], []) - | String_key -> Prim (loc, T_string, [], []) - | Bytes_key -> Prim (loc, T_bytes, [], []) - | Mutez_key -> Prim (loc, T_mutez, [], []) - | Bool_key -> Prim (loc, T_bool, [], []) - | Key_hash_key -> Prim (loc, T_key_hash, [], []) - | Key_key -> Prim (loc, T_key, [], []) - | Timestamp_key -> Prim (loc, T_timestamp, [], []) - | Address_key -> Prim (loc, T_address, [], []) - | Tx_rollup_l2_address_key -> Prim (loc, T_tx_rollup_l2_address, [], []) - | Chain_id_key -> Prim (loc, T_chain_id, [], []) - | Pair_key (l, r, _meta, YesYes) -> ( + | Unit_t -> Prim (loc, T_unit, [], []) + | Never_t -> Prim (loc, T_never, [], []) + | Int_t -> Prim (loc, T_int, [], []) + | Nat_t -> Prim (loc, T_nat, [], []) + | Signature_t -> Prim (loc, T_signature, [], []) + | String_t -> Prim (loc, T_string, [], []) + | Bytes_t -> Prim (loc, T_bytes, [], []) + | Mutez_t -> Prim (loc, T_mutez, [], []) + | Bool_t -> Prim (loc, T_bool, [], []) + | Key_hash_t -> Prim (loc, T_key_hash, [], []) + | Key_t -> Prim (loc, T_key, [], []) + | Timestamp_t -> Prim (loc, T_timestamp, [], []) + | Address_t -> Prim (loc, T_address, [], []) + | Tx_rollup_l2_address_t -> Prim (loc, T_tx_rollup_l2_address, [], []) + | Chain_id_t -> Prim (loc, T_chain_id, [], []) + | Pair_t (l, r, _meta, YesYes) -> ( let tl = unparse_comparable_ty_uncarbonated ~loc l in let tr = unparse_comparable_ty_uncarbonated ~loc r in (* Fold [pair a1 (pair ... (pair an-1 an))] into [pair a1 ... an] *) @@ -211,11 +211,11 @@ let rec unparse_comparable_ty_uncarbonated : match tr with | Prim (_, T_pair, ts, []) -> Prim (loc, T_pair, tl :: ts, []) | _ -> Prim (loc, T_pair, [tl; tr], [])) - | Union_key (l, r, _meta, YesYes) -> + | Union_t (l, r, _meta, YesYes) -> let tl = unparse_comparable_ty_uncarbonated ~loc l in let tr = unparse_comparable_ty_uncarbonated ~loc r in Prim (loc, T_or, [tl; tr], []) - | Option_key (t, _meta, Yes) -> + | Option_t (t, _meta, Yes) -> Prim (loc, T_option, [unparse_comparable_ty_uncarbonated ~loc t], []) let unparse_memo_size ~loc memo_size = @@ -342,32 +342,32 @@ let[@coq_axiom_with_reason "gadt"] rec comparable_ty_of_ty : fun ctxt loc ty -> Gas.consume ctxt Typecheck_costs.comparable_ty_of_ty_cycle >>? fun ctxt -> match ty with - | Unit_t -> ok ((Unit_key : a comparable_ty), ctxt) - | Never_t -> ok (Never_key, ctxt) - | Int_t -> ok (Int_key, ctxt) - | Nat_t -> ok (Nat_key, ctxt) - | Signature_t -> ok (Signature_key, ctxt) - | String_t -> ok (String_key, ctxt) - | Bytes_t -> ok (Bytes_key, ctxt) - | Mutez_t -> ok (Mutez_key, ctxt) - | Bool_t -> ok (Bool_key, ctxt) - | Key_hash_t -> ok (Key_hash_key, ctxt) - | Key_t -> ok (Key_key, ctxt) - | Timestamp_t -> ok (Timestamp_key, ctxt) - | Address_t -> ok (Address_key, ctxt) - | Tx_rollup_l2_address_t -> ok (Tx_rollup_l2_address_key, ctxt) - | Chain_id_t -> ok (Chain_id_key, ctxt) + | Unit_t -> ok ((Unit_t : a comparable_ty), ctxt) + | Never_t -> ok (Never_t, ctxt) + | Int_t -> ok (Int_t, ctxt) + | Nat_t -> ok (Nat_t, ctxt) + | Signature_t -> ok (Signature_t, ctxt) + | String_t -> ok (String_t, ctxt) + | Bytes_t -> ok (Bytes_t, ctxt) + | Mutez_t -> ok (Mutez_t, ctxt) + | Bool_t -> ok (Bool_t, ctxt) + | Key_hash_t -> ok (Key_hash_t, ctxt) + | Key_t -> ok (Key_t, ctxt) + | Timestamp_t -> ok (Timestamp_t, ctxt) + | Address_t -> ok (Address_t, ctxt) + | Tx_rollup_l2_address_t -> ok (Tx_rollup_l2_address_t, ctxt) + | Chain_id_t -> ok (Chain_id_t, ctxt) | Pair_t (l, r, pname, _) -> comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) -> comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) -> - (Pair_key (lty, rty, pname, YesYes), ctxt) + (Pair_t (lty, rty, pname, YesYes), ctxt) | Union_t (l, r, meta, _) -> comparable_ty_of_ty ctxt loc l >>? fun (lty, ctxt) -> comparable_ty_of_ty ctxt loc r >|? fun (rty, ctxt) -> - (Union_key (lty, rty, meta, YesYes), ctxt) + (Union_t (lty, rty, meta, YesYes), ctxt) | Option_t (tt, meta, _) -> comparable_ty_of_ty ctxt loc tt >|? fun (ty, ctxt) -> - (Option_key (ty, meta, Yes), ctxt) + (Option_t (ty, meta, Yes), ctxt) | Lambda_t _ | List_t _ | Ticket_t _ | Set_t _ | Map_t _ | Big_map_t _ | Contract_t _ | Operation_t | Bls12_381_fr_t | Bls12_381_g1_t | Bls12_381_g2_t | Sapling_state_t _ | Sapling_transaction_t _ @@ -589,8 +589,8 @@ let unparse_option ~loc unparse_v ctxt = function let comparable_comb_witness2 : type t. t comparable_ty -> (t, unit -> unit -> unit) comb_witness = function - | Pair_key (_, Pair_key _, _, YesYes) -> Comb_Pair (Comb_Pair Comb_Any) - | Pair_key _ -> Comb_Pair Comb_Any + | Pair_t (_, Pair_t _, _, YesYes) -> Comb_Pair (Comb_Pair Comb_Any) + | Pair_t _ -> Comb_Pair Comb_Any | _ -> Comb_Any let[@coq_axiom_with_reason "gadt"] rec unparse_comparable_data : @@ -612,36 +612,35 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_comparable_data : >>?= fun ctxt -> match (ty, a) with - | (Unit_key, v) -> Lwt.return @@ unparse_unit ~loc ctxt v - | (Int_key, v) -> Lwt.return @@ unparse_int ~loc ctxt v - | (Nat_key, v) -> Lwt.return @@ unparse_nat ~loc ctxt v - | (String_key, s) -> Lwt.return @@ unparse_string ~loc ctxt s - | (Bytes_key, s) -> Lwt.return @@ unparse_bytes ~loc ctxt s - | (Bool_key, b) -> Lwt.return @@ unparse_bool ~loc ctxt b - | (Timestamp_key, t) -> Lwt.return @@ unparse_timestamp ~loc ctxt mode t - | (Address_key, address) -> - Lwt.return @@ unparse_address ~loc ctxt mode address - | (Tx_rollup_l2_address_key, address) -> + | (Unit_t, v) -> Lwt.return @@ unparse_unit ~loc ctxt v + | (Int_t, v) -> Lwt.return @@ unparse_int ~loc ctxt v + | (Nat_t, v) -> Lwt.return @@ unparse_nat ~loc ctxt v + | (String_t, s) -> Lwt.return @@ unparse_string ~loc ctxt s + | (Bytes_t, s) -> Lwt.return @@ unparse_bytes ~loc ctxt s + | (Bool_t, b) -> Lwt.return @@ unparse_bool ~loc ctxt b + | (Timestamp_t, t) -> Lwt.return @@ unparse_timestamp ~loc ctxt mode t + | (Address_t, address) -> Lwt.return @@ unparse_address ~loc ctxt mode address + | (Tx_rollup_l2_address_t, address) -> Lwt.return @@ unparse_tx_rollup_l2_address ~loc ctxt mode address - | (Signature_key, s) -> Lwt.return @@ unparse_signature ~loc ctxt mode s - | (Mutez_key, v) -> Lwt.return @@ unparse_mutez ~loc ctxt v - | (Key_key, k) -> Lwt.return @@ unparse_key ~loc ctxt mode k - | (Key_hash_key, k) -> Lwt.return @@ unparse_key_hash ~loc ctxt mode k - | (Chain_id_key, chain_id) -> + | (Signature_t, s) -> Lwt.return @@ unparse_signature ~loc ctxt mode s + | (Mutez_t, v) -> Lwt.return @@ unparse_mutez ~loc ctxt v + | (Key_t, k) -> Lwt.return @@ unparse_key ~loc ctxt mode k + | (Key_hash_t, k) -> Lwt.return @@ unparse_key_hash ~loc ctxt mode k + | (Chain_id_t, chain_id) -> Lwt.return @@ unparse_chain_id ~loc ctxt mode chain_id - | (Pair_key (tl, tr, _, YesYes), pair) -> + | (Pair_t (tl, tr, _, YesYes), pair) -> let r_witness = comparable_comb_witness2 tr in let unparse_l ctxt v = unparse_comparable_data ~loc ctxt mode tl v in let unparse_r ctxt v = unparse_comparable_data ~loc ctxt mode tr v in unparse_pair ~loc unparse_l unparse_r ctxt mode r_witness pair - | (Union_key (tl, tr, _, YesYes), v) -> + | (Union_t (tl, tr, _, YesYes), v) -> let unparse_l ctxt v = unparse_comparable_data ~loc ctxt mode tl v in let unparse_r ctxt v = unparse_comparable_data ~loc ctxt mode tr v in unparse_union ~loc unparse_l unparse_r ctxt v - | (Option_key (t, _, Yes), v) -> + | (Option_t (t, _, Yes), v) -> let unparse_v ctxt v = unparse_comparable_data ~loc ctxt mode t v in unparse_option ~loc unparse_v ctxt v - | (Never_key, _) -> . + | (Never_t, _) -> . let pack_node unparsed ctxt = Gas.consume ctxt (Script.strip_locations_cost unparsed) >>? fun ctxt -> @@ -673,10 +672,9 @@ let hash_comparable_data ctxt ty data = checking this property when adding new types. *) let check_dupable_comparable_ty : type a. a comparable_ty -> unit = function - | Unit_key | Never_key | Int_key | Nat_key | Signature_key | String_key - | Bytes_key | Mutez_key | Bool_key | Key_hash_key | Key_key | Timestamp_key - | Chain_id_key | Address_key | Tx_rollup_l2_address_key | Pair_key _ - | Union_key _ | Option_key _ -> + | Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t + | Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t + | Tx_rollup_l2_address_t | Pair_t _ | Union_t _ | Option_t _ -> () let check_dupable_ty ctxt loc ty = @@ -791,56 +789,55 @@ let rec comparable_ty_eq : (ty_of_comparable_ty tb)) in match (ta, tb) with - | (Unit_key, Unit_key) -> - return (Eq : (ta comparable_ty, tb comparable_ty) eq) - | (Unit_key, _) -> not_equal () - | (Never_key, Never_key) -> return Eq - | (Never_key, _) -> not_equal () - | (Int_key, Int_key) -> return Eq - | (Int_key, _) -> not_equal () - | (Nat_key, Nat_key) -> return Eq - | (Nat_key, _) -> not_equal () - | (Signature_key, Signature_key) -> return Eq - | (Signature_key, _) -> not_equal () - | (String_key, String_key) -> return Eq - | (String_key, _) -> not_equal () - | (Bytes_key, Bytes_key) -> return Eq - | (Bytes_key, _) -> not_equal () - | (Mutez_key, Mutez_key) -> return Eq - | (Mutez_key, _) -> not_equal () - | (Bool_key, Bool_key) -> return Eq - | (Bool_key, _) -> not_equal () - | (Key_hash_key, Key_hash_key) -> return Eq - | (Key_hash_key, _) -> not_equal () - | (Key_key, Key_key) -> return Eq - | (Key_key, _) -> not_equal () - | (Timestamp_key, Timestamp_key) -> return Eq - | (Timestamp_key, _) -> not_equal () - | (Chain_id_key, Chain_id_key) -> return Eq - | (Chain_id_key, _) -> not_equal () - | (Address_key, Address_key) -> return Eq - | (Address_key, _) -> not_equal () - | (Tx_rollup_l2_address_key, Tx_rollup_l2_address_key) -> return Eq - | (Tx_rollup_l2_address_key, _) -> not_equal () - | ( Pair_key (left_a, right_a, meta_a, YesYes), - Pair_key (left_b, right_b, meta_b, YesYes) ) -> + | (Unit_t, Unit_t) -> return (Eq : (ta comparable_ty, tb comparable_ty) eq) + | (Unit_t, _) -> not_equal () + | (Never_t, Never_t) -> return Eq + | (Never_t, _) -> not_equal () + | (Int_t, Int_t) -> return Eq + | (Int_t, _) -> not_equal () + | (Nat_t, Nat_t) -> return Eq + | (Nat_t, _) -> not_equal () + | (Signature_t, Signature_t) -> return Eq + | (Signature_t, _) -> not_equal () + | (String_t, String_t) -> return Eq + | (String_t, _) -> not_equal () + | (Bytes_t, Bytes_t) -> return Eq + | (Bytes_t, _) -> not_equal () + | (Mutez_t, Mutez_t) -> return Eq + | (Mutez_t, _) -> not_equal () + | (Bool_t, Bool_t) -> return Eq + | (Bool_t, _) -> not_equal () + | (Key_hash_t, Key_hash_t) -> return Eq + | (Key_hash_t, _) -> not_equal () + | (Key_t, Key_t) -> return Eq + | (Key_t, _) -> not_equal () + | (Timestamp_t, Timestamp_t) -> return Eq + | (Timestamp_t, _) -> not_equal () + | (Chain_id_t, Chain_id_t) -> return Eq + | (Chain_id_t, _) -> not_equal () + | (Address_t, Address_t) -> return Eq + | (Address_t, _) -> not_equal () + | (Tx_rollup_l2_address_t, Tx_rollup_l2_address_t) -> return Eq + | (Tx_rollup_l2_address_t, _) -> not_equal () + | ( Pair_t (left_a, right_a, meta_a, YesYes), + Pair_t (left_b, right_b, meta_b, YesYes) ) -> let* () = type_metadata_eq meta_a meta_b in let* Eq = comparable_ty_eq ~error_details left_a left_b in let+ Eq = comparable_ty_eq ~error_details right_a right_b in (Eq : (ta comparable_ty, tb comparable_ty) eq) - | (Pair_key _, _) -> not_equal () - | ( Union_key (left_a, right_a, meta_a, YesYes), - Union_key (left_b, right_b, meta_b, YesYes) ) -> + | (Pair_t _, _) -> not_equal () + | ( Union_t (left_a, right_a, meta_a, YesYes), + Union_t (left_b, right_b, meta_b, YesYes) ) -> let* () = type_metadata_eq meta_a meta_b in let* Eq = comparable_ty_eq ~error_details left_a left_b in let+ Eq = comparable_ty_eq ~error_details right_a right_b in (Eq : (ta comparable_ty, tb comparable_ty) eq) - | (Union_key _, _) -> not_equal () - | (Option_key (ta, meta_a, Yes), Option_key (tb, meta_b, Yes)) -> + | (Union_t _, _) -> not_equal () + | (Option_t (ta, meta_a, Yes), Option_t (tb, meta_b, Yes)) -> let* () = type_metadata_eq meta_a meta_b in let+ Eq = comparable_ty_eq ~error_details ta tb in (Eq : (ta comparable_ty, tb comparable_ty) eq) - | (Option_key _, _) -> not_equal () + | (Option_t _, _) -> not_equal () let memo_size_eq : type error_trace. @@ -2386,7 +2383,7 @@ let parse_option parse_v ctxt ~legacy = function let comparable_comb_witness1 : type t. t comparable_ty -> (t, unit -> unit) comb_witness = function - | Pair_key _ -> Comb_Pair Comb_Any + | Pair_t _ -> Comb_Pair Comb_Any | _ -> Comb_Any let[@coq_axiom_with_reason "gadt"] rec parse_comparable_data : @@ -2413,42 +2410,41 @@ let[@coq_axiom_with_reason "gadt"] rec parse_comparable_data : fun ctxt -> let legacy = false in match (ty, script_data) with - | (Unit_key, expr) -> + | (Unit_t, expr) -> Lwt.return @@ traced_no_lwt @@ (parse_unit ctxt ~legacy expr : (a * context) tzresult) - | (Bool_key, expr) -> + | (Bool_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_bool ctxt ~legacy expr - | (String_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_string ctxt expr - | (Bytes_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_bytes ctxt expr - | (Int_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_int ctxt expr - | (Nat_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_nat ctxt expr - | (Mutez_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_mutez ctxt expr - | (Timestamp_key, expr) -> + | (String_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_string ctxt expr + | (Bytes_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_bytes ctxt expr + | (Int_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_int ctxt expr + | (Nat_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_nat ctxt expr + | (Mutez_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_mutez ctxt expr + | (Timestamp_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_timestamp ctxt expr - | (Key_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_key ctxt expr - | (Key_hash_key, expr) -> + | (Key_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_key ctxt expr + | (Key_hash_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_key_hash ctxt expr - | (Signature_key, expr) -> + | (Signature_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_signature ctxt expr - | (Chain_id_key, expr) -> + | (Chain_id_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_chain_id ctxt expr - | (Address_key, expr) -> - Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr - | (Tx_rollup_l2_address_key, expr) -> + | (Address_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr + | (Tx_rollup_l2_address_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_tx_rollup_l2_address ctxt expr - | (Pair_key (tl, tr, _, YesYes), expr) -> + | (Pair_t (tl, tr, _, YesYes), expr) -> let r_witness = comparable_comb_witness1 tr in let parse_l ctxt v = parse_comparable_data ?type_logger ctxt tl v in let parse_r ctxt v = parse_comparable_data ?type_logger ctxt tr v in traced @@ parse_pair parse_l parse_r ctxt ~legacy r_witness expr - | (Union_key (tl, tr, _, YesYes), expr) -> + | (Union_t (tl, tr, _, YesYes), expr) -> let parse_l ctxt v = parse_comparable_data ?type_logger ctxt tl v in let parse_r ctxt v = parse_comparable_data ?type_logger ctxt tr v in traced @@ parse_union parse_l parse_r ctxt ~legacy expr - | (Option_key (t, _, Yes), expr) -> + | (Option_t (t, _, Yes), expr) -> let parse_v ctxt v = parse_comparable_data ?type_logger ctxt t v in traced @@ parse_option parse_v ctxt ~legacy expr - | (Never_key, expr) -> Lwt.return @@ traced_no_lwt @@ parse_never expr + | (Never_t, expr) -> Lwt.return @@ traced_no_lwt @@ parse_never expr (* -- parse data of any type -- *) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index ce2142c54a6ff553c733b4435de988cba5783d34..7d344c3dd308e23cf47cd854c8e16a6fc979e92c 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -312,38 +312,6 @@ type end_of_stack = empty_cell * empty_cell type 'a ty_metadata = {size : 'a Type_size.t} [@@unboxed] -type _ comparable_ty = - | Unit_key : unit comparable_ty - | Never_key : never comparable_ty - | Int_key : z num comparable_ty - | Nat_key : n num comparable_ty - | Signature_key : signature comparable_ty - | String_key : Script_string.t comparable_ty - | Bytes_key : Bytes.t comparable_ty - | Mutez_key : Tez.t comparable_ty - | Bool_key : bool comparable_ty - | Key_hash_key : public_key_hash comparable_ty - | Key_key : public_key comparable_ty - | Timestamp_key : Script_timestamp.t comparable_ty - | Chain_id_key : Script_chain_id.t comparable_ty - | Address_key : address comparable_ty - | Tx_rollup_l2_address_key : tx_rollup_l2_address comparable_ty - | Pair_key : - 'a comparable_ty - * 'b comparable_ty - * ('a, 'b) pair ty_metadata - * (yes, yes, yes) dand - -> ('a, 'b) pair comparable_ty - | Union_key : - 'a comparable_ty - * 'b comparable_ty - * ('a, 'b) union ty_metadata - * (yes, yes, yes) dand - -> ('a, 'b) union comparable_ty - | Option_key : - 'v comparable_ty * 'v option ty_metadata * yes dbool - -> 'v option comparable_ty - (* This signature contains the exact set of functions used in the @@ -1307,6 +1275,8 @@ and ('ty, 'comparable) ty = | Chest_key_t : (Script_timelock.chest_key, no) ty | Chest_t : (Script_timelock.chest, no) ty +and 'ty comparable_ty = ('ty, yes) ty + and ('top_ty, 'resty) stack_ty = | Item_t : ('ty, _) ty * ('ty2, 'rest) stack_ty @@ -1823,16 +1793,15 @@ let ty_metadata : type a ac. (a, ac) ty -> a ty_metadata = function meta_basic let comparable_ty_metadata : type a. a comparable_ty -> a ty_metadata = function - | Unit_key | Never_key | Int_key | Nat_key | Signature_key | String_key - | Bytes_key | Mutez_key | Bool_key | Key_hash_key | Key_key | Timestamp_key - | Chain_id_key | Address_key | Tx_rollup_l2_address_key -> + | Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t + | Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t + | Tx_rollup_l2_address_t -> meta_basic - | Pair_key (_, _, meta, YesYes) -> meta - | Union_key (_, _, meta, YesYes) -> meta - | Option_key (_, meta, Yes) -> meta + | Pair_t (_, _, meta, YesYes) -> meta + | Union_t (_, _, meta, YesYes) -> meta + | Option_t (_, meta, Yes) -> meta -let ty_size : type v vc. (v, vc) ty -> v Type_size.t = - fun t -> (ty_metadata t).size +let ty_size t = (ty_metadata t).size let comparable_ty_size t = (comparable_ty_metadata t).size @@ -1876,55 +1845,55 @@ type 'v ty_ex_c = Ty_ex_c : ('v, _) ty -> 'v ty_ex_c [@@ocaml.unboxed] let unit_t = Unit_t -let unit_key = Unit_key +let unit_key = unit_t let int_t = Int_t -let int_key = Int_key +let int_key = int_t let nat_t = Nat_t -let nat_key = Nat_key +let nat_key = nat_t let signature_t = Signature_t -let signature_key = Signature_key +let signature_key = signature_t let string_t = String_t -let string_key = String_key +let string_key = string_t let bytes_t = Bytes_t -let bytes_key = Bytes_key +let bytes_key = bytes_t let mutez_t = Mutez_t -let mutez_key = Mutez_key +let mutez_key = mutez_t let key_hash_t = Key_hash_t -let key_hash_key = Key_hash_key +let key_hash_key = key_hash_t let key_t = Key_t -let key_key = Key_key +let key_key = key_t let timestamp_t = Timestamp_t -let timestamp_key = Timestamp_key +let timestamp_key = timestamp_t let address_t = Address_t -let address_key = Address_key +let address_key = address_t let bool_t = Bool_t -let bool_key = Bool_key +let bool_key = bool_t let tx_rollup_l2_address_t = Tx_rollup_l2_address_t -let tx_rollup_l2_address_key = Tx_rollup_l2_address_key +let tx_rollup_l2_address_key = tx_rollup_l2_address_t let pair_t : type a ac b bc. @@ -1940,8 +1909,8 @@ let comparable_pair_t loc l r = Pair_t (l, r, {size}, YesYes) let pair_key loc l r = - Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r) - >|? fun size -> Pair_key (l, r, {size}, YesYes) + Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> + Pair_t (l, r, {size}, YesYes) let pair_3_key loc l m r = pair_key loc m r >>? fun r -> pair_key loc l r @@ -1962,8 +1931,8 @@ let union_bytes_bool_t = Union_t (bytes_t, bool_t, {size = Type_size.three}, YesYes) let union_key loc l r = - Type_size.compound2 loc (comparable_ty_size l) (comparable_ty_size r) - >|? fun size -> Union_key (l, r, {size}, YesYes) + Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> + Union_t (l, r, {size}, YesYes) let lambda_t loc l r = Type_size.compound2 loc (ty_size l) (ty_size r) >|? fun size -> @@ -2007,8 +1976,7 @@ let option_pair_int_nat_t = Yes ) let option_key loc t = - Type_size.compound1 loc (comparable_ty_size t) >|? fun size -> - Option_key (t, {size}, Yes) + Type_size.compound1 loc (ty_size t) >|? fun size -> Option_t (t, {size}, Yes) let list_t loc t = Type_size.compound1 loc (ty_size t) >|? fun size -> List_t (t, {size}) @@ -2043,11 +2011,11 @@ let sapling_state_t ~memo_size = Sapling_state_t memo_size let chain_id_t = Chain_id_t -let chain_id_key = Chain_id_key +let chain_id_key = chain_id_t let never_t = Never_t -let never_key = Never_key +let never_key = never_t let bls12_381_g1_t = Bls12_381_g1_t @@ -2274,13 +2242,13 @@ let (ty_traverse, comparable_ty_traverse) = in let return () = (continue [@ocaml.tailcall]) accu in match ty with - | Unit_key | Int_key | Nat_key | Signature_key | String_key | Bytes_key - | Mutez_key | Key_hash_key | Key_key | Timestamp_key | Address_key - | Tx_rollup_l2_address_key | Bool_key | Chain_id_key | Never_key -> + | Unit_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t | Mutez_t + | Key_hash_t | Key_t | Timestamp_t | Address_t | Tx_rollup_l2_address_t + | Bool_t | Chain_id_t | Never_t -> (return [@ocaml.tailcall]) () - | Pair_key (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2 - | Union_key (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2 - | Option_key (ty, _, Yes) -> (next [@ocaml.tailcall]) ty + | Pair_t (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2 + | Union_t (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2 + | Option_t (ty, _, Yes) -> (next [@ocaml.tailcall]) ty and aux' : type ret t tc accu. accu ty_traverse -> accu -> (t, tc) ty -> (accu -> ret) -> ret = @@ -2444,17 +2412,17 @@ let value_traverse (type t tc) (ty : ((t, tc) ty, t comparable_ty) union) in let return () = (continue [@ocaml.tailcall]) accu in match ty with - | Unit_key | Int_key | Nat_key | Signature_key | String_key | Bytes_key - | Mutez_key | Key_hash_key | Key_key | Timestamp_key | Address_key - | Tx_rollup_l2_address_key | Bool_key | Chain_id_key | Never_key -> + | Unit_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t | Mutez_t + | Key_hash_t | Key_t | Timestamp_t | Address_t | Tx_rollup_l2_address_t + | Bool_t | Chain_id_t | Never_t -> (return [@ocaml.tailcall]) () - | Pair_key (ty1, ty2, _, YesYes) -> + | Pair_t (ty1, ty2, _, YesYes) -> (next2 [@ocaml.tailcall]) ty1 ty2 (fst x) (snd x) - | Union_key (ty1, ty2, _, YesYes) -> ( + | Union_t (ty1, ty2, _, YesYes) -> ( match x with | L l -> (next [@ocaml.tailcall]) ty1 l | R r -> (next [@ocaml.tailcall]) ty2 r) - | Option_key (ty, _, Yes) -> ( + | Option_t (ty, _, Yes) -> ( match x with | None -> (return [@ocaml.tailcall]) () | Some v -> (next [@ocaml.tailcall]) ty v) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 2caa8f18942dd8e79f1b03b4a42281f22a83f775..94d13289a90664af9cf354b6cd5778beae0986db 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -187,38 +187,6 @@ end type 'a ty_metadata = {size : 'a Type_size.t} [@@unboxed] -type _ comparable_ty = - | Unit_key : unit comparable_ty - | Never_key : never comparable_ty - | Int_key : z num comparable_ty - | Nat_key : n num comparable_ty - | Signature_key : signature comparable_ty - | String_key : Script_string.t comparable_ty - | Bytes_key : Bytes.t comparable_ty - | Mutez_key : Tez.t comparable_ty - | Bool_key : bool comparable_ty - | Key_hash_key : public_key_hash comparable_ty - | Key_key : public_key comparable_ty - | Timestamp_key : Script_timestamp.t comparable_ty - | Chain_id_key : Script_chain_id.t comparable_ty - | Address_key : address comparable_ty - | Tx_rollup_l2_address_key : tx_rollup_l2_address comparable_ty - | Pair_key : - 'a comparable_ty - * 'b comparable_ty - * ('a, 'b) pair ty_metadata - * (yes, yes, yes) dand - -> ('a, 'b) pair comparable_ty - | Union_key : - 'a comparable_ty - * 'b comparable_ty - * ('a, 'b) union ty_metadata - * (yes, yes, yes) dand - -> ('a, 'b) union comparable_ty - | Option_key : - 'v comparable_ty * 'v option ty_metadata * yes dbool - -> 'v option comparable_ty - module type Boxed_set_OPS = sig type t @@ -1406,6 +1374,8 @@ and ('ty, 'comparable) ty = | Chest_key_t : (Script_timelock.chest_key, no) ty | Chest_t : (Script_timelock.chest, no) ty +and 'ty comparable_ty = ('ty, yes) ty + and ('top_ty, 'resty) stack_ty = | Item_t : ('ty, _) ty * ('ty2, 'rest) stack_ty @@ -1633,31 +1603,31 @@ val union_key : val option_key : Script.location -> 'v comparable_ty -> 'v option comparable_ty tzresult -val unit_t : (unit, yes) ty +val unit_t : unit comparable_ty -val int_t : (z num, yes) ty +val int_t : z num comparable_ty -val nat_t : (n num, yes) ty +val nat_t : n num comparable_ty -val signature_t : (signature, yes) ty +val signature_t : signature comparable_ty -val string_t : (Script_string.t, yes) ty +val string_t : Script_string.t comparable_ty -val bytes_t : (Bytes.t, yes) ty +val bytes_t : Bytes.t comparable_ty -val mutez_t : (Tez.t, yes) ty +val mutez_t : Tez.t comparable_ty -val key_hash_t : (public_key_hash, yes) ty +val key_hash_t : public_key_hash comparable_ty -val key_t : (public_key, yes) ty +val key_t : public_key comparable_ty -val timestamp_t : (Script_timestamp.t, yes) ty +val timestamp_t : Script_timestamp.t comparable_ty -val address_t : (address, yes) ty +val address_t : address comparable_ty -val tx_rollup_l2_address_t : (tx_rollup_l2_address, yes) ty +val tx_rollup_l2_address_t : tx_rollup_l2_address comparable_ty -val bool_t : (bool, yes) ty +val bool_t : bool comparable_ty val pair_t : Script.location -> ('a, _) ty -> ('b, _) ty -> ('a, 'b) pair ty_ex_c tzresult @@ -1675,9 +1645,9 @@ val comparable_union_t : Script.location -> ('a, yes) ty -> ('b, yes) ty -> - (('a, 'b) union, yes) ty tzresult + ('a, 'b) union comparable_ty tzresult -val union_bytes_bool_t : ((Bytes.t, bool) union, yes) ty +val union_bytes_bool_t : (Bytes.t, bool) union comparable_ty val lambda_t : Script.location -> @@ -1687,21 +1657,21 @@ val lambda_t : val option_t : Script.location -> ('v, 'c) ty -> ('v option, 'c) ty tzresult -val option_mutez_t : (Tez.t option, yes) ty +val option_mutez_t : Tez.t option comparable_ty -val option_string_t : (Script_string.t option, yes) ty +val option_string_t : Script_string.t option comparable_ty -val option_bytes_t : (Bytes.t option, yes) ty +val option_bytes_t : Bytes.t option comparable_ty -val option_nat_t : (n num option, yes) ty +val option_nat_t : n num option comparable_ty -val option_pair_nat_nat_t : ((n num, n num) pair option, yes) ty +val option_pair_nat_nat_t : (n num, n num) pair option comparable_ty -val option_pair_nat_mutez_t : ((n num, Tez.t) pair option, yes) ty +val option_pair_nat_mutez_t : (n num, Tez.t) pair option comparable_ty -val option_pair_mutez_mutez_t : ((Tez.t, Tez.t) pair option, yes) ty +val option_pair_mutez_mutez_t : (Tez.t, Tez.t) pair option comparable_ty -val option_pair_int_nat_t : ((z num, n num) pair option, yes) ty +val option_pair_int_nat_t : (z num, n num) pair option comparable_ty val list_t : Script.location -> ('v, _) ty -> ('v boxed_list, no) ty tzresult @@ -1736,9 +1706,9 @@ val sapling_state_t : memo_size:Sapling.Memo_size.t -> (Sapling.state, no) ty val operation_t : (operation, no) ty -val chain_id_t : (Script_chain_id.t, yes) ty +val chain_id_t : Script_chain_id.t comparable_ty -val never_t : (never, yes) ty +val never_t : never comparable_ty val bls12_381_g1_t : (Script_bls.G1.t, no) ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml index 43a3c8b836b8c533250be12e42ff77a2a26f6af5..44174014b62498b2e777886cbbfeddbacdbe0e64 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -45,26 +45,26 @@ let ty_traverse_f = type a. nodes_and_size -> a comparable_ty -> nodes_and_size = fun accu cty -> match cty with - | Unit_key -> ret_succ_adding accu base_basic - | Int_key -> ret_succ_adding accu base_basic - | Nat_key -> ret_succ_adding accu base_basic - | Signature_key -> ret_succ_adding accu base_basic - | String_key -> ret_succ_adding accu base_basic - | Bytes_key -> ret_succ_adding accu base_basic - | Mutez_key -> ret_succ_adding accu base_basic - | Key_hash_key -> ret_succ_adding accu base_basic - | Key_key -> ret_succ_adding accu base_basic - | Timestamp_key -> ret_succ_adding accu base_basic - | Address_key -> ret_succ_adding accu base_basic - | Tx_rollup_l2_address_key -> ret_succ_adding accu base_basic - | Bool_key -> ret_succ_adding accu base_basic - | Chain_id_key -> ret_succ_adding accu base_basic - | Never_key -> ret_succ_adding accu base_basic - | Pair_key (_ty1, _ty2, a, YesYes) -> + | Unit_t -> ret_succ_adding accu base_basic + | Int_t -> ret_succ_adding accu base_basic + | Nat_t -> ret_succ_adding accu base_basic + | Signature_t -> ret_succ_adding accu base_basic + | String_t -> ret_succ_adding accu base_basic + | Bytes_t -> ret_succ_adding accu base_basic + | Mutez_t -> ret_succ_adding accu base_basic + | Key_hash_t -> ret_succ_adding accu base_basic + | Key_t -> ret_succ_adding accu base_basic + | Timestamp_t -> ret_succ_adding accu base_basic + | Address_t -> ret_succ_adding accu base_basic + | Tx_rollup_l2_address_t -> ret_succ_adding accu base_basic + | Bool_t -> ret_succ_adding accu base_basic + | Chain_id_t -> ret_succ_adding accu base_basic + | Never_t -> ret_succ_adding accu base_basic + | Pair_t (_ty1, _ty2, a, YesYes) -> ret_succ_adding accu @@ (base_compound a +! (word_size *? 3)) - | Union_key (_ty1, _ty2, a, YesYes) -> + | Union_t (_ty1, _ty2, a, YesYes) -> ret_succ_adding accu @@ (base_compound a +! (word_size *? 3)) - | Option_key (_ty, a, Yes) -> + | Option_t (_ty, a, Yes) -> ret_succ_adding accu @@ (base_compound a +! (word_size *? 2)) and apply : type a ac. nodes_and_size -> (a, ac) ty -> nodes_and_size = fun accu ty -> @@ -330,26 +330,26 @@ let rec value_size : type a. nodes_and_size -> a comparable_ty -> a -> nodes_and_size = fun accu ty x -> match ty with - | Unit_key -> ret_succ accu - | Int_key -> ret_succ_adding accu (script_int_size x) - | Nat_key -> ret_succ_adding accu (script_nat_size x) - | Signature_key -> ret_succ_adding accu signature_size - | String_key -> ret_succ_adding accu (script_string_size x) - | Bytes_key -> ret_succ_adding accu (bytes_size x) - | Mutez_key -> ret_succ_adding accu mutez_size - | Key_hash_key -> ret_succ_adding accu (key_hash_size x) - | Key_key -> ret_succ_adding accu (public_key_size x) - | Timestamp_key -> ret_succ_adding accu (timestamp_size x) - | Address_key -> ret_succ_adding accu (address_size x) - | Tx_rollup_l2_address_key -> + | Unit_t -> ret_succ accu + | Int_t -> ret_succ_adding accu (script_int_size x) + | Nat_t -> ret_succ_adding accu (script_nat_size x) + | Signature_t -> ret_succ_adding accu signature_size + | String_t -> ret_succ_adding accu (script_string_size x) + | Bytes_t -> ret_succ_adding accu (bytes_size x) + | Mutez_t -> ret_succ_adding accu mutez_size + | Key_hash_t -> ret_succ_adding accu (key_hash_size x) + | Key_t -> ret_succ_adding accu (public_key_size x) + | Timestamp_t -> ret_succ_adding accu (timestamp_size x) + | Address_t -> ret_succ_adding accu (address_size x) + | Tx_rollup_l2_address_t -> ret_succ_adding accu (tx_rollup_l2_address_size x) - | Bool_key -> ret_succ accu - | Pair_key (_, _, _, YesYes) -> ret_succ_adding accu h2w - | Union_key (_, _, _, YesYes) -> ret_succ_adding accu h1w - | Option_key (_, _, Yes) -> + | Bool_t -> ret_succ accu + | Pair_t (_, _, _, YesYes) -> ret_succ_adding accu h2w + | Union_t (_, _, _, YesYes) -> ret_succ_adding accu h1w + | Option_t (_, _, Yes) -> ret_succ_adding accu (option_size (fun _ -> !!0) x) - | Chain_id_key -> ret_succ_adding accu chain_id_size - | Never_key -> ( match x with _ -> .) + | Chain_id_t -> ret_succ_adding accu chain_id_size + | Never_t -> ( match x with _ -> .) in value_traverse ty x accu {apply; apply_comparable} [@@coq_axiom_with_reason "unreachable expressions '.' not handled for now"] diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml b/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml index 12e3a4124e4e370818475e098a9d9b075bb76e30..28b83767cbc602d9d2d75a1b45fb461d706edd2a 100644 --- a/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml +++ b/src/proto_alpha/lib_protocol/test/pbt/test_script_comparison.ml @@ -50,38 +50,37 @@ let rec reference_compare_comparable : type a. a comparable_ty -> a -> a -> int = fun ty x y -> match (ty, x, y) with - | (Unit_key, (), ()) -> 0 - | (Never_key, _, _) -> . - | (Signature_key, x, y) -> normalize_compare @@ Script_signature.compare x y - | (String_key, x, y) -> normalize_compare @@ Script_string.compare x y - | (Bool_key, x, y) -> normalize_compare @@ Compare.Bool.compare x y - | (Mutez_key, x, y) -> normalize_compare @@ Tez.compare x y - | (Key_hash_key, x, y) -> + | (Unit_t, (), ()) -> 0 + | (Never_t, _, _) -> . + | (Signature_t, x, y) -> normalize_compare @@ Script_signature.compare x y + | (String_t, x, y) -> normalize_compare @@ Script_string.compare x y + | (Bool_t, x, y) -> normalize_compare @@ Compare.Bool.compare x y + | (Mutez_t, x, y) -> normalize_compare @@ Tez.compare x y + | (Key_hash_t, x, y) -> normalize_compare @@ Signature.Public_key_hash.compare x y - | (Key_key, x, y) -> normalize_compare @@ Signature.Public_key.compare x y - | (Int_key, x, y) -> normalize_compare @@ Script_int.compare x y - | (Nat_key, x, y) -> normalize_compare @@ Script_int.compare x y - | (Timestamp_key, x, y) -> normalize_compare @@ Script_timestamp.compare x y - | (Address_key, x, y) -> + | (Key_t, x, y) -> normalize_compare @@ Signature.Public_key.compare x y + | (Int_t, x, y) -> normalize_compare @@ Script_int.compare x y + | (Nat_t, x, y) -> normalize_compare @@ Script_int.compare x y + | (Timestamp_t, x, y) -> normalize_compare @@ Script_timestamp.compare x y + | (Address_t, x, y) -> normalize_compare @@ Script_comparable.compare_address x y - | (Tx_rollup_l2_address_key, x, y) -> + | (Tx_rollup_l2_address_t, x, y) -> normalize_compare @@ Script_comparable.compare_tx_rollup_l2_address x y - | (Bytes_key, x, y) -> normalize_compare @@ Compare.Bytes.compare x y - | (Chain_id_key, x, y) -> normalize_compare @@ Script_chain_id.compare x y - | (Pair_key (tl, tr, _, YesYes), (lx, rx), (ly, ry)) -> + | (Bytes_t, x, y) -> normalize_compare @@ Compare.Bytes.compare x y + | (Chain_id_t, x, y) -> normalize_compare @@ Script_chain_id.compare x y + | (Pair_t (tl, tr, _, YesYes), (lx, rx), (ly, ry)) -> let cl = reference_compare_comparable tl lx ly in if Compare.Int.(cl = 0) then reference_compare_comparable tr rx ry else cl - | (Union_key (tl, _, _, YesYes), L x, L y) -> + | (Union_t (tl, _, _, YesYes), L x, L y) -> reference_compare_comparable tl x y - | (Union_key _, L _, R _) -> -1 - | (Union_key _, R _, L _) -> 1 - | (Union_key (_, tr, _, YesYes), R x, R y) -> + | (Union_t _, L _, R _) -> -1 + | (Union_t _, R _, L _) -> 1 + | (Union_t (_, tr, _, YesYes), R x, R y) -> reference_compare_comparable tr x y - | (Option_key _, None, None) -> 0 - | (Option_key _, None, Some _) -> -1 - | (Option_key _, Some _, None) -> 1 - | (Option_key (t, _, Yes), Some x, Some y) -> - reference_compare_comparable t x y + | (Option_t _, None, None) -> 0 + | (Option_t _, None, Some _) -> -1 + | (Option_t _, Some _, None) -> 1 + | (Option_t (t, _, Yes), Some x, Some y) -> reference_compare_comparable t x y (* Generation of one to three values of the same comparable type. *) diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index d024631f13b2e401d873607e00aa622ee1ceedf9..2956a01816d120a9d451c17ee3df8916aefd4a50 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -100,7 +100,7 @@ module Ticket_inspection = struct case. Note that in case tickets are made comparable, this function needs to change - so that constructors like [Union_key] and [Pair_key] are traversed + so that constructors like [Union_t] and [Pair_t] are traversed recursively. *) let has_tickets_of_comparable : @@ -109,24 +109,24 @@ module Ticket_inspection = struct fun key_ty k -> let open Script_typed_ir in match key_ty with - | Unit_key -> (k [@ocaml.tailcall]) False_ht - | Never_key -> (k [@ocaml.tailcall]) False_ht - | Int_key -> (k [@ocaml.tailcall]) False_ht - | Nat_key -> (k [@ocaml.tailcall]) False_ht - | Signature_key -> (k [@ocaml.tailcall]) False_ht - | String_key -> (k [@ocaml.tailcall]) False_ht - | Bytes_key -> (k [@ocaml.tailcall]) False_ht - | Mutez_key -> (k [@ocaml.tailcall]) False_ht - | Bool_key -> (k [@ocaml.tailcall]) False_ht - | Key_hash_key -> (k [@ocaml.tailcall]) False_ht - | Key_key -> (k [@ocaml.tailcall]) False_ht - | Timestamp_key -> (k [@ocaml.tailcall]) False_ht - | Chain_id_key -> (k [@ocaml.tailcall]) False_ht - | Address_key -> (k [@ocaml.tailcall]) False_ht - | Tx_rollup_l2_address_key -> (k [@ocaml.tailcall]) False_ht - | Pair_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht - | Union_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht - | Option_key (_, _, Yes) -> (k [@ocaml.tailcall]) False_ht + | Unit_t -> (k [@ocaml.tailcall]) False_ht + | Never_t -> (k [@ocaml.tailcall]) False_ht + | Int_t -> (k [@ocaml.tailcall]) False_ht + | Nat_t -> (k [@ocaml.tailcall]) False_ht + | Signature_t -> (k [@ocaml.tailcall]) False_ht + | String_t -> (k [@ocaml.tailcall]) False_ht + | Bytes_t -> (k [@ocaml.tailcall]) False_ht + | Mutez_t -> (k [@ocaml.tailcall]) False_ht + | Bool_t -> (k [@ocaml.tailcall]) False_ht + | Key_hash_t -> (k [@ocaml.tailcall]) False_ht + | Key_t -> (k [@ocaml.tailcall]) False_ht + | Timestamp_t -> (k [@ocaml.tailcall]) False_ht + | Chain_id_t -> (k [@ocaml.tailcall]) False_ht + | Address_t -> (k [@ocaml.tailcall]) False_ht + | Tx_rollup_l2_address_t -> (k [@ocaml.tailcall]) False_ht + | Pair_t (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht + | Union_t (_, _, _, YesYes) -> (k [@ocaml.tailcall]) False_ht + | Option_t (_, _, Yes) -> (k [@ocaml.tailcall]) False_ht (* Short circuit pairing of two [has_tickets] values. If neither left nor right branch contains a ticket, [False_ht] is @@ -274,24 +274,24 @@ module Ticket_collection = struct fun ctxt comp_ty acc k -> let open Script_typed_ir in match comp_ty with - | Unit_key -> (k [@ocaml.tailcall]) ctxt acc - | Never_key -> (k [@ocaml.tailcall]) ctxt acc - | Int_key -> (k [@ocaml.tailcall]) ctxt acc - | Nat_key -> (k [@ocaml.tailcall]) ctxt acc - | Signature_key -> (k [@ocaml.tailcall]) ctxt acc - | String_key -> (k [@ocaml.tailcall]) ctxt acc - | Bytes_key -> (k [@ocaml.tailcall]) ctxt acc - | Mutez_key -> (k [@ocaml.tailcall]) ctxt acc - | Bool_key -> (k [@ocaml.tailcall]) ctxt acc - | Key_hash_key -> (k [@ocaml.tailcall]) ctxt acc - | Key_key -> (k [@ocaml.tailcall]) ctxt acc - | Timestamp_key -> (k [@ocaml.tailcall]) ctxt acc - | Chain_id_key -> (k [@ocaml.tailcall]) ctxt acc - | Address_key -> (k [@ocaml.tailcall]) ctxt acc - | Tx_rollup_l2_address_key -> (k [@ocaml.tailcall]) ctxt acc - | Pair_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc - | Union_key (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc - | Option_key (_, _, Yes) -> (k [@ocaml.tailcall]) ctxt acc + | Unit_t -> (k [@ocaml.tailcall]) ctxt acc + | Never_t -> (k [@ocaml.tailcall]) ctxt acc + | Int_t -> (k [@ocaml.tailcall]) ctxt acc + | Nat_t -> (k [@ocaml.tailcall]) ctxt acc + | Signature_t -> (k [@ocaml.tailcall]) ctxt acc + | String_t -> (k [@ocaml.tailcall]) ctxt acc + | Bytes_t -> (k [@ocaml.tailcall]) ctxt acc + | Mutez_t -> (k [@ocaml.tailcall]) ctxt acc + | Bool_t -> (k [@ocaml.tailcall]) ctxt acc + | Key_hash_t -> (k [@ocaml.tailcall]) ctxt acc + | Key_t -> (k [@ocaml.tailcall]) ctxt acc + | Timestamp_t -> (k [@ocaml.tailcall]) ctxt acc + | Chain_id_t -> (k [@ocaml.tailcall]) ctxt acc + | Address_t -> (k [@ocaml.tailcall]) ctxt acc + | Tx_rollup_l2_address_t -> (k [@ocaml.tailcall]) ctxt acc + | Pair_t (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc + | Union_t (_, _, _, YesYes) -> (k [@ocaml.tailcall]) ctxt acc + | Option_t (_, _, Yes) -> (k [@ocaml.tailcall]) ctxt acc let tickets_of_set : type a ret.