Skip to main content

🍬 Script_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Micheline.
Require TezosOfOCaml.Environment.V8.Proofs.Utils.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Michelson_v1_primitives.

Lemma expr_encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Script_repr.expr_encoding.
  apply Micheline.canonical_encoding_is_valid.
  apply Michelson_v1_primitives.prim_encoding_is_valid.
Qed.
#[global] Hint Resolve expr_encoding_is_valid : Data_encoding_db.

Lemma location_encoding_is_valid : Data_encoding.Valid.t (fun _True) Script_repr.location_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve location_encoding_is_valid : Data_encoding_db.

Lemma lazy_expr_encoding_is_valid : Data_encoding.Valid.t (fun _True) Script_repr.lazy_expr_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve lazy_expr_encoding_is_valid : Data_encoding_db.

Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True) Script_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma deserialization_cost_estimated_from_bytes_is_valid length
  : Gas_limit_repr.Cost.Valid.t
    (Script_repr.deserialization_cost_estimated_from_bytes length).
  unfold Script_repr.deserialization_cost_estimated_from_bytes.
  apply Saturation_repr.mul_is_valid.
  { now apply Saturation_repr.Valid.decide. }
  { apply Saturation_repr.safe_int_is_valid. }
Qed.

Lemma force_decode_cost_is_valid {a : Set} (lexpr : Data_encoding.lazy_t a)
  : Gas_limit_repr.Cost.Valid.t (Script_repr.force_decode_cost lexpr).
  unfold Script_repr.force_decode_cost, Data_encoding.apply_lazy.
  destruct lexpr; try now apply Saturation_repr.Valid.decide.
  apply deserialization_cost_estimated_from_bytes_is_valid.
Qed.

A simpler implementation of [Script_repr.micheline_nodes].
Module Reference_micheline_nodes.
  Reserved Notation "'micheline_nodes_list".

  Fixpoint micheline_nodes {l} (node : Script_repr.michelson_node l) : int :=
    let micheline_nodes_list := 'micheline_nodes_list l in
    match node with
    | Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ ⇒ 1
    | Micheline.Prim _ _ subterms _ | Micheline.Seq _ subterms
      micheline_nodes_list subterms +i 1
    end

  where "'micheline_nodes_list" :=
    (fun (l : Set) ⇒ fix micheline_nodes_list
      (subterms : list (Script_repr.michelson_node l)) {struct subterms} : int :=
      match subterms with
      | [] ⇒ 0
      | cons n nodesmicheline_nodes n +i micheline_nodes_list nodes
      end).

  Definition micheline_nodes_list {l : Set} := 'micheline_nodes_list l.
End Reference_micheline_nodes.

How to unfold the continuation of [Script_repr.micheline_fold_aux].
Fixpoint micheline_fold_aux_continuation {A l : Set}
  (node : Script_repr.michelson_node l)
  (f : A Script_repr.michelson_node l A) {struct node}
  : (acc_value : A) {B : Set} (k : A B),
    Script_repr.micheline_fold_aux node f acc_value k =
    k (Script_repr.micheline_fold_aux node f acc_value id).
  assert (micheline_fold_nodes_continuation :
     (subterms : list (Script_repr.michelson_node l)) (acc_value : A)
      {B : Set} (k : A B),
    Script_repr.micheline_fold_nodes subterms f acc_value k =
    k (Script_repr.micheline_fold_nodes subterms f acc_value id)
  ).
  { induction subterms; intros; try reflexivity; simpl.
    match goal with
    | [H : _ |- _] ⇒ rewrite H
    end.
    rewrite micheline_fold_aux_continuation.
    f_equal.
    match goal with
    | [H : _ |- _ = Script_repr.micheline_fold_nodes _ _ _ ?k] ⇒
      now rewrite (H _ _ k)
    end.
  }
  { intros.
    destruct node; try reflexivity.
    all:
      simpl;
      fold (@Script_repr.micheline_fold_nodes l A B); sfirstorder.
  }
Qed.

