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

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

Module Impl_core_default_Default_for_payment_channel_AccountId.
  Definition Self : Ty.t := Ty.path "payment_channel::AccountId".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructTuple
          "payment_channel::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_payment_channel_AccountId.

Module Impl_core_clone_Clone_for_payment_channel_AccountId.
  Definition Self : Ty.t := Ty.path "payment_channel::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_payment_channel_AccountId.

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

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

Module Impl_core_cmp_PartialEq_for_payment_channel_AccountId.
  Definition Self : Ty.t := Ty.path "payment_channel::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 |),
              "payment_channel::AccountId",
              0
            |)
          |),
          M.read (|
            M.SubPointer.get_struct_tuple_field (|
              M.read (| other |),
              "payment_channel::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_payment_channel_AccountId.

Module Impl_core_cmp_Eq_for_payment_channel_AccountId.
  Definition Self : Ty.t := Ty.path "payment_channel::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_payment_channel_AccountId.

Module Impl_core_convert_From_array_Usize_32_u8_for_payment_channel_AccountId.
  Definition Self : Ty.t := Ty.path "payment_channel::AccountId".
  
  (*
      fn from(value: [u8; 32]) -> Self {
          unimplemented!()
      }
  *)
  Parameter from : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *)
      [ (* T *) Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ] ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_array_Usize_32_u8_for_payment_channel_AccountId.

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

Axiom Timestamp : (Ty.path "payment_channel::Timestamp") = (Ty.path "u64").

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

(* StructRecord
  {
    name := "PaymentChannel";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("sender", Ty.path "payment_channel::AccountId");
        ("recipient", Ty.path "payment_channel::AccountId");
        ("expiration", Ty.apply (Ty.path "core::option::Option") [] [ Ty.path "u64" ]);
        ("withdrawn", Ty.path "u128");
        ("close_duration", Ty.path "u64")
      ];
  } *)

(*
Enum Error
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "CallerIsNotSender";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "CallerIsNotRecipient";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "AmountIsLessThanWithdrawn";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "TransferFailed";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "NotYetExpired";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "InvalidSignature";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

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

Module Impl_core_cmp_PartialEq_for_payment_channel_Error.
  Definition Self : Ty.t := Ty.path "payment_channel::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
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "payment_channel::Error" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "payment_channel::Error" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (| BinOp.eq (| M.read (| __self_discr |), M.read (| __arg1_discr |) |) |)
        |)))
    | _, _, _ => 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_payment_channel_Error.

Module Impl_core_cmp_Eq_for_payment_channel_Error.
  Definition Self : Ty.t := Ty.path "payment_channel::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_payment_channel_Error.

Axiom Result :
  forall (T : Ty.t),
  (Ty.apply (Ty.path "payment_channel::Result") [] [ T ]) =
    (Ty.apply (Ty.path "core::result::Result") [] [ T; Ty.path "payment_channel::Error" ]).

(* StructRecord
  {
    name := "SenderCloseStarted";
    const_params := [];
    ty_params := [];
    fields := [ ("expiration", Ty.path "u64"); ("close_duration", Ty.path "u64") ];
  } *)

(*
Enum Event
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "SenderCloseStarted";
        item := StructTuple [ Ty.path "payment_channel::SenderCloseStarted" ];
        discriminant := None;
      }
    ];
}
*)

