Skip to main content

✒️ Contract_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "contract.balance_too_low" "Balance too low"
      "An operation tried to spend more tokens than the contract has"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Contract_repr.contract × Tez_repr.t × Tez_repr.t) ⇒
            let '(c_value, b_value, a_value) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Balance of contract "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " too low ("
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal ") to spend "
                          (CamlinternalFormatBasics.Alpha
                            CamlinternalFormatBasics.End_of_format))))))
                "Balance of contract %a too low (%a) to spend %a")
              Contract_repr.pp c_value Tez_repr.pp b_value Tez_repr.pp a_value))
      (Data_encoding.obj3
        (Data_encoding.req None None "contract" Contract_repr.encoding)
        (Data_encoding.req None None "balance" Tez_repr.encoding)
        (Data_encoding.req None None "amount" Tez_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Balance_too_low" then
            let '(c_value, b_value, a_value) :=
              cast (Contract_repr.contract × Tez_repr.t × Tez_repr.t) payload in
            Some (c_value, b_value, a_value)
          else None
        end)
      (fun (function_parameter :
        Contract_repr.contract × Tez_repr.t × Tez_repr.t) ⇒
        let '(c_value, b_value, a_value) := function_parameter in
        Build_extensible "Balance_too_low"
          (Contract_repr.contract × Tez_repr.t × Tez_repr.t)
          (c_value, b_value, a_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "contract.counter_in_the_future"
      "Invalid counter (not yet reached) in a manager operation"
      "An operation assumed a contract counter in the future"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Contract_repr.contract × Z.t × Z.t) ⇒
            let '(contract, exp, found) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Counter "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " not yet reached for contract "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal " (expected "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ")" % char
                              CamlinternalFormatBasics.End_of_format)))))))
                "Counter %a not yet reached for contract %a (expected %a)")
              Z.pp_print found Contract_repr.pp contract Z.pp_print exp))
      (Data_encoding.obj3
        (Data_encoding.req None None "contract" Contract_repr.encoding)
        (Data_encoding.req None None "expected" Data_encoding.z_value)
        (Data_encoding.req None None "found" Data_encoding.z_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Counter_in_the_future" then
            let '(c_value, x_value, y_value) :=
              cast (Contract_repr.contract × Z.t × Z.t) payload in
            Some (c_value, x_value, y_value)
          else None
        end)
      (fun (function_parameter : Contract_repr.contract × Z.t × Z.t) ⇒
        let '(c_value, x_value, y_value) := function_parameter in
        Build_extensible "Counter_in_the_future"
          (Contract_repr.contract × Z.t × Z.t) (c_value, x_value, y_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "contract.counter_in_the_past"
      "Invalid counter (already used) in a manager operation"
      "An operation assumed a contract counter in the past"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Contract_repr.contract × Z.t × Z.t) ⇒
            let '(contract, exp, found) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Counter "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal
                      " already used for contract "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal " (expected "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal ")" % char
                              CamlinternalFormatBasics.End_of_format)))))))
                "Counter %a already used for contract %a (expected %a)")
              Z.pp_print found Contract_repr.pp contract Z.pp_print exp))
      (Data_encoding.obj3
        (Data_encoding.req None None "contract" Contract_repr.encoding)
        (Data_encoding.req None None "expected" Data_encoding.z_value)
        (Data_encoding.req None None "found" Data_encoding.z_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Counter_in_the_past" then
            let '(c_value, x_value, y_value) :=
              cast (Contract_repr.contract × Z.t × Z.t) payload in
            Some (c_value, x_value, y_value)
          else None
        end)
      (fun (function_parameter : Contract_repr.contract × Z.t × Z.t) ⇒
        let '(c_value, x_value, y_value) := function_parameter in
        Build_extensible "Counter_in_the_past"
          (Contract_repr.contract × Z.t × Z.t) (c_value, x_value, y_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "contract.non_existing_contract" "Non existing contract"
      "A contract handle is not present in the context (either it never was or it has been destroyed)"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (contract : Contract_repr.contract) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Contract "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " does not exist"
                      CamlinternalFormatBasics.End_of_format)))
                "Contract %a does not exist") Contract_repr.pp contract))
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Contract_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Non_existing_contract" then
            let c_value := cast Contract_repr.contract payload in
            Some c_value
          else None
        end)
      (fun (c_value : Contract_repr.contract) ⇒
        Build_extensible "Non_existing_contract" Contract_repr.contract c_value)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "contract.manager.inconsistent_public_key" "Inconsistent public key"
      "A provided manager public key is different with the public key stored in the contract"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : Signature.public_key × Signature.public_key)
            ⇒
            let '(eh, ph) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Expected manager public key "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.String_literal " but "
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal " was provided"
                          CamlinternalFormatBasics.End_of_format)))))
                "Expected manager public key %s but %s was provided")
              (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) ph)
              (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) eh)))
      (Data_encoding.obj2
        (Data_encoding.req None None "public_key"
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
        (Data_encoding.req None None "expected_public_key"
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inconsistent_public_key" then
            let '(eh, ph) :=
              cast (Signature.public_key × Signature.public_key) payload in
            Some (eh, ph)
          else None
        end)
      (fun (function_parameter : Signature.public_key × Signature.public_key) ⇒
        let '(eh, ph) := function_parameter in
        Build_extensible "Inconsistent_public_key"
          (Signature.public_key × Signature.public_key) (eh, ph)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent "contract.failure"
      "Contract storage failure" "Unexpected contract storage error"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (s_value : string) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Contract_storage.Failure "
                  (CamlinternalFormatBasics.Caml_string
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format))
                "Contract_storage.Failure %S") s_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "message" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Failure" then
            let s_value := cast string payload in
            Some s_value
          else None
        end)
      (fun (s_value : string) ⇒ Build_extensible "Failure" string s_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "implicit.empty_implicit_contract" "Empty implicit contract"
      "No manager operations are allowed on an empty implicit contract."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (implicit : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Empty implicit contract ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                "Empty implicit contract (%a)")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              implicit))
      (Data_encoding.obj1
        (Data_encoding.req None None "implicit"
          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 "Empty_implicit_contract" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "Empty_implicit_contract" Signature.public_key_hash
          c_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "implicit.empty_implicit_delegated_contract"
      "Empty implicit delegated contract"
      "Emptying an implicit delegated account is not allowed."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (implicit : Signature.public_key_hash) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Emptying implicit delegated contract ("
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                "Emptying implicit delegated contract (%a)")
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
              implicit))
      (Data_encoding.obj1
        (Data_encoding.req None None "implicit"
          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 "Empty_implicit_delegated_contract" then
            let c_value := cast Signature.public_key_hash payload in
            Some c_value
          else None
        end)
      (fun (c_value : Signature.public_key_hash) ⇒
        Build_extensible "Empty_implicit_delegated_contract"
          Signature.public_key_hash c_value) in
  Error_monad.register_error_kind Error_monad.Permanent
    "frozen_bonds.must_be_spent_at_once" "Partial spending of frozen bonds"
    "Frozen bonds must be spent at once."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : Contract_repr.contract × Bond_id_repr.t) ⇒
          let '(contract, bond_id) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The frozen funds for contract ("
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal ") and bond ("
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.String_literal
                        ") are not allowed to be partially withdrawn. The amount withdrawn must be equal to the entire deposit for the said bond."
                        CamlinternalFormatBasics.End_of_format)))))
              "The frozen funds for contract (%a) and bond (%a) are not allowed to be partially withdrawn. The amount withdrawn must be equal to the entire deposit for the said bond.")
            Contract_repr.pp contract Bond_id_repr.pp bond_id))
    (Data_encoding.obj2
      (Data_encoding.req None None "contract" Contract_repr.encoding)
      (Data_encoding.req None None "bond_id" Bond_id_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Frozen_bonds_must_be_spent_at_once" then
          let '(c_value, b_value) :=
            cast (Contract_repr.t × Bond_id_repr.t) payload in
          Some (c_value, b_value)
        else None
      end)
    (fun (function_parameter : Contract_repr.contract × Bond_id_repr.t) ⇒
      let '(c_value, b_value) := function_parameter in
      Build_extensible "Frozen_bonds_must_be_spent_at_once"
        (Contract_repr.contract × Bond_id_repr.t) (c_value, b_value)).

Definition failwith {A : Set} (msg : string) : M? A :=
  Error_monad.fail (Build_extensible "Failure" string msg).

Module Legacy_big_map_diff.
Records for the constructor parameters
  Module ConstructorRecords_item.
    Module item.
      Module Update.
        Record record {big_map diff_key diff_key_hash diff_value : Set} : Set := Build {
          big_map : big_map;
          diff_key : diff_key;
          diff_key_hash : diff_key_hash;
          diff_value : diff_value;
        }.
        Arguments record : clear implicits.
        Definition with_big_map
          {t_big_map t_diff_key t_diff_key_hash t_diff_value} big_map
          (r : record t_big_map t_diff_key t_diff_key_hash t_diff_value) :=
          Build t_big_map t_diff_key t_diff_key_hash t_diff_value big_map
            r.(diff_key) r.(diff_key_hash) r.(diff_value).
        Definition with_diff_key
          {t_big_map t_diff_key t_diff_key_hash t_diff_value} diff_key
          (r : record t_big_map t_diff_key t_diff_key_hash t_diff_value) :=
          Build t_big_map t_diff_key t_diff_key_hash t_diff_value r.(big_map)
            diff_key r.(diff_key_hash) r.(diff_value).
        Definition with_diff_key_hash
          {t_big_map t_diff_key t_diff_key_hash t_diff_value} diff_key_hash
          (r : record t_big_map t_diff_key t_diff_key_hash t_diff_value) :=
          Build t_big_map t_diff_key t_diff_key_hash t_diff_value r.(big_map)
            r.(diff_key) diff_key_hash r.(diff_value).
        Definition with_diff_value
          {t_big_map t_diff_key t_diff_key_hash t_diff_value} diff_value
          (r : record t_big_map t_diff_key t_diff_key_hash t_diff_value) :=
          Build t_big_map t_diff_key t_diff_key_hash t_diff_value r.(big_map)
            r.(diff_key) r.(diff_key_hash) diff_value.
      End Update.
      Definition Update_skeleton := Update.record.

      Module Copy.
        Record record {src dst : Set} : Set := Build {
          src : src;
          dst : dst;
        }.
        Arguments record : clear implicits.
        Definition with_src {t_src t_dst} src (r : record t_src t_dst) :=
          Build t_src t_dst src r.(dst).
        Definition with_dst {t_src t_dst} dst (r : record t_src t_dst) :=
          Build t_src t_dst r.(src) dst.
      End Copy.
      Definition Copy_skeleton := Copy.record.

      Module Alloc.
        Record record {big_map key_type value_type : Set} : Set := Build {
          big_map : big_map;
          key_type : key_type;
          value_type : value_type;
        }.
        Arguments record : clear implicits.
        Definition with_big_map {t_big_map t_key_type t_value_type} big_map
          (r : record t_big_map t_key_type t_value_type) :=
          Build t_big_map t_key_type t_value_type big_map r.(key_type)
            r.(value_type).
        Definition with_key_type {t_big_map t_key_type t_value_type} key_type
          (r : record t_big_map t_key_type t_value_type) :=
          Build t_big_map t_key_type t_value_type r.(big_map) key_type
            r.(value_type).
        Definition with_value_type {t_big_map t_key_type t_value_type}
          value_type (r : record t_big_map t_key_type t_value_type) :=
          Build t_big_map t_key_type t_value_type r.(big_map) r.(key_type)
            value_type.
      End Alloc.
      Definition Alloc_skeleton := Alloc.record.
    End item.
  End ConstructorRecords_item.
  Import ConstructorRecords_item.

  Reserved Notation "'item.Update".
  Reserved Notation "'item.Copy".
  Reserved Notation "'item.Alloc".

  Inductive item : Set :=
  | Update : 'item.Update item
  | Clear : Z.t item
  | Copy : 'item.Copy item
  | Alloc : 'item.Alloc item
  
  where "'item.Update" :=
    (item.Update_skeleton Z.t Script_repr.expr Script_expr_hash.t
      (option Script_repr.expr))
  and "'item.Copy" := (item.Copy_skeleton Z.t Z.t)
  and "'item.Alloc" :=
    (item.Alloc_skeleton Z.t Script_repr.expr Script_repr.expr).

  Module item.
    Include ConstructorRecords_item.item.
    Definition Update := 'item.Update.
    Definition Copy := 'item.Copy.
    Definition Alloc := 'item.Alloc.
  End item.

  Definition t : Set := list item.

  Definition item_encoding : Data_encoding.encoding item :=
    Data_encoding.union None
      [
        Data_encoding.case_value "update" None (Data_encoding.Tag 0)
          (Data_encoding.obj5
            (Data_encoding.req None None "action"
              (Data_encoding.constant "update"))
            (Data_encoding.req None None "big_map" Data_encoding.z_value)
            (Data_encoding.req None None "key_hash"
              Script_expr_hash.encoding)
            (Data_encoding.req None None "key" Script_repr.expr_encoding)
            (Data_encoding.opt None None "value"
              Script_repr.expr_encoding))
          (fun (function_parameter : item) ⇒
            match function_parameter with
            |
              Update {|
                item.Update.big_map := big_map;
                  item.Update.diff_key := diff_key;
                  item.Update.diff_key_hash := diff_key_hash;
                  item.Update.diff_value := diff_value
                  |} ⇒
              Some
                (tt, big_map, diff_key_hash, diff_key,
                  diff_value)
            | _None
            end)
          (fun (function_parameter :
            unit × Z.t × Script_expr_hash.t × Script_repr.expr ×
              option Script_repr.expr) ⇒
            let '(_, big_map, diff_key_hash, diff_key, diff_value) :=
              function_parameter in
            Update
              {| item.Update.big_map := big_map;
                item.Update.diff_key := diff_key;
                item.Update.diff_key_hash := diff_key_hash;
                item.Update.diff_value := diff_value; |});
        Data_encoding.case_value "remove" None (Data_encoding.Tag 1)
          (Data_encoding.obj2
            (Data_encoding.req None None "action"
              (Data_encoding.constant "remove"))
            (Data_encoding.req None None "big_map" Data_encoding.z_value))
          (fun (function_parameter : item) ⇒
            match function_parameter with
            | Clear big_mapSome (tt, big_map)
            | _None
            end)
          (fun (function_parameter : unit × Z.t) ⇒
            let '(_, big_map) := function_parameter in
            Clear big_map);
        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_big_map"
              Data_encoding.z_value)
            (Data_encoding.req None None "destination_big_map"
              Data_encoding.z_value))
          (fun (function_parameter : item) ⇒
            match function_parameter with
            | Copy {| item.Copy.src := src; item.Copy.dst := dst |} ⇒
              Some (tt, src, dst)
            | _None
            end)
          (fun (function_parameter : unit × Z.t × Z.t) ⇒
            let '(_, src, dst) := function_parameter in
            Copy {| item.Copy.src := src; item.Copy.dst := dst; |});
        Data_encoding.case_value "alloc" None (Data_encoding.Tag 3)
          (Data_encoding.obj4
            (Data_encoding.req None None "action"
              (Data_encoding.constant "alloc"))
            (Data_encoding.req None None "big_map" Data_encoding.z_value)
            (Data_encoding.req None None "key_type"
              Script_repr.expr_encoding)
            (Data_encoding.req None None "value_type"
              Script_repr.expr_encoding))
          (fun (function_parameter : item) ⇒
            match function_parameter with
            |
              Alloc {|
                item.Alloc.big_map := big_map;
                  item.Alloc.key_type := key_type;
                  item.Alloc.value_type := value_type
                  |} ⇒
              Some (tt, big_map, key_type, value_type)
            | _None
            end)
          (fun (function_parameter :
            unit × Z.t × Script_repr.expr × Script_repr.expr) ⇒
            let '(_, big_map, key_type, value_type) :=
              function_parameter in
            Alloc
              {| item.Alloc.big_map := big_map;
                item.Alloc.key_type := key_type;
                item.Alloc.value_type := value_type; |})
      ].

  Definition encoding : Data_encoding.encoding (list item) :=
    Data_encoding.list_value None item_encoding.

  Definition to_lazy_storage_diff (legacy_diffs : list item)
    : list Lazy_storage_diff.diffs_item :=
    let rev_head {A B C D : Set}
      (diffs : list (A × Lazy_storage_diff.diff B C (list D)))
      : list (A × Lazy_storage_diff.diff B C (list D)) :=
      match diffs with
      | []nil
      | cons (_, Lazy_storage_diff.Remove) _diffs
      |
        cons
          (id,
            Lazy_storage_diff.Update {|
              Lazy_storage_diff.diff.Update.init := init_value;
                Lazy_storage_diff.diff.Update.updates := updates
                |}) rest
        cons
          (id,
            (Lazy_storage_diff.Update
              {| Lazy_storage_diff.diff.Update.init := init_value;
                Lazy_storage_diff.diff.Update.updates := List.rev updates; |}))
          rest
      end in
    List.rev_map
      (fun (function_parameter :
        Z.t ×
          Lazy_storage_diff.diff
            Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)
            Lazy_storage_kind.Big_map.alloc Lazy_storage_kind.Big_map.updates)
        ⇒
        let '(id, diff_value) := function_parameter in
        let id :=
          Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.of_legacy_USE_ONLY_IN_Legacy_big_map_diff)
            id in
        Lazy_storage_diff.make Lazy_storage_kind.Big_map id diff_value)
      (rev_head
        (List.fold_left
          (fun (new_diff :
            list
              (Z.t ×
                Lazy_storage_diff.diff
                  Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)
                  Lazy_storage_kind.Big_map.alloc
                  Lazy_storage_kind.Big_map.updates)) ⇒
            fun (item : item) ⇒
              match item with
              | Clear id
                cons (id, Lazy_storage_diff.Remove) (rev_head new_diff)
              | Copy {| item.Copy.src := src; item.Copy.dst := dst |} ⇒
                let src :=
                  Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.of_legacy_USE_ONLY_IN_Legacy_big_map_diff)
                    src in
                cons
                  (dst,
                    (Lazy_storage_diff.Update
                      {|
                        Lazy_storage_diff.diff.Update.init :=
                          Lazy_storage_diff.Copy
                            {| Lazy_storage_diff.init.Copy.src := src; |};
                        Lazy_storage_diff.diff.Update.updates := nil; |}))
                  (rev_head new_diff)
              |
                Alloc {|
                  item.Alloc.big_map := big_map;
                    item.Alloc.key_type := key_type;
                    item.Alloc.value_type := value_type
                    |} ⇒
                cons
                  (big_map,
                    (Lazy_storage_diff.Update
                      {|
                        Lazy_storage_diff.diff.Update.init :=
                          Lazy_storage_diff.Alloc
                            {|
                              Lazy_storage_kind.Big_map.alloc.key_type :=
                                key_type;
                              Lazy_storage_kind.Big_map.alloc.value_type :=
                                value_type; |};
                        Lazy_storage_diff.diff.Update.updates := nil; |}))
                  (rev_head new_diff)
              |
                Update {|
                  item.Update.big_map := big_map;
                    item.Update.diff_key := key_value;
                    item.Update.diff_key_hash := key_hash;
                    item.Update.diff_value := value_value
                    |} ⇒
                match
                  (new_diff,
                    match new_diff with
                    | cons (id, diff_value) restid =Z big_map
                    | _false
                    end) with
                | (cons (id, diff_value) rest, true)
                  let diff_value :=
                    match diff_value with
                    | Lazy_storage_diff.Remove
                      (* ❌ Assert instruction is not handled. *)
                      assert
                        (Lazy_storage_diff.diff
                          Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t)
                          Lazy_storage_kind.Big_map.alloc
                          (list Lazy_storage_kind.Big_map.update)) false
                    |
                      Lazy_storage_diff.Update {|
                        Lazy_storage_diff.diff.Update.init := init_value;
                          Lazy_storage_diff.diff.Update.updates := updates
                          |} ⇒
                      let updates :=
                        cons
                          {| Lazy_storage_kind.Big_map.update.key := key_value;
                            Lazy_storage_kind.Big_map.update.key_hash :=
                              key_hash;
                            Lazy_storage_kind.Big_map.update.value :=
                              value_value; |} updates in
                      Lazy_storage_diff.Update
                        {| Lazy_storage_diff.diff.Update.init := init_value;
                          Lazy_storage_diff.diff.Update.updates := updates; |}
                    end in
                  cons (id, diff_value) rest
                | (new_diff, _)
                  let updates :=
                    [
                      {| Lazy_storage_kind.Big_map.update.key := key_value;
                        Lazy_storage_kind.Big_map.update.key_hash
                          := key_hash;
                        Lazy_storage_kind.Big_map.update.value
                          := value_value; |}
                    ] in
                  cons
                    (big_map,
                      (Lazy_storage_diff.Update
                        {|
                          Lazy_storage_diff.diff.Update.init :=
                            Lazy_storage_diff.Existing;
                          Lazy_storage_diff.diff.Update.updates := updates; |}))
                    (rev_head new_diff)
                end
              end) nil legacy_diffs)).

  Axiom of_lazy_storage_diff : list Lazy_storage_diff.diffs_item list item.
