Support for renaming using the rename attribute in charon (#239)

* support for renaming using the rename attribute in charon

* support for global decl

* add support for renaming field

* applied suggested changes and began adding support for variant

* finished support for renaming variant

* applied suggested changes

* add tests

* fixed variant and field renaming

* update charon-pin

* update flake.lock

* Update the charon pin

* Fix an issue with renaming trait method implementations

* Fix an issue with the renaming of trait implementations

* Fix an issue when renaming enumerations

* Update the Charon pin

* Fix the F* tests

* Fix an issue with the spans for the loops

* Fix the tests

* Update a comment

* Use fuel in the coq tests

* Generate the template decreases clauses by default

---------

Co-authored-by: Escherichia <escherichia@charlotte>
Co-authored-by: Son Ho <hosonmarc@gmail.com>

7 files changed, 81 insertions, 6 deletions

diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs
index ddad2ad3..3d5b0e81 100644
--- a/tests/src/arrays.rs
+++ b/tests/src/arrays.rs
@@ -1,5 +1,5 @@
 //@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-decreases-clauses
 //@ [fstar] aeneas-args=-split-files
 //! Exercise the translation of arrays, with features supported by Eurydice
 
diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options
index 5a1e4180..c59ada7a 100644
--- a/tests/src/betree/aeneas-test-options
+++ b/tests/src/betree/aeneas-test-options
@@ -1,4 +1,4 @@
 charon-args=--polonius --opaque=betree_utils
 [!borrow-check] aeneas-args=-backward-no-state-update -test-trans-units -state -split-files
 [coq] aeneas-args=-use-fuel
-[fstar] aeneas-args=-decreases-clauses -template-clauses
+[fstar] aeneas-args=-decreases-clauses
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
index 9ff448db..12a95d0f 100644
--- a/tests/src/hashmap.rs
+++ b/tests/src/hashmap.rs
@@ -1,7 +1,7 @@
 //@ charon-args=--opaque=utils
 //@ [!borrow-check] aeneas-args=-state -split-files
 //@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-decreases-clauses
 //@ [lean] aeneas-args=-no-gen-lib-entry
 // ^ the `-no-gen-lib-entry` is because we add a custom import in the Hashmap.lean file: we do not
 // want to overwrite it.
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
index afc52ace..8a558b9d 100644
--- a/tests/src/loops.rs
+++ b/tests/src/loops.rs
@@ -1,5 +1,5 @@
 //@ [coq] aeneas-args=-use-fuel
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-decreases-clauses
 //@ [fstar] aeneas-args=-split-files
 //@ [coq,fstar] subdir=misc
 use std::vec::Vec;
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index d4ca5af3..dffbb470 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -14,4 +14,4 @@ Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
 Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36
 Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42
-Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66
+Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66
diff --git a/tests/src/rename_attribute.rs b/tests/src/rename_attribute.rs
new file mode 100644
index 00000000..78765817
--- /dev/null
+++ b/tests/src/rename_attribute.rs
@@ -0,0 +1,75 @@
+//@ [fstar] aeneas-args=-decreases-clauses -split-files
+//@ [coq] aeneas-args=-use-fuel
+#![feature(register_tool)]
+#![register_tool(charon)]
+#![register_tool(aeneas)]
+
+#[charon::rename("BoolTest")]
+pub trait BoolTrait {
+    // Required method
+    #[charon::rename("getTest")]
+    fn get_bool(&self) -> bool;
+
+    // Provided method
+    #[charon::rename("retTest")]
+    fn ret_true(&self) -> bool {
+        true
+    }
+}
+
+#[charon::rename("BoolImpl")]
+impl BoolTrait for bool {
+    fn get_bool(&self) -> bool {
+        *self
+    }
+}
+
+#[charon::rename("BoolFn")]
+pub fn test_bool_trait<T>(x: bool) -> bool {
+    x.get_bool() && x.ret_true()
+}
+
+#[charon::rename("TypeTest")]
+type Test = i32;
+
+#[charon::rename("VariantsTest")]
+enum SimpleEnum {
+    #[charon::rename("Variant1")]
+    FirstVariant,
+    SecondVariant,
+    ThirdVariant,
+}
+
+#[charon::rename("StructTest")]
+struct Foo {
+    #[charon::rename("FieldTest")]
+    field1: u32,
+}
+
+#[charon::rename("Const_Test")]
+const C: u32 = 100 + 10 + 1;
+
+#[aeneas::rename("Const_Aeneas11")]
+const CA: u32 = 10 + 1;
+
+#[charon::rename("Factfn")]
+fn factorial(n: u64) -> u64 {
+    if n <= 1 {
+        1
+    } else {
+        return n * factorial(n - 1);
+    }
+}
+
+#[charon::rename("No_borrows_sum")]
+pub fn sum(max: u32) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < max {
+        s += i;
+        i += 1;
+    }
+
+    s *= 2;
+    s
+}
diff --git a/tests/src/traits.rs b/tests/src/traits.rs
index fd50db8c..36389cdf 100644
--- a/tests/src/traits.rs
+++ b/tests/src/traits.rs
@@ -1,4 +1,4 @@
-//@ [fstar] aeneas-args=-decreases-clauses -template-clauses
+//@ [fstar] aeneas-args=-decreases-clauses
 pub trait BoolTrait {
     // Required method
     fn get_bool(&self) -> bool;