🍬 Script_typed_ir.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Module step_constants.
Record record : Set := Build {
source : Alpha_context.Contract.t;
payer : Signature.public_key_hash;
self : Contract_hash.t;
amount : Alpha_context.Tez.t;
balance : Alpha_context.Tez.t;
chain_id : Chain_id.t;
now : Script_timestamp.t;
level : Script_int.num;
}.
Definition with_source source (r : record) :=
Build source r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_payer payer (r : record) :=
Build r.(source) payer r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_self self (r : record) :=
Build r.(source) r.(payer) self r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_amount amount (r : record) :=
Build r.(source) r.(payer) r.(self) amount r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_balance balance (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) balance r.(chain_id) r.(now)
r.(level).
Definition with_chain_id chain_id (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) chain_id r.(now)
r.(level).
Definition with_now now (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) now
r.(level).
Definition with_level level (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id)
r.(now) level.
End step_constants.
Definition step_constants := step_constants.record.
Inductive never : Set :=.
Module address.
Record record : Set := Build {
destination : Alpha_context.Destination.t;
entrypoint : Alpha_context.Entrypoint.t;
}.
Definition with_destination destination (r : record) :=
Build destination r.(entrypoint).
Definition with_entrypoint entrypoint (r : record) :=
Build r.(destination) entrypoint.
End address.
Definition address := address.record.
Module Script_signature.
Inductive t : Set :=
| Signature_tag : Alpha_context.signature → t.
Definition make (s_value : Alpha_context.signature) : t :=
Signature_tag s_value.
Definition get (function_parameter : t) : Alpha_context.signature :=
let 'Signature_tag s_value := function_parameter in
s_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let 'Signature_tag x_value := function_parameter in
x_value)
(fun (x_value : Alpha_context.signature) ⇒ Signature_tag x_value) None
Signature.encoding.
Definition of_b58check_opt (x_value : string) : option t :=
Option.map make (Signature.of_b58check_opt x_value).
Definition check
(watermark : option Signature.watermark) (pub_key : Signature.public_key)
(function_parameter : t) : bytes → bool :=
let 'Signature_tag s_value := function_parameter in
fun (bytes_value : bytes) ⇒
Signature.check watermark pub_key s_value bytes_value.
Definition compare (function_parameter : t) : t → int :=
let 'Signature_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Signature_tag y_value := function_parameter in
Signature.compare x_value y_value.
Definition size_value : int := Signature.size_value.
End Script_signature.
Definition signature : Set := Script_signature.t.
Definition tx_rollup_l2_address : Set := Tx_rollup_l2_address.Indexable.value.
Definition pair (a b : Set) : Set := a × b.
Inductive union (a b : Set) : Set :=
| L : a → union a b
| R : b → union a b.
Arguments L {_ _}.
Arguments R {_ _}.
Module Script_chain_id.
Inductive t : Set :=
| Chain_id_tag : Chain_id.t → t.
Definition make (x_value : Chain_id.t) : t := Chain_id_tag x_value.
Definition compare (function_parameter : t) : t → int :=
let 'Chain_id_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Chain_id_tag y_value := function_parameter in
Chain_id.compare x_value y_value.
Definition size_value : int := Chain_id.size_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let 'Chain_id_tag x_value := function_parameter in
x_value) make None Chain_id.encoding.
Definition to_b58check (function_parameter : t) : string :=
let 'Chain_id_tag x_value := function_parameter in
Chain_id.to_b58check x_value.
Definition of_b58check_opt (x_value : string) : option t :=
Option.map make (Chain_id.of_b58check_opt x_value).
End Script_chain_id.
Module Script_bls.
Module S.
Record signature {t fr : Set} : Set := {
t := t;
fr := fr;
add : t → t → t;
mul : t → fr → t;
negate : t → t;
of_bytes_opt : Bytes.t → option t;
to_bytes : t → Bytes.t;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Fr.
Inductive t : Set :=
| Fr_tag : Bls.Primitive.Fr.(S.PRIME_FIELD.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'Fr_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Fr_tag y_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.add) x_value y_value).
Definition mul (function_parameter : t) : t → t :=
let 'Fr_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Fr_tag y_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'Fr_tag x_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒ Fr_tag x_value)
(Bls.Primitive.Fr.(S.PRIME_FIELD.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'Fr_tag x_value := function_parameter in
Bls.Primitive.Fr.(S.PRIME_FIELD.to_bytes) x_value.
Definition of_z (z_value : Z.t) : t :=
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.of_z) z_value).
Definition to_z (function_parameter : t) : Z.t :=
let 'Fr_tag x_value := function_parameter in
Bls.Primitive.Fr.(S.PRIME_FIELD.to_z) x_value.
End Fr.
Module G1.
Inductive t : Set :=
| G1_tag : Bls.Primitive.G1.(S.CURVE.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'G1_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'G1_tag y_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.add) x_value y_value).
Definition mul (function_parameter : t) : Fr.t → t :=
let 'G1_tag x_value := function_parameter in
fun (function_parameter : Fr.t) ⇒
let 'Fr.Fr_tag y_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G1_tag x_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.G1.(S.CURVE.t)) ⇒ G1_tag x_value)
(Bls.Primitive.G1.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G1_tag x_value := function_parameter in
Bls.Primitive.G1.(S.CURVE.to_bytes) x_value.
(* G1 *)
Definition module :=
{|
S.add := add;
S.mul := mul;
S.negate := negate;
S.of_bytes_opt := of_bytes_opt;
S.to_bytes := to_bytes
|}.
End G1.
Definition G1 := G1.module.
Module G2.
Inductive t : Set :=
| G2_tag : Bls.Primitive.G2.(S.CURVE.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'G2_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'G2_tag y_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.add) x_value y_value).
Definition mul (function_parameter : t) : Fr.t → t :=
let 'G2_tag x_value := function_parameter in
fun (function_parameter : Fr.t) ⇒
let 'Fr.Fr_tag y_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G2_tag x_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.G2.(S.CURVE.t)) ⇒ G2_tag x_value)
(Bls.Primitive.G2.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G2_tag x_value := function_parameter in
Bls.Primitive.G2.(S.CURVE.to_bytes) x_value.
(* G2 *)
Definition module :=
{|
S.add := add;
S.mul := mul;
S.negate := negate;
S.of_bytes_opt := of_bytes_opt;
S.to_bytes := to_bytes
|}.
End G2.
Definition G2 := G2.module.
Definition pairing_check (l_value : list (G1.(S.t) × G2.(S.t))) : bool :=
let l_value :=
List.map
(fun (function_parameter : G1.(S.t) × G2.(S.t)) ⇒
let '(G1.G1_tag x_value, G2.G2_tag y_value) := function_parameter in
(x_value, y_value)) l_value in
Bls.Primitive.pairing_check l_value.
End Script_bls.
Module Script_timelock.
Inductive chest_key : Set :=
| Chest_key_tag : Timelock.chest_key → chest_key.
Definition make_chest_key (chest_key_value : Timelock.chest_key)
: chest_key := Chest_key_tag chest_key_value.
Definition chest_key_encoding : Data_encoding.encoding chest_key :=
Data_encoding.conv
(fun (function_parameter : chest_key) ⇒
let 'Chest_key_tag x_value := function_parameter in
x_value) (fun (x_value : Timelock.chest_key) ⇒ Chest_key_tag x_value)
None Timelock.chest_key_encoding.
Inductive chest : Set :=
| Chest_tag : Timelock.chest → chest.
Definition make_chest (chest_value : Timelock.chest) : chest :=
Chest_tag chest_value.
Definition chest_encoding : Data_encoding.encoding chest :=
Data_encoding.conv
(fun (function_parameter : chest) ⇒
let 'Chest_tag x_value := function_parameter in
x_value) (fun (x_value : Timelock.chest) ⇒ Chest_tag x_value) None
Timelock.chest_encoding.
Definition open_chest (function_parameter : chest)
: chest_key → int → Timelock.opening_result :=
let 'Chest_tag chest_value := function_parameter in
fun (function_parameter : chest_key) ⇒
let 'Chest_key_tag chest_key_value := function_parameter in
fun (time : int) ⇒ Timelock.open_chest chest_value chest_key_value time.
Definition get_plaintext_size (function_parameter : chest) : int :=
let 'Chest_tag x_value := function_parameter in
Timelock.get_plaintext_size x_value.
End Script_timelock.
Definition ticket_amount : Set := Ticket_amount.t.
Module ticket.
Record record {a : Set} : Set := Build {
ticketer : Alpha_context.Contract.t;
contents : a;
amount : ticket_amount;
}.
Arguments record : clear implicits.
Definition with_ticketer {t_a} ticketer (r : record t_a) :=
Build t_a ticketer r.(contents) r.(amount).
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a r.(ticketer) contents r.(amount).
Definition with_amount {t_a} amount (r : record t_a) :=
Build t_a r.(ticketer) r.(contents) amount.
End ticket.
Definition ticket := ticket.record.
Module TYPE_SIZE.
Record signature {t : Set} : Set := {
t := t;
check_eq :
∀ {error_context error_trace : Set},
Script_tc_errors.error_details error_context → t → t →
Pervasives.result unit error_trace;
to_int : t → Saturation_repr.t;
one : t;
two : t;
three : t;
four : t;
compound1 : Alpha_context.Script.location → t → M? t;
compound2 : Alpha_context.Script.location → t → t → M? t;
}.
End TYPE_SIZE.
Definition TYPE_SIZE := @TYPE_SIZE.signature.
Arguments TYPE_SIZE {_}.
Module Type_size.
Definition t : Set := int.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Module step_constants.
Record record : Set := Build {
source : Alpha_context.Contract.t;
payer : Signature.public_key_hash;
self : Contract_hash.t;
amount : Alpha_context.Tez.t;
balance : Alpha_context.Tez.t;
chain_id : Chain_id.t;
now : Script_timestamp.t;
level : Script_int.num;
}.
Definition with_source source (r : record) :=
Build source r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_payer payer (r : record) :=
Build r.(source) payer r.(self) r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_self self (r : record) :=
Build r.(source) r.(payer) self r.(amount) r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_amount amount (r : record) :=
Build r.(source) r.(payer) r.(self) amount r.(balance) r.(chain_id) r.(now)
r.(level).
Definition with_balance balance (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) balance r.(chain_id) r.(now)
r.(level).
Definition with_chain_id chain_id (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) chain_id r.(now)
r.(level).
Definition with_now now (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id) now
r.(level).
Definition with_level level (r : record) :=
Build r.(source) r.(payer) r.(self) r.(amount) r.(balance) r.(chain_id)
r.(now) level.
End step_constants.
Definition step_constants := step_constants.record.
Inductive never : Set :=.
Module address.
Record record : Set := Build {
destination : Alpha_context.Destination.t;
entrypoint : Alpha_context.Entrypoint.t;
}.
Definition with_destination destination (r : record) :=
Build destination r.(entrypoint).
Definition with_entrypoint entrypoint (r : record) :=
Build r.(destination) entrypoint.
End address.
Definition address := address.record.
Module Script_signature.
Inductive t : Set :=
| Signature_tag : Alpha_context.signature → t.
Definition make (s_value : Alpha_context.signature) : t :=
Signature_tag s_value.
Definition get (function_parameter : t) : Alpha_context.signature :=
let 'Signature_tag s_value := function_parameter in
s_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let 'Signature_tag x_value := function_parameter in
x_value)
(fun (x_value : Alpha_context.signature) ⇒ Signature_tag x_value) None
Signature.encoding.
Definition of_b58check_opt (x_value : string) : option t :=
Option.map make (Signature.of_b58check_opt x_value).
Definition check
(watermark : option Signature.watermark) (pub_key : Signature.public_key)
(function_parameter : t) : bytes → bool :=
let 'Signature_tag s_value := function_parameter in
fun (bytes_value : bytes) ⇒
Signature.check watermark pub_key s_value bytes_value.
Definition compare (function_parameter : t) : t → int :=
let 'Signature_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Signature_tag y_value := function_parameter in
Signature.compare x_value y_value.
Definition size_value : int := Signature.size_value.
End Script_signature.
Definition signature : Set := Script_signature.t.
Definition tx_rollup_l2_address : Set := Tx_rollup_l2_address.Indexable.value.
Definition pair (a b : Set) : Set := a × b.
Inductive union (a b : Set) : Set :=
| L : a → union a b
| R : b → union a b.
Arguments L {_ _}.
Arguments R {_ _}.
Module Script_chain_id.
Inductive t : Set :=
| Chain_id_tag : Chain_id.t → t.
Definition make (x_value : Chain_id.t) : t := Chain_id_tag x_value.
Definition compare (function_parameter : t) : t → int :=
let 'Chain_id_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Chain_id_tag y_value := function_parameter in
Chain_id.compare x_value y_value.
Definition size_value : int := Chain_id.size_value.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv
(fun (function_parameter : t) ⇒
let 'Chain_id_tag x_value := function_parameter in
x_value) make None Chain_id.encoding.
Definition to_b58check (function_parameter : t) : string :=
let 'Chain_id_tag x_value := function_parameter in
Chain_id.to_b58check x_value.
Definition of_b58check_opt (x_value : string) : option t :=
Option.map make (Chain_id.of_b58check_opt x_value).
End Script_chain_id.
Module Script_bls.
Module S.
Record signature {t fr : Set} : Set := {
t := t;
fr := fr;
add : t → t → t;
mul : t → fr → t;
negate : t → t;
of_bytes_opt : Bytes.t → option t;
to_bytes : t → Bytes.t;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _}.
Module Fr.
Inductive t : Set :=
| Fr_tag : Bls.Primitive.Fr.(S.PRIME_FIELD.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'Fr_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Fr_tag y_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.add) x_value y_value).
Definition mul (function_parameter : t) : t → t :=
let 'Fr_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'Fr_tag y_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'Fr_tag x_value := function_parameter in
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.Fr.(S.PRIME_FIELD.t)) ⇒ Fr_tag x_value)
(Bls.Primitive.Fr.(S.PRIME_FIELD.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'Fr_tag x_value := function_parameter in
Bls.Primitive.Fr.(S.PRIME_FIELD.to_bytes) x_value.
Definition of_z (z_value : Z.t) : t :=
Fr_tag (Bls.Primitive.Fr.(S.PRIME_FIELD.of_z) z_value).
Definition to_z (function_parameter : t) : Z.t :=
let 'Fr_tag x_value := function_parameter in
Bls.Primitive.Fr.(S.PRIME_FIELD.to_z) x_value.
End Fr.
Module G1.
Inductive t : Set :=
| G1_tag : Bls.Primitive.G1.(S.CURVE.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'G1_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'G1_tag y_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.add) x_value y_value).
Definition mul (function_parameter : t) : Fr.t → t :=
let 'G1_tag x_value := function_parameter in
fun (function_parameter : Fr.t) ⇒
let 'Fr.Fr_tag y_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G1_tag x_value := function_parameter in
G1_tag (Bls.Primitive.G1.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.G1.(S.CURVE.t)) ⇒ G1_tag x_value)
(Bls.Primitive.G1.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G1_tag x_value := function_parameter in
Bls.Primitive.G1.(S.CURVE.to_bytes) x_value.
(* G1 *)
Definition module :=
{|
S.add := add;
S.mul := mul;
S.negate := negate;
S.of_bytes_opt := of_bytes_opt;
S.to_bytes := to_bytes
|}.
End G1.
Definition G1 := G1.module.
Module G2.
Inductive t : Set :=
| G2_tag : Bls.Primitive.G2.(S.CURVE.t) → t.
Definition add (function_parameter : t) : t → t :=
let 'G2_tag x_value := function_parameter in
fun (function_parameter : t) ⇒
let 'G2_tag y_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.add) x_value y_value).
Definition mul (function_parameter : t) : Fr.t → t :=
let 'G2_tag x_value := function_parameter in
fun (function_parameter : Fr.t) ⇒
let 'Fr.Fr_tag y_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G2_tag x_value := function_parameter in
G2_tag (Bls.Primitive.G2.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls.Primitive.G2.(S.CURVE.t)) ⇒ G2_tag x_value)
(Bls.Primitive.G2.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G2_tag x_value := function_parameter in
Bls.Primitive.G2.(S.CURVE.to_bytes) x_value.
(* G2 *)
Definition module :=
{|
S.add := add;
S.mul := mul;
S.negate := negate;
S.of_bytes_opt := of_bytes_opt;
S.to_bytes := to_bytes
|}.
End G2.
Definition G2 := G2.module.
Definition pairing_check (l_value : list (G1.(S.t) × G2.(S.t))) : bool :=
let l_value :=
List.map
(fun (function_parameter : G1.(S.t) × G2.(S.t)) ⇒
let '(G1.G1_tag x_value, G2.G2_tag y_value) := function_parameter in
(x_value, y_value)) l_value in
Bls.Primitive.pairing_check l_value.
End Script_bls.
Module Script_timelock.
Inductive chest_key : Set :=
| Chest_key_tag : Timelock.chest_key → chest_key.
Definition make_chest_key (chest_key_value : Timelock.chest_key)
: chest_key := Chest_key_tag chest_key_value.
Definition chest_key_encoding : Data_encoding.encoding chest_key :=
Data_encoding.conv
(fun (function_parameter : chest_key) ⇒
let 'Chest_key_tag x_value := function_parameter in
x_value) (fun (x_value : Timelock.chest_key) ⇒ Chest_key_tag x_value)
None Timelock.chest_key_encoding.
Inductive chest : Set :=
| Chest_tag : Timelock.chest → chest.
Definition make_chest (chest_value : Timelock.chest) : chest :=
Chest_tag chest_value.
Definition chest_encoding : Data_encoding.encoding chest :=
Data_encoding.conv
(fun (function_parameter : chest) ⇒
let 'Chest_tag x_value := function_parameter in
x_value) (fun (x_value : Timelock.chest) ⇒ Chest_tag x_value) None
Timelock.chest_encoding.
Definition open_chest (function_parameter : chest)
: chest_key → int → Timelock.opening_result :=
let 'Chest_tag chest_value := function_parameter in
fun (function_parameter : chest_key) ⇒
let 'Chest_key_tag chest_key_value := function_parameter in
fun (time : int) ⇒ Timelock.open_chest chest_value chest_key_value time.
Definition get_plaintext_size (function_parameter : chest) : int :=
let 'Chest_tag x_value := function_parameter in
Timelock.get_plaintext_size x_value.
End Script_timelock.
Definition ticket_amount : Set := Ticket_amount.t.
Module ticket.
Record record {a : Set} : Set := Build {
ticketer : Alpha_context.Contract.t;
contents : a;
amount : ticket_amount;
}.
Arguments record : clear implicits.
Definition with_ticketer {t_a} ticketer (r : record t_a) :=
Build t_a ticketer r.(contents) r.(amount).
Definition with_contents {t_a} contents (r : record t_a) :=
Build t_a r.(ticketer) contents r.(amount).
Definition with_amount {t_a} amount (r : record t_a) :=
Build t_a r.(ticketer) r.(contents) amount.
End ticket.
Definition ticket := ticket.record.
Module TYPE_SIZE.
Record signature {t : Set} : Set := {
t := t;
check_eq :
∀ {error_context error_trace : Set},
Script_tc_errors.error_details error_context → t → t →
Pervasives.result unit error_trace;
to_int : t → Saturation_repr.t;
one : t;
two : t;
three : t;
four : t;
compound1 : Alpha_context.Script.location → t → M? t;
compound2 : Alpha_context.Script.location → t → t → M? t;
}.
End TYPE_SIZE.
Definition TYPE_SIZE := @TYPE_SIZE.signature.
Arguments TYPE_SIZE {_}.
Module Type_size.
Definition t : Set := int.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Saturation_repr.mul_safe_of_int_exn
Alpha_context.Constants.michelson_maximum_type_size in
tt.
Definition to_int : int → Saturation_repr.t :=
Saturation_repr.mul_safe_of_int_exn.
Definition one : int := 1.
Definition two : int := 2.
Definition three : int := 3.
Definition four : int := 4.
Definition check_eq {A error_trace : Set}
(error_details : Script_tc_errors.error_details A) (x_value : int)
(y_value : int) : Pervasives.result unit error_trace :=
if x_value =i y_value then
Result.return_unit
else
Pervasives.Error
match error_details with
| Script_tc_errors.Fast ⇒
cast error_trace Script_tc_errors.Inconsistent_types_fast
| Script_tc_errors.Informative _ ⇒
cast error_trace
(Error_monad.trace_of_error
(Build_extensible "Inconsistent_type_sizes" (t × t)
(x_value, y_value)))
end.
Definition of_int
(loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
let max_size := Alpha_context.Constants.michelson_maximum_type_size in
if size_value ≤i max_size then
return? size_value
else
Error_monad.error_value
(Build_extensible "Type_too_large" (Alpha_context.Script.location × int)
(loc_value, max_size)).
Definition compound1
(loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
of_int loc_value (1 +i size_value).
Definition compound2
(loc_value : Alpha_context.Script.location) (size1 : int) (size2 : int)
: M? int := of_int loc_value ((1 +i size1) +i size2).
(* Type_size *)
Definition module :=
{|
TYPE_SIZE.check_eq _ _ := check_eq;
TYPE_SIZE.to_int := to_int;
TYPE_SIZE.one := one;
TYPE_SIZE.two := two;
TYPE_SIZE.three := three;
TYPE_SIZE.four := four;
TYPE_SIZE.compound1 := compound1;
TYPE_SIZE.compound2 := compound2
|}.
End Type_size.
Definition Type_size : TYPE_SIZE (t := _) := Type_size.module.
Inductive empty_cell : Set :=
| EmptyCell : empty_cell.
Definition end_of_stack : Set := empty_cell × empty_cell.
Module ty_metadata.
Record record : Set := Build {
size : Type_size.(TYPE_SIZE.t);
}.
Definition with_size size (r : record) :=
Build size.
End ty_metadata.
Definition ty_metadata := ty_metadata.record.
Module Boxed_set_OPS.
Record signature {t elt : Set} : Set := {
t := t;
elt := elt;
elt_size : elt → int;
empty : t;
add : elt → t → t;
mem : elt → t → bool;
remove : elt → t → t;
fold : ∀ {a : Set}, (elt → a → a) → t → a → a;
}.
End Boxed_set_OPS.
Definition Boxed_set_OPS := @Boxed_set_OPS.signature.
Arguments Boxed_set_OPS {_ _}.
Module Boxed_set.
Record signature {elt OPS_t : Set} : Set := {
elt := elt;
OPS : Boxed_set_OPS (t := OPS_t) (elt := elt);
boxed : OPS.(Boxed_set_OPS.t);
size_value : int;
}.
End Boxed_set.
Definition Boxed_set := @Boxed_set.signature.
Arguments Boxed_set {_ _}.
Inductive set (elt : Set) : Set :=
| Set_tag : {OPS_t : Set @ Boxed_set (elt := elt) (OPS_t := OPS_t)} → set elt.
Arguments Set_tag {_}.
Module Boxed_map_OPS.
Record signature {t : Set → Set} {key : Set} : Set := {
t := t;
key := key;
key_size : key → int;
empty : ∀ {value : Set}, t value;
add : ∀ {value : Set}, key → value → t value → t value;
remove : ∀ {value : Set}, key → t value → t value;
find : ∀ {value : Set}, key → t value → option value;
fold :
∀ {a value : Set}, (key → value → a → a) → t value → a → a;
fold_es :
∀ {a value : Set},
(key → value → a → M? a) → t value → a → M? a;
}.
End Boxed_map_OPS.
Definition Boxed_map_OPS := @Boxed_map_OPS.signature.
Arguments Boxed_map_OPS {_ _}.
Module Boxed_map.
Record signature {key value : Set} {OPS_t : Set → Set} : Set := {
key := key;
value := value;
OPS : Boxed_map_OPS (t := OPS_t) (key := key);
boxed : OPS.(Boxed_map_OPS.t) value;
size_value : int;
boxed_map_tag : unit;
}.
End Boxed_map.
Definition Boxed_map := @Boxed_map.signature.
Arguments Boxed_map {_ _ _}.
Inductive map (key value : Set) : Set :=
| Map_tag :
{OPS_t : Set → Set @
Boxed_map (key := key) (value := value) (OPS_t := OPS_t)} → map key value.
Arguments Map_tag {_ _}.
Definition Big_map_overlay :=
Map.Make
(let t : Set := Script_expr_hash.t in
let compare := Script_expr_hash.compare in
{|
Compare.COMPARABLE.compare := compare
|}).
Module big_map_overlay.
Record record {key value : Set} : Set := Build {
map : Big_map_overlay.(Map.S.t) (key × option value);
size : int;
}.
Arguments record : clear implicits.
Definition with_map {t_key t_value} map (r : record t_key t_value) :=
Build t_key t_value map r.(size).
Definition with_size {t_key t_value} size (r : record t_key t_value) :=
Build t_key t_value r.(map) size.
End big_map_overlay.
Definition big_map_overlay := big_map_overlay.record.
Module view.
Record record : Set := Build {
input_ty : Alpha_context.Script.node;
output_ty : Alpha_context.Script.node;
view_code : Alpha_context.Script.node;
}.
Definition with_input_ty input_ty (r : record) :=
Build input_ty r.(output_ty) r.(view_code).
Definition with_output_ty output_ty (r : record) :=
Build r.(input_ty) output_ty r.(view_code).
Definition with_view_code view_code (r : record) :=
Build r.(input_ty) r.(output_ty) view_code.
End view.
Definition view := view.record.
Definition view_map : Set := map Script_string.t view.
Module entrypoint_info.
Record record : Set := Build {
name : Alpha_context.Entrypoint.t;
original_type_expr : Alpha_context.Script.node;
}.
Definition with_name name (r : record) :=
Build name r.(original_type_expr).
Definition with_original_type_expr original_type_expr (r : record) :=
Build r.(name) original_type_expr.
End entrypoint_info.
Definition entrypoint_info := entrypoint_info.record.
let '_ :=
Saturation_repr.mul_safe_of_int_exn
Alpha_context.Constants.michelson_maximum_type_size in
tt.
Definition to_int : int → Saturation_repr.t :=
Saturation_repr.mul_safe_of_int_exn.
Definition one : int := 1.
Definition two : int := 2.
Definition three : int := 3.
Definition four : int := 4.
Definition check_eq {A error_trace : Set}
(error_details : Script_tc_errors.error_details A) (x_value : int)
(y_value : int) : Pervasives.result unit error_trace :=
if x_value =i y_value then
Result.return_unit
else
Pervasives.Error
match error_details with
| Script_tc_errors.Fast ⇒
cast error_trace Script_tc_errors.Inconsistent_types_fast
| Script_tc_errors.Informative _ ⇒
cast error_trace
(Error_monad.trace_of_error
(Build_extensible "Inconsistent_type_sizes" (t × t)
(x_value, y_value)))
end.
Definition of_int
(loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
let max_size := Alpha_context.Constants.michelson_maximum_type_size in
if size_value ≤i max_size then
return? size_value
else
Error_monad.error_value
(Build_extensible "Type_too_large" (Alpha_context.Script.location × int)
(loc_value, max_size)).
Definition compound1
(loc_value : Alpha_context.Script.location) (size_value : int) : M? int :=
of_int loc_value (1 +i size_value).
Definition compound2
(loc_value : Alpha_context.Script.location) (size1 : int) (size2 : int)
: M? int := of_int loc_value ((1 +i size1) +i size2).
(* Type_size *)
Definition module :=
{|
TYPE_SIZE.check_eq _ _ := check_eq;
TYPE_SIZE.to_int := to_int;
TYPE_SIZE.one := one;
TYPE_SIZE.two := two;
TYPE_SIZE.three := three;
TYPE_SIZE.four := four;
TYPE_SIZE.compound1 := compound1;
TYPE_SIZE.compound2 := compound2
|}.
End Type_size.
Definition Type_size : TYPE_SIZE (t := _) := Type_size.module.
Inductive empty_cell : Set :=
| EmptyCell : empty_cell.
Definition end_of_stack : Set := empty_cell × empty_cell.
Module ty_metadata.
Record record : Set := Build {
size : Type_size.(TYPE_SIZE.t);
}.
Definition with_size size (r : record) :=
Build size.
End ty_metadata.
Definition ty_metadata := ty_metadata.record.
Module Boxed_set_OPS.
Record signature {t elt : Set} : Set := {
t := t;
elt := elt;
elt_size : elt → int;
empty : t;
add : elt → t → t;
mem : elt → t → bool;
remove : elt → t → t;
fold : ∀ {a : Set}, (elt → a → a) → t → a → a;
}.
End Boxed_set_OPS.
Definition Boxed_set_OPS := @Boxed_set_OPS.signature.
Arguments Boxed_set_OPS {_ _}.
Module Boxed_set.
Record signature {elt OPS_t : Set} : Set := {
elt := elt;
OPS : Boxed_set_OPS (t := OPS_t) (elt := elt);
boxed : OPS.(Boxed_set_OPS.t);
size_value : int;
}.
End Boxed_set.
Definition Boxed_set := @Boxed_set.signature.
Arguments Boxed_set {_ _}.
Inductive set (elt : Set) : Set :=
| Set_tag : {OPS_t : Set @ Boxed_set (elt := elt) (OPS_t := OPS_t)} → set elt.
Arguments Set_tag {_}.
Module Boxed_map_OPS.
Record signature {t : Set → Set} {key : Set} : Set := {
t := t;
key := key;
key_size : key → int;
empty : ∀ {value : Set}, t value;
add : ∀ {value : Set}, key → value → t value → t value;
remove : ∀ {value : Set}, key → t value → t value;
find : ∀ {value : Set}, key → t value → option value;
fold :
∀ {a value : Set}, (key → value → a → a) → t value → a → a;
fold_es :
∀ {a value : Set},
(key → value → a → M? a) → t value → a → M? a;
}.
End Boxed_map_OPS.
Definition Boxed_map_OPS := @Boxed_map_OPS.signature.
Arguments Boxed_map_OPS {_ _}.
Module Boxed_map.
Record signature {key value : Set} {OPS_t : Set → Set} : Set := {
key := key;
value := value;
OPS : Boxed_map_OPS (t := OPS_t) (key := key);
boxed : OPS.(Boxed_map_OPS.t) value;
size_value : int;
boxed_map_tag : unit;
}.
End Boxed_map.
Definition Boxed_map := @Boxed_map.signature.
Arguments Boxed_map {_ _ _}.
Inductive map (key value : Set) : Set :=
| Map_tag :
{OPS_t : Set → Set @
Boxed_map (key := key) (value := value) (OPS_t := OPS_t)} → map key value.
Arguments Map_tag {_ _}.
Definition Big_map_overlay :=
Map.Make
(let t : Set := Script_expr_hash.t in
let compare := Script_expr_hash.compare in
{|
Compare.COMPARABLE.compare := compare
|}).
Module big_map_overlay.
Record record {key value : Set} : Set := Build {
map : Big_map_overlay.(Map.S.t) (key × option value);
size : int;
}.
Arguments record : clear implicits.
Definition with_map {t_key t_value} map (r : record t_key t_value) :=
Build t_key t_value map r.(size).
Definition with_size {t_key t_value} size (r : record t_key t_value) :=
Build t_key t_value r.(map) size.
End big_map_overlay.
Definition big_map_overlay := big_map_overlay.record.
Module view.
Record record : Set := Build {
input_ty : Alpha_context.Script.node;
output_ty : Alpha_context.Script.node;
view_code : Alpha_context.Script.node;
}.
Definition with_input_ty input_ty (r : record) :=
Build input_ty r.(output_ty) r.(view_code).
Definition with_output_ty output_ty (r : record) :=
Build r.(input_ty) output_ty r.(view_code).
Definition with_view_code view_code (r : record) :=
Build r.(input_ty) r.(output_ty) view_code.
End view.
Definition view := view.record.
Definition view_map : Set := map Script_string.t view.
Module entrypoint_info.
Record record : Set := Build {
name : Alpha_context.Entrypoint.t;
original_type_expr : Alpha_context.Script.node;
}.
Definition with_name name (r : record) :=
Build name r.(original_type_expr).
Definition with_original_type_expr original_type_expr (r : record) :=
Build r.(name) original_type_expr.
End entrypoint_info.
Definition entrypoint_info := entrypoint_info.record.
Records for the constructor parameters
Module ConstructorRecords_nested_entrypoints.
Module nested_entrypoints.
Module Entrypoints_Union.
Record record {_left _right : Set} : Set := Build {
_left : _left;
_right : _right;
}.
Arguments record : clear implicits.
Definition with__left {t__left t__right} _left
(r : record t__left t__right) :=
Build t__left t__right _left r.(_right).
Definition with__right {t__left t__right} _right
(r : record t__left t__right) :=
Build t__left t__right r.(_left) _right.
End Entrypoints_Union.
Definition Entrypoints_Union_skeleton := Entrypoints_Union.record.
End nested_entrypoints.
End ConstructorRecords_nested_entrypoints.
Import ConstructorRecords_nested_entrypoints.
Module entrypoints_node.
Record record {at_node nested : Set} : Set := Build {
at_node : at_node;
nested : nested;
}.
Arguments record : clear implicits.
Definition with_at_node {t_at_node t_nested} at_node
(r : record t_at_node t_nested) :=
Build t_at_node t_nested at_node r.(nested).
Definition with_nested {t_at_node t_nested} nested
(r : record t_at_node t_nested) :=
Build t_at_node t_nested r.(at_node) nested.
End entrypoints_node.
Definition entrypoints_node_skeleton := entrypoints_node.record.
Reserved Notation "'nested_entrypoints.Entrypoints_Union".
Reserved Notation "'entrypoints_node".
Inductive nested_entrypoints : Set :=
| Entrypoints_Union :
'nested_entrypoints.Entrypoints_Union → nested_entrypoints
| Entrypoints_None : nested_entrypoints
where "'entrypoints_node" :=
(entrypoints_node_skeleton (option entrypoint_info) nested_entrypoints)
and "'nested_entrypoints.Entrypoints_Union" :=
(nested_entrypoints.Entrypoints_Union_skeleton 'entrypoints_node
'entrypoints_node).
Module nested_entrypoints.
Include ConstructorRecords_nested_entrypoints.nested_entrypoints.
Definition Entrypoints_Union := 'nested_entrypoints.Entrypoints_Union.
End nested_entrypoints.
Definition entrypoints_node := 'entrypoints_node.
Definition no_entrypoints : entrypoints_node :=
{| entrypoints_node.at_node := None;
entrypoints_node.nested := Entrypoints_None; |}.
Inductive logging_event : Set :=
| LogEntry : logging_event
| LogExit : Alpha_context.Script.location → logging_event.
Module nested_entrypoints.
Module Entrypoints_Union.
Record record {_left _right : Set} : Set := Build {
_left : _left;
_right : _right;
}.
Arguments record : clear implicits.
Definition with__left {t__left t__right} _left
(r : record t__left t__right) :=
Build t__left t__right _left r.(_right).
Definition with__right {t__left t__right} _right
(r : record t__left t__right) :=
Build t__left t__right r.(_left) _right.
End Entrypoints_Union.
Definition Entrypoints_Union_skeleton := Entrypoints_Union.record.
End nested_entrypoints.
End ConstructorRecords_nested_entrypoints.
Import ConstructorRecords_nested_entrypoints.
Module entrypoints_node.
Record record {at_node nested : Set} : Set := Build {
at_node : at_node;
nested : nested;
}.
Arguments record : clear implicits.
Definition with_at_node {t_at_node t_nested} at_node
(r : record t_at_node t_nested) :=
Build t_at_node t_nested at_node r.(nested).
Definition with_nested {t_at_node t_nested} nested
(r : record t_at_node t_nested) :=
Build t_at_node t_nested r.(at_node) nested.
End entrypoints_node.
Definition entrypoints_node_skeleton := entrypoints_node.record.
Reserved Notation "'nested_entrypoints.Entrypoints_Union".
Reserved Notation "'entrypoints_node".
Inductive nested_entrypoints : Set :=
| Entrypoints_Union :
'nested_entrypoints.Entrypoints_Union → nested_entrypoints
| Entrypoints_None : nested_entrypoints
where "'entrypoints_node" :=
(entrypoints_node_skeleton (option entrypoint_info) nested_entrypoints)
and "'nested_entrypoints.Entrypoints_Union" :=
(nested_entrypoints.Entrypoints_Union_skeleton 'entrypoints_node
'entrypoints_node).
Module nested_entrypoints.
Include ConstructorRecords_nested_entrypoints.nested_entrypoints.
Definition Entrypoints_Union := 'nested_entrypoints.Entrypoints_Union.
End nested_entrypoints.
Definition entrypoints_node := 'entrypoints_node.
Definition no_entrypoints : entrypoints_node :=
{| entrypoints_node.at_node := None;
entrypoints_node.nested := Entrypoints_None; |}.
Inductive logging_event : Set :=
| LogEntry : logging_event
| LogExit : Alpha_context.Script.location → logging_event.
Records for the constructor parameters
Module
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Module kinstr.
Module IIf_none.
Record record {loc branch_if_none branch_if_some k : Set} : Set := Build {
loc : loc;
branch_if_none : branch_if_none;
branch_if_some : branch_if_some;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_none t_branch_if_some t_k} loc
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k loc r.(branch_if_none)
r.(branch_if_some) r.(k).
Definition with_branch_if_none
{t_loc t_branch_if_none t_branch_if_some t_k} branch_if_none
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc) branch_if_none
r.(branch_if_some) r.(k).
Definition with_branch_if_some
{t_loc t_branch_if_none t_branch_if_some t_k} branch_if_some
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
r.(branch_if_none) branch_if_some r.(k).
Definition with_k {t_loc t_branch_if_none t_branch_if_some t_k} k
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
r.(branch_if_none) r.(branch_if_some) k.
End IIf_none.
Definition IIf_none_skeleton := IIf_none.record.
Module IOpt_map.
Record record {loc body k : Set} : Set := Build {
loc : loc;
body : body;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_body t_k} loc
(r : record t_loc t_body t_k) :=
Build t_loc t_body t_k loc r.(body) r.(k).
Definition with_body {t_loc t_body t_k} body
(r : record t_loc t_body t_k) :=
Build t_loc t_body t_k r.(loc) body r.(k).
Definition with_k {t_loc t_body t_k} k (r : record t_loc t_body t_k) :=
Build t_loc t_body t_k r.(loc) r.(body) k.
End IOpt_map.
Definition IOpt_map_skeleton := IOpt_map.record.
Module IIf_left.
Record record {loc branch_if_left branch_if_right k : Set} : Set := Build {
loc : loc;
branch_if_left : branch_if_left;
branch_if_right : branch_if_right;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_left t_branch_if_right t_k} loc
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k loc
r.(branch_if_left) r.(branch_if_right) r.(k).
Definition with_branch_if_left
{t_loc t_branch_if_left t_branch_if_right t_k} branch_if_left
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
branch_if_left r.(branch_if_right) r.(k).
Definition with_branch_if_right
{t_loc t_branch_if_left t_branch_if_right t_k} branch_if_right
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
r.(branch_if_left) branch_if_right r.(k).
Definition with_k {t_loc t_branch_if_left t_branch_if_right t_k} k
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
r.(branch_if_left) r.(branch_if_right) k.
End IIf_left.
Definition IIf_left_skeleton := IIf_left.record.
Module IIf_cons.
Record record {loc branch_if_cons branch_if_nil k : Set} : Set := Build {
loc : loc;
branch_if_cons : branch_if_cons;
branch_if_nil : branch_if_nil;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_cons t_branch_if_nil t_k} loc
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k loc r.(branch_if_cons)
r.(branch_if_nil) r.(k).
Definition with_branch_if_cons
{t_loc t_branch_if_cons t_branch_if_nil t_k} branch_if_cons
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc) branch_if_cons
r.(branch_if_nil) r.(k).
Definition with_branch_if_nil {t_loc t_branch_if_cons t_branch_if_nil t_k}
branch_if_nil (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
r.(branch_if_cons) branch_if_nil r.(k).
Definition with_k {t_loc t_branch_if_cons t_branch_if_nil t_k} k
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
r.(branch_if_cons) r.(branch_if_nil) k.
End IIf_cons.
Definition IIf_cons_skeleton := IIf_cons.record.
Module IIf.
Record record {loc branch_if_true branch_if_false k : Set} : Set := Build {
loc : loc;
branch_if_true : branch_if_true;
branch_if_false : branch_if_false;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_true t_branch_if_false t_k} loc
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k loc
r.(branch_if_true) r.(branch_if_false) r.(k).
Definition with_branch_if_true
{t_loc t_branch_if_true t_branch_if_false t_k} branch_if_true
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
branch_if_true r.(branch_if_false) r.(k).
Definition with_branch_if_false
{t_loc t_branch_if_true t_branch_if_false t_k} branch_if_false
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
r.(branch_if_true) branch_if_false r.(k).
Definition with_k {t_loc t_branch_if_true t_branch_if_false t_k} k
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
r.(branch_if_true) r.(branch_if_false) k.
End IIf.
Definition IIf_skeleton := IIf.record.
Module ICreate_contract.
Record record {loc storage_type code k : Set} : Set := Build {
loc : loc;
storage_type : storage_type;
code : code;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_storage_type t_code t_k} loc
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k loc r.(storage_type) r.(code)
r.(k).
Definition with_storage_type {t_loc t_storage_type t_code t_k}
storage_type (r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) storage_type r.(code)
r.(k).
Definition with_code {t_loc t_storage_type t_code t_k} code
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) code
r.(k).
Definition with_k {t_loc t_storage_type t_code t_k} k
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) r.(code)
k.
End ICreate_contract.
Definition ICreate_contract_skeleton := ICreate_contract.record.
Module IEmit.
Record record {loc tag ty unparsed_ty k : Set} : Set := Build {
loc : loc;
tag : tag;
ty : ty;
unparsed_ty : unparsed_ty;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_tag t_ty t_unparsed_ty t_k} loc
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k loc r.(tag) r.(ty)
r.(unparsed_ty) r.(k).
Definition with_tag {t_loc t_tag t_ty t_unparsed_ty t_k} tag
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) tag r.(ty)
r.(unparsed_ty) r.(k).
Definition with_ty {t_loc t_tag t_ty t_unparsed_ty t_k} ty
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) ty
r.(unparsed_ty) r.(k).
Definition with_unparsed_ty {t_loc t_tag t_ty t_unparsed_ty t_k}
unparsed_ty (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
unparsed_ty r.(k).
Definition with_k {t_loc t_tag t_ty t_unparsed_ty t_k} k
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
r.(unparsed_ty) k.
End IEmit.
Definition IEmit_skeleton := IEmit.record.
End kinstr.
Module typed_contract.
Module Typed_originated.
Record record {arg_ty contract_hash entrypoint : Set} : Set := Build {
arg_ty : arg_ty;
contract_hash : contract_hash;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_contract_hash t_entrypoint} arg_ty
(r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint arg_ty r.(contract_hash)
r.(entrypoint).
Definition with_contract_hash {t_arg_ty t_contract_hash t_entrypoint}
contract_hash (r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) contract_hash
r.(entrypoint).
Definition with_entrypoint {t_arg_ty t_contract_hash t_entrypoint}
entrypoint (r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) r.(contract_hash)
entrypoint.
End Typed_originated.
Definition Typed_originated_skeleton := Typed_originated.record.
Module Typed_tx_rollup.
Record record {arg_ty tx_rollup : Set} : Set := Build {
arg_ty : arg_ty;
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_tx_rollup} arg_ty
(r : record t_arg_ty t_tx_rollup) :=
Build t_arg_ty t_tx_rollup arg_ty r.(tx_rollup).
Definition with_tx_rollup {t_arg_ty t_tx_rollup} tx_rollup
(r : record t_arg_ty t_tx_rollup) :=
Build t_arg_ty t_tx_rollup r.(arg_ty) tx_rollup.
End Typed_tx_rollup.
Definition Typed_tx_rollup_skeleton := Typed_tx_rollup.record.
Module Typed_sc_rollup.
Record record {arg_ty sc_rollup entrypoint : Set} : Set := Build {
arg_ty : arg_ty;
sc_rollup : sc_rollup;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_sc_rollup t_entrypoint} arg_ty
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint arg_ty r.(sc_rollup)
r.(entrypoint).
Definition with_sc_rollup {t_arg_ty t_sc_rollup t_entrypoint} sc_rollup
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) sc_rollup
r.(entrypoint).
Definition with_entrypoint {t_arg_ty t_sc_rollup t_entrypoint} entrypoint
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) r.(sc_rollup)
entrypoint.
End Typed_sc_rollup.
Definition Typed_sc_rollup_skeleton := Typed_sc_rollup.record.
Module Typed_zk_rollup.
Record record {arg_ty zk_rollup : Set} : Set := Build {
arg_ty : arg_ty;
zk_rollup : zk_rollup;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_zk_rollup} arg_ty
(r : record t_arg_ty t_zk_rollup) :=
Build t_arg_ty t_zk_rollup arg_ty r.(zk_rollup).
Definition with_zk_rollup {t_arg_ty t_zk_rollup} zk_rollup
(r : record t_arg_ty t_zk_rollup) :=
Build t_arg_ty t_zk_rollup r.(arg_ty) zk_rollup.
End Typed_zk_rollup.
Definition Typed_zk_rollup_skeleton := Typed_zk_rollup.record.
End typed_contract.
Module big_map.
Module Big_map.
Record record {id diff key_type value_type : Set} : Set := Build {
id : id;
diff : diff;
key_type : key_type;
value_type : value_type;
}.
Arguments record : clear implicits.
Definition with_id {t_id t_diff t_key_type t_value_type} id
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type id r.(diff) r.(key_type)
r.(value_type).
Definition with_diff {t_id t_diff t_key_type t_value_type} diff
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) diff r.(key_type)
r.(value_type).
Definition with_key_type {t_id t_diff t_key_type t_value_type} key_type
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) key_type
r.(value_type).
Definition with_value_type {t_id t_diff t_key_type t_value_type}
value_type (r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) r.(key_type)
value_type.
End Big_map.
Definition Big_map_skeleton := Big_map.record.
End big_map.
Module view_signature.
Module View_signature.
Record record {name input_ty output_ty : Set} : Set := Build {
name : name;
input_ty : input_ty;
output_ty : output_ty;
}.
Arguments record : clear implicits.
Definition with_name {t_name t_input_ty t_output_ty} name
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty name r.(input_ty) r.(output_ty).
Definition with_input_ty {t_name t_input_ty t_output_ty} input_ty
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty r.(name) input_ty r.(output_ty).
Definition with_output_ty {t_name t_input_ty t_output_ty} output_ty
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty r.(name) r.(input_ty) output_ty.
End View_signature.
Definition View_signature_skeleton := View_signature.record.
End view_signature.
Module internal_operation_contents.
Module Transaction_to_implicit.
Record record {destination amount : Set} : Set := Build {
destination : destination;
amount : amount;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_amount} destination
(r : record t_destination t_amount) :=
Build t_destination t_amount destination r.(amount).
Definition with_amount {t_destination t_amount} amount
(r : record t_destination t_amount) :=
Build t_destination t_amount r.(destination) amount.
End Transaction_to_implicit.
Definition Transaction_to_implicit_skeleton :=
Transaction_to_implicit.record.
Module Transaction_to_smart_contract.
Record record {destination amount entrypoint location parameters_ty
parameters unparsed_parameters : Set} : Set := Build {
destination : destination;
amount : amount;
entrypoint : entrypoint;
location : location;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} destination
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters destination r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_amount
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} amount
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) amount
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_entrypoint
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} entrypoint
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
entrypoint r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_location
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} location
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) location r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} parameters_ty
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) parameters_ty r.(parameters)
r.(unparsed_parameters).
Definition with_parameters
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} parameters
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) parameters
r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} unparsed_parameters
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
unparsed_parameters.
End Transaction_to_smart_contract.
Definition Transaction_to_smart_contract_skeleton :=
Transaction_to_smart_contract.record.
Module Transaction_to_tx_rollup.
Record record {destination parameters_ty parameters unparsed_parameters :
Set} : Set := Build {
destination : destination;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
destination
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters_ty
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
unparsed_parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
End Transaction_to_tx_rollup.
Definition Transaction_to_tx_rollup_skeleton :=
Transaction_to_tx_rollup.record.
Module Transaction_to_sc_rollup.
Record record {destination entrypoint parameters_ty parameters
unparsed_parameters : Set} : Set := Build {
destination : destination;
entrypoint : entrypoint;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} destination
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters destination r.(entrypoint) r.(parameters_ty)
r.(parameters) r.(unparsed_parameters).
Definition with_entrypoint
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} entrypoint
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) entrypoint r.(parameters_ty)
r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} parameters_ty
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) parameters_ty
r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} parameters
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} unparsed_parameters
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
r.(parameters) unparsed_parameters.
End Transaction_to_sc_rollup.
Definition Transaction_to_sc_rollup_skeleton :=
Transaction_to_sc_rollup.record.
Module Event.
Record record {ty tag unparsed_data : Set} : Set := Build {
ty : ty;
tag : tag;
unparsed_data : unparsed_data;
}.
Arguments record : clear implicits.
Definition with_ty {t_ty t_tag t_unparsed_data} ty
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data ty r.(tag) r.(unparsed_data).
Definition with_tag {t_ty t_tag t_unparsed_data} tag
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data r.(ty) tag r.(unparsed_data).
Definition with_unparsed_data {t_ty t_tag t_unparsed_data} unparsed_data
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data r.(ty) r.(tag) unparsed_data.
End Event.
Definition Event_skeleton := Event.record.
Module Transaction_to_zk_rollup.
Record record {destination parameters_ty parameters unparsed_parameters :
Set} : Set := Build {
destination : destination;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
destination
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters_ty
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
unparsed_parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
End Transaction_to_zk_rollup.
Definition Transaction_to_zk_rollup_skeleton :=
Transaction_to_zk_rollup.record.
Module Origination.
Record record {delegate code unparsed_storage credit preorigination
storage_type storage : Set} : Set := Build {
delegate : delegate;
code : code;
unparsed_storage : unparsed_storage;
credit : credit;
preorigination : preorigination;
storage_type : storage_type;
storage : storage;
}.
Arguments record : clear implicits.
Definition with_delegate
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} delegate
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage delegate r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_code
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} code
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) code r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_unparsed_storage
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} unparsed_storage
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) unparsed_storage
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_credit
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} credit
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
credit r.(preorigination) r.(storage_type) r.(storage).
Definition with_preorigination
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} preorigination
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) preorigination r.(storage_type) r.(storage).
Definition with_storage_type
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} storage_type
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) storage_type r.(storage).
Definition with_storage
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} storage
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) storage.
End Origination.
Definition Origination_skeleton := Origination.record.
End internal_operation_contents.
End
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Import
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Module operation.
Record record {piop lazy_storage_diff : Set} : Set := Build {
piop : piop;
lazy_storage_diff : lazy_storage_diff;
}.
Arguments record : clear implicits.
Definition with_piop {t_piop t_lazy_storage_diff} piop
(r : record t_piop t_lazy_storage_diff) :=
Build t_piop t_lazy_storage_diff piop r.(lazy_storage_diff).
Definition with_lazy_storage_diff {t_piop t_lazy_storage_diff}
lazy_storage_diff (r : record t_piop t_lazy_storage_diff) :=
Build t_piop t_lazy_storage_diff r.(piop) lazy_storage_diff.
End operation.
Definition operation_skeleton := operation.record.
Module internal_operation.
Record record {source operation nonce : Set} : Set := Build {
source : source;
operation : operation;
nonce : nonce;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_operation t_nonce} source
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce source r.(operation) r.(nonce).
Definition with_operation {t_source t_operation t_nonce} operation
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce r.(source) operation r.(nonce).
Definition with_nonce {t_source t_operation t_nonce} nonce
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce r.(source) r.(operation) nonce.
End internal_operation.
Definition internal_operation_skeleton := internal_operation.record.
Module kdescr.
Record record {kloc kbef kaft kinstr : Set} : Set := Build {
kloc : kloc;
kbef : kbef;
kaft : kaft;
kinstr : kinstr;
}.
Arguments record : clear implicits.
Definition with_kloc {t_kloc t_kbef t_kaft t_kinstr} kloc
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr kloc r.(kbef) r.(kaft) r.(kinstr).
Definition with_kbef {t_kloc t_kbef t_kaft t_kinstr} kbef
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) kbef r.(kaft) r.(kinstr).
Definition with_kaft {t_kloc t_kbef t_kaft t_kinstr} kaft
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) kaft r.(kinstr).
Definition with_kinstr {t_kloc t_kbef t_kaft t_kinstr} kinstr
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) r.(kaft) kinstr.
End kdescr.
Definition kdescr_skeleton := kdescr.record.
Module logger.
Record record {log_interp get_log klog ilog log_kinstr : Set} : Set := Build {
log_interp : log_interp;
get_log : get_log;
klog : klog;
ilog : ilog;
log_kinstr : log_kinstr;
}.
Arguments record : clear implicits.
Definition with_log_interp {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
log_interp (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr log_interp
r.(get_log) r.(klog) r.(ilog) r.(log_kinstr).
Definition with_get_log {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
get_log (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
get_log r.(klog) r.(ilog) r.(log_kinstr).
Definition with_klog {t_log_interp t_get_log t_klog t_ilog t_log_kinstr} klog
(r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) klog r.(ilog) r.(log_kinstr).
Definition with_ilog {t_log_interp t_get_log t_klog t_ilog t_log_kinstr} ilog
(r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) r.(klog) ilog r.(log_kinstr).
Definition with_log_kinstr {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
log_kinstr (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) r.(klog) r.(ilog) log_kinstr.
End logger.
Definition logger_skeleton := logger.record.
Module entrypoints.
Record record {root original_type_expr : Set} : Set := Build {
root : root;
original_type_expr : original_type_expr;
}.
Arguments record : clear implicits.
Definition with_root {t_root t_original_type_expr} root
(r : record t_root t_original_type_expr) :=
Build t_root t_original_type_expr root r.(original_type_expr).
Definition with_original_type_expr {t_root t_original_type_expr}
original_type_expr (r : record t_root t_original_type_expr) :=
Build t_root t_original_type_expr r.(root) original_type_expr.
End entrypoints.
Definition entrypoints_skeleton := entrypoints.record.
Reserved Notation "'kinstr.IIf_none".
Reserved Notation "'kinstr.IOpt_map".
Reserved Notation "'kinstr.IIf_left".
Reserved Notation "'kinstr.IIf_cons".
Reserved Notation "'kinstr.IIf".
Reserved Notation "'kinstr.ICreate_contract".
Reserved Notation "'kinstr.IEmit".
Reserved Notation "'typed_contract.Typed_originated".
Reserved Notation "'typed_contract.Typed_tx_rollup".
Reserved Notation "'typed_contract.Typed_sc_rollup".
Reserved Notation "'typed_contract.Typed_zk_rollup".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'internal_operation_contents.Transaction_to_implicit".
Reserved Notation "'internal_operation_contents.Transaction_to_smart_contract".
Reserved Notation "'internal_operation_contents.Transaction_to_tx_rollup".
Reserved Notation "'internal_operation_contents.Transaction_to_sc_rollup".
Reserved Notation "'internal_operation_contents.Event".
Reserved Notation "'internal_operation_contents.Transaction_to_zk_rollup".
Reserved Notation "'internal_operation_contents.Origination".
Reserved Notation "'entrypoints".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'step_type".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".
Inductive kinstr : Set :=
| IDrop : Alpha_context.Script.location → kinstr → kinstr
| IDup : Alpha_context.Script.location → kinstr → kinstr
| ISwap : Alpha_context.Script.location → kinstr → kinstr
| IConst : ∀ {t : Set},
Alpha_context.Script.location → ty → t → kinstr → kinstr
| ICons_pair : Alpha_context.Script.location → kinstr → kinstr
| ICar : Alpha_context.Script.location → kinstr → kinstr
| ICdr : Alpha_context.Script.location → kinstr → kinstr
| IUnpair : Alpha_context.Script.location → kinstr → kinstr
| ICons_some : Alpha_context.Script.location → kinstr → kinstr
| ICons_none : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_none : 'kinstr.IIf_none → kinstr
| IOpt_map : 'kinstr.IOpt_map → kinstr
| ICons_left : Alpha_context.Script.location → ty → kinstr → kinstr
| ICons_right : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_left : 'kinstr.IIf_left → kinstr
| ICons_list : Alpha_context.Script.location → kinstr → kinstr
| INil : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_cons : 'kinstr.IIf_cons → kinstr
| IList_map :
Alpha_context.Script.location → kinstr → option ty → kinstr → kinstr
| IList_iter :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IList_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_set :
Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| ISet_iter :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr →
kinstr
| ISet_mem : Alpha_context.Script.location → kinstr → kinstr
| ISet_update : Alpha_context.Script.location → kinstr → kinstr
| ISet_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_map :
Alpha_context.Script.location → 'comparable_ty → option ty → kinstr →
kinstr
| IMap_map :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IMap_iter :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IMap_mem : Alpha_context.Script.location → kinstr → kinstr
| IMap_get : Alpha_context.Script.location → kinstr → kinstr
| IMap_update : Alpha_context.Script.location → kinstr → kinstr
| IMap_get_and_update : Alpha_context.Script.location → kinstr → kinstr
| IMap_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_big_map :
Alpha_context.Script.location → 'comparable_ty → ty → kinstr → kinstr
| IBig_map_mem : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_get : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_update : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_get_and_update : Alpha_context.Script.location → kinstr → kinstr
| IConcat_string : Alpha_context.Script.location → kinstr → kinstr
| IConcat_string_pair : Alpha_context.Script.location → kinstr → kinstr
| ISlice_string : Alpha_context.Script.location → kinstr → kinstr
| IString_size : Alpha_context.Script.location → kinstr → kinstr
| IConcat_bytes : Alpha_context.Script.location → kinstr → kinstr
| IConcat_bytes_pair : Alpha_context.Script.location → kinstr → kinstr
| ISlice_bytes : Alpha_context.Script.location → kinstr → kinstr
| IBytes_size : Alpha_context.Script.location → kinstr → kinstr
| ILsl_bytes : Alpha_context.Script.location → kinstr → kinstr
| ILsr_bytes : Alpha_context.Script.location → kinstr → kinstr
| IOr_bytes : Alpha_context.Script.location → kinstr → kinstr
| IAnd_bytes : Alpha_context.Script.location → kinstr → kinstr
| IXor_bytes : Alpha_context.Script.location → kinstr → kinstr
| INot_bytes : Alpha_context.Script.location → kinstr → kinstr
| IAdd_seconds_to_timestamp : Alpha_context.Script.location → kinstr → kinstr
| IAdd_timestamp_to_seconds : Alpha_context.Script.location → kinstr → kinstr
| ISub_timestamp_seconds : Alpha_context.Script.location → kinstr → kinstr
| IDiff_timestamps : Alpha_context.Script.location → kinstr → kinstr
| IAdd_tez : Alpha_context.Script.location → kinstr → kinstr
| ISub_tez : Alpha_context.Script.location → kinstr → kinstr
| ISub_tez_legacy : Alpha_context.Script.location → kinstr → kinstr
| IMul_teznat : Alpha_context.Script.location → kinstr → kinstr
| IMul_nattez : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_teznat : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_tez : Alpha_context.Script.location → kinstr → kinstr
| IOr : Alpha_context.Script.location → kinstr → kinstr
| IAnd : Alpha_context.Script.location → kinstr → kinstr
| IXor : Alpha_context.Script.location → kinstr → kinstr
| INot : Alpha_context.Script.location → kinstr → kinstr
| IIs_nat : Alpha_context.Script.location → kinstr → kinstr
| INeg : Alpha_context.Script.location → kinstr → kinstr
| IAbs_int : Alpha_context.Script.location → kinstr → kinstr
| IInt_nat : Alpha_context.Script.location → kinstr → kinstr
| IAdd_int : Alpha_context.Script.location → kinstr → kinstr
| IAdd_nat : Alpha_context.Script.location → kinstr → kinstr
| ISub_int : Alpha_context.Script.location → kinstr → kinstr
| IMul_int : Alpha_context.Script.location → kinstr → kinstr
| IMul_nat : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_int : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_nat : Alpha_context.Script.location → kinstr → kinstr
| ILsl_nat : Alpha_context.Script.location → kinstr → kinstr
| ILsr_nat : Alpha_context.Script.location → kinstr → kinstr
| IOr_nat : Alpha_context.Script.location → kinstr → kinstr
| IAnd_nat : Alpha_context.Script.location → kinstr → kinstr
| IAnd_int_nat : Alpha_context.Script.location → kinstr → kinstr
| IXor_nat : Alpha_context.Script.location → kinstr → kinstr
| INot_int : Alpha_context.Script.location → kinstr → kinstr
| IIf : 'kinstr.IIf → kinstr
| ILoop : Alpha_context.Script.location → kinstr → kinstr → kinstr
| ILoop_left : Alpha_context.Script.location → kinstr → kinstr → kinstr
| IDip :
Alpha_context.Script.location → kinstr → option ty → kinstr → kinstr
| IExec : Alpha_context.Script.location → option stack_ty → kinstr → kinstr
| IApply : Alpha_context.Script.location → ty → kinstr → kinstr
| ILambda : Alpha_context.Script.location → lambda → kinstr → kinstr
| IFailwith : Alpha_context.Script.location → ty → kinstr
| ICompare : Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| IEq : Alpha_context.Script.location → kinstr → kinstr
| INeq : Alpha_context.Script.location → kinstr → kinstr
| ILt : Alpha_context.Script.location → kinstr → kinstr
| IGt : Alpha_context.Script.location → kinstr → kinstr
| ILe : Alpha_context.Script.location → kinstr → kinstr
| IGe : Alpha_context.Script.location → kinstr → kinstr
| IAddress : Alpha_context.Script.location → kinstr → kinstr
| IContract :
Alpha_context.Script.location → ty → Alpha_context.Entrypoint.t → kinstr →
kinstr
| IView :
Alpha_context.Script.location → view_signature → option stack_ty →
kinstr → kinstr
| ITransfer_tokens : Alpha_context.Script.location → kinstr → kinstr
| IImplicit_account : Alpha_context.Script.location → kinstr → kinstr
| ICreate_contract : 'kinstr.ICreate_contract → kinstr
| ISet_delegate : Alpha_context.Script.location → kinstr → kinstr
| INow : Alpha_context.Script.location → kinstr → kinstr
| IMin_block_time : Alpha_context.Script.location → kinstr → kinstr
| IBalance : Alpha_context.Script.location → kinstr → kinstr
| ILevel : Alpha_context.Script.location → kinstr → kinstr
| ICheck_signature : Alpha_context.Script.location → kinstr → kinstr
| IHash_key : Alpha_context.Script.location → kinstr → kinstr
| IPack : Alpha_context.Script.location → ty → kinstr → kinstr
| IUnpack : Alpha_context.Script.location → ty → kinstr → kinstr
| IBlake2b : Alpha_context.Script.location → kinstr → kinstr
| ISha256 : Alpha_context.Script.location → kinstr → kinstr
| ISha512 : Alpha_context.Script.location → kinstr → kinstr
| ISource : Alpha_context.Script.location → kinstr → kinstr
| ISender : Alpha_context.Script.location → kinstr → kinstr
| ISelf :
Alpha_context.Script.location → ty → Alpha_context.Entrypoint.t → kinstr →
kinstr
| ISelf_address : Alpha_context.Script.location → kinstr → kinstr
| IAmount : Alpha_context.Script.location → kinstr → kinstr
| ISapling_empty_state :
Alpha_context.Script.location → Alpha_context.Sapling.Memo_size.t →
kinstr → kinstr
| ISapling_verify_update : Alpha_context.Script.location → kinstr → kinstr
| ISapling_verify_update_deprecated :
Alpha_context.Script.location → kinstr → kinstr
| IDig :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IDug :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IDipn :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr → kinstr
| IDropn :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IChainId : Alpha_context.Script.location → kinstr → kinstr
| INever : Alpha_context.Script.location → kinstr
| IVoting_power : Alpha_context.Script.location → kinstr → kinstr
| ITotal_voting_power : Alpha_context.Script.location → kinstr → kinstr
| IKeccak : Alpha_context.Script.location → kinstr → kinstr
| ISha3 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_z_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_fr_z : Alpha_context.Script.location → kinstr → kinstr
| IInt_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IPairing_check_bls12_381 : Alpha_context.Script.location → kinstr → kinstr
| IComb :
Alpha_context.Script.location → int → comb_gadt_witness → kinstr → kinstr
| IUncomb :
Alpha_context.Script.location → int → uncomb_gadt_witness → kinstr →
kinstr
| IComb_get :
Alpha_context.Script.location → int → comb_get_gadt_witness → kinstr →
kinstr
| IComb_set :
Alpha_context.Script.location → int → comb_set_gadt_witness → kinstr →
kinstr
| IDup_n :
Alpha_context.Script.location → int → dup_n_gadt_witness → kinstr → kinstr
| ITicket :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| ITicket_deprecated :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| IRead_ticket :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| ISplit_ticket : Alpha_context.Script.location → kinstr → kinstr
| IJoin_tickets :
Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| IOpen_chest : Alpha_context.Script.location → kinstr → kinstr
| IEmit : 'kinstr.IEmit → kinstr
| IHalt : Alpha_context.Script.location → kinstr
| ILog :
Alpha_context.Script.location → stack_ty → logging_event → 'logger →
kinstr → kinstr
with lambda : Set :=
| Lam : 'kdescr → Alpha_context.Script.node → lambda
| LamRec : 'kdescr → Alpha_context.Script.node → lambda
with typed_contract : Set :=
| Typed_implicit : Alpha_context.public_key_hash → typed_contract
| Typed_originated : 'typed_contract.Typed_originated → typed_contract
| Typed_tx_rollup : 'typed_contract.Typed_tx_rollup → typed_contract
| Typed_sc_rollup : 'typed_contract.Typed_sc_rollup → typed_contract
| Typed_zk_rollup : 'typed_contract.Typed_zk_rollup → typed_contract
with continuation : Set :=
| KNil : continuation
| KCons : kinstr → continuation → continuation
| KReturn : ∀ {s : Set},
s → option stack_ty → continuation → continuation
| KMap_head : ∀ {a b : Set}, (a → b) → continuation → continuation
| KUndip : ∀ {b : Set}, b → option ty → continuation → continuation
| KLoop_in : kinstr → continuation → continuation
| KLoop_in_left : kinstr → continuation → continuation
| KIter : ∀ {a : Set},
kinstr → option ty → list a → continuation → continuation
| KList_enter_body : ∀ {a b : Set},
kinstr → list a → Script_list.t b → option ty → int → continuation →
continuation
| KList_exit_body : ∀ {a b : Set},
kinstr → list a → Script_list.t b → option ty → int → continuation →
continuation
| KMap_enter_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → option ty → continuation → continuation
| KMap_exit_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → a → option ty → continuation →
continuation
| KView_exit : step_constants → continuation → continuation
| KLog : continuation → stack_ty → 'logger → continuation
with klog : Set :=
| Klog : ∀ {a s r f : Set},
('logger → Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → stack_ty → continuation →
continuation → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter)) → klog
with ilog : Set :=
| Ilog : ∀ {a s r f : Set},
('logger → logging_event → stack_ty → 'step_type a s r f) → ilog
with log_kinstr : Set :=
| Log_kinstr : ('logger → stack_ty → kinstr → kinstr) → log_kinstr
with ty : Set :=
| Unit_t : ty
| Int_t : ty
| Nat_t : ty
| Signature_t : ty
| String_t : ty
| Bytes_t : ty
| Mutez_t : ty
| Key_hash_t : ty
| Key_t : ty
| Timestamp_t : ty
| Address_t : ty
| Tx_rollup_l2_address_t : ty
| Bool_t : ty
| Pair_t : ty → ty → ty_metadata → Dependent_bool.dand → ty
| Union_t : ty → ty → ty_metadata → Dependent_bool.dand → ty
| Lambda_t : ty → ty → ty_metadata → ty
| Option_t : ty → ty_metadata → Dependent_bool.dbool → ty
| List_t : ty → ty_metadata → ty
| Set_t : 'comparable_ty → ty_metadata → ty
| Map_t : 'comparable_ty → ty → ty_metadata → ty
| Big_map_t : 'comparable_ty → ty → ty_metadata → ty
| Contract_t : ty → ty_metadata → ty
| Sapling_transaction_t : Alpha_context.Sapling.Memo_size.t → ty
| Sapling_transaction_deprecated_t : Alpha_context.Sapling.Memo_size.t → ty
| Sapling_state_t : Alpha_context.Sapling.Memo_size.t → ty
| Operation_t : ty
| Chain_id_t : ty
| Never_t : ty
| Bls12_381_g1_t : ty
| Bls12_381_g2_t : ty
| Bls12_381_fr_t : ty
| Ticket_t : 'comparable_ty → ty_metadata → ty
| Chest_key_t : ty
| Chest_t : ty
with stack_ty : Set :=
| Item_t : ty → stack_ty → stack_ty
| Bot_t : stack_ty
with big_map : Set :=
| Big_map : ∀ {key value : Set}, 'big_map.Big_map key value → big_map
with stack_prefix_preservation_witness : Set :=
| KPrefix :
Alpha_context.Script.location → ty → stack_prefix_preservation_witness →
stack_prefix_preservation_witness
| KRest : stack_prefix_preservation_witness
with comb_gadt_witness : Set :=
| Comb_one : comb_gadt_witness
| Comb_succ : comb_gadt_witness → comb_gadt_witness
with uncomb_gadt_witness : Set :=
| Uncomb_one : uncomb_gadt_witness
| Uncomb_succ : uncomb_gadt_witness → uncomb_gadt_witness
with comb_get_gadt_witness : Set :=
| Comb_get_zero : comb_get_gadt_witness
| Comb_get_one : comb_get_gadt_witness
| Comb_get_plus_two : comb_get_gadt_witness → comb_get_gadt_witness
with comb_set_gadt_witness : Set :=
| Comb_set_zero : comb_set_gadt_witness
| Comb_set_one : comb_set_gadt_witness
| Comb_set_plus_two : comb_set_gadt_witness → comb_set_gadt_witness
with dup_n_gadt_witness : Set :=
| Dup_n_zero : dup_n_gadt_witness
| Dup_n_succ : dup_n_gadt_witness → dup_n_gadt_witness
with view_signature : Set :=
| View_signature : 'view_signature.View_signature → view_signature
with internal_operation_contents : Set :=
| Transaction_to_implicit :
'internal_operation_contents.Transaction_to_implicit →
internal_operation_contents
| Transaction_to_smart_contract : ∀ {a : Set},
'internal_operation_contents.Transaction_to_smart_contract a →
internal_operation_contents
| Transaction_to_tx_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_tx_rollup a →
internal_operation_contents
| Transaction_to_sc_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_sc_rollup a →
internal_operation_contents
| Event : 'internal_operation_contents.Event → internal_operation_contents
| Transaction_to_zk_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_zk_rollup a →
internal_operation_contents
| Origination : ∀ {storage : Set},
'internal_operation_contents.Origination storage →
internal_operation_contents
| Delegation : option Signature.public_key_hash → internal_operation_contents
with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation → packed_internal_operation
where "'entrypoints" :=
(entrypoints_skeleton entrypoints_node Alpha_context.Script.node)
and "'logging_function" :=
(fun (t_c t_u : Set) ⇒ kinstr → Alpha_context.context →
Alpha_context.Script.location → stack_ty → t_c × t_u → unit)
and "'execution_trace" :=
(list
(Alpha_context.Script.location × Alpha_context.Gas.Arith.fp ×
list Alpha_context.Script.expr))
and "'step_type" :=
(fun (t_a t_s t_r t_f : Set) ⇒ Local_gas_counter.outdated_context ×
step_constants → Local_gas_counter.local_gas_counter → kinstr →
continuation → t_a → t_s →
M?
(t_r × t_f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter))
and "'comparable_ty" := ((fun _ ⇒ ty) tt)
and "'kdescr" :=
(kdescr_skeleton Alpha_context.Script.location stack_ty stack_ty kinstr)
and "'internal_operation" :=
(internal_operation_skeleton Alpha_context.Contract.t
internal_operation_contents int)
and "'operation" :=
(operation_skeleton packed_internal_operation
(option Alpha_context.Lazy_storage.diffs))
and "'logger" :=
(logger_skeleton (∀ {c u : Set}, 'logging_function c u)
(unit → M? (option 'execution_trace)) klog ilog log_kinstr)
and "'kinstr.IIf_none" :=
(kinstr.IIf_none_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IOpt_map" :=
(kinstr.IOpt_map_skeleton Alpha_context.Script.location kinstr kinstr)
and "'kinstr.IIf_left" :=
(kinstr.IIf_left_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf_cons" :=
(kinstr.IIf_cons_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf" :=
(kinstr.IIf_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
(kinstr.ICreate_contract_skeleton Alpha_context.Script.location ty
Alpha_context.Script.expr kinstr)
and "'kinstr.IEmit" :=
(kinstr.IEmit_skeleton Alpha_context.Script.location
Alpha_context.Entrypoint.t ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_originated" :=
(typed_contract.Typed_originated_skeleton ty Contract_hash.t
Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_tx_rollup" :=
(typed_contract.Typed_tx_rollup_skeleton ty Alpha_context.Tx_rollup.t)
and "'typed_contract.Typed_sc_rollup" :=
(typed_contract.Typed_sc_rollup_skeleton ty Alpha_context.Sc_rollup.t
Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_zk_rollup" :=
(typed_contract.Typed_zk_rollup_skeleton ty Alpha_context.Zk_rollup.t)
and "'big_map.Big_map" :=
(fun (t_key t_value : Set) ⇒ big_map.Big_map_skeleton
(option Alpha_context.Big_map.Id.t) (big_map_overlay t_key t_value)
'comparable_ty ty)
and "'view_signature.View_signature" :=
(view_signature.View_signature_skeleton Script_string.t ty ty)
and "'internal_operation_contents.Transaction_to_implicit" :=
(internal_operation_contents.Transaction_to_implicit_skeleton
Signature.public_key_hash Alpha_context.Tez.tez)
and "'internal_operation_contents.Transaction_to_smart_contract" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_smart_contract_skeleton
Contract_hash.t Alpha_context.Tez.tez Alpha_context.Entrypoint.t
Alpha_context.Script.location ty t_a Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_tx_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_tx_rollup_skeleton
Alpha_context.Tx_rollup.t ty (pair (ticket t_a) tx_rollup_l2_address)
Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_sc_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_sc_rollup_skeleton
Alpha_context.Sc_rollup.t Alpha_context.Entrypoint.t ty t_a
Alpha_context.Script.expr)
and "'internal_operation_contents.Event" :=
(internal_operation_contents.Event_skeleton Alpha_context.Script.expr
Alpha_context.Entrypoint.t Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_zk_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_zk_rollup_skeleton
Alpha_context.Zk_rollup.t ty (pair (ticket t_a) bytes)
Alpha_context.Script.expr)
and "'internal_operation_contents.Origination" :=
(fun (t_storage : Set) ⇒ internal_operation_contents.Origination_skeleton
(option Signature.public_key_hash) Alpha_context.Script.expr
Alpha_context.Script.expr Alpha_context.Tez.tez Contract_hash.t ty t_storage).
Module kinstr.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.kinstr.
Definition IIf_none := 'kinstr.IIf_none.
Definition IOpt_map := 'kinstr.IOpt_map.
Definition IIf_left := 'kinstr.IIf_left.
Definition IIf_cons := 'kinstr.IIf_cons.
Definition IIf := 'kinstr.IIf.
Definition ICreate_contract := 'kinstr.ICreate_contract.
Definition IEmit := 'kinstr.IEmit.
End kinstr.
Module typed_contract.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.typed_contract.
Definition Typed_originated := 'typed_contract.Typed_originated.
Definition Typed_tx_rollup := 'typed_contract.Typed_tx_rollup.
Definition Typed_sc_rollup := 'typed_contract.Typed_sc_rollup.
Definition Typed_zk_rollup := 'typed_contract.Typed_zk_rollup.
End typed_contract.
Module big_map.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.big_map.
Definition Big_map := 'big_map.Big_map.
End big_map.
Module view_signature.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.view_signature.
Definition View_signature := 'view_signature.View_signature.
End view_signature.
Module internal_operation_contents.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.internal_operation_contents.
Definition Transaction_to_implicit :=
'internal_operation_contents.Transaction_to_implicit.
Definition Transaction_to_smart_contract :=
'internal_operation_contents.Transaction_to_smart_contract.
Definition Transaction_to_tx_rollup :=
'internal_operation_contents.Transaction_to_tx_rollup.
Definition Transaction_to_sc_rollup :=
'internal_operation_contents.Transaction_to_sc_rollup.
Definition Event := 'internal_operation_contents.Event.
Definition Transaction_to_zk_rollup :=
'internal_operation_contents.Transaction_to_zk_rollup.
Definition Origination := 'internal_operation_contents.Origination.
End internal_operation_contents.
Definition entrypoints := 'entrypoints.
Definition logging_function := 'logging_function.
Definition execution_trace := 'execution_trace.
Definition logger := 'logger.
Definition step_type := 'step_type.
Definition comparable_ty := 'comparable_ty.
Definition kdescr := 'kdescr.
Definition internal_operation := 'internal_operation.
Definition operation := 'operation.
Inductive ex_ty : Set :=
| Ex_ty : ty → ex_ty.
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Module kinstr.
Module IIf_none.
Record record {loc branch_if_none branch_if_some k : Set} : Set := Build {
loc : loc;
branch_if_none : branch_if_none;
branch_if_some : branch_if_some;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_none t_branch_if_some t_k} loc
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k loc r.(branch_if_none)
r.(branch_if_some) r.(k).
Definition with_branch_if_none
{t_loc t_branch_if_none t_branch_if_some t_k} branch_if_none
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc) branch_if_none
r.(branch_if_some) r.(k).
Definition with_branch_if_some
{t_loc t_branch_if_none t_branch_if_some t_k} branch_if_some
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
r.(branch_if_none) branch_if_some r.(k).
Definition with_k {t_loc t_branch_if_none t_branch_if_some t_k} k
(r : record t_loc t_branch_if_none t_branch_if_some t_k) :=
Build t_loc t_branch_if_none t_branch_if_some t_k r.(loc)
r.(branch_if_none) r.(branch_if_some) k.
End IIf_none.
Definition IIf_none_skeleton := IIf_none.record.
Module IOpt_map.
Record record {loc body k : Set} : Set := Build {
loc : loc;
body : body;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_body t_k} loc
(r : record t_loc t_body t_k) :=
Build t_loc t_body t_k loc r.(body) r.(k).
Definition with_body {t_loc t_body t_k} body
(r : record t_loc t_body t_k) :=
Build t_loc t_body t_k r.(loc) body r.(k).
Definition with_k {t_loc t_body t_k} k (r : record t_loc t_body t_k) :=
Build t_loc t_body t_k r.(loc) r.(body) k.
End IOpt_map.
Definition IOpt_map_skeleton := IOpt_map.record.
Module IIf_left.
Record record {loc branch_if_left branch_if_right k : Set} : Set := Build {
loc : loc;
branch_if_left : branch_if_left;
branch_if_right : branch_if_right;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_left t_branch_if_right t_k} loc
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k loc
r.(branch_if_left) r.(branch_if_right) r.(k).
Definition with_branch_if_left
{t_loc t_branch_if_left t_branch_if_right t_k} branch_if_left
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
branch_if_left r.(branch_if_right) r.(k).
Definition with_branch_if_right
{t_loc t_branch_if_left t_branch_if_right t_k} branch_if_right
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
r.(branch_if_left) branch_if_right r.(k).
Definition with_k {t_loc t_branch_if_left t_branch_if_right t_k} k
(r : record t_loc t_branch_if_left t_branch_if_right t_k) :=
Build t_loc t_branch_if_left t_branch_if_right t_k r.(loc)
r.(branch_if_left) r.(branch_if_right) k.
End IIf_left.
Definition IIf_left_skeleton := IIf_left.record.
Module IIf_cons.
Record record {loc branch_if_cons branch_if_nil k : Set} : Set := Build {
loc : loc;
branch_if_cons : branch_if_cons;
branch_if_nil : branch_if_nil;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_cons t_branch_if_nil t_k} loc
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k loc r.(branch_if_cons)
r.(branch_if_nil) r.(k).
Definition with_branch_if_cons
{t_loc t_branch_if_cons t_branch_if_nil t_k} branch_if_cons
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc) branch_if_cons
r.(branch_if_nil) r.(k).
Definition with_branch_if_nil {t_loc t_branch_if_cons t_branch_if_nil t_k}
branch_if_nil (r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
r.(branch_if_cons) branch_if_nil r.(k).
Definition with_k {t_loc t_branch_if_cons t_branch_if_nil t_k} k
(r : record t_loc t_branch_if_cons t_branch_if_nil t_k) :=
Build t_loc t_branch_if_cons t_branch_if_nil t_k r.(loc)
r.(branch_if_cons) r.(branch_if_nil) k.
End IIf_cons.
Definition IIf_cons_skeleton := IIf_cons.record.
Module IIf.
Record record {loc branch_if_true branch_if_false k : Set} : Set := Build {
loc : loc;
branch_if_true : branch_if_true;
branch_if_false : branch_if_false;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_branch_if_true t_branch_if_false t_k} loc
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k loc
r.(branch_if_true) r.(branch_if_false) r.(k).
Definition with_branch_if_true
{t_loc t_branch_if_true t_branch_if_false t_k} branch_if_true
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
branch_if_true r.(branch_if_false) r.(k).
Definition with_branch_if_false
{t_loc t_branch_if_true t_branch_if_false t_k} branch_if_false
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
r.(branch_if_true) branch_if_false r.(k).
Definition with_k {t_loc t_branch_if_true t_branch_if_false t_k} k
(r : record t_loc t_branch_if_true t_branch_if_false t_k) :=
Build t_loc t_branch_if_true t_branch_if_false t_k r.(loc)
r.(branch_if_true) r.(branch_if_false) k.
End IIf.
Definition IIf_skeleton := IIf.record.
Module ICreate_contract.
Record record {loc storage_type code k : Set} : Set := Build {
loc : loc;
storage_type : storage_type;
code : code;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_storage_type t_code t_k} loc
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k loc r.(storage_type) r.(code)
r.(k).
Definition with_storage_type {t_loc t_storage_type t_code t_k}
storage_type (r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) storage_type r.(code)
r.(k).
Definition with_code {t_loc t_storage_type t_code t_k} code
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) code
r.(k).
Definition with_k {t_loc t_storage_type t_code t_k} k
(r : record t_loc t_storage_type t_code t_k) :=
Build t_loc t_storage_type t_code t_k r.(loc) r.(storage_type) r.(code)
k.
End ICreate_contract.
Definition ICreate_contract_skeleton := ICreate_contract.record.
Module IEmit.
Record record {loc tag ty unparsed_ty k : Set} : Set := Build {
loc : loc;
tag : tag;
ty : ty;
unparsed_ty : unparsed_ty;
k : k;
}.
Arguments record : clear implicits.
Definition with_loc {t_loc t_tag t_ty t_unparsed_ty t_k} loc
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k loc r.(tag) r.(ty)
r.(unparsed_ty) r.(k).
Definition with_tag {t_loc t_tag t_ty t_unparsed_ty t_k} tag
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) tag r.(ty)
r.(unparsed_ty) r.(k).
Definition with_ty {t_loc t_tag t_ty t_unparsed_ty t_k} ty
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) ty
r.(unparsed_ty) r.(k).
Definition with_unparsed_ty {t_loc t_tag t_ty t_unparsed_ty t_k}
unparsed_ty (r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
unparsed_ty r.(k).
Definition with_k {t_loc t_tag t_ty t_unparsed_ty t_k} k
(r : record t_loc t_tag t_ty t_unparsed_ty t_k) :=
Build t_loc t_tag t_ty t_unparsed_ty t_k r.(loc) r.(tag) r.(ty)
r.(unparsed_ty) k.
End IEmit.
Definition IEmit_skeleton := IEmit.record.
End kinstr.
Module typed_contract.
Module Typed_originated.
Record record {arg_ty contract_hash entrypoint : Set} : Set := Build {
arg_ty : arg_ty;
contract_hash : contract_hash;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_contract_hash t_entrypoint} arg_ty
(r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint arg_ty r.(contract_hash)
r.(entrypoint).
Definition with_contract_hash {t_arg_ty t_contract_hash t_entrypoint}
contract_hash (r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) contract_hash
r.(entrypoint).
Definition with_entrypoint {t_arg_ty t_contract_hash t_entrypoint}
entrypoint (r : record t_arg_ty t_contract_hash t_entrypoint) :=
Build t_arg_ty t_contract_hash t_entrypoint r.(arg_ty) r.(contract_hash)
entrypoint.
End Typed_originated.
Definition Typed_originated_skeleton := Typed_originated.record.
Module Typed_tx_rollup.
Record record {arg_ty tx_rollup : Set} : Set := Build {
arg_ty : arg_ty;
tx_rollup : tx_rollup;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_tx_rollup} arg_ty
(r : record t_arg_ty t_tx_rollup) :=
Build t_arg_ty t_tx_rollup arg_ty r.(tx_rollup).
Definition with_tx_rollup {t_arg_ty t_tx_rollup} tx_rollup
(r : record t_arg_ty t_tx_rollup) :=
Build t_arg_ty t_tx_rollup r.(arg_ty) tx_rollup.
End Typed_tx_rollup.
Definition Typed_tx_rollup_skeleton := Typed_tx_rollup.record.
Module Typed_sc_rollup.
Record record {arg_ty sc_rollup entrypoint : Set} : Set := Build {
arg_ty : arg_ty;
sc_rollup : sc_rollup;
entrypoint : entrypoint;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_sc_rollup t_entrypoint} arg_ty
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint arg_ty r.(sc_rollup)
r.(entrypoint).
Definition with_sc_rollup {t_arg_ty t_sc_rollup t_entrypoint} sc_rollup
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) sc_rollup
r.(entrypoint).
Definition with_entrypoint {t_arg_ty t_sc_rollup t_entrypoint} entrypoint
(r : record t_arg_ty t_sc_rollup t_entrypoint) :=
Build t_arg_ty t_sc_rollup t_entrypoint r.(arg_ty) r.(sc_rollup)
entrypoint.
End Typed_sc_rollup.
Definition Typed_sc_rollup_skeleton := Typed_sc_rollup.record.
Module Typed_zk_rollup.
Record record {arg_ty zk_rollup : Set} : Set := Build {
arg_ty : arg_ty;
zk_rollup : zk_rollup;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_zk_rollup} arg_ty
(r : record t_arg_ty t_zk_rollup) :=
Build t_arg_ty t_zk_rollup arg_ty r.(zk_rollup).
Definition with_zk_rollup {t_arg_ty t_zk_rollup} zk_rollup
(r : record t_arg_ty t_zk_rollup) :=
Build t_arg_ty t_zk_rollup r.(arg_ty) zk_rollup.
End Typed_zk_rollup.
Definition Typed_zk_rollup_skeleton := Typed_zk_rollup.record.
End typed_contract.
Module big_map.
Module Big_map.
Record record {id diff key_type value_type : Set} : Set := Build {
id : id;
diff : diff;
key_type : key_type;
value_type : value_type;
}.
Arguments record : clear implicits.
Definition with_id {t_id t_diff t_key_type t_value_type} id
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type id r.(diff) r.(key_type)
r.(value_type).
Definition with_diff {t_id t_diff t_key_type t_value_type} diff
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) diff r.(key_type)
r.(value_type).
Definition with_key_type {t_id t_diff t_key_type t_value_type} key_type
(r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) key_type
r.(value_type).
Definition with_value_type {t_id t_diff t_key_type t_value_type}
value_type (r : record t_id t_diff t_key_type t_value_type) :=
Build t_id t_diff t_key_type t_value_type r.(id) r.(diff) r.(key_type)
value_type.
End Big_map.
Definition Big_map_skeleton := Big_map.record.
End big_map.
Module view_signature.
Module View_signature.
Record record {name input_ty output_ty : Set} : Set := Build {
name : name;
input_ty : input_ty;
output_ty : output_ty;
}.
Arguments record : clear implicits.
Definition with_name {t_name t_input_ty t_output_ty} name
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty name r.(input_ty) r.(output_ty).
Definition with_input_ty {t_name t_input_ty t_output_ty} input_ty
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty r.(name) input_ty r.(output_ty).
Definition with_output_ty {t_name t_input_ty t_output_ty} output_ty
(r : record t_name t_input_ty t_output_ty) :=
Build t_name t_input_ty t_output_ty r.(name) r.(input_ty) output_ty.
End View_signature.
Definition View_signature_skeleton := View_signature.record.
End view_signature.
Module internal_operation_contents.
Module Transaction_to_implicit.
Record record {destination amount : Set} : Set := Build {
destination : destination;
amount : amount;
}.
Arguments record : clear implicits.
Definition with_destination {t_destination t_amount} destination
(r : record t_destination t_amount) :=
Build t_destination t_amount destination r.(amount).
Definition with_amount {t_destination t_amount} amount
(r : record t_destination t_amount) :=
Build t_destination t_amount r.(destination) amount.
End Transaction_to_implicit.
Definition Transaction_to_implicit_skeleton :=
Transaction_to_implicit.record.
Module Transaction_to_smart_contract.
Record record {destination amount entrypoint location parameters_ty
parameters unparsed_parameters : Set} : Set := Build {
destination : destination;
amount : amount;
entrypoint : entrypoint;
location : location;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} destination
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters destination r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_amount
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} amount
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) amount
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_entrypoint
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} entrypoint
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
entrypoint r.(location) r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_location
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} location
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) location r.(parameters_ty) r.(parameters)
r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} parameters_ty
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) parameters_ty r.(parameters)
r.(unparsed_parameters).
Definition with_parameters
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} parameters
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) parameters
r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters} unparsed_parameters
(r :
record t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters) :=
Build t_destination t_amount t_entrypoint t_location t_parameters_ty
t_parameters t_unparsed_parameters r.(destination) r.(amount)
r.(entrypoint) r.(location) r.(parameters_ty) r.(parameters)
unparsed_parameters.
End Transaction_to_smart_contract.
Definition Transaction_to_smart_contract_skeleton :=
Transaction_to_smart_contract.record.
Module Transaction_to_tx_rollup.
Record record {destination parameters_ty parameters unparsed_parameters :
Set} : Set := Build {
destination : destination;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
destination
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters_ty
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
unparsed_parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
End Transaction_to_tx_rollup.
Definition Transaction_to_tx_rollup_skeleton :=
Transaction_to_tx_rollup.record.
Module Transaction_to_sc_rollup.
Record record {destination entrypoint parameters_ty parameters
unparsed_parameters : Set} : Set := Build {
destination : destination;
entrypoint : entrypoint;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} destination
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters destination r.(entrypoint) r.(parameters_ty)
r.(parameters) r.(unparsed_parameters).
Definition with_entrypoint
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} entrypoint
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) entrypoint r.(parameters_ty)
r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} parameters_ty
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) parameters_ty
r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} parameters
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters} unparsed_parameters
(r :
record t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_entrypoint t_parameters_ty t_parameters
t_unparsed_parameters r.(destination) r.(entrypoint) r.(parameters_ty)
r.(parameters) unparsed_parameters.
End Transaction_to_sc_rollup.
Definition Transaction_to_sc_rollup_skeleton :=
Transaction_to_sc_rollup.record.
Module Event.
Record record {ty tag unparsed_data : Set} : Set := Build {
ty : ty;
tag : tag;
unparsed_data : unparsed_data;
}.
Arguments record : clear implicits.
Definition with_ty {t_ty t_tag t_unparsed_data} ty
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data ty r.(tag) r.(unparsed_data).
Definition with_tag {t_ty t_tag t_unparsed_data} tag
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data r.(ty) tag r.(unparsed_data).
Definition with_unparsed_data {t_ty t_tag t_unparsed_data} unparsed_data
(r : record t_ty t_tag t_unparsed_data) :=
Build t_ty t_tag t_unparsed_data r.(ty) r.(tag) unparsed_data.
End Event.
Definition Event_skeleton := Event.record.
Module Transaction_to_zk_rollup.
Record record {destination parameters_ty parameters unparsed_parameters :
Set} : Set := Build {
destination : destination;
parameters_ty : parameters_ty;
parameters : parameters;
unparsed_parameters : unparsed_parameters;
}.
Arguments record : clear implicits.
Definition with_destination
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
destination
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
destination r.(parameters_ty) r.(parameters) r.(unparsed_parameters).
Definition with_parameters_ty
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters_ty
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) parameters_ty r.(parameters) r.(unparsed_parameters).
Definition with_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) parameters r.(unparsed_parameters).
Definition with_unparsed_parameters
{t_destination t_parameters_ty t_parameters t_unparsed_parameters}
unparsed_parameters
(r :
record t_destination t_parameters_ty t_parameters
t_unparsed_parameters) :=
Build t_destination t_parameters_ty t_parameters t_unparsed_parameters
r.(destination) r.(parameters_ty) r.(parameters) unparsed_parameters.
End Transaction_to_zk_rollup.
Definition Transaction_to_zk_rollup_skeleton :=
Transaction_to_zk_rollup.record.
Module Origination.
Record record {delegate code unparsed_storage credit preorigination
storage_type storage : Set} : Set := Build {
delegate : delegate;
code : code;
unparsed_storage : unparsed_storage;
credit : credit;
preorigination : preorigination;
storage_type : storage_type;
storage : storage;
}.
Arguments record : clear implicits.
Definition with_delegate
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} delegate
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage delegate r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_code
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} code
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) code r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_unparsed_storage
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} unparsed_storage
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) unparsed_storage
r.(credit) r.(preorigination) r.(storage_type) r.(storage).
Definition with_credit
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} credit
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
credit r.(preorigination) r.(storage_type) r.(storage).
Definition with_preorigination
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} preorigination
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) preorigination r.(storage_type) r.(storage).
Definition with_storage_type
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} storage_type
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) storage_type r.(storage).
Definition with_storage
{t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage} storage
(r :
record t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage) :=
Build t_delegate t_code t_unparsed_storage t_credit t_preorigination
t_storage_type t_storage r.(delegate) r.(code) r.(unparsed_storage)
r.(credit) r.(preorigination) r.(storage_type) storage.
End Origination.
Definition Origination_skeleton := Origination.record.
End internal_operation_contents.
End
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Import
ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.
Module operation.
Record record {piop lazy_storage_diff : Set} : Set := Build {
piop : piop;
lazy_storage_diff : lazy_storage_diff;
}.
Arguments record : clear implicits.
Definition with_piop {t_piop t_lazy_storage_diff} piop
(r : record t_piop t_lazy_storage_diff) :=
Build t_piop t_lazy_storage_diff piop r.(lazy_storage_diff).
Definition with_lazy_storage_diff {t_piop t_lazy_storage_diff}
lazy_storage_diff (r : record t_piop t_lazy_storage_diff) :=
Build t_piop t_lazy_storage_diff r.(piop) lazy_storage_diff.
End operation.
Definition operation_skeleton := operation.record.
Module internal_operation.
Record record {source operation nonce : Set} : Set := Build {
source : source;
operation : operation;
nonce : nonce;
}.
Arguments record : clear implicits.
Definition with_source {t_source t_operation t_nonce} source
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce source r.(operation) r.(nonce).
Definition with_operation {t_source t_operation t_nonce} operation
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce r.(source) operation r.(nonce).
Definition with_nonce {t_source t_operation t_nonce} nonce
(r : record t_source t_operation t_nonce) :=
Build t_source t_operation t_nonce r.(source) r.(operation) nonce.
End internal_operation.
Definition internal_operation_skeleton := internal_operation.record.
Module kdescr.
Record record {kloc kbef kaft kinstr : Set} : Set := Build {
kloc : kloc;
kbef : kbef;
kaft : kaft;
kinstr : kinstr;
}.
Arguments record : clear implicits.
Definition with_kloc {t_kloc t_kbef t_kaft t_kinstr} kloc
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr kloc r.(kbef) r.(kaft) r.(kinstr).
Definition with_kbef {t_kloc t_kbef t_kaft t_kinstr} kbef
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) kbef r.(kaft) r.(kinstr).
Definition with_kaft {t_kloc t_kbef t_kaft t_kinstr} kaft
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) kaft r.(kinstr).
Definition with_kinstr {t_kloc t_kbef t_kaft t_kinstr} kinstr
(r : record t_kloc t_kbef t_kaft t_kinstr) :=
Build t_kloc t_kbef t_kaft t_kinstr r.(kloc) r.(kbef) r.(kaft) kinstr.
End kdescr.
Definition kdescr_skeleton := kdescr.record.
Module logger.
Record record {log_interp get_log klog ilog log_kinstr : Set} : Set := Build {
log_interp : log_interp;
get_log : get_log;
klog : klog;
ilog : ilog;
log_kinstr : log_kinstr;
}.
Arguments record : clear implicits.
Definition with_log_interp {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
log_interp (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr log_interp
r.(get_log) r.(klog) r.(ilog) r.(log_kinstr).
Definition with_get_log {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
get_log (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
get_log r.(klog) r.(ilog) r.(log_kinstr).
Definition with_klog {t_log_interp t_get_log t_klog t_ilog t_log_kinstr} klog
(r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) klog r.(ilog) r.(log_kinstr).
Definition with_ilog {t_log_interp t_get_log t_klog t_ilog t_log_kinstr} ilog
(r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) r.(klog) ilog r.(log_kinstr).
Definition with_log_kinstr {t_log_interp t_get_log t_klog t_ilog t_log_kinstr}
log_kinstr (r : record t_log_interp t_get_log t_klog t_ilog t_log_kinstr) :=
Build t_log_interp t_get_log t_klog t_ilog t_log_kinstr r.(log_interp)
r.(get_log) r.(klog) r.(ilog) log_kinstr.
End logger.
Definition logger_skeleton := logger.record.
Module entrypoints.
Record record {root original_type_expr : Set} : Set := Build {
root : root;
original_type_expr : original_type_expr;
}.
Arguments record : clear implicits.
Definition with_root {t_root t_original_type_expr} root
(r : record t_root t_original_type_expr) :=
Build t_root t_original_type_expr root r.(original_type_expr).
Definition with_original_type_expr {t_root t_original_type_expr}
original_type_expr (r : record t_root t_original_type_expr) :=
Build t_root t_original_type_expr r.(root) original_type_expr.
End entrypoints.
Definition entrypoints_skeleton := entrypoints.record.
Reserved Notation "'kinstr.IIf_none".
Reserved Notation "'kinstr.IOpt_map".
Reserved Notation "'kinstr.IIf_left".
Reserved Notation "'kinstr.IIf_cons".
Reserved Notation "'kinstr.IIf".
Reserved Notation "'kinstr.ICreate_contract".
Reserved Notation "'kinstr.IEmit".
Reserved Notation "'typed_contract.Typed_originated".
Reserved Notation "'typed_contract.Typed_tx_rollup".
Reserved Notation "'typed_contract.Typed_sc_rollup".
Reserved Notation "'typed_contract.Typed_zk_rollup".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'internal_operation_contents.Transaction_to_implicit".
Reserved Notation "'internal_operation_contents.Transaction_to_smart_contract".
Reserved Notation "'internal_operation_contents.Transaction_to_tx_rollup".
Reserved Notation "'internal_operation_contents.Transaction_to_sc_rollup".
Reserved Notation "'internal_operation_contents.Event".
Reserved Notation "'internal_operation_contents.Transaction_to_zk_rollup".
Reserved Notation "'internal_operation_contents.Origination".
Reserved Notation "'entrypoints".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'step_type".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".
Inductive kinstr : Set :=
| IDrop : Alpha_context.Script.location → kinstr → kinstr
| IDup : Alpha_context.Script.location → kinstr → kinstr
| ISwap : Alpha_context.Script.location → kinstr → kinstr
| IConst : ∀ {t : Set},
Alpha_context.Script.location → ty → t → kinstr → kinstr
| ICons_pair : Alpha_context.Script.location → kinstr → kinstr
| ICar : Alpha_context.Script.location → kinstr → kinstr
| ICdr : Alpha_context.Script.location → kinstr → kinstr
| IUnpair : Alpha_context.Script.location → kinstr → kinstr
| ICons_some : Alpha_context.Script.location → kinstr → kinstr
| ICons_none : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_none : 'kinstr.IIf_none → kinstr
| IOpt_map : 'kinstr.IOpt_map → kinstr
| ICons_left : Alpha_context.Script.location → ty → kinstr → kinstr
| ICons_right : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_left : 'kinstr.IIf_left → kinstr
| ICons_list : Alpha_context.Script.location → kinstr → kinstr
| INil : Alpha_context.Script.location → ty → kinstr → kinstr
| IIf_cons : 'kinstr.IIf_cons → kinstr
| IList_map :
Alpha_context.Script.location → kinstr → option ty → kinstr → kinstr
| IList_iter :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IList_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_set :
Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| ISet_iter :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr →
kinstr
| ISet_mem : Alpha_context.Script.location → kinstr → kinstr
| ISet_update : Alpha_context.Script.location → kinstr → kinstr
| ISet_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_map :
Alpha_context.Script.location → 'comparable_ty → option ty → kinstr →
kinstr
| IMap_map :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IMap_iter :
Alpha_context.Script.location → option ty → kinstr → kinstr → kinstr
| IMap_mem : Alpha_context.Script.location → kinstr → kinstr
| IMap_get : Alpha_context.Script.location → kinstr → kinstr
| IMap_update : Alpha_context.Script.location → kinstr → kinstr
| IMap_get_and_update : Alpha_context.Script.location → kinstr → kinstr
| IMap_size : Alpha_context.Script.location → kinstr → kinstr
| IEmpty_big_map :
Alpha_context.Script.location → 'comparable_ty → ty → kinstr → kinstr
| IBig_map_mem : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_get : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_update : Alpha_context.Script.location → kinstr → kinstr
| IBig_map_get_and_update : Alpha_context.Script.location → kinstr → kinstr
| IConcat_string : Alpha_context.Script.location → kinstr → kinstr
| IConcat_string_pair : Alpha_context.Script.location → kinstr → kinstr
| ISlice_string : Alpha_context.Script.location → kinstr → kinstr
| IString_size : Alpha_context.Script.location → kinstr → kinstr
| IConcat_bytes : Alpha_context.Script.location → kinstr → kinstr
| IConcat_bytes_pair : Alpha_context.Script.location → kinstr → kinstr
| ISlice_bytes : Alpha_context.Script.location → kinstr → kinstr
| IBytes_size : Alpha_context.Script.location → kinstr → kinstr
| ILsl_bytes : Alpha_context.Script.location → kinstr → kinstr
| ILsr_bytes : Alpha_context.Script.location → kinstr → kinstr
| IOr_bytes : Alpha_context.Script.location → kinstr → kinstr
| IAnd_bytes : Alpha_context.Script.location → kinstr → kinstr
| IXor_bytes : Alpha_context.Script.location → kinstr → kinstr
| INot_bytes : Alpha_context.Script.location → kinstr → kinstr
| IAdd_seconds_to_timestamp : Alpha_context.Script.location → kinstr → kinstr
| IAdd_timestamp_to_seconds : Alpha_context.Script.location → kinstr → kinstr
| ISub_timestamp_seconds : Alpha_context.Script.location → kinstr → kinstr
| IDiff_timestamps : Alpha_context.Script.location → kinstr → kinstr
| IAdd_tez : Alpha_context.Script.location → kinstr → kinstr
| ISub_tez : Alpha_context.Script.location → kinstr → kinstr
| ISub_tez_legacy : Alpha_context.Script.location → kinstr → kinstr
| IMul_teznat : Alpha_context.Script.location → kinstr → kinstr
| IMul_nattez : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_teznat : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_tez : Alpha_context.Script.location → kinstr → kinstr
| IOr : Alpha_context.Script.location → kinstr → kinstr
| IAnd : Alpha_context.Script.location → kinstr → kinstr
| IXor : Alpha_context.Script.location → kinstr → kinstr
| INot : Alpha_context.Script.location → kinstr → kinstr
| IIs_nat : Alpha_context.Script.location → kinstr → kinstr
| INeg : Alpha_context.Script.location → kinstr → kinstr
| IAbs_int : Alpha_context.Script.location → kinstr → kinstr
| IInt_nat : Alpha_context.Script.location → kinstr → kinstr
| IAdd_int : Alpha_context.Script.location → kinstr → kinstr
| IAdd_nat : Alpha_context.Script.location → kinstr → kinstr
| ISub_int : Alpha_context.Script.location → kinstr → kinstr
| IMul_int : Alpha_context.Script.location → kinstr → kinstr
| IMul_nat : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_int : Alpha_context.Script.location → kinstr → kinstr
| IEdiv_nat : Alpha_context.Script.location → kinstr → kinstr
| ILsl_nat : Alpha_context.Script.location → kinstr → kinstr
| ILsr_nat : Alpha_context.Script.location → kinstr → kinstr
| IOr_nat : Alpha_context.Script.location → kinstr → kinstr
| IAnd_nat : Alpha_context.Script.location → kinstr → kinstr
| IAnd_int_nat : Alpha_context.Script.location → kinstr → kinstr
| IXor_nat : Alpha_context.Script.location → kinstr → kinstr
| INot_int : Alpha_context.Script.location → kinstr → kinstr
| IIf : 'kinstr.IIf → kinstr
| ILoop : Alpha_context.Script.location → kinstr → kinstr → kinstr
| ILoop_left : Alpha_context.Script.location → kinstr → kinstr → kinstr
| IDip :
Alpha_context.Script.location → kinstr → option ty → kinstr → kinstr
| IExec : Alpha_context.Script.location → option stack_ty → kinstr → kinstr
| IApply : Alpha_context.Script.location → ty → kinstr → kinstr
| ILambda : Alpha_context.Script.location → lambda → kinstr → kinstr
| IFailwith : Alpha_context.Script.location → ty → kinstr
| ICompare : Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| IEq : Alpha_context.Script.location → kinstr → kinstr
| INeq : Alpha_context.Script.location → kinstr → kinstr
| ILt : Alpha_context.Script.location → kinstr → kinstr
| IGt : Alpha_context.Script.location → kinstr → kinstr
| ILe : Alpha_context.Script.location → kinstr → kinstr
| IGe : Alpha_context.Script.location → kinstr → kinstr
| IAddress : Alpha_context.Script.location → kinstr → kinstr
| IContract :
Alpha_context.Script.location → ty → Alpha_context.Entrypoint.t → kinstr →
kinstr
| IView :
Alpha_context.Script.location → view_signature → option stack_ty →
kinstr → kinstr
| ITransfer_tokens : Alpha_context.Script.location → kinstr → kinstr
| IImplicit_account : Alpha_context.Script.location → kinstr → kinstr
| ICreate_contract : 'kinstr.ICreate_contract → kinstr
| ISet_delegate : Alpha_context.Script.location → kinstr → kinstr
| INow : Alpha_context.Script.location → kinstr → kinstr
| IMin_block_time : Alpha_context.Script.location → kinstr → kinstr
| IBalance : Alpha_context.Script.location → kinstr → kinstr
| ILevel : Alpha_context.Script.location → kinstr → kinstr
| ICheck_signature : Alpha_context.Script.location → kinstr → kinstr
| IHash_key : Alpha_context.Script.location → kinstr → kinstr
| IPack : Alpha_context.Script.location → ty → kinstr → kinstr
| IUnpack : Alpha_context.Script.location → ty → kinstr → kinstr
| IBlake2b : Alpha_context.Script.location → kinstr → kinstr
| ISha256 : Alpha_context.Script.location → kinstr → kinstr
| ISha512 : Alpha_context.Script.location → kinstr → kinstr
| ISource : Alpha_context.Script.location → kinstr → kinstr
| ISender : Alpha_context.Script.location → kinstr → kinstr
| ISelf :
Alpha_context.Script.location → ty → Alpha_context.Entrypoint.t → kinstr →
kinstr
| ISelf_address : Alpha_context.Script.location → kinstr → kinstr
| IAmount : Alpha_context.Script.location → kinstr → kinstr
| ISapling_empty_state :
Alpha_context.Script.location → Alpha_context.Sapling.Memo_size.t →
kinstr → kinstr
| ISapling_verify_update : Alpha_context.Script.location → kinstr → kinstr
| ISapling_verify_update_deprecated :
Alpha_context.Script.location → kinstr → kinstr
| IDig :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IDug :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IDipn :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr → kinstr
| IDropn :
Alpha_context.Script.location → int → stack_prefix_preservation_witness →
kinstr → kinstr
| IChainId : Alpha_context.Script.location → kinstr → kinstr
| INever : Alpha_context.Script.location → kinstr
| IVoting_power : Alpha_context.Script.location → kinstr → kinstr
| ITotal_voting_power : Alpha_context.Script.location → kinstr → kinstr
| IKeccak : Alpha_context.Script.location → kinstr → kinstr
| ISha3 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| IAdd_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_z_fr : Alpha_context.Script.location → kinstr → kinstr
| IMul_bls12_381_fr_z : Alpha_context.Script.location → kinstr → kinstr
| IInt_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_g1 : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_g2 : Alpha_context.Script.location → kinstr → kinstr
| INeg_bls12_381_fr : Alpha_context.Script.location → kinstr → kinstr
| IPairing_check_bls12_381 : Alpha_context.Script.location → kinstr → kinstr
| IComb :
Alpha_context.Script.location → int → comb_gadt_witness → kinstr → kinstr
| IUncomb :
Alpha_context.Script.location → int → uncomb_gadt_witness → kinstr →
kinstr
| IComb_get :
Alpha_context.Script.location → int → comb_get_gadt_witness → kinstr →
kinstr
| IComb_set :
Alpha_context.Script.location → int → comb_set_gadt_witness → kinstr →
kinstr
| IDup_n :
Alpha_context.Script.location → int → dup_n_gadt_witness → kinstr → kinstr
| ITicket :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| ITicket_deprecated :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| IRead_ticket :
Alpha_context.Script.location → option 'comparable_ty → kinstr → kinstr
| ISplit_ticket : Alpha_context.Script.location → kinstr → kinstr
| IJoin_tickets :
Alpha_context.Script.location → 'comparable_ty → kinstr → kinstr
| IOpen_chest : Alpha_context.Script.location → kinstr → kinstr
| IEmit : 'kinstr.IEmit → kinstr
| IHalt : Alpha_context.Script.location → kinstr
| ILog :
Alpha_context.Script.location → stack_ty → logging_event → 'logger →
kinstr → kinstr
with lambda : Set :=
| Lam : 'kdescr → Alpha_context.Script.node → lambda
| LamRec : 'kdescr → Alpha_context.Script.node → lambda
with typed_contract : Set :=
| Typed_implicit : Alpha_context.public_key_hash → typed_contract
| Typed_originated : 'typed_contract.Typed_originated → typed_contract
| Typed_tx_rollup : 'typed_contract.Typed_tx_rollup → typed_contract
| Typed_sc_rollup : 'typed_contract.Typed_sc_rollup → typed_contract
| Typed_zk_rollup : 'typed_contract.Typed_zk_rollup → typed_contract
with continuation : Set :=
| KNil : continuation
| KCons : kinstr → continuation → continuation
| KReturn : ∀ {s : Set},
s → option stack_ty → continuation → continuation
| KMap_head : ∀ {a b : Set}, (a → b) → continuation → continuation
| KUndip : ∀ {b : Set}, b → option ty → continuation → continuation
| KLoop_in : kinstr → continuation → continuation
| KLoop_in_left : kinstr → continuation → continuation
| KIter : ∀ {a : Set},
kinstr → option ty → list a → continuation → continuation
| KList_enter_body : ∀ {a b : Set},
kinstr → list a → Script_list.t b → option ty → int → continuation →
continuation
| KList_exit_body : ∀ {a b : Set},
kinstr → list a → Script_list.t b → option ty → int → continuation →
continuation
| KMap_enter_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → option ty → continuation → continuation
| KMap_exit_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → a → option ty → continuation →
continuation
| KView_exit : step_constants → continuation → continuation
| KLog : continuation → stack_ty → 'logger → continuation
with klog : Set :=
| Klog : ∀ {a s r f : Set},
('logger → Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → stack_ty → continuation →
continuation → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter)) → klog
with ilog : Set :=
| Ilog : ∀ {a s r f : Set},
('logger → logging_event → stack_ty → 'step_type a s r f) → ilog
with log_kinstr : Set :=
| Log_kinstr : ('logger → stack_ty → kinstr → kinstr) → log_kinstr
with ty : Set :=
| Unit_t : ty
| Int_t : ty
| Nat_t : ty
| Signature_t : ty
| String_t : ty
| Bytes_t : ty
| Mutez_t : ty
| Key_hash_t : ty
| Key_t : ty
| Timestamp_t : ty
| Address_t : ty
| Tx_rollup_l2_address_t : ty
| Bool_t : ty
| Pair_t : ty → ty → ty_metadata → Dependent_bool.dand → ty
| Union_t : ty → ty → ty_metadata → Dependent_bool.dand → ty
| Lambda_t : ty → ty → ty_metadata → ty
| Option_t : ty → ty_metadata → Dependent_bool.dbool → ty
| List_t : ty → ty_metadata → ty
| Set_t : 'comparable_ty → ty_metadata → ty
| Map_t : 'comparable_ty → ty → ty_metadata → ty
| Big_map_t : 'comparable_ty → ty → ty_metadata → ty
| Contract_t : ty → ty_metadata → ty
| Sapling_transaction_t : Alpha_context.Sapling.Memo_size.t → ty
| Sapling_transaction_deprecated_t : Alpha_context.Sapling.Memo_size.t → ty
| Sapling_state_t : Alpha_context.Sapling.Memo_size.t → ty
| Operation_t : ty
| Chain_id_t : ty
| Never_t : ty
| Bls12_381_g1_t : ty
| Bls12_381_g2_t : ty
| Bls12_381_fr_t : ty
| Ticket_t : 'comparable_ty → ty_metadata → ty
| Chest_key_t : ty
| Chest_t : ty
with stack_ty : Set :=
| Item_t : ty → stack_ty → stack_ty
| Bot_t : stack_ty
with big_map : Set :=
| Big_map : ∀ {key value : Set}, 'big_map.Big_map key value → big_map
with stack_prefix_preservation_witness : Set :=
| KPrefix :
Alpha_context.Script.location → ty → stack_prefix_preservation_witness →
stack_prefix_preservation_witness
| KRest : stack_prefix_preservation_witness
with comb_gadt_witness : Set :=
| Comb_one : comb_gadt_witness
| Comb_succ : comb_gadt_witness → comb_gadt_witness
with uncomb_gadt_witness : Set :=
| Uncomb_one : uncomb_gadt_witness
| Uncomb_succ : uncomb_gadt_witness → uncomb_gadt_witness
with comb_get_gadt_witness : Set :=
| Comb_get_zero : comb_get_gadt_witness
| Comb_get_one : comb_get_gadt_witness
| Comb_get_plus_two : comb_get_gadt_witness → comb_get_gadt_witness
with comb_set_gadt_witness : Set :=
| Comb_set_zero : comb_set_gadt_witness
| Comb_set_one : comb_set_gadt_witness
| Comb_set_plus_two : comb_set_gadt_witness → comb_set_gadt_witness
with dup_n_gadt_witness : Set :=
| Dup_n_zero : dup_n_gadt_witness
| Dup_n_succ : dup_n_gadt_witness → dup_n_gadt_witness
with view_signature : Set :=
| View_signature : 'view_signature.View_signature → view_signature
with internal_operation_contents : Set :=
| Transaction_to_implicit :
'internal_operation_contents.Transaction_to_implicit →
internal_operation_contents
| Transaction_to_smart_contract : ∀ {a : Set},
'internal_operation_contents.Transaction_to_smart_contract a →
internal_operation_contents
| Transaction_to_tx_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_tx_rollup a →
internal_operation_contents
| Transaction_to_sc_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_sc_rollup a →
internal_operation_contents
| Event : 'internal_operation_contents.Event → internal_operation_contents
| Transaction_to_zk_rollup : ∀ {a : Set},
'internal_operation_contents.Transaction_to_zk_rollup a →
internal_operation_contents
| Origination : ∀ {storage : Set},
'internal_operation_contents.Origination storage →
internal_operation_contents
| Delegation : option Signature.public_key_hash → internal_operation_contents
with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation → packed_internal_operation
where "'entrypoints" :=
(entrypoints_skeleton entrypoints_node Alpha_context.Script.node)
and "'logging_function" :=
(fun (t_c t_u : Set) ⇒ kinstr → Alpha_context.context →
Alpha_context.Script.location → stack_ty → t_c × t_u → unit)
and "'execution_trace" :=
(list
(Alpha_context.Script.location × Alpha_context.Gas.Arith.fp ×
list Alpha_context.Script.expr))
and "'step_type" :=
(fun (t_a t_s t_r t_f : Set) ⇒ Local_gas_counter.outdated_context ×
step_constants → Local_gas_counter.local_gas_counter → kinstr →
continuation → t_a → t_s →
M?
(t_r × t_f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter))
and "'comparable_ty" := ((fun _ ⇒ ty) tt)
and "'kdescr" :=
(kdescr_skeleton Alpha_context.Script.location stack_ty stack_ty kinstr)
and "'internal_operation" :=
(internal_operation_skeleton Alpha_context.Contract.t
internal_operation_contents int)
and "'operation" :=
(operation_skeleton packed_internal_operation
(option Alpha_context.Lazy_storage.diffs))
and "'logger" :=
(logger_skeleton (∀ {c u : Set}, 'logging_function c u)
(unit → M? (option 'execution_trace)) klog ilog log_kinstr)
and "'kinstr.IIf_none" :=
(kinstr.IIf_none_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IOpt_map" :=
(kinstr.IOpt_map_skeleton Alpha_context.Script.location kinstr kinstr)
and "'kinstr.IIf_left" :=
(kinstr.IIf_left_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf_cons" :=
(kinstr.IIf_cons_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.IIf" :=
(kinstr.IIf_skeleton Alpha_context.Script.location kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
(kinstr.ICreate_contract_skeleton Alpha_context.Script.location ty
Alpha_context.Script.expr kinstr)
and "'kinstr.IEmit" :=
(kinstr.IEmit_skeleton Alpha_context.Script.location
Alpha_context.Entrypoint.t ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_originated" :=
(typed_contract.Typed_originated_skeleton ty Contract_hash.t
Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_tx_rollup" :=
(typed_contract.Typed_tx_rollup_skeleton ty Alpha_context.Tx_rollup.t)
and "'typed_contract.Typed_sc_rollup" :=
(typed_contract.Typed_sc_rollup_skeleton ty Alpha_context.Sc_rollup.t
Alpha_context.Entrypoint.t)
and "'typed_contract.Typed_zk_rollup" :=
(typed_contract.Typed_zk_rollup_skeleton ty Alpha_context.Zk_rollup.t)
and "'big_map.Big_map" :=
(fun (t_key t_value : Set) ⇒ big_map.Big_map_skeleton
(option Alpha_context.Big_map.Id.t) (big_map_overlay t_key t_value)
'comparable_ty ty)
and "'view_signature.View_signature" :=
(view_signature.View_signature_skeleton Script_string.t ty ty)
and "'internal_operation_contents.Transaction_to_implicit" :=
(internal_operation_contents.Transaction_to_implicit_skeleton
Signature.public_key_hash Alpha_context.Tez.tez)
and "'internal_operation_contents.Transaction_to_smart_contract" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_smart_contract_skeleton
Contract_hash.t Alpha_context.Tez.tez Alpha_context.Entrypoint.t
Alpha_context.Script.location ty t_a Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_tx_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_tx_rollup_skeleton
Alpha_context.Tx_rollup.t ty (pair (ticket t_a) tx_rollup_l2_address)
Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_sc_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_sc_rollup_skeleton
Alpha_context.Sc_rollup.t Alpha_context.Entrypoint.t ty t_a
Alpha_context.Script.expr)
and "'internal_operation_contents.Event" :=
(internal_operation_contents.Event_skeleton Alpha_context.Script.expr
Alpha_context.Entrypoint.t Alpha_context.Script.expr)
and "'internal_operation_contents.Transaction_to_zk_rollup" :=
(fun (t_a : Set) ⇒ internal_operation_contents.Transaction_to_zk_rollup_skeleton
Alpha_context.Zk_rollup.t ty (pair (ticket t_a) bytes)
Alpha_context.Script.expr)
and "'internal_operation_contents.Origination" :=
(fun (t_storage : Set) ⇒ internal_operation_contents.Origination_skeleton
(option Signature.public_key_hash) Alpha_context.Script.expr
Alpha_context.Script.expr Alpha_context.Tez.tez Contract_hash.t ty t_storage).
Module kinstr.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.kinstr.
Definition IIf_none := 'kinstr.IIf_none.
Definition IOpt_map := 'kinstr.IOpt_map.
Definition IIf_left := 'kinstr.IIf_left.
Definition IIf_cons := 'kinstr.IIf_cons.
Definition IIf := 'kinstr.IIf.
Definition ICreate_contract := 'kinstr.ICreate_contract.
Definition IEmit := 'kinstr.IEmit.
End kinstr.
Module typed_contract.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.typed_contract.
Definition Typed_originated := 'typed_contract.Typed_originated.
Definition Typed_tx_rollup := 'typed_contract.Typed_tx_rollup.
Definition Typed_sc_rollup := 'typed_contract.Typed_sc_rollup.
Definition Typed_zk_rollup := 'typed_contract.Typed_zk_rollup.
End typed_contract.
Module big_map.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.big_map.
Definition Big_map := 'big_map.Big_map.
End big_map.
Module view_signature.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.view_signature.
Definition View_signature := 'view_signature.View_signature.
End view_signature.
Module internal_operation_contents.
Include ConstructorRecords_kinstr_typed_contract_big_map_view_signature_internal_operation_contents.internal_operation_contents.
Definition Transaction_to_implicit :=
'internal_operation_contents.Transaction_to_implicit.
Definition Transaction_to_smart_contract :=
'internal_operation_contents.Transaction_to_smart_contract.
Definition Transaction_to_tx_rollup :=
'internal_operation_contents.Transaction_to_tx_rollup.
Definition Transaction_to_sc_rollup :=
'internal_operation_contents.Transaction_to_sc_rollup.
Definition Event := 'internal_operation_contents.Event.
Definition Transaction_to_zk_rollup :=
'internal_operation_contents.Transaction_to_zk_rollup.
Definition Origination := 'internal_operation_contents.Origination.
End internal_operation_contents.
Definition entrypoints := 'entrypoints.
Definition logging_function := 'logging_function.
Definition execution_trace := 'execution_trace.
Definition logger := 'logger.
Definition step_type := 'step_type.
Definition comparable_ty := 'comparable_ty.
Definition kdescr := 'kdescr.
Definition internal_operation := 'internal_operation.
Definition operation := 'operation.
Inductive ex_ty : Set :=
| Ex_ty : ty → ex_ty.
Records for the constructor parameters
Module ConstructorRecords_script.
Module script.
Module Script.
Record record {code arg_type storage storage_type views entrypoints
code_size : Set} : Set := Build {
code : code;
arg_type : arg_type;
storage : storage;
storage_type : storage_type;
views : views;
entrypoints : entrypoints;
code_size : code_size;
}.
Arguments record : clear implicits.
Definition with_code
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size code r.(arg_type) r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_arg_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} arg_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) arg_type r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) storage r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) storage_type r.(views)
r.(entrypoints) r.(code_size).
Definition with_views
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} views
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type) views
r.(entrypoints) r.(code_size).
Definition with_entrypoints
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} entrypoints
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) entrypoints r.(code_size).
Definition with_code_size
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code_size
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) r.(entrypoints) code_size.
End Script.
Definition Script_skeleton := Script.record.
End script.
End ConstructorRecords_script.
Import ConstructorRecords_script.
Reserved Notation "'script.Script".
Inductive script (storage : Set) : Set :=
| Script : 'script.Script storage → script storage
where "'script.Script" :=
(fun (t_storage : Set) ⇒ script.Script_skeleton lambda ty t_storage ty
view_map entrypoints Cache_memory_helpers.sint).
Module script.
Include ConstructorRecords_script.script.
Definition Script := 'script.Script.
End script.
Arguments Script {_}.
Definition manager_kind (function_parameter : internal_operation_contents)
: Alpha_context.Kind.manager :=
match function_parameter with
| Transaction_to_implicit _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_smart_contract _ ⇒
Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_tx_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_sc_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_zk_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Event _ ⇒ Alpha_context.Kind.Event_manager_kind
| Origination _ ⇒ Alpha_context.Kind.Origination_manager_kind
| Delegation _ ⇒ Alpha_context.Kind.Delegation_manager_kind
end.
Definition kinstr_location (i_value : kinstr) : Alpha_context.Script.location :=
match i_value with
| IDrop loc_value _ ⇒ loc_value
| IDup loc_value _ ⇒ loc_value
| ISwap loc_value _ ⇒ loc_value
| IConst loc_value _ _ _ ⇒ loc_value
| ICons_pair loc_value _ ⇒ loc_value
| ICar loc_value _ ⇒ loc_value
| ICdr loc_value _ ⇒ loc_value
| IUnpair loc_value _ ⇒ loc_value
| ICons_some loc_value _ ⇒ loc_value
| ICons_none loc_value _ _ ⇒ loc_value
| IIf_none {| kinstr.IIf_none.loc := loc_value |} ⇒ loc_value
| IOpt_map {| kinstr.IOpt_map.loc := loc_value |} ⇒ loc_value
| ICons_left loc_value _ _ ⇒ loc_value
| ICons_right loc_value _ _ ⇒ loc_value
| IIf_left {| kinstr.IIf_left.loc := loc_value |} ⇒ loc_value
| ICons_list loc_value _ ⇒ loc_value
| INil loc_value _ _ ⇒ loc_value
| IIf_cons {| kinstr.IIf_cons.loc := loc_value |} ⇒ loc_value
| IList_map loc_value _ _ _ ⇒ loc_value
| IList_iter loc_value _ _ _ ⇒ loc_value
| IList_size loc_value _ ⇒ loc_value
| IEmpty_set loc_value _ _ ⇒ loc_value
| ISet_iter loc_value _ _ _ ⇒ loc_value
| ISet_mem loc_value _ ⇒ loc_value
| ISet_update loc_value _ ⇒ loc_value
| ISet_size loc_value _ ⇒ loc_value
| IEmpty_map loc_value _ _ _ ⇒ loc_value
| IMap_map loc_value _ _ _ ⇒ loc_value
| IMap_iter loc_value _ _ _ ⇒ loc_value
| IMap_mem loc_value _ ⇒ loc_value
| IMap_get loc_value _ ⇒ loc_value
| IMap_update loc_value _ ⇒ loc_value
| IMap_get_and_update loc_value _ ⇒ loc_value
| IMap_size loc_value _ ⇒ loc_value
| IEmpty_big_map loc_value _ _ _ ⇒ loc_value
| IBig_map_mem loc_value _ ⇒ loc_value
| IBig_map_get loc_value _ ⇒ loc_value
| IBig_map_update loc_value _ ⇒ loc_value
| IBig_map_get_and_update loc_value _ ⇒ loc_value
| IConcat_string loc_value _ ⇒ loc_value
| IConcat_string_pair loc_value _ ⇒ loc_value
| ISlice_string loc_value _ ⇒ loc_value
| IString_size loc_value _ ⇒ loc_value
| IConcat_bytes loc_value _ ⇒ loc_value
| IConcat_bytes_pair loc_value _ ⇒ loc_value
| ISlice_bytes loc_value _ ⇒ loc_value
| IBytes_size loc_value _ ⇒ loc_value
| ILsl_bytes loc_value _ ⇒ loc_value
| ILsr_bytes loc_value _ ⇒ loc_value
| IOr_bytes loc_value _ ⇒ loc_value
| IAnd_bytes loc_value _ ⇒ loc_value
| IXor_bytes loc_value _ ⇒ loc_value
| INot_bytes loc_value _ ⇒ loc_value
| IAdd_seconds_to_timestamp loc_value _ ⇒ loc_value
| IAdd_timestamp_to_seconds loc_value _ ⇒ loc_value
| ISub_timestamp_seconds loc_value _ ⇒ loc_value
| IDiff_timestamps loc_value _ ⇒ loc_value
| IAdd_tez loc_value _ ⇒ loc_value
| ISub_tez loc_value _ ⇒ loc_value
| ISub_tez_legacy loc_value _ ⇒ loc_value
| IMul_teznat loc_value _ ⇒ loc_value
| IMul_nattez loc_value _ ⇒ loc_value
| IEdiv_teznat loc_value _ ⇒ loc_value
| IEdiv_tez loc_value _ ⇒ loc_value
| IOr loc_value _ ⇒ loc_value
| IAnd loc_value _ ⇒ loc_value
| IXor loc_value _ ⇒ loc_value
| INot loc_value _ ⇒ loc_value
| IIs_nat loc_value _ ⇒ loc_value
| INeg loc_value _ ⇒ loc_value
| IAbs_int loc_value _ ⇒ loc_value
| IInt_nat loc_value _ ⇒ loc_value
| IAdd_int loc_value _ ⇒ loc_value
| IAdd_nat loc_value _ ⇒ loc_value
| ISub_int loc_value _ ⇒ loc_value
| IMul_int loc_value _ ⇒ loc_value
| IMul_nat loc_value _ ⇒ loc_value
| IEdiv_int loc_value _ ⇒ loc_value
| IEdiv_nat loc_value _ ⇒ loc_value
| ILsl_nat loc_value _ ⇒ loc_value
| ILsr_nat loc_value _ ⇒ loc_value
| IOr_nat loc_value _ ⇒ loc_value
| IAnd_nat loc_value _ ⇒ loc_value
| IAnd_int_nat loc_value _ ⇒ loc_value
| IXor_nat loc_value _ ⇒ loc_value
| INot_int loc_value _ ⇒ loc_value
| IIf {| kinstr.IIf.loc := loc_value |} ⇒ loc_value
| ILoop loc_value _ _ ⇒ loc_value
| ILoop_left loc_value _ _ ⇒ loc_value
| IDip loc_value _ _ _ ⇒ loc_value
| IExec loc_value _ _ ⇒ loc_value
| IApply loc_value _ _ ⇒ loc_value
| ILambda loc_value _ _ ⇒ loc_value
| IFailwith loc_value _ ⇒ loc_value
| ICompare loc_value _ _ ⇒ loc_value
| IEq loc_value _ ⇒ loc_value
| INeq loc_value _ ⇒ loc_value
| ILt loc_value _ ⇒ loc_value
| IGt loc_value _ ⇒ loc_value
| ILe loc_value _ ⇒ loc_value
| IGe loc_value _ ⇒ loc_value
| IAddress loc_value _ ⇒ loc_value
| IContract loc_value _ _ _ ⇒ loc_value
| ITransfer_tokens loc_value _ ⇒ loc_value
| IView loc_value _ _ _ ⇒ loc_value
| IImplicit_account loc_value _ ⇒ loc_value
| ICreate_contract {| kinstr.ICreate_contract.loc := loc_value |} ⇒ loc_value
| ISet_delegate loc_value _ ⇒ loc_value
| INow loc_value _ ⇒ loc_value
| IMin_block_time loc_value _ ⇒ loc_value
| IBalance loc_value _ ⇒ loc_value
| ILevel loc_value _ ⇒ loc_value
| ICheck_signature loc_value _ ⇒ loc_value
| IHash_key loc_value _ ⇒ loc_value
| IPack loc_value _ _ ⇒ loc_value
| IUnpack loc_value _ _ ⇒ loc_value
| IBlake2b loc_value _ ⇒ loc_value
| ISha256 loc_value _ ⇒ loc_value
| ISha512 loc_value _ ⇒ loc_value
| ISource loc_value _ ⇒ loc_value
| ISender loc_value _ ⇒ loc_value
| ISelf loc_value _ _ _ ⇒ loc_value
| ISelf_address loc_value _ ⇒ loc_value
| IAmount loc_value _ ⇒ loc_value
| ISapling_empty_state loc_value _ _ ⇒ loc_value
| ISapling_verify_update loc_value _ ⇒ loc_value
| ISapling_verify_update_deprecated loc_value _ ⇒ loc_value
| IDig loc_value _ _ _ ⇒ loc_value
| IDug loc_value _ _ _ ⇒ loc_value
| IDipn loc_value _ _ _ _ ⇒ loc_value
| IDropn loc_value _ _ _ ⇒ loc_value
| IChainId loc_value _ ⇒ loc_value
| INever loc_value ⇒ loc_value
| IVoting_power loc_value _ ⇒ loc_value
| ITotal_voting_power loc_value _ ⇒ loc_value
| IKeccak loc_value _ ⇒ loc_value
| ISha3 loc_value _ ⇒ loc_value
| IAdd_bls12_381_g1 loc_value _ ⇒ loc_value
| IAdd_bls12_381_g2 loc_value _ ⇒ loc_value
| IAdd_bls12_381_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_g1 loc_value _ ⇒ loc_value
| IMul_bls12_381_g2 loc_value _ ⇒ loc_value
| IMul_bls12_381_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_z_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_fr_z loc_value _ ⇒ loc_value
| IInt_bls12_381_fr loc_value _ ⇒ loc_value
| INeg_bls12_381_g1 loc_value _ ⇒ loc_value
| INeg_bls12_381_g2 loc_value _ ⇒ loc_value
| INeg_bls12_381_fr loc_value _ ⇒ loc_value
| IPairing_check_bls12_381 loc_value _ ⇒ loc_value
| IComb loc_value _ _ _ ⇒ loc_value
| IUncomb loc_value _ _ _ ⇒ loc_value
| IComb_get loc_value _ _ _ ⇒ loc_value
| IComb_set loc_value _ _ _ ⇒ loc_value
| IDup_n loc_value _ _ _ ⇒ loc_value
| ITicket loc_value _ _ ⇒ loc_value
| ITicket_deprecated loc_value _ _ ⇒ loc_value
| IRead_ticket loc_value _ _ ⇒ loc_value
| ISplit_ticket loc_value _ ⇒ loc_value
| IJoin_tickets loc_value _ _ ⇒ loc_value
| IOpen_chest loc_value _ ⇒ loc_value
| IEmit {| kinstr.IEmit.loc := loc_value |} ⇒ loc_value
| IHalt loc_value ⇒ loc_value
| ILog loc_value _ _ _ _ ⇒ loc_value
end.
Definition meta_basic : ty_metadata :=
{| ty_metadata.size := Type_size.(TYPE_SIZE.one); |}.
Definition ty_metadata_value (function_parameter : ty) : ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta _ ⇒ meta
| Union_t _ _ meta _ ⇒ meta
| Option_t _ meta _ ⇒ meta
| Lambda_t _ _ meta ⇒ meta
| List_t _ meta ⇒ meta
| Set_t _ meta ⇒ meta
| Map_t _ _ meta ⇒ meta
| Big_map_t _ _ meta ⇒ meta
| Ticket_t _ meta ⇒ meta
| Contract_t _ meta ⇒ meta
|
(Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Bls12_381_g1_t | Bls12_381_g2_t |
Bls12_381_fr_t | Chest_t | Chest_key_t) ⇒ meta_basic
end.
Definition ty_size (t_value : ty) : Type_size.(TYPE_SIZE.t) :=
(ty_metadata_value t_value).(ty_metadata.size).
Definition is_comparable (function_parameter : ty) : Dependent_bool.dbool :=
match function_parameter with
| Never_t ⇒ Dependent_bool.Yes
| Unit_t ⇒ Dependent_bool.Yes
| Int_t ⇒ Dependent_bool.Yes
| Nat_t ⇒ Dependent_bool.Yes
| Signature_t ⇒ Dependent_bool.Yes
| String_t ⇒ Dependent_bool.Yes
| Bytes_t ⇒ Dependent_bool.Yes
| Mutez_t ⇒ Dependent_bool.Yes
| Bool_t ⇒ Dependent_bool.Yes
| Key_hash_t ⇒ Dependent_bool.Yes
| Key_t ⇒ Dependent_bool.Yes
| Timestamp_t ⇒ Dependent_bool.Yes
| Chain_id_t ⇒ Dependent_bool.Yes
| Address_t ⇒ Dependent_bool.Yes
| Tx_rollup_l2_address_t ⇒ Dependent_bool.Yes
| Pair_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Union_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Option_t _ _ cmp ⇒ cmp
| Lambda_t _ _ _ ⇒ Dependent_bool.No
| List_t _ _ ⇒ Dependent_bool.No
| Set_t _ _ ⇒ Dependent_bool.No
| Map_t _ _ _ ⇒ Dependent_bool.No
| Big_map_t _ _ _ ⇒ Dependent_bool.No
| Ticket_t _ _ ⇒ Dependent_bool.No
| Contract_t _ _ ⇒ Dependent_bool.No
| Sapling_transaction_t _ ⇒ Dependent_bool.No
| Sapling_transaction_deprecated_t _ ⇒ Dependent_bool.No
| Sapling_state_t _ ⇒ Dependent_bool.No
| Operation_t ⇒ Dependent_bool.No
| Bls12_381_g1_t ⇒ Dependent_bool.No
| Bls12_381_g2_t ⇒ Dependent_bool.No
| Bls12_381_fr_t ⇒ Dependent_bool.No
| Chest_t ⇒ Dependent_bool.No
| Chest_key_t ⇒ Dependent_bool.No
end.
Inductive ty_ex_c : Set :=
| Ty_ex_c : ty → ty_ex_c.
Definition unit_t : ty := Unit_t.
Definition int_t : ty := Int_t.
Definition nat_t : ty := Nat_t.
Definition signature_t : ty := Signature_t.
Definition string_t : ty := String_t.
Definition bytes_t : ty := Bytes_t.
Definition mutez_t : ty := Mutez_t.
Definition key_hash_t : ty := Key_hash_t.
Definition key_t : ty := Key_t.
Definition timestamp_t : ty := Timestamp_t.
Definition address_t : ty := Address_t.
Definition bool_t : ty := Bool_t.
Definition tx_rollup_l2_address_t : ty := Tx_rollup_l2_address_t.
Definition pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Pair_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition pair_3_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (m_value : ty)
(r_value : ty) : M? ty_ex_c :=
let? 'Ty_ex_c r_value := pair_t loc_value m_value r_value in
pair_t loc_value l_value r_value.
Definition comparable_pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Pair_t l_value r_value {| ty_metadata.size := size_value; |}
Dependent_bool.YesYes).
Definition comparable_pair_3_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (m_value : ty)
(r_value : ty) : M? ty :=
let? r_value := comparable_pair_t loc_value m_value r_value in
comparable_pair_t loc_value l_value r_value.
Definition union_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Union_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition union_bytes_bool_t : ty :=
Union_t bytes_t bool_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes.
Definition comparable_union_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Union_t l_value r_value {| ty_metadata.size := size_value; |}
Dependent_bool.YesYes).
Definition lambda_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Lambda_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition option_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
let cmp := is_comparable t_value in
return? (Option_t t_value {| ty_metadata.size := size_value; |} cmp).
Definition option_mutez_t : ty :=
Option_t mutez_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_string_t : ty :=
Option_t string_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_bytes_t : ty :=
Option_t bytes_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_nat_t : ty :=
Option_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_pair_nat_nat_t : ty :=
Option_t
(Pair_t nat_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_nat_mutez_t : ty :=
Option_t
(Pair_t nat_t mutez_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_mutez_mutez_t : ty :=
Option_t
(Pair_t mutez_t mutez_t
{| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_int_nat_t : ty :=
Option_t
(Pair_t int_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition list_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (List_t t_value {| ty_metadata.size := size_value; |}).
Definition operation_t : ty := Operation_t.
Definition list_operation_t : ty :=
List_t operation_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}.
Definition set_t
(loc_value : Alpha_context.Script.location) (t_value : comparable_ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Set_t t_value {| ty_metadata.size := size_value; |}).
Definition map_t
(loc_value : Alpha_context.Script.location) (l_value : comparable_ty)
(r_value : ty) : M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Map_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition big_map_t
(loc_value : Alpha_context.Script.location) (l_value : comparable_ty)
(r_value : ty) : M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Big_map_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition contract_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Contract_t t_value {| ty_metadata.size := size_value; |}).
Definition contract_unit_t : ty :=
Contract_t unit_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}.
Definition sapling_transaction_t (memo_size : Alpha_context.Sapling.Memo_size.t)
: ty := Sapling_transaction_t memo_size.
Definition sapling_transaction_deprecated_t
(memo_size : Alpha_context.Sapling.Memo_size.t) : ty :=
Sapling_transaction_deprecated_t memo_size.
Definition sapling_state_t (memo_size : Alpha_context.Sapling.Memo_size.t)
: ty := Sapling_state_t memo_size.
Definition chain_id_t : ty := Chain_id_t.
Definition never_t : ty := Never_t.
Definition bls12_381_g1_t : ty := Bls12_381_g1_t.
Definition bls12_381_g2_t : ty := Bls12_381_g2_t.
Definition bls12_381_fr_t : ty := Bls12_381_fr_t.
Definition ticket_t
(loc_value : Alpha_context.Script.location) (t_value : comparable_ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Ticket_t t_value {| ty_metadata.size := size_value; |}).
Definition chest_key_t : ty := Chest_key_t.
Definition chest_t : ty := Chest_t.
Module kinstr_traverse.
Record record {a : Set} : Set := Build {
apply : a → kinstr → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End kinstr_traverse.
Definition kinstr_traverse := kinstr_traverse.record.
Definition kinstr_traverse_value {accu : Set}
(i_value : kinstr) (init_value : accu) (f_value : kinstr_traverse accu)
: accu :=
let fix aux {ret : Set}
(accu_value : accu) (t_value : kinstr) (continue : accu → ret) : ret :=
let accu_value := f_value.(kinstr_traverse.apply) accu_value t_value in
let next (k_value : kinstr) : ret :=
aux accu_value k_value (fun (accu_value : accu) ⇒ continue accu_value) in
let next2 (k1 : kinstr) (k2 : kinstr) : ret :=
aux accu_value k1
(fun (accu_value : accu) ⇒
aux accu_value k2 (fun (accu_value : accu) ⇒ continue accu_value)) in
let next3 (k1 : kinstr) (k2 : kinstr) (k3 : kinstr) : ret :=
aux accu_value k1
(fun (accu_value : accu) ⇒
aux accu_value k2
(fun (accu_value : accu) ⇒
aux accu_value k3 (fun (accu_value : accu) ⇒ continue accu_value)))
in
let _return (function_parameter : unit) : ret :=
let '_ := function_parameter in
continue accu_value in
match t_value with
| IDrop _ k_value ⇒ next k_value
| IDup _ k_value ⇒ next k_value
| ISwap _ k_value ⇒ next k_value
| IConst _ _ _ k_value ⇒ next k_value
| ICons_pair _ k_value ⇒ next k_value
| ICar _ k_value ⇒ next k_value
| ICdr _ k_value ⇒ next k_value
| IUnpair _ k_value ⇒ next k_value
| ICons_some _ k_value ⇒ next k_value
| ICons_none _ _ k_value ⇒ next k_value
|
IIf_none {|
kinstr.IIf_none.loc := _;
kinstr.IIf_none.branch_if_none := k1;
kinstr.IIf_none.branch_if_some := k2;
kinstr.IIf_none.k := k_value
|} ⇒ next3 k1 k2 k_value
|
IOpt_map {|
kinstr.IOpt_map.loc := _;
kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value
|} ⇒ next2 body k_value
| ICons_left _ _ k_value ⇒ next k_value
| ICons_right _ _ k_value ⇒ next k_value
|
IIf_left {|
kinstr.IIf_left.loc := _;
kinstr.IIf_left.branch_if_left := k1;
kinstr.IIf_left.branch_if_right := k2;
kinstr.IIf_left.k := k_value
|} ⇒ next3 k1 k2 k_value
| ICons_list _ k_value ⇒ next k_value
| INil _ _ k_value ⇒ next k_value
|
IIf_cons {|
kinstr.IIf_cons.loc := _;
kinstr.IIf_cons.branch_if_cons := k2;
kinstr.IIf_cons.branch_if_nil := k1;
kinstr.IIf_cons.k := k_value
|} ⇒ next3 k1 k2 k_value
| IList_map _ k1 _ k2 ⇒ next2 k1 k2
| IList_iter _ _ k1 k2 ⇒ next2 k1 k2
| IList_size _ k_value ⇒ next k_value
| IEmpty_set _ _ k_value ⇒ next k_value
| ISet_iter _ _ k1 k2 ⇒ next2 k1 k2
| ISet_mem _ k_value ⇒ next k_value
| ISet_update _ k_value ⇒ next k_value
| ISet_size _ k_value ⇒ next k_value
| IEmpty_map _ _ _ k_value ⇒ next k_value
| IMap_map _ _ k1 k2 ⇒ next2 k1 k2
| IMap_iter _ _ k1 k2 ⇒ next2 k1 k2
| IMap_mem _ k_value ⇒ next k_value
| IMap_get _ k_value ⇒ next k_value
| IMap_update _ k_value ⇒ next k_value
| IMap_get_and_update _ k_value ⇒ next k_value
| IMap_size _ k_value ⇒ next k_value
| IEmpty_big_map _ _ _ k_value ⇒ next k_value
| IBig_map_mem _ k_value ⇒ next k_value
| IBig_map_get _ k_value ⇒ next k_value
| IBig_map_update _ k_value ⇒ next k_value
| IBig_map_get_and_update _ k_value ⇒ next k_value
| IConcat_string _ k_value ⇒ next k_value
| IConcat_string_pair _ k_value ⇒ next k_value
| ISlice_string _ k_value ⇒ next k_value
| IString_size _ k_value ⇒ next k_value
| IConcat_bytes _ k_value ⇒ next k_value
| IConcat_bytes_pair _ k_value ⇒ next k_value
| ISlice_bytes _ k_value ⇒ next k_value
| IBytes_size _ k_value ⇒ next k_value
| ILsl_bytes _ k_value ⇒ next k_value
| ILsr_bytes _ k_value ⇒ next k_value
| IOr_bytes _ k_value ⇒ next k_value
| IAnd_bytes _ k_value ⇒ next k_value
| IXor_bytes _ k_value ⇒ next k_value
| INot_bytes _ k_value ⇒ next k_value
| IAdd_seconds_to_timestamp _ k_value ⇒ next k_value
| IAdd_timestamp_to_seconds _ k_value ⇒ next k_value
| ISub_timestamp_seconds _ k_value ⇒ next k_value
| IDiff_timestamps _ k_value ⇒ next k_value
| IAdd_tez _ k_value ⇒ next k_value
| ISub_tez _ k_value ⇒ next k_value
| ISub_tez_legacy _ k_value ⇒ next k_value
| IMul_teznat _ k_value ⇒ next k_value
| IMul_nattez _ k_value ⇒ next k_value
| IEdiv_teznat _ k_value ⇒ next k_value
| IEdiv_tez _ k_value ⇒ next k_value
| IOr _ k_value ⇒ next k_value
| IAnd _ k_value ⇒ next k_value
| IXor _ k_value ⇒ next k_value
| INot _ k_value ⇒ next k_value
| IIs_nat _ k_value ⇒ next k_value
| INeg _ k_value ⇒ next k_value
| IAbs_int _ k_value ⇒ next k_value
| IInt_nat _ k_value ⇒ next k_value
| IAdd_int _ k_value ⇒ next k_value
| IAdd_nat _ k_value ⇒ next k_value
| ISub_int _ k_value ⇒ next k_value
| IMul_int _ k_value ⇒ next k_value
| IMul_nat _ k_value ⇒ next k_value
| IEdiv_int _ k_value ⇒ next k_value
| IEdiv_nat _ k_value ⇒ next k_value
| ILsl_nat _ k_value ⇒ next k_value
| ILsr_nat _ k_value ⇒ next k_value
| IOr_nat _ k_value ⇒ next k_value
| IAnd_nat _ k_value ⇒ next k_value
| IAnd_int_nat _ k_value ⇒ next k_value
| IXor_nat _ k_value ⇒ next k_value
| INot_int _ k_value ⇒ next k_value
|
IIf {|
kinstr.IIf.loc := _;
kinstr.IIf.branch_if_true := k1;
kinstr.IIf.branch_if_false := k2;
kinstr.IIf.k := k_value
|} ⇒ next3 k1 k2 k_value
| ILoop _ k1 k2 ⇒ next2 k1 k2
| ILoop_left _ k1 k2 ⇒ next2 k1 k2
| IDip _ k1 _ k2 ⇒ next2 k1 k2
| IExec _ _ k_value ⇒ next k_value
| IApply _ _ k_value ⇒ next k_value
| ILambda _ _ k_value ⇒ next k_value
| IFailwith _ _ ⇒ _return tt
| ICompare _ _ k_value ⇒ next k_value
| IEq _ k_value ⇒ next k_value
| INeq _ k_value ⇒ next k_value
| ILt _ k_value ⇒ next k_value
| IGt _ k_value ⇒ next k_value
| ILe _ k_value ⇒ next k_value
| IGe _ k_value ⇒ next k_value
| IAddress _ k_value ⇒ next k_value
| IContract _ _ _ k_value ⇒ next k_value
| IView _ _ _ k_value ⇒ next k_value
| ITransfer_tokens _ k_value ⇒ next k_value
| IImplicit_account _ k_value ⇒ next k_value
| ICreate_contract {| kinstr.ICreate_contract.k := k_value |} ⇒
next k_value
| ISet_delegate _ k_value ⇒ next k_value
| INow _ k_value ⇒ next k_value
| IMin_block_time _ k_value ⇒ next k_value
| IBalance _ k_value ⇒ next k_value
| ILevel _ k_value ⇒ next k_value
| ICheck_signature _ k_value ⇒ next k_value
| IHash_key _ k_value ⇒ next k_value
| IPack _ _ k_value ⇒ next k_value
| IUnpack _ _ k_value ⇒ next k_value
| IBlake2b _ k_value ⇒ next k_value
| ISha256 _ k_value ⇒ next k_value
| ISha512 _ k_value ⇒ next k_value
| ISource _ k_value ⇒ next k_value
| ISender _ k_value ⇒ next k_value
| ISelf _ _ _ k_value ⇒ next k_value
| ISelf_address _ k_value ⇒ next k_value
| IAmount _ k_value ⇒ next k_value
| ISapling_empty_state _ _ k_value ⇒ next k_value
| ISapling_verify_update _ k_value ⇒ next k_value
| ISapling_verify_update_deprecated _ k_value ⇒ next k_value
| IDig _ _ _ k_value ⇒ next k_value
| IDug _ _ _ k_value ⇒ next k_value
| IDipn _ _ _ k1 k2 ⇒ next2 k1 k2
| IDropn _ _ _ k_value ⇒ next k_value
| IChainId _ k_value ⇒ next k_value
| INever _ ⇒ _return tt
| IVoting_power _ k_value ⇒ next k_value
| ITotal_voting_power _ k_value ⇒ next k_value
| IKeccak _ k_value ⇒ next k_value
| ISha3 _ k_value ⇒ next k_value
| IAdd_bls12_381_g1 _ k_value ⇒ next k_value
| IAdd_bls12_381_g2 _ k_value ⇒ next k_value
| IAdd_bls12_381_fr _ k_value ⇒ next k_value
| IMul_bls12_381_g1 _ k_value ⇒ next k_value
| IMul_bls12_381_g2 _ k_value ⇒ next k_value
| IMul_bls12_381_fr _ k_value ⇒ next k_value
| IMul_bls12_381_z_fr _ k_value ⇒ next k_value
| IMul_bls12_381_fr_z _ k_value ⇒ next k_value
| IInt_bls12_381_fr _ k_value ⇒ next k_value
| INeg_bls12_381_g1 _ k_value ⇒ next k_value
| INeg_bls12_381_g2 _ k_value ⇒ next k_value
| INeg_bls12_381_fr _ k_value ⇒ next k_value
| IPairing_check_bls12_381 _ k_value ⇒ next k_value
| IComb _ _ _ k_value ⇒ next k_value
| IUncomb _ _ _ k_value ⇒ next k_value
| IComb_get _ _ _ k_value ⇒ next k_value
| IComb_set _ _ _ k_value ⇒ next k_value
| IDup_n _ _ _ k_value ⇒ next k_value
| ITicket _ _ k_value ⇒ next k_value
| ITicket_deprecated _ _ k_value ⇒ next k_value
| IRead_ticket _ _ k_value ⇒ next k_value
| ISplit_ticket _ k_value ⇒ next k_value
| IJoin_tickets _ _ k_value ⇒ next k_value
| IOpen_chest _ k_value ⇒ next k_value
| IEmit {| kinstr.IEmit.k := k_value |} ⇒ next k_value
| IHalt _ ⇒ _return tt
| ILog _ _ _ _ k_value ⇒ next k_value
end in
aux init_value i_value (fun (accu_value : accu) ⇒ accu_value).
Module ty_traverse.
Record record {a : Set} : Set := Build {
apply : a → ty → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End ty_traverse.
Definition ty_traverse := ty_traverse.record.
Module Ty_traverse.
Reserved Notation "'next2".
Reserved Notation "'next".
Fixpoint aux {accu ret : Set}
(f_value : ty_traverse accu) (accu_value : accu) (ty_value : ty)
(continue : accu → ret) : ret :=
let next2 {accu ret} := 'next2 accu ret in
let next {accu ret} := 'next accu ret in
let accu_value := f_value.(ty_traverse.apply) accu_value ty_value in
match ty_value with
|
(Unit_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t | Mutez_t |
Key_hash_t | Key_t | Timestamp_t | Address_t | Tx_rollup_l2_address_t |
Bool_t | Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Chain_id_t | Never_t | Bls12_381_g1_t |
Bls12_381_g2_t | Bls12_381_fr_t) ⇒ continue accu_value
| Ticket_t cty _ ⇒ aux f_value accu_value cty continue
| (Chest_key_t | Chest_t) ⇒ continue accu_value
| Pair_t ty1 ty2 _ _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Union_t ty1 ty2 _ _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Lambda_t ty1 ty2 _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Option_t ty1 _ _ ⇒ next f_value accu_value ty1 continue
| List_t ty1 _ ⇒ next f_value accu_value ty1 continue
| Set_t cty _ ⇒ aux f_value accu_value cty continue
| Map_t cty ty1 _ ⇒
aux f_value accu_value cty
(fun (accu_value : accu) ⇒ next f_value accu_value ty1 continue)
| Big_map_t cty ty1 _ ⇒
aux f_value accu_value cty
(fun (accu_value : accu) ⇒ next f_value accu_value ty1 continue)
| Contract_t ty1 _ ⇒ next f_value accu_value ty1 continue
end
where "'next2" :=
(fun (accu ret : Set) ⇒ fun
(f_value : ty_traverse accu) (accu_value : accu) (ty1 : ty) (ty2 : ty)
(continue : accu → ret) ⇒
aux f_value accu_value ty1
(fun (accu_value : accu) ⇒
aux f_value accu_value ty2
(fun (accu_value : accu) ⇒ continue accu_value)))
and "'next" :=
(fun (accu ret : Set) ⇒ fun
(f_value : ty_traverse accu) (accu_value : accu) (ty1 : ty)
(continue : accu → ret) ⇒
aux f_value accu_value ty1
(fun (accu_value : accu) ⇒ continue accu_value)).
Definition next2 {accu ret : Set} := 'next2 accu ret.
Definition next {accu ret : Set} := 'next accu ret.
End Ty_traverse.
Definition ty_traverse_value {A : Set}
(ty_value : ty) (init_value : A) (f_value : ty_traverse A) : A :=
Ty_traverse.aux f_value init_value ty_value
(fun (accu_value : A) ⇒ accu_value).
Module stack_ty_traverse.
Record record {accu : Set} : Set := Build {
apply : accu → stack_ty → accu;
}.
Arguments record : clear implicits.
Definition with_apply {t_accu} apply (r : record t_accu) :=
Build t_accu apply.
End stack_ty_traverse.
Definition stack_ty_traverse := stack_ty_traverse.record.
Definition stack_ty_traverse_value {accu : Set}
(sty : stack_ty) (init_value : accu) (f_value : stack_ty_traverse accu)
: accu :=
let fix aux (accu_value : accu) (sty : stack_ty) : accu :=
match sty with
| Bot_t ⇒ f_value.(stack_ty_traverse.apply) accu_value sty
| Item_t _ sty' ⇒
aux (f_value.(stack_ty_traverse.apply) accu_value sty) sty'
end in
aux init_value sty.
Module value_traverse.
Record record {a : Set} : Set := Build {
apply : ∀ {t : Set}, a → ty → t → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End value_traverse.
Definition value_traverse := value_traverse.record.
Module Value_traverse.
#[bypass_check(guard)]
Fixpoint aux {accu t ret : Set}
(f_value : value_traverse accu) (accu_value : accu) (ty_value : ty)
(x_value : t) (continue : accu → ret) {struct ty_value} : ret :=
let accu_value := f_value.(value_traverse.apply) accu_value ty_value x_value
in
let next2 {D E : Set} (ty1 : ty) (ty2 : ty) (x1 : D) (x2 : E) : ret :=
aux f_value accu_value ty1 x1
(fun (accu_value : accu) ⇒
aux f_value accu_value ty2 x2
(fun (accu_value : accu) ⇒ continue accu_value)) in
let next {D : Set} (ty1 : ty) (x1 : D) : ret :=
aux f_value accu_value ty1 x1
(fun (accu_value : accu) ⇒ continue accu_value) in
let _return (function_parameter : unit) : ret :=
let '_ := function_parameter in
continue accu_value in
let fix on_list {D : Set}
(ty' : ty) (accu_value : accu) (function_parameter : list D) : ret :=
match function_parameter with
| [] ⇒ continue accu_value
| cons x_value xs ⇒
aux f_value accu_value ty' x_value
(fun (accu_value : accu) ⇒ on_list ty' accu_value xs)
end in
match (ty_value, x_value) with
|
((Unit_t, _) | (Int_t, _) | (Nat_t, _) | (Signature_t, _) | (String_t, _)
| (Bytes_t, _) | (Mutez_t, _) | (Key_hash_t, _) | (Key_t, _) |
(Timestamp_t, _) | (Address_t, _) | (Tx_rollup_l2_address_t, _) |
(Bool_t, _) | (Sapling_transaction_t _, _) |
(Sapling_transaction_deprecated_t _, _) | (Sapling_state_t _, _) |
(Operation_t, _) | (Chain_id_t, _) | (Never_t, _) | (Bls12_381_g1_t, _) |
(Bls12_381_g2_t, _) | (Bls12_381_fr_t, _) | (Chest_key_t, _) |
(Chest_t, _) | (Lambda_t _ _ _, _)) ⇒ _return tt
| (Pair_t ty1 ty2 _ _, x_value) ⇒
let 'existT _ [__2, __3] [x_value, ty2, ty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒ [__2 × __3 ** ty ** ty]) [x_value, ty2, ty1] in
next2 ty1 ty2 (Pervasives.fst x_value) (Pervasives.snd x_value)
| (Union_t ty1 ty2 _ _, x_value) ⇒
let 'existT _ [__4, __5] [x_value, ty2, ty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__4, __5] ⇒ [union __4 __5 ** ty ** ty]) [x_value, ty2, ty1]
in
match x_value with
| L l_value ⇒ next ty1 l_value
| R r_value ⇒ next ty2 r_value
end
| (Option_t ty_value _ _, x_value) ⇒
let 'existT _ __6 [x_value, ty_value] :=
cast_exists (Es := Set) (fun __6 ⇒ [option __6 ** ty])
[x_value, ty_value] in
match x_value with
| None ⇒ _return tt
| Some v_value ⇒ next ty_value v_value
end
| (Ticket_t cty _, x_value) ⇒
let 'existT _ __7 [x_value, cty] :=
cast_exists (Es := Set) (fun __7 ⇒ [ticket __7 ** comparable_ty])
[x_value, cty] in
aux f_value accu_value cty x_value.(ticket.contents) continue
| (List_t ty' _, x_value) ⇒
let 'existT _ __8 [x_value, ty'] :=
cast_exists (Es := Set) (fun __8 ⇒ [Script_list.t __8 ** ty])
[x_value, ty'] in
on_list ty' accu_value x_value.(Script_list.t.elements)
| (Map_t kty ty' _, x_value) ⇒
let 'existT _ [__9, __10] [x_value, ty', kty] :=
cast_exists (Es := [Set ** Set])
(fun '[__9, __10] ⇒ [map __9 __10 ** ty ** comparable_ty])
[x_value, ty', kty] in
let 'Map_tag M := x_value in
let 'existS _ _ M := M in
let bindings :=
M.(Boxed_map.OPS).(Boxed_map_OPS.fold)
(fun (k_value : __9) ⇒
fun (v_value : __10) ⇒
fun (bs : list (__9 × __10)) ⇒ cons (k_value, v_value) bs)
M.(Boxed_map.boxed) nil in
on_bindings f_value accu_value kty ty' continue bindings
| (Set_t ty' _, x_value) ⇒
let 'existT _ __11 [x_value, ty'] :=
cast_exists (Es := Set) (fun __11 ⇒ [set __11 ** comparable_ty])
[x_value, ty'] in
let 'Set_tag M := x_value in
let 'existS _ _ M := M in
let elements :=
M.(Boxed_set.OPS).(Boxed_set_OPS.fold)
(fun (x_value : __11) ⇒
fun (s_value : list __11) ⇒ cons x_value s_value)
M.(Boxed_set.boxed) nil in
on_list ty' accu_value elements
| (Big_map_t _ _ _, _) ⇒ _return tt
| (Contract_t _ _, _) ⇒ _return tt
end
with on_bindings {accu ret k v : Set}
(f_value : value_traverse accu) (accu_value : accu) (kty : comparable_ty)
(ty' : ty) (continue : accu → ret) (xs : list (k × v)) {struct xs} : ret :=
match xs with
| [] ⇒ continue accu_value
| cons (k_value, v_value) xs ⇒
aux f_value accu_value kty k_value
(fun (accu_value : accu) ⇒
aux f_value accu_value ty' v_value
(fun (accu_value : accu) ⇒
on_bindings f_value accu_value kty ty' continue xs))
end.
End Value_traverse.
Definition value_traverse_value {t B : Set}
(ty_value : ty) (x_value : t) (init_value : B) (f_value : value_traverse B)
: B :=
Value_traverse.aux f_value init_value ty_value x_value
(fun (accu_value : B) ⇒ accu_value).
Definition stack_top_ty (function_parameter : stack_ty) : ty_ex_c :=
match function_parameter with
| Item_t ty_value _ ⇒ Ty_ex_c ty_value
| _ ⇒ unreachable_gadt_branch
end.
Module Typed_contract.
Definition destination (function_parameter : typed_contract)
: Alpha_context.Destination.t :=
match function_parameter with
| Typed_implicit pkh ⇒
Alpha_context.Destination.Contract (Contract_repr.Implicit pkh)
|
Typed_originated {|
typed_contract.Typed_originated.contract_hash := contract_hash |} ⇒
Alpha_context.Destination.Contract
(Contract_repr.Originated contract_hash)
|
Typed_tx_rollup {|
typed_contract.Typed_tx_rollup.tx_rollup := tx_rollup |} ⇒
Alpha_context.Destination.Tx_rollup tx_rollup
|
Typed_sc_rollup {|
typed_contract.Typed_sc_rollup.sc_rollup := sc_rollup |} ⇒
Alpha_context.Destination.Sc_rollup sc_rollup
|
Typed_zk_rollup {|
typed_contract.Typed_zk_rollup.zk_rollup := zk_rollup |} ⇒
Alpha_context.Destination.Zk_rollup zk_rollup
end.
Definition arg_ty (function_parameter : typed_contract) : ty_ex_c :=
match function_parameter with
| Typed_implicit _ ⇒ Ty_ex_c Unit_t
| Typed_originated {| typed_contract.Typed_originated.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_tx_rollup {| typed_contract.Typed_tx_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_sc_rollup {| typed_contract.Typed_sc_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_zk_rollup {| typed_contract.Typed_zk_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
end.
Definition entrypoint (function_parameter : typed_contract)
: Alpha_context.Entrypoint.t :=
match function_parameter with
| Typed_implicit _ ⇒ Alpha_context.Entrypoint.default
| Typed_tx_rollup _ ⇒ Alpha_context.Entrypoint.deposit
|
(Typed_originated {|
typed_contract.Typed_originated.entrypoint := entrypoint |} |
Typed_sc_rollup {|
typed_contract.Typed_sc_rollup.entrypoint := entrypoint |}) ⇒
entrypoint
| Typed_zk_rollup _ ⇒ Alpha_context.Entrypoint.deposit
end.
End Typed_contract.
Module script.
Module Script.
Record record {code arg_type storage storage_type views entrypoints
code_size : Set} : Set := Build {
code : code;
arg_type : arg_type;
storage : storage;
storage_type : storage_type;
views : views;
entrypoints : entrypoints;
code_size : code_size;
}.
Arguments record : clear implicits.
Definition with_code
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size code r.(arg_type) r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_arg_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} arg_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) arg_type r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) storage r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) storage_type r.(views)
r.(entrypoints) r.(code_size).
Definition with_views
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} views
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type) views
r.(entrypoints) r.(code_size).
Definition with_entrypoints
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} entrypoints
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) entrypoints r.(code_size).
Definition with_code_size
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code_size
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) r.(entrypoints) code_size.
End Script.
Definition Script_skeleton := Script.record.
End script.
End ConstructorRecords_script.
Import ConstructorRecords_script.
Reserved Notation "'script.Script".
Inductive script (storage : Set) : Set :=
| Script : 'script.Script storage → script storage
where "'script.Script" :=
(fun (t_storage : Set) ⇒ script.Script_skeleton lambda ty t_storage ty
view_map entrypoints Cache_memory_helpers.sint).
Module script.
Include ConstructorRecords_script.script.
Definition Script := 'script.Script.
End script.
Arguments Script {_}.
Definition manager_kind (function_parameter : internal_operation_contents)
: Alpha_context.Kind.manager :=
match function_parameter with
| Transaction_to_implicit _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_smart_contract _ ⇒
Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_tx_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_sc_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Transaction_to_zk_rollup _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Event _ ⇒ Alpha_context.Kind.Event_manager_kind
| Origination _ ⇒ Alpha_context.Kind.Origination_manager_kind
| Delegation _ ⇒ Alpha_context.Kind.Delegation_manager_kind
end.
Definition kinstr_location (i_value : kinstr) : Alpha_context.Script.location :=
match i_value with
| IDrop loc_value _ ⇒ loc_value
| IDup loc_value _ ⇒ loc_value
| ISwap loc_value _ ⇒ loc_value
| IConst loc_value _ _ _ ⇒ loc_value
| ICons_pair loc_value _ ⇒ loc_value
| ICar loc_value _ ⇒ loc_value
| ICdr loc_value _ ⇒ loc_value
| IUnpair loc_value _ ⇒ loc_value
| ICons_some loc_value _ ⇒ loc_value
| ICons_none loc_value _ _ ⇒ loc_value
| IIf_none {| kinstr.IIf_none.loc := loc_value |} ⇒ loc_value
| IOpt_map {| kinstr.IOpt_map.loc := loc_value |} ⇒ loc_value
| ICons_left loc_value _ _ ⇒ loc_value
| ICons_right loc_value _ _ ⇒ loc_value
| IIf_left {| kinstr.IIf_left.loc := loc_value |} ⇒ loc_value
| ICons_list loc_value _ ⇒ loc_value
| INil loc_value _ _ ⇒ loc_value
| IIf_cons {| kinstr.IIf_cons.loc := loc_value |} ⇒ loc_value
| IList_map loc_value _ _ _ ⇒ loc_value
| IList_iter loc_value _ _ _ ⇒ loc_value
| IList_size loc_value _ ⇒ loc_value
| IEmpty_set loc_value _ _ ⇒ loc_value
| ISet_iter loc_value _ _ _ ⇒ loc_value
| ISet_mem loc_value _ ⇒ loc_value
| ISet_update loc_value _ ⇒ loc_value
| ISet_size loc_value _ ⇒ loc_value
| IEmpty_map loc_value _ _ _ ⇒ loc_value
| IMap_map loc_value _ _ _ ⇒ loc_value
| IMap_iter loc_value _ _ _ ⇒ loc_value
| IMap_mem loc_value _ ⇒ loc_value
| IMap_get loc_value _ ⇒ loc_value
| IMap_update loc_value _ ⇒ loc_value
| IMap_get_and_update loc_value _ ⇒ loc_value
| IMap_size loc_value _ ⇒ loc_value
| IEmpty_big_map loc_value _ _ _ ⇒ loc_value
| IBig_map_mem loc_value _ ⇒ loc_value
| IBig_map_get loc_value _ ⇒ loc_value
| IBig_map_update loc_value _ ⇒ loc_value
| IBig_map_get_and_update loc_value _ ⇒ loc_value
| IConcat_string loc_value _ ⇒ loc_value
| IConcat_string_pair loc_value _ ⇒ loc_value
| ISlice_string loc_value _ ⇒ loc_value
| IString_size loc_value _ ⇒ loc_value
| IConcat_bytes loc_value _ ⇒ loc_value
| IConcat_bytes_pair loc_value _ ⇒ loc_value
| ISlice_bytes loc_value _ ⇒ loc_value
| IBytes_size loc_value _ ⇒ loc_value
| ILsl_bytes loc_value _ ⇒ loc_value
| ILsr_bytes loc_value _ ⇒ loc_value
| IOr_bytes loc_value _ ⇒ loc_value
| IAnd_bytes loc_value _ ⇒ loc_value
| IXor_bytes loc_value _ ⇒ loc_value
| INot_bytes loc_value _ ⇒ loc_value
| IAdd_seconds_to_timestamp loc_value _ ⇒ loc_value
| IAdd_timestamp_to_seconds loc_value _ ⇒ loc_value
| ISub_timestamp_seconds loc_value _ ⇒ loc_value
| IDiff_timestamps loc_value _ ⇒ loc_value
| IAdd_tez loc_value _ ⇒ loc_value
| ISub_tez loc_value _ ⇒ loc_value
| ISub_tez_legacy loc_value _ ⇒ loc_value
| IMul_teznat loc_value _ ⇒ loc_value
| IMul_nattez loc_value _ ⇒ loc_value
| IEdiv_teznat loc_value _ ⇒ loc_value
| IEdiv_tez loc_value _ ⇒ loc_value
| IOr loc_value _ ⇒ loc_value
| IAnd loc_value _ ⇒ loc_value
| IXor loc_value _ ⇒ loc_value
| INot loc_value _ ⇒ loc_value
| IIs_nat loc_value _ ⇒ loc_value
| INeg loc_value _ ⇒ loc_value
| IAbs_int loc_value _ ⇒ loc_value
| IInt_nat loc_value _ ⇒ loc_value
| IAdd_int loc_value _ ⇒ loc_value
| IAdd_nat loc_value _ ⇒ loc_value
| ISub_int loc_value _ ⇒ loc_value
| IMul_int loc_value _ ⇒ loc_value
| IMul_nat loc_value _ ⇒ loc_value
| IEdiv_int loc_value _ ⇒ loc_value
| IEdiv_nat loc_value _ ⇒ loc_value
| ILsl_nat loc_value _ ⇒ loc_value
| ILsr_nat loc_value _ ⇒ loc_value
| IOr_nat loc_value _ ⇒ loc_value
| IAnd_nat loc_value _ ⇒ loc_value
| IAnd_int_nat loc_value _ ⇒ loc_value
| IXor_nat loc_value _ ⇒ loc_value
| INot_int loc_value _ ⇒ loc_value
| IIf {| kinstr.IIf.loc := loc_value |} ⇒ loc_value
| ILoop loc_value _ _ ⇒ loc_value
| ILoop_left loc_value _ _ ⇒ loc_value
| IDip loc_value _ _ _ ⇒ loc_value
| IExec loc_value _ _ ⇒ loc_value
| IApply loc_value _ _ ⇒ loc_value
| ILambda loc_value _ _ ⇒ loc_value
| IFailwith loc_value _ ⇒ loc_value
| ICompare loc_value _ _ ⇒ loc_value
| IEq loc_value _ ⇒ loc_value
| INeq loc_value _ ⇒ loc_value
| ILt loc_value _ ⇒ loc_value
| IGt loc_value _ ⇒ loc_value
| ILe loc_value _ ⇒ loc_value
| IGe loc_value _ ⇒ loc_value
| IAddress loc_value _ ⇒ loc_value
| IContract loc_value _ _ _ ⇒ loc_value
| ITransfer_tokens loc_value _ ⇒ loc_value
| IView loc_value _ _ _ ⇒ loc_value
| IImplicit_account loc_value _ ⇒ loc_value
| ICreate_contract {| kinstr.ICreate_contract.loc := loc_value |} ⇒ loc_value
| ISet_delegate loc_value _ ⇒ loc_value
| INow loc_value _ ⇒ loc_value
| IMin_block_time loc_value _ ⇒ loc_value
| IBalance loc_value _ ⇒ loc_value
| ILevel loc_value _ ⇒ loc_value
| ICheck_signature loc_value _ ⇒ loc_value
| IHash_key loc_value _ ⇒ loc_value
| IPack loc_value _ _ ⇒ loc_value
| IUnpack loc_value _ _ ⇒ loc_value
| IBlake2b loc_value _ ⇒ loc_value
| ISha256 loc_value _ ⇒ loc_value
| ISha512 loc_value _ ⇒ loc_value
| ISource loc_value _ ⇒ loc_value
| ISender loc_value _ ⇒ loc_value
| ISelf loc_value _ _ _ ⇒ loc_value
| ISelf_address loc_value _ ⇒ loc_value
| IAmount loc_value _ ⇒ loc_value
| ISapling_empty_state loc_value _ _ ⇒ loc_value
| ISapling_verify_update loc_value _ ⇒ loc_value
| ISapling_verify_update_deprecated loc_value _ ⇒ loc_value
| IDig loc_value _ _ _ ⇒ loc_value
| IDug loc_value _ _ _ ⇒ loc_value
| IDipn loc_value _ _ _ _ ⇒ loc_value
| IDropn loc_value _ _ _ ⇒ loc_value
| IChainId loc_value _ ⇒ loc_value
| INever loc_value ⇒ loc_value
| IVoting_power loc_value _ ⇒ loc_value
| ITotal_voting_power loc_value _ ⇒ loc_value
| IKeccak loc_value _ ⇒ loc_value
| ISha3 loc_value _ ⇒ loc_value
| IAdd_bls12_381_g1 loc_value _ ⇒ loc_value
| IAdd_bls12_381_g2 loc_value _ ⇒ loc_value
| IAdd_bls12_381_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_g1 loc_value _ ⇒ loc_value
| IMul_bls12_381_g2 loc_value _ ⇒ loc_value
| IMul_bls12_381_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_z_fr loc_value _ ⇒ loc_value
| IMul_bls12_381_fr_z loc_value _ ⇒ loc_value
| IInt_bls12_381_fr loc_value _ ⇒ loc_value
| INeg_bls12_381_g1 loc_value _ ⇒ loc_value
| INeg_bls12_381_g2 loc_value _ ⇒ loc_value
| INeg_bls12_381_fr loc_value _ ⇒ loc_value
| IPairing_check_bls12_381 loc_value _ ⇒ loc_value
| IComb loc_value _ _ _ ⇒ loc_value
| IUncomb loc_value _ _ _ ⇒ loc_value
| IComb_get loc_value _ _ _ ⇒ loc_value
| IComb_set loc_value _ _ _ ⇒ loc_value
| IDup_n loc_value _ _ _ ⇒ loc_value
| ITicket loc_value _ _ ⇒ loc_value
| ITicket_deprecated loc_value _ _ ⇒ loc_value
| IRead_ticket loc_value _ _ ⇒ loc_value
| ISplit_ticket loc_value _ ⇒ loc_value
| IJoin_tickets loc_value _ _ ⇒ loc_value
| IOpen_chest loc_value _ ⇒ loc_value
| IEmit {| kinstr.IEmit.loc := loc_value |} ⇒ loc_value
| IHalt loc_value ⇒ loc_value
| ILog loc_value _ _ _ _ ⇒ loc_value
end.
Definition meta_basic : ty_metadata :=
{| ty_metadata.size := Type_size.(TYPE_SIZE.one); |}.
Definition ty_metadata_value (function_parameter : ty) : ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta _ ⇒ meta
| Union_t _ _ meta _ ⇒ meta
| Option_t _ meta _ ⇒ meta
| Lambda_t _ _ meta ⇒ meta
| List_t _ meta ⇒ meta
| Set_t _ meta ⇒ meta
| Map_t _ _ meta ⇒ meta
| Big_map_t _ _ meta ⇒ meta
| Ticket_t _ meta ⇒ meta
| Contract_t _ meta ⇒ meta
|
(Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Bls12_381_g1_t | Bls12_381_g2_t |
Bls12_381_fr_t | Chest_t | Chest_key_t) ⇒ meta_basic
end.
Definition ty_size (t_value : ty) : Type_size.(TYPE_SIZE.t) :=
(ty_metadata_value t_value).(ty_metadata.size).
Definition is_comparable (function_parameter : ty) : Dependent_bool.dbool :=
match function_parameter with
| Never_t ⇒ Dependent_bool.Yes
| Unit_t ⇒ Dependent_bool.Yes
| Int_t ⇒ Dependent_bool.Yes
| Nat_t ⇒ Dependent_bool.Yes
| Signature_t ⇒ Dependent_bool.Yes
| String_t ⇒ Dependent_bool.Yes
| Bytes_t ⇒ Dependent_bool.Yes
| Mutez_t ⇒ Dependent_bool.Yes
| Bool_t ⇒ Dependent_bool.Yes
| Key_hash_t ⇒ Dependent_bool.Yes
| Key_t ⇒ Dependent_bool.Yes
| Timestamp_t ⇒ Dependent_bool.Yes
| Chain_id_t ⇒ Dependent_bool.Yes
| Address_t ⇒ Dependent_bool.Yes
| Tx_rollup_l2_address_t ⇒ Dependent_bool.Yes
| Pair_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Union_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Option_t _ _ cmp ⇒ cmp
| Lambda_t _ _ _ ⇒ Dependent_bool.No
| List_t _ _ ⇒ Dependent_bool.No
| Set_t _ _ ⇒ Dependent_bool.No
| Map_t _ _ _ ⇒ Dependent_bool.No
| Big_map_t _ _ _ ⇒ Dependent_bool.No
| Ticket_t _ _ ⇒ Dependent_bool.No
| Contract_t _ _ ⇒ Dependent_bool.No
| Sapling_transaction_t _ ⇒ Dependent_bool.No
| Sapling_transaction_deprecated_t _ ⇒ Dependent_bool.No
| Sapling_state_t _ ⇒ Dependent_bool.No
| Operation_t ⇒ Dependent_bool.No
| Bls12_381_g1_t ⇒ Dependent_bool.No
| Bls12_381_g2_t ⇒ Dependent_bool.No
| Bls12_381_fr_t ⇒ Dependent_bool.No
| Chest_t ⇒ Dependent_bool.No
| Chest_key_t ⇒ Dependent_bool.No
end.
Inductive ty_ex_c : Set :=
| Ty_ex_c : ty → ty_ex_c.
Definition unit_t : ty := Unit_t.
Definition int_t : ty := Int_t.
Definition nat_t : ty := Nat_t.
Definition signature_t : ty := Signature_t.
Definition string_t : ty := String_t.
Definition bytes_t : ty := Bytes_t.
Definition mutez_t : ty := Mutez_t.
Definition key_hash_t : ty := Key_hash_t.
Definition key_t : ty := Key_t.
Definition timestamp_t : ty := Timestamp_t.
Definition address_t : ty := Address_t.
Definition bool_t : ty := Bool_t.
Definition tx_rollup_l2_address_t : ty := Tx_rollup_l2_address_t.
Definition pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Pair_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition pair_3_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (m_value : ty)
(r_value : ty) : M? ty_ex_c :=
let? 'Ty_ex_c r_value := pair_t loc_value m_value r_value in
pair_t loc_value l_value r_value.
Definition comparable_pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Pair_t l_value r_value {| ty_metadata.size := size_value; |}
Dependent_bool.YesYes).
Definition comparable_pair_3_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (m_value : ty)
(r_value : ty) : M? ty :=
let? r_value := comparable_pair_t loc_value m_value r_value in
comparable_pair_t loc_value l_value r_value.
Definition union_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Union_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition union_bytes_bool_t : ty :=
Union_t bytes_t bool_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes.
Definition comparable_union_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Union_t l_value r_value {| ty_metadata.size := size_value; |}
Dependent_bool.YesYes).
Definition lambda_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Lambda_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition option_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
let cmp := is_comparable t_value in
return? (Option_t t_value {| ty_metadata.size := size_value; |} cmp).
Definition option_mutez_t : ty :=
Option_t mutez_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_string_t : ty :=
Option_t string_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_bytes_t : ty :=
Option_t bytes_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_nat_t : ty :=
Option_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}
Dependent_bool.Yes.
Definition option_pair_nat_nat_t : ty :=
Option_t
(Pair_t nat_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_nat_mutez_t : ty :=
Option_t
(Pair_t nat_t mutez_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_mutez_mutez_t : ty :=
Option_t
(Pair_t mutez_t mutez_t
{| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition option_pair_int_nat_t : ty :=
Option_t
(Pair_t int_t nat_t {| ty_metadata.size := Type_size.(TYPE_SIZE.three); |}
Dependent_bool.YesYes)
{| ty_metadata.size := Type_size.(TYPE_SIZE.four); |} Dependent_bool.Yes.
Definition list_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (List_t t_value {| ty_metadata.size := size_value; |}).
Definition operation_t : ty := Operation_t.
Definition list_operation_t : ty :=
List_t operation_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}.
Definition set_t
(loc_value : Alpha_context.Script.location) (t_value : comparable_ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Set_t t_value {| ty_metadata.size := size_value; |}).
Definition map_t
(loc_value : Alpha_context.Script.location) (l_value : comparable_ty)
(r_value : ty) : M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Map_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition big_map_t
(loc_value : Alpha_context.Script.location) (l_value : comparable_ty)
(r_value : ty) : M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return? (Big_map_t l_value r_value {| ty_metadata.size := size_value; |}).
Definition contract_t (loc_value : Alpha_context.Script.location) (t_value : ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Contract_t t_value {| ty_metadata.size := size_value; |}).
Definition contract_unit_t : ty :=
Contract_t unit_t {| ty_metadata.size := Type_size.(TYPE_SIZE.two); |}.
Definition sapling_transaction_t (memo_size : Alpha_context.Sapling.Memo_size.t)
: ty := Sapling_transaction_t memo_size.
Definition sapling_transaction_deprecated_t
(memo_size : Alpha_context.Sapling.Memo_size.t) : ty :=
Sapling_transaction_deprecated_t memo_size.
Definition sapling_state_t (memo_size : Alpha_context.Sapling.Memo_size.t)
: ty := Sapling_state_t memo_size.
Definition chain_id_t : ty := Chain_id_t.
Definition never_t : ty := Never_t.
Definition bls12_381_g1_t : ty := Bls12_381_g1_t.
Definition bls12_381_g2_t : ty := Bls12_381_g2_t.
Definition bls12_381_fr_t : ty := Bls12_381_fr_t.
Definition ticket_t
(loc_value : Alpha_context.Script.location) (t_value : comparable_ty)
: M? ty :=
let? size_value := Type_size.(TYPE_SIZE.compound1) loc_value (ty_size t_value)
in
return? (Ticket_t t_value {| ty_metadata.size := size_value; |}).
Definition chest_key_t : ty := Chest_key_t.
Definition chest_t : ty := Chest_t.
Module kinstr_traverse.
Record record {a : Set} : Set := Build {
apply : a → kinstr → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End kinstr_traverse.
Definition kinstr_traverse := kinstr_traverse.record.
Definition kinstr_traverse_value {accu : Set}
(i_value : kinstr) (init_value : accu) (f_value : kinstr_traverse accu)
: accu :=
let fix aux {ret : Set}
(accu_value : accu) (t_value : kinstr) (continue : accu → ret) : ret :=
let accu_value := f_value.(kinstr_traverse.apply) accu_value t_value in
let next (k_value : kinstr) : ret :=
aux accu_value k_value (fun (accu_value : accu) ⇒ continue accu_value) in
let next2 (k1 : kinstr) (k2 : kinstr) : ret :=
aux accu_value k1
(fun (accu_value : accu) ⇒
aux accu_value k2 (fun (accu_value : accu) ⇒ continue accu_value)) in
let next3 (k1 : kinstr) (k2 : kinstr) (k3 : kinstr) : ret :=
aux accu_value k1
(fun (accu_value : accu) ⇒
aux accu_value k2
(fun (accu_value : accu) ⇒
aux accu_value k3 (fun (accu_value : accu) ⇒ continue accu_value)))
in
let _return (function_parameter : unit) : ret :=
let '_ := function_parameter in
continue accu_value in
match t_value with
| IDrop _ k_value ⇒ next k_value
| IDup _ k_value ⇒ next k_value
| ISwap _ k_value ⇒ next k_value
| IConst _ _ _ k_value ⇒ next k_value
| ICons_pair _ k_value ⇒ next k_value
| ICar _ k_value ⇒ next k_value
| ICdr _ k_value ⇒ next k_value
| IUnpair _ k_value ⇒ next k_value
| ICons_some _ k_value ⇒ next k_value
| ICons_none _ _ k_value ⇒ next k_value
|
IIf_none {|
kinstr.IIf_none.loc := _;
kinstr.IIf_none.branch_if_none := k1;
kinstr.IIf_none.branch_if_some := k2;
kinstr.IIf_none.k := k_value
|} ⇒ next3 k1 k2 k_value
|
IOpt_map {|
kinstr.IOpt_map.loc := _;
kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value
|} ⇒ next2 body k_value
| ICons_left _ _ k_value ⇒ next k_value
| ICons_right _ _ k_value ⇒ next k_value
|
IIf_left {|
kinstr.IIf_left.loc := _;
kinstr.IIf_left.branch_if_left := k1;
kinstr.IIf_left.branch_if_right := k2;
kinstr.IIf_left.k := k_value
|} ⇒ next3 k1 k2 k_value
| ICons_list _ k_value ⇒ next k_value
| INil _ _ k_value ⇒ next k_value
|
IIf_cons {|
kinstr.IIf_cons.loc := _;
kinstr.IIf_cons.branch_if_cons := k2;
kinstr.IIf_cons.branch_if_nil := k1;
kinstr.IIf_cons.k := k_value
|} ⇒ next3 k1 k2 k_value
| IList_map _ k1 _ k2 ⇒ next2 k1 k2
| IList_iter _ _ k1 k2 ⇒ next2 k1 k2
| IList_size _ k_value ⇒ next k_value
| IEmpty_set _ _ k_value ⇒ next k_value
| ISet_iter _ _ k1 k2 ⇒ next2 k1 k2
| ISet_mem _ k_value ⇒ next k_value
| ISet_update _ k_value ⇒ next k_value
| ISet_size _ k_value ⇒ next k_value
| IEmpty_map _ _ _ k_value ⇒ next k_value
| IMap_map _ _ k1 k2 ⇒ next2 k1 k2
| IMap_iter _ _ k1 k2 ⇒ next2 k1 k2
| IMap_mem _ k_value ⇒ next k_value
| IMap_get _ k_value ⇒ next k_value
| IMap_update _ k_value ⇒ next k_value
| IMap_get_and_update _ k_value ⇒ next k_value
| IMap_size _ k_value ⇒ next k_value
| IEmpty_big_map _ _ _ k_value ⇒ next k_value
| IBig_map_mem _ k_value ⇒ next k_value
| IBig_map_get _ k_value ⇒ next k_value
| IBig_map_update _ k_value ⇒ next k_value
| IBig_map_get_and_update _ k_value ⇒ next k_value
| IConcat_string _ k_value ⇒ next k_value
| IConcat_string_pair _ k_value ⇒ next k_value
| ISlice_string _ k_value ⇒ next k_value
| IString_size _ k_value ⇒ next k_value
| IConcat_bytes _ k_value ⇒ next k_value
| IConcat_bytes_pair _ k_value ⇒ next k_value
| ISlice_bytes _ k_value ⇒ next k_value
| IBytes_size _ k_value ⇒ next k_value
| ILsl_bytes _ k_value ⇒ next k_value
| ILsr_bytes _ k_value ⇒ next k_value
| IOr_bytes _ k_value ⇒ next k_value
| IAnd_bytes _ k_value ⇒ next k_value
| IXor_bytes _ k_value ⇒ next k_value
| INot_bytes _ k_value ⇒ next k_value
| IAdd_seconds_to_timestamp _ k_value ⇒ next k_value
| IAdd_timestamp_to_seconds _ k_value ⇒ next k_value
| ISub_timestamp_seconds _ k_value ⇒ next k_value
| IDiff_timestamps _ k_value ⇒ next k_value
| IAdd_tez _ k_value ⇒ next k_value
| ISub_tez _ k_value ⇒ next k_value
| ISub_tez_legacy _ k_value ⇒ next k_value
| IMul_teznat _ k_value ⇒ next k_value
| IMul_nattez _ k_value ⇒ next k_value
| IEdiv_teznat _ k_value ⇒ next k_value
| IEdiv_tez _ k_value ⇒ next k_value
| IOr _ k_value ⇒ next k_value
| IAnd _ k_value ⇒ next k_value
| IXor _ k_value ⇒ next k_value
| INot _ k_value ⇒ next k_value
| IIs_nat _ k_value ⇒ next k_value
| INeg _ k_value ⇒ next k_value
| IAbs_int _ k_value ⇒ next k_value
| IInt_nat _ k_value ⇒ next k_value
| IAdd_int _ k_value ⇒ next k_value
| IAdd_nat _ k_value ⇒ next k_value
| ISub_int _ k_value ⇒ next k_value
| IMul_int _ k_value ⇒ next k_value
| IMul_nat _ k_value ⇒ next k_value
| IEdiv_int _ k_value ⇒ next k_value
| IEdiv_nat _ k_value ⇒ next k_value
| ILsl_nat _ k_value ⇒ next k_value
| ILsr_nat _ k_value ⇒ next k_value
| IOr_nat _ k_value ⇒ next k_value
| IAnd_nat _ k_value ⇒ next k_value
| IAnd_int_nat _ k_value ⇒ next k_value
| IXor_nat _ k_value ⇒ next k_value
| INot_int _ k_value ⇒ next k_value
|
IIf {|
kinstr.IIf.loc := _;
kinstr.IIf.branch_if_true := k1;
kinstr.IIf.branch_if_false := k2;
kinstr.IIf.k := k_value
|} ⇒ next3 k1 k2 k_value
| ILoop _ k1 k2 ⇒ next2 k1 k2
| ILoop_left _ k1 k2 ⇒ next2 k1 k2
| IDip _ k1 _ k2 ⇒ next2 k1 k2
| IExec _ _ k_value ⇒ next k_value
| IApply _ _ k_value ⇒ next k_value
| ILambda _ _ k_value ⇒ next k_value
| IFailwith _ _ ⇒ _return tt
| ICompare _ _ k_value ⇒ next k_value
| IEq _ k_value ⇒ next k_value
| INeq _ k_value ⇒ next k_value
| ILt _ k_value ⇒ next k_value
| IGt _ k_value ⇒ next k_value
| ILe _ k_value ⇒ next k_value
| IGe _ k_value ⇒ next k_value
| IAddress _ k_value ⇒ next k_value
| IContract _ _ _ k_value ⇒ next k_value
| IView _ _ _ k_value ⇒ next k_value
| ITransfer_tokens _ k_value ⇒ next k_value
| IImplicit_account _ k_value ⇒ next k_value
| ICreate_contract {| kinstr.ICreate_contract.k := k_value |} ⇒
next k_value
| ISet_delegate _ k_value ⇒ next k_value
| INow _ k_value ⇒ next k_value
| IMin_block_time _ k_value ⇒ next k_value
| IBalance _ k_value ⇒ next k_value
| ILevel _ k_value ⇒ next k_value
| ICheck_signature _ k_value ⇒ next k_value
| IHash_key _ k_value ⇒ next k_value
| IPack _ _ k_value ⇒ next k_value
| IUnpack _ _ k_value ⇒ next k_value
| IBlake2b _ k_value ⇒ next k_value
| ISha256 _ k_value ⇒ next k_value
| ISha512 _ k_value ⇒ next k_value
| ISource _ k_value ⇒ next k_value
| ISender _ k_value ⇒ next k_value
| ISelf _ _ _ k_value ⇒ next k_value
| ISelf_address _ k_value ⇒ next k_value
| IAmount _ k_value ⇒ next k_value
| ISapling_empty_state _ _ k_value ⇒ next k_value
| ISapling_verify_update _ k_value ⇒ next k_value
| ISapling_verify_update_deprecated _ k_value ⇒ next k_value
| IDig _ _ _ k_value ⇒ next k_value
| IDug _ _ _ k_value ⇒ next k_value
| IDipn _ _ _ k1 k2 ⇒ next2 k1 k2
| IDropn _ _ _ k_value ⇒ next k_value
| IChainId _ k_value ⇒ next k_value
| INever _ ⇒ _return tt
| IVoting_power _ k_value ⇒ next k_value
| ITotal_voting_power _ k_value ⇒ next k_value
| IKeccak _ k_value ⇒ next k_value
| ISha3 _ k_value ⇒ next k_value
| IAdd_bls12_381_g1 _ k_value ⇒ next k_value
| IAdd_bls12_381_g2 _ k_value ⇒ next k_value
| IAdd_bls12_381_fr _ k_value ⇒ next k_value
| IMul_bls12_381_g1 _ k_value ⇒ next k_value
| IMul_bls12_381_g2 _ k_value ⇒ next k_value
| IMul_bls12_381_fr _ k_value ⇒ next k_value
| IMul_bls12_381_z_fr _ k_value ⇒ next k_value
| IMul_bls12_381_fr_z _ k_value ⇒ next k_value
| IInt_bls12_381_fr _ k_value ⇒ next k_value
| INeg_bls12_381_g1 _ k_value ⇒ next k_value
| INeg_bls12_381_g2 _ k_value ⇒ next k_value
| INeg_bls12_381_fr _ k_value ⇒ next k_value
| IPairing_check_bls12_381 _ k_value ⇒ next k_value
| IComb _ _ _ k_value ⇒ next k_value
| IUncomb _ _ _ k_value ⇒ next k_value
| IComb_get _ _ _ k_value ⇒ next k_value
| IComb_set _ _ _ k_value ⇒ next k_value
| IDup_n _ _ _ k_value ⇒ next k_value
| ITicket _ _ k_value ⇒ next k_value
| ITicket_deprecated _ _ k_value ⇒ next k_value
| IRead_ticket _ _ k_value ⇒ next k_value
| ISplit_ticket _ k_value ⇒ next k_value
| IJoin_tickets _ _ k_value ⇒ next k_value
| IOpen_chest _ k_value ⇒ next k_value
| IEmit {| kinstr.IEmit.k := k_value |} ⇒ next k_value
| IHalt _ ⇒ _return tt
| ILog _ _ _ _ k_value ⇒ next k_value
end in
aux init_value i_value (fun (accu_value : accu) ⇒ accu_value).
Module ty_traverse.
Record record {a : Set} : Set := Build {
apply : a → ty → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End ty_traverse.
Definition ty_traverse := ty_traverse.record.
Module Ty_traverse.
Reserved Notation "'next2".
Reserved Notation "'next".
Fixpoint aux {accu ret : Set}
(f_value : ty_traverse accu) (accu_value : accu) (ty_value : ty)
(continue : accu → ret) : ret :=
let next2 {accu ret} := 'next2 accu ret in
let next {accu ret} := 'next accu ret in
let accu_value := f_value.(ty_traverse.apply) accu_value ty_value in
match ty_value with
|
(Unit_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t | Mutez_t |
Key_hash_t | Key_t | Timestamp_t | Address_t | Tx_rollup_l2_address_t |
Bool_t | Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Chain_id_t | Never_t | Bls12_381_g1_t |
Bls12_381_g2_t | Bls12_381_fr_t) ⇒ continue accu_value
| Ticket_t cty _ ⇒ aux f_value accu_value cty continue
| (Chest_key_t | Chest_t) ⇒ continue accu_value
| Pair_t ty1 ty2 _ _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Union_t ty1 ty2 _ _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Lambda_t ty1 ty2 _ ⇒ next2 f_value accu_value ty1 ty2 continue
| Option_t ty1 _ _ ⇒ next f_value accu_value ty1 continue
| List_t ty1 _ ⇒ next f_value accu_value ty1 continue
| Set_t cty _ ⇒ aux f_value accu_value cty continue
| Map_t cty ty1 _ ⇒
aux f_value accu_value cty
(fun (accu_value : accu) ⇒ next f_value accu_value ty1 continue)
| Big_map_t cty ty1 _ ⇒
aux f_value accu_value cty
(fun (accu_value : accu) ⇒ next f_value accu_value ty1 continue)
| Contract_t ty1 _ ⇒ next f_value accu_value ty1 continue
end
where "'next2" :=
(fun (accu ret : Set) ⇒ fun
(f_value : ty_traverse accu) (accu_value : accu) (ty1 : ty) (ty2 : ty)
(continue : accu → ret) ⇒
aux f_value accu_value ty1
(fun (accu_value : accu) ⇒
aux f_value accu_value ty2
(fun (accu_value : accu) ⇒ continue accu_value)))
and "'next" :=
(fun (accu ret : Set) ⇒ fun
(f_value : ty_traverse accu) (accu_value : accu) (ty1 : ty)
(continue : accu → ret) ⇒
aux f_value accu_value ty1
(fun (accu_value : accu) ⇒ continue accu_value)).
Definition next2 {accu ret : Set} := 'next2 accu ret.
Definition next {accu ret : Set} := 'next accu ret.
End Ty_traverse.
Definition ty_traverse_value {A : Set}
(ty_value : ty) (init_value : A) (f_value : ty_traverse A) : A :=
Ty_traverse.aux f_value init_value ty_value
(fun (accu_value : A) ⇒ accu_value).
Module stack_ty_traverse.
Record record {accu : Set} : Set := Build {
apply : accu → stack_ty → accu;
}.
Arguments record : clear implicits.
Definition with_apply {t_accu} apply (r : record t_accu) :=
Build t_accu apply.
End stack_ty_traverse.
Definition stack_ty_traverse := stack_ty_traverse.record.
Definition stack_ty_traverse_value {accu : Set}
(sty : stack_ty) (init_value : accu) (f_value : stack_ty_traverse accu)
: accu :=
let fix aux (accu_value : accu) (sty : stack_ty) : accu :=
match sty with
| Bot_t ⇒ f_value.(stack_ty_traverse.apply) accu_value sty
| Item_t _ sty' ⇒
aux (f_value.(stack_ty_traverse.apply) accu_value sty) sty'
end in
aux init_value sty.
Module value_traverse.
Record record {a : Set} : Set := Build {
apply : ∀ {t : Set}, a → ty → t → a;
}.
Arguments record : clear implicits.
Definition with_apply {t_a} apply (r : record t_a) :=
Build t_a apply.
End value_traverse.
Definition value_traverse := value_traverse.record.
Module Value_traverse.
#[bypass_check(guard)]
Fixpoint aux {accu t ret : Set}
(f_value : value_traverse accu) (accu_value : accu) (ty_value : ty)
(x_value : t) (continue : accu → ret) {struct ty_value} : ret :=
let accu_value := f_value.(value_traverse.apply) accu_value ty_value x_value
in
let next2 {D E : Set} (ty1 : ty) (ty2 : ty) (x1 : D) (x2 : E) : ret :=
aux f_value accu_value ty1 x1
(fun (accu_value : accu) ⇒
aux f_value accu_value ty2 x2
(fun (accu_value : accu) ⇒ continue accu_value)) in
let next {D : Set} (ty1 : ty) (x1 : D) : ret :=
aux f_value accu_value ty1 x1
(fun (accu_value : accu) ⇒ continue accu_value) in
let _return (function_parameter : unit) : ret :=
let '_ := function_parameter in
continue accu_value in
let fix on_list {D : Set}
(ty' : ty) (accu_value : accu) (function_parameter : list D) : ret :=
match function_parameter with
| [] ⇒ continue accu_value
| cons x_value xs ⇒
aux f_value accu_value ty' x_value
(fun (accu_value : accu) ⇒ on_list ty' accu_value xs)
end in
match (ty_value, x_value) with
|
((Unit_t, _) | (Int_t, _) | (Nat_t, _) | (Signature_t, _) | (String_t, _)
| (Bytes_t, _) | (Mutez_t, _) | (Key_hash_t, _) | (Key_t, _) |
(Timestamp_t, _) | (Address_t, _) | (Tx_rollup_l2_address_t, _) |
(Bool_t, _) | (Sapling_transaction_t _, _) |
(Sapling_transaction_deprecated_t _, _) | (Sapling_state_t _, _) |
(Operation_t, _) | (Chain_id_t, _) | (Never_t, _) | (Bls12_381_g1_t, _) |
(Bls12_381_g2_t, _) | (Bls12_381_fr_t, _) | (Chest_key_t, _) |
(Chest_t, _) | (Lambda_t _ _ _, _)) ⇒ _return tt
| (Pair_t ty1 ty2 _ _, x_value) ⇒
let 'existT _ [__2, __3] [x_value, ty2, ty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒ [__2 × __3 ** ty ** ty]) [x_value, ty2, ty1] in
next2 ty1 ty2 (Pervasives.fst x_value) (Pervasives.snd x_value)
| (Union_t ty1 ty2 _ _, x_value) ⇒
let 'existT _ [__4, __5] [x_value, ty2, ty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__4, __5] ⇒ [union __4 __5 ** ty ** ty]) [x_value, ty2, ty1]
in
match x_value with
| L l_value ⇒ next ty1 l_value
| R r_value ⇒ next ty2 r_value
end
| (Option_t ty_value _ _, x_value) ⇒
let 'existT _ __6 [x_value, ty_value] :=
cast_exists (Es := Set) (fun __6 ⇒ [option __6 ** ty])
[x_value, ty_value] in
match x_value with
| None ⇒ _return tt
| Some v_value ⇒ next ty_value v_value
end
| (Ticket_t cty _, x_value) ⇒
let 'existT _ __7 [x_value, cty] :=
cast_exists (Es := Set) (fun __7 ⇒ [ticket __7 ** comparable_ty])
[x_value, cty] in
aux f_value accu_value cty x_value.(ticket.contents) continue
| (List_t ty' _, x_value) ⇒
let 'existT _ __8 [x_value, ty'] :=
cast_exists (Es := Set) (fun __8 ⇒ [Script_list.t __8 ** ty])
[x_value, ty'] in
on_list ty' accu_value x_value.(Script_list.t.elements)
| (Map_t kty ty' _, x_value) ⇒
let 'existT _ [__9, __10] [x_value, ty', kty] :=
cast_exists (Es := [Set ** Set])
(fun '[__9, __10] ⇒ [map __9 __10 ** ty ** comparable_ty])
[x_value, ty', kty] in
let 'Map_tag M := x_value in
let 'existS _ _ M := M in
let bindings :=
M.(Boxed_map.OPS).(Boxed_map_OPS.fold)
(fun (k_value : __9) ⇒
fun (v_value : __10) ⇒
fun (bs : list (__9 × __10)) ⇒ cons (k_value, v_value) bs)
M.(Boxed_map.boxed) nil in
on_bindings f_value accu_value kty ty' continue bindings
| (Set_t ty' _, x_value) ⇒
let 'existT _ __11 [x_value, ty'] :=
cast_exists (Es := Set) (fun __11 ⇒ [set __11 ** comparable_ty])
[x_value, ty'] in
let 'Set_tag M := x_value in
let 'existS _ _ M := M in
let elements :=
M.(Boxed_set.OPS).(Boxed_set_OPS.fold)
(fun (x_value : __11) ⇒
fun (s_value : list __11) ⇒ cons x_value s_value)
M.(Boxed_set.boxed) nil in
on_list ty' accu_value elements
| (Big_map_t _ _ _, _) ⇒ _return tt
| (Contract_t _ _, _) ⇒ _return tt
end
with on_bindings {accu ret k v : Set}
(f_value : value_traverse accu) (accu_value : accu) (kty : comparable_ty)
(ty' : ty) (continue : accu → ret) (xs : list (k × v)) {struct xs} : ret :=
match xs with
| [] ⇒ continue accu_value
| cons (k_value, v_value) xs ⇒
aux f_value accu_value kty k_value
(fun (accu_value : accu) ⇒
aux f_value accu_value ty' v_value
(fun (accu_value : accu) ⇒
on_bindings f_value accu_value kty ty' continue xs))
end.
End Value_traverse.
Definition value_traverse_value {t B : Set}
(ty_value : ty) (x_value : t) (init_value : B) (f_value : value_traverse B)
: B :=
Value_traverse.aux f_value init_value ty_value x_value
(fun (accu_value : B) ⇒ accu_value).
Definition stack_top_ty (function_parameter : stack_ty) : ty_ex_c :=
match function_parameter with
| Item_t ty_value _ ⇒ Ty_ex_c ty_value
| _ ⇒ unreachable_gadt_branch
end.
Module Typed_contract.
Definition destination (function_parameter : typed_contract)
: Alpha_context.Destination.t :=
match function_parameter with
| Typed_implicit pkh ⇒
Alpha_context.Destination.Contract (Contract_repr.Implicit pkh)
|
Typed_originated {|
typed_contract.Typed_originated.contract_hash := contract_hash |} ⇒
Alpha_context.Destination.Contract
(Contract_repr.Originated contract_hash)
|
Typed_tx_rollup {|
typed_contract.Typed_tx_rollup.tx_rollup := tx_rollup |} ⇒
Alpha_context.Destination.Tx_rollup tx_rollup
|
Typed_sc_rollup {|
typed_contract.Typed_sc_rollup.sc_rollup := sc_rollup |} ⇒
Alpha_context.Destination.Sc_rollup sc_rollup
|
Typed_zk_rollup {|
typed_contract.Typed_zk_rollup.zk_rollup := zk_rollup |} ⇒
Alpha_context.Destination.Zk_rollup zk_rollup
end.
Definition arg_ty (function_parameter : typed_contract) : ty_ex_c :=
match function_parameter with
| Typed_implicit _ ⇒ Ty_ex_c Unit_t
| Typed_originated {| typed_contract.Typed_originated.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_tx_rollup {| typed_contract.Typed_tx_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_sc_rollup {| typed_contract.Typed_sc_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
| Typed_zk_rollup {| typed_contract.Typed_zk_rollup.arg_ty := arg_ty |} ⇒
Ty_ex_c arg_ty
end.
Definition entrypoint (function_parameter : typed_contract)
: Alpha_context.Entrypoint.t :=
match function_parameter with
| Typed_implicit _ ⇒ Alpha_context.Entrypoint.default
| Typed_tx_rollup _ ⇒ Alpha_context.Entrypoint.deposit
|
(Typed_originated {|
typed_contract.Typed_originated.entrypoint := entrypoint |} |
Typed_sc_rollup {|
typed_contract.Typed_sc_rollup.entrypoint := entrypoint |}) ⇒
entrypoint
| Typed_zk_rollup _ ⇒ Alpha_context.Entrypoint.deposit
end.
End Typed_contract.