End Legacy_big_map_diff.

Definition update_script_lazy_storage
  (c_value : Raw_context.t)
  (function_parameter : option Lazy_storage_diff.diffs)
  : M? (Raw_context.t × Z.t) :=
  match function_parameter with
  | Nonereturn? (c_value, Z.zero)
  | Some diffsLazy_storage_diff.apply c_value diffs
  end.

Definition create_base
  (c_value : Raw_context.t) (prepaid_bootstrap_storage : bool)
  (contract : Contract_repr.contract) (balance : Tez_repr.t)
  (manager : option Signature.public_key_hash)
  (script : option (Script_repr.t × option Lazy_storage_diff.diffs))
  (function_parameter : unit) : M? Raw_context.t :=
  let '_ := function_parameter in
  let? c_value :=
    match Contract_repr.is_implicit contract with
    | Nonereturn? c_value
    | Some _
      let? counter :=
        Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.get)
          c_value in
      Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.init_value)
        c_value contract counter
    end in
  let? c_value :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.init_value)
      c_value contract balance in
  let? c_value :=
    match manager with
    | Some manager
      Contract_manager_storage.init_value c_value contract
        (Manager_repr.Hash manager)
    | Nonereturn? c_value
    end in
  match script with
  |
    Some
      ({| Script_repr.t.code := code; Script_repr.t.storage := storage_value |},
        lazy_storage_diff)
    let? '(c_value, code_size) :=
      Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        c_value contract code in
    let? '(c_value, storage_size) :=
      Storage.Contract.Storage.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        c_value contract storage_value in
    let? '(c_value, lazy_storage_size) :=
      update_script_lazy_storage c_value lazy_storage_diff in
    let total_size :=
      ((Z.of_int code_size) +Z (Z.of_int storage_size)) +Z lazy_storage_size in
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (total_size Z Z.zero) in
    let prepaid_bootstrap_storage :=
      if prepaid_bootstrap_storage then
        total_size
      else
        Z.zero in
    let? c_value :=
      Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.init_value)
        c_value contract prepaid_bootstrap_storage in
    Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.init_value)
      c_value contract total_size
  | Nonereturn? c_value
  end.

