✒️ Contract_storage.v

Translated 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.t × 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.t × Tez_repr.t × Tez_repr.t) payload in
            Some (c_value, b_value, a_value)
          else None
        end)
      (fun (function_parameter : Contract_repr.t × Tez_repr.t × Tez_repr.t) ⇒
        let '(c_value, b_value, a_value) := function_parameter in
        Build_extensible "Balance_too_low"
          (Contract_repr.t × 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.t × Manager_counter_repr.t × Manager_counter_repr.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)")
              Manager_counter_repr.pp found Contract_repr.pp contract
              Manager_counter_repr.pp exp))
      (Data_encoding.obj3
        (Data_encoding.req None None "contract" Contract_repr.encoding)
        (Data_encoding.req None None "expected"
          Manager_counter_repr.encoding_for_errors)
        (Data_encoding.req None None "found"
          Manager_counter_repr.encoding_for_errors))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Counter_in_the_future" then
            let '{|
              Counter_in_the_future.contract := contract;
                Counter_in_the_future.expected := expected;
                Counter_in_the_future.found := found
                |} := cast Counter_in_the_future payload in
            Some (contract, expected, found)
          else None
        end)
      (fun (function_parameter :
        Contract_repr.t × Manager_counter_repr.t × Manager_counter_repr.t) ⇒
        let '(contract, expected, found) := function_parameter in
        Build_extensible "Counter_in_the_future" Counter_in_the_future
          {| Counter_in_the_future.contract := contract;
            Counter_in_the_future.expected := expected;
            Counter_in_the_future.found := found; |}) 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.t × Manager_counter_repr.t × Manager_counter_repr.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)")
              Manager_counter_repr.pp found Contract_repr.pp contract
              Manager_counter_repr.pp exp))
      (Data_encoding.obj3
        (Data_encoding.req None None "contract" Contract_repr.encoding)
        (Data_encoding.req None None "expected"
          Manager_counter_repr.encoding_for_errors)
        (Data_encoding.req None None "found"
          Manager_counter_repr.encoding_for_errors))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Counter_in_the_past" then
            let '{|
              Counter_in_the_past.contract := contract;
                Counter_in_the_past.expected := expected;
                Counter_in_the_past.found := found
                |} := cast Counter_in_the_past payload in
            Some (contract, expected, found)
          else None
        end)
      (fun (function_parameter :
        Contract_repr.t × Manager_counter_repr.t × Manager_counter_repr.t) ⇒
        let '(contract, expected, found) := function_parameter in
        Build_extensible "Counter_in_the_past" Counter_in_the_past
          {| Counter_in_the_past.contract := contract;
            Counter_in_the_past.expected := expected;
            Counter_in_the_past.found := found; |}) 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.t) ⇒
            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.t payload in
            Some c_value
          else None
        end)
      (fun (c_value : Contract_repr.t) ⇒
        Build_extensible "Non_existing_contract" Contract_repr.t 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.t × 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.t × Bond_id_repr.t) ⇒
      let '(c_value, b_value) := function_parameter in
      Build_extensible "Frozen_bonds_must_be_spent_at_once"
        (Contract_repr.t × Bond_id_repr.t) (c_value, b_value)).

