Skip to main content

🎫 Ticket_lazy_storage_diff.v

Translated OCaml

Gitlab , 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.
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.
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.
A module for keeping track of script-key-hashes. It's used for looking up keys for multiple big-map updates referencing the same key.
Definition Key_hash_map :=
  Carbonated_map.Make
    (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.context) (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
        | Nonereturn? (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_valuereturn? (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.context) ⇒
            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.context) :=
  let? '(Script_ir_translator.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.context) ⇒
        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_ir_translator.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_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 (node_value : Micheline.canonical Alpha_context.Script.prim) ⇒
          (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.fail
      (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].
Inspects the given [Lazy_storage.diffs_item] and prepends all ticket-token diffs, resulting from the updates, to the given accumulator [acc].
Definition collect_token_diffs_of_big_map_diff
  (ctxt : Alpha_context.context)
  (diff_item : Alpha_context.Lazy_storage.diffs_item)
  (acc_value : list (Ticket_token.ex_token × Z.t))
  : M? (list (Ticket_token.ex_token × Z.t) × Alpha_context.context) :=
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      Ticket_costs.Constants.cost_collect_tickets_step in
  match diff_item with
  |
    Alpha_context.Lazy_storage.Item Lazy_storage_kind.Big_map big_map_id
      Alpha_context.Lazy_storage.Remove
    let big_map_id := cast Alpha_context.Big_map.Id.t big_map_id in
    collect_token_diffs_of_big_map ctxt neg_token_and_amount big_map_id
      acc_value
  |
    Alpha_context.Lazy_storage.Item Lazy_storage_kind.Big_map big_map_id
      (Alpha_context.Lazy_storage.Update {|
        Alpha_context.Lazy_storage.diff.Update.init := init_value;
          Alpha_context.Lazy_storage.diff.Update.updates := updates
          |}) ⇒
    let '[updates, init_value, big_map_id] :=
      cast
        [Lazy_storage_kind.Big_map.updates **
          Alpha_context.Lazy_storage.init Alpha_context.Big_map.Id.t
            Lazy_storage_kind.Big_map.alloc ** Alpha_context.Big_map.Id.t]
        [updates, init_value, big_map_id] in
    match init_value with
    | Alpha_context.Lazy_storage.Existing
      collect_token_diffs_of_big_map_and_updates ctxt big_map_id updates
        acc_value
    |
      Alpha_context.Lazy_storage.Copy {|
        Alpha_context.Lazy_storage.init.Copy.src := src |} ⇒
      let? '(acc_value, ctxt) :=
        collect_token_diffs_of_big_map ctxt token_and_amount src acc_value in
      collect_token_diffs_of_big_map_and_updates ctxt src updates acc_value
    |
      Alpha_context.Lazy_storage.Alloc {|
        Lazy_storage_kind.Big_map.alloc.key_type := _;
          Lazy_storage_kind.Big_map.alloc.value_type := value_type
          |} ⇒
      collect_token_diffs_of_big_map_updates ctxt big_map_id value_type updates
        acc_value
    end
  | Alpha_context.Lazy_storage.Item Lazy_storage_kind.Sapling_state _ _
    return? (acc_value, ctxt)
  end.

Definition ticket_diffs_of_lazy_storage_diff
  (ctxt : Alpha_context.context)
  (diffs_items : list Alpha_context.Lazy_storage.diffs_item)
  : M? (list (Ticket_token.ex_token × Z.t) × Alpha_context.context) :=
  List.fold_left_es
    (fun (function_parameter :
      list (Ticket_token.ex_token × Z.t) × Alpha_context.context) ⇒
      let '(acc_value, ctxt) := function_parameter in
      fun (diff_item : Alpha_context.Lazy_storage.diffs_item) ⇒
        collect_token_diffs_of_big_map_diff ctxt diff_item acc_value)
    (nil, ctxt) diffs_items.