(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Module bound.
  (* StructRecord
    {
      name := "BoundMeter";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("pkg_bounds", Ty.path "move_bytecode_verifier_meter::bound::Bounds");
          ("mod_bounds", Ty.path "move_bytecode_verifier_meter::bound::Bounds");
          ("fun_bounds", Ty.path "move_bytecode_verifier_meter::bound::Bounds")
        ];
    } *)
  
  (* StructRecord
    {
      name := "Bounds";
      const_params := [];
      ty_params := [];
      fields :=
        [
          ("name", Ty.path "alloc::string::String");
          ("units", Ty.path "u128");
          ("max", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u128" ])
        ];
    } *)
  
  Module Impl_move_bytecode_verifier_meter_Meter_for_move_bytecode_verifier_meter_bound_BoundMeter.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier_meter::bound::BoundMeter".
    
    (*
        fn enter_scope(&mut self, name: &str, scope: Scope) {
            let bounds = self.get_bounds_mut(scope);
            bounds.name = name.into();
            bounds.units = 0;
        }
    *)
    Definition enter_scope (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; name; scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let name := M.alloc (| name |) in
          let scope := M.alloc (| scope |) in
          M.read (|
            let~ bounds :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                    "get_bounds_mut",
                    []
                  |),
                  [ M.read (| self |); M.read (| scope |) ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| bounds |),
                  "move_bytecode_verifier_meter::bound::Bounds",
                  "name"
                |),
                M.call_closure (|
                  M.get_trait_method (|
                    "core::convert::Into",
                    Ty.apply (Ty.path "&") [] [ Ty.path "str" ],
                    [ Ty.path "alloc::string::String" ],
                    "into",
                    []
                  |),
                  [ M.read (| name |) ]
                |)
              |) in
            let~ _ :=
              M.write (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| bounds |),
                  "move_bytecode_verifier_meter::bound::Bounds",
                  "units"
                |),
                Value.Integer IntegerKind.U128 0
              |) in
            M.alloc (| Value.Tuple [] |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn transfer(&mut self, from: Scope, to: Scope, factor: f32) -> PartialVMResult<()> {
            let units = (self.get_bounds_mut(from).units as f32 * factor) as u128;
            self.add(to, units)
        }
    *)
    Definition transfer (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; from; to; factor ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let from := M.alloc (| from |) in
          let to := M.alloc (| to |) in
          let factor := M.alloc (| factor |) in
          M.read (|
            let~ units :=
              M.alloc (|
                M.rust_cast
                  (BinOp.Wrap.mul (|
                    M.rust_cast
                      (M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                              "get_bounds_mut",
                              []
                            |),
                            [ M.read (| self |); M.read (| from |) ]
                          |),
                          "move_bytecode_verifier_meter::bound::Bounds",
                          "units"
                        |)
                      |)),
                    M.read (| factor |)
                  |))
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "move_bytecode_verifier_meter::Meter",
                  Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                  [],
                  "add",
                  []
                |),
                [ M.read (| self |); M.read (| to |); M.read (| units |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    (*
        fn add(&mut self, scope: Scope, units: u128) -> PartialVMResult<()> {
            self.get_bounds_mut(scope).add(units)
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; scope; units ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let scope := M.alloc (| scope |) in
          let units := M.alloc (| units |) in
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "move_bytecode_verifier_meter::bound::Bounds",
              "add",
              []
            |),
            [
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                  "get_bounds_mut",
                  []
                |),
                [ M.read (| self |); M.read (| scope |) ]
              |);
              M.read (| units |)
            ]
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Implements :
      M.IsTraitInstance
        "move_bytecode_verifier_meter::Meter"
        Self
        (* Trait polymorphic types *) []
        (* Instance *)
        [
          ("enter_scope", InstanceField.Method enter_scope);
          ("transfer", InstanceField.Method transfer);
          ("add", InstanceField.Method add)
        ].
  End Impl_move_bytecode_verifier_meter_Meter_for_move_bytecode_verifier_meter_bound_BoundMeter.
  
  Module Impl_move_bytecode_verifier_meter_bound_Bounds.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier_meter::bound::Bounds".
    
    (*
        fn add(&mut self, units: u128) -> PartialVMResult<()> {
            if let Some(max) = self.max {
                let new_units = self.units.saturating_add(units);
                if new_units > max {
                    // TODO: change to a new status PROGRAM_TOO_COMPLEX once this is rolled out. For
                    // now we use an existing code to avoid breaking changes on potential rollback.
                    return Err(PartialVMError::new(StatusCode::CONSTRAINT_NOT_SATISFIED)
                        .with_message(format!(
                            "program too complex (in `{}` with `{} current + {} new > {} max`)",
                            self.name, self.units, units, max
                        )));
                }
                self.units = new_units;
            }
            Ok(())
        }
    *)
    Definition add (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; units ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let units := M.alloc (| units |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "move_bytecode_verifier_meter::bound::Bounds",
                              "max"
                            |) in
                          let γ0_0 :=
                            M.SubPointer.get_struct_tuple_field (|
                              γ,
                              "core::option::Option::Some",
                              0
                            |) in
                          let max := M.copy (| γ0_0 |) in
                          let~ new_units :=
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "u128",
                                  "saturating_add",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "move_bytecode_verifier_meter::bound::Bounds",
                                      "units"
                                    |)
                                  |);
                                  M.read (| units |)
                                ]
                              |)
                            |) in
                          let~ _ :=
                            M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.gt (| M.read (| new_units |), M.read (| max |) |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    M.alloc (|
                                      M.never_to_any (|
                                        M.read (|
                                          M.return_ (|
                                            Value.StructTuple
                                              "core::result::Result::Err"
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.path
                                                      "move_binary_format::errors::PartialVMError",
                                                    "with_message",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.path
                                                          "move_binary_format::errors::PartialVMError",
                                                        "new",
                                                        []
                                                      |),
                                                      [
                                                        Value.StructTuple
                                                          "move_core_types::vm_status::StatusCode::CONSTRAINT_NOT_SATISFIED"
                                                          []
                                                      ]
                                                    |);
                                                    M.call_closure (|
                                                      M.get_function (|
                                                        "core::hint::must_use",
                                                        [ Ty.path "alloc::string::String" ]
                                                      |),
                                                      [
                                                        M.read (|
                                                          let~ res :=
                                                            M.alloc (|
                                                              M.call_closure (|
                                                                M.get_function (|
                                                                  "alloc::fmt::format",
                                                                  []
                                                                |),
                                                                [
                                                                  M.call_closure (|
                                                                    M.get_associated_function (|
                                                                      Ty.path
                                                                        "core::fmt::Arguments",
                                                                      "new_v1",
                                                                      []
                                                                    |),
                                                                    [
                                                                      M.alloc (|
                                                                        Value.Array
                                                                          [
                                                                            M.read (|
                                                                              Value.String
                                                                                "program too complex (in `"
                                                                            |);
                                                                            M.read (|
                                                                              Value.String
                                                                                "` with `"
                                                                            |);
                                                                            M.read (|
                                                                              Value.String
                                                                                " current + "
                                                                            |);
                                                                            M.read (|
                                                                              Value.String " new > "
                                                                            |);
                                                                            M.read (|
                                                                              Value.String " max`)"
                                                                            |)
                                                                          ]
                                                                      |);
                                                                      M.alloc (|
                                                                        Value.Array
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::rt::Argument",
                                                                                "new_display",
                                                                                [
                                                                                  Ty.path
                                                                                    "alloc::string::String"
                                                                                ]
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| self |),
                                                                                  "move_bytecode_verifier_meter::bound::Bounds",
                                                                                  "name"
                                                                                |)
                                                                              ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::rt::Argument",
                                                                                "new_display",
                                                                                [ Ty.path "u128" ]
                                                                              |),
                                                                              [
                                                                                M.SubPointer.get_struct_record_field (|
                                                                                  M.read (| self |),
                                                                                  "move_bytecode_verifier_meter::bound::Bounds",
                                                                                  "units"
                                                                                |)
                                                                              ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::rt::Argument",
                                                                                "new_display",
                                                                                [ Ty.path "u128" ]
                                                                              |),
                                                                              [ units ]
                                                                            |);
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.path
                                                                                  "core::fmt::rt::Argument",
                                                                                "new_display",
                                                                                [ Ty.path "u128" ]
                                                                              |),
                                                                              [ max ]
                                                                            |)
                                                                          ]
                                                                      |)
                                                                    ]
                                                                  |)
                                                                ]
                                                              |)
                                                            |) in
                                                          res
                                                        |)
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              ]
                                          |)
                                        |)
                                      |)
                                    |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          let~ _ :=
                            M.write (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "move_bytecode_verifier_meter::bound::Bounds",
                                "units"
                              |),
                              M.read (| new_units |)
                            |) in
                          M.alloc (| Value.Tuple [] |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_add : M.IsAssociatedFunction Self "add" add.
  End Impl_move_bytecode_verifier_meter_bound_Bounds.
  
  Module Impl_move_bytecode_verifier_meter_bound_BoundMeter.
    Definition Self : Ty.t := Ty.path "move_bytecode_verifier_meter::bound::BoundMeter".
    
    (*
        pub fn new(config: MeterConfig) -> Self {
            Self {
                pkg_bounds: Bounds {
                    name: "<unknown>".to_string(),
                    units: 0,
                    max: config.max_per_pkg_meter_units,
                },
                mod_bounds: Bounds {
                    name: "<unknown>".to_string(),
                    units: 0,
                    max: config.max_per_mod_meter_units,
                },
                fun_bounds: Bounds {
                    name: "<unknown>".to_string(),
                    units: 0,
                    max: config.max_per_fun_meter_units,
                },
            }
        }
    *)
    Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ config ] =>
        ltac:(M.monadic
          (let config := M.alloc (| config |) in
          Value.StructRecord
            "move_bytecode_verifier_meter::bound::BoundMeter"
            [
              ("pkg_bounds",
                Value.StructRecord
                  "move_bytecode_verifier_meter::bound::Bounds"
                  [
                    ("name",
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::string::ToString",
                          Ty.path "str",
                          [],
                          "to_string",
                          []
                        |),
                        [ M.read (| Value.String "<unknown>" |) ]
                      |));
                    ("units", Value.Integer IntegerKind.U128 0);
                    ("max",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          config,
                          "move_vm_config::verifier::MeterConfig",
                          "max_per_pkg_meter_units"
                        |)
                      |))
                  ]);
              ("mod_bounds",
                Value.StructRecord
                  "move_bytecode_verifier_meter::bound::Bounds"
                  [
                    ("name",
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::string::ToString",
                          Ty.path "str",
                          [],
                          "to_string",
                          []
                        |),
                        [ M.read (| Value.String "<unknown>" |) ]
                      |));
                    ("units", Value.Integer IntegerKind.U128 0);
                    ("max",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          config,
                          "move_vm_config::verifier::MeterConfig",
                          "max_per_mod_meter_units"
                        |)
                      |))
                  ]);
              ("fun_bounds",
                Value.StructRecord
                  "move_bytecode_verifier_meter::bound::Bounds"
                  [
                    ("name",
                      M.call_closure (|
                        M.get_trait_method (|
                          "alloc::string::ToString",
                          Ty.path "str",
                          [],
                          "to_string",
                          []
                        |),
                        [ M.read (| Value.String "<unknown>" |) ]
                      |));
                    ("units", Value.Integer IntegerKind.U128 0);
                    ("max",
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          config,
                          "move_vm_config::verifier::MeterConfig",
                          "max_per_fun_meter_units"
                        |)
                      |))
                  ])
            ]))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
    
    (*
        fn get_bounds_mut(&mut self, scope: Scope) -> &mut Bounds {
            match scope {
                Scope::Package => &mut self.pkg_bounds,
                Scope::Module => &mut self.mod_bounds,
                Scope::Function => &mut self.fun_bounds,
                Scope::Transaction => panic!("transaction scope unsupported."),
            }
        }
    *)
    Definition get_bounds_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let scope := M.alloc (| scope |) in
          M.read (|
            M.match_operator (|
              scope,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Package" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "pkg_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Module" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "mod_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Function" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "fun_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_bytecode_verifier_meter::Scope::Transaction"
                      |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [ M.read (| Value.String "transaction scope unsupported." |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_bounds_mut :
      M.IsAssociatedFunction Self "get_bounds_mut" get_bounds_mut.
    
    (*
        fn get_bounds(&self, scope: Scope) -> &Bounds {
            match scope {
                Scope::Package => &self.pkg_bounds,
                Scope::Module => &self.mod_bounds,
                Scope::Function => &self.fun_bounds,
                Scope::Transaction => panic!("transaction scope unsupported."),
            }
        }
    *)
    Definition get_bounds (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let scope := M.alloc (| scope |) in
          M.read (|
            M.match_operator (|
              scope,
              [
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Package" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "pkg_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Module" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "mod_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (| γ, "move_bytecode_verifier_meter::Scope::Function" |) in
                    M.alloc (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "move_bytecode_verifier_meter::bound::BoundMeter",
                        "fun_bounds"
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (let _ :=
                      M.is_struct_tuple (|
                        γ,
                        "move_bytecode_verifier_meter::Scope::Transaction"
                      |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic_fmt", [] |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "core::fmt::Arguments",
                                "new_const",
                                []
                              |),
                              [
                                M.alloc (|
                                  Value.Array
                                    [ M.read (| Value.String "transaction scope unsupported." |) ]
                                |)
                              ]
                            |)
                          ]
                        |)
                      |)
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_bounds : M.IsAssociatedFunction Self "get_bounds" get_bounds.
    
    (*
        pub fn get_usage(&self, scope: Scope) -> u128 {
            self.get_bounds(scope).units
        }
    *)
    Definition get_usage (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let scope := M.alloc (| scope |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                  "get_bounds",
                  []
                |),
                [ M.read (| self |); M.read (| scope |) ]
              |),
              "move_bytecode_verifier_meter::bound::Bounds",
              "units"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_usage : M.IsAssociatedFunction Self "get_usage" get_usage.
    
    (*
        pub fn get_limit(&self, scope: Scope) -> Option<u128> {
            self.get_bounds(scope).max
        }
    *)
    Definition get_limit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ self; scope ] =>
        ltac:(M.monadic
          (let self := M.alloc (| self |) in
          let scope := M.alloc (| scope |) in
          M.read (|
            M.SubPointer.get_struct_record_field (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "move_bytecode_verifier_meter::bound::BoundMeter",
                  "get_bounds",
                  []
                |),
                [ M.read (| self |); M.read (| scope |) ]
              |),
              "move_bytecode_verifier_meter::bound::Bounds",
              "max"
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom AssociatedFunction_get_limit : M.IsAssociatedFunction Self "get_limit" get_limit.
  End Impl_move_bytecode_verifier_meter_bound_BoundMeter.
End bound.
