🎫 Ticket_lazy_storage_diff.v

Translated OCaml

File generated by coq-of-ocaml

Init function; without side-effects in Coq

Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "Failed_to_load_big_map_value_type" "Failed to load big-map value type"
    "Failed to load big-map value type when computing ticket diffs."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (big_map_id : Alpha_context.Big_map.Id.t) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Failed to load big-map value type for big-map-id: '"
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "'" % char
                    CamlinternalFormatBasics.End_of_format)))
              "Failed to load big-map value type for big-map-id: '%a'")
            Z.pp_print (Alpha_context.Big_map.Id.unparse_to_z big_map_id)))
    (Data_encoding.obj1
      (Data_encoding.req None None "big_map_id"
        Alpha_context.Big_map.Id.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Failed_to_load_big_map_value_type" then
          let big_map_id := cast Alpha_context.Big_map.Id.t payload in
          Some big_map_id
        else None
      end)
    (fun (big_map_id : Alpha_context.Big_map.Id.t) ⇒
      Build_extensible "Failed_to_load_big_map_value_type"
        Alpha_context.Big_map.Id.t big_map_id).

Extracts the ticket-token and amount from an ex_ticket value.

Definition token_and_amount
  (ctxt : Alpha_context.context) (ex_ticket : Ticket_scanner.ex_ticket)
  : M ? ((Ticket_token.ex_token × Z.t) × Alpha_context.context ) :=
  let ? ctxt :=
    Alpha_context.Gas.consume ctxt
      Ticket_costs.Constants.cost_collect_tickets_step in
  let '(token, amount) :=
    Ticket_scanner.ex_token_and_amount_of_ex_ticket ex_ticket in
  return ? ((token, (Script_int.to_zint amount)), ctxt).

Extracts the ticket-token and amount from an ex_ticket value and returns the opposite of the amount. This is used to account for removal of tickets inside big maps when either a ticket is taken out of a big map or a whole big map is dropped.

Definition neg_token_and_amount
  (ctxt : Alpha_context.context) (ex_ticket : Ticket_scanner.ex_ticket)
  : M ? ((Ticket_token.ex_token × Z.t) × Alpha_context.context ) :=
  let ? '((token , amount ), ctxt ) := token_and_amount ctxt ex_ticket in
  let ? ctxt := Alpha_context.Gas.consume ctxt (Ticket_costs.negate_cost amount)
    in
  return ? ((token, (Z.neg amount)), ctxt).

Definition parse_value_type
  (ctxt : Alpha_context.context)
  (value_type : Micheline.canonical Alpha_context.Script.prim)
  : M ? (Script_typed_ir.ex_ty × Alpha_context.context ) :=
  Script_ir_translator.parse_big_map_value_ty ctxt true
    (Micheline.root_value value_type).

Collects all ticket-token balances contained in the given node and prepends them to the accumulator [acc]. The given [get_token_and_amount] function extracts the ticket-token and amount (either positive or negative) from an [ex_ticket] value, depending on whether the diff stems from adding or removing a value containing tickets.

Definition collect_token_diffs_of_node {a : Set} {A : Set}
  (ctxt : Alpha_context.context)
  (has_tickets_value : Ticket_scanner.has_tickets)
  (node_value : Micheline.canonical Alpha_context.Script.prim)
  (get_token_and_amount :
    Alpha_context.context → Ticket_scanner.ex_ticket →
    M ? (A × Alpha_context.context )) (acc_value : list A)
  : M ? (list A × Alpha_context.context ) :=
  let ? '(ex_tickets , ctxt ) :=
    (Ticket_scanner.tickets_of_node (a := a)) ctxt true has_tickets_value
      (Micheline.root_value node_value) in
  Error_monad.op_gtgtquestioneq
    (List.fold_left_e
      (fun (function_parameter : list A × Alpha_context.context) ⇒
        let '(acc_value, ctxt) := function_parameter in
        fun (ticket : Ticket_scanner.ex_ticket) ⇒
          let ? '(item , ctxt ) := get_token_and_amount ctxt ticket in
          return ? ((cons item acc_value), ctxt)) (acc_value, ctxt) ex_tickets)
    Error_monad._return.

Definition Key_hash_map :=
  Carbonated_map.Make
    (let context : Set := Alpha_context.context in
    let consume := Alpha_context.Gas.consume in
    {|
      Carbonated_map.GAS.consume := consume
    |})
    (let t : Set := Script_expr_hash.t in
    let compare := Script_expr_hash.compare in
    let compare_cost {A : Set} (function_parameter : A)
      : Alpha_context.Gas.cost :=
      let '_ := function_parameter in
      Ticket_costs.Constants.cost_compare_ticket_hash in
    {|
      Carbonated_map.COMPARABLE.compare := compare;
      Carbonated_map.COMPARABLE.compare_cost := compare_cost
    |}).

Collects all ticket-token diffs from a big-map update and prepends them to the accumulator [acc].

Definition collect_token_diffs_of_big_map_update {a : Set}
  (ctxt : Alpha_context.t) (big_map_id : Alpha_context.Big_map.Id.t)
  (has_tickets_value : Ticket_scanner.has_tickets)
  (function_parameter : Lazy_storage_kind.Big_map.update)
  : Key_hash_map.(Carbonated_map.S.t) (option Script_repr.expr) →
  list (Ticket_token.ex_token × Z.t) →
  M ?
    (list (Ticket_token.ex_token × Z.t) ×
      Key_hash_map.(Carbonated_map.S.t) (option Script_repr.expr) ×
      Alpha_context.context ) :=
  let '{|
    Lazy_storage_kind.Big_map.update.key := _;
      Lazy_storage_kind.Big_map.update.key_hash := key_hash;
      Lazy_storage_kind.Big_map.update.value := value_value
      |} := function_parameter in
  fun (already_updated :
    Key_hash_map.(Carbonated_map.S.t) (option Script_repr.expr)) ⇒
    fun (acc_value : list (Ticket_token.ex_token × Z.t)) ⇒
      let collect_token_diffs_of_node_option {A : Set}
        (ctxt : Alpha_context.context)
        (get_token_and_amount :
          Alpha_context.context → Ticket_scanner.ex_ticket →
          M ? (A × Alpha_context.context ))
        (expr_opt : option (Micheline.canonical Alpha_context.Script.prim))
        (acc_value : list A) : M ? (list A × Alpha_context.context ) :=
        match expr_opt with
        | Some expr ⇒
          (collect_token_diffs_of_node (a := a)) ctxt has_tickets_value expr
            get_token_and_amount acc_value
        | None ⇒ return ? (acc_value, ctxt)
        end in
      let ? '(old_value , ctxt ) :=
        let ? '(val_opt , ctxt ) :=
          Key_hash_map.(Carbonated_map.S.find) ctxt key_hash already_updated in
        match val_opt with
        | Some updated_value ⇒ return ? (updated_value, ctxt)
        | None ⇒
          let ? '(ctxt , old_value ) :=
            Alpha_context.Big_map.get_opt ctxt big_map_id key_hash in
          return ? (old_value, ctxt)
        end in
      let ? '(acc_value , ctxt ) :=
        collect_token_diffs_of_node_option ctxt neg_token_and_amount old_value
          acc_value in
      let ? '(already_updated , ctxt ) :=
        Key_hash_map.(Carbonated_map.S.update) ctxt key_hash
          (fun (ctxt : Alpha_context.t) ⇒
            fun (function_parameter : option (option Script_repr.expr)) ⇒
              let '_ := function_parameter in
              return ? ((Some value_value), ctxt)) already_updated in
      let ? '(tickets , ctxt ) :=
        collect_token_diffs_of_node_option ctxt token_and_amount value_value
          acc_value in
      return ? (tickets, already_updated, ctxt).