Definition raw_originate
  (c_value : Raw_context.t) (prepaid_bootstrap_storage : bool)
  (contract : Contract_repr.contract)
  (script : Script_repr.t × option Lazy_storage_diff.diffs)
  : M? Raw_context.t :=
  create_base c_value prepaid_bootstrap_storage contract Tez_repr.zero None
    (Some script) tt.

Definition create_implicit
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  (balance : Tez_repr.t) : M? Raw_context.t :=
  create_base c_value false (Contract_repr.implicit_contract manager) balance
    (Some manager) None tt.

Definition delete (c_value : Raw_context.t) (contract : Contract_repr.contract)
  : M? Raw_context.t :=
  match Contract_repr.is_implicit contract with
  | Nonefailwith "Non implicit contracts cannot be removed"
  | Some _
    let? c_value := Contract_delegate_storage.unlink c_value contract in
    let? c_value :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.remove_existing)
        c_value contract in
    let? c_value := Contract_manager_storage.remove_existing c_value contract in
    let? c_value :=
      Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.remove_existing)
        c_value contract in
    let? '(c_value, _, _) :=
      Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        c_value contract in
    let? '(c_value, _, _) :=
      Storage.Contract.Storage.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
        c_value contract in
    let c_value :=
      Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.remove)
        c_value contract in
    Error_monad.op_gtpipeeq
      (Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.remove)
        c_value contract) Error_monad.ok
  end.

