⚗️ Liquidity_baking_migration.v

Translated OCaml

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.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Fees_storage.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_cpmm.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_lqt.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Migration_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
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 null_address : bytes :=
  Bytes.of_string
    (String.String "000"
      (String.String "000"
        (String.String "000"
          (String.String "000"
            (String.String "000"
              (String.String "000"
                (String.String "000"
                  (String.String "000"
                    (String.String "000"
                      (String.String "000"
                        (String.String "000"
                          (String.String "000"
                            (String.String "000"
                              (String.String "000"
                                (String.String "000"
                                  (String.String "000"
                                    (String.String "000"
                                      (String.String "000"
                                        (String.String "000"
                                          (String.String "000"
                                            (String.String "000"
                                              (String.String "000" "")))))))))))))))))))))).

Definition mainnet_tzBTC_address : Contract_hash.t :=
  Contract_hash.of_b58check_exn "KT1PWx2mnDueood7fEmfbBDKx1D9BAnnXitn".

If token_pool, xtz_pool, or lqt_total are ever zero the CPMM will be permanently broken. Therefore, we initialize it with the null address registered as a liquidity provider with 1 satoshi tzBTC and 100 mutez (roughly the current exchange rate).

Definition cpmm_init_storage (token_address : string) (lqt_address : string)
  : Script_repr.lazy_expr :=
  Script_repr.lazy_expr_value
    (Micheline.strip_locations
      (Micheline.Prim 0 Michelson_v1_primitives.D_Pair
        [
          Micheline.Int 1 Z.one;
          Micheline.Int 2 (Z.of_int 100);
          Micheline.Int 3 (Z.of_int 100);
          Micheline.String 4 token_address;
          Micheline.String 5 lqt_address
        ] nil)).

Definition lqt_init_storage (cpmm_address : string) : Script_repr.lazy_expr :=
  Script_repr.lazy_expr_value
    (Micheline.strip_locations
      (Micheline.Prim 0 Michelson_v1_primitives.D_Pair
        [
          Micheline.Seq 1
            [
              Micheline.Prim 2 Michelson_v1_primitives.D_Elt
                [
                  Micheline.Bytes 3
                    null_address;
                  Micheline.Int 4
                    (Z.of_int
                      100)
                ] nil
            ];
          Micheline.Seq 5 nil;
          Micheline.String 6 cpmm_address;
          Micheline.Int 7 (Z.of_int 100)
        ] nil)).

Definition test_fa12_init_storage (manager : string) : Script_repr.lazy_expr :=
  Script_repr.lazy_expr_value
    (Micheline.strip_locations
      (Micheline.Prim 0 Michelson_v1_primitives.D_Pair
        [
          Micheline.Seq 1 nil;
          Micheline.Seq 2 nil;
          Micheline.String 3 manager;
          Micheline.Int 4 (Z.of_int 10000)
        ] nil)).

Definition originate
  (ctxt : Raw_context.t) (address_hash : Contract_hash.t) (balance : Tez_repr.t)
  (script : Script_repr.t × option Lazy_storage_diff.diffs)
  : M? (Raw_context.t × Migration_repr.origination_result) :=
  let? ctxt := Contract_storage.raw_originate ctxt true address_hash script in
  let address := Contract_repr.Originated address_hash in
  let? size_value := Contract_storage.used_storage_space ctxt address in
  let? '(ctxt, _, origination_updates) :=
    Fees_storage.burn_origination_fees (Some Receipt_repr.Protocol_migration)
      ctxt (Z.of_int64 Int64.max_int)
      (Token.Source_infinite Token.Liquidity_baking_subsidies) in
  let? '(ctxt, _, storage_updates) :=
    Fees_storage.burn_storage_fees (Some Receipt_repr.Protocol_migration) ctxt
      (Z.of_int64 Int64.max_int)
      (Token.Source_infinite Token.Liquidity_baking_subsidies) size_value in
  let? '(ctxt, transfer_updates) :=
    Token.transfer (Some Receipt_repr.Protocol_migration) ctxt
      (Token.Source_infinite Token.Liquidity_baking_subsidies)
      (Token.Sink_container (Token.Contract address)) balance in
  let balance_updates :=
    Pervasives.op_at origination_updates
      (Pervasives.op_at storage_updates transfer_updates) in
  let result_value :=
    {| Migration_repr.origination_result.balance_updates := balance_updates;
      Migration_repr.origination_result.originated_contracts :=
        [ address_hash ];
      Migration_repr.origination_result.storage_size := size_value;
      Migration_repr.origination_result.paid_storage_size_diff := size_value; |}
    in
  return? (ctxt, result_value).