Collects all ticket-token diffs from a list of big-map updates and prepends them to the accumulator [acc].

Definition collect_token_diffs_of_big_map_updates
  (ctxt : Alpha_context.context) (big_map_id : Alpha_context.Big_map.Id.t)
  (value_type : Micheline.canonical Alpha_context.Script.prim)
  (updates : list Lazy_storage_kind.Big_map.update)
  (acc_value : list (Ticket_token.ex_token × Z.t))
  : M ? (list (Ticket_token.ex_token × Z.t) × Alpha_context.t ) :=
  let ? '(Script_typed_ir.Ex_ty value_type , ctxt ) :=
    parse_value_type ctxt value_type in
  let 'existT _ __Ex_ty_'a [ctxt, value_type] :=
    cast_exists (Es := Set)
      (fun __Ex_ty_'a ⇒ [Alpha_context.context ** Script_typed_ir.ty])
      [ctxt, value_type] in
  let ? '(has_tickets_value , ctxt ) :=
    Ticket_scanner.type_has_tickets ctxt value_type in
  let ? '(acc_value , _already_updated , ctxt ) :=
    List.fold_left_es
      (fun (function_parameter :
        list (Ticket_token.ex_token × Z.t) ×
          Key_hash_map.(Carbonated_map.S.t) (option Script_repr.expr) ×
          Alpha_context.t) ⇒
        let '(acc_value, already_updated, ctxt) := function_parameter in
        fun (update : Lazy_storage_kind.Big_map.update) ⇒
          (collect_token_diffs_of_big_map_update (a := __Ex_ty_'a)) ctxt
            big_map_id has_tickets_value update already_updated acc_value)
      (acc_value, Key_hash_map.(Carbonated_map.S.empty), ctxt) updates in
  return ? (acc_value, ctxt).

Given a big-map id, this function collects ticket-token diffs and prepends them to the accumulator [acc].

Definition collect_token_diffs_of_big_map {A : Set}
  (ctxt : Alpha_context.context)
  (get_token_and_amount :
    Alpha_context.context → Ticket_scanner.ex_ticket →
    M ? (A × Alpha_context.context )) (big_map_id : Alpha_context.Big_map.Id.t)
  (acc_value : list A) : M ? (list A × Alpha_context.context ) :=
  let ? ctxt :=
    Alpha_context.Gas.consume ctxt
      Ticket_costs.Constants.cost_collect_tickets_step in
  let ? '(ctxt , key_val_tys ) := Alpha_context.Big_map._exists ctxt big_map_id in
  match key_val_tys with
  | Some (_key_ty, value_ty) ⇒
    let ? '(Script_typed_ir.Ex_ty value_type , ctxt ) :=
      parse_value_type ctxt value_ty in
    let 'existT _ __Ex_ty_'a [ctxt, value_type] :=
      cast_exists (Es := Set)
        (fun __Ex_ty_'a ⇒ [Alpha_context.context ** Script_typed_ir.ty])
        [ctxt, value_type] in
    let ? '(has_tickets_value , ctxt ) :=
      Ticket_scanner.type_has_tickets ctxt value_type in
    let ? '(ctxt , exprs ) :=
      Alpha_context.Big_map.list_key_values None None ctxt big_map_id in
    List.fold_left_es
      (fun (function_parameter : list A × Alpha_context.context) ⇒
        let '(acc_value, ctxt) := function_parameter in
        fun (function_parameter :
          Script_expr_hash.t × Micheline.canonical Alpha_context.Script.prim) ⇒
          let '(_key_hash, node_value) := function_parameter in
          (collect_token_diffs_of_node (a := __Ex_ty_'a)) ctxt has_tickets_value
            node_value get_token_and_amount acc_value) (acc_value, ctxt) exprs
  | None ⇒
    Error_monad.tzfail
      (Build_extensible "Failed_to_load_big_map_value_type"
        Alpha_context.Big_map.Id.t big_map_id)
  end.

Collects ticket-token diffs from a big-map and a list of updates, and prepends them to the given accumulator [acc].

Definition collect_token_diffs_of_big_map_and_updates
  (ctxt : Alpha_context.context) (big_map_id : Alpha_context.Big_map.Id.t)
  (updates : list Lazy_storage_kind.Big_map.update)
  (acc_value : list (Ticket_token.ex_token × Z.t))
  : M ? (list (Ticket_token.ex_token × Z.t) × Alpha_context.t ) :=
  let ? ctxt :=
    Alpha_context.Gas.consume ctxt
      Ticket_costs.Constants.cost_collect_tickets_step in
  let ? '(ctxt , key_val_opt ) := Alpha_context.Big_map._exists ctxt big_map_id in
  match key_val_opt with
  | Some (_val, value_type) ⇒
    collect_token_diffs_of_big_map_updates ctxt big_map_id value_type updates
      acc_value
  | None ⇒
    Error_monad.tzfail
      (Build_extensible "Failed_to_load_big_map_value_type"
        Alpha_context.Big_map.Id.t big_map_id)
  end.

Inspects the given [Lazy_storage.diffs_item] and prepends all ticket-token diffs, resulting from the updates, to the given accumulator [acc].