🍬 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" :=
(
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" :=
(