Definition originate_test_fa12
  (typecheck :
    Raw_context.t → Script_repr.t →
    M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  (ctxt : Raw_context.t) (admin : Signature.public_key_hash)
  : M?
    (Raw_context.t × Contract_hash.t × list Migration_repr.origination_result) :=
  let? '(ctxt, fa12_address) :=
    Contract_storage.fresh_contract_from_current_nonce ctxt in
  let script :=
    {|
      Script_repr.t.code :=
        Script_repr.lazy_expr_value Liquidity_baking_lqt.script;
      Script_repr.t.storage :=
        test_fa12_init_storage
          (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.to_b58check)
            admin); |} in
  let? '(script, ctxt) := typecheck ctxt script in
  let? '(ctxt, origination_result) :=
    originate ctxt fa12_address (Tez_repr.of_mutez_exn 1000000) script in
  return? (ctxt, fa12_address, [ origination_result ]).

Definition first_bootstrap_account : Signature.public_key_hash :=
  Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
    (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.of_b58check_exn)
      "edpkuBknW28nW72KG6RoHtYW7p12T6GKc7nAbwYX5m8Wd9sDVC9yav").

Definition check_tzBTC {A : Set}
  (typecheck :
    Raw_context.t → Script_repr.t →
    M? ((Script_repr.t × option Lazy_storage_diff.diffs) × Raw_context.t))
  (current_level : int32) (ctxt : Raw_context.t)
  (f_value :
    Raw_context.t → Contract_hash.t →
    list Migration_repr.origination_result → M? (Raw_context.t × list A))
  : M? (Raw_context.t × list A) :=
  let function_parameter :=
    Contract_storage._exists ctxt
      (Contract_repr.Originated mainnet_tzBTC_address) in
  match function_parameter with
  | true ⇒ f_value ctxt mainnet_tzBTC_address nil
  | false ⇒
    if current_level <i32 1437862 then
      let? '(ctxt, token_address, token_result) :=
        originate_test_fa12 typecheck ctxt first_bootstrap_account in
      f_value ctxt token_address token_result
    else
      return? (ctxt, nil)
  end.

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))
  : M? (Raw_context.t × list Migration_repr.origination_result) :=
  let nonce_value := Operation_hash.hash_string None [ "Drip, drip, drip." ] in
  let ctxt := Raw_context.init_origination_nonce ctxt nonce_value in
  let? ctxt :=
    Storage.Liquidity_baking.Toggle_ema.(Storage_sigs.Single_data_storage.init_value)
      ctxt 0 in
  let current_level :=
    Raw_level_repr.to_int32 (Level_storage.current ctxt).(Level_repr.t.level) in
  let? '(ctxt, cpmm_address) :=
    Contract_storage.fresh_contract_from_current_nonce ctxt in
  let? '(ctxt, lqt_address) :=
    Contract_storage.fresh_contract_from_current_nonce ctxt in
  let? ctxt :=
    Storage.Liquidity_baking.Cpmm_address.(Storage_sigs.Single_data_storage.init_value)
      ctxt cpmm_address in
  check_tzBTC typecheck current_level ctxt
    (fun (ctxt : Raw_context.t) ⇒
      fun (token_address : Contract_hash.t) ⇒
        fun (token_result : list Migration_repr.origination_result) ⇒
          let cpmm_script :=
            {|
              Script_repr.t.code :=
                Script_repr.lazy_expr_value Liquidity_baking_cpmm.script;
              Script_repr.t.storage :=
                cpmm_init_storage (Contract_hash.to_b58check token_address)
                  (Contract_hash.to_b58check lqt_address); |} in
          let? '(cpmm_script, ctxt) := typecheck ctxt cpmm_script in
          let lqt_script :=
            {|
              Script_repr.t.code :=
                Script_repr.lazy_expr_value Liquidity_baking_lqt.script;
              Script_repr.t.storage :=
                lqt_init_storage (Contract_hash.to_b58check cpmm_address); |} in
          let? '(lqt_script, ctxt) := typecheck ctxt lqt_script in
          let? '(ctxt, cpmm_result) :=
            originate ctxt cpmm_address (Tez_repr.of_mutez_exn 100) cpmm_script
            in
          let? '(ctxt, lqt_result) :=
            originate ctxt lqt_address Tez_repr.zero lqt_script in
          let ctxt := Raw_context.unset_origination_nonce ctxt in
          return?
            (ctxt, (Pervasives.op_at [ cpmm_result; lqt_result ] token_result))).