Module Impl_payment_channel_Env.
  Definition Self : Ty.t := Ty.path "payment_channel::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 |),
            "payment_channel::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 terminate_contract(&self, sender: AccountId) {
          unimplemented!()
      }
  *)
  Parameter terminate_contract : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_terminate_contract :
    M.IsAssociatedFunction Self "terminate_contract" terminate_contract.
  
  (*
      fn transfer(&self, recipient: AccountId, amount: Balance) -> Result<()> {
          unimplemented!()
      }
  *)
  Parameter transfer : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_transfer : M.IsAssociatedFunction Self "transfer" transfer.
  
  (*
      fn block_timestamp(&self) -> Timestamp {
          unimplemented!()
      }
  *)
  Parameter block_timestamp : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_block_timestamp :
    M.IsAssociatedFunction Self "block_timestamp" block_timestamp.
  
  (*
      fn balance(&self) -> Balance {
          unimplemented!()
      }
  *)
  Parameter balance : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom AssociatedFunction_balance : M.IsAssociatedFunction Self "balance" balance.
  
  (*
      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_payment_channel_Env.

(* Trait *)
(* Empty module 'HashOutput' *)

(* Trait *)
(* Empty module 'CryptoHash' *)

(*
pub fn hash_encoded<H, T>(input: &T, output: &mut <H as HashOutput>::Type)
where
    H: CryptoHash,
{
    unimplemented!()
}
*)
Parameter hash_encoded : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_hash_encoded : M.IsFunction "payment_channel::hash_encoded" hash_encoded.

(*
pub fn ecdsa_recover(
    signature: &[u8; 65],
    message_hash: &[u8; 32],
    output: &mut [u8; 33],
) -> Result<()> {
    unimplemented!()
}
*)
Parameter ecdsa_recover : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.

Axiom Function_ecdsa_recover : M.IsFunction "payment_channel::ecdsa_recover" ecdsa_recover.

(*
Enum Sha2x256
{
  const_params := [];
  ty_params := [];
  variants := [];
}
*)

(*
Enum Keccak256
{
  const_params := [];
  ty_params := [];
  variants := [];
}
*)

(*
Enum Blake2x256
{
  const_params := [];
  ty_params := [];
  variants := [];
}
*)

(*
Enum Blake2x128
{
  const_params := [];
  ty_params := [];
  variants := [];
}
*)

Module Impl_payment_channel_HashOutput_for_payment_channel_Sha2x256.
  Definition Self : Ty.t := Ty.path "payment_channel::Sha2x256".
  
  (*     type Type = [u8; 32]; *)
  Definition _Type_ : Ty.t :=
    Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ].
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::HashOutput"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("Type_", InstanceField.Ty _Type_) ].
End Impl_payment_channel_HashOutput_for_payment_channel_Sha2x256.

Module Impl_payment_channel_HashOutput_for_payment_channel_Keccak256.
  Definition Self : Ty.t := Ty.path "payment_channel::Keccak256".
  
  (*     type Type = [u8; 32]; *)
  Definition _Type_ : Ty.t :=
    Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ].
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::HashOutput"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("Type_", InstanceField.Ty _Type_) ].
End Impl_payment_channel_HashOutput_for_payment_channel_Keccak256.

Module Impl_payment_channel_HashOutput_for_payment_channel_Blake2x256.
  Definition Self : Ty.t := Ty.path "payment_channel::Blake2x256".
  
  (*     type Type = [u8; 32]; *)
  Definition _Type_ : Ty.t :=
    Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 32 ] [ Ty.path "u8" ].
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::HashOutput"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("Type_", InstanceField.Ty _Type_) ].
End Impl_payment_channel_HashOutput_for_payment_channel_Blake2x256.

Module Impl_payment_channel_HashOutput_for_payment_channel_Blake2x128.
  Definition Self : Ty.t := Ty.path "payment_channel::Blake2x128".
  
  (*     type Type = [u8; 16]; *)
  Definition _Type_ : Ty.t :=
    Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 16 ] [ Ty.path "u8" ].
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::HashOutput"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("Type_", InstanceField.Ty _Type_) ].
End Impl_payment_channel_HashOutput_for_payment_channel_Blake2x128.

Module Impl_payment_channel_CryptoHash_for_payment_channel_Sha2x256.
  Definition Self : Ty.t := Ty.path "payment_channel::Sha2x256".
  
  (*
      fn hash(input: &[u8], output: &mut <Self as HashOutput>::Type) {
          unimplemented!()
      }
  *)
  Parameter hash : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::CryptoHash"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("hash", InstanceField.Method hash) ].
End Impl_payment_channel_CryptoHash_for_payment_channel_Sha2x256.

Module Impl_payment_channel_CryptoHash_for_payment_channel_Keccak256.
  Definition Self : Ty.t := Ty.path "payment_channel::Keccak256".
  
  (*
      fn hash(input: &[u8], output: &mut <Self as HashOutput>::Type) {
          unimplemented!()
      }
  *)
  Parameter hash : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::CryptoHash"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("hash", InstanceField.Method hash) ].