Definition allocated (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M? bool :=
  let? function_parameter :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.find)
      c_value contract in
  match function_parameter with
  | NoneError_monad.return_false
  | Some _Error_monad.return_true
  end.

Definition _exists (c_value : Raw_context.t) (contract : Contract_repr.contract)
  : M? bool :=
  match Contract_repr.is_implicit contract with
  | Some _Error_monad.return_true
  | Noneallocated c_value contract
  end.

Definition must_exist
  (c_value : Raw_context.t) (contract : Contract_repr.contract) : M? unit :=
  let? function_parameter := _exists c_value contract in
  match function_parameter with
  | trueError_monad.return_unit
  | false
    Error_monad.fail
      (Build_extensible "Non_existing_contract" Contract_repr.contract contract)
  end.

Definition must_be_allocated
  (c_value : Raw_context.t) (contract : Contract_repr.t) : M? unit :=
  let? function_parameter := allocated c_value contract in
  match function_parameter with
  | trueError_monad.return_unit
  | false
    match Contract_repr.is_implicit contract with
    | Some pkh
      Error_monad.fail
        (Build_extensible "Empty_implicit_contract" Signature.public_key_hash
          pkh)
    | None
      Error_monad.fail
        (Build_extensible "Non_existing_contract" Contract_repr.t contract)
    end
  end.