Definition failwith {A : Set} (msg : string) : M ? A :=
  Error_monad.tzfail (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_map ⇒ Some (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)
    : M ? (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
    Error_monad.op_gtpipequestion
      (Error_monad.op_gtpipequestion
        (List.fold_left_e
          (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 ⇒
                return ?
                  (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
                return ?
                  (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
                    |} ⇒
                return ?
                  (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) rest ⇒ id =Z big_map
                    | _ ⇒ false
                    end) with
                | (cons (id, diff_value) rest, true) ⇒
                  let ? diff_value :=
                    match diff_value with
                    | Lazy_storage_diff.Remove ⇒
                      Error_monad.error_value
                        (Build_extensible "Asserted" unit tt)
                    |
                      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
                      return ?
                        (Lazy_storage_diff.Update
                          {| Lazy_storage_diff.diff.Update.init := init_value;
                            Lazy_storage_diff.diff.Update.updates := updates; |})
                    end in
                  return ? (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
                  Pervasives.Ok
                    (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) rev_head)
      (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)).

  Definition of_lazy_storage_diff (diffs : list Lazy_storage_diff.diffs_item)
    : list item :=
    List.flatten
      (List.rev
        (List.fold_left
          (fun (legacy_diffs : list (list item)) ⇒
            fun (arg : Lazy_storage_diff.diffs_item) ⇒
              let 'Lazy_storage_diff.Item kind_value id diff_value := arg in
              let 'existT _ [__Item_'i, __Item_'a, __Item_'u]
                [diff_value, id, kind_value] :=
                cast_exists (Es := [Set ** Set ** Set])
                  (fun '[__Item_'i , __Item_'a , __Item_'u ] ⇒
                    [Lazy_storage_diff.diff __Item_'i __Item_'a __Item_'u **
                      __Item_'i ** Lazy_storage_kind.t])
                  [diff_value, id, kind_value] in
              cast (list (list item))
              (let diffs :=
                match kind_value with
                | Lazy_storage_kind.Big_map ⇒
                  let id :=
                    Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.to_legacy_USE_ONLY_IN_Legacy_big_map_diff)
                      (cast Storage.Big_map.id id) in
                  match diff_value with
                  | Lazy_storage_diff.Remove ⇒ [ Clear id ]
                  |
                    Lazy_storage_diff.Update {|
                      Lazy_storage_diff.diff.Update.init := init_value;
                        Lazy_storage_diff.diff.Update.updates := updates
                        |} ⇒
                    let '[updates, init_value] :=
                      cast
                        [__Item_'u **
                          Lazy_storage_diff.init __Item_'i __Item_'a]
                        [updates, init_value] in
                    let updates :=
                      List.rev_map
                        (fun (function_parameter :
                          Lazy_storage_kind.Big_map.update) ⇒
                          let '{|
                            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
                              |} := function_parameter in
                          Update
                            {| item.Update.big_map := id;
                              item.Update.diff_key := key_value;
                              item.Update.diff_key_hash := key_hash;
                              item.Update.diff_value := value_value; |})
                        (cast (list Lazy_storage_kind.Big_map.update) updates)
                      in
                    match init_value with
                    | Lazy_storage_diff.Existing ⇒ updates
                    |
                      Lazy_storage_diff.Copy {|
                        Lazy_storage_diff.init.Copy.src := src |} ⇒
                      let src :=
                        Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.to_legacy_USE_ONLY_IN_Legacy_big_map_diff)
                          (cast Storage.Big_map.id src) in
                      cons
                        (Copy {| item.Copy.src := src; item.Copy.dst := id; |})
                        updates
                    | Lazy_storage_diff.Alloc r_value ⇒
                      let '{|
                        Lazy_storage_kind.Big_map.alloc.key_type := key_type;
                          Lazy_storage_kind.Big_map.alloc.value_type :=
                            value_type
                          |} := cast Lazy_storage_kind.Big_map.alloc r_value in
                      cons
                        (Alloc
                          {| item.Alloc.big_map := id;
                            item.Alloc.key_type := key_type;
                            item.Alloc.value_type := value_type; |}) updates
                    end
                  end
                | _ ⇒ nil
                end in
              cons diffs legacy_diffs)) nil diffs)).
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
  | None ⇒ return ? (c_value, Z.zero)
  | Some diffs ⇒ Lazy_storage_diff.apply c_value diffs
  end.

Definition raw_originate
  (c_value : Raw_context.t) (prepaid_bootstrap_storage : bool)
  (contract : Contract_hash.t)
  (script : Script_repr.t × option Lazy_storage_diff.diffs)
  : M ? Raw_context.t :=
  let contract := Contract_repr.Originated contract in
  let ? c_value :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
      c_value contract Tez_repr.zero in
  let
    '({| Script_repr.t.code := code; Script_repr.t.storage := storage_value |},
      lazy_storage_diff) := script in
  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
  if total_size ≥Z Z.zero then
    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
  else
    Error_monad.error_value (Build_extensible "Asserted" unit tt).

