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

(* StructRecord
  {
    name := "Mapping";
    const_params := [];
    ty_params := [ "K"; "V" ];
    fields :=
      [
        ("_key", Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ]);
        ("_value", Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ])
      ];
  } *)

Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_multisig_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "multisig::Mapping") [] [ K; V ].
  
  (* Default *)
  Definition default (K V : Ty.t) (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    let Self : Ty.t := Self K V in
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "multisig::Mapping"
          [
            ("_key",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ K ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("_value",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "core::marker::PhantomData") [] [ V ],
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    forall (K V : Ty.t),
    M.IsTraitInstance
      "core::default::Default"
      (Self K V)
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method (default K V)) ].
End Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_multisig_Mapping_K_V.

Module Impl_multisig_Mapping_K_V.
  Definition Self (K V : Ty.t) : Ty.t := Ty.apply (Ty.path "multisig::Mapping") [] [ K; V ].
  
  (*
      fn contains(&self, _key: &K) -> bool {
          unimplemented!()
      }
  *)
  Parameter contains : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_contains :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "contains" (contains K V).
  
  (*
      fn get(&self, _key: &K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter get : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_get :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "get" (get K V).
  
  (*
      fn insert(&mut self, _key: K, _value: V) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter insert : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_insert :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "insert" (insert K V).
  
  (*
      fn remove(&self, _key: K) {
          unimplemented!()
      }
  *)
  Parameter remove : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_remove :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "remove" (remove K V).
  
  (*
      fn size(&self, _key: K) -> Option<u32> {
          unimplemented!()
      }
  *)
  Parameter size : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_size :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "size" (size K V).
  
  (*
      fn take(&self, _key: K) -> Option<V> {
          unimplemented!()
      }
  *)
  Parameter take : forall (K V : Ty.t), (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_take :
    forall (K V : Ty.t),
    M.IsAssociatedFunction (Self K V) "take" (take K V).
End Impl_multisig_Mapping_K_V.

(* StructTuple
  {
    name := "AccountId";
    const_params := [];
    ty_params := [];
    fields := [ Ty.path "u128" ];
  } *)

Module Impl_core_default_Default_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "multisig::AccountId"
          [
            M.call_closure (|
              M.get_trait_method (| "core::default::Default", Ty.path "u128", [], "default", [] |),
              []
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_AccountId.

Module Impl_core_fmt_Debug_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_tuple_field1_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "AccountId" |);
            M.alloc (|
              M.SubPointer.get_struct_tuple_field (| M.read (| self |), "multisig::AccountId", 0 |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::fmt::Debug"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
End Impl_core_fmt_Debug_for_multisig_AccountId.

Module Impl_core_clone_Clone_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_AccountId.

Module Impl_core_marker_Copy_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_AccountId.

Module Impl_core_marker_StructuralPartialEq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_multisig_AccountId.

Module Impl_core_cmp_PartialEq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        BinOp.eq (|
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "multisig::AccountId", 0 |)
          |),
          M.read (|
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "multisig::AccountId", 0 |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_multisig_AccountId.

Module Impl_core_cmp_Eq_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* Eq *)
  Definition assert_receiver_is_total_eq
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_multisig_AccountId.

Module Impl_core_cmp_PartialOrd_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* PartialOrd *)
  Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.call_closure (|
          M.get_trait_method (|
            "core::cmp::PartialOrd",
            Ty.path "u128",
            [ Ty.path "u128" ],
            "partial_cmp",
            []
          |),
          [
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "multisig::AccountId", 0 |);
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "multisig::AccountId", 0 |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_multisig_AccountId.

Module Impl_core_cmp_Ord_for_multisig_AccountId.
  Definition Self : Ty.t := Ty.path "multisig::AccountId".
  
  (* Ord *)
  Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.call_closure (|
          M.get_trait_method (| "core::cmp::Ord", Ty.path "u128", [], "cmp", [] |),
          [
            M.SubPointer.get_struct_tuple_field (| M.read (| self |), "multisig::AccountId", 0 |);
            M.SubPointer.get_struct_tuple_field (| M.read (| other |), "multisig::AccountId", 0 |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_multisig_AccountId.

Axiom Balance : (Ty.path "multisig::Balance") = (Ty.path "u128").

(* StructRecord
  {
    name := "Env";
    const_params := [];
    ty_params := [];
    fields := [ ("caller", Ty.path "multisig::AccountId") ];
  } *)

Definition value_MAX_OWNERS : Value.t :=
  M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U32 50 |))).

Axiom TransactionId : (Ty.path "multisig::TransactionId") = (Ty.path "u32").

Definition value_WRONG_TRANSACTION_ID : Value.t :=
  M.run ltac:(M.monadic (Value.String "The user specified an invalid transaction id. Abort.")).

(* StructTuple
  {
    name := "CallInput";
    const_params := [];
    ty_params := [];
    fields := [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ];
  } *)

(*
Enum ConfirmationStatus
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Confirmed";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "ConfirmationsNeeded";
        item := StructTuple [ Ty.path "u32" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_clone_Clone_for_multisig_ConfirmationStatus.
  Definition Self : Ty.t := Ty.path "multisig::ConfirmationStatus".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.match_operator (|
            Value.DeclaredButUndefined,
            [ fun γ => ltac:(M.monadic (M.read (| self |))) ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_ConfirmationStatus.

Module Impl_core_marker_Copy_for_multisig_ConfirmationStatus.
  Definition Self : Ty.t := Ty.path "multisig::ConfirmationStatus".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_ConfirmationStatus.

(* StructRecord
  {
    name := "Transaction";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("callee", Ty.path "multisig::AccountId");
        ("selector",
          Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ]);
        ("input",
          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]);
        ("transferred_value", Ty.path "u128");
        ("gas_limit", Ty.path "u64");
        ("allow_reentry", Ty.path "bool")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Transaction.
  Definition Self : Ty.t := Ty.path "multisig::Transaction".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "multisig::Transaction"
          [
            ("callee",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "multisig::AccountId",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("selector",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("input",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("transferred_value",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "u128",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("gas_limit",
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.path "u64", [], "default", [] |),
                []
              |));
            ("allow_reentry",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "bool",
                  [],
                  "default",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Transaction.

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "TransactionFailed";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_clone_Clone_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  (* Clone *)
  Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (| M.read (| self |) |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::clone::Clone"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("clone", InstanceField.Method clone) ].
End Impl_core_clone_Clone_for_multisig_Error.

Module Impl_core_marker_Copy_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_multisig_Error.

Module Impl_core_marker_StructuralPartialEq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_multisig_Error.

Module Impl_core_cmp_PartialEq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  (* PartialEq *)
  Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        Value.Bool true))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("eq", InstanceField.Method eq) ].
End Impl_core_cmp_PartialEq_for_multisig_Error.

Module Impl_core_cmp_Eq_for_multisig_Error.
  Definition Self : Ty.t := Ty.path "multisig::Error".
  
  (* Eq *)
  Definition assert_receiver_is_total_eq
      (ε : list Value.t)
      (τ : list Ty.t)
      (α : list Value.t)
      : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        Value.Tuple []))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Eq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *)
      [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
End Impl_core_cmp_Eq_for_multisig_Error.

(* StructRecord
  {
    name := "Transactions";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transactions",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ]);
        ("next_id", Ty.path "u32")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Transactions.
  Definition Self : Ty.t := Ty.path "multisig::Transactions".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "multisig::Transactions"
          [
            ("transactions",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("next_id",
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.path "u32", [], "default", [] |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Transactions.

(* StructRecord
  {
    name := "Confirmation";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transaction", Ty.path "u32");
        ("from", Ty.path "multisig::AccountId");
        ("status", Ty.path "multisig::ConfirmationStatus")
      ];
  } *)

(* StructRecord
  {
    name := "Revocation";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32"); ("from", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "Submission";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32") ];
  } *)

(* StructRecord
  {
    name := "Cancellation";
    const_params := [];
    ty_params := [];
    fields := [ ("transaction", Ty.path "u32") ];
  } *)

(* StructRecord
  {
    name := "Execution";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("transaction", Ty.path "u32");
        ("result",
          Ty.apply
            (Ty.path "core::result::Result")
            []
            [
              Ty.apply
                (Ty.path "core::option::Option")
                []
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                ];
              Ty.path "multisig::Error"
            ])
      ];
  } *)

(* StructRecord
  {
    name := "OwnerAddition";
    const_params := [];
    ty_params := [];
    fields := [ ("owner", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "OwnerRemoval";
    const_params := [];
    ty_params := [];
    fields := [ ("owner", Ty.path "multisig::AccountId") ];
  } *)

(* StructRecord
  {
    name := "RequirementChange";
    const_params := [];
    ty_params := [];
    fields := [ ("new_requirement", Ty.path "u32") ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "Confirmation";
        item := StructTuple [ Ty.path "multisig::Confirmation" ];
        discriminant := None;
      };
      {
        name := "Revocation";
        item := StructTuple [ Ty.path "multisig::Revocation" ];
        discriminant := None;
      };
      {
        name := "Submission";
        item := StructTuple [ Ty.path "multisig::Submission" ];
        discriminant := None;
      };
      {
        name := "Cancellation";
        item := StructTuple [ Ty.path "multisig::Cancellation" ];
        discriminant := None;
      };
      {
        name := "Execution";
        item := StructTuple [ Ty.path "multisig::Execution" ];
        discriminant := None;
      };
      {
        name := "OwnerAddition";
        item := StructTuple [ Ty.path "multisig::OwnerAddition" ];
        discriminant := None;
      };
      {
        name := "OwnerRemoval";
        item := StructTuple [ Ty.path "multisig::OwnerRemoval" ];
        discriminant := None;
      };
      {
        name := "RequirementChange";
        item := StructTuple [ Ty.path "multisig::RequirementChange" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_multisig_Env.
  Definition Self : Ty.t := Ty.path "multisig::Env".
  
  (*
      fn caller(&self) -> AccountId {
          self.caller
      }
  *)
  Definition caller (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          M.SubPointer.get_struct_record_field (| M.read (| self |), "multisig::Env", "caller" |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_caller : M.IsAssociatedFunction Self "caller" caller.
  
  (*
      fn emit_event(&self, _event: Event) {
          unimplemented!()
      }
  *)
  Parameter emit_event : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_emit_event : M.IsAssociatedFunction Self "emit_event" emit_event.
  
  (*
      fn transferred_value(&self) -> Balance {
          unimplemented!()
      }
  *)
  Parameter transferred_value : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_transferred_value :
    M.IsAssociatedFunction Self "transferred_value" transferred_value.
  
  (*
      fn account_id(&self) -> AccountId {
          unimplemented!()
      }
  *)
  Parameter account_id : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_account_id : M.IsAssociatedFunction Self "account_id" account_id.
End Impl_multisig_Env.

(* StructRecord
  {
    name := "Multisig";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("confirmations",
          Ty.apply
            (Ty.path "multisig::Mapping")
            []
            [ Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ]; Ty.tuple [] ]);
        ("confirmation_count",
          Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "u32"; Ty.path "u32" ]);
        ("transactions",
          Ty.apply
            (Ty.path "multisig::Mapping")
            []
            [ Ty.path "u32"; Ty.path "multisig::Transaction" ]);
        ("transaction_list", Ty.path "multisig::Transactions");
        ("owners",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ]);
        ("is_owner",
          Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "multisig::AccountId"; Ty.tuple [] ]);
        ("requirement", Ty.path "u32")
      ];
  } *)

Module Impl_core_default_Default_for_multisig_Multisig.
  Definition Self : Ty.t := Ty.path "multisig::Multisig".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "multisig::Multisig"
          [
            ("confirmations",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ]; Ty.tuple [] ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("confirmation_count",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "u32"; Ty.path "u32" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("transactions",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "multisig::Transaction" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("transaction_list",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "multisig::Transactions",
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("owners",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("is_owner",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("requirement",
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.path "u32", [], "default", [] |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::default::Default"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("default", InstanceField.Method default) ].
End Impl_core_default_Default_for_multisig_Multisig.

(*
fn ensure_requirement_is_valid(owners: u32, requirement: u32) {
    assert!(0 < requirement && requirement <= owners && owners <= MAX_OWNERS);
}
*)
Definition ensure_requirement_is_valid (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ owners; requirement ] =>
    ltac:(M.monadic
      (let owners := M.alloc (| owners |) in
      let requirement := M.alloc (| requirement |) in
      M.read (|
        let~ _ :=
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        UnOp.not (|
                          LogicalOp.and (|
                            LogicalOp.and (|
                              BinOp.lt (|
                                Value.Integer IntegerKind.U32 0,
                                M.read (| requirement |)
                              |),
                              ltac:(M.monadic
                                (BinOp.le (| M.read (| requirement |), M.read (| owners |) |)))
                            |),
                            ltac:(M.monadic
                              (BinOp.le (|
                                M.read (| owners |),
                                M.read (| M.get_constant (| "multisig::MAX_OWNERS" |) |)
                              |)))
                          |)
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    M.never_to_any (|
                      M.call_closure (|
                        M.get_function (| "core::panicking::panic", [] |),
                        [
                          M.read (|
                            Value.String
                              "assertion failed: 0 < requirement && requirement <= owners && owners <= MAX_OWNERS"
                          |)
                        ]
                      |)
                    |)
                  |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |) in
        M.alloc (| Value.Tuple [] |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_ensure_requirement_is_valid :
  M.IsFunction "multisig::ensure_requirement_is_valid" ensure_requirement_is_valid.

Module Impl_multisig_Multisig.
  Definition Self : Ty.t := Ty.path "multisig::Multisig".
  
  (*
      fn init_env() -> Env {
          unimplemented!()
      }
  *)
  Parameter init_env : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_init_env : M.IsAssociatedFunction Self "init_env" init_env.
  
  (*
      fn env(&self) -> Env {
          Self::init_env()
      }
  *)
  Definition env (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "multisig::Multisig", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      pub fn new(requirement: u32, mut owners: Vec<AccountId>) -> Self {
          let mut contract = Multisig::default();
          owners.sort_unstable();
          owners.dedup();
          ensure_requirement_is_valid(owners.len() as u32, requirement);
  
          for owner in &owners {
              contract.is_owner.insert( *owner, ());
          }
  
          contract.owners = owners;
          contract.transaction_list = Default::default();
          contract.requirement = requirement;
          contract
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ requirement; owners ] =>
      ltac:(M.monadic
        (let requirement := M.alloc (| requirement |) in
        let owners := M.alloc (| owners |) in
        M.read (|
          let~ contract :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "multisig::Multisig",
                  [],
                  "default",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "slice") [] [ Ty.path "multisig::AccountId" ],
                  "sort_unstable",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::deref::DerefMut",
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                      [],
                      "deref_mut",
                      []
                    |),
                    [ owners ]
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                  "dedup",
                  []
                |),
                [ owners ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "multisig::ensure_requirement_is_valid", [] |),
                [
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                        "len",
                        []
                      |),
                      [ owners ]
                    |));
                  M.read (| requirement |)
                ]
              |)
            |) in
          let~ _ :=
            M.use
              (M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::collect::IntoIterator",
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ]
                        ],
                      [],
                      "into_iter",
                      []
                    |),
                    [ owners ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let iter := M.copy (| γ |) in
                      M.loop (|
                        ltac:(M.monadic
                          (let~ _ :=
                            M.match_operator (|
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::iter::traits::iterator::Iterator",
                                    Ty.apply
                                      (Ty.path "core::slice::iter::Iter")
                                      []
                                      [ Ty.path "multisig::AccountId" ],
                                    [],
                                    "next",
                                    []
                                  |),
                                  [ iter ]
                                |)
                              |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let _ :=
                                      M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                    M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ0_0 :=
                                      M.SubPointer.get_struct_tuple_field (|
                                        γ,
                                        "core::option::Option::Some",
                                        0
                                      |) in
                                    let owner := M.copy (| γ0_0 |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.apply
                                              (Ty.path "multisig::Mapping")
                                              []
                                              [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                                            "insert",
                                            []
                                          |),
                                          [
                                            M.SubPointer.get_struct_record_field (|
                                              contract,
                                              "multisig::Multisig",
                                              "is_owner"
                                            |);
                                            M.read (| M.read (| owner |) |);
                                            Value.Tuple []
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                              ]
                            |) in
                          M.alloc (| Value.Tuple [] |)))
                      |)))
                ]
              |)) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (| contract, "multisig::Multisig", "owners" |),
              M.read (| owners |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (|
                contract,
                "multisig::Multisig",
                "transaction_list"
              |),
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.path "multisig::Transactions",
                  [],
                  "default",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (|
                contract,
                "multisig::Multisig",
                "requirement"
              |),
              M.read (| requirement |)
            |) in
          contract
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      fn ensure_confirmed(&self, trans_id: TransactionId) {
          assert!(
              self.confirmation_count
                  .get(&trans_id)
                  .expect(WRONG_TRANSACTION_ID)
                  >= self.requirement
          );
      }
  *)
  Definition ensure_confirmed (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.ge (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                                  "expect",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "multisig::Mapping")
                                        []
                                        [ Ty.path "u32"; Ty.path "u32" ],
                                      "get",
                                      []
                                    |),
                                    [
                                      M.SubPointer.get_struct_record_field (|
                                        M.read (| self |),
                                        "multisig::Multisig",
                                        "confirmation_count"
                                      |);
                                      trans_id
                                    ]
                                  |);
                                  M.read (| M.get_constant (| "multisig::WRONG_TRANSACTION_ID" |) |)
                                ]
                              |),
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "multisig::Multisig",
                                  "requirement"
                                |)
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String
                                "assertion failed: self.confirmation_count.get(&trans_id).expect(WRONG_TRANSACTION_ID) >=
    self.requirement"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_confirmed :
    M.IsAssociatedFunction Self "ensure_confirmed" ensure_confirmed.
  
  (*
      fn ensure_transaction_exists(&self, trans_id: TransactionId) {
          self.transactions
              .get(&trans_id)
              .expect(WRONG_TRANSACTION_ID);
      }
  *)
  Definition ensure_transaction_exists (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "multisig::Transaction" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "multisig::Mapping")
                        []
                        [ Ty.path "u32"; Ty.path "multisig::Transaction" ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "multisig::Multisig",
                        "transactions"
                      |);
                      trans_id
                    ]
                  |);
                  M.read (| M.get_constant (| "multisig::WRONG_TRANSACTION_ID" |) |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_transaction_exists :
    M.IsAssociatedFunction Self "ensure_transaction_exists" ensure_transaction_exists.
  
  (*
      fn ensure_owner(&self, owner: &AccountId) {
          assert!(self.is_owner.contains(owner));
      }
  *)
  Definition ensure_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "multisig::Mapping")
                                  []
                                  [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                                "contains",
                                []
                              |),
                              [
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "multisig::Multisig",
                                  "is_owner"
                                |);
                                M.read (| owner |)
                              ]
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String "assertion failed: self.is_owner.contains(owner)"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_owner : M.IsAssociatedFunction Self "ensure_owner" ensure_owner.
  
  (*
      fn ensure_caller_is_owner(&self) {
          self.ensure_owner(&self.env().caller());
      }
  *)
  Definition ensure_caller_is_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "ensure_owner", [] |),
                [
                  M.read (| self |);
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Env", "caller", [] |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                            [ M.read (| self |) ]
                          |)
                        |)
                      ]
                    |)
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_caller_is_owner :
    M.IsAssociatedFunction Self "ensure_caller_is_owner" ensure_caller_is_owner.
  
  (*
      fn ensure_from_wallet(&self) {
          assert_eq!(self.env().caller(), self.env().account_id());
      }
  *)
  Definition ensure_from_wallet (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "multisig::Env", "caller", [] |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "multisig::Multisig",
                                "env",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)
                        ]
                      |)
                    |);
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "multisig::Env", "account_id", [] |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "multisig::Multisig",
                                "env",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |)
                        ]
                      |)
                    |)
                  ]
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  UnOp.not (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "multisig::AccountId",
                                        [ Ty.path "multisig::AccountId" ],
                                        "eq",
                                        []
                                      |),
                                      [ M.read (| left_val |); M.read (| right_val |) ]
                                    |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Eq" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [
                                          Ty.path "multisig::AccountId";
                                          Ty.path "multisig::AccountId"
                                        ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple "core::option::Option::None" []
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_from_wallet :
    M.IsAssociatedFunction Self "ensure_from_wallet" ensure_from_wallet.
  
  (*
      fn ensure_no_owner(&self, owner: &AccountId) {
          assert!(!self.is_owner.contains(owner));
      }
  *)
  Definition ensure_no_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            UnOp.not (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "multisig::Mapping")
                                    []
                                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                                  "contains",
                                  []
                                |),
                                [
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "multisig::Multisig",
                                    "is_owner"
                                  |);
                                  M.read (| owner |)
                                ]
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String "assertion failed: !self.is_owner.contains(owner)"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_ensure_no_owner :
    M.IsAssociatedFunction Self "ensure_no_owner" ensure_no_owner.
  
  (*
      pub fn add_owner(&mut self, new_owner: AccountId) {
          self.ensure_from_wallet();
          self.ensure_no_owner(&new_owner);
          ensure_requirement_is_valid(self.owners.len() as u32 + 1, self.requirement);
          self.is_owner.insert(new_owner, ());
          self.owners.push(new_owner);
          self.env()
              .emit_event(Event::OwnerAddition(OwnerAddition { owner: new_owner }));
      }
  *)
  Definition add_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; new_owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let new_owner := M.alloc (| new_owner |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_from_wallet",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "ensure_no_owner", [] |),
                [ M.read (| self |); new_owner ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "multisig::ensure_requirement_is_valid", [] |),
                [
                  BinOp.Wrap.add (|
                    M.rust_cast
                      (M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::vec::Vec")
                            []
                            [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                          "len",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "multisig::Multisig",
                            "owners"
                          |)
                        ]
                      |)),
                    Value.Integer IntegerKind.U32 1
                  |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "multisig::Multisig",
                      "requirement"
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "is_owner"
                  |);
                  M.read (| new_owner |);
                  Value.Tuple []
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                  "push",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "owners"
                  |);
                  M.read (| new_owner |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::OwnerAddition"
                    [
                      Value.StructRecord
                        "multisig::OwnerAddition"
                        [ ("owner", M.read (| new_owner |)) ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_add_owner : M.IsAssociatedFunction Self "add_owner" add_owner.
  
  (*
      fn owner_index(&self, owner: &AccountId) -> u32 {
          self.owners.iter().position(|x| *x == *owner).expect(
              "This is only called after it was already verified that the id is
                 actually an owner.",
          ) as u32
      }
  *)
  Definition owner_index (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.rust_cast
          (M.call_closure (|
            M.get_associated_function (|
              Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
              "expect",
              []
            |),
            [
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::iterator::Iterator",
                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "multisig::AccountId" ],
                  [],
                  "position",
                  [
                    Ty.function
                      [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "multisig::AccountId" ] ] ]
                      (Ty.path "bool")
                  ]
                |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply (Ty.path "slice") [] [ Ty.path "multisig::AccountId" ],
                        "iter",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                            [],
                            "deref",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "owners"
                            |)
                          ]
                        |)
                      ]
                    |)
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let x := M.copy (| γ |) in
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::cmp::PartialEq",
                                        Ty.path "multisig::AccountId",
                                        [ Ty.path "multisig::AccountId" ],
                                        "eq",
                                        []
                                      |),
                                      [ M.read (| x |); M.read (| owner |) ]
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |);
              M.read (|
                Value.String
                  "This is only called after it was already verified that the id is
               actually an owner."
              |)
            ]
          |))))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_owner_index : M.IsAssociatedFunction Self "owner_index" owner_index.
  
  (*
      fn clean_owner_confirmations(&mut self, owner: &AccountId) {
          for trans_id in &self.transaction_list.transactions {
              let key = ( *trans_id, *owner);
              if self.confirmations.contains(&key) {
                  self.confirmations.remove(key);
                  let mut count = self.confirmation_count.get(trans_id).unwrap_or(0 as u32);
                  count -= 1;
                  self.confirmation_count.insert( *trans_id, count);
              }
          }
      }
  *)
  Definition clean_owner_confirmations (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.read (|
          M.use
            (M.match_operator (|
              M.alloc (|
                M.call_closure (|
                  M.get_trait_method (|
                    "core::iter::traits::collect::IntoIterator",
                    Ty.apply
                      (Ty.path "&")
                      []
                      [
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ]
                      ],
                    [],
                    "into_iter",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "multisig::Multisig",
                        "transaction_list"
                      |),
                      "multisig::Transactions",
                      "transactions"
                    |)
                  ]
                |)
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let iter := M.copy (| γ |) in
                    M.loop (|
                      ltac:(M.monadic
                        (let~ _ :=
                          M.match_operator (|
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::iter::traits::iterator::Iterator",
                                  Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u32" ],
                                  [],
                                  "next",
                                  []
                                |),
                                [ iter ]
                              |)
                            |),
                            [
                              fun γ =>
                                ltac:(M.monadic
                                  (let _ :=
                                    M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                                  M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |)));
                              fun γ =>
                                ltac:(M.monadic
                                  (let γ0_0 :=
                                    M.SubPointer.get_struct_tuple_field (|
                                      γ,
                                      "core::option::Option::Some",
                                      0
                                    |) in
                                  let trans_id := M.copy (| γ0_0 |) in
                                  let~ key :=
                                    M.alloc (|
                                      Value.Tuple
                                        [
                                          M.read (| M.read (| trans_id |) |);
                                          M.read (| M.read (| owner |) |)
                                        ]
                                    |) in
                                  M.match_operator (|
                                    M.alloc (| Value.Tuple [] |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ :=
                                            M.use
                                              (M.alloc (|
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "multisig::Mapping")
                                                      []
                                                      [
                                                        Ty.tuple
                                                          [
                                                            Ty.path "u32";
                                                            Ty.path "multisig::AccountId"
                                                          ];
                                                        Ty.tuple []
                                                      ],
                                                    "contains",
                                                    []
                                                  |),
                                                  [
                                                    M.SubPointer.get_struct_record_field (|
                                                      M.read (| self |),
                                                      "multisig::Multisig",
                                                      "confirmations"
                                                    |);
                                                    key
                                                  ]
                                                |)
                                              |)) in
                                          let _ :=
                                            M.is_constant_or_break_match (|
                                              M.read (| γ |),
                                              Value.Bool true
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "multisig::Mapping")
                                                    []
                                                    [
                                                      Ty.tuple
                                                        [
                                                          Ty.path "u32";
                                                          Ty.path "multisig::AccountId"
                                                        ];
                                                      Ty.tuple []
                                                    ],
                                                  "remove",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "multisig::Multisig",
                                                    "confirmations"
                                                  |);
                                                  M.read (| key |)
                                                ]
                                              |)
                                            |) in
                                          let~ count :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.path "u32" ],
                                                  "unwrap_or",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "multisig::Mapping")
                                                        []
                                                        [ Ty.path "u32"; Ty.path "u32" ],
                                                      "get",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "multisig::Multisig",
                                                        "confirmation_count"
                                                      |);
                                                      M.read (| trans_id |)
                                                    ]
                                                  |);
                                                  M.read (|
                                                    M.use
                                                      (M.alloc (|
                                                        Value.Integer IntegerKind.U32 0
                                                      |))
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            let β := count in
                                            M.write (|
                                              β,
                                              BinOp.Wrap.sub (|
                                                M.read (| β |),
                                                Value.Integer IntegerKind.U32 1
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "multisig::Mapping")
                                                    []
                                                    [ Ty.path "u32"; Ty.path "u32" ],
                                                  "insert",
                                                  []
                                                |),
                                                [
                                                  M.SubPointer.get_struct_record_field (|
                                                    M.read (| self |),
                                                    "multisig::Multisig",
                                                    "confirmation_count"
                                                  |);
                                                  M.read (| M.read (| trans_id |) |);
                                                  M.read (| count |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (| Value.Tuple [] |)));
                                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |)))
                            ]
                          |) in
                        M.alloc (| Value.Tuple [] |)))
                    |)))
              ]
            |))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_clean_owner_confirmations :
    M.IsAssociatedFunction Self "clean_owner_confirmations" clean_owner_confirmations.
  
  (*
      pub fn remove_owner(&mut self, owner: AccountId) {
          self.ensure_from_wallet();
          self.ensure_owner(&owner);
          let len = self.owners.len() as u32 - 1;
          let requirement = u32::min(len, self.requirement);
          ensure_requirement_is_valid(len, requirement);
          let owner_index = self.owner_index(&owner) as usize;
          self.owners.swap_remove(owner_index);
          self.is_owner.remove(owner);
          self.requirement = requirement;
          self.clean_owner_confirmations(&owner);
          self.env()
              .emit_event(Event::OwnerRemoval(OwnerRemoval { owner }));
      }
  *)
  Definition remove_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let owner := M.alloc (| owner |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_from_wallet",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "ensure_owner", [] |),
                [ M.read (| self |); owner ]
              |)
            |) in
          let~ len :=
            M.alloc (|
              BinOp.Wrap.sub (|
                M.rust_cast
                  (M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "alloc::vec::Vec")
                        []
                        [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                      "len",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "multisig::Multisig",
                        "owners"
                      |)
                    ]
                  |)),
                Value.Integer IntegerKind.U32 1
              |)
            |) in
          let~ requirement :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (| "core::cmp::Ord", Ty.path "u32", [], "min", [] |),
                [
                  M.read (| len |);
                  M.read (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "multisig::Multisig",
                      "requirement"
                    |)
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "multisig::ensure_requirement_is_valid", [] |),
                [ M.read (| len |); M.read (| requirement |) ]
              |)
            |) in
          let~ owner_index :=
            M.alloc (|
              M.rust_cast
                (M.call_closure (|
                  M.get_associated_function (| Ty.path "multisig::Multisig", "owner_index", [] |),
                  [ M.read (| self |); owner ]
                |))
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                  "swap_remove",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "owners"
                  |);
                  M.read (| owner_index |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                  "remove",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "is_owner"
                  |);
                  M.read (| owner |)
                ]
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "multisig::Multisig",
                "requirement"
              |),
              M.read (| requirement |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "clean_owner_confirmations",
                  []
                |),
                [ M.read (| self |); owner ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::OwnerRemoval"
                    [ Value.StructRecord "multisig::OwnerRemoval" [ ("owner", M.read (| owner |)) ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_remove_owner : M.IsAssociatedFunction Self "remove_owner" remove_owner.
  
  (*
      pub fn replace_owner(&mut self, old_owner: AccountId, new_owner: AccountId) {
          self.ensure_from_wallet();
          self.ensure_owner(&old_owner);
          self.ensure_no_owner(&new_owner);
          let owner_index = self.owner_index(&old_owner);
          self.owners[owner_index as usize] = new_owner;
          self.is_owner.remove(old_owner);
          self.is_owner.insert(new_owner, ());
          self.clean_owner_confirmations(&old_owner);
          self.env()
              .emit_event(Event::OwnerRemoval(OwnerRemoval { owner: old_owner }));
          self.env()
              .emit_event(Event::OwnerAddition(OwnerAddition { owner: new_owner }));
      }
  *)
  Definition replace_owner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; old_owner; new_owner ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let old_owner := M.alloc (| old_owner |) in
        let new_owner := M.alloc (| new_owner |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_from_wallet",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "ensure_owner", [] |),
                [ M.read (| self |); old_owner ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "ensure_no_owner", [] |),
                [ M.read (| self |); new_owner ]
              |)
            |) in
          let~ owner_index :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Multisig", "owner_index", [] |),
                [ M.read (| self |); old_owner ]
              |)
            |) in
          let~ _ :=
            M.write (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::index::IndexMut",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                  [ Ty.path "usize" ],
                  "index_mut",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "owners"
                  |);
                  M.rust_cast (M.read (| owner_index |))
                ]
              |),
              M.read (| new_owner |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                  "remove",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "is_owner"
                  |);
                  M.read (| old_owner |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "multisig::AccountId"; Ty.tuple [] ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "is_owner"
                  |);
                  M.read (| new_owner |);
                  Value.Tuple []
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "clean_owner_confirmations",
                  []
                |),
                [ M.read (| self |); old_owner ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::OwnerRemoval"
                    [
                      Value.StructRecord
                        "multisig::OwnerRemoval"
                        [ ("owner", M.read (| old_owner |)) ]
                    ]
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::OwnerAddition"
                    [
                      Value.StructRecord
                        "multisig::OwnerAddition"
                        [ ("owner", M.read (| new_owner |)) ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_replace_owner :
    M.IsAssociatedFunction Self "replace_owner" replace_owner.
  
  (*
      pub fn change_requirement(&mut self, new_requirement: u32) {
          self.ensure_from_wallet();
          ensure_requirement_is_valid(self.owners.len() as u32, new_requirement);
          self.requirement = new_requirement;
          self.env()
              .emit_event(Event::RequirementChange(RequirementChange {
                  new_requirement,
              }));
      }
  *)
  Definition change_requirement (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; new_requirement ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let new_requirement := M.alloc (| new_requirement |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_from_wallet",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "multisig::ensure_requirement_is_valid", [] |),
                [
                  M.rust_cast
                    (M.call_closure (|
                      M.get_associated_function (|
                        Ty.apply
                          (Ty.path "alloc::vec::Vec")
                          []
                          [ Ty.path "multisig::AccountId"; Ty.path "alloc::alloc::Global" ],
                        "len",
                        []
                      |),
                      [
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "multisig::Multisig",
                          "owners"
                        |)
                      ]
                    |));
                  M.read (| new_requirement |)
                ]
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "multisig::Multisig",
                "requirement"
              |),
              M.read (| new_requirement |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::RequirementChange"
                    [
                      Value.StructRecord
                        "multisig::RequirementChange"
                        [ ("new_requirement", M.read (| new_requirement |)) ]
                    ]
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_change_requirement :
    M.IsAssociatedFunction Self "change_requirement" change_requirement.
  
  (*
      fn confirm_by_caller(
          &mut self,
          confirmer: AccountId,
          transaction: TransactionId,
      ) -> ConfirmationStatus {
          let mut count = self
              .confirmation_count
              .get(&transaction)
              .unwrap_or(0 as u32);
          let key = (transaction, confirmer);
          let new_confirmation = !self.confirmations.contains(&key);
          if new_confirmation {
              count += 1;
              self.confirmations.insert(key, ());
              self.confirmation_count.insert(transaction, count);
          }
          let status = {
              if count >= self.requirement {
                  ConfirmationStatus::Confirmed
              } else {
                  ConfirmationStatus::ConfirmationsNeeded(self.requirement - count)
              }
          };
          if new_confirmation {
              self.env().emit_event(Event::Confirmation(Confirmation {
                  transaction,
                  from: confirmer,
                  status,
              }));
          }
          status
      }
  *)
  Definition confirm_by_caller (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; confirmer; transaction ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let confirmer := M.alloc (| confirmer |) in
        let transaction := M.alloc (| transaction |) in
        M.read (|
          let~ count :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                  "unwrap_or",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply (Ty.path "multisig::Mapping") [] [ Ty.path "u32"; Ty.path "u32" ],
                      "get",
                      []
                    |),
                    [
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "multisig::Multisig",
                        "confirmation_count"
                      |);
                      transaction
                    ]
                  |);
                  M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U32 0 |)) |)
                ]
              |)
            |) in
          let~ key :=
            M.alloc (| Value.Tuple [ M.read (| transaction |); M.read (| confirmer |) ] |) in
          let~ new_confirmation :=
            M.alloc (|
              UnOp.not (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "multisig::Mapping")
                      []
                      [ Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ]; Ty.tuple [] ],
                    "contains",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "multisig::Multisig",
                      "confirmations"
                    |);
                    key
                  ]
                |)
              |)
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use new_confirmation in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      let β := count in
                      M.write (|
                        β,
                        BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U32 1 |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "multisig::Mapping")
                              []
                              [
                                Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ];
                                Ty.tuple []
                              ],
                            "insert",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "confirmations"
                            |);
                            M.read (| key |);
                            Value.Tuple []
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "multisig::Mapping")
                              []
                              [ Ty.path "u32"; Ty.path "u32" ],
                            "insert",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "confirmation_count"
                            |);
                            M.read (| transaction |);
                            M.read (| count |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          let~ status :=
            M.copy (|
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.ge (|
                              M.read (| count |),
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "multisig::Multisig",
                                  "requirement"
                                |)
                              |)
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      M.alloc (|
                        Value.StructTuple "multisig::ConfirmationStatus::Confirmed" []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "multisig::ConfirmationStatus::ConfirmationsNeeded"
                          [
                            BinOp.Wrap.sub (|
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "multisig::Multisig",
                                  "requirement"
                                |)
                              |),
                              M.read (| count |)
                            |)
                          ]
                      |)))
                ]
              |)
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ := M.use new_confirmation in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "multisig::Multisig",
                                  "env",
                                  []
                                |),
                                [ M.read (| self |) ]
                              |)
                            |);
                            Value.StructTuple
                              "multisig::Event::Confirmation"
                              [
                                Value.StructRecord
                                  "multisig::Confirmation"
                                  [
                                    ("transaction", M.read (| transaction |));
                                    ("from", M.read (| confirmer |));
                                    ("status", M.read (| status |))
                                  ]
                              ]
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          status
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_confirm_by_caller :
    M.IsAssociatedFunction Self "confirm_by_caller" confirm_by_caller.
  
  (*
      pub fn submit_transaction(
          &mut self,
          transaction: Transaction,
      ) -> (TransactionId, ConfirmationStatus) {
          self.ensure_caller_is_owner();
          let trans_id = self.transaction_list.next_id;
          self.transaction_list.next_id = trans_id
              .checked_add(1 as u32)
              .expect("Transaction ids exhausted.");
          self.transactions.insert(trans_id, transaction);
          self.transaction_list.transactions.push(trans_id);
          self.env().emit_event(Event::Submission(Submission {
              transaction: trans_id,
          }));
          (
              trans_id,
              self.confirm_by_caller(self.env().caller(), trans_id),
          )
      }
  *)
  Definition submit_transaction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; transaction ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let transaction := M.alloc (| transaction |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_caller_is_owner",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ trans_id :=
            M.copy (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "multisig::Multisig",
                  "transaction_list"
                |),
                "multisig::Transactions",
                "next_id"
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_struct_record_field (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "multisig::Multisig",
                  "transaction_list"
                |),
                "multisig::Transactions",
                "next_id"
              |),
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (| Ty.path "u32", "checked_add", [] |),
                    [
                      M.read (| trans_id |);
                      M.read (| M.use (M.alloc (| Value.Integer IntegerKind.U32 1 |)) |)
                    ]
                  |);
                  M.read (| Value.String "Transaction ids exhausted." |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "multisig::Transaction" ],
                  "insert",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "transactions"
                  |);
                  M.read (| trans_id |);
                  M.read (| transaction |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ],
                  "push",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.SubPointer.get_struct_record_field (|
                      M.read (| self |),
                      "multisig::Multisig",
                      "transaction_list"
                    |),
                    "multisig::Transactions",
                    "transactions"
                  |);
                  M.read (| trans_id |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::Submission"
                    [
                      Value.StructRecord
                        "multisig::Submission"
                        [ ("transaction", M.read (| trans_id |)) ]
                    ]
                ]
              |)
            |) in
          M.alloc (|
            Value.Tuple
              [
                M.read (| trans_id |);
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.path "multisig::Multisig",
                    "confirm_by_caller",
                    []
                  |),
                  [
                    M.read (| self |);
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Env", "caller", [] |),
                      [
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                            [ M.read (| self |) ]
                          |)
                        |)
                      ]
                    |);
                    M.read (| trans_id |)
                  ]
                |)
              ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_submit_transaction :
    M.IsAssociatedFunction Self "submit_transaction" submit_transaction.
  
  (*
      fn take_transaction(&mut self, trans_id: TransactionId) -> Option<Transaction> {
          let transaction = self.transactions.get(&trans_id);
          if transaction.is_some() {
              self.transactions.remove(trans_id);
              let pos = self
                  .transaction_list
                  .transactions
                  .iter()
                  .position(|t| t == &trans_id)
                  .expect("The transaction exists hence it must also be in the list.");
              self.transaction_list.transactions.swap_remove(pos);
              for owner in self.owners.iter() {
                  self.confirmations.remove((trans_id, *owner));
              }
              self.confirmation_count.remove(trans_id);
          }
          transaction
      }
  *)
  Definition take_transaction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ transaction :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "multisig::Mapping")
                    []
                    [ Ty.path "u32"; Ty.path "multisig::Transaction" ],
                  "get",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "multisig::Multisig",
                    "transactions"
                  |);
                  trans_id
                ]
              |)
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "core::option::Option")
                                []
                                [ Ty.path "multisig::Transaction" ],
                              "is_some",
                              []
                            |),
                            [ transaction ]
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "multisig::Mapping")
                              []
                              [ Ty.path "u32"; Ty.path "multisig::Transaction" ],
                            "remove",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "transactions"
                            |);
                            M.read (| trans_id |)
                          ]
                        |)
                      |) in
                    let~ pos :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "usize" ],
                            "expect",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::iterator::Iterator",
                                Ty.apply (Ty.path "core::slice::iter::Iter") [] [ Ty.path "u32" ],
                                [],
                                "position",
                                [
                                  Ty.function
                                    [ Ty.tuple [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ] ] ]
                                    (Ty.path "bool")
                                ]
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply (Ty.path "slice") [] [ Ty.path "u32" ],
                                      "iter",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::deref::Deref",
                                          Ty.apply
                                            (Ty.path "alloc::vec::Vec")
                                            []
                                            [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ],
                                          [],
                                          "deref",
                                          []
                                        |),
                                        [
                                          M.SubPointer.get_struct_record_field (|
                                            M.SubPointer.get_struct_record_field (|
                                              M.read (| self |),
                                              "multisig::Multisig",
                                              "transaction_list"
                                            |),
                                            "multisig::Transactions",
                                            "transactions"
                                          |)
                                        ]
                                      |)
                                    ]
                                  |)
                                |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (let t := M.copy (| γ |) in
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::cmp::PartialEq",
                                                      Ty.apply (Ty.path "&") [] [ Ty.path "u32" ],
                                                      [ Ty.apply (Ty.path "&") [] [ Ty.path "u32" ]
                                                      ],
                                                      "eq",
                                                      []
                                                    |),
                                                    [ t; M.alloc (| trans_id |) ]
                                                  |)))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |);
                            M.read (|
                              Value.String
                                "The transaction exists hence it must also be in the list."
                            |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::vec::Vec")
                              []
                              [ Ty.path "u32"; Ty.path "alloc::alloc::Global" ],
                            "swap_remove",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "multisig::Multisig",
                                "transaction_list"
                              |),
                              "multisig::Transactions",
                              "transactions"
                            |);
                            M.read (| pos |)
                          ]
                        |)
                      |) in
                    let~ _ :=
                      M.use
                        (M.match_operator (|
                          M.alloc (|
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::iter::traits::collect::IntoIterator",
                                Ty.apply
                                  (Ty.path "core::slice::iter::Iter")
                                  []
                                  [ Ty.path "multisig::AccountId" ],
                                [],
                                "into_iter",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "multisig::AccountId" ],
                                    "iter",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [
                                            Ty.path "multisig::AccountId";
                                            Ty.path "alloc::alloc::Global"
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.read (| self |),
                                          "multisig::Multisig",
                                          "owners"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let iter := M.copy (| γ |) in
                                M.loop (|
                                  ltac:(M.monadic
                                    (let~ _ :=
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::iter::traits::iterator::Iterator",
                                              Ty.apply
                                                (Ty.path "core::slice::iter::Iter")
                                                []
                                                [ Ty.path "multisig::AccountId" ],
                                              [],
                                              "next",
                                              []
                                            |),
                                            [ iter ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let _ :=
                                                M.is_struct_tuple (|
                                                  γ,
                                                  "core::option::Option::None"
                                                |) in
                                              M.alloc (|
                                                M.never_to_any (| M.read (| M.break (||) |) |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::option::Option::Some",
                                                  0
                                                |) in
                                              let owner := M.copy (| γ0_0 |) in
                                              let~ _ :=
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "multisig::Mapping")
                                                        []
                                                        [
                                                          Ty.tuple
                                                            [
                                                              Ty.path "u32";
                                                              Ty.path "multisig::AccountId"
                                                            ];
                                                          Ty.tuple []
                                                        ],
                                                      "remove",
                                                      []
                                                    |),
                                                    [
                                                      M.SubPointer.get_struct_record_field (|
                                                        M.read (| self |),
                                                        "multisig::Multisig",
                                                        "confirmations"
                                                      |);
                                                      Value.Tuple
                                                        [
                                                          M.read (| trans_id |);
                                                          M.read (| M.read (| owner |) |)
                                                        ]
                                                    ]
                                                  |)
                                                |) in
                                              M.alloc (| Value.Tuple [] |)))
                                        ]
                                      |) in
                                    M.alloc (| Value.Tuple [] |)))
                                |)))
                          ]
                        |)) in
                    let~ _ :=
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "multisig::Mapping")
                              []
                              [ Ty.path "u32"; Ty.path "u32" ],
                            "remove",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "confirmation_count"
                            |);
                            M.read (| trans_id |)
                          ]
                        |)
                      |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          transaction
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_take_transaction :
    M.IsAssociatedFunction Self "take_transaction" take_transaction.
  
  (*
      pub fn cancel_transaction(&mut self, trans_id: TransactionId) {
          self.ensure_from_wallet();
          if self.take_transaction(trans_id).is_some() {
              self.env().emit_event(Event::Cancellation(Cancellation {
                  transaction: trans_id,
              }));
          }
      }
  *)
  Definition cancel_transaction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_from_wallet",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::option::Option")
                              []
                              [ Ty.path "multisig::Transaction" ],
                            "is_some",
                            []
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "multisig::Multisig",
                                  "take_transaction",
                                  []
                                |),
                                [ M.read (| self |); M.read (| trans_id |) ]
                              |)
                            |)
                          ]
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "multisig::Multisig",
                                "env",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |);
                          Value.StructTuple
                            "multisig::Event::Cancellation"
                            [
                              Value.StructRecord
                                "multisig::Cancellation"
                                [ ("transaction", M.read (| trans_id |)) ]
                            ]
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_cancel_transaction :
    M.IsAssociatedFunction Self "cancel_transaction" cancel_transaction.
  
  (*
      pub fn confirm_transaction(&mut self, trans_id: TransactionId) -> ConfirmationStatus {
          self.ensure_caller_is_owner();
          self.ensure_transaction_exists(trans_id);
          self.confirm_by_caller(self.env().caller(), trans_id)
      }
  *)
  Definition confirm_transaction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_caller_is_owner",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_transaction_exists",
                  []
                |),
                [ M.read (| self |); M.read (| trans_id |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "multisig::Multisig", "confirm_by_caller", [] |),
              [
                M.read (| self |);
                M.call_closure (|
                  M.get_associated_function (| Ty.path "multisig::Env", "caller", [] |),
                  [
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                        [ M.read (| self |) ]
                      |)
                    |)
                  ]
                |);
                M.read (| trans_id |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_confirm_transaction :
    M.IsAssociatedFunction Self "confirm_transaction" confirm_transaction.
  
  (*
      pub fn revoke_confirmation(&mut self, trans_id: TransactionId) {
          self.ensure_caller_is_owner();
          let caller = self.env().caller();
          if self.confirmations.contains(&(trans_id, caller)) {
              self.confirmations.remove((trans_id, caller));
              let mut confirmation_count = self
                  .confirmation_count
                  .get(&trans_id)
                  .expect("There is a entry in `self.confirmations`. Hence a count must exit.");
              // Will not underflow as there is at least one confirmation
              confirmation_count -= 1;
              self.confirmation_count.insert(trans_id, confirmation_count);
              self.env().emit_event(Event::Revocation(Revocation {
                  transaction: trans_id,
                  from: caller,
              }));
          }
      }
  *)
  Definition revoke_confirmation (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_caller_is_owner",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ caller :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |)
                ]
              |)
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "multisig::Mapping")
                              []
                              [
                                Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ];
                                Ty.tuple []
                              ],
                            "contains",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_record_field (|
                              M.read (| self |),
                              "multisig::Multisig",
                              "confirmations"
                            |);
                            M.alloc (| Value.Tuple [ M.read (| trans_id |); M.read (| caller |) ] |)
                          ]
                        |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "multisig::Mapping")
                            []
                            [ Ty.tuple [ Ty.path "u32"; Ty.path "multisig::AccountId" ]; Ty.tuple []
                            ],
                          "remove",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "multisig::Multisig",
                            "confirmations"
                          |);
                          Value.Tuple [ M.read (| trans_id |); M.read (| caller |) ]
                        ]
                      |)
                    |) in
                  let~ confirmation_count :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u32" ],
                          "expect",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.apply
                                (Ty.path "multisig::Mapping")
                                []
                                [ Ty.path "u32"; Ty.path "u32" ],
                              "get",
                              []
                            |),
                            [
                              M.SubPointer.get_struct_record_field (|
                                M.read (| self |),
                                "multisig::Multisig",
                                "confirmation_count"
                              |);
                              trans_id
                            ]
                          |);
                          M.read (|
                            Value.String
                              "There is a entry in `self.confirmations`. Hence a count must exit."
                          |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    let β := confirmation_count in
                    M.write (|
                      β,
                      BinOp.Wrap.sub (| M.read (| β |), Value.Integer IntegerKind.U32 1 |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "multisig::Mapping")
                            []
                            [ Ty.path "u32"; Ty.path "u32" ],
                          "insert",
                          []
                        |),
                        [
                          M.SubPointer.get_struct_record_field (|
                            M.read (| self |),
                            "multisig::Multisig",
                            "confirmation_count"
                          |);
                          M.read (| trans_id |);
                          M.read (| confirmation_count |)
                        ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                        [
                          M.alloc (|
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "multisig::Multisig",
                                "env",
                                []
                              |),
                              [ M.read (| self |) ]
                            |)
                          |);
                          Value.StructTuple
                            "multisig::Event::Revocation"
                            [
                              Value.StructRecord
                                "multisig::Revocation"
                                [
                                  ("transaction", M.read (| trans_id |));
                                  ("from", M.read (| caller |))
                                ]
                            ]
                        ]
                      |)
                    |) in
                  M.alloc (| Value.Tuple [] |)));
              fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_revoke_confirmation :
    M.IsAssociatedFunction Self "revoke_confirmation" revoke_confirmation.
  
  (*
      pub fn invoke_transaction(&mut self, trans_id: TransactionId) -> Result<(), Error> {
          self.ensure_confirmed(trans_id);
          let t = self.take_transaction(trans_id).expect(WRONG_TRANSACTION_ID);
          assert!(self.env().transferred_value() == t.transferred_value);
          // let result = build_call()
          //     .call(t.callee)
          //     .gas_limit(t.gas_limit)
          //     .transferred_value(t.transferred_value)
          //     .call_flags(CallFlags::default().set_allow_reentry(t.allow_reentry))
          //     .exec_input(ExecutionInput::new(t.selector.into()).push_arg(CallInput(&t.input)))
          //     .returns::<()>()
          //     .try_invoke();
          let result: Result<Result<Vec<u8>, ()>, ()> = todo!();
  
          let result = match result {
              Ok(Ok(_)) => Ok(()),
              _ => Err(Error::TransactionFailed),
          };
  
          self.env().emit_event(Event::Execution(Execution {
              transaction: trans_id,
              result: result.map(|_| None),
          }));
          result
      }
  *)
  Definition invoke_transaction (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; trans_id ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let trans_id := M.alloc (| trans_id |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "multisig::Multisig",
                  "ensure_confirmed",
                  []
                |),
                [ M.read (| self |); M.read (| trans_id |) ]
              |)
            |) in
          let~ t :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "multisig::Transaction" ],
                  "expect",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "multisig::Multisig",
                      "take_transaction",
                      []
                    |),
                    [ M.read (| self |); M.read (| trans_id |) ]
                  |);
                  M.read (| M.get_constant (| "multisig::WRONG_TRANSACTION_ID" |) |)
                ]
              |)
            |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.eq (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.path "multisig::Env",
                                  "transferred_value",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "multisig::Multisig",
                                        "env",
                                        []
                                      |),
                                      [ M.read (| self |) ]
                                    |)
                                  |)
                                ]
                              |),
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  t,
                                  "multisig::Transaction",
                                  "transferred_value"
                                |)
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String
                                "assertion failed: self.env().transferred_value() == t.transferred_value"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          let~ result :=
            M.alloc (|
              M.never_to_any (|
                M.call_closure (|
                  M.get_function (| "core::panicking::panic", [] |),
                  [ M.read (| Value.String "not yet implemented" |) ]
                |)
              |)
            |) in
          let~ result :=
            M.copy (|
              M.match_operator (|
                result,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "core::result::Result::Ok",
                          0
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "multisig::Error::TransactionFailed" [] ]
                      |)))
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (| Ty.path "multisig::Env", "emit_event", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "multisig::Multisig", "env", [] |),
                      [ M.read (| self |) ]
                    |)
                  |);
                  Value.StructTuple
                    "multisig::Event::Execution"
                    [
                      Value.StructRecord
                        "multisig::Execution"
                        [
                          ("transaction", M.read (| trans_id |));
                          ("result",
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.tuple []; Ty.path "multisig::Error" ],
                                "map",
                                [
                                  Ty.apply
                                    (Ty.path "core::option::Option")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "alloc::vec::Vec")
                                        []
                                        [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                                    ];
                                  Ty.function
                                    [ Ty.tuple [ Ty.tuple [] ] ]
                                    (Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [
                                        Ty.apply
                                          (Ty.path "alloc::vec::Vec")
                                          []
                                          [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                                      ])
                                ]
                              |),
                              [
                                M.read (| result |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (Value.StructTuple
                                                    "core::option::Option::None"
                                                    []))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |))
                        ]
                    ]
                ]
              |)
            |) in
          result
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_invoke_transaction :
    M.IsAssociatedFunction Self "invoke_transaction" invoke_transaction.
  
  (*
      pub fn eval_transaction(&mut self, trans_id: TransactionId) -> Result<Vec<u8>, Error> {
          self.ensure_confirmed(trans_id);
          let t = self.take_transaction(trans_id).expect(WRONG_TRANSACTION_ID);
          // let result = build_call()
          //     .call(t.callee)
          //     .gas_limit(t.gas_limit)
          //     .transferred_value(t.transferred_value)
          //     .call_flags(CallFlags::default().set_allow_reentry(t.allow_reentry))
          //     .exec_input(ExecutionInput::new(t.selector.into()).push_arg(CallInput(&t.input)))
          //     .returns::<Vec<u8>>()
          //     .try_invoke();
          let result: Result<Result<Vec<u8>, ()>, ()> = todo!();
  
          let result = match result {
              Ok(Ok(v)) => Ok(v),
              _ => Err(Error::TransactionFailed),
          };
  
          self.env().emit_event(Event::Execution(Execution {
              transaction: trans_id,
              result: result.clone().map(Some),
          }));
          result
      }
  *)
  Parameter eval_transaction : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_eval_transaction :
    M.IsAssociatedFunction Self "eval_transaction" eval_transaction.
End Impl_multisig_Multisig.