Definition list_value (c_value : Raw_context.t) : list Contract_repr.t :=
  Storage.Contract.list_value c_value.

Definition fresh_contract_from_current_nonce (c_value : Raw_context.t)
  : M? (Raw_context.t × Contract_repr.contract) :=
  let? '(c_value, nonce_value) :=
    Raw_context.increment_origination_nonce c_value in
  return? (c_value, (Contract_repr.originated_contract nonce_value)).

Definition originated_from_current_nonce
  (ctxt_since : Raw_context.t) (ctxt_until : Raw_context.t)
  : M? (list Contract_repr.contract) :=
  let? since := Raw_context.get_origination_nonce ctxt_since in
  let? until := Raw_context.get_origination_nonce ctxt_until in
  List.filter_es
    (fun (contract : Contract_repr.contract) ⇒ _exists ctxt_until contract)
    (Contract_repr.originated_contracts since until).

Definition check_counter_increment
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  (counter : Z.t) : M? unit :=
  let contract := Contract_repr.implicit_contract manager in
  let? contract_counter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.get) c_value
      contract in
  let expected := Z.succ contract_counter in
  if expected =Z counter then
    Error_monad.return_unit
  else
    if expected >Z counter then
      Error_monad.fail
        (Build_extensible "Counter_in_the_past"
          (Contract_repr.contract × Z.t × Z.t) (contract, expected, counter))
    else
      Error_monad.fail
        (Build_extensible "Counter_in_the_future"
          (Contract_repr.contract × Z.t × Z.t) (contract, expected, counter)).