Definition create_implicit
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  (balance : Tez_repr.t) : M ? Raw_context.t :=
  let contract := Contract_repr.Implicit manager in
  let ? counter :=
    Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.get)
      c_value in
  let ? c_value :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
      c_value contract counter in
  let ? c_value :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.init_value)
      c_value contract balance in
  Contract_manager_storage.init_value c_value contract
    (Manager_repr.Hash manager).

Definition delete (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M ? Raw_context.t :=
  match contract with
  | Contract_repr.Originated _ ⇒
    failwith "Non implicit contracts cannot be removed"
  | Contract_repr.Implicit _ ⇒
    let ? c_value := Contract_delegate_storage.unlink c_value contract in
    let update (local : Storage.Contract.local_context)
      : M ? Storage.Contract.local_context :=
      let ? local :=
        Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.Local).(Storage_sigs.Indexed_data_storage_with_local_context_Local.remove_existing)
          local in
      let ? local :=
        Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.Local).(Storage_sigs.Indexed_data_storage_with_local_context_Local.remove_existing)
          local in
      Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.Local).(Storage_sigs.Indexed_data_storage_with_local_context_Local.remove_existing)
        local in
    let ? '(c_value , _) :=
      Storage.Contract.with_local_context c_value contract
        (fun (local : Storage.Contract.local_context) ⇒
          let ? local := update local in
          return ? (local, tt)) in
    return ? c_value
  end.

Definition allocated (c_value : Raw_context.t) (contract : Contract_repr.t)
  : bool :=
  Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.mem)
    c_value contract.

Definition _exists (c_value : Raw_context.t) (contract : Contract_repr.t)
  : bool :=
  match contract with
  | Contract_repr.Implicit _ ⇒ true
  | Contract_repr.Originated _ ⇒ allocated c_value contract
  end.

Definition must_exist (c_value : Raw_context.t) (contract : Contract_repr.t)
  : M ? unit :=
  let function_parameter := _exists c_value contract in
  match function_parameter with
  | true ⇒ Error_monad.return_unit
  | false ⇒
    Error_monad.tzfail
      (Build_extensible "Non_existing_contract" Contract_repr.t 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
  | true ⇒ Error_monad.return_unit
  | false ⇒
    match contract with
    | Contract_repr.Implicit pkh ⇒
      Error_monad.tzfail
        (Build_extensible "Empty_implicit_contract" Signature.public_key_hash
          pkh)
    | Contract_repr.Originated _ ⇒
      Error_monad.tzfail
        (Build_extensible "Non_existing_contract" Contract_repr.t contract)
    end
  end.

Definition list_value (c_value : Raw_context.t) : M ? (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_hash.t ) :=
  let ? '(c_value , nonce_value ) :=
    Raw_context.increment_origination_nonce c_value in
  return ? (c_value, (Contract_hash.of_nonce nonce_value)).

Definition originated_from_current_nonce
  (ctxt_since : Raw_context.t) (ctxt_until : Raw_context.t)
  : M ? (list Contract_hash.t ) :=
  let ? since := Raw_context.get_origination_nonce ctxt_since in
  let ? until := Raw_context.get_origination_nonce ctxt_until in
  let ? ocs := Contract_repr.originated_contracts since until in
  Error_monad.op_gtpipeeq
    (List.filter_s
      (fun (contract : Contract_hash.t) ⇒
        _exists ctxt_until (Contract_repr.Originated contract)) ocs)
    Error_monad.ok.

Definition check_counter_increment
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  (counter : Manager_counter_repr.t) : M ? unit :=
  let contract := Contract_repr.Implicit manager in
  let ? contract_counter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.get)
      c_value contract in
  let expected := Manager_counter_repr.succ contract_counter in
  if Manager_counter_repr.op_eq expected counter then
    Error_monad.return_unit
  else
    if Manager_counter_repr.op_gt expected counter then
      Error_monad.tzfail
        (Build_extensible "Counter_in_the_past" Counter_in_the_past
          {| Counter_in_the_past.contract := contract;
            Counter_in_the_past.expected := expected;
            Counter_in_the_past.found := counter; |})
    else
      Error_monad.tzfail
        (Build_extensible "Counter_in_the_future" Counter_in_the_future
          {| Counter_in_the_future.contract := contract;
            Counter_in_the_future.expected := expected;
            Counter_in_the_future.found := counter; |}).

