🍬 Script_typed_ir.v
Translated OCaml
See proofs, See simulations, Gitlab , OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Unset Positivity Checking.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Module step_constants.
Record record : Set := Build {
source : Alpha_context.Contract.t;
payer : Alpha_context.Contract.t;
self : Alpha_context.Contract.t;
amount : Alpha_context.Tez.t;
balance : Alpha_context.Tez.t;
chain_id : Chain_id.t;
now : Alpha_context.Script_timestamp.t;
level : Alpha_context.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.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 (Bls12_381.Fr.(S.PRIME_FIELD.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls12_381.Fr.(S.PRIME_FIELD.t)) ⇒ Fr_tag x_value)
(Bls12_381.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
Bls12_381.Fr.(S.PRIME_FIELD.to_bytes) x_value.
Definition of_z (z_value : Z.t) : t :=
Fr_tag (Bls12_381.Fr.(S.PRIME_FIELD.of_z) z_value).
Definition to_z (function_parameter : t) : Z.t :=
let 'Fr_tag x_value := function_parameter in
Bls12_381.Fr.(S.PRIME_FIELD.to_z) x_value.
End Fr.
Module G1.
Inductive t : Set :=
| G1_tag : Bls12_381.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 (Bls12_381.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 (Bls12_381.G1.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G1_tag x_value := function_parameter in
G1_tag (Bls12_381.G1.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map (fun (x_value : Bls12_381.G1.(S.CURVE.t)) ⇒ G1_tag x_value)
(Bls12_381.G1.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G1_tag x_value := function_parameter in
Bls12_381.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.G2.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G2_tag x_value := function_parameter in
G2_tag (Bls12_381.G2.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map (fun (x_value : Bls12_381.G2.(S.CURVE.t)) ⇒ G2_tag x_value)
(Bls12_381.G2.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G2_tag x_value := function_parameter in
Bls12_381.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
Bls12_381.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.
Module ticket.
Record record {a : Set} : Set := Build {
ticketer : Alpha_context.Contract.t;
contents : a;
amount : Alpha_context.Script_int.num;
}.
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_trace : Set},
Script_tc_errors.error_details → 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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Module step_constants.
Record record : Set := Build {
source : Alpha_context.Contract.t;
payer : Alpha_context.Contract.t;
self : Alpha_context.Contract.t;
amount : Alpha_context.Tez.t;
balance : Alpha_context.Tez.t;
chain_id : Chain_id.t;
now : Alpha_context.Script_timestamp.t;
level : Alpha_context.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.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 (Bls12_381.Fr.(S.PRIME_FIELD.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map
(fun (x_value : Bls12_381.Fr.(S.PRIME_FIELD.t)) ⇒ Fr_tag x_value)
(Bls12_381.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
Bls12_381.Fr.(S.PRIME_FIELD.to_bytes) x_value.
Definition of_z (z_value : Z.t) : t :=
Fr_tag (Bls12_381.Fr.(S.PRIME_FIELD.of_z) z_value).
Definition to_z (function_parameter : t) : Z.t :=
let 'Fr_tag x_value := function_parameter in
Bls12_381.Fr.(S.PRIME_FIELD.to_z) x_value.
End Fr.
Module G1.
Inductive t : Set :=
| G1_tag : Bls12_381.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 (Bls12_381.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 (Bls12_381.G1.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G1_tag x_value := function_parameter in
G1_tag (Bls12_381.G1.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map (fun (x_value : Bls12_381.G1.(S.CURVE.t)) ⇒ G1_tag x_value)
(Bls12_381.G1.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G1_tag x_value := function_parameter in
Bls12_381.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 : Bls12_381.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 (Bls12_381.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 (Bls12_381.G2.(S.CURVE.mul) x_value y_value).
Definition negate (function_parameter : t) : t :=
let 'G2_tag x_value := function_parameter in
G2_tag (Bls12_381.G2.(S.CURVE.negate) x_value).
Definition of_bytes_opt (bytes_value : Bytes.t) : option t :=
Option.map (fun (x_value : Bls12_381.G2.(S.CURVE.t)) ⇒ G2_tag x_value)
(Bls12_381.G2.(S.CURVE.of_bytes_opt) bytes_value).
Definition to_bytes (function_parameter : t) : Bytes.t :=
let 'G2_tag x_value := function_parameter in
Bls12_381.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
Bls12_381.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.
Module ticket.
Record record {a : Set} : Set := Build {
ticketer : Alpha_context.Contract.t;
contents : a;
amount : Alpha_context.Script_int.num;
}.
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_trace : Set},
Script_tc_errors.error_details → 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 {error_trace : Set}
(error_details : Script_tc_errors.error_details) (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 boxed_list.
Record record {elt : Set} : Set := Build {
elements : list elt;
length : int;
}.
Arguments record : clear implicits.
Definition with_elements {t_elt} elements (r : record t_elt) :=
Build t_elt elements r.(length).
Definition with_length {t_elt} length (r : record t_elt) :=
Build t_elt r.(elements) length.
End boxed_list.
Definition boxed_list := boxed_list.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 Alpha_context.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 {error_trace : Set}
(error_details : Script_tc_errors.error_details) (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 boxed_list.
Record record {elt : Set} : Set := Build {
elements : list elt;
length : int;
}.
Arguments record : clear implicits.
Definition with_elements {t_elt} elements (r : record t_elt) :=
Build t_elt elements r.(length).
Definition with_length {t_elt} length (r : record t_elt) :=
Build t_elt r.(elements) length.
End boxed_list.
Definition boxed_list := boxed_list.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 Alpha_context.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; |}.
Module entrypoints.
Record record : Set := Build {
root : entrypoints_node;
original_type_expr : Alpha_context.Script.node;
}.
Definition with_root root (r : record) :=
Build root r.(original_type_expr).
Definition with_original_type_expr original_type_expr (r : record) :=
Build r.(root) original_type_expr.
End entrypoints.
Definition entrypoints := entrypoints.record.
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; |}.
Module entrypoints.
Record record : Set := Build {
root : entrypoints_node;
original_type_expr : Alpha_context.Script.node;
}.
Definition with_root root (r : record) :=
Build root r.(original_type_expr).
Definition with_original_type_expr original_type_expr (r : record) :=
Build r.(root) original_type_expr.
End entrypoints.
Definition entrypoints := entrypoints.record.
Records for the constructor parameters
Module
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
Module script.
Module Script.
Record record {code arg_type storage storage_type views entrypoints
code_size : Set} : Set := Build {
code : code;
arg_type : arg_type;
storage : storage;
storage_type : storage_type;
views : views;
entrypoints : entrypoints;
code_size : code_size;
}.
Arguments record : clear implicits.
Definition with_code
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size code r.(arg_type) r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_arg_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} arg_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) arg_type r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) storage r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) storage_type r.(views)
r.(entrypoints) r.(code_size).
Definition with_views
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} views
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type) views
r.(entrypoints) r.(code_size).
Definition with_entrypoints
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} entrypoints
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) entrypoints r.(code_size).
Definition with_code_size
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code_size
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) r.(entrypoints) code_size.
End Script.
Definition Script_skeleton := Script.record.
End script.
Module kinstr.
Module IIf_none.
Record record {kinfo branch_if_none branch_if_some k : Set} : Set := Build {
kinfo : kinfo;
branch_if_none : branch_if_none;
branch_if_some : branch_if_some;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_none t_branch_if_some t_k}
kinfo (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k kinfo
r.(branch_if_none) r.(branch_if_some) r.(k).
Definition with_branch_if_none
{t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_none
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
branch_if_none r.(branch_if_some) r.(k).
Definition with_branch_if_some
{t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_some
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
r.(branch_if_none) branch_if_some r.(k).
Definition with_k {t_kinfo t_branch_if_none t_branch_if_some t_k} k
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
r.(branch_if_none) r.(branch_if_some) k.
End IIf_none.
Definition IIf_none_skeleton := IIf_none.record.
Module IOpt_map.
Record record {kinfo body k : Set} : Set := Build {
kinfo : kinfo;
body : body;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_body t_k} kinfo
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k kinfo r.(body) r.(k).
Definition with_body {t_kinfo t_body t_k} body
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k r.(kinfo) body r.(k).
Definition with_k {t_kinfo t_body t_k} k
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k r.(kinfo) r.(body) k.
End IOpt_map.
Definition IOpt_map_skeleton := IOpt_map.record.
Module IIf_left.
Record record {kinfo branch_if_left branch_if_right k : Set} : Set := Build {
kinfo : kinfo;
branch_if_left : branch_if_left;
branch_if_right : branch_if_right;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_left t_branch_if_right t_k}
kinfo (r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k kinfo
r.(branch_if_left) r.(branch_if_right) r.(k).
Definition with_branch_if_left
{t_kinfo t_branch_if_left t_branch_if_right t_k} branch_if_left
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
branch_if_left r.(branch_if_right) r.(k).
Definition with_branch_if_right
{t_kinfo t_branch_if_left t_branch_if_right t_k} branch_if_right
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
r.(branch_if_left) branch_if_right r.(k).
Definition with_k {t_kinfo t_branch_if_left t_branch_if_right t_k} k
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
r.(branch_if_left) r.(branch_if_right) k.
End IIf_left.
Definition IIf_left_skeleton := IIf_left.record.
Module IIf_cons.
Record record {kinfo branch_if_cons branch_if_nil k : Set} : Set := Build {
kinfo : kinfo;
branch_if_cons : branch_if_cons;
branch_if_nil : branch_if_nil;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_cons t_branch_if_nil t_k} kinfo
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k kinfo
r.(branch_if_cons) r.(branch_if_nil) r.(k).
Definition with_branch_if_cons
{t_kinfo t_branch_if_cons t_branch_if_nil t_k} branch_if_cons
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
branch_if_cons r.(branch_if_nil) r.(k).
Definition with_branch_if_nil
{t_kinfo t_branch_if_cons t_branch_if_nil t_k} branch_if_nil
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
r.(branch_if_cons) branch_if_nil r.(k).
Definition with_k {t_kinfo t_branch_if_cons t_branch_if_nil t_k} k
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
r.(branch_if_cons) r.(branch_if_nil) k.
End IIf_cons.
Definition IIf_cons_skeleton := IIf_cons.record.
Module IIf.
Record record {kinfo branch_if_true branch_if_false k : Set} : Set := Build {
kinfo : kinfo;
branch_if_true : branch_if_true;
branch_if_false : branch_if_false;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_true t_branch_if_false t_k}
kinfo (r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k kinfo
r.(branch_if_true) r.(branch_if_false) r.(k).
Definition with_branch_if_true
{t_kinfo t_branch_if_true t_branch_if_false t_k} branch_if_true
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
branch_if_true r.(branch_if_false) r.(k).
Definition with_branch_if_false
{t_kinfo t_branch_if_true t_branch_if_false t_k} branch_if_false
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
r.(branch_if_true) branch_if_false r.(k).
Definition with_k {t_kinfo t_branch_if_true t_branch_if_false t_k} k
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
r.(branch_if_true) r.(branch_if_false) k.
End IIf.
Definition IIf_skeleton := IIf.record.
Module ICreate_contract.
Record record {kinfo storage_type code k : Set} : Set := Build {
kinfo : kinfo;
storage_type : storage_type;
code : code;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_storage_type t_code t_k} kinfo
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k kinfo r.(storage_type) r.(code)
r.(k).
Definition with_storage_type {t_kinfo t_storage_type t_code t_k}
storage_type (r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) storage_type r.(code)
r.(k).
Definition with_code {t_kinfo t_storage_type t_code t_k} code
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type) code
r.(k).
Definition with_k {t_kinfo t_storage_type t_code t_k} k
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type)
r.(code) k.
End ICreate_contract.
Definition ICreate_contract_skeleton := ICreate_contract.record.
End kinstr.
Module typed_contract.
Module Typed_contract.
Record record {arg_ty address : Set} : Set := Build {
arg_ty : arg_ty;
address : address;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_address} arg_ty
(r : record t_arg_ty t_address) :=
Build t_arg_ty t_address arg_ty r.(address).
Definition with_address {t_arg_ty t_address} address
(r : record t_arg_ty t_address) :=
Build t_arg_ty t_address r.(arg_ty) address.
End Typed_contract.
Definition Typed_contract_skeleton := Typed_contract.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 manager_operation.
Module Transaction.
Record record {transaction location parameters_ty parameters : Set} : Set := Build {
transaction : transaction;
location : location;
parameters_ty : parameters_ty;
parameters : parameters;
}.
Arguments record : clear implicits.
Definition with_transaction
{t_transaction t_location t_parameters_ty t_parameters} transaction
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters transaction
r.(location) r.(parameters_ty) r.(parameters).
Definition with_location
{t_transaction t_location t_parameters_ty t_parameters} location
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) location r.(parameters_ty) r.(parameters).
Definition with_parameters_ty
{t_transaction t_location t_parameters_ty t_parameters} parameters_ty
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) r.(location) parameters_ty r.(parameters).
Definition with_parameters
{t_transaction t_location t_parameters_ty t_parameters} parameters
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) r.(location) r.(parameters_ty) parameters.
End Transaction.
Definition Transaction_skeleton := Transaction.record.
Module Origination.
Record record {origination preorigination storage_type storage : Set} :
Set := Build {
origination : origination;
preorigination : preorigination;
storage_type : storage_type;
storage : storage;
}.
Arguments record : clear implicits.
Definition with_origination
{t_origination t_preorigination t_storage_type t_storage} origination
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
origination r.(preorigination) r.(storage_type) r.(storage).
Definition with_preorigination
{t_origination t_preorigination t_storage_type t_storage} preorigination
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) preorigination r.(storage_type) r.(storage).
Definition with_storage_type
{t_origination t_preorigination t_storage_type t_storage} storage_type
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) r.(preorigination) storage_type r.(storage).
Definition with_storage
{t_origination t_preorigination t_storage_type t_storage} storage
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) r.(preorigination) r.(storage_type) storage.
End Origination.
Definition Origination_skeleton := Origination.record.
End manager_operation.
End
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
Import
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
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 kinfo.
Record record {iloc kstack_ty : Set} : Set := Build {
iloc : iloc;
kstack_ty : kstack_ty;
}.
Arguments record : clear implicits.
Definition with_iloc {t_iloc t_kstack_ty} iloc
(r : record t_iloc t_kstack_ty) :=
Build t_iloc t_kstack_ty iloc r.(kstack_ty).
Definition with_kstack_ty {t_iloc t_kstack_ty} kstack_ty
(r : record t_iloc t_kstack_ty) :=
Build t_iloc t_kstack_ty r.(iloc) kstack_ty.
End kinfo.
Definition kinfo_skeleton := kinfo.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 log_entry log_control log_exit get_log : Set} : Set := Build {
log_interp : log_interp;
log_entry : log_entry;
log_control : log_control;
log_exit : log_exit;
get_log : get_log;
}.
Arguments record : clear implicits.
Definition with_log_interp
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_interp
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log log_interp
r.(log_entry) r.(log_control) r.(log_exit) r.(get_log).
Definition with_log_entry
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_entry
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) log_entry r.(log_control) r.(log_exit) r.(get_log).
Definition with_log_control
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_control
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) log_control r.(log_exit) r.(get_log).
Definition with_log_exit
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_exit
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) r.(log_control) log_exit r.(get_log).
Definition with_get_log
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} get_log
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) r.(log_control) r.(log_exit) get_log.
End logger.
Definition logger_skeleton := logger.record.
Reserved Notation "'script.Script".
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 "'typed_contract.Typed_contract".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'kinfo".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".
Inductive script : Set :=
| Script : ∀ {storage : Set}, 'script.Script storage → script
with kinstr : Set :=
| IDrop : 'kinfo → kinstr → kinstr
| IDup : 'kinfo → kinstr → kinstr
| ISwap : 'kinfo → kinstr → kinstr
| IConst : ∀ {ty : Set}, 'kinfo → ty → kinstr → kinstr
| ICons_pair : 'kinfo → kinstr → kinstr
| ICar : 'kinfo → kinstr → kinstr
| ICdr : 'kinfo → kinstr → kinstr
| IUnpair : 'kinfo → kinstr → kinstr
| ICons_some : 'kinfo → kinstr → kinstr
| ICons_none : 'kinfo → kinstr → kinstr
| IIf_none : 'kinstr.IIf_none → kinstr
| IOpt_map : 'kinstr.IOpt_map → kinstr
| ICons_left : 'kinfo → kinstr → kinstr
| ICons_right : 'kinfo → kinstr → kinstr
| IIf_left : 'kinstr.IIf_left → kinstr
| ICons_list : 'kinfo → kinstr → kinstr
| INil : 'kinfo → kinstr → kinstr
| IIf_cons : 'kinstr.IIf_cons → kinstr
| IList_map : 'kinfo → kinstr → kinstr → kinstr
| IList_iter : 'kinfo → kinstr → kinstr → kinstr
| IList_size : 'kinfo → kinstr → kinstr
| IEmpty_set : 'kinfo → 'comparable_ty → kinstr → kinstr
| ISet_iter : 'kinfo → kinstr → kinstr → kinstr
| ISet_mem : 'kinfo → kinstr → kinstr
| ISet_update : 'kinfo → kinstr → kinstr
| ISet_size : 'kinfo → kinstr → kinstr
| IEmpty_map : 'kinfo → 'comparable_ty → kinstr → kinstr
| IMap_map : 'kinfo → kinstr → kinstr → kinstr
| IMap_iter : 'kinfo → kinstr → kinstr → kinstr
| IMap_mem : 'kinfo → kinstr → kinstr
| IMap_get : 'kinfo → kinstr → kinstr
| IMap_update : 'kinfo → kinstr → kinstr
| IMap_get_and_update : 'kinfo → kinstr → kinstr
| IMap_size : 'kinfo → kinstr → kinstr
| IEmpty_big_map : 'kinfo → 'comparable_ty → ty → kinstr → kinstr
| IBig_map_mem : 'kinfo → kinstr → kinstr
| IBig_map_get : 'kinfo → kinstr → kinstr
| IBig_map_update : 'kinfo → kinstr → kinstr
| IBig_map_get_and_update : 'kinfo → kinstr → kinstr
| IConcat_string : 'kinfo → kinstr → kinstr
| IConcat_string_pair : 'kinfo → kinstr → kinstr
| ISlice_string : 'kinfo → kinstr → kinstr
| IString_size : 'kinfo → kinstr → kinstr
| IConcat_bytes : 'kinfo → kinstr → kinstr
| IConcat_bytes_pair : 'kinfo → kinstr → kinstr
| ISlice_bytes : 'kinfo → kinstr → kinstr
| IBytes_size : 'kinfo → kinstr → kinstr
| IAdd_seconds_to_timestamp : 'kinfo → kinstr → kinstr
| IAdd_timestamp_to_seconds : 'kinfo → kinstr → kinstr
| ISub_timestamp_seconds : 'kinfo → kinstr → kinstr
| IDiff_timestamps : 'kinfo → kinstr → kinstr
| IAdd_tez : 'kinfo → kinstr → kinstr
| ISub_tez : 'kinfo → kinstr → kinstr
| ISub_tez_legacy : 'kinfo → kinstr → kinstr
| IMul_teznat : 'kinfo → kinstr → kinstr
| IMul_nattez : 'kinfo → kinstr → kinstr
| IEdiv_teznat : 'kinfo → kinstr → kinstr
| IEdiv_tez : 'kinfo → kinstr → kinstr
| IOr : 'kinfo → kinstr → kinstr
| IAnd : 'kinfo → kinstr → kinstr
| IXor : 'kinfo → kinstr → kinstr
| INot : 'kinfo → kinstr → kinstr
| IIs_nat : 'kinfo → kinstr → kinstr
| INeg : 'kinfo → kinstr → kinstr
| IAbs_int : 'kinfo → kinstr → kinstr
| IInt_nat : 'kinfo → kinstr → kinstr
| IAdd_int : 'kinfo → kinstr → kinstr
| IAdd_nat : 'kinfo → kinstr → kinstr
| ISub_int : 'kinfo → kinstr → kinstr
| IMul_int : 'kinfo → kinstr → kinstr
| IMul_nat : 'kinfo → kinstr → kinstr
| IEdiv_int : 'kinfo → kinstr → kinstr
| IEdiv_nat : 'kinfo → kinstr → kinstr
| ILsl_nat : 'kinfo → kinstr → kinstr
| ILsr_nat : 'kinfo → kinstr → kinstr
| IOr_nat : 'kinfo → kinstr → kinstr
| IAnd_nat : 'kinfo → kinstr → kinstr
| IAnd_int_nat : 'kinfo → kinstr → kinstr
| IXor_nat : 'kinfo → kinstr → kinstr
| INot_int : 'kinfo → kinstr → kinstr
| IIf : 'kinstr.IIf → kinstr
| ILoop : 'kinfo → kinstr → kinstr → kinstr
| ILoop_left : 'kinfo → kinstr → kinstr → kinstr
| IDip : 'kinfo → kinstr → kinstr → kinstr
| IExec : 'kinfo → kinstr → kinstr
| IApply : 'kinfo → ty → kinstr → kinstr
| ILambda : 'kinfo → lambda → kinstr → kinstr
| IFailwith : 'kinfo → Alpha_context.Script.location → ty → kinstr
| ICompare : 'kinfo → 'comparable_ty → kinstr → kinstr
| IEq : 'kinfo → kinstr → kinstr
| INeq : 'kinfo → kinstr → kinstr
| ILt : 'kinfo → kinstr → kinstr
| IGt : 'kinfo → kinstr → kinstr
| ILe : 'kinfo → kinstr → kinstr
| IGe : 'kinfo → kinstr → kinstr
| IAddress : 'kinfo → kinstr → kinstr
| IContract : 'kinfo → ty → Alpha_context.Entrypoint.t → kinstr → kinstr
| IView : 'kinfo → view_signature → kinstr → kinstr
| ITransfer_tokens : 'kinfo → kinstr → kinstr
| IImplicit_account : 'kinfo → kinstr → kinstr
| ICreate_contract : 'kinstr.ICreate_contract → kinstr
| ISet_delegate : 'kinfo → kinstr → kinstr
| INow : 'kinfo → kinstr → kinstr
| IMin_block_time : 'kinfo → kinstr → kinstr
| IBalance : 'kinfo → kinstr → kinstr
| ILevel : 'kinfo → kinstr → kinstr
| ICheck_signature : 'kinfo → kinstr → kinstr
| IHash_key : 'kinfo → kinstr → kinstr
| IPack : 'kinfo → ty → kinstr → kinstr
| IUnpack : 'kinfo → ty → kinstr → kinstr
| IBlake2b : 'kinfo → kinstr → kinstr
| ISha256 : 'kinfo → kinstr → kinstr
| ISha512 : 'kinfo → kinstr → kinstr
| ISource : 'kinfo → kinstr → kinstr
| ISender : 'kinfo → kinstr → kinstr
| ISelf : 'kinfo → ty → Alpha_context.Entrypoint.t → kinstr → kinstr
| ISelf_address : 'kinfo → kinstr → kinstr
| IAmount : 'kinfo → kinstr → kinstr
| ISapling_empty_state :
'kinfo → Alpha_context.Sapling.Memo_size.t → kinstr → kinstr
| ISapling_verify_update : 'kinfo → kinstr → kinstr
| ISapling_verify_update_deprecated : 'kinfo → kinstr → kinstr
| IDig : 'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IDug : 'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IDipn :
'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr →
kinstr
| IDropn :
'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IChainId : 'kinfo → kinstr → kinstr
| INever : 'kinfo → kinstr
| IVoting_power : 'kinfo → kinstr → kinstr
| ITotal_voting_power : 'kinfo → kinstr → kinstr
| IKeccak : 'kinfo → kinstr → kinstr
| ISha3 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_g1 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_g2 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_g1 : 'kinfo → kinstr → kinstr
| IMul_bls12_381_g2 : 'kinfo → kinstr → kinstr
| IMul_bls12_381_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_z_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_fr_z : 'kinfo → kinstr → kinstr
| IInt_bls12_381_fr : 'kinfo → kinstr → kinstr
| INeg_bls12_381_g1 : 'kinfo → kinstr → kinstr
| INeg_bls12_381_g2 : 'kinfo → kinstr → kinstr
| INeg_bls12_381_fr : 'kinfo → kinstr → kinstr
| IPairing_check_bls12_381 : 'kinfo → kinstr → kinstr
| IComb : 'kinfo → int → comb_gadt_witness → kinstr → kinstr
| IUncomb : 'kinfo → int → uncomb_gadt_witness → kinstr → kinstr
| IComb_get : 'kinfo → int → comb_get_gadt_witness → kinstr → kinstr
| IComb_set : 'kinfo → int → comb_set_gadt_witness → kinstr → kinstr
| IDup_n : 'kinfo → int → dup_n_gadt_witness → kinstr → kinstr
| ITicket : 'kinfo → kinstr → kinstr
| IRead_ticket : 'kinfo → kinstr → kinstr
| ISplit_ticket : 'kinfo → kinstr → kinstr
| IJoin_tickets : 'kinfo → 'comparable_ty → kinstr → kinstr
| IOpen_chest : 'kinfo → kinstr → kinstr
| IHalt : 'kinfo → kinstr
| ILog : 'kinfo → logging_event → 'logger → kinstr → kinstr
with logging_event : Set :=
| LogEntry : logging_event
| LogExit : 'kinfo → logging_event
with lambda : Set :=
| Lam : 'kdescr → Alpha_context.Script.node → lambda
with typed_contract : Set :=
| Typed_contract : 'typed_contract.Typed_contract → typed_contract
with continuation : Set :=
| KNil : continuation
| KCons : kinstr → continuation → continuation
| KReturn : ∀ {s : Set}, s → continuation → continuation
| KMap_head : ∀ {a b : Set}, (a → b) → continuation → continuation
| KUndip : ∀ {b : Set}, b → continuation → continuation
| KLoop_in : kinstr → continuation → continuation
| KLoop_in_left : kinstr → continuation → continuation
| KIter : ∀ {a : Set}, kinstr → list a → continuation → continuation
| KList_enter_body : ∀ {a b : Set},
kinstr → list a → list b → int → continuation → continuation
| KList_exit_body : ∀ {a b : Set},
kinstr → list a → list b → int → continuation → continuation
| KMap_enter_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → continuation → continuation
| KMap_exit_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → a → continuation → continuation
| KView_exit : step_constants → continuation → continuation
| KLog : continuation → 'logger → continuation
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 :
'kinfo → 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 manager_operation : Set :=
| Transaction : ∀ {a : Set},
'manager_operation.Transaction a → manager_operation
| Origination : ∀ {storage : Set},
'manager_operation.Origination storage → manager_operation
| Delegation : option Signature.public_key_hash → manager_operation
with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation → packed_internal_operation
where "'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.t ×
list Alpha_context.Script.expr))
and "'comparable_ty" := ((fun _ ⇒ ty) tt)
and "'kdescr" :=
(kdescr_skeleton Alpha_context.Script.location stack_ty stack_ty kinstr)
and "'kinfo" := (kinfo_skeleton Alpha_context.Script.location stack_ty)
and "'internal_operation" :=
(internal_operation_skeleton Alpha_context.Contract.contract manager_operation
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)
(∀ {a s : Set}, 'logging_function a s) (continuation → unit)
(∀ {c u : Set}, 'logging_function c u)
(unit → M? (option 'execution_trace)))
and "'script.Script" :=
(fun (t_storage : Set) ⇒ script.Script_skeleton lambda ty t_storage ty
view_map entrypoints Cache_memory_helpers.sint)
and "'kinstr.IIf_none" := (kinstr.IIf_none_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IOpt_map" := (kinstr.IOpt_map_skeleton 'kinfo kinstr kinstr)
and "'kinstr.IIf_left" := (kinstr.IIf_left_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf_cons" := (kinstr.IIf_cons_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf" := (kinstr.IIf_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
(kinstr.ICreate_contract_skeleton 'kinfo ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_contract" :=
(typed_contract.Typed_contract_skeleton ty address)
and "'big_map.Big_map" :=
(fun (t_key t_value : Set) ⇒ big_map.Big_map_skeleton
(option Alpha_context.Big_map.Id.t) (big_map_overlay t_key t_value)
'comparable_ty ty)
and "'view_signature.View_signature" :=
(view_signature.View_signature_skeleton Alpha_context.Script_string.t ty ty)
and "'manager_operation.Transaction" :=
(fun (t_a : Set) ⇒ manager_operation.Transaction_skeleton
Alpha_context.transaction Alpha_context.Script.location ty t_a)
and "'manager_operation.Origination" :=
(fun (t_storage : Set) ⇒ manager_operation.Origination_skeleton
Alpha_context.origination Alpha_context.Contract.t ty t_storage).
Module script.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.script.
Definition Script := 'script.Script.
End script.
Module kinstr.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.kinstr.
Definition IIf_none := 'kinstr.IIf_none.
Definition IOpt_map := 'kinstr.IOpt_map.
Definition IIf_left := 'kinstr.IIf_left.
Definition IIf_cons := 'kinstr.IIf_cons.
Definition IIf := 'kinstr.IIf.
Definition ICreate_contract := 'kinstr.ICreate_contract.
End kinstr.
Module typed_contract.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.typed_contract.
Definition Typed_contract := 'typed_contract.Typed_contract.
End typed_contract.
Module big_map.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.big_map.
Definition Big_map := 'big_map.Big_map.
End big_map.
Module view_signature.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.view_signature.
Definition View_signature := 'view_signature.View_signature.
End view_signature.
Module manager_operation.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.manager_operation.
Definition Transaction := 'manager_operation.Transaction.
Definition Origination := 'manager_operation.Origination.
End manager_operation.
Definition logging_function := 'logging_function.
Definition execution_trace := 'execution_trace.
Definition logger := 'logger.
Definition comparable_ty := 'comparable_ty.
Definition kdescr := 'kdescr.
Definition kinfo := 'kinfo.
Definition internal_operation := 'internal_operation.
Definition operation := 'operation.
Inductive packed_manager_operation : Set :=
| Manager : manager_operation → packed_manager_operation.
Definition manager_kind (function_parameter : manager_operation)
: Alpha_context.Kind.manager :=
match function_parameter with
| Transaction _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Origination _ ⇒ Alpha_context.Kind.Origination_manager_kind
| Delegation _ ⇒ Alpha_context.Kind.Delegation_manager_kind
end.
Definition kinfo_of_kinstr (i_value : kinstr) : kinfo :=
match i_value with
| IDrop kinfo_value _ ⇒ kinfo_value
| IDup kinfo_value _ ⇒ kinfo_value
| ISwap kinfo_value _ ⇒ kinfo_value
| IConst kinfo_value _ _ ⇒ kinfo_value
| ICons_pair kinfo_value _ ⇒ kinfo_value
| ICar kinfo_value _ ⇒ kinfo_value
| ICdr kinfo_value _ ⇒ kinfo_value
| IUnpair kinfo_value _ ⇒ kinfo_value
| ICons_some kinfo_value _ ⇒ kinfo_value
| ICons_none kinfo_value _ ⇒ kinfo_value
| IIf_none {| kinstr.IIf_none.kinfo := kinfo_value |} ⇒ kinfo_value
| IOpt_map {| kinstr.IOpt_map.kinfo := kinfo_value |} ⇒ kinfo_value
| ICons_left kinfo_value _ ⇒ kinfo_value
| ICons_right kinfo_value _ ⇒ kinfo_value
| IIf_left {| kinstr.IIf_left.kinfo := kinfo_value |} ⇒ kinfo_value
| ICons_list kinfo_value _ ⇒ kinfo_value
| INil kinfo_value _ ⇒ kinfo_value
| IIf_cons {| kinstr.IIf_cons.kinfo := kinfo_value |} ⇒ kinfo_value
| IList_map kinfo_value _ _ ⇒ kinfo_value
| IList_iter kinfo_value _ _ ⇒ kinfo_value
| IList_size kinfo_value _ ⇒ kinfo_value
| IEmpty_set kinfo_value _ _ ⇒ kinfo_value
| ISet_iter kinfo_value _ _ ⇒ kinfo_value
| ISet_mem kinfo_value _ ⇒ kinfo_value
| ISet_update kinfo_value _ ⇒ kinfo_value
| ISet_size kinfo_value _ ⇒ kinfo_value
| IEmpty_map kinfo_value _ _ ⇒ kinfo_value
| IMap_map kinfo_value _ _ ⇒ kinfo_value
| IMap_iter kinfo_value _ _ ⇒ kinfo_value
| IMap_mem kinfo_value _ ⇒ kinfo_value
| IMap_get kinfo_value _ ⇒ kinfo_value
| IMap_update kinfo_value _ ⇒ kinfo_value
| IMap_get_and_update kinfo_value _ ⇒ kinfo_value
| IMap_size kinfo_value _ ⇒ kinfo_value
| IEmpty_big_map kinfo_value _ _ _ ⇒ kinfo_value
| IBig_map_mem kinfo_value _ ⇒ kinfo_value
| IBig_map_get kinfo_value _ ⇒ kinfo_value
| IBig_map_update kinfo_value _ ⇒ kinfo_value
| IBig_map_get_and_update kinfo_value _ ⇒ kinfo_value
| IConcat_string kinfo_value _ ⇒ kinfo_value
| IConcat_string_pair kinfo_value _ ⇒ kinfo_value
| ISlice_string kinfo_value _ ⇒ kinfo_value
| IString_size kinfo_value _ ⇒ kinfo_value
| IConcat_bytes kinfo_value _ ⇒ kinfo_value
| IConcat_bytes_pair kinfo_value _ ⇒ kinfo_value
| ISlice_bytes kinfo_value _ ⇒ kinfo_value
| IBytes_size kinfo_value _ ⇒ kinfo_value
| IAdd_seconds_to_timestamp kinfo_value _ ⇒ kinfo_value
| IAdd_timestamp_to_seconds kinfo_value _ ⇒ kinfo_value
| ISub_timestamp_seconds kinfo_value _ ⇒ kinfo_value
| IDiff_timestamps kinfo_value _ ⇒ kinfo_value
| IAdd_tez kinfo_value _ ⇒ kinfo_value
| ISub_tez kinfo_value _ ⇒ kinfo_value
| ISub_tez_legacy kinfo_value _ ⇒ kinfo_value
| IMul_teznat kinfo_value _ ⇒ kinfo_value
| IMul_nattez kinfo_value _ ⇒ kinfo_value
| IEdiv_teznat kinfo_value _ ⇒ kinfo_value
| IEdiv_tez kinfo_value _ ⇒ kinfo_value
| IOr kinfo_value _ ⇒ kinfo_value
| IAnd kinfo_value _ ⇒ kinfo_value
| IXor kinfo_value _ ⇒ kinfo_value
| INot kinfo_value _ ⇒ kinfo_value
| IIs_nat kinfo_value _ ⇒ kinfo_value
| INeg kinfo_value _ ⇒ kinfo_value
| IAbs_int kinfo_value _ ⇒ kinfo_value
| IInt_nat kinfo_value _ ⇒ kinfo_value
| IAdd_int kinfo_value _ ⇒ kinfo_value
| IAdd_nat kinfo_value _ ⇒ kinfo_value
| ISub_int kinfo_value _ ⇒ kinfo_value
| IMul_int kinfo_value _ ⇒ kinfo_value
| IMul_nat kinfo_value _ ⇒ kinfo_value
| IEdiv_int kinfo_value _ ⇒ kinfo_value
| IEdiv_nat kinfo_value _ ⇒ kinfo_value
| ILsl_nat kinfo_value _ ⇒ kinfo_value
| ILsr_nat kinfo_value _ ⇒ kinfo_value
| IOr_nat kinfo_value _ ⇒ kinfo_value
| IAnd_nat kinfo_value _ ⇒ kinfo_value
| IAnd_int_nat kinfo_value _ ⇒ kinfo_value
| IXor_nat kinfo_value _ ⇒ kinfo_value
| INot_int kinfo_value _ ⇒ kinfo_value
| IIf {| kinstr.IIf.kinfo := kinfo_value |} ⇒ kinfo_value
| ILoop kinfo_value _ _ ⇒ kinfo_value
| ILoop_left kinfo_value _ _ ⇒ kinfo_value
| IDip kinfo_value _ _ ⇒ kinfo_value
| IExec kinfo_value _ ⇒ kinfo_value
| IApply kinfo_value _ _ ⇒ kinfo_value
| ILambda kinfo_value _ _ ⇒ kinfo_value
| IFailwith kinfo_value _ _ ⇒ kinfo_value
| ICompare kinfo_value _ _ ⇒ kinfo_value
| IEq kinfo_value _ ⇒ kinfo_value
| INeq kinfo_value _ ⇒ kinfo_value
| ILt kinfo_value _ ⇒ kinfo_value
| IGt kinfo_value _ ⇒ kinfo_value
| ILe kinfo_value _ ⇒ kinfo_value
| IGe kinfo_value _ ⇒ kinfo_value
| IAddress kinfo_value _ ⇒ kinfo_value
| IContract kinfo_value _ _ _ ⇒ kinfo_value
| ITransfer_tokens kinfo_value _ ⇒ kinfo_value
| IView kinfo_value _ _ ⇒ kinfo_value
| IImplicit_account kinfo_value _ ⇒ kinfo_value
| ICreate_contract {| kinstr.ICreate_contract.kinfo := kinfo_value |} ⇒
kinfo_value
| ISet_delegate kinfo_value _ ⇒ kinfo_value
| INow kinfo_value _ ⇒ kinfo_value
| IMin_block_time kinfo_value _ ⇒ kinfo_value
| IBalance kinfo_value _ ⇒ kinfo_value
| ILevel kinfo_value _ ⇒ kinfo_value
| ICheck_signature kinfo_value _ ⇒ kinfo_value
| IHash_key kinfo_value _ ⇒ kinfo_value
| IPack kinfo_value _ _ ⇒ kinfo_value
| IUnpack kinfo_value _ _ ⇒ kinfo_value
| IBlake2b kinfo_value _ ⇒ kinfo_value
| ISha256 kinfo_value _ ⇒ kinfo_value
| ISha512 kinfo_value _ ⇒ kinfo_value
| ISource kinfo_value _ ⇒ kinfo_value
| ISender kinfo_value _ ⇒ kinfo_value
| ISelf kinfo_value _ _ _ ⇒ kinfo_value
| ISelf_address kinfo_value _ ⇒ kinfo_value
| IAmount kinfo_value _ ⇒ kinfo_value
| ISapling_empty_state kinfo_value _ _ ⇒ kinfo_value
| ISapling_verify_update kinfo_value _ ⇒ kinfo_value
| ISapling_verify_update_deprecated kinfo_value _ ⇒ kinfo_value
| IDig kinfo_value _ _ _ ⇒ kinfo_value
| IDug kinfo_value _ _ _ ⇒ kinfo_value
| IDipn kinfo_value _ _ _ _ ⇒ kinfo_value
| IDropn kinfo_value _ _ _ ⇒ kinfo_value
| IChainId kinfo_value _ ⇒ kinfo_value
| INever kinfo_value ⇒ kinfo_value
| IVoting_power kinfo_value _ ⇒ kinfo_value
| ITotal_voting_power kinfo_value _ ⇒ kinfo_value
| IKeccak kinfo_value _ ⇒ kinfo_value
| ISha3 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_z_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_fr_z kinfo_value _ ⇒ kinfo_value
| IInt_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IPairing_check_bls12_381 kinfo_value _ ⇒ kinfo_value
| IComb kinfo_value _ _ _ ⇒ kinfo_value
| IUncomb kinfo_value _ _ _ ⇒ kinfo_value
| IComb_get kinfo_value _ _ _ ⇒ kinfo_value
| IComb_set kinfo_value _ _ _ ⇒ kinfo_value
| IDup_n kinfo_value _ _ _ ⇒ kinfo_value
| ITicket kinfo_value _ ⇒ kinfo_value
| IRead_ticket kinfo_value _ ⇒ kinfo_value
| ISplit_ticket kinfo_value _ ⇒ kinfo_value
| IJoin_tickets kinfo_value _ _ ⇒ kinfo_value
| IHalt kinfo_value ⇒ kinfo_value
| ILog kinfo_value _ _ _ ⇒ kinfo_value
| IOpen_chest kinfo_value _ ⇒ kinfo_value
end.
Module kinstr_rewritek.
Record record : Set := Build {
apply : kinstr → kinstr;
}.
Definition with_apply apply (r : record) :=
Build apply.
End kinstr_rewritek.
Definition kinstr_rewritek := kinstr_rewritek.record.
Definition kinstr_rewritek_value (i_value : kinstr) (f_value : kinstr_rewritek)
: kinstr :=
match i_value with
| IDrop kinfo_value k_value ⇒
IDrop kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IDup kinfo_value k_value ⇒
IDup kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISwap kinfo_value k_value ⇒
ISwap kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConst kinfo_value x_value k_value ⇒
IConst kinfo_value x_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_pair kinfo_value k_value ⇒
ICons_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICar kinfo_value k_value ⇒
ICar kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICdr kinfo_value k_value ⇒
ICdr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IUnpair kinfo_value k_value ⇒
IUnpair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_some kinfo_value k_value ⇒
ICons_some kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_none kinfo_value k_value ⇒
ICons_none kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_none {|
kinstr.IIf_none.kinfo := kinfo_value;
kinstr.IIf_none.branch_if_none := branch_if_none;
kinstr.IIf_none.branch_if_some := branch_if_some;
kinstr.IIf_none.k := k_value
|} ⇒
IIf_none
{| kinstr.IIf_none.kinfo := kinfo_value;
kinstr.IIf_none.branch_if_none :=
f_value.(kinstr_rewritek.apply) branch_if_none;
kinstr.IIf_none.branch_if_some :=
f_value.(kinstr_rewritek.apply) branch_if_some;
kinstr.IIf_none.k := f_value.(kinstr_rewritek.apply) k_value; |}
|
IOpt_map {|
kinstr.IOpt_map.kinfo := kinfo_value;
kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value
|} ⇒
let body := f_value.(kinstr_rewritek.apply) body in
let k_value := f_value.(kinstr_rewritek.apply) k_value in
IOpt_map
{| kinstr.IOpt_map.kinfo := kinfo_value; kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value; |}
| ICons_left kinfo_value k_value ⇒
ICons_left kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_right kinfo_value k_value ⇒
ICons_right kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_left {|
kinstr.IIf_left.kinfo := kinfo_value;
kinstr.IIf_left.branch_if_left := branch_if_left;
kinstr.IIf_left.branch_if_right := branch_if_right;
kinstr.IIf_left.k := k_value
|} ⇒
IIf_left
{| kinstr.IIf_left.kinfo := kinfo_value;
kinstr.IIf_left.branch_if_left :=
f_value.(kinstr_rewritek.apply) branch_if_left;
kinstr.IIf_left.branch_if_right :=
f_value.(kinstr_rewritek.apply) branch_if_right;
kinstr.IIf_left.k := f_value.(kinstr_rewritek.apply) k_value; |}
| ICons_list kinfo_value k_value ⇒
ICons_list kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INil kinfo_value k_value ⇒
INil kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_cons {|
kinstr.IIf_cons.kinfo := kinfo_value;
kinstr.IIf_cons.branch_if_cons := branch_if_cons;
kinstr.IIf_cons.branch_if_nil := branch_if_nil;
kinstr.IIf_cons.k := k_value
|} ⇒
IIf_cons
{| kinstr.IIf_cons.kinfo := kinfo_value;
kinstr.IIf_cons.branch_if_cons :=
f_value.(kinstr_rewritek.apply) branch_if_cons;
kinstr.IIf_cons.branch_if_nil :=
f_value.(kinstr_rewritek.apply) branch_if_nil;
kinstr.IIf_cons.k := f_value.(kinstr_rewritek.apply) k_value; |}
| IList_map kinfo_value body k_value ⇒
IList_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IList_iter kinfo_value body k_value ⇒
IList_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IList_size kinfo_value k_value ⇒
IList_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_set kinfo_value ty k_value ⇒
IEmpty_set kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| ISet_iter kinfo_value body k_value ⇒
ISet_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| ISet_mem kinfo_value k_value ⇒
ISet_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISet_update kinfo_value k_value ⇒
ISet_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISet_size kinfo_value k_value ⇒
ISet_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_map kinfo_value cty k_value ⇒
IEmpty_map kinfo_value cty (f_value.(kinstr_rewritek.apply) k_value)
| IMap_map kinfo_value body k_value ⇒
IMap_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IMap_iter kinfo_value body k_value ⇒
IMap_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IMap_mem kinfo_value k_value ⇒
IMap_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_get kinfo_value k_value ⇒
IMap_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_update kinfo_value k_value ⇒
IMap_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_get_and_update kinfo_value k_value ⇒
IMap_get_and_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_size kinfo_value k_value ⇒
IMap_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_big_map kinfo_value cty ty k_value ⇒
IEmpty_big_map kinfo_value cty ty (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_mem kinfo_value k_value ⇒
IBig_map_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_get kinfo_value k_value ⇒
IBig_map_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_update kinfo_value k_value ⇒
IBig_map_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_get_and_update kinfo_value k_value ⇒
IBig_map_get_and_update kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IConcat_string kinfo_value k_value ⇒
IConcat_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_string_pair kinfo_value k_value ⇒
IConcat_string_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISlice_string kinfo_value k_value ⇒
ISlice_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IString_size kinfo_value k_value ⇒
IString_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_bytes kinfo_value k_value ⇒
IConcat_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_bytes_pair kinfo_value k_value ⇒
IConcat_bytes_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISlice_bytes kinfo_value k_value ⇒
ISlice_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBytes_size kinfo_value k_value ⇒
IBytes_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_seconds_to_timestamp kinfo_value k_value ⇒
IAdd_seconds_to_timestamp kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IAdd_timestamp_to_seconds kinfo_value k_value ⇒
IAdd_timestamp_to_seconds kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| ISub_timestamp_seconds kinfo_value k_value ⇒
ISub_timestamp_seconds kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IDiff_timestamps kinfo_value k_value ⇒
IDiff_timestamps kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_tez kinfo_value k_value ⇒
IAdd_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_tez kinfo_value k_value ⇒
ISub_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_tez_legacy kinfo_value k_value ⇒
ISub_tez_legacy kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_teznat kinfo_value k_value ⇒
IMul_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_nattez kinfo_value k_value ⇒
IMul_nattez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_teznat kinfo_value k_value ⇒
IEdiv_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_tez kinfo_value k_value ⇒
IEdiv_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IOr kinfo_value k_value ⇒
IOr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd kinfo_value k_value ⇒
IAnd kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IXor kinfo_value k_value ⇒
IXor kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INot kinfo_value k_value ⇒
INot kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IIs_nat kinfo_value k_value ⇒
IIs_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg kinfo_value k_value ⇒
INeg kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAbs_int kinfo_value k_value ⇒
IAbs_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IInt_nat kinfo_value k_value ⇒
IInt_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_int kinfo_value k_value ⇒
IAdd_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_nat kinfo_value k_value ⇒
IAdd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_int kinfo_value k_value ⇒
ISub_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_int kinfo_value k_value ⇒
IMul_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_nat kinfo_value k_value ⇒
IMul_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_int kinfo_value k_value ⇒
IEdiv_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_nat kinfo_value k_value ⇒
IEdiv_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILsl_nat kinfo_value k_value ⇒
ILsl_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILsr_nat kinfo_value k_value ⇒
ILsr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IOr_nat kinfo_value k_value ⇒
IOr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd_nat kinfo_value k_value ⇒
IAnd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd_int_nat kinfo_value k_value ⇒
IAnd_int_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IXor_nat kinfo_value k_value ⇒
IXor_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INot_int kinfo_value k_value ⇒
INot_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf {|
kinstr.IIf.kinfo := kinfo_value;
kinstr.IIf.branch_if_true := branch_if_true;
kinstr.IIf.branch_if_false := branch_if_false;
kinstr.IIf.k := k_value
|} ⇒
IIf
{| kinstr.IIf.kinfo := kinfo_value;
kinstr.IIf.branch_if_true :=
f_value.(kinstr_rewritek.apply) branch_if_true;
kinstr.IIf.branch_if_false :=
f_value.(kinstr_rewritek.apply) branch_if_false;
kinstr.IIf.k := f_value.(kinstr_rewritek.apply) k_value; |}
| ILoop kinfo_value kbody k_value ⇒
ILoop kinfo_value (f_value.(kinstr_rewritek.apply) kbody)
(f_value.(kinstr_rewritek.apply) k_value)
| ILoop_left kinfo_value kl kr ⇒
ILoop_left kinfo_value (f_value.(kinstr_rewritek.apply) kl)
(f_value.(kinstr_rewritek.apply) kr)
| IDip kinfo_value body k_value ⇒
IDip kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IExec kinfo_value k_value ⇒
IExec kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IApply kinfo_value ty k_value ⇒
IApply kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| ILambda kinfo_value l_value k_value ⇒
ILambda kinfo_value l_value (f_value.(kinstr_rewritek.apply) k_value)
| IFailwith kinfo_value i_value ty ⇒ IFailwith kinfo_value i_value ty
| ICompare kinfo_value ty k_value ⇒
ICompare kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IEq kinfo_value k_value ⇒
IEq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeq kinfo_value k_value ⇒
INeq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILt kinfo_value k_value ⇒
ILt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IGt kinfo_value k_value ⇒
IGt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILe kinfo_value k_value ⇒
ILe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IGe kinfo_value k_value ⇒
IGe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAddress kinfo_value k_value ⇒
IAddress kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IContract kinfo_value ty code k_value ⇒
IContract kinfo_value ty code (f_value.(kinstr_rewritek.apply) k_value)
| ITransfer_tokens kinfo_value k_value ⇒
ITransfer_tokens kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IView kinfo_value view_signature k_value ⇒
IView kinfo_value view_signature (f_value.(kinstr_rewritek.apply) k_value)
| IImplicit_account kinfo_value k_value ⇒
IImplicit_account kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
ICreate_contract {|
kinstr.ICreate_contract.kinfo := kinfo_value;
kinstr.ICreate_contract.storage_type := storage_type;
kinstr.ICreate_contract.code := code;
kinstr.ICreate_contract.k := k_value
|} ⇒
let k_value := f_value.(kinstr_rewritek.apply) k_value in
ICreate_contract
{| kinstr.ICreate_contract.kinfo := kinfo_value;
kinstr.ICreate_contract.storage_type := storage_type;
kinstr.ICreate_contract.code := code;
kinstr.ICreate_contract.k := k_value; |}
| ISet_delegate kinfo_value k_value ⇒
ISet_delegate kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INow kinfo_value k_value ⇒
INow kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMin_block_time kinfo_value k_value ⇒
IMin_block_time kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBalance kinfo_value k_value ⇒
IBalance kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILevel kinfo_value k_value ⇒
ILevel kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICheck_signature kinfo_value k_value ⇒
ICheck_signature kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IHash_key kinfo_value k_value ⇒
IHash_key kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IPack kinfo_value ty k_value ⇒
IPack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IUnpack kinfo_value ty k_value ⇒
IUnpack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IBlake2b kinfo_value k_value ⇒
IBlake2b kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha256 kinfo_value k_value ⇒
ISha256 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha512 kinfo_value k_value ⇒
ISha512 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISource kinfo_value k_value ⇒
ISource kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISender kinfo_value k_value ⇒
ISender kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISelf kinfo_value ty s_value k_value ⇒
ISelf kinfo_value ty s_value (f_value.(kinstr_rewritek.apply) k_value)
| ISelf_address kinfo_value k_value ⇒
ISelf_address kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAmount kinfo_value k_value ⇒
IAmount kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISapling_empty_state kinfo_value s_value k_value ⇒
ISapling_empty_state kinfo_value s_value
(f_value.(kinstr_rewritek.apply) k_value)
| ISapling_verify_update kinfo_value k_value ⇒
ISapling_verify_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISapling_verify_update_deprecated kinfo_value k_value ⇒
ISapling_verify_update_deprecated kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IDig kinfo_value n_value p_value k_value ⇒
IDig kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IDug kinfo_value n_value p_value k_value ⇒
IDug kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IDipn kinfo_value n_value p_value k1 k2 ⇒
IDipn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k1)
(f_value.(kinstr_rewritek.apply) k2)
| IDropn kinfo_value n_value p_value k_value ⇒
IDropn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IChainId kinfo_value k_value ⇒
IChainId kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INever kinfo_value ⇒ INever kinfo_value
| IVoting_power kinfo_value k_value ⇒
IVoting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ITotal_voting_power kinfo_value k_value ⇒
ITotal_voting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IKeccak kinfo_value k_value ⇒
IKeccak kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha3 kinfo_value k_value ⇒
ISha3 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_g1 kinfo_value k_value ⇒
IAdd_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_g2 kinfo_value k_value ⇒
IAdd_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_fr kinfo_value k_value ⇒
IAdd_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_g1 kinfo_value k_value ⇒
IMul_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_g2 kinfo_value k_value ⇒
IMul_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_fr kinfo_value k_value ⇒
IMul_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_z_fr kinfo_value k_value ⇒
IMul_bls12_381_z_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_fr_z kinfo_value k_value ⇒
IMul_bls12_381_fr_z kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IInt_bls12_381_fr kinfo_value k_value ⇒
IInt_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_g1 kinfo_value k_value ⇒
INeg_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_g2 kinfo_value k_value ⇒
INeg_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_fr kinfo_value k_value ⇒
INeg_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IPairing_check_bls12_381 kinfo_value k_value ⇒
IPairing_check_bls12_381 kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb kinfo_value n_value p_value k_value ⇒
IComb kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IUncomb kinfo_value n_value p_value k_value ⇒
IUncomb kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb_get kinfo_value n_value p_value k_value ⇒
IComb_get kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb_set kinfo_value n_value p_value k_value ⇒
IComb_set kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IDup_n kinfo_value n_value p_value k_value ⇒
IDup_n kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| ITicket kinfo_value k_value ⇒
ITicket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IRead_ticket kinfo_value k_value ⇒
IRead_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISplit_ticket kinfo_value k_value ⇒
ISplit_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IJoin_tickets kinfo_value ty k_value ⇒
IJoin_tickets kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IHalt kinfo_value ⇒ IHalt kinfo_value
| ILog kinfo_value event logger k_value ⇒
ILog kinfo_value event logger k_value
| IOpen_chest kinfo_value k_value ⇒
IOpen_chest kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
end.
Definition meta_basic : ty_metadata :=
{| ty_metadata.size := Type_size.(TYPE_SIZE.one); |}.
Definition ty_metadata_value (function_parameter : ty) : ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta _ ⇒ meta
| Union_t _ _ meta _ ⇒ meta
| Option_t _ meta _ ⇒ meta
| Lambda_t _ _ meta ⇒ meta
| List_t _ meta ⇒ meta
| Set_t _ meta ⇒ meta
| Map_t _ _ meta ⇒ meta
| Big_map_t _ _ meta ⇒ meta
| Ticket_t _ meta ⇒ meta
| Contract_t _ meta ⇒ meta
|
(Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Bls12_381_g1_t | Bls12_381_g2_t |
Bls12_381_fr_t | Chest_t | Chest_key_t) ⇒ meta_basic
end.
Definition comparable_ty_metadata (function_parameter : comparable_ty)
: ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta Dependent_bool.YesYes ⇒ meta
| Union_t _ _ meta Dependent_bool.YesYes ⇒ meta
| Option_t _ meta Dependent_bool.Yes ⇒ meta
| _ ⇒ unreachable_gadt_branch
end.
Definition ty_size (t_value : ty) : Type_size.(TYPE_SIZE.t) :=
(ty_metadata_value t_value).(ty_metadata.size).
Definition comparable_ty_size (t_value : comparable_ty)
: Type_size.(TYPE_SIZE.t) :=
(comparable_ty_metadata t_value).(ty_metadata.size).
Definition is_comparable (function_parameter : ty) : Dependent_bool.dbool :=
match function_parameter with
| Never_t ⇒ Dependent_bool.Yes
| Unit_t ⇒ Dependent_bool.Yes
| Int_t ⇒ Dependent_bool.Yes
| Nat_t ⇒ Dependent_bool.Yes
| Signature_t ⇒ Dependent_bool.Yes
| String_t ⇒ Dependent_bool.Yes
| Bytes_t ⇒ Dependent_bool.Yes
| Mutez_t ⇒ Dependent_bool.Yes
| Bool_t ⇒ Dependent_bool.Yes
| Key_hash_t ⇒ Dependent_bool.Yes
| Key_t ⇒ Dependent_bool.Yes
| Timestamp_t ⇒ Dependent_bool.Yes
| Chain_id_t ⇒ Dependent_bool.Yes
| Address_t ⇒ Dependent_bool.Yes
| Tx_rollup_l2_address_t ⇒ Dependent_bool.Yes
| Pair_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Union_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Option_t _ _ cmp ⇒ cmp
| Lambda_t _ _ _ ⇒ Dependent_bool.No
| List_t _ _ ⇒ Dependent_bool.No
| Set_t _ _ ⇒ Dependent_bool.No
| Map_t _ _ _ ⇒ Dependent_bool.No
| Big_map_t _ _ _ ⇒ Dependent_bool.No
| Ticket_t _ _ ⇒ Dependent_bool.No
| Contract_t _ _ ⇒ Dependent_bool.No
| Sapling_transaction_t _ ⇒ Dependent_bool.No
| Sapling_transaction_deprecated_t _ ⇒ Dependent_bool.No
| Sapling_state_t _ ⇒ Dependent_bool.No
| Operation_t ⇒ Dependent_bool.No
| Bls12_381_g1_t ⇒ Dependent_bool.No
| Bls12_381_g2_t ⇒ Dependent_bool.No
| Bls12_381_fr_t ⇒ Dependent_bool.No
| Chest_t ⇒ Dependent_bool.No
| Chest_key_t ⇒ Dependent_bool.No
end.
Inductive ty_ex_c : Set :=
| Ty_ex_c : ty → ty_ex_c.
Definition unit_t : ty := Unit_t.
Definition unit_key : ty := unit_t.
Definition int_t : ty := Int_t.
Definition int_key : ty := int_t.
Definition nat_t : ty := Nat_t.
Definition nat_key : ty := nat_t.
Definition signature_t : ty := Signature_t.
Definition signature_key : ty := signature_t.
Definition string_t : ty := String_t.
Definition string_key : ty := string_t.
Definition bytes_t : ty := Bytes_t.
Definition bytes_key : ty := bytes_t.
Definition mutez_t : ty := Mutez_t.
Definition mutez_key : ty := mutez_t.
Definition key_hash_t : ty := Key_hash_t.
Definition key_hash_key : ty := key_hash_t.
Definition key_t : ty := Key_t.
Definition key_key : ty := key_t.
Definition timestamp_t : ty := Timestamp_t.
Definition timestamp_key : ty := timestamp_t.
Definition address_t : ty := Address_t.
Definition address_key : ty := address_t.
Definition bool_t : ty := Bool_t.
Definition bool_key : ty := bool_t.
Definition tx_rollup_l2_address_t : ty := Tx_rollup_l2_address_t.
Definition tx_rollup_l2_address_key : ty := tx_rollup_l2_address_t.
Definition pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Pair_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition comparable_pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Pair_t l_value
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
Module script.
Module Script.
Record record {code arg_type storage storage_type views entrypoints
code_size : Set} : Set := Build {
code : code;
arg_type : arg_type;
storage : storage;
storage_type : storage_type;
views : views;
entrypoints : entrypoints;
code_size : code_size;
}.
Arguments record : clear implicits.
Definition with_code
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size code r.(arg_type) r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_arg_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} arg_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) arg_type r.(storage) r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) storage r.(storage_type) r.(views)
r.(entrypoints) r.(code_size).
Definition with_storage_type
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} storage_type
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) storage_type r.(views)
r.(entrypoints) r.(code_size).
Definition with_views
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} views
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type) views
r.(entrypoints) r.(code_size).
Definition with_entrypoints
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} entrypoints
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) entrypoints r.(code_size).
Definition with_code_size
{t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size} code_size
(r :
record t_code t_arg_type t_storage t_storage_type t_views
t_entrypoints t_code_size) :=
Build t_code t_arg_type t_storage t_storage_type t_views t_entrypoints
t_code_size r.(code) r.(arg_type) r.(storage) r.(storage_type)
r.(views) r.(entrypoints) code_size.
End Script.
Definition Script_skeleton := Script.record.
End script.
Module kinstr.
Module IIf_none.
Record record {kinfo branch_if_none branch_if_some k : Set} : Set := Build {
kinfo : kinfo;
branch_if_none : branch_if_none;
branch_if_some : branch_if_some;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_none t_branch_if_some t_k}
kinfo (r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k kinfo
r.(branch_if_none) r.(branch_if_some) r.(k).
Definition with_branch_if_none
{t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_none
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
branch_if_none r.(branch_if_some) r.(k).
Definition with_branch_if_some
{t_kinfo t_branch_if_none t_branch_if_some t_k} branch_if_some
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
r.(branch_if_none) branch_if_some r.(k).
Definition with_k {t_kinfo t_branch_if_none t_branch_if_some t_k} k
(r : record t_kinfo t_branch_if_none t_branch_if_some t_k) :=
Build t_kinfo t_branch_if_none t_branch_if_some t_k r.(kinfo)
r.(branch_if_none) r.(branch_if_some) k.
End IIf_none.
Definition IIf_none_skeleton := IIf_none.record.
Module IOpt_map.
Record record {kinfo body k : Set} : Set := Build {
kinfo : kinfo;
body : body;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_body t_k} kinfo
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k kinfo r.(body) r.(k).
Definition with_body {t_kinfo t_body t_k} body
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k r.(kinfo) body r.(k).
Definition with_k {t_kinfo t_body t_k} k
(r : record t_kinfo t_body t_k) :=
Build t_kinfo t_body t_k r.(kinfo) r.(body) k.
End IOpt_map.
Definition IOpt_map_skeleton := IOpt_map.record.
Module IIf_left.
Record record {kinfo branch_if_left branch_if_right k : Set} : Set := Build {
kinfo : kinfo;
branch_if_left : branch_if_left;
branch_if_right : branch_if_right;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_left t_branch_if_right t_k}
kinfo (r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k kinfo
r.(branch_if_left) r.(branch_if_right) r.(k).
Definition with_branch_if_left
{t_kinfo t_branch_if_left t_branch_if_right t_k} branch_if_left
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
branch_if_left r.(branch_if_right) r.(k).
Definition with_branch_if_right
{t_kinfo t_branch_if_left t_branch_if_right t_k} branch_if_right
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
r.(branch_if_left) branch_if_right r.(k).
Definition with_k {t_kinfo t_branch_if_left t_branch_if_right t_k} k
(r : record t_kinfo t_branch_if_left t_branch_if_right t_k) :=
Build t_kinfo t_branch_if_left t_branch_if_right t_k r.(kinfo)
r.(branch_if_left) r.(branch_if_right) k.
End IIf_left.
Definition IIf_left_skeleton := IIf_left.record.
Module IIf_cons.
Record record {kinfo branch_if_cons branch_if_nil k : Set} : Set := Build {
kinfo : kinfo;
branch_if_cons : branch_if_cons;
branch_if_nil : branch_if_nil;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_cons t_branch_if_nil t_k} kinfo
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k kinfo
r.(branch_if_cons) r.(branch_if_nil) r.(k).
Definition with_branch_if_cons
{t_kinfo t_branch_if_cons t_branch_if_nil t_k} branch_if_cons
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
branch_if_cons r.(branch_if_nil) r.(k).
Definition with_branch_if_nil
{t_kinfo t_branch_if_cons t_branch_if_nil t_k} branch_if_nil
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
r.(branch_if_cons) branch_if_nil r.(k).
Definition with_k {t_kinfo t_branch_if_cons t_branch_if_nil t_k} k
(r : record t_kinfo t_branch_if_cons t_branch_if_nil t_k) :=
Build t_kinfo t_branch_if_cons t_branch_if_nil t_k r.(kinfo)
r.(branch_if_cons) r.(branch_if_nil) k.
End IIf_cons.
Definition IIf_cons_skeleton := IIf_cons.record.
Module IIf.
Record record {kinfo branch_if_true branch_if_false k : Set} : Set := Build {
kinfo : kinfo;
branch_if_true : branch_if_true;
branch_if_false : branch_if_false;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_branch_if_true t_branch_if_false t_k}
kinfo (r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k kinfo
r.(branch_if_true) r.(branch_if_false) r.(k).
Definition with_branch_if_true
{t_kinfo t_branch_if_true t_branch_if_false t_k} branch_if_true
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
branch_if_true r.(branch_if_false) r.(k).
Definition with_branch_if_false
{t_kinfo t_branch_if_true t_branch_if_false t_k} branch_if_false
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
r.(branch_if_true) branch_if_false r.(k).
Definition with_k {t_kinfo t_branch_if_true t_branch_if_false t_k} k
(r : record t_kinfo t_branch_if_true t_branch_if_false t_k) :=
Build t_kinfo t_branch_if_true t_branch_if_false t_k r.(kinfo)
r.(branch_if_true) r.(branch_if_false) k.
End IIf.
Definition IIf_skeleton := IIf.record.
Module ICreate_contract.
Record record {kinfo storage_type code k : Set} : Set := Build {
kinfo : kinfo;
storage_type : storage_type;
code : code;
k : k;
}.
Arguments record : clear implicits.
Definition with_kinfo {t_kinfo t_storage_type t_code t_k} kinfo
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k kinfo r.(storage_type) r.(code)
r.(k).
Definition with_storage_type {t_kinfo t_storage_type t_code t_k}
storage_type (r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) storage_type r.(code)
r.(k).
Definition with_code {t_kinfo t_storage_type t_code t_k} code
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type) code
r.(k).
Definition with_k {t_kinfo t_storage_type t_code t_k} k
(r : record t_kinfo t_storage_type t_code t_k) :=
Build t_kinfo t_storage_type t_code t_k r.(kinfo) r.(storage_type)
r.(code) k.
End ICreate_contract.
Definition ICreate_contract_skeleton := ICreate_contract.record.
End kinstr.
Module typed_contract.
Module Typed_contract.
Record record {arg_ty address : Set} : Set := Build {
arg_ty : arg_ty;
address : address;
}.
Arguments record : clear implicits.
Definition with_arg_ty {t_arg_ty t_address} arg_ty
(r : record t_arg_ty t_address) :=
Build t_arg_ty t_address arg_ty r.(address).
Definition with_address {t_arg_ty t_address} address
(r : record t_arg_ty t_address) :=
Build t_arg_ty t_address r.(arg_ty) address.
End Typed_contract.
Definition Typed_contract_skeleton := Typed_contract.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 manager_operation.
Module Transaction.
Record record {transaction location parameters_ty parameters : Set} : Set := Build {
transaction : transaction;
location : location;
parameters_ty : parameters_ty;
parameters : parameters;
}.
Arguments record : clear implicits.
Definition with_transaction
{t_transaction t_location t_parameters_ty t_parameters} transaction
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters transaction
r.(location) r.(parameters_ty) r.(parameters).
Definition with_location
{t_transaction t_location t_parameters_ty t_parameters} location
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) location r.(parameters_ty) r.(parameters).
Definition with_parameters_ty
{t_transaction t_location t_parameters_ty t_parameters} parameters_ty
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) r.(location) parameters_ty r.(parameters).
Definition with_parameters
{t_transaction t_location t_parameters_ty t_parameters} parameters
(r : record t_transaction t_location t_parameters_ty t_parameters) :=
Build t_transaction t_location t_parameters_ty t_parameters
r.(transaction) r.(location) r.(parameters_ty) parameters.
End Transaction.
Definition Transaction_skeleton := Transaction.record.
Module Origination.
Record record {origination preorigination storage_type storage : Set} :
Set := Build {
origination : origination;
preorigination : preorigination;
storage_type : storage_type;
storage : storage;
}.
Arguments record : clear implicits.
Definition with_origination
{t_origination t_preorigination t_storage_type t_storage} origination
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
origination r.(preorigination) r.(storage_type) r.(storage).
Definition with_preorigination
{t_origination t_preorigination t_storage_type t_storage} preorigination
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) preorigination r.(storage_type) r.(storage).
Definition with_storage_type
{t_origination t_preorigination t_storage_type t_storage} storage_type
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) r.(preorigination) storage_type r.(storage).
Definition with_storage
{t_origination t_preorigination t_storage_type t_storage} storage
(r : record t_origination t_preorigination t_storage_type t_storage) :=
Build t_origination t_preorigination t_storage_type t_storage
r.(origination) r.(preorigination) r.(storage_type) storage.
End Origination.
Definition Origination_skeleton := Origination.record.
End manager_operation.
End
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
Import
ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.
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 kinfo.
Record record {iloc kstack_ty : Set} : Set := Build {
iloc : iloc;
kstack_ty : kstack_ty;
}.
Arguments record : clear implicits.
Definition with_iloc {t_iloc t_kstack_ty} iloc
(r : record t_iloc t_kstack_ty) :=
Build t_iloc t_kstack_ty iloc r.(kstack_ty).
Definition with_kstack_ty {t_iloc t_kstack_ty} kstack_ty
(r : record t_iloc t_kstack_ty) :=
Build t_iloc t_kstack_ty r.(iloc) kstack_ty.
End kinfo.
Definition kinfo_skeleton := kinfo.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 log_entry log_control log_exit get_log : Set} : Set := Build {
log_interp : log_interp;
log_entry : log_entry;
log_control : log_control;
log_exit : log_exit;
get_log : get_log;
}.
Arguments record : clear implicits.
Definition with_log_interp
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_interp
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log log_interp
r.(log_entry) r.(log_control) r.(log_exit) r.(get_log).
Definition with_log_entry
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_entry
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) log_entry r.(log_control) r.(log_exit) r.(get_log).
Definition with_log_control
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_control
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) log_control r.(log_exit) r.(get_log).
Definition with_log_exit
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} log_exit
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) r.(log_control) log_exit r.(get_log).
Definition with_get_log
{t_log_interp t_log_entry t_log_control t_log_exit t_get_log} get_log
(r : record t_log_interp t_log_entry t_log_control t_log_exit t_get_log) :=
Build t_log_interp t_log_entry t_log_control t_log_exit t_get_log
r.(log_interp) r.(log_entry) r.(log_control) r.(log_exit) get_log.
End logger.
Definition logger_skeleton := logger.record.
Reserved Notation "'script.Script".
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 "'typed_contract.Typed_contract".
Reserved Notation "'big_map.Big_map".
Reserved Notation "'view_signature.View_signature".
Reserved Notation "'manager_operation.Transaction".
Reserved Notation "'manager_operation.Origination".
Reserved Notation "'logging_function".
Reserved Notation "'execution_trace".
Reserved Notation "'logger".
Reserved Notation "'comparable_ty".
Reserved Notation "'kdescr".
Reserved Notation "'kinfo".
Reserved Notation "'internal_operation".
Reserved Notation "'operation".
Inductive script : Set :=
| Script : ∀ {storage : Set}, 'script.Script storage → script
with kinstr : Set :=
| IDrop : 'kinfo → kinstr → kinstr
| IDup : 'kinfo → kinstr → kinstr
| ISwap : 'kinfo → kinstr → kinstr
| IConst : ∀ {ty : Set}, 'kinfo → ty → kinstr → kinstr
| ICons_pair : 'kinfo → kinstr → kinstr
| ICar : 'kinfo → kinstr → kinstr
| ICdr : 'kinfo → kinstr → kinstr
| IUnpair : 'kinfo → kinstr → kinstr
| ICons_some : 'kinfo → kinstr → kinstr
| ICons_none : 'kinfo → kinstr → kinstr
| IIf_none : 'kinstr.IIf_none → kinstr
| IOpt_map : 'kinstr.IOpt_map → kinstr
| ICons_left : 'kinfo → kinstr → kinstr
| ICons_right : 'kinfo → kinstr → kinstr
| IIf_left : 'kinstr.IIf_left → kinstr
| ICons_list : 'kinfo → kinstr → kinstr
| INil : 'kinfo → kinstr → kinstr
| IIf_cons : 'kinstr.IIf_cons → kinstr
| IList_map : 'kinfo → kinstr → kinstr → kinstr
| IList_iter : 'kinfo → kinstr → kinstr → kinstr
| IList_size : 'kinfo → kinstr → kinstr
| IEmpty_set : 'kinfo → 'comparable_ty → kinstr → kinstr
| ISet_iter : 'kinfo → kinstr → kinstr → kinstr
| ISet_mem : 'kinfo → kinstr → kinstr
| ISet_update : 'kinfo → kinstr → kinstr
| ISet_size : 'kinfo → kinstr → kinstr
| IEmpty_map : 'kinfo → 'comparable_ty → kinstr → kinstr
| IMap_map : 'kinfo → kinstr → kinstr → kinstr
| IMap_iter : 'kinfo → kinstr → kinstr → kinstr
| IMap_mem : 'kinfo → kinstr → kinstr
| IMap_get : 'kinfo → kinstr → kinstr
| IMap_update : 'kinfo → kinstr → kinstr
| IMap_get_and_update : 'kinfo → kinstr → kinstr
| IMap_size : 'kinfo → kinstr → kinstr
| IEmpty_big_map : 'kinfo → 'comparable_ty → ty → kinstr → kinstr
| IBig_map_mem : 'kinfo → kinstr → kinstr
| IBig_map_get : 'kinfo → kinstr → kinstr
| IBig_map_update : 'kinfo → kinstr → kinstr
| IBig_map_get_and_update : 'kinfo → kinstr → kinstr
| IConcat_string : 'kinfo → kinstr → kinstr
| IConcat_string_pair : 'kinfo → kinstr → kinstr
| ISlice_string : 'kinfo → kinstr → kinstr
| IString_size : 'kinfo → kinstr → kinstr
| IConcat_bytes : 'kinfo → kinstr → kinstr
| IConcat_bytes_pair : 'kinfo → kinstr → kinstr
| ISlice_bytes : 'kinfo → kinstr → kinstr
| IBytes_size : 'kinfo → kinstr → kinstr
| IAdd_seconds_to_timestamp : 'kinfo → kinstr → kinstr
| IAdd_timestamp_to_seconds : 'kinfo → kinstr → kinstr
| ISub_timestamp_seconds : 'kinfo → kinstr → kinstr
| IDiff_timestamps : 'kinfo → kinstr → kinstr
| IAdd_tez : 'kinfo → kinstr → kinstr
| ISub_tez : 'kinfo → kinstr → kinstr
| ISub_tez_legacy : 'kinfo → kinstr → kinstr
| IMul_teznat : 'kinfo → kinstr → kinstr
| IMul_nattez : 'kinfo → kinstr → kinstr
| IEdiv_teznat : 'kinfo → kinstr → kinstr
| IEdiv_tez : 'kinfo → kinstr → kinstr
| IOr : 'kinfo → kinstr → kinstr
| IAnd : 'kinfo → kinstr → kinstr
| IXor : 'kinfo → kinstr → kinstr
| INot : 'kinfo → kinstr → kinstr
| IIs_nat : 'kinfo → kinstr → kinstr
| INeg : 'kinfo → kinstr → kinstr
| IAbs_int : 'kinfo → kinstr → kinstr
| IInt_nat : 'kinfo → kinstr → kinstr
| IAdd_int : 'kinfo → kinstr → kinstr
| IAdd_nat : 'kinfo → kinstr → kinstr
| ISub_int : 'kinfo → kinstr → kinstr
| IMul_int : 'kinfo → kinstr → kinstr
| IMul_nat : 'kinfo → kinstr → kinstr
| IEdiv_int : 'kinfo → kinstr → kinstr
| IEdiv_nat : 'kinfo → kinstr → kinstr
| ILsl_nat : 'kinfo → kinstr → kinstr
| ILsr_nat : 'kinfo → kinstr → kinstr
| IOr_nat : 'kinfo → kinstr → kinstr
| IAnd_nat : 'kinfo → kinstr → kinstr
| IAnd_int_nat : 'kinfo → kinstr → kinstr
| IXor_nat : 'kinfo → kinstr → kinstr
| INot_int : 'kinfo → kinstr → kinstr
| IIf : 'kinstr.IIf → kinstr
| ILoop : 'kinfo → kinstr → kinstr → kinstr
| ILoop_left : 'kinfo → kinstr → kinstr → kinstr
| IDip : 'kinfo → kinstr → kinstr → kinstr
| IExec : 'kinfo → kinstr → kinstr
| IApply : 'kinfo → ty → kinstr → kinstr
| ILambda : 'kinfo → lambda → kinstr → kinstr
| IFailwith : 'kinfo → Alpha_context.Script.location → ty → kinstr
| ICompare : 'kinfo → 'comparable_ty → kinstr → kinstr
| IEq : 'kinfo → kinstr → kinstr
| INeq : 'kinfo → kinstr → kinstr
| ILt : 'kinfo → kinstr → kinstr
| IGt : 'kinfo → kinstr → kinstr
| ILe : 'kinfo → kinstr → kinstr
| IGe : 'kinfo → kinstr → kinstr
| IAddress : 'kinfo → kinstr → kinstr
| IContract : 'kinfo → ty → Alpha_context.Entrypoint.t → kinstr → kinstr
| IView : 'kinfo → view_signature → kinstr → kinstr
| ITransfer_tokens : 'kinfo → kinstr → kinstr
| IImplicit_account : 'kinfo → kinstr → kinstr
| ICreate_contract : 'kinstr.ICreate_contract → kinstr
| ISet_delegate : 'kinfo → kinstr → kinstr
| INow : 'kinfo → kinstr → kinstr
| IMin_block_time : 'kinfo → kinstr → kinstr
| IBalance : 'kinfo → kinstr → kinstr
| ILevel : 'kinfo → kinstr → kinstr
| ICheck_signature : 'kinfo → kinstr → kinstr
| IHash_key : 'kinfo → kinstr → kinstr
| IPack : 'kinfo → ty → kinstr → kinstr
| IUnpack : 'kinfo → ty → kinstr → kinstr
| IBlake2b : 'kinfo → kinstr → kinstr
| ISha256 : 'kinfo → kinstr → kinstr
| ISha512 : 'kinfo → kinstr → kinstr
| ISource : 'kinfo → kinstr → kinstr
| ISender : 'kinfo → kinstr → kinstr
| ISelf : 'kinfo → ty → Alpha_context.Entrypoint.t → kinstr → kinstr
| ISelf_address : 'kinfo → kinstr → kinstr
| IAmount : 'kinfo → kinstr → kinstr
| ISapling_empty_state :
'kinfo → Alpha_context.Sapling.Memo_size.t → kinstr → kinstr
| ISapling_verify_update : 'kinfo → kinstr → kinstr
| ISapling_verify_update_deprecated : 'kinfo → kinstr → kinstr
| IDig : 'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IDug : 'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IDipn :
'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr →
kinstr
| IDropn :
'kinfo → int → stack_prefix_preservation_witness → kinstr → kinstr
| IChainId : 'kinfo → kinstr → kinstr
| INever : 'kinfo → kinstr
| IVoting_power : 'kinfo → kinstr → kinstr
| ITotal_voting_power : 'kinfo → kinstr → kinstr
| IKeccak : 'kinfo → kinstr → kinstr
| ISha3 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_g1 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_g2 : 'kinfo → kinstr → kinstr
| IAdd_bls12_381_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_g1 : 'kinfo → kinstr → kinstr
| IMul_bls12_381_g2 : 'kinfo → kinstr → kinstr
| IMul_bls12_381_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_z_fr : 'kinfo → kinstr → kinstr
| IMul_bls12_381_fr_z : 'kinfo → kinstr → kinstr
| IInt_bls12_381_fr : 'kinfo → kinstr → kinstr
| INeg_bls12_381_g1 : 'kinfo → kinstr → kinstr
| INeg_bls12_381_g2 : 'kinfo → kinstr → kinstr
| INeg_bls12_381_fr : 'kinfo → kinstr → kinstr
| IPairing_check_bls12_381 : 'kinfo → kinstr → kinstr
| IComb : 'kinfo → int → comb_gadt_witness → kinstr → kinstr
| IUncomb : 'kinfo → int → uncomb_gadt_witness → kinstr → kinstr
| IComb_get : 'kinfo → int → comb_get_gadt_witness → kinstr → kinstr
| IComb_set : 'kinfo → int → comb_set_gadt_witness → kinstr → kinstr
| IDup_n : 'kinfo → int → dup_n_gadt_witness → kinstr → kinstr
| ITicket : 'kinfo → kinstr → kinstr
| IRead_ticket : 'kinfo → kinstr → kinstr
| ISplit_ticket : 'kinfo → kinstr → kinstr
| IJoin_tickets : 'kinfo → 'comparable_ty → kinstr → kinstr
| IOpen_chest : 'kinfo → kinstr → kinstr
| IHalt : 'kinfo → kinstr
| ILog : 'kinfo → logging_event → 'logger → kinstr → kinstr
with logging_event : Set :=
| LogEntry : logging_event
| LogExit : 'kinfo → logging_event
with lambda : Set :=
| Lam : 'kdescr → Alpha_context.Script.node → lambda
with typed_contract : Set :=
| Typed_contract : 'typed_contract.Typed_contract → typed_contract
with continuation : Set :=
| KNil : continuation
| KCons : kinstr → continuation → continuation
| KReturn : ∀ {s : Set}, s → continuation → continuation
| KMap_head : ∀ {a b : Set}, (a → b) → continuation → continuation
| KUndip : ∀ {b : Set}, b → continuation → continuation
| KLoop_in : kinstr → continuation → continuation
| KLoop_in_left : kinstr → continuation → continuation
| KIter : ∀ {a : Set}, kinstr → list a → continuation → continuation
| KList_enter_body : ∀ {a b : Set},
kinstr → list a → list b → int → continuation → continuation
| KList_exit_body : ∀ {a b : Set},
kinstr → list a → list b → int → continuation → continuation
| KMap_enter_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → continuation → continuation
| KMap_exit_body : ∀ {a b c : Set},
kinstr → list (a × b) → map a c → a → continuation → continuation
| KView_exit : step_constants → continuation → continuation
| KLog : continuation → 'logger → continuation
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 :
'kinfo → 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 manager_operation : Set :=
| Transaction : ∀ {a : Set},
'manager_operation.Transaction a → manager_operation
| Origination : ∀ {storage : Set},
'manager_operation.Origination storage → manager_operation
| Delegation : option Signature.public_key_hash → manager_operation
with packed_internal_operation : Set :=
| Internal_operation : 'internal_operation → packed_internal_operation
where "'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.t ×
list Alpha_context.Script.expr))
and "'comparable_ty" := ((fun _ ⇒ ty) tt)
and "'kdescr" :=
(kdescr_skeleton Alpha_context.Script.location stack_ty stack_ty kinstr)
and "'kinfo" := (kinfo_skeleton Alpha_context.Script.location stack_ty)
and "'internal_operation" :=
(internal_operation_skeleton Alpha_context.Contract.contract manager_operation
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)
(∀ {a s : Set}, 'logging_function a s) (continuation → unit)
(∀ {c u : Set}, 'logging_function c u)
(unit → M? (option 'execution_trace)))
and "'script.Script" :=
(fun (t_storage : Set) ⇒ script.Script_skeleton lambda ty t_storage ty
view_map entrypoints Cache_memory_helpers.sint)
and "'kinstr.IIf_none" := (kinstr.IIf_none_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IOpt_map" := (kinstr.IOpt_map_skeleton 'kinfo kinstr kinstr)
and "'kinstr.IIf_left" := (kinstr.IIf_left_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf_cons" := (kinstr.IIf_cons_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.IIf" := (kinstr.IIf_skeleton 'kinfo kinstr kinstr kinstr)
and "'kinstr.ICreate_contract" :=
(kinstr.ICreate_contract_skeleton 'kinfo ty Alpha_context.Script.expr kinstr)
and "'typed_contract.Typed_contract" :=
(typed_contract.Typed_contract_skeleton ty address)
and "'big_map.Big_map" :=
(fun (t_key t_value : Set) ⇒ big_map.Big_map_skeleton
(option Alpha_context.Big_map.Id.t) (big_map_overlay t_key t_value)
'comparable_ty ty)
and "'view_signature.View_signature" :=
(view_signature.View_signature_skeleton Alpha_context.Script_string.t ty ty)
and "'manager_operation.Transaction" :=
(fun (t_a : Set) ⇒ manager_operation.Transaction_skeleton
Alpha_context.transaction Alpha_context.Script.location ty t_a)
and "'manager_operation.Origination" :=
(fun (t_storage : Set) ⇒ manager_operation.Origination_skeleton
Alpha_context.origination Alpha_context.Contract.t ty t_storage).
Module script.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.script.
Definition Script := 'script.Script.
End script.
Module kinstr.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.kinstr.
Definition IIf_none := 'kinstr.IIf_none.
Definition IOpt_map := 'kinstr.IOpt_map.
Definition IIf_left := 'kinstr.IIf_left.
Definition IIf_cons := 'kinstr.IIf_cons.
Definition IIf := 'kinstr.IIf.
Definition ICreate_contract := 'kinstr.ICreate_contract.
End kinstr.
Module typed_contract.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.typed_contract.
Definition Typed_contract := 'typed_contract.Typed_contract.
End typed_contract.
Module big_map.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.big_map.
Definition Big_map := 'big_map.Big_map.
End big_map.
Module view_signature.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.view_signature.
Definition View_signature := 'view_signature.View_signature.
End view_signature.
Module manager_operation.
Include ConstructorRecords_script_kinstr_typed_contract_big_map_view_signature_manager_operation.manager_operation.
Definition Transaction := 'manager_operation.Transaction.
Definition Origination := 'manager_operation.Origination.
End manager_operation.
Definition logging_function := 'logging_function.
Definition execution_trace := 'execution_trace.
Definition logger := 'logger.
Definition comparable_ty := 'comparable_ty.
Definition kdescr := 'kdescr.
Definition kinfo := 'kinfo.
Definition internal_operation := 'internal_operation.
Definition operation := 'operation.
Inductive packed_manager_operation : Set :=
| Manager : manager_operation → packed_manager_operation.
Definition manager_kind (function_parameter : manager_operation)
: Alpha_context.Kind.manager :=
match function_parameter with
| Transaction _ ⇒ Alpha_context.Kind.Transaction_manager_kind
| Origination _ ⇒ Alpha_context.Kind.Origination_manager_kind
| Delegation _ ⇒ Alpha_context.Kind.Delegation_manager_kind
end.
Definition kinfo_of_kinstr (i_value : kinstr) : kinfo :=
match i_value with
| IDrop kinfo_value _ ⇒ kinfo_value
| IDup kinfo_value _ ⇒ kinfo_value
| ISwap kinfo_value _ ⇒ kinfo_value
| IConst kinfo_value _ _ ⇒ kinfo_value
| ICons_pair kinfo_value _ ⇒ kinfo_value
| ICar kinfo_value _ ⇒ kinfo_value
| ICdr kinfo_value _ ⇒ kinfo_value
| IUnpair kinfo_value _ ⇒ kinfo_value
| ICons_some kinfo_value _ ⇒ kinfo_value
| ICons_none kinfo_value _ ⇒ kinfo_value
| IIf_none {| kinstr.IIf_none.kinfo := kinfo_value |} ⇒ kinfo_value
| IOpt_map {| kinstr.IOpt_map.kinfo := kinfo_value |} ⇒ kinfo_value
| ICons_left kinfo_value _ ⇒ kinfo_value
| ICons_right kinfo_value _ ⇒ kinfo_value
| IIf_left {| kinstr.IIf_left.kinfo := kinfo_value |} ⇒ kinfo_value
| ICons_list kinfo_value _ ⇒ kinfo_value
| INil kinfo_value _ ⇒ kinfo_value
| IIf_cons {| kinstr.IIf_cons.kinfo := kinfo_value |} ⇒ kinfo_value
| IList_map kinfo_value _ _ ⇒ kinfo_value
| IList_iter kinfo_value _ _ ⇒ kinfo_value
| IList_size kinfo_value _ ⇒ kinfo_value
| IEmpty_set kinfo_value _ _ ⇒ kinfo_value
| ISet_iter kinfo_value _ _ ⇒ kinfo_value
| ISet_mem kinfo_value _ ⇒ kinfo_value
| ISet_update kinfo_value _ ⇒ kinfo_value
| ISet_size kinfo_value _ ⇒ kinfo_value
| IEmpty_map kinfo_value _ _ ⇒ kinfo_value
| IMap_map kinfo_value _ _ ⇒ kinfo_value
| IMap_iter kinfo_value _ _ ⇒ kinfo_value
| IMap_mem kinfo_value _ ⇒ kinfo_value
| IMap_get kinfo_value _ ⇒ kinfo_value
| IMap_update kinfo_value _ ⇒ kinfo_value
| IMap_get_and_update kinfo_value _ ⇒ kinfo_value
| IMap_size kinfo_value _ ⇒ kinfo_value
| IEmpty_big_map kinfo_value _ _ _ ⇒ kinfo_value
| IBig_map_mem kinfo_value _ ⇒ kinfo_value
| IBig_map_get kinfo_value _ ⇒ kinfo_value
| IBig_map_update kinfo_value _ ⇒ kinfo_value
| IBig_map_get_and_update kinfo_value _ ⇒ kinfo_value
| IConcat_string kinfo_value _ ⇒ kinfo_value
| IConcat_string_pair kinfo_value _ ⇒ kinfo_value
| ISlice_string kinfo_value _ ⇒ kinfo_value
| IString_size kinfo_value _ ⇒ kinfo_value
| IConcat_bytes kinfo_value _ ⇒ kinfo_value
| IConcat_bytes_pair kinfo_value _ ⇒ kinfo_value
| ISlice_bytes kinfo_value _ ⇒ kinfo_value
| IBytes_size kinfo_value _ ⇒ kinfo_value
| IAdd_seconds_to_timestamp kinfo_value _ ⇒ kinfo_value
| IAdd_timestamp_to_seconds kinfo_value _ ⇒ kinfo_value
| ISub_timestamp_seconds kinfo_value _ ⇒ kinfo_value
| IDiff_timestamps kinfo_value _ ⇒ kinfo_value
| IAdd_tez kinfo_value _ ⇒ kinfo_value
| ISub_tez kinfo_value _ ⇒ kinfo_value
| ISub_tez_legacy kinfo_value _ ⇒ kinfo_value
| IMul_teznat kinfo_value _ ⇒ kinfo_value
| IMul_nattez kinfo_value _ ⇒ kinfo_value
| IEdiv_teznat kinfo_value _ ⇒ kinfo_value
| IEdiv_tez kinfo_value _ ⇒ kinfo_value
| IOr kinfo_value _ ⇒ kinfo_value
| IAnd kinfo_value _ ⇒ kinfo_value
| IXor kinfo_value _ ⇒ kinfo_value
| INot kinfo_value _ ⇒ kinfo_value
| IIs_nat kinfo_value _ ⇒ kinfo_value
| INeg kinfo_value _ ⇒ kinfo_value
| IAbs_int kinfo_value _ ⇒ kinfo_value
| IInt_nat kinfo_value _ ⇒ kinfo_value
| IAdd_int kinfo_value _ ⇒ kinfo_value
| IAdd_nat kinfo_value _ ⇒ kinfo_value
| ISub_int kinfo_value _ ⇒ kinfo_value
| IMul_int kinfo_value _ ⇒ kinfo_value
| IMul_nat kinfo_value _ ⇒ kinfo_value
| IEdiv_int kinfo_value _ ⇒ kinfo_value
| IEdiv_nat kinfo_value _ ⇒ kinfo_value
| ILsl_nat kinfo_value _ ⇒ kinfo_value
| ILsr_nat kinfo_value _ ⇒ kinfo_value
| IOr_nat kinfo_value _ ⇒ kinfo_value
| IAnd_nat kinfo_value _ ⇒ kinfo_value
| IAnd_int_nat kinfo_value _ ⇒ kinfo_value
| IXor_nat kinfo_value _ ⇒ kinfo_value
| INot_int kinfo_value _ ⇒ kinfo_value
| IIf {| kinstr.IIf.kinfo := kinfo_value |} ⇒ kinfo_value
| ILoop kinfo_value _ _ ⇒ kinfo_value
| ILoop_left kinfo_value _ _ ⇒ kinfo_value
| IDip kinfo_value _ _ ⇒ kinfo_value
| IExec kinfo_value _ ⇒ kinfo_value
| IApply kinfo_value _ _ ⇒ kinfo_value
| ILambda kinfo_value _ _ ⇒ kinfo_value
| IFailwith kinfo_value _ _ ⇒ kinfo_value
| ICompare kinfo_value _ _ ⇒ kinfo_value
| IEq kinfo_value _ ⇒ kinfo_value
| INeq kinfo_value _ ⇒ kinfo_value
| ILt kinfo_value _ ⇒ kinfo_value
| IGt kinfo_value _ ⇒ kinfo_value
| ILe kinfo_value _ ⇒ kinfo_value
| IGe kinfo_value _ ⇒ kinfo_value
| IAddress kinfo_value _ ⇒ kinfo_value
| IContract kinfo_value _ _ _ ⇒ kinfo_value
| ITransfer_tokens kinfo_value _ ⇒ kinfo_value
| IView kinfo_value _ _ ⇒ kinfo_value
| IImplicit_account kinfo_value _ ⇒ kinfo_value
| ICreate_contract {| kinstr.ICreate_contract.kinfo := kinfo_value |} ⇒
kinfo_value
| ISet_delegate kinfo_value _ ⇒ kinfo_value
| INow kinfo_value _ ⇒ kinfo_value
| IMin_block_time kinfo_value _ ⇒ kinfo_value
| IBalance kinfo_value _ ⇒ kinfo_value
| ILevel kinfo_value _ ⇒ kinfo_value
| ICheck_signature kinfo_value _ ⇒ kinfo_value
| IHash_key kinfo_value _ ⇒ kinfo_value
| IPack kinfo_value _ _ ⇒ kinfo_value
| IUnpack kinfo_value _ _ ⇒ kinfo_value
| IBlake2b kinfo_value _ ⇒ kinfo_value
| ISha256 kinfo_value _ ⇒ kinfo_value
| ISha512 kinfo_value _ ⇒ kinfo_value
| ISource kinfo_value _ ⇒ kinfo_value
| ISender kinfo_value _ ⇒ kinfo_value
| ISelf kinfo_value _ _ _ ⇒ kinfo_value
| ISelf_address kinfo_value _ ⇒ kinfo_value
| IAmount kinfo_value _ ⇒ kinfo_value
| ISapling_empty_state kinfo_value _ _ ⇒ kinfo_value
| ISapling_verify_update kinfo_value _ ⇒ kinfo_value
| ISapling_verify_update_deprecated kinfo_value _ ⇒ kinfo_value
| IDig kinfo_value _ _ _ ⇒ kinfo_value
| IDug kinfo_value _ _ _ ⇒ kinfo_value
| IDipn kinfo_value _ _ _ _ ⇒ kinfo_value
| IDropn kinfo_value _ _ _ ⇒ kinfo_value
| IChainId kinfo_value _ ⇒ kinfo_value
| INever kinfo_value ⇒ kinfo_value
| IVoting_power kinfo_value _ ⇒ kinfo_value
| ITotal_voting_power kinfo_value _ ⇒ kinfo_value
| IKeccak kinfo_value _ ⇒ kinfo_value
| ISha3 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| IAdd_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_z_fr kinfo_value _ ⇒ kinfo_value
| IMul_bls12_381_fr_z kinfo_value _ ⇒ kinfo_value
| IInt_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_g1 kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_g2 kinfo_value _ ⇒ kinfo_value
| INeg_bls12_381_fr kinfo_value _ ⇒ kinfo_value
| IPairing_check_bls12_381 kinfo_value _ ⇒ kinfo_value
| IComb kinfo_value _ _ _ ⇒ kinfo_value
| IUncomb kinfo_value _ _ _ ⇒ kinfo_value
| IComb_get kinfo_value _ _ _ ⇒ kinfo_value
| IComb_set kinfo_value _ _ _ ⇒ kinfo_value
| IDup_n kinfo_value _ _ _ ⇒ kinfo_value
| ITicket kinfo_value _ ⇒ kinfo_value
| IRead_ticket kinfo_value _ ⇒ kinfo_value
| ISplit_ticket kinfo_value _ ⇒ kinfo_value
| IJoin_tickets kinfo_value _ _ ⇒ kinfo_value
| IHalt kinfo_value ⇒ kinfo_value
| ILog kinfo_value _ _ _ ⇒ kinfo_value
| IOpen_chest kinfo_value _ ⇒ kinfo_value
end.
Module kinstr_rewritek.
Record record : Set := Build {
apply : kinstr → kinstr;
}.
Definition with_apply apply (r : record) :=
Build apply.
End kinstr_rewritek.
Definition kinstr_rewritek := kinstr_rewritek.record.
Definition kinstr_rewritek_value (i_value : kinstr) (f_value : kinstr_rewritek)
: kinstr :=
match i_value with
| IDrop kinfo_value k_value ⇒
IDrop kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IDup kinfo_value k_value ⇒
IDup kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISwap kinfo_value k_value ⇒
ISwap kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConst kinfo_value x_value k_value ⇒
IConst kinfo_value x_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_pair kinfo_value k_value ⇒
ICons_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICar kinfo_value k_value ⇒
ICar kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICdr kinfo_value k_value ⇒
ICdr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IUnpair kinfo_value k_value ⇒
IUnpair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_some kinfo_value k_value ⇒
ICons_some kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_none kinfo_value k_value ⇒
ICons_none kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_none {|
kinstr.IIf_none.kinfo := kinfo_value;
kinstr.IIf_none.branch_if_none := branch_if_none;
kinstr.IIf_none.branch_if_some := branch_if_some;
kinstr.IIf_none.k := k_value
|} ⇒
IIf_none
{| kinstr.IIf_none.kinfo := kinfo_value;
kinstr.IIf_none.branch_if_none :=
f_value.(kinstr_rewritek.apply) branch_if_none;
kinstr.IIf_none.branch_if_some :=
f_value.(kinstr_rewritek.apply) branch_if_some;
kinstr.IIf_none.k := f_value.(kinstr_rewritek.apply) k_value; |}
|
IOpt_map {|
kinstr.IOpt_map.kinfo := kinfo_value;
kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value
|} ⇒
let body := f_value.(kinstr_rewritek.apply) body in
let k_value := f_value.(kinstr_rewritek.apply) k_value in
IOpt_map
{| kinstr.IOpt_map.kinfo := kinfo_value; kinstr.IOpt_map.body := body;
kinstr.IOpt_map.k := k_value; |}
| ICons_left kinfo_value k_value ⇒
ICons_left kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICons_right kinfo_value k_value ⇒
ICons_right kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_left {|
kinstr.IIf_left.kinfo := kinfo_value;
kinstr.IIf_left.branch_if_left := branch_if_left;
kinstr.IIf_left.branch_if_right := branch_if_right;
kinstr.IIf_left.k := k_value
|} ⇒
IIf_left
{| kinstr.IIf_left.kinfo := kinfo_value;
kinstr.IIf_left.branch_if_left :=
f_value.(kinstr_rewritek.apply) branch_if_left;
kinstr.IIf_left.branch_if_right :=
f_value.(kinstr_rewritek.apply) branch_if_right;
kinstr.IIf_left.k := f_value.(kinstr_rewritek.apply) k_value; |}
| ICons_list kinfo_value k_value ⇒
ICons_list kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INil kinfo_value k_value ⇒
INil kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf_cons {|
kinstr.IIf_cons.kinfo := kinfo_value;
kinstr.IIf_cons.branch_if_cons := branch_if_cons;
kinstr.IIf_cons.branch_if_nil := branch_if_nil;
kinstr.IIf_cons.k := k_value
|} ⇒
IIf_cons
{| kinstr.IIf_cons.kinfo := kinfo_value;
kinstr.IIf_cons.branch_if_cons :=
f_value.(kinstr_rewritek.apply) branch_if_cons;
kinstr.IIf_cons.branch_if_nil :=
f_value.(kinstr_rewritek.apply) branch_if_nil;
kinstr.IIf_cons.k := f_value.(kinstr_rewritek.apply) k_value; |}
| IList_map kinfo_value body k_value ⇒
IList_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IList_iter kinfo_value body k_value ⇒
IList_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IList_size kinfo_value k_value ⇒
IList_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_set kinfo_value ty k_value ⇒
IEmpty_set kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| ISet_iter kinfo_value body k_value ⇒
ISet_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| ISet_mem kinfo_value k_value ⇒
ISet_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISet_update kinfo_value k_value ⇒
ISet_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISet_size kinfo_value k_value ⇒
ISet_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_map kinfo_value cty k_value ⇒
IEmpty_map kinfo_value cty (f_value.(kinstr_rewritek.apply) k_value)
| IMap_map kinfo_value body k_value ⇒
IMap_map kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IMap_iter kinfo_value body k_value ⇒
IMap_iter kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IMap_mem kinfo_value k_value ⇒
IMap_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_get kinfo_value k_value ⇒
IMap_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_update kinfo_value k_value ⇒
IMap_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_get_and_update kinfo_value k_value ⇒
IMap_get_and_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMap_size kinfo_value k_value ⇒
IMap_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEmpty_big_map kinfo_value cty ty k_value ⇒
IEmpty_big_map kinfo_value cty ty (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_mem kinfo_value k_value ⇒
IBig_map_mem kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_get kinfo_value k_value ⇒
IBig_map_get kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_update kinfo_value k_value ⇒
IBig_map_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBig_map_get_and_update kinfo_value k_value ⇒
IBig_map_get_and_update kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IConcat_string kinfo_value k_value ⇒
IConcat_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_string_pair kinfo_value k_value ⇒
IConcat_string_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISlice_string kinfo_value k_value ⇒
ISlice_string kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IString_size kinfo_value k_value ⇒
IString_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_bytes kinfo_value k_value ⇒
IConcat_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IConcat_bytes_pair kinfo_value k_value ⇒
IConcat_bytes_pair kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISlice_bytes kinfo_value k_value ⇒
ISlice_bytes kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBytes_size kinfo_value k_value ⇒
IBytes_size kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_seconds_to_timestamp kinfo_value k_value ⇒
IAdd_seconds_to_timestamp kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IAdd_timestamp_to_seconds kinfo_value k_value ⇒
IAdd_timestamp_to_seconds kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| ISub_timestamp_seconds kinfo_value k_value ⇒
ISub_timestamp_seconds kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IDiff_timestamps kinfo_value k_value ⇒
IDiff_timestamps kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_tez kinfo_value k_value ⇒
IAdd_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_tez kinfo_value k_value ⇒
ISub_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_tez_legacy kinfo_value k_value ⇒
ISub_tez_legacy kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_teznat kinfo_value k_value ⇒
IMul_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_nattez kinfo_value k_value ⇒
IMul_nattez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_teznat kinfo_value k_value ⇒
IEdiv_teznat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_tez kinfo_value k_value ⇒
IEdiv_tez kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IOr kinfo_value k_value ⇒
IOr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd kinfo_value k_value ⇒
IAnd kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IXor kinfo_value k_value ⇒
IXor kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INot kinfo_value k_value ⇒
INot kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IIs_nat kinfo_value k_value ⇒
IIs_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg kinfo_value k_value ⇒
INeg kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAbs_int kinfo_value k_value ⇒
IAbs_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IInt_nat kinfo_value k_value ⇒
IInt_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_int kinfo_value k_value ⇒
IAdd_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_nat kinfo_value k_value ⇒
IAdd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISub_int kinfo_value k_value ⇒
ISub_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_int kinfo_value k_value ⇒
IMul_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_nat kinfo_value k_value ⇒
IMul_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_int kinfo_value k_value ⇒
IEdiv_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IEdiv_nat kinfo_value k_value ⇒
IEdiv_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILsl_nat kinfo_value k_value ⇒
ILsl_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILsr_nat kinfo_value k_value ⇒
ILsr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IOr_nat kinfo_value k_value ⇒
IOr_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd_nat kinfo_value k_value ⇒
IAnd_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAnd_int_nat kinfo_value k_value ⇒
IAnd_int_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IXor_nat kinfo_value k_value ⇒
IXor_nat kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INot_int kinfo_value k_value ⇒
INot_int kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
IIf {|
kinstr.IIf.kinfo := kinfo_value;
kinstr.IIf.branch_if_true := branch_if_true;
kinstr.IIf.branch_if_false := branch_if_false;
kinstr.IIf.k := k_value
|} ⇒
IIf
{| kinstr.IIf.kinfo := kinfo_value;
kinstr.IIf.branch_if_true :=
f_value.(kinstr_rewritek.apply) branch_if_true;
kinstr.IIf.branch_if_false :=
f_value.(kinstr_rewritek.apply) branch_if_false;
kinstr.IIf.k := f_value.(kinstr_rewritek.apply) k_value; |}
| ILoop kinfo_value kbody k_value ⇒
ILoop kinfo_value (f_value.(kinstr_rewritek.apply) kbody)
(f_value.(kinstr_rewritek.apply) k_value)
| ILoop_left kinfo_value kl kr ⇒
ILoop_left kinfo_value (f_value.(kinstr_rewritek.apply) kl)
(f_value.(kinstr_rewritek.apply) kr)
| IDip kinfo_value body k_value ⇒
IDip kinfo_value (f_value.(kinstr_rewritek.apply) body)
(f_value.(kinstr_rewritek.apply) k_value)
| IExec kinfo_value k_value ⇒
IExec kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IApply kinfo_value ty k_value ⇒
IApply kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| ILambda kinfo_value l_value k_value ⇒
ILambda kinfo_value l_value (f_value.(kinstr_rewritek.apply) k_value)
| IFailwith kinfo_value i_value ty ⇒ IFailwith kinfo_value i_value ty
| ICompare kinfo_value ty k_value ⇒
ICompare kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IEq kinfo_value k_value ⇒
IEq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeq kinfo_value k_value ⇒
INeq kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILt kinfo_value k_value ⇒
ILt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IGt kinfo_value k_value ⇒
IGt kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILe kinfo_value k_value ⇒
ILe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IGe kinfo_value k_value ⇒
IGe kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAddress kinfo_value k_value ⇒
IAddress kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IContract kinfo_value ty code k_value ⇒
IContract kinfo_value ty code (f_value.(kinstr_rewritek.apply) k_value)
| ITransfer_tokens kinfo_value k_value ⇒
ITransfer_tokens kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IView kinfo_value view_signature k_value ⇒
IView kinfo_value view_signature (f_value.(kinstr_rewritek.apply) k_value)
| IImplicit_account kinfo_value k_value ⇒
IImplicit_account kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
|
ICreate_contract {|
kinstr.ICreate_contract.kinfo := kinfo_value;
kinstr.ICreate_contract.storage_type := storage_type;
kinstr.ICreate_contract.code := code;
kinstr.ICreate_contract.k := k_value
|} ⇒
let k_value := f_value.(kinstr_rewritek.apply) k_value in
ICreate_contract
{| kinstr.ICreate_contract.kinfo := kinfo_value;
kinstr.ICreate_contract.storage_type := storage_type;
kinstr.ICreate_contract.code := code;
kinstr.ICreate_contract.k := k_value; |}
| ISet_delegate kinfo_value k_value ⇒
ISet_delegate kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INow kinfo_value k_value ⇒
INow kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMin_block_time kinfo_value k_value ⇒
IMin_block_time kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IBalance kinfo_value k_value ⇒
IBalance kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ILevel kinfo_value k_value ⇒
ILevel kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ICheck_signature kinfo_value k_value ⇒
ICheck_signature kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IHash_key kinfo_value k_value ⇒
IHash_key kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IPack kinfo_value ty k_value ⇒
IPack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IUnpack kinfo_value ty k_value ⇒
IUnpack kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IBlake2b kinfo_value k_value ⇒
IBlake2b kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha256 kinfo_value k_value ⇒
ISha256 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha512 kinfo_value k_value ⇒
ISha512 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISource kinfo_value k_value ⇒
ISource kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISender kinfo_value k_value ⇒
ISender kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISelf kinfo_value ty s_value k_value ⇒
ISelf kinfo_value ty s_value (f_value.(kinstr_rewritek.apply) k_value)
| ISelf_address kinfo_value k_value ⇒
ISelf_address kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAmount kinfo_value k_value ⇒
IAmount kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISapling_empty_state kinfo_value s_value k_value ⇒
ISapling_empty_state kinfo_value s_value
(f_value.(kinstr_rewritek.apply) k_value)
| ISapling_verify_update kinfo_value k_value ⇒
ISapling_verify_update kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISapling_verify_update_deprecated kinfo_value k_value ⇒
ISapling_verify_update_deprecated kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IDig kinfo_value n_value p_value k_value ⇒
IDig kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IDug kinfo_value n_value p_value k_value ⇒
IDug kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IDipn kinfo_value n_value p_value k1 k2 ⇒
IDipn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k1)
(f_value.(kinstr_rewritek.apply) k2)
| IDropn kinfo_value n_value p_value k_value ⇒
IDropn kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IChainId kinfo_value k_value ⇒
IChainId kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INever kinfo_value ⇒ INever kinfo_value
| IVoting_power kinfo_value k_value ⇒
IVoting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ITotal_voting_power kinfo_value k_value ⇒
ITotal_voting_power kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IKeccak kinfo_value k_value ⇒
IKeccak kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISha3 kinfo_value k_value ⇒
ISha3 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_g1 kinfo_value k_value ⇒
IAdd_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_g2 kinfo_value k_value ⇒
IAdd_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IAdd_bls12_381_fr kinfo_value k_value ⇒
IAdd_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_g1 kinfo_value k_value ⇒
IMul_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_g2 kinfo_value k_value ⇒
IMul_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_fr kinfo_value k_value ⇒
IMul_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_z_fr kinfo_value k_value ⇒
IMul_bls12_381_z_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IMul_bls12_381_fr_z kinfo_value k_value ⇒
IMul_bls12_381_fr_z kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IInt_bls12_381_fr kinfo_value k_value ⇒
IInt_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_g1 kinfo_value k_value ⇒
INeg_bls12_381_g1 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_g2 kinfo_value k_value ⇒
INeg_bls12_381_g2 kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| INeg_bls12_381_fr kinfo_value k_value ⇒
INeg_bls12_381_fr kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IPairing_check_bls12_381 kinfo_value k_value ⇒
IPairing_check_bls12_381 kinfo_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb kinfo_value n_value p_value k_value ⇒
IComb kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| IUncomb kinfo_value n_value p_value k_value ⇒
IUncomb kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb_get kinfo_value n_value p_value k_value ⇒
IComb_get kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IComb_set kinfo_value n_value p_value k_value ⇒
IComb_set kinfo_value n_value p_value
(f_value.(kinstr_rewritek.apply) k_value)
| IDup_n kinfo_value n_value p_value k_value ⇒
IDup_n kinfo_value n_value p_value (f_value.(kinstr_rewritek.apply) k_value)
| ITicket kinfo_value k_value ⇒
ITicket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IRead_ticket kinfo_value k_value ⇒
IRead_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| ISplit_ticket kinfo_value k_value ⇒
ISplit_ticket kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
| IJoin_tickets kinfo_value ty k_value ⇒
IJoin_tickets kinfo_value ty (f_value.(kinstr_rewritek.apply) k_value)
| IHalt kinfo_value ⇒ IHalt kinfo_value
| ILog kinfo_value event logger k_value ⇒
ILog kinfo_value event logger k_value
| IOpen_chest kinfo_value k_value ⇒
IOpen_chest kinfo_value (f_value.(kinstr_rewritek.apply) k_value)
end.
Definition meta_basic : ty_metadata :=
{| ty_metadata.size := Type_size.(TYPE_SIZE.one); |}.
Definition ty_metadata_value (function_parameter : ty) : ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta _ ⇒ meta
| Union_t _ _ meta _ ⇒ meta
| Option_t _ meta _ ⇒ meta
| Lambda_t _ _ meta ⇒ meta
| List_t _ meta ⇒ meta
| Set_t _ meta ⇒ meta
| Map_t _ _ meta ⇒ meta
| Big_map_t _ _ meta ⇒ meta
| Ticket_t _ meta ⇒ meta
| Contract_t _ meta ⇒ meta
|
(Sapling_transaction_t _ | Sapling_transaction_deprecated_t _ |
Sapling_state_t _ | Operation_t | Bls12_381_g1_t | Bls12_381_g2_t |
Bls12_381_fr_t | Chest_t | Chest_key_t) ⇒ meta_basic
end.
Definition comparable_ty_metadata (function_parameter : comparable_ty)
: ty_metadata :=
match function_parameter with
|
(Unit_t | Never_t | Int_t | Nat_t | Signature_t | String_t | Bytes_t |
Mutez_t | Bool_t | Key_hash_t | Key_t | Timestamp_t | Chain_id_t | Address_t
| Tx_rollup_l2_address_t) ⇒ meta_basic
| Pair_t _ _ meta Dependent_bool.YesYes ⇒ meta
| Union_t _ _ meta Dependent_bool.YesYes ⇒ meta
| Option_t _ meta Dependent_bool.Yes ⇒ meta
| _ ⇒ unreachable_gadt_branch
end.
Definition ty_size (t_value : ty) : Type_size.(TYPE_SIZE.t) :=
(ty_metadata_value t_value).(ty_metadata.size).
Definition comparable_ty_size (t_value : comparable_ty)
: Type_size.(TYPE_SIZE.t) :=
(comparable_ty_metadata t_value).(ty_metadata.size).
Definition is_comparable (function_parameter : ty) : Dependent_bool.dbool :=
match function_parameter with
| Never_t ⇒ Dependent_bool.Yes
| Unit_t ⇒ Dependent_bool.Yes
| Int_t ⇒ Dependent_bool.Yes
| Nat_t ⇒ Dependent_bool.Yes
| Signature_t ⇒ Dependent_bool.Yes
| String_t ⇒ Dependent_bool.Yes
| Bytes_t ⇒ Dependent_bool.Yes
| Mutez_t ⇒ Dependent_bool.Yes
| Bool_t ⇒ Dependent_bool.Yes
| Key_hash_t ⇒ Dependent_bool.Yes
| Key_t ⇒ Dependent_bool.Yes
| Timestamp_t ⇒ Dependent_bool.Yes
| Chain_id_t ⇒ Dependent_bool.Yes
| Address_t ⇒ Dependent_bool.Yes
| Tx_rollup_l2_address_t ⇒ Dependent_bool.Yes
| Pair_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Union_t _ _ _ dand_value ⇒ Dependent_bool.dbool_of_dand dand_value
| Option_t _ _ cmp ⇒ cmp
| Lambda_t _ _ _ ⇒ Dependent_bool.No
| List_t _ _ ⇒ Dependent_bool.No
| Set_t _ _ ⇒ Dependent_bool.No
| Map_t _ _ _ ⇒ Dependent_bool.No
| Big_map_t _ _ _ ⇒ Dependent_bool.No
| Ticket_t _ _ ⇒ Dependent_bool.No
| Contract_t _ _ ⇒ Dependent_bool.No
| Sapling_transaction_t _ ⇒ Dependent_bool.No
| Sapling_transaction_deprecated_t _ ⇒ Dependent_bool.No
| Sapling_state_t _ ⇒ Dependent_bool.No
| Operation_t ⇒ Dependent_bool.No
| Bls12_381_g1_t ⇒ Dependent_bool.No
| Bls12_381_g2_t ⇒ Dependent_bool.No
| Bls12_381_fr_t ⇒ Dependent_bool.No
| Chest_t ⇒ Dependent_bool.No
| Chest_key_t ⇒ Dependent_bool.No
end.
Inductive ty_ex_c : Set :=
| Ty_ex_c : ty → ty_ex_c.
Definition unit_t : ty := Unit_t.
Definition unit_key : ty := unit_t.
Definition int_t : ty := Int_t.
Definition int_key : ty := int_t.
Definition nat_t : ty := Nat_t.
Definition nat_key : ty := nat_t.
Definition signature_t : ty := Signature_t.
Definition signature_key : ty := signature_t.
Definition string_t : ty := String_t.
Definition string_key : ty := string_t.
Definition bytes_t : ty := Bytes_t.
Definition bytes_key : ty := bytes_t.
Definition mutez_t : ty := Mutez_t.
Definition mutez_key : ty := mutez_t.
Definition key_hash_t : ty := Key_hash_t.
Definition key_hash_key : ty := key_hash_t.
Definition key_t : ty := Key_t.
Definition key_key : ty := key_t.
Definition timestamp_t : ty := Timestamp_t.
Definition timestamp_key : ty := timestamp_t.
Definition address_t : ty := Address_t.
Definition address_key : ty := address_t.
Definition bool_t : ty := Bool_t.
Definition bool_key : ty := bool_t.
Definition tx_rollup_l2_address_t : ty := Tx_rollup_l2_address_t.
Definition tx_rollup_l2_address_key : ty := tx_rollup_l2_address_t.
Definition pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty_ex_c :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
let 'Dependent_bool.Ex_dand cmp :=
Dependent_bool.dand_value (is_comparable l_value) (is_comparable r_value) in
return?
(Ty_ex_c (Pair_t l_value r_value {| ty_metadata.size := size_value; |} cmp)).
Definition comparable_pair_t
(loc_value : Alpha_context.Script.location) (l_value : ty) (r_value : ty)
: M? ty :=
let? size_value :=
Type_size.(TYPE_SIZE.compound2) loc_value (ty_size l_value)
(ty_size r_value) in
return?
(Pair_t l_value