End Impl_payment_channel_CryptoHash_for_payment_channel_Keccak256.

Module Impl_payment_channel_CryptoHash_for_payment_channel_Blake2x256.
  Definition Self : Ty.t := Ty.path "payment_channel::Blake2x256".
  
  (*
      fn hash(input: &[u8], output: &mut <Self as HashOutput>::Type) {
          unimplemented!()
      }
  *)
  Parameter hash : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::CryptoHash"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("hash", InstanceField.Method hash) ].
End Impl_payment_channel_CryptoHash_for_payment_channel_Blake2x256.

Module Impl_payment_channel_CryptoHash_for_payment_channel_Blake2x128.
  Definition Self : Ty.t := Ty.path "payment_channel::Blake2x128".
  
  (*
      fn hash(input: &[u8], output: &mut <Self as HashOutput>::Type) {
          unimplemented!()
      }
  *)
  Parameter hash : (list Value.t) -> (list Ty.t) -> (list Value.t) -> M.
  
  Axiom Implements :
    M.IsTraitInstance
      "payment_channel::CryptoHash"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("hash", InstanceField.Method hash) ].
End Impl_payment_channel_CryptoHash_for_payment_channel_Blake2x128.

Module Impl_payment_channel_PaymentChannel.
  Definition Self : Ty.t := Ty.path "payment_channel::PaymentChannel".
  
  (*
      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 "payment_channel::PaymentChannel", "init_env", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_env : M.IsAssociatedFunction Self "env" env.
  
  (*
      fn is_signature_valid(&self, amount: Balance, signature: [u8; 65]) -> bool {
          let encodable = (self.env().account_id(), amount);
          let mut message = <Sha2x256 as HashOutput>::Type::default();
          hash_encoded::<Sha2x256, _>(&encodable, &mut message);
  
          let mut pub_key = [0; 33];
          ecdsa_recover(&signature, &message, &mut pub_key)
              .unwrap_or_else(|err| panic!("recover failed: {err:?}"));
          let mut signature_account_id = [0; 32];
          <Blake2x256 as CryptoHash>::hash(&pub_key, &mut signature_account_id);
  
          self.recipient == signature_account_id.into()
      }
  *)
  Definition is_signature_valid (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; amount; signature ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let amount := M.alloc (| amount |) in
        let signature := M.alloc (| signature |) in
        M.read (|
          let~ encodable :=
            M.alloc (|
              Value.Tuple
                [
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "payment_channel::Env",
                      "account_id",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "payment_channel::PaymentChannel",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |);
                  M.read (| amount |)
                ]
            |) in
          let~ message :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [ Ty.path "u8" ],
                  [],
                  "default",
                  []
                |),
                []
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "payment_channel::hash_encoded",
                  [
                    Ty.path "payment_channel::Sha2x256";
                    Ty.tuple [ Ty.path "payment_channel::AccountId"; Ty.path "u128" ]
                  ]
                |),
                [ encodable; message ]
              |)
            |) in
          let~ pub_key :=
            M.alloc (|
              repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 33 |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "core::result::Result")
                    []
                    [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                  "unwrap_or_else",
                  [ Ty.function [ Ty.tuple [ Ty.path "payment_channel::Error" ] ] (Ty.tuple []) ]
                |),
                [
                  M.call_closure (|
                    M.get_function (| "payment_channel::ecdsa_recover", [] |),
                    [ signature; message; pub_key ]
                  |);
                  M.closure
                    (fun γ =>
                      ltac:(M.monadic
                        match γ with
                        | [ α0 ] =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| α0 |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let err := M.copy (| γ |) in
                                    M.never_to_any (|
                                      M.call_closure (|
                                        M.get_function (|
                                          "std::panicking::begin_panic",
                                          [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ]
                                        |),
                                        [ M.read (| Value.String "recover failed: {err:?}" |) ]
                                      |)
                                    |)))
                              ]
                            |)))
                        | _ => M.impossible "wrong number of arguments"
                        end))
                ]
              |)
            |) in
          let~ signature_account_id :=
            M.alloc (|
              repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 32 |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "payment_channel::CryptoHash",
                  Ty.path "payment_channel::Blake2x256",
                  [],
                  "hash",
                  []
                |),
                [ pub_key; signature_account_id ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.path "payment_channel::AccountId",
                [ Ty.path "payment_channel::AccountId" ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "payment_channel::PaymentChannel",
                  "recipient"
                |);
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::Into",
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 32 ]
                        [ Ty.path "u8" ],
                      [ Ty.path "payment_channel::AccountId" ],
                      "into",
                      []
                    |),
                    [ M.read (| signature_account_id |) ]
                  |)
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_signature_valid :
    M.IsAssociatedFunction Self "is_signature_valid" is_signature_valid.
  
  (*
      pub fn new(recipient: AccountId, close_duration: Timestamp) -> Self {
          Self {
              sender: Self::init_env().caller(),
              recipient,
              expiration: None,
              withdrawn: 0,
              close_duration,
          }
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ recipient; close_duration ] =>
      ltac:(M.monadic
        (let recipient := M.alloc (| recipient |) in
        let close_duration := M.alloc (| close_duration |) in
        Value.StructRecord
          "payment_channel::PaymentChannel"
          [
            ("sender",
              M.call_closure (|
                M.get_associated_function (| Ty.path "payment_channel::Env", "caller", [] |),
                [
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "payment_channel::PaymentChannel",
                        "init_env",
                        []
                      |),
                      []
                    |)
                  |)
                ]
              |));
            ("recipient", M.read (| recipient |));
            ("expiration", Value.StructTuple "core::option::Option::None" []);
            ("withdrawn", Value.Integer IntegerKind.U128 0);
            ("close_duration", M.read (| close_duration |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      fn close_inner(&mut self, amount: Balance, signature: [u8; 65]) -> Result<()> {
          if self.env().caller() != self.recipient {
              return Err(Error::CallerIsNotRecipient);
          }
  
          if amount < self.withdrawn {
              return Err(Error::AmountIsLessThanWithdrawn);
          }
  
          // Signature validation
          if !self.is_signature_valid(amount, signature) {
              return Err(Error::InvalidSignature);
          }
  
          self.env()
              .transfer(self.recipient, amount - self.withdrawn)
              .map_err(|_| Error::TransferFailed)?;
  
          Ok(())
      }
  *)
  Definition close_inner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; amount; signature ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let amount := M.alloc (| amount |) in
        let signature := M.alloc (| signature |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "payment_channel::AccountId",
                                  [ Ty.path "payment_channel::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "payment_channel::Env",
                                        "caller",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "payment_channel::PaymentChannel",
                                              "env",
                                              []
                                            |),
                                            [ M.read (| self |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "recipient"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "payment_channel::Error::CallerIsNotRecipient"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| amount |),
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "withdrawn"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "payment_channel::Error::AmountIsLessThanWithdrawn"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              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.path "payment_channel::PaymentChannel",
                                    "is_signature_valid",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| amount |); M.read (| signature |) ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "payment_channel::Error::InvalidSignature" []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                            "map_err",
                            [
                              Ty.path "payment_channel::Error";
                              Ty.function
                                [ Ty.tuple [ Ty.path "payment_channel::Error" ] ]
                                (Ty.path "payment_channel::Error")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "payment_channel::Env",
                                "transfer",
                                []
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "payment_channel::PaymentChannel",
                                      "env",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "recipient"
                                  |)
                                |);
                                BinOp.Wrap.sub (|
                                  M.read (| amount |),
                                  M.read (|
                                    M.SubPointer.get_struct_record_field (|
                                      M.read (| self |),
                                      "payment_channel::PaymentChannel",
                                      "withdrawn"
                                    |)
                                  |)
                                |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (Value.StructTuple
                                                "payment_channel::Error::TransferFailed"
                                                []))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "payment_channel::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_close_inner : M.IsAssociatedFunction Self "close_inner" close_inner.
  
  (*
      pub fn close(&mut self, amount: Balance, signature: [u8; 65]) -> Result<()> {
          self.close_inner(amount, signature)?;
          self.env().terminate_contract(self.sender);
  
          Ok(())
      }
  *)
  Definition close (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; amount; signature ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let amount := M.alloc (| amount |) in
        let signature := M.alloc (| signature |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "payment_channel::PaymentChannel",
                            "close_inner",
                            []
                          |),
                          [ M.read (| self |); M.read (| amount |); M.read (| signature |) ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "payment_channel::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "payment_channel::Env",
                      "terminate_contract",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "payment_channel::PaymentChannel",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      M.read (|
                        M.SubPointer.get_struct_record_field (|
                          M.read (| self |),
                          "payment_channel::PaymentChannel",
                          "sender"
                        |)
                      |)
                    ]
                  |)
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_close : M.IsAssociatedFunction Self "close" close.
  
  (*
      pub fn start_sender_close(&mut self) -> Result<()> {
          if self.env().caller() != self.sender {
              return Err(Error::CallerIsNotSender);
          }
  
          let now = self.env().block_timestamp();
          let expiration = now + self.close_duration;
  
          self.env()
              .emit_event(Event::SenderCloseStarted(SenderCloseStarted {
                  expiration,
                  close_duration: self.close_duration,
              }));
  
          self.expiration = Some(expiration);
  
          Ok(())
      }
  *)
  Definition start_sender_close (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "payment_channel::AccountId",
                                  [ Ty.path "payment_channel::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "payment_channel::Env",
                                        "caller",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "payment_channel::PaymentChannel",
                                              "env",
                                              []
                                            |),
                                            [ M.read (| self |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "sender"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "payment_channel::Error::CallerIsNotSender" []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ now :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "payment_channel::Env",
                      "block_timestamp",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "payment_channel::PaymentChannel",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |)
                    ]
                  |)
                |) in
              let~ expiration :=
                M.alloc (|
                  BinOp.Wrap.add (|
                    M.read (| now |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "payment_channel::PaymentChannel",
                        "close_duration"
                      |)
                    |)
                  |)
                |) in
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.path "payment_channel::Env",
                      "emit_event",
                      []
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "payment_channel::PaymentChannel",
                            "env",
                            []
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      Value.StructTuple
                        "payment_channel::Event::SenderCloseStarted"
                        [
                          Value.StructRecord
                            "payment_channel::SenderCloseStarted"
                            [
                              ("expiration", M.read (| expiration |));
                              ("close_duration",
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "close_duration"
                                  |)
                                |))
                            ]
                        ]
                    ]
                  |)
                |) in
              let~ _ :=
                M.write (|
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "payment_channel::PaymentChannel",
                    "expiration"
                  |),
                  Value.StructTuple "core::option::Option::Some" [ M.read (| expiration |) ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_start_sender_close :
    M.IsAssociatedFunction Self "start_sender_close" start_sender_close.
  
  (*
      pub fn claim_timeout(&mut self) -> Result<()> {
          match self.expiration {
              Some(expiration) => {
                  // expiration is set. Check if it's reached and if so, release the
                  // funds and terminate the contract.
                  let now = self.env().block_timestamp();
                  if now < expiration {
                      return Err(Error::NotYetExpired);
                  }
  
                  self.env().terminate_contract(self.sender);
  
                  Ok(())
              }
  
              None => Err(Error::NotYetExpired),
          }
      }
  *)
  Definition claim_timeout (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              M.match_operator (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "payment_channel::PaymentChannel",
                  "expiration"
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::option::Option::Some",
                          0
                        |) in
                      let expiration := M.copy (| γ0_0 |) in
                      let~ now :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "payment_channel::Env",
                              "block_timestamp",
                              []
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "payment_channel::PaymentChannel",
                                    "env",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |)
                            ]
                          |)
                        |) in
                      let~ _ :=
                        M.match_operator (|
                          M.alloc (| Value.Tuple [] |),
                          [
                            fun γ =>
                              ltac:(M.monadic
                                (let γ :=
                                  M.use
                                    (M.alloc (|
                                      BinOp.lt (| M.read (| now |), M.read (| expiration |) |)
                                    |)) in
                                let _ :=
                                  M.is_constant_or_break_match (|
                                    M.read (| γ |),
                                    Value.Bool true
                                  |) in
                                M.alloc (|
                                  M.never_to_any (|
                                    M.read (|
                                      M.return_ (|
                                        Value.StructTuple
                                          "core::result::Result::Err"
                                          [
                                            Value.StructTuple
                                              "payment_channel::Error::NotYetExpired"
                                              []
                                          ]
                                      |)
                                    |)
                                  |)
                                |)));
                            fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                          ]
                        |) in
                      let~ _ :=
                        M.alloc (|
                          M.call_closure (|
                            M.get_associated_function (|
                              Ty.path "payment_channel::Env",
                              "terminate_contract",
                              []
                            |),
                            [
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "payment_channel::PaymentChannel",
                                    "env",
                                    []
                                  |),
                                  [ M.read (| self |) ]
                                |)
                              |);
                              M.read (|
                                M.SubPointer.get_struct_record_field (|
                                  M.read (| self |),
                                  "payment_channel::PaymentChannel",
                                  "sender"
                                |)
                              |)
                            ]
                          |)
                        |) in
                      M.alloc (|
                        Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ]
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
                      M.alloc (|
                        Value.StructTuple
                          "core::result::Result::Err"
                          [ Value.StructTuple "payment_channel::Error::NotYetExpired" [] ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_claim_timeout :
    M.IsAssociatedFunction Self "claim_timeout" claim_timeout.
  
  (*
      pub fn withdraw(&mut self, amount: Balance, signature: [u8; 65]) -> Result<()> {
          if self.env().caller() != self.recipient {
              return Err(Error::CallerIsNotRecipient);
          }
  
          // Signature validation
          if !self.is_signature_valid(amount, signature) {
              return Err(Error::InvalidSignature);
          }
  
          // Make sure there's something to withdraw (guards against underflow)
          if amount < self.withdrawn {
              return Err(Error::AmountIsLessThanWithdrawn);
          }
  
          let amount_to_withdraw = amount - self.withdrawn;
          self.withdrawn += amount_to_withdraw;
  
          self.env()
              .transfer(self.recipient, amount_to_withdraw)
              .map_err(|_| Error::TransferFailed)?;
  
          Ok(())
      }
  *)
  Definition withdraw (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; amount; signature ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let amount := M.alloc (| amount |) in
        let signature := M.alloc (| signature |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.path "payment_channel::AccountId",
                                  [ Ty.path "payment_channel::AccountId" ],
                                  "ne",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "payment_channel::Env",
                                        "caller",
                                        []
                                      |),
                                      [
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "payment_channel::PaymentChannel",
                                              "env",
                                              []
                                            |),
                                            [ M.read (| self |) ]
                                          |)
                                        |)
                                      ]
                                    |)
                                  |);
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "recipient"
                                  |)
                                ]
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "payment_channel::Error::CallerIsNotRecipient"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              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.path "payment_channel::PaymentChannel",
                                    "is_signature_valid",
                                    []
                                  |),
                                  [ M.read (| self |); M.read (| amount |); M.read (| signature |) ]
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [ Value.StructTuple "payment_channel::Error::InvalidSignature" []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| amount |),
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "withdrawn"
                                  |)
                                |)
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                Value.StructTuple
                                  "core::result::Result::Err"
                                  [
                                    Value.StructTuple
                                      "payment_channel::Error::AmountIsLessThanWithdrawn"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ amount_to_withdraw :=
                M.alloc (|
                  BinOp.Wrap.sub (|
                    M.read (| amount |),
                    M.read (|
                      M.SubPointer.get_struct_record_field (|
                        M.read (| self |),
                        "payment_channel::PaymentChannel",
                        "withdrawn"
                      |)
                    |)
                  |)
                |) in
              let~ _ :=
                let β :=
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "payment_channel::PaymentChannel",
                    "withdrawn"
                  |) in
                M.write (|
                  β,
                  BinOp.Wrap.add (| M.read (| β |), M.read (| amount_to_withdraw |) |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::ops::try_trait::Try",
                        Ty.apply
                          (Ty.path "core::result::Result")
                          []
                          [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                        [],
                        "branch",
                        []
                      |),
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                            "map_err",
                            [
                              Ty.path "payment_channel::Error";
                              Ty.function
                                [ Ty.tuple [ Ty.path "payment_channel::Error" ] ]
                                (Ty.path "payment_channel::Error")
                            ]
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.path "payment_channel::Env",
                                "transfer",
                                []
                              |),
                              [
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.path "payment_channel::PaymentChannel",
                                      "env",
                                      []
                                    |),
                                    [ M.read (| self |) ]
                                  |)
                                |);
                                M.read (|
                                  M.SubPointer.get_struct_record_field (|
                                    M.read (| self |),
                                    "payment_channel::PaymentChannel",
                                    "recipient"
                                  |)
                                |);
                                M.read (| amount_to_withdraw |)
                              ]
                            |);
                            M.closure
                              (fun γ =>
                                ltac:(M.monadic
                                  match γ with
                                  | [ α0 ] =>
                                    ltac:(M.monadic
                                      (M.match_operator (|
                                        M.alloc (| α0 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (Value.StructTuple
                                                "payment_channel::Error::TransferFailed"
                                                []))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      ]
                    |)
                  |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Break",
                            0
                          |) in
                        let residual := M.copy (| γ0_0 |) in
                        M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              M.return_ (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::try_trait::FromResidual",
                                    Ty.apply
                                      (Ty.path "core::result::Result")
                                      []
                                      [ Ty.tuple []; Ty.path "payment_channel::Error" ],
                                    [
                                      Ty.apply
                                        (Ty.path "core::result::Result")
                                        []
                                        [
                                          Ty.path "core::convert::Infallible";
                                          Ty.path "payment_channel::Error"
                                        ]
                                    ],
                                    "from_residual",
                                    []
                                  |),
                                  [ M.read (| residual |) ]
                                |)
                              |)
                            |)
                          |)
                        |)));
                    fun γ =>
                      ltac:(M.monadic
                        (let γ0_0 :=
                          M.SubPointer.get_struct_tuple_field (|
                            γ,
                            "core::ops::control_flow::ControlFlow::Continue",
                            0
                          |) in
                        let val := M.copy (| γ0_0 |) in
                        val))
                  ]
                |) in
              M.alloc (| Value.StructTuple "core::result::Result::Ok" [ Value.Tuple [] ] |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_withdraw : M.IsAssociatedFunction Self "withdraw" withdraw.
  
  (*
      pub fn get_sender(&self) -> AccountId {
          self.sender
      }
  *)
  Definition get_sender (ε : 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 |),
            "payment_channel::PaymentChannel",
            "sender"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_sender : M.IsAssociatedFunction Self "get_sender" get_sender.
  
  (*
      pub fn get_recipient(&self) -> AccountId {
          self.recipient
      }
  *)
  Definition get_recipient (ε : 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 |),
            "payment_channel::PaymentChannel",
            "recipient"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_recipient :
    M.IsAssociatedFunction Self "get_recipient" get_recipient.
  
  (*
      pub fn get_expiration(&self) -> Option<Timestamp> {
          self.expiration
      }
  *)
  Definition get_expiration (ε : 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 |),
            "payment_channel::PaymentChannel",
            "expiration"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_expiration :
    M.IsAssociatedFunction Self "get_expiration" get_expiration.
  
  (*
      pub fn get_withdrawn(&self) -> Balance {
          self.withdrawn
      }
  *)
  Definition get_withdrawn (ε : 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 |),
            "payment_channel::PaymentChannel",
            "withdrawn"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_withdrawn :
    M.IsAssociatedFunction Self "get_withdrawn" get_withdrawn.
  
  (*
      pub fn get_close_duration(&self) -> Timestamp {
          self.close_duration
      }
  *)
  Definition get_close_duration (ε : 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 |),
            "payment_channel::PaymentChannel",
            "close_duration"
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_close_duration :
    M.IsAssociatedFunction Self "get_close_duration" get_close_duration.
  
  (*
      pub fn get_balance(&self) -> Balance {
          self.env().balance()
      }
  *)
  Definition get_balance (ε : 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 "payment_channel::Env", "balance", [] |),
          [
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.path "payment_channel::PaymentChannel",
                  "env",
                  []
                |),
                [ M.read (| self |) ]
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_balance : M.IsAssociatedFunction Self "get_balance" get_balance.
End Impl_payment_channel_PaymentChannel.
