From 4aa17bfb835a3c791299f9fa2c3553010bfc88b9 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 25 Apr 2024 14:17:23 +0800
Subject: [PATCH 01/32] Experimental translation for CI test

---
 .../ink_contracts/simulations/constants.v     | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
new file mode 100644
index 000000000..f17c9b08f
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -0,0 +1,36 @@
+(* custom_type/constants.v *)
+Require Import CoqOfRust.CoqOfRust.
+Require CoqOfRust.core.simulations.default.
+Require Import CoqOfRust.core.simulations.option.
+Require Import CoqOfRust.core.simulations.integer.
+Require Import CoqOfRust.core.simulations.bool.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+Require Import CoqOfRust.simulations.M.
+
+(*
+static LANGUAGE: &str = "Rust";
+const THRESHOLD: i32 = 10;
+*)
+
+Definition LANGUAGE := mk_str "Rust".
+Definition THRESHOLD := i32.Make 10.
+
+(* 
+fn is_big(n: i32) -> bool {
+    // Access constant in some function
+    n > THRESHOLD
+}
+*)
+
+Definition is_big 
+  (n: Nat) : bool := n >? THRESHOLD.
+
+(*
+fn main() {
+    let n = 16;
+} *)
+
+Definition main : Unit :=
+  let n := i32.Make 16 in
+  (* pure Value.DeclaredButUndefined *)
+  ().
\ No newline at end of file

From fefd563ac2480e483b45480b4bfd22e91c61efb6 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 07:45:49 +0800
Subject: [PATCH 02/32] Add traits.v

---
 .../ink_contracts/simulations/traits.v        | 140 ++++++++++++++++++
 1 file changed, 140 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
new file mode 100644
index 000000000..e43219462
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -0,0 +1,140 @@
+(* traits/traits.rs *)
+(* struct Sheep {
+  naked: bool,
+  name: &'static str,
+} *)
+
+(* TODO: Apply definition of Pointer.t
+  Inductive t (Value : Set) : Set :=
+  | Immediate (value : Value)
+  | Mutable {Address : Set} (address : Address) (path : Path.t).
+*)
+
+Module Sheep.
+  Record t : Set := {
+    naked: bool,
+    name: Pointer.t string,
+  }.
+
+  Global Instance IsToValue : ToValue t := {
+    Φ := Ty.path "traits::Sheep";
+    φ x :=
+      Value.StructRecord "traits::Sheep" [
+        ("naked", φ x.(naked));
+        ("name", φ x.(name));
+      ];
+  }.
+
+      (* 
+    fn new(name: &'static str) -> Sheep {
+      Sheep {
+          name: name,
+          naked: false,
+      }
+    } *)
+    (* TODO: Is this the correct way to construct record in Coq? *)
+    Definition new (name: Pointer.t string) : MS? traits.Sheep.t := 
+    returnS? {| name := name;
+      naked := false
+      |}.
+
+    (*   
+    fn name(&self) -> &'static str {
+      self.name
+    }
+    *)
+    Definition name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t ) := returnS? (Pointer.t.Immediate (Value.t.String self.name)).
+    (* 
+    fn noise(&self) -> &'static str {
+        if self.is_naked() {
+            "baaaaah?"
+        } else {
+            "baaaaah!"
+        }
+    } *)
+    Definition noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str) := returnS? (if is_naked(self) then "baaaaah?" else "baaaaah!").
+
+    (* NOTE: unimplemented since it involves println *)
+    (* fn talk(&self) {
+        // For example, we can add some quiet contemplation.
+        println!("{} pauses briefly... {}", self.name, self.noise());
+    } *)
+    Definition talk (self: Pointer.t traits.Sheep.t): MS? unit := returnS? tt.
+    
+    (*
+    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;
+          }
+      }
+    }
+    *)
+    (* 
+    TODO: apply RecordUpdate to simulate the update of the variable?
+    *)
+    Definition shear (self: traits.Sheep.t) : MS? State unit := 
+      if is_naked(self) then tt else tt.
+End Sheep.
+
+(*
+impl Sheep {
+  fn is_naked(&self) -> bool {
+      self.naked
+  }
+}
+*)
+Definition is_naked (self: traits.Sheep.t) : bool :=
+  self.naked.
+
+(*
+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: str) : traits.Sheep.t; 
+    name (self: traits.Sheep.t) : str;
+    noise (self: traits.Sheep.t) : str;
+    talk : unit;
+  }.
+
+  (* TODO: Add the IsTrait method here? *)
+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 unit := 
+  (* Is this notation still in use? *)
+  let dolly := traits.Animal::["new"] "Dolly" in
+  let _ := dolly::["talk"] in
+  let _ := dolly::["shear"] in
+  let _ := dolly::["talk"] in
+  returnS? tt.
\ No newline at end of file

From 895a12eb17296dcc200b8fbf9940e5f5bd07701a Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 10:34:38 +0800
Subject: [PATCH 03/32] Update `traits.v`

---
 .../ink_contracts/simulations/traits.v        | 45 ++++++++++---------
 1 file changed, 25 insertions(+), 20 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index e43219462..d8b2a6e77 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -13,7 +13,7 @@
 Module Sheep.
   Record t : Set := {
     naked: bool,
-    name: Pointer.t string,
+    name: Pointer.t.Immediate string,
   }.
 
   Global Instance IsToValue : ToValue t := {
@@ -26,24 +26,26 @@ Module Sheep.
   }.
 
       (* 
-    fn new(name: &'static str) -> Sheep {
-      Sheep {
-          name: name,
-          naked: false,
-      }
-    } *)
-    (* TODO: Is this the correct way to construct record in Coq? *)
+      fn new(name: &'static str) -> Sheep {
+        Sheep {
+            name: name,
+            naked: false,
+        }
+      } *)
+    (* NOTE: Is this the correct way to construct record in Coq? *)
     Definition new (name: Pointer.t string) : MS? traits.Sheep.t := 
-    returnS? {| name := name;
-      naked := false
+      returnS? {| naked := false;
+        name := Pointer.t.Immediate (Value.t.String name);
       |}.
 
     (*   
-    fn name(&self) -> &'static str {
-      self.name
-    }
+      fn name(&self) -> &'static str {
+        self.name
+      }
     *)
-    Definition name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t ) := returnS? (Pointer.t.Immediate (Value.t.String self.name)).
+    (* NOTE: How to extract record entries from a record that is wrapped in Pointer.t type? *)
+    Definition name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t ) := 
+      returnS? (Pointer.t.Immediate (Value.t.String self.name)).
     (* 
     fn noise(&self) -> &'static str {
         if self.is_naked() {
@@ -52,7 +54,8 @@ Module Sheep.
             "baaaaah!"
         }
     } *)
