Skip to main content

🍬 Script_family.v

Simulations

See proofs, Gitlab , OCaml

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.

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
    | Unitunit
    | Num _Script_int.num
    | SignatureScript_typed_ir.Script_signature.t
    | StringScript_string.t
    | BytesBytes.t
    | MutezTez_repr.t
    | Key_hashpublic_key_hash
    | Keypublic_key
    | TimestampScript_timestamp.t
    | AddressScript_typed_ir.address
    | Tx_rollup_l2_addressScript_typed_ir.tx_rollup_l2_address
    | Boolbool
    | Pair ty1 ty2to_Set ty1 × to_Set ty2
    | Union ty1 ty2Script_typed_ir.union (to_Set ty1) (to_Set ty2)
    | Lambda ty_arg ty_resScript_typed_ir.lambda
    | Option tyoption (to_Set ty)
    | List tyScript_list.t (to_Set ty)
    | Set_ kScript_typed_ir.set (to_Set k)
    | Map k vScript_typed_ir.map (to_Set k) (to_Set v)
    | Big_map k vScript_typed_ir.big_map
    | Contract tyScript_typed_ir.typed_contract
    | Sapling_transactionAlpha_context.Sapling.transaction
    | Sapling_transaction_deprecated
      Alpha_context.Sapling.legacy_transaction
    | Sapling_stateAlpha_context.Sapling.state
    | OperationScript_typed_ir.operation
    | Chain_idScript_typed_ir.Script_chain_id.t
    | NeverScript_typed_ir.never
    | Bls12_381_g1Script_typed_ir.Script_bls.G1.t
    | Bls12_381_g2Script_typed_ir.Script_bls.G2.t
    | Bls12_381_frScript_typed_ir.Script_bls.Fr.t
    | Ticket tyScript_typed_ir.ticket (to_Set ty)
    | Chest_keyScript_typed_ir.Script_timelock.chest_key
    | ChestScript_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.

The implementation type for the tail of a stack.
  Fixpoint to_Set_tail (tys : t) : Set :=
    match tys with
    | []Script_typed_ir.empty_cell
    | _ :: tysto_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.