Skip to main content

🎫 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.
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.
The function [make] is valid.
The function [make_uncarbonated] is valid.