Definition increment_counter
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  : M? Raw_context.t :=
  let contract := Contract_repr.implicit_contract manager in
  let? global_counter :=
    Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.get)
      c_value in
  let? c_value :=
    Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.update)
      c_value (Z.succ global_counter) in
  let? contract_counter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.get) c_value
      contract in
  Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.update) c_value
    contract (Z.succ contract_counter).

Definition get_script_code
  (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M? (Raw_context.t × option Script_repr.lazy_expr) :=
  Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
    c_value contract.

Definition get_script (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M? (Raw_context.t × option Script_repr.t) :=
  let? '(c_value, code) :=
    Storage.Contract.Code.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      c_value contract in
  let? '(c_value, storage_value) :=
    Storage.Contract.Storage.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      c_value contract in
  match (code, storage_value) with
  | (None, None)return? (c_value, None)
  | (Some code, Some storage_value)
    return?
      (c_value,
        (Some
          {| Script_repr.t.code := code; Script_repr.t.storage := storage_value;
            |}))
  | ((None, Some _) | (Some _, None)) ⇒ failwith "get_script"
  end.

Definition get_storage (ctxt : Raw_context.t) (contract : Contract_repr.t)
  : M? (Raw_context.t × option Script_repr.expr) :=
  let? function_parameter :=
    Storage.Contract.Storage.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt contract in
  match function_parameter with
  | (ctxt, None)return? (ctxt, None)
  | (ctxt, Some storage_value)
    let? ctxt :=
      Raw_context.consume_gas ctxt (Script_repr.force_decode_cost storage_value)
      in
    let? storage_value := Script_repr.force_decode storage_value in
    return? (ctxt, (Some storage_value))
  end.

Definition get_counter
  (c_value : Raw_context.t) (manager : Signature.public_key_hash) : M? Z.t :=
  let contract := Contract_repr.implicit_contract manager in
  let? function_parameter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage.find) c_value
      contract in
  match function_parameter with
  | None
    match Contract_repr.is_implicit contract with
    | Some _
      Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.get)
        c_value
    | Nonefailwith "get_counter"
    end
  | Some v_valuereturn? v_value
  end.

