🎫 Ticket_storage.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.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Ticket_hash_repr.

Module Negative_ticket_balance.
  Record record : Set := Build {
    key : Ticket_hash_repr.t;
    balance : Z.t;
  }.
  Definition with_key key (r : record) :=
    Build key r.(balance).
  Definition with_balance balance (r : record) :=
    Build r.(key) balance.
End Negative_ticket_balance.
Definition Negative_ticket_balance := Negative_ticket_balance.record.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Negative_ticket_balance" "Negative ticket balance"
      "Attempted to set a negative ticket balance value"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Ticket_hash_repr.t × Z.t) ⇒
            let '(key_value, balance) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Attempted to set negative ticket balance value '"
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal "' for key "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.Char_literal "." % char
                          CamlinternalFormatBasics.End_of_format)))))
                "Attempted to set negative ticket balance value '%a' for key %a.")
              Z.pp_print balance Ticket_hash_repr.pp key_value))
      (Data_encoding.obj2
        (Data_encoding.req None None "key" Ticket_hash_repr.encoding)
        (Data_encoding.req None None "balance" Data_encoding.z_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Negative_ticket_balance" then
            let '{|
              Negative_ticket_balance.key := key_value;
                Negative_ticket_balance.balance := balance
                |} := cast Negative_ticket_balance payload in
            Some (key_value, balance)
          else None
        end)
      (fun (function_parameter : Ticket_hash_repr.t × Z.t) ⇒
        let '(key_value, balance) := function_parameter in
        Build_extensible "Negative_ticket_balance" Negative_ticket_balance
          {| Negative_ticket_balance.key := key_value;
            Negative_ticket_balance.balance := balance; |}) in
  Error_monad.register_error_kind Error_monad.Permanent "Used_storage_underflow"
    "Ticket balance used storage underflow"
    "Attempt to free more bytes than allocated for the tickets balance" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Used_storage_space_underflow" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Used_storage_space_underflow" unit tt).

Definition get_balance (ctxt : Raw_context.t) (key_value : Ticket_hash_repr.t)
  : M? (option Z.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Storage.Ticket_balance.Table.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt key_value in
  return? (res, ctxt).

Definition set_balance
  (ctxt : Raw_context.t) (key_value : Ticket_hash_repr.t) (balance : Z.t)
  : M? (Z.t × Raw_context.t) :=
  let cost_of_key := Z.of_int 65 in
  let? '_ :=
    Error_monad.fail_when (balance <Z Z.zero)
      (Build_extensible "Negative_ticket_balance" Negative_ticket_balance
        {| Negative_ticket_balance.key := key_value;
          Negative_ticket_balance.balance := balance; |}) in
  if balance =Z Z.zero then
    let? '(ctxt, freed, existed) :=
      Storage.Ticket_balance.Table.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        ctxt key_value in
    let freed :=
      if existed then
        Z.neg (cost_of_key +Z (Z.of_int freed))
      else
        Z.zero in
    return? (freed, ctxt)
  else
    let? '(ctxt, size_diff, existed) :=
      Storage.Ticket_balance.Table.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
        ctxt key_value balance in
    let size_diff :=
      let z_diff := Z.of_int size_diff in
      if existed then
        z_diff
      else
        cost_of_key +Z z_diff in
    return? (size_diff, ctxt).

Definition adjust_balance
  (ctxt : Raw_context.t) (key_value : Ticket_hash_repr.t) (delta : Z.t)
  : M? (Z.t × Raw_context.t) :=
  let? '(res, ctxt) := get_balance ctxt key_value in
  let old_balance := Option.value_value res Z.zero in
  set_balance ctxt key_value (old_balance +Z delta).

Definition adjust_storage_space (ctxt : Raw_context.t) (storage_diff : Z.t)
  : M? (Z.t × Raw_context.t) :=
  if storage_diff =Z Z.zero then
    return? (Z.zero, ctxt)
  else
    let? used_storage :=
      Storage.Ticket_balance.Used_storage_space.(Storage_sigs.Single_data_storage.find)
        ctxt in
    let used_storage := Option.value_value used_storage Z.zero in
    let? paid_storage :=
      Storage.Ticket_balance.Paid_storage_space.(Storage_sigs.Single_data_storage.find)
        ctxt in
    let paid_storage := Option.value_value paid_storage Z.zero in
    let new_used_storage := used_storage +Z storage_diff in
    let? '_ :=
      Error_monad.error_when (new_used_storage <Z Z.zero)
        (Build_extensible "Used_storage_space_underflow" unit tt) in
    let ctxt :=
      Storage.Ticket_balance.Used_storage_space.(Storage_sigs.Single_data_storage.add)
        ctxt new_used_storage in
    let diff_value := new_used_storage -Z paid_storage in
    if Z.zero <Z diff_value then
      let ctxt :=
        Storage.Ticket_balance.Paid_storage_space.(Storage_sigs.Single_data_storage.add)
          ctxt new_used_storage in
      return? (diff_value, ctxt)
    else
      return? (Z.zero, ctxt).