-    Definition noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str) := returnS? (if is_naked(self) then "baaaaah?" else "baaaaah!").
+    Definition noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str) := 
+      returnS? (Pointer.t.Immediate (Value.t.String (if is_naked(self) then "baaaaah?" else "baaaaah!"))).
 
     (* NOTE: unimplemented since it involves println *)
     (* fn talk(&self) {
@@ -79,7 +82,9 @@ Module Sheep.
     TODO: apply RecordUpdate to simulate the update of the variable?
     *)
     Definition shear (self: traits.Sheep.t) : MS? State unit := 
-      if is_naked(self) then tt else tt.
+      returnS? (if is_naked(self) then tt else tt).
+
+    (* TODO: Make a `IsOfTrait` or something to indicate that Sheep is of Animal trait *)
 End Sheep.
 
 (*
@@ -110,10 +115,10 @@ trait Animal {
 
 Module Animal.
   Class Trait (Self : Set) : Set := {
-    new (name: str) : traits.Sheep.t; 
-    name (self: traits.Sheep.t) : str;
-    noise (self: traits.Sheep.t) : str;
-    talk : unit;
+    new (name: Pointer.t str) : MS? traits.Sheep.t; 
+    name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str);
+    noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str);
+    talk (self: Pointer.t traits.Sheep.t) : MS? unit;
   }.
 
   (* TODO: Add the IsTrait method here? *)

From 377ef39aa35754476b58d5dde7fd33e3c72e9683 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 13:38:16 +0800
Subject: [PATCH 04/32] Update `traits.v`

---
 .../ink_contracts/simulations/traits.v        | 157 +++++++++---------
 1 file changed, 83 insertions(+), 74 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index d8b2a6e77..d4eee9d2e 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,15 +1,19 @@
 (* traits/traits.rs *)
+
+(* Questions:
+1. Should I translate reference types to Pointer types? It looks like it adds a lot of complexity
+*)
+
+(* TODO:
+1. Distinguish between functions that read the variables and functions that also writes to it
+2. Identify the way to translate them
+
+*)
+
 (* struct Sheep {
   naked: bool,
   name: &'static str,
 } *)
-
-(* TODO: Apply definition of Pointer.t
-  Inductive t (Value : Set) : Set :=
-  | Immediate (value : Value)
-  | Mutable {Address : Set} (address : Address) (path : Path.t).
-*)
-
 Module Sheep.
   Record t : Set := {
     naked: bool,
@@ -24,68 +28,47 @@ Module Sheep.
         ("name", φ x.(name));
       ];
   }.
+End Sheep.
 
-      (* 
-      fn new(name: &'static str) -> Sheep {
-        Sheep {
-            name: name,
-            naked: false,
-        }
-      } *)
-    (* NOTE: Is this the correct way to construct record in Coq? *)
-    Definition new (name: Pointer.t string) : MS? traits.Sheep.t := 
-      returnS? {| naked := false;
-        name := Pointer.t.Immediate (Value.t.String name);
-      |}.
-
-    (*   
-      fn name(&self) -> &'static str {
-        self.name
-      }
-    *)
-    (* NOTE: How to extract record entries from a record that is wrapped in Pointer.t type? *)
-    Definition name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t ) := 
-      returnS? (Pointer.t.Immediate (Value.t.String self.name)).
-    (* 
-    fn noise(&self) -> &'static str {
-        if self.is_naked() {
-            "baaaaah?"
-        } else {
-            "baaaaah!"
-        }
-    } *)
-    Definition noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str) := 
-      returnS? (Pointer.t.Immediate (Value.t.String (if is_naked(self) then "baaaaah?" else "baaaaah!"))).
-
-    (* NOTE: unimplemented since it involves println *)
-    (* fn talk(&self) {
-        // For example, we can add some quiet contemplation.
-        println!("{} pauses briefly... {}", self.name, self.noise());
-    } *)
-    Definition talk (self: Pointer.t traits.Sheep.t): MS? unit := returnS? tt.
-    
-    (*
-    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;
-          }
-      }
+(*  ** Simulation of functions ** *)
+(* 
+fn new(name: &'static str) -> Sheep {
+  Sheep {
+      name: name,
+      naked: false,
+  }
+} *)
+(* NOTE: Is this the correct way to construct record in Coq? *)
+Definition new (name: String) : traits.Sheep.t := 
+  {| naked := false;
+    name := name;
+  |}.
+
+(*   
+fn name(&self) -> &'static str {
+  self.name
+}
+*)
+Definition name (self: traits.Sheep.t) : String := 
+  self.name.
+
+(* 
+fn noise(&self) -> &'static str {
+    if self.is_naked() {
+        "baaaaah?"
+    } else {
+        "baaaaah!"
     }
-    *)
-    (* 
-    TODO: apply RecordUpdate to simulate the update of the variable?
-    *)
-    Definition shear (self: traits.Sheep.t) : MS? State unit := 
-      returnS? (if is_naked(self) then tt else tt).
-
-    (* TODO: Make a `IsOfTrait` or something to indicate that Sheep is of Animal trait *)
-End Sheep.
+} *)
+Definition noise (self: traits.Sheep.t) : String := 
+  if is_naked(self) then "baaaaah?" else "baaaaah!".
+
+(* NOTE: unimplemented since it involves println *)
+(* 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.
 
 (*
 impl Sheep {
@@ -97,6 +80,31 @@ impl Sheep {
 Definition is_naked (self: traits.Sheep.t) : bool :=
   self.naked.
 
+(* Simulation of a 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;
+      }
+  }
+}
+*)
+(* TODO: Finish this function *)
+Definition shear (self: traits.Sheep.t) : unit := 
+  letS? '(storage) := readS? in
+  if is_naked(self) then tt else tt.
+
 (*
 trait Animal {
   // Associated function signature; `Self` refers to the implementor type.
@@ -115,13 +123,14 @@ trait Animal {
 
 Module Animal.
   Class Trait (Self : Set) : Set := {
-    new (name: Pointer.t str) : MS? traits.Sheep.t; 
-    name (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str);
-    noise (self: Pointer.t traits.Sheep.t) : MS? (Pointer.t str);
-    talk (self: Pointer.t traits.Sheep.t) : MS? unit;
+    new (name: String) : traits.Sheep.t; 
+    name (self: traits.Sheep.t) : String;
+    noise (self: traits.Sheep.t) : String;
+    talk (self: traits.Sheep.t) : unit;
   }.
 
-  (* TODO: Add the IsTrait method here? *)
+  (* TODO: Define the `TraitHasRun` struct to express that `Sheep` implements `Animal` *)
+
 End Animal.
 
 (*
@@ -138,8 +147,8 @@ fn main() {
 Definition main : 
   MS? State.t unit := 
   (* Is this notation still in use? *)
-  let dolly := traits.Animal::["new"] "Dolly" in
+  (* let dolly := traits.Animal::["new"] "Dolly" in
   let _ := dolly::["talk"] in
   let _ := dolly::["shear"] in
-  let _ := dolly::["talk"] in
+  let _ := dolly::["talk"] in *)
   returnS? tt.
\ No newline at end of file

From bb472dae3be0aa35e913dfb139d5fa5524ecbeef Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 13:51:31 +0800
Subject: [PATCH 05/32] Update `traits.v`: Finished function definitions

---
 .../ink_contracts/simulations/traits.v        | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index d4eee9d2e..64935049c 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,9 +1,5 @@
 (* traits/traits.rs *)
 
-(* Questions:
-1. Should I translate reference types to Pointer types? It looks like it adds a lot of complexity
-*)
-
 (* TODO:
 1. Distinguish between functions that read the variables and functions that also writes to it
 2. Identify the way to translate them
@@ -39,8 +35,8 @@ fn new(name: &'static str) -> Sheep {
   }
 } *)
 (* NOTE: Is this the correct way to construct record in Coq? *)
-Definition new (name: String) : traits.Sheep.t := 
-  {| naked := false;
+Definition new (name: string) : traits.Sheep.t := 
+  traits.Animal {| naked := false;
     name := name;
   |}.
 
@@ -49,7 +45,7 @@ fn name(&self) -> &'static str {
   self.name
 }
 *)
-Definition name (self: traits.Sheep.t) : String := 
+Definition name (self: traits.Sheep.t) : string := 
   self.name.
 
 (* 
@@ -60,7 +56,7 @@ fn noise(&self) -> &'static str {
         "baaaaah!"
     }
 } *)
-Definition noise (self: traits.Sheep.t) : String := 
+Definition noise (self: traits.Sheep.t) : string := 
   if is_naked(self) then "baaaaah?" else "baaaaah!".
 
 (* NOTE: unimplemented since it involves println *)
@@ -100,10 +96,14 @@ impl Sheep {
   }
 }
 *)