Definition get_balance (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M? Tez_repr.t :=
  let? function_parameter :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.find)
      c_value contract in
  match function_parameter with
  | None
    match Contract_repr.is_implicit contract with
    | Some _return? Tez_repr.zero
    | Nonefailwith "get_balance"
    end
  | Some v_valuereturn? v_value
  end.

Definition get_balance_carbonated
  (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M? (Raw_context.t × Tez_repr.t) :=
  let? c_value :=
    Raw_context.consume_gas c_value (Storage_costs.read_access 4 8) in
  let? balance := get_balance c_value contract in
  return? (c_value, balance).

Definition update_script_storage
  (c_value : Raw_context.t) (contract : Contract_repr.t)
  (storage_value : Script_repr.expr)
  (lazy_storage_diff : option Lazy_storage_diff.diffs) : M? Raw_context.t :=
  let storage_value := Script_repr.lazy_expr_value storage_value in
  let? '(c_value, lazy_storage_size_diff) :=
    update_script_lazy_storage c_value lazy_storage_diff in
  let? '(c_value, size_diff) :=
    Storage.Contract.Storage.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      c_value contract storage_value in
  let? previous_size :=
    Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.get)
      c_value contract in
  let new_size :=
    previous_size +Z (lazy_storage_size_diff +Z (Z.of_int size_diff)) in
  Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.update)
    c_value contract new_size.

Definition spend_only_call_from_token
  (c_value : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
  : M? Raw_context.t :=
  let? balance :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.find)
      c_value contract in
  let balance := Option.value_value balance Tez_repr.zero in
  match Tez_repr.op_minusquestion balance amount with
  | Pervasives.Error _
    Error_monad.fail
      (Build_extensible "Balance_too_low"
        (Contract_repr.t × Tez_repr.t × Tez_repr.t) (contract, balance, amount))
  | Pervasives.Ok new_balance
    let? c_value :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.update)
        c_value contract new_balance in
    let? c_value := Stake_storage.remove_contract_stake c_value contract amount
      in
    if Tez_repr.op_gt new_balance Tez_repr.zero then
      return? c_value
    else
      match Contract_repr.is_implicit contract with
      | Nonereturn? c_value
      | Some pkh
        let? function_parameter :=
          Contract_delegate_storage.find c_value contract in
        match function_parameter with
        | Some pkh'
          if
            Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) pkh
              pkh'
          then
            return? c_value
          else
            Error_monad.fail
              (Build_extensible "Empty_implicit_delegated_contract"
                Signature.public_key_hash pkh)
        | Nonereturn? c_value
        end
      end
  end.

Definition credit_only_call_from_token
  (c_value : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
  : M? Raw_context.t :=
  let? function_parameter :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.find)
      c_value contract in
  match function_parameter with
  | None
    match Contract_repr.is_implicit contract with
    | None
      Error_monad.fail
        (Build_extensible "Non_existing_contract" Contract_repr.t contract)
    | Some managercreate_implicit c_value manager amount
    end
  | Some balance
    let? balance := Tez_repr.op_plusquestion amount balance in
    let? c_value :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.update)
        c_value contract balance in
    Stake_storage.add_contract_stake c_value contract amount
  end.

Definition init_value (c_value : Raw_context.t) : M? Raw_context.t :=
  let? c_value :=
    Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.init_value)
      c_value Z.zero in
  Lazy_storage_diff.init_value c_value.

Definition used_storage_space
  (c_value : Raw_context.t) (contract : Contract_repr.t) : M? Z.t :=
  Error_monad.op_gtpipeeqquestion
    (Storage.Contract.Used_storage_space.(Storage_sigs.Indexed_data_storage.find)
      c_value contract) (fun x_1Option.value_value x_1 Z.zero).

Definition
  (c_value : Raw_context.t) (contract : Contract_repr.t) : M? Z.t :=
  Error_monad.op_gtpipeeqquestion
    (Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.find)
      c_value contract) (fun x_1Option.value_value x_1 Z.zero).