Definition increment_counter
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  : M ? Raw_context.t :=
  let contract := Contract_repr.Implicit 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 (Manager_counter_repr.succ global_counter) in
  let ? contract_counter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.get)
      c_value contract in
  Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.update)
    c_value contract (Manager_counter_repr.succ contract_counter).

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

Definition get_script
  (c_value : Raw_context.t) (contract_hash : Contract_hash.t)
  : M ? (Raw_context.t × option Script_repr.t ) :=
  let contract := Contract_repr.Originated contract_hash in
  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_hash : Contract_hash.t)
  : M ? (Raw_context.t × option Script_repr.expr ) :=
  let contract := Contract_repr.Originated contract_hash in
  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 ? Manager_counter_repr.t :=
  let contract := Contract_repr.Implicit manager in
  let ? function_parameter :=
    Storage.Contract.Counter.(Storage_sigs.Indexed_data_storage_with_local_context.find)
      c_value contract in
  match function_parameter with
  | None ⇒
    match contract with
    | Contract_repr.Implicit _ ⇒
      Storage.Contract.Global_counter.(Storage.Simple_single_data_storage.get)
        c_value
    | Contract_repr.Originated _ ⇒ failwith "get_counter"
    end
  | Some v_value ⇒ return ? 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_with_local_context.find)
      c_value contract in
  match function_parameter with
  | None ⇒
    match contract with
    | Contract_repr.Implicit _ ⇒ return ? Tez_repr.zero
    | Contract_repr.Originated _ ⇒ failwith "get_balance"
    end
  | Some v_value ⇒ return ? 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 check_allocated_and_get_balance
  (c_value : Raw_context.t) (pkh : Signature.public_key_hash) : M ? Tez_repr.t :=
  let ? balance_opt :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.find)
      c_value (Contract_repr.Implicit pkh) in
  match balance_opt with
  | None ⇒
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Empty_implicit_contract" Signature.public_key_hash pkh)
  | Some balance ⇒ return ? balance
  end.

Definition update_script_storage
  (c_value : Raw_context.t) (contract_hash : Contract_hash.t)
  (storage_value : Script_repr.expr)
  (lazy_storage_diff : option Lazy_storage_diff.diffs) : M ? Raw_context.t :=
  let contract := Contract_repr.Originated contract_hash in
  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_from_balance
  (contract : Contract_repr.t) (balance : Tez_repr.t) (amount : Tez_repr.t)
  : M ? Tez_repr.t :=
  Error_monad.record_trace
    (Build_extensible "Balance_too_low"
      (Contract_repr.t × Tez_repr.t × Tez_repr.t) (contract, balance, amount))
    (Tez_repr.op_minusquestion balance amount).

Definition check_emptiable
  (c_value : Raw_context.t) (contract : Contract_repr.t) : M ? unit :=
  match contract with
  | Contract_repr.Originated _ ⇒ Error_monad.Lwt_result_syntax.return_unit
  | Contract_repr.Implicit pkh ⇒
    let ? delegate := Contract_delegate_storage.find c_value contract in
    match delegate with
    | Some pkh' ⇒
      if
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) pkh pkh'
      then
        Error_monad.Lwt_result_syntax.return_unit
      else
        Error_monad.error_value
          (Build_extensible "Empty_implicit_delegated_contract"
            Signature.public_key_hash pkh)
    | None ⇒ Error_monad.Lwt_result_syntax.return_unit
    end
  end.

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_with_local_context.find)
      c_value contract in
  let balance := Option.value_value balance Tez_repr.zero in
  let ? new_balance := spend_from_balance contract balance amount in
  let ? c_value :=
    Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.update)
      c_value contract new_balance in
  let ? c_value := Stake_storage.remove_contract_stake c_value contract amount in
  Error_monad.Lwt_result_syntax.op_letplus
    (Error_monad.when_ (Tez_repr.op_lteq new_balance Tez_repr.zero)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        check_emptiable c_value contract))
    (fun function_parameter ⇒
      let '_ := function_parameter in
      c_value).

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_with_local_context.find)
      c_value contract in
  match function_parameter with
  | None ⇒
    match contract with
    | Contract_repr.Originated _ ⇒
      Error_monad.tzfail
        (Build_extensible "Non_existing_contract" Contract_repr.t contract)
    | Contract_repr.Implicit manager ⇒ create_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_with_local_context.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 Manager_counter_repr.init_value 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_1 ⇒ Option.value_value x_1 Z.zero).