-(* TODO: Finish this function *)
-Definition shear (self: traits.Sheep.t) : unit := 
+Definition shear (self: traits.Sheep.t) : MS? unit := 
   letS? '(storage) := readS? in
-  if is_naked(self) then tt else tt.
+  if is_naked(self) then tt else 
+  letS? _ = writeS? (
+    storage <| traits.Animal.naked := true |>,
+  )
+  in
+  returnS? tt.
 
 (*
 trait Animal {
@@ -123,9 +123,9 @@ trait Animal {
 
 Module Animal.
   Class Trait (Self : Set) : Set := {
-    new (name: String) : traits.Sheep.t; 
-    name (self: traits.Sheep.t) : String;
-    noise (self: traits.Sheep.t) : String;
+    new (name: string) : traits.Sheep.t; 
+    name (self: traits.Sheep.t) : string;
+    noise (self: traits.Sheep.t) : string;
     talk (self: traits.Sheep.t) : unit;
   }.
 

From bc1369076bf6c442003feb99c83d9076549d7191 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 13:52:00 +0800
Subject: [PATCH 06/32] `traits.v`: Remove comments

---
 .../default/examples/ink_contracts/simulations/traits.v     | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 64935049c..5bd1d6004 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,11 +1,5 @@
 (* traits/traits.rs *)
 
-(* TODO:
-1. Distinguish between functions that read the variables and functions that also writes to it
-2. Identify the way to translate them
-
-*)
-
 (* struct Sheep {
   naked: bool,
   name: &'static str,

From 287f430598012597604cc9f99fb37fc9ef8f3cd1 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 13:55:00 +0800
Subject: [PATCH 07/32] Minor fixes

---
 .../default/examples/ink_contracts/simulations/traits.v       | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 5bd1d6004..3bea634d6 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -7,7 +7,7 @@
 Module Sheep.
   Record t : Set := {
     naked: bool,
-    name: Pointer.t.Immediate string,
+    name: string,
   }.
 
   Global Instance IsToValue : ToValue t := {
@@ -140,7 +140,7 @@ fn main() {
 
 Definition main : 
   MS? State.t unit := 
-  (* Is this notation still in use? *)
+  (* NOTE: Is this notation still in use? *)
   (* let dolly := traits.Animal::["new"] "Dolly" in
   let _ := dolly::["talk"] in
   let _ := dolly::["shear"] in

From 5c83ccd73d92a614664601e1379e2e4100ac89d9 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 14:09:14 +0800
Subject: [PATCH 08/32] Update `traits.v`

---
 .../default/examples/ink_contracts/simulations/traits.v     | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 3bea634d6..5bd8b8908 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -140,7 +140,11 @@ fn main() {
 
 Definition main : 
   MS? State.t unit := 
-  (* NOTE: Is this notation still in use? *)
+  let dolly := new("Dolly") in
+  let _ = talk(dolly) in
+  let _ = shear(dolly) in
+  let _ = talk(dolly) in
+  (* NOTE: Is the following notation still in use? *)
   (* let dolly := traits.Animal::["new"] "Dolly" in
   let _ := dolly::["talk"] in
   let _ := dolly::["shear"] in

From 6ed6eee2568259d1c158c56c244ddd1c07c61d01 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 14:10:59 +0800
Subject: [PATCH 09/32] Update `traits.v`

---
 .../default/examples/ink_contracts/simulations/traits.v      | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 5bd8b8908..dc8640d17 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,5 +1,10 @@
 (* traits/traits.rs *)
 
+(* TODO:
+1. Check (if it's necessary) how to implement `TraitHasRun` for `Animal` and `Sheep`
+2. Check if the `main` function has defined correctly
+*)
+
 (* struct Sheep {
   naked: bool,
   name: &'static str,

From 8a94f10c05ab1aa2fec4978cdd45c2d47d4103c7 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 17:12:17 +0800
Subject: [PATCH 10/32] Update `traits.v` according to comments

---
 .../ink_contracts/simulations/traits.v        | 33 ++++++++++---------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index dc8640d17..c5b93a99c 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,4 +1,11 @@
 (* traits/traits.rs *)
+Require Import CoqOfRust.CoqOfRust.
+Require CoqOfRust.core.simulations.default.
+Require CoqOfRust.core.simulations.option.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+Require Import CoqOfRust.simulations.M.
+
+Import simulations.M.Notations.
 
 (* TODO:
 1. Check (if it's necessary) how to implement `TraitHasRun` for `Animal` and `Sheep`
@@ -35,8 +42,8 @@ fn new(name: &'static str) -> Sheep {
 } *)
 (* NOTE: Is this the correct way to construct record in Coq? *)
 Definition new (name: string) : traits.Sheep.t := 
-  traits.Animal {| naked := false;
-    name := name;
+  {| Sheep.naked := false;
+    Sheep.name := name;
   |}.
 
 (*   
@@ -45,7 +52,7 @@ fn name(&self) -> &'static str {
 }
 *)
 Definition name (self: traits.Sheep.t) : string := 
-  self.name.
+  self.Sheep.name.
 
 (* 
 fn noise(&self) -> &'static str {
@@ -58,7 +65,6 @@ fn noise(&self) -> &'static str {
 Definition noise (self: traits.Sheep.t) : string := 
   if is_naked(self) then "baaaaah?" else "baaaaah!".
 
-(* NOTE: unimplemented since it involves println *)
 (* fn talk(&self) {
     // For example, we can add some quiet contemplation.
     println!("{} pauses briefly... {}", self.name, self.noise());
@@ -73,9 +79,9 @@ impl Sheep {
 }
 *)
 Definition is_naked (self: traits.Sheep.t) : bool :=
-  self.naked.
+  self.Sheep.naked.
 
-(* Simulation of a function that modifies a variable *)
+(* ** Simulation of a function that modifies a variable ** *)
 
 Module State.
   Definition t : Set := traits.Sheep.t.
@@ -96,7 +102,7 @@ impl Sheep {
 }
 *)
 Definition shear (self: traits.Sheep.t) : MS? unit := 
-  letS? '(storage) := readS? in
+  letS? storage := readS? in
   if is_naked(self) then tt else 
   letS? _ = writeS? (
     storage <| traits.Animal.naked := true |>,
@@ -145,13 +151,8 @@ fn main() {
 
 Definition main : 
   MS? State.t unit := 
-  let dolly := new("Dolly") in
-  let _ = talk(dolly) in
-  let _ = shear(dolly) in
-  let _ = talk(dolly) in
-  (* NOTE: Is the following notation still in use? *)
-  (* let dolly := traits.Animal::["new"] "Dolly" in
-  let _ := dolly::["talk"] in
-  let _ := dolly::["shear"] in
-  let _ := dolly::["talk"] in *)
+  let dolly := new "Dolly" in
+  let _ = talk dolly in
+  let _ = shear dolly in
+  let _ = talk dolly in
   returnS? tt.
\ No newline at end of file

From 5cad99518b90f6615d5a32c80999121351d23d5a Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 17:14:02 +0800
Subject: [PATCH 11/32] Update `constants.v` according to comment

---
 .../ink_contracts/simulations/constants.v        | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
index f17c9b08f..f17675e1e 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -1,12 +1,12 @@
-(* custom_type/constants.v *)
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
-Require Import CoqOfRust.core.simulations.option.
-Require Import CoqOfRust.core.simulations.integer.
-Require Import CoqOfRust.core.simulations.bool.
+Require CoqOfRust.core.simulations.option.
 Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
 Require Import CoqOfRust.simulations.M.
 
+Import simulations.M.Notations.
+(* custom_type/constants.v *)
+
 (*
 static LANGUAGE: &str = "Rust";
 const THRESHOLD: i32 = 10;
@@ -22,15 +22,15 @@ fn is_big(n: i32) -> bool {
 }
 *)
 
+(* TODO: figure out how to compare i32 *)
 Definition is_big 
-  (n: Nat) : bool := n >? THRESHOLD.
+  (n: i32.t) : bool := n >? THRESHOLD.
 
 (*
 fn main() {
     let n = 16;
 } *)
 
-Definition main : Unit :=
+Definition main : MS? unit :=
   let n := i32.Make 16 in
-  (* pure Value.DeclaredButUndefined *)
-  ().
\ No newline at end of file
+  returnS? tt.
\ No newline at end of file

From 81fc18c75022fa1cfb6665ae3bb0fb85da0ab528 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 17:22:08 +0800
Subject: [PATCH 12/32] More minor fixes

---
 .../default/examples/ink_contracts/simulations/traits.v     | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index c5b93a99c..d8bd79b32 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -52,7 +52,7 @@ fn name(&self) -> &'static str {
 }
 *)
 Definition name (self: traits.Sheep.t) : string := 
-  self.Sheep.name.
+  self.(Sheep.name).
 
 (* 
 fn noise(&self) -> &'static str {
@@ -63,7 +63,7 @@ fn noise(&self) -> &'static str {
     }
 } *)
 Definition noise (self: traits.Sheep.t) : string := 
-  if is_naked(self) then "baaaaah?" else "baaaaah!".
+  if (is_naked self) then "baaaaah?" else "baaaaah!".
 
 (* fn talk(&self) {
     // For example, we can add some quiet contemplation.
@@ -79,7 +79,7 @@ impl Sheep {
 }
 *)
 Definition is_naked (self: traits.Sheep.t) : bool :=
-  self.Sheep.naked.
+  self.(Sheep.naked).
 
 (* ** Simulation of a function that modifies a variable ** *)
 

From 83ce23f185eb793037ccddc81807140a61b8a343 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Fri, 3 May 2024 17:23:31 +0800
Subject: [PATCH 13/32] More fixes according to comments

---
 .../default/examples/ink_contracts/simulations/constants.v    | 3 ++-
 .../default/examples/ink_contracts/simulations/traits.v       | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
index f17675e1e..43376a64f 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -33,4 +33,5 @@ fn main() {
 
 Definition main : MS? unit :=
   let n := i32.Make 16 in
-  returnS? tt.
\ No newline at end of file
+  returnS? tt.
+  
\ No newline at end of file
diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index d8bd79b32..a8d6e36fe 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -40,7 +40,6 @@ fn new(name: &'static str) -> Sheep {
       naked: false,
   }
 } *)
-(* NOTE: Is this the correct way to construct record in Coq? *)
 Definition new (name: string) : traits.Sheep.t := 
   {| Sheep.naked := false;
     Sheep.name := name;
@@ -155,4 +154,5 @@ Definition main :
   let _ = talk dolly in
   let _ = shear dolly in
   let _ = talk dolly in
-  returnS? tt.
\ No newline at end of file
+  returnS? tt.
+  
\ No newline at end of file

From f443776700a0e600ef3d6d86b0ff2b6e2a680bc2 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 17:21:54 +0800
Subject: [PATCH 14/32] Compiler-checked `constants.v`

---
 .../ink_contracts/simulations/constants.v       | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
index 43376a64f..4128b0aed 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -1,19 +1,19 @@
+(* custom_type/constants.v *)
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
 Require CoqOfRust.core.simulations.option.
 Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
 Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.lib.simulations.lib.
 
 Import simulations.M.Notations.
-(* custom_type/constants.v *)
 
 (*
 static LANGUAGE: &str = "Rust";
 const THRESHOLD: i32 = 10;
 *)
-
 Definition LANGUAGE := mk_str "Rust".
-Definition THRESHOLD := i32.Make 10.
+Definition THRESHOLD : i32.t := i32.Make 10.
 
 (* 
 fn is_big(n: i32) -> bool {
@@ -22,16 +22,17 @@ fn is_big(n: i32) -> bool {
 }
 *)
 
-(* TODO: figure out how to compare i32 *)
 Definition is_big 
-  (n: i32.t) : bool := n >? THRESHOLD.
+  (n: i32.t) : bool := 
+  let get_n := i32.get n in
+  let get_THRESHOLD := i32.get THRESHOLD in
+  get_n >? get_THRESHOLD.
 
 (*
 fn main() {
     let n = 16;
 } *)
 
-Definition main : MS? unit :=
+Definition main : unit :=
   let n := i32.Make 16 in
-  returnS? tt.
-  
\ No newline at end of file
+  tt.

From 555eac595eaf4facac968f3103017b18ac80605b Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 21:04:33 +0800
Subject: [PATCH 15/32] Compiler-passed `traits.v` with unfixed bug

---
 .../ink_contracts/simulations/traits.v        | 46 +++++++++----------
 1 file changed, 23 insertions(+), 23 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index a8d6e36fe..3f84b0616 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -18,16 +18,17 @@ Import simulations.M.Notations.
 } *)
 Module Sheep.
   Record t : Set := {
-    naked: bool,
-    name: string,
+    naked: bool;
+    name: string;
   }.
 
   Global Instance IsToValue : ToValue t := {
     Φ := Ty.path "traits::Sheep";
     φ x :=
       Value.StructRecord "traits::Sheep" [
-        ("naked", φ x.(naked));
-        ("name", φ x.(name));
+      (* TODO: figure out the correct way to fill this *)
+        (* ("naked", φ x.(naked));
+        ("name", φ x.(name)) *)
       ];
   }.
 End Sheep.
@@ -53,6 +54,16 @@ fn name(&self) -> &'static str {
 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() {
@@ -70,16 +81,6 @@ Definition noise (self: traits.Sheep.t) : string :=
 } *)
 Definition talk (self: traits.Sheep.t): unit := tt.
 
-(*
-impl Sheep {
-  fn is_naked(&self) -> bool {
-      self.naked
-  }
-}
-*)
-Definition is_naked (self: traits.Sheep.t) : bool :=
-  self.(Sheep.naked).
-
 (* ** Simulation of a function that modifies a variable ** *)
 
 Module State.
@@ -100,11 +101,11 @@ impl Sheep {
   }
 }
 *)
-Definition shear (self: traits.Sheep.t) : MS? unit := 
+Definition shear (self: traits.Sheep.t) : MS? State.t string unit := 
   letS? storage := readS? in
-  if is_naked(self) then tt else 
-  letS? _ = writeS? (
-    storage <| traits.Animal.naked := true |>,
+  if is_naked(self) then (returnS? tt) else 
+  letS? _ := writeS? (
+    storage <| traits.Sheep.naked := true |>
   )
   in
   returnS? tt.
@@ -149,10 +150,9 @@ fn main() {
 } *)
 
 Definition main : 
-  MS? State.t unit := 
+  MS? State.t string unit := 
   let dolly := new "Dolly" in
-  let _ = talk dolly in
-  let _ = shear dolly in
-  let _ = talk dolly in
+  let _ := talk dolly in
+  let _ := shear dolly in
+  let _ := talk dolly in
   returnS? tt.
-  
\ No newline at end of file

From dcfe96455e77f0fb0914f66a7704240d7697e01d Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 22:17:25 +0800
Subject: [PATCH 16/32] Fixed all bugs of `traits.v`

---
 .../ink_contracts/simulations/traits.v        | 21 ++++++++-----------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 3f84b0616..f9e8312b3 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,16 +1,14 @@
 (* traits/traits.rs *)
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
-Require CoqOfRust.core.simulations.option.
-Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+Require Import CoqOfRust.core.simulations.option.
+Require Import CoqOfRust.core.simulations.result.
+Require Import CoqOfRust.core.simulations.integer.
+Require Import CoqOfRust.core.simulations.bool.
 Require Import CoqOfRust.simulations.M.
 
 Import simulations.M.Notations.
-
-(* TODO:
-1. Check (if it's necessary) how to implement `TraitHasRun` for `Animal` and `Sheep`
-2. Check if the `main` function has defined correctly
-*)
+Import simulations.bool.Notations.
 
 (* struct Sheep {
   naked: bool,
@@ -26,14 +24,13 @@ Module Sheep.
     Φ := Ty.path "traits::Sheep";
     φ x :=
       Value.StructRecord "traits::Sheep" [
-      (* TODO: figure out the correct way to fill this *)
-        (* ("naked", φ x.(naked));
-        ("name", φ x.(name)) *)
+        ("naked", Value.Bool x.(naked));
+        ("name", Value.String x.(name))
       ];
   }.
 End Sheep.
 
-(*  ** Simulation of functions ** *)
+(* ** Simulation of functions ** *)
 (* 
 fn new(name: &'static str) -> Sheep {
   Sheep {
@@ -81,7 +78,7 @@ Definition noise (self: traits.Sheep.t) : string :=
 } *)
 Definition talk (self: traits.Sheep.t): unit := tt.
 
-(* ** Simulation of a function that modifies a variable ** *)
+(* ** Simulation of function that modifies a variable ** *)
 
 Module State.
   Definition t : Set := traits.Sheep.t.

From dcfaf13b5cd881d7cd399238fcd1846158978ea0 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 22:35:38 +0800
Subject: [PATCH 17/32] Add initial `erc.1155.v`

---
 .../ink_contracts/simulations/erc1155.v       | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v

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..869f9a46d
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
@@ -0,0 +1,24 @@
+Require Import CoqOfRust.CoqOfRust.
+Require CoqOfRust.core.simulations.default.
+Require Import CoqOfRust.core.simulations.option.
+Require Import CoqOfRust.core.simulations.integer.
+Require Import CoqOfRust.core.simulations.bool.
+Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+Require Import CoqOfRust.simulations.M.
+
+Module AccountId.
+  Inductive t : Set :=
+  | Make (account_id : Z).
+
+  Global Instance IsToValue : ToValue t := {
+    Φ := Ty.path "erc1155::AccountId";
+    φ '(Make x) :=
+      Value.StructTuple "erc1155::AccountId" [Value.Integer Integer.U128 x];
+  }.
+End AccountId.
+
+Module Env.
+  Record t : Set := {
+    caller : AccountId.t;
+  }.
+End Env.
\ No newline at end of file

From 309606be188f6c89d0b1827b73ad783eeee68acf Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 23:50:44 +0800
Subject: [PATCH 18/32] Update erc1155

---
 .../ink_contracts/simulations/erc1155.v       | 140 +++++++++++++++++-
 1 file changed, 137 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
index 869f9a46d..0f4d15fba 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
@@ -6,19 +6,153 @@ 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 x) :=
-      Value.StructTuple "erc1155::AccountId" [Value.Integer Integer.U128 x];
+    φ '(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 IsToValue : ToValue t := {
+    Φ := Ty.path "erc1155::Balance";
+    φ '(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;
   }.
-End Env.
\ No newline at end of file
+
+  (* TODO: fix below code *)
+  Global Instance IsToValue : ToValue t := {
+    Φ := Ty.path "erc1155::Env";
+    φ '(Make x) :=
+      Value.StructTuple "erc1155::Env" φ x;
+  }.
+End Env.
+
+(* TODO *)
+
+(* 
+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 IsToValue : ToValue t := {
+    Φ := Ty.path "erc1155::TokenId";
+    φ '(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.
\ No newline at end of file

From 33cf84ccc1ddb58bde32964a0b3f3cf65b5a58b9 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Sun, 5 May 2024 23:54:00 +0800
Subject: [PATCH 19/32] More updates on `erc1155.v`

---
 .../ink_contracts/simulations/erc1155.v       | 62 ++++++++++++++++++-
 1 file changed, 59 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
index 0f4d15fba..209fb401d 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
@@ -58,7 +58,7 @@ Module Env.
   }.
 End Env.
 
-(* TODO *)
+(* ******** IN PROGRESS ******** *)
 
 (* 
 fn zero_address() -> AccountId {
@@ -123,7 +123,7 @@ Module Result.
   Definition t (T : Set) : Set := core.result.Result T Error.
 End Result.
 
-(* pub trait Erc1155 { *)
+(* pub trait Erc1155 { .. }*)
 Module Erc1155.
   Class Trait (Self : Set) : Set := {
   (* 
@@ -155,4 +155,60 @@ Module Erc1155.
   (* fn is_approved_for_all(&self, owner: AccountId, operator: AccountId) -> bool; *)
 
   }.
-End Erc1155.
\ No newline at end of file
+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),
+} *)

From 89ccad6da4c626b1dccb6a3a82093779a2dfcbfb Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 13 May 2024 14:54:54 +0800
Subject: [PATCH 20/32] Update `traits.v`

---
 .../ink_contracts/simulations/traits.v        | 50 ++++++++++++++++---
 1 file changed, 44 insertions(+), 6 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index f9e8312b3..e5fd6af65 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -7,6 +7,8 @@ Require Import CoqOfRust.core.simulations.integer.
 Require Import CoqOfRust.core.simulations.bool.
 Require Import CoqOfRust.simulations.M.
 
+Require Import CoqOfRust.proofs.M.
+
 Import simulations.M.Notations.
 Import simulations.bool.Notations.
 
@@ -125,14 +127,50 @@ trait Animal {
 
 Module Animal.
   Class Trait (Self : Set) : Set := {
-    new (name: string) : traits.Sheep.t; 
-    name (self: traits.Sheep.t) : string;
-    noise (self: traits.Sheep.t) : string;
-    talk (self: traits.Sheep.t) : unit;
+    new (name: string) : Self;
+    name (self: Self) : string;
+    noise (self: Self) : string;
+    talk (self: Self) : unit;
   }.
 
-  (* TODO: Define the `TraitHasRun` struct to express that `Sheep` implements `Animal` *)
-
+  (* 
+  Error: Unable to satisfy the following constraints:
+  In environment:
+  TraitHasRun : forall Self : Set,
+                ToValue Self -> Trait Self -> Prop
+  Self : Set
+  H : ToValue Self
+  H0 : Trait Self
+  new : list Ty.t -> list Value.t -> M
+
+  ?ToValue : "ToValue (string -> ?Self)"
+
+  ?Trait : "Trait ?Self"
+  *)
+
+  Record TraitHasRun (Self : Set)
+    `{ToValue Self}
+    `{traits.Animal.Trait Self} :
+    Prop := {
+      new : exists new,
+        IsTraitMethod 
+        (* (trait_name : string) *)
+        "traits.Animal.Trait" 
+        (* (self_ty : Ty.t) *)
+        (Φ Self) 
+        (* (trait_tys : list Ty.t) *)
+        [ ] 
+        (* (method_name : string) *)
+        "new" 
+        (* (method : list Ty.t -> list Value.t -> M) *)
+        new
+        /\ 
+        Run.pure 
+          (* (e : M)  *)
+          (new [] []) (* NOTE: What should be the two list here for this function? *)
+          (* (result : Value.t + Exception.t)  *)
+          (inl (φ traits.Animal.new));
+  }.
 End Animal.
 
 (*

From 09fb45552c75558cc786d0e16a79149dca6a3dce Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 13 May 2024 16:13:05 +0800
Subject: [PATCH 21/32] Finished defining `traits.v` for simulation(?)

---
 .../ink_contracts/simulations/traits.v        | 26 ++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index e5fd6af65..83f6f4ec2 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -109,6 +109,15 @@ Definition shear (self: traits.Sheep.t) : MS? State.t string unit :=
   in
   returnS? tt.
 
+(* Misc: Instances for string's ToValue *)
+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.
@@ -152,7 +161,7 @@ Module Animal.
     `{ToValue Self}
     `{traits.Animal.Trait Self} :
     Prop := {
-      new : exists new,
+      new_exists : exists new,
         IsTraitMethod 
         (* (trait_name : string) *)
         "traits.Animal.Trait" 
@@ -170,6 +179,21 @@ Module Animal.
           (new [] []) (* NOTE: What should be the two list here for this function? *)
           (* (result : Value.t + Exception.t)  *)
           (inl (φ traits.Animal.new));
+
+      name_exists : exists name,
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "name" name 
+        /\
+        Run.pure (name [] []) (inl (φ traits.Animal.name));
+
+      noise_exists : exists noise, 
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "noise" noise 
+          /\
+          Run.pure (noise [] []) (inl (φ traits.Animal.noise));
+
+      talk_exists : exists talk,
+        IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 
+        /\
+        Run.pure (talk [] []) (inl (φ traits.Animal.talk));
   }.
 End Animal.
 

From fdff43f0faada66b564cdb1b94ebecc3093696b0 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 13 May 2024 16:16:19 +0800
Subject: [PATCH 22/32] remove comments

---
 .../examples/ink_contracts/simulations/traits.v   | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 83f6f4ec2..0c161f3b1 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -142,21 +142,6 @@ Module Animal.
     talk (self: Self) : unit;
   }.
 
-  (* 
-  Error: Unable to satisfy the following constraints:
-  In environment:
-  TraitHasRun : forall Self : Set,
-                ToValue Self -> Trait Self -> Prop
-  Self : Set
-  H : ToValue Self
-  H0 : Trait Self
-  new : list Ty.t -> list Value.t -> M
-
-  ?ToValue : "ToValue (string -> ?Self)"
-
-  ?Trait : "Trait ?Self"
-  *)
-
   Record TraitHasRun (Self : Set)
     `{ToValue Self}
     `{traits.Animal.Trait Self} :

From 419d9c7596e8b1b0a6c8a39822f8363c45122844 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 13 May 2024 16:17:09 +0800
Subject: [PATCH 23/32] minor fixes

---
 .../default/examples/ink_contracts/simulations/traits.v      | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 0c161f3b1..03150b8fc 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -109,13 +109,10 @@ Definition shear (self: traits.Sheep.t) : MS? State.t string unit :=
   in
   returnS? tt.
 
-(* Misc: Instances for string's ToValue *)
+(* 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.
 
 (*

From 9aa87c444b489d930613c4ac67d6208d3fa271f5 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 13 May 2024 16:23:07 +0800
Subject: [PATCH 24/32] format fix

---
 .../default/examples/ink_contracts/simulations/traits.v       | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 03150b8fc..51bb05310 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -169,8 +169,8 @@ Module Animal.
 
       noise_exists : exists noise, 
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "noise" noise 
-          /\
-          Run.pure (noise [] []) (inl (φ traits.Animal.noise));
+        /\
+        Run.pure (noise [] []) (inl (φ traits.Animal.noise));
 
       talk_exists : exists talk,
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 

From e7c562f5bd24a27514778dfc7db469f922fa8a3d Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 22 May 2024 09:09:12 +0800
Subject: [PATCH 25/32] draft update

---
 .../examples/ink_contracts/proofs/constants.v        | 12 ++++++++++++
 .../default/examples/ink_contracts/proofs/traits.v   | 11 +++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/ink_contracts/proofs/constants.v
 create mode 100644 CoqOfRust/examples/default/examples/ink_contracts/proofs/traits.v

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

From 40c77d71a0302022efcc3422430371fd7d12ff18 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 22 May 2024 11:58:09 +0800
Subject: [PATCH 26/32] snapshot

---
 .../default/examples/ink_contracts/simulations/constants.v   | 4 ++--
 .../default/examples/ink_contracts/simulations/traits.v      | 5 ++++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
index 4128b0aed..4bb779f7f 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -12,8 +12,8 @@ Import simulations.M.Notations.
 static LANGUAGE: &str = "Rust";
 const THRESHOLD: i32 = 10;
 *)
-Definition LANGUAGE := mk_str "Rust".
-Definition THRESHOLD : i32.t := i32.Make 10.
+Definition LANGUAGE : string :=  "Rust".
+Definition THRESHOLD : A := 10.
 
 (* 
 fn is_big(n: i32) -> bool {
diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 51bb05310..032f85a11 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -22,8 +22,11 @@ Module Sheep.
     name: string;
   }.
 
-  Global Instance IsToValue : ToValue t := {
+  Global Instance IsToTy : ToTy t := {
     Φ := Ty.path "traits::Sheep";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
     φ x :=
       Value.StructRecord "traits::Sheep" [
         ("naked", Value.Bool x.(naked));

From ab0ba4a1cd57811a2940ec55aef2b133b0b8e0e7 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 22 May 2024 19:26:02 +0800
Subject: [PATCH 27/32] Update `traits.v`

---
 .../default/examples/ink_contracts/simulations/traits.v  | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 032f85a11..6311d69af 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -1,9 +1,9 @@
 (* traits/traits.rs *)
+(* TODO: Move this file to a separate location from ink contracts *)
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
 Require Import CoqOfRust.core.simulations.option.
 Require Import CoqOfRust.core.simulations.result.
-Require Import CoqOfRust.core.simulations.integer.
 Require Import CoqOfRust.core.simulations.bool.
 Require Import CoqOfRust.simulations.M.
 
@@ -112,6 +112,9 @@ Definition shear (self: traits.Sheep.t) : MS? State.t string unit :=
   in
   returnS? tt.
 
+(* ToTy Instances *)
+(* TODO: Finish them *)
+
 (* Missing ToValue instances to define TraitHasRun *)
 Global Instance IsToValue_string : ToValue string. Admitted.
 Global Instance IsToValue_string_self {Self : Set} : ToValue (string -> Self). Admitted.
@@ -142,7 +145,7 @@ Module Animal.
     talk (self: Self) : unit;
   }.
 
-  Record TraitHasRun (Self : Set)
+  (* Record TraitHasRun (Self : Set)
     `{ToValue Self}
     `{traits.Animal.Trait Self} :
     Prop := {
@@ -179,7 +182,7 @@ Module Animal.
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 
         /\
         Run.pure (talk [] []) (inl (φ traits.Animal.talk));
-  }.
+  }. *)
 End Animal.
 
 (*

From c32c5fbe118e74a1e493a63dbfa974d39f27b634 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 22 May 2024 20:41:00 +0800
Subject: [PATCH 28/32] Fix `traits.v`

---
 .../examples/ink_contracts/simulations/traits.v       | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
index 6311d69af..34f6a5835 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
@@ -113,7 +113,11 @@ Definition shear (self: traits.Sheep.t) : MS? State.t string unit :=
   returnS? tt.
 
 (* ToTy Instances *)
-(* TODO: Finish them *)
+
+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.
@@ -145,8 +149,9 @@ Module Animal.
     talk (self: Self) : unit;
   }.
 
-  (* Record TraitHasRun (Self : Set)
+  Record TraitHasRun (Self : Set)
     `{ToValue Self}
+    `{ToTy Self}
     `{traits.Animal.Trait Self} :
     Prop := {
       new_exists : exists new,
@@ -182,7 +187,7 @@ Module Animal.
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 
         /\
         Run.pure (talk [] []) (inl (φ traits.Animal.talk));
-  }. *)
+  }.
 End Animal.
 
 (*

From 57b1481d81d32e12c53cf96ba6de567e4b9f5287 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Thu, 23 May 2024 14:51:19 +0800
Subject: [PATCH 29/32] Update `constants.v`

---
 .../examples/ink_contracts/simulations/constants.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
index 4bb779f7f..c0fafc798 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
@@ -2,9 +2,9 @@
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
 Require CoqOfRust.core.simulations.option.
-Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
+(* Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib. *)
 Require Import CoqOfRust.simulations.M.
-Require Import CoqOfRust.lib.simulations.lib.
+(* Require Import CoqOfRust.lib.simulations.lib. *)
 
 Import simulations.M.Notations.
 
@@ -13,7 +13,7 @@ static LANGUAGE: &str = "Rust";
 const THRESHOLD: i32 = 10;
 *)
 Definition LANGUAGE : string :=  "Rust".
-Definition THRESHOLD : A := 10.
+Definition THRESHOLD : Z := 10.
 
 (* 
 fn is_big(n: i32) -> bool {
@@ -23,9 +23,9 @@ fn is_big(n: i32) -> bool {
 *)
 
 Definition is_big 
-  (n: i32.t) : bool := 
-  let get_n := i32.get n in
-  let get_THRESHOLD := i32.get THRESHOLD in
+  (n: Z) : bool := 
+  let get_n := n in
+  let get_THRESHOLD := THRESHOLD in
   get_n >? get_THRESHOLD.
 
 (*
@@ -34,5 +34,5 @@ fn main() {
 } *)
 
 Definition main : unit :=
-  let n := i32.Make 16 in
+  let n := 16 in
   tt.

From 315d42b13c38ea9fb31a96eedbc6508d15810ebf Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 27 May 2024 13:10:14 +0800
Subject: [PATCH 30/32] Update `erc1155.v`

---
 .../ink_contracts/simulations/erc1155.v         | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
index 209fb401d..21d785ae8 100644
--- a/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
+++ b/CoqOfRust/examples/default/examples/ink_contracts/simulations/erc1155.v
@@ -1,7 +1,6 @@
 Require Import CoqOfRust.CoqOfRust.
 Require CoqOfRust.core.simulations.default.
 Require Import CoqOfRust.core.simulations.option.
-Require Import CoqOfRust.core.simulations.integer.
 Require Import CoqOfRust.core.simulations.bool.
 Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib.
 Require Import CoqOfRust.simulations.M.
@@ -32,8 +31,11 @@ Module Balance.
   Inductive t : Set :=
   | Make (balance : Z).
 
-  Global Instance IsToValue : ToValue t := {
+  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];
   }.
@@ -50,9 +52,11 @@ Module Env.
     caller : AccountId.t;
   }.
 
-  (* TODO: fix below code *)
-  Global Instance IsToValue : ToValue t := {
+  Global Instance IsToTy : ToTy t := {
     Φ := Ty.path "erc1155::Env";
+  }.
+
+  Global Instance IsToValue : ToValue t := {
     φ '(Make x) :=
       Value.StructTuple "erc1155::Env" φ x;
   }.
@@ -79,8 +83,11 @@ Module TokenId.
   Inductive t : Set :=
   | Make (token_id : Z).
 
-  Global Instance IsToValue : ToValue t := {
+  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];
   }.

From 29671f548cf7b802bc59f396f6e773ebcd688931 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Tue, 28 May 2024 17:11:37 +0800
Subject: [PATCH 31/32] Fix file location after merging main

---
 .../default/examples/{ink_contracts => }/simulations/constants.v  | 0
 .../default/examples/{ink_contracts => }/simulations/traits.v     | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename CoqOfRust/examples/default/examples/{ink_contracts => }/simulations/constants.v (100%)
 rename CoqOfRust/examples/default/examples/{ink_contracts => }/simulations/traits.v (100%)

diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v b/CoqOfRust/examples/default/examples/simulations/constants.v
similarity index 100%
rename from CoqOfRust/examples/default/examples/ink_contracts/simulations/constants.v
rename to CoqOfRust/examples/default/examples/simulations/constants.v
diff --git a/CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v b/CoqOfRust/examples/default/examples/simulations/traits.v
similarity index 100%
rename from CoqOfRust/examples/default/examples/ink_contracts/simulations/traits.v
rename to CoqOfRust/examples/default/examples/simulations/traits.v

From 9897d2658e9b4828b643d4c67ef60e91aee7c42f Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Tue, 28 May 2024 17:25:03 +0800
Subject: [PATCH 32/32] Update according to main & delete redundant deps

---
 .../default/examples/simulations/constants.v  |  5 --
 .../default/examples/simulations/traits.v     | 60 +++++++------------
 2 files changed, 20 insertions(+), 45 deletions(-)

diff --git a/CoqOfRust/examples/default/examples/simulations/constants.v b/CoqOfRust/examples/default/examples/simulations/constants.v
index c0fafc798..dbac65e60 100644
--- a/CoqOfRust/examples/default/examples/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/simulations/constants.v
@@ -1,11 +1,6 @@
 (* custom_type/constants.v *)
 Require Import CoqOfRust.CoqOfRust.
-Require CoqOfRust.core.simulations.default.
-Require CoqOfRust.core.simulations.option.
-(* Require CoqOfRust.examples.default.examples.ink_contracts.simulations.lib. *)
 Require Import CoqOfRust.simulations.M.
-(* Require Import CoqOfRust.lib.simulations.lib. *)
-
 Import simulations.M.Notations.
 
 (*
diff --git a/CoqOfRust/examples/default/examples/simulations/traits.v b/CoqOfRust/examples/default/examples/simulations/traits.v
index 34f6a5835..4b9c48ea2 100644
--- a/CoqOfRust/examples/default/examples/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/simulations/traits.v
@@ -1,14 +1,8 @@
 (* traits/traits.rs *)
-(* TODO: Move this file to a separate location from ink contracts *)
 Require Import CoqOfRust.CoqOfRust.
-Require CoqOfRust.core.simulations.default.
-Require Import CoqOfRust.core.simulations.option.
-Require Import CoqOfRust.core.simulations.result.
 Require Import CoqOfRust.core.simulations.bool.
 Require Import CoqOfRust.simulations.M.
-
 Require Import CoqOfRust.proofs.M.
-
 Import simulations.M.Notations.
 Import simulations.bool.Notations.
 
@@ -149,45 +143,31 @@ Module Animal.
     talk (self: Self) : unit;
   }.
 
-  Record TraitHasRun (Self : Set)
+  Record InstanceWithRun (Self : Set)
     `{ToValue Self}
     `{ToTy Self}
-    `{traits.Animal.Trait Self} :
-    Prop := {
-      new_exists : exists new,
-        IsTraitMethod 
-        (* (trait_name : string) *)
-        "traits.Animal.Trait" 
-        (* (self_ty : Ty.t) *)
-        (Φ Self) 
-        (* (trait_tys : list Ty.t) *)
-        [ ] 
-        (* (method_name : string) *)
-        "new" 
-        (* (method : list Ty.t -> list Value.t -> M) *)
-        new
-        /\ 
-        Run.pure 
-          (* (e : M)  *)
-          (new [] []) (* NOTE: What should be the two list here for this function? *)
-          (* (result : Value.t + Exception.t)  *)
-          (inl (φ traits.Animal.new));
-
-      name_exists : exists name,
+    `{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 [] []) (inl (φ traits.Animal.name));
-
-      noise_exists : exists noise, 
+        *
+        Run.pure (name [] []) (fun v => inl (φ v))
+      };
+      noise_exists : {noise @
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "noise" noise 
-        /\
-        Run.pure (noise [] []) (inl (φ traits.Animal.noise));
-
-      talk_exists : exists talk,
+        *
+        Run.pure (noise [] []) (fun v => inl (φ v))
+      };
+      talk_exists : {talk @
         IsTraitMethod "traits.Animal.Trait" (Φ Self) [ ] "talk" talk 
-        /\
-        Run.pure (talk [] []) (inl (φ traits.Animal.talk));
-  }.
+        *
+        Run.pure (talk [] []) (fun v => inl (φ v))
+      };
+    }.
 End Animal.
 
 (*