Skip to main content

🐣 Bootstrap_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Contract_manager_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Delegate_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Token.

Definition init_account
  (function_parameter :
    Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin))
  : Parameters_repr.bootstrap_account
  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 : Parameters_repr.bootstrap_account) ⇒
    let '{|
      Parameters_repr.bootstrap_account.public_key_hash := public_key_hash;
        Parameters_repr.bootstrap_account.public_key := public_key;
        Parameters_repr.bootstrap_account.amount := amount
        |} := function_parameter in
    let contract := Contract_repr.implicit_contract public_key_hash in
    let? '(ctxt, new_balance_updates) :=
      Token.transfer (Some Receipt_repr.Protocol_migration) ctxt
        (Token.Source_infinite Token.Bootstrap)
        (Token.Sink_container (Token.Contract contract)) amount in
    let? ctxt :=
      match public_key with
      | Some public_key
        let? ctxt :=
          Contract_manager_storage.reveal_manager_key ctxt public_key_hash
            public_key in
        Delegate_storage.set ctxt contract (Some public_key_hash)
      | Nonereturn? ctxt
      end in
    return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).

Definition init_contract
  (typecheck :
    Raw_context.t Script_repr.t
    M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  (function_parameter :
    Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin))
  : Parameters_repr.bootstrap_contract
  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 : Parameters_repr.bootstrap_contract) ⇒
    let '{|
      Parameters_repr.bootstrap_contract.delegate := delegate;
        Parameters_repr.bootstrap_contract.amount := amount;
        Parameters_repr.bootstrap_contract.script := script
        |} := function_parameter in
    let? '(ctxt, contract) :=
      Contract_storage.fresh_contract_from_current_nonce ctxt in
    let? '(script, ctxt) := typecheck ctxt script in
    let? ctxt := Contract_storage.raw_originate ctxt true contract script in
    let? ctxt :=
      match delegate with
      | Nonereturn? ctxt
      | Some delegateDelegate_storage.init_value ctxt contract delegate
      end in
    let origin := Receipt_repr.Protocol_migration in
    let? '(ctxt, new_balance_updates) :=
      Token.transfer (Some origin) ctxt (Token.Source_infinite Token.Bootstrap)
        (Token.Sink_container (Token.Contract contract)) amount in
    return? (ctxt, (Pervasives.op_at new_balance_updates balance_updates)).

Definition init_value
  (ctxt : Raw_context.t)
  (typecheck :
    Raw_context.t Script_repr.t
    M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  (no_reward_cycles : option int)
  (accounts : list Parameters_repr.bootstrap_account)
  (contracts : list Parameters_repr.bootstrap_contract)
  : M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let nonce_value := Operation_hash.hash_string None [ "Un festival de GADT." ]
    in
  let ctxt := Raw_context.init_origination_nonce ctxt nonce_value in
  let? '(ctxt, balance_updates) :=
    List.fold_left_es init_account (ctxt, nil) accounts in
  let? '(ctxt, balance_updates) :=
    List.fold_left_es (init_contract typecheck) (ctxt, balance_updates)
      contracts in
  let? ctxt :=
    match no_reward_cycles with
    | Nonereturn? ctxt
    | Some cycles
      let constants := Raw_context.constants ctxt in
      let ctxt :=
        Raw_context.patch_constants ctxt
          (fun (c_value : Constants_repr.parametric) ⇒
            Constants_repr.parametric.with_endorsing_reward_per_slot
              Tez_repr.zero
              (Constants_repr.parametric.with_baking_reward_bonus_per_slot
                Tez_repr.zero
                (Constants_repr.parametric.with_baking_reward_fixed_portion
                  Tez_repr.zero c_value))) in
      Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.init_value)
        ctxt (Cycle_repr.of_int32_exn (Int32.of_int cycles))
        {|
          Storage.Ramp_up.reward.baking_reward_fixed_portion :=
            constants.(Constants_repr.parametric.baking_reward_fixed_portion);
          Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
            constants.(Constants_repr.parametric.baking_reward_bonus_per_slot);
          Storage.Ramp_up.reward.endorsing_reward_per_slot :=
            constants.(Constants_repr.parametric.endorsing_reward_per_slot); |}
    end in
  return? (ctxt, balance_updates).

Definition cycle_end (ctxt : Raw_context.t) (last_cycle : Cycle_repr.cycle)
  : M? Raw_context.t :=
  let next_cycle := Cycle_repr.succ last_cycle in
  let? function_parameter :=
    Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.find) ctxt
      next_cycle in
  match function_parameter with
  | Nonereturn? ctxt
  |
    Some {|
      Storage.Ramp_up.reward.baking_reward_fixed_portion :=
        baking_reward_fixed_portion;
        Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
          baking_reward_bonus_per_slot;
        Storage.Ramp_up.reward.endorsing_reward_per_slot :=
          endorsing_reward_per_slot
        |} ⇒
    let? ctxt :=
      Storage.Ramp_up.Rewards.(Storage_sigs.Indexed_data_storage.remove_existing)
        ctxt next_cycle in
    Error_monad.op_gtpipeeq
      (Raw_context.patch_constants ctxt
        (fun (c_value : Constants_repr.parametric) ⇒
          Constants_repr.parametric.with_endorsing_reward_per_slot
            endorsing_reward_per_slot
            (Constants_repr.parametric.with_baking_reward_bonus_per_slot
              baking_reward_bonus_per_slot
              (Constants_repr.parametric.with_baking_reward_fixed_portion
                baking_reward_fixed_portion c_value)))) Error_monad.ok
  end.