🎫 Ticket_costs.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.

Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Script_family.

Module Constants.

The value [cost_collect_tickets_step] is valid.

  Lemma cost_collect_tickets_step_is_valid :
    Saturation_repr.Valid.t
      Ticket_costs.Constants.cost_collect_tickets_step.
  Proof.
    easy.
  Qed.

The function [cost_has_tickets_of_ty] is valid.

  Lemma cost_has_tickets_of_ty_is_valid type_size :
    Saturation_repr.Valid.t (
      Ticket_costs.Constants.cost_has_tickets_of_ty type_size
    ).
  Proof.
    unfold Ticket_costs.Constants.cost_has_tickets_of_ty.
    apply Saturation_repr.add_is_valid.
  Qed.

The value [cost_compare_ticket_hash] is valid.

  Lemma cost_compare_ticket_hash_is_valid :
    Saturation_repr.Valid.t Ticket_costs.Constants.cost_compare_ticket_hash.
  Proof.
    easy.
  Qed.

The value [cost_compare_key_contract] is valid.

  Lemma cost_compare_key_contract_is_valid :
    Saturation_repr.Valid.t Ticket_costs.Constants.cost_compare_key_contract.
  Proof.
    easy.
  Qed.
End Constants.

The function [consume_gas_steps] is valid.

Lemma consume_gas_steps_is_valid ctxt step_cost num_steps :
  Raw_context.Valid.t ctxt →
  Saturation_repr.Valid.t step_cost →
  letP? ctxt := Ticket_costs.consume_gas_steps ctxt step_cost num_steps in
  Raw_context.Valid.t ctxt.
Proof.
  intros H_ctxt H_step_cost.
  unfold Ticket_costs.consume_gas_steps.
  destruct (_ ≤i _); simpl; [easy|].
  apply Raw_context.consume_gas_is_valid; try assumption.
  apply Gas_limit_repr.atomic_step_cost_is_valid.
  apply Saturation_repr.mul_is_valid; try assumption.
  apply Saturation_repr.safe_int_is_valid.
Qed.

The function [has_tickets_of_ty_cost] is valid.

Lemma has_tickets_of_ty_cost_is_valid (ty : Script_typed_ir.ty) :
  Saturation_repr.Valid.t
    (Ticket_costs.has_tickets_of_ty_cost ty).
Proof.

@TODO : prove the lemma. Old proof with simulations.

  (* unfold Ticket_costs.has_tickets_of_ty_cost.
  apply Constants.cost_has_tickets_of_ty_is_valid. *)
Admitted.

The function [negate_cost] is valid.

Lemma negate_cost_is_valid z_value :
  Saturation_repr.Valid.t (Ticket_costs.negate_cost z_value).
Proof.
  unfold Ticket_costs.negate_cost.
  apply Saturation_repr.add_is_valid.
Qed.

The function [add_int_cost] is valid.

Lemma add_int_cost_is_valid x y :
  Saturation_repr.Valid.t (Ticket_costs.add_int_cost x y).
Proof.
  apply Saturation_repr.add_is_valid.
Qed.

The function [add_z_cost] is valid.

Lemma add_z_cost_is_valid x y :
  Saturation_repr.Valid.t (Ticket_costs.add_z_cost x y).
Proof.
  apply Saturation_repr.add_is_valid.
Qed.