🦥 Lazy_storage_diff.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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Module Next.
  Record signature {id : Set} : Set := {
    id := id;
    init_value : Raw_context.t → M? Raw_context.t;
    incr : Raw_context.t → M? (Raw_context.t × id);
  }.
End Next.
Definition Next := @Next.signature.
Arguments Next {_}.

Module Total_bytes.
  Record signature {id : Set} : Set := {
    id := id;
    init_value : Raw_context.t → id → Z.t → M? Raw_context.t;
    get : Raw_context.t → id → M? Z.t;
    update : Raw_context.t → id → Z.t → M? Raw_context.t;
  }.
End Total_bytes.
Definition Total_bytes := @Total_bytes.signature.
Arguments Total_bytes {_}.

Operations to be defined on a lazy storage type.

Module OPS.
  Record signature {Id_t alloc updates : Set} : Set := {
    Id : Lazy_storage_kind.ID (t := Id_t);
    alloc := alloc;
    updates := updates;
    title : string;
    alloc_encoding : Data_encoding.t alloc;
    updates_encoding : Data_encoding.t updates;
    alloc_in_memory_size : alloc → Cache_memory_helpers.nodes_and_size;
    updates_in_memory_size : updates → Cache_memory_helpers.nodes_and_size;
    bytes_size_for_empty : Z.t;
    alloc_value :
      Raw_context.t → Id.(Lazy_storage_kind.ID.t) → alloc → M? Raw_context.t;
    apply_updates :
      Raw_context.t → Id.(Lazy_storage_kind.ID.t) → updates →
      M? (Raw_context.t × Z.t);
    Next : Next (id := Id.(Lazy_storage_kind.ID.t));
    Total_bytes : Total_bytes (id := Id.(Lazy_storage_kind.ID.t));
    

Deep copy.

    copy :
      Raw_context.t → Id.(Lazy_storage_kind.ID.t) →
      Id.(Lazy_storage_kind.ID.t) → M? Raw_context.t;
    

Deep deletion.

    remove : Raw_context.t → Id.(Lazy_storage_kind.ID.t) → Raw_context.t;
  }.
End OPS.
Definition OPS := @OPS.signature.
Arguments OPS {_ _ _}.

