ink_env.v

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

Require CoqOfRust.ink.ink_primitives.
Require CoqOfRust.ink.ink_storage_traits.
Require CoqOfRust.ink.parity_scale_codec.
Require CoqOfRust.ink.scale_decode.
Require CoqOfRust.ink.scale_encode.
Require CoqOfRust.ink.ink_engine.

Module arithmetic.
  Module Saturating.
    Class Trait (Self : Set) : Type := {
      saturating_add `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
      saturating_sub `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
      saturating_mul `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
      saturating_pow `{H' : State.Trait} : Self -> usize -> M (H := H') Self;
    }.
    
    Global Instance Method_saturating_add `{H' : State.Trait} `(Trait)
      : Notation.Dot "saturating_add" := {
      Notation.dot := saturating_add;
    }.
    Global Instance Method_saturating_sub `{H' : State.Trait} `(Trait)
      : Notation.Dot "saturating_sub" := {
      Notation.dot := saturating_sub;
    }.
    Global Instance Method_saturating_mul `{H' : State.Trait} `(Trait)
      : Notation.Dot "saturating_mul" := {
      Notation.dot := saturating_mul;
    }.
    Global Instance Method_saturating_pow `{H' : State.Trait} `(Trait)
      : Notation.Dot "saturating_pow" := {
      Notation.dot := saturating_pow;
    }.
  End Saturating.
  
  Module BaseArithmetic.
    Unset Primitive Projections.
    Class Trait
        (Self : Set)
        `{core.marker.Sized.Trait Self}
        `{core.convert.From.Trait Self (T := u8)}
        `{num_traits.bounds.Bounded.Trait Self}
        `{core.cmp.Ord.Trait Self}
        `{core.cmp.PartialOrd.Trait Self (Rhs := Self)}
        `{num_traits.identities.Zero.Trait Self}
        `{num_traits.identities.One.Trait Self}
        `{num_traits.bounds.Bounded.Trait Self}
        `{core.ops.arith.Add.Trait Self (Rhs := Self)}
        `{core.ops.arith.AddAssign.Trait Self (Rhs := Self)}
        `{core.ops.arith.Sub.Trait Self (Rhs := Self)}
        `{core.ops.arith.SubAssign.Trait Self (Rhs := Self)}
        `{core.ops.arith.Mul.Trait Self (Rhs := Self)}
        `{core.ops.arith.MulAssign.Trait Self (Rhs := Self)}
        `{core.ops.arith.Div.Trait Self (Rhs := Self)}
        `{core.ops.arith.DivAssign.Trait Self (Rhs := Self)}
        `{num_traits.ops.checked.CheckedMul.Trait Self}
        `{ink_env.arithmetic.Saturating.Trait Self}
        `{core.convert.TryFrom.Trait Self (T := u16)}
        `{core.convert.TryFrom.Trait Self (T := u32)}
        `{core.convert.TryFrom.Trait Self (T := u64)}
        `{core.convert.TryFrom.Trait Self (T := u128)}
        `{core.convert.TryFrom.Trait Self (T := usize)}
        `{core.convert.TryInto.Trait Self (T := u16)}
        `{core.convert.TryInto.Trait Self (T := u32)}
        `{core.convert.TryInto.Trait Self (T := u64)}
        `{core.convert.TryInto.Trait Self (T := u128)}
        `{core.convert.TryInto.Trait Self (T := usize)} :
        Type := {
    }.
    Global Set Primitive Projections.
  End BaseArithmetic.
  
  Module AtLeast32Bit.
    Unset Primitive Projections.
    Class Trait
        (Self : Set)
        `{ink_env.arithmetic.BaseArithmetic.Trait Self}
        `{core.convert.From.Trait Self (T := u16)}
        `{core.convert.From.Trait Self (T := u32)} :
        Type := {
    }.
    Global Set Primitive Projections.
  End AtLeast32Bit.
  
  Module AtLeast32BitUnsigned.
    Unset Primitive Projections.
    Class Trait
        (Self : Set)
        `{ink_env.arithmetic.AtLeast32Bit.Trait Self}
        `{num_traits.sign.Unsigned.Trait Self} :
        Type := {
    }.
    Global Set Primitive Projections.
  End AtLeast32BitUnsigned.
End arithmetic.

Module types.
  Module FromLittleEndian.
    Class Trait (Self : Set) : Type := {
      Bytes : Set;
      _
        :
        Sigma
          `(core.default.Default.Trait Bytes)
          `(core.convert.AsRef.Trait Bytes (T := Slice u8))
          `(core.convert.AsMut.Trait Bytes (T := Slice u8)),
        unit;
      from_le_bytes `{H' : State.Trait} : Bytes -> M (H := H') Self;
    }.
    
    Global Instance Method_Bytes `(Trait)
      : Notation.DoubleColonType Self "Bytes" := {
      Notation.double_colon_type := Bytes;
    }.
    Global Instance Method_from_le_bytes `{H' : State.Trait} `(Trait)
      : Notation.Dot "from_le_bytes" := {
      Notation.dot := from_le_bytes;
    }.
  End FromLittleEndian.
  
  Module AccountIdGuard.
    Unset Primitive Projections.
    Class Trait (Self : Set) : Type := {
    }.
    Global Set Primitive Projections.
  End AccountIdGuard.
  
  Module CodecAsType.
    Unset Primitive Projections.
    Class Trait
        (Self : Set)
        `{scale_decode.DecodeAsType.Trait Self}
        `{scale_encode.EncodeAsType.Trait Self} :
        Type := {
    }.
    Global Set Primitive Projections.
  End CodecAsType.
  
  Module Environment.
    Print parity_scale_codec.codec.Codec.Trait.

    Class Boxed_Codec (Self : Set) : Type := {
      Encode :: parity_scale_codec.codec.Encode.Trait Self;
      Decode :: parity_scale_codec.codec.Decode.Trait Self;
      Main :: parity_scale_codec.codec.Codec.Trait Self;
    }.

    Global Instance Boxed_Codec_from_Codec (Self : Set)
      `{parity_scale_codec.codec.Codec.Trait Self} :
      Boxed_Codec Self := {
      Encode := _;
      Decode := _;
      Main := _;
    }.

    Class Trait (Self : Set) : Type := {
      MAX_EVENT_TOPICS `{H' : State.Trait} : usize;
      AccountId : Set;
      _
        :
        Sigma
          `(parity_scale_codec.codec.Codec.Trait AccountId)
          `(ink_env.types.CodecAsType.Trait AccountId)
          `(core.clone.Clone.Trait AccountId)
          `(core.cmp.PartialEq.Trait AccountId
              (Rhs := core.cmp.PartialEq.Default.Rhs AccountId))
          `(core.cmp.Eq.Trait AccountId)
          `(core.cmp.Ord.Trait AccountId)
          `(core.convert.AsRef.Trait AccountId (T := Slice u8))
          `(core.convert.AsMut.Trait AccountId (T := Slice u8)),
        unit;
      AccountId_is_Codec :: Boxed_Codec AccountId;
      Balance : Set;
      _
        :
        Sigma
          `(parity_scale_codec.codec.Codec.Trait Balance)
          `(ink_env.types.CodecAsType.Trait Balance)
          `(core.marker.Copy.Trait Balance)
          `(core.clone.Clone.Trait Balance)
          `(core.cmp.PartialEq.Trait Balance
              (Rhs := core.cmp.PartialEq.Default.Rhs Balance))
          `(core.cmp.Eq.Trait Balance)
          `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait Balance)
          `(ink_env.types.FromLittleEndian.Trait Balance),
        unit;
      Hash : Set;
      _
        :
        Sigma
          `(parity_scale_codec.codec.Codec.Trait Hash)
          `(ink_env.types.CodecAsType.Trait Hash)
          `(core.marker.Copy.Trait Hash)
          `(core.clone.Clone.Trait Hash)
          `(ink_primitives.types.Clear.Trait Hash)
          `(core.cmp.PartialEq.Trait Hash
              (Rhs := core.cmp.PartialEq.Default.Rhs Hash))
          `(core.cmp.Eq.Trait Hash)
          `(core.cmp.Ord.Trait Hash)
          `(core.convert.AsRef.Trait Hash (T := Slice u8))
          `(core.convert.AsMut.Trait Hash (T := Slice u8)),
        unit;
      Timestamp : Set;
      _
        :
        Sigma
          `(parity_scale_codec.codec.Codec.Trait Timestamp)
          `(ink_env.types.CodecAsType.Trait Timestamp)
          `(core.marker.Copy.Trait Timestamp)
          `(core.clone.Clone.Trait Timestamp)
          `(core.cmp.PartialEq.Trait Timestamp
              (Rhs := core.cmp.PartialEq.Default.Rhs Timestamp))
          `(core.cmp.Eq.Trait Timestamp)
          `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait Timestamp)
          `(ink_env.types.FromLittleEndian.Trait Timestamp),
        unit;
      BlockNumber : Set;
      _
        :
        Sigma
          `(parity_scale_codec.codec.Codec.Trait BlockNumber)
          `(ink_env.types.CodecAsType.Trait BlockNumber)
          `(core.marker.Copy.Trait BlockNumber)
          `(core.clone.Clone.Trait BlockNumber)
          `(core.cmp.PartialEq.Trait BlockNumber
              (Rhs := core.cmp.PartialEq.Default.Rhs BlockNumber))
          `(core.cmp.Eq.Trait BlockNumber)
          `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait BlockNumber)
          `(ink_env.types.FromLittleEndian.Trait BlockNumber),
        unit;
      ChainExtension : Set;
    }.

    Definition fn_requiring_encode (T : Set)
      `{parity_scale_codec.codec.Encode.Trait T} :
      unit :=
      tt.

    Global Instance Method_AccountId `(Trait)
      : Notation.DoubleColonType Self "AccountId" := {
      Notation.double_colon_type := AccountId;
    }.

    Definition calling_fn (Env : Set) `{Trait Env} : unit :=
      fn_requiring_encode (Env::type["AccountId"]).
    
    Set Printing All.
    Print calling_fn.

    Global Instance Method_MAX_EVENT_TOPICS `{H' : State.Trait} `(Trait)
      : Notation.Dot "MAX_EVENT_TOPICS" := {
      Notation.dot := MAX_EVENT_TOPICS;
    }.
    Global Instance Method_Balance `(Trait)
      : Notation.DoubleColonType Self "Balance" := {
      Notation.double_colon_type := Balance;
    }.
    Global Instance Method_Hash `(Trait)
      : Notation.DoubleColonType Self "Hash" := {
      Notation.double_colon_type := Hash;
    }.
    Global Instance Method_Timestamp `(Trait)
      : Notation.DoubleColonType Self "Timestamp" := {
      Notation.double_colon_type := Timestamp;
    }.
    Global Instance Method_BlockNumber `(Trait)
      : Notation.DoubleColonType Self "BlockNumber" := {
      Notation.double_colon_type := BlockNumber;
    }.
    Global Instance Method_ChainExtension `(Trait)
      : Notation.DoubleColonType Self "ChainExtension" := {
      Notation.double_colon_type := ChainExtension;
    }.
  End Environment.
  
  Module NoChainExtension.
    Inductive t : Set :=
    .
  End NoChainExtension.
  Definition NoChainExtension : Set := NoChainExtension.t.
  
  Module DefaultEnvironment.
    Inductive t : Set :=
    .
  End DefaultEnvironment.
  Definition DefaultEnvironment : Set := DefaultEnvironment.t.
  
  Definition Balance : Set := u128.
  
  Definition Timestamp : Set := u64.
  
  Definition Gas : Set := u64.
  
  Definition BlockNumber : Set := u32.
End types.

Module FromLittleEndian.
  Class Trait (Self : Set) : Type := {
    Bytes : Set;
    _
      :
      Sigma
        `(core.default.Default.Trait Bytes)
        `(core.convert.AsRef.Trait Bytes (T := Slice u8))
        `(core.convert.AsMut.Trait Bytes (T := Slice u8)),
      unit;
    from_le_bytes `{H' : State.Trait} : Bytes -> M (H := H') Self;
  }.
  
  Global Instance Method_Bytes `(Trait)
    : Notation.DoubleColonType Self "Bytes" := {
    Notation.double_colon_type := Bytes;
  }.
  Global Instance Method_from_le_bytes `{H' : State.Trait} `(Trait)
    : Notation.Dot "from_le_bytes" := {
    Notation.dot := from_le_bytes;
  }.
End FromLittleEndian.

Module AccountIdGuard.
  Unset Primitive Projections.
  Class Trait (Self : Set) : Type := {
  }.
  Global Set Primitive Projections.
End AccountIdGuard.

Module CodecAsType.
  Unset Primitive Projections.
  Class Trait
      (Self : Set)
      `{scale_decode.DecodeAsType.Trait Self}
      `{scale_encode.EncodeAsType.Trait Self} :
      Type := {
  }.
  Global Set Primitive Projections.
End CodecAsType.

Module Environment.
  Class Trait (Self : Set) : Type := {
    MAX_EVENT_TOPICS `{H' : State.Trait} : usize;
    AccountId : Set;
    _
      :
      Sigma
        `(parity_scale_codec.codec.Codec.Trait AccountId)
        `(ink_env.types.CodecAsType.Trait AccountId)
        `(core.clone.Clone.Trait AccountId)
        `(core.cmp.PartialEq.Trait AccountId
            (Rhs := core.cmp.PartialEq.Default.Rhs AccountId))
        `(core.cmp.Eq.Trait AccountId)
        `(core.cmp.Ord.Trait AccountId)
        `(core.convert.AsRef.Trait AccountId (T := Slice u8))
        `(core.convert.AsMut.Trait AccountId (T := Slice u8)),
      unit;
    Balance : Set;
    _
      :
      Sigma
        `(parity_scale_codec.codec.Codec.Trait Balance)
        `(ink_env.types.CodecAsType.Trait Balance)
        `(core.marker.Copy.Trait Balance)
        `(core.clone.Clone.Trait Balance)
        `(core.cmp.PartialEq.Trait Balance
            (Rhs := core.cmp.PartialEq.Default.Rhs Balance))
        `(core.cmp.Eq.Trait Balance)
        `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait Balance)
        `(ink_env.types.FromLittleEndian.Trait Balance),
      unit;
    Hash : Set;
    _
      :
      Sigma
        `(parity_scale_codec.codec.Codec.Trait Hash)
        `(ink_env.types.CodecAsType.Trait Hash)
        `(core.marker.Copy.Trait Hash)
        `(core.clone.Clone.Trait Hash)
        `(ink_primitives.types.Clear.Trait Hash)
        `(core.cmp.PartialEq.Trait Hash
            (Rhs := core.cmp.PartialEq.Default.Rhs Hash))
        `(core.cmp.Eq.Trait Hash)
        `(core.cmp.Ord.Trait Hash)
        `(core.convert.AsRef.Trait Hash (T := Slice u8))
        `(core.convert.AsMut.Trait Hash (T := Slice u8)),
      unit;
    Timestamp : Set;
    _
      :
      Sigma
        `(parity_scale_codec.codec.Codec.Trait Timestamp)
        `(ink_env.types.CodecAsType.Trait Timestamp)
        `(core.marker.Copy.Trait Timestamp)
        `(core.clone.Clone.Trait Timestamp)
        `(core.cmp.PartialEq.Trait Timestamp
            (Rhs := core.cmp.PartialEq.Default.Rhs Timestamp))
        `(core.cmp.Eq.Trait Timestamp)
        `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait Timestamp)
        `(ink_env.types.FromLittleEndian.Trait Timestamp),
      unit;
    BlockNumber : Set;
    _
      :
      Sigma
        `(parity_scale_codec.codec.Codec.Trait BlockNumber)
        `(ink_env.types.CodecAsType.Trait BlockNumber)
        `(core.marker.Copy.Trait BlockNumber)
        `(core.clone.Clone.Trait BlockNumber)
        `(core.cmp.PartialEq.Trait BlockNumber
            (Rhs := core.cmp.PartialEq.Default.Rhs BlockNumber))
        `(core.cmp.Eq.Trait BlockNumber)
        `(ink_env.arithmetic.AtLeast32BitUnsigned.Trait BlockNumber)
        `(ink_env.types.FromLittleEndian.Trait BlockNumber),
      unit;
    ChainExtension : Set;
  }.
  
  Global Instance Method_MAX_EVENT_TOPICS `{H' : State.Trait} `(Trait)
    : Notation.Dot "MAX_EVENT_TOPICS" := {
    Notation.dot := MAX_EVENT_TOPICS;
  }.
  Global Instance Method_AccountId `(Trait)
    : Notation.DoubleColonType Self "AccountId" := {
    Notation.double_colon_type := AccountId;
  }.
  Global Instance Method_Balance `(Trait)
    : Notation.DoubleColonType Self "Balance" := {
    Notation.double_colon_type := Balance;
  }.
  Global Instance Method_Hash `(Trait)
    : Notation.DoubleColonType Self "Hash" := {
    Notation.double_colon_type := Hash;
  }.
  Global Instance Method_Timestamp `(Trait)
    : Notation.DoubleColonType Self "Timestamp" := {
    Notation.double_colon_type := Timestamp;
  }.
  Global Instance Method_BlockNumber `(Trait)
    : Notation.DoubleColonType Self "BlockNumber" := {
    Notation.double_colon_type := BlockNumber;
  }.
  Global Instance Method_ChainExtension `(Trait)
    : Notation.DoubleColonType Self "ChainExtension" := {
    Notation.double_colon_type := ChainExtension;
  }.
End Environment.

Module NoChainExtension.
  Inductive t : Set :=
  .
End NoChainExtension.
Definition NoChainExtension : Set := NoChainExtension.t.

Module DefaultEnvironment.
  Inductive t : Set :=
  .
End DefaultEnvironment.
Definition DefaultEnvironment : Set := DefaultEnvironment.t.

Definition Balance : Set := u128.

Definition Timestamp : Set := u64.

Definition Gas : Set := u64.

Definition BlockNumber : Set := u32.

Module contract.
  Module ContractEnv.
    Class Trait (Self : Set) : Type := {
      Env : Set;
      _ : Sigma `(ink_env.types.Environment.Trait Env), unit;
    }.
    
    Global Instance Method_Env `(Trait)
      : Notation.DoubleColonType Self "Env" := {
      Notation.double_colon_type := Env;
    }.
  End ContractEnv.

  Print ContractEnv.Trait.

  Module ContractEnvBis.
    Class Trait (Self : Set) : Type := {
      Env : Set;
      Environment_for_Env :: ink_env.types.Environment.Trait Env;
    }.
    
    Global Instance Method_Env `(Trait)
      : Notation.DoubleColonType Self "Env" := {
      Notation.double_colon_type := Env;
    }.
  End ContractEnvBis.

  Module ContractReference.
    Class Trait (Self : Set) : Type := {
      Type_ : Set;
    }.
    
    Global Instance Method_Type_ `(Trait)
      : Notation.DoubleColonType Self "Type_" := {
      Notation.double_colon_type := Type_;
    }.
  End ContractReference.
End contract.

Module call.
  Module common.
    Module ReturnType.
      Section ReturnType.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          _ : core.marker.PhantomData (T);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_0 : Notation.Dot 0 := {
          Notation.dot '(Build_t x0) := x0;
        }.
      End ReturnType.
    End ReturnType.
    Definition ReturnType := @ReturnType.t.
    
    Module Set_.
      Section Set_.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          _ : T;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_0 : Notation.Dot 0 := {
          Notation.dot '(Build_t x0) := x0;
        }.
      End Set_.
    End Set_.
    Definition Set_ := @Set_.t.
    
    Module Unset_.
      Section Unset_.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          _ : core.marker.PhantomData (T);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_0 : Notation.Dot 0 := {
          Notation.dot '(Build_t x0) := x0;
        }.
      End Unset_.
    End Unset_.
    Definition Unset_ := @Unset_.t.
    
    Module Unwrap.
      Class Trait (Self : Set) : Type := {
        Output : Set;
        unwrap_or_else
          `{H' : State.Trait}
          {F : Set}
          `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
          :
          Self -> F -> M (H := H') Output;
      }.
      
      Global Instance Method_Output `(Trait)
        : Notation.DoubleColonType Self "Output" := {
        Notation.double_colon_type := Output;
      }.
      Global Instance Method_unwrap_or_else `{H' : State.Trait} `(Trait)
        : Notation.Dot "unwrap_or_else" := {
        Notation.dot
          {F : Set}
          `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
          :=
          unwrap_or_else (F := F) (H'0 := H'0);
      }.
    End Unwrap.
  End common.
  
  Module selector.
    Module Selector.
      Unset Primitive Projections.
      Record t : Set := {
        bytes : list u8;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_bytes : Notation.Dot "bytes" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End Selector.
    Definition Selector : Set := Selector.t.
  End selector.
  
  Module execution_input.
    Module ExecutionInput.
      Section ExecutionInput.
        Context {Args : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          selector : ink_env.call.selector.Selector;
          args : Args;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_selector : Notation.Dot "selector" := {
          Notation.dot '(Build_t x0 _) := x0;
        }.
        Global Instance Get_AF_selector : Notation.DoubleColon t "selector" := {
          Notation.double_colon '(Build_t x0 _) := x0;
        }.
        Global Instance Get_args : Notation.Dot "args" := {
          Notation.dot '(Build_t _ x1) := x1;
        }.
        Global Instance Get_AF_args : Notation.DoubleColon t "args" := {
          Notation.double_colon '(Build_t _ x1) := x1;
        }.
      End ExecutionInput.
    End ExecutionInput.
    Definition ExecutionInput (Args : Set) : Set :=
      ExecutionInput.t (Args := Args).
    
    Module ArgumentList.
      Section ArgumentList.
        Context {Head Rest : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          head : Head;
          rest : Rest;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_head : Notation.Dot "head" := {
          Notation.dot '(Build_t x0 _) := x0;
        }.
        Global Instance Get_AF_head : Notation.DoubleColon t "head" := {
          Notation.double_colon '(Build_t x0 _) := x0;
        }.
        Global Instance Get_rest : Notation.Dot "rest" := {
          Notation.dot '(Build_t _ x1) := x1;
        }.
        Global Instance Get_AF_rest : Notation.DoubleColon t "rest" := {
          Notation.double_colon '(Build_t _ x1) := x1;
        }.
      End ArgumentList.
    End ArgumentList.
    Definition ArgumentList (Head Rest : Set) : Set :=
      ArgumentList.t (Head := Head) (Rest := Rest).
    
    Module Argument.
      Section Argument.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          arg : T;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_arg : Notation.Dot "arg" := {
          Notation.dot '(Build_t x0) := x0;
        }.
        Global Instance Get_AF_arg : Notation.DoubleColon t "arg" := {
          Notation.double_colon '(Build_t x0) := x0;
        }.
      End Argument.
    End Argument.
    Definition Argument (T : Set) : Set := Argument.t (T := T).
    
    Definition ArgsList (Head Rest : Set) : Set :=
      ink_env.call.execution_input.ArgumentList
        (ink_env.call.execution_input.Argument Head)
        Rest.
    
    Module ArgumentListEnd.
      Inductive t : Set := Build.
    End ArgumentListEnd.
    Definition ArgumentListEnd := @ArgumentListEnd.t.
    
    Definition EmptyArgumentList : Set :=
      ink_env.call.execution_input.ArgumentList
        ink_env.call.execution_input.ArgumentListEnd
        ink_env.call.execution_input.ArgumentListEnd.
  End execution_input.
  
  Module create_builder.
    Module state.
      Module Salt.
        Inductive t : Set :=
        .
      End Salt.
      Definition Salt : Set := Salt.t.
    End state.
    
    Module FromAccountId.
      Class Trait (Self : Set) {T : Set} `{ink_env.types.Environment.Trait T} :
          Type := {
        from_account_id `{H' : State.Trait}
          :
          (ink_env.types.Environment.AccountId (Self := T)) -> M (H := H') Self;
      }.
      
      Global Instance Method_from_account_id `{H' : State.Trait} `(Trait)
        : Notation.Dot "from_account_id" := {
        Notation.dot := from_account_id;
      }.
    End FromAccountId.
    
    Module ConstructorReturnType.
      Class Trait (Self : Set) {C : Set} : Type := {
        IS_RESULT `{H' : State.Trait} : bool;
        Output : Set;
        Error : Set;
        _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit;
        ok `{H' : State.Trait} : C -> M (H := H') Output;
      }.
      
      Global Instance Method_IS_RESULT `{H' : State.Trait} `(Trait)
        : Notation.Dot "IS_RESULT" := {
        Notation.dot := IS_RESULT;
      }.
      Global Instance Method_Output `(Trait)
        : Notation.DoubleColonType Self "Output" := {
        Notation.double_colon_type := Output;
      }.
      Global Instance Method_Error `(Trait)
        : Notation.DoubleColonType Self "Error" := {
        Notation.double_colon_type := Error;
      }.
      Global Instance Method_ok `{H' : State.Trait} `(Trait)
        : Notation.Dot "ok" := {
        Notation.dot := ok;
      }.
      Global Instance Method_err `{H' : State.Trait} `(Trait)
        : Notation.Dot "err" := {
        Notation.dot (_err : Error)
          :=
          (axiom : M (H := H') (core.option.Option Output));
      }.
    End ConstructorReturnType.
    
    Module CreateParams.
      Section CreateParams.
        Context {E ContractRef Args Salt R : Set}.
        Context `{ink_env.types.Environment.Trait E}.
        Unset Primitive Projections.
        Record t : Set := {
          code_hash : E::type["Hash"];
          gas_limit : u64;
          endowment : E::type["Balance"];
          exec_input : ink_env.call.execution_input.ExecutionInput Args;
          salt_bytes : Salt;
          _return_type : ink_env.call.common.ReturnType R;
          _phantom : core.marker.PhantomData (ContractRef);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_code_hash : Notation.Dot "code_hash" := {
          Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
        }.
        Global Instance Get_AF_code_hash
          : Notation.DoubleColon t "code_hash" := {
          Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
        }.
        Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
          Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
        }.
        Global Instance Get_AF_gas_limit
          : Notation.DoubleColon t "gas_limit" := {
          Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
        }.
        Global Instance Get_endowment : Notation.Dot "endowment" := {
          Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
        }.
        Global Instance Get_AF_endowment
          : Notation.DoubleColon t "endowment" := {
          Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
        }.
        Global Instance Get_exec_input : Notation.Dot "exec_input" := {
          Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
        }.
        Global Instance Get_AF_exec_input
          : Notation.DoubleColon t "exec_input" := {
          Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
        }.
        Global Instance Get_salt_bytes : Notation.Dot "salt_bytes" := {
          Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
        }.
        Global Instance Get_AF_salt_bytes
          : Notation.DoubleColon t "salt_bytes" := {
          Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
        }.
        Global Instance Get__return_type : Notation.Dot "_return_type" := {
          Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
        }.
        Global Instance Get_AF__return_type
          : Notation.DoubleColon t "_return_type" := {
          Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
        }.
        Global Instance Get__phantom : Notation.Dot "_phantom" := {
          Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
        }.
        Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
          Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
        }.
      End CreateParams.
    End CreateParams.
    Definition CreateParams
        (E ContractRef Args Salt R : Set)
        `{ink_env.types.Environment.Trait E}
        : Set :=
      CreateParams.t
        (E := E)
        (ContractRef := ContractRef)
        (Args := Args)
        (Salt := Salt)
        (R := R).
    
    Module CreateBuilder.
      Section CreateBuilder.
        Context
          {E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set}.
        Context `{ink_env.types.Environment.Trait E}.
        Unset Primitive Projections.
        Record t : Set := {
          code_hash : CodeHash;
          gas_limit : GasLimit;
          endowment : Endowment;
          exec_input : Args;
          salt : Salt;
          return_type : RetType;
          _phantom : core.marker.PhantomData (E * ContractRef);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_code_hash : Notation.Dot "code_hash" := {
          Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
        }.
        Global Instance Get_AF_code_hash
          : Notation.DoubleColon t "code_hash" := {
          Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
        }.
        Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
          Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
        }.
        Global Instance Get_AF_gas_limit
          : Notation.DoubleColon t "gas_limit" := {
          Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
        }.
        Global Instance Get_endowment : Notation.Dot "endowment" := {
          Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
        }.
        Global Instance Get_AF_endowment
          : Notation.DoubleColon t "endowment" := {
          Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
        }.
        Global Instance Get_exec_input : Notation.Dot "exec_input" := {
          Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
        }.
        Global Instance Get_AF_exec_input
          : Notation.DoubleColon t "exec_input" := {
          Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
        }.
        Global Instance Get_salt : Notation.Dot "salt" := {
          Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
        }.
        Global Instance Get_AF_salt : Notation.DoubleColon t "salt" := {
          Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
        }.
        Global Instance Get_return_type : Notation.Dot "return_type" := {
          Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
        }.
        Global Instance Get_AF_return_type
          : Notation.DoubleColon t "return_type" := {
          Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
        }.
        Global Instance Get__phantom : Notation.Dot "_phantom" := {
          Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
        }.
        Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
          Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
        }.
      End CreateBuilder.
    End CreateBuilder.
    Definition CreateBuilder
        (E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set)
        `{ink_env.types.Environment.Trait E}
        : Set :=
      CreateBuilder.t
        (E := E)
        (ContractRef := ContractRef)
        (CodeHash := CodeHash)
        (GasLimit := GasLimit)
        (Endowment := Endowment)
        (Args := Args)
        (Salt := Salt)
        (RetType := RetType).
  End create_builder.
End call.

Module engine.
  Module off_chain.
    Module call_data.
      Module CallData.
        Unset Primitive Projections.
        Record t : Set := {
          bytes : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_bytes : Notation.Dot "bytes" := {
          Notation.dot '(Build_t x0) := x0;
        }.
        Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
          Notation.double_colon '(Build_t x0) := x0;
        }.
      End CallData.
      Definition CallData : Set := CallData.t.
    End call_data.
    
    Module impls.
      Module TopicsBuilder.
        Unset Primitive Projections.
        Record t : Set := {
          topics
            :
            alloc.vec.Vec
              (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
              alloc.vec.Vec.Default.A;
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_topics : Notation.Dot "topics" := {
          Notation.dot '(Build_t x0) := x0;
        }.
        Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
          Notation.double_colon '(Build_t x0) := x0;
        }.
      End TopicsBuilder.
      Definition TopicsBuilder : Set := TopicsBuilder.t.
    End impls.
    
    Module EnvInstance.
      Unset Primitive Projections.
      Record t : Set := {
        engine : ink_engine.ext.Engine;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_engine : Notation.Dot "engine" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_engine : Notation.DoubleColon t "engine" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End EnvInstance.
    Definition EnvInstance : Set := EnvInstance.t.
    
    Module AccountError.
      Inductive t : Set :=
      | Decoding (_ : parity_scale_codec.error.Error)
      | UnexpectedUserAccount
      | NoAccountForId (_ : alloc.vec.Vec u8 alloc.vec.Vec.Default.A).
    End AccountError.
    Definition AccountError : Set := AccountError.t.
    
    Module OffChainError.
      Inductive t : Set :=
      | Account (_ : ink_env.engine.off_chain.AccountError)
      | UninitializedBlocks
      | UninitializedExecutionContext
      | UnregisteredChainExtension.
    End OffChainError.
    Definition OffChainError : Set := OffChainError.t.
  End off_chain.
End engine.

Module hash.
  Module private.
    Module Sealed.
      Unset Primitive Projections.
      Class Trait (Self : Set) : Type := {
      }.
      Global Set Primitive Projections.
    End Sealed.
  End private.
  
  Module HashOutput.
    Class Trait (Self : Set) `{ink_env.hash.private.Sealed.Trait Self} :
        Type := {
      Type_ : Set;
      _ : Sigma `(core.default.Default.Trait Type_), unit;
    }.
    
    Global Instance Method_Type_ `(Trait)
      : Notation.DoubleColonType Self "Type_" := {
      Notation.double_colon_type := Type_;
    }.
  End HashOutput.
  
  Module CryptoHash.
    Class Trait (Self : Set) `{ink_env.hash.HashOutput.Trait Self} : Type := {
      hash `{H' : State.Trait}
        :
        (ref (Slice u8)) ->
          (mut_ref (ink_env.hash.HashOutput.Type_ (Self := Self))) ->
          M (H := H') unit;
    }.
    
    Global Instance Method_hash `{H' : State.Trait} `(Trait)
      : Notation.Dot "hash" := {
      Notation.dot := hash;
    }.
  End CryptoHash.
  
  Module Sha2x256.
    Inductive t : Set :=
    .
  End Sha2x256.
  Definition Sha2x256 : Set := Sha2x256.t.
  
  Module Keccak256.
    Inductive t : Set :=
    .
  End Keccak256.
  Definition Keccak256 : Set := Keccak256.t.
  
  Module Blake2x256.
    Inductive t : Set :=
    .
  End Blake2x256.
  Definition Blake2x256 : Set := Blake2x256.t.
  
  Module Blake2x128.
    Inductive t : Set :=
    .
  End Blake2x128.
  Definition Blake2x128 : Set := Blake2x128.t.
End hash.

Module topics.
  Module TopicsBuilderBackend.
    Class Trait (Self : Set) {E : Set} `{ink_env.types.Environment.Trait E} :
        Type := {
      Output : Set;
      expect `{H' : State.Trait} : (mut_ref Self) -> usize -> M (H := H') unit;
      push_topic
        `{H' : State.Trait}
        {T : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait T}
        :
        (mut_ref Self) -> (ref T) -> M (H := H') unit;
      output `{H' : State.Trait} : Self -> M (H := H') Output;
    }.
    
    Global Instance Method_Output `(Trait)
      : Notation.DoubleColonType Self "Output" := {
      Notation.double_colon_type := Output;
    }.
    Global Instance Method_expect `{H' : State.Trait} `(Trait)
      : Notation.Dot "expect" := {
      Notation.dot := expect;
    }.
    Global Instance Method_push_topic `{H' : State.Trait} `(Trait)
      : Notation.Dot "push_topic" := {
      Notation.dot {T : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait T}
        :=
        push_topic (T := T) (H'0 := H'0);
    }.
    Global Instance Method_output `{H' : State.Trait} `(Trait)
      : Notation.Dot "output" := {
      Notation.dot := output;
    }.
  End TopicsBuilderBackend.
  
  Module TopicsBuilder.
    Section TopicsBuilder.
      Context {S E B : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        backend : B;
        state : core.marker.PhantomData (S * E);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_backend : Notation.Dot "backend" := {
        Notation.dot '(Build_t x0 _) := x0;
      }.
      Global Instance Get_AF_backend : Notation.DoubleColon t "backend" := {
        Notation.double_colon '(Build_t x0 _) := x0;
      }.
      Global Instance Get_state : Notation.Dot "state" := {
        Notation.dot '(Build_t _ x1) := x1;
      }.
      Global Instance Get_AF_state : Notation.DoubleColon t "state" := {
        Notation.double_colon '(Build_t _ x1) := x1;
      }.
    End TopicsBuilder.
  End TopicsBuilder.
  Definition TopicsBuilder (S E B : Set) : Set :=
    TopicsBuilder.t (S := S) (E := E) (B := B).
  
  Module state.
    Module Uninit.
      Inductive t : Set :=
      .
    End Uninit.
    Definition Uninit : Set := Uninit.t.
    
    Module HasRemainingTopics.
      Inductive t : Set :=
      .
    End HasRemainingTopics.
    Definition HasRemainingTopics : Set := HasRemainingTopics.t.
    
    Module NoRemainingTopics.
      Inductive t : Set :=
      .
    End NoRemainingTopics.
    Definition NoRemainingTopics : Set := NoRemainingTopics.t.
  End state.
  
  Module SomeRemainingTopics.
    Class Trait (Self : Set) : Type := {
      Next : Set;
    }.
    
    Global Instance Method_Next `(Trait)
      : Notation.DoubleColonType Self "Next" := {
      Notation.double_colon_type := Next;
    }.
  End SomeRemainingTopics.
  
  Module EventTopicsAmount.
    Class Trait (Self : Set) : Type := {
      AMOUNT `{H' : State.Trait} : usize;
    }.
    
    Global Instance Method_AMOUNT `{H' : State.Trait} `(Trait)
      : Notation.Dot "AMOUNT" := {
      Notation.dot := AMOUNT;
    }.
  End EventTopicsAmount.
  
  Module Topics.
    Class Trait (Self : Set) : Type := {
      RemainingTopics : Set;
      _ : Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), unit;
      topics
        `{H' : State.Trait}
        {E B : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : ink_env.topics.TopicsBuilderBackend.Trait B (E := E)}
        :
        (ref Self) ->
          (ink_env.topics.TopicsBuilder ink_env.topics.state.Uninit E B) ->
          M (H := H') (ink_env.topics.TopicsBuilderBackend.Output (Self := B));
    }.
    
    Global Instance Method_RemainingTopics `(Trait)
      : Notation.DoubleColonType Self "RemainingTopics" := {
      Notation.double_colon_type := RemainingTopics;
    }.
    Global Instance Method_topics `{H' : State.Trait} `(Trait)
      : Notation.Dot "topics" := {
      Notation.dot
        {E B : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : ink_env.topics.TopicsBuilderBackend.Trait B (E := E)}
        :=
        topics (E := E) (B := B) (H'0 := H'0) (H'1 := H'1);
    }.
  End Topics.
  
  Module PrefixedValue.
    Section PrefixedValue.
      Context {T : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        prefix : ref (Slice u8);
        value : ref T;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_prefix : Notation.Dot "prefix" := {
        Notation.dot '(Build_t x0 _) := x0;
      }.
      Global Instance Get_AF_prefix : Notation.DoubleColon t "prefix" := {
        Notation.double_colon '(Build_t x0 _) := x0;
      }.
      Global Instance Get_value : Notation.Dot "value" := {
        Notation.dot '(Build_t _ x1) := x1;
      }.
      Global Instance Get_AF_value : Notation.DoubleColon t "value" := {
        Notation.double_colon '(Build_t _ x1) := x1;
      }.
    End PrefixedValue.
  End PrefixedValue.
  Definition PrefixedValue (T : Set) : Set := PrefixedValue.t (T := T).
End topics.

Module backend_and_call_builder_and_engine_and_engine_test_api_and_error.
  Module Error.
    Inductive t : Set :=
    | Decode (_ : parity_scale_codec.error.Error)
    | OffChain (_ : ink_env.engine.off_chain.OffChainError)
    | CalleeTrapped
    | CalleeReverted
    | KeyNotFound
    | _BelowSubsistenceThreshold
    | TransferFailed
    | _EndowmentTooLow
    | CodeNotFound
    | NotCallable
    | Unknown
    | LoggingDisabled
    | CallRuntimeFailed
    | EcdsaRecoveryFailed.
  End Error.
  Definition Error : Set := Error.t.
  
  Definition Result (T : Set) : Set :=
    core.result.Result
      T
      ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Error.
  
  Module EmittedEvent.
    Unset Primitive Projections.
    Record t : Set := {
      topics
        :
        alloc.vec.Vec
          (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
          alloc.vec.Vec.Default.A;
      data : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_topics : Notation.Dot "topics" := {
      Notation.dot '(Build_t x0 _) := x0;
    }.
    Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
      Notation.double_colon '(Build_t x0 _) := x0;
    }.
    Global Instance Get_data : Notation.Dot "data" := {
      Notation.dot '(Build_t _ x1) := x1;
    }.
    Global Instance Get_AF_data : Notation.DoubleColon t "data" := {
      Notation.double_colon '(Build_t _ x1) := x1;
    }.
  End EmittedEvent.
  Definition EmittedEvent : Set := EmittedEvent.t.
  
  Parameter set_account_balance :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["AccountId"] -> T::type["Balance"] -> M (H := H') unit.
  
  Parameter get_account_balance :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["AccountId"] ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            T::type["Balance"]).
  
  Parameter register_chain_extension :
      forall
        `{H' : State.Trait}
        {E : Set}
        `{ink_engine.chain_extension.ChainExtension.Trait E},
      E -> M (H := H') unit.
  
  Parameter recorded_debug_messages :
      forall `{H' : State.Trait},
      M (H := H') ink_engine.test_api.RecordedDebugMessages.
  
  Parameter set_clear_storage_disabled :
      forall `{H' : State.Trait},
      bool -> M (H := H') unit.
  
  Parameter advance_block :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      M (H := H') unit.
  
  Parameter set_caller :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      T::type["AccountId"] -> M (H := H') unit.
  
  Parameter set_callee :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      T::type["AccountId"] -> M (H := H') unit.
  
  Parameter set_contract :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      T::type["AccountId"] -> M (H := H') unit.
  
  Parameter is_contract :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      T::type["AccountId"] -> M (H := H') bool.
  
  Parameter callee :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      M (H := H') T::type["AccountId"].
  
  Parameter get_contract_storage_rw :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      (ref T::type["AccountId"]) -> M (H := H') (usize * usize).
  
  Parameter set_value_transferred :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["Balance"] -> M (H := H') unit.
  
  Parameter transfer_in :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["Balance"] -> M (H := H') unit.
  
  Parameter count_used_storage_cells :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      (ref T::type["AccountId"]) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            usize).
  
  Parameter set_block_timestamp :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["Timestamp"] -> M (H := H') unit.
  
  Parameter set_block_number :
      forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
      T::type["BlockNumber"] -> M (H := H') unit.
  
  Module DefaultAccounts.
    Section DefaultAccounts.
      Context {T : Set}.
      Context `{ink_env.types.Environment.Trait T}.
      Unset Primitive Projections.
      Record t : Set := {
        alice : T::type["AccountId"];
        bob : T::type["AccountId"];
        charlie : T::type["AccountId"];
        django : T::type["AccountId"];
        eve : T::type["AccountId"];
        frank : T::type["AccountId"];
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_alice : Notation.Dot "alice" := {
        Notation.dot '(Build_t x0 _ _ _ _ _) := x0;
      }.
      Global Instance Get_AF_alice : Notation.DoubleColon t "alice" := {
        Notation.double_colon '(Build_t x0 _ _ _ _ _) := x0;
      }.
      Global Instance Get_bob : Notation.Dot "bob" := {
        Notation.dot '(Build_t _ x1 _ _ _ _) := x1;
      }.
      Global Instance Get_AF_bob : Notation.DoubleColon t "bob" := {
        Notation.double_colon '(Build_t _ x1 _ _ _ _) := x1;
      }.
      Global Instance Get_charlie : Notation.Dot "charlie" := {
        Notation.dot '(Build_t _ _ x2 _ _ _) := x2;
      }.
      Global Instance Get_AF_charlie : Notation.DoubleColon t "charlie" := {
        Notation.double_colon '(Build_t _ _ x2 _ _ _) := x2;
      }.
      Global Instance Get_django : Notation.Dot "django" := {
        Notation.dot '(Build_t _ _ _ x3 _ _) := x3;
      }.
      Global Instance Get_AF_django : Notation.DoubleColon t "django" := {
        Notation.double_colon '(Build_t _ _ _ x3 _ _) := x3;
      }.
      Global Instance Get_eve : Notation.Dot "eve" := {
        Notation.dot '(Build_t _ _ _ _ x4 _) := x4;
      }.
      Global Instance Get_AF_eve : Notation.DoubleColon t "eve" := {
        Notation.double_colon '(Build_t _ _ _ _ x4 _) := x4;
      }.
      Global Instance Get_frank : Notation.Dot "frank" := {
        Notation.dot '(Build_t _ _ _ _ _ x5) := x5;
      }.
      Global Instance Get_AF_frank : Notation.DoubleColon t "frank" := {
        Notation.double_colon '(Build_t _ _ _ _ _ x5) := x5;
      }.
    End DefaultAccounts.
  End DefaultAccounts.
  Definition DefaultAccounts
      (T : Set)
      `{ink_env.types.Environment.Trait T}
      : Set :=
    DefaultAccounts.t (T := T).
  
  Parameter run_test :
      forall
        `{H' : State.Trait}
        {T F : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.ops.function.FnOnce.Trait F
            (Args := ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DefaultAccounts
              T)}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      F ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter default_accounts :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.convert.From.Trait
              (ink_env.types.Environment.AccountId (Self := T))
            (T := list u8)},
      M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DefaultAccounts
            T).
  
  Parameter recorded_events_ret_ty :
      Sigma (Ty : Set) `(core.iter.traits.iterator.Iterator.Trait Ty),
      unit.
  Parameter recorded_events :
      forall `{H' : State.Trait},
      M (H := H') (projT1 recorded_events_ret_ty).
  
  Parameter assert_contract_termination :
      forall
        `{H' : State.Trait}
        {T F : Set}
        `{ink_env.types.Environment.Trait T}
        `{core.ops.function.FnMut.Trait F (Args := unit)}
        `{core.panic.unwind_safe.UnwindSafe.Trait F}
        `{core.fmt.Debug.Trait
              (ink_env.types.Environment.AccountId (Self := T))}
        `{core.fmt.Debug.Trait (ink_env.types.Environment.Balance (Self := T))},
      F -> T::type["AccountId"] -> T::type["Balance"] -> M (H := H') unit.
  
  Module CallFlags.
    Unset Primitive Projections.
    Record t : Set := {
      forward_input : bool;
      clone_input : bool;
      tail_call : bool;
      allow_reentry : bool;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_forward_input : Notation.Dot "forward_input" := {
      Notation.dot '(Build_t x0 _ _ _) := x0;
    }.
    Global Instance Get_AF_forward_input
      : Notation.DoubleColon t "forward_input" := {
      Notation.double_colon '(Build_t x0 _ _ _) := x0;
    }.
    Global Instance Get_clone_input : Notation.Dot "clone_input" := {
      Notation.dot '(Build_t _ x1 _ _) := x1;
    }.
    Global Instance Get_AF_clone_input
      : Notation.DoubleColon t "clone_input" := {
      Notation.double_colon '(Build_t _ x1 _ _) := x1;
    }.
    Global Instance Get_tail_call : Notation.Dot "tail_call" := {
      Notation.dot '(Build_t _ _ x2 _) := x2;
    }.
    Global Instance Get_AF_tail_call : Notation.DoubleColon t "tail_call" := {
      Notation.double_colon '(Build_t _ _ x2 _) := x2;
    }.
    Global Instance Get_allow_reentry : Notation.Dot "allow_reentry" := {
      Notation.dot '(Build_t _ _ _ x3) := x3;
    }.
    Global Instance Get_AF_allow_reentry
      : Notation.DoubleColon t "allow_reentry" := {
      Notation.double_colon '(Build_t _ _ _ x3) := x3;
    }.
  End CallFlags.
  Definition CallFlags : Set := CallFlags.t.
  
  Module CallParams.
    Section CallParams.
      Context {E CallType Args R : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        call_type : CallType;
        call_flags
          :
          ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallFlags;
        _return_type : ink_env.call.common.ReturnType R;
        exec_input : ink_env.call.execution_input.ExecutionInput Args;
        _phantom : core.marker.PhantomData (E);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_call_type : Notation.Dot "call_type" := {
        Notation.dot '(Build_t x0 _ _ _ _) := x0;
      }.
      Global Instance Get_AF_call_type : Notation.DoubleColon t "call_type" := {
        Notation.double_colon '(Build_t x0 _ _ _ _) := x0;
      }.
      Global Instance Get_call_flags : Notation.Dot "call_flags" := {
        Notation.dot '(Build_t _ x1 _ _ _) := x1;
      }.
      Global Instance Get_AF_call_flags
        : Notation.DoubleColon t "call_flags" := {
        Notation.double_colon '(Build_t _ x1 _ _ _) := x1;
      }.
      Global Instance Get__return_type : Notation.Dot "_return_type" := {
        Notation.dot '(Build_t _ _ x2 _ _) := x2;
      }.
      Global Instance Get_AF__return_type
        : Notation.DoubleColon t "_return_type" := {
        Notation.double_colon '(Build_t _ _ x2 _ _) := x2;
      }.
      Global Instance Get_exec_input : Notation.Dot "exec_input" := {
        Notation.dot '(Build_t _ _ _ x3 _) := x3;
      }.
      Global Instance Get_AF_exec_input
        : Notation.DoubleColon t "exec_input" := {
        Notation.double_colon '(Build_t _ _ _ x3 _) := x3;
      }.
      Global Instance Get__phantom : Notation.Dot "_phantom" := {
        Notation.dot '(Build_t _ _ _ _ x4) := x4;
      }.
      Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
        Notation.double_colon '(Build_t _ _ _ _ x4) := x4;
      }.
    End CallParams.
  End CallParams.
  Definition CallParams
      (E CallType Args R : Set)
      `{ink_env.types.Environment.Trait E}
      : Set :=
    CallParams.t (E := E) (CallType := CallType) (Args := Args) (R := R).
  
  Module Call.
    Section Call.
      Context {E : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        callee : E::type["AccountId"];
        gas_limit : ink_env.types.Gas;
        transferred_value : E::type["Balance"];
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_callee : Notation.Dot "callee" := {
        Notation.dot '(Build_t x0 _ _) := x0;
      }.
      Global Instance Get_AF_callee : Notation.DoubleColon t "callee" := {
        Notation.double_colon '(Build_t x0 _ _) := x0;
      }.
      Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
        Notation.dot '(Build_t _ x1 _) := x1;
      }.
      Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
        Notation.double_colon '(Build_t _ x1 _) := x1;
      }.
      Global Instance Get_transferred_value
        : Notation.Dot "transferred_value" := {
        Notation.dot '(Build_t _ _ x2) := x2;
      }.
      Global Instance Get_AF_transferred_value
        : Notation.DoubleColon t "transferred_value" := {
        Notation.double_colon '(Build_t _ _ x2) := x2;
      }.
    End Call.
  End Call.
  Definition Call (E : Set) `{ink_env.types.Environment.Trait E} : Set :=
    Call.t (E := E).
  
  Module DelegateCall.
    Section DelegateCall.
      Context {E : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        code_hash : E::type["Hash"];
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_code_hash : Notation.Dot "code_hash" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End DelegateCall.
  End DelegateCall.
  Definition DelegateCall
      (E : Set)
      `{ink_env.types.Environment.Trait E}
      : Set :=
    DelegateCall.t (E := E).
  
  Module ReturnFlags.
    Unset Primitive Projections.
    Record t : Set := {
      value : u32;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_value : Notation.Dot "value" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_value : Notation.DoubleColon t "value" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End ReturnFlags.
  Definition ReturnFlags : Set := ReturnFlags.t.
  
  Module EnvBackend.
    Class Trait (Self : Set) : Type := {
      set_contract_storage
        `{H' : State.Trait}
        {K V : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait V}
        :
        (mut_ref Self) ->
          (ref K) ->
          (ref V) ->
          M (H := H') (core.option.Option u32);
      get_contract_storage
        `{H' : State.Trait}
        {K R : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait R}
        :
        (mut_ref Self) ->
          (ref K) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              (core.option.Option R));
      take_contract_storage
        `{H' : State.Trait}
        {K R : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait R}
        :
        (mut_ref Self) ->
          (ref K) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              (core.option.Option R));
      contains_contract_storage
        `{H' : State.Trait}
        {K : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        :
        (mut_ref Self) -> (ref K) -> M (H := H') (core.option.Option u32);
      clear_contract_storage
        `{H' : State.Trait}
        {K : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        :
        (mut_ref Self) -> (ref K) -> M (H := H') (core.option.Option u32);
      decode_input
        `{H' : State.Trait}
        {T : Set}
        `{H'0 : parity_scale_codec.codec.Decode.Trait T}
        :
        (mut_ref Self) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              T);
      return_value
        `{H' : State.Trait}
        {R : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait R}
        :
        (mut_ref Self) ->
          ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.ReturnFlags
          ->
          (ref R) ->
          M (H := H') Empty_set;
      debug_message `{H' : State.Trait}
        :
        (mut_ref Self) -> (ref str) -> M (H := H') unit;
      hash_bytes
        `{H' : State.Trait}
        {H : Set}
        `{H'0 : ink_env.hash.CryptoHash.Trait H}
        :
        (mut_ref Self) ->
          (ref (Slice u8)) ->
          (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
          M (H := H') unit;
      hash_encoded
        `{H' : State.Trait}
        {H T : Set}
        `{H'0 : ink_env.hash.CryptoHash.Trait H}
        `{H'1 : parity_scale_codec.codec.Encode.Trait T}
        :
        (mut_ref Self) ->
          (ref T) ->
          (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
          M (H := H') unit;
      ecdsa_recover `{H' : State.Trait}
        :
        (mut_ref Self) ->
          (ref (list u8)) ->
          (ref (list u8)) ->
          (mut_ref (list u8)) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              unit);
      ecdsa_to_eth_address `{H' : State.Trait}
        :
        (mut_ref Self) ->
          (ref (list u8)) ->
          (mut_ref (list u8)) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              unit);
      call_chain_extension
        `{H' : State.Trait}
        {I T E ErrorCode F D : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait I}
        `{H'1 : parity_scale_codec.codec.Decode.Trait T}
        `{H'2 : core.convert.From.Trait E (T := ErrorCode)}
        `{H'3 : core.ops.function.FnOnce.Trait F (Args := u32)}
        `{H'4 : core.ops.function.FnOnce.Trait D (Args := ref (Slice u8))}
        :
        (mut_ref Self) ->
          u32 ->
          (ref I) ->
          F ->
          D ->
          M (H := H') (core.result.Result T E);
      set_code_hash `{H' : State.Trait}
        :
        (mut_ref Self) ->
          (ref (Slice u8)) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              unit);
    }.
    
    Global Instance Method_set_contract_storage `{H' : State.Trait} `(Trait)
      : Notation.Dot "set_contract_storage" := {
      Notation.dot
        {K V : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait V}
        :=
        set_contract_storage (K := K) (V := V) (H'0 := H'0) (H'1 := H'1);
    }.
    Global Instance Method_get_contract_storage `{H' : State.Trait} `(Trait)
      : Notation.Dot "get_contract_storage" := {
      Notation.dot
        {K R : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait R}
        :=
        get_contract_storage (K := K) (R := R) (H'0 := H'0) (H'1 := H'1);
    }.
    Global Instance Method_take_contract_storage `{H' : State.Trait} `(Trait)
      : Notation.Dot "take_contract_storage" := {
      Notation.dot
        {K R : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        `{H'1 : ink_storage_traits.storage.Storable.Trait R}
        :=
        take_contract_storage (K := K) (R := R) (H'0 := H'0) (H'1 := H'1);
    }.
    Global Instance
        Method_contains_contract_storage
        `{H' : State.Trait}
        `(Trait)
      : Notation.Dot "contains_contract_storage" := {
      Notation.dot {K : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        :=
        contains_contract_storage (K := K) (H'0 := H'0);
    }.
    Global Instance Method_clear_contract_storage `{H' : State.Trait} `(Trait)
      : Notation.Dot "clear_contract_storage" := {
      Notation.dot {K : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait K}
        :=
        clear_contract_storage (K := K) (H'0 := H'0);
    }.
    Global Instance Method_decode_input `{H' : State.Trait} `(Trait)
      : Notation.Dot "decode_input" := {
      Notation.dot {T : Set} `{H'0 : parity_scale_codec.codec.Decode.Trait T}
        :=
        decode_input (T := T) (H'0 := H'0);
    }.
    Global Instance Method_return_value `{H' : State.Trait} `(Trait)
      : Notation.Dot "return_value" := {
      Notation.dot {R : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait R}
        :=
        return_value (R := R) (H'0 := H'0);
    }.
    Global Instance Method_debug_message `{H' : State.Trait} `(Trait)
      : Notation.Dot "debug_message" := {
      Notation.dot := debug_message;
    }.
    Global Instance Method_hash_bytes `{H' : State.Trait} `(Trait)
      : Notation.Dot "hash_bytes" := {
      Notation.dot {H : Set} `{H'0 : ink_env.hash.CryptoHash.Trait H}
        :=
        hash_bytes (H := H) (H'0 := H'0);
    }.
    Global Instance Method_hash_encoded `{H' : State.Trait} `(Trait)
      : Notation.Dot "hash_encoded" := {
      Notation.dot
        {H T : Set}
        `{H'0 : ink_env.hash.CryptoHash.Trait H}
        `{H'1 : parity_scale_codec.codec.Encode.Trait T}
        :=
        hash_encoded (H := H) (T := T) (H'0 := H'0) (H'1 := H'1);
    }.
    Global Instance Method_ecdsa_recover `{H' : State.Trait} `(Trait)
      : Notation.Dot "ecdsa_recover" := {
      Notation.dot := ecdsa_recover;
    }.
    Global Instance Method_ecdsa_to_eth_address `{H' : State.Trait} `(Trait)
      : Notation.Dot "ecdsa_to_eth_address" := {
      Notation.dot := ecdsa_to_eth_address;
    }.
    Global Instance Method_call_chain_extension `{H' : State.Trait} `(Trait)
      : Notation.Dot "call_chain_extension" := {
      Notation.dot
        {I T E ErrorCode F D : Set}
        `{H'0 : parity_scale_codec.codec.Encode.Trait I}
        `{H'1 : parity_scale_codec.codec.Decode.Trait T}
        `{H'2 : core.convert.From.Trait E (T := ErrorCode)}
        `{H'3 : core.ops.function.FnOnce.Trait F (Args := u32)}
        `{H'4 : core.ops.function.FnOnce.Trait D (Args := ref (Slice u8))}
        :=
        call_chain_extension
            (I := I)
            (T := T)
            (E := E)
            (ErrorCode := ErrorCode)
            (F := F)
            (D := D)
          (H'0 := H'0)
          (H'1 := H'1)
          (H'2 := H'2)
          (H'3 := H'3)
          (H'4 := H'4);
    }.
    Global Instance Method_set_code_hash `{H' : State.Trait} `(Trait)
      : Notation.Dot "set_code_hash" := {
      Notation.dot := set_code_hash;
    }.
  End EnvBackend.
  
  Module TypedEnvBackend.
    Class Trait
        (Self : Set)
        `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.EnvBackend.Trait
              Self} :
        Type := {
      caller
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["AccountId"];
      transferred_value
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["Balance"];
      weight_to_fee
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> u64 -> M (H := H') E::type["Balance"];
      gas_left
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') u64;
      block_timestamp
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["Timestamp"];
      account_id
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["AccountId"];
      balance
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["Balance"];
      block_number
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["BlockNumber"];
      minimum_balance
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') E::type["Balance"];
      emit_event
        `{H' : State.Trait}
        {E Event : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : ink_env.topics.Topics.Trait Event}
        `{H'2 : parity_scale_codec.codec.Encode.Trait Event}
        :
        (mut_ref Self) -> Event -> M (H := H') unit;
      invoke_contract
        `{H' : State.Trait}
        {E Args R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'2 : parity_scale_codec.codec.Decode.Trait R}
        :
        (mut_ref Self) ->
          (ref
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
              E
              (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
                E)
              Args
              R))
          ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              (ink_primitives.MessageResult R));
      invoke_contract_delegate
        `{H' : State.Trait}
        {E Args R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'2 : parity_scale_codec.codec.Decode.Trait R}
        :
        (mut_ref Self) ->
          (ref
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
              E
              (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DelegateCall
                E)
              Args
              R))
          ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              (ink_primitives.MessageResult R));
      instantiate_contract
        `{H' : State.Trait}
        {E ContractRef Args Salt R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1
          :
          ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
        `{H'2 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'3 : core.convert.AsRef.Trait Salt (T := Slice u8)}
        `{H'4
          :
          ink_env.call.create_builder.ConstructorReturnType.Trait R
            (C := ContractRef)}
        :
        (mut_ref Self) ->
          (ref
            (ink_env.call.create_builder.CreateParams
              E
              ContractRef
              Args
              Salt
              R))
          ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              (ink_primitives.ConstructorResult
                (ink_env.call.create_builder.ConstructorReturnType.Output
                  (Self := R))));
      terminate_contract
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> E::type["AccountId"] -> M (H := H') Empty_set;
      transfer
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) ->
          E::type["AccountId"] ->
          E::type["Balance"] ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              unit);
      is_contract
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> (ref E::type["AccountId"]) -> M (H := H') bool;
      caller_is_origin
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) -> M (H := H') bool;
      code_hash
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) ->
          (ref E::type["AccountId"]) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              E::type["Hash"]);
      own_code_hash
        `{H' : State.Trait}
        {E : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        :
        (mut_ref Self) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              E::type["Hash"]);
      call_runtime
        `{H' : State.Trait}
        {E Call : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Call}
        :
        (mut_ref Self) ->
          (ref Call) ->
          M (H := H')
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
              unit);
    }.
    
    Global Instance Method_caller `{H' : State.Trait} `(Trait)
      : Notation.Dot "caller" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        caller (E := E) (H'0 := H'0);
    }.
    Global Instance Method_transferred_value `{H' : State.Trait} `(Trait)
      : Notation.Dot "transferred_value" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        transferred_value (E := E) (H'0 := H'0);
    }.
    Global Instance Method_weight_to_fee `{H' : State.Trait} `(Trait)
      : Notation.Dot "weight_to_fee" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        weight_to_fee (E := E) (H'0 := H'0);
    }.
    Global Instance Method_gas_left `{H' : State.Trait} `(Trait)
      : Notation.Dot "gas_left" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        gas_left (E := E) (H'0 := H'0);
    }.
    Global Instance Method_block_timestamp `{H' : State.Trait} `(Trait)
      : Notation.Dot "block_timestamp" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        block_timestamp (E := E) (H'0 := H'0);
    }.
    Global Instance Method_account_id `{H' : State.Trait} `(Trait)
      : Notation.Dot "account_id" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        account_id (E := E) (H'0 := H'0);
    }.
    Global Instance Method_balance `{H' : State.Trait} `(Trait)
      : Notation.Dot "balance" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        balance (E := E) (H'0 := H'0);
    }.
    Global Instance Method_block_number `{H' : State.Trait} `(Trait)
      : Notation.Dot "block_number" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        block_number (E := E) (H'0 := H'0);
    }.
    Global Instance Method_minimum_balance `{H' : State.Trait} `(Trait)
      : Notation.Dot "minimum_balance" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        minimum_balance (E := E) (H'0 := H'0);
    }.
    Global Instance Method_emit_event `{H' : State.Trait} `(Trait)
      : Notation.Dot "emit_event" := {
      Notation.dot
        {E Event : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : ink_env.topics.Topics.Trait Event}
        `{H'2 : parity_scale_codec.codec.Encode.Trait Event}
        :=
        emit_event (E := E) (Event := Event)
          (H'0 := H'0)
          (H'1 := H'1)
          (H'2 := H'2);
    }.
    Global Instance Method_invoke_contract `{H' : State.Trait} `(Trait)
      : Notation.Dot "invoke_contract" := {
      Notation.dot
        {E Args R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'2 : parity_scale_codec.codec.Decode.Trait R}
        :=
        invoke_contract (E := E) (Args := Args) (R := R)
          (H'0 := H'0)
          (H'1 := H'1)
          (H'2 := H'2);
    }.
    Global Instance Method_invoke_contract_delegate `{H' : State.Trait} `(Trait)
      : Notation.Dot "invoke_contract_delegate" := {
      Notation.dot
        {E Args R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'2 : parity_scale_codec.codec.Decode.Trait R}
        :=
        invoke_contract_delegate (E := E) (Args := Args) (R := R)
          (H'0 := H'0)
          (H'1 := H'1)
          (H'2 := H'2);
    }.
    Global Instance Method_instantiate_contract `{H' : State.Trait} `(Trait)
      : Notation.Dot "instantiate_contract" := {
      Notation.dot
        {E ContractRef Args Salt R : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1
          :
          ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
        `{H'2 : parity_scale_codec.codec.Encode.Trait Args}
        `{H'3 : core.convert.AsRef.Trait Salt (T := Slice u8)}
        `{H'4
          :
          ink_env.call.create_builder.ConstructorReturnType.Trait R
            (C := ContractRef)}
        :=
        instantiate_contract
            (E := E)
            (ContractRef := ContractRef)
            (Args := Args)
            (Salt := Salt)
            (R := R)
          (H'0 := H'0)
          (H'1 := H'1)
          (H'2 := H'2)
          (H'3 := H'3)
          (H'4 := H'4);
    }.
    Global Instance Method_terminate_contract `{H' : State.Trait} `(Trait)
      : Notation.Dot "terminate_contract" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        terminate_contract (E := E) (H'0 := H'0);
    }.
    Global Instance Method_transfer `{H' : State.Trait} `(Trait)
      : Notation.Dot "transfer" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        transfer (E := E) (H'0 := H'0);
    }.
    Global Instance Method_is_contract `{H' : State.Trait} `(Trait)
      : Notation.Dot "is_contract" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        is_contract (E := E) (H'0 := H'0);
    }.
    Global Instance Method_caller_is_origin `{H' : State.Trait} `(Trait)
      : Notation.Dot "caller_is_origin" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        caller_is_origin (E := E) (H'0 := H'0);
    }.
    Global Instance Method_code_hash `{H' : State.Trait} `(Trait)
      : Notation.Dot "code_hash" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        code_hash (E := E) (H'0 := H'0);
    }.
    Global Instance Method_own_code_hash `{H' : State.Trait} `(Trait)
      : Notation.Dot "own_code_hash" := {
      Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
        :=
        own_code_hash (E := E) (H'0 := H'0);
    }.
    Global Instance Method_call_runtime `{H' : State.Trait} `(Trait)
      : Notation.Dot "call_runtime" := {
      Notation.dot
        {E Call : Set}
        `{H'0 : ink_env.types.Environment.Trait E}
        `{H'1 : parity_scale_codec.codec.Encode.Trait Call}
        :=
        call_runtime (E := E) (Call := Call) (H'0 := H'0) (H'1 := H'1);
    }.
  End TypedEnvBackend.
  
  Module OnInstance.
    Class Trait
        (Self : Set)
        `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.EnvBackend.Trait
              Self}
        `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.TypedEnvBackend.Trait
              Self} :
        Type := {
      on_instance
        `{H' : State.Trait}
        {F R : Set}
        `{H'0 : core.ops.function.FnOnce.Trait F (Args := mut_ref Self)}
        :
        F -> M (H := H') R;
    }.
    
    Global Instance Method_on_instance `{H' : State.Trait} `(Trait)
      : Notation.Dot "on_instance" := {
      Notation.dot
        {F R : Set}
        `{H'0 : core.ops.function.FnOnce.Trait F (Args := mut_ref Self)}
        :=
        on_instance (F := F) (R := R) (H'0 := H'0);
    }.
  End OnInstance.
  
  Module CallBuilder.
    Section CallBuilder.
      Context {E CallType Args RetType : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        call_type : CallType;
        call_flags
          :
          ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallFlags;
        exec_input : Args;
        return_type : RetType;
        _phantom : core.marker.PhantomData (E);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_call_type : Notation.Dot "call_type" := {
        Notation.dot '(Build_t x0 _ _ _ _) := x0;
      }.
      Global Instance Get_AF_call_type : Notation.DoubleColon t "call_type" := {
        Notation.double_colon '(Build_t x0 _ _ _ _) := x0;
      }.
      Global Instance Get_call_flags : Notation.Dot "call_flags" := {
        Notation.dot '(Build_t _ x1 _ _ _) := x1;
      }.
      Global Instance Get_AF_call_flags
        : Notation.DoubleColon t "call_flags" := {
        Notation.double_colon '(Build_t _ x1 _ _ _) := x1;
      }.
      Global Instance Get_exec_input : Notation.Dot "exec_input" := {
        Notation.dot '(Build_t _ _ x2 _ _) := x2;
      }.
      Global Instance Get_AF_exec_input
        : Notation.DoubleColon t "exec_input" := {
        Notation.double_colon '(Build_t _ _ x2 _ _) := x2;
      }.
      Global Instance Get_return_type : Notation.Dot "return_type" := {
        Notation.dot '(Build_t _ _ _ x3 _) := x3;
      }.
      Global Instance Get_AF_return_type
        : Notation.DoubleColon t "return_type" := {
        Notation.double_colon '(Build_t _ _ _ x3 _) := x3;
      }.
      Global Instance Get__phantom : Notation.Dot "_phantom" := {
        Notation.dot '(Build_t _ _ _ _ x4) := x4;
      }.
      Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
        Notation.double_colon '(Build_t _ _ _ _ x4) := x4;
      }.
    End CallBuilder.
  End CallBuilder.
  Definition CallBuilder
      (E CallType Args RetType : Set)
      `{ink_env.types.Environment.Trait E}
      : Set :=
    CallBuilder.t
      (E := E)
      (CallType := CallType)
      (Args := Args)
      (RetType := RetType).
  
  Parameter build_call :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallBuilder
            E
            (ink_env.call.common.Unset_
              (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
                E))
            (ink_env.call.common.Unset_
              (ink_env.call.execution_input.ExecutionInput
                ink_env.call.execution_input.EmptyArgumentList))
            (ink_env.call.common.Unset_ (ink_env.call.common.ReturnType unit))).
End backend_and_call_builder_and_engine_and_engine_test_api_and_error.

Module api.
  Parameter caller :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["AccountId"].
  
  Parameter transferred_value :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["Balance"].
  
  Parameter weight_to_fee :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      ink_env.types.Gas -> M (H := H') E::type["Balance"].
  
  Parameter gas_left :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') ink_env.types.Gas.
  
  Parameter block_timestamp :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["Timestamp"].
  
  Parameter account_id :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["AccountId"].
  
  Parameter balance :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["Balance"].
  
  Parameter block_number :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["BlockNumber"].
  
  Parameter minimum_balance :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') E::type["Balance"].
  
  Parameter emit_event :
      forall
        `{H' : State.Trait}
        {E Event : Set}
        `{ink_env.types.Environment.Trait E}
        `{ink_env.topics.Topics.Trait Event}
        `{parity_scale_codec.codec.Encode.Trait Event},
      Event -> M (H := H') unit.
  
  Parameter set_contract_storage :
      forall
        `{H' : State.Trait}
        {K V : Set}
        `{parity_scale_codec.codec.Encode.Trait K}
        `{ink_storage_traits.storage.Storable.Trait V},
      (ref K) -> (ref V) -> M (H := H') (core.option.Option u32).
  
  Parameter get_contract_storage :
      forall
        `{H' : State.Trait}
        {K R : Set}
        `{parity_scale_codec.codec.Encode.Trait K}
        `{ink_storage_traits.storage.Storable.Trait R},
      (ref K) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (core.option.Option R)).
  
  Parameter take_contract_storage :
      forall
        `{H' : State.Trait}
        {K R : Set}
        `{parity_scale_codec.codec.Encode.Trait K}
        `{ink_storage_traits.storage.Storable.Trait R},
      (ref K) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (core.option.Option R)).
  
  Parameter contains_contract_storage :
      forall
        `{H' : State.Trait}
        {K : Set}
        `{parity_scale_codec.codec.Encode.Trait K},
      (ref K) -> M (H := H') (core.option.Option u32).
  
  Parameter clear_contract_storage :
      forall
        `{H' : State.Trait}
        {K : Set}
        `{parity_scale_codec.codec.Encode.Trait K},
      (ref K) -> M (H := H') (core.option.Option u32).
  
  Parameter invoke_contract :
      forall
        `{H' : State.Trait}
        {E Args R : Set}
        `{ink_env.types.Environment.Trait E}
        `{parity_scale_codec.codec.Encode.Trait Args}
        `{parity_scale_codec.codec.Decode.Trait R},
      (ref
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
            E
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
              E)
            Args
            R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.MessageResult R)).
  
  Parameter invoke_contract_delegate :
      forall
        `{H' : State.Trait}
        {E Args R : Set}
        `{ink_env.types.Environment.Trait E}
        `{parity_scale_codec.codec.Encode.Trait Args}
        `{parity_scale_codec.codec.Decode.Trait R},
      (ref
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
            E
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DelegateCall
              E)
            Args
            R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.MessageResult R)).
  
  Parameter instantiate_contract :
      forall
        `{H' : State.Trait}
        {E ContractRef Args Salt R : Set}
        `{ink_env.types.Environment.Trait E}
        `{ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
        `{parity_scale_codec.codec.Encode.Trait Args}
        `{core.convert.AsRef.Trait Salt (T := Slice u8)}
        `{ink_env.call.create_builder.ConstructorReturnType.Trait R
            (C := ContractRef)},
      (ref (ink_env.call.create_builder.CreateParams E ContractRef Args Salt R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.ConstructorResult
              (ink_env.call.create_builder.ConstructorReturnType.Output
                (Self := R)))).
  
  Parameter terminate_contract :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      E::type["AccountId"] -> M (H := H') Empty_set.
  
  Parameter transfer :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      E::type["AccountId"] ->
        E::type["Balance"] ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter decode_input :
      forall
        `{H' : State.Trait}
        {T : Set}
        `{parity_scale_codec.codec.Decode.Trait T},
      M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            T).
  
  Parameter return_value :
      forall
        `{H' : State.Trait}
        {R : Set}
        `{parity_scale_codec.codec.Encode.Trait R},
      ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.ReturnFlags
        ->
        (ref R) ->
        M (H := H') Empty_set.
  
  Parameter debug_message :
      forall `{H' : State.Trait},
      (ref str) -> M (H := H') unit.
  
  Parameter hash_bytes :
      forall `{H' : State.Trait} {H : Set} `{ink_env.hash.CryptoHash.Trait H},
      (ref (Slice u8)) ->
        (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
        M (H := H') unit.
  
  Parameter hash_encoded :
      forall
        `{H' : State.Trait}
        {H T : Set}
        `{ink_env.hash.CryptoHash.Trait H}
        `{parity_scale_codec.codec.Encode.Trait T},
      (ref T) ->
        (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
        M (H := H') unit.
  
  Parameter ecdsa_recover :
      forall `{H' : State.Trait},
      (ref (list u8)) ->
        (ref (list u8)) ->
        (mut_ref (list u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter ecdsa_to_eth_address :
      forall `{H' : State.Trait},
      (ref (list u8)) ->
        (mut_ref (list u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter is_contract :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      (ref E::type["AccountId"]) -> M (H := H') bool.
  
  Parameter code_hash :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      (ref E::type["AccountId"]) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            E::type["Hash"]).
  
  Parameter own_code_hash :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            E::type["Hash"]).
  
  Parameter caller_is_origin :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      M (H := H') bool.
  
  Parameter set_code_hash :
      forall `{H' : State.Trait},
      (ref (list u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter set_code_hash2 :
      forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
      (ref E::type["Hash"]) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
  
  Parameter call_runtime :
      forall
        `{H' : State.Trait}
        {E Call : Set}
        `{ink_env.types.Environment.Trait E}
        `{parity_scale_codec.codec.Encode.Trait Call},
      (ref Call) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit).
End api.

Parameter caller :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["AccountId"].

Parameter transferred_value :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["Balance"].

Parameter weight_to_fee :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    ink_env.types.Gas -> M (H := H') E::type["Balance"].

Parameter gas_left :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') ink_env.types.Gas.

Parameter block_timestamp :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["Timestamp"].

Parameter account_id :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["AccountId"].

Parameter balance :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["Balance"].

Parameter block_number :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["BlockNumber"].

Parameter minimum_balance :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') E::type["Balance"].

Parameter emit_event :
    forall
      `{H' : State.Trait}
      {E Event : Set}
      `{ink_env.types.Environment.Trait E}
      `{ink_env.topics.Topics.Trait Event}
      `{parity_scale_codec.codec.Encode.Trait Event},
    Event -> M (H := H') unit.

Parameter set_contract_storage :
    forall
      `{H' : State.Trait}
      {K V : Set}
      `{parity_scale_codec.codec.Encode.Trait K}
      `{ink_storage_traits.storage.Storable.Trait V},
    (ref K) -> (ref V) -> M (H := H') (core.option.Option u32).

Parameter get_contract_storage :
    forall
      `{H' : State.Trait}
      {K R : Set}
      `{parity_scale_codec.codec.Encode.Trait K}
      `{ink_storage_traits.storage.Storable.Trait R},
    (ref K) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          (core.option.Option R)).

Parameter take_contract_storage :
    forall
      `{H' : State.Trait}
      {K R : Set}
      `{parity_scale_codec.codec.Encode.Trait K}
      `{ink_storage_traits.storage.Storable.Trait R},
    (ref K) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          (core.option.Option R)).

Parameter contains_contract_storage :
    forall
      `{H' : State.Trait}
      {K : Set}
      `{parity_scale_codec.codec.Encode.Trait K},
    (ref K) -> M (H := H') (core.option.Option u32).

Parameter clear_contract_storage :
    forall
      `{H' : State.Trait}
      {K : Set}
      `{parity_scale_codec.codec.Encode.Trait K},
    (ref K) -> M (H := H') (core.option.Option u32).

Parameter invoke_contract :
    forall
      `{H' : State.Trait}
      {E Args R : Set}
      `{ink_env.types.Environment.Trait E}
      `{parity_scale_codec.codec.Encode.Trait Args}
      `{parity_scale_codec.codec.Decode.Trait R},
    (ref
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
          E
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
            E)
          Args
          R))
      ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          (ink_primitives.MessageResult R)).

Parameter invoke_contract_delegate :
    forall
      `{H' : State.Trait}
      {E Args R : Set}
      `{ink_env.types.Environment.Trait E}
      `{parity_scale_codec.codec.Encode.Trait Args}
      `{parity_scale_codec.codec.Decode.Trait R},
    (ref
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
          E
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DelegateCall
            E)
          Args
          R))
      ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          (ink_primitives.MessageResult R)).

Parameter instantiate_contract :
    forall
      `{H' : State.Trait}
      {E ContractRef Args Salt R : Set}
      `{ink_env.types.Environment.Trait E}
      `{ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
      `{parity_scale_codec.codec.Encode.Trait Args}
      `{core.convert.AsRef.Trait Salt (T := Slice u8)}
      `{ink_env.call.create_builder.ConstructorReturnType.Trait R
          (C := ContractRef)},
    (ref (ink_env.call.create_builder.CreateParams E ContractRef Args Salt R))
      ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          (ink_primitives.ConstructorResult
            (ink_env.call.create_builder.ConstructorReturnType.Output
              (Self := R)))).

Parameter terminate_contract :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    E::type["AccountId"] -> M (H := H') Empty_set.

Parameter transfer :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    E::type["AccountId"] ->
      E::type["Balance"] ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter decode_input :
    forall
      `{H' : State.Trait}
      {T : Set}
      `{parity_scale_codec.codec.Decode.Trait T},
    M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          T).

Parameter return_value :
    forall
      `{H' : State.Trait}
      {R : Set}
      `{parity_scale_codec.codec.Encode.Trait R},
    ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.ReturnFlags
      ->
      (ref R) ->
      M (H := H') Empty_set.

Parameter debug_message :
    forall `{H' : State.Trait},
    (ref str) -> M (H := H') unit.

Parameter hash_bytes :
    forall `{H' : State.Trait} {H : Set} `{ink_env.hash.CryptoHash.Trait H},
    (ref (Slice u8)) ->
      (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
      M (H := H') unit.

Parameter hash_encoded :
    forall
      `{H' : State.Trait}
      {H T : Set}
      `{ink_env.hash.CryptoHash.Trait H}
      `{parity_scale_codec.codec.Encode.Trait T},
    (ref T) ->
      (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
      M (H := H') unit.

Parameter ecdsa_recover :
    forall `{H' : State.Trait},
    (ref (list u8)) ->
      (ref (list u8)) ->
      (mut_ref (list u8)) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter ecdsa_to_eth_address :
    forall `{H' : State.Trait},
    (ref (list u8)) ->
      (mut_ref (list u8)) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter is_contract :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    (ref E::type["AccountId"]) -> M (H := H') bool.

Parameter code_hash :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    (ref E::type["AccountId"]) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          E::type["Hash"]).

Parameter own_code_hash :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          E::type["Hash"]).

Parameter caller_is_origin :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H') bool.

Parameter set_code_hash :
    forall `{H' : State.Trait},
    (ref (list u8)) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter set_code_hash2 :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    (ref E::type["Hash"]) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter call_runtime :
    forall
      `{H' : State.Trait}
      {E Call : Set}
      `{ink_env.types.Environment.Trait E}
      `{parity_scale_codec.codec.Encode.Trait Call},
    (ref Call) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Module BaseArithmetic.
  Unset Primitive Projections.
  Class Trait
      (Self : Set)
      `{core.marker.Sized.Trait Self}
      `{core.convert.From.Trait Self (T := u8)}
      `{num_traits.bounds.Bounded.Trait Self}
      `{core.cmp.Ord.Trait Self}
      `{core.cmp.PartialOrd.Trait Self (Rhs := Self)}
      `{num_traits.identities.Zero.Trait Self}
      `{num_traits.identities.One.Trait Self}
      `{num_traits.bounds.Bounded.Trait Self}
      `{core.ops.arith.Add.Trait Self (Rhs := Self)}
      `{core.ops.arith.AddAssign.Trait Self (Rhs := Self)}
      `{core.ops.arith.Sub.Trait Self (Rhs := Self)}
      `{core.ops.arith.SubAssign.Trait Self (Rhs := Self)}
      `{core.ops.arith.Mul.Trait Self (Rhs := Self)}
      `{core.ops.arith.MulAssign.Trait Self (Rhs := Self)}
      `{core.ops.arith.Div.Trait Self (Rhs := Self)}
      `{core.ops.arith.DivAssign.Trait Self (Rhs := Self)}
      `{num_traits.ops.checked.CheckedMul.Trait Self}
      `{ink_env.arithmetic.Saturating.Trait Self}
      `{core.convert.TryFrom.Trait Self (T := u16)}
      `{core.convert.TryFrom.Trait Self (T := u32)}
      `{core.convert.TryFrom.Trait Self (T := u64)}
      `{core.convert.TryFrom.Trait Self (T := u128)}
      `{core.convert.TryFrom.Trait Self (T := usize)}
      `{core.convert.TryInto.Trait Self (T := u16)}
      `{core.convert.TryInto.Trait Self (T := u32)}
      `{core.convert.TryInto.Trait Self (T := u64)}
      `{core.convert.TryInto.Trait Self (T := u128)}
      `{core.convert.TryInto.Trait Self (T := usize)} :
      Type := {
  }.
  Global Set Primitive Projections.
End BaseArithmetic.

Module AtLeast32Bit.
  Unset Primitive Projections.
  Class Trait
      (Self : Set)
      `{ink_env.arithmetic.BaseArithmetic.Trait Self}
      `{core.convert.From.Trait Self (T := u16)}
      `{core.convert.From.Trait Self (T := u32)} :
      Type := {
  }.
  Global Set Primitive Projections.
End AtLeast32Bit.

Module AtLeast32BitUnsigned.
  Unset Primitive Projections.
  Class Trait
      (Self : Set)
      `{ink_env.arithmetic.AtLeast32Bit.Trait Self}
      `{num_traits.sign.Unsigned.Trait Self} :
      Type := {
  }.
  Global Set Primitive Projections.
End AtLeast32BitUnsigned.

Module Saturating.
  Class Trait (Self : Set) : Type := {
    saturating_add `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
    saturating_sub `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
    saturating_mul `{H' : State.Trait} : Self -> Self -> M (H := H') Self;
    saturating_pow `{H' : State.Trait} : Self -> usize -> M (H := H') Self;
  }.
  
  Global Instance Method_saturating_add `{H' : State.Trait} `(Trait)
    : Notation.Dot "saturating_add" := {
    Notation.dot := saturating_add;
  }.
  Global Instance Method_saturating_sub `{H' : State.Trait} `(Trait)
    : Notation.Dot "saturating_sub" := {
    Notation.dot := saturating_sub;
  }.
  Global Instance Method_saturating_mul `{H' : State.Trait} `(Trait)
    : Notation.Dot "saturating_mul" := {
    Notation.dot := saturating_mul;
  }.
  Global Instance Method_saturating_pow `{H' : State.Trait} `(Trait)
    : Notation.Dot "saturating_pow" := {
    Notation.dot := saturating_pow;
  }.
End Saturating.

Module Error.
  Inductive t : Set :=
  | Decode (_ : parity_scale_codec.error.Error)
  | OffChain (_ : ink_env.engine.off_chain.OffChainError)
  | CalleeTrapped
  | CalleeReverted
  | KeyNotFound
  | _BelowSubsistenceThreshold
  | TransferFailed
  | _EndowmentTooLow
  | CodeNotFound
  | NotCallable
  | Unknown
  | LoggingDisabled
  | CallRuntimeFailed
  | EcdsaRecoveryFailed.
End Error.
Definition Error : Set := Error.t.

Definition Result (T : Set) : Set :=
  core.result.Result
    T
    ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Error.

Module EmittedEvent.
  Unset Primitive Projections.
  Record t : Set := {
    topics
      :
      alloc.vec.Vec
        (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
        alloc.vec.Vec.Default.A;
    data : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_topics : Notation.Dot "topics" := {
    Notation.dot '(Build_t x0 _) := x0;
  }.
  Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
    Notation.double_colon '(Build_t x0 _) := x0;
  }.
  Global Instance Get_data : Notation.Dot "data" := {
    Notation.dot '(Build_t _ x1) := x1;
  }.
  Global Instance Get_AF_data : Notation.DoubleColon t "data" := {
    Notation.double_colon '(Build_t _ x1) := x1;
  }.
End EmittedEvent.
Definition EmittedEvent : Set := EmittedEvent.t.

Parameter set_account_balance :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["AccountId"] -> T::type["Balance"] -> M (H := H') unit.

Parameter get_account_balance :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["AccountId"] ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          T::type["Balance"]).

Parameter register_chain_extension :
    forall
      `{H' : State.Trait}
      {E : Set}
      `{ink_engine.chain_extension.ChainExtension.Trait E},
    E -> M (H := H') unit.

Parameter recorded_debug_messages :
    forall `{H' : State.Trait},
    M (H := H') ink_engine.test_api.RecordedDebugMessages.

Parameter set_clear_storage_disabled :
    forall `{H' : State.Trait},
    bool -> M (H := H') unit.

Parameter advance_block :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    M (H := H') unit.

Parameter set_caller :
    forall
      `{H' : State.Trait}
      {T : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.convert.From.Trait
            (ink_env.types.Environment.AccountId (Self := T))
          (T := list u8)},
    T::type["AccountId"] -> M (H := H') unit.

Parameter set_callee :
    forall
      `{H' : State.Trait}
      {T : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.convert.From.Trait
            (ink_env.types.Environment.AccountId (Self := T))
          (T := list u8)},
    T::type["AccountId"] -> M (H := H') unit.

Parameter set_contract :
    forall
      `{H' : State.Trait}
      {T : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.convert.From.Trait
            (ink_env.types.Environment.AccountId (Self := T))
          (T := list u8)},
    T::type["AccountId"] -> M (H := H') unit.



Parameter callee :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    M (H := H') T::type["AccountId"].

Parameter get_contract_storage_rw :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    (ref T::type["AccountId"]) -> M (H := H') (usize * usize).

Parameter set_value_transferred :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["Balance"] -> M (H := H') unit.

Parameter transfer_in :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["Balance"] -> M (H := H') unit.

Parameter count_used_storage_cells :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    (ref T::type["AccountId"]) ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          usize).

Parameter set_block_timestamp :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["Timestamp"] -> M (H := H') unit.

Parameter set_block_number :
    forall `{H' : State.Trait} {T : Set} `{ink_env.types.Environment.Trait T},
    T::type["BlockNumber"] -> M (H := H') unit.

Parameter run_test :
    forall
      `{H' : State.Trait}
      {T F : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.ops.function.FnOnce.Trait F
          (Args := ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DefaultAccounts
            T)}
      `{core.convert.From.Trait
            (ink_env.types.Environment.AccountId (Self := T))
          (T := list u8)},
    F ->
      M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
          unit).

Parameter default_accounts :
    forall
      `{H' : State.Trait}
      {T : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.convert.From.Trait
            (ink_env.types.Environment.AccountId (Self := T))
          (T := list u8)},
    M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DefaultAccounts
          T).

Module DefaultAccounts.
  Section DefaultAccounts.
    Context {T : Set}.
    Context `{ink_env.types.Environment.Trait T}.
    Unset Primitive Projections.
    Record t : Set := {
      alice : T::type["AccountId"];
      bob : T::type["AccountId"];
      charlie : T::type["AccountId"];
      django : T::type["AccountId"];
      eve : T::type["AccountId"];
      frank : T::type["AccountId"];
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_alice : Notation.Dot "alice" := {
      Notation.dot '(Build_t x0 _ _ _ _ _) := x0;
    }.
    Global Instance Get_AF_alice : Notation.DoubleColon t "alice" := {
      Notation.double_colon '(Build_t x0 _ _ _ _ _) := x0;
    }.
    Global Instance Get_bob : Notation.Dot "bob" := {
      Notation.dot '(Build_t _ x1 _ _ _ _) := x1;
    }.
    Global Instance Get_AF_bob : Notation.DoubleColon t "bob" := {
      Notation.double_colon '(Build_t _ x1 _ _ _ _) := x1;
    }.
    Global Instance Get_charlie : Notation.Dot "charlie" := {
      Notation.dot '(Build_t _ _ x2 _ _ _) := x2;
    }.
    Global Instance Get_AF_charlie : Notation.DoubleColon t "charlie" := {
      Notation.double_colon '(Build_t _ _ x2 _ _ _) := x2;
    }.
    Global Instance Get_django : Notation.Dot "django" := {
      Notation.dot '(Build_t _ _ _ x3 _ _) := x3;
    }.
    Global Instance Get_AF_django : Notation.DoubleColon t "django" := {
      Notation.double_colon '(Build_t _ _ _ x3 _ _) := x3;
    }.
    Global Instance Get_eve : Notation.Dot "eve" := {
      Notation.dot '(Build_t _ _ _ _ x4 _) := x4;
    }.
    Global Instance Get_AF_eve : Notation.DoubleColon t "eve" := {
      Notation.double_colon '(Build_t _ _ _ _ x4 _) := x4;
    }.
    Global Instance Get_frank : Notation.Dot "frank" := {
      Notation.dot '(Build_t _ _ _ _ _ x5) := x5;
    }.
    Global Instance Get_AF_frank : Notation.DoubleColon t "frank" := {
      Notation.double_colon '(Build_t _ _ _ _ _ x5) := x5;
    }.
  End DefaultAccounts.
End DefaultAccounts.
Definition DefaultAccounts
    (T : Set)
    `{ink_env.types.Environment.Trait T}
    : Set :=
  DefaultAccounts.t (T := T).

Parameter recorded_events_ret_ty :
    Sigma (Ty : Set) `(core.iter.traits.iterator.Iterator.Trait Ty),
    unit.
Parameter recorded_events :
    forall `{H' : State.Trait},
    M (H := H') (projT1 recorded_events_ret_ty).

Parameter assert_contract_termination :
    forall
      `{H' : State.Trait}
      {T F : Set}
      `{ink_env.types.Environment.Trait T}
      `{core.ops.function.FnMut.Trait F (Args := unit)}
      `{core.panic.unwind_safe.UnwindSafe.Trait F}
      `{core.fmt.Debug.Trait (ink_env.types.Environment.AccountId (Self := T))}
      `{core.fmt.Debug.Trait (ink_env.types.Environment.Balance (Self := T))},
    F -> T::type["AccountId"] -> T::type["Balance"] -> M (H := H') unit.

Module OnInstance.
  Class Trait
      (Self : Set)
      `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.EnvBackend.Trait
            Self}
      `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.TypedEnvBackend.Trait
            Self} :
      Type := {
    on_instance
      `{H' : State.Trait}
      {F R : Set}
      `{H'0 : core.ops.function.FnOnce.Trait F (Args := mut_ref Self)}
      :
      F -> M (H := H') R;
  }.
  
  Global Instance Method_on_instance `{H' : State.Trait} `(Trait)
    : Notation.Dot "on_instance" := {
    Notation.dot
      {F R : Set}
      `{H'0 : core.ops.function.FnOnce.Trait F (Args := mut_ref Self)}
      :=
      on_instance (F := F) (R := R) (H'0 := H'0);
  }.
End OnInstance.

Module CallParams.
  Section CallParams.
    Context {E CallType Args R : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      call_type : CallType;
      call_flags
        :
        ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallFlags;
      _return_type : ink_env.call.common.ReturnType R;
      exec_input : ink_env.call.execution_input.ExecutionInput Args;
      _phantom : core.marker.PhantomData (E);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_call_type : Notation.Dot "call_type" := {
      Notation.dot '(Build_t x0 _ _ _ _) := x0;
    }.
    Global Instance Get_AF_call_type : Notation.DoubleColon t "call_type" := {
      Notation.double_colon '(Build_t x0 _ _ _ _) := x0;
    }.
    Global Instance Get_call_flags : Notation.Dot "call_flags" := {
      Notation.dot '(Build_t _ x1 _ _ _) := x1;
    }.
    Global Instance Get_AF_call_flags : Notation.DoubleColon t "call_flags" := {
      Notation.double_colon '(Build_t _ x1 _ _ _) := x1;
    }.
    Global Instance Get__return_type : Notation.Dot "_return_type" := {
      Notation.dot '(Build_t _ _ x2 _ _) := x2;
    }.
    Global Instance Get_AF__return_type
      : Notation.DoubleColon t "_return_type" := {
      Notation.double_colon '(Build_t _ _ x2 _ _) := x2;
    }.
    Global Instance Get_exec_input : Notation.Dot "exec_input" := {
      Notation.dot '(Build_t _ _ _ x3 _) := x3;
    }.
    Global Instance Get_AF_exec_input : Notation.DoubleColon t "exec_input" := {
      Notation.double_colon '(Build_t _ _ _ x3 _) := x3;
    }.
    Global Instance Get__phantom : Notation.Dot "_phantom" := {
      Notation.dot '(Build_t _ _ _ _ x4) := x4;
    }.
    Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
      Notation.double_colon '(Build_t _ _ _ _ x4) := x4;
    }.
  End CallParams.
End CallParams.
Definition CallParams
    (E CallType Args R : Set)
    `{ink_env.types.Environment.Trait E}
    : Set :=
  CallParams.t (E := E) (CallType := CallType) (Args := Args) (R := R).

Parameter build_call :
    forall `{H' : State.Trait} {E : Set} `{ink_env.types.Environment.Trait E},
    M (H := H')
        (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallBuilder
          E
          (ink_env.call.common.Unset_
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
              E))
          (ink_env.call.common.Unset_
            (ink_env.call.execution_input.ExecutionInput
              ink_env.call.execution_input.EmptyArgumentList))
          (ink_env.call.common.Unset_ (ink_env.call.common.ReturnType unit))).

Module Call.
  Section Call.
    Context {E : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      callee : E::type["AccountId"];
      gas_limit : ink_env.types.Gas;
      transferred_value : E::type["Balance"];
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_callee : Notation.Dot "callee" := {
      Notation.dot '(Build_t x0 _ _) := x0;
    }.
    Global Instance Get_AF_callee : Notation.DoubleColon t "callee" := {
      Notation.double_colon '(Build_t x0 _ _) := x0;
    }.
    Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
      Notation.dot '(Build_t _ x1 _) := x1;
    }.
    Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
      Notation.double_colon '(Build_t _ x1 _) := x1;
    }.
    Global Instance Get_transferred_value
      : Notation.Dot "transferred_value" := {
      Notation.dot '(Build_t _ _ x2) := x2;
    }.
    Global Instance Get_AF_transferred_value
      : Notation.DoubleColon t "transferred_value" := {
      Notation.double_colon '(Build_t _ _ x2) := x2;
    }.
  End Call.
End Call.
Definition Call (E : Set) `{ink_env.types.Environment.Trait E} : Set :=
  Call.t (E := E).

Module DelegateCall.
  Section DelegateCall.
    Context {E : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      code_hash : E::type["Hash"];
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_code_hash : Notation.Dot "code_hash" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End DelegateCall.
End DelegateCall.
Definition DelegateCall (E : Set) `{ink_env.types.Environment.Trait E} : Set :=
  DelegateCall.t (E := E).

Module CallBuilder.
  Section CallBuilder.
    Context {E CallType Args RetType : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      call_type : CallType;
      call_flags
        :
        ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallFlags;
      exec_input : Args;
      return_type : RetType;
      _phantom : core.marker.PhantomData (E);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_call_type : Notation.Dot "call_type" := {
      Notation.dot '(Build_t x0 _ _ _ _) := x0;
    }.
    Global Instance Get_AF_call_type : Notation.DoubleColon t "call_type" := {
      Notation.double_colon '(Build_t x0 _ _ _ _) := x0;
    }.
    Global Instance Get_call_flags : Notation.Dot "call_flags" := {
      Notation.dot '(Build_t _ x1 _ _ _) := x1;
    }.
    Global Instance Get_AF_call_flags : Notation.DoubleColon t "call_flags" := {
      Notation.double_colon '(Build_t _ x1 _ _ _) := x1;
    }.
    Global Instance Get_exec_input : Notation.Dot "exec_input" := {
      Notation.dot '(Build_t _ _ x2 _ _) := x2;
    }.
    Global Instance Get_AF_exec_input : Notation.DoubleColon t "exec_input" := {
      Notation.double_colon '(Build_t _ _ x2 _ _) := x2;
    }.
    Global Instance Get_return_type : Notation.Dot "return_type" := {
      Notation.dot '(Build_t _ _ _ x3 _) := x3;
    }.
    Global Instance Get_AF_return_type
      : Notation.DoubleColon t "return_type" := {
      Notation.double_colon '(Build_t _ _ _ x3 _) := x3;
    }.
    Global Instance Get__phantom : Notation.Dot "_phantom" := {
      Notation.dot '(Build_t _ _ _ _ x4) := x4;
    }.
    Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
      Notation.double_colon '(Build_t _ _ _ _ x4) := x4;
    }.
  End CallBuilder.
End CallBuilder.
Definition CallBuilder
    (E CallType Args RetType : Set)
    `{ink_env.types.Environment.Trait E}
    : Set :=
  CallBuilder.t
    (E := E)
    (CallType := CallType)
    (Args := Args)
    (RetType := RetType).

Module ReturnFlags.
  Unset Primitive Projections.
  Record t : Set := {
    value : u32;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_value : Notation.Dot "value" := {
    Notation.dot '(Build_t x0) := x0;
  }.
  Global Instance Get_AF_value : Notation.DoubleColon t "value" := {
    Notation.double_colon '(Build_t x0) := x0;
  }.
End ReturnFlags.
Definition ReturnFlags : Set := ReturnFlags.t.

Module CallFlags.
  Unset Primitive Projections.
  Record t : Set := {
    forward_input : bool;
    clone_input : bool;
    tail_call : bool;
    allow_reentry : bool;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_forward_input : Notation.Dot "forward_input" := {
    Notation.dot '(Build_t x0 _ _ _) := x0;
  }.
  Global Instance Get_AF_forward_input
    : Notation.DoubleColon t "forward_input" := {
    Notation.double_colon '(Build_t x0 _ _ _) := x0;
  }.
  Global Instance Get_clone_input : Notation.Dot "clone_input" := {
    Notation.dot '(Build_t _ x1 _ _) := x1;
  }.
  Global Instance Get_AF_clone_input : Notation.DoubleColon t "clone_input" := {
    Notation.double_colon '(Build_t _ x1 _ _) := x1;
  }.
  Global Instance Get_tail_call : Notation.Dot "tail_call" := {
    Notation.dot '(Build_t _ _ x2 _) := x2;
  }.
  Global Instance Get_AF_tail_call : Notation.DoubleColon t "tail_call" := {
    Notation.double_colon '(Build_t _ _ x2 _) := x2;
  }.
  Global Instance Get_allow_reentry : Notation.Dot "allow_reentry" := {
    Notation.dot '(Build_t _ _ _ x3) := x3;
  }.
  Global Instance Get_AF_allow_reentry
    : Notation.DoubleColon t "allow_reentry" := {
    Notation.double_colon '(Build_t _ _ _ x3) := x3;
  }.
End CallFlags.
Definition CallFlags : Set := CallFlags.t.

Module EnvBackend.
  Class Trait (Self : Set) : Type := {
    set_contract_storage
      `{H' : State.Trait}
      {K V : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait V}
      :
      (mut_ref Self) ->
        (ref K) ->
        (ref V) ->
        M (H := H') (core.option.Option u32);
    get_contract_storage
      `{H' : State.Trait}
      {K R : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait R}
      :
      (mut_ref Self) ->
        (ref K) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (core.option.Option R));
    take_contract_storage
      `{H' : State.Trait}
      {K R : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait R}
      :
      (mut_ref Self) ->
        (ref K) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (core.option.Option R));
    contains_contract_storage
      `{H' : State.Trait}
      {K : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      :
      (mut_ref Self) -> (ref K) -> M (H := H') (core.option.Option u32);
    clear_contract_storage
      `{H' : State.Trait}
      {K : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      :
      (mut_ref Self) -> (ref K) -> M (H := H') (core.option.Option u32);
    decode_input
      `{H' : State.Trait}
      {T : Set}
      `{H'0 : parity_scale_codec.codec.Decode.Trait T}
      :
      (mut_ref Self) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            T);
    return_value
      `{H' : State.Trait}
      {R : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait R}
      :
      (mut_ref Self) ->
        ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.ReturnFlags
        ->
        (ref R) ->
        M (H := H') Empty_set;
    debug_message `{H' : State.Trait}
      :
      (mut_ref Self) -> (ref str) -> M (H := H') unit;
    hash_bytes
      `{H' : State.Trait}
      {H : Set}
      `{H'0 : ink_env.hash.CryptoHash.Trait H}
      :
      (mut_ref Self) ->
        (ref (Slice u8)) ->
        (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
        M (H := H') unit;
    hash_encoded
      `{H' : State.Trait}
      {H T : Set}
      `{H'0 : ink_env.hash.CryptoHash.Trait H}
      `{H'1 : parity_scale_codec.codec.Encode.Trait T}
      :
      (mut_ref Self) ->
        (ref T) ->
        (mut_ref (ink_env.hash.HashOutput.Type_ (Self := H))) ->
        M (H := H') unit;
    ecdsa_recover `{H' : State.Trait}
      :
      (mut_ref Self) ->
        (ref (list u8)) ->
        (ref (list u8)) ->
        (mut_ref (list u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit);
    ecdsa_to_eth_address `{H' : State.Trait}
      :
      (mut_ref Self) ->
        (ref (list u8)) ->
        (mut_ref (list u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit);
    call_chain_extension
      `{H' : State.Trait}
      {I T E ErrorCode F D : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait I}
      `{H'1 : parity_scale_codec.codec.Decode.Trait T}
      `{H'2 : core.convert.From.Trait E (T := ErrorCode)}
      `{H'3 : core.ops.function.FnOnce.Trait F (Args := u32)}
      `{H'4 : core.ops.function.FnOnce.Trait D (Args := ref (Slice u8))}
      :
      (mut_ref Self) ->
        u32 ->
        (ref I) ->
        F ->
        D ->
        M (H := H') (core.result.Result T E);
    set_code_hash `{H' : State.Trait}
      :
      (mut_ref Self) ->
        (ref (Slice u8)) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit);
  }.
  
  Global Instance Method_set_contract_storage `{H' : State.Trait} `(Trait)
    : Notation.Dot "set_contract_storage" := {
    Notation.dot
      {K V : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait V}
      :=
      set_contract_storage (K := K) (V := V) (H'0 := H'0) (H'1 := H'1);
  }.
  Global Instance Method_get_contract_storage `{H' : State.Trait} `(Trait)
    : Notation.Dot "get_contract_storage" := {
    Notation.dot
      {K R : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait R}
      :=
      get_contract_storage (K := K) (R := R) (H'0 := H'0) (H'1 := H'1);
  }.
  Global Instance Method_take_contract_storage `{H' : State.Trait} `(Trait)
    : Notation.Dot "take_contract_storage" := {
    Notation.dot
      {K R : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      `{H'1 : ink_storage_traits.storage.Storable.Trait R}
      :=
      take_contract_storage (K := K) (R := R) (H'0 := H'0) (H'1 := H'1);
  }.
  Global Instance Method_contains_contract_storage `{H' : State.Trait} `(Trait)
    : Notation.Dot "contains_contract_storage" := {
    Notation.dot {K : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      :=
      contains_contract_storage (K := K) (H'0 := H'0);
  }.
  Global Instance Method_clear_contract_storage `{H' : State.Trait} `(Trait)
    : Notation.Dot "clear_contract_storage" := {
    Notation.dot {K : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait K}
      :=
      clear_contract_storage (K := K) (H'0 := H'0);
  }.
  Global Instance Method_decode_input `{H' : State.Trait} `(Trait)
    : Notation.Dot "decode_input" := {
    Notation.dot {T : Set} `{H'0 : parity_scale_codec.codec.Decode.Trait T}
      :=
      decode_input (T := T) (H'0 := H'0);
  }.
  Global Instance Method_return_value `{H' : State.Trait} `(Trait)
    : Notation.Dot "return_value" := {
    Notation.dot {R : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait R}
      :=
      return_value (R := R) (H'0 := H'0);
  }.
  Global Instance Method_debug_message `{H' : State.Trait} `(Trait)
    : Notation.Dot "debug_message" := {
    Notation.dot := debug_message;
  }.
  Global Instance Method_hash_bytes `{H' : State.Trait} `(Trait)
    : Notation.Dot "hash_bytes" := {
    Notation.dot {H : Set} `{H'0 : ink_env.hash.CryptoHash.Trait H}
      :=
      hash_bytes (H := H) (H'0 := H'0);
  }.
  Global Instance Method_hash_encoded `{H' : State.Trait} `(Trait)
    : Notation.Dot "hash_encoded" := {
    Notation.dot
      {H T : Set}
      `{H'0 : ink_env.hash.CryptoHash.Trait H}
      `{H'1 : parity_scale_codec.codec.Encode.Trait T}
      :=
      hash_encoded (H := H) (T := T) (H'0 := H'0) (H'1 := H'1);
  }.
  Global Instance Method_ecdsa_recover `{H' : State.Trait} `(Trait)
    : Notation.Dot "ecdsa_recover" := {
    Notation.dot := ecdsa_recover;
  }.
  Global Instance Method_ecdsa_to_eth_address `{H' : State.Trait} `(Trait)
    : Notation.Dot "ecdsa_to_eth_address" := {
    Notation.dot := ecdsa_to_eth_address;
  }.
  Global Instance Method_call_chain_extension `{H' : State.Trait} `(Trait)
    : Notation.Dot "call_chain_extension" := {
    Notation.dot
      {I T E ErrorCode F D : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait I}
      `{H'1 : parity_scale_codec.codec.Decode.Trait T}
      `{H'2 : core.convert.From.Trait E (T := ErrorCode)}
      `{H'3 : core.ops.function.FnOnce.Trait F (Args := u32)}
      `{H'4 : core.ops.function.FnOnce.Trait D (Args := ref (Slice u8))}
      :=
      call_chain_extension
          (I := I)
          (T := T)
          (E := E)
          (ErrorCode := ErrorCode)
          (F := F)
          (D := D)
        (H'0 := H'0)
        (H'1 := H'1)
        (H'2 := H'2)
        (H'3 := H'3)
        (H'4 := H'4);
  }.
  Global Instance Method_set_code_hash `{H' : State.Trait} `(Trait)
    : Notation.Dot "set_code_hash" := {
    Notation.dot := set_code_hash;
  }.
End EnvBackend.

Module TypedEnvBackend.
  Class Trait
      (Self : Set)
      `{ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.EnvBackend.Trait
            Self} :
      Type := {
    caller
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["AccountId"];
    transferred_value
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["Balance"];
    weight_to_fee
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> u64 -> M (H := H') E::type["Balance"];
    gas_left
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') u64;
    block_timestamp
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["Timestamp"];
    account_id
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["AccountId"];
    balance
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["Balance"];
    block_number
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["BlockNumber"];
    minimum_balance
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') E::type["Balance"];
    emit_event
      `{H' : State.Trait}
      {E Event : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : ink_env.topics.Topics.Trait Event}
      `{H'2 : parity_scale_codec.codec.Encode.Trait Event}
      :
      (mut_ref Self) -> Event -> M (H := H') unit;
    invoke_contract
      `{H' : State.Trait}
      {E Args R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'2 : parity_scale_codec.codec.Decode.Trait R}
      :
      (mut_ref Self) ->
        (ref
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
            E
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Call
              E)
            Args
            R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.MessageResult R));
    invoke_contract_delegate
      `{H' : State.Trait}
      {E Args R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'2 : parity_scale_codec.codec.Decode.Trait R}
      :
      (mut_ref Self) ->
        (ref
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.CallParams
            E
            (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.DelegateCall
              E)
            Args
            R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.MessageResult R));
    instantiate_contract
      `{H' : State.Trait}
      {E ContractRef Args Salt R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1
        :
        ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
      `{H'2 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'3 : core.convert.AsRef.Trait Salt (T := Slice u8)}
      `{H'4
        :
        ink_env.call.create_builder.ConstructorReturnType.Trait R
          (C := ContractRef)}
      :
      (mut_ref Self) ->
        (ref
          (ink_env.call.create_builder.CreateParams E ContractRef Args Salt R))
        ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            (ink_primitives.ConstructorResult
              (ink_env.call.create_builder.ConstructorReturnType.Output
                (Self := R))));
    terminate_contract
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> E::type["AccountId"] -> M (H := H') Empty_set;
    transfer
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) ->
        E::type["AccountId"] ->
        E::type["Balance"] ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit);
    is_contract
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> (ref E::type["AccountId"]) -> M (H := H') bool;
    caller_is_origin
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) -> M (H := H') bool;
    code_hash
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) ->
        (ref E::type["AccountId"]) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            E::type["Hash"]);
    own_code_hash
      `{H' : State.Trait}
      {E : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      :
      (mut_ref Self) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            E::type["Hash"]);
    call_runtime
      `{H' : State.Trait}
      {E Call : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Call}
      :
      (mut_ref Self) ->
        (ref Call) ->
        M (H := H')
          (ink_env.backend_and_call_builder_and_engine_and_engine_test_api_and_error.Result
            unit);
  }.
  
  Global Instance Method_caller `{H' : State.Trait} `(Trait)
    : Notation.Dot "caller" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      caller (E := E) (H'0 := H'0);
  }.
  Global Instance Method_transferred_value `{H' : State.Trait} `(Trait)
    : Notation.Dot "transferred_value" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      transferred_value (E := E) (H'0 := H'0);
  }.
  Global Instance Method_weight_to_fee `{H' : State.Trait} `(Trait)
    : Notation.Dot "weight_to_fee" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      weight_to_fee (E := E) (H'0 := H'0);
  }.
  Global Instance Method_gas_left `{H' : State.Trait} `(Trait)
    : Notation.Dot "gas_left" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      gas_left (E := E) (H'0 := H'0);
  }.
  Global Instance Method_block_timestamp `{H' : State.Trait} `(Trait)
    : Notation.Dot "block_timestamp" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      block_timestamp (E := E) (H'0 := H'0);
  }.
  Global Instance Method_account_id `{H' : State.Trait} `(Trait)
    : Notation.Dot "account_id" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      account_id (E := E) (H'0 := H'0);
  }.
  Global Instance Method_balance `{H' : State.Trait} `(Trait)
    : Notation.Dot "balance" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      balance (E := E) (H'0 := H'0);
  }.
  Global Instance Method_block_number `{H' : State.Trait} `(Trait)
    : Notation.Dot "block_number" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      block_number (E := E) (H'0 := H'0);
  }.
  Global Instance Method_minimum_balance `{H' : State.Trait} `(Trait)
    : Notation.Dot "minimum_balance" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      minimum_balance (E := E) (H'0 := H'0);
  }.
  Global Instance Method_emit_event `{H' : State.Trait} `(Trait)
    : Notation.Dot "emit_event" := {
    Notation.dot
      {E Event : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : ink_env.topics.Topics.Trait Event}
      `{H'2 : parity_scale_codec.codec.Encode.Trait Event}
      :=
      emit_event (E := E) (Event := Event)
        (H'0 := H'0)
        (H'1 := H'1)
        (H'2 := H'2);
  }.
  Global Instance Method_invoke_contract `{H' : State.Trait} `(Trait)
    : Notation.Dot "invoke_contract" := {
    Notation.dot
      {E Args R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'2 : parity_scale_codec.codec.Decode.Trait R}
      :=
      invoke_contract (E := E) (Args := Args) (R := R)
        (H'0 := H'0)
        (H'1 := H'1)
        (H'2 := H'2);
  }.
  Global Instance Method_invoke_contract_delegate `{H' : State.Trait} `(Trait)
    : Notation.Dot "invoke_contract_delegate" := {
    Notation.dot
      {E Args R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'2 : parity_scale_codec.codec.Decode.Trait R}
      :=
      invoke_contract_delegate (E := E) (Args := Args) (R := R)
        (H'0 := H'0)
        (H'1 := H'1)
        (H'2 := H'2);
  }.
  Global Instance Method_instantiate_contract `{H' : State.Trait} `(Trait)
    : Notation.Dot "instantiate_contract" := {
    Notation.dot
      {E ContractRef Args Salt R : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1
        :
        ink_env.call.create_builder.FromAccountId.Trait ContractRef (T := E)}
      `{H'2 : parity_scale_codec.codec.Encode.Trait Args}
      `{H'3 : core.convert.AsRef.Trait Salt (T := Slice u8)}
      `{H'4
        :
        ink_env.call.create_builder.ConstructorReturnType.Trait R
          (C := ContractRef)}
      :=
      instantiate_contract
          (E := E)
          (ContractRef := ContractRef)
          (Args := Args)
          (Salt := Salt)
          (R := R)
        (H'0 := H'0)
        (H'1 := H'1)
        (H'2 := H'2)
        (H'3 := H'3)
        (H'4 := H'4);
  }.
  Global Instance Method_terminate_contract `{H' : State.Trait} `(Trait)
    : Notation.Dot "terminate_contract" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      terminate_contract (E := E) (H'0 := H'0);
  }.
  Global Instance Method_transfer `{H' : State.Trait} `(Trait)
    : Notation.Dot "transfer" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      transfer (E := E) (H'0 := H'0);
  }.
  Global Instance Method_is_contract `{H' : State.Trait} `(Trait)
    : Notation.Dot "is_contract" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      is_contract (E := E) (H'0 := H'0);
  }.
  Global Instance Method_caller_is_origin `{H' : State.Trait} `(Trait)
    : Notation.Dot "caller_is_origin" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      caller_is_origin (E := E) (H'0 := H'0);
  }.
  Global Instance Method_code_hash `{H' : State.Trait} `(Trait)
    : Notation.Dot "code_hash" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      code_hash (E := E) (H'0 := H'0);
  }.
  Global Instance Method_own_code_hash `{H' : State.Trait} `(Trait)
    : Notation.Dot "own_code_hash" := {
    Notation.dot {E : Set} `{H'0 : ink_env.types.Environment.Trait E}
      :=
      own_code_hash (E := E) (H'0 := H'0);
  }.
  Global Instance Method_call_runtime `{H' : State.Trait} `(Trait)
    : Notation.Dot "call_runtime" := {
    Notation.dot
      {E Call : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : parity_scale_codec.codec.Encode.Trait Call}
      :=
      call_runtime (E := E) (Call := Call) (H'0 := H'0) (H'1 := H'1);
  }.
End TypedEnvBackend.

Module common.
  Module ReturnType.
    Section ReturnType.
      Context {T : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        _ : core.marker.PhantomData (T);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_0 : Notation.Dot 0 := {
        Notation.dot '(Build_t x0) := x0;
      }.
    End ReturnType.
  End ReturnType.
  Definition ReturnType := @ReturnType.t.
  
  Module Set_.
    Section Set_.
      Context {T : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        _ : T;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_0 : Notation.Dot 0 := {
        Notation.dot '(Build_t x0) := x0;
      }.
    End Set_.
  End Set_.
  Definition Set_ := @Set_.t.
  
  Module Unset_.
    Section Unset_.
      Context {T : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        _ : core.marker.PhantomData (T);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_0 : Notation.Dot 0 := {
        Notation.dot '(Build_t x0) := x0;
      }.
    End Unset_.
  End Unset_.
  Definition Unset_ := @Unset_.t.
  
  Module Unwrap.
    Class Trait (Self : Set) : Type := {
      Output : Set;
      unwrap_or_else
        `{H' : State.Trait}
        {F : Set}
        `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
        :
        Self -> F -> M (H := H') Output;
    }.
    
    Global Instance Method_Output `(Trait)
      : Notation.DoubleColonType Self "Output" := {
      Notation.double_colon_type := Output;
    }.
    Global Instance Method_unwrap_or_else `{H' : State.Trait} `(Trait)
      : Notation.Dot "unwrap_or_else" := {
      Notation.dot
        {F : Set}
        `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
        :=
        unwrap_or_else (F := F) (H'0 := H'0);
    }.
  End Unwrap.
End common.

Module ReturnType.
  Section ReturnType.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      _ : core.marker.PhantomData (T);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_0 : Notation.Dot 0 := {
      Notation.dot '(Build_t x0) := x0;
    }.
  End ReturnType.
End ReturnType.
Definition ReturnType := @ReturnType.t.

Module Set_.
  Section Set_.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      _ : T;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_0 : Notation.Dot 0 := {
      Notation.dot '(Build_t x0) := x0;
    }.
  End Set_.
End Set_.
Definition Set_ := @Set_.t.

Module Unset_.
  Section Unset_.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      _ : core.marker.PhantomData (T);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_0 : Notation.Dot 0 := {
      Notation.dot '(Build_t x0) := x0;
    }.
  End Unset_.
End Unset_.
Definition Unset_ := @Unset_.t.

Module Unwrap.
  Class Trait (Self : Set) : Type := {
    Output : Set;
    unwrap_or_else
      `{H' : State.Trait}
      {F : Set}
      `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
      :
      Self -> F -> M (H := H') Output;
  }.
  
  Global Instance Method_Output `(Trait)
    : Notation.DoubleColonType Self "Output" := {
    Notation.double_colon_type := Output;
  }.
  Global Instance Method_unwrap_or_else `{H' : State.Trait} `(Trait)
    : Notation.Dot "unwrap_or_else" := {
    Notation.dot
      {F : Set}
      `{H'0 : core.ops.function.FnOnce.Trait F (Args := unit)}
      :=
      unwrap_or_else (F := F) (H'0 := H'0);
  }.
End Unwrap.

Module create_builder.
  Module state.
    Module Salt.
      Inductive t : Set :=
      .
    End Salt.
    Definition Salt : Set := Salt.t.
  End state.
  
  Module FromAccountId.
    Class Trait (Self : Set) {T : Set} `{ink_env.types.Environment.Trait T} :
        Type := {
      from_account_id `{H' : State.Trait}
        :
        (ink_env.types.Environment.AccountId (Self := T)) -> M (H := H') Self;
    }.
    
    Global Instance Method_from_account_id `{H' : State.Trait} `(Trait)
      : Notation.Dot "from_account_id" := {
      Notation.dot := from_account_id;
    }.
  End FromAccountId.
  
  Module ConstructorReturnType.
    Class Trait (Self : Set) {C : Set} : Type := {
      IS_RESULT `{H' : State.Trait} : bool;
      Output : Set;
      Error : Set;
      _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit;
      ok `{H' : State.Trait} : C -> M (H := H') Output;
    }.
    
    Global Instance Method_IS_RESULT `{H' : State.Trait} `(Trait)
      : Notation.Dot "IS_RESULT" := {
      Notation.dot := IS_RESULT;
    }.
    Global Instance Method_Output `(Trait)
      : Notation.DoubleColonType Self "Output" := {
      Notation.double_colon_type := Output;
    }.
    Global Instance Method_Error `(Trait)
      : Notation.DoubleColonType Self "Error" := {
      Notation.double_colon_type := Error;
    }.
    Global Instance Method_ok `{H' : State.Trait} `(Trait)
      : Notation.Dot "ok" := {
      Notation.dot := ok;
    }.
    Global Instance Method_err `{H' : State.Trait} `(Trait)
      : Notation.Dot "err" := {
      Notation.dot (_err : Error)
        :=
        (axiom : M (H := H') (core.option.Option Output));
    }.
  End ConstructorReturnType.
  
  Module CreateParams.
    Section CreateParams.
      Context {E ContractRef Args Salt R : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        code_hash : E::type["Hash"];
        gas_limit : u64;
        endowment : E::type["Balance"];
        exec_input : ink_env.call.execution_input.ExecutionInput Args;
        salt_bytes : Salt;
        _return_type : ink_env.call.common.ReturnType R;
        _phantom : core.marker.PhantomData (ContractRef);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_code_hash : Notation.Dot "code_hash" := {
        Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
      }.
      Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
        Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
      }.
      Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
        Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
      }.
      Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
        Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
      }.
      Global Instance Get_endowment : Notation.Dot "endowment" := {
        Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
      }.
      Global Instance Get_AF_endowment : Notation.DoubleColon t "endowment" := {
        Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
      }.
      Global Instance Get_exec_input : Notation.Dot "exec_input" := {
        Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
      }.
      Global Instance Get_AF_exec_input
        : Notation.DoubleColon t "exec_input" := {
        Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
      }.
      Global Instance Get_salt_bytes : Notation.Dot "salt_bytes" := {
        Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
      }.
      Global Instance Get_AF_salt_bytes
        : Notation.DoubleColon t "salt_bytes" := {
        Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
      }.
      Global Instance Get__return_type : Notation.Dot "_return_type" := {
        Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
      }.
      Global Instance Get_AF__return_type
        : Notation.DoubleColon t "_return_type" := {
        Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
      }.
      Global Instance Get__phantom : Notation.Dot "_phantom" := {
        Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
      }.
      Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
        Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
      }.
    End CreateParams.
  End CreateParams.
  Definition CreateParams
      (E ContractRef Args Salt R : Set)
      `{ink_env.types.Environment.Trait E}
      : Set :=
    CreateParams.t
      (E := E)
      (ContractRef := ContractRef)
      (Args := Args)
      (Salt := Salt)
      (R := R).
  
  Module CreateBuilder.
    Section CreateBuilder.
      Context
        {E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set}.
      Context `{ink_env.types.Environment.Trait E}.
      Unset Primitive Projections.
      Record t : Set := {
        code_hash : CodeHash;
        gas_limit : GasLimit;
        endowment : Endowment;
        exec_input : Args;
        salt : Salt;
        return_type : RetType;
        _phantom : core.marker.PhantomData (E * ContractRef);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_code_hash : Notation.Dot "code_hash" := {
        Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
      }.
      Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
        Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
      }.
      Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
        Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
      }.
      Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
        Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
      }.
      Global Instance Get_endowment : Notation.Dot "endowment" := {
        Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
      }.
      Global Instance Get_AF_endowment : Notation.DoubleColon t "endowment" := {
        Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
      }.
      Global Instance Get_exec_input : Notation.Dot "exec_input" := {
        Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
      }.
      Global Instance Get_AF_exec_input
        : Notation.DoubleColon t "exec_input" := {
        Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
      }.
      Global Instance Get_salt : Notation.Dot "salt" := {
        Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
      }.
      Global Instance Get_AF_salt : Notation.DoubleColon t "salt" := {
        Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
      }.
      Global Instance Get_return_type : Notation.Dot "return_type" := {
        Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
      }.
      Global Instance Get_AF_return_type
        : Notation.DoubleColon t "return_type" := {
        Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
      }.
      Global Instance Get__phantom : Notation.Dot "_phantom" := {
        Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
      }.
      Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
        Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
      }.
    End CreateBuilder.
  End CreateBuilder.
  Definition CreateBuilder
      (E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set)
      `{ink_env.types.Environment.Trait E}
      : Set :=
    CreateBuilder.t
      (E := E)
      (ContractRef := ContractRef)
      (CodeHash := CodeHash)
      (GasLimit := GasLimit)
      (Endowment := Endowment)
      (Args := Args)
      (Salt := Salt)
      (RetType := RetType).
End create_builder.

Module state.
  Module Salt.
    Inductive t : Set :=
    .
  End Salt.
  Definition Salt : Set := Salt.t.
End state.

Module Salt.
  Inductive t : Set :=
  .
End Salt.
Definition Salt : Set := Salt.t.

Module FromAccountId.
  Class Trait (Self : Set) {T : Set} `{ink_env.types.Environment.Trait T} :
      Type := {
    from_account_id `{H' : State.Trait}
      :
      (ink_env.types.Environment.AccountId (Self := T)) -> M (H := H') Self;
  }.
  
  Global Instance Method_from_account_id `{H' : State.Trait} `(Trait)
    : Notation.Dot "from_account_id" := {
    Notation.dot := from_account_id;
  }.
End FromAccountId.

Module ConstructorReturnType.
  Class Trait (Self : Set) {C : Set} : Type := {
    IS_RESULT `{H' : State.Trait} : bool;
    Output : Set;
    Error : Set;
    _ : Sigma `(parity_scale_codec.codec.Decode.Trait Error), unit;
    ok `{H' : State.Trait} : C -> M (H := H') Output;
  }.
  
  Global Instance Method_IS_RESULT `{H' : State.Trait} `(Trait)
    : Notation.Dot "IS_RESULT" := {
    Notation.dot := IS_RESULT;
  }.
  Global Instance Method_Output `(Trait)
    : Notation.DoubleColonType Self "Output" := {
    Notation.double_colon_type := Output;
  }.
  Global Instance Method_Error `(Trait)
    : Notation.DoubleColonType Self "Error" := {
    Notation.double_colon_type := Error;
  }.
  Global Instance Method_ok `{H' : State.Trait} `(Trait)
    : Notation.Dot "ok" := {
    Notation.dot := ok;
  }.
  Global Instance Method_err `{H' : State.Trait} `(Trait)
    : Notation.Dot "err" := {
    Notation.dot (_err : Error)
      :=
      (axiom : M (H := H') (core.option.Option Output));
  }.
End ConstructorReturnType.

Module CreateParams.
  Section CreateParams.
    Context {E ContractRef Args Salt R : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      code_hash : E::type["Hash"];
      gas_limit : u64;
      endowment : E::type["Balance"];
      exec_input : ink_env.call.execution_input.ExecutionInput Args;
      salt_bytes : Salt;
      _return_type : ink_env.call.common.ReturnType R;
      _phantom : core.marker.PhantomData (ContractRef);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_code_hash : Notation.Dot "code_hash" := {
      Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
    }.
    Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
      Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
    }.
    Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
      Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
    }.
    Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
      Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
    }.
    Global Instance Get_endowment : Notation.Dot "endowment" := {
      Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
    }.
    Global Instance Get_AF_endowment : Notation.DoubleColon t "endowment" := {
      Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
    }.
    Global Instance Get_exec_input : Notation.Dot "exec_input" := {
      Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
    }.
    Global Instance Get_AF_exec_input : Notation.DoubleColon t "exec_input" := {
      Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
    }.
    Global Instance Get_salt_bytes : Notation.Dot "salt_bytes" := {
      Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
    }.
    Global Instance Get_AF_salt_bytes : Notation.DoubleColon t "salt_bytes" := {
      Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
    }.
    Global Instance Get__return_type : Notation.Dot "_return_type" := {
      Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
    }.
    Global Instance Get_AF__return_type
      : Notation.DoubleColon t "_return_type" := {
      Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
    }.
    Global Instance Get__phantom : Notation.Dot "_phantom" := {
      Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
    }.
    Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
      Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
    }.
  End CreateParams.
End CreateParams.
Definition CreateParams
    (E ContractRef Args Salt R : Set)
    `{ink_env.types.Environment.Trait E}
    : Set :=
  CreateParams.t
    (E := E)
    (ContractRef := ContractRef)
    (Args := Args)
    (Salt := Salt)
    (R := R).

Module CreateBuilder.
  Section CreateBuilder.
    Context {E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set}.
    Context `{ink_env.types.Environment.Trait E}.
    Unset Primitive Projections.
    Record t : Set := {
      code_hash : CodeHash;
      gas_limit : GasLimit;
      endowment : Endowment;
      exec_input : Args;
      salt : Salt;
      return_type : RetType;
      _phantom : core.marker.PhantomData (E * ContractRef);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_code_hash : Notation.Dot "code_hash" := {
      Notation.dot '(Build_t x0 _ _ _ _ _ _) := x0;
    }.
    Global Instance Get_AF_code_hash : Notation.DoubleColon t "code_hash" := {
      Notation.double_colon '(Build_t x0 _ _ _ _ _ _) := x0;
    }.
    Global Instance Get_gas_limit : Notation.Dot "gas_limit" := {
      Notation.dot '(Build_t _ x1 _ _ _ _ _) := x1;
    }.
    Global Instance Get_AF_gas_limit : Notation.DoubleColon t "gas_limit" := {
      Notation.double_colon '(Build_t _ x1 _ _ _ _ _) := x1;
    }.
    Global Instance Get_endowment : Notation.Dot "endowment" := {
      Notation.dot '(Build_t _ _ x2 _ _ _ _) := x2;
    }.
    Global Instance Get_AF_endowment : Notation.DoubleColon t "endowment" := {
      Notation.double_colon '(Build_t _ _ x2 _ _ _ _) := x2;
    }.
    Global Instance Get_exec_input : Notation.Dot "exec_input" := {
      Notation.dot '(Build_t _ _ _ x3 _ _ _) := x3;
    }.
    Global Instance Get_AF_exec_input : Notation.DoubleColon t "exec_input" := {
      Notation.double_colon '(Build_t _ _ _ x3 _ _ _) := x3;
    }.
    Global Instance Get_salt : Notation.Dot "salt" := {
      Notation.dot '(Build_t _ _ _ _ x4 _ _) := x4;
    }.
    Global Instance Get_AF_salt : Notation.DoubleColon t "salt" := {
      Notation.double_colon '(Build_t _ _ _ _ x4 _ _) := x4;
    }.
    Global Instance Get_return_type : Notation.Dot "return_type" := {
      Notation.dot '(Build_t _ _ _ _ _ x5 _) := x5;
    }.
    Global Instance Get_AF_return_type
      : Notation.DoubleColon t "return_type" := {
      Notation.double_colon '(Build_t _ _ _ _ _ x5 _) := x5;
    }.
    Global Instance Get__phantom : Notation.Dot "_phantom" := {
      Notation.dot '(Build_t _ _ _ _ _ _ x6) := x6;
    }.
    Global Instance Get_AF__phantom : Notation.DoubleColon t "_phantom" := {
      Notation.double_colon '(Build_t _ _ _ _ _ _ x6) := x6;
    }.
  End CreateBuilder.
End CreateBuilder.
Definition CreateBuilder
    (E ContractRef CodeHash GasLimit Endowment Args Salt RetType : Set)
    `{ink_env.types.Environment.Trait E}
    : Set :=
  CreateBuilder.t
    (E := E)
    (ContractRef := ContractRef)
    (CodeHash := CodeHash)
    (GasLimit := GasLimit)
    (Endowment := Endowment)
    (Args := Args)
    (Salt := Salt)
    (RetType := RetType).

Module execution_input.
  Module ExecutionInput.
    Section ExecutionInput.
      Context {Args : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        selector : ink_env.call.selector.Selector;
        args : Args;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_selector : Notation.Dot "selector" := {
        Notation.dot '(Build_t x0 _) := x0;
      }.
      Global Instance Get_AF_selector : Notation.DoubleColon t "selector" := {
        Notation.double_colon '(Build_t x0 _) := x0;
      }.
      Global Instance Get_args : Notation.Dot "args" := {
        Notation.dot '(Build_t _ x1) := x1;
      }.
      Global Instance Get_AF_args : Notation.DoubleColon t "args" := {
        Notation.double_colon '(Build_t _ x1) := x1;
      }.
    End ExecutionInput.
  End ExecutionInput.
  Definition ExecutionInput (Args : Set) : Set :=
    ExecutionInput.t (Args := Args).
  
  Module ArgumentList.
    Section ArgumentList.
      Context {Head Rest : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        head : Head;
        rest : Rest;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_head : Notation.Dot "head" := {
        Notation.dot '(Build_t x0 _) := x0;
      }.
      Global Instance Get_AF_head : Notation.DoubleColon t "head" := {
        Notation.double_colon '(Build_t x0 _) := x0;
      }.
      Global Instance Get_rest : Notation.Dot "rest" := {
        Notation.dot '(Build_t _ x1) := x1;
      }.
      Global Instance Get_AF_rest : Notation.DoubleColon t "rest" := {
        Notation.double_colon '(Build_t _ x1) := x1;
      }.
    End ArgumentList.
  End ArgumentList.
  Definition ArgumentList (Head Rest : Set) : Set :=
    ArgumentList.t (Head := Head) (Rest := Rest).
  
  Module Argument.
    Section Argument.
      Context {T : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        arg : T;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_arg : Notation.Dot "arg" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_arg : Notation.DoubleColon t "arg" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End Argument.
  End Argument.
  Definition Argument (T : Set) : Set := Argument.t (T := T).
  
  Definition ArgsList (Head Rest : Set) : Set :=
    ink_env.call.execution_input.ArgumentList
      (ink_env.call.execution_input.Argument Head)
      Rest.
  
  Module ArgumentListEnd.
    Inductive t : Set := Build.
  End ArgumentListEnd.
  Definition ArgumentListEnd := @ArgumentListEnd.t.
  
  Definition EmptyArgumentList : Set :=
    ink_env.call.execution_input.ArgumentList
      ink_env.call.execution_input.ArgumentListEnd
      ink_env.call.execution_input.ArgumentListEnd.
End execution_input.

Module ExecutionInput.
  Section ExecutionInput.
    Context {Args : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      selector : ink_env.call.selector.Selector;
      args : Args;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_selector : Notation.Dot "selector" := {
      Notation.dot '(Build_t x0 _) := x0;
    }.
    Global Instance Get_AF_selector : Notation.DoubleColon t "selector" := {
      Notation.double_colon '(Build_t x0 _) := x0;
    }.
    Global Instance Get_args : Notation.Dot "args" := {
      Notation.dot '(Build_t _ x1) := x1;
    }.
    Global Instance Get_AF_args : Notation.DoubleColon t "args" := {
      Notation.double_colon '(Build_t _ x1) := x1;
    }.
  End ExecutionInput.
End ExecutionInput.
Definition ExecutionInput (Args : Set) : Set := ExecutionInput.t (Args := Args).

Module ArgumentList.
  Section ArgumentList.
    Context {Head Rest : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      head : Head;
      rest : Rest;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_head : Notation.Dot "head" := {
      Notation.dot '(Build_t x0 _) := x0;
    }.
    Global Instance Get_AF_head : Notation.DoubleColon t "head" := {
      Notation.double_colon '(Build_t x0 _) := x0;
    }.
    Global Instance Get_rest : Notation.Dot "rest" := {
      Notation.dot '(Build_t _ x1) := x1;
    }.
    Global Instance Get_AF_rest : Notation.DoubleColon t "rest" := {
      Notation.double_colon '(Build_t _ x1) := x1;
    }.
  End ArgumentList.
End ArgumentList.
Definition ArgumentList (Head Rest : Set) : Set :=
  ArgumentList.t (Head := Head) (Rest := Rest).

Definition ArgsList (Head Rest : Set) : Set :=
  ink_env.call.execution_input.ArgumentList
    (ink_env.call.execution_input.Argument Head)
    Rest.

Module Argument.
  Section Argument.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      arg : T;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_arg : Notation.Dot "arg" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_arg : Notation.DoubleColon t "arg" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End Argument.
End Argument.
Definition Argument (T : Set) : Set := Argument.t (T := T).

Module ArgumentListEnd.
  Inductive t : Set := Build.
End ArgumentListEnd.
Definition ArgumentListEnd := @ArgumentListEnd.t.

Definition EmptyArgumentList : Set :=
  ink_env.call.execution_input.ArgumentList
    ink_env.call.execution_input.ArgumentListEnd
    ink_env.call.execution_input.ArgumentListEnd.

Module selector.
  Module Selector.
    Unset Primitive Projections.
    Record t : Set := {
      bytes : list u8;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_bytes : Notation.Dot "bytes" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End Selector.
  Definition Selector : Set := Selector.t.
End selector.

Module Selector.
  Unset Primitive Projections.
  Record t : Set := {
    bytes : list u8;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_bytes : Notation.Dot "bytes" := {
    Notation.dot '(Build_t x0) := x0;
  }.
  Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
    Notation.double_colon '(Build_t x0) := x0;
  }.
End Selector.
Definition Selector : Set := Selector.t.

Module chain_extension.
  Module FromStatusCode.
    Class Trait (Self : Set) `{core.marker.Sized.Trait Self} : Type := {
      from_status_code `{H' : State.Trait}
        :
        u32 -> M (H := H') (core.result.Result unit Self);
    }.
    
    Global Instance Method_from_status_code `{H' : State.Trait} `(Trait)
      : Notation.Dot "from_status_code" := {
      Notation.dot := from_status_code;
    }.
  End FromStatusCode.
  
  Module ChainExtensionMethod.
    Section ChainExtensionMethod.
      Context {I O ErrorCode : Set}.
      Unset Primitive Projections.
      Record t : Set := {
        func_id : u32;
        state : core.marker.PhantomData ((I * O) * ErrorCode);
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_func_id : Notation.Dot "func_id" := {
        Notation.dot '(Build_t x0 _) := x0;
      }.
      Global Instance Get_AF_func_id : Notation.DoubleColon t "func_id" := {
        Notation.double_colon '(Build_t x0 _) := x0;
      }.
      Global Instance Get_state : Notation.Dot "state" := {
        Notation.dot '(Build_t _ x1) := x1;
      }.
      Global Instance Get_AF_state : Notation.DoubleColon t "state" := {
        Notation.double_colon '(Build_t _ x1) := x1;
      }.
    End ChainExtensionMethod.
  End ChainExtensionMethod.
  Definition ChainExtensionMethod (I O ErrorCode : Set) : Set :=
    ChainExtensionMethod.t (I := I) (O := O) (ErrorCode := ErrorCode).
  
  Module state.
    Module IgnoreErrorCode.
      Inductive t : Set :=
      .
    End IgnoreErrorCode.
    Definition IgnoreErrorCode : Set := IgnoreErrorCode.t.
    
    Module HandleErrorCode.
      Section HandleErrorCode.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          error_code : core.marker.PhantomData (T);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_error_code : Notation.Dot "error_code" := {
          Notation.dot '(Build_t x0) := x0;
        }.
        Global Instance Get_AF_error_code
          : Notation.DoubleColon t "error_code" := {
          Notation.double_colon '(Build_t x0) := x0;
        }.
      End HandleErrorCode.
    End HandleErrorCode.
    Definition HandleErrorCode (T : Set) : Set := HandleErrorCode.t (T := T).
  End state.
  
  Module private.
    Module IsResultTypeSealed.
      Unset Primitive Projections.
      Class Trait (Self : Set) : Type := {
      }.
      Global Set Primitive Projections.
    End IsResultTypeSealed.
  End private.
  
  Module IsResultType.
    Class Trait
        (Self : Set)
        `{ink_env.chain_extension.private.IsResultTypeSealed.Trait Self} :
        Type := {
      Ok : Set;
      Err : Set;
    }.
    
    Global Instance Method_Ok `(Trait) : Notation.DoubleColonType Self "Ok" := {
      Notation.double_colon_type := Ok;
    }.
    Global Instance Method_Err `(Trait)
      : Notation.DoubleColonType Self "Err" := {
      Notation.double_colon_type := Err;
    }.
  End IsResultType.
End chain_extension.

Module FromStatusCode.
  Class Trait (Self : Set) `{core.marker.Sized.Trait Self} : Type := {
    from_status_code `{H' : State.Trait}
      :
      u32 -> M (H := H') (core.result.Result unit Self);
  }.
  
  Global Instance Method_from_status_code `{H' : State.Trait} `(Trait)
    : Notation.Dot "from_status_code" := {
    Notation.dot := from_status_code;
  }.
End FromStatusCode.

Module ChainExtensionMethod.
  Section ChainExtensionMethod.
    Context {I O ErrorCode : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      func_id : u32;
      state : core.marker.PhantomData ((I * O) * ErrorCode);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_func_id : Notation.Dot "func_id" := {
      Notation.dot '(Build_t x0 _) := x0;
    }.
    Global Instance Get_AF_func_id : Notation.DoubleColon t "func_id" := {
      Notation.double_colon '(Build_t x0 _) := x0;
    }.
    Global Instance Get_state : Notation.Dot "state" := {
      Notation.dot '(Build_t _ x1) := x1;
    }.
    Global Instance Get_AF_state : Notation.DoubleColon t "state" := {
      Notation.double_colon '(Build_t _ x1) := x1;
    }.
  End ChainExtensionMethod.
End ChainExtensionMethod.
Definition ChainExtensionMethod (I O ErrorCode : Set) : Set :=
  ChainExtensionMethod.t (I := I) (O := O) (ErrorCode := ErrorCode).

Module Wrap_state_1.
  Module state.
    Module IgnoreErrorCode.
      Inductive t : Set :=
      .
    End IgnoreErrorCode.
    Definition IgnoreErrorCode : Set := IgnoreErrorCode.t.
    
    Module HandleErrorCode.
      Section HandleErrorCode.
        Context {T : Set}.
        Unset Primitive Projections.
        Record t : Set := {
          error_code : core.marker.PhantomData (T);
        }.
        Global Set Primitive Projections.
        
        Global Instance Get_error_code : Notation.Dot "error_code" := {
          Notation.dot '(Build_t x0) := x0;
        }.
        Global Instance Get_AF_error_code
          : Notation.DoubleColon t "error_code" := {
          Notation.double_colon '(Build_t x0) := x0;
        }.
      End HandleErrorCode.
    End HandleErrorCode.
    Definition HandleErrorCode (T : Set) : Set := HandleErrorCode.t (T := T).
  End state.
End Wrap_state_1.
Import Wrap_state_1.

Module IgnoreErrorCode.
  Inductive t : Set :=
  .
End IgnoreErrorCode.
Definition IgnoreErrorCode : Set := IgnoreErrorCode.t.

Module HandleErrorCode.
  Section HandleErrorCode.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      error_code : core.marker.PhantomData (T);
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_error_code : Notation.Dot "error_code" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_error_code : Notation.DoubleColon t "error_code" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End HandleErrorCode.
End HandleErrorCode.
Definition HandleErrorCode (T : Set) : Set := HandleErrorCode.t (T := T).

Module IsResultType.
  Class Trait
      (Self : Set)
      `{ink_env.chain_extension.private.IsResultTypeSealed.Trait Self} :
      Type := {
    Ok : Set;
    Err : Set;
  }.
  
  Global Instance Method_Ok `(Trait) : Notation.DoubleColonType Self "Ok" := {
    Notation.double_colon_type := Ok;
  }.
  Global Instance Method_Err `(Trait) : Notation.DoubleColonType Self "Err" := {
    Notation.double_colon_type := Err;
  }.
End IsResultType.

Module private.
  Module IsResultTypeSealed.
    Unset Primitive Projections.
    Class Trait (Self : Set) : Type := {
    }.
    Global Set Primitive Projections.
  End IsResultTypeSealed.
End private.

Module IsResultTypeSealed.
  Unset Primitive Projections.
  Class Trait (Self : Set) : Type := {
  }.
  Global Set Primitive Projections.
End IsResultTypeSealed.

Module ContractEnv.
  Class Trait (Self : Set) : Type := {
    Env : Set;
    _ : Sigma `(ink_env.types.Environment.Trait Env), unit;
  }.
  
  Global Instance Method_Env `(Trait) : Notation.DoubleColonType Self "Env" := {
    Notation.double_colon_type := Env;
  }.
End ContractEnv.

Module ContractReference.
  Class Trait (Self : Set) : Type := {
    Type_ : Set;
  }.
  
  Global Instance Method_Type_ `(Trait)
    : Notation.DoubleColonType Self "Type_" := {
    Notation.double_colon_type := Type_;
  }.
End ContractReference.

Module off_chain.
  Module call_data.
    Module CallData.
      Unset Primitive Projections.
      Record t : Set := {
        bytes : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_bytes : Notation.Dot "bytes" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End CallData.
    Definition CallData : Set := CallData.t.
  End call_data.
  
  Module impls.
    Module TopicsBuilder.
      Unset Primitive Projections.
      Record t : Set := {
        topics
          :
          alloc.vec.Vec
            (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
            alloc.vec.Vec.Default.A;
      }.
      Global Set Primitive Projections.
      
      Global Instance Get_topics : Notation.Dot "topics" := {
        Notation.dot '(Build_t x0) := x0;
      }.
      Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
        Notation.double_colon '(Build_t x0) := x0;
      }.
    End TopicsBuilder.
    Definition TopicsBuilder : Set := TopicsBuilder.t.
  End impls.
  
  Module EnvInstance.
    Unset Primitive Projections.
    Record t : Set := {
      engine : ink_engine.ext.Engine;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_engine : Notation.Dot "engine" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_engine : Notation.DoubleColon t "engine" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End EnvInstance.
  Definition EnvInstance : Set := EnvInstance.t.
  
  Module AccountError.
    Inductive t : Set :=
    | Decoding (_ : parity_scale_codec.error.Error)
    | UnexpectedUserAccount
    | NoAccountForId (_ : alloc.vec.Vec u8 alloc.vec.Vec.Default.A).
  End AccountError.
  Definition AccountError : Set := AccountError.t.
  
  Module OffChainError.
    Inductive t : Set :=
    | Account (_ : ink_env.engine.off_chain.AccountError)
    | UninitializedBlocks
    | UninitializedExecutionContext
    | UnregisteredChainExtension.
  End OffChainError.
  Definition OffChainError : Set := OffChainError.t.
End off_chain.

Module call_data.
  Module CallData.
    Unset Primitive Projections.
    Record t : Set := {
      bytes : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_bytes : Notation.Dot "bytes" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End CallData.
  Definition CallData : Set := CallData.t.
End call_data.

Module CallData.
  Unset Primitive Projections.
  Record t : Set := {
    bytes : alloc.vec.Vec u8 alloc.vec.Vec.Default.A;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_bytes : Notation.Dot "bytes" := {
    Notation.dot '(Build_t x0) := x0;
  }.
  Global Instance Get_AF_bytes : Notation.DoubleColon t "bytes" := {
    Notation.double_colon '(Build_t x0) := x0;
  }.
End CallData.
Definition CallData : Set := CallData.t.

Module impls.
  Module TopicsBuilder.
    Unset Primitive Projections.
    Record t : Set := {
      topics
        :
        alloc.vec.Vec
          (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
          alloc.vec.Vec.Default.A;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_topics : Notation.Dot "topics" := {
      Notation.dot '(Build_t x0) := x0;
    }.
    Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
      Notation.double_colon '(Build_t x0) := x0;
    }.
  End TopicsBuilder.
  Definition TopicsBuilder : Set := TopicsBuilder.t.
End impls.

Module TopicsBuilder.
  Unset Primitive Projections.
  Record t : Set := {
    topics
      :
      alloc.vec.Vec
        (alloc.vec.Vec u8 alloc.vec.Vec.Default.A)
        alloc.vec.Vec.Default.A;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_topics : Notation.Dot "topics" := {
    Notation.dot '(Build_t x0) := x0;
  }.
  Global Instance Get_AF_topics : Notation.DoubleColon t "topics" := {
    Notation.double_colon '(Build_t x0) := x0;
  }.
End TopicsBuilder.
Definition TopicsBuilder : Set := TopicsBuilder.t.

Module EnvInstance.
  Unset Primitive Projections.
  Record t : Set := {
    engine : ink_engine.ext.Engine;
  }.
  Global Set Primitive Projections.
  
  Global Instance Get_engine : Notation.Dot "engine" := {
    Notation.dot '(Build_t x0) := x0;
  }.
  Global Instance Get_AF_engine : Notation.DoubleColon t "engine" := {
    Notation.double_colon '(Build_t x0) := x0;
  }.
End EnvInstance.
Definition EnvInstance : Set := EnvInstance.t.

Module OffChainError.
  Inductive t : Set :=
  | Account (_ : ink_env.engine.off_chain.AccountError)
  | UninitializedBlocks
  | UninitializedExecutionContext
  | UnregisteredChainExtension.
End OffChainError.
Definition OffChainError : Set := OffChainError.t.

Module AccountError.
  Inductive t : Set :=
  | Decoding (_ : parity_scale_codec.error.Error)
  | UnexpectedUserAccount
  | NoAccountForId (_ : alloc.vec.Vec u8 alloc.vec.Vec.Default.A).
End AccountError.
Definition AccountError : Set := AccountError.t.

Module HashOutput.
  Class Trait (Self : Set) `{ink_env.hash.private.Sealed.Trait Self} : Type := {
    Type_ : Set;
    _ : Sigma `(core.default.Default.Trait Type_), unit;
  }.
  
  Global Instance Method_Type_ `(Trait)
    : Notation.DoubleColonType Self "Type_" := {
    Notation.double_colon_type := Type_;
  }.
End HashOutput.

Module CryptoHash.
  Class Trait (Self : Set) `{ink_env.hash.HashOutput.Trait Self} : Type := {
    hash `{H' : State.Trait}
      :
      (ref (Slice u8)) ->
        (mut_ref (ink_env.hash.HashOutput.Type_ (Self := Self))) ->
        M (H := H') unit;
  }.
  
  Global Instance Method_hash `{H' : State.Trait} `(Trait)
    : Notation.Dot "hash" := {
    Notation.dot := hash;
  }.
End CryptoHash.

Module Sha2x256.
  Inductive t : Set :=
  .
End Sha2x256.
Definition Sha2x256 : Set := Sha2x256.t.

Module Keccak256.
  Inductive t : Set :=
  .
End Keccak256.
Definition Keccak256 : Set := Keccak256.t.

Module Blake2x256.
  Inductive t : Set :=
  .
End Blake2x256.
Definition Blake2x256 : Set := Blake2x256.t.

Module Blake2x128.
  Inductive t : Set :=
  .
End Blake2x128.
Definition Blake2x128 : Set := Blake2x128.t.

Module Wrap_private_1.
  Module private.
    Module Sealed.
      Unset Primitive Projections.
      Class Trait (Self : Set) : Type := {
      }.
      Global Set Primitive Projections.
    End Sealed.
  End private.
End Wrap_private_1.
Import Wrap_private_1.

Module Sealed.
  Unset Primitive Projections.
  Class Trait (Self : Set) : Type := {
  }.
  Global Set Primitive Projections.
End Sealed.

Module TopicsBuilderBackend.
  Class Trait (Self : Set) {E : Set} `{ink_env.types.Environment.Trait E} :
      Type := {
    Output : Set;
    expect `{H' : State.Trait} : (mut_ref Self) -> usize -> M (H := H') unit;
    push_topic
      `{H' : State.Trait}
      {T : Set}
      `{H'0 : parity_scale_codec.codec.Encode.Trait T}
      :
      (mut_ref Self) -> (ref T) -> M (H := H') unit;
    output `{H' : State.Trait} : Self -> M (H := H') Output;
  }.
  
  Global Instance Method_Output `(Trait)
    : Notation.DoubleColonType Self "Output" := {
    Notation.double_colon_type := Output;
  }.
  Global Instance Method_expect `{H' : State.Trait} `(Trait)
    : Notation.Dot "expect" := {
    Notation.dot := expect;
  }.
  Global Instance Method_push_topic `{H' : State.Trait} `(Trait)
    : Notation.Dot "push_topic" := {
    Notation.dot {T : Set} `{H'0 : parity_scale_codec.codec.Encode.Trait T}
      :=
      push_topic (T := T) (H'0 := H'0);
  }.
  Global Instance Method_output `{H' : State.Trait} `(Trait)
    : Notation.Dot "output" := {
    Notation.dot := output;
  }.
End TopicsBuilderBackend.


Module Wrap_state_2.
  Module state.
    Module Uninit.
      Inductive t : Set :=
      .
    End Uninit.
    Definition Uninit : Set := Uninit.t.
    
    Module HasRemainingTopics.
      Inductive t : Set :=
      .
    End HasRemainingTopics.
    Definition HasRemainingTopics : Set := HasRemainingTopics.t.
    
    Module NoRemainingTopics.
      Inductive t : Set :=
      .
    End NoRemainingTopics.
    Definition NoRemainingTopics : Set := NoRemainingTopics.t.
  End state.
End Wrap_state_2.
Import Wrap_state_2.

Module Uninit.
  Inductive t : Set :=
  .
End Uninit.
Definition Uninit : Set := Uninit.t.

Module HasRemainingTopics.
  Inductive t : Set :=
  .
End HasRemainingTopics.
Definition HasRemainingTopics : Set := HasRemainingTopics.t.

Module NoRemainingTopics.
  Inductive t : Set :=
  .
End NoRemainingTopics.
Definition NoRemainingTopics : Set := NoRemainingTopics.t.

Module SomeRemainingTopics.
  Class Trait (Self : Set) : Type := {
    Next : Set;
  }.
  
  Global Instance Method_Next `(Trait)
    : Notation.DoubleColonType Self "Next" := {
    Notation.double_colon_type := Next;
  }.
End SomeRemainingTopics.

Module EventTopicsAmount.
  Class Trait (Self : Set) : Type := {
    AMOUNT `{H' : State.Trait} : usize;
  }.
  
  Global Instance Method_AMOUNT `{H' : State.Trait} `(Trait)
    : Notation.Dot "AMOUNT" := {
    Notation.dot := AMOUNT;
  }.
End EventTopicsAmount.

Module Topics.
  Class Trait (Self : Set) : Type := {
    RemainingTopics : Set;
    _ : Sigma `(ink_env.topics.EventTopicsAmount.Trait RemainingTopics), unit;
    topics
      `{H' : State.Trait}
      {E B : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : ink_env.topics.TopicsBuilderBackend.Trait B (E := E)}
      :
      (ref Self) ->
        (ink_env.topics.TopicsBuilder ink_env.topics.state.Uninit E B) ->
        M (H := H') (ink_env.topics.TopicsBuilderBackend.Output (Self := B));
  }.
  
  Global Instance Method_RemainingTopics `(Trait)
    : Notation.DoubleColonType Self "RemainingTopics" := {
    Notation.double_colon_type := RemainingTopics;
  }.
  Global Instance Method_topics `{H' : State.Trait} `(Trait)
    : Notation.Dot "topics" := {
    Notation.dot
      {E B : Set}
      `{H'0 : ink_env.types.Environment.Trait E}
      `{H'1 : ink_env.topics.TopicsBuilderBackend.Trait B (E := E)}
      :=
      topics (E := E) (B := B) (H'0 := H'0) (H'1 := H'1);
  }.
End Topics.

Module PrefixedValue.
  Section PrefixedValue.
    Context {T : Set}.
    Unset Primitive Projections.
    Record t : Set := {
      prefix : ref (Slice u8);
      value : ref T;
    }.
    Global Set Primitive Projections.
    
    Global Instance Get_prefix : Notation.Dot "prefix" := {
      Notation.dot '(Build_t x0 _) := x0;
    }.
    Global Instance Get_AF_prefix : Notation.DoubleColon t "prefix" := {
      Notation.double_colon '(Build_t x0 _) := x0;
    }.
    Global Instance Get_value : Notation.Dot "value" := {
      Notation.dot '(Build_t _ x1) := x1;
    }.
    Global Instance Get_AF_value : Notation.DoubleColon t "value" := {
      Notation.double_colon '(Build_t _ x1) := x1;
    }.
  End PrefixedValue.
End PrefixedValue.
Definition PrefixedValue (T : Set) : Set := PrefixedValue.t (T := T).