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>

1 files changed, 75 insertions, 0 deletions

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
+}