Module Big_map.
  Include Lazy_storage_kind.Big_map.

  Definition alloc_in_memory_size (function_parameter : alloc)
    : int × Saturation_repr.t :=
    let '{|
      Lazy_storage_kind.Big_map.alloc.key_type := key_type;
        Lazy_storage_kind.Big_map.alloc.value_type := value_type
        |} := function_parameter in
    Cache_memory_helpers.ret_adding
      (Cache_memory_helpers.op_plusplus
        (Cache_memory_helpers.expr_size key_type)
        (Cache_memory_helpers.expr_size value_type))
      (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
        (Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size 2)).

  Definition updates_in_memory_size (updates : list update)
    : int × Saturation_repr.t :=
    let update_size (function_parameter : update) : int × Saturation_repr.t :=
      let '{|
        Lazy_storage_kind.Big_map.update.key := key_value;
          Lazy_storage_kind.Big_map.update.key_hash := _;
          Lazy_storage_kind.Big_map.update.value := value_value
          |} := function_parameter in
      Cache_memory_helpers.ret_adding
        (Cache_memory_helpers.op_plusplus
          (Cache_memory_helpers.expr_size key_value)
          (Cache_memory_helpers.option_size_vec Cache_memory_helpers.expr_size
            value_value))
        (Cache_memory_helpers.op_plusquestion
          (Cache_memory_helpers.op_plusexclamation
            Cache_memory_helpers.header_size
            (Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size
              3)) Script_expr_hash.size_value) in
    Cache_memory_helpers.list_fold_size update_size updates.

  Definition bytes_size_for_big_map_key : int := 65.

  Definition bytes_size_for_empty : Z.t :=
    let bytes_size_for_big_map := 33 in
    Z.of_int bytes_size_for_big_map.

  Definition alloc_value
    (ctxt : Raw_context.t)
    (id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
    (function_parameter : alloc) : M? Raw_context.t :=
    let '{|
      Lazy_storage_kind.Big_map.alloc.key_type := key_type;
        Lazy_storage_kind.Big_map.alloc.value_type := value_type
        |} := function_parameter in
    let key_type :=
      Micheline.strip_locations
        (Script_repr.strip_annotations (Micheline.root_value key_type)) in
    let value_type :=
      Micheline.strip_locations
        (Script_repr.strip_annotations (Micheline.root_value value_type)) in
    let? ctxt :=
      Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.init_value)
        ctxt id key_type in
    Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.init_value)
      ctxt id value_type.

  Definition apply_update
    (ctxt : Raw_context.t) (id : Storage.Big_map.id)
    (function_parameter : update) : M? (Raw_context.t × Z.t) :=
    let '{|
      Lazy_storage_kind.Big_map.update.key :=
        _key_is_shown_only_on_the_receipt_in_print_big_map_diff;
        Lazy_storage_kind.Big_map.update.key_hash := key_hash;
        Lazy_storage_kind.Big_map.update.value := value_value
        |} := function_parameter in
    match value_value with
    | None ⇒
      let? '(ctxt, freed, existed) :=
        Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.remove)
          (ctxt, id) key_hash in
      let freed :=
        if existed then
          freed +i bytes_size_for_big_map_key
        else
          freed in
      return? (ctxt, (Z.of_int (Pervasives.op_tildeminus freed)))
    | Some v_value ⇒
      let? '(ctxt, size_diff, existed) :=
        Storage.Big_map.Contents.(Storage_sigs.Indexed_carbonated_data_storage.add)
          (ctxt, id) key_hash v_value in
      let size_diff :=
        if existed then
          size_diff
        else
          size_diff +i bytes_size_for_big_map_key in
      return? (ctxt, (Z.of_int size_diff))
    end.

  Definition apply_updates
    (ctxt : Raw_context.t) (id : Storage.Big_map.id) (updates : list update)
    : M? (Raw_context.t × Z.t) :=
    List.fold_left_es
      (fun (function_parameter : Raw_context.t × Z.t) ⇒
        let '(ctxt, size_value) := function_parameter in
        fun (update : update) ⇒
          let? '(ctxt, added_size) := apply_update ctxt id update in
          return? (ctxt, (size_value +Z added_size))) (ctxt, Z.zero) updates.

  Include Storage.Big_map.
End Big_map.

Definition ops (id alloc updates : Set) : Set :=
  {_ : unit @ OPS (Id_t := id) (alloc := alloc) (updates := updates)}.

