🍬 Script_typed_ir.v

Proofs

Recursive predicate specifying that a [ty] from [ty] is comparable.

Validity predicate for the type [Script_typed_ir.ty]

    Fixpoint t (ty : Script_typed_ir.ty) : Prop :=
      match ty with
      | Script_typed_ir.Unit_t
      | Script_typed_ir.Int_t
      | Script_typed_ir.Nat_t
      | Script_typed_ir.Signature_t
      | Script_typed_ir.String_t
      | Script_typed_ir.Bytes_t
      | Script_typed_ir.Mutez_t
      | Script_typed_ir.Key_hash_t
      | Script_typed_ir.Key_t
      | Script_typed_ir.Timestamp_t
      | Script_typed_ir.Address_t
      | Script_typed_ir.Tx_rollup_l2_address_t
      | Script_typed_ir.Bool_t ⇒ True
      | Script_typed_ir.Pair_t ty1 ty2 metadata dep_bool
      | Script_typed_ir.Union_t ty1 ty2 metadata dep_bool ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size ty1 +i
            Script_typed_ir.ty_size ty2) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
          ( let d1 := Script_typed_ir.is_comparable ty1 in
            let d2 := Script_typed_ir.is_comparable ty2 in
            let '(Dependent_bool.Ex_dand dnd) :=
            Dependent_bool.dand_value d1 d2 in dnd = dep_bool ) ∧
            t ty1 ∧ t ty2
      | Script_typed_ir.Lambda_t ty1 ty2 metadata ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size ty1 +i
            Script_typed_ir.ty_size ty2) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
          t ty1 ∧ t ty2
      | Script_typed_ir.Option_t ty metadata dep_bool ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size ty) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
          t ty
      | Script_typed_ir.List_t ty metadata ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size ty) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
          t ty
      | Script_typed_ir.Set_t comp_ty metadata ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size comp_ty) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size )
          ∧ t comp_ty ∧ Comparable.t comp_ty
      | Script_typed_ir.Map_t comp_ty ty metadata
      | Script_typed_ir.Big_map_t comp_ty ty metadata ⇒
          ( let sz := (1 +i Script_typed_ir.ty_size comp_ty +i
            Script_typed_ir.ty_size ty) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
          Comparable.t comp_ty ∧ t comp_ty ∧ t ty
      | Script_typed_ir.Contract_t ty metadata ⇒ t ty ∧
          ( let sz := (1 +i Script_typed_ir.ty_size ty) in
            metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
            sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
            t ty
      | Script_typed_ir.Sapling_transaction_t memo
      | Script_typed_ir.Sapling_transaction_deprecated_t memo
      | Script_typed_ir.Sapling_state_t memo ⇒
          Sapling_repr.Memo_size.Valid.t memo
      | Script_typed_ir.Operation_t
      | Script_typed_ir.Chain_id_t
      | Script_typed_ir.Never_t
      | Script_typed_ir.Bls12_381_g1_t
      | Script_typed_ir.Bls12_381_g2_t
      | Script_typed_ir.Bls12_381_fr_t ⇒ True
      | Script_typed_ir.Ticket_t comp_ty metadata ⇒
        ( let sz := (1 +i Script_typed_ir.ty_size comp_ty) in
           metadata = {| Script_typed_ir.ty_metadata.size := sz |} ∧
           sz ≤ Alpha_context.Constants.michelson_maximum_type_size ) ∧
        Comparable.t comp_ty ∧ t comp_ty
      | Script_typed_ir.Chest_key_t
      | Script_typed_ir.Chest_t ⇒ True
      end.

IMPORTANT: [proj_rel] below should be replaced everywhere with the underlying function it defines, which is [to_Ty_t] below. Defining the validity of the type [ty] of Michelson types' ASTs. More precisely, [proj_rel ty0 ty] when the AST of [ty0 : Ty.t] is a collapse of the AST of [ty]. @TODO specify when/why it's needed (probably unnecessary) @TODO should probably be renamed or removed

The predicate [t] above is functional. [to_Ty_t sty] computes the unique [ty] such that [t ty sty]. [to_Ty_t] is (and will probably remain) surjective in Proto_alpha (Lima).

We consider size of all [x : Script_typed_ir.ty] within the nodes are Valid, i.e. 0 <= x <= Saturation_repr.saturated.

    Axiom saturation_ty_size : ∀ (arg_type : Script_typed_ir.ty),
      Saturation_repr.Valid.t (Sc_rollup_costs.is_valid_parameters_ty_cost
        (Script_typed_ir.Type_size.to_int (Script_typed_ir.ty_size arg_type))).

  End Valid.
End ty.

@TODO Not sure if the predicate below really are validity predicates. @TODO When checked, define the suitable modules.

Module stack_ty.
Module Valid.

Validity predicate for the type [stack_ty].

  Inductive t : Stack_ty.t → stack_ty → Prop :=
  | Item_t {ty_ rest} ty script_rest :
    ty.Valid.proj_rel ty_ ty →
    t rest script_rest →
    t (ty_ :: rest) (Script_typed_ir.Item_t ty script_rest)
  | Bot_t :
    t [] Script_typed_ir.Bot_t.
  End Valid.
End stack_ty.

@TODO: Every type [foo] which does not need a recursively defined predicate should be put outside module [Script_typed_ir.Valid] and put in a module [foo].

Module Valid.

Validity predicate for [stack_prefix_preservation_witness].

  Inductive stack_prefix_preservation_witness :
    Stack_ty.t → Stack_ty.t → Stack_ty.t → Stack_ty.t →
    stack_prefix_preservation_witness → Prop :=
  | KPrefix : ∀ {a s t u v} loc ty witn,
      ty.Valid.proj_rel a ty →
      stack_prefix_preservation_witness s t u v witn →
      stack_prefix_preservation_witness s t (a :: u) (a :: v)
        (Script_typed_ir.KPrefix loc ty witn)
  | KRest : ∀ {s t}, stack_prefix_preservation_witness s t s t
                       Script_typed_ir.KRest.

Validity predicate for [comb_gadt_witness].

  Inductive comb_gadt_witness : Stack_ty.t → Stack_ty.t →
    comb_gadt_witness → Prop :=
  | Comb_one : ∀ {s}, comb_gadt_witness s s Script_typed_ir.Comb_one
  | Comb_succ : ∀ {a b s s'} w1,
      comb_gadt_witness s (b :: s') w1 →
      comb_gadt_witness (a :: s) (Ty.Pair a b :: s')
        (Script_typed_ir.Comb_succ w1) .

Validity predicate for [uncomb_gadt_witness].

  Inductive uncomb_gadt_witness : Stack_ty.t → Stack_ty.t →
    uncomb_gadt_witness → Prop :=
  | Uncomb_one : ∀ {s}, uncomb_gadt_witness s s Script_typed_ir.Uncomb_one
  | Uncomb_succ : ∀ {a b s s'} w1,
      uncomb_gadt_witness (b :: s) s' w1 →
      uncomb_gadt_witness (Ty.Pair a b :: s) (a :: s')
        (Script_typed_ir.Uncomb_succ w1).

Validity predicate for [comb_get_gadt_witness].

  Inductive comb_get_gadt_witness : Ty.t → Ty.t →
    comb_get_gadt_witness → Prop :=
  | Comb_get_zero : ∀ {b}, comb_get_gadt_witness b b
      Script_typed_ir.Comb_get_zero
  | Comb_get_one : ∀ {a b}, comb_get_gadt_witness (Ty.Pair a b) a
      Script_typed_ir.Comb_get_one
  | Comb_get_plus_two : ∀ {a b c} w1,
      comb_get_gadt_witness b c w1→
      comb_get_gadt_witness (Ty.Pair a b) c
        (Script_typed_ir.Comb_get_plus_two w1).

Validity predicate for [comb_set_gadt_witness].

  Inductive comb_set_gadt_witness : Ty.t → Ty.t → Ty.t →
    comb_set_gadt_witness → Prop :=
  | Comb_set_zero : ∀ {v a}, comb_set_gadt_witness v a v
      Script_typed_ir.Comb_set_zero
  | Comb_set_one : ∀ {v a b},
      comb_set_gadt_witness v (Ty.Pair a b) (Ty.Pair v b)
        Script_typed_ir.Comb_set_one
  | Comb_set_plus_two : ∀ {v a b c} w1,
      comb_set_gadt_witness v b c w1 →
      comb_set_gadt_witness v (Ty.Pair a b) (Ty.Pair a c)
        (Script_typed_ir.Comb_set_plus_two w1).

Validity predicate for [dup_n_gadt_witness].

  Inductive dup_n_gadt_witness : Stack_ty.t → Ty.t →
    dup_n_gadt_witness → Prop :=
  | Dup_n_zero : ∀ {a s}, dup_n_gadt_witness (a :: s) a
      (Script_typed_ir.Dup_n_zero)
  | Dup_n_succ : ∀ {a b s} w1, dup_n_gadt_witness s b w1 →
      dup_n_gadt_witness (a :: s) b (Script_typed_ir.Dup_n_succ w1).

Validity predicate for [view_signature].

  Inductive view_signature : Ty.t → Ty.t → view_signature → Prop :=
  | View_signature {a b} name tya tyb :
    (* input_ty *)
    ty.Valid.proj_rel a tya →
    (* output_ty *)
    ty.Valid.proj_rel b tyb →
    view_signature a b
      (Script_typed_ir.View_signature
         {|
           Script_typed_ir.view_signature.View_signature.name := name;
           Script_typed_ir.view_signature.View_signature.input_ty := tya;
           Script_typed_ir.view_signature.View_signature.output_ty := tyb;
         |}).

  Reserved Notation "'Script_Map".

The predicate [kinstr st1 st2 k] specifies that the instruction [k] is valid and produces the stack [st2] from the stack [st1]. @TODO add the suitable validity condition, e.g. comparability and so on. For the future, it could be useful to---if possible: Define a validity predicate with [st1] and [k] as sole variables. Define a function computing [st2] from [st1] and [k], when [st1] are valid. Prove that this function outputs a valid [st2]. This would in particular prove that [Michelson] specifies a unique [st2] when [st1] and [st2] are given.

Validity predicate for [value].

Validity predicate for [kdescr]

  with kdescr : Stack_ty.t → Stack_ty.t → Script_typed_ir.kdescr → Prop :=
  | Kdescr loc bef aft instr vbef vaft :
    stack_ty.Valid.t vbef bef →
    stack_ty.Valid.t vaft aft →
    kinstr vbef vaft instr →
    kdescr vbef vaft
      {|
        Script_typed_ir.kdescr.kloc := loc;
        Script_typed_ir.kdescr.kbef := bef;
        Script_typed_ir.kdescr.kaft := aft;
        Script_typed_ir.kdescr.kinstr := instr;
      |}

Validity predicate for [lambda]

  with lambda : Stack_ty.t → Stack_ty.t → Script_typed_ir.lambda → Prop :=
  | Lam k_descr node arg ret :
    kdescr [arg] [ret] k_descr →
    lambda [arg] [ret] (Script_typed_ir.Lam k_descr node)
  | LamRec k_descr node arg ret :
    kdescr [arg ; Ty.Lambda arg ret] [ret] k_descr →
    lambda [arg ; Ty.Lambda arg ret] [ret] (Script_typed_ir.LamRec k_descr node)

  where
  "'Script_Map" :=
    (fun (k : Ty.t)
       (tyk : Script_typed_ir.ty)
       (k_cmp : ty.Comparable.t tyk)
       (k_tyk : ty.Valid.proj_rel k tyk) ⇒
       Map.Make {|
           Compare.COMPARABLE.compare :=
             Script_comparable.compare_comparable tyk; |}).

  Definition Script_Map
    (k : Ty.t)
    (tyk : Script_typed_ir.ty)
    (k_cmp : ty.Comparable.t tyk)
    (k_tyk : ty.Valid.proj_rel k tyk) : Map.S (key := Ty.to_Set k) :=
    'Script_Map k tyk k_cmp k_tyk.

Validity predicate for [typed_contract]

Validity predicate for [continuation]

Validity predicate for [Script_typed_ir.ticket], which actually uses a clone of [value.Ticket_value] above.

    Inductive t : ∀ (a : Ty.t), Script_typed_ir.ticket (Ty.to_Set a) → Prop :=
      | Ticket a ticketer amount (contents : Ty.to_Set a) :
        Valid.value a contents → Ticket_amount.Valid.t amount →
        t a
          {|
            Script_typed_ir.ticket.ticketer := ticketer;
            Script_typed_ir.ticket.contents := contents;
            Script_typed_ir.ticket.amount := amount;
          |}.
  End Valid.
End ticket.

Module Script_signature.
  Import Proto_alpha.Script_typed_ir.Script_signature.

  Lemma make_get (s : t) : make (get s) = s.
  Proof.
    now destruct s.
  Qed.

  Lemma get_make (s : Signature.t) : get (make s) = s.
  Proof.
    reflexivity.
  Qed.

  Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

  Definition canonize (s : t) : t :=
    make (Signature.canonize (get s)).

  Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) canonize compare.
  Proof.
    apply (Compare.equality (Compare.projection get Signature.compare));
      [sauto lq: on|].
    eapply Compare.implies.
    { eapply Compare.projection_is_valid.
      apply Signature.compare_is_valid.
    }
    all: unfold canonize, get; hauto l: on.
  Qed.
End Script_signature.

Module tx_rollup_l2_address.
  Module Valid.

Validity predicate for [tx_rollup_l2_address]. Note that it clones [value.Tx_rollup_l2_address_value].

    Definition t (x : Script_typed_ir.tx_rollup_l2_address) : Prop :=
      Indexable.Value.Valid.t x.
  End Valid.
End tx_rollup_l2_address.

Module Script_chain_id.
  Import Proto_alpha.Script_typed_ir.Script_chain_id.

  Lemma compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id compare.
  Proof.
    apply (Compare.equality (
      let proj '(Chain_id_tag x) := x in
      Compare.projection proj Chain_id.compare
    )); [sauto q: on|].
    eapply Compare.implies.
    { eapply Compare.projection_is_valid.
      apply Chain_id.compare_is_valid.
    }
    all: sauto q: on.
  Qed.

  Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Script_chain_id.

Module Script_timelock.
  Import Proto_alpha.Script_typed_ir.Script_timelock.

  Lemma chest_key_encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) chest_key_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve chest_key_encoding_is_valid : Data_encoding_db.

  Lemma chest_encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) chest_encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve chest_encoding_is_valid : Data_encoding_db.

End Script_timelock.

Module step_constants.
  Module Valid.

The validity of the step_constants

    Record t (sc : step_constants) : Prop := {
      amount : Tez_repr.Valid.t sc.(step_constants.amount);
      balance : Tez_repr.Valid.t sc.(step_constants.balance);
      level : Script_int.n_num.Valid.t sc.(step_constants.level);
    }.
  End Valid.
End step_constants.

Module Type_size.
  Module Valid.

Validity predicate for the type [Type_size.t].

    Definition t (x : Script_typed_ir.Type_size.t) : Prop :=
      0 ≤ x ≤ Constants_repr.michelson_maximum_type_size.
    #[global] Hint Unfold
      t
      Constants_repr.michelson_maximum_type_size
      : tezos_z.
  End Valid.

The function [of_int] is valid.

  Lemma of_int_is_valid loc_value size_value :
    Pervasives.Int.Valid.non_negative size_value →
    letP ? size := Type_size.of_int loc_value size_value in
    Valid.t size.
  Proof.
    intros H_size_value.
    unfold Type_size.of_int.
    destruct (_ ≤i _) eqn:?; simpl; [|easy].
    lia.
  Qed.

The function [compound1] is valid.

  Lemma compound1_is_valid loc_value size_value :
    Valid.t size_value →
    letP ? size := Type_size.compound1 loc_value size_value in
    Valid.t size.
  Proof.
    intros H_size_value.
    apply of_int_is_valid.
    lia.
  Qed.

The function [compound2] is valid.

  Lemma compound2_is_valid loc_value size1 size2 :
    Valid.t size1 →
    Valid.t size2 →
    letP ? size := Type_size.compound2 loc_value size1 size2 in
    Valid.t size.
  Proof.
    intros Hsize1 Hsize2.
    apply of_int_is_valid.
    lia.
  Qed.
End Type_size.

Module ty_metadata.
  Module Valid.
    Import Proto_alpha.Script_typed_ir.ty_metadata.

Validity predicate for the type [ty_metadata].

    Record t (x : Script_typed_ir.ty_metadata) : Prop := {
      size : Type_size.Valid.t x.(size);
    }.
  End Valid.
End ty_metadata.

Module ex_ty.
  Module Valid.

Validity predicate for the type [ex_ty], which: in coq-of-ocaml, is an alias of [ty]. in OCaml, is specified with: [type ex_ty = Ex_ty : ('a, _) ty -> ex_ty]

    Definition t ex_ty :=
      let 'Ex_ty ty := ex_ty in ty.Valid.t ty.
  End Valid.
End ex_ty.

The value [meta_basic] is valid.

Lemma meta_basic_is_valid : ty_metadata.Valid.t Script_typed_ir.meta_basic.
Proof.
easy.
Qed.

The function [ticket_t] is valid

Lemma ticket_t_is_valid loc_value t_value :
  ty.Comparable.t t_value → ty.Valid.t t_value →
  letP ? ty := Script_typed_ir.ticket_t loc_value t_value
  in ty.Comparable.t ty.
Proof.
Admitted.