From c18e46f3f1254a06e61dd7fde7b95eac4dc08c6d Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 30 Nov 2021 10:41:37 +0100 Subject: [PATCH 01/19] Proto/Micheslon: add Nomadic Labs copyright. --- .../lib_benchmark/michelson_samplers.ml | 2 +- .../lib_benchmark/michelson_samplers.mli | 2 +- .../interpreter_benchmarks.ml | 2 +- .../interpreter_workload.ml | 2 +- src/proto_alpha/lib_benchmarks_proto/size.ml | 2 +- src/proto_alpha/lib_protocol/alpha_context.ml | 2 +- .../lib_protocol/alpha_context.mli | 2 +- .../lib_protocol/michelson_v1_gas.ml | 2 +- .../lib_protocol/michelson_v1_gas.mli | 1 + .../lib_protocol/script_comparable.ml | 1 + .../lib_protocol/script_int_repr.ml | 1 + .../lib_protocol/script_int_repr.mli | 1 + .../lib_protocol/script_interpreter.ml | 2 +- .../lib_protocol/script_interpreter_defs.ml | 2 +- .../lib_protocol/script_ir_translator.ml | 1 + .../lib_protocol/script_ir_translator.mli | 1 + src/proto_alpha/lib_protocol/script_map.ml | 1 + src/proto_alpha/lib_protocol/script_set.ml | 1 + .../lib_protocol/script_string_repr.ml | 2 +- .../lib_protocol/script_string_repr.mli | 2 +- .../lib_protocol/script_timestamp_repr.ml | 1 + .../lib_protocol/script_timestamp_repr.mli | 1 + .../lib_protocol/script_typed_ir.ml | 1 + .../lib_protocol/script_typed_ir.mli | 1 + .../lib_protocol/script_typed_ir_size.ml | 2 +- .../lib_protocol/script_typed_ir_size.mli | 2 +- .../michelson/test_typechecking.ml | 25 +++++++++++++++++++ .../test/pbt/test_script_comparison.ml | 2 +- src/proto_alpha/lib_protocol/tez_repr.ml | 2 +- src/proto_alpha/lib_protocol/tez_repr.mli | 2 +- .../lib_protocol/ticket_balance_key.ml | 1 + .../lib_protocol/ticket_scanner.ml | 1 + 32 files changed, 56 insertions(+), 17 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index 3a6103d3dc5a..9af0814916db 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.mli b/src/proto_alpha/lib_benchmark/michelson_samplers.mli index 813638f3cab2..4ab6d5bd30be 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.mli +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.mli @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index 3ec52df528f6..e2cc54fa76ca 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml index 7f48a5271d5b..93a80c06aa08 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_benchmarks_proto/size.ml b/src/proto_alpha/lib_benchmarks_proto/size.ml index e3a3e0c14a61..834b27b7c713 100644 --- a/src/proto_alpha/lib_benchmarks_proto/size.ml +++ b/src/proto_alpha/lib_benchmarks_proto/size.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/alpha_context.ml b/src/proto_alpha/lib_protocol/alpha_context.ml index d4706d7c734e..cd38eb3b12b6 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.ml +++ b/src/proto_alpha/lib_protocol/alpha_context.ml @@ -2,7 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) -(* Copyright (c) 2019-2020 Nomadic Labs *) +(* Copyright (c) 2019-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 4049cb49dabe..51a7d6eb282c 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -2,7 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) -(* Copyright (c) 2019-2021 Nomadic Labs *) +(* Copyright (c) 2019-2022 Nomadic Labs *) (* Copyright (c) 2021 Trili Tech, *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 55f8e60ec364..6c5e392eb43b 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -2,7 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) -(* Copyright (c) 2019-2020 Nomadic Labs *) +(* Copyright (c) 2019-2022 Nomadic Labs *) (* Copyright (c) 2020 Metastate AG *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli index 2b4674cbcca1..bd90bd06db55 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2019-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml index 93c58db7b90f..da761092cd9c 100644 --- a/src/proto_alpha/lib_protocol/script_comparable.ml +++ b/src/proto_alpha/lib_protocol/script_comparable.ml @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* Copyright (c) 2020 Metastate AG *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) diff --git a/src/proto_alpha/lib_protocol/script_int_repr.ml b/src/proto_alpha/lib_protocol/script_int_repr.ml index f5eff71ab42c..7bea740237a0 100644 --- a/src/proto_alpha/lib_protocol/script_int_repr.ml +++ b/src/proto_alpha/lib_protocol/script_int_repr.ml @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_int_repr.mli b/src/proto_alpha/lib_protocol/script_int_repr.mli index b31894d5982f..b104b3620141 100644 --- a/src/proto_alpha/lib_protocol/script_int_repr.mli +++ b/src/proto_alpha/lib_protocol/script_int_repr.mli @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index f979279bd2b5..ce1e602a42a4 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -3,7 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml index bcafd60fcf2c..1b9c2a9ed962 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 655d8db2d99f..55a938c0e308 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -3,6 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.mli b/src/proto_alpha/lib_protocol/script_ir_translator.mli index 24c1d6ef4daa..0fef3a64fd54 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.mli +++ b/src/proto_alpha/lib_protocol/script_ir_translator.mli @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_map.ml b/src/proto_alpha/lib_protocol/script_map.ml index d53d16aeefeb..4404669e8e79 100644 --- a/src/proto_alpha/lib_protocol/script_map.ml +++ b/src/proto_alpha/lib_protocol/script_map.ml @@ -3,6 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_set.ml b/src/proto_alpha/lib_protocol/script_set.ml index 703ffae7aaa7..76cbb2249a06 100644 --- a/src/proto_alpha/lib_protocol/script_set.ml +++ b/src/proto_alpha/lib_protocol/script_set.ml @@ -3,6 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_string_repr.ml b/src/proto_alpha/lib_protocol/script_string_repr.ml index e6e45dd9ee6d..a3507f16fa32 100644 --- a/src/proto_alpha/lib_protocol/script_string_repr.ml +++ b/src/proto_alpha/lib_protocol/script_string_repr.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_string_repr.mli b/src/proto_alpha/lib_protocol/script_string_repr.mli index f94b65b389e1..1ff35728088c 100644 --- a/src/proto_alpha/lib_protocol/script_string_repr.mli +++ b/src/proto_alpha/lib_protocol/script_string_repr.mli @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_timestamp_repr.ml b/src/proto_alpha/lib_protocol/script_timestamp_repr.ml index 22b51a4945f0..aed8577b5d5b 100644 --- a/src/proto_alpha/lib_protocol/script_timestamp_repr.ml +++ b/src/proto_alpha/lib_protocol/script_timestamp_repr.ml @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_timestamp_repr.mli b/src/proto_alpha/lib_protocol/script_timestamp_repr.mli index 2e628dae2991..3e735bbe65e2 100644 --- a/src/proto_alpha/lib_protocol/script_timestamp_repr.mli +++ b/src/proto_alpha/lib_protocol/script_timestamp_repr.mli @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 5d9fe73d0af7..788c4789bb6d 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -3,6 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 4991feaedf3e..c1e55c91ae4f 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -3,6 +3,7 @@ (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) (* Copyright (c) 2020 Metastate AG *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) 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 c9825ec644ba..bcb1ca429426 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir_size.mli b/src/proto_alpha/lib_protocol/script_typed_ir_size.mli index b40ad8c45156..9b51ba8b8cac 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.mli @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml index 2a5e6d612a89..3718c81602e9 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml @@ -1,3 +1,28 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021-2022 Nomadic Labs *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + (** Testing ------- Component: Protocol (type-checking) 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 640f7266f377..b5b4471f748b 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 @@ -1,7 +1,7 @@ (*****************************************************************************) (* *) (* Open Source License *) -(* Copyright (c) 2021 Nomadic Labs, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/tez_repr.ml b/src/proto_alpha/lib_protocol/tez_repr.ml index 5636b07a16f0..b1612b974c07 100644 --- a/src/proto_alpha/lib_protocol/tez_repr.ml +++ b/src/proto_alpha/lib_protocol/tez_repr.ml @@ -2,7 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) -(* Copyright (c) 2020 Nomadic Labs *) +(* Copyright (c) 2020-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/tez_repr.mli b/src/proto_alpha/lib_protocol/tez_repr.mli index 168dcac9b04f..155edc54df51 100644 --- a/src/proto_alpha/lib_protocol/tez_repr.mli +++ b/src/proto_alpha/lib_protocol/tez_repr.mli @@ -2,7 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2018 Dynamic Ledger Solutions, Inc. *) -(* Copyright (c) 2020 Nomadic Labs *) +(* Copyright (c) 2020-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/ticket_balance_key.ml b/src/proto_alpha/lib_protocol/ticket_balance_key.ml index 2a12426b0e29..1011c9a0824f 100644 --- a/src/proto_alpha/lib_protocol/ticket_balance_key.ml +++ b/src/proto_alpha/lib_protocol/ticket_balance_key.ml @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2021 Trili Tech, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index ddccfb016cc7..c553c3d22d75 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -2,6 +2,7 @@ (* *) (* Open Source License *) (* Copyright (c) 2021 Trili Tech, *) +(* Copyright (c) 2021-2022 Nomadic Labs *) (* *) (* Permission is hereby granted, free of charge, to any person obtaining a *) (* copy of this software and associated documentation files (the "Software"),*) -- GitLab From 5cde8dac10420e6a776757735bb42b51f5b2b004 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 30 Nov 2021 11:00:07 +0100 Subject: [PATCH 02/19] Proto/Michelson: make Script_string_repr.t algebraic. --- .../lib_protocol/script_string_repr.ml | 22 +++++++++++-------- .../lib_protocol/script_string_repr.mli | 6 ++++- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/proto_alpha/lib_protocol/script_string_repr.ml b/src/proto_alpha/lib_protocol/script_string_repr.ml index a3507f16fa32..b3108eb31ef2 100644 --- a/src/proto_alpha/lib_protocol/script_string_repr.ml +++ b/src/proto_alpha/lib_protocol/script_string_repr.ml @@ -25,7 +25,9 @@ (** Strings of printable characters *) -type t = string (* Invariant: contains only printable characters *) +type repr = string (* Invariant: contains only printable characters *) + +type t = String_tag of repr [@@ocaml.unboxed] type error += Non_printable_character of (int * string) @@ -52,11 +54,11 @@ let () = (function Non_printable_character (pos, s) -> Some (pos, s) | _ -> None) (fun (pos, s) -> Non_printable_character (pos, s)) -let empty = "" +let empty = String_tag "" let of_string v = let rec check_printable_ascii i = - if Compare.Int.(i < 0) then ok v + if Compare.Int.(i < 0) then ok (String_tag v) else match v.[i] with | '\n' | '\x20' .. '\x7E' -> check_printable_ascii (i - 1) @@ -64,14 +66,16 @@ let of_string v = in check_printable_ascii (String.length v - 1) -let to_string s = s +let to_string (String_tag s) = s -let compare = Compare.String.compare +let compare (String_tag x) (String_tag y) = Compare.String.compare x y -let length = String.length +let length (String_tag s) = String.length s -let concat_pair x y = x ^ y +let concat_pair (String_tag x) (String_tag y) = String_tag (x ^ y) -let concat l = String.concat "" l +let concat l = + let l = List.map (fun (String_tag s) -> s) l in + String_tag (String.concat "" l) -let sub s offset length = String.sub s offset length +let sub (String_tag s) offset length = String_tag (String.sub s offset length) diff --git a/src/proto_alpha/lib_protocol/script_string_repr.mli b/src/proto_alpha/lib_protocol/script_string_repr.mli index 1ff35728088c..e76a3b15e67c 100644 --- a/src/proto_alpha/lib_protocol/script_string_repr.mli +++ b/src/proto_alpha/lib_protocol/script_string_repr.mli @@ -25,7 +25,11 @@ (** Strings of printable characters *) -type t +type repr + +(** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) +type t = String_tag of repr [@@ocaml.unboxed] type error += Non_printable_character of (int * string) -- GitLab From 56536db745bad900c2dfc01d24b6ff05c5c260d7 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 30 Nov 2021 13:48:22 +0100 Subject: [PATCH 03/19] Proto/Michelson: make Tez_repr.t algebraic. --- .../lib_protocol/alpha_context.mli | 6 +- src/proto_alpha/lib_protocol/tez_repr.ml | 88 +++++++++++++------ src/proto_alpha/lib_protocol/tez_repr.mli | 6 +- 3 files changed, 72 insertions(+), 28 deletions(-) diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 51a7d6eb282c..a1bc60ac3169 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -89,7 +89,11 @@ module Slot : sig end module Tez : sig - include BASIC_DATA + type repr + + type t = Tez_tag of repr [@@ocaml.unboxed] + + include BASIC_DATA with type t := t type tez = t diff --git a/src/proto_alpha/lib_protocol/tez_repr.ml b/src/proto_alpha/lib_protocol/tez_repr.ml index b1612b974c07..44a82ec6668f 100644 --- a/src/proto_alpha/lib_protocol/tez_repr.ml +++ b/src/proto_alpha/lib_protocol/tez_repr.ml @@ -28,7 +28,11 @@ let id = "tez" let name = "mutez" -include Compare.Int64 (* invariant: positive *) +open Compare.Int64 (* invariant: positive *) + +type repr = t + +type t = Tez_tag of repr [@@ocaml.unboxed] type error += | Addition_overflow of t * t (* `Temporary *) @@ -39,17 +43,19 @@ type error += (* `Temporary *) -let zero = 0L +let zero = Tez_tag 0L (* all other constant are defined from the value of one micro tez *) -let one_mutez = 1L +let one_mutez = Tez_tag 1L -let one_cent = Int64.mul one_mutez 10_000L +let mul_int (Tez_tag tez) i = Tez_tag (Int64.mul tez i) -let fifty_cents = Int64.mul one_cent 50L +let one_cent = mul_int one_mutez 10_000L + +let fifty_cents = mul_int one_cent 50L (* 1 tez = 100 cents = 1_000_000 mutez *) -let one = Int64.mul one_cent 100L +let one = mul_int one_cent 100L let of_string s = let triplets = function @@ -70,7 +76,8 @@ let of_string s = let len = String.length s in String.init 6 (fun i -> if Compare.Int.(i < len) then s.[i] else '0') in - Int64.of_string_opt (remove_commas left ^ pad_to_six (remove_commas right)) + let prepared = remove_commas left ^ pad_to_six (remove_commas right) in + Option.map (fun i -> Tez_tag i) (Int64.of_string_opt prepared) in match String.split_on_char '.' s with | [left; right] -> @@ -86,7 +93,7 @@ let of_string s = else None | _ -> None -let pp ppf amount = +let pp ppf (Tez_tag amount) = let mult_int = 1_000_000L in let[@coq_struct "amount"] rec left ppf amount = let (d, r) = (Int64.(div amount 1000L), Int64.(rem amount 1000L)) in @@ -111,24 +118,33 @@ let pp ppf amount = let to_string t = Format.asprintf "%a" pp t -let ( -? ) t1 t2 = - if t2 <= t1 then ok (Int64.sub t1 t2) - else error (Subtraction_underflow (t1, t2)) +let ( -? ) tez1 tez2 = + let (Tez_tag t1) = tez1 in + let (Tez_tag t2) = tez2 in + if t2 <= t1 then ok (Tez_tag (Int64.sub t1 t2)) + else error (Subtraction_underflow (tez1, tez2)) -let sub_opt t1 t2 = if t2 <= t1 then Some (Int64.sub t1 t2) else None +let sub_opt (Tez_tag t1) (Tez_tag t2) = + if t2 <= t1 then Some (Tez_tag (Int64.sub t1 t2)) else None -let ( +? ) t1 t2 = +let ( +? ) tez1 tez2 = + let (Tez_tag t1) = tez1 in + let (Tez_tag t2) = tez2 in let t = Int64.add t1 t2 in - if t < t1 then error (Addition_overflow (t1, t2)) else ok t + if t < t1 then error (Addition_overflow (tez1, tez2)) else ok (Tez_tag t) -let ( *? ) t m = - if m < 0L then error (Negative_multiplicator (t, m)) - else if m = 0L then ok 0L - else if t > Int64.(div max_int m) then error (Multiplication_overflow (t, m)) - else ok (Int64.mul t m) +let ( *? ) tez m = + let (Tez_tag t) = tez in + if m < 0L then error (Negative_multiplicator (tez, m)) + else if m = 0L then ok (Tez_tag 0L) + else if t > Int64.(div max_int m) then + error (Multiplication_overflow (tez, m)) + else ok (Tez_tag (Int64.mul t m)) -let ( /? ) t d = - if d <= 0L then error (Invalid_divisor (t, d)) else ok (Int64.div t d) +let ( /? ) tez d = + let (Tez_tag t) = tez in + if d <= 0L then error (Invalid_divisor (tez, d)) + else ok (Tez_tag (Int64.div t d)) let mul_exn t m = match t *? Int64.(of_int m) with @@ -140,18 +156,18 @@ let div_exn t d = | Ok v -> v | Error _ -> invalid_arg "div_exn" -let of_mutez t = if t < 0L then None else Some t +let of_mutez t = if t < 0L then None else Some (Tez_tag t) let of_mutez_exn x = match of_mutez x with None -> invalid_arg "Tez.of_mutez" | Some v -> v -let to_mutez t = t +let to_mutez (Tez_tag t) = t let encoding = let open Data_encoding in - Data_encoding.def - name - (check_size 10 (conv Z.of_int64 (Json.wrap_error Z.to_int64) n)) + let decode (Tez_tag t) = Z.of_int64 t in + let encode = Json.wrap_error (fun i -> Tez_tag (Z.to_int64 i)) in + Data_encoding.def name (check_size 10 (conv decode encode n)) let () = let open Data_encoding in @@ -243,3 +259,23 @@ let () = (fun (a, b) -> Invalid_divisor (a, b)) type tez = t + +let compare (Tez_tag x) (Tez_tag y) = compare x y + +let ( = ) (Tez_tag x) (Tez_tag y) = x = y + +let ( <> ) (Tez_tag x) (Tez_tag y) = x <> y + +let ( < ) (Tez_tag x) (Tez_tag y) = x < y + +let ( > ) (Tez_tag x) (Tez_tag y) = x > y + +let ( <= ) (Tez_tag x) (Tez_tag y) = x <= y + +let ( >= ) (Tez_tag x) (Tez_tag y) = x >= y + +let equal (Tez_tag x) (Tez_tag y) = equal x y + +let max (Tez_tag x) (Tez_tag y) = Tez_tag (max x y) + +let min (Tez_tag x) (Tez_tag y) = Tez_tag (min x y) diff --git a/src/proto_alpha/lib_protocol/tez_repr.mli b/src/proto_alpha/lib_protocol/tez_repr.mli index 155edc54df51..1ceab70371f0 100644 --- a/src/proto_alpha/lib_protocol/tez_repr.mli +++ b/src/proto_alpha/lib_protocol/tez_repr.mli @@ -24,7 +24,11 @@ (* *) (*****************************************************************************) -type t +type repr + +(** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) +type t = Tez_tag of repr [@@ocaml.unboxed] type tez = t -- GitLab From 67f5439832e310c6d6656439fcf6327bd8dd6a20 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 30 Nov 2021 16:49:23 +0100 Subject: [PATCH 04/19] Proto/Michelson: make Script_timestamp_repr.t algebraic. --- .../lib_protocol/alpha_context.mli | 4 ++- .../lib_protocol/script_timestamp_repr.ml | 29 +++++++++++-------- .../lib_protocol/script_timestamp_repr.mli | 8 +++-- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index a1bc60ac3169..0316d4953830 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -464,7 +464,9 @@ module Script_int : module type of Script_int_repr module Script_timestamp : sig open Script_int - type t + type repr + + type t = Timestamp_tag of repr [@@ocaml.unboxed] val compare : t -> t -> int diff --git a/src/proto_alpha/lib_protocol/script_timestamp_repr.ml b/src/proto_alpha/lib_protocol/script_timestamp_repr.ml index aed8577b5d5b..f62077e31915 100644 --- a/src/proto_alpha/lib_protocol/script_timestamp_repr.ml +++ b/src/proto_alpha/lib_protocol/script_timestamp_repr.ml @@ -24,33 +24,38 @@ (* *) (*****************************************************************************) -type t = Z.t +type repr = Z.t -let compare = Z.compare +type t = Timestamp_tag of repr [@@ocaml.unboxed] -let of_int64 = Z.of_int64 +let compare (Timestamp_tag x) (Timestamp_tag y) = Z.compare x y + +let of_int64 i = Timestamp_tag (Z.of_int64 i) let of_string x = match Time_repr.of_notation x with - | None -> Option.catch (fun () -> Z.of_string x) + | None -> Option.catch (fun () -> Timestamp_tag (Z.of_string x)) | Some time -> Some (of_int64 (Time_repr.to_seconds time)) -let to_notation x = +let to_notation (Timestamp_tag x) = Option.catch (fun () -> Time_repr.to_notation (Time.of_seconds (Z.to_int64 x))) -let to_num_str = Z.to_string +let to_num_str (Timestamp_tag x) = Z.to_string x let to_string x = match to_notation x with None -> to_num_str x | Some s -> s -let diff x y = Script_int_repr.of_zint @@ Z.sub x y +let diff (Timestamp_tag x) (Timestamp_tag y) = + Script_int_repr.of_zint @@ Z.sub x y -let sub_delta t delta = Z.sub t (Script_int_repr.to_zint delta) +let sub_delta (Timestamp_tag t) delta = + Timestamp_tag (Z.sub t (Script_int_repr.to_zint delta)) -let add_delta t delta = Z.add t (Script_int_repr.to_zint delta) +let add_delta (Timestamp_tag t) delta = + Timestamp_tag (Z.add t (Script_int_repr.to_zint delta)) -let to_zint x = x +let to_zint (Timestamp_tag x) = x -let of_zint x = x +let of_zint x = Timestamp_tag x -let encoding : t Data_encoding.encoding = Data_encoding.z +let encoding = Data_encoding.(conv to_zint of_zint z) diff --git a/src/proto_alpha/lib_protocol/script_timestamp_repr.mli b/src/proto_alpha/lib_protocol/script_timestamp_repr.mli index 3e735bbe65e2..258302cd26a7 100644 --- a/src/proto_alpha/lib_protocol/script_timestamp_repr.mli +++ b/src/proto_alpha/lib_protocol/script_timestamp_repr.mli @@ -29,9 +29,13 @@ open Script_int_repr +type repr + (** Representation of timestamps specific to the Michelson interpreter. - A number of seconds since the epoch. *) -type t + A number of seconds since the epoch. + [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) +type t = Timestamp_tag of repr [@@ocaml.unboxed] (** Convert a number of seconds since the epoch to a timestamp.*) val of_int64 : int64 -> t -- GitLab From 22669a946e68533f92de485d7373e0a00236f4fe Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 5 Jan 2022 23:28:05 +0100 Subject: [PATCH 05/19] Proto/Michelson: make Script_typed_ir.address unique. --- .../lib_benchmark/michelson_samplers.ml | 15 ++++---- src/proto_alpha/lib_benchmarks_proto/size.ml | 2 +- .../lib_protocol/script_comparable.ml | 8 +++-- .../lib_protocol/script_interpreter.ml | 32 +++++++++-------- .../lib_protocol/script_ir_translator.ml | 34 ++++++++++--------- .../lib_protocol/script_typed_ir.ml | 2 +- .../lib_protocol/script_typed_ir.mli | 2 +- .../lib_protocol/script_typed_ir_size.ml | 6 ++-- .../test/helpers/liquidity_baking_machine.ml | 4 +-- .../michelson/test_typechecking.ml | 4 +-- .../lib_protocol/ticket_balance_key.ml | 8 +++-- 11 files changed, 67 insertions(+), 50 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index 9af0814916db..b0893a438ad2 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -488,9 +488,12 @@ end) end = struct let address rng_state = if Base_samplers.uniform_bool rng_state then - ( Alpha_context.Contract.implicit_contract - (Crypto_samplers.pkh rng_state), - Alpha_context.Entrypoint.default ) + { + contract = + Alpha_context.Contract.implicit_contract + (Crypto_samplers.pkh rng_state); + entrypoint = Alpha_context.Entrypoint.default; + } else (* For a description of the format, see tezos-codec describe alpha.contract binary encoding *) @@ -506,7 +509,7 @@ end) Alpha_context.Entrypoint.of_string_strict_exn @@ Base_samplers.string ~size:{min = 1; max = 31} rng_state in - (contract, ep) + {contract; entrypoint = ep} let chain_id rng_state = let string = Base_samplers.uniform_string ~nbytes:4 rng_state in @@ -662,8 +665,8 @@ end) arg Script_typed_ir.ty -> arg Script_typed_ir.typed_contract sampler = fun arg_ty -> let open M in - let* addr = value (address_t ~annot:None) in - return (arg_ty, addr) + let* address = value (address_t ~annot:None) in + return (arg_ty, address) and generate_operation : (Alpha_context.packed_internal_operation diff --git a/src/proto_alpha/lib_benchmarks_proto/size.ml b/src/proto_alpha/lib_benchmarks_proto/size.ml index 834b27b7c713..e6b8431dfe25 100644 --- a/src/proto_alpha/lib_benchmarks_proto/size.ml +++ b/src/proto_alpha/lib_benchmarks_proto/size.ml @@ -139,7 +139,7 @@ let public_key (public_key : Signature.public_key) : t = let chain_id (_chain_id : Chain_id.t) : t = Chain_id.size let address (addr : Script_typed_ir.address) : t = - let (_contract, entrypoint) = addr in + let entrypoint = addr.entrypoint in Signature.Public_key_hash.size + String.length (Alpha_context.Entrypoint.to_string entrypoint) diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml index da761092cd9c..79a947cd2b1e 100644 --- a/src/proto_alpha/lib_protocol/script_comparable.ml +++ b/src/proto_alpha/lib_protocol/script_comparable.ml @@ -28,9 +28,11 @@ open Alpha_context open Script_typed_ir -let compare_address (x, ex) (y, ey) = - let lres = Contract.compare x y in - if Compare.Int.(lres = 0) then Entrypoint.compare ex ey else lres +let compare_address {contract = contract1; entrypoint = entrypoint1} + {contract = contract2; entrypoint = entrypoint2} = + let lres = Contract.compare contract1 contract2 in + if Compare.Int.(lres = 0) then Entrypoint.compare entrypoint1 entrypoint2 + else lres type compare_comparable_cont = | Compare_comparable : diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index ce1e602a42a4..c33a8add5541 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -986,11 +986,10 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = let (_, address) = accu in (step [@ocaml.tailcall]) g gas k ks address stack | IContract (kinfo, t, entrypoint, k) -> ( - let (contract, contract_entrypoint) = accu in + let addr = accu in let entrypoint_opt = - if Entrypoint.is_default contract_entrypoint then Some entrypoint - else if Entrypoint.is_default entrypoint then - Some contract_entrypoint + if Entrypoint.is_default addr.entrypoint then Some entrypoint + else if Entrypoint.is_default entrypoint then Some addr.entrypoint else (* both entrypoints are non-default *) None in match entrypoint_opt with @@ -1000,7 +999,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = ctxt kinfo.iloc t - contract + addr.contract ~entrypoint >>=? fun (ctxt, maybe_contract) -> let gas = update_local_gas_counter ctxt in @@ -1010,18 +1009,22 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) | ITransfer_tokens (_, k) -> let p = accu in - let (amount, ((tp, (destination, entrypoint)), stack)) = stack in + let (amount, ((tp, addr_dst), stack)) = stack in + let destination = addr_dst.contract in + let entrypoint = addr_dst.entrypoint in transfer (ctxt, sc) gas amount tp p destination entrypoint >>=? fun (accu, ctxt, gas) -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack | IImplicit_account (_, k) -> let key = accu in let contract = Contract.implicit_contract key in - let res = (unit_t ~annot:None, (contract, Entrypoint.default)) in + let entrypoint = Entrypoint.default in + let res = (unit_t ~annot:None, {contract; entrypoint}) in (step [@ocaml.tailcall]) g gas k ks res stack | IView (_, View_signature {name; input_ty; output_ty}, k) -> ( let input = accu in - let ((c, _entrypoint_is_ignored), stack) = stack in + let (addr, stack) = stack in + let c = addr.contract in let ctxt = update_context gas ctxt in Contract.get_script ctxt c >>=? fun (ctxt, script_opt) -> let return_none ctxt = @@ -1144,7 +1147,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = credit init >>=? fun (res, contract, ctxt, gas) -> - let stack = ((contract, Entrypoint.default), stack) in + let stack = ({contract; entrypoint = Entrypoint.default}, stack) in (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack | ISet_delegate (_, k) -> let delegate = accu in @@ -1187,16 +1190,16 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = let hash = Raw_hashes.sha512 bytes in (step [@ocaml.tailcall]) g gas k ks hash stack | ISource (_, k) -> - let res = (sc.payer, Entrypoint.default) in + let res = {contract = sc.payer; entrypoint = Entrypoint.default} in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | ISender (_, k) -> - let res = (sc.source, Entrypoint.default) in + let res = {contract = sc.source; entrypoint = Entrypoint.default} in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | ISelf (_, ty, entrypoint, k) -> - let res = (ty, (sc.self, entrypoint)) in + let res = (ty, {contract = sc.self; entrypoint}) in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | ISelf_address (_, k) -> - let res = (sc.self, Entrypoint.default) in + let res = {contract = sc.self; entrypoint = Entrypoint.default} in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | IAmount (_, k) -> let accu = sc.amount and stack = (accu, stack) in @@ -1423,7 +1426,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = | IRead_ticket (_, k) -> let {ticketer; contents; amount} = accu in let stack = (accu, stack) in - let accu = ((ticketer, Entrypoint.default), (contents, amount)) in + let addr = {contract = ticketer; entrypoint = Entrypoint.default} in + let accu = (addr, (contents, amount)) in (step [@ocaml.tailcall]) g gas k ks accu stack | ISplit_ticket (_, k) -> let ticket = accu and ((amount_a, amount_b), stack) = stack in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 55a938c0e308..9d8a0e040e77 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -465,19 +465,19 @@ let unparse_timestamp ~loc ctxt mode t = | None -> ok (Int (loc, Script_timestamp.to_zint t), ctxt) | Some s -> ok (String (loc, s), ctxt)) -let unparse_address ~loc ctxt mode (c, entrypoint) = +let unparse_address ~loc ctxt mode {contract; entrypoint} = Gas.consume ctxt Unparse_costs.contract >|? fun ctxt -> match mode with | Optimized | Optimized_legacy -> let bytes = Data_encoding.Binary.to_bytes_exn Data_encoding.(tup2 Contract.encoding Entrypoint.value_encoding) - (c, entrypoint) + (contract, entrypoint) in (Bytes (loc, bytes), ctxt) | Readable -> let notation = - Contract.to_b58check c ^ Entrypoint.to_address_suffix entrypoint + Contract.to_b58check contract ^ Entrypoint.to_address_suffix entrypoint in (String (loc, notation), ctxt) @@ -2253,7 +2253,7 @@ let parse_address ctxt : Script.node -> (address * context) tzresult = function Data_encoding.(tup2 Contract.encoding Entrypoint.value_encoding) bytes with - | Some addr -> Ok (addr, ctxt) + | Some (contract, entrypoint) -> Ok ({contract; entrypoint}, ctxt) | None -> error @@ Invalid_syntactic_constant @@ -2268,7 +2268,8 @@ let parse_address ctxt : Script.node -> (address * context) tzresult = function Entrypoint.of_string_strict ~loc name >|? fun entrypoint -> (String.sub s 0 pos, entrypoint)) >>? fun (addr, entrypoint) -> - Contract.of_b58check addr >|? fun c -> ((c, entrypoint), ctxt) + Contract.of_b58check addr >|? fun contract -> + ({contract; entrypoint}, ctxt) | expr -> error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr) @@ -2592,7 +2593,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr | (Contract_t (ty, _), expr) -> traced - ( parse_address ctxt expr >>?= fun ((c, entrypoint), ctxt) -> + ( parse_address ctxt expr >>?= fun (address, ctxt) -> let loc = location expr in parse_contract ~stack_depth:(stack_depth + 1) @@ -2600,9 +2601,9 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : ctxt loc ty - c - ~entrypoint - >|=? fun (ctxt, _) -> ((ty, (c, entrypoint)), ctxt) ) + address.contract + ~entrypoint:address.entrypoint + >|=? fun (ctxt, _) -> ((ty, address), ctxt) ) (* Pairs *) | (Pair_t ((tl, _, _), (tr, _, _), _), expr) -> let r_witness = comb_witness1 tr in @@ -2658,8 +2659,8 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : if allow_forged then opened_ticket_type (location expr) t >>?= fun ty -> parse_comparable_data ?type_logger ctxt ty expr - >|=? fun (((ticketer, _entrypoint), (contents, amount)), ctxt) -> - ({ticketer; contents; amount}, ctxt) + >|=? fun (({contract; entrypoint = _}, (contents, amount)), ctxt) -> + ({ticketer = contract; contents; amount}, ctxt) else traced_fail (Unexpected_forged_value (location expr)) (* Sets *) | (Set_t (t, _ty_name), (Seq (loc, vs) as expr)) -> @@ -5216,7 +5217,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra Lwt.return ( ty_eq ~legacy:true ctxt loc arg (unit_t ~annot:None) >|? fun (Eq, ctxt) -> - let contract : arg typed_contract = (arg, (contract, entrypoint)) in + let contract : arg typed_contract = (arg, {contract; entrypoint}) in (ctxt, contract) ) else fail (No_such_entrypoint entrypoint) | None -> ( @@ -5255,7 +5256,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra >>? fun (entrypoint_arg, ctxt) -> entrypoint_arg >|? fun (entrypoint, arg) -> let contract : arg typed_contract = - (arg, (contract, entrypoint)) + (arg, {contract; entrypoint}) in (ctxt, contract) )) @@ -5405,7 +5406,7 @@ let parse_contract_for_script : match eq_ty with | Ok (Eq, _ty) -> let contract : arg typed_contract = - (arg, (contract, entrypoint)) + (arg, {contract; entrypoint}) in (ctxt, Some contract) | Error Inconsistent_types_fast -> (ctxt, None) ) @@ -5451,7 +5452,7 @@ let parse_contract_for_script : match entrypoint_arg with | Ok (entrypoint, arg) -> let contract : arg typed_contract = - (arg, (contract, entrypoint)) + (arg, {contract; entrypoint}) in (ctxt, Some contract) | Error Inconsistent_types_fast -> (ctxt, None))) )) @@ -5800,12 +5801,13 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data : (* ideally we would like to allow a little overhead here because it is only used for unparsing *) opened_ticket_type loc t >>?= fun opened_ticket_ty -> let t = ty_of_comparable_ty opened_ticket_ty in + let addr = {contract = ticketer; entrypoint = Entrypoint.default} in (unparse_data [@tailcall]) ctxt ~stack_depth mode t - ((ticketer, Entrypoint.default), (contents, amount)) + (addr, (contents, amount)) | (Set_t (t, _), set) -> List.fold_left_es (fun (l, ctxt) item -> diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 788c4789bb6d..1a31aaa41a1b 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -63,7 +63,7 @@ type step_constants = { type never = | -type address = Contract.t * Entrypoint.t +type address = {contract : Contract.t; entrypoint : Entrypoint.t} type ('a, 'b) pair = 'a * 'b diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index c1e55c91ae4f..14db2ea40cf5 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -44,7 +44,7 @@ type step_constants = { type never = | -type address = Contract.t * Entrypoint.t +type address = {contract : Contract.t; entrypoint : Entrypoint.t} type ('a, 'b) pair = 'a * 'b 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 bcb1ca429426..5c6104f80c31 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -137,8 +137,10 @@ let timestamp_size x = Script_timestamp.to_zint x |> z_size let contract_size = Contract.in_memory_size -let address_size ((c, s) : address) = - h2w +! contract_size c +! Entrypoint.in_memory_size s +let address_size addr = + h2w + +! contract_size addr.contract + +! Entrypoint.in_memory_size addr.entrypoint let view_signature_size (View_signature {name; input_ty; output_ty}) = ret_adding diff --git a/src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_machine.ml b/src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_machine.ml index 00561546aac2..68b417ed27e2 100644 --- a/src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_machine.ml +++ b/src/proto_alpha/lib_protocol/test/helpers/liquidity_baking_machine.ml @@ -737,7 +737,7 @@ module ConcreteBaseMachine : Lqt_fa12_repr.Storage.getBalance_opt (B blk) ~contract:env.tzbtc_contract - (contract, Entrypoint.default) + {contract; entrypoint = Entrypoint.default} >>=? fun mamount -> pure (Option.value (Option.map Z.to_int mamount) ~default:0) @@ -745,7 +745,7 @@ module ConcreteBaseMachine : Lqt_fa12_repr.Storage.getBalance_opt (B blk) ~contract:env.liquidity_contract - (contract, Entrypoint.default) + {contract; entrypoint = Entrypoint.default} >>=? fun mamount -> pure (Option.value (Option.map Z.to_int mamount) ~default:0) diff --git a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml index 3718c81602e9..e4e7081e7cbb 100644 --- a/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml +++ b/src/proto_alpha/lib_protocol/test/integration/michelson/test_typechecking.ml @@ -707,7 +707,7 @@ let test_parse_address () = ctxt (address_t ~annot:None) (String (-1, "KT1FAKEFAKEFAKEFAKEFAKEFAKEFAKGGSE2x%")) - (kt1fake, Entrypoint.default) + {contract = kt1fake; entrypoint = Entrypoint.default} >>=? fun ctxt -> (* tz1% (empty entrypoint) *) wrap_error_lwt @@ -718,7 +718,7 @@ let test_parse_address () = ctxt (address_t ~annot:None) (String (-1, "tz1fakefakefakefakefakefakefakcphLA5%")) - (tz1fake, Entrypoint.default) + {contract = tz1fake; entrypoint = Entrypoint.default} >|=? fun _ctxt -> () let test_unparse_data loc ctxt ty x ~expected_readable ~expected_optimized = diff --git a/src/proto_alpha/lib_protocol/ticket_balance_key.ml b/src/proto_alpha/lib_protocol/ticket_balance_key.ml index 1011c9a0824f..e38d1e013466 100644 --- a/src/proto_alpha/lib_protocol/ticket_balance_key.ml +++ b/src/proto_alpha/lib_protocol/ticket_balance_key.ml @@ -44,8 +44,12 @@ let ticket_balance_key ctxt ~owner Gas.consume ctxt (Script.strip_annotations_cost cont_ty_unstripped) >>?= fun ctxt -> let typ = Script.strip_annotations cont_ty_unstripped in - let ticketer_address = (ticketer, Entrypoint.default) in - let owner_address = (owner, Entrypoint.default) in + let ticketer_address = + Script_typed_ir.{contract = ticketer; entrypoint = Entrypoint.default} + in + let owner_address = + Script_typed_ir.{contract = owner; entrypoint = Entrypoint.default} + in let address_t = Script_typed_ir.address_t ~annot:None in Script_ir_translator.unparse_data ctxt -- GitLab From 3661f865b1d295732301975664e94873f56f1528 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 5 Jan 2022 23:58:46 +0100 Subject: [PATCH 06/19] Proto/Michelson: make Script_typed_ir.typed_contract unique. --- .../lib_benchmark/michelson_samplers.ml | 2 +- .../lib_protocol/script_interpreter.ml | 17 +++++------ .../lib_protocol/script_ir_translator.ml | 28 ++++++++----------- .../lib_protocol/script_typed_ir.ml | 2 +- .../lib_protocol/script_typed_ir.mli | 2 +- .../lib_protocol/script_typed_ir_size.ml | 2 +- 6 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index b0893a438ad2..baf71242d102 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -666,7 +666,7 @@ end) fun arg_ty -> let open M in let* address = value (address_t ~annot:None) in - return (arg_ty, address) + return {arg_ty; address} and generate_operation : (Alpha_context.packed_internal_operation diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index c33a8add5541..1ec094c4dcb0 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -983,8 +983,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = >>=? fun (opt, ctxt, gas) -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks opt stack | IAddress (_, k) -> - let (_, address) = accu in - (step [@ocaml.tailcall]) g gas k ks address stack + (step [@ocaml.tailcall]) g gas k ks accu.address stack | IContract (kinfo, t, entrypoint, k) -> ( let addr = accu in let entrypoint_opt = @@ -1009,17 +1008,19 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) | ITransfer_tokens (_, k) -> let p = accu in - let (amount, ((tp, addr_dst), stack)) = stack in - let destination = addr_dst.contract in - let entrypoint = addr_dst.entrypoint in + let (amount, (tcontract, stack)) = stack in + let tp = tcontract.arg_ty in + let destination = tcontract.address.contract in + let entrypoint = tcontract.address.entrypoint in transfer (ctxt, sc) gas amount tp p destination entrypoint >>=? fun (accu, ctxt, gas) -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks accu stack | IImplicit_account (_, k) -> let key = accu in + let arg_ty = unit_t ~annot:None in let contract = Contract.implicit_contract key in - let entrypoint = Entrypoint.default in - let res = (unit_t ~annot:None, {contract; entrypoint}) in + let address = {contract; entrypoint = Entrypoint.default} in + let res = {arg_ty; address} in (step [@ocaml.tailcall]) g gas k ks res stack | IView (_, View_signature {name; input_ty; output_ty}, k) -> ( let input = accu in @@ -1196,7 +1197,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = let res = {contract = sc.source; entrypoint = Entrypoint.default} in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | ISelf (_, ty, entrypoint, k) -> - let res = (ty, {contract = sc.self; entrypoint}) in + let res = {arg_ty = ty; address = {contract = sc.self; entrypoint}} in (step [@ocaml.tailcall]) g gas k ks res (accu, stack) | ISelf_address (_, k) -> let res = {contract = sc.self; entrypoint = Entrypoint.default} in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 9d8a0e040e77..d1b42cf63039 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -481,7 +481,7 @@ let unparse_address ~loc ctxt mode {contract; entrypoint} = in (String (loc, notation), ctxt) -let unparse_contract ~loc ctxt mode (_, address) = +let unparse_contract ~loc ctxt mode {arg_ty = _; address} = unparse_address ~loc ctxt mode address let unparse_signature ~loc ctxt mode s = @@ -2591,7 +2591,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : Lwt.return @@ traced_no_lwt @@ parse_chain_id ctxt expr | (Address_t _, expr) -> Lwt.return @@ traced_no_lwt @@ parse_address ctxt expr - | (Contract_t (ty, _), expr) -> + | (Contract_t (arg_ty, _), expr) -> traced ( parse_address ctxt expr >>?= fun (address, ctxt) -> let loc = location expr in @@ -2600,10 +2600,10 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : ~legacy ctxt loc - ty + arg_ty address.contract ~entrypoint:address.entrypoint - >|=? fun (ctxt, _) -> ((ty, address), ctxt) ) + >|=? fun (ctxt, _) -> ({arg_ty; address}, ctxt) ) (* Pairs *) | (Pair_t ((tl, _, _), (tr, _, _), _), expr) -> let r_witness = comb_witness1 tr in @@ -5217,8 +5217,7 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra Lwt.return ( ty_eq ~legacy:true ctxt loc arg (unit_t ~annot:None) >|? fun (Eq, ctxt) -> - let contract : arg typed_contract = (arg, {contract; entrypoint}) in - (ctxt, contract) ) + (ctxt, {arg_ty = arg; address = {contract; entrypoint}}) ) else fail (No_such_entrypoint entrypoint) | None -> ( (* Originated account *) @@ -5254,11 +5253,8 @@ and[@coq_axiom_with_reason "complex mutually recursive definition"] parse_contra entrypoint loc >>? fun (entrypoint_arg, ctxt) -> - entrypoint_arg >|? fun (entrypoint, arg) -> - let contract : arg typed_contract = - (arg, {contract; entrypoint}) - in - (ctxt, contract) )) + entrypoint_arg >|? fun (entrypoint, arg_ty) -> + (ctxt, {arg_ty; address = {contract; entrypoint}}) )) and parse_view_name ctxt : Script.node -> (Script_string.t * context) tzresult = function @@ -5405,8 +5401,8 @@ let parse_contract_for_script : >|? fun (eq_ty, ctxt) -> match eq_ty with | Ok (Eq, _ty) -> - let contract : arg typed_contract = - (arg, {contract; entrypoint}) + let contract = + {arg_ty = arg; address = {contract; entrypoint}} in (ctxt, Some contract) | Error Inconsistent_types_fast -> (ctxt, None) ) @@ -5450,9 +5446,9 @@ let parse_contract_for_script : loc >|? fun (entrypoint_arg, ctxt) -> match entrypoint_arg with - | Ok (entrypoint, arg) -> - let contract : arg typed_contract = - (arg, {contract; entrypoint}) + | Ok (entrypoint, arg_ty) -> + let contract = + {arg_ty; address = {contract; entrypoint}} in (ctxt, Some contract) | Error Inconsistent_types_fast -> (ctxt, None))) )) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 1a31aaa41a1b..0186df3a5ecd 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -1046,7 +1046,7 @@ and ('arg, 'ret) lambda = -> ('arg, 'ret) lambda [@@coq_force_gadt] -and 'arg typed_contract = 'arg ty * address +and 'arg typed_contract = {arg_ty : 'arg ty; address : address} and (_, _, _, _) continuation = | KNil : ('r, 'f, 'r, 'f) continuation diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 14db2ea40cf5..60ce3e22d3ef 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -1057,7 +1057,7 @@ and ('arg, 'ret) lambda = -> ('arg, 'ret) lambda [@@coq_force_gadt] -and 'arg typed_contract = 'arg ty * address +and 'arg typed_contract = {arg_ty : 'arg ty; address : address} (* 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 5c6104f80c31..5bc3c2aa999a 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -168,7 +168,7 @@ let comb_set_gadt_witness_size = peano_shape_proof let dup_n_gadt_witness_size = peano_shape_proof -let contract_size (arg_ty, address) = +let contract_size {arg_ty; address} = ret_adding (ty_size arg_ty) (h2w +! address_size address) let sapling_state_size {Sapling.id; diff; memo_size = _} = -- GitLab From 19ad1adf96f5d99fb95a6739fd51d3435aaeac47 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Thu, 6 Jan 2022 00:20:14 +0100 Subject: [PATCH 07/19] Proto/Michelson: make Script_typed_ir.operation unique. --- src/proto_alpha/lib_benchmark/michelson_samplers.ml | 7 ++----- src/proto_alpha/lib_protocol/script_interpreter.ml | 10 ++++++---- .../lib_protocol/script_interpreter_defs.ml | 7 +++---- src/proto_alpha/lib_protocol/script_ir_translator.ml | 4 ++-- src/proto_alpha/lib_protocol/script_typed_ir.ml | 5 ++++- src/proto_alpha/lib_protocol/script_typed_ir.mli | 5 ++++- src/proto_alpha/lib_protocol/script_typed_ir_size.ml | 9 +++------ 7 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index baf71242d102..90b87f92dd0a 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -668,13 +668,10 @@ end) let* address = value (address_t ~annot:None) in return {arg_ty; address} - and generate_operation : - (Alpha_context.packed_internal_operation - * Alpha_context.Lazy_storage.diffs option) - sampler = + and generate_operation : Script_typed_ir.operation sampler = fun rng_state -> let transfer = generate_transfer_tokens rng_state in - (transfer, None) + Script_typed_ir.{piop = transfer; lazy_storage_diff = None} and generate_transfer_tokens : Alpha_context.packed_internal_operation sampler = diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 1ec094c4dcb0..3f10f486a82b 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1155,9 +1155,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = let operation = Delegation delegate in let ctxt = update_context gas ctxt in fresh_internal_nonce ctxt >>?= fun (ctxt, nonce) -> - let res = - (Internal_operation {source = sc.self; operation; nonce}, None) - in + let piop = Internal_operation {source = sc.self; operation; nonce} in + let res = {piop; lazy_storage_diff = None} in let gas = update_local_gas_counter ctxt in let ctxt = outdated ctxt in (step [@ocaml.tailcall]) (ctxt, sc) gas k ks res stack @@ -1732,7 +1731,10 @@ let execute logger ctxt mode step_constants ~entrypoint ~internal ) >>=? fun (unparsed_storage, ctxt) -> Lwt.return - (let (ops, op_diffs) = List.split ops.elements in + (let op_to_couple op = (op.piop, op.lazy_storage_diff) in + let (ops, op_diffs) = + ops.elements |> List.map op_to_couple |> List.split + in let lazy_storage_diff = match List.flatten diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml index 1b9c2a9ed962..53e8eb21a35a 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml @@ -524,7 +524,7 @@ let transfer (ctxt, sc) gas amount tp p destination entrypoint = in fresh_internal_nonce ctxt >>?= fun (ctxt, nonce) -> let iop = {source = sc.self; operation; nonce} in - let res = (Internal_operation iop, lazy_storage_diff) in + let res = {piop = Internal_operation iop; lazy_storage_diff} in let gas = update_local_gas_counter ctxt in let ctxt = outdated ctxt in return (res, ctxt, gas) @@ -599,9 +599,8 @@ let create_contract (ctxt, sc) gas storage_type param_type code views root_name } in fresh_internal_nonce ctxt >>?= fun (ctxt, nonce) -> - let res = - (Internal_operation {source = sc.self; operation; nonce}, lazy_storage_diff) - in + let piop = Internal_operation {source = sc.self; operation; nonce} in + let res = {piop; lazy_storage_diff} in let gas = update_local_gas_counter ctxt in let ctxt = outdated ctxt in return (res, contract, ctxt, gas) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index d1b42cf63039..91f9c3372f9f 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -520,9 +520,9 @@ let unparse_key_hash ~loc ctxt mode k = Gas.consume ctxt Unparse_costs.key_hash_readable >|? fun ctxt -> (String (loc, Signature.Public_key_hash.to_b58check k), ctxt) -let unparse_operation ~loc ctxt (op, _big_map_diff) = +let unparse_operation ~loc ctxt {piop; lazy_storage_diff = _} = let bytes = - Data_encoding.Binary.to_bytes_exn Operation.internal_operation_encoding op + Data_encoding.Binary.to_bytes_exn Operation.internal_operation_encoding piop in Gas.consume ctxt (Unparse_costs.operation bytes) >|? fun ctxt -> (Bytes (loc, bytes), ctxt) diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 0186df3a5ecd..5a1d83554831 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -69,7 +69,10 @@ type ('a, 'b) pair = 'a * 'b type ('a, 'b) union = L of 'a | R of 'b -type operation = packed_internal_operation * Lazy_storage.diffs option +type operation = { + piop : packed_internal_operation; + lazy_storage_diff : Lazy_storage.diffs option; +} type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 60ce3e22d3ef..7904eb24e35c 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -50,7 +50,10 @@ type ('a, 'b) pair = 'a * 'b type ('a, 'b) union = L of 'a | R of 'b -type operation = packed_internal_operation * Lazy_storage.diffs option +type operation = { + piop : packed_internal_operation; + lazy_storage_diff : Lazy_storage.diffs option; +} type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} 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 5bc3c2aa999a..8e707e20bf2e 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -177,13 +177,10 @@ let sapling_state_size {Sapling.id; diff; memo_size = _} = +! Sapling.diff_in_memory_size diff +! sapling_memo_size_size -let operation_size - (operation : - packed_internal_operation * Lazy_storage.diffs_item list option) = - let (poi, diffs) = operation in +let operation_size {piop; lazy_storage_diff} = ret_adding - (Operation.packed_internal_operation_in_memory_size poi - ++ option_size_vec Lazy_storage.diffs_in_memory_size diffs) + (Operation.packed_internal_operation_in_memory_size piop + ++ option_size_vec Lazy_storage.diffs_in_memory_size lazy_storage_diff) h2w let chain_id_size = h1w +? Chain_id.size -- GitLab From 46b8e00e2c57b8fa7b9bc765f06cf2625198551c Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 14 Dec 2021 17:34:58 +0100 Subject: [PATCH 08/19] Proto/Michelson: make Script_typed_ir.Script_chain_id.t algebraic. --- .../lib_benchmark/michelson_samplers.ml | 2 +- src/proto_alpha/lib_benchmarks_proto/size.ml | 3 +- .../lib_protocol/script_comparable.ml | 3 +- .../lib_protocol/script_interpreter.ml | 6 ++-- .../lib_protocol/script_ir_translator.ml | 14 +++++---- .../lib_protocol/script_typed_ir.ml | 25 ++++++++++++++-- .../lib_protocol/script_typed_ir.mli | 30 +++++++++++++++---- .../test/pbt/test_script_comparison.ml | 2 +- 8 files changed, 65 insertions(+), 20 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index 90b87f92dd0a..f4c592d9096d 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -513,7 +513,7 @@ end) let chain_id rng_state = let string = Base_samplers.uniform_string ~nbytes:4 rng_state in - Data_encoding.Binary.of_string_exn Chain_id.encoding string + Data_encoding.Binary.of_string_exn Script_chain_id.encoding string let rec value : type a. a Script_typed_ir.ty -> a sampler = let open Script_typed_ir in diff --git a/src/proto_alpha/lib_benchmarks_proto/size.ml b/src/proto_alpha/lib_benchmarks_proto/size.ml index e6b8431dfe25..2420c0a3875f 100644 --- a/src/proto_alpha/lib_benchmarks_proto/size.ml +++ b/src/proto_alpha/lib_benchmarks_proto/size.ml @@ -136,7 +136,8 @@ let key_hash (_keyhash : Signature.public_key_hash) : t = let public_key (public_key : Signature.public_key) : t = Signature.Public_key.size public_key -let chain_id (_chain_id : Chain_id.t) : t = Chain_id.size +let chain_id (_chain_id : Script_typed_ir.Script_chain_id.t) : t = + Script_typed_ir.Script_chain_id.size let address (addr : Script_typed_ir.address) : t = let entrypoint = addr.entrypoint in diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml index 79a947cd2b1e..ce9ca359b481 100644 --- a/src/proto_alpha/lib_protocol/script_comparable.ml +++ b/src/proto_alpha/lib_protocol/script_comparable.ml @@ -61,7 +61,8 @@ let compare_comparable : type a. a comparable_ty -> a -> a -> int = (apply [@tailcall]) (Script_timestamp.compare x y) k | (Address_key _, x, y) -> (apply [@tailcall]) (compare_address x y) k | (Bytes_key _, x, y) -> (apply [@tailcall]) (Compare.Bytes.compare x y) k - | (Chain_id_key _, x, y) -> (apply [@tailcall]) (Chain_id.compare x y) k + | (Chain_id_key _, x, y) -> + (apply [@tailcall]) (Script_chain_id.compare x y) k | (Pair_key ((tl, _), (tr, _), _), (lx, rx), (ly, ry)) -> (compare_comparable [@tailcall]) tl diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 3f10f486a82b..0f8363ea7259 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1255,7 +1255,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = let transaction = accu in let (state, stack) = stack in let address = Contract.to_b58check sc.self in - let chain_id = Chain_id.to_b58check sc.chain_id in + let sc_chain_id = Script_chain_id.make sc.chain_id in + let chain_id = Script_chain_id.to_b58check sc_chain_id in let anti_replay = address ^ chain_id in let ctxt = update_context gas ctxt in Sapling.verify_update ctxt state transaction anti_replay @@ -1268,7 +1269,8 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) (ctxt, sc) gas k ks state stack | None -> (step [@ocaml.tailcall]) (ctxt, sc) gas k ks None stack) | IChainId (_, k) -> - let accu = sc.chain_id and stack = (accu, stack) in + let accu = Script_chain_id.make sc.chain_id + and stack = (accu, stack) in (step [@ocaml.tailcall]) g gas k ks accu stack | INever _ -> ( match accu with _ -> .) | IVoting_power (_, k) -> diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 91f9c3372f9f..8685bffdb5dd 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -532,12 +532,12 @@ let unparse_chain_id ~loc ctxt mode chain_id = | Optimized | Optimized_legacy -> Gas.consume ctxt Unparse_costs.chain_id_optimized >|? fun ctxt -> let bytes = - Data_encoding.Binary.to_bytes_exn Chain_id.encoding chain_id + Data_encoding.Binary.to_bytes_exn Script_chain_id.encoding chain_id in (Bytes (loc, bytes), ctxt) | Readable -> Gas.consume ctxt Unparse_costs.chain_id_readable >|? fun ctxt -> - (String (loc, Chain_id.to_b58check chain_id), ctxt) + (String (loc, Script_chain_id.to_b58check chain_id), ctxt) let unparse_bls12_381_g1 ~loc ctxt x = Gas.consume ctxt Unparse_costs.bls12_381_g1 >|? fun ctxt -> @@ -2224,11 +2224,13 @@ let parse_signature ctxt : Script.node -> (signature * context) tzresult = | expr -> error @@ Invalid_kind (location expr, [String_kind; Bytes_kind], kind expr) -let parse_chain_id ctxt : Script.node -> (Chain_id.t * context) tzresult = - function +let parse_chain_id ctxt : Script.node -> (Script_chain_id.t * context) tzresult + = function | Bytes (loc, bytes) as expr -> ( Gas.consume ctxt Typecheck_costs.chain_id_optimized >>? fun ctxt -> - match Data_encoding.Binary.of_bytes_opt Chain_id.encoding bytes with + match + Data_encoding.Binary.of_bytes_opt Script_chain_id.encoding bytes + with | Some k -> ok (k, ctxt) | None -> error @@ -2236,7 +2238,7 @@ let parse_chain_id ctxt : Script.node -> (Chain_id.t * context) tzresult = (loc, strip_locations expr, "a valid chain id")) | String (loc, s) as expr -> ( Gas.consume ctxt Typecheck_costs.chain_id_readable >>? fun ctxt -> - match Chain_id.of_b58check_opt s with + match Script_chain_id.of_b58check_opt s with | Some s -> ok (s, ctxt) | None -> error diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 5a1d83554831..3c48a10b7fa0 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -74,6 +74,23 @@ type operation = { lazy_storage_diff : Lazy_storage.diffs option; } +module Script_chain_id = struct + type t = Chain_id_tag of Chain_id.t [@@ocaml.unboxed] + + let make x = Chain_id_tag x + + let compare (Chain_id_tag x) (Chain_id_tag y) = Chain_id.compare x y + + let size = Chain_id.size + + let encoding = + Data_encoding.conv (fun (Chain_id_tag x) -> x) make Chain_id.encoding + + let to_b58check (Chain_id_tag x) = Chain_id.to_b58check x + + let of_b58check_opt x = Option.map make (Chain_id.of_b58check_opt x) +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} module type TYPE_SIZE = sig @@ -184,7 +201,9 @@ type _ comparable_ty = | Timestamp_key : Script_timestamp.t ty_metadata -> Script_timestamp.t comparable_ty - | Chain_id_key : Chain_id.t ty_metadata -> Chain_id.t comparable_ty + | Chain_id_key : + Script_chain_id.t ty_metadata + -> Script_chain_id.t comparable_ty | Address_key : address ty_metadata -> address comparable_ty | Pair_key : ('a comparable_ty * field_annot option) @@ -919,7 +938,7 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('b, 'u, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr | IChainId : - ('a, 's) kinfo * (Chain_id.t, 'a * 's, 'r, 'f) kinstr + ('a, 's) kinfo * (Script_chain_id.t, 'a * 's, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr | INever : (never, 's) kinfo -> (never, 's, 'r, 'f) kinstr | IVoting_power : @@ -1172,7 +1191,7 @@ and 'ty ty = Sapling.Memo_size.t * Sapling.state ty_metadata -> Sapling.state ty | Operation_t : operation ty_metadata -> operation ty - | Chain_id_t : Chain_id.t ty_metadata -> Chain_id.t ty + | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 7904eb24e35c..a59fb4559180 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -55,6 +55,24 @@ type operation = { lazy_storage_diff : Lazy_storage.diffs option; } +module Script_chain_id : sig + (** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type t = Chain_id_tag of Chain_id.t [@@ocaml.unboxed] + + val make : Chain_id.t -> t + + val compare : t -> t -> int + + val size : int + + val encoding : t Data_encoding.t + + val to_b58check : t -> string + + val of_b58check_opt : string -> t option +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} type empty_cell = EmptyCell @@ -90,7 +108,9 @@ type _ comparable_ty = | Timestamp_key : Script_timestamp.t ty_metadata -> Script_timestamp.t comparable_ty - | Chain_id_key : Chain_id.t ty_metadata -> Chain_id.t comparable_ty + | Chain_id_key : + Script_chain_id.t ty_metadata + -> Script_chain_id.t comparable_ty | Address_key : address ty_metadata -> address comparable_ty | Pair_key : ('a comparable_ty * field_annot option) @@ -130,7 +150,7 @@ val key_key : annot:type_annot option -> public_key comparable_ty val timestamp_key : annot:type_annot option -> Script_timestamp.t comparable_ty -val chain_id_key : annot:type_annot option -> Chain_id.t comparable_ty +val chain_id_key : annot:type_annot option -> Script_chain_id.t comparable_ty val address_key : annot:type_annot option -> address comparable_ty @@ -926,7 +946,7 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('b, 'u, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr | IChainId : - ('a, 's) kinfo * (Chain_id.t, 'a * 's, 'r, 'f) kinstr + ('a, 's) kinfo * (Script_chain_id.t, 'a * 's, 'r, 'f) kinstr -> ('a, 's, 'r, 'f) kinstr | INever : (never, 's) kinfo -> (never, 's, 'r, 'f) kinstr | IVoting_power : @@ -1279,7 +1299,7 @@ and 'ty ty = Sapling.Memo_size.t * Sapling.state ty_metadata -> Sapling.state ty | Operation_t : operation ty_metadata -> operation ty - | Chain_id_t : Chain_id.t ty_metadata -> Chain_id.t ty + | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty @@ -1528,7 +1548,7 @@ val sapling_state_t : val operation_t : annot:type_annot option -> operation ty -val chain_id_t : annot:type_annot option -> Chain_id.t ty +val chain_id_t : annot:type_annot option -> Script_chain_id.t ty val never_t : annot:type_annot option -> never ty 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 b5b4471f748b..6a0012dfbbda 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 @@ -65,7 +65,7 @@ let rec reference_compare_comparable : type a. a comparable_ty -> a -> a -> int | (Address_key _, x, y) -> normalize_compare @@ Script_comparable.compare_address x y | (Bytes_key _, x, y) -> normalize_compare @@ Compare.Bytes.compare x y - | (Chain_id_key _, x, y) -> normalize_compare @@ Chain_id.compare x y + | (Chain_id_key _, x, y) -> normalize_compare @@ Script_chain_id.compare x y | (Pair_key ((tl, _), (tr, _), _), (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 -- GitLab From 958a973202c9b3a2bc4ac0dedb11e3f0f12742ef Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 15 Dec 2021 10:04:04 +0100 Subject: [PATCH 09/19] Proto/Michelson: make Script_typed_ir.Script_bls.Fr.t algebraic. --- .../lib_benchmark/michelson_samplers.ml | 4 +- .../lib_protocol/script_interpreter.ml | 16 ++-- .../lib_protocol/script_ir_translator.ml | 6 +- .../lib_protocol/script_typed_ir.ml | 78 ++++++++++++++----- .../lib_protocol/script_typed_ir.mli | 72 ++++++++++++----- 5 files changed, 124 insertions(+), 52 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index f4c592d9096d..2b7d5bd22dd9 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -691,10 +691,10 @@ end) | Some x -> x | None -> assert false - and generate_bls12_381_fr : Environment.Bls12_381.Fr.t sampler = + and generate_bls12_381_fr : Script_bls.Fr.t sampler = fun rng_state -> let b = Bls12_381.Fr.(to_bytes (random ~state:rng_state ())) in - match Environment.Bls12_381.Fr.of_bytes_opt b with + match Script_bls.Fr.of_bytes_opt b with | Some x -> x | None -> assert false diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 0f8363ea7259..dfdf6990cf4c 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1307,7 +1307,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IAdd_bls12_381_fr (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.Fr.add x y in + let accu = Script_bls.Fr.add x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_g1 (_, k) -> let x = accu and (y, stack) = stack in @@ -1319,21 +1319,21 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_fr (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.Fr.mul x y in + let accu = Script_bls.Fr.mul x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_fr_z (_, k) -> let x = accu and (y, stack) = stack in - let x = Bls12_381.Fr.of_z (Script_int.to_zint x) in - let res = Bls12_381.Fr.mul x y in + let x = Script_bls.Fr.of_z (Script_int.to_zint x) in + let res = Script_bls.Fr.mul x y in (step [@ocaml.tailcall]) g gas k ks res stack | IMul_bls12_381_z_fr (_, k) -> let y = accu and (x, stack) = stack in - let x = Bls12_381.Fr.of_z (Script_int.to_zint x) in - let res = Bls12_381.Fr.mul x y in + let x = Script_bls.Fr.of_z (Script_int.to_zint x) in + let res = Script_bls.Fr.mul x y in (step [@ocaml.tailcall]) g gas k ks res stack | IInt_bls12_381_fr (_, k) -> let x = accu in - let res = Script_int.of_zint (Bls12_381.Fr.to_z x) in + let res = Script_int.of_zint (Script_bls.Fr.to_z x) in (step [@ocaml.tailcall]) g gas k ks res stack | INeg_bls12_381_g1 (_, k) -> let x = accu in @@ -1345,7 +1345,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | INeg_bls12_381_fr (_, k) -> let x = accu in - let accu = Bls12_381.Fr.negate x in + let accu = Script_bls.Fr.negate x in (step [@ocaml.tailcall]) g gas k ks accu stack | IPairing_check_bls12_381 (_, k) -> let pairs = accu in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 8685bffdb5dd..f7f31b61ea5a 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -551,7 +551,7 @@ let unparse_bls12_381_g2 ~loc ctxt x = let unparse_bls12_381_fr ~loc ctxt x = Gas.consume ctxt Unparse_costs.bls12_381_fr >|? fun ctxt -> - let bytes = Bls12_381.Fr.to_bytes x in + let bytes = Script_bls.Fr.to_bytes x in (Bytes (loc, bytes), ctxt) let unparse_with_data_encoding ~loc ctxt s unparse_cost encoding = @@ -2767,12 +2767,12 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr)) | (Bls12_381_fr_t _, Bytes (_, bs)) -> ( Gas.consume ctxt Typecheck_costs.bls12_381_fr >>?= fun ctxt -> - match Bls12_381.Fr.of_bytes_opt bs with + match Script_bls.Fr.of_bytes_opt bs with | Some pt -> return (pt, ctxt) | None -> fail_parse_data ()) | (Bls12_381_fr_t _, Int (_, v)) -> Gas.consume ctxt Typecheck_costs.bls12_381_fr >>?= fun ctxt -> - return (Bls12_381.Fr.of_z v, ctxt) + return (Script_bls.Fr.of_z v, ctxt) | (Bls12_381_fr_t _, expr) -> traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr)) (* diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 3c48a10b7fa0..0ec25207a20f 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -91,6 +91,44 @@ module Script_chain_id = struct let of_b58check_opt x = Option.map make (Chain_id.of_b58check_opt x) end +module Script_bls = struct + module type S = sig + type t + + type fr + + val add : t -> t -> t + + val mul : t -> fr -> t + + val negate : t -> t + + val of_bytes_opt : Bytes.t -> t option + + val to_bytes : t -> Bytes.t + end + + module Fr = struct + type t = Fr_tag of Bls12_381.Fr.t [@@ocaml.unboxed] + + open Bls12_381.Fr + + let add (Fr_tag x) (Fr_tag y) = Fr_tag (add x y) + + let mul (Fr_tag x) (Fr_tag y) = Fr_tag (mul x y) + + let negate (Fr_tag x) = Fr_tag (negate x) + + let of_bytes_opt bytes = Option.map (fun x -> Fr_tag x) (of_bytes_opt bytes) + + let to_bytes (Fr_tag x) = to_bytes x + + let of_z z = Fr_tag (of_z z) + + let to_z (Fr_tag x) = to_z x + end +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} module type TYPE_SIZE = sig @@ -962,30 +1000,32 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, Bls12_381.G2.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_fr : - (Bls12_381.Fr.t, Bls12_381.Fr.t * 's) kinfo - * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g1 : - (Bls12_381.G1.t, Bls12_381.Fr.t * 's) kinfo + (Bls12_381.G1.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + -> (Bls12_381.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : - (Bls12_381.G2.t, Bls12_381.Fr.t * 's) kinfo + (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + -> (Bls12_381.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_fr : - (Bls12_381.Fr.t, Bls12_381.Fr.t * 's) kinfo - * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_z_fr : - (Bls12_381.Fr.t, 'a num * 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 'a num * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 'a num * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 'a num * 's, 'r, 'f) kinstr | IMul_bls12_381_fr_z : - ('a num, Bls12_381.Fr.t * 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> ('a num, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + ('a num, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> ('a num, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IInt_bls12_381_fr : - (Bls12_381.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g1 : (Bls12_381.G1.t, 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr -> (Bls12_381.G1.t, 's, 'r, 'f) kinstr @@ -993,8 +1033,8 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr | INeg_bls12_381_fr : - (Bls12_381.Fr.t, 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr @@ -1195,7 +1235,7 @@ and 'ty ty = | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty - | Bls12_381_fr_t : Bls12_381.Fr.t ty_metadata -> Bls12_381.Fr.t ty + | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty | Chest_t : Timelock.chest ty_metadata -> Timelock.chest ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index a59fb4559180..69003e448db1 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -73,6 +73,36 @@ module Script_chain_id : sig val of_b58check_opt : string -> t option end +module Script_bls : sig + module type S = sig + type t + + type fr + + val add : t -> t -> t + + val mul : t -> fr -> t + + val negate : t -> t + + val of_bytes_opt : Bytes.t -> t option + + val to_bytes : t -> Bytes.t + end + + module Fr : sig + (** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type t = Fr_tag of Bls12_381.Fr.t [@@ocaml.unboxed] + + include S with type t := t and type fr := t + + val of_z : Z.t -> t + + val to_z : t -> Z.t + end +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} type empty_cell = EmptyCell @@ -970,30 +1000,32 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, Bls12_381.G2.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_fr : - (Bls12_381.Fr.t, Bls12_381.Fr.t * 's) kinfo - * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g1 : - (Bls12_381.G1.t, Bls12_381.Fr.t * 's) kinfo + (Bls12_381.G1.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + -> (Bls12_381.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : - (Bls12_381.G2.t, Bls12_381.Fr.t * 's) kinfo + (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + -> (Bls12_381.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_fr : - (Bls12_381.Fr.t, Bls12_381.Fr.t * 's) kinfo - * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_z_fr : - (Bls12_381.Fr.t, 'a num * 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 'a num * 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 'a num * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 'a num * 's, 'r, 'f) kinstr | IMul_bls12_381_fr_z : - ('a num, Bls12_381.Fr.t * 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> ('a num, Bls12_381.Fr.t * 's, 'r, 'f) kinstr + ('a num, Script_bls.Fr.t * 's) kinfo + * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> ('a num, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IInt_bls12_381_fr : - (Bls12_381.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g1 : (Bls12_381.G1.t, 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr -> (Bls12_381.G1.t, 's, 'r, 'f) kinstr @@ -1001,8 +1033,8 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr | INeg_bls12_381_fr : - (Bls12_381.Fr.t, 's) kinfo * (Bls12_381.Fr.t, 's, 'r, 'f) kinstr - -> (Bls12_381.Fr.t, 's, 'r, 'f) kinstr + (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr + -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr @@ -1303,7 +1335,7 @@ and 'ty ty = | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty - | Bls12_381_fr_t : Bls12_381.Fr.t ty_metadata -> Bls12_381.Fr.t ty + | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty | Chest_t : Timelock.chest ty_metadata -> Timelock.chest ty @@ -1556,7 +1588,7 @@ val bls12_381_g1_t : annot:type_annot option -> Bls12_381.G1.t ty val bls12_381_g2_t : annot:type_annot option -> Bls12_381.G2.t ty -val bls12_381_fr_t : annot:type_annot option -> Bls12_381.Fr.t ty +val bls12_381_fr_t : annot:type_annot option -> Script_bls.Fr.t ty val ticket_t : Script.location -> -- GitLab From 74f99e373f25e6bbe78c184094221ad3e248ad86 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 15 Dec 2021 10:02:48 +0100 Subject: [PATCH 10/19] Proto/Michelson: make Script_typed_ir.Script_bls.G1.t algebraic. --- .../lib_benchmark/michelson_samplers.ml | 4 +- .../lib_protocol/script_interpreter.ml | 6 +-- .../lib_protocol/script_ir_translator.ml | 4 +- .../lib_protocol/script_typed_ir.ml | 38 +++++++++++++------ .../lib_protocol/script_typed_ir.mli | 32 ++++++++++------ 5 files changed, 54 insertions(+), 30 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index 2b7d5bd22dd9..c8ff9dce609f 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -677,10 +677,10 @@ end) Alpha_context.packed_internal_operation sampler = fun _rng_state -> fail_sampling "generate_transfer_tokens: unimplemented" - and generate_bls12_381_g1 : Environment.Bls12_381.G1.t sampler = + and generate_bls12_381_g1 : Script_bls.G1.t sampler = fun rng_state -> let b = Bls12_381.G1.(to_bytes (random ~state:rng_state ())) in - match Environment.Bls12_381.G1.of_bytes_opt b with + match Script_bls.G1.of_bytes_opt b with | Some x -> x | None -> assert false diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index dfdf6990cf4c..3bb257e22d34 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1299,7 +1299,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks hash stack | IAdd_bls12_381_g1 (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.G1.add x y in + let accu = Script_bls.G1.add x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IAdd_bls12_381_g2 (_, k) -> let x = accu and (y, stack) = stack in @@ -1311,7 +1311,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_g1 (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.G1.mul x y in + let accu = Script_bls.G1.mul x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_g2 (_, k) -> let x = accu and (y, stack) = stack in @@ -1337,7 +1337,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks res stack | INeg_bls12_381_g1 (_, k) -> let x = accu in - let accu = Bls12_381.G1.negate x in + let accu = Script_bls.G1.negate x in (step [@ocaml.tailcall]) g gas k ks accu stack | INeg_bls12_381_g2 (_, k) -> let x = accu in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index f7f31b61ea5a..af750a6b5ed9 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -541,7 +541,7 @@ let unparse_chain_id ~loc ctxt mode chain_id = let unparse_bls12_381_g1 ~loc ctxt x = Gas.consume ctxt Unparse_costs.bls12_381_g1 >|? fun ctxt -> - let bytes = Bls12_381.G1.to_bytes x in + let bytes = Script_bls.G1.to_bytes x in (Bytes (loc, bytes), ctxt) let unparse_bls12_381_g2 ~loc ctxt x = @@ -2753,7 +2753,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : (* Bls12_381 types *) | (Bls12_381_g1_t _, Bytes (_, bs)) -> ( Gas.consume ctxt Typecheck_costs.bls12_381_g1 >>?= fun ctxt -> - match Bls12_381.G1.of_bytes_opt bs with + match Script_bls.G1.of_bytes_opt bs with | Some pt -> return (pt, ctxt) | None -> fail_parse_data ()) | (Bls12_381_g1_t _, expr) -> diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 0ec25207a20f..a92ed6ab2d01 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -127,6 +127,22 @@ module Script_bls = struct let to_z (Fr_tag x) = to_z x end + + module G1 = struct + type t = G1_tag of Bls12_381.G1.t [@@ocaml.unboxed] + + open Bls12_381.G1 + + let add (G1_tag x) (G1_tag y) = G1_tag (add x y) + + let mul (G1_tag x) (Fr.Fr_tag y) = G1_tag (mul x y) + + let negate (G1_tag x) = G1_tag (negate x) + + let of_bytes_opt bytes = Option.map (fun x -> G1_tag x) (of_bytes_opt bytes) + + let to_bytes (G1_tag x) = to_bytes x + end end type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} @@ -992,9 +1008,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr -> (bytes, 's, 'r, 'f) kinstr | IAdd_bls12_381_g1 : - (Bls12_381.G1.t, Bls12_381.G1.t * 's) kinfo - * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Bls12_381.G1.t * 's, 'r, 'f) kinstr + (Script_bls.G1.t, Script_bls.G1.t * 's) kinfo + * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, Script_bls.G1.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_g2 : (Bls12_381.G2.t, Bls12_381.G2.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1004,9 +1020,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g1 : - (Bls12_381.G1.t, Script_bls.Fr.t * 's) kinfo - * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.G1.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1027,8 +1043,8 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g1 : - (Bls12_381.G1.t, 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, 's, 'r, 'f) kinstr + (Script_bls.G1.t, 's) kinfo * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g2 : (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1036,9 +1052,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : - ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo + ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr - -> ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr + -> ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr | IComb : ('a, 's) kinfo * int @@ -1233,7 +1249,7 @@ and 'ty ty = | Operation_t : operation ty_metadata -> operation ty | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty - | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty + | Bls12_381_g1_t : Script_bls.G1.t ty_metadata -> Script_bls.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 69003e448db1..bae432ef3dad 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -101,6 +101,14 @@ module Script_bls : sig val to_z : t -> Z.t end + + module G1 : sig + (** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type t = G1_tag of Bls12_381.G1.t [@@ocaml.unboxed] + + include S with type t := t and type fr := Fr.t + end end type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} @@ -992,9 +1000,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (bytes, 's) kinfo * (bytes, 's, 'r, 'f) kinstr -> (bytes, 's, 'r, 'f) kinstr | IAdd_bls12_381_g1 : - (Bls12_381.G1.t, Bls12_381.G1.t * 's) kinfo - * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Bls12_381.G1.t * 's, 'r, 'f) kinstr + (Script_bls.G1.t, Script_bls.G1.t * 's) kinfo + * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, Script_bls.G1.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_g2 : (Bls12_381.G2.t, Bls12_381.G2.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1004,9 +1012,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g1 : - (Bls12_381.G1.t, Script_bls.Fr.t * 's) kinfo - * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.G1.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1027,8 +1035,8 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.Fr.t, 's) kinfo * (z num, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g1 : - (Bls12_381.G1.t, 's) kinfo * (Bls12_381.G1.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G1.t, 's, 'r, 'f) kinstr + (Script_bls.G1.t, 's) kinfo * (Script_bls.G1.t, 's, 'r, 'f) kinstr + -> (Script_bls.G1.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g2 : (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr @@ -1036,9 +1044,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : - ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo + ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr - -> ((Bls12_381.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr + -> ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr | IComb : ('a, 's) kinfo * int @@ -1333,7 +1341,7 @@ and 'ty ty = | Operation_t : operation ty_metadata -> operation ty | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty - | Bls12_381_g1_t : Bls12_381.G1.t ty_metadata -> Bls12_381.G1.t ty + | Bls12_381_g1_t : Script_bls.G1.t ty_metadata -> Script_bls.G1.t ty | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty @@ -1584,7 +1592,7 @@ val chain_id_t : annot:type_annot option -> Script_chain_id.t ty val never_t : annot:type_annot option -> never ty -val bls12_381_g1_t : annot:type_annot option -> Bls12_381.G1.t ty +val bls12_381_g1_t : annot:type_annot option -> Script_bls.G1.t ty val bls12_381_g2_t : annot:type_annot option -> Bls12_381.G2.t ty -- GitLab From 88baacf49855f53d3390209186955009dca3a026 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 15 Dec 2021 00:11:41 +0100 Subject: [PATCH 11/19] Proto/Michelson: make Script_typed_ir.Script_bls.G2.t algebraic. --- .../lib_benchmark/michelson_samplers.ml | 4 +- .../lib_protocol/script_interpreter.ml | 8 ++-- .../lib_protocol/script_ir_translator.ml | 4 +- .../lib_protocol/script_typed_ir.ml | 42 ++++++++++++++----- .../lib_protocol/script_typed_ir.mli | 34 +++++++++------ 5 files changed, 61 insertions(+), 31 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index c8ff9dce609f..b1c7011e647a 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -684,10 +684,10 @@ end) | Some x -> x | None -> assert false - and generate_bls12_381_g2 : Environment.Bls12_381.G2.t sampler = + and generate_bls12_381_g2 : Script_bls.G2.t sampler = fun rng_state -> let b = Bls12_381.G2.(to_bytes (random ~state:rng_state ())) in - match Environment.Bls12_381.G2.of_bytes_opt b with + match Script_bls.G2.of_bytes_opt b with | Some x -> x | None -> assert false diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 3bb257e22d34..315e135b7e1d 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1303,7 +1303,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IAdd_bls12_381_g2 (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.G2.add x y in + let accu = Script_bls.G2.add x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IAdd_bls12_381_fr (_, k) -> let x = accu and (y, stack) = stack in @@ -1315,7 +1315,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_g2 (_, k) -> let x = accu and (y, stack) = stack in - let accu = Bls12_381.G2.mul x y in + let accu = Script_bls.G2.mul x y in (step [@ocaml.tailcall]) g gas k ks accu stack | IMul_bls12_381_fr (_, k) -> let x = accu and (y, stack) = stack in @@ -1341,7 +1341,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | INeg_bls12_381_g2 (_, k) -> let x = accu in - let accu = Bls12_381.G2.negate x in + let accu = Script_bls.G2.negate x in (step [@ocaml.tailcall]) g gas k ks accu stack | INeg_bls12_381_fr (_, k) -> let x = accu in @@ -1349,7 +1349,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = (step [@ocaml.tailcall]) g gas k ks accu stack | IPairing_check_bls12_381 (_, k) -> let pairs = accu in - let check = Bls12_381.pairing_check pairs.elements in + let check = Script_bls.pairing_check pairs.elements in (step [@ocaml.tailcall]) g gas k ks check stack | IComb (_, _, witness, k) -> let rec aux : diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index af750a6b5ed9..c00bfe7ceefb 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -546,7 +546,7 @@ let unparse_bls12_381_g1 ~loc ctxt x = let unparse_bls12_381_g2 ~loc ctxt x = Gas.consume ctxt Unparse_costs.bls12_381_g2 >|? fun ctxt -> - let bytes = Bls12_381.G2.to_bytes x in + let bytes = Script_bls.G2.to_bytes x in (Bytes (loc, bytes), ctxt) let unparse_bls12_381_fr ~loc ctxt x = @@ -2760,7 +2760,7 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : traced_fail (Invalid_kind (location expr, [Bytes_kind], kind expr)) | (Bls12_381_g2_t _, Bytes (_, bs)) -> ( Gas.consume ctxt Typecheck_costs.bls12_381_g2 >>?= fun ctxt -> - match Bls12_381.G2.of_bytes_opt bs with + match Script_bls.G2.of_bytes_opt bs with | Some pt -> return (pt, ctxt) | None -> fail_parse_data ()) | (Bls12_381_g2_t _, expr) -> diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index a92ed6ab2d01..77bd8dd22766 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -143,6 +143,26 @@ module Script_bls = struct let to_bytes (G1_tag x) = to_bytes x end + + module G2 = struct + type t = G2_tag of Bls12_381.G2.t [@@ocaml.unboxed] + + open Bls12_381.G2 + + let add (G2_tag x) (G2_tag y) = G2_tag (add x y) + + let mul (G2_tag x) (Fr.Fr_tag y) = G2_tag (mul x y) + + let negate (G2_tag x) = G2_tag (negate x) + + let of_bytes_opt bytes = Option.map (fun x -> G2_tag x) (of_bytes_opt bytes) + + let to_bytes (G2_tag x) = to_bytes x + end + + let pairing_check l = + let l = List.map (fun (G1.G1_tag x, G2.G2_tag y) -> (x, y)) l in + Bls12_381.pairing_check l end type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} @@ -1012,9 +1032,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, Script_bls.G1.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_g2 : - (Bls12_381.G2.t, Bls12_381.G2.t * 's) kinfo - * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Bls12_381.G2.t * 's, 'r, 'f) kinstr + (Script_bls.G2.t, Script_bls.G2.t * 's) kinfo + * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, Script_bls.G2.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_fr : (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr @@ -1024,9 +1044,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : - (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo - * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.G2.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_fr : (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr @@ -1046,15 +1066,15 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.G1.t, 's) kinfo * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g2 : - (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr + (Script_bls.G2.t, 's) kinfo * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, 's, 'r, 'f) kinstr | INeg_bls12_381_fr : (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : - ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo + ((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr - -> ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr + -> ((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's, 'r, 'f) kinstr | IComb : ('a, 's) kinfo * int @@ -1250,7 +1270,7 @@ and 'ty ty = | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Script_bls.G1.t ty_metadata -> Script_bls.G1.t ty - | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty + | Bls12_381_g2_t : Script_bls.G2.t ty_metadata -> Script_bls.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index bae432ef3dad..d76c7bfe1090 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -109,6 +109,16 @@ module Script_bls : sig include S with type t := t and type fr := Fr.t end + + module G2 : sig + (** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type t = G2_tag of Bls12_381.G2.t [@@ocaml.unboxed] + + include S with type t := t and type fr := Fr.t + end + + val pairing_check : (G1.t * G2.t) list -> bool end type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} @@ -1004,9 +1014,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, Script_bls.G1.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_g2 : - (Bls12_381.G2.t, Bls12_381.G2.t * 's) kinfo - * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Bls12_381.G2.t * 's, 'r, 'f) kinstr + (Script_bls.G2.t, Script_bls.G2.t * 's) kinfo + * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, Script_bls.G2.t * 's, 'r, 'f) kinstr | IAdd_bls12_381_fr : (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr @@ -1016,9 +1026,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_g2 : - (Bls12_381.G2.t, Script_bls.Fr.t * 's) kinfo - * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr + (Script_bls.G2.t, Script_bls.Fr.t * 's) kinfo + * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, Script_bls.Fr.t * 's, 'r, 'f) kinstr | IMul_bls12_381_fr : (Script_bls.Fr.t, Script_bls.Fr.t * 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr @@ -1038,15 +1048,15 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = (Script_bls.G1.t, 's) kinfo * (Script_bls.G1.t, 's, 'r, 'f) kinstr -> (Script_bls.G1.t, 's, 'r, 'f) kinstr | INeg_bls12_381_g2 : - (Bls12_381.G2.t, 's) kinfo * (Bls12_381.G2.t, 's, 'r, 'f) kinstr - -> (Bls12_381.G2.t, 's, 'r, 'f) kinstr + (Script_bls.G2.t, 's) kinfo * (Script_bls.G2.t, 's, 'r, 'f) kinstr + -> (Script_bls.G2.t, 's, 'r, 'f) kinstr | INeg_bls12_381_fr : (Script_bls.Fr.t, 's) kinfo * (Script_bls.Fr.t, 's, 'r, 'f) kinstr -> (Script_bls.Fr.t, 's, 'r, 'f) kinstr | IPairing_check_bls12_381 : - ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's) kinfo + ((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's) kinfo * (bool, 's, 'r, 'f) kinstr - -> ((Script_bls.G1.t, Bls12_381.G2.t) pair boxed_list, 's, 'r, 'f) kinstr + -> ((Script_bls.G1.t, Script_bls.G2.t) pair boxed_list, 's, 'r, 'f) kinstr | IComb : ('a, 's) kinfo * int @@ -1342,7 +1352,7 @@ and 'ty ty = | Chain_id_t : Script_chain_id.t ty_metadata -> Script_chain_id.t ty | Never_t : never ty_metadata -> never ty | Bls12_381_g1_t : Script_bls.G1.t ty_metadata -> Script_bls.G1.t ty - | Bls12_381_g2_t : Bls12_381.G2.t ty_metadata -> Bls12_381.G2.t ty + | Bls12_381_g2_t : Script_bls.G2.t ty_metadata -> Script_bls.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty @@ -1594,7 +1604,7 @@ val never_t : annot:type_annot option -> never ty val bls12_381_g1_t : annot:type_annot option -> Script_bls.G1.t ty -val bls12_381_g2_t : annot:type_annot option -> Bls12_381.G2.t ty +val bls12_381_g2_t : annot:type_annot option -> Script_bls.G2.t ty val bls12_381_fr_t : annot:type_annot option -> Script_bls.Fr.t ty -- GitLab From ef0f939d1dcc68a3384de196f1060b5ab3b8c699 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 15 Dec 2021 13:54:33 +0100 Subject: [PATCH 12/19] Proto/Michelson: make Script_typed_ir.Script_timelock.chest algebraic. --- .../interpreter_benchmarks.ml | 6 +++-- .../interpreter_workload.ml | 2 +- .../lib_protocol/michelson_v1_gas.ml | 4 ++- .../lib_protocol/michelson_v1_gas.mli | 3 ++- .../lib_protocol/script_interpreter.ml | 2 +- .../lib_protocol/script_ir_translator.ml | 9 ++++--- .../lib_protocol/script_typed_ir.ml | 27 ++++++++++++++++--- .../lib_protocol/script_typed_ir.mli | 27 ++++++++++++++++--- .../lib_protocol/script_typed_ir_size.ml | 2 +- 9 files changed, 65 insertions(+), 17 deletions(-) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index e2cc54fa76ca..5a8b322f340d 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -23,6 +23,7 @@ (* *) (*****************************************************************************) +module Timelock_samplers = Timelock open Protocol (* ------------------------------------------------------------------------- *) @@ -2794,6 +2795,7 @@ module Registration_section = struct halt (union bytes bool @$ bot) ) let resulting_stack chest chest_key time = + let chest = Script_timelock.make_chest chest in ( chest_key, ( chest, ( Script_int_repr.is_nat (Script_int_repr.of_int time) @@ -2807,7 +2809,7 @@ module Registration_section = struct ~kinstr ~stack_sampler:(fun _ rng_state () -> let (chest, chest_key) = - Timelock.chest_sampler ~plaintext_size:1 ~time:0 ~rng_state + Timelock_samplers.chest_sampler ~plaintext_size:1 ~time:0 ~rng_state in resulting_stack chest chest_key 0) () @@ -2830,7 +2832,7 @@ module Registration_section = struct in let (chest, chest_key) = - Timelock.chest_sampler ~plaintext_size ~time ~rng_state + Timelock_samplers.chest_sampler ~plaintext_size ~time ~rng_state in resulting_stack chest chest_key time) () diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml index 93a80c06aa08..d01507284385 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml @@ -1432,7 +1432,7 @@ let extract_ir_sized_step : | (IHalt _, _) -> Instructions.halt | (ILog _, _) -> Instructions.log | (IOpen_chest (_, _), (_, (chest, (time, _)))) -> - let plaintext_size = Timelock.get_plaintext_size chest - 1 in + let plaintext_size = Script_timelock.get_plaintext_size chest - 1 in let log_time = Z.log2 Z.(one + Script_int_repr.to_zint time) in Instructions.open_chest log_time plaintext_size diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 6c5e392eb43b..3994f39c4b1a 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -1300,7 +1300,9 @@ module Cost_of = struct (cost_N_ISplit_ticket (int_bytes amount_a) (int_bytes amount_b)) let open_chest ~chest ~time = - let plaintext = Timelock.get_plaintext_size chest in + let plaintext = + Script_typed_ir.Script_timelock.get_plaintext_size chest + in let log_time = Z.log2 Z.(add one time) in atomic_step_cost (cost_N_IOpen_chest ~chest:plaintext ~time:log_time) diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli index bd90bd06db55..bc8316375098 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli @@ -360,7 +360,8 @@ module Cost_of : sig 'a Script_typed_ir.ticket -> Gas.cost - val open_chest : chest:Timelock.chest -> time:Z.t -> Gas.cost + val open_chest : + chest:Script_typed_ir.Script_timelock.chest -> time:Z.t -> Gas.cost module Control : sig val nil : Gas.cost diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 315e135b7e1d..803f7730d885 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1476,7 +1476,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = match Alpha_context.Script_int.to_int time_z with | None -> R false | Some time -> ( - match open_chest chest chest_key ~time with + match Script_timelock.open_chest chest chest_key ~time with | Correct bytes -> L bytes | Bogus_cipher -> R false | Bogus_opening -> R true) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index c00bfe7ceefb..8473e33b31ce 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -2829,7 +2829,9 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : | (Chest_t _, Bytes (_, bytes)) -> ( Gas.consume ctxt (Typecheck_costs.chest ~bytes:(Bytes.length bytes)) >>?= fun ctxt -> - match Data_encoding.Binary.of_bytes_opt Timelock.chest_encoding bytes with + match + Data_encoding.Binary.of_bytes_opt Script_timelock.chest_encoding bytes + with | Some chest -> return (chest, ctxt) | None -> fail_parse_data ()) | (Chest_t _, expr) -> @@ -5906,8 +5908,9 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data : ~loc ctxt s - (Unparse_costs.chest ~plaintext_size:(Timelock.get_plaintext_size s)) - Timelock.chest_encoding + (Unparse_costs.chest + ~plaintext_size:(Script_timelock.get_plaintext_size s)) + Script_timelock.chest_encoding and unparse_items : type k v. diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 77bd8dd22766..6d42b254f3fb 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -165,6 +165,23 @@ module Script_bls = struct Bls12_381.pairing_check l end +module Script_timelock = struct + type chest = Chest_tag of Timelock.chest [@@ocaml.unboxed] + + let make_chest chest = Chest_tag chest + + let chest_encoding = + Data_encoding.conv + (fun (Chest_tag x) -> x) + (fun x -> Chest_tag x) + Timelock.chest_encoding + + let open_chest (Chest_tag chest) chest_key ~time = + Timelock.open_chest chest chest_key ~time + + let get_plaintext_size (Chest_tag x) = Timelock.get_plaintext_size x +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} module type TYPE_SIZE = sig @@ -1122,9 +1139,13 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('a ticket option, 's, 'r, 'f) kinstr -> ('a ticket * 'a ticket, 's, 'r, 'f) kinstr | IOpen_chest : - (Timelock.chest_key, Timelock.chest * (n num * 's)) kinfo + (Timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo * ((bytes, bool) union, 's, 'r, 'f) kinstr - -> (Timelock.chest_key, Timelock.chest * (n num * 's), 'r, 'f) kinstr + -> ( Timelock.chest_key, + Script_timelock.chest * (n num * 's), + 'r, + 'f ) + kinstr (* Internal control instructions ----------------------------- @@ -1274,7 +1295,7 @@ and 'ty ty = | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty - | Chest_t : Timelock.chest ty_metadata -> Timelock.chest ty + | Chest_t : Script_timelock.chest ty_metadata -> Script_timelock.chest ty and ('top_ty, 'resty) stack_ty = | Item_t : 'ty ty * ('ty2, 'rest) stack_ty -> ('ty, 'ty2 * 'rest) stack_ty diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index d76c7bfe1090..edd13a315aca 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -121,6 +121,21 @@ module Script_bls : sig val pairing_check : (G1.t * G2.t) list -> bool end +module Script_timelock : sig + (** [chest] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type chest = Chest_tag of Timelock.chest [@@ocaml.unboxed] + + val make_chest : Timelock.chest -> chest + + val chest_encoding : chest Data_encoding.t + + val open_chest : + chest -> Timelock.chest_key -> time:int -> Timelock.opening_result + + val get_plaintext_size : chest -> int +end + type 'a ticket = {ticketer : Contract.t; contents : 'a; amount : n num} type empty_cell = EmptyCell @@ -1104,9 +1119,13 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('a ticket option, 's, 'r, 'f) kinstr -> ('a ticket * 'a ticket, 's, 'r, 'f) kinstr | IOpen_chest : - (Timelock.chest_key, Timelock.chest * (n num * 's)) kinfo + (Timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo * ((bytes, bool) union, 's, 'r, 'f) kinstr - -> (Timelock.chest_key, Timelock.chest * (n num * 's), 'r, 'f) kinstr + -> ( Timelock.chest_key, + Script_timelock.chest * (n num * 's), + 'r, + 'f ) + kinstr (* Internal control instructions @@ -1356,7 +1375,7 @@ and 'ty ty = | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty - | Chest_t : Timelock.chest ty_metadata -> Timelock.chest ty + | Chest_t : Script_timelock.chest ty_metadata -> Script_timelock.chest ty and ('top_ty, 'resty) stack_ty = | Item_t : 'ty ty * ('ty2, 'rest) stack_ty -> ('ty, 'ty2 * 'rest) stack_ty @@ -1616,7 +1635,7 @@ val ticket_t : val chest_key_t : annot:type_annot option -> Timelock.chest_key ty -val chest_t : annot:type_annot option -> Timelock.chest ty +val chest_t : annot:type_annot option -> Script_timelock.chest 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 8e707e20bf2e..03c36068830f 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -199,7 +199,7 @@ let chest_size chest = *) let locked_value_size = 256 in let rsa_public_size = 256 in - let ciphertext_size = Timelock.get_plaintext_size chest in + let ciphertext_size = Script_timelock.get_plaintext_size chest in h3w +? (locked_value_size + rsa_public_size + ciphertext_size) let chest_key_size _ = -- GitLab From e4a5e46ea3f16d266269af101b965725a0330f07 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Fri, 17 Dec 2021 16:34:57 +0100 Subject: [PATCH 13/19] Proto/Michelson: make Script_typed_ir.Script_timelock.chest_key algebraic. --- .../interpreter_benchmarks.ml | 1 + .../lib_protocol/script_ir_translator.ml | 6 ++++-- .../lib_protocol/script_typed_ir.ml | 20 ++++++++++++++---- .../lib_protocol/script_typed_ir.mli | 21 +++++++++++++------ 4 files changed, 36 insertions(+), 12 deletions(-) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index 5a8b322f340d..c222f4e6007a 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -2796,6 +2796,7 @@ module Registration_section = struct let resulting_stack chest chest_key time = let chest = Script_timelock.make_chest chest in + let chest_key = Script_timelock.make_chest_key chest_key in ( chest_key, ( chest, ( Script_int_repr.is_nat (Script_int_repr.of_int time) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 8473e33b31ce..9d9038219827 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -2820,7 +2820,9 @@ let[@coq_axiom_with_reason "gadt"] rec parse_data : | (Chest_key_t _, Bytes (_, bytes)) -> ( Gas.consume ctxt Typecheck_costs.chest_key >>?= fun ctxt -> match - Data_encoding.Binary.of_bytes_opt Timelock.chest_key_encoding bytes + Data_encoding.Binary.of_bytes_opt + Script_timelock.chest_key_encoding + bytes with | Some chest_key -> return (chest_key, ctxt) | None -> fail_parse_data ()) @@ -5902,7 +5904,7 @@ let[@coq_axiom_with_reason "gadt"] rec unparse_data : ctxt s Unparse_costs.chest_key - Timelock.chest_key_encoding + Script_timelock.chest_key_encoding | (Chest_t _, s) -> unparse_with_data_encoding ~loc diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index 6d42b254f3fb..c6e3668a0163 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -166,6 +166,16 @@ module Script_bls = struct end module Script_timelock = struct + type chest_key = Chest_key_tag of Timelock.chest_key [@@ocaml.unboxed] + + let make_chest_key chest_key = Chest_key_tag chest_key + + let chest_key_encoding = + Data_encoding.conv + (fun (Chest_key_tag x) -> x) + (fun x -> Chest_key_tag x) + Timelock.chest_key_encoding + type chest = Chest_tag of Timelock.chest [@@ocaml.unboxed] let make_chest chest = Chest_tag chest @@ -176,7 +186,7 @@ module Script_timelock = struct (fun x -> Chest_tag x) Timelock.chest_encoding - let open_chest (Chest_tag chest) chest_key ~time = + let open_chest (Chest_tag chest) (Chest_key_tag chest_key) ~time = Timelock.open_chest chest chest_key ~time let get_plaintext_size (Chest_tag x) = Timelock.get_plaintext_size x @@ -1139,9 +1149,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('a ticket option, 's, 'r, 'f) kinstr -> ('a ticket * 'a ticket, 's, 'r, 'f) kinstr | IOpen_chest : - (Timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo + (Script_timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo * ((bytes, bool) union, 's, 'r, 'f) kinstr - -> ( Timelock.chest_key, + -> ( Script_timelock.chest_key, Script_timelock.chest * (n num * 's), 'r, 'f ) @@ -1294,7 +1304,9 @@ and 'ty ty = | Bls12_381_g2_t : Script_bls.G2.t ty_metadata -> Script_bls.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty - | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty + | Chest_key_t : + Script_timelock.chest_key ty_metadata + -> Script_timelock.chest_key ty | Chest_t : Script_timelock.chest ty_metadata -> Script_timelock.chest ty and ('top_ty, 'resty) stack_ty = diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index edd13a315aca..3a9dc42bccb6 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -122,6 +122,14 @@ module Script_bls : sig end module Script_timelock : sig + (** [chest_key] is made algebraic in order to distinguish it from the other + type parameters of [Script_typed_ir.ty]. *) + type chest_key = Chest_key_tag of Timelock.chest_key [@@ocaml.unboxed] + + val make_chest_key : Timelock.chest_key -> chest_key + + val chest_key_encoding : chest_key Data_encoding.t + (** [chest] is made algebraic in order to distinguish it from the other type parameters of [Script_typed_ir.ty]. *) type chest = Chest_tag of Timelock.chest [@@ocaml.unboxed] @@ -130,8 +138,7 @@ module Script_timelock : sig val chest_encoding : chest Data_encoding.t - val open_chest : - chest -> Timelock.chest_key -> time:int -> Timelock.opening_result + val open_chest : chest -> chest_key -> time:int -> Timelock.opening_result val get_plaintext_size : chest -> int end @@ -1119,9 +1126,9 @@ and ('before_top, 'before, 'result_top, 'result) kinstr = * ('a ticket option, 's, 'r, 'f) kinstr -> ('a ticket * 'a ticket, 's, 'r, 'f) kinstr | IOpen_chest : - (Timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo + (Script_timelock.chest_key, Script_timelock.chest * (n num * 's)) kinfo * ((bytes, bool) union, 's, 'r, 'f) kinstr - -> ( Timelock.chest_key, + -> ( Script_timelock.chest_key, Script_timelock.chest * (n num * 's), 'r, 'f ) @@ -1374,7 +1381,9 @@ and 'ty ty = | Bls12_381_g2_t : Script_bls.G2.t ty_metadata -> Script_bls.G2.t ty | Bls12_381_fr_t : Script_bls.Fr.t ty_metadata -> Script_bls.Fr.t ty | Ticket_t : 'a comparable_ty * 'a ticket ty_metadata -> 'a ticket ty - | Chest_key_t : Timelock.chest_key ty_metadata -> Timelock.chest_key ty + | Chest_key_t : + Script_timelock.chest_key ty_metadata + -> Script_timelock.chest_key ty | Chest_t : Script_timelock.chest ty_metadata -> Script_timelock.chest ty and ('top_ty, 'resty) stack_ty = @@ -1633,7 +1642,7 @@ val ticket_t : annot:type_annot option -> 'a ticket ty tzresult -val chest_key_t : annot:type_annot option -> Timelock.chest_key ty +val chest_key_t : annot:type_annot option -> Script_timelock.chest_key ty val chest_t : annot:type_annot option -> Script_timelock.chest ty -- GitLab From 653208159d244eecd502358dcb569bc3c9dff3e1 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Fri, 3 Dec 2021 20:04:47 +0100 Subject: [PATCH 14/19] Proto/Michelson: make Script_int_repr.num algebraic. --- .../lib_protocol/script_int_repr.ml | 84 +++++++++++-------- .../lib_protocol/script_int_repr.mli | 6 +- 2 files changed, 52 insertions(+), 38 deletions(-) diff --git a/src/proto_alpha/lib_protocol/script_int_repr.ml b/src/proto_alpha/lib_protocol/script_int_repr.ml index 7bea740237a0..fba40417adb4 100644 --- a/src/proto_alpha/lib_protocol/script_int_repr.ml +++ b/src/proto_alpha/lib_protocol/script_int_repr.ml @@ -29,86 +29,96 @@ type n = Natural_tag type z = Integer_tag (* We could define `num` as a GADT with constructors for `n` and `z`. - This would enable factorizing the code a bit in the Michelson interpreter and - also make formal the claim that `num` is only instantiated with `n` and `z`, - but it would result in space and time overheads when manipulating `num`s, by - having to deconstruct to and reconstruct from `Z.t`. *) -type 't num = Z.t + This would enable factorizing the code a bit in the Michelson interpreter and + also make formal the claim that `num` is only instantiated with `n` and `z`, + but it would result in space and time overheads when manipulating `num`s, by + having to deconstruct to and reconstruct from `Z.t`. *) +type 't repr = Z.t -let compare x y = Z.compare x y +type 't num = Num_tag of 't repr [@@ocaml.unboxed] -let zero = Z.zero +let compare (Num_tag x) (Num_tag y) = Z.compare x y -let zero_n = Z.zero +let zero = Num_tag Z.zero -let one_n = Z.one +let zero_n = Num_tag Z.zero -let to_string x = Z.to_string x +let one_n = Num_tag Z.one -let of_string s = Option.catch (fun () -> Z.of_string s) +let to_string (Num_tag x) = Z.to_string x -let of_int32 n = Z.of_int64 @@ Int64.of_int32 n +let of_string s = Option.catch (fun () -> Num_tag (Z.of_string s)) -let to_int64 x = Option.catch (fun () -> Z.to_int64 x) +let of_int32 n = Num_tag (Z.of_int64 @@ Int64.of_int32 n) -let of_int64 n = Z.of_int64 n +let to_int64 (Num_tag x) = Option.catch (fun () -> Z.to_int64 x) -let to_int x = Option.catch (fun () -> Z.to_int x) +let of_int64 n = Num_tag (Z.of_int64 n) -let of_int n = Z.of_int n +let to_int (Num_tag x) = Option.catch (fun () -> Z.to_int x) -let of_zint x = x +let of_int n = Num_tag (Z.of_int n) -let to_zint x = x +let of_zint x = Num_tag x -let add x y = Z.add x y +let to_zint (Num_tag x) = x -let sub x y = Z.sub x y +let add (Num_tag x) (Num_tag y) = Num_tag (Z.add x y) -let mul x y = Z.mul x y +let sub (Num_tag x) (Num_tag y) = Num_tag (Z.sub x y) -let ediv x y = Option.catch (fun () -> Z.ediv_rem x y) +let mul (Num_tag x) (Num_tag y) = Num_tag (Z.mul x y) + +let ediv (Num_tag x) (Num_tag y) = + let ediv_tagged x y = + let (quo, rem) = Z.ediv_rem x y in + (Num_tag quo, Num_tag rem) + in + Option.catch (fun () -> ediv_tagged x y) let add_n = add -let succ_n = Z.succ +let succ_n (Num_tag x) = Num_tag (Z.succ x) let mul_n = mul let ediv_n = ediv -let abs x = Z.abs x +let abs (Num_tag x) = Num_tag (Z.abs x) -let is_nat x = if Compare.Z.(x < Z.zero) then None else Some x +let is_nat (Num_tag x) = + if Compare.Z.(x < Z.zero) then None else Some (Num_tag x) -let neg x = Z.neg x +let neg (Num_tag x) = Num_tag (Z.neg x) -let int x = x +let int (Num_tag x) = Num_tag x -let shift_left x y = +let shift_left (Num_tag x) (Num_tag y) = if Compare.Int.(Z.compare y (Z.of_int 256) > 0) then None else let y = Z.to_int y in - Some (Z.shift_left x y) + Some (Num_tag (Z.shift_left x y)) -let shift_right x y = +let shift_right (Num_tag x) (Num_tag y) = if Compare.Int.(Z.compare y (Z.of_int 256) > 0) then None else let y = Z.to_int y in - Some (Z.shift_right x y) + Some (Num_tag (Z.shift_right x y)) let shift_left_n = shift_left let shift_right_n = shift_right -let logor x y = Z.logor x y +let logor (Num_tag x) (Num_tag y) = Num_tag (Z.logor x y) -let logxor x y = Z.logxor x y +let logxor (Num_tag x) (Num_tag y) = Num_tag (Z.logxor x y) -let logand x y = Z.logand x y +let logand (Num_tag x) (Num_tag y) = Num_tag (Z.logand x y) -let lognot x = Z.lognot x +let lognot (Num_tag x) = Num_tag (Z.lognot x) -let z_encoding : z num Data_encoding.encoding = Data_encoding.z +let z_encoding : z num Data_encoding.encoding = + Data_encoding.(conv (fun (Num_tag z) -> z) (fun z -> Num_tag z) z) -let n_encoding : n num Data_encoding.encoding = Data_encoding.n +let n_encoding : n num Data_encoding.encoding = + Data_encoding.(conv (fun (Num_tag n) -> n) (fun n -> Num_tag n) n) diff --git a/src/proto_alpha/lib_protocol/script_int_repr.mli b/src/proto_alpha/lib_protocol/script_int_repr.mli index b104b3620141..1dbb5425330d 100644 --- a/src/proto_alpha/lib_protocol/script_int_repr.mli +++ b/src/proto_alpha/lib_protocol/script_int_repr.mli @@ -30,7 +30,11 @@ This is internally a [Z.t]. This module mostly adds signedness preservation guarantees. *) -type 't num [@@coq_phantom] +type 't repr [@@coq_phantom] + +(** [num] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) +type 't num = Num_tag of 't repr [@@ocaml.unboxed] (** Flag for natural numbers. *) type n = Natural_tag -- GitLab From 9b301eafdd507504672702789238e0df16c8adf9 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Mon, 6 Dec 2021 15:26:23 +0100 Subject: [PATCH 15/19] Proto/Michelson: make Script_typed_ir.Script_signature.t algebraic. --- .../lib_benchmark/michelson_samplers.ml | 5 +++- .../interpreter_benchmarks.ml | 1 + src/proto_alpha/lib_benchmarks_proto/size.ml | 3 ++- .../lib_protocol/script_comparable.ml | 3 ++- .../lib_protocol/script_interpreter.ml | 2 +- .../lib_protocol/script_ir_translator.ml | 7 +++-- .../lib_protocol/script_typed_ir.ml | 25 +++++++++++++++++ .../lib_protocol/script_typed_ir.mli | 27 +++++++++++++++++++ .../test/pbt/test_script_comparison.ml | 2 +- 9 files changed, 68 insertions(+), 7 deletions(-) diff --git a/src/proto_alpha/lib_benchmark/michelson_samplers.ml b/src/proto_alpha/lib_benchmark/michelson_samplers.ml index b1c7011e647a..caa555e6c11d 100644 --- a/src/proto_alpha/lib_benchmark/michelson_samplers.ml +++ b/src/proto_alpha/lib_benchmark/michelson_samplers.ml @@ -515,6 +515,9 @@ end) let string = Base_samplers.uniform_string ~nbytes:4 rng_state in Data_encoding.Binary.of_string_exn Script_chain_id.encoding string + let signature rng_state = + Script_signature.make (Michelson_base.signature rng_state) + let rec value : type a. a Script_typed_ir.ty -> a sampler = let open Script_typed_ir in fun typ -> @@ -523,7 +526,7 @@ end) | Unit_t _ -> M.return () | Int_t _ -> Michelson_base.int | Nat_t _ -> Michelson_base.nat - | Signature_t _ -> Michelson_base.signature + | Signature_t _ -> signature | String_t _ -> Michelson_base.string | Bytes_t _ -> Michelson_base.bytes | Mutez_t _ -> Michelson_base.tez diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index c222f4e6007a..06c80120c0a6 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -2285,6 +2285,7 @@ module Registration_section = struct rng_state in let signed_message = Signature.sign sk unsigned_message in + let signed_message = Script_signature.make signed_message in (pk, (signed_message, (unsigned_message, eos)))) () diff --git a/src/proto_alpha/lib_benchmarks_proto/size.ml b/src/proto_alpha/lib_benchmarks_proto/size.ml index 2420c0a3875f..51ead05967e6 100644 --- a/src/proto_alpha/lib_benchmarks_proto/size.ml +++ b/src/proto_alpha/lib_benchmarks_proto/size.ml @@ -128,7 +128,8 @@ let mutez (_tez : Alpha_context.Tez.tez) : t = let bool (_ : bool) : t = 1 -let signature (_signature : Signature.t) : t = Signature.size +let signature (_signature : Script_typed_ir.Script_signature.t) : t = + Script_typed_ir.Script_signature.size let key_hash (_keyhash : Signature.public_key_hash) : t = Signature.Public_key_hash.size diff --git a/src/proto_alpha/lib_protocol/script_comparable.ml b/src/proto_alpha/lib_protocol/script_comparable.ml index ce9ca359b481..b921eaae61e5 100644 --- a/src/proto_alpha/lib_protocol/script_comparable.ml +++ b/src/proto_alpha/lib_protocol/script_comparable.ml @@ -47,7 +47,8 @@ let compare_comparable : type a. a comparable_ty -> a -> a -> int = match (kind, x, y) with | (Unit_key _, (), ()) -> (apply [@tailcall]) 0 k | (Never_key _, _, _) -> . - | (Signature_key _, x, y) -> (apply [@tailcall]) (Signature.compare x y) k + | (Signature_key _, 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 diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 803f7730d885..46622fb6c5b9 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -1171,7 +1171,7 @@ and step : type a s b t r f. (a, s, b, t, r, f) step_type = | INow (_, k) -> (step [@ocaml.tailcall]) g gas k ks sc.now (accu, stack) | ICheck_signature (_, k) -> let key = accu and (signature, (message, stack)) = stack in - let res = Signature.check key signature message in + let res = Script_signature.check key signature message in (step [@ocaml.tailcall]) g gas k ks res stack | IHash_key (_, k) -> let key = accu in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 9d9038219827..15cf37280342 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -485,6 +485,7 @@ let unparse_contract ~loc ctxt mode {arg_ty = _; address} = unparse_address ~loc ctxt mode address let unparse_signature ~loc ctxt mode s = + let s = Script_signature.get s in match mode with | Optimized | Optimized_legacy -> Gas.consume ctxt Unparse_costs.signature_optimized >|? fun ctxt -> @@ -2207,7 +2208,9 @@ let parse_signature ctxt : Script.node -> (signature * context) tzresult = function | Bytes (loc, bytes) as expr (* As unparsed with [Optimized]. *) -> ( Gas.consume ctxt Typecheck_costs.signature_optimized >>? fun ctxt -> - match Data_encoding.Binary.of_bytes_opt Signature.encoding bytes with + match + Data_encoding.Binary.of_bytes_opt Script_signature.encoding bytes + with | Some k -> ok (k, ctxt) | None -> error @@ -2215,7 +2218,7 @@ let parse_signature ctxt : Script.node -> (signature * context) tzresult = (loc, strip_locations expr, "a valid signature")) | String (loc, s) as expr (* As unparsed with [Readable]. *) -> ( Gas.consume ctxt Typecheck_costs.signature_readable >>? fun ctxt -> - match Signature.of_b58check_opt s with + match Script_signature.of_b58check_opt s with | Some s -> ok (s, ctxt) | None -> error diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index c6e3668a0163..a49f02e3d6c1 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -65,6 +65,31 @@ type never = | type address = {contract : Contract.t; entrypoint : Entrypoint.t} +module Script_signature = struct + type t = Signature_tag of signature [@@ocaml.unboxed] + + let make s = Signature_tag s + + let get (Signature_tag s) = s + + let encoding = + Data_encoding.conv + (fun (Signature_tag x) -> x) + (fun x -> Signature_tag x) + Signature.encoding + + let of_b58check_opt x = Option.map make (Signature.of_b58check_opt x) + + let check ?watermark pub_key (Signature_tag s) bytes = + Signature.check ?watermark pub_key s bytes + + let compare (Signature_tag x) (Signature_tag y) = Signature.compare x y + + let size = Signature.size +end + +type signature = Script_signature.t + type ('a, 'b) pair = 'a * 'b type ('a, 'b) union = L of 'a | R of 'b diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 3a9dc42bccb6..3e7dafa66284 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -46,6 +46,33 @@ type never = | type address = {contract : Contract.t; entrypoint : Entrypoint.t} +module Script_signature : sig + (** [t] is made algebraic in order to distinguish it from the other type + parameters of [Script_typed_ir.ty]. *) + type t = Signature_tag of signature [@@ocaml.unboxed] + + val make : signature -> t + + val get : t -> signature + + val encoding : t Data_encoding.t + + val of_b58check_opt : string -> t option + + val check : + ?watermark:Signature.watermark -> + Signature.Public_key.t -> + t -> + Bytes.t -> + bool + + val compare : t -> t -> int + + val size : int +end + +type signature = Script_signature.t + type ('a, 'b) pair = 'a * 'b type ('a, 'b) union = L of 'a | R of 'b 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 6a0012dfbbda..c61f17a2146b 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 @@ -52,7 +52,7 @@ let rec reference_compare_comparable : type a. a comparable_ty -> a -> a -> int match (ty, x, y) with | (Unit_key _, (), ()) -> 0 | (Never_key _, _, _) -> . - | (Signature_key _, x, y) -> normalize_compare @@ Signature.compare x y + | (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 -- GitLab From ab1ead80638aa0d9c4953fb72e2df4790d8c5fe1 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 7 Dec 2021 10:31:54 +0100 Subject: [PATCH 16/19] Proto/Michelson: make Script_typed_ir.set algebraic. --- .../interpreter_workload.ml | 4 +- src/proto_alpha/lib_protocol/TEZOS_PROTOCOL | 4 +- src/proto_alpha/lib_protocol/dune.inc | 20 +++---- .../lib_protocol/michelson_v1_gas.ml | 9 ++-- src/proto_alpha/lib_protocol/script_set.ml | 52 +++++++++++-------- src/proto_alpha/lib_protocol/script_set.mli | 15 ++++-- .../lib_protocol/script_typed_ir.ml | 5 +- .../lib_protocol/script_typed_ir.mli | 5 +- .../lib_protocol/script_typed_ir_size.ml | 2 +- 9 files changed, 67 insertions(+), 49 deletions(-) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml index d01507284385..8a369495bd94 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml @@ -1203,11 +1203,11 @@ let extract_ir_sized_step : | (IEmpty_set (_, _, _), _) -> Instructions.empty_set | (ISet_iter _, (set, _)) -> Instructions.set_iter (Size.set set) | (ISet_mem (_, _), (v, (set, _))) -> - let (module S) = set in + let (module S) = Script_set.get set in let sz = size_of_comparable_value S.elt_ty v in Instructions.set_mem sz (Size.set set) | (ISet_update (_, _), (v, (_flag, (set, _)))) -> - let (module S) = set in + let (module S) = Script_set.get set in let sz = size_of_comparable_value S.elt_ty v in Instructions.set_update sz (Size.set set) | (ISet_size (_, _), (set, _)) -> Instructions.set_size (Size.set set) diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index 048ea910ea79..36b6a9def8d0 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -104,12 +104,12 @@ "Gas_monad", "Script_ir_annot", "Script_typed_ir", + "Script_comparable", + "Script_set", "Script_typed_ir_size", "Script_typed_ir_size_costs", "Michelson_v1_gas", "Script_list", - "Script_comparable", - "Script_set", "Script_map", "Script_tc_context", "Script_ir_translator", diff --git a/src/proto_alpha/lib_protocol/dune.inc b/src/proto_alpha/lib_protocol/dune.inc index a5a26bb85448..6f2f7a6d3848 100644 --- a/src/proto_alpha/lib_protocol/dune.inc +++ b/src/proto_alpha/lib_protocol/dune.inc @@ -124,12 +124,12 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end gas_monad.mli gas_monad.ml script_ir_annot.mli script_ir_annot.ml script_typed_ir.mli script_typed_ir.ml + script_comparable.mli script_comparable.ml + script_set.mli script_set.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_comparable.mli script_comparable.ml - script_set.mli script_set.ml script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml @@ -262,12 +262,12 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end gas_monad.mli gas_monad.ml script_ir_annot.mli script_ir_annot.ml script_typed_ir.mli script_typed_ir.ml + script_comparable.mli script_comparable.ml + script_set.mli script_set.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_comparable.mli script_comparable.ml - script_set.mli script_set.ml script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml @@ -400,12 +400,12 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end gas_monad.mli gas_monad.ml script_ir_annot.mli script_ir_annot.ml script_typed_ir.mli script_typed_ir.ml + script_comparable.mli script_comparable.ml + script_set.mli script_set.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_comparable.mli script_comparable.ml - script_set.mli script_set.ml script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml @@ -560,12 +560,12 @@ include Tezos_raw_protocol_alpha.Main Gas_monad Script_ir_annot Script_typed_ir + Script_comparable + Script_set Script_typed_ir_size Script_typed_ir_size_costs Michelson_v1_gas Script_list - Script_comparable - Script_set Script_map Script_tc_context Script_ir_translator @@ -739,12 +739,12 @@ include Tezos_raw_protocol_alpha.Main gas_monad.mli gas_monad.ml script_ir_annot.mli script_ir_annot.ml script_typed_ir.mli script_typed_ir.ml + script_comparable.mli script_comparable.ml + script_set.mli script_set.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_comparable.mli script_comparable.ml - script_set.mli script_set.ml script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 3994f39c4b1a..3c155f136910 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -1005,7 +1005,8 @@ module Cost_of = struct let empty_set = atomic_step_cost cost_N_IEmpty_set - let set_iter (type a) ((module Box) : a Script_typed_ir.set) = + let set_iter (type a) (set : a Script_typed_ir.set) = + let (module Box) = Script_set.get set in atomic_step_cost (cost_N_ISet_iter Box.size) let set_size = atomic_step_cost cost_N_ISet_size @@ -1443,15 +1444,17 @@ module Cost_of = struct let intercept = atomic_step_cost (S.safe_int 80) in Gas.(intercept +@ (S.safe_int 2 * log2 size *@ per_elt_cost)) - let set_mem (type a) (elt : a) ((module Box) : a Script_typed_ir.set) = + let set_mem (type a) (elt : a) (set : a Script_typed_ir.set) = let open S_syntax in + let (module Box) = Script_set.get set in let per_elt_cost = compare Box.elt_ty elt elt in let size = S.safe_int Box.size in let intercept = atomic_step_cost (S.safe_int 115) in Gas.(intercept +@ (log2 size *@ per_elt_cost)) - let set_update (type a) (elt : a) ((module Box) : a Script_typed_ir.set) = + let set_update (type a) (elt : a) (set : a Script_typed_ir.set) = let open S_syntax in + let (module Box) = Script_set.get set in let per_elt_cost = compare Box.elt_ty elt elt in let size = S.safe_int Box.size in let intercept = atomic_step_cost (S.safe_int 130) in diff --git a/src/proto_alpha/lib_protocol/script_set.ml b/src/proto_alpha/lib_protocol/script_set.ml index 76cbb2249a06..2567a9593c95 100644 --- a/src/proto_alpha/lib_protocol/script_set.ml +++ b/src/proto_alpha/lib_protocol/script_set.ml @@ -28,6 +28,10 @@ open Alpha_context open Script_typed_ir +let make x = Set_tag x + +let get (Set_tag x) = x + let empty : type a. a comparable_ty -> a set = fun ty -> let module OPS = Set.Make (struct @@ -35,42 +39,44 @@ let empty : type a. a comparable_ty -> a set = let compare = Script_comparable.compare_comparable ty end) in - (module struct - type elt = a + Set_tag + (module struct + type elt = a - let elt_ty = ty + let elt_ty = ty - module OPS = OPS + module OPS = OPS - let boxed = OPS.empty + let boxed = OPS.empty - let size = 0 - end) + let size = 0 + end) let update : type a. a -> bool -> a set -> a set = - fun v b (module Box) -> - (module struct - type elt = a + fun v b (Set_tag (module Box)) -> + Set_tag + (module struct + type elt = a - let elt_ty = Box.elt_ty + let elt_ty = Box.elt_ty - module OPS = Box.OPS + module OPS = Box.OPS - let boxed = - if b then Box.OPS.add v Box.boxed else Box.OPS.remove v Box.boxed + let boxed = + if b then Box.OPS.add v Box.boxed else Box.OPS.remove v Box.boxed - let size = - let mem = Box.OPS.mem v Box.boxed in - if mem then if b then Box.size else Box.size - 1 - else if b then Box.size + 1 - else Box.size - end) + let size = + let mem = Box.OPS.mem v Box.boxed in + if mem then if b then Box.size else Box.size - 1 + else if b then Box.size + 1 + else Box.size + end) let mem : type elt. elt -> elt set -> bool = - fun v (module Box) -> Box.OPS.mem v Box.boxed + fun v (Set_tag (module Box)) -> Box.OPS.mem v Box.boxed let fold : type elt acc. (elt -> acc -> acc) -> elt set -> acc -> acc = - fun f (module Box) -> Box.OPS.fold f Box.boxed + fun f (Set_tag (module Box)) -> Box.OPS.fold f Box.boxed let size : type elt. elt set -> Script_int.n Script_int.num = - fun (module Box) -> Script_int.(abs (of_int Box.size)) + fun (Set_tag (module Box)) -> Script_int.(abs (of_int Box.size)) diff --git a/src/proto_alpha/lib_protocol/script_set.mli b/src/proto_alpha/lib_protocol/script_set.mli index f97a434c25ab..fe50a5e944c6 100644 --- a/src/proto_alpha/lib_protocol/script_set.mli +++ b/src/proto_alpha/lib_protocol/script_set.mli @@ -25,13 +25,18 @@ (*****************************************************************************) open Alpha_context +open Script_typed_ir -val empty : 'a Script_typed_ir.comparable_ty -> 'a Script_typed_ir.set +val make : (module Boxed_set with type elt = 'elt) -> 'elt set -val fold : ('elt -> 'acc -> 'acc) -> 'elt Script_typed_ir.set -> 'acc -> 'acc +val get : 'elt set -> (module Boxed_set with type elt = 'elt) -val update : 'a -> bool -> 'a Script_typed_ir.set -> 'a Script_typed_ir.set +val empty : 'a comparable_ty -> 'a set -val mem : 'elt -> 'elt Script_typed_ir.set -> bool +val fold : ('elt -> 'acc -> 'acc) -> 'elt set -> 'acc -> 'acc -val size : 'elt Script_typed_ir.set -> Script_int.n Script_int.num +val update : 'a -> bool -> 'a set -> 'a set + +val mem : 'elt -> 'elt set -> bool + +val size : 'elt set -> Script_int.n Script_int.num diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index a49f02e3d6c1..e78841b4f18c 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -449,7 +449,8 @@ module type Boxed_set = sig val size : int end -type 'elt set = (module Boxed_set with type elt = 'elt) +type 'elt set = Set_tag of (module Boxed_set with type elt = 'elt) +[@@ocaml.unboxed] (* @@ -2305,7 +2306,7 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f let bindings = M.OPS.fold (fun k v bs -> (k, v) :: bs) M.boxed [] in on_bindings accu kty ty' continue bindings | Set_t (ty', _) -> - let module M = (val x) in + let (Set_tag (module M)) = x in let elements = M.OPS.fold (fun x s -> x :: s) M.boxed [] in on_list' accu ty' elements continue | Big_map_t (_, _, _) -> diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 3e7dafa66284..43558fd1af76 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -306,7 +306,10 @@ module type Boxed_set = sig val size : int end -type 'elt set = (module Boxed_set with type elt = 'elt) +(** [set] is made algebraic in order to distinguish it from the other type + parameters of [ty]. *) +type 'elt set = Set_tag of (module Boxed_set with type elt = 'elt) +[@@ocaml.unboxed] module type Boxed_map_OPS = sig type t 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 03c36068830f..0f3fe182adce 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -261,7 +261,7 @@ let rec value_size : | Option_t (_, _) -> ret_succ_adding accu (option_size (fun _ -> !!0) x) | List_t (_, _) -> ret_succ_adding accu (h2w +! (h2w *? x.length)) | Set_t (_, _) -> - let module M = (val x) in + let module M = (val Script_set.get x) in let boxing_space = !!300 in ret_succ_adding accu (boxing_space +! (h4w *? M.size)) | Map_t (_, _, _) -> -- GitLab From da3e31d6dc1da68b65000f0b838c2d05c2ad300c Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 7 Dec 2021 11:11:54 +0100 Subject: [PATCH 17/19] Proto/Michelson: make Script_typed_ir.map algebraic. --- .../interpreter_benchmarks.ml | 4 +- .../interpreter_workload.ml | 15 +++-- src/proto_alpha/lib_protocol/TEZOS_PROTOCOL | 2 +- src/proto_alpha/lib_protocol/dune.inc | 10 ++-- .../lib_protocol/michelson_v1_gas.ml | 17 +++--- .../lib_protocol/script_ir_translator.ml | 8 ++- src/proto_alpha/lib_protocol/script_map.ml | 58 ++++++++++--------- src/proto_alpha/lib_protocol/script_map.mli | 30 +++++----- .../lib_protocol/script_typed_ir.ml | 5 +- .../lib_protocol/script_typed_ir.mli | 5 +- .../lib_protocol/script_typed_ir_size.ml | 2 +- .../lib_protocol/ticket_scanner.ml | 3 +- 12 files changed, 92 insertions(+), 67 deletions(-) diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml index 06c80120c0a6..c89d4241b008 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_benchmarks.ml @@ -1236,7 +1236,7 @@ module Registration_section = struct (Script_map.empty int_cmp) keys in - let (module M) = map in + let (module M) = Script_map.get_module map in let key = M.OPS.fold (fun k _ -> function None -> Some k | x -> x) M.boxed None |> WithExceptions.Option.get ~loc:__LOC__ @@ -1411,7 +1411,7 @@ module Registration_section = struct (Script_map.empty int_cmp) keys in - let (module M) = map in + let (module M) = Script_map.get_module map in let key = M.OPS.fold (fun k _ -> function None -> Some k | x -> x) M.boxed None |> WithExceptions.Option.get ~loc:__LOC__ diff --git a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml index 8a369495bd94..ecfc28d8fcb1 100644 --- a/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml +++ b/src/proto_alpha/lib_benchmarks_proto/interpreter_workload.ml @@ -1214,16 +1214,20 @@ let extract_ir_sized_step : | (IEmpty_map (_, _, _), _) -> Instructions.empty_map | (IMap_map _, (map, _)) -> Instructions.map_map (Size.map map) | (IMap_iter _, (map, _)) -> Instructions.map_iter (Size.map map) - | (IMap_mem (_, _), (v, (((module Map) as map), _))) -> + | (IMap_mem (_, _), (v, (map, _))) -> + let (module Map) = Script_map.get_module map in let key_size = size_of_comparable_value Map.key_ty v in Instructions.map_mem key_size (Size.map map) - | (IMap_get (_, _), (v, (((module Map) as map), _))) -> + | (IMap_get (_, _), (v, (map, _))) -> + let (module Map) = Script_map.get_module map in let key_size = size_of_comparable_value Map.key_ty v in Instructions.map_get key_size (Size.map map) - | (IMap_update (_, _), (v, (_elt_opt, (((module Map) as map), _)))) -> + | (IMap_update (_, _), (v, (_elt_opt, (map, _)))) -> + let (module Map) = Script_map.get_module map in let key_size = size_of_comparable_value Map.key_ty v in Instructions.map_update key_size (Size.map map) - | (IMap_get_and_update (_, _), (v, (_elt_opt, (((module Map) as map), _)))) -> + | (IMap_get_and_update (_, _), (v, (_elt_opt, (map, _)))) -> + let (module Map) = Script_map.get_module map in let key_size = size_of_comparable_value Map.key_ty v in Instructions.map_get_and_update key_size (Size.map map) | (IMap_size (_, _), (map, _)) -> Instructions.map_size (Size.map map) @@ -1454,7 +1458,8 @@ let extract_control_trace (type bef_top bef aft_top aft) | KList_exit_body (_, _, _, _, _) -> Control.list_exit_body | KMap_enter_body (_, xs, _, _) -> Control.map_enter_body (Size.of_int (List.length xs)) - | KMap_exit_body (_, _, ((module Map) as map), k, _) -> + | KMap_exit_body (_, _, map, k, _) -> + let (module Map) = Script_map.get_module map in let key_size = size_of_comparable_value Map.key_ty k in Control.map_exit_body key_size (Size.map map) | KView_exit _ -> Control.view_exit diff --git a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL index 36b6a9def8d0..bd35f3a774f9 100644 --- a/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL +++ b/src/proto_alpha/lib_protocol/TEZOS_PROTOCOL @@ -106,11 +106,11 @@ "Script_typed_ir", "Script_comparable", "Script_set", + "Script_map", "Script_typed_ir_size", "Script_typed_ir_size_costs", "Michelson_v1_gas", "Script_list", - "Script_map", "Script_tc_context", "Script_ir_translator", "Script_cache", diff --git a/src/proto_alpha/lib_protocol/dune.inc b/src/proto_alpha/lib_protocol/dune.inc index 6f2f7a6d3848..583b2e98430c 100644 --- a/src/proto_alpha/lib_protocol/dune.inc +++ b/src/proto_alpha/lib_protocol/dune.inc @@ -126,11 +126,11 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_typed_ir.mli script_typed_ir.ml script_comparable.mli script_comparable.ml script_set.mli script_set.ml + script_map.mli script_map.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml script_cache.mli script_cache.ml @@ -264,11 +264,11 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_typed_ir.mli script_typed_ir.ml script_comparable.mli script_comparable.ml script_set.mli script_set.ml + script_map.mli script_map.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml script_cache.mli script_cache.ml @@ -402,11 +402,11 @@ module CamlinternalFormatBasics = struct include CamlinternalFormatBasics end script_typed_ir.mli script_typed_ir.ml script_comparable.mli script_comparable.ml script_set.mli script_set.ml + script_map.mli script_map.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml script_cache.mli script_cache.ml @@ -562,11 +562,11 @@ include Tezos_raw_protocol_alpha.Main Script_typed_ir Script_comparable Script_set + Script_map Script_typed_ir_size Script_typed_ir_size_costs Michelson_v1_gas Script_list - Script_map Script_tc_context Script_ir_translator Script_cache @@ -741,11 +741,11 @@ include Tezos_raw_protocol_alpha.Main script_typed_ir.mli script_typed_ir.ml script_comparable.mli script_comparable.ml script_set.mli script_set.ml + script_map.mli script_map.ml script_typed_ir_size.mli script_typed_ir_size.ml script_typed_ir_size_costs.mli script_typed_ir_size_costs.ml michelson_v1_gas.mli michelson_v1_gas.ml script_list.mli script_list.ml - script_map.mli script_map.ml script_tc_context.mli script_tc_context.ml script_ir_translator.mli script_ir_translator.ml script_cache.mli script_cache.ml diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 3c155f136910..04032bfaa655 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -1013,10 +1013,12 @@ module Cost_of = struct let empty_map = atomic_step_cost cost_N_IEmpty_map - let map_map (type k v) ((module Box) : (k, v) Script_typed_ir.map) = + let map_map (type k v) (map : (k, v) Script_typed_ir.map) = + let (module Box) = Script_map.get_module map in atomic_step_cost (cost_N_IMap_map Box.size) - let map_iter (type k v) ((module Box) : (k, v) Script_typed_ir.map) = + let map_iter (type k v) (map : (k, v) Script_typed_ir.map) = + let (module Box) = Script_map.get_module map in atomic_step_cost (cost_N_IMap_iter Box.size) let map_size = atomic_step_cost cost_N_IMap_size @@ -1462,9 +1464,9 @@ module Cost_of = struct on non-structured data *) Gas.(intercept +@ (S.safe_int 2 * log2 size *@ per_elt_cost)) - let map_mem (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) - = + let map_mem (type k v) (elt : k) (map : (k, v) Script_typed_ir.map) = let open S_syntax in + let (module Box) = Script_map.get_module map in let per_elt_cost = compare Box.key_ty elt elt in let size = S.safe_int Box.size in let intercept = atomic_step_cost (S.safe_int 80) in @@ -1472,9 +1474,9 @@ module Cost_of = struct let map_get = map_mem - let map_update (type k v) (elt : k) - ((module Box) : (k, v) Script_typed_ir.map) = + let map_update (type k v) (elt : k) (map : (k, v) Script_typed_ir.map) = let open S_syntax in + let (module Box) = Script_map.get_module map in let per_elt_cost = compare Box.key_ty elt elt in let size = S.safe_int Box.size in let intercept = atomic_step_cost (S.safe_int 80) in @@ -1483,8 +1485,9 @@ module Cost_of = struct Gas.(intercept +@ (S.safe_int 2 * log2 size *@ per_elt_cost)) let map_get_and_update (type k v) (elt : k) - ((module Box) : (k, v) Script_typed_ir.map) = + (map : (k, v) Script_typed_ir.map) = let open S_syntax in + let (module Box) = Script_map.get_module map in let per_elt_cost = compare Box.key_ty elt elt in let size = S.safe_int Box.size in let intercept = atomic_step_cost (S.safe_int 80) in diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 15cf37280342..12be2ee7a1b4 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -6339,7 +6339,8 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode >|=? fun (ctxt, l, ids_to_copy, acc) -> let reversed = {length = l.length; elements = List.rev l.elements} in (ctxt, reversed, ids_to_copy, acc) - | (Map_f has_lazy_storage, Map_t (_, ty, _), (module M)) -> + | (Map_f has_lazy_storage, Map_t (_, ty, _), map) -> + let (module M) = Script_map.get_module map in let bindings m = M.OPS.fold (fun k v bs -> (k, v) :: bs) m [] in List.fold_left_es (fun (ctxt, m, ids_to_copy, acc) (k, x) -> @@ -6363,7 +6364,10 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode let size = M.size end in ( ctxt, - (module M : Boxed_map with type key = M.key and type value = M.value), + Script_map.make + (module M : Boxed_map + with type key = M.key + and type value = M.value), ids_to_copy, acc ) | (_, Option_t (_, _), None) -> return (ctxt, None, ids_to_copy, acc) diff --git a/src/proto_alpha/lib_protocol/script_map.ml b/src/proto_alpha/lib_protocol/script_map.ml index 4404669e8e79..ed7605ff4923 100644 --- a/src/proto_alpha/lib_protocol/script_map.ml +++ b/src/proto_alpha/lib_protocol/script_map.ml @@ -28,8 +28,12 @@ open Alpha_context open Script_typed_ir +let make x = Map_tag x + +let get_module (Map_tag x) = x + let key_ty : type a b. (a, b) map -> a comparable_ty = - fun (module Box) -> Box.key_ty + fun (Map_tag (module Box)) -> Box.key_ty let empty : type a b. a comparable_ty -> (a, b) map = fun ty -> @@ -38,31 +42,32 @@ let empty : type a b. a comparable_ty -> (a, b) map = let compare = Script_comparable.compare_comparable ty end) in - (module struct - type key = a + Map_tag + (module struct + type key = a - type value = b + type value = b - let key_ty = ty + let key_ty = ty - module OPS = struct - type value = b + module OPS = struct + type value = b - include OPS + include OPS - type nonrec t = value t - end + type nonrec t = value t + end - let boxed = OPS.empty + let boxed = OPS.empty - let size = 0 - end) + let size = 0 + end) let get : type key value. key -> (key, value) map -> value option = - fun k (module Box) -> Box.OPS.find k Box.boxed + fun k (Map_tag (module Box)) -> Box.OPS.find k Box.boxed let update : type a b. a -> b option -> (a, b) map -> (a, b) map = - fun k v (module Box) -> + fun k v (Map_tag (module Box)) -> let (boxed, size) = let contains = match Box.OPS.find k Box.boxed with None -> false | _ -> true @@ -71,28 +76,29 @@ let update : type a b. a -> b option -> (a, b) map -> (a, b) map = | Some v -> (Box.OPS.add k v Box.boxed, Box.size + if contains then 0 else 1) | None -> (Box.OPS.remove k Box.boxed, Box.size - if contains then 1 else 0) in - (module struct - type key = a + Map_tag + (module struct + type key = a - type value = b + type value = b - let key_ty = Box.key_ty + let key_ty = Box.key_ty - module OPS = Box.OPS + module OPS = Box.OPS - let boxed = boxed + let boxed = boxed - let size = size - end) + let size = size + end) let mem : type key value. key -> (key, value) map -> bool = - fun k (module Box) -> + fun k (Map_tag (module Box)) -> match Box.OPS.find k Box.boxed with None -> false | _ -> true let fold : type key value acc. (key -> value -> acc -> acc) -> (key, value) map -> acc -> acc = - fun f (module Box) -> Box.OPS.fold f Box.boxed + fun f (Map_tag (module Box)) -> Box.OPS.fold f Box.boxed let size : type key value. (key, value) map -> Script_int.n Script_int.num = - fun (module Box) -> Script_int.(abs (of_int Box.size)) + fun (Map_tag (module Box)) -> Script_int.(abs (of_int Box.size)) diff --git a/src/proto_alpha/lib_protocol/script_map.mli b/src/proto_alpha/lib_protocol/script_map.mli index 7bd3cd51e4b4..5ed0630c880b 100644 --- a/src/proto_alpha/lib_protocol/script_map.mli +++ b/src/proto_alpha/lib_protocol/script_map.mli @@ -25,25 +25,27 @@ (*****************************************************************************) open Alpha_context +open Script_typed_ir -val empty : 'a Script_typed_ir.comparable_ty -> ('a, 'b) Script_typed_ir.map +val make : + (module Boxed_map with type key = 'key and type value = 'value) -> + ('key, 'value) map + +val get_module : + ('key, 'value) map -> + (module Boxed_map with type key = 'key and type value = 'value) + +val empty : 'a comparable_ty -> ('a, 'b) map val fold : - ('key -> 'value -> 'acc -> 'acc) -> - ('key, 'value) Script_typed_ir.map -> - 'acc -> - 'acc + ('key -> 'value -> 'acc -> 'acc) -> ('key, 'value) map -> 'acc -> 'acc -val update : - 'a -> - 'b option -> - ('a, 'b) Script_typed_ir.map -> - ('a, 'b) Script_typed_ir.map +val update : 'a -> 'b option -> ('a, 'b) map -> ('a, 'b) map -val mem : 'key -> ('key, 'value) Script_typed_ir.map -> bool +val mem : 'key -> ('key, 'value) map -> bool -val get : 'key -> ('key, 'value) Script_typed_ir.map -> 'value option +val get : 'key -> ('key, 'value) map -> 'value option -val key_ty : ('a, 'b) Script_typed_ir.map -> 'a Script_typed_ir.comparable_ty +val key_ty : ('a, 'b) map -> 'a comparable_ty -val size : ('a, 'b) Script_typed_ir.map -> Script_int.n Script_int.num +val size : ('a, 'b) map -> Script_int.n Script_int.num diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.ml b/src/proto_alpha/lib_protocol/script_typed_ir.ml index e78841b4f18c..6cd41703eb82 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir.ml @@ -490,7 +490,8 @@ module type Boxed_map = sig end type ('key, 'value) map = - (module Boxed_map with type key = 'key and type value = 'value) + | Map_tag of (module Boxed_map with type key = 'key and type value = 'value) +[@@ocaml.unboxed] module Big_map_overlay = Map.Make (struct type t = Script_expr_hash.t @@ -2302,7 +2303,7 @@ let value_traverse (type t) (ty : (t ty, t comparable_ty) union) (x : t) init f | Ticket_t (cty, _) -> (aux' [@ocaml.tailcall]) accu cty x.contents continue | List_t (ty', _) -> on_list ty' accu x.elements | Map_t (kty, ty', _) -> - let module M = (val x) in + let (Map_tag (module M)) = x in let bindings = M.OPS.fold (fun k v bs -> (k, v) :: bs) M.boxed [] in on_bindings accu kty ty' continue bindings | Set_t (ty', _) -> diff --git a/src/proto_alpha/lib_protocol/script_typed_ir.mli b/src/proto_alpha/lib_protocol/script_typed_ir.mli index 43558fd1af76..2045c405029f 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir.mli +++ b/src/proto_alpha/lib_protocol/script_typed_ir.mli @@ -343,8 +343,11 @@ module type Boxed_map = sig val size : int end +(** [map] is made algebraic in order to distinguish it from the other type + parameters of [ty]. *) type ('key, 'value) map = - (module Boxed_map with type key = 'key and type value = 'value) + | Map_tag of (module Boxed_map with type key = 'key and type value = 'value) +[@@ocaml.unboxed] module Big_map_overlay : Map.S with type key = Script_expr_hash.t 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 0f3fe182adce..3702057e3bc5 100644 --- a/src/proto_alpha/lib_protocol/script_typed_ir_size.ml +++ b/src/proto_alpha/lib_protocol/script_typed_ir_size.ml @@ -265,7 +265,7 @@ let rec value_size : let boxing_space = !!300 in ret_succ_adding accu (boxing_space +! (h4w *? M.size)) | Map_t (_, _, _) -> - let module M = (val x) in + let module M = (val Script_map.get_module x) in let boxing_space = !!300 in ret_succ_adding accu (boxing_space +! (h5w *? M.size)) | Big_map_t (cty, ty', _) -> diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index c553c3d22d75..20b285d2a876 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -447,7 +447,8 @@ module Ticket_collection = struct accumulator -> ret continuation -> ret tzresult Lwt.t = - fun ~include_lazy ctxt val_hty val_ty (module M) acc k -> + fun ~include_lazy ctxt val_hty val_ty map acc k -> + let (module M) = Script_map.get_module map in consume_gas_steps ctxt ~num_steps:1 >>?= fun ctxt -> (* Pay gas for folding over the values *) consume_gas_steps ctxt ~num_steps:M.size >>?= fun ctxt -> -- GitLab From 9e41cd18b094e891d82e3e47cd5171dc03e1b044 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Wed, 8 Dec 2021 00:13:58 +0100 Subject: [PATCH 18/19] Proto/Michelson: remove unused pattern cases. --- src/proto_alpha/lib_protocol/script_interpreter_defs.ml | 1 - src/proto_alpha/lib_protocol/script_ir_translator.ml | 6 +----- src/proto_alpha/lib_protocol/ticket_scanner.ml | 4 ---- 3 files changed, 1 insertion(+), 10 deletions(-) diff --git a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml index 53e8eb21a35a..0e139df04683 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter_defs.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter_defs.ml @@ -492,7 +492,6 @@ let apply ctxt gas capture_ty capture lam = let lam' = Lam (full_descr, full_expr) in let gas = update_local_gas_counter ctxt in return (lam', outdated ctxt, gas) - | _ -> assert false (* [transfer (ctxt, sc) gas tez tp p destination entrypoint] creates an operation that transfers an amount of [tez] to diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index 12be2ee7a1b4..a78595bfcbdf 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -4999,11 +4999,7 @@ and[@coq_axiom_with_reason "gadt"] parse_instr : {apply = (fun kinfo k -> IJoin_tickets (kinfo, contents_ty, k))} in let stack = Item_t (res_ty, rest) in - typed ctxt loc instr stack - | _ -> - (* TODO: https://gitlab.com/tezos/tezos/-/issues/1962 - fix injectivity of types *) - assert false) + typed ctxt loc instr stack) (* Timelocks *) | ( Prim (loc, I_OPEN_CHEST, [], _), Item_t (Chest_key_t _, Item_t (Chest_t _, Item_t (Nat_t _, rest))) ) -> diff --git a/src/proto_alpha/lib_protocol/ticket_scanner.ml b/src/proto_alpha/lib_protocol/ticket_scanner.ml index 20b285d2a876..1090c458e610 100644 --- a/src/proto_alpha/lib_protocol/ticket_scanner.ml +++ b/src/proto_alpha/lib_protocol/ticket_scanner.ml @@ -26,9 +26,6 @@ open Alpha_context -(* Impossible error *) -type error += Unsupported_type_invariant_violated - type error += Unsupported_non_empty_overlay | Unsupported_type_operation let () = @@ -403,7 +400,6 @@ module Ticket_collection = struct else (k [@ocaml.tailcall]) ctxt acc | (True_ht, Ticket_t (comp_ty, _)) -> (k [@ocaml.tailcall]) ctxt (Ex_ticket (comp_ty, x) :: acc) - | _ -> fail Unsupported_type_invariant_violated and tickets_of_list : type a ret. -- GitLab From 5bb522acf9245c98c744bacea2ee71b29a12b015 Mon Sep 17 00:00:00 2001 From: Nicolas Ayache Date: Tue, 7 Dec 2021 23:55:25 +0100 Subject: [PATCH 19/19] Proto/Michelson: enrich has_lazy_storage. --- .../lib_protocol/script_ir_translator.ml | 28 ++++++++----------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/src/proto_alpha/lib_protocol/script_ir_translator.ml b/src/proto_alpha/lib_protocol/script_ir_translator.ml index a78595bfcbdf..fdf22faecf2b 100644 --- a/src/proto_alpha/lib_protocol/script_ir_translator.ml +++ b/src/proto_alpha/lib_protocol/script_ir_translator.ml @@ -6199,8 +6199,10 @@ let diff_of_sapling_state ctxt ~temporary ~ids_to_copy Please keep the usage of this GADT local. *) + type 'ty has_lazy_storage = - | True_f : _ has_lazy_storage + | Big_map_f : ('a, 'b) big_map has_lazy_storage + | Sapling_state_f : Sapling.state has_lazy_storage | False_f : _ has_lazy_storage | Pair_f : 'a has_lazy_storage * 'b has_lazy_storage @@ -6229,8 +6231,8 @@ let rec has_lazy_storage : type t. t ty -> t has_lazy_storage = | (h1, h2) -> cons h1 h2 in match ty with - | Big_map_t (_, _, _) -> True_f - | Sapling_state_t _ -> True_f + | Big_map_t (_, _, _) -> Big_map_f + | Sapling_state_t _ -> Sapling_state_f | Unit_t _ -> False_f | Int_t _ -> False_f | Nat_t _ -> False_f @@ -6287,7 +6289,7 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>?= fun ctxt -> match (has_lazy_storage, ty, x) with | (False_f, _, _) -> return (ctxt, x, ids_to_copy, acc) - | (_, Big_map_t (_, _, _), map) -> + | (Big_map_f, Big_map_t (_, _, _), map) -> diff_of_big_map ctxt mode ~temporary ~ids_to_copy map >|=? fun (diff, id, ctxt) -> let map = @@ -6300,7 +6302,7 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode let diff = Lazy_storage.make Big_map id diff in let ids_to_copy = Lazy_storage.IdSet.add Big_map id ids_to_copy in (ctxt, map, ids_to_copy, diff :: acc) - | (_, Sapling_state_t _, sapling_state) -> + | (Sapling_state_f, Sapling_state_t _, sapling_state) -> diff_of_sapling_state ctxt ~temporary ~ids_to_copy sapling_state >|=? fun (diff, id, ctxt) -> let sapling_state = @@ -6367,10 +6369,6 @@ let[@coq_axiom_with_reason "gadt"] extract_lazy_storage_updates ctxt mode ids_to_copy, acc ) | (_, Option_t (_, _), None) -> return (ctxt, None, ids_to_copy, acc) - | _ -> - (* TODO: https://gitlab.com/tezos/tezos/-/issues/1962 - fix injectivity of types *) - assert false in let has_lazy_storage = has_lazy_storage ty in aux ctxt mode ~temporary ids_to_copy acc ty x ~has_lazy_storage @@ -6398,16 +6396,16 @@ let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage : fun ~f ~init ctxt ty x ~has_lazy_storage -> Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt -> match (has_lazy_storage, ty, x) with - | (_, Big_map_t (_, _, _), {id = Some id; _}) -> + | (Big_map_f, Big_map_t (_, _, _), {id = Some id; _}) -> Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt -> ok (f.f Big_map id (Fold_lazy_storage.Ok init), ctxt) - | (_, Sapling_state_t _, {id = Some id; _}) -> + | (Sapling_state_f, Sapling_state_t _, {id = Some id; _}) -> Gas.consume ctxt Typecheck_costs.parse_instr_cycle >>? fun ctxt -> ok (f.f Sapling_state id (Fold_lazy_storage.Ok init), ctxt) | (False_f, _, _) -> ok (Fold_lazy_storage.Ok init, ctxt) - | (_, Big_map_t (_, _, _), {id = None; _}) -> + | (Big_map_f, Big_map_t (_, _, _), {id = None; _}) -> ok (Fold_lazy_storage.Ok init, ctxt) - | (_, Sapling_state_t _, {id = None; _}) -> + | (Sapling_state_f, Sapling_state_t _, {id = None; _}) -> ok (Fold_lazy_storage.Ok init, ctxt) | (Pair_f (hl, hr), Pair_t ((tyl, _, _), (tyr, _, _), _), (xl, xr)) -> ( fold_lazy_storage ~f ~init ctxt tyl xl ~has_lazy_storage:hl @@ -6444,10 +6442,6 @@ let[@coq_axiom_with_reason "gadt"] rec fold_lazy_storage : | Fold_lazy_storage.Error -> ok (init, ctxt)) m (ok (Fold_lazy_storage.Ok init, ctxt)) - | _ -> - (* TODO: https://gitlab.com/tezos/tezos/-/issues/1962 - fix injectivity of types *) - assert false let[@coq_axiom_with_reason "gadt"] collect_lazy_storage ctxt ty x = let has_lazy_storage = has_lazy_storage ty in -- GitLab