🐣 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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
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_consensus_key.
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.

Init function; without side-effects in Coq

Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "bootstrap.unrevealed_public_key"
    "Forbidden delegation from unrevealed public key"
    "Tried to delegate from an unrevealed public key"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (delegate : Signature.public_key_hash) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Delegation from an unrevealed public key (for "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal ") is forbidden."
                    CamlinternalFormatBasics.End_of_format)))
              "Delegation from an unrevealed public key (for %a) is forbidden.")
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) delegate))
    (Data_encoding.obj1
      (Data_encoding.req None None "delegator"
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Unrevealed_public_key" then
          let pkh := cast Signature.public_key_hash payload in
          Some pkh
        else None
      end)
    (fun (pkh : Signature.public_key_hash) ⇒
      Build_extensible "Unrevealed_public_key" Signature.public_key_hash pkh).

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;
        Parameters_repr.bootstrap_account.delegate_to := delegate_to;
        Parameters_repr.bootstrap_account.consensus_key := consensus_key
        |} := function_parameter in
    let contract := Contract_repr.Implicit 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 None ctxt public_key_hash
            public_key in
        let? ctxt :=
          Delegate_storage.Contract.set ctxt contract
            (Some (Option.value_value delegate_to public_key_hash)) in
        match consensus_key with
        | None ⇒ return? ctxt
        | Some consensus_key ⇒
          Delegate_consensus_key.init_value ctxt public_key_hash consensus_key
        end
      | None ⇒
        let? '_ :=
          Error_monad.fail_when (Option.is_some delegate_to)
            (Build_extensible "Unrevealed_public_key" Signature.public_key_hash
              public_key_hash) in
        return? 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_hash) :=
      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_hash script
      in
    let contract := Contract_repr.Originated contract_hash in
    let? ctxt :=
      match delegate with
      | None ⇒ return? ctxt
      | Some delegate ⇒
        Delegate_storage.Contract.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
    | None ⇒ return? ctxt
    | Some cycles ⇒
      let constants := Raw_context.constants ctxt in
      let ctxt :=
        Raw_context.patch_constants ctxt
          (fun (c_value : Constants_parametric_repr.t) ⇒
            Constants_parametric_repr.t.with_endorsing_reward_per_slot
              Tez_repr.zero
              (Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
                Tez_repr.zero
                (Constants_parametric_repr.t.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_parametric_repr.t.baking_reward_fixed_portion);
          Storage.Ramp_up.reward.baking_reward_bonus_per_slot :=
            constants.(Constants_parametric_repr.t.baking_reward_bonus_per_slot);
          Storage.Ramp_up.reward.endorsing_reward_per_slot :=
            constants.(Constants_parametric_repr.t.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
  | None ⇒ return? 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_parametric_repr.t) ⇒
          Constants_parametric_repr.t.with_endorsing_reward_per_slot
            endorsing_reward_per_slot
            (Constants_parametric_repr.t.with_baking_reward_bonus_per_slot
              baking_reward_bonus_per_slot
              (Constants_parametric_repr.t.with_baking_reward_fixed_portion
                baking_reward_fixed_portion c_value)))) Error_monad.ok
  end.