🎫 Ticket_costs.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Module S := Saturation_repr.

Module Constants.
  Definition cost_collect_tickets_step : S.t := S.safe_int 80.

  Definition cost_has_tickets_of_ty (type_size : S.t) : S.t :=
    S.add (S.safe_int 10) (S.mul (S.safe_int 6) type_size).

  Definition cost_compare_ticket_hash : S.t := S.safe_int 10.

  Definition cost_compare_key_contract : S.t := S.safe_int 10.
End Constants.

Definition consume_gas_steps
  (ctxt : Alpha_context.context) (step_cost : S.t) (num_steps : int)
  : M? Alpha_context.context :=
  let op_star := S.mul in
  if num_steps ≤i 0 then
    Pervasives.Ok ctxt
  else
    let gas :=
      Alpha_context.Gas.atomic_step_cost
        (op_star step_cost (Saturation_repr.safe_int num_steps)) in
    Alpha_context.Gas.consume ctxt gas.

Definition has_tickets_of_ty_cost (ty_value : Script_typed_ir.ty) : S.t :=
  Constants.cost_has_tickets_of_ty
    (Script_typed_ir.Type_size.to_int (Script_typed_ir.ty_size ty_value)).

Reusing the gas model from [Michelson_v1_gas.Cost_of.neg] Approximating 0.066076 x term

Definition negate_cost (z_value : Z.t) : Alpha_context.Gas.cost :=
  let size_value := (7 +i (Z.numbits z_value)) /i 8 in
  Alpha_context.Gas.op_plusat (S.safe_int 25)
    (S.shift_right (S.safe_int size_value) 4).

Reusing the gas model from [Michelson_v1_gas.Cost_of.add]

Definition add_int_cost
  : Script_int.num → Script_int.num → Alpha_context.Gas.cost :=
  Michelson_v1_gas.Cost_of.Interpreter.add_int.

Reusing the gas model from [Michelson_v1_gas.Cost_of.add]

Definition add_z_cost (z1 : Z.t) (z2 : Z.t) : Alpha_context.Gas.cost :=
  add_int_cost (Script_int.of_zint z1) (Script_int.of_zint z2).