How to unfold the continuation of [Script_repr.micheline_fold_nodes].
Fixpoint micheline_fold_nodes_continuation {A B l : Set}
  (nodes : list (Script_repr.michelson_node l))
  (f : A Script_repr.michelson_node l A)
  (acc_value : A) (k : A B) {struct nodes}
  : Script_repr.micheline_fold_nodes nodes f acc_value k =
    k (Script_repr.micheline_fold_nodes nodes f acc_value id).
  destruct nodes; try reflexivity; simpl.
  rewrite micheline_fold_nodes_continuation.
  rewrite micheline_fold_aux_continuation.
  f_equal.
  match goal with
  | [|- _ = Script_repr.micheline_fold_nodes _ _ _ ?k'] ⇒
    now rewrite micheline_fold_nodes_continuation with (k := k')
  end.
Qed.

Fixpoint micheline_nodes_like_reference_aux {l}
  (node : Script_repr.michelson_node l) acc
  : Pervasives.Int.Valid.t acc
    Script_repr.micheline_fold_aux node (fun acc '_acc +i 1) acc id =
    Reference_micheline_nodes.micheline_nodes node +i acc.
  assert (micheline_nodes_list_like_reference :
     (subterms : list (Script_repr.michelson_node l)) (acc' : int),
      Pervasives.Int.Valid.t acc'
      Script_repr.micheline_fold_nodes subterms (fun n '_n +i 1) acc' id =
      Reference_micheline_nodes.micheline_nodes_list subterms +i acc'
  ).
  { unfold Pervasives.Int.Valid.t, Pervasives.max_int, Pervasives.min_int.
    induction subterms as [|x xs IHl]; simpl; intros.
    { unfold id; Utils.tezos_z_auto. }
    { rewrite micheline_fold_nodes_continuation.
      rewrite micheline_fold_aux_continuation.
      unfold id; simpl.
      match goal with
      | [H : _ |- _] ⇒ rewrite H
      end.
      rewrite micheline_nodes_like_reference_aux.
      { Utils.tezos_z_auto. }
      { Utils.tezos_z_auto. }
      { apply H. } } }
  {
    unfold Pervasives.Int.Valid.t, Pervasives.max_int, Pervasives.min_int in micheline_nodes_list_like_reference;
    autounfold with tezos_z in micheline_nodes_list_like_reference;
    unfold Script_repr.micheline_fold_aux, "+i";
    assert (Hid : {A : Set} {x : A}, id x = x) by reflexivity;
    destruct node; autounfold with tezos_z; try rewrite Hid.

    all:
      try rewrite micheline_nodes_list_like_reference;
      try unfold Reference_micheline_nodes.micheline_nodes_list,
        Reference_micheline_nodes.micheline_nodes,
        Script_repr.michelson_node, Michelson_v1_primitives;
      try Utils.tezos_z_auto.

    all:
      unfold Reference_micheline_nodes.micheline_nodes_list,
        Reference_micheline_nodes.micheline_nodes,
        Script_repr.michelson_node;
      Utils.tezos_z_auto.
   }
Qed.

Lemma reference_micheline_nodes_micheline_nodes_is_valid : (node : Script_repr.node),
  Pervasives.Int.Valid.t (Reference_micheline_nodes.micheline_nodes node).
  unfold Script_repr.node, Script_repr.michelson_node,
    Script_repr.location, Reference_micheline_nodes.micheline_nodes.
  destruct node; Utils.tezos_z_auto.
Qed.

[Script_repr.micheline_nodes] behaves like its reference implementation.
Lemma micheline_nodes_like_reference (node : Script_repr.node)
  : Script_repr.micheline_nodes node =
    Reference_micheline_nodes.micheline_nodes node.

  unfold Script_repr.micheline_nodes, Script_repr.fold.
  rewrite micheline_nodes_like_reference_aux.
  rewrite Pervasives.Int.Valid.int_plus_0_r_eq.
  { reflexivity. }
  { apply reference_micheline_nodes_micheline_nodes_is_valid. }
  { Utils.tezos_z_auto. }
Qed.

Module Micheline_size.
  Import Script_repr.
  Import Script_repr.Micheline_size.t.

  Module Valid.
    Record t (x : Micheline_size.t) : Prop := {
      nodes : Saturation_repr.Valid.t x.(nodes);
      string_bytes : Saturation_repr.Valid.t x.(string_bytes);
      z_bytes : Saturation_repr.Valid.t x.(z_bytes);
    }.
  End Valid.

  Lemma make_is_valid : (nodes string_bytes z_bytes : Script_repr.S.t),
      Saturation_repr.Valid.t nodes
      Saturation_repr.Valid.t string_bytes
      Saturation_repr.Valid.t z_bytes
      Valid.t (Micheline_size.make nodes string_bytes z_bytes).
    intros; constructor; trivial.
  Qed.

  Lemma zero_is_valid : Valid.t Micheline_size.zero.
    constructor; constructor; simpl;
      unfold S.zero, Saturation_repr.saturated, Pervasives.max_int; lia.
  Qed.

  Lemma add_int_is_valid : acc_value n_value,
      Valid.t acc_value
      Valid.t (Micheline_size.add_int acc_value n_value).
    intros acc_value n_value [Hns Hsb Hz];
      constructor; simpl; trivial; apply Saturation_repr.add_is_valid.
  Qed.

  Lemma add_string_is_valid : acc_value n_value,
      Valid.t acc_value Valid.t (Micheline_size.add_string acc_value n_value).
    intros av nv H; destruct H; constructor; trivial;
    apply Saturation_repr.add_is_valid.
  Qed.

  Lemma add_bytes_is_valid : acc_value n_value,
      Valid.t acc_value
      Valid.t (Micheline_size.add_bytes acc_value n_value).
    intros av nv H; destruct H; constructor; trivial;
    apply Saturation_repr.add_is_valid.
  Qed.

  Lemma add_node_is_valid : s_value,
      Valid.t s_value Valid.t (Micheline_size.add_node s_value).
    intros sv H; destruct sv, H; constructor; trivial;
    apply Saturation_repr.add_is_valid.
  Qed.

  Lemma of_annots_is_valid : acc_value annots,
      Valid.t acc_value Valid.t (Micheline_size.of_annots acc_value annots).
    unfold Micheline_size.of_annots.
    intros av ans; revert av.
    induction ans;
      hauto lq: on use: add_string_is_valid.
  Qed.

  (* We disable guard checking as it is done for the OCaml translation *)
  #[bypass_check(guard=yes)]
  Fixpoint of_nodes_is_valid {A B : Set}
    (nodes : list (Micheline.node A B)) more_nodes acc {struct nodes} :
    Valid.t acc
    Valid.t (Micheline_size.of_nodes acc nodes more_nodes).
    (* We allow ourselves to only make in our proof recursive calls with
       the same arguments as in the code. Thus, if we suppose that the
       code terminates, the proof should always terminate. To do so,
       we introduce a value [H] with the same [nodes] and [more_nodes]
       parameters as what appears in the code when there is a recursive call. *)

    refine (
      match nodes with
      | []
        match more_nodes with
        | []_
        | cons nodes more_nodes
          let H := of_nodes_is_valid A B nodes more_nodes in
          _
        end
      | cons (Micheline.Int _ n_value) nodes
        let H := of_nodes_is_valid A B nodes more_nodes in
        _
      | cons (Micheline.String _ s_value) nodes
        let H := of_nodes_is_valid A B nodes more_nodes in
        _
      | cons (Micheline.Bytes _ s_value) nodes
        let H := of_nodes_is_valid A B nodes more_nodes in
        _
      | cons (Micheline.Prim _ _ args annots) nodes
        let H := of_nodes_is_valid A B args (cons nodes more_nodes) in
        _
      | cons (Micheline.Seq _ args) nodes
        let H := of_nodes_is_valid A B args (cons nodes more_nodes) in
        _
      end
    );
      (* We clear [of_nodes_is_valid] from the proof context so that
         we cannot call it by mistake. *)

      try (assert (H_ind := H); clear H); clear of_nodes_is_valid.

    (* There we do our proof as usual. *)
    all:
      intros; simpl; trivial; apply H_ind; trivial;
      try apply add_int_is_valid;
      try apply add_string_is_valid;
      try apply add_bytes_is_valid;
      try apply of_annots_is_valid;
      try apply add_node_is_valid;
      trivial.
  Qed.

  Lemma of_node_is_valid : {A B} node_value,
      Valid.t (@Micheline_size.of_node A B node_value).
    intros A B nv; apply of_nodes_is_valid, zero_is_valid.
  Qed.

  Lemma dot_product_is_valid : s1 s2,
      Valid.t s1 Valid.t s2
      Proofs.Saturation_repr.Valid.t (Micheline_size.dot_product s1 s2).
    intros s1 s2 H1 H2; unfold Micheline_size.dot_product;
    apply Saturation_repr.add_is_valid.
  Qed.
End Micheline_size.

Module Micheline_decoding.
  Import Micheline_size.
  Import Script_repr.

  Lemma micheline_size_dependent_cost_is_valid :
    Valid.t Micheline_decoding.micheline_size_dependent_cost.
    apply make_is_valid; apply Saturation_repr.safe_int_is_valid.
  Qed.
End Micheline_decoding.

Module Micheline_encoding.
  Import Micheline_size.
  Import Script_repr.

  Lemma micheline_size_dependent_cost_is_valid :
    Valid.t Micheline_encoding.micheline_size_dependent_cost.
    apply make_is_valid; apply Saturation_repr.safe_int_is_valid.
  Qed.
End Micheline_encoding.

Lemma serialization_cost_is_valid :
   size_value : Script_repr.Micheline_size.t,
    Micheline_size.Valid.t size_value
    Gas_limit_repr.Cost.Valid.t (Script_repr.serialization_cost size_value).
  intros sv H; unfold Script_repr.serialization_cost;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        Micheline_size.dot_product_is_valid; [assumption|];
  apply Micheline_encoding.micheline_size_dependent_cost_is_valid.
Qed.

Lemma deserialization_cost_is_valid :
   size_value,
    Micheline_size.Valid.t size_value
    Gas_limit_repr.Cost.Valid.t (Script_repr.deserialization_cost size_value).
  intros sv H; unfold Script_repr.deserialization_cost;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        Micheline_size.dot_product_is_valid; [assumption|];
  apply Micheline_decoding.micheline_size_dependent_cost_is_valid.
Qed.

Lemma serialization_cost_estimated_from_bytes_is_valid :
   bytes_len,
    Gas_limit_repr.Cost.Valid.t
      (Script_repr.serialization_cost_estimated_from_bytes bytes_len).
  intro bl; unfold Script_repr.serialization_cost_estimated_from_bytes;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        Saturation_repr.mul_is_valid;
  apply Saturation_repr.safe_int_is_valid.
Qed.

Lemma cost_micheline_strip_locations_is_valid :
   size_value,
    Gas_limit_repr.Cost.Valid.t
      (Script_repr.cost_micheline_strip_locations size_value).
  intro sv; unfold Script_repr.cost_micheline_strip_locations;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        Saturation_repr.mul_is_valid;
  apply Saturation_repr.safe_int_is_valid.
Qed.

Lemma cost_micheline_strip_annotations_is_valid :
   size_value,
    Gas_limit_repr.Cost.Valid.t
      (Script_repr.cost_micheline_strip_annotations size_value).
  intro sv; unfold Script_repr.cost_micheline_strip_annotations;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        Saturation_repr.mul_is_valid;
  apply Saturation_repr.safe_int_is_valid.
Qed.

Lemma bytes_node_cost_is_valid :
   s_value,
    Gas_limit_repr.Cost.Valid.t (Script_repr.bytes_node_cost s_value).
  intro sv; unfold Script_repr.bytes_node_cost;
  apply serialization_cost_estimated_from_bytes_is_valid.
Qed.

Lemma deserialized_cost_is_valid :
   {A} (expr : Micheline.canonical A),
    Gas_limit_repr.Cost.Valid.t (Script_repr.deserialized_cost expr).
  intros A expr; unfold Script_repr.deserialized_cost;
  apply Gas_limit_repr.atomic_step_cost_is_valid,
        deserialization_cost_is_valid,
        Micheline_size.of_node_is_valid.
Qed.

Lemma stable_force_decode_cost_is_valid :
   lexpr,
    Gas_limit_repr.Cost.Valid.t (Script_repr.stable_force_decode_cost lexpr).
  intro lexpr; unfold Script_repr.stable_force_decode_cost;
  destruct (apply_lazy _);
  apply deserialization_cost_estimated_from_bytes_is_valid.
Qed.

Lemma force_bytes_cost_is_valid :
   {A} (expr : Data_encoding.lazy_t (Micheline.canonical A)),
    Gas_limit_repr.Cost.Valid.t (Script_repr.force_bytes_cost expr).
  intros A expr; unfold Script_repr.force_bytes_cost, apply_lazy;
  destruct expr; [apply Gas_limit_repr.free_is_valid..|];
  apply serialization_cost_is_valid, Micheline_size.of_node_is_valid.
Qed.

Unit parameter


Axiom is_unit_parameter_implies_eq : parameter,
  Script_repr.is_unit_parameter parameter = true
  parameter = Script_repr.unit_parameter.

Fixpoint nodes_eq_string_annotations_aux (node : Script_repr.node) :
  Reference_micheline_nodes.micheline_nodes node =
  Reference_micheline_nodes.micheline_nodes (Script_repr.strip_annotations node).
  destruct node; try reflexivity; simpl;
    fold (Reference_micheline_nodes.micheline_nodes_list
      (l := Script_repr.location)) in *;
    match goal with
    | l : list _ |- _induction l
    end;
    try reflexivity; simpl;
    repeat rewrite Pervasives.int_add_assoc;
    congruence.
Qed.

Lemma nodes_eq_string_annotations (node : Script_repr.node) :
  Script_repr.micheline_nodes node =
  Script_repr.micheline_nodes (Script_repr.strip_annotations node).
  repeat rewrite micheline_nodes_like_reference.
  apply nodes_eq_string_annotations_aux.
Qed.

The function [strip_locations_cost] is valid. Currently no pre-condition on [n]
Lemma strip_locations_cost_is_valid {A B : Set} node :
  Saturation_repr.Valid.t (Script_repr.strip_locations_cost
    (A := A) (B:=B) node).
Proof.
Admitted.

The function [strip_annotations_cost] is valid.
Lemma strip_annotations_cost_is_valid {A B : Set} node :
  Saturation_repr.Valid.t (Script_repr.strip_annotations_cost
    (A := A) (B:=B) node).
Proof.
Admitted.