diff --git a/CoqOfRust/examples/default/examples/ink_contracts/proofs/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/proofs/constants.v
new file mode 100644
index 000000000..73c3a6d14
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/proofs/constants.v
@@ -0,0 +1,12 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.proofs.M.
+Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.lib.proofs.lib.
+Require CoqOfRust.core.proofs.option.
+Require CoqOfRust.examples.default.examples.ink_contracts.proofs.lib.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.constants.
+(* TODO: Refer to real translated code *)
+(* Require CoqOfRust.examples.default.examples.ink_contracts.constants. *)
+
+Import simulations.M.Notations.
+Import Run.
diff --git a/CoqOfRust/examples/default/examples/ink_contracts/proofs/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/proofs/traits.v
new file mode 100644
index 000000000..3ec911064
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/proofs/traits.v
@@ -0,0 +1,11 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.proofs.M.
+Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.lib.proofs.lib.
+Require CoqOfRust.core.proofs.option.
+Require CoqOfRust.examples.default.examples.ink_contracts.proofs.lib.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.traits.
+Require CoqOfRust.examples.default.examples.ink_contracts.erc20.
+
+Import simulations.M.Notations.
+Import Run.
\ No newline at end of file
diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
new file mode 100644
index 000000000..21d785ae8
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
@@ -0,0 +1,221 @@
+Require Import CoqOfRust.CoqOfRust.
+Require CoqOfRust.core.simulations.default.
+Require Import CoqOfRust.core.simulations.option.
+Require Import CoqOfRust.core.simulations.bool.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+Require Import CoqOfRust.simulations.M.
+
+(* TODO:
+- Check the Mapping structure in erc1155
+
+*)
+
+(* ******** Primitives ******** *)
+
+(* 
+struct AccountId(u128);
+*)
+Module AccountId.
+  Inductive t : Set :=
+  | Make (account_id : Z).
+
+  Global Instance IsToValue : ToValue t := {
+    Φ := Ty.path "erc1155::AccountId";
+    φ '(Make account_id) :=
+      Value.StructTuple "erc1155::AccountId" [Value.Integer Integer.U128 account_id];
+  }.
+End AccountId.
+
+(* type Balance = u128; *)
+Module Balance.
+  Inductive t : Set :=
+  | Make (balance : Z).
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "erc1155::Balance";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ '(Make balance) :=
+      Value.StructTuple "erc1155::Balance" [Value.Integer Integer.U128 balance];
+  }.
+End Balance.
+
+(* 
+struct Env {
+    caller: AccountId,
+}
+*)
+
+Module Env.
+  Record t : Set := {
+    caller : AccountId.t;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "erc1155::Env";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ '(Make x) :=
+      Value.StructTuple "erc1155::Env" φ x;
+  }.
+End Env.
+
+(* ******** IN PROGRESS ******** *)
+
+(* 
+fn zero_address() -> AccountId {
+    [0u8; 32].into()
+}
+*)
+
+(* 
+const ON_ERC_1155_RECEIVED_SELECTOR: [u8; 4] = [0xF2, 0x3A, 0x6E, 0x61];
+*)
+
+(* 
+const _ON_ERC_1155_BATCH_RECEIVED_SELECTOR: [u8; 4] = [0xBC, 0x19, 0x7C, 0x81];
+*)
+
+(* pub type TokenId = u128; *)
+Module TokenId.
+  Inductive t : Set :=
+  | Make (token_id : Z).
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "erc1155::TokenId";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ '(Make token_id) :=
+      Value.StructTuple "erc1155::TokenId" [Value.Integer Integer.U128 token_id];
+  }.
+End TokenId. 
+
+(* 
+// The ERC-1155 error types.
+#[derive(PartialEq, Eq)]
+pub enum Error {
+    /// This token ID has not yet been created by the contract.
+    UnexistentToken,
+    /// The caller tried to sending tokens to the zero-address (`0x00`).
+    ZeroAddressTransfer,
+    /// The caller is not approved to transfer tokens on behalf of the account.
+    NotApproved,
+    /// The account does not have enough funds to complete the transfer.
+    InsufficientBalance,
+    /// An account does not need to approve themselves to transfer tokens.
+    SelfApproval,
+    /// The number of tokens being transferred does not match the specified number of
+    /// transfers.
+    BatchTransferMismatch,
+}
+*)
+Module Error.
+  Inductive t : Set :=
+  | UnexistentToken
+  | ZeroAddressTransfer
+  | NotApproved
+  | InsufficientBalance
+  | SelfApproval
+  | BatchTransferMismatch.
+
+  (* TODO: finish the ToValue here? *)
+End Error.
+
+(* pub type Result<T> = core::result::Result<T, Error>; *)
+Module Result.
+  (* TODO: Check if this is the right way to use the Result *)
+  Definition t (T : Set) : Set := core.result.Result T Error.
+End Result.
+
+(* pub trait Erc1155 { .. }*)
+Module Erc1155.
+  Class Trait (Self : Set) : Set := {
+  (* 
+    fn safe_transfer_from(
+        &mut self,
+        from: AccountId,
+        to: AccountId,
+        token_id: TokenId,
+        value: Balance,
+        data: Vec<u8>,
+    ) -> Result<()>;
+  *)
+
+  (* fn safe_batch_transfer_from(
+      &mut self,
+      from: AccountId,
+      to: AccountId,
+      token_ids: Vec<TokenId>,
+      values: Vec<Balance>,
+      data: Vec<u8>,
+  ) -> Result<()>; *)
+
+  (* fn balance_of(&self, owner: AccountId, token_id: TokenId) -> Balance; *)
+
+  (* fn balance_of_batch(&self, owners: Vec<AccountId>, token_ids: Vec<TokenId>) -> Vec<Balance>; *)
+
+  (* fn set_approval_for_all(&mut self, operator: AccountId, approved: bool) -> Result<()>; *)
+  
+  (* fn is_approved_for_all(&self, owner: AccountId, operator: AccountId) -> bool; *)
+
+  }.
+End Erc1155.
+
+(* pub trait Erc1155TokenReceiver { .. } *)
+Module Erc1155TokenReceiver.
+  Class Trait (Self : Set) : Set := { 
+  (* fn on_received(
+      &mut self,
+      operator: AccountId,
+      from: AccountId,
+      token_id: TokenId,
+      value: Balance,
+      data: Vec<u8>,
+  ) -> Vec<u8>; *)
+
+  (* fn on_batch_received(
+      &mut self,
+      operator: AccountId,
+      from: AccountId,
+      token_ids: Vec<TokenId>,
+      values: Vec<Balance>,
+      data: Vec<u8>,
+  ) -> Vec<u8>; *)
+  }.
+End Erc1155TokenReceiver.
+
+(* type Owner = AccountId;
+type Operator = AccountId; *)
+
+(* pub struct TransferSingle {
+    operator: Option<AccountId>,
+    from: Option<AccountId>,
+    to: Option<AccountId>,
+    token_id: TokenId,
+    value: Balance,
+} *)
+Module TransferSingle.
+  Record t : Set := {
+
+  }.
+End TransferSingle.
+
+(* pub struct ApprovalForAll {
+    owner: AccountId,
+    operator: AccountId,
+    approved: bool,
+}
+
+pub struct Uri {
+    value: String,
+    token_id: TokenId,
+}
+
+enum Event {
+    TransferSingle(TransferSingle),
+    ApprovalForAll(ApprovalForAll),
+    Uri(Uri),
+} *)
diff --git a/CoqOfRust/examples/default/examples/simulations/constants.v b/CoqOfRust/examples/default/examples/simulations/constants.v
new file mode 100644
index 000000000..dbac65e60
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/simulations/constants.v
@@ -0,0 +1,33 @@
+(* custom_type/constants.v *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.simulations.M.
+Import simulations.M.Notations.
+
+(*
+static LANGUAGE: &str = "Rust";
+const THRESHOLD: i32 = 10;
+*)
+Definition LANGUAGE : string :=  "Rust".
+Definition THRESHOLD : Z := 10.
+
+(* 
+fn is_big(n: i32) -> bool {
+    // Access constant in some function
+    n > THRESHOLD
+}
+*)
+
+Definition is_big 
+  (n: Z) : bool := 
+  let get_n := n in
+  let get_THRESHOLD := THRESHOLD in
+  get_n >? get_THRESHOLD.
+
+(*
+fn main() {
+    let n = 16;
+} *)
+
+Definition main : unit :=
+  let n := 16 in
+  tt.
diff --git a/CoqOfRust/examples/default/examples/simulations/traits.v b/CoqOfRust/examples/default/examples/simulations/traits.v
new file mode 100644
index 000000000..4b9c48ea2
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/simulations/traits.v
@@ -0,0 +1,190 @@
+(* traits/traits.rs *)
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.core.simulations.bool.
+Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.proofs.M.
+Import simulations.M.Notations.
+Import simulations.bool.Notations.
+
+(* struct Sheep {
+  naked: bool,
+  name: &'static str,
+} *)
+Module Sheep.
+  Record t : Set := {
+    naked: bool;
+    name: string;
+  }.
+
+  Global Instance IsToTy : ToTy t := {
+    Φ := Ty.path "traits::Sheep";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    φ x :=
+      Value.StructRecord "traits::Sheep" [
+        ("naked", Value.Bool x.(naked));
+        ("name", Value.String x.(name))
+      ];
+  }.
+End Sheep.
+
+(* ** Simulation of functions ** *)
+(* 
+fn new(name: &'static str) -> Sheep {
+  Sheep {
+      name: name,
+      naked: false,
+  }
+} *)
+Definition new (name: string) : traits.Sheep.t := 
+  {| Sheep.naked := false;
+    Sheep.name := name;
+  |}.
+
+(*   
+fn name(&self) -> &'static str {
+  self.name
+}
+*)
+Definition name (self: traits.Sheep.t) : string := 
+  self.(Sheep.name).
+
+(*
+impl Sheep {
+  fn is_naked(&self) -> bool {
+      self.naked
+  }
+}
+*)
+Definition is_naked (self: traits.Sheep.t) : bool :=
+  self.(Sheep.naked).
+
+(* 
+fn noise(&self) -> &'static str {
+    if self.is_naked() {
+        "baaaaah?"
+    } else {
+        "baaaaah!"
+    }
+} *)
+Definition noise (self: traits.Sheep.t) : string := 
+  if (is_naked self) then "baaaaah?" else "baaaaah!".
+
+(* fn talk(&self) {
+    // For example, we can add some quiet contemplation.
+    println!("{} pauses briefly... {}", self.name, self.noise());
+} *)
+Definition talk (self: traits.Sheep.t): unit := tt.
+
+(* ** Simulation of function that modifies a variable ** *)
+
+Module State.
+  Definition t : Set := traits.Sheep.t.
+End State.
+
+(*
+impl Sheep {
+  fn shear(&mut self) {
+      if self.is_naked() {
+          // Implementor methods can use the implementor's trait methods.
+          println!("{} is already naked...", self.name());
+      } else {
+          println!("{} gets a haircut!", self.name);
+
+          self.naked = true;
+      }
+  }
+}
+*)
+Definition shear (self: traits.Sheep.t) : MS? State.t string unit := 
+  letS? storage := readS? in
+  if is_naked(self) then (returnS? tt) else 
+  letS? _ := writeS? (
+    storage <| traits.Sheep.naked := true |>
+  )
+  in
+  returnS? tt.
+
+(* ToTy Instances *)
+
+Global Instance IsToTy_string : ToTy string. Admitted.
+Global Instance IsToTy_string_self {Self : Set} : ToTy (string -> Self). Admitted.
+Global Instance IsToTy_self_string {Self : Set} : ToTy (Self -> string). Admitted.
+Global Instance IsToTy_self_unit {Self : Set} : ToTy (Self -> unit). Admitted.
+
+(* Missing ToValue instances to define TraitHasRun *)
+Global Instance IsToValue_string : ToValue string. Admitted.
+Global Instance IsToValue_string_self {Self : Set} : ToValue (string -> Self). Admitted.
+Global Instance IsToValue_self_string {Self : Set} : ToValue (Self -> string). Admitted.
+Global Instance IsToValue_self_unit {Self : Set} : ToValue (Self -> unit). Admitted.
+
+(*
+trait Animal {
+  // Associated function signature; `Self` refers to the implementor type.
+  fn new(name: &'static str) -> Self;
+
+  // Method signatures; these will return a string.
+  fn name(&self) -> &'static str;
+  fn noise(&self) -> &'static str;
+
+  // Traits can provide default method definitions.
+  fn talk(&self) {
+      println!("{} says {}", self.name(), self.noise());
+  }
+}
+*)
+
+Module Animal.
+  Class Trait (Self : Set) : Set := {
+    new (name: string) : Self;
+    name (self: Self) : string;
+    noise (self: Self) : string;
+    talk (self: Self) : unit;
+  }.
+
+  Record InstanceWithRun (Self : Set)
+    `{ToValue Self}
+    `{ToTy Self}
+    `{traits.Animal.Trait Self} : Set := {
+      new_exists : {new @ 
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [] "new" new
+        *
+        Run.pure (new [] []) (fun v => inl (φ v))
+      };
+      name_exists : {name @
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "name" name 
+        *
+        Run.pure (name [] []) (fun v => inl (φ v))
+      };
+      noise_exists : {noise @
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "noise" noise 
+        *
+        Run.pure (noise [] []) (fun v => inl (φ v))
+      };
+      talk_exists : {talk @
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 
+        *
+        Run.pure (talk [] []) (fun v => inl (φ v))
+      };
+    }.
+End Animal.
+
+(*
+fn main() {
+  // Type annotation is necessary in this case.
+  let mut dolly: Sheep = Animal::new("Dolly");
+  // TODO ^ Try removing the type annotations.
+
+  dolly.talk();
+  dolly.shear();
+  dolly.talk();
+} *)
+
+Definition main : 
+  MS? State.t string unit := 
+  let dolly := new "Dolly" in
+  let _ := talk dolly in
+  let _ := shear dolly in
+  let _ := talk dolly in
+  returnS? tt.