From 5addecad494a248ad518898c77290813e504faf9 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Mon, 27 May 2024 23:49:24 +0800
Subject: [PATCH 1/3] Add example simulations

---
 .../default/examples/simulations/constants.v  |  36 +++
 .../default/examples/simulations/traits.v     | 209 ++++++++++++++++++
 2 files changed, 245 insertions(+)
 create mode 100644 CoqOfRust/examples/default/examples/simulations/constants.v
 create mode 100644 CoqOfRust/examples/default/examples/simulations/traits.v

diff --git a/CoqOfRust/examples/default/examples/simulations/constants.v b/CoqOfRust/examples/default/examples/simulations/constants.v
new file mode 100644
index 000000000..76c461009
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/simulations/constants.v
@@ -0,0 +1,36 @@
+(* custom_type/constants.v *)
+Require Import CoqOfRust.CoqOfRust.
+Require CoqOfRust.core.simulations.default.
+Require CoqOfRust.core.simulations.option.
+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..68cf7113f
--- /dev/null
+++ b/CoqOfRust/examples/default/examples/simulations/traits.v
@@ -0,0 +1,209 @@
+(* 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.
+
+(* 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 TraitHasRun (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,
+        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.
+
+(*
+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.

From 71430fa953fe692b5a2e7f1c9dee407913320c38 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Tue, 28 May 2024 02:18:23 +0800
Subject: [PATCH 2/3] remove comment

---
 CoqOfRust/examples/default/examples/simulations/traits.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CoqOfRust/examples/default/examples/simulations/traits.v b/CoqOfRust/examples/default/examples/simulations/traits.v
index 68cf7113f..a3d1b04ed 100644
--- a/CoqOfRust/examples/default/examples/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/simulations/traits.v
@@ -1,5 +1,4 @@
 (* 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.

From 3db5d18a8318ee61954c0a20c0e6cca3e2678e80 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Tue, 28 May 2024 17:31:54 +0800
Subject: [PATCH 3/3] Update according to newest main

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

diff --git a/CoqOfRust/examples/default/examples/simulations/constants.v b/CoqOfRust/examples/default/examples/simulations/constants.v
index 76c461009..dbac65e60 100644
--- a/CoqOfRust/examples/default/examples/simulations/constants.v
+++ b/CoqOfRust/examples/default/examples/simulations/constants.v
@@ -1,9 +1,6 @@
 (* custom_type/constants.v *)
 Require Import CoqOfRust.CoqOfRust.
-Require CoqOfRust.core.simulations.default.
-Require CoqOfRust.core.simulations.option.
 Require Import CoqOfRust.simulations.M.
-
 Import simulations.M.Notations.
 
 (*
diff --git a/CoqOfRust/examples/default/examples/simulations/traits.v b/CoqOfRust/examples/default/examples/simulations/traits.v
index a3d1b04ed..4b9c48ea2 100644
--- a/CoqOfRust/examples/default/examples/simulations/traits.v
+++ b/CoqOfRust/examples/default/examples/simulations/traits.v
@@ -1,13 +1,8 @@
 (* traits/traits.rs *)
 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.
 
@@ -112,6 +107,7 @@ Definition shear (self: traits.Sheep.t) : MS? State.t string unit :=
   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.
@@ -147,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.
 
 (*