Definition paid_storage_space
  (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_1 ⇒ Option.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 increase_paid_storage
  (c_value : Raw_context.t) (contract_hash : Contract_hash.t)
  (storage_incr : Z.t) : M ? Raw_context.t :=
  let contract := Contract_repr.Originated contract_hash in
  let ? already_paid_space :=
    Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.get)
      c_value contract in
  let new_storage_space := already_paid_space +Z storage_incr in
  Storage.Contract.Paid_storage_space.(Storage_sigs.Indexed_data_storage.update)
    c_value contract new_storage_space.

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_with_local_context.get)
      ctxt contract in
  let ? new_balance := f_value balance amount in
  Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.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_1 ⇒ Option.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_with_local_context.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].

Definition spend_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.remove_contract_stake ctxt contract amount in
  let ? '(ctxt , frozen_bonds ) :=
    Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      (ctxt, contract) bond_id in
  let ? '_ :=
    Error_monad.error_when (Tez_repr.op_ltgt frozen_bonds amount)
      (Build_extensible "Frozen_bonds_must_be_spent_at_once"
        (Contract_repr.t × Bond_id_repr.t) (contract, bond_id)) in
  let ? '(ctxt , _) :=
    Storage.Contract.Frozen_bonds.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing)
      (ctxt, contract) bond_id in
  let ? total :=
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.get)
      ctxt contract in
  let ? new_total := Tez_repr.op_minusquestion total amount in
  if Tez_repr.op_eq new_total Tez_repr.zero then
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.remove_existing)
      ctxt contract
  else
    Storage.Contract.Total_frozen_bonds.(Storage_sigs.Indexed_data_storage.update)
      ctxt contract new_total.

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 → M ? A) → M ? A :=
  Storage.Contract.fold_bond_ids (ctxt, contract).

Indicate whether the given implicit contract should avoid deletion when it is emptied.

Definition should_keep_empty_implicit_contract
  (ctxt : Raw_context.t) (contract : Contract_repr.t) : M ? bool :=
  let ? has_frozen_bonds := has_frozen_bonds ctxt contract in
  if has_frozen_bonds then
    Error_monad.Lwt_result_syntax.return_true
  else
    let ? function_parameter := Contract_delegate_storage.find ctxt contract in
    match function_parameter with
    | Some _ ⇒ Error_monad.Lwt_result_syntax.return_true
    | None ⇒ Error_monad.Lwt_result_syntax.return_false
    end.

Definition ensure_deallocated_if_empty
  (ctxt : Raw_context.t) (contract : Contract_repr.t) : M ? Raw_context.t :=
  match contract with
  | Contract_repr.Originated _ ⇒ return ? ctxt
  | Contract_repr.Implicit _ ⇒
    let ? balance_opt :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.find)
        ctxt contract in
    match balance_opt with
    | None ⇒ return ? ctxt
    | Some balance ⇒
      if Tez_repr.op_ltgt balance Tez_repr.zero then
        return ? ctxt
      else
        let ? keep_contract := should_keep_empty_implicit_contract ctxt contract
          in
        if keep_contract then
          return ? ctxt
        else
          delete ctxt contract
    end
  end.

Definition simulate_spending
  (ctxt : Raw_context.t) (balance : Tez_repr.t) (amount : Tez_repr.t)
  (source : Signature.public_key_hash) : M ? (Tez_repr.t × bool) :=
  let contract := Contract_repr.Implicit source in
  let ? new_balance := spend_from_balance contract balance amount in
  let ? still_allocated :=
    if Tez_repr.op_gt new_balance Tez_repr.zero then
      Error_monad.Lwt_result_syntax.return_true
    else
      let ? '_ := check_emptiable ctxt contract in
      should_keep_empty_implicit_contract ctxt contract in
  return ? (new_balance, still_allocated).