Definition set_paid_storage_space_and_return_fees_to_pay
  (c_value : Raw_context.t) (contract : Contract_repr.t)
  (new_storage_space : Z.t) : M? (Z.t × Raw_context.t) :=
  let? already_paid_space :=
    Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.get)
      c_value contract in
  if already_paid_space Z new_storage_space then
    return? (Z.zero, c_value)
  else
    let to_pay := new_storage_space -Z already_paid_space in
    let? c_value :=
      Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.update)
        c_value contract new_storage_space in
    return? (to_pay, c_value).

Definition update_balance {A : Set}
  (ctxt : Raw_context.t) (contract : Contract_repr.t)
  (f_value : Tez_repr.t A M? Tez_repr.t) (amount : A)
  : M? Raw_context.t :=
  let? balance :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.get)
      ctxt contract in
  let? new_balance := f_value balance amount in
  Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.update)
    ctxt contract new_balance.

Definition increase_balance_only_call_from_token
  (ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
  : M? Raw_context.t :=
  update_balance ctxt contract Tez_repr.op_plusquestion amount.

Definition decrease_balance_only_call_from_token
  (ctxt : Raw_context.t) (contract : Contract_repr.t) (amount : Tez_repr.t)
  : M? Raw_context.t :=
  update_balance ctxt contract Tez_repr.op_minusquestion amount.

Definition get_frozen_bonds (ctxt : Raw_context.t) (contract : Contract_repr.t)
  : M? Tez_repr.t :=
  Error_monad.op_gtpipeeqquestion
    (Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.find)
      ctxt contract) (fun x_1Option.value_value x_1 Tez_repr.zero).

Definition get_balance_and_frozen_bonds
  (ctxt : Raw_context.t) (contract : Contract_repr.t) : M? Tez_repr.t :=
  let? balance :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.get)
      ctxt contract in
  let? total_bonds := get_frozen_bonds ctxt contract in
  Tez_repr.op_plusquestion balance total_bonds.

Definition bond_allocated
  (ctxt : Raw_context.t) (contract : Contract_repr.t) (bond_id : Bond_id_repr.t)
  : M? (Raw_context.t × bool) :=
  Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
    (ctxt, contract) bond_id.

Definition find_bond
  (ctxt : Raw_context.t) (contract : Contract_repr.t) (bond_id : Bond_id_repr.t)
  : M? (Raw_context.t × option Tez_repr.t) :=
  Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
    (ctxt, contract) bond_id.

PRE : [amount > 0], fulfilled by unique caller [Token.transfer].
PRE : [amount > 0], fulfilled by unique caller [Token.transfer].
Definition credit_bond_only_call_from_token
  (ctxt : Raw_context.t) (contract : Contract_repr.t) (bond_id : Bond_id_repr.t)
  (amount : Tez_repr.t) : M? Raw_context.t :=
  let? '_ :=
    Error_monad.fail_when (Tez_repr.op_eq amount Tez_repr.zero)
      (Build_extensible "Failure" string "Expecting : [amount > 0]") in
  let? ctxt := Stake_storage.add_contract_stake ctxt contract amount in
  let? '(ctxt, _) :=
    let? '(ctxt, frozen_bonds_opt) :=
      Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
        (ctxt, contract) bond_id in
    match frozen_bonds_opt with
    | None
      Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
        (ctxt, contract) bond_id amount
    | Some frozen_bonds
      let? new_amount := Tez_repr.op_plusquestion frozen_bonds amount in
      Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
        (ctxt, contract) bond_id new_amount
    end in
  let? function_parameter :=
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.find)
      ctxt contract in
  match function_parameter with
  | None
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.init_value)
      ctxt contract amount
  | Some total
    let? new_total := Tez_repr.op_plusquestion total amount in
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.update)
      ctxt contract new_total
  end.

Definition has_frozen_bonds {A : Set}
  (ctxt : Raw_context.t) (contract : Contract_repr.t)
  : Pervasives.result bool A :=
  Error_monad.op_gtpipeeq
    (Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.mem)
      ctxt contract) Error_monad.ok.

Definition fold_on_bond_ids {A : Set}
  (ctxt : Raw_context.t) (contract : Contract_repr.t)
  : Variant.t A (Bond_id_repr.t A A) A :=
  Storage.Contract.fold_bond_ids (ctxt, contract).

Definition ensure_deallocated_if_empty
  (ctxt : Raw_context.t) (contract : Contract_repr.contract)
  : M? Raw_context.t :=
  match Contract_repr.is_implicit contract with
  | Nonereturn? ctxt
  | Some _
    let? balance_opt :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.find)
        ctxt contract in
    match balance_opt with
    | Nonereturn? ctxt
    | Some balance
      if Tez_repr.op_ltgt balance Tez_repr.zero then
        return? ctxt
      else
        let? has_frozen_bonds := has_frozen_bonds ctxt contract in
        if has_frozen_bonds then
          return? ctxt
        else
          let? function_parameter :=
            Contract_delegate_storage.find ctxt contract in
          match function_parameter with
          | Some _return? ctxt
          | Nonedelete ctxt contract
          end
    end
  end.