Skip to main content

🎫 Ticket_balance_migration_for_j.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.

Definition add_ticket_balance
  (contract : Alpha_context.Destination.t) (ctxt : Alpha_context.context)
  (ticket : Ticket_scanner.ex_ticket) : M? (Z.t × Alpha_context.context) :=
  let '(token, amount) := Ticket_token.token_and_amount_of_ex_ticket ticket in
  let? '(hash_value, ctxt) := Ticket_balance_key.of_ex_token ctxt contract token
    in
  Alpha_context.Ticket_balance.adjust_balance ctxt hash_value
    (Alpha_context.Script_int.to_zint amount).

Definition update_contract_tickets
  (ctxt : Alpha_context.context) (contract : Alpha_context.Contract.contract)
  : M? (Z.t × Alpha_context.context) :=
  let? '(ctxt, script) := Alpha_context.Contract.get_script ctxt contract in
  match script with
  | Nonereturn? (Z.zero, ctxt)
  | Some script
    let? '(ex_script, ctxt) :=
      Script_ir_translator.parse_script None ctxt true true script in
    let
      'Script_ir_translator.Ex_script
        (Script_typed_ir.Script {|
          Script_typed_ir.script.Script.storage := storage_value;
            Script_typed_ir.script.Script.storage_type := storage_type
            |}) := ex_script in
    let? '(has_tickets_value, ctxt) :=
      Ticket_scanner.type_has_tickets ctxt storage_type in
    let? '(tickets, ctxt) :=
      Ticket_scanner.tickets_of_value ctxt true has_tickets_value storage_value
      in
    List.fold_left_es
      (fun (function_parameter : Z.t × Alpha_context.context) ⇒
        let '(acc_size, ctxt) := function_parameter in
        fun (t_value : Ticket_scanner.ex_ticket) ⇒
          let? '(added_size, ctxt) :=
            add_ticket_balance (Alpha_context.Destination.Contract contract)
              ctxt t_value in
          return? ((acc_size +Z added_size), ctxt)) (Z.zero, ctxt) tickets
  end.

Definition is_originated (contract : Alpha_context.Contract.contract) : bool :=
  match Alpha_context.Contract.is_originated contract with
  | Some _true
  | _false
  end.

Definition init_value (ctxt : Alpha_context.context)
  : M? Alpha_context.context :=
  let contracts := Alpha_context.Contract.list_value ctxt in
  let contracts := List.filter is_originated contracts in
  let? '(added_size, ctxt) :=
    List.fold_left_es
      (fun (function_parameter : Z.t × Alpha_context.context) ⇒
        let '(acc_size, ctxt) := function_parameter in
        fun (t_value : Alpha_context.Contract.contract) ⇒
          let? '(added_size, ctxt) := update_contract_tickets ctxt t_value in
          return? ((added_size +Z acc_size), ctxt)) (Z.zero, ctxt) contracts in
  let? '(_sponsored_storage, ctxt) :=
    Alpha_context.Ticket_balance.adjust_storage_space ctxt added_size in
  return? ctxt.