🍬 Script_family.v

Proofs

See simulations, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Simulations.Script_family.

Module Ty.

[Prop]ositional predicate specifying comparable Michelson types.

  Fixpoint is_Comparable (ty : Ty.t) : Prop :=
    match ty with
    | Ty.Unit
    | Ty.Never
    | Ty.Num _
    | Ty.Signature
    | Ty.String
    | Ty.Bytes
    | Ty.Mutez
    | Ty.Bool
    | Ty.Key_hash
    | Ty.Key
    | Ty.Timestamp
    | Ty.Chain_id
    | Ty.Address
    | Ty.Tx_rollup_l2_address ⇒ True
    | Ty.Pair t1 t2 ⇒
          is_Comparable t1
        ∧ is_Comparable t2
    | Ty.Union t1 t2 ⇒
          is_Comparable t1
        ∧ is_Comparable t2
    | Ty.Option t' ⇒
        is_Comparable t'
    | _ ⇒ False
    end.

The validity of a type.

  Module Valid.
    Fixpoint t (ty : Ty.t) : Prop :=
      match ty with
      | Ty.Unit ⇒ True
      | Ty.Num _ ⇒ True
      | Ty.Signature ⇒ True
      | Ty.String ⇒ True
      | Ty.Bytes ⇒ True
      | Ty.Mutez ⇒ True
      | Ty.Key_hash ⇒ True
      | Ty.Key ⇒ True
      | Ty.Timestamp ⇒ True
      | Ty.Address ⇒ True
      | Ty.Tx_rollup_l2_address ⇒ True
      | Ty.Bool ⇒ True
      | Ty.Pair ty1 ty2 ⇒ t ty1 ∧ t ty2
      | Ty.Union ty1 ty2 ⇒ t ty1 ∧ t ty2
      | Ty.Lambda arg ret ⇒ t arg ∧ t ret
      | Ty.Option ty ⇒ t ty
      | Ty.List ty ⇒ t ty
      | Ty.Set_ key ⇒ is_Comparable key ∧ t key
      | Ty.Map key value ⇒ is_Comparable key ∧ t key ∧ t value
      | Ty.Big_map key value ⇒ is_Comparable key ∧ t key ∧ t value
      | Ty.Contract ty ⇒ t ty
      | Ty.Sapling_transaction ⇒ True
      | Ty.Sapling_transaction_deprecated ⇒ True
      | Ty.Sapling_state ⇒ True
      | Ty.Operation ⇒ True
      | Ty.Chain_id ⇒ True
      | Ty.Never ⇒ True
      | Ty.Bls12_381_g1 ⇒ True
      | Ty.Bls12_381_g2 ⇒ True
      | Ty.Bls12_381_fr ⇒ True
      | Ty.Ticket ty ⇒ is_Comparable ty ∧ t ty
      | Ty.Chest_key ⇒ True
      | Ty.Chest ⇒ True
      end.
  End Valid.
End Ty.

Module Stack_ty.

The validity of a stack family.

  Module Valid.
    Definition t (tys : Stack_ty.t) : Prop :=
      List.Forall Ty.Valid.t tys.
  End Valid.
End Stack_ty.