Skip to main content

🦥 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.Proto_alpha.Environment.
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 .
  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.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.Non_iterable_indexed_carbonated_data_storage_with_values.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.Non_iterable_indexed_carbonated_data_storage_with_values.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.

Axiom get_ops : {i a u : Set}, Lazy_storage_kind.t ops i a u.

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
          | RemoveSome 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
    | ExistingCache_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
  | RemoveCache_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
      | Existingreturn? (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.

Axiom item_encoding : Data_encoding.encoding diffs_item.

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) :=
  (let arg := Data_encoding.def "lazy_storage_diff" in
  fun (eta : Data_encoding.encoding (list diffs_item)) ⇒ arg None None eta)
    (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.

Axiom fresh : {i : Set},
  Lazy_storage_kind.t bool Raw_context.t M? (Raw_context.t × i).

Axiom init_value : Raw_context.t M? Raw_context.t.

Axiom cleanup_temporaries : Raw_context.t Raw_context.t.