Module Sapling_state.
  Include Lazy_storage_kind.Sapling_state.

  Definition alloc_in_memory_size (function_parameter : alloc)
    : int × Saturation_repr.t :=
    let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := _ |} :=
      function_parameter in
    (Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
      (Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
        Cache_memory_helpers.word_size)).

  Definition updates_in_memory_size (update : Sapling_repr.diff)
    : int × Saturation_repr.t :=
    (Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
      (Sapling_repr.diff_in_memory_size update)).

  Definition bytes_size_for_empty : Z.t := Z.of_int 33.

  Definition alloc_value
    (ctxt : Raw_context.t) (id : Storage.Sapling.id)
    (function_parameter : alloc) : M? Raw_context.t :=
    let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := memo_size |} :=
      function_parameter in
    Sapling_storage.init_value ctxt id memo_size.

  Definition apply_updates
    (ctxt : Raw_context.t) (id : Storage.Sapling.id)
    (updates : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
    Sapling_storage.apply_diff ctxt id updates.

  Include Storage.Sapling.
End Sapling_state.

Definition get_ops {i a u : Set} (function_parameter : Lazy_storage_kind.t)
  : ops i a u :=
  match function_parameter with
  | Lazy_storage_kind.Big_map ⇒
    cast (ops i a u)
    (existS (A := unit) (fun _ ⇒ _) tt
      {|
        OPS.Id := Big_map.Id;
        OPS.title := Big_map.title;
        OPS.alloc_encoding := Big_map.alloc_encoding;
        OPS.updates_encoding := Big_map.updates_encoding;
        OPS.alloc_in_memory_size := Big_map.alloc_in_memory_size;
        OPS.updates_in_memory_size := Big_map.updates_in_memory_size;
        OPS.bytes_size_for_empty := Big_map.bytes_size_for_empty;
        OPS.alloc_value := Big_map.alloc_value;
        OPS.apply_updates := Big_map.apply_updates;
        OPS.Next := cast (Next) Big_map.Next;
        OPS.Total_bytes := cast (Total_bytes) Big_map.Total_bytes;
        OPS.copy := Big_map.copy;
        OPS.remove := Big_map.remove
      |})
  | Lazy_storage_kind.Sapling_state ⇒
    cast (ops i a u)
    (existS (A := unit) (fun _ ⇒ _) tt
      {|
        OPS.Id := Sapling_state.Id;
        OPS.title := Sapling_state.title;
        OPS.alloc_encoding := Sapling_state.alloc_encoding;
        OPS.updates_encoding := Sapling_state.updates_encoding;
        OPS.alloc_in_memory_size := Sapling_state.alloc_in_memory_size;
        OPS.updates_in_memory_size := Sapling_state.updates_in_memory_size;
        OPS.bytes_size_for_empty := Sapling_state.bytes_size_for_empty;
        OPS.alloc_value := Sapling_state.alloc_value;
        OPS.apply_updates := Sapling_state.apply_updates;
        OPS.Next := axiom;
        OPS.Total_bytes := cast (Total_bytes) Sapling_state.Total_bytes;
        OPS.copy := Sapling_state.copy;
        OPS.remove := Sapling_state.remove
      |})
  end.

Records for the constructor parameters

Module ConstructorRecords_init.
  Module init.
    Module Copy.
      Record record {src : Set} : Set := Build {
        src : src;
      }.
      Arguments record : clear implicits.
      Definition with_src {t_src} src (r : record t_src) :=
        Build t_src src.
    End Copy.
    Definition Copy_skeleton := Copy.record.
  End init.
End ConstructorRecords_init.
Import ConstructorRecords_init.

Reserved Notation "'init.Copy".

Inductive init (id alloc : Set) : Set :=
| Existing : init id alloc
| Copy : 'init.Copy id → init id alloc
| Alloc : alloc → init id alloc

where "'init.Copy" := (fun (t_id : Set) ⇒ init.Copy_skeleton t_id).

Module init.
  Include ConstructorRecords_init.init.
  Definition Copy := 'init.Copy.
End init.

Arguments Existing {_ _}.
Arguments Copy {_ _}.
Arguments Alloc {_ _}.

Records for the constructor parameters

Module ConstructorRecords_diff.
  Module diff.
    Module Update.
      Record record {init updates : Set} : Set := Build {
        init : init;
        updates : updates;
      }.
      Arguments record : clear implicits.
      Definition with_init {t_init t_updates} init
        (r : record t_init t_updates) :=
        Build t_init t_updates init r.(updates).
      Definition with_updates {t_init t_updates} updates
        (r : record t_init t_updates) :=
        Build t_init t_updates r.(init) updates.
    End Update.
    Definition Update_skeleton := Update.record.
  End diff.
End ConstructorRecords_diff.
Import ConstructorRecords_diff.

Reserved Notation "'diff.Update".

Inductive diff (id alloc updates : Set) : Set :=
| Remove : diff id alloc updates
| Update : 'diff.Update alloc id updates → diff id alloc updates

where "'diff.Update" :=
  (fun (t_alloc t_id t_updates : Set) ⇒ diff.Update_skeleton
    (init t_id t_alloc) t_updates).

Module diff.
  Include ConstructorRecords_diff.diff.
  Definition Update := 'diff.Update.
End diff.

Arguments Remove {_ _ _}.
Arguments Update {_ _ _}.

Definition diff_encoding {i a u : Set} (OPS : ops i a u)
  : Data_encoding.t (diff i a u) :=
  let 'existS _ _ OPS := OPS in
  Data_encoding.union None
    [
      Data_encoding.case_value "update" None (Data_encoding.Tag 0)
        (Data_encoding.obj2
          (Data_encoding.req None None "action"
            (Data_encoding.constant "update"))
          (Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
        (fun (function_parameter : diff i a u) ⇒
          match function_parameter with
          |
            Update {|
              diff.Update.init := Existing;
                diff.Update.updates := updates
                |} ⇒ Some (tt, updates)
          | _ ⇒ None
          end)
        (fun (function_parameter : unit × u) ⇒
          let '(_, updates) := function_parameter in
          Update
            {| diff.Update.init := Existing;
              diff.Update.updates := updates; |});
      Data_encoding.case_value "remove" None (Data_encoding.Tag 1)
        (Data_encoding.obj1
          (Data_encoding.req None None "action"
            (Data_encoding.constant "remove")))
        (fun (function_parameter : diff i a u) ⇒
          match function_parameter with
          | Remove ⇒ Some tt
          | _ ⇒ None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Remove);
      Data_encoding.case_value "copy" None (Data_encoding.Tag 2)
        (Data_encoding.obj3
          (Data_encoding.req None None "action"
            (Data_encoding.constant "copy"))
          (Data_encoding.req None None "source"
            OPS.(OPS.Id).(Lazy_storage_kind.ID.encoding))
          (Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
        (fun (function_parameter : diff i a u) ⇒
          match function_parameter with
          |
            Update {|
              diff.Update.init := Copy {| init.Copy.src := src |};
                diff.Update.updates := updates
                |} ⇒ Some (tt, src, updates)
          | _ ⇒ None
          end)
        (fun (function_parameter : unit × i × u) ⇒
          let '(_, src, updates) := function_parameter in
          Update
            {| diff.Update.init := Copy {| init.Copy.src := src; |};
              diff.Update.updates := updates; |});
      Data_encoding.case_value "alloc" None (Data_encoding.Tag 3)
        (Data_encoding.merge_objs
          (Data_encoding.obj2
            (Data_encoding.req None None "action"
              (Data_encoding.constant "alloc"))
            (Data_encoding.req None None "updates"
              OPS.(OPS.updates_encoding))) OPS.(OPS.alloc_encoding))
        (fun (function_parameter : diff i a u) ⇒
          match function_parameter with
          |
            Update {|
              diff.Update.init := Alloc alloc_value;
                diff.Update.updates := updates
                |} ⇒ Some ((tt, updates), alloc_value)
          | _ ⇒ None
          end)
        (fun (function_parameter : (unit × u) × a) ⇒
          let '((_, updates), alloc_value) := function_parameter in
          Update
            {| diff.Update.init := Alloc alloc_value;
              diff.Update.updates := updates; |})
    ].

Definition init_size {i a u : Set} (OPS : ops i a u)
  : init i a → Cache_memory_helpers.nodes_and_size :=
  let 'existS _ _ OPS := OPS in
  fun (init_value : init i a) ⇒
    match init_value with
    | Existing ⇒ Cache_memory_helpers.zero
    | Copy {| init.Copy.src := _id_is_a_Z_fitting_in_an_int_for_a_long_time |}
      ⇒
      (Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
        (Cache_memory_helpers.op_plusexclamation
          Cache_memory_helpers.header_size Cache_memory_helpers.word_size))
    | Alloc alloc_value ⇒
      Cache_memory_helpers.ret_adding
        (OPS.(OPS.alloc_in_memory_size) alloc_value)
        (Cache_memory_helpers.op_plusexclamation
          Cache_memory_helpers.header_size Cache_memory_helpers.word_size)
    end.

Definition updates_size {i a u : Set} (OPS : ops i a u)
  : u → Cache_memory_helpers.nodes_and_size :=
  let 'existS _ _ OPS := OPS in
  fun (updates : u) ⇒ OPS.(OPS.updates_in_memory_size) updates.

Definition diff_in_memory_size {A B C : Set}
  (kind_value : Lazy_storage_kind.t) (diff_value : diff A B C)
  : int × Saturation_repr.t :=
  match diff_value with
  | Remove ⇒ Cache_memory_helpers.zero
  | Update {| diff.Update.init := init_value; diff.Update.updates := updates |}
    ⇒
    let ops := get_ops kind_value in
    Cache_memory_helpers.ret_adding
      (Cache_memory_helpers.op_plusplus (init_size ops init_value)
        (updates_size ops updates)) Cache_memory_helpers.h2w
  end.

[apply_updates ctxt ops ~id init] applies the updates [updates] on lazy storage [id] on storage context [ctxt] using operations [ops] and returns the updated storage context and the added size in bytes (may be negative).

Definition apply_updates {i a u : Set} (ctxt : Raw_context.t) (OPS : ops i a u)
  : i → u → M? (Raw_context.t × Z.t) :=
  let 'existS _ _ OPS := OPS in
  fun (id : i) ⇒
    fun (updates : u) ⇒
      let? '(ctxt, updates_size) := OPS.(OPS.apply_updates) ctxt id updates in
      if Z.equal updates_size Z.zero then
        return? (ctxt, updates_size)
      else
        let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
        let? ctxt :=
          OPS.(OPS.Total_bytes).(Total_bytes.update) ctxt id
            (size_value +Z updates_size) in
        return? (ctxt, updates_size).

[apply_init ctxt ops ~id init] applies the initialization [init] on lazy storage [id] on storage context [ctxt] using operations [ops] and returns the updated storage context and the added size in bytes (may be negative).

If [id] represents a temporary lazy storage, the added size may be wrong.

Definition apply_init {i a u : Set} (ctxt : Raw_context.t) (OPS : ops i a u)
  : i → init i a → M? (Raw_context.t × Z.t) :=
  let 'existS _ _ OPS := OPS in
  fun (id : i) ⇒
    fun (init_value : init i a) ⇒
      match init_value with
      | Existing ⇒ return? (ctxt, Z.zero)
      | Copy {| init.Copy.src := src |} ⇒
        let? ctxt := OPS.(OPS.copy) ctxt src id in
        if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
          return? (ctxt, Z.zero)
        else
          let? copy_size := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt src in
          return? (ctxt, (copy_size +Z OPS.(OPS.bytes_size_for_empty)))
      | Alloc alloc_value ⇒
        let? ctxt :=
          OPS.(OPS.Total_bytes).(Total_bytes.init_value) ctxt id Z.zero in
        let? ctxt := OPS.(OPS.alloc_value) ctxt id alloc_value in
        return? (ctxt, OPS.(OPS.bytes_size_for_empty))
      end.

[apply_diff ctxt ops ~id diff] applies the diff [diff] on lazy storage [id] on storage context [ctxt] using operations [ops] and returns the updated storage context and the added size in bytes (may be negative).

If [id] represents a temporary lazy storage, the added size may be wrong.

Definition apply_diff {i a u : Set}
  (ctxt : Raw_context.t) (function_parameter : ops i a u)
  : i → diff i a u → M? (Raw_context.t × Z.t) :=
  let 'OPS as ops := function_parameter in
  let 'existS _ _ OPS := OPS in
  fun (id : i) ⇒
    fun (diff_value : diff i a u) ⇒
      match diff_value with
      | Remove ⇒
        if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
          let ctxt := OPS.(OPS.remove) ctxt id in
          return? (ctxt, Z.zero)
        else
          let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
          let ctxt := OPS.(OPS.remove) ctxt id in
          return? (ctxt, (Z.neg (size_value +Z OPS.(OPS.bytes_size_for_empty))))
      |
        Update {|
          diff.Update.init := init_value; diff.Update.updates := updates |}
        ⇒
        let? '(ctxt, init_size) := apply_init ctxt ops id init_value in
        let? '(ctxt, updates_size) := apply_updates ctxt ops id updates in
        return? (ctxt, (init_size +Z updates_size))
      end.

Inductive diffs_item : Set :=
| Item : ∀ {i a u : Set},
  Lazy_storage_kind.t → i → diff i a u → diffs_item.

Definition make {i a u : Set}
  (k_value : Lazy_storage_kind.t) (id : i) (diff_value : diff i a u)
  : diffs_item := Item k_value id diff_value.

Definition item_encoding : Data_encoding.encoding diffs_item :=
  Data_encoding.union None
    (List.map
      (fun (function_parameter : int × Lazy_storage_kind.ex) ⇒
        let '(tag, Lazy_storage_kind.Ex_Kind k_value) := function_parameter in
        let 'existT _ [__Ex_Kind, __Ex_Kind1, __Ex_Kind2] [k_value, tag] :=
          cast_exists (Es := [Set ** Set ** Set])
            (fun '[__Ex_Kind, __Ex_Kind1, __Ex_Kind2] ⇒
              [Lazy_storage_kind.t ** int]) [k_value, tag] in
        let ops := get_ops k_value in
        let OPS := ops in
        let 'existS _ _ OPS := OPS in
        let title := OPS.(OPS.title) in
        Data_encoding.case_value title None (Data_encoding.Tag tag)
          (Data_encoding.obj3
            (Data_encoding.req None None "kind" (Data_encoding.constant title))
            (Data_encoding.req None None "id"
              OPS.(OPS.Id).(Lazy_storage_kind.ID.encoding))
            (Data_encoding.req None None "diff" (diff_encoding ops)))
          (fun (function_parameter : diffs_item) ⇒
            let 'Item kind_value id diff_value := function_parameter in
            match Lazy_storage_kind.equal k_value kind_value with
            | Lazy_storage_kind.Eq ⇒
              cast
                (option
                  (unit × __Ex_Kind × diff __Ex_Kind __Ex_Kind1 __Ex_Kind2))
              (Some (tt, id, diff_value))
            | Lazy_storage_kind.Neq ⇒
              cast
                (option
                  (unit × __Ex_Kind × diff __Ex_Kind __Ex_Kind1 __Ex_Kind2))
              (None :
                option (unit × __Ex_Kind × diff __Ex_Kind __Ex_Kind1 __Ex_Kind2))
            end)
          (fun (function_parameter :
            unit × __Ex_Kind × diff __Ex_Kind __Ex_Kind1 __Ex_Kind2) ⇒
            let '(_, id, diff_value) := function_parameter in
            Item k_value id diff_value)) Lazy_storage_kind.all).

Definition item_in_memory_size (function_parameter : diffs_item)
  : int × Saturation_repr.t :=
  let
    'Item kind_value _id_is_a_Z_fitting_in_an_int_for_a_long_time diff_value :=
    function_parameter in
  Cache_memory_helpers.ret_adding (diff_in_memory_size kind_value diff_value)
    Cache_memory_helpers.h3w.

Definition diffs : Set := list diffs_item.

Definition diffs_in_memory_size (diffs : list diffs_item)
  : int × Saturation_repr.t :=
  Cache_memory_helpers.list_fold_size item_in_memory_size diffs.

Definition encoding : Data_encoding.encoding (list diffs_item) :=
  Data_encoding.def "lazy_storage_diff" None None
    (Data_encoding.list_value None item_encoding).

Definition apply (ctxt : Raw_context.t) (diffs : list diffs_item)
  : M? (Raw_context.t × Z.t) :=
  List.fold_left_es
    (fun (function_parameter : Raw_context.t × Z.t) ⇒
      let '(ctxt, total_size) := function_parameter in
      fun (function_parameter : diffs_item) ⇒
        let 'Item k_value id diff_value := function_parameter in
        let ops := get_ops k_value in
        let? '(ctxt, added_size) := apply_diff ctxt ops id diff_value in
        let OPS := ops in
        return?
          (let 'existS _ _ OPS := OPS in
          (ctxt,
            (if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
              total_size
            else
              total_size +Z added_size)))) (ctxt, Z.zero) diffs.

Definition fresh {i a u : Set}
  (kind_value : Lazy_storage_kind.t) (temporary : bool) (ctxt : Raw_context.t)
  : M? (Raw_context.t × i) :=
  if temporary then
    return?
      (Raw_context.fold_map_temporary_lazy_storage_ids ctxt
        (fun (temp_ids : Lazy_storage_kind.Temp_ids.t) ⇒
          Lazy_storage_kind.Temp_ids.fresh kind_value temp_ids))
  else
    let 'kind_value := kind_value in
    let kind_value := cast Lazy_storage_kind.t kind_value in
    let m_value := get_ops kind_value in
    let OPS := (m_value : ops i a u) in
    let 'existS _ _ OPS := OPS in
    OPS.(OPS.Next).(Next.incr) ctxt.

Definition init_value (ctxt : Raw_context.t) : M? Raw_context.t :=
  List.fold_left_es
    (fun (ctxt : Raw_context.t) ⇒
      fun (function_parameter : int × Lazy_storage_kind.ex) ⇒
        let '(_tag, Lazy_storage_kind.Ex_Kind k_value) := function_parameter in
        let 'existT _ [__Ex_Kind, __Ex_Kind1, __Ex_Kind2] [k_value, _tag] :=
          cast_exists (Es := [Set ** Set ** Set])
            (fun '[__Ex_Kind, __Ex_Kind1, __Ex_Kind2] ⇒
              [Lazy_storage_kind.t ** int]) [k_value, _tag] in
        let OPS := ((get_ops k_value) : ops __Ex_Kind __Ex_Kind1 __Ex_Kind2) in
        let 'existS _ _ OPS := OPS in
        OPS.(OPS.Next).(Next.init_value) ctxt) ctxt Lazy_storage_kind.all.

Definition cleanup_temporaries (ctxt : Raw_context.t) : Raw_context.t :=
  Raw_context.map_temporary_lazy_storage_ids_s ctxt
    (fun (temp_ids : Lazy_storage_kind.Temp_ids.t) ⇒
      let ctxt :=
        List.fold_left_s
          (fun (ctxt : Raw_context.t) ⇒
            fun (function_parameter : int × Lazy_storage_kind.ex) ⇒
              let '(_tag, Lazy_storage_kind.Ex_Kind k_value) :=
                function_parameter in
              let 'existT _ [__Ex_Kind, __Ex_Kind1, __Ex_Kind2] [k_value, _tag]
                :=
                cast_exists (Es := [Set ** Set ** Set])
                  (fun '[__Ex_Kind, __Ex_Kind1, __Ex_Kind2] ⇒
                    [Lazy_storage_kind.t ** int]) [k_value, _tag] in
              let OPS :=
                ((get_ops k_value) : ops __Ex_Kind __Ex_Kind1 __Ex_Kind2) in
              let 'existS _ _ OPS := OPS in
              Lazy_storage_kind.Temp_ids.fold_s k_value OPS.(OPS.remove)
                temp_ids ctxt) ctxt Lazy_storage_kind.all in
      (ctxt, Lazy_storage_kind.Temp_ids.init_value)).