🏁 Init_storage.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.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Bootstrap_storage.
Require TezosOfOCaml.Proto_alpha.Commitment_repr.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Delegate_cycles.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Legacy_script_patches.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_migration.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_storage.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Seed_storage.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.
Require TezosOfOCaml.Proto_alpha.Vote_storage.

Definition patch_script
  (function_parameter : string × Script_expr_hash.t × Script_repr.expr)
  : Raw_context.t → M? Raw_context.t :=
  let '(address, hash_value, patched_code) := function_parameter in
  fun (ctxt : Raw_context.t) ⇒
    let? contract := Contract_repr.of_b58check address in
    let? '(ctxt, code_opt) :=
      Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
        ctxt contract in
    let '_ :=
      Logging.log Logging.Notice
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Patching "
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.String_literal "... "
                CamlinternalFormatBasics.End_of_format))) "Patching %s... ")
        address in
    match code_opt with
    | Some old_code ⇒
      let old_bin := Data_encoding.force_bytes old_code in
      let old_hash := Script_expr_hash.hash_bytes None [ old_bin ] in
      if Script_expr_hash.equal old_hash hash_value then
        let new_code := Script_repr.lazy_expr_value patched_code in
        let? '(ctxt, size_diff) :=
          Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
            ctxt contract new_code in
        let '_ :=
          Logging.log Logging.Notice
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Contract "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal
                    " successfully patched"
                    CamlinternalFormatBasics.End_of_format)))
              "Contract %s successfully patched") address in
        let size_diff := Z.of_int size_diff in
        let? prev_size :=
          Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.get)
            ctxt contract in
        let new_size := prev_size +Z size_diff in
        let? ctxt :=
          Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.update)
            ctxt contract new_size in
        if Z.gt size_diff Z.zero then
          let? prev_paid_size :=
            Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.get)
              ctxt contract in
          let paid_size := prev_paid_size +Z size_diff in
          Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.update)
            ctxt contract paid_size
        else
          return? ctxt
      else
        let '_ :=
          Logging.log Logging.Error
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Patching "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal
                    " was skipped because its script does not have the expected hash (expected: "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal ", found: "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Char_literal ")" % char
                            CamlinternalFormatBasics.End_of_format)))))))
              "Patching %s was skipped because its script does not have the expected hash (expected: %a, found: %a)")
            address Script_expr_hash.pp hash_value Script_expr_hash.pp old_hash
          in
        return? ctxt
    | None ⇒
      let '_ :=
        Logging.log Logging.Error
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "Patching "
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                (CamlinternalFormatBasics.String_literal
                  " was skipped because no script was found for it in the context."
                  CamlinternalFormatBasics.End_of_format)))
            "Patching %s was skipped because no script was found for it in the context.")
          address in
      return? ctxt
    end.

Definition prepare_first_block {A : Set}
  (_chain_id : A) (ctxt : Context.t)
  (typecheck :
    Raw_context.t → Script_repr.t →
    M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  (level : int32) (timestamp : Time.t) (predecessor : Block_hash.t)
  : M? Raw_context.t :=
  let? '(previous_protocol, ctxt) :=
    Raw_context.prepare_first_block level timestamp ctxt in
  let parametric_value := Raw_context.constants ctxt in
  let ctxt :=
    let ctxt :=
      Raw_context.Cache.(Context.CACHE.set_cache_layout) ctxt
        (Constants_repr.cache_layout parametric_value) in
    Raw_context.Cache.(Context.CACHE.clear) ctxt in
  let? '(ctxt, balance_updates) :=
    match previous_protocol with
    | Raw_context.Genesis param ⇒
      let? level := Raw_level_repr.of_int32 level in
      let? ctxt :=
        Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.init_value)
          ctxt level in
      let? ctxt :=
        Storage.Block_round.(Storage.Simple_single_data_storage.init_value) ctxt
          Round_repr.zero in
      let init_commitment
        (function_parameter :
          Raw_context.t ×
            list
              (Receipt_repr.balance × Receipt_repr.balance_update ×
                Receipt_repr.update_origin))
        : Commitment_repr.t →
        M?
          (Raw_context.t ×
            list
              (Receipt_repr.balance × Receipt_repr.balance_update ×
                Receipt_repr.update_origin)) :=
        let '(ctxt, balance_updates) := function_parameter in
        fun (function_parameter : Commitment_repr.t) ⇒
          let '{|
            Commitment_repr.t.blinded_public_key_hash := blinded_public_key_hash;
              Commitment_repr.t.amount := amount
              |} := function_parameter in
          let? '(ctxt, new_balance_updates) :=
            Token.transfer None ctxt
              (Token.Source_infinite Token.Initial_commitments)
              (Token.Sink_container
                (Token.Collected_commitments blinded_public_key_hash)) amount in
          return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates))
        in
      let? '(ctxt, commitments_balance_updates) :=
        List.fold_left_es init_commitment (ctxt, nil)
          param.(Parameters_repr.t.commitments) in
      let? ctxt :=
        Storage.Stake.Last_snapshot.(Storage_sigs.Single_data_storage.init_value)
          ctxt 0 in
      let? ctxt :=
        Seed_storage.init_value
          param.(Parameters_repr.t.constants).(Constants_parametric_repr.t.initial_seed)
          ctxt in
      let? ctxt := Contract_storage.init_value ctxt in
      let? '(ctxt, bootstrap_balance_updates) :=
        Bootstrap_storage.init_value ctxt typecheck
          param.(Parameters_repr.t.no_reward_cycles)
          param.(Parameters_repr.t.bootstrap_accounts)
          param.(Parameters_repr.t.bootstrap_contracts) in
      let? '(ctxt, deposits_balance_updates) :=
        Delegate_cycles.init_first_cycles ctxt Receipt_repr.Protocol_migration
        in
      let? ctxt :=
        Vote_storage.init_value ctxt
          (Level_storage.current ctxt).(Level_repr.t.level_position) in
      let? ctxt := Vote_storage.update_listings ctxt in
      let? '(ctxt, operation_results) :=
        Liquidity_baking_migration.init_value ctxt typecheck in
      let? ctxt :=
        Storage.Pending_migration.Operation_results.(Storage_sigs.Single_data_storage.init_value)
          ctxt operation_results in
      let? ctxt := Sc_rollup_inbox_storage.init_value timestamp predecessor ctxt
        in
      return?
        (ctxt,
          (Pervasives.op_at commitments_balance_updates
            (Pervasives.op_at bootstrap_balance_updates deposits_balance_updates)))
    | Raw_context.Lima_015 ⇒
      let? level := Raw_level_repr.of_int32 level in
      let? ctxt :=
        Storage.Tenderbake.First_level_of_protocol.(Storage_sigs.Single_data_storage.update)
          ctxt level in
      let? ctxt := Sc_rollup_inbox_storage.init_value timestamp predecessor ctxt
        in
      return? (ctxt, nil)
    end in
  let? ctxt :=
    List.fold_right_es patch_script Legacy_script_patches.addresses_to_patch
      ctxt in
  let? balance_updates := Receipt_repr.group_balance_updates balance_updates in
  let ctxt :=
    Storage.Pending_migration.Balance_updates.(Storage_sigs.Single_data_storage.add)
      ctxt balance_updates in
  return? ctxt.

Definition prepare
  (ctxt : Context.t) (level : Int32.t) (predecessor_timestamp : Time.t)
  (timestamp : Time.t)
  : M?
    (Raw_context.t × Receipt_repr.balance_updates ×
      list Migration_repr.origination_result) :=
  let? ctxt := Raw_context.prepare level predecessor_timestamp timestamp ctxt in
  Storage.Pending_migration.remove ctxt.