🍬 Script_family.v
Simulations
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Module Ty.
Module Num.
Inductive t : Set :=
| Int : t
| Nat : t.
End Num.
Inductive t : Set :=
| Unit : t
| Num : Num.t → t
| Signature : t
| String : t
| Bytes : t
| Mutez : t
| Key_hash : t
| Key : t
| Timestamp : t
| Address : t
| Tx_rollup_l2_address : t
| Bool : t
| Pair : t → t → t
| Union : t → t → t
| Lambda : t → t → t
| Option : t → t
| List : t → t
| Set_ : t → t
| Map : t → t → t
| Big_map : t → t → t
| Contract : t → t
| Sapling_transaction : t
| Sapling_transaction_deprecated : t
| Sapling_state : t
| Operation : t
| Chain_id : t
| Never : t
| Bls12_381_g1 : t
| Bls12_381_g2 : t
| Bls12_381_fr : t
| Ticket : t → t
| Chest_key : t
| Chest : t.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Module Ty.
Module Num.
Inductive t : Set :=
| Int : t
| Nat : t.
End Num.
Inductive t : Set :=
| Unit : t
| Num : Num.t → t
| Signature : t
| String : t
| Bytes : t
| Mutez : t
| Key_hash : t
| Key : t
| Timestamp : t
| Address : t
| Tx_rollup_l2_address : t
| Bool : t
| Pair : t → t → t
| Union : t → t → t
| Lambda : t → t → t
| Option : t → t
| List : t → t
| Set_ : t → t
| Map : t → t → t
| Big_map : t → t → t
| Contract : t → t
| Sapling_transaction : t
| Sapling_transaction_deprecated : t
| Sapling_state : t
| Operation : t
| Chain_id : t
| Never : t
| Bls12_381_g1 : t
| Bls12_381_g2 : t
| Bls12_381_fr : t
| Ticket : t → t
| Chest_key : t
| Chest : t.
Return the [Set] corresponding to a [Ty.t]. This is a generic version
depending on [parametrized_sets].
Fixpoint to_Set (ty : Ty.t) : Set :=
match ty with
| Unit ⇒ unit
| Num _ ⇒ Script_int.num
| Signature ⇒ Script_typed_ir.Script_signature.t
| String ⇒ Script_string.t
| Bytes ⇒ Bytes.t
| Mutez ⇒ Tez_repr.t
| Key_hash ⇒ public_key_hash
| Key ⇒ public_key
| Timestamp ⇒ Script_timestamp.t
| Address ⇒ Script_typed_ir.address
| Tx_rollup_l2_address ⇒ Script_typed_ir.tx_rollup_l2_address
| Bool ⇒ bool
| Pair ty1 ty2 ⇒ to_Set ty1 × to_Set ty2
| Union ty1 ty2 ⇒ Script_typed_ir.union (to_Set ty1) (to_Set ty2)
| Lambda ty_arg ty_res ⇒ Script_typed_ir.lambda
| Option ty ⇒ option (to_Set ty)
| List ty ⇒ Script_list.t (to_Set ty)
| Set_ k ⇒ Script_typed_ir.set (to_Set k)
| Map k v ⇒ Script_typed_ir.map (to_Set k) (to_Set v)
| Big_map k v ⇒ Script_typed_ir.big_map
| Contract ty ⇒ Script_typed_ir.typed_contract
| Sapling_transaction ⇒ Alpha_context.Sapling.transaction
| Sapling_transaction_deprecated ⇒
Alpha_context.Sapling.legacy_transaction
| Sapling_state ⇒ Alpha_context.Sapling.state
| Operation ⇒ Script_typed_ir.operation
| Chain_id ⇒ Script_typed_ir.Script_chain_id.t
| Never ⇒ Script_typed_ir.never
| Bls12_381_g1 ⇒ Script_typed_ir.Script_bls.G1.t
| Bls12_381_g2 ⇒ Script_typed_ir.Script_bls.G2.t
| Bls12_381_fr ⇒ Script_typed_ir.Script_bls.Fr.t
| Ticket ty ⇒ Script_typed_ir.ticket (to_Set ty)
| Chest_key ⇒ Script_typed_ir.Script_timelock.chest_key
| Chest ⇒ Script_typed_ir.Script_timelock.chest
end.
End Ty.
Module Stack_ty.
Definition t : Set := list Ty.t.
match ty with
| Unit ⇒ unit
| Num _ ⇒ Script_int.num
| Signature ⇒ Script_typed_ir.Script_signature.t
| String ⇒ Script_string.t
| Bytes ⇒ Bytes.t
| Mutez ⇒ Tez_repr.t
| Key_hash ⇒ public_key_hash
| Key ⇒ public_key
| Timestamp ⇒ Script_timestamp.t
| Address ⇒ Script_typed_ir.address
| Tx_rollup_l2_address ⇒ Script_typed_ir.tx_rollup_l2_address
| Bool ⇒ bool
| Pair ty1 ty2 ⇒ to_Set ty1 × to_Set ty2
| Union ty1 ty2 ⇒ Script_typed_ir.union (to_Set ty1) (to_Set ty2)
| Lambda ty_arg ty_res ⇒ Script_typed_ir.lambda
| Option ty ⇒ option (to_Set ty)
| List ty ⇒ Script_list.t (to_Set ty)
| Set_ k ⇒ Script_typed_ir.set (to_Set k)
| Map k v ⇒ Script_typed_ir.map (to_Set k) (to_Set v)
| Big_map k v ⇒ Script_typed_ir.big_map
| Contract ty ⇒ Script_typed_ir.typed_contract
| Sapling_transaction ⇒ Alpha_context.Sapling.transaction
| Sapling_transaction_deprecated ⇒
Alpha_context.Sapling.legacy_transaction
| Sapling_state ⇒ Alpha_context.Sapling.state
| Operation ⇒ Script_typed_ir.operation
| Chain_id ⇒ Script_typed_ir.Script_chain_id.t
| Never ⇒ Script_typed_ir.never
| Bls12_381_g1 ⇒ Script_typed_ir.Script_bls.G1.t
| Bls12_381_g2 ⇒ Script_typed_ir.Script_bls.G2.t
| Bls12_381_fr ⇒ Script_typed_ir.Script_bls.Fr.t
| Ticket ty ⇒ Script_typed_ir.ticket (to_Set ty)
| Chest_key ⇒ Script_typed_ir.Script_timelock.chest_key
| Chest ⇒ Script_typed_ir.Script_timelock.chest
end.
End Ty.
Module Stack_ty.
Definition t : Set := list Ty.t.
We always represent a stack as a couple with a default head value. This
is to follow the OCaml's convention of always having an [accu] value in
addition of the rest of the [stack]. Here we get the implementation type
for the head of a stack.
Definition to_Set_head (tys : t) : Set :=
match tys with
| [] ⇒ Script_typed_ir.empty_cell
| ty :: _ ⇒ Ty.to_Set ty
end.
match tys with
| [] ⇒ Script_typed_ir.empty_cell
| ty :: _ ⇒ Ty.to_Set ty
end.
The implementation type for the tail of a stack.
Fixpoint to_Set_tail (tys : t) : Set :=
match tys with
| [] ⇒ Script_typed_ir.empty_cell
| _ :: tys ⇒ to_Set_head tys × to_Set_tail tys
end.
match tys with
| [] ⇒ Script_typed_ir.empty_cell
| _ :: tys ⇒ to_Set_head tys × to_Set_tail tys
end.
The implementation type for a stack. It is always syntactically a
couple, so we can call the [fst] and [snd] operators on it to retrieve
the [accu] and [stack] element following the convention in
the OCaml code
Definition to_Set (tys : t) : Set :=
to_Set_head tys × to_Set_tail tys.
Arguments to_Set _ /. (* We automatically unfold this definition *)
End Stack_ty.
to_Set_head tys × to_Set_tail tys.
Arguments to_Set _ /. (* We automatically unfold this definition *)
End Stack_ty.