🎫 Ticket_hash_builder.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_builder.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_repr.

The function [hash_bytes_cost] is valid.

Lemma hash_bytes_cost_is_valid bytes_value :
  Saturation_repr.Valid.t (Ticket_hash_builder.hash_bytes_cost bytes_value).
Proof.
  unfold Ticket_hash_builder.hash_bytes_cost.
  apply Gas_limit_repr.atomic_step_cost_is_valid.
  apply Saturation_repr.add_is_valid.
Qed.

The function [hash_of_node] is valid.

Lemma hash_of_node_is_valid {A : Set} ctxt node_value :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    Ticket_hash_builder.hash_of_node (A := A)ctxt node_value in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt.
  unfold Ticket_hash_builder.hash_of_node.
  eapply Error.split_letP. {
    apply Raw_context.consume_gas_is_valid; try assumption.
    apply Script_repr.strip_locations_cost_is_valid.
  }
  clear ctxt H_ctxt; intros ctxt H_ctxt.
  destruct Data_encoding.Binary.to_bytes_opt; simpl; [|easy].
  eapply Error.split_letP. {
    apply Raw_context.consume_gas_is_valid; try assumption.
    apply hash_bytes_cost_is_valid.
  }
  clear ctxt H_ctxt; intros ctxt H_ctxt.
  trivial.
Qed.

The function [hash_of_node_uncarbonated] is valid.

Lemma hash_of_node_uncarbonated_is_valid {A : Set} node_value :
  letP? _ :=
    Ticket_hash_builder.hash_of_node_uncarbonated (A := A) node_value in
  True.
Proof.
  unfold Ticket_hash_builder.hash_of_node_uncarbonated.
  now destruct Data_encoding.Binary.to_bytes_opt.
Qed.

The function [make] is valid.

Lemma make_is_valid ctxt ticketer ty_value contents owner :
  Raw_context.Valid.t ctxt →
  letP? '(_, ctxt) :=
    Ticket_hash_builder.make ctxt ticketer ty_value contents owner in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt.
  unfold Ticket_hash_builder.make.
  now apply hash_of_node_is_valid.
Qed.

The function [make_uncarbonated] is valid.

Lemma make_uncarbonated_is_valid ticketer ty_value contents owner :
  letP? _ :=
    Ticket_hash_builder.make_uncarbonated ticketer ty_value contents owner in
  True.
Proof.
  unfold Ticket_hash_builder.make_uncarbonated.
  apply hash_of_node_uncarbonated